awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
x y : P
rw :
  ((pointReflection ((lineMap x y : (a : R) → P) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) :
          Perm P) :
        (a : P) → P)
      x =
    y
rw₁ :
  HVAdd.hVAdd (β := P) ((lineMap x y : (a : R) → P) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) -ᵥ x)
      ((lineMap x y : (a : R) → P) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) : P) =
    y
rw₂ :
  ((HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (y -ᵥ x) +ᵥ
          x) -ᵥ
        x) +ᵥ
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (y -ᵥ x) +ᵥ
        x =
    y
rw₃ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (y -ᵥ x) +ᵥ
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (y -ᵥ x) +ᵥ
        x =
    y
rw₄ :
  (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (y -ᵥ x) +
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (y -ᵥ x)) +ᵥ
      x =
    y
rw₅ :
  HAdd.hAdd (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) •
        (y -ᵥ x) +ᵥ
      x =
    y
⊢ (pointReflection (midpoint R x y) : (a : P) → P) x = y
have rw₆ : HMul.hMul (α := R) 2 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) • (y -ᵥ x) +ᵥ x = y
Tactic: rw [midpoint, pointReflection_apply, lineMap_apply, vadd_vsub, vadd_vadd, ← add_smul, ← two_mul,
    mul_invOf_self, one_smul, vsub_vadd]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
x y : P
rw :
  ((pointReflection ((lineMap x y : (a : R) → P) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) :
          Perm P) :
        (a : P) → P)
      x =
    y
rw₁ :
  HVAdd.hVAdd (β := P) ((lineMap x y : (a : R) → P) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) -ᵥ x)
      ((lineMap x y : (a : R) → P) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) : P) =
    y
rw₂ :
  ((HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (y -ᵥ x) +ᵥ
          x) -ᵥ
        x) +ᵥ
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (y -ᵥ x) +ᵥ
        x =
    y
rw₃ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (y -ᵥ x) +ᵥ
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (y -ᵥ x) +ᵥ
        x =
    y
rw₄ :
  (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (y -ᵥ x) +
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (y -ᵥ x)) +ᵥ
      x =
    y
rw₅ :
  HAdd.hAdd (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) •
        (y -ᵥ x) +ᵥ
      x =
    y
rw₆ : HMul.hMul (α := R) 2 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) • (y -ᵥ x) +ᵥ x = y
⊢ (pointReflection (midpoint R x y) : (a : P) → P) x = y
have rw₇ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 (y -ᵥ x) +ᵥ x = y
Tactic: rw [midpoint, pointReflection_apply, lineMap_apply, vadd_vsub, vadd_vadd, ← add_smul, ← two_mul,
    mul_invOf_self, one_smul, vsub_vadd]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
x y : P
rw :
  ((pointReflection ((lineMap x y : (a : R) → P) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) :
          Perm P) :
        (a : P) → P)
      x =
    y
rw₁ :
  HVAdd.hVAdd (β := P) ((lineMap x y : (a : R) → P) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) -ᵥ x)
      ((lineMap x y : (a : R) → P) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) : P) =
    y
rw₂ :
  ((HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (y -ᵥ x) +ᵥ
          x) -ᵥ
        x) +ᵥ
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (y -ᵥ x) +ᵥ
        x =
    y
rw₃ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (y -ᵥ x) +ᵥ
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (y -ᵥ x) +ᵥ
        x =
    y
rw₄ :
  (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (y -ᵥ x) +
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (y -ᵥ x)) +ᵥ
      x =
    y
rw₅ :
  HAdd.hAdd (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) •
        (y -ᵥ x) +ᵥ
      x =
    y
rw₆ : HMul.hMul (α := R) 2 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) • (y -ᵥ x) +ᵥ x = y
rw₇ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 (y -ᵥ x) +ᵥ x = y
⊢ (pointReflection (midpoint R x y) : (a : P) → P) x = y
have rw₈ : (y -ᵥ x) +ᵥ x = y
Tactic: rw [midpoint, pointReflection_apply, lineMap_apply, vadd_vsub, vadd_vadd, ← add_smul, ← two_mul,
    mul_invOf_self, one_smul, vsub_vadd]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
x y : P
rw :
  ((pointReflection ((lineMap x y : (a : R) → P) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) :
          Perm P) :
        (a : P) → P)
      x =
    y
rw₁ :
  HVAdd.hVAdd (β := P) ((lineMap x y : (a : R) → P) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) -ᵥ x)
      ((lineMap x y : (a : R) → P) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) : P) =
    y
rw₂ :
  ((HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (y -ᵥ x) +ᵥ
          x) -ᵥ
        x) +ᵥ
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (y -ᵥ x) +ᵥ
        x =
    y
rw₃ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (y -ᵥ x) +ᵥ
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (y -ᵥ x) +ᵥ
        x =
    y
rw₄ :
  (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (y -ᵥ x) +
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (y -ᵥ x)) +ᵥ
      x =
    y
