awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint
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
rw₃ 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)
⊢ midpoint R x y = midpoint R y x

Tactic:
rw [midpoint, ← lineMap_apply_one_sub, one_sub_invOf_two, midpoint]

Premises used: one_sub_invOf_two, midpoint, AffineMap.lineMap_apply_one_sub
-- Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint
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
rw₁ rw₂ : x = x
⊢ (pointReflection R (midpoint R x y) : (a : P) → P) y = x

Tactic:
rw [midpoint_comm, AffineEquiv.pointReflection_midpoint_left]

Premises used: midpoint_comm, AffineEquiv.pointReflection_midpoint_left
-- Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint
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
rw₁ rw₂ : x = x
⊢ (pointReflection (midpoint R x y) : (a : P) → P) y = x

Tactic:
rw [midpoint_comm, Equiv.pointReflection_midpoint_left]

Premises used: midpoint_comm, Equiv.pointReflection_midpoint_left
-- Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint
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₂ -ᵥ midpoint R p₃ p₄ = midpoint R (p₁ -ᵥ p₃) (p₂ -ᵥ p₄)

Tactic:
lineMap_vsub_lineMap _ _ _ _ _

Premises used: midpoint, AffineMap.lineMap_vsub_lineMap
-- Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint
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
v v' : V
p p' : P
⊢ midpoint R v v' +ᵥ midpoint R p p' = midpoint R (v +ᵥ p) (v' +ᵥ p')

Tactic:
lineMap_vadd_lineMap _ _ _ _ _

Premises used: midpoint, AffineMap.lineMap_vadd_lineMap
-- Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint
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 z : P
⊢ midpoint R x y = z ↔ (pointReflection R z : (a : P) → P) x = y

Tactic:
eq_comm.trans
    ((injective_pointReflection_left_of_module R x).eq_iff'
        (AffineEquiv.pointReflection_midpoint_left x y)).symm

Premises used: Function.Injective.eq_iff', eq_comm, AffineEquiv.injective_pointReflection_left_of_module, Iff.trans, AffineEquiv.pointReflection_midpoint_left, Iff.symm
-- Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint
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 ((Equiv.pointReflection x : (a : P) → P) y) y = x

Tactic:
midpoint_eq_iff.2 <| Equiv.pointReflection_involutive _ _

Premises used: Iff.mpr, Equiv.pointReflection_involutive, midpoint_eq_iff
-- Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint
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 y ((Equiv.pointReflection x : (a : P) → P) y) = x

Tactic:
midpoint_eq_iff.2 rfl

Premises used: Iff.mpr, midpoint_eq_iff, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint
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 ((pointReflection R x : (a : P) → P) y) y = x

Tactic:
midpoint_pointReflection_left x y

Premises used: midpoint_pointReflection_left
-- Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint
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 y ((pointReflection R x : (a : P) → P) y) = x

Tactic:
midpoint_pointReflection_right x y

Premises used: midpoint_pointReflection_right
-- Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint
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₁)

Tactic:
lineMap_vsub_left _ _ _

Premises used: AffineMap.lineMap_vsub_left, midpoint
-- Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint
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₂)
rw₁ 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₂)
⊢ 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]

Premises used: midpoint_comm, midpoint_vsub_left
-- Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint
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₂)

Tactic:
left_vsub_lineMap _ _ _

Premises used: AffineMap.left_vsub_lineMap, midpoint
-- Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint
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₁)
rw₁ 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₁)
⊢ 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]

Premises used: midpoint_comm, left_vsub_midpoint
-- Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint
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
v₁ v₂ : V
⊢ midpoint R v₁ v₂ - v₁ =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (v₂ - v₁)

Tactic:
midpoint_vsub_left v₁ v₂

Premises used: midpoint_vsub_left
-- Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint
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
v₁ v₂ : V
⊢ midpoint R v₁ v₂ - v₂ =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (v₁ - v₂)

Tactic:
midpoint_vsub_right v₁ v₂

Premises used: midpoint_vsub_right
-- Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint
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
v₁ v₂ : V
⊢ v₁ - midpoint R v₁ v₂ =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (v₁ - v₂)

Tactic:
left_vsub_midpoint v₁ v₂

Premises used: left_vsub_midpoint
-- Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint
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
v₁ v₂ : V
⊢ v₂ - midpoint R v₁ v₂ =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (v₂ - v₁)

