internlm/Lean-Github huggingface dataset:
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
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
⊢ length b e < length b d
Tactic:
rw [He.2.1, hlen]
Proof state after:
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
⊢ ↑n * length b c < ↑(Nat.succ n) * length b c
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
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
⊢ ↑n * length b c < ↑(Nat.succ n) * length b c
Tactic:
simp
Proof state after:
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
⊢ ↑n * length b c < (↑n + 1) * length b c
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
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
⊢ ↑n * length b c < (↑n + 1) * length b c
Tactic:
linarith [len_pos_of_nq bc]
Proof state after:
no goals
Theorem: rescale_triangle_of_base_inductive
Proof state before:
case inl
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
this : length b e < length b d
h : B b e d
⊢ B b e d
Tactic:
exact h
Proof state after:
no goals
Theorem: rescale_triangle_of_base_inductive
Proof state before:
case inr
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
this : length b e < length b d
h : B e b d
⊢ B b e d
Tactic:
exfalso
Proof state after:
case inr.h
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
this : length b e < length b d
h : B e b d
⊢ False
Theorem: rescale_triangle_of_base_inductive
Proof state before:
case inr.h
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
this : length b e < length b d
h : B e b d
⊢ False
Tactic:
exact not_B324_of_B123_B124 Bbce Bbcd (B124_of_B134_B123 h (B_symm Bbce))
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
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
Bbed : B b e d
⊢ length b c = length e d
Tactic:
have := length_sum_of_B Bbed
Proof state after:
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
Bbed : B b e d
this : length b e + length e d = length b d
⊢ length b c = length e d
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
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
Bbed : B b e d
this : length b e + length e d = length b d
⊢ length b c = length e d
Tactic:
rw [hlen, He.2.1] at this
Proof state after:
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
Bbed : B b e d
this : ↑n * length b c + length e d = ↑(Nat.succ n) * length b c
⊢ length b c = length e d
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
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
Bbed : B b e d
this : ↑n * length b c + length e d = ↑(Nat.succ n) * length b c
⊢ length b c = length e d
Tactic:
simp [one_mul] at this
Proof state after:
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
Bbed : B b e d
this : ↑n * length b c + length e d = (↑n + 1) * length b c
⊢ length b c = length e d
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
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
Bbed : B b e d
this : ↑n * length b c + length e d = (↑n + 1) * length b c
⊢ length b c = length e d
Tactic:
linarith
Proof state after:
no goals
Theorem: rescale_triangle_of_base_B
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
Bbcd : B b c d
aL : ¬online a L
⊢ area a b d = ↑n * area a b c
Tactic:
exact rescale_triangle_of_base_inductive a bL cL aL d dL hlen Bbcd
Proof state after:
no goals
Theorem: rescale_triangle_of_base_notcbd
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
hB : ¬B c b d
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 n1 : n =1
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
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : n = 1
⊢ 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
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : ¬n = 1
⊢ area a b d = ↑n * area a b c
Theorem: rescale_triangle_of_base_notcbd
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
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : ¬n = 1
⊢ area a b d = ↑n * area a b c
Tactic:
have cd: c ≠ d := fun cd => by
  have n0 := length_eq_zero_iff.not.mpr bd
  rw [cd] at hlen; field_simp at hlen; exact n1 hlen
Proof state after:
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
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : ¬n = 1
cd : c ≠ d
⊢ area a b d = ↑n * area a b c
Theorem: rescale_triangle_of_base_notcbd
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
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : ¬n = 1
cd : c ≠ d
⊢ area a b d = ↑n * area a b c
Tactic:
have: length b c < length b d := by
  have := len_pos_of_nq bc
  have n_ge1 := gt1_of_n1_n0 n0 n1; simp [*]
