Theorem: pt_of_line_ne_pt (Pythagoras/euclid_I_extras.lean)

State before:
i : incidence_geometry
a : point
L : line
⊢ ∃ b, b ≠ a ∧ online b L
Tactic:
obtain ⟨ b, c, Hbc ⟩ := online_ne_of_line L
State after:
case intro.intro
i : incidence_geometry
a : point
L : line
b c : point
Hbc : b ≠ c ∧ online b L ∧ online c L
⊢ ∃ b, b ≠ a ∧ online b L

State before:
case intro.intro
i : incidence_geometry
a : point
L : line
b c : point
Hbc : b ≠ c ∧ online b L ∧ online c L
⊢ ∃ b, b ≠ a ∧ online b L
Tactic:
by_cases b = a
State after:
case pos
i : incidence_geometry
a : point
L : line
b c : point
Hbc : b ≠ c ∧ online b L ∧ online c L
h : b = a
⊢ ∃ b, b ≠ a ∧ online b L

case neg
i : incidence_geometry
a : point
L : line
b c : point
Hbc : b ≠ c ∧ online b L ∧ online c L
h : ¬b = a
⊢ ∃ b, b ≠ a ∧ online b L

State before:
case pos
i : incidence_geometry
a : point
L : line
b c : point
Hbc : b ≠ c ∧ online b L ∧ online c L
h : b = a
⊢ ∃ b, b ≠ a ∧ online b L
Tactic:
simp_rw [h] at Hbc
State after:
case pos
i : incidence_geometry
a : point
L : line
b c : point
h : b = a
Hbc : a ≠ c ∧ online a L ∧ online c L
⊢ ∃ b, b ≠ a ∧ online b L

State before:
case pos
i : incidence_geometry
a : point
L : line
b c : point
h : b = a
Hbc : a ≠ c ∧ online a L ∧ online c L
⊢ ∃ b, b ≠ a ∧ online b L
Tactic:
exact ⟨c, Hbc.1.symm, Hbc.2.2 ⟩
State after:
no goals

State before:
case neg
i : incidence_geometry
a : point
L : line
b c : point
Hbc : b ≠ c ∧ online b L ∧ online c L
h : ¬b = a
⊢ ∃ b, b ≠ a ∧ online b L
Tactic:
exact ⟨ b, h, Hbc.2.1 ⟩
State after:
no goals