Theorem: para_trans
Proof state before:
case neg
i : incidence_geometry
L M N : line
pLM : para L M
pLN : para L N
MN : ¬M = N
npMN : ¬M = N ∧ ¬para M N
c : point
cM : online c M
cN : online c N
cL : ¬online c L
d : point
dL : online d L
O : line
cO : online c O
dO : online d O
cd : c ≠ d
LO : L ≠ O
α : circle
Hα : center_circle c α ∧ on_circle d α
cα : in_circle c α
αM : line_circle_inter M α
αN : line_circle_inter N α
a a' : point
aa' : a ≠ a'
aM : online a M
a'M : online a' M
aα : on_circle a α ∧ on_circle a' α
b' b : point
bb' : b' ≠ b
b'N : online b' N
bN : online b N
bα : on_circle b' α ∧ on_circle b α
Baca' : B a c a'
Bbcb' : B b' c b
ac : a ≠ c
b'c : b' ≠ c
bc : b ≠ c
aO : ¬online a O
b'O : ¬online b' O
bO : ¬online b O
aN : ¬online a N
b'M : ¬online b' M
bM : ¬online b M
NO : N ≠ O
MO : M ≠ O
ssbaO : ¬sameside b' a O
nsbb'O : ¬sameside b' b O
ssabO : sameside a b O
⊢ False

case pos
i : incidence_geometry
L M N : line
pLM : para L M
pLN : para L N
MN : ¬M = N
npMN : ¬M = N ∧ ¬para M N
c : point
cM : online c M
cN : online c N
cL : ¬online c L
d : point
dL : online d L
O : line
cO : online c O
dO : online d O
cd : c ≠ d
LO : L ≠ O
α : circle
Hα : center_circle c α ∧ on_circle d α
cα : in_circle c α
αM : line_circle_inter M α
αN : line_circle_inter N α
a a' : point
aa' : a ≠ a'
aM : online a M
a'M : online a' M
aα : on_circle a α ∧ on_circle a' α
b b' : point
bb' : b ≠ b'
bN : online b N
b'N : online b' N
bα : on_circle b α ∧ on_circle b' α
Baca' : B a c a'
Bbcb' : B b c b'
ac : a ≠ c
bc : b ≠ c
b'c : b' ≠ c
aO : ¬online a O
bO : ¬online b O
b'O : ¬online b' O
aN : ¬online a N
bM : ¬online b M
b'M : ¬online b' M
NO : N ≠ O
MO : M ≠ O
ssbaO : sameside b a O
ssabO : sameside a b O
⊢ False
Tactic:
all_goals
  have ss1 := sameside_of_sameside_not_sameside cd cO cN cM dO bN aM aN (sameside_symm ssabO)
  have ss2 := not_sameside_of_sameside_sameside cO cM cN dO aM bN ssabO
  have ss: sameside d a N ∨ sameside d b M := by tauto
  obtain ⟨e0, e0d, -⟩ := pt_of_line_ne_pt d L
  obtain ⟨β, hβ⟩ := circle_of_ne e0d.symm
  have dβ := inside_circle_of_center hβ.1
  have βL := line_circle_inter_of_inside_online dL dβ
  obtain ⟨e, e', ee', eL, e'L, eβ⟩ := pts_of_line_circle_inter βL
  have Bede' := B_of_line_circle_inter ee' dL eL e'L eβ.1 eβ.2 dβ
  have ed := ne_12_of_B Bede'
  have e'd := (ne_23_of_B Bede').symm
  have hneO : ¬ online e O := fun eO => LO (line_unique_of_pts ed eL dL eO dO)
  have hne'O : ¬ online e' O := fun he'O => LO (line_unique_of_pts e'd e'L dL he'O dO)
  by_cases nsaeO: sameside a e' O
  have nse'eO := not_sameside13_of_B123_online2 (B_symm Bede') dO
  have dsaeO := diffside_of_sameside_diffside (sameside_symm nsaeO) ⟨hne'O, hneO, nse'eO⟩
  swap; swap_var e ↔ e'; swap_var eL ↔ e'L; swap_var ed ↔ e'd; swap_var hneO ↔ hne'O
  have dsaeO: diffside a e O := ⟨aO, hneO, nsaeO⟩
  all_goals
    have dsbeO := diffside_of_sameside_diffside ssabO dsaeO
    have acd := alternate_eq_of_para aM cM cO dO dL eL dsaeO (para_symm pLM)
    have bcd := alternate_eq_of_para bN cN cO dO dL eL dsbeO (para_symm pLN)
    cases ss with
    | inl ssdaN =>
      have sum := (angle_add_iff_sameside bc.symm cd cN bN cO dO aO aN NO).2 ⟨sameside_symm ssabO, ssdaN⟩
      rw [acd, bcd, self_eq_add_left] at sum
      exact aN ((angle_zero_iff_online bc.symm ac.symm cN bN).2 sum).1
    | inr ssdbM =>
      have sum := (angle_add_iff_sameside ac.symm cd cM aM cO dO bO bM MO).2 ⟨ssabO, ssdbM⟩
      rw [acd, bcd, self_eq_add_left] at sum;
      exact bM ((angle_zero_iff_online ac.symm bc.symm cM aM).2 sum).1
Proof state after:
no goals