Proof state after:
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
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : ¬n = 1
cd : c ≠ d
this : length b c < length b d
⊢ area a b d = ↑n * area a b c
Theorem: rescale_triangle_of_base_notcbd
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
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : ¬n = 1
cd : c ≠ d
this : length b c < length b d
⊢ area a b d = ↑n * area a b c
Tactic:
have hBs := B_of_three_online_ne_short this bc bd cd bL cL dL
Proof state after:
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
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : ¬n = 1
cd : c ≠ d
this : length b c < length b d
hBs : B b c d ∨ B c b d
⊢ area a b d = ↑n * area a b c
Theorem: rescale_triangle_of_base_notcbd
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
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : ¬n = 1
cd : c ≠ d
this : length b c < length b d
hBs : B b c d ∨ B c b d
⊢ area a b d = ↑n * area a b c
Tactic:
cases hBs with
| inl hBs => exact rescale_triangle_of_base_B a bL cL dL hlen hBs aL
| inr hBs => exfalso; exact hB hBs
Proof state after:
no goals
Theorem: rescale_triangle_of_base_notcbd
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
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : n = 1
⊢ area a b d = ↑n * area a b c
Tactic:
rw [n1] 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 = ↑1 * length b c
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : n = 1
⊢ area a b d = ↑n * area a b c
Theorem: rescale_triangle_of_base_notcbd
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 = ↑1 * length b c
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : n = 1
⊢ area a b d = ↑n * area a b c
Tactic:
rw [n1]
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 = ↑1 * length b c
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : n = 1
⊢ area a b d = ↑1 * area a b c
Theorem: rescale_triangle_of_base_notcbd
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 = ↑1 * length b c
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : n = 1
⊢ area a b d = ↑1 * area a b c
Tactic:
simp [Nat.cast_one] 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
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : n = 1
hlen : length b d = length b c
⊢ area a b d = ↑1 * area a b c
Theorem: rescale_triangle_of_base_notcbd
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
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : n = 1
hlen : length b d = length b c
⊢ area a b d = ↑1 * area a b c
Tactic:
simp [Nat.cast_one]
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
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : n = 1
hlen : length b d = length b c
⊢ area a b d = area a b c
Theorem: rescale_triangle_of_base_notcbd
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
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : n = 1
hlen : length b d = length b c
⊢ area a b d = area a b c
Tactic:
exact (eq_area_of_eq_base_samevertex a bL cL bL dL hlen.symm).symm
Proof state after:
no goals
Theorem: rescale_triangle_of_base_notcbd
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
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : ¬n = 1
cd : c = d
⊢ False
Tactic:
have n0 := length_eq_zero_iff.not.mpr bd
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
hB : ¬B c b d
bc : b ≠ c
n0✝ : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : ¬n = 1
cd : c = d
n0 : ¬length b d = 0
⊢ False
Theorem: rescale_triangle_of_base_notcbd
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
hB : ¬B c b d
bc : b ≠ c
n0✝ : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : ¬n = 1
cd : c = d
n0 : ¬length b d = 0
⊢ False
Tactic:
rw [cd] 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 : length b d = ↑n * length b d
hB : ¬B c b d
bc : b ≠ c
n0✝ : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : ¬n = 1
cd : c = d
n0 : ¬length b d = 0
⊢ False
Theorem: rescale_triangle_of_base_notcbd
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 d
hB : ¬B c b d
bc : b ≠ c
n0✝ : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : ¬n = 1
cd : c = d
n0 : ¬length b d = 0
⊢ False
Tactic:
field_simp 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
hB : ¬B c b d
bc : b ≠ c
n0✝ : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : ¬n = 1
cd : c = d
n0 : ¬length b d = 0
hlen : n = 1
⊢ False
Theorem: rescale_triangle_of_base_notcbd
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
hB : ¬B c b d
bc : b ≠ c
n0✝ : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : ¬n = 1
cd : c = d
n0 : ¬length b d = 0
hlen : n = 1
⊢ False
Tactic:
exact n1 hlen
Proof state after:
no goals
Theorem: rescale_triangle_of_base_notcbd
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
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : ¬n = 1
cd : c ≠ d
⊢ length b c < length b d
Tactic:
have := len_pos_of_nq bc
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
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : ¬n = 1
cd : c ≠ d
this : 0 < length b c
⊢ length b c < length b d
Theorem: rescale_triangle_of_base_notcbd
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
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : ¬n = 1
cd : c ≠ d
this : 0 < length b c
⊢ length b c < length b d
Tactic:
have n_ge1 := gt1_of_n1_n0 n0 n1
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
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : ¬n = 1
cd : c ≠ d
this : 0 < length b c
n_ge1 : n > 1
⊢ length b c < length b d
Theorem: rescale_triangle_of_base_notcbd
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
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : ¬n = 1
cd : c ≠ d
this : 0 < length b c
n_ge1 : n > 1
⊢ length b c < length b d
Tactic:
simp [*]
Proof state after:
no goals
Theorem: rescale_triangle_of_base_notcbd
Proof state before:
case neg.inl
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
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : ¬n = 1
cd : c ≠ d
this : length b c < length b d
hBs : B b c d
⊢ area a b d = ↑n * area a b c
Tactic:
exact rescale_triangle_of_base_B a bL cL dL hlen hBs aL
Proof state after:
no goals
Theorem: rescale_triangle_of_base_notcbd
Proof state before:
case neg.inr
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
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : ¬n = 1
cd : c ≠ d
this : length b c < length b d
hBs : B c b d
⊢ area a b d = ↑n * area a b c
Tactic:
exfalso
Proof state after:
case neg.inr.h
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
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : ¬n = 1
cd : c ≠ d
this : length b c < length b d
hBs : B c b d
⊢ False
Theorem: rescale_triangle_of_base_notcbd
Proof state before:
case neg.inr.h
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
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : ¬n = 1
cd : c ≠ d
this : length b c < length b d
hBs : B c b d
⊢ False
Tactic:
exact hB hBs
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
⊢ area a b d = ↑n * area a b c
Tactic:
by_cases bc : b = c
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
⊢ 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
⊢ 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
⊢ area a b d = ↑n * area a b c
Tactic:
by_cases n0 : n = 0
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
⊢ 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
⊢ 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
⊢ area a b d = ↑n * area a b c
Tactic:
have bd: b ≠ d := fun bd => by
  rw [length_eq_zero_iff.mpr bd, zero_eq_mul, Nat.cast_eq_zero] at hlen
  cases hlen with
  | inl hlen => exact n0 hlen
  | inr hlen => exact bc (length_eq_zero_iff.mp hlen)
Proof state after:
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