Theorem: parallel_projection (Pythagoras/euclid_I_extras.lean)

State before:
i : incidence_geometry
a : point
L M N : line
aM : online a M
pMN : para M N
pLM : ¬para L M
aL : ¬online a L
⊢ ∃ b O, online b N ∧ online b O ∧ online a O ∧ para L O
Tactic:
have pLN : ¬ para L N := fun pLN => by
  cases para_trans (para_symm pMN) (para_symm pLN) with
  | inl h => rw [h] at aM; exact aL aM
  | inr h => exact pLM (para_symm h)
State after:
i : incidence_geometry
a : point
L M N : line
aM : online a M
pMN : para M N
pLM : ¬para L M
aL : ¬online a L
pLN : ¬para L N
⊢ ∃ b O, online b N ∧ online b O ∧ online a O ∧ para L O

State before:
i : incidence_geometry
a : point
L M N : line
aM : online a M
pMN : para M N
pLM : ¬para L M
aL : ¬online a L
pLN : ¬para L N
⊢ ∃ b O, online b N ∧ online b O ∧ online a O ∧ para L O
Tactic:
obtain ⟨ d, dL, dN ⟩ := pt_of_line_line pLN
State after:
case intro.intro
i : incidence_geometry
a : point
L M N : line
aM : online a M
pMN : para M N
pLM : ¬para L M
aL : ¬online a L
pLN : ¬para L N
d : point
dL : online d L
dN : online d N
⊢ ∃ b O, online b N ∧ online b O ∧ online a O ∧ para L O

State before:
case intro.intro
i : incidence_geometry
a : point
L M N : line
aM : online a M
pMN : para M N
pLM : ¬para L M
aL : ¬online a L
pLN : ¬para L N
d : point
dL : online d L
dN : online d N
⊢ ∃ b O, online b N ∧ online b O ∧ online a O ∧ para L O
Tactic:
obtain ⟨ O, aO, pLO ⟩ := para_of_offline aL
State after:
case intro.intro.intro.intro
i : incidence_geometry
a : point
L M N : line
aM : online a M
pMN : para M N
pLM : ¬para L M
aL : ¬online a L
pLN : ¬para L N
d : point
dL : online d L
dN : online d N
O : line
aO : online a O
pLO : para L O
⊢ ∃ b O, online b N ∧ online b O ∧ online a O ∧ para L O

State before:
case intro.intro.intro.intro
i : incidence_geometry
a : point
L M N : line
aM : online a M
pMN : para M N
pLM : ¬para L M
aL : ¬online a L
pLN : ¬para L N
d : point
dL : online d L
dN : online d N
O : line
aO : online a O
pLO : para L O
⊢ ∃ b O, online b N ∧ online b O ∧ online a O ∧ para L O
Tactic:
have pON : ¬ para O N := fun pON => by
  have pNO := para_trans pON (para_symm pLO)
  cases pNO with
  | inl pNO => rw [pNO] at pMN; exact pLM (para_symm pMN)
  | inr pNO => exact (offline_of_para dL (para_symm pNO)) dN
State after:
case intro.intro.intro.intro
i : incidence_geometry
a : point
L M N : line
aM : online a M
pMN : para M N
pLM : ¬para L M
aL : ¬online a L
pLN : ¬para L N
d : point
dL : online d L
dN : online d N
O : line
aO : online a O
pLO : para L O
pON : ¬para O N
⊢ ∃ b O, online b N ∧ online b O ∧ online a O ∧ para L O

State before:
case intro.intro.intro.intro
i : incidence_geometry
a : point
L M N : line
aM : online a M
pMN : para M N
pLM : ¬para L M
aL : ¬online a L
pLN : ¬para L N
d : point
dL : online d L
dN : online d N
O : line
aO : online a O
pLO : para L O
pON : ¬para O N
⊢ ∃ b O, online b N ∧ online b O ∧ online a O ∧ para L O
Tactic:
obtain ⟨ b, bO, bN ⟩ := pt_of_line_line pON
State after:
case intro.intro.intro.intro.intro.intro
i : incidence_geometry
a : point
L M N : line
aM : online a M
pMN : para M N
pLM : ¬para L M
aL : ¬online a L
pLN : ¬para L N
d : point
dL : online d L
dN : online d N
O : line
aO : online a O
pLO : para L O
pON : ¬para O N
b : point
bO : online b O
bN : online b N
⊢ ∃ b O, online b N ∧ online b O ∧ online a O ∧ para L O

