Theorem: rescale_triangle_of_base (Pythagoras/euclid_VI.lean)

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
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

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
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

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)
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

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
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

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
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

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
State after:
no goals

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
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

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
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

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)]
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

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]
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
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

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
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

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
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

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)]
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

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]
State after:
no goals

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
State after:
no goals

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
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

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)
State after:
no goals

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
State after:
no goals

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)
State after:
no goals

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]
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

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]
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

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]
State after:
no goals

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
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

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⟩
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

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
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

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
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

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
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

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]
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

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]
State after:
no goals

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]
State after:
no goals

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]
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

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
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

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
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

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
State after:
no goals