awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
hmem1 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.medial.points)) (s.medial.points 0)
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.points)) (s.medial.points 0)

Tactic:
have hmem2 : s.medial.points 0 ∈ affineSpan k (Set.range s.points) := by
    apply Set.mem_of_mem_of_subset (s.faceOppositeCentroid_mem_affineSpan_face 0)
    exact affineSpan_mono k (by simp)
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
hmem1 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.medial.points)) (s.medial.points 0)
hmem2 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.points)) (s.medial.points 0)
rw :
  Eq (α := Submodule k V) (direction (affineSpan k (Set.range s.medial.points)))
    (direction (affineSpan k (Set.range s.points)))
⊢ Eq (α := AffineSubspace k P) (affineSpan k (Set.range s.medial.points)) (affineSpan k (Set.range s.points))

Tactic:
rw [eq_iff_direction_eq_of_mem hmem1 hmem2]

Premises used: AffineSubspace.eq_iff_direction_eq_of_mem
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
hmem1 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.medial.points)) (s.medial.points 0)
hmem2 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.points)) (s.medial.points 0)
simp_rw :
  Eq (α := Submodule k V) (Submodule.span k (Set.range s.medial.points -ᵥ Set.range s.medial.points))
    (Submodule.span k (Set.range s.points -ᵥ Set.range s.points))
⊢ Eq (α := Submodule k V) (direction (affineSpan k (Set.range s.medial.points)))
    (direction (affineSpan k (Set.range s.points)))

Tactic:
simp_rw [direction_affineSpan, vectorSpan_def]

Premises used: direction_affineSpan, vectorSpan_def
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
hmem1 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.medial.points)) (s.medial.points 0)
hmem2 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.points)) (s.medial.points 0)
this :
  Set.range s.medial.points -ᵥ Set.range s.medial.points =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (-(↑n : k))⁻¹ (Set.range s.points -ᵥ Set.range s.points)
hr : IsUnit.{u_1} (M := k) (-(↑n : k))⁻¹
⊢ Eq (α := Submodule k V) (Submodule.span k (Set.range s.medial.points -ᵥ Set.range s.medial.points))
    (Submodule.span k (Set.range s.points -ᵥ Set.range s.points))

Tactic:
rw [this, Submodule.span_smul_eq_of_isUnit]

Premises used: Submodule.span_smul_eq_of_isUnit
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
hmem1 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.medial.points)) (s.medial.points 0)
hmem2 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.points)) (s.medial.points 0)
this :
  Set.range s.medial.points -ᵥ Set.range s.medial.points =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (-(↑n : k))⁻¹ (Set.range s.points -ᵥ Set.range s.points)
⊢ IsUnit.{u_1} (M := k) (-(↑n : k))⁻¹

Tactic:
simpa using NeZero.ne n

Premises used: NeZero.ne
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
hmem1 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.medial.points)) (s.medial.points 0)
hmem2 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.points)) (s.medial.points 0)
suffices :
  Set.range s.medial.points -ᵥ Set.range s.medial.points =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (-(↑n : k))⁻¹ (Set.range s.points -ᵥ Set.range s.points)
⊢ Eq (α := Submodule k V) (Submodule.span k (Set.range s.medial.points -ᵥ Set.range s.medial.points))
    (Submodule.span k (Set.range s.points -ᵥ Set.range s.points))

Tactic:
suffices Set.range s.medial.points -ᵥ Set.range s.medial.points
    = (-n : k)⁻¹ • (Set.range s.points -ᵥ Set.range s.points) by
    rw [this, Submodule.span_smul_eq_of_isUnit]
    simpa using NeZero.ne n
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
hmem1 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.medial.points)) (s.medial.points 0)
hmem2 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.points)) (s.medial.points 0)
h :
  ∀ (v : V),
    v ∈ Set.range s.medial.points -ᵥ Set.range s.medial.points ↔
      v ∈ HSMul.hSMul.{u_1, u_2, u_2} (α := k) (-(↑n : k))⁻¹ (Set.range s.points -ᵥ Set.range s.points)
⊢ Set.range s.medial.points -ᵥ Set.range s.medial.points =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (-(↑n : k))⁻¹ (Set.range s.points -ᵥ Set.range s.points)

