internlm/Lean-Github huggingface dataset:
Theorem: rescale_length
Proof state before:
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
hn : ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)
n0 : n = 0
⊢ length a b = ↑(Nat.succ 0) * length a b ∧ (Nat.succ 0 ≥ 2 ∧ a ≠ b → B a b b)
Tactic:
simp
Proof state after:
no goals
Theorem: rescale_length
Proof state before:
case pos
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
hn : ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)
n0 : ¬n = 0
n1 : n = 1
⊢ ∃ c, online c L ∧ length a c = ↑(Nat.succ n) * length a b ∧ (Nat.succ n ≥ 2 ∧ a ≠ b → B a b c)
Tactic:
obtain ⟨ e, He ⟩ := length_eq_B_of_ne_four ab ab
Proof state after:
case pos.intro
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
hn : ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)
n0 : ¬n = 0
n1 : n = 1
e : point
He : B a b e ∧ length a b = length b e
⊢ ∃ c, online c L ∧ length a c = ↑(Nat.succ n) * length a b ∧ (Nat.succ n ≥ 2 ∧ a ≠ b → B a b c)
Theorem: rescale_length
Proof state before:
case pos.intro
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
hn : ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)
n0 : ¬n = 0
n1 : n = 1
e : point
He : B a b e ∧ length a b = length b e
⊢ ∃ c, online c L ∧ length a c = ↑(Nat.succ n) * length a b ∧ (Nat.succ n ≥ 2 ∧ a ≠ b → B a b c)
Tactic:
use e
Proof state after:
case pos.intro
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
hn : ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)
n0 : ¬n = 0
n1 : n = 1
e : point
He : B a b e ∧ length a b = length b e
⊢ online e L ∧ length a e = ↑(Nat.succ n) * length a b ∧ (Nat.succ n ≥ 2 ∧ a ≠ b → B a b e)
Theorem: rescale_length
Proof state before:
case pos.intro
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
hn : ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)
n0 : ¬n = 0
n1 : n = 1
e : point
He : B a b e ∧ length a b = length b e
⊢ online e L ∧ length a e = ↑(Nat.succ n) * length a b ∧ (Nat.succ n ≥ 2 ∧ a ≠ b → B a b e)
Tactic:
simp_rw [(length_sum_of_B He.1).symm, He.2, n1]
Proof state after:
case pos.intro
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
hn : ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)
n0 : ¬n = 0
n1 : n = 1
e : point
He : B a b e ∧ length a b = length b e
⊢ online e L ∧ length b e + length b e = ↑(Nat.succ 1) * length b e ∧ (True ∧ a ≠ b → B a b e)
Theorem: rescale_length
Proof state before:
case pos.intro
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
hn : ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)
n0 : ¬n = 0
n1 : n = 1
e : point
He : B a b e ∧ length a b = length b e
⊢ online e L ∧ length b e + length b e = ↑(Nat.succ 1) * length b e ∧ (True ∧ a ≠ b → B a b e)
Tactic:
simp
Proof state after:
case pos.intro
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
hn : ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)
n0 : ¬n = 0
n1 : n = 1
e : point
He : B a b e ∧ length a b = length b e
⊢ online e L ∧ length b e + length b e = (1 + 1) * length b e ∧ (¬a = b → B a b e)
Theorem: rescale_length
Proof state before:
case pos.intro
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
hn : ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)
n0 : ¬n = 0
n1 : n = 1
e : point
He : B a b e ∧ length a b = length b e
⊢ online e L ∧ length b e + length b e = (1 + 1) * length b e ∧ (¬a = b → B a b e)
Tactic:
ring_nf
Proof state after:
case pos.intro
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
hn : ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)
n0 : ¬n = 0
n1 : n = 1
e : point
He : B a b e ∧ length a b = length b e
⊢ online e L ∧ True ∧ (¬a = b → B a b e)
Theorem: rescale_length
Proof state before:
case pos.intro
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
hn : ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)
n0 : ¬n = 0
n1 : n = 1
e : point
He : B a b e ∧ length a b = length b e
⊢ online e L ∧ True ∧ (¬a = b → B a b e)
Tactic:
refine' ⟨ online_3_of_B He.1 aL bL, (by tauto), fun _ => He.1 ⟩
Proof state after:
no goals
Theorem: rescale_length
Proof state before:
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
hn : ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)
n0 : ¬n = 0
n1 : n = 1
e : point
He : B a b e ∧ length a b = length b e
⊢ True
Tactic:
tauto
Proof state after:
no goals
Theorem: rescale_length
Proof state before:
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
n0 : ¬n = 0
n1 : ¬n = 1
d : point
Hd : online d L ∧ length a d = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b d)
⊢ a ≠ d
Tactic:
apply nq_of_len_pos
Proof state after:
case length
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
n0 : ¬n = 0
n1 : ¬n = 1
d : point
Hd : online d L ∧ length a d = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b d)
⊢ 0 < length a d
Theorem: rescale_length
Proof state before:
case length
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
n0 : ¬n = 0
n1 : ¬n = 1
d : point
Hd : online d L ∧ length a d = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b d)
⊢ 0 < length a d
Tactic:
rw [Hd.2.1]
Proof state after:
case length
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
n0 : ¬n = 0
n1 : ¬n = 1
d : point
Hd : online d L ∧ length a d = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b d)
⊢ 0 < ↑n * length a b
Theorem: rescale_length
Proof state before:
case length
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
n0 : ¬n = 0
n1 : ¬n = 1
d : point
Hd : online d L ∧ length a d = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b d)
⊢ 0 < ↑n * length a b
Tactic:
simp [Nat.pos_of_ne_zero n0, zero_lt_mul_left, Nat.cast_pos]
Proof state after:
case length
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
n0 : ¬n = 0
n1 : ¬n = 1
d : point
Hd : online d L ∧ length a d = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b d)
⊢ 0 < length a b
Theorem: rescale_length
Proof state before:
case length
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
n0 : ¬n = 0
n1 : ¬n = 1
d : point
Hd : online d L ∧ length a d = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b d)
⊢ 0 < length a b
Tactic:
exact len_pos_of_nq ab
Proof state after:
no goals
Theorem: rescale_length
Proof state before:
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
n0 : ¬n = 0
n1 : ¬n = 1
d : point
Hd : online d L ∧ length a d = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b d)
ad : a ≠ d
e : point
He : B a d e ∧ length a b = length d e
this : B a b d
⊢ True
Tactic:
tauto
Proof state after:
no goals
Theorem: rescale_triangle_of_base_inductive
Proof state before:
case zero
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
⊢ ∀ (d : point), online d L → length b d = ↑Nat.zero * length b c → B b c d → area a b d = ↑Nat.zero * area a b c
Tactic:
simp
Proof state after:
case zero
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
⊢ ∀ (d : point), online d L → length b d = 0 → B b c d → area a b d = 0
Theorem: rescale_triangle_of_base_inductive
Proof state before:
case zero
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
⊢ ∀ (d : point), online d L → length b d = 0 → B b c d → area a b d = 0
Tactic:
intros d _ hlen _
Proof state after:
case zero
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
d : point
a✝¹ : online d L
hlen : length b d = 0
a✝ : B b c d
⊢ area a b d = 0
Theorem: rescale_triangle_of_base_inductive
Proof state before:
case zero
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
d : point
a✝¹ : online d L
hlen : length b d = 0
a✝ : B b c d
⊢ area a b d = 0
Tactic:
rw [length_eq_zero_iff.mp hlen, area_of_eq a d d (by tauto)]
Proof state after:
no goals
Theorem: rescale_triangle_of_base_inductive
Proof state before:
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
d : point
a✝¹ : online d L
hlen : length b d = 0
a✝ : B b c d
⊢ a = d ∨ a = d ∨ d = d
Tactic:
tauto
Proof state after:
no goals
Theorem: rescale_triangle_of_base_inductive
Proof state before:
case succ
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
⊢ ∀ (d : point),
    online d L → length b d = ↑(Nat.succ n) * length b c → B b c d → area a b d = ↑(Nat.succ n) * area a b c
