internlm/Lean-Github huggingface dataset:
Theorem: lt_area_of_lt_base_sameedge_nBfbc
Proof state before:
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
bc : b ≠ c
bf : b ≠ f
aL : ¬online a L
hB : ¬B f b c
hlen : length b f < length b c
⊢ area a b c > area a b f
Tactic:
have cf: c ≠ f := fun cf => by rw [cf, lt_self_iff_false] at hlen; exact hlen
Proof state after:
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
bc : b ≠ c
bf : b ≠ f
aL : ¬online a L
hB : ¬B f b c
hlen : length b f < length b c
cf : c ≠ f
⊢ area a b c > area a b f
Theorem: lt_area_of_lt_base_sameedge_nBfbc
Proof state before:
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
bc : b ≠ c
bf : b ≠ f
aL : ¬online a L
hB : ¬B f b c
hlen : length b f < length b c
cf : c ≠ f
⊢ area a b c > area a b f
Tactic:
have := B_of_three_online_ne_short hlen bf bc cf.symm bL fL cL
Proof state after:
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
bc : b ≠ c
bf : b ≠ f
aL : ¬online a L
hB : ¬B f b c
hlen : length b f < length b c
cf : c ≠ f
this : B b f c ∨ B f b c
⊢ area a b c > area a b f
Theorem: lt_area_of_lt_base_sameedge_nBfbc
Proof state before:
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
bc : b ≠ c
bf : b ≠ f
aL : ¬online a L
hB : ¬B f b c
hlen : length b f < length b c
cf : c ≠ f
this : B b f c ∨ B f b c
⊢ area a b c > area a b f
Tactic:
cases this with
| inl h => exact lt_area_of_lt_base_sameedge_Bbfc a bL cL fL h bc bf cf aL hlen
| inr h => exfalso; exact hB h
Proof state after:
no goals
Theorem: lt_area_of_lt_base_sameedge_nBfbc
Proof state before:
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
bc : b ≠ c
bf : b ≠ f
aL : ¬online a L
hB : ¬B f b c
hlen : length b f < length b c
cf : c = f
⊢ False
Tactic:
rw [cf, lt_self_iff_false] at hlen
Proof state after:
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
bc : b ≠ c
bf : b ≠ f
aL : ¬online a L
hB : ¬B f b c
hlen : False
cf : c = f
⊢ False
Theorem: lt_area_of_lt_base_sameedge_nBfbc
Proof state before:
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
bc : b ≠ c
bf : b ≠ f
aL : ¬online a L
hB : ¬B f b c
hlen : False
cf : c = f
⊢ False
Tactic:
exact hlen
Proof state after:
no goals
Theorem: lt_area_of_lt_base_sameedge_nBfbc
Proof state before:
case inl
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
bc : b ≠ c
bf : b ≠ f
aL : ¬online a L
hB : ¬B f b c
hlen : length b f < length b c
cf : c ≠ f
h : B b f c
⊢ area a b c > area a b f
Tactic:
exact lt_area_of_lt_base_sameedge_Bbfc a bL cL fL h bc bf cf aL hlen
Proof state after:
no goals
Theorem: lt_area_of_lt_base_sameedge_nBfbc
Proof state before:
case inr
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
bc : b ≠ c
bf : b ≠ f
aL : ¬online a L
hB : ¬B f b c
hlen : length b f < length b c
cf : c ≠ f
h : B f b c
⊢ area a b c > area a b f
Tactic:
exfalso
Proof state after:
case inr.h
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
bc : b ≠ c
bf : b ≠ f
aL : ¬online a L
hB : ¬B f b c
hlen : length b f < length b c
cf : c ≠ f
h : B f b c
⊢ False
Theorem: lt_area_of_lt_base_sameedge_nBfbc
Proof state before:
case inr.h
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
bc : b ≠ c
bf : b ≠ f
aL : ¬online a L
hB : ¬B f b c
hlen : length b f < length b c
cf : c ≠ f
h : B f b c
⊢ False
Tactic:
exact hB h
Proof state after:
no goals
Theorem: lt_area_of_lt_base_sameedge
Proof state before:
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
bc : b ≠ c
bf : b ≠ f
aL : ¬online a L
⊢ length b c > length b f → area a b c > area a b f
Tactic:
intro hlen
Proof state after:
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
bc : b ≠ c
bf : b ≠ f
aL : ¬online a L
hlen : length b c > length b f
⊢ area a b c > area a b f
Theorem: lt_area_of_lt_base_sameedge
Proof state before:
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
bc : b ≠ c
bf : b ≠ f
aL : ¬online a L
hlen : length b c > length b f
⊢ area a b c > area a b f
Tactic:
by_cases Bfbc: B f b c
Proof state after:
case pos
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
bc : b ≠ c
bf : b ≠ f
aL : ¬online a L
hlen : length b c > length b f
Bfbc : B f b c
⊢ area a b c > area a b f

