internlm/Lean-Github huggingface dataset:
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
ed : e ≠ d
⊢ area a b d = area a b e + area a b c
Tactic:
have Bbed : B b e d := by
  have: length b e < length b d := by rw [He.2.1, hlen]; simp; linarith [len_pos_of_nq bc]
  have := B_of_three_online_ne_short this be bd ed bL He.1 dL
  
  cases this with
  | inl h => exact h
  | inr h =>
    exfalso
    exact not_B324_of_B123_B124 Bbce Bbcd (B124_of_B134_B123 h (B_symm 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
ed : e ≠ d
Bbed : B b e d
⊢ 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
ed : e ≠ d
Bbed : B b e d
⊢ area a b d = area a b e + area a b c
Tactic:
rw [((area_add_iff_B be ed bd.symm bL He.1 dL aL).mp Bbed).symm]
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
Bbed : B b e d
⊢ area a b e + area a d e = 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
ed : e ≠ d
Bbed : B b e d
⊢ area a b e + area a d e = area a b e + area a b c
Tactic:
have: length b c = length e d := by
  have := length_sum_of_B Bbed
  rw [hlen, He.2.1] at this; simp [one_mul] at this; linarith
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
Bbed : B b e d
this : length b c = length e d
⊢ area a b e + area a d e = 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
ed : e ≠ d
Bbed : B b e d
this : length b c = length e d
⊢ area a b e + area a d e = area a b e + area a b c
Tactic:
perm [eq_area_of_eq_base_samevertex a bL cL He.1 dL 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
Bbed : B b e d
this✝ : length b c = length e d
this : area a b c = area a d e
⊢ area a b e + area a d e = 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
ed : e ≠ d
Bbed : B b e d
this✝ : length b c = length e d
this : area a b c = area a d e
⊢ area a b e + area a d e = area a b e + area a b c
Tactic:
rw [this]
Proof state after:
no goals
Theorem: rescale_triangle_of_base_inductive
Proof state before:
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
Tactic:
rw [← length_sum_of_B Bbcd, n0] at hlen
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 c + length c d = ↑(Nat.succ 0) * 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 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 c + length c d = ↑(Nat.succ 0) * 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:
simp at hlen
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
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : n = 0
hlen : length c d = 0
⊢ area a b d = ↑(Nat.succ n) * area a b c
Theorem: rescale_triangle_of_base_inductive
Proof state before:
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
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : n = 0
hlen : length c d = 0
⊢ area a b d = ↑(Nat.succ n) * area a b c
Tactic:
exfalso
Proof state after:
case pos.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
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : n = 0
hlen : length c d = 0
⊢ False
Theorem: rescale_triangle_of_base_inductive
Proof state before:
case pos.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
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : n = 0
hlen : length c d = 0
⊢ False
Tactic:
exact cd (length_eq_zero_iff.mp hlen)
Proof state after:
no goals
Theorem: rescale_triangle_of_base_inductive
Proof state before:
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
Tactic:
rw [← length_sum_of_B Bbcd, n1,] at hlen
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 c + length c d = ↑(Nat.succ 1) * 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 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 c + length c d = ↑(Nat.succ 1) * 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 at hlen
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
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : n = 1
hlen : length b c + length c d = (1 + 1) * length b c
⊢ area a b d = ↑(Nat.succ n) * area a b c
Theorem: rescale_triangle_of_base_inductive
Proof state before:
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
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : n = 1
hlen : length b c + length c d = (1 + 1) * length b c
⊢ area a b d = ↑(Nat.succ n) * area a b c
Tactic:
rw [← (area_add_iff_B bc cd bd.symm bL cL dL aL).mp Bbcd, n1]
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
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : n = 1
hlen : length b c + length c d = (1 + 1) * length b c
⊢ area a b c + area a d c = ↑(Nat.succ 1) * area a b c
Theorem: rescale_triangle_of_base_inductive
Proof state before:
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
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : n = 1
hlen : length b c + length c d = (1 + 1) * length b c
⊢ area a b c + area a d c = ↑(Nat.succ 1) * area a b c
Tactic:
perm
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
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : n = 1
hlen : length b c + length c d = (1 + 1) * length b c
⊢ area a b c + area a c d = ↑(Nat.succ 1) * area a b c
Theorem: rescale_triangle_of_base_inductive
Proof state before:
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
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : n = 1
hlen : length b c + length c d = (1 + 1) * length b c
⊢ area a b c + area a c d = ↑(Nat.succ 1) * area a b c
Tactic:
simp
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
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : n = 1
hlen : length b c + length c d = (1 + 1) * length b c
⊢ area a b c + area a c d = (1 + 1) * area a b c
Theorem: rescale_triangle_of_base_inductive
Proof state before:
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
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : n = 1
hlen : length b c + length c d = (1 + 1) * length b c
⊢ area a b c + area a c d = (1 + 1) * area a b c
Tactic:
ring_nf
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
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : n = 1
hlen : length b c + length c d = (1 + 1) * length b c
⊢ area a b c + area a c d = area a b c * 2
Theorem: rescale_triangle_of_base_inductive
Proof state before:
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
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : n = 1
hlen : length b c + length c d = (1 + 1) * length b c
⊢ area a b c + area a c d = area a b c * 2
Tactic:
simp [mul_two]
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
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : n = 1
hlen : length b c + length c d = (1 + 1) * length b c
⊢ area a c d = area a b c
Theorem: rescale_triangle_of_base_inductive
Proof state before:
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
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : n = 1
hlen : length b c + length c d = (1 + 1) * length b c
⊢ area a c d = area a b c
Tactic:
apply (eq_area_of_eq_base_samevertex a bL cL cL dL (by linarith)).symm
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
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : n = 1
hlen : length b c + length c d = (1 + 1) * length b c
⊢ length b c = length c d
Tactic:
linarith
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
⊢ False
Tactic:
have := He.2.1
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
this : length b e = ↑n * length b c
⊢ False
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
this : length b e = ↑n * length b c
⊢ False
Tactic:
rw [ed, hlen] 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
this : ↑(Nat.succ n) * length b c = ↑n * length b c
⊢ False
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
this : ↑(Nat.succ n) * length b c = ↑n * length b c
⊢ False
Tactic:
simp 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
this : length b c = 0
⊢ False
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
this : length b c = 0
⊢ False
Tactic:
exact bc (length_eq_zero_iff.mp this)
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
⊢ B b e d
Tactic:
have: length b e < length b d := by rw [He.2.1, hlen]; simp; linarith [len_pos_of_nq bc]
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
this : length b e < length b d
⊢ B b 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
this : length b e < length b d
⊢ B b e d
Tactic:
have := B_of_three_online_ne_short this be bd ed bL He.1 dL
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
this✝ : length b e < length b d
this : B b e d ∨ B e b d
⊢ B b 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
this✝ : length b e < length b d
this : B b e d ∨ B e b d
⊢ B b e d
Tactic:
cases this with
| inl h => exact h
| inr h =>
  exfalso
  exact not_B324_of_B123_B124 Bbce Bbcd (B124_of_B134_B123 h (B_symm Bbce))
Proof state after:
no goals