Theorem: aux (Pythagoras/pythagoras_2.lean)

State before:
i : incidence_geometry
a b c : point
Tabc : ¬colinear a b c
ang_a : rightangle ≤ angle b a c
⊢ ∃ d, B b d c ∧ angle b d a = rightangle ∧ angle c d a = rightangle
Tactic:
obtain ⟨_, bL, cL⟩ := line_of_pts b c
State after:
case intro.intro
i : incidence_geometry
a b c : point
Tabc : ¬colinear a b c
ang_a : rightangle ≤ angle b a c
w✝ : line
bL : online b w✝
cL : online c w✝
⊢ ∃ d, B b d c ∧ angle b d a = rightangle ∧ angle c d a = rightangle

State before:
case intro.intro
i : incidence_geometry
a b c : point
Tabc : ¬colinear a b c
ang_a : rightangle ≤ angle b a c
w✝ : line
bL : online b w✝
cL : online c w✝
⊢ ∃ d, B b d c ∧ angle b d a = rightangle ∧ angle c d a = rightangle
Tactic:
have aL := online_1_of_triangle bL cL Tabc
State after:
case intro.intro
i : incidence_geometry
a b c : point
Tabc : ¬colinear a b c
ang_a : rightangle ≤ angle b a c
w✝ : line
bL : online b w✝
cL : online c w✝
aL : ¬online a w✝
⊢ ∃ d, B b d c ∧ angle b d a = rightangle ∧ angle c d a = rightangle

State before:
case intro.intro
i : incidence_geometry
a b c : point
Tabc : ¬colinear a b c
ang_a : rightangle ≤ angle b a c
w✝ : line
bL : online b w✝
cL : online c w✝
aL : ¬online a w✝
⊢ ∃ d, B b d c ∧ angle b d a = rightangle ∧ angle c d a = rightangle
Tactic:
obtain ⟨d, adc, adb, Bcdb⟩ := pythlem (ne_23_of_tri Tabc).symm cL bL aL ang_a
State after:
case intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
Tabc : ¬colinear a b c
ang_a : rightangle ≤ angle b a c
w✝ : line
bL : online b w✝
cL : online c w✝
aL : ¬online a w✝
d : point
adc : angle a d c = rightangle
adb : angle a d b = rightangle
Bcdb : B c d b
⊢ ∃ d, B b d c ∧ angle b d a = rightangle ∧ angle c d a = rightangle

State before:
case intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
Tabc : ¬colinear a b c
ang_a : rightangle ≤ angle b a c
w✝ : line
bL : online b w✝
cL : online c w✝
aL : ¬online a w✝
d : point
adc : angle a d c = rightangle
adb : angle a d b = rightangle
Bcdb : B c d b
⊢ ∃ d, B b d c ∧ angle b d a = rightangle ∧ angle c d a = rightangle
Tactic:
exact ⟨d, B_symm Bcdb, (by perma), (by perma)⟩
State after:
no goals

State before:
i : incidence_geometry
a b c : point
Tabc : ¬colinear a b c
ang_a : rightangle ≤ angle b a c
w✝ : line
bL : online b w✝
cL : online c w✝
aL : ¬online a w✝
d : point
adc : angle a d c = rightangle
adb : angle a d b = rightangle
Bcdb : B c d b
⊢ angle b d a = rightangle
Tactic:
perma
State after:
no goals

State before:
i : incidence_geometry
a b c : point
Tabc : ¬colinear a b c
ang_a : rightangle ≤ angle b a c
w✝ : line
bL : online b w✝
cL : online c w✝
aL : ¬online a w✝
d : point
adc : angle a d c = rightangle
adb : angle a d b = rightangle
Bcdb : B c d b
⊢ angle c d a = rightangle
Tactic:
perma
State after:
no goals