Tactic:
ext v
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
hmem1 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.medial.points)) (s.medial.points 0)
hmem2 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.points)) (s.medial.points 0)
v : V
this :
  (∃ (a : Fin (n + 1)) (b : Fin (n + 1)),
      HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points b -ᵥ s.points a) = v) ↔
    ∃ (a : Fin (n + 1)) (b : Fin (n + 1)),
      -HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points a -ᵥ s.points b) = v
⊢ v ∈ Set.range s.medial.points -ᵥ Set.range s.medial.points ↔
    v ∈ HSMul.hSMul.{u_1, u_2, u_2} (α := k) (-(↑n : k))⁻¹ (Set.range s.points -ᵥ Set.range s.points)

Tactic:
simpa [Set.mem_vsub, Set.mem_smul_set, medial_points,
      faceOppositeCentroid_vsub_faceOppositeCentroid]

Premises used: Set.mem_vsub, Set.mem_smul_set, Affine.Simplex.medial_points, Affine.Simplex.faceOppositeCentroid_vsub_faceOppositeCentroid
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
hmem1 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.medial.points)) (s.medial.points 0)
hmem2 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.points)) (s.medial.points 0)
v : V
h :
  (∃ (a : Fin (n + 1)) (b : Fin (n + 1)),
      HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points b -ᵥ s.points a) = v) ↔
    ∃ (a : Fin (n + 1)) (b : Fin (n + 1)),
      -HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points a -ᵥ s.points b) = v
⊢ v ∈ Set.range s.medial.points -ᵥ Set.range s.medial.points ↔
    v ∈ HSMul.hSMul.{u_1, u_2, u_2} (α := k) (-(↑n : k))⁻¹ (Set.range s.points -ᵥ Set.range s.points)

Tactic:
suffices (∃ a b, (n : k)⁻¹ • (s.points b -ᵥ s.points a) = v) ↔
    ∃ a b, -((n : k)⁻¹ • (s.points a -ᵥ s.points b)) = v by
    simpa [Set.mem_vsub, Set.mem_smul_set, medial_points,
      faceOppositeCentroid_vsub_faceOppositeCentroid]
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
hmem1 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.medial.points)) (s.medial.points 0)
hmem2 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.points)) (s.medial.points 0)
v : V
h :
  ∀ (a b : Fin (n + 1)),
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points b -ᵥ s.points a) =
      -HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points a -ᵥ s.points b)
⊢ (∃ (a : Fin (n + 1)) (b : Fin (n + 1)),
      HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points b -ᵥ s.points a) = v) ↔
    ∃ (a : Fin (n + 1)) (b : Fin (n + 1)),
      -HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points a -ᵥ s.points b) = v

Tactic:
congrm ∃ a b, ?_ = v
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
hmem1 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.medial.points)) (s.medial.points 0)
hmem2 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.points)) (s.medial.points 0)
v : V
a b : Fin (n + 1)
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points b -ᵥ s.points a) =
    -HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points a -ᵥ s.points b)

Tactic:
simp [← smul_neg]

Premises used: smul_neg
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
S : AffineSubspace k P
hS : affineSpan k (Set.range s.points) ≤ S
⊢ Nonempty.{u_3 + 1} ↥S

Tactic:
haveI := Nonempty.map (AffineSubspace.inclusion hS) inferInstance
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
S : AffineSubspace k P
hS : affineSpan k (Set.range s.points) ≤ S
this : Nonempty.{u_3 + 1} ↥S
h :
  ∀ (i : Fin (n + 1)),
    (↑((s.restrict S hS).medial.points i) : P) = (↑(points (s.medial.restrict S ⋯ : Simplex k (↥S) n) i) : P)
⊢ (s.restrict S hS).medial = s.medial.restrict S ⋯

Tactic:
ext i
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
S : AffineSubspace k P
hS : affineSpan k (Set.range s.points) ≤ S
this : Nonempty.{u_3 + 1} ↥S
i : Fin (n + 1)
⊢ (↑((s.restrict S hS).medial.points i) : P) = (↑(points (s.medial.restrict S ⋯ : Simplex k (↥S) n) i) : P)

Tactic:
simp [medial_points]

Premises used: Affine.Simplex.medial_points
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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
⊢ slope f = fun (a b : k) ↦ (b - a)⁻¹ • (f b -ᵥ f a)

Tactic:
rfl