Tactic:
intros d dL hlen Bbcd
Proof state after:
case succ
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
⊢ area a b d = ↑(Nat.succ n) * area a b c
Theorem: rescale_triangle_of_base_inductive
Proof state before:
case succ
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
⊢ area a b d = ↑(Nat.succ n) * area a b c
Tactic:
have bc := ne_12_of_B Bbcd
Proof state after:
case succ
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
⊢ area a b d = ↑(Nat.succ n) * area a b c
Theorem: rescale_triangle_of_base_inductive
Proof state before:
case succ
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
⊢ area a b d = ↑(Nat.succ n) * area a b c
Tactic:
have bd := ne_13_of_B Bbcd
Proof state after:
case succ
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
⊢ area a b d = ↑(Nat.succ n) * area a b c
Theorem: rescale_triangle_of_base_inductive
Proof state before:
case succ
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
⊢ area a b d = ↑(Nat.succ n) * area a b c
Tactic:
have cd := ne_23_of_B Bbcd
Proof state after:
case succ
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
⊢ area a b d = ↑(Nat.succ n) * area a b c
Theorem: rescale_triangle_of_base_inductive
Proof state before:
case succ
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
⊢ area a b d = ↑(Nat.succ n) * area a b c
Tactic:
by_cases n0 : n = 0
Proof state after:
case pos
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : n = 0
⊢ area a b d = ↑(Nat.succ n) * area a b c