State before:
case intro.intro.intro.intro.intro.intro
i : incidence_geometry
a : point
L M N : line
aM : online a M
pMN : para M N
pLM : ¬para L M
aL : ¬online a L
pLN : ¬para L N
d : point
dL : online d L
dN : online d N
O : line
aO : online a O
pLO : para L O
pON : ¬para O N
b : point
bO : online b O
bN : online b N
⊢ ∃ b O, online b N ∧ online b O ∧ online a O ∧ para L O
Tactic:
exact ⟨ b, O, bN, bO, aO, pLO ⟩
State after:
no goals

State before:
i : incidence_geometry
a : point
L M N : line
aM : online a M
pMN : para M N
pLM : ¬para L M
aL : ¬online a L
pLN : para L N
⊢ False
Tactic:
cases para_trans (para_symm pMN) (para_symm pLN) with
| inl h => rw [h] at aM; exact aL aM
| inr h => exact pLM (para_symm h)
State after:
no goals

State before:
case inl
i : incidence_geometry
a : point
L M N : line
aM : online a M
pMN : para M N
pLM : ¬para L M
aL : ¬online a L
pLN : para L N
h : M = L
⊢ False
Tactic:
rw [h] at aM
State after:
case inl
i : incidence_geometry
a : point
L M N : line
aM : online a L
pMN : para M N
pLM : ¬para L M
aL : ¬online a L
pLN : para L N
h : M = L
⊢ False

State before:
case inl
i : incidence_geometry
a : point
L M N : line
aM : online a L
pMN : para M N
pLM : ¬para L M
aL : ¬online a L
pLN : para L N
h : M = L
⊢ False
Tactic:
exact aL aM
State after:
no goals

State before:
case inr
i : incidence_geometry
a : point
L M N : line
aM : online a M
pMN : para M N
pLM : ¬para L M
aL : ¬online a L
pLN : para L N
h : para M L
⊢ False
Tactic:
exact pLM (para_symm h)
State after:
no goals

State before:
i : incidence_geometry
a : point
L M N : line
aM : online a M
pMN : para M N
pLM : ¬para L M
aL : ¬online a L
pLN : ¬para L N
d : point
dL : online d L
dN : online d N
O : line
aO : online a O
pLO : para L O
pON : para O N
⊢ False
Tactic:
have pNO := para_trans pON (para_symm pLO)
State after:
i : incidence_geometry
a : point
L M N : line
aM : online a M
pMN : para M N
pLM : ¬para L M
aL : ¬online a L
pLN : ¬para L N
d : point
dL : online d L
dN : online d N
O : line
aO : online a O
pLO : para L O
pON : para O N
pNO : N = L ∨ para N L
⊢ False

State before:
i : incidence_geometry
a : point
L M N : line
aM : online a M
pMN : para M N
pLM : ¬para L M
aL : ¬online a L
pLN : ¬para L N
d : point
dL : online d L
dN : online d N
O : line
aO : online a O
pLO : para L O
pON : para O N
pNO : N = L ∨ para N L
⊢ False
Tactic:
cases pNO with
| inl pNO => rw [pNO] at pMN; exact pLM (para_symm pMN)
| inr pNO => exact (offline_of_para dL (para_symm pNO)) dN
State after:
no goals

State before:
case inl
i : incidence_geometry
a : point
L M N : line
aM : online a M
pMN : para M N
pLM : ¬para L M
aL : ¬online a L
pLN : ¬para L N
d : point
dL : online d L
dN : online d N
O : line
aO : online a O
pLO : para L O
pON : para O N
pNO : N = L
⊢ False
Tactic:
rw [pNO] at pMN
State after:
case inl
i : incidence_geometry
a : point
L M N : line
aM : online a M
pMN : para M L
pLM : ¬para L M
aL : ¬online a L
pLN : ¬para L N
d : point
dL : online d L
dN : online d N
O : line
aO : online a O
pLO : para L O
pON : para O N
pNO : N = L
⊢ False

State before:
case inl
i : incidence_geometry
a : point
L M N : line
aM : online a M
pMN : para M L
pLM : ¬para L M
aL : ¬online a L
pLN : ¬para L N
d : point
dL : online d L
dN : online d N
O : line
aO : online a O
pLO : para L O
pON : para O N
pNO : N = L
⊢ False
Tactic:
exact pLM (para_symm pMN)
State after:
no goals

State before:
case inr
i : incidence_geometry
a : point
L M N : line
aM : online a M
pMN : para M N
pLM : ¬para L M
aL : ¬online a L
pLN : ¬para L N
d : point
dL : online d L
dN : online d N
O : line
aO : online a O
pLO : para L O
pON : para O N
pNO : para N L
⊢ False
Tactic:
exact (offline_of_para dL (para_symm pNO)) dN
State after:
no goals