## Stream: new members

#### 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

(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 = π,
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,