Premises used: slope, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
Goal:
k : Type u_1
inst : Field k
f : k → k
a b : k
⊢ slope f a b = (f b - f a) / (b - a)

Tactic:
(div_eq_inv_mul _ _).symm

Premises used: slope, div_eq_inv_mul, Eq.symm
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
Goal:
k : Type u_1
inst : Field k
f : k → k
a : k
⊢ slope f a = fun (b : k) ↦ (f b - f a) / (b - a)

Tactic:
(div_eq_inv_mul _ _).symm

Premises used: slope, div_eq_inv_mul, Eq.symm
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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
rw : (a - a)⁻¹ • (f a -ᵥ f a) = 0
rw₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := k) 0⁻¹ (f a -ᵥ f a) = 0
rw₂ : HSMul.hSMul.{u_1, u_2, u_2} (α := k) 0 (f a -ᵥ f a) = 0
rw₃ rw₄ : Eq.{u_2 + 1} (α := E) 0 0
⊢ slope f a a = 0

Tactic:
rw [slope, sub_self, inv_zero, zero_smul]

Premises used: sub_self, inv_zero, slope, zero_smul
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
Goal:
k : Type u_1
E : Type u_2
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
f : k → E
a b : k
⊢ slope f a b = (b - a)⁻¹ • (f b - f a)

Tactic:
rfl

Premises used: slope, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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
inl : (a - a) • slope f a a = f a -ᵥ f a
inr : ∀ (hne : a ≠ b), (b - a) • slope f a b = f b -ᵥ f a
⊢ (b - a) • slope f a b = f b -ᵥ f a

Tactic:
rcases eq_or_ne a b with (rfl | hne)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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
inl₂ inl₃ : Eq.{u_2 + 1} (α := E) 0 0
⊢ (a - a) • slope f a a = f a -ᵥ f a

Tactic:
rw [sub_self, zero_smul, vsub_self]

Premises used: sub_self, zero_smul, vsub_self
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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
inr₁ inr₂ : f b -ᵥ f a = f b -ᵥ f a
⊢ (b - a) • slope f a b = f b -ᵥ f a

Tactic:
rw [slope, smul_inv_smul₀ (sub_ne_zero.2 hne.symm)]

Premises used: Iff.mpr, smul_inv_smul₀, sub_ne_zero, Ne.symm, slope
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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
rw₁ rw₂ : f b = f b
⊢ (b - a) • slope f a b +ᵥ f a = f b

Tactic:
rw [sub_smul_slope, vsub_vadd]

Premises used: sub_smul_slope, vsub_vadd
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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
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
⊢ (slope.{u_1, u_2, u_3} (PE := PE) fun (x : k) ↦ f x +ᵥ c) = slope f

Tactic:
ext a b
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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
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:
simp only [slope, vadd_vsub_vadd_cancel_right, vsub_eq_sub]

Premises used: vadd_vsub_vadd_cancel_right, slope, vsub_eq_sub
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
Goal:
k : Type u_1
E : Type u_2
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
f : k → E
a b : k
h : a ≠ b
⊢ slope (PE := E) (fun (x : k) ↦ (x - a) • f x) a b = f b

Tactic:
simp [slope, inv_smul_smul₀ (sub_ne_zero.2 h.symm)]

Premises used: Iff.mpr, inv_smul_smul₀, sub_ne_zero, Ne.symm, slope
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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)
rw₃ rw₄ : f a = f a
⊢ f a = f b

Tactic:
rw [← sub_smul_slope_vadd f a b, h, smul_zero, zero_vadd]

Premises used: smul_zero, sub_smul_slope_vadd, zero_vadd
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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 : Type u_4
PF : Type u_5
inst_4 : AddCommGroup F
inst_5 : Module k F
inst_6 : AddTorsor F PF
f : PE →ᵃ[k] PF
g : k → PE
a b : k
⊢ slope.{u_1, u_4, u_5} (PE := PF) ((⇑f : (a : PE) → PF) ∘ g) a b = (f.linear : (a : E) → F) (slope g a b)

Tactic:
simp only [slope, (· ∘ ·), f.linear.map_smul, f.linearMap_vsub]