rw₅ :
  HAdd.hAdd (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) •
        (y -ᵥ x) +ᵥ
      x =
    y
rw₆ : HMul.hMul (α := R) 2 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) • (y -ᵥ x) +ᵥ x = y
rw₇ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 (y -ᵥ x) +ᵥ x = y
rw₈ : (y -ᵥ x) +ᵥ x = y
⊢ (pointReflection (midpoint R x y) : (a : P) → P) x = y
have rw₉ : y = y
Tactic: rw [midpoint, pointReflection_apply, lineMap_apply, vadd_vsub, vadd_vadd, ← add_smul, ← two_mul,
    mul_invOf_self, one_smul, vsub_vadd]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
x y : P
⊢ midpoint R x y = midpoint R y x
have rw : (lineMap x y : (a : R) → P) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) = midpoint R y x
Tactic: rw [midpoint, ← lineMap_apply_one_sub, one_sub_invOf_two, midpoint]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
x y : P
rw : (lineMap x y : (a : R) → P) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) = midpoint R y x
⊢ midpoint R x y = midpoint R y x
have rw₁ : (lineMap y x : (a : R) → P) (HSub.hSub (α := R) 1 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) =
  midpoint R y x
Tactic: rw [midpoint, ← lineMap_apply_one_sub, one_sub_invOf_two, midpoint]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
x y : P
rw : (lineMap x y : (a : R) → P) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) = midpoint R y x
rw₁ :
  (lineMap y x : (a : R) → P) (HSub.hSub (α := R) 1 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) =
    midpoint R y x
⊢ midpoint R x y = midpoint R y x
have rw₂ : (lineMap y x : (a : R) → P) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) = midpoint R y x
Tactic: rw [midpoint, ← lineMap_apply_one_sub, one_sub_invOf_two, midpoint]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
x y : P
rw : (lineMap x y : (a : R) → P) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) = midpoint R y x
rw₁ :
  (lineMap y x : (a : R) → P) (HSub.hSub (α := R) 1 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) =
    midpoint R y x
rw₂ : (lineMap y x : (a : R) → P) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) = midpoint R y x
⊢ midpoint R x y = midpoint R y x
have rw₃ : Eq.{u_4 + 1} (α := P) ((lineMap y x : (a : R) → P) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) : P)
  ((lineMap y x : (a : R) → P) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) : P)
Tactic: rw [midpoint, ← lineMap_apply_one_sub, one_sub_invOf_two, midpoint]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
x y : P
⊢ (pointReflection R (midpoint R x y) : (a : P) → P) y = x
have rw : (pointReflection R (midpoint R y x) : (a : P) → P) y = x
Tactic: rw [midpoint_comm, AffineEquiv.pointReflection_midpoint_left]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
x y : P
rw : (pointReflection R (midpoint R y x) : (a : P) → P) y = x
⊢ (pointReflection R (midpoint R x y) : (a : P) → P) y = x
have rw₁ : x = x
Tactic: rw [midpoint_comm, AffineEquiv.pointReflection_midpoint_left]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
x y : P
⊢ (pointReflection (midpoint R x y) : (a : P) → P) y = x
have rw : (pointReflection (midpoint R y x) : (a : P) → P) y = x
Tactic: rw [midpoint_comm, Equiv.pointReflection_midpoint_left]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
x y : P
rw : (pointReflection (midpoint R y x) : (a : P) → P) y = x
⊢ (pointReflection (midpoint R x y) : (a : P) → P) y = x
have rw₁ : x = x
Tactic: rw [midpoint_comm, Equiv.pointReflection_midpoint_left]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
p₁ p₂ : P
⊢ midpoint R p₁ p₂ -ᵥ p₂ =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₂)
have rw : midpoint R p₂ p₁ -ᵥ p₂ =
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₂)
Tactic: rw [midpoint_comm, midpoint_vsub_left]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
p₁ p₂ : P
rw :
  midpoint R p₂ p₁ -ᵥ p₂ =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₂)
⊢ midpoint R p₁ p₂ -ᵥ p₂ =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₂)
have rw₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₂) =
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₂)
Tactic: rw [midpoint_comm, midpoint_vsub_left]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
p₁ p₂ : P
⊢ p₂ -ᵥ midpoint R p₁ p₂ =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₂ -ᵥ p₁)
have rw : p₂ -ᵥ midpoint R p₂ p₁ =
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₂ -ᵥ p₁)
Tactic: rw [midpoint_comm, left_vsub_midpoint]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
p₁ p₂ : P
rw :
  p₂ -ᵥ midpoint R p₂ p₁ =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₂ -ᵥ p₁)
