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 x' y y' : P
rw : midpoint R x y -ᵥ midpoint R x' y' = 0 ↔ x -ᵥ x' = y' -ᵥ y
rw₁ : midpoint R (x -ᵥ x') (y -ᵥ y') = 0 ↔ x -ᵥ x' = y' -ᵥ y
rw₂ : (pointReflection R 0 : (a : V) → V) (x -ᵥ x') = y -ᵥ y' ↔ x -ᵥ x' = y' -ᵥ y
rw₃ : HVAdd.hVAdd (β := V) (0 -ᵥ (x -ᵥ x')) 0 = y -ᵥ y' ↔ x -ᵥ x' = y' -ᵥ y
rw₄ : HVAdd.hVAdd (β := V) (0 - (x -ᵥ x')) 0 = y -ᵥ y' ↔ x -ᵥ x' = y' -ᵥ y
rw₅ : HVAdd.hVAdd (β := V) (-(x -ᵥ x')) 0 = y -ᵥ y' ↔ x -ᵥ x' = y' -ᵥ y
rw₆ : -(x -ᵥ x') + 0 = y -ᵥ y' ↔ x -ᵥ x' = y' -ᵥ y
⊢ midpoint R x y = midpoint R x' y' ↔ x -ᵥ x' = y' -ᵥ y
have rw₇ : -(x -ᵥ x') = y -ᵥ y' ↔ x -ᵥ x' = y' -ᵥ y
Tactic: rw [← @vsub_eq_zero_iff_eq V, midpoint_vsub_midpoint, midpoint_eq_iff, pointReflection_apply,
    vsub_eq_sub, zero_sub, vadd_eq_add, add_zero, neg_eq_iff_eq_neg, neg_vsub_eq_vsub_rev]
-- 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 x' y y' : P
rw : midpoint R x y -ᵥ midpoint R x' y' = 0 ↔ x -ᵥ x' = y' -ᵥ y
rw₁ : midpoint R (x -ᵥ x') (y -ᵥ y') = 0 ↔ x -ᵥ x' = y' -ᵥ y
rw₂ : (pointReflection R 0 : (a : V) → V) (x -ᵥ x') = y -ᵥ y' ↔ x -ᵥ x' = y' -ᵥ y
rw₃ : HVAdd.hVAdd (β := V) (0 -ᵥ (x -ᵥ x')) 0 = y -ᵥ y' ↔ x -ᵥ x' = y' -ᵥ y
rw₄ : HVAdd.hVAdd (β := V) (0 - (x -ᵥ x')) 0 = y -ᵥ y' ↔ x -ᵥ x' = y' -ᵥ y
rw₅ : HVAdd.hVAdd (β := V) (-(x -ᵥ x')) 0 = y -ᵥ y' ↔ x -ᵥ x' = y' -ᵥ y
rw₆ : -(x -ᵥ x') + 0 = y -ᵥ y' ↔ x -ᵥ x' = y' -ᵥ y
rw₇ : -(x -ᵥ x') = y -ᵥ y' ↔ x -ᵥ x' = y' -ᵥ y
⊢ midpoint R x y = midpoint R x' y' ↔ x -ᵥ x' = y' -ᵥ y
have rw₈ : x -ᵥ x' = -(y -ᵥ y') ↔ x -ᵥ x' = y' -ᵥ y
Tactic: rw [← @vsub_eq_zero_iff_eq V, midpoint_vsub_midpoint, midpoint_eq_iff, pointReflection_apply,
    vsub_eq_sub, zero_sub, vadd_eq_add, add_zero, neg_eq_iff_eq_neg, neg_vsub_eq_vsub_rev]
-- 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 x' y y' : P
rw : midpoint R x y -ᵥ midpoint R x' y' = 0 ↔ x -ᵥ x' = y' -ᵥ y
rw₁ : midpoint R (x -ᵥ x') (y -ᵥ y') = 0 ↔ x -ᵥ x' = y' -ᵥ y
rw₂ : (pointReflection R 0 : (a : V) → V) (x -ᵥ x') = y -ᵥ y' ↔ x -ᵥ x' = y' -ᵥ y
rw₃ : HVAdd.hVAdd (β := V) (0 -ᵥ (x -ᵥ x')) 0 = y -ᵥ y' ↔ x -ᵥ x' = y' -ᵥ y
rw₄ : HVAdd.hVAdd (β := V) (0 - (x -ᵥ x')) 0 = y -ᵥ y' ↔ x -ᵥ x' = y' -ᵥ y
rw₅ : HVAdd.hVAdd (β := V) (-(x -ᵥ x')) 0 = y -ᵥ y' ↔ x -ᵥ x' = y' -ᵥ y
rw₆ : -(x -ᵥ x') + 0 = y -ᵥ y' ↔ x -ᵥ x' = y' -ᵥ y
rw₇ : -(x -ᵥ x') = y -ᵥ y' ↔ x -ᵥ x' = y' -ᵥ y
rw₈ : x -ᵥ x' = -(y -ᵥ y') ↔ x -ᵥ x' = y' -ᵥ y
⊢ midpoint R x y = midpoint R x' y' ↔ x -ᵥ x' = y' -ᵥ y
have rw₉ : x -ᵥ x' = y' -ᵥ y ↔ x -ᵥ x' = y' -ᵥ y
Tactic: rw [← @vsub_eq_zero_iff_eq V, midpoint_vsub_midpoint, midpoint_eq_iff, pointReflection_apply,
    vsub_eq_sub, zero_sub, vadd_eq_add, add_zero, neg_eq_iff_eq_neg, neg_vsub_eq_vsub_rev]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
x y : V
⊢ midpoint R x y +ᵥ midpoint R x y = midpoint R x y +ᵥ midpoint R y x
have rw : midpoint R y x +ᵥ midpoint R y x = midpoint R y x +ᵥ midpoint R y x
Tactic: rw [midpoint_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
x y : V
⊢ midpoint R x y +ᵥ midpoint R y x = x + y
have rw : midpoint R (x +ᵥ y) (y +ᵥ x) = x + y
Tactic: rw [midpoint_vadd_midpoint, vadd_eq_add, vadd_eq_add, add_comm, midpoint_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
x y : V
rw : midpoint R (x +ᵥ y) (y +ᵥ x) = x + y
⊢ midpoint R x y +ᵥ midpoint R y x = x + y
have rw₁ : midpoint R (x + y) (y +ᵥ x) = x + y
Tactic: rw [midpoint_vadd_midpoint, vadd_eq_add, vadd_eq_add, add_comm, midpoint_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
x y : V
rw : midpoint R (x +ᵥ y) (y +ᵥ x) = x + y
rw₁ : midpoint R (x + y) (y +ᵥ x) = x + y
⊢ midpoint R x y +ᵥ midpoint R y x = x + y
have rw₂ : midpoint R (x + y) (y + x) = x + y
Tactic: rw [midpoint_vadd_midpoint, vadd_eq_add, vadd_eq_add, add_comm, midpoint_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
x y : V
rw : midpoint R (x +ᵥ y) (y +ᵥ x) = x + y
rw₁ : midpoint R (x + y) (y +ᵥ x) = x + y
rw₂ : midpoint R (x + y) (y + x) = x + y
⊢ midpoint R x y +ᵥ midpoint R y x = x + y
have rw₃ : midpoint R (y + x) (y + x) = y + x
Tactic: rw [midpoint_vadd_midpoint, vadd_eq_add, vadd_eq_add, add_comm, midpoint_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
x y : V
rw : midpoint R (x +ᵥ y) (y +ᵥ x) = x + y
rw₁ : midpoint R (x + y) (y +ᵥ x) = x + y
rw₂ : midpoint R (x + y) (y + x) = x + y
rw₃ : midpoint R (y + x) (y + x) = y + x
⊢ midpoint R x y +ᵥ midpoint R y x = x + y
have rw₄ : y + x = y + x
Tactic: rw [midpoint_vadd_midpoint, vadd_eq_add, vadd_eq_add, add_comm, midpoint_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
x y : V
⊢ midpoint R x y =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y)
have rw : (pointReflection R
        (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y)) :
      (a : V) → V)
    x =
  y
Tactic: rw [midpoint_eq_iff, pointReflection_apply, vsub_eq_sub, vadd_eq_add, sub_add_eq_add_sub, ←
    two_smul R, smul_smul, mul_invOf_self, one_smul, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
x y : V
rw :
  (pointReflection R
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
            (x + y)) :
        (a : V) → V)
      x =
    y
⊢ midpoint R x y =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y)
have rw₁ : (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) -ᵥ x) +ᵥ
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) =
  y
Tactic: rw [midpoint_eq_iff, pointReflection_apply, vsub_eq_sub, vadd_eq_add, sub_add_eq_add_sub, ←
    two_smul R, smul_smul, mul_invOf_self, one_smul, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
x y : V
rw :
  (pointReflection R
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
            (x + y)) :
        (a : V) → V)
      x =
    y
rw₁ :
  (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) -ᵥ x) +ᵥ
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) =
    y
⊢ midpoint R x y =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y)
have rw₂ : (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) - x) +ᵥ
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) =
  y
Tactic: rw [midpoint_eq_iff, pointReflection_apply, vsub_eq_sub, vadd_eq_add, sub_add_eq_add_sub, ←
    two_smul R, smul_smul, mul_invOf_self, one_smul, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
x y : V
rw :
  (pointReflection R
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
            (x + y)) :
        (a : V) → V)
      x =
    y
rw₁ :
  (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) -ᵥ x) +ᵥ
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) =
    y
rw₂ :
  (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) - x) +ᵥ
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) =
    y
⊢ midpoint R x y =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y)
have rw₃ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) - x +
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) =
  y
Tactic: rw [midpoint_eq_iff, pointReflection_apply, vsub_eq_sub, vadd_eq_add, sub_add_eq_add_sub, ←
    two_smul R, smul_smul, mul_invOf_self, one_smul, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
x y : V
rw :
  (pointReflection R
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
            (x + y)) :
        (a : V) → V)
      x =
    y
rw₁ :
  (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) -ᵥ x) +ᵥ
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) =
    y
rw₂ :
  (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) - x) +ᵥ
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) =
    y
rw₃ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) - x +
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) =
    y
⊢ midpoint R x y =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y)
have rw₄ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) +
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) -
    x =
  y
Tactic: rw [midpoint_eq_iff, pointReflection_apply, vsub_eq_sub, vadd_eq_add, sub_add_eq_add_sub, ←
    two_smul R, smul_smul, mul_invOf_self, one_smul, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
x y : V
rw :
  (pointReflection R
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
            (x + y)) :
        (a : V) → V)
      x =
    y
rw₁ :
  (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) -ᵥ x) +ᵥ
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) =
    y
rw₂ :
  (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) - x) +ᵥ
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) =
    y
rw₃ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) - x +
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) =
    y