Tactic:
right_vsub_midpoint v₁ v₂

Premises used: right_vsub_midpoint
-- Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint
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
rw₁ rw₂ : x = y ↔ x = y
⊢ midpoint R x y = x ↔ x = y

Tactic:
rw [midpoint_eq_iff, pointReflection_self]

Premises used: midpoint_eq_iff, AffineEquiv.pointReflection_self
-- Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint
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
rw₁ rw₂ : x = y ↔ x = y
⊢ x = midpoint R x y ↔ x = y

Tactic:
rw [eq_comm, midpoint_eq_left_iff]

Premises used: midpoint_eq_left_iff, eq_comm
-- Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint
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
rw₂ rw₃ : x = y ↔ x = y
⊢ midpoint R x y = y ↔ x = y

Tactic:
rw [midpoint_comm, midpoint_eq_left_iff, eq_comm]

Premises used: midpoint_eq_left_iff, midpoint_comm, eq_comm
-- Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint
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
rw₁ rw₂ : x = y ↔ x = y
⊢ y = midpoint R x y ↔ x = y

Tactic:
rw [eq_comm, midpoint_eq_right_iff]

Premises used: midpoint_eq_right_iff, eq_comm
-- Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint
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
rw₉ rw₁₀ : x -ᵥ x' = y' -ᵥ y ↔ x -ᵥ x' = y' -ᵥ y
⊢ midpoint R x y = midpoint R x' 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]

Premises used: vsub_eq_zero_iff_eq, neg_eq_iff_eq_neg, midpoint_vsub_midpoint, AffineEquiv.pointReflection_apply, midpoint_eq_iff, vadd_eq_add, neg_vsub_eq_vsub_rev, add_zero, vsub_eq_sub, zero_sub
-- Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint
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 z : P
⊢ midpoint R x y = z ↔ (Equiv.pointReflection z : (a : P) → P) x = y

Tactic:
midpoint_eq_iff

Premises used: midpoint_eq_iff
-- Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint
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
R' : Type u_6
inst_5 : Ring R'
inst_6 : Invertible (α := R') 2
inst_7 : Module R' V
x y : P
⊢ midpoint R x y = midpoint R' x y

Tactic:
(midpoint_eq_iff' R).2 <| (midpoint_eq_iff' R').1 rfl

Premises used: Iff.mpr, midpoint_eq_iff', Iff.mp, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint
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 : P
⊢ midpoint R x x = x

Tactic:
lineMap_same_apply _ _

Premises used: AffineMap.lineMap_same_apply, midpoint
-- Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint
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 rw₁ : midpoint R y x +ᵥ midpoint R y x = midpoint R y x +ᵥ midpoint R y x
⊢ midpoint R x y +ᵥ midpoint R x y = midpoint R x y +ᵥ midpoint R y x

Tactic:
rw [midpoint_comm]

Premises used: midpoint_comm
-- Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint
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
rw₄ rw₅ : y + x = y + x
⊢ midpoint R x y +ᵥ midpoint R y x = x + y

Tactic:
rw [midpoint_vadd_midpoint, vadd_eq_add, vadd_eq_add, add_comm, midpoint_self]

Premises used: midpoint_self, add_comm, midpoint_vadd_midpoint, vadd_eq_add
-- Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint
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
⊢ 0 -ᵥ x = y -ᵥ (x + y)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint
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
rw₉ rw₁₀ : y = y
⊢ midpoint R x y =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (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]

Premises used: add_sub_cancel_left, two_smul, smul_smul, mul_invOf_self, one_smul, AffineEquiv.pointReflection_apply, midpoint_eq_iff, vadd_eq_add, sub_add_eq_add_sub, vsub_eq_sub
-- Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint
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
rw₂ rw₃ : Eq.{u_2 + 1} (α := V) 0 0
⊢ midpoint R x (-x) = 0

Tactic:
rw [midpoint_eq_smul_add, add_neg_cancel, smul_zero]

Premises used: add_neg_cancel, midpoint_eq_smul_add, smul_zero
-- Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint
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

Tactic:
simpa using midpoint_self_neg R (-x)

Premises used: Neg.neg, midpoint_self_neg
-- Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint
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 x +ᵥ midpoint R (-y) y = x
⊢ midpoint R (x - y) (x + y) = x

Tactic:
rw [sub_eq_add_neg, ← vadd_eq_add, ← vadd_eq_add, ← midpoint_vadd_midpoint]

Premises used: sub_eq_add_neg, midpoint_vadd_midpoint, vadd_eq_add
-- Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint
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 x +ᵥ midpoint R (-y) y = x

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint
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) (x + y) = x
⊢ midpoint R (x + y) (x - y) = x

Tactic:
rw [midpoint_comm]

Premises used: midpoint_comm
-- Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint
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

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint
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₂ -ᵥ p₃) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₂ -ᵥ p₃)
rw₁ :
  midpoint R 0 (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 _) (0 + (p₂ -ᵥ p₃)) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₂ -ᵥ p₃)