⊢ p₂ -ᵥ midpoint R p₁ p₂ =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₂ -ᵥ p₁)
have rw₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₂ -ᵥ p₁) =
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₂ -ᵥ p₁)
Tactic: rw [midpoint_comm, left_vsub_midpoint]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
p₁ p₂ p : P
⊢ midpoint R p₁ p₂ -ᵥ p =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p) +
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₂ -ᵥ p)
have rw : midpoint R p₁ p₂ -ᵥ p =
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (p₁ -ᵥ p₂ - (p -ᵥ p₂)) +
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₂ -ᵥ p)
Tactic: rw [← vsub_sub_vsub_cancel_right p₁ p p₂, smul_sub, sub_eq_add_neg, ← smul_neg,
    neg_vsub_eq_vsub_rev, add_assoc, invOf_two_smul_add_invOf_two_smul, ← vadd_vsub_assoc,
    midpoint_comm, midpoint, lineMap_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
p₁ p₂ p : P
rw :
  midpoint R p₁ p₂ -ᵥ p =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
        (p₁ -ᵥ p₂ - (p -ᵥ p₂)) +
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₂ -ᵥ p)
⊢ midpoint R p₁ p₂ -ᵥ p =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p) +
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₂ -ᵥ p)
have rw₁ : midpoint R p₁ p₂ -ᵥ p =
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₂) -
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p -ᵥ p₂) +
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₂ -ᵥ p)
Tactic: rw [← vsub_sub_vsub_cancel_right p₁ p p₂, smul_sub, sub_eq_add_neg, ← smul_neg,
    neg_vsub_eq_vsub_rev, add_assoc, invOf_two_smul_add_invOf_two_smul, ← vadd_vsub_assoc,
    midpoint_comm, midpoint, lineMap_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
p₁ p₂ p : P
rw :
  midpoint R p₁ p₂ -ᵥ p =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
        (p₁ -ᵥ p₂ - (p -ᵥ p₂)) +
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₂ -ᵥ p)
rw₁ :
  midpoint R p₁ p₂ -ᵥ p =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₂) -
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p -ᵥ p₂) +
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₂ -ᵥ p)
⊢ midpoint R p₁ p₂ -ᵥ p =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p) +
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₂ -ᵥ p)
have rw₂ : midpoint R p₁ p₂ -ᵥ p =
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₂) +
      -HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p -ᵥ p₂) +
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₂ -ᵥ p)
Tactic: rw [← vsub_sub_vsub_cancel_right p₁ p p₂, smul_sub, sub_eq_add_neg, ← smul_neg,
    neg_vsub_eq_vsub_rev, add_assoc, invOf_two_smul_add_invOf_two_smul, ← vadd_vsub_assoc,
    midpoint_comm, midpoint, lineMap_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
p₁ p₂ p : P
rw :
  midpoint R p₁ p₂ -ᵥ p =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
        (p₁ -ᵥ p₂ - (p -ᵥ p₂)) +
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₂ -ᵥ p)
rw₁ :
  midpoint R p₁ p₂ -ᵥ p =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₂) -
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p -ᵥ p₂) +
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₂ -ᵥ p)
rw₂ :
  midpoint R p₁ p₂ -ᵥ p =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₂) +
        -HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p -ᵥ p₂) +
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₂ -ᵥ p)
⊢ midpoint R p₁ p₂ -ᵥ p =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p) +
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₂ -ᵥ p)
have rw₃ : midpoint R p₁ p₂ -ᵥ p =
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₂) +
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (-(p -ᵥ p₂)) +
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₂ -ᵥ p)
Tactic: rw [← vsub_sub_vsub_cancel_right p₁ p p₂, smul_sub, sub_eq_add_neg, ← smul_neg,
    neg_vsub_eq_vsub_rev, add_assoc, invOf_two_smul_add_invOf_two_smul, ← vadd_vsub_assoc,
    midpoint_comm, midpoint, lineMap_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
p₁ p₂ p : P
rw :
  midpoint R p₁ p₂ -ᵥ p =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
        (p₁ -ᵥ p₂ - (p -ᵥ p₂)) +
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₂ -ᵥ p)
rw₁ :
  midpoint R p₁ p₂ -ᵥ p =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₂) -
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p -ᵥ p₂) +
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₂ -ᵥ p)
rw₂ :
  midpoint R p₁ p₂ -ᵥ p =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₂) +
        -HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p -ᵥ p₂) +
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₂ -ᵥ p)
rw₃ :
  midpoint R p₁ p₂ -ᵥ p =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₂) +
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
          (-(p -ᵥ p₂)) +
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₂ -ᵥ p)
⊢ midpoint R p₁ p₂ -ᵥ p =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p) +
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₂ -ᵥ p)
have rw₄ : midpoint R p₁ p₂ -ᵥ p =
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₂) +
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₂ -ᵥ p) +
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₂ -ᵥ p)
Tactic: rw [← vsub_sub_vsub_cancel_right p₁ p p₂, smul_sub, sub_eq_add_neg, ← smul_neg,
    neg_vsub_eq_vsub_rev, add_assoc, invOf_two_smul_add_invOf_two_smul, ← vadd_vsub_assoc,
    midpoint_comm, midpoint, lineMap_apply]