rw₄ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) +
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) -
      x =
    y
⊢ midpoint R x y =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y)
have rw₅ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y)) -
    x =
  y
Tactic: rw [midpoint_eq_iff, pointReflection_apply, vsub_eq_sub, vadd_eq_add, sub_add_eq_add_sub, ←
    two_smul R, smul_smul, mul_invOf_self, one_smul, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
x y : V
rw :
  (pointReflection R
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
            (x + y)) :
        (a : V) → V)
      x =
    y
rw₁ :
  (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) -ᵥ x) +ᵥ
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) =
    y
rw₂ :
  (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) - x) +ᵥ
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) =
    y
rw₃ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) - x +
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) =
    y
rw₄ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) +
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) -
      x =
    y
rw₅ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2
        (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y)) -
      x =
    y
⊢ midpoint R x y =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y)
have rw₆ : HMul.hMul (α := R) 2 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) • (x + y) - x = y
Tactic: rw [midpoint_eq_iff, pointReflection_apply, vsub_eq_sub, vadd_eq_add, sub_add_eq_add_sub, ←
    two_smul R, smul_smul, mul_invOf_self, one_smul, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
x y : V
rw :
  (pointReflection R
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
            (x + y)) :
        (a : V) → V)
      x =
    y
rw₁ :
  (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) -ᵥ x) +ᵥ
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) =
    y
