internlm/Lean-Github huggingface dataset:
Theorem: area_of_parallelogram
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c d : point
L M N O : line
abcd : paragram a b c d L M N O
aL : online a L
bL : online b L
bM : online b M
cM : online c M
cN : online c N
dN : online d N
dO : online d O
aO : online a O
pLN : para L N
pMO : para M O
bcda : paragram b c d a M N O L
⊢ area a b c + area a d c = 2 * area a b c ∧ area b a d + area b c d = 2 * area a b c
Tactic:
constructor
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.left
i : incidence_geometry
a b c d : point
L M N O : line
abcd : paragram a b c d L M N O
aL : online a L
bL : online b L
bM : online b M
cM : online c M
cN : online c N
dN : online d N
dO : online d O
aO : online a O
pLN : para L N
pMO : para M O
bcda : paragram b c d a M N O L
⊢ area a b c + area a d c = 2 * area a b c

case intro.intro.intro.intro.intro.intro.intro.intro.intro.right
i : incidence_geometry
a b c d : point
L M N O : line
abcd : paragram a b c d L M N O
aL : online a L
bL : online b L
bM : online b M
cM : online c M
cN : online c N
dN : online d N
dO : online d O
aO : online a O
pLN : para L N
pMO : para M O
bcda : paragram b c d a M N O L
⊢ area b a d + area b c d = 2 * area a b c
Theorem: area_of_parallelogram
Proof state before:
i : incidence_geometry
a b c d : point
L M N O : line
abcd : paragram a b c d L M N O
aL : online a L
bL : online b L
bM : online b M
cM : online c M
cN : online c N
dN : online d N
dO : online d O
aO : online a O
pLN : para L N
pMO : para M O
⊢ paragram b c d a M N O L
Tactic:
splitAll <;> perma only [para]
Proof state after:
no goals
Theorem: area_of_parallelogram
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.left
i : incidence_geometry
a b c d : point
L M N O : line
abcd : paragram a b c d L M N O
aL : online a L
bL : online b L
bM : online b M
cM : online c M
cN : online c N
dN : online d N
dO : online d O
aO : online a O
pLN : para L N
pMO : para M O
bcda : paragram b c d a M N O L
⊢ area a b c + area a d c = 2 * area a b c
Tactic:
linperm [(len_ang_area_eq_of_parallelogram bcda).2.2]
Proof state after:
no goals
Theorem: area_of_parallelogram
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.right
i : incidence_geometry
a b c d : point
L M N O : line
abcd : paragram a b c d L M N O
aL : online a L
bL : online b L
bM : online b M
cM : online c M
cN : online c N
dN : online d N
dO : online d O
aO : online a O
pLN : para L N
pMO : para M O
bcda : paragram b c d a M N O L
⊢ area b a d + area b c d = 2 * area a b c
Tactic:
linperm [(len_ang_area_eq_of_parallelogram abcd).2.2, triarea cN dN bL aL (by perma)]
Proof state after:
no goals
Theorem: area_of_parallelogram
Proof state before:
i : incidence_geometry
a b c d : point
L M N O : line
abcd : paragram a b c d L M N O
aL : online a L
bL : online b L
bM : online b M
cM : online c M
cN : online c N
dN : online d N
dO : online d O
aO : online a O
pLN : para L N
pMO : para M O
bcda : paragram b c d a M N O L
⊢ para N L
Tactic:
perma
Proof state after:
no goals
Theorem: not_online_of_triangle
Proof state before:
i : incidence_geometry
a b c : point
L M : line
aL : online a L
bL : online b L
bM : online b M
cM : online c M
hn : ¬online a M
bc : b ≠ c
cL : online c L
⊢ False
Tactic:
rw [line_unique_of_pts bc bL cL bM cM] at aL
Proof state after:
i : incidence_geometry
a b c : point
L M : line
aL : online a M
bL : online b L
bM : online b M
cM : online c M
hn : ¬online a M
bc : b ≠ c
cL : online c L
⊢ False
Theorem: not_online_of_triangle
Proof state before:
i : incidence_geometry
a b c : point
L M : line
aL : online a M
bL : online b L
bM : online b M
cM : online c M
hn : ¬online a M
bc : b ≠ c
cL : online c L
⊢ False
Tactic:
exact hn aL
Proof state after:
no goals
Theorem: parallel_of_line_pt
Proof state before:
i : incidence_geometry
a : point
L : line
aL : ¬online a L
⊢ ∃ M, online a M ∧ para L M
Tactic:
dsimp [para]
Proof state after:
i : incidence_geometry
a : point
L : line
aL : ¬online a L
⊢ ∃ M, online a M ∧ ∀ (e : point), ¬online e L ∨ ¬online e M
Theorem: parallel_of_line_pt
Proof state before:
i : incidence_geometry
a : point
L : line
aL : ¬online a L
⊢ ∃ M, online a M ∧ ∀ (e : point), ¬online e L ∨ ¬online e M
Tactic:
exact para_of_offline aL
Proof state after:
no goals
Theorem: parallel_projection
Proof 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)
Proof 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
Theorem: parallel_projection
Proof 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
Proof 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
Theorem: parallel_projection
Proof 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
Proof 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
Theorem: parallel_projection
Proof 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
Proof 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
Theorem: parallel_projection
Proof 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
Proof 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
Theorem: parallel_projection
Proof 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 ⟩
Proof state after:
no goals
Theorem: parallel_projection
Proof 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)
Proof state after:
no goals
Theorem: parallel_projection
Proof 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
Proof 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
Theorem: parallel_projection
Proof 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
Proof state after:
no goals
Theorem: parallel_projection
Proof 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)
Proof state after:
no goals
Theorem: parallel_projection
Proof 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)
Proof 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
Theorem: parallel_projection
Proof 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
Proof state after:
no goals
Theorem: parallel_projection
Proof 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
Proof 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
Theorem: parallel_projection
Proof 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)
Proof state after:
no goals
Theorem: parallel_projection
Proof 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
Proof state after:
no goals
Theorem: not_para_of_online_online
Proof state before:
i : incidence_geometry
a : point
L M : line
hL : online a L
hM : online a M
⊢ ¬para L M
Tactic:
simp_rw [para, not_forall, not_or, not_not]
Proof state after:
i : incidence_geometry
a : point
L M : line
hL : online a L
hM : online a M
⊢ ∃ x, online x L ∧ online x M
Theorem: not_para_of_online_online
Proof state before:
i : incidence_geometry
a : point
L M : line
hL : online a L
hM : online a M
⊢ ∃ x, online x L ∧ online x M
Tactic:
exact ⟨ a, hL, hM ⟩
Proof state after:
no goals
Theorem: diffside_of_trapezoid
Proof 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
Proof 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
Theorem: diffside_of_trapezoid
Proof 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
Proof 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
Theorem: diffside_of_trapezoid
Proof 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, _ ⟩
Proof 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
Theorem: diffside_of_trapezoid
Proof 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, _ ⟩
Proof 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
Theorem: diffside_of_trapezoid
Proof 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)
Proof 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
Theorem: diffside_of_trapezoid
Proof 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
Proof state after:
no goals
Theorem: diffside_of_trapezoid
Proof 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
Proof 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
Theorem: diffside_of_trapezoid
Proof 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, _ ⟩
Proof 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
Theorem: diffside_of_trapezoid
Proof 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 ⟩
Proof state after:
no goals
Theorem: not_B_of_short
Proof state before:
i : incidence_geometry
a b c : point
hlen : length a b < length a c
hBacb : B a c b
⊢ False
Tactic:
rw [(length_sum_of_B hBacb).symm] at hlen
Proof state after:
i : incidence_geometry
a b c : point
hlen : length a c + length c b < length a c
hBacb : B a c b
⊢ False
Theorem: not_B_of_short
Proof state before:
i : incidence_geometry
a b c : point
hlen : length a c + length c b < length a c
hBacb : B a c b
⊢ False
Tactic:
linarith [length_nonneg c b]
Proof state after:
no goals
Theorem: B_of_three_online_ne_short
Proof state before:
i : incidence_geometry
a b c : point
L : line
hlen : length a b < length a c
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
aL : online a L
bL : online b L
cL : online c L
⊢ B a b c ∨ B b a c
Tactic:
have := B_of_three_online_ne ab ac bc aL bL cL
Proof state after:
i : incidence_geometry
a b c : point
L : line
hlen : length a b < length a c
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
aL : online a L
bL : online b L
cL : online c L
this : B a b c ∨ B b a c ∨ B a c b
⊢ B a b c ∨ B b a c
Theorem: B_of_three_online_ne_short
Proof state before:
i : incidence_geometry
a b c : point
L : line
hlen : length a b < length a c
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
aL : online a L
bL : online b L
cL : online c L
this : B a b c ∨ B b a c ∨ B a c b
⊢ B a b c ∨ B b a c
Tactic:
convert this
Proof state after:
case h.e'_2.a
i : incidence_geometry
a b c : point
L : line
hlen : length a b < length a c
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
aL : online a L
bL : online b L
cL : online c L
this : B a b c ∨ B b a c ∨ B a c b
⊢ B b a c ↔ B b a c ∨ B a c b
Theorem: B_of_three_online_ne_short
Proof state before:
case h.e'_2.a
i : incidence_geometry
a b c : point
L : line
hlen : length a b < length a c
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
aL : online a L
bL : online b L
cL : online c L
this : B a b c ∨ B b a c ∨ B a c b
⊢ B b a c ↔ B b a c ∨ B a c b
Tactic:
simp [not_B_of_short hlen]
Proof state after:
no goals
Theorem: same_length_B_of_ne_ge
Proof state before:
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < length c d
⊢ ∃ p, B a b p ∧ length a p = length c d
Tactic:
have cd : c ≠ d := fun cd => by
  rw [cd, length_eq_zero_iff.mpr rfl] at big;
  exact not_lt_of_ge (length_nonneg a b) big