rw₃ 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₃)
⊢ midpoint R p₁ 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_vsub_midpoint, vsub_self, midpoint_eq_smul_add, zero_add]

Premises used: midpoint_eq_smul_add, zero_add, midpoint_vsub_midpoint, vsub_self
-- Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint
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₃ -ᵥ p₃) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₂)
rw₁ :
  midpoint R (p₁ -ᵥ p₂) 0 =
    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₂ + 0) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₂)
rw₃ 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₂)
⊢ midpoint R p₁ 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_vsub_midpoint, vsub_self, midpoint_eq_smul_add, add_zero]

Premises used: midpoint_eq_smul_add, midpoint_vsub_midpoint, add_zero, vsub_self
-- Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup E
inst_3 : Module R E
inst_4 : Ring R'
inst_5 : Invertible (α := R') 2
inst_6 : AddCommGroup F
inst_7 : Module R' F
f : E → F
h0 : f 0 = 0
hm : ∀ (x y : E), f (midpoint R x y) = midpoint R' (f x) (f y)
x y : E
rw : f (x + y) = 0 + f (x + y)
rw₁ rw₂ : f (x + y) = f (x + y)
⊢ f (x + y) = f 0 + f (x + y)

Tactic:
rw [h0, zero_add]

Premises used: zero_add
-- Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup E
inst_3 : Module R E
inst_4 : Ring R'
inst_5 : Invertible (α := R') 2
inst_6 : AddCommGroup F
inst_7 : Module R' F
f : E → F
h0 : f 0 = 0
hm : ∀ (x y : E), f (midpoint R x y) = midpoint R' (f x) (f y)
x y : E
rw : f (midpoint R 0 (x + y)) + f (midpoint R 0 (x + y)) = f (midpoint R x y) + f (midpoint R x y)
rw₁ rw₂ : f (midpoint R x y) + f (midpoint R x y) = f (midpoint R x y) + f (midpoint R x y)
⊢ midpoint R' (f 0) (f (x + y)) + midpoint R' (f 0) (f (x + y)) = f (midpoint R x y) + f (midpoint R x y)

Tactic:
rw [← hm, midpoint_zero_add]

Premises used: midpoint_zero_add
-- Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup E
inst_3 : Module R E
inst_4 : Ring R'
inst_5 : Invertible (α := R') 2
inst_6 : AddCommGroup F
inst_7 : Module R' F
f : E → F
h0 : f 0 = 0
hm : ∀ (x y : E), f (midpoint R x y) = midpoint R' (f x) (f y)
x y : E
rw : midpoint R' (f x) (f y) + midpoint R' (f x) (f y) = f x + f y
rw₁ rw₂ : f x + f y = f x + f y
⊢ f (midpoint R x y) + f (midpoint R x y) = f x + f y

Tactic:
rw [hm, midpoint_add_self]

Premises used: midpoint_add_self
-- Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup E
inst_3 : Module R E
inst_4 : Ring R'
inst_5 : Invertible (α := R') 2
inst_6 : AddCommGroup F
inst_7 : Module R' F
f : E → F
h0 : f 0 = 0
hm : ∀ (x y : E), f (midpoint R x y) = midpoint R' (f x) (f y)
⊢ (⇑(ofMapMidpoint R R' f h0 hm) : (a : E) → F) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.MidpointZero
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing R
inst_1 : CharZero R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
a b : P
⊢ (lineMap a b : (a : R) → P) 2⁻¹ = midpoint R a b

Tactic:
rfl

Premises used: midpoint, rfl