Theorem: diffside_of_trapezoid (Pythagoras/euclid_I_extras.lean)

State before:
i : incidence_geometry
a b c d : point
L M N O : line
aL : online a L
bL : online b L
bM : online b M
cM : online c M
cN : online c N
dN : online d N
bO : online b O
dO : online d O
pLN : para L N
h_nondeg : a ≠ b ∧ c ≠ d
⊢ diffside a c O ∨ diffside a d M
Tactic:
by_cases h_ss : sameside a c O
State after:
case pos
i : incidence_geometry
a b c d : point
L M N O : line
aL : online a L
bL : online b L
bM : online b M
cM : online c M
cN : online c N
dN : online d N
bO : online b O
dO : online d O
pLN : para L N
h_nondeg : a ≠ b ∧ c ≠ d
h_ss : sameside a c O
⊢ diffside a c O ∨ diffside a d M

case neg
i : incidence_geometry
a b c d : point
L M N O : line
aL : online a L
bL : online b L
bM : online b M
cM : online c M
cN : online c N
dN : online d N
bO : online b O
dO : online d O
pLN : para L N
h_nondeg : a ≠ b ∧ c ≠ d
h_ss : ¬sameside a c O
⊢ diffside a c O ∨ diffside a d M

State before:
case pos
i : incidence_geometry
a b c d : point
L M N O : line
aL : online a L
bL : online b L
bM : online b M
cM : online c M
cN : online c N
dN : online d N
bO : online b O
dO : online d O
pLN : para L N
h_nondeg : a ≠ b ∧ c ≠ d
h_ss : sameside a c O
⊢ diffside a c O ∨ diffside a d M
Tactic:
right
State after:
case pos.h
i : incidence_geometry
a b c d : point
L M N O : line
aL : online a L
bL : online b L
bM : online b M
cM : online c M
cN : online c N
dN : online d N
bO : online b O
dO : online d O
pLN : para L N
h_nondeg : a ≠ b ∧ c ≠ d
h_ss : sameside a c O
⊢ diffside a d M

State before:
case pos.h
i : incidence_geometry
a b c d : point
L M N O : line
aL : online a L
bL : online b L
bM : online b M
cM : online c M
cN : online c N
dN : online d N
bO : online b O
dO : online d O
pLN : para L N
h_nondeg : a ≠ b ∧ c ≠ d
h_ss : sameside a c O
⊢ diffside a d M
Tactic:
refine' ⟨ not_online_of_triangle cM bM bL aL (offline_of_para cN (para_symm pLN)) h_nondeg.1.symm, _ ⟩
State after:
case pos.h
i : incidence_geometry
a b c d : point
L M N O : line
aL : online a L
bL : online b L
bM : online b M
cM : online c M
cN : online c N
dN : online d N
bO : online b O
dO : online d O
pLN : para L N
h_nondeg : a ≠ b ∧ c ≠ d
h_ss : sameside a c O
⊢ ¬online d M ∧ ¬sameside a d M

State before:
case pos.h
i : incidence_geometry
a b c d : point
L M N O : line
aL : online a L
bL : online b L
bM : online b M
cM : online c M
cN : online c N
dN : online d N
bO : online b O
dO : online d O
pLN : para L N
h_nondeg : a ≠ b ∧ c ≠ d
h_ss : sameside a c O
⊢ ¬online d M ∧ ¬sameside a d M
Tactic:
refine' ⟨ not_online_of_triangle bM cM cN dN (offline_of_para bL pLN) h_nondeg.2, _ ⟩
State after:
case pos.h
i : incidence_geometry
a b c d : point
L M N O : line
aL : online a L
bL : online b L
bM : online b M
cM : online c M
cN : online c N
dN : online d N
bO : online b O
dO : online d O
pLN : para L N
h_nondeg : a ≠ b ∧ c ≠ d
h_ss : sameside a c O
⊢ ¬sameside a d M

State before:
case pos.h
i : incidence_geometry
a b c d : point
L M N O : line
aL : online a L
bL : online b L
bM : online b M
cM : online c M
cN : online c N
dN : online d N
bO : online b O
dO : online d O
pLN : para L N
h_nondeg : a ≠ b ∧ c ≠ d
h_ss : sameside a c O
⊢ ¬sameside a d M
Tactic:
have := sameside_of_para_online cN dN (para_symm pLN)
State after:
case pos.h
i : incidence_geometry
a b c d : point
L M N O : line
aL : online a L
bL : online b L
bM : online b M
cM : online c M
cN : online c N
dN : online d N
bO : online b O
dO : online d O
pLN : para L N
h_nondeg : a ≠ b ∧ c ≠ d
h_ss : sameside a c O
this : sameside c d L
⊢ ¬sameside a d M

State before:
case pos.h
i : incidence_geometry
a b c d : point
L M N O : line
aL : online a L
bL : online b L
bM : online b M
cM : online c M
cN : online c N
dN : online d N
bO : online b O
dO : online d O
pLN : para L N
h_nondeg : a ≠ b ∧ c ≠ d
h_ss : sameside a c O
this : sameside c d L
⊢ ¬sameside a d M
Tactic:
exact not_sameside_of_sameside_sameside bL bM bO aL cM dO this h_ss
State after:
no goals

State before:
case neg
i : incidence_geometry
a b c d : point
L M N O : line
aL : online a L
bL : online b L
bM : online b M
cM : online c M
cN : online c N
dN : online d N
bO : online b O
dO : online d O
pLN : para L N
h_nondeg : a ≠ b ∧ c ≠ d
h_ss : ¬sameside a c O
⊢ diffside a c O ∨ diffside a d M
Tactic:
left
State after:
case neg.h
i : incidence_geometry
a b c d : point
L M N O : line
aL : online a L
bL : online b L
bM : online b M
cM : online c M
cN : online c N
dN : online d N
bO : online b O
dO : online d O
pLN : para L N
h_nondeg : a ≠ b ∧ c ≠ d
h_ss : ¬sameside a c O
⊢ diffside a c O

State before:
case neg.h
i : incidence_geometry
a b c d : point
L M N O : line
aL : online a L
bL : online b L
bM : online b M
cM : online c M
cN : online c N
dN : online d N
bO : online b O
dO : online d O
pLN : para L N
h_nondeg : a ≠ b ∧ c ≠ d
h_ss : ¬sameside a c O
⊢ diffside a c O
Tactic:
refine' ⟨ not_online_of_triangle dO bO bL aL (offline_of_para dN (para_symm pLN)) h_nondeg.1.symm, _ ⟩
State after:
case neg.h
i : incidence_geometry
a b c d : point
L M N O : line
aL : online a L
bL : online b L
bM : online b M
cM : online c M
cN : online c N
dN : online d N
bO : online b O
dO : online d O
pLN : para L N
h_nondeg : a ≠ b ∧ c ≠ d
h_ss : ¬sameside a c O
⊢ ¬online c O ∧ ¬sameside a c O

State before:
case neg.h
i : incidence_geometry
a b c d : point
L M N O : line
aL : online a L
bL : online b L
bM : online b M
cM : online c M
cN : online c N
dN : online d N
bO : online b O
dO : online d O
pLN : para L N
h_nondeg : a ≠ b ∧ c ≠ d
h_ss : ¬sameside a c O
⊢ ¬online c O ∧ ¬sameside a c O
Tactic:
refine' ⟨ not_online_of_triangle bO dO dN cN (offline_of_para bL pLN) h_nondeg.2.symm, h_ss ⟩
State after:
no goals