Theorem: perpendicular_of_online'' (Pythagoras/pythagoras_2.lean)

State before:
i : incidence_geometry
a b : point
L : line
f : point
ab : a ≠ b
aL : online a L
bL : online b L
fL : ¬online f L
⊢ ∃ c, diffside c f L ∧ angle a b c = rightangle
Tactic:
rcases length_eq_B_of_ne ab ab.symm with ⟨d, Babd, _⟩
State after:
case intro.intro
i : incidence_geometry
a b : point
L : line
f : point
ab : a ≠ b
aL : online a L
bL : online b L
fL : ¬online f L
d : point
Babd : B a b d
right✝ : length b a = length b d
⊢ ∃ c, diffside c f L ∧ angle a b c = rightangle

State before:
case intro.intro
i : incidence_geometry
a b : point
L : line
f : point
ab : a ≠ b
aL : online a L
bL : online b L
fL : ¬online f L
d : point
Babd : B a b d
right✝ : length b a = length b d
⊢ ∃ c, diffside c f L ∧ angle a b c = rightangle
Tactic:
rcases diffside_of_not_online fL with ⟨f', f'L, ff'L⟩
State after:
case intro.intro.intro.intro
i : incidence_geometry
a b : point
L : line
f : point
ab : a ≠ b
aL : online a L
bL : online b L
fL : ¬online f L
d : point
Babd : B a b d
right✝ : length b a = length b d
f' : point
f'L : ¬online f' L
ff'L : ¬sameside f f' L
⊢ ∃ c, diffside c f L ∧ angle a b c = rightangle

State before:
case intro.intro.intro.intro
i : incidence_geometry
a b : point
L : line
f : point
ab : a ≠ b
aL : online a L
bL : online b L
fL : ¬online f L
d : point
Babd : B a b d
right✝ : length b a = length b d
f' : point
f'L : ¬online f' L
ff'L : ¬sameside f f' L
⊢ ∃ c, diffside c f L ∧ angle a b c = rightangle
Tactic:
rcases perpendicular_of_online Babd aL bL f'L with ⟨c, cf'L, right, _⟩
State after:
case intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b : point
L : line
f : point
ab : a ≠ b
aL : online a L
bL : online b L
fL : ¬online f L
d : point
Babd : B a b d
right✝¹ : length b a = length b d
f' : point
f'L : ¬online f' L
ff'L : ¬sameside f f' L
c : point
cf'L : sameside c f' L
right : angle c b a = rightangle
right✝ : angle c b d = rightangle
⊢ ∃ c, diffside c f L ∧ angle a b c = rightangle

State before:
case intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b : point
L : line
f : point
ab : a ≠ b
aL : online a L
bL : online b L
fL : ¬online f L
d : point
Babd : B a b d
right✝¹ : length b a = length b d
f' : point
f'L : ¬online f' L
ff'L : ¬sameside f f' L
c : point
cf'L : sameside c f' L
right : angle c b a = rightangle
right✝ : angle c b d = rightangle
⊢ ∃ c, diffside c f L ∧ angle a b c = rightangle
Tactic:
exact ⟨c, diffside_of_sameside_diffside (sameside_symm cf'L) ⟨f'L, fL, not_sameside_symm ff'L⟩ , by perma[right]⟩
State after:
no goals

State before:
i : incidence_geometry
a b : point
L : line
f : point
ab : a ≠ b
aL : online a L
bL : online b L
fL : ¬online f L
d : point
Babd : B a b d
right✝¹ : length b a = length b d
f' : point
f'L : ¬online f' L
ff'L : ¬sameside f f' L
c : point
cf'L : sameside c f' L
right : angle c b a = rightangle
right✝ : angle c b d = rightangle
⊢ angle a b c = rightangle
Tactic:
perma[right]
State after:
no goals