awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a : k
inl : HSMul.hSMul.{u_1, u_2, u_2} (α := k) 0 (slope f a a) = f a -ᵥ f a
⊢ (a - a) • slope f a a = f a -ᵥ f a
have inl₁ : 0 = f a -ᵥ f a
Tactic: rw [sub_self, zero_smul, vsub_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a : k
inl : HSMul.hSMul.{u_1, u_2, u_2} (α := k) 0 (slope f a a) = f a -ᵥ f a
inl₁ : 0 = f a -ᵥ f a
⊢ (a - a) • slope f a a = f a -ᵥ f a
have inl₂ : Eq.{u_2 + 1} (α := E) 0 0
Tactic: rw [sub_self, zero_smul, vsub_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a b : k
hne : a ≠ b
⊢ (b - a) • slope f a b = f b -ᵥ f a
have inr : (b - a) • (b - a)⁻¹ • (f b -ᵥ f a) = f b -ᵥ f a
Tactic: rw [slope, smul_inv_smul₀ (sub_ne_zero.2 hne.symm)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a b : k
hne : a ≠ b
inr : (b - a) • (b - a)⁻¹ • (f b -ᵥ f a) = f b -ᵥ f a
⊢ (b - a) • slope f a b = f b -ᵥ f a
have inr₁ : f b -ᵥ f a = f b -ᵥ f a
Tactic: rw [slope, smul_inv_smul₀ (sub_ne_zero.2 hne.symm)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a b : k
⊢ (b - a) • slope f a b +ᵥ f a = f b
have rw : (f b -ᵥ f a) +ᵥ f a = f b
Tactic: rw [sub_smul_slope, vsub_vadd]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a b : k
rw : (f b -ᵥ f a) +ᵥ f a = f b
⊢ (b - a) • slope f a b +ᵥ f a = f b
have rw₁ : f b = f b
Tactic: rw [sub_smul_slope, vsub_vadd]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → E
c : PE
⊢ (slope.{u_1, u_2, u_3} (PE := PE) fun (x : k) ↦ f x +ᵥ c) = slope f
have h : ∀ (a b : k), slope.{u_1, u_2, u_3} (PE := PE) (fun (x : k) ↦ f x +ᵥ c) a b = slope f a b
Tactic: ext a b
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a b : k
h : slope f a b = 0
⊢ f a = f b
have rw : f a = (b - a) • slope f a b +ᵥ f a
Tactic: rw [← sub_smul_slope_vadd f a b, h, smul_zero, zero_vadd]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a b : k
h : slope f a b = 0
rw : f a = (b - a) • slope f a b +ᵥ f a
⊢ f a = f b
have rw₁ : f a = HSMul.hSMul (β := E) (b - a) 0 +ᵥ f a
Tactic: rw [← sub_smul_slope_vadd f a b, h, smul_zero, zero_vadd]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a b : k
h : slope f a b = 0
rw : f a = (b - a) • slope f a b +ᵥ f a
rw₁ : f a = HSMul.hSMul (β := E) (b - a) 0 +ᵥ f a
⊢ f a = f b
have rw₂ : f a = HVAdd.hVAdd.{u_2, u_3, u_3} (α := E) 0 (f a)
Tactic: rw [← sub_smul_slope_vadd f a b, h, smul_zero, zero_vadd]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a b : k
h : slope f a b = 0
rw : f a = (b - a) • slope f a b +ᵥ f a
rw₁ : f a = HSMul.hSMul (β := E) (b - a) 0 +ᵥ f a
rw₂ : f a = HVAdd.hVAdd.{u_2, u_3, u_3} (α := E) 0 (f a)
⊢ f a = f b
have rw₃ : f a = f a
Tactic: rw [← sub_smul_slope_vadd f a b, h, smul_zero, zero_vadd]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a b : k
⊢ slope f a b = slope f b a
have rw : (b - a)⁻¹ • (f b -ᵥ f a) = slope f b a
Tactic: rw [slope, slope, ← neg_vsub_eq_vsub_rev, smul_neg, ← neg_smul, neg_inv, neg_sub]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a b : k
rw : (b - a)⁻¹ • (f b -ᵥ f a) = slope f b a
⊢ slope f a b = slope f b a
have rw₁ : (b - a)⁻¹ • (f b -ᵥ f a) = (a - b)⁻¹ • (f a -ᵥ f b)
Tactic: rw [slope, slope, ← neg_vsub_eq_vsub_rev, smul_neg, ← neg_smul, neg_inv, neg_sub]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a b : k
rw : (b - a)⁻¹ • (f b -ᵥ f a) = slope f b a
rw₁ : (b - a)⁻¹ • (f b -ᵥ f a) = (a - b)⁻¹ • (f a -ᵥ f b)
⊢ slope f a b = slope f b a
have rw₂ : (b - a)⁻¹ • -(f a -ᵥ f b) = (a - b)⁻¹ • (f a -ᵥ f b)
Tactic: rw [slope, slope, ← neg_vsub_eq_vsub_rev, smul_neg, ← neg_smul, neg_inv, neg_sub]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a b : k
rw : (b - a)⁻¹ • (f b -ᵥ f a) = slope f b a
rw₁ : (b - a)⁻¹ • (f b -ᵥ f a) = (a - b)⁻¹ • (f a -ᵥ f b)
rw₂ : (b - a)⁻¹ • -(f a -ᵥ f b) = (a - b)⁻¹ • (f a -ᵥ f b)
⊢ slope f a b = slope f b a
have rw₃ : -((b - a)⁻¹ • (f a -ᵥ f b)) = (a - b)⁻¹ • (f a -ᵥ f b)
Tactic: rw [slope, slope, ← neg_vsub_eq_vsub_rev, smul_neg, ← neg_smul, neg_inv, neg_sub]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a b : k
rw : (b - a)⁻¹ • (f b -ᵥ f a) = slope f b a
rw₁ : (b - a)⁻¹ • (f b -ᵥ f a) = (a - b)⁻¹ • (f a -ᵥ f b)
rw₂ : (b - a)⁻¹ • -(f a -ᵥ f b) = (a - b)⁻¹ • (f a -ᵥ f b)
rw₃ : -((b - a)⁻¹ • (f a -ᵥ f b)) = (a - b)⁻¹ • (f a -ᵥ f b)
⊢ slope f a b = slope f b a
have rw₄ : -(b - a)⁻¹ • (f a -ᵥ f b) = (a - b)⁻¹ • (f a -ᵥ f b)
Tactic: rw [slope, slope, ← neg_vsub_eq_vsub_rev, smul_neg, ← neg_smul, neg_inv, neg_sub]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a b : k
rw : (b - a)⁻¹ • (f b -ᵥ f a) = slope f b a
rw₁ : (b - a)⁻¹ • (f b -ᵥ f a) = (a - b)⁻¹ • (f a -ᵥ f b)
rw₂ : (b - a)⁻¹ • -(f a -ᵥ f b) = (a - b)⁻¹ • (f a -ᵥ f b)
rw₃ : -((b - a)⁻¹ • (f a -ᵥ f b)) = (a - b)⁻¹ • (f a -ᵥ f b)
rw₄ : -(b - a)⁻¹ • (f a -ᵥ f b) = (a - b)⁻¹ • (f a -ᵥ f b)
⊢ slope f a b = slope f b a
have rw₅ : (-(b - a))⁻¹ • (f a -ᵥ f b) = (a - b)⁻¹ • (f a -ᵥ f b)
Tactic: rw [slope, slope, ← neg_vsub_eq_vsub_rev, smul_neg, ← neg_smul, neg_inv, neg_sub]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a b : k
rw : (b - a)⁻¹ • (f b -ᵥ f a) = slope f b a
rw₁ : (b - a)⁻¹ • (f b -ᵥ f a) = (a - b)⁻¹ • (f a -ᵥ f b)
rw₂ : (b - a)⁻¹ • -(f a -ᵥ f b) = (a - b)⁻¹ • (f a -ᵥ f b)
rw₃ : -((b - a)⁻¹ • (f a -ᵥ f b)) = (a - b)⁻¹ • (f a -ᵥ f b)
rw₄ : -(b - a)⁻¹ • (f a -ᵥ f b) = (a - b)⁻¹ • (f a -ᵥ f b)
rw₅ : (-(b - a))⁻¹ • (f a -ᵥ f b) = (a - b)⁻¹ • (f a -ᵥ f b)
⊢ slope f a b = slope f b a
have rw₆ : (a - b)⁻¹ • (f a -ᵥ f b) = (a - b)⁻¹ • (f a -ᵥ f b)
Tactic: rw [slope, slope, ← neg_vsub_eq_vsub_rev, smul_neg, ← neg_smul, neg_inv, neg_sub]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
f : k → E
⊢ slope (-f) = -slope f
have h : ∀ (x y : k), slope (-f) x y = (-slope f) x y
Tactic: ext x y
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a b c : k
⊢ ((b - a) / (c - a)) • slope f a b + ((c - b) / (c - a)) • slope f b c = slope f a c
have pos : ∀ (hab : a = b), ((b - a) / (c - a)) • slope f a b + ((c - b) / (c - a)) • slope f b c = slope f a c
Tactic: by_cases hab : a = b
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a b c : k
pos : ∀ (hab : a = b), ((b - a) / (c - a)) • slope f a b + ((c - b) / (c - a)) • slope f b c = slope f a c
⊢ ((b - a) / (c - a)) • slope f a b + ((c - b) / (c - a)) • slope f b c = slope f a c
have neg : ∀ (hab : ¬a = b), ((b - a) / (c - a)) • slope f a b + ((c - b) / (c - a)) • slope f b c = slope f a c
Tactic: by_cases hab : a = b
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a b c : k
hab : a = b
⊢ ((b - a) / (c - a)) • slope f a b + ((c - b) / (c - a)) • slope f b c = slope f a c
have pos : ((a - a) / (c - a)) • slope f a a + ((c - a) / (c - a)) • slope f a c = slope f a c
Tactic: subst hab
Cleared hypotheses: b, hab
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a c : k
⊢ ((a - a) / (c - a)) • slope f a a + ((c - a) / (c - a)) • slope f a c = slope f a c
have pos : ((c - a) / (c - a)) • slope f a c = slope f a c
Tactic: rw [sub_self, zero_div, zero_smul, zero_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a c : k
⊢ ((c - a) / (c - a)) • slope f a c = slope f a c
have pos : ∀ (hac : a = c), ((c - a) / (c - a)) • slope f a c = slope f a c
Tactic: by_cases hac : a = c
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a c : k
pos : ∀ (hac : a = c), ((c - a) / (c - a)) • slope f a c = slope f a c
⊢ ((c - a) / (c - a)) • slope f a c = slope f a c
have neg : ∀ (hac : ¬a = c), ((c - a) / (c - a)) • slope f a c = slope f a c
Tactic: by_cases hac : a = c
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a c : k
hac : ¬a = c
⊢ ((c - a) / (c - a)) • slope f a c = slope f a c
have neg : HSMul.hSMul.{u_1, u_2, u_2} (α := k) 1 (slope f a c) = slope f a c
Tactic: rw [div_self (sub_ne_zero.2 <| Ne.symm hac), one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a c : k
hac : ¬a = c
neg : HSMul.hSMul.{u_1, u_2, u_2} (α := k) 1 (slope f a c) = slope f a c
⊢ ((c - a) / (c - a)) • slope f a c = slope f a c
have neg₁ : slope f a c = slope f a c
Tactic: rw [div_self (sub_ne_zero.2 <| Ne.symm hac), one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a b c : k
hab : ¬a = b
⊢ ((b - a) / (c - a)) • slope f a b + ((c - b) / (c - a)) • slope f b c = slope f a c
have pos : ∀ (hbc : b = c), ((b - a) / (c - a)) • slope f a b + ((c - b) / (c - a)) • slope f b c = slope f a c
Tactic: by_cases hbc : b = c
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a b c : k
hab : ¬a = b
pos : ∀ (hbc : b = c), ((b - a) / (c - a)) • slope f a b + ((c - b) / (c - a)) • slope f b c = slope f a c
⊢ ((b - a) / (c - a)) • slope f a b + ((c - b) / (c - a)) • slope f b c = slope f a c
have neg : ∀ (hbc : ¬b = c), ((b - a) / (c - a)) • slope f a b + ((c - b) / (c - a)) • slope f b c = slope f a c
Tactic: by_cases hbc : b = c
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a b c : k
hab : ¬a = b
hbc : b = c
⊢ ((b - a) / (c - a)) • slope f a b + ((c - b) / (c - a)) • slope f b c = slope f a c
have pos : ((b - a) / (b - a)) • slope f a b + ((b - b) / (b - a)) • slope f b b = slope f a b
Tactic: subst hbc
Cleared hypotheses: c, hbc
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a b c : k
hab : ¬a = b
hbc : ¬b = c
⊢ ((b - a) / (c - a)) • slope f a b + ((c - b) / (c - a)) • slope f b c = slope f a c
have neg : ((c - b) / (c - a)) • slope f b c + ((b - a) / (c - a)) • slope f a b = slope f a c
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a b c : k
hab : ¬a = b
hbc : ¬b = c
⊢ ((c - b) / (c - a)) • slope f b c + ((b - a) / (c - a)) • slope f a b = slope f a c
have neg : ((c - b) / (c - a)) • (c - b)⁻¹ • (f c -ᵥ f b) + ((b - a) / (c - a)) • (b - a)⁻¹ • (f b -ᵥ f a) =
  (c - a)⁻¹ • (f c -ᵥ f a)
Tactic: simp_rw [slope, div_eq_inv_mul, mul_smul, ← smul_add,
    smul_inv_smul₀ (sub_ne_zero.2 <| Ne.symm hab), smul_inv_smul₀ (sub_ne_zero.2 <| Ne.symm hbc),
    vsub_add_vsub_cancel]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a b c : k
hab : ¬a = b
hbc : ¬b = c
neg :
  ((c - b) / (c - a)) • (c - b)⁻¹ • (f c -ᵥ f b) + ((b - a) / (c - a)) • (b - a)⁻¹ • (f b -ᵥ f a) =
    (c - a)⁻¹ • (f c -ᵥ f a)
⊢ ((c - b) / (c - a)) • slope f b c + ((b - a) / (c - a)) • slope f a b = slope f a c
have neg₁ : ((c - a)⁻¹ * (c - b)) • (c - b)⁻¹ • (f c -ᵥ f b) + ((c - a)⁻¹ * (b - a)) • (b - a)⁻¹ • (f b -ᵥ f a) =
  (c - a)⁻¹ • (f c -ᵥ f a)
Tactic: simp_rw [slope, div_eq_inv_mul, mul_smul, ← smul_add,
    smul_inv_smul₀ (sub_ne_zero.2 <| Ne.symm hab), smul_inv_smul₀ (sub_ne_zero.2 <| Ne.symm hbc),
    vsub_add_vsub_cancel]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a b c : k
hab : ¬a = b
hbc : ¬b = c
neg :
  ((c - b) / (c - a)) • (c - b)⁻¹ • (f c -ᵥ f b) + ((b - a) / (c - a)) • (b - a)⁻¹ • (f b -ᵥ f a) =
    (c - a)⁻¹ • (f c -ᵥ f a)
neg₁ :
  ((c - a)⁻¹ * (c - b)) • (c - b)⁻¹ • (f c -ᵥ f b) + ((c - a)⁻¹ * (b - a)) • (b - a)⁻¹ • (f b -ᵥ f a) =
    (c - a)⁻¹ • (f c -ᵥ f a)
⊢ ((c - b) / (c - a)) • slope f b c + ((b - a) / (c - a)) • slope f a b = slope f a c
have neg₂ : (c - a)⁻¹ • (c - b) • (c - b)⁻¹ • (f c -ᵥ f b) + (c - a)⁻¹ • (b - a) • (b - a)⁻¹ • (f b -ᵥ f a) =
  (c - a)⁻¹ • (f c -ᵥ f a)
Tactic: simp_rw [slope, div_eq_inv_mul, mul_smul, ← smul_add,
    smul_inv_smul₀ (sub_ne_zero.2 <| Ne.symm hab), smul_inv_smul₀ (sub_ne_zero.2 <| Ne.symm hbc),
    vsub_add_vsub_cancel]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a b c : k
hab : ¬a = b
hbc : ¬b = c
neg :
  ((c - b) / (c - a)) • (c - b)⁻¹ • (f c -ᵥ f b) + ((b - a) / (c - a)) • (b - a)⁻¹ • (f b -ᵥ f a) =
    (c - a)⁻¹ • (f c -ᵥ f a)
neg₁ :
  ((c - a)⁻¹ * (c - b)) • (c - b)⁻¹ • (f c -ᵥ f b) + ((c - a)⁻¹ * (b - a)) • (b - a)⁻¹ • (f b -ᵥ f a) =
    (c - a)⁻¹ • (f c -ᵥ f a)
neg₂ :
  (c - a)⁻¹ • (c - b) • (c - b)⁻¹ • (f c -ᵥ f b) + (c - a)⁻¹ • (b - a) • (b - a)⁻¹ • (f b -ᵥ f a) =
    (c - a)⁻¹ • (f c -ᵥ f a)
⊢ ((c - b) / (c - a)) • slope f b c + ((b - a) / (c - a)) • slope f a b = slope f a c
have neg₃ : (c - a)⁻¹ • ((c - b) • (c - b)⁻¹ • (f c -ᵥ f b) + (b - a) • (b - a)⁻¹ • (f b -ᵥ f a)) = (c - a)⁻¹ • (f c -ᵥ f a)
Tactic: simp_rw [slope, div_eq_inv_mul, mul_smul, ← smul_add,
    smul_inv_smul₀ (sub_ne_zero.2 <| Ne.symm hab), smul_inv_smul₀ (sub_ne_zero.2 <| Ne.symm hbc),
    vsub_add_vsub_cancel]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a b c : k
hab : ¬a = b
hbc : ¬b = c
neg :
  ((c - b) / (c - a)) • (c - b)⁻¹ • (f c -ᵥ f b) + ((b - a) / (c - a)) • (b - a)⁻¹ • (f b -ᵥ f a) =
    (c - a)⁻¹ • (f c -ᵥ f a)
neg₁ :
  ((c - a)⁻¹ * (c - b)) • (c - b)⁻¹ • (f c -ᵥ f b) + ((c - a)⁻¹ * (b - a)) • (b - a)⁻¹ • (f b -ᵥ f a) =
    (c - a)⁻¹ • (f c -ᵥ f a)
neg₂ :
  (c - a)⁻¹ • (c - b) • (c - b)⁻¹ • (f c -ᵥ f b) + (c - a)⁻¹ • (b - a) • (b - a)⁻¹ • (f b -ᵥ f a) =
    (c - a)⁻¹ • (f c -ᵥ f a)
neg₃ : (c - a)⁻¹ • ((c - b) • (c - b)⁻¹ • (f c -ᵥ f b) + (b - a) • (b - a)⁻¹ • (f b -ᵥ f a)) = (c - a)⁻¹ • (f c -ᵥ f a)
⊢ ((c - b) / (c - a)) • slope f b c + ((b - a) / (c - a)) • slope f a b = slope f a c
have neg₄ : (c - a)⁻¹ • ((c - b) • (c - b)⁻¹ • (f c -ᵥ f b) + (f b -ᵥ f a)) = (c - a)⁻¹ • (f c -ᵥ f a)
Tactic: simp_rw [slope, div_eq_inv_mul, mul_smul, ← smul_add,
    smul_inv_smul₀ (sub_ne_zero.2 <| Ne.symm hab), smul_inv_smul₀ (sub_ne_zero.2 <| Ne.symm hbc),
    vsub_add_vsub_cancel]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a b c : k
hab : ¬a = b
hbc : ¬b = c
neg :
  ((c - b) / (c - a)) • (c - b)⁻¹ • (f c -ᵥ f b) + ((b - a) / (c - a)) • (b - a)⁻¹ • (f b -ᵥ f a) =
    (c - a)⁻¹ • (f c -ᵥ f a)
neg₁ :
  ((c - a)⁻¹ * (c - b)) • (c - b)⁻¹ • (f c -ᵥ f b) + ((c - a)⁻¹ * (b - a)) • (b - a)⁻¹ • (f b -ᵥ f a) =
    (c - a)⁻¹ • (f c -ᵥ f a)
neg₂ :
  (c - a)⁻¹ • (c - b) • (c - b)⁻¹ • (f c -ᵥ f b) + (c - a)⁻¹ • (b - a) • (b - a)⁻¹ • (f b -ᵥ f a) =
    (c - a)⁻¹ • (f c -ᵥ f a)
neg₃ : (c - a)⁻¹ • ((c - b) • (c - b)⁻¹ • (f c -ᵥ f b) + (b - a) • (b - a)⁻¹ • (f b -ᵥ f a)) = (c - a)⁻¹ • (f c -ᵥ f a)
neg₄ : (c - a)⁻¹ • ((c - b) • (c - b)⁻¹ • (f c -ᵥ f b) + (f b -ᵥ f a)) = (c - a)⁻¹ • (f c -ᵥ f a)
⊢ ((c - b) / (c - a)) • slope f b c + ((b - a) / (c - a)) • slope f a b = slope f a c
have neg₅ : (c - a)⁻¹ • (f c -ᵥ f b + (f b -ᵥ f a)) = (c - a)⁻¹ • (f c -ᵥ f a)
Tactic: simp_rw [slope, div_eq_inv_mul, mul_smul, ← smul_add,
    smul_inv_smul₀ (sub_ne_zero.2 <| Ne.symm hab), smul_inv_smul₀ (sub_ne_zero.2 <| Ne.symm hbc),
    vsub_add_vsub_cancel]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a b c : k
h : a ≠ c
⊢ (lineMap (slope f a b) (slope f b c) : (a : k) → E) ((c - b) / (c - a)) = slope f a c
have simp : (1 - (c - b) / (c - a)) • slope f a b = ((b - a) / (c - a)) • slope f a b
Tactic: simp only [lineMap_apply_module, ← sub_div_sub_smul_slope_add_sub_div_sub_smul_slope f a b c,
    add_left_inj]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a b c : k
h : a ≠ c
⊢ (1 - (c - b) / (c - a)) • slope f a b = ((b - a) / (c - a)) • slope f a b
have match_scalars : (1 - (c - b) / (c - a)) * 1 = (b - a) / (c - a) * 1
Tactic: match_scalars
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a b r : k
⊢ (lineMap (slope f ((lineMap a b : (a : k) → k) r) b) (slope f a ((lineMap a b : (a : k) → k) r)) : (a : k) → E) r =
    slope f a b
have inl : (lineMap (slope f ((lineMap a a : (a : k) → k) r) a) (slope f a ((lineMap a a : (a : k) → k) r)) : (a : k) → E) r =
  slope f a a
Tactic: obtain rfl | hab : a = b ∨ a ≠ b := Classical.em _
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a b r : k
inl :
  (lineMap (slope f ((lineMap a a : (a : k) → k) r) a) (slope f a ((lineMap a a : (a : k) → k) r)) : (a : k) → E) r =
    slope f a a
⊢ (lineMap (slope f ((lineMap a b : (a : k) → k) r) b) (slope f a ((lineMap a b : (a : k) → k) r)) : (a : k) → E) r =
    slope f a b
have inr : ∀ (hab : a ≠ b),
  (lineMap (slope f ((lineMap a b : (a : k) → k) r) b) (slope f a ((lineMap a b : (a : k) → k) r)) : (a : k) → E) r =
    slope f a b
Tactic: obtain rfl | hab : a = b ∨ a ≠ b := Classical.em _
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a b r : k
hab : a ≠ b
⊢ (lineMap (slope f ((lineMap a b : (a : k) → k) r) b) (slope f a ((lineMap a b : (a : k) → k) r)) : (a : k) → E) r =
    slope f a b
have inr : (lineMap (slope f b ((lineMap a b : (a : k) → k) r)) (slope f ((lineMap a b : (a : k) → k) r) a) : (a : k) → E) r =
  slope f b a
Tactic: rw [slope_comm _ a, slope_comm _ a, slope_comm _ _ b]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a b r : k
hab : a ≠ b
⊢ (lineMap (slope f b ((lineMap a b : (a : k) → k) r)) (slope f ((lineMap a b : (a : k) → k) r) a) : (a : k) → E) r =
    slope f b a
have h : r = HSub.hSub (β := k) a ((lineMap a b : (a : k) → k) r : k) / (a - b)
Tactic: convert! lineMap_slope_slope_sub_div_sub f b (lineMap a b r) a hab.symm using 2
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a b r : k
hab : a ≠ b
⊢ r = HSub.hSub (β := k) a ((lineMap a b : (a : k) → k) r : k) / (a - b)
have h : r = (a - ((1 - r) * a + r * b)) / (a - b)
Tactic: rw [lineMap_apply_ring, eq_div_iff (sub_ne_zero.2 hab), sub_mul, one_mul, mul_sub, ← sub_sub,
    sub_sub_cancel]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a b r : k
hab : a ≠ b
h : r = (a - ((1 - r) * a + r * b)) / (a - b)
⊢ r = HSub.hSub (β := k) a ((lineMap a b : (a : k) → k) r : k) / (a - b)
have h₁ : r * (a - b) = a - ((1 - r) * a + r * b)
Tactic: rw [lineMap_apply_ring, eq_div_iff (sub_ne_zero.2 hab), sub_mul, one_mul, mul_sub, ← sub_sub,
    sub_sub_cancel]