# Zulip Chat Archive

## Stream: new members

### Topic: MohanadAhmed

#### MohanadAhmed (May 14 2022 at 14:06):

Hello everyone

New one here.

Just started learning lean. Hoping this would be fun.

Went through tutorials at https://github.com/leanprover-community/tutorials

And then though I would start with school geometry like showing that angles of equilateral triangle are all pi/3

Any comments are welcome.

(Not sure how to post code directly so attaching it)

Thanks and looking forward to learning.

#### Patrick Johnson (May 14 2022 at 14:17):

See #backticks to learn how to post code directly.

#### MohanadAhmed (May 14 2022 at 14:34):

```
lemma equi_triangle_pi_3 {p1 p2 p3 : P}
(h1 : dist p1 p2 = dist p1 p3) (h2: dist p2 p1 = dist p2 p3)
(ha : p2 ≠ p1) (hb : p3 ≠ p1) :
∠ p1 p2 p3 = (π / 3) ∧ ∠ p1 p3 p2 = π / 3 ∧ ∠ p2 p1 p3 = π / 3 :=
begin
have eq12 : ∠ p1 p2 p3 = ∠ p1 p3 p2 ∧ ∠ p2 p1 p3 = ∠ p2 p3 p1,
{apply equi_triangle h1 h2},
cases eq12 with eq1 eq2,
have eqx : ∠ p1 p3 p2 = ∠ p2 p3 p1,
{apply euclidean_geometry.angle_comm},
have eqy : ∠ p3 p1 p2 = ∠ p2 p1 p3,
{apply euclidean_geometry.angle_comm},
have eqπ : ∠ p1 p2 p3 + ∠ p2 p3 p1 + ∠ p3 p1 p2 = π,
{apply euclidean_geometry.angle_add_angle_add_angle_eq_pi ha hb},
rw eq1 at eqπ,
rw eqx at eqπ,
rw eqy at eqπ,
rw eq2 at eqπ,
have xp3: ∠ p2 p3 p1 = π / 3, {by linarith},
rw xp3 at eq2,
rw ← eqx at xp3,
rw xp3 at eq1,
split, {linarith}, {split, {linarith}, {linarith}},
end
```

#### MohanadAhmed (May 14 2022 at 14:35):

Thanks a lot @Patrick Johnson

#### Julian Berman (May 14 2022 at 14:59):

Welcome! I'm sure one can do even better, but angle brackets are cool, and the tactic#rintro and tactic#rcases tactics are nice.

#### Patrick Johnson (May 14 2022 at 15:38):

You can use semicolons to reduce duplication. Semicolon applies the tactic on the right to all goals produces by the tactic on the left. For example

```
split,
{ apply euclidean_geometry.angle_eq_angle_of_dist_eq h1 },
{ apply euclidean_geometry.angle_eq_angle_of_dist_eq h2 },
```

becomes:

```
split; apply euclidean_geometry.angle_eq_angle_of_dist_eq; assumption,
```

tactic#assumption closes the goal using an appropriate assumption. Also note that

```
split, {linarith}, {split, {linarith}, {linarith}},
```

can be simplified to

```
refine ⟨_, _, _⟩; linarith,
```

Tactic `linarith`

takes an optional list of assumptions as argument, so you don't need so much `have`

statements and you don't even need `equi_triangle`

lemma. Here is a simplified proof:

```
import geometry.euclidean.triangle
open euclidean_geometry
open_locale euclidean_geometry
open_locale real
lemma equi_triangle_pi_3 {V P : Type*}
[inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P]
{p1 p2 p3 : P}
(h1 : dist p1 p2 = dist p1 p3) (h2: dist p2 p1 = dist p2 p3)
(ha : p2 ≠ p1) (hb : p3 ≠ p1) :
∠ p1 p2 p3 = π / 3 ∧ ∠ p1 p3 p2 = π / 3 ∧ ∠ p2 p1 p3 = π / 3 :=
begin
refine ⟨_, _, _⟩; linarith
[ angle_comm p1 p3 p2,
angle_comm p3 p1 p2,
angle_eq_angle_of_dist_eq h1,
angle_eq_angle_of_dist_eq h2,
angle_add_angle_add_angle_eq_pi ha hb ],
end
```

Last updated: Dec 20 2023 at 11:08 UTC