case neg
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
bc : b ≠ c
bf : b ≠ f
aL : ¬online a L
hlen : length b c > length b f
Bfbc : ¬B f b c
⊢ area a b c > area a b f
Theorem: lt_area_of_lt_base_sameedge
Proof state before:
case pos
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
bc : b ≠ c
bf : b ≠ f
aL : ¬online a L
hlen : length b c > length b f
Bfbc : B f b c
⊢ area a b c > area a b f
Tactic:
obtain ⟨ e, He ⟩ := rescale_length 2 fL bL
Proof state after:
case pos.intro
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
bc : b ≠ c
bf : b ≠ f
aL : ¬online a L
hlen : length b c > length b f
Bfbc : B f b c
e : point
He : online e L ∧ length f e = ↑2 * length f b ∧ (2 ≥ 2 ∧ f ≠ b → B f b e)
⊢ area a b c > area a b f
Theorem: lt_area_of_lt_base_sameedge
Proof state before:
case pos.intro
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
bc : b ≠ c
bf : b ≠ f
aL : ¬online a L
hlen : length b c > length b f
Bfbc : B f b c
e : point
He : online e L ∧ length f e = ↑2 * length f b ∧ (2 ≥ 2 ∧ f ≠ b → B f b e)
⊢ area a b c > area a b f
Tactic:
have Bfbe := He.2.2 ⟨ by simp [ge_iff_le], bf.symm ⟩
Proof state after:
case pos.intro
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
bc : b ≠ c
bf : b ≠ f
aL : ¬online a L
hlen : length b c > length b f
Bfbc : B f b c
e : point
He : online e L ∧ length f e = ↑2 * length f b ∧ (2 ≥ 2 ∧ f ≠ b → B f b e)
Bfbe : B f b e
⊢ area a b c > area a b f
Theorem: lt_area_of_lt_base_sameedge
Proof state before:
case pos.intro
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
bc : b ≠ c
bf : b ≠ f
aL : ¬online a L
hlen : length b c > length b f
Bfbc : B f b c
e : point
He : online e L ∧ length f e = ↑2 * length f b ∧ (2 ≥ 2 ∧ f ≠ b → B f b e)
Bfbe : B f b e
⊢ area a b c > area a b f
Tactic:
have Lbe : length b e = length b f := by
  perm [length_sum_of_B Bfbe]; perm at He; norm_cast at this He; linarith