rw₂ :
  (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) - x) +ᵥ
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) =
    y
rw₃ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) - x +
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) =
    y
rw₄ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) +
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) -
      x =
    y
rw₅ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2
        (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y)) -
      x =
    y
rw₆ : HMul.hMul (α := R) 2 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) • (x + y) - x = y
⊢ midpoint R x y =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y)
have rw₇ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 (x + y) - x = y
Tactic: rw [midpoint_eq_iff, pointReflection_apply, vsub_eq_sub, vadd_eq_add, sub_add_eq_add_sub, ←
    two_smul R, smul_smul, mul_invOf_self, one_smul, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
x y : V
rw :
  (pointReflection R
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
            (x + y)) :
        (a : V) → V)
      x =
    y
rw₁ :
  (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) -ᵥ x) +ᵥ
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) =
    y
rw₂ :
  (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) - x) +ᵥ
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) =
    y
rw₃ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) - x +
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) =
    y
rw₄ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) +
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) -
      x =
    y
rw₅ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2
        (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y)) -
      x =
    y
rw₆ : HMul.hMul (α := R) 2 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) • (x + y) - x = y
rw₇ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 (x + y) - x = y
⊢ midpoint R x y =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y)
have rw₈ : x + y - x = y
Tactic: rw [midpoint_eq_iff, pointReflection_apply, vsub_eq_sub, vadd_eq_add, sub_add_eq_add_sub, ←
    two_smul R, smul_smul, mul_invOf_self, one_smul, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
x y : V
rw :
  (pointReflection R
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
            (x + y)) :
        (a : V) → V)
      x =
    y
