internlm/Lean-Github huggingface dataset:
Theorem: rescale_triangle_of_base
Proof state before:
case neg
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
bc : ¬b = c
n0 : ¬n = 0
bd : b ≠ d
⊢ area a b d = ↑n * area a b c
Tactic:
by_cases aL : online a L
Proof state after:
case pos
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
bc : ¬b = c
n0 : ¬n = 0
bd : b ≠ d
aL : online a L
⊢ area a b d = ↑n * area a b c

case neg
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
bc : ¬b = c
n0 : ¬n = 0
bd : b ≠ d
aL : ¬online a L
⊢ area a b d = ↑n * area a b c
Theorem: rescale_triangle_of_base
Proof state before:
case neg
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
bc : ¬b = c
n0 : ¬n = 0
bd : b ≠ d
aL : ¬online a L
⊢ area a b d = ↑n * area a b c
Tactic:
by_cases h_B_cbd : B c b d
Proof state after:
case pos
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
bc : ¬b = c
n0 : ¬n = 0
bd : b ≠ d
aL : ¬online a L
h_B_cbd : B c b d
⊢ area a b d = ↑n * area a b c

case neg
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
bc : ¬b = c
n0 : ¬n = 0
bd : b ≠ d
aL : ¬online a L
h_B_cbd : ¬B c b d
⊢ area a b d = ↑n * area a b c
Theorem: rescale_triangle_of_base
Proof state before:
case neg
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
bc : ¬b = c
n0 : ¬n = 0
bd : b ≠ d
aL : ¬online a L
h_B_cbd : ¬B c b d
⊢ area a b d = ↑n * area a b c
Tactic:
exact rescale_triangle_of_base_notcbd a bL cL dL hlen h_B_cbd bc n0 bd aL
Proof state after:
no goals
Theorem: rescale_triangle_of_base
Proof state before:
case pos
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
bc : b = c
⊢ area a b d = ↑n * area a b c
Tactic:
rw [length_eq_zero_iff.mpr bc, mul_zero] at hlen
Proof state after:
case pos
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = 0
bc : b = c
⊢ area a b d = ↑n * area a b c
Theorem: rescale_triangle_of_base
Proof state before:
case pos
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = 0
bc : b = c
⊢ area a b d = ↑n * area a b c
Tactic:
have := length_eq_zero_iff.mp hlen
Proof state after:
case pos
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = 0
bc : b = c
this : b = d
⊢ area a b d = ↑n * area a b c
Theorem: rescale_triangle_of_base
Proof state before:
case pos
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = 0
bc : b = c
this : b = d
⊢ area a b d = ↑n * area a b c
Tactic:
rw [area_of_eq a b d (by tauto), area_of_eq a b c (by tauto)]
Proof state after:
case pos
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = 0
bc : b = c
this : b = d
⊢ 0 = ↑n * 0
Theorem: rescale_triangle_of_base
Proof state before:
case pos
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = 0
bc : b = c
this : b = d
⊢ 0 = ↑n * 0
Tactic:
simp [mul_zero]
Proof state after:
no goals
Theorem: rescale_triangle_of_base
Proof state before:
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = 0
bc : b = c
this : b = d
⊢ a = b ∨ a = d ∨ b = d
Tactic:
tauto
Proof state after:
no goals
Theorem: rescale_triangle_of_base
Proof state before:
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = 0
bc : b = c
this : b = d
⊢ a = b ∨ a = c ∨ b = c
Tactic:
tauto
Proof state after:
no goals
Theorem: rescale_triangle_of_base
Proof state before:
case pos
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
bc : ¬b = c
n0 : n = 0
⊢ area a b d = ↑n * area a b c
Tactic:
rw [n0] at hlen
Proof state after:
case pos
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑0 * length b c
bc : ¬b = c
n0 : n = 0
⊢ area a b d = ↑n * area a b c
Theorem: rescale_triangle_of_base
Proof state before:
case pos
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑0 * length b c
bc : ¬b = c
n0 : n = 0
⊢ area a b d = ↑n * area a b c
Tactic:
simp [Nat.cast_zero] at hlen
Proof state after:
case pos
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
bc : ¬b = c
n0 : n = 0
hlen : length b d = 0
⊢ area a b d = ↑n * area a b c
Theorem: rescale_triangle_of_base
Proof state before:
case pos
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
bc : ¬b = c
n0 : n = 0
hlen : length b d = 0
⊢ area a b d = ↑n * area a b c
Tactic:
have := length_eq_zero_iff.mp hlen
Proof state after:
case pos
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
bc : ¬b = c
n0 : n = 0
hlen : length b d = 0
this : b = d
⊢ area a b d = ↑n * area a b c
Theorem: rescale_triangle_of_base
Proof state before:
case pos
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
bc : ¬b = c
n0 : n = 0
hlen : length b d = 0
this : b = d
⊢ area a b d = ↑n * area a b c
Tactic:
rw [n0, area_of_eq a b d (by tauto)]
Proof state after:
case pos
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
bc : ¬b = c
n0 : n = 0
hlen : length b d = 0
this : b = d
⊢ 0 = ↑0 * area a b c
Theorem: rescale_triangle_of_base
Proof state before:
case pos
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
bc : ¬b = c
n0 : n = 0
hlen : length b d = 0
this : b = d
⊢ 0 = ↑0 * area a b c
Tactic:
simp [Nat.cast_zero]
Proof state after:
no goals
Theorem: rescale_triangle_of_base
Proof state before:
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
bc : ¬b = c
n0 : n = 0
hlen : length b d = 0
this : b = d
⊢ a = b ∨ a = d ∨ b = d
Tactic:
tauto
Proof state after:
no goals
Theorem: rescale_triangle_of_base
Proof state before:
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
bc : ¬b = c
n0 : ¬n = 0
bd : b = d
⊢ False
Tactic:
rw [length_eq_zero_iff.mpr bd, zero_eq_mul, Nat.cast_eq_zero] at hlen
Proof state after:
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : n = 0 ∨ length b c = 0
bc : ¬b = c
n0 : ¬n = 0
bd : b = d
⊢ False
Theorem: rescale_triangle_of_base
Proof state before:
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : n = 0 ∨ length b c = 0
bc : ¬b = c
n0 : ¬n = 0
bd : b = d
⊢ False
Tactic:
cases hlen with
| inl hlen => exact n0 hlen
| inr hlen => exact bc (length_eq_zero_iff.mp hlen)
Proof state after:
no goals
Theorem: rescale_triangle_of_base
Proof state before:
case inl
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
bc : ¬b = c
n0 : ¬n = 0
bd : b = d
hlen : n = 0
⊢ False
Tactic:
exact n0 hlen
Proof state after:
no goals
Theorem: rescale_triangle_of_base
Proof state before:
case inr
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
bc : ¬b = c
n0 : ¬n = 0
bd : b = d
hlen : length b c = 0
⊢ False
Tactic:
exact bc (length_eq_zero_iff.mp hlen)
Proof state after:
no goals
Theorem: rescale_triangle_of_base
Proof state before:
case pos
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
bc : ¬b = c
n0 : ¬n = 0
bd : b ≠ d
aL : online a L
⊢ area a b d = ↑n * area a b c
Tactic:
perm [(area_zero_iff_online bc bL cL).mpr aL]
Proof state after:
case pos
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
bc : ¬b = c
n0 : ¬n = 0
bd : b ≠ d
aL : online a L
this : area a b c = 0
⊢ area a b d = ↑n * area a b c
Theorem: rescale_triangle_of_base
Proof state before:
case pos
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
bc : ¬b = c
n0 : ¬n = 0
bd : b ≠ d
aL : online a L
this : area a b c = 0
⊢ area a b d = ↑n * area a b c
Tactic:
rw [this]
Proof state after:
case pos
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
bc : ¬b = c
n0 : ¬n = 0
bd : b ≠ d
aL : online a L
this : area a b c = 0
⊢ area a b d = ↑n * 0
Theorem: rescale_triangle_of_base
Proof state before:
case pos
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
bc : ¬b = c
n0 : ¬n = 0
bd : b ≠ d
aL : online a L
this : area a b c = 0
⊢ area a b d = ↑n * 0
Tactic:
linperm [(area_zero_iff_online bd bL dL).mpr aL]
Proof state after:
no goals
Theorem: rescale_triangle_of_base
Proof state before:
case pos
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
bc : ¬b = c
n0 : ¬n = 0
bd : b ≠ d
aL : ¬online a L
h_B_cbd : B c b d
⊢ area a b d = ↑n * area a b c
Tactic:
obtain ⟨ e, He ⟩ := rescale_length 2 cL bL
Proof state after:
case pos.intro
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
bc : ¬b = c
n0 : ¬n = 0
bd : b ≠ d
aL : ¬online a L
h_B_cbd : B c b d
e : point
He : online e L ∧ length c e = ↑2 * length c b ∧ (2 ≥ 2 ∧ c ≠ b → B c b e)
⊢ area a b d = ↑n * area a b c
Theorem: rescale_triangle_of_base
Proof state before:
case pos.intro
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
bc : ¬b = c
n0 : ¬n = 0
bd : b ≠ d
aL : ¬online a L
h_B_cbd : B c b d
e : point
He : online e L ∧ length c e = ↑2 * length c b ∧ (2 ≥ 2 ∧ c ≠ b → B c b e)
⊢ area a b d = ↑n * area a b c
Tactic:
have Bcbe := He.2.2 ⟨ by simp [ge_iff_le], fun cb => bc cb.symm⟩
Proof state after:
case pos.intro
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
bc : ¬b = c
n0 : ¬n = 0
bd : b ≠ d
aL : ¬online a L
h_B_cbd : B c b d
e : point
He : online e L ∧ length c e = ↑2 * length c b ∧ (2 ≥ 2 ∧ c ≠ b → B c b e)
Bcbe : B c b e
⊢ area a b d = ↑n * area a b c
Theorem: rescale_triangle_of_base
Proof state before:
case pos.intro
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
bc : ¬b = c
n0 : ¬n = 0
bd : b ≠ d
aL : ¬online a L
h_B_cbd : B c b d
e : point
He : online e L ∧ length c e = ↑2 * length c b ∧ (2 ≥ 2 ∧ c ≠ b → B c b e)
Bcbe : B c b e
⊢ area a b d = ↑n * area a b c
Tactic:
have Lbe : length b e = length b c := by
  perm [length_sum_of_B Bcbe]
  rw [He.2.1] at this; norm_cast at this; linperm
