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
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)
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)
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₂) +
    (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
⊢ p -ᵥ midpoint R 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₂)
Tactic: rw [← neg_vsub_eq_vsub_rev, midpoint_vsub, neg_add, ← smul_neg, ← smul_neg, neg_vsub_eq_vsub_rev,
    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
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₁) +
      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₁) +
      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)) =
  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 [← neg_vsub_eq_vsub_rev, midpoint_vsub, neg_add, ← smul_neg, ← smul_neg, neg_vsub_eq_vsub_rev,
    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
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₁) +
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p -ᵥ p₂)
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)) =
    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₂)
⊢ p -ᵥ midpoint R 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₂ : -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₁) +
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p -ᵥ p₂)
Tactic: rw [← neg_vsub_eq_vsub_rev, midpoint_vsub, neg_add, ← smul_neg, ← smul_neg, neg_vsub_eq_vsub_rev,
    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
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₁) +
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p -ᵥ p₂)
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)) =
    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₂ :
  -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₁) +
      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₁) +
      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) =
  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 [← neg_vsub_eq_vsub_rev, midpoint_vsub, neg_add, ← smul_neg, ← smul_neg, neg_vsub_eq_vsub_rev,
    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
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₁) +
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p -ᵥ p₂)
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)) =
    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₂ :
  -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₁) +
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p -ᵥ p₂)
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) =
    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₂)
⊢ p -ᵥ midpoint R 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₄ : 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₁) +
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p -ᵥ p₂)
Tactic: rw [← neg_vsub_eq_vsub_rev, midpoint_vsub, neg_add, ← smul_neg, ← smul_neg, neg_vsub_eq_vsub_rev,
    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 y : P
⊢ midpoint R x y = x ↔ x = y
have rw : (pointReflection R x : (a : P) → P) x = y ↔ x = y
Tactic: rw [midpoint_eq_iff, pointReflection_self]
-- 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 x : (a : P) → P) x = y ↔ x = y
⊢ midpoint R x y = x ↔ x = y
have rw₁ : x = y ↔ x = y
Tactic: rw [midpoint_eq_iff, pointReflection_self]
-- 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
⊢ x = midpoint R x y ↔ x = y
have rw : midpoint R x y = x ↔ x = y
Tactic: rw [eq_comm, midpoint_eq_left_iff]
-- 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 : midpoint R x y = x ↔ x = y
⊢ x = midpoint R x y ↔ x = y
have rw₁ : x = y ↔ x = y
Tactic: rw [eq_comm, midpoint_eq_left_iff]
-- 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 = y ↔ x = y
have rw : midpoint R y x = y ↔ x = y
Tactic: rw [midpoint_comm, midpoint_eq_left_iff, eq_comm]
-- 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 : midpoint R y x = y ↔ x = y
⊢ midpoint R x y = y ↔ x = y
have rw₁ : y = x ↔ x = y
Tactic: rw [midpoint_comm, midpoint_eq_left_iff, eq_comm]
-- 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 : midpoint R y x = y ↔ x = y
rw₁ : y = x ↔ x = y
⊢ midpoint R x y = y ↔ x = y
have rw₂ : x = y ↔ x = y
Tactic: rw [midpoint_comm, midpoint_eq_left_iff, eq_comm]
-- 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
⊢ y = midpoint R x y ↔ x = y
have rw : midpoint R x y = y ↔ x = y
Tactic: rw [eq_comm, midpoint_eq_right_iff]
-- 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 : midpoint R x y = y ↔ x = y
⊢ y = midpoint R x y ↔ x = y
have rw₁ : x = y ↔ x = y
Tactic: rw [eq_comm, midpoint_eq_right_iff]
-- 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
⊢ midpoint R x y = midpoint R x' y' ↔ x -ᵥ x' = y' -ᵥ y
have rw : midpoint R x y -ᵥ midpoint R x' y' = 0 ↔ 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
⊢ midpoint R x y = midpoint R x' y' ↔ x -ᵥ x' = y' -ᵥ y
have rw₁ : midpoint R (x -ᵥ x') (y -ᵥ y') = 0 ↔ 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
⊢ midpoint R x y = midpoint R x' y' ↔ x -ᵥ x' = y' -ᵥ y
have rw₂ : (pointReflection R 0 : (a : V) → V) (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
⊢ midpoint R x y = midpoint R x' y' ↔ x -ᵥ x' = y' -ᵥ y
have rw₃ : HVAdd.hVAdd (β := V) (0 -ᵥ (x -ᵥ x')) 0 = 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
⊢ midpoint R x y = midpoint R x' y' ↔ x -ᵥ x' = y' -ᵥ y
have rw₄ : HVAdd.hVAdd (β := V) (0 - (x -ᵥ x')) 0 = 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
⊢ midpoint R x y = midpoint R x' y' ↔ x -ᵥ x' = y' -ᵥ y
have rw₅ : HVAdd.hVAdd (β := V) (-(x -ᵥ x')) 0 = 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
⊢ midpoint R x y = midpoint R x' y' ↔ x -ᵥ x' = y' -ᵥ y
have rw₆ : -(x -ᵥ x') + 0 = 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]