Premises used: Function.comp, AffineMap.linearMap_vsub, slope, LinearMap.map_smul, AffineMap.linear
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
Goal:
k : Type u_1
E : Type u_2
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
F : Type u_4
inst_3 : AddCommGroup F
inst_4 : Module k F
f : E →ₗ[k] F
g : k → E
a b : k
⊢ slope (PE := F) ((⇑f : (a : E) → F) ∘ g) a b = (f : (a : E) → F) (slope g a b)

Tactic:
f.toAffineMap.slope_comp g a b

Premises used: AffineMap.slope_comp, LinearMap.toAffineMap
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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)
rw₆ rw₇ : (a - b)⁻¹ • (f a -ᵥ f b) = (a - b)⁻¹ • (f a -ᵥ f b)
⊢ slope f a b = slope f b a

Tactic:
rw [slope, slope, ← neg_vsub_eq_vsub_rev, smul_neg, ← neg_smul, neg_inv, neg_sub]

Premises used: neg_smul, neg_sub, smul_neg, slope, neg_inv, neg_vsub_eq_vsub_rev
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
Goal:
k : Type u_1
E : Type u_2
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
f : k → E
x y : k
⊢ slope (PE := E) (fun (t : k) ↦ -f t) x y = -slope f x y

Tactic:
simp only [slope_def_module, neg_sub_neg, ← smul_neg, neg_sub]

Premises used: neg_sub, smul_neg, neg_sub_neg, slope_def_module
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
Goal:
k : Type u_1
E : Type u_2
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
f : k → E
h : ∀ (x y : k), slope (-f) x y = (-slope f) x y
⊢ slope (-f) = -slope f

Tactic:
ext x y
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
Goal:
k : Type u_1
E : Type u_2
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
f : k → E
x y : k
⊢ slope (-f) x y = (-slope f) x y

Tactic:
slope_neg f x y

Premises used: slope_neg
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
Goal:
k : Type u_1
E : Type u_2
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
f : k → E
x y : k
⊢ slope (-f) x y = (-slope f) x y

Tactic:
exact slope_neg f x y

Premises used: slope_neg
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
Goal:
k : Type u_1
E : Type u_2
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
f : k → E
a b : k
⊢ slope f a b = 0 ↔ f a = f b

Tactic:
simp [slope, sub_eq_zero, eq_comm, or_iff_right_of_imp (congr_arg _)]

Premises used: sub_eq_zero, slope, eq_comm, congr_arg, or_iff_right_of_imp
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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
neg : ∀ (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

Tactic:
by_cases hab : a = b
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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 : ((a - a) / (c - a)) • slope f a a + ((c - a) / (c - a)) • slope f a 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

Tactic:
subst hab
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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 : ((c - a) / (c - a)) • slope f a c = slope f a c
⊢ ((a - a) / (c - a)) • slope f a a + ((c - a) / (c - a)) • slope f a c = slope f a c

Tactic:
rw [sub_self, zero_div, zero_smul, zero_add]

Premises used: sub_self, zero_div, zero_add, zero_smul
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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
neg : ∀ (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

Tactic:
by_cases hac : a = c
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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

Tactic:
simp [hac]
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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
neg₁ neg₂ : slope f a c = slope f a c
⊢ ((c - a) / (c - a)) • slope f a c = slope f a c

Tactic:
rw [div_self (sub_ne_zero.2 <| Ne.symm hac), one_smul]

Premises used: Iff.mpr, sub_ne_zero, Ne.symm, one_smul, div_self
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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
neg : ∀ (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

Tactic:
by_cases hbc : b = c
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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
pos : ((b - a) / (b - a)) • slope f a b + ((b - b) / (b - a)) • slope f b b = slope f a b
⊢ ((b - a) / (c - a)) • slope f a b + ((c - b) / (c - a)) • slope f b c = slope f a c

Tactic:
subst hbc
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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
hab : ¬a = b
⊢ ((b - a) / (b - a)) • slope f a b + ((b - b) / (b - a)) • slope f b b = slope f a b

Tactic:
simp [sub_ne_zero.2 (Ne.symm hab)]

Premises used: Iff.mpr, sub_ne_zero, Ne.symm
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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)) • slope f b c + ((b - a) / (c - a)) • slope f a b = slope f a c
⊢ ((b - a) / (c - a)) • slope f a b + ((c - b) / (c - a)) • slope f b c = slope f a c

Tactic:
rw [add_comm]

Premises used: add_comm