Proof state after:
case pos.intro
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
bc : ¬b = c
n0 : ¬n = 0
bd : b ≠ d
aL : ¬online a L
h_B_cbd : B c b d
e : point
He : online e L ∧ length c e = ↑2 * length c b ∧ (2 ≥ 2 ∧ c ≠ b → B c b e)
Bcbe : B c b e
Lbe : length b e = length b c
⊢ area a b d = ↑n * area a b c
Theorem: rescale_triangle_of_base
Proof state before:
case pos.intro
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
bc : ¬b = c
n0 : ¬n = 0
bd : b ≠ d
aL : ¬online a L
h_B_cbd : B c b d
e : point
He : online e L ∧ length c e = ↑2 * length c b ∧ (2 ≥ 2 ∧ c ≠ b → B c b e)
Bcbe : B c b e
Lbe : length b e = length b c
⊢ area a b d = ↑n * area a b c
Tactic:
rw [← Lbe] at hlen
Proof state after:
case pos.intro
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
bc : ¬b = c
n0 : ¬n = 0
bd : b ≠ d
aL : ¬online a L
h_B_cbd : B c b d
e : point
hlen : length b d = ↑n * length b e
He : online e L ∧ length c e = ↑2 * length c b ∧ (2 ≥ 2 ∧ c ≠ b → B c b e)
Bcbe : B c b e
Lbe : length b e = length b c
⊢ area a b d = ↑n * area a b c
Theorem: rescale_triangle_of_base
Proof state before:
case pos.intro
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
bc : ¬b = c
n0 : ¬n = 0
bd : b ≠ d
aL : ¬online a L
h_B_cbd : B c b d
e : point
hlen : length b d = ↑n * length b e
He : online e L ∧ length c e = ↑2 * length c b ∧ (2 ≥ 2 ∧ c ≠ b → B c b e)
Bcbe : B c b e
Lbe : length b e = length b c
⊢ area a b d = ↑n * area a b c
Tactic:
have := not_B324_of_B123_B124 Bcbe h_B_cbd
Proof state after:
case pos.intro
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
bc : ¬b = c
n0 : ¬n = 0
bd : b ≠ d
aL : ¬online a L
h_B_cbd : B c b d
e : point
hlen : length b d = ↑n * length b e
He : online e L ∧ length c e = ↑2 * length c b ∧ (2 ≥ 2 ∧ c ≠ b → B c b e)
Bcbe : B c b e
Lbe : length b e = length b c
this : ¬B e b d
⊢ area a b d = ↑n * area a b c
Theorem: rescale_triangle_of_base
Proof state before:
case pos.intro
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
bc : ¬b = c
n0 : ¬n = 0
bd : b ≠ d
aL : ¬online a L
h_B_cbd : B c b d
e : point
hlen : length b d = ↑n * length b e
He : online e L ∧ length c e = ↑2 * length c b ∧ (2 ≥ 2 ∧ c ≠ b → B c b e)
Bcbe : B c b e
Lbe : length b e = length b c
this : ¬B e b d
⊢ area a b d = ↑n * area a b c
Tactic:
rw [rescale_triangle_of_base_notcbd a bL He.1 dL hlen this (ne_23_of_B Bcbe) n0 bd aL]
Proof state after:
case pos.intro
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
bc : ¬b = c
n0 : ¬n = 0
bd : b ≠ d
aL : ¬online a L
h_B_cbd : B c b d
e : point
hlen : length b d = ↑n * length b e
He : online e L ∧ length c e = ↑2 * length c b ∧ (2 ≥ 2 ∧ c ≠ b → B c b e)
Bcbe : B c b e
Lbe : length b e = length b c
this : ¬B e b d
⊢ ↑n * area a b e = ↑n * area a b c
Theorem: rescale_triangle_of_base
Proof state before:
case pos.intro
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
bc : ¬b = c
n0 : ¬n = 0
bd : b ≠ d
aL : ¬online a L
h_B_cbd : B c b d
e : point
hlen : length b d = ↑n * length b e
He : online e L ∧ length c e = ↑2 * length c b ∧ (2 ≥ 2 ∧ c ≠ b → B c b e)
Bcbe : B c b e
Lbe : length b e = length b c
this : ¬B e b d
⊢ ↑n * area a b e = ↑n * area a b c
Tactic:
rw [eq_area_of_eq_base_samevertex a bL He.1 bL cL Lbe]
Proof state after:
no goals
Theorem: rescale_triangle_of_base
Proof state before:
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
bc : ¬b = c
n0 : ¬n = 0
bd : b ≠ d
aL : ¬online a L
h_B_cbd : B c b d
e : point
He : online e L ∧ length c e = ↑2 * length c b ∧ (2 ≥ 2 ∧ c ≠ b → B c b e)
⊢ 2 ≥ 2
Tactic:
simp [ge_iff_le]
Proof state after:
no goals
Theorem: rescale_triangle_of_base
Proof state before:
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
bc : ¬b = c
n0 : ¬n = 0
bd : b ≠ d
aL : ¬online a L
h_B_cbd : B c b d
e : point
He : online e L ∧ length c e = ↑2 * length c b ∧ (2 ≥ 2 ∧ c ≠ b → B c b e)
Bcbe : B c b e
⊢ length b e = length b c
Tactic:
perm [length_sum_of_B Bcbe]
Proof state after:
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
bc : ¬b = c
n0 : ¬n = 0
bd : b ≠ d
aL : ¬online a L
h_B_cbd : B c b d
e : point
He : online e L ∧ length c e = ↑2 * length c b ∧ (2 ≥ 2 ∧ c ≠ b → B c b e)
Bcbe : B c b e
this : length b c + length b e = length c e
⊢ length b e = length b c
Theorem: rescale_triangle_of_base
Proof state before:
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
bc : ¬b = c
n0 : ¬n = 0
bd : b ≠ d
aL : ¬online a L
h_B_cbd : B c b d
e : point
He : online e L ∧ length c e = ↑2 * length c b ∧ (2 ≥ 2 ∧ c ≠ b → B c b e)
Bcbe : B c b e
this : length b c + length b e = length c e
⊢ length b e = length b c
Tactic:
rw [He.2.1] at this
Proof state after:
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
bc : ¬b = c
n0 : ¬n = 0
bd : b ≠ d
aL : ¬online a L
h_B_cbd : B c b d
e : point
He : online e L ∧ length c e = ↑2 * length c b ∧ (2 ≥ 2 ∧ c ≠ b → B c b e)
Bcbe : B c b e
this : length b c + length b e = ↑2 * length c b
⊢ length b e = length b c
Theorem: rescale_triangle_of_base
Proof state before:
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
bc : ¬b = c
n0 : ¬n = 0
bd : b ≠ d
aL : ¬online a L
h_B_cbd : B c b d
e : point
He : online e L ∧ length c e = ↑2 * length c b ∧ (2 ≥ 2 ∧ c ≠ b → B c b e)
Bcbe : B c b e
this : length b c + length b e = ↑2 * length c b
⊢ length b e = length b c
Tactic:
norm_cast at this
Proof state after:
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
bc : ¬b = c
n0 : ¬n = 0
bd : b ≠ d
aL : ¬online a L
h_B_cbd : B c b d
e : point
He : online e L ∧ length c e = ↑2 * length c b ∧ (2 ≥ 2 ∧ c ≠ b → B c b e)
Bcbe : B c b e
this : length b c + length b e = 2 * length c b
⊢ length b e = length b c
Theorem: rescale_triangle_of_base
Proof state before:
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
bc : ¬b = c
n0 : ¬n = 0
bd : b ≠ d
aL : ¬online a L
h_B_cbd : B c b d
e : point
He : online e L ∧ length c e = ↑2 * length c b ∧ (2 ≥ 2 ∧ c ≠ b → B c b e)
Bcbe : B c b e
this : length b c + length b e = 2 * length c b
⊢ length b e = length b c
Tactic:
linperm
Proof state after:
no goals
Theorem: lt_area_of_lt_base_sameedge_Bbfc
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
hB : B b f c
bc : b ≠ c
bf : b ≠ f
cf : c ≠ f
aL : ¬online a L
⊢ length b c > length b f → area a b c > area a b f
Tactic:
have := (area_add_iff_B bf cf.symm bc.symm bL fL cL aL).mp hB
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
hB : B b f c
bc : b ≠ c
bf : b ≠ f
cf : c ≠ f
aL : ¬online a L
this : area a b f + area a c f = area a b c
⊢ length b c > length b f → area a b c > area a b f
Theorem: lt_area_of_lt_base_sameedge_Bbfc
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
hB : B b f c
bc : b ≠ c
bf : b ≠ f
cf : c ≠ f
aL : ¬online a L
this : area a b f + area a c f = area a b c
⊢ length b c > length b f → area a b c > area a b f
Tactic:
intro
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
hB : B b f c
bc : b ≠ c
bf : b ≠ f
cf : c ≠ f
aL : ¬online a L
this : area a b f + area a c f = area a b c
a✝ : length b c > length b f
⊢ area a b c > area a b f
Theorem: lt_area_of_lt_base_sameedge_Bbfc
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
hB : B b f c
bc : b ≠ c
bf : b ≠ f
cf : c ≠ f
aL : ¬online a L
this : area a b f + area a c f = area a b c
a✝ : length b c > length b f
⊢ area a b c > area a b f
Tactic:
rw [← this]
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
hB : B b f c
bc : b ≠ c
bf : b ≠ f
cf : c ≠ f
aL : ¬online a L
this : area a b f + area a c f = area a b c
a✝ : length b c > length b f
⊢ area a b f + area a c f > area a b f
Theorem: lt_area_of_lt_base_sameedge_Bbfc
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
hB : B b f c
bc : b ≠ c
bf : b ≠ f
cf : c ≠ f
aL : ¬online a L
this : area a b f + area a c f = area a b c
a✝ : length b c > length b f
⊢ area a b f + area a c f > area a b f
Tactic:
simp [gt_iff_lt, lt_add_iff_pos_right]
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
hB : B b f c
bc : b ≠ c
bf : b ≠ f
cf : c ≠ f
aL : ¬online a L
this : area a b f + area a c f = area a b c
a✝ : length b c > length b f
⊢ 0 < area a c f
Theorem: lt_area_of_lt_base_sameedge_Bbfc
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
hB : B b f c
bc : b ≠ c
bf : b ≠ f
cf : c ≠ f
aL : ¬online a L
this : area a b f + area a c f = area a b c
a✝ : length b c > length b f
⊢ 0 < area a c f
Tactic:
have : area a c f ≠ 0 := by perma [(area_zero_iff_online cf cL fL).not.mpr aL]
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
hB : B b f c
bc : b ≠ c
bf : b ≠ f
cf : c ≠ f
aL : ¬online a L
this✝ : area a b f + area a c f = area a b c
a✝ : length b c > length b f
this : area a c f ≠ 0
⊢ 0 < area a c f
Theorem: lt_area_of_lt_base_sameedge_Bbfc
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
hB : B b f c
bc : b ≠ c
bf : b ≠ f
cf : c ≠ f
aL : ¬online a L
this✝ : area a b f + area a c f = area a b c
a✝ : length b c > length b f
this : area a c f ≠ 0
⊢ 0 < area a c f
Tactic:
exact (Ne.symm this).lt_of_le (area_nonneg a c f)
Proof state after:
no goals
Theorem: lt_area_of_lt_base_sameedge_Bbfc
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
hB : B b f c
bc : b ≠ c
bf : b ≠ f
cf : c ≠ f
aL : ¬online a L
this : area a b f + area a c f = area a b c
a✝ : length b c > length b f
⊢ area a c f ≠ 0
Tactic:
perma [(area_zero_iff_online cf cL fL).not.mpr aL]
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
⊢ 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
hB : ¬B f b c
hlen : length b c > length b 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 c > length b f
⊢ area a b c > area a b f
Tactic:
simp [gt_iff_lt] 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 : length b f < length b c
⊢ area a b c > area a b f