Theorem: aux2 (Pythagoras/pythagoras_2.lean)

State before:
i : incidence_geometry
a b c : point
Tabc : triangle a b c
⊢ length b a ≠ 0 ∧ length c a ≠ 0 ∧ length b c ≠ 0 ∧ length c b ≠ 0
Tactic:
have ba := length_eq_zero_iff.not.mpr $ ne_21_of_tri Tabc
State after:
i : incidence_geometry
a b c : point
Tabc : triangle a b c
ba : ¬length b a = 0
⊢ length b a ≠ 0 ∧ length c a ≠ 0 ∧ length b c ≠ 0 ∧ length c b ≠ 0

State before:
i : incidence_geometry
a b c : point
Tabc : triangle a b c
ba : ¬length b a = 0
⊢ length b a ≠ 0 ∧ length c a ≠ 0 ∧ length b c ≠ 0 ∧ length c b ≠ 0
Tactic:
have ca := length_eq_zero_iff.not.mpr $ ne_31_of_tri Tabc
State after:
i : incidence_geometry
a b c : point
Tabc : triangle a b c
ba : ¬length b a = 0
ca : ¬length c a = 0
⊢ length b a ≠ 0 ∧ length c a ≠ 0 ∧ length b c ≠ 0 ∧ length c b ≠ 0

State before:
i : incidence_geometry
a b c : point
Tabc : triangle a b c
ba : ¬length b a = 0
ca : ¬length c a = 0
⊢ length b a ≠ 0 ∧ length c a ≠ 0 ∧ length b c ≠ 0 ∧ length c b ≠ 0
Tactic:
have bc := length_eq_zero_iff.not.mpr $ ne_23_of_tri Tabc
State after:
i : incidence_geometry
a b c : point
Tabc : triangle a b c
ba : ¬length b a = 0
ca : ¬length c a = 0
bc : ¬length b c = 0
⊢ length b a ≠ 0 ∧ length c a ≠ 0 ∧ length b c ≠ 0 ∧ length c b ≠ 0

State before:
i : incidence_geometry
a b c : point
Tabc : triangle a b c
ba : ¬length b a = 0
ca : ¬length c a = 0
bc : ¬length b c = 0
⊢ length b a ≠ 0 ∧ length c a ≠ 0 ∧ length b c ≠ 0 ∧ length c b ≠ 0
Tactic:
have cb := fun h => bc ((length_symm b c).trans h)
State after:
i : incidence_geometry
a b c : point
Tabc : triangle a b c
ba : ¬length b a = 0
ca : ¬length c a = 0
bc : ¬length b c = 0
cb : length c b = 0 → False
⊢ length b a ≠ 0 ∧ length c a ≠ 0 ∧ length b c ≠ 0 ∧ length c b ≠ 0

State before:
i : incidence_geometry
a b c : point
Tabc : triangle a b c
ba : ¬length b a = 0
ca : ¬length c a = 0
bc : ¬length b c = 0
cb : length c b = 0 → False
⊢ length b a ≠ 0 ∧ length c a ≠ 0 ∧ length b c ≠ 0 ∧ length c b ≠ 0
Tactic:
exact ⟨ ba, ca, bc, cb ⟩
State after:
no goals