rw₁ :
  (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) -ᵥ x) +ᵥ
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) =
    y
rw₂ :
  (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) - x) +ᵥ
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) =
    y
rw₃ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) - x +
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) =
    y
rw₄ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) +
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y) -
      x =
    y
rw₅ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2
        (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y)) -
      x =
    y
rw₆ : HMul.hMul (α := R) 2 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) • (x + y) - x = y
rw₇ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 (x + y) - x = y
rw₈ : x + y - x = y
⊢ midpoint R x y =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + y)
have rw₉ : y = y
Tactic: rw [midpoint_eq_iff, pointReflection_apply, vsub_eq_sub, vadd_eq_add, sub_add_eq_add_sub, ←
    two_smul R, smul_smul, mul_invOf_self, one_smul, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
x : V
⊢ midpoint R x (-x) = 0
have rw : HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + -x) = 0
Tactic: rw [midpoint_eq_smul_add, add_neg_cancel, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
x : V
rw : HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + -x) = 0
⊢ midpoint R x (-x) = 0
have rw₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) 0 = 0
Tactic: rw [midpoint_eq_smul_add, add_neg_cancel, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
x : V
rw : HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + -x) = 0
rw₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) 0 = 0
⊢ midpoint R x (-x) = 0
have rw₂ : Eq.{u_2 + 1} (α := V) 0 0
Tactic: rw [midpoint_eq_smul_add, add_neg_cancel, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
x y : V
⊢ midpoint R (x - y) (x + y) = x
have rw : midpoint R x x +ᵥ midpoint R (-y) y = x
Tactic: rw [sub_eq_add_neg, ← vadd_eq_add, ← vadd_eq_add, ← midpoint_vadd_midpoint]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
x y : V
⊢ midpoint R (x + y) (x - y) = x
have rw : midpoint R (x - y) (x + y) = x
Tactic: rw [midpoint_comm]