Proof state after:
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < length c d
cd : c ≠ d
⊢ ∃ p, B a b p ∧ length a p = length c d
Theorem: same_length_B_of_ne_ge
Proof state before:
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < length c d
cd : c ≠ d
⊢ ∃ p, B a b p ∧ length a p = length c d
Tactic:
obtain ⟨q, Hq⟩ := length_eq_B_of_ne_four ab.symm cd
Proof state after:
case intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < length c d
cd : c ≠ d
q : point
Hq : B b a q ∧ length c d = length a q
⊢ ∃ p, B a b p ∧ length a p = length c d
Theorem: same_length_B_of_ne_ge
Proof state before:
case intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < length c d
cd : c ≠ d
q : point
Hq : B b a q ∧ length c d = length a q
⊢ ∃ p, B a b p ∧ length a p = length c d
Tactic:
have aq : a ≠ q := fun aq => by
  rw [aq, length_eq_zero_iff.mpr rfl] at Hq; rw [Hq.2] at big
  exact not_lt_of_ge (length_nonneg a b) big
Proof state after:
case intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < length c d
cd : c ≠ d
q : point
Hq : B b a q ∧ length c d = length a q
aq : a ≠ q
⊢ ∃ p, B a b p ∧ length a p = length c d
Theorem: same_length_B_of_ne_ge
Proof state before:
case intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < length c d
cd : c ≠ d
q : point
Hq : B b a q ∧ length c d = length a q
aq : a ≠ q
⊢ ∃ p, B a b p ∧ length a p = length c d
Tactic:
obtain ⟨C, hC⟩ := circle_of_ne aq
Proof state after:
case intro.intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < length c d
cd : c ≠ d
q : point
Hq : B b a q ∧ length c d = length a q
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
⊢ ∃ p, B a b p ∧ length a p = length c d
Theorem: same_length_B_of_ne_ge
Proof state before:
case intro.intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < length c d
cd : c ≠ d
q : point
Hq : B b a q ∧ length c d = length a q
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
⊢ ∃ p, B a b p ∧ length a p = length c d
Tactic:
obtain ⟨p, Hp⟩ := pt_oncircle_of_inside_ne aq.symm (inside_circle_of_center hC.1)
Proof state after:
case intro.intro.intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < length c d
cd : c ≠ d
q : point
Hq : B b a q ∧ length c d = length a q
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
Hp : B q a p ∧ on_circle p C
⊢ ∃ p, B a b p ∧ length a p = length c d
Theorem: same_length_B_of_ne_ge
Proof state before:
case intro.intro.intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < length c d
cd : c ≠ d
q : point
Hq : B b a q ∧ length c d = length a q
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
Hp : B q a p ∧ on_circle p C
⊢ ∃ p, B a b p ∧ length a p = length c d
Tactic:
obtain ⟨AB, aAB, bAB⟩ := line_of_pts a b
Proof state after:
case intro.intro.intro.intro.intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < length c d
cd : c ≠ d
q : point
Hq : B b a q ∧ length c d = length a q
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
⊢ ∃ p, B a b p ∧ length a p = length c d