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'
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
ss1 : ¬sameside d a N → sameside d b M
ss2 : sameside d a N → ¬sameside d b M
ss : sameside d a N ∨ sameside d b M
e0 : point
e0d : e0 ≠ d
β : circle
hβ : center_circle d β ∧ on_circle e0 β
dβ : in_circle d β
βL : line_circle_inter L β
e' e : point
ee' : e' ≠ e
e'L : online e' L
eL : online e L
eβ : on_circle e' β ∧ on_circle e β
Bede' : B e' d e
e'd : e' ≠ d
ed : e ≠ d
hne'O : ¬online e' O
hneO : ¬online e O
nsaeO : ¬sameside a e O
dsaeO : diffside a e 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
ss1 : ¬sameside d a N → sameside d b M
ss2 : sameside d a N → ¬sameside d b M
ss : sameside d a N ∨ sameside d b M
e0 : point
e0d : e0 ≠ d
β : circle
hβ : center_circle d β ∧ on_circle e0 β
dβ : in_circle d β
βL : line_circle_inter L β
e e' : point
ee' : e ≠ e'
eL : online e L
e'L : online e' L
eβ : on_circle e β ∧ on_circle e' β
Bede' : B e d e'
ed : e ≠ d
e'd : e' ≠ d
hneO : ¬online e O
hne'O : ¬online e' O
nsaeO : sameside a e' O
nse'eO : ¬sameside e' e O
dsaeO : diffside a e O
⊢ False
Tactic:
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