case neg
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
⊢ area a b d = ↑(Nat.succ n) * area a b c
Theorem: rescale_triangle_of_base_inductive
Proof state before:
case neg
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
⊢ area a b d = ↑(Nat.succ n) * area a b c
Tactic:
by_cases n1 : n = 1
Proof state after:
case pos
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : n = 1
⊢ area a b d = ↑(Nat.succ n) * area a b c

case neg
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
⊢ area a b d = ↑(Nat.succ n) * area a b c
Theorem: rescale_triangle_of_base_inductive
Proof state before:
case neg
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
⊢ area a b d = ↑(Nat.succ n) * area a b c
Tactic:
simp [Nat.cast_succ]
Proof state after:
case neg
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
⊢ area a b d = (↑n + 1) * area a b c
Theorem: rescale_triangle_of_base_inductive
Proof state before:
case neg
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
⊢ area a b d = (↑n + 1) * area a b c
Tactic:
rw [add_mul]
Proof state after:
case neg
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
⊢ area a b d = ↑n * area a b c + 1 * area a b c
Theorem: rescale_triangle_of_base_inductive
Proof state before:
case neg
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
⊢ area a b d = ↑n * area a b c + 1 * area a b c
Tactic:
simp [one_mul]
Proof state after:
case neg
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
⊢ area a b d = ↑n * area a b c + area a b c
Theorem: rescale_triangle_of_base_inductive
Proof state before:
case neg
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
⊢ area a b d = ↑n * area a b c + area a b c
Tactic:
obtain ⟨ e, He ⟩ := rescale_length n bL cL
Proof state after:
case neg.intro
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
⊢ area a b d = ↑n * area a b c + area a b c
Theorem: rescale_triangle_of_base_inductive
Proof state before:
case neg.intro
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
⊢ area a b d = ↑n * area a b c + area a b c
Tactic:
have Bbce := He.2.2 ⟨ ge2_of_n1_n0 n0 n1, bc ⟩
Proof state after:
case neg.intro
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
Bbce : B b c e
⊢ area a b d = ↑n * area a b c + area a b c
Theorem: rescale_triangle_of_base_inductive
Proof state before:
case neg.intro
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
Bbce : B b c e
⊢ area a b d = ↑n * area a b c + area a b c
Tactic:
rw [← hn e He.1 He.2.1 Bbce]
Proof state after:
case neg.intro
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
Bbce : B b c e
⊢ area a b d = area a b e + area a b c
Theorem: rescale_triangle_of_base_inductive
Proof state before:
case neg.intro
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
Bbce : B b c e
⊢ area a b d = area a b e + area a b c
Tactic:
have be := ne_13_of_B Bbce
Proof state after:
case neg.intro
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
Bbce : B b c e
be : b ≠ e
⊢ area a b d = area a b e + area a b c
Theorem: rescale_triangle_of_base_inductive
Proof state before:
case neg.intro
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
Bbce : B b c e
be : b ≠ e
⊢ area a b d = area a b e + area a b c
Tactic:
have ed : e ≠ d := fun ed => by
  have := He.2.1; rw [ed, hlen] at this; simp at this
  exact bc (length_eq_zero_iff.mp this)
Proof state after:
case neg.intro
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
Bbce : B b c e
be : b ≠ e
ed : e ≠ d
⊢ area a b d = area a b e + area a b c