Proof state after:
case pos.intro
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
bc : b ≠ c
bf : b ≠ f
aL : ¬online a L
hlen : length b c > length b f
Bfbc : B f b c
e : point
He : online e L ∧ length f e = ↑2 * length f b ∧ (2 ≥ 2 ∧ f ≠ b → B f b e)
Bfbe : B f b e
Lbe : length b e = length b f
⊢ area a b c > area a b f
Theorem: lt_area_of_lt_base_sameedge
Proof state before:
case pos.intro
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
bc : b ≠ c
bf : b ≠ f
aL : ¬online a L
hlen : length b c > length b f
Bfbc : B f b c
e : point
He : online e L ∧ length f e = ↑2 * length f b ∧ (2 ≥ 2 ∧ f ≠ b → B f b e)
Bfbe : B f b e
Lbe : length b e = length b f
⊢ area a b c > area a b f
Tactic:
rw [← eq_area_of_eq_base_samevertex a bL He.1 bL fL Lbe]
Proof state after:
case pos.intro
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
bc : b ≠ c
bf : b ≠ f
aL : ¬online a L
hlen : length b c > length b f
Bfbc : B f b c
e : point
He : online e L ∧ length f e = ↑2 * length f b ∧ (2 ≥ 2 ∧ f ≠ b → B f b e)
Bfbe : B f b e
Lbe : length b e = length b f
⊢ area a b c > area a b e
Theorem: lt_area_of_lt_base_sameedge
Proof state before:
case pos.intro
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
bc : b ≠ c
bf : b ≠ f
aL : ¬online a L
hlen : length b c > length b f
Bfbc : B f b c
e : point
He : online e L ∧ length f e = ↑2 * length f b ∧ (2 ≥ 2 ∧ f ≠ b → B f b e)
Bfbe : B f b e
Lbe : length b e = length b f
⊢ area a b c > area a b e
Tactic:
rw [← Lbe] at hlen
Proof state after:
case pos.intro
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
bc : b ≠ c
bf : b ≠ f
aL : ¬online a L
Bfbc : B f b c
e : point
hlen : length b c > length b e
He : online e L ∧ length f e = ↑2 * length f b ∧ (2 ≥ 2 ∧ f ≠ b → B f b e)
Bfbe : B f b e
Lbe : length b e = length b f
⊢ area a b c > area a b e
Theorem: lt_area_of_lt_base_sameedge
Proof state before:
case pos.intro
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
bc : b ≠ c
bf : b ≠ f
aL : ¬online a L
Bfbc : B f b c
e : point
hlen : length b c > length b e
He : online e L ∧ length f e = ↑2 * length f b ∧ (2 ≥ 2 ∧ f ≠ b → B f b e)
Bfbe : B f b e
Lbe : length b e = length b f
⊢ area a b c > area a b e
Tactic:
exact lt_area_of_lt_base_sameedge_nBfbc a bL cL He.1 bc (ne_23_of_B Bfbe) aL (not_B324_of_B123_B124 Bfbe Bfbc) hlen
Proof state after:
no goals
Theorem: lt_area_of_lt_base_sameedge
Proof state before:
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
bc : b ≠ c
bf : b ≠ f
aL : ¬online a L
hlen : length b c > length b f
Bfbc : B f b c
e : point
He : online e L ∧ length f e = ↑2 * length f b ∧ (2 ≥ 2 ∧ f ≠ b → B f b e)
⊢ 2 ≥ 2
Tactic:
simp [ge_iff_le]
Proof state after:
no goals
Theorem: lt_area_of_lt_base_sameedge
Proof state before:
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
bc : b ≠ c
bf : b ≠ f
aL : ¬online a L
hlen : length b c > length b f
Bfbc : B f b c
e : point
He : online e L ∧ length f e = ↑2 * length f b ∧ (2 ≥ 2 ∧ f ≠ b → B f b e)
Bfbe : B f b e
⊢ length b e = length b f
Tactic:
perm [length_sum_of_B Bfbe]
Proof state after:
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
bc : b ≠ c
bf : b ≠ f
aL : ¬online a L
hlen : length b c > length b f
Bfbc : B f b c
e : point
He : online e L ∧ length f e = ↑2 * length f b ∧ (2 ≥ 2 ∧ f ≠ b → B f b e)
Bfbe : B f b e
this : length b f + length b e = length e f
⊢ length b e = length b f
Theorem: lt_area_of_lt_base_sameedge
Proof state before:
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
bc : b ≠ c
bf : b ≠ f
aL : ¬online a L
hlen : length b c > length b f
Bfbc : B f b c
e : point
He : online e L ∧ length f e = ↑2 * length f b ∧ (2 ≥ 2 ∧ f ≠ b → B f b e)
Bfbe : B f b e
this : length b f + length b e = length e f
⊢ length b e = length b f
Tactic:
perm at He
Proof state after:
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
bc : b ≠ c
bf : b ≠ f
aL : ¬online a L
hlen : length b c > length b f
Bfbc : B f b c
e : point
He : online e L ∧ length e f = ↑2 * length b f ∧ (2 ≥ 2 ∧ f ≠ b → B f b e)
Bfbe : B f b e
this : length b f + length b e = length e f
⊢ length b e = length b f
Theorem: lt_area_of_lt_base_sameedge
Proof state before:
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
bc : b ≠ c
bf : b ≠ f
aL : ¬online a L
hlen : length b c > length b f
Bfbc : B f b c
e : point
He : online e L ∧ length e f = ↑2 * length b f ∧ (2 ≥ 2 ∧ f ≠ b → B f b e)
Bfbe : B f b e
this : length b f + length b e = length e f
⊢ length b e = length b f
Tactic:
norm_cast at this He
Proof state after:
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
bc : b ≠ c
bf : b ≠ f
aL : ¬online a L
hlen : length b c > length b f
Bfbc : B f b c
e : point
Bfbe : B f b e
this : length b f + length b e = length e f
He : online e L ∧ length e f = 2 * length b f ∧ (True ∧ ¬f = b → B f b e)
⊢ length b e = length b f
Theorem: lt_area_of_lt_base_sameedge
Proof state before:
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
bc : b ≠ c
bf : b ≠ f
aL : ¬online a L
hlen : length b c > length b f
Bfbc : B f b c
e : point
Bfbe : B f b e
this : length b f + length b e = length e f
He : online e L ∧ length e f = 2 * length b f ∧ (True ∧ ¬f = b → B f b e)
⊢ length b e = length b f
Tactic:
linarith
Proof state after:
no goals
Theorem: lt_area_of_lt_base_sameedge
Proof state before:
case neg
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
bc : b ≠ c
bf : b ≠ f
aL : ¬online a L
hlen : length b c > length b f
Bfbc : ¬B f b c
⊢ area a b c > area a b f
Tactic:
exact lt_area_of_lt_base_sameedge_nBfbc a bL cL fL bc bf aL Bfbc hlen
Proof state after:
no goals
Theorem: lt_area_of_lt_base
Proof state before:
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
⊢ length b c > length e f → area a b c > area d e f
Tactic:
intro hlen
Proof state after:
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
⊢ area a b c > area d e f
Theorem: lt_area_of_lt_base
Proof state before:
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
⊢ area a b c > area d e f
Tactic:
have bc : b ≠ c := fun bc => by
  rw [length_eq_zero_iff.mpr bc] at hlen
  exact (not_le_of_gt hlen) (length_nonneg e f)
Proof state after:
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
⊢ area a b c > area d e f
Theorem: lt_area_of_lt_base
Proof state before:
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
⊢ area a b c > area d e f
Tactic:
have aL := offline_of_para aM (para_symm pLM)
Proof state after:
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
⊢ area a b c > area d e f
Theorem: lt_area_of_lt_base
Proof state before:
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
⊢ area a b c > area d e f
Tactic:
have dL := offline_of_para dM (para_symm pLM)
Proof state after:
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
⊢ area a b c > area d e f
Theorem: lt_area_of_lt_base
Proof state before:
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
⊢ area a b c > area d e f
Tactic:
by_cases ef: e = f
Proof state after:
case pos
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : e = f
⊢ area a b c > area d e f

case neg
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
⊢ area a b c > area d e f
Theorem: lt_area_of_lt_base
Proof state before:
case neg
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
⊢ area a b c > area d e f
Tactic:
obtain ⟨ O, dO, eO ⟩ := line_of_pts d e
Proof state after:
case neg.intro.intro
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
⊢ area a b c > area d e f
Theorem: lt_area_of_lt_base
Proof state before:
case neg.intro.intro
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
⊢ area a b c > area d e f
Tactic:
have := not_online_of_triangle dO eO eL fL dL ef
Proof state after:
case neg.intro.intro
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this : ¬online f O
⊢ area a b c > area d e f
Theorem: lt_area_of_lt_base
Proof state before:
case neg.intro.intro
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this : ¬online f O
⊢ area a b c > area d e f
Tactic:
obtain ⟨ g, N, gM, gN, fN, pON ⟩ := parallel_projection fL pLM (not_para_of_online_online eO eL) this
Proof state after:
case neg.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
⊢ area a b c > area d e f
Theorem: lt_area_of_lt_base
Proof state before:
case neg.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
⊢ area a b c > area d e f
Tactic:
have efgd : paragram e f g d L N M O := by splitAll <;> perma only [para] at *
Proof state after:
case neg.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
⊢ area a b c > area d e f
Theorem: lt_area_of_lt_base
Proof state before:
case neg.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
⊢ area a b c > area d e f
Tactic:
perm [(len_ang_area_eq_of_parallelogram efgd).1]
Proof state after:
case neg.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this✝ : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
this : length e f = length d g
⊢ area a b c > area d e f
Theorem: lt_area_of_lt_base
Proof state before:
case neg.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this✝ : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
this : length e f = length d g
⊢ area a b c > area d e f
Tactic:
have dg : d ≠ g := ne_of_ne_len ef this
Proof state after:
case neg.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this✝ : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
this : length e f = length d g
dg : d ≠ g
⊢ area a b c > area d e f
Theorem: lt_area_of_lt_base
Proof state before:
case neg.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this✝ : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
this : length e f = length d g
dg : d ≠ g
⊢ area a b c > area d e f
Tactic:
obtain ⟨ P, bP, dP ⟩ := line_of_pts b d
Proof state after:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this✝ : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
this : length e f = length d g
dg : d ≠ g
P : line
bP : online b P
dP : online d P
⊢ area a b c > area d e f