awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.PerpBisector (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b p : P
hab : a ≠ b
hp : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector a b) p
s : ℝ
h_wbtw : Wbtw ℝ a b ((AffineMap.lineMap a b : (a : ℝ) → P) s)
rw : ⟪p -ᵥ midpoint ℝ a b, (AffineMap.lineMap a b : (a : ℝ) → P) s -ᵥ a + (a -ᵥ midpoint ℝ a b)⟫ = 0
rw₁ : ⟪p -ᵥ midpoint ℝ a b, s • (b -ᵥ a) + (a -ᵥ midpoint ℝ a b)⟫ = 0
rw₂ :
  ⟪p -ᵥ midpoint ℝ a b,
      s • (b -ᵥ a) + HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (a -ᵥ b)⟫ =
    0
rw₃ :
  ⟪p -ᵥ midpoint ℝ a b,
      s • (b -ᵥ a) + HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (-(b -ᵥ a))⟫ =
    0
⊢ ⟪p -ᵥ midpoint ℝ a b, (AffineMap.lineMap a b : (a : ℝ) → P) s -ᵥ midpoint ℝ a b⟫ = 0
have rw₄ : ⟪p -ᵥ midpoint ℝ a b,
    s • (b -ᵥ a) + -HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (b -ᵥ a)⟫ =
  0
Tactic: rw [← vsub_add_vsub_cancel (AffineMap.lineMap a b s) a, AffineMap.lineMap_vsub_left,
        left_vsub_midpoint, ← neg_vsub_eq_vsub_rev b a, smul_neg, ← sub_eq_add_neg,
        inner_sub_right, inner_smul_right, inner_smul_right,
        mem_perpBisector_iff_inner_eq_zero.mp hp, mul_zero, mul_zero, sub_self]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.PerpBisector (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b p : P
hab : a ≠ b
hp : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector a b) p
s : ℝ
h_wbtw : Wbtw ℝ a b ((AffineMap.lineMap a b : (a : ℝ) → P) s)
rw : ⟪p -ᵥ midpoint ℝ a b, (AffineMap.lineMap a b : (a : ℝ) → P) s -ᵥ a + (a -ᵥ midpoint ℝ a b)⟫ = 0
rw₁ : ⟪p -ᵥ midpoint ℝ a b, s • (b -ᵥ a) + (a -ᵥ midpoint ℝ a b)⟫ = 0
rw₂ :
  ⟪p -ᵥ midpoint ℝ a b,
      s • (b -ᵥ a) + HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (a -ᵥ b)⟫ =
    0
rw₃ :
  ⟪p -ᵥ midpoint ℝ a b,
      s • (b -ᵥ a) + HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (-(b -ᵥ a))⟫ =
    0
rw₄ :
  ⟪p -ᵥ midpoint ℝ a b,
      s • (b -ᵥ a) + -HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (b -ᵥ a)⟫ =
    0
⊢ ⟪p -ᵥ midpoint ℝ a b, (AffineMap.lineMap a b : (a : ℝ) → P) s -ᵥ midpoint ℝ a b⟫ = 0
have rw₅ : ⟪p -ᵥ midpoint ℝ a b,
    s • (b -ᵥ a) - HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (b -ᵥ a)⟫ =
  0
Tactic: rw [← vsub_add_vsub_cancel (AffineMap.lineMap a b s) a, AffineMap.lineMap_vsub_left,
        left_vsub_midpoint, ← neg_vsub_eq_vsub_rev b a, smul_neg, ← sub_eq_add_neg,
        inner_sub_right, inner_smul_right, inner_smul_right,
        mem_perpBisector_iff_inner_eq_zero.mp hp, mul_zero, mul_zero, sub_self]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.PerpBisector (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b p : P
hab : a ≠ b
hp : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector a b) p
s : ℝ
h_wbtw : Wbtw ℝ a b ((AffineMap.lineMap a b : (a : ℝ) → P) s)
rw : ⟪p -ᵥ midpoint ℝ a b, (AffineMap.lineMap a b : (a : ℝ) → P) s -ᵥ a + (a -ᵥ midpoint ℝ a b)⟫ = 0
rw₁ : ⟪p -ᵥ midpoint ℝ a b, s • (b -ᵥ a) + (a -ᵥ midpoint ℝ a b)⟫ = 0
rw₂ :
  ⟪p -ᵥ midpoint ℝ a b,
      s • (b -ᵥ a) + HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (a -ᵥ b)⟫ =
    0
rw₃ :
  ⟪p -ᵥ midpoint ℝ a b,
      s • (b -ᵥ a) + HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (-(b -ᵥ a))⟫ =
    0
rw₄ :
  ⟪p -ᵥ midpoint ℝ a b,
      s • (b -ᵥ a) + -HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (b -ᵥ a)⟫ =
    0
rw₅ :
  ⟪p -ᵥ midpoint ℝ a b,
      s • (b -ᵥ a) - HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (b -ᵥ a)⟫ =
    0
⊢ ⟪p -ᵥ midpoint ℝ a b, (AffineMap.lineMap a b : (a : ℝ) → P) s -ᵥ midpoint ℝ a b⟫ = 0
have rw₆ : ⟪p -ᵥ midpoint ℝ a b, s • (b -ᵥ a)⟫ -
    ⟪p -ᵥ midpoint ℝ a b,
      HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (b -ᵥ a)⟫ =
  0
Tactic: rw [← vsub_add_vsub_cancel (AffineMap.lineMap a b s) a, AffineMap.lineMap_vsub_left,
        left_vsub_midpoint, ← neg_vsub_eq_vsub_rev b a, smul_neg, ← sub_eq_add_neg,
        inner_sub_right, inner_smul_right, inner_smul_right,
        mem_perpBisector_iff_inner_eq_zero.mp hp, mul_zero, mul_zero, sub_self]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.PerpBisector (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b p : P
hab : a ≠ b
hp : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector a b) p
s : ℝ
h_wbtw : Wbtw ℝ a b ((AffineMap.lineMap a b : (a : ℝ) → P) s)
rw : ⟪p -ᵥ midpoint ℝ a b, (AffineMap.lineMap a b : (a : ℝ) → P) s -ᵥ a + (a -ᵥ midpoint ℝ a b)⟫ = 0
rw₁ : ⟪p -ᵥ midpoint ℝ a b, s • (b -ᵥ a) + (a -ᵥ midpoint ℝ a b)⟫ = 0
rw₂ :
  ⟪p -ᵥ midpoint ℝ a b,
      s • (b -ᵥ a) + HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (a -ᵥ b)⟫ =
    0
rw₃ :
  ⟪p -ᵥ midpoint ℝ a b,
      s • (b -ᵥ a) + HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (-(b -ᵥ a))⟫ =
    0
rw₄ :
  ⟪p -ᵥ midpoint ℝ a b,
      s • (b -ᵥ a) + -HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (b -ᵥ a)⟫ =
    0
rw₅ :
  ⟪p -ᵥ midpoint ℝ a b,
      s • (b -ᵥ a) - HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (b -ᵥ a)⟫ =
    0
rw₆ :
  ⟪p -ᵥ midpoint ℝ a b, s • (b -ᵥ a)⟫ -
      ⟪p -ᵥ midpoint ℝ a b,
        HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (b -ᵥ a)⟫ =
    0
⊢ ⟪p -ᵥ midpoint ℝ a b, (AffineMap.lineMap a b : (a : ℝ) → P) s -ᵥ midpoint ℝ a b⟫ = 0
have rw₇ : s * ⟪p -ᵥ midpoint ℝ a b, b -ᵥ a⟫ -
    ⟪p -ᵥ midpoint ℝ a b,
      HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (b -ᵥ a)⟫ =
  0
Tactic: rw [← vsub_add_vsub_cancel (AffineMap.lineMap a b s) a, AffineMap.lineMap_vsub_left,
        left_vsub_midpoint, ← neg_vsub_eq_vsub_rev b a, smul_neg, ← sub_eq_add_neg,
        inner_sub_right, inner_smul_right, inner_smul_right,
        mem_perpBisector_iff_inner_eq_zero.mp hp, mul_zero, mul_zero, sub_self]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.PerpBisector (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b p : P
hab : a ≠ b
hp : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector a b) p
s : ℝ
h_wbtw : Wbtw ℝ a b ((AffineMap.lineMap a b : (a : ℝ) → P) s)
rw : ⟪p -ᵥ midpoint ℝ a b, (AffineMap.lineMap a b : (a : ℝ) → P) s -ᵥ a + (a -ᵥ midpoint ℝ a b)⟫ = 0
rw₁ : ⟪p -ᵥ midpoint ℝ a b, s • (b -ᵥ a) + (a -ᵥ midpoint ℝ a b)⟫ = 0
rw₂ :
  ⟪p -ᵥ midpoint ℝ a b,
      s • (b -ᵥ a) + HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (a -ᵥ b)⟫ =
    0
rw₃ :
  ⟪p -ᵥ midpoint ℝ a b,
      s • (b -ᵥ a) + HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (-(b -ᵥ a))⟫ =
    0
rw₄ :
  ⟪p -ᵥ midpoint ℝ a b,
      s • (b -ᵥ a) + -HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (b -ᵥ a)⟫ =
    0
rw₅ :
  ⟪p -ᵥ midpoint ℝ a b,
      s • (b -ᵥ a) - HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (b -ᵥ a)⟫ =
    0
rw₆ :
  ⟪p -ᵥ midpoint ℝ a b, s • (b -ᵥ a)⟫ -
      ⟪p -ᵥ midpoint ℝ a b,
        HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (b -ᵥ a)⟫ =
    0
rw₇ :
  s * ⟪p -ᵥ midpoint ℝ a b, b -ᵥ a⟫ -
      ⟪p -ᵥ midpoint ℝ a b,
        HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (b -ᵥ a)⟫ =
    0
⊢ ⟪p -ᵥ midpoint ℝ a b, (AffineMap.lineMap a b : (a : ℝ) → P) s -ᵥ midpoint ℝ a b⟫ = 0
have rw₈ : s * ⟪p -ᵥ midpoint ℝ a b, b -ᵥ a⟫ -
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ * ⟪p -ᵥ midpoint ℝ a b, b -ᵥ a⟫ =
  0
Tactic: rw [← vsub_add_vsub_cancel (AffineMap.lineMap a b s) a, AffineMap.lineMap_vsub_left,
        left_vsub_midpoint, ← neg_vsub_eq_vsub_rev b a, smul_neg, ← sub_eq_add_neg,
        inner_sub_right, inner_smul_right, inner_smul_right,
        mem_perpBisector_iff_inner_eq_zero.mp hp, mul_zero, mul_zero, sub_self]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.PerpBisector (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b p : P
hab : a ≠ b
hp : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector a b) p
s : ℝ
h_wbtw : Wbtw ℝ a b ((AffineMap.lineMap a b : (a : ℝ) → P) s)
rw : ⟪p -ᵥ midpoint ℝ a b, (AffineMap.lineMap a b : (a : ℝ) → P) s -ᵥ a + (a -ᵥ midpoint ℝ a b)⟫ = 0
rw₁ : ⟪p -ᵥ midpoint ℝ a b, s • (b -ᵥ a) + (a -ᵥ midpoint ℝ a b)⟫ = 0
rw₂ :
  ⟪p -ᵥ midpoint ℝ a b,
      s • (b -ᵥ a) + HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (a -ᵥ b)⟫ =
    0
rw₃ :
  ⟪p -ᵥ midpoint ℝ a b,
      s • (b -ᵥ a) + HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (-(b -ᵥ a))⟫ =
    0
rw₄ :
  ⟪p -ᵥ midpoint ℝ a b,
      s • (b -ᵥ a) + -HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (b -ᵥ a)⟫ =
    0
rw₅ :
  ⟪p -ᵥ midpoint ℝ a b,
      s • (b -ᵥ a) - HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (b -ᵥ a)⟫ =
    0
rw₆ :
  ⟪p -ᵥ midpoint ℝ a b, s • (b -ᵥ a)⟫ -
      ⟪p -ᵥ midpoint ℝ a b,
        HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (b -ᵥ a)⟫ =
    0
rw₇ :
  s * ⟪p -ᵥ midpoint ℝ a b, b -ᵥ a⟫ -
      ⟪p -ᵥ midpoint ℝ a b,
        HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (b -ᵥ a)⟫ =
    0
rw₈ :
  s * ⟪p -ᵥ midpoint ℝ a b, b -ᵥ a⟫ -
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ * ⟪p -ᵥ midpoint ℝ a b, b -ᵥ a⟫ =
    0
⊢ ⟪p -ᵥ midpoint ℝ a b, (AffineMap.lineMap a b : (a : ℝ) → P) s -ᵥ midpoint ℝ a b⟫ = 0
have rw₉ : s * 0 - HMul.hMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) 0 = 0
Tactic: rw [← vsub_add_vsub_cancel (AffineMap.lineMap a b s) a, AffineMap.lineMap_vsub_left,
        left_vsub_midpoint, ← neg_vsub_eq_vsub_rev b a, smul_neg, ← sub_eq_add_neg,
        inner_sub_right, inner_smul_right, inner_smul_right,
        mem_perpBisector_iff_inner_eq_zero.mp hp, mul_zero, mul_zero, sub_self]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.PerpBisector (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b p : P
hab : a ≠ b
hp : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector a b) p
s : ℝ
h_wbtw : Wbtw ℝ a b ((AffineMap.lineMap a b : (a : ℝ) → P) s)
rw : ⟪p -ᵥ midpoint ℝ a b, (AffineMap.lineMap a b : (a : ℝ) → P) s -ᵥ a + (a -ᵥ midpoint ℝ a b)⟫ = 0
rw₁ : ⟪p -ᵥ midpoint ℝ a b, s • (b -ᵥ a) + (a -ᵥ midpoint ℝ a b)⟫ = 0
rw₂ :
  ⟪p -ᵥ midpoint ℝ a b,
      s • (b -ᵥ a) + HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (a -ᵥ b)⟫ =
    0
rw₃ :
  ⟪p -ᵥ midpoint ℝ a b,
      s • (b -ᵥ a) + HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (-(b -ᵥ a))⟫ =
    0
rw₄ :
  ⟪p -ᵥ midpoint ℝ a b,
      s • (b -ᵥ a) + -HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (b -ᵥ a)⟫ =
    0
rw₅ :
  ⟪p -ᵥ midpoint ℝ a b,
      s • (b -ᵥ a) - HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (b -ᵥ a)⟫ =
    0
rw₆ :
  ⟪p -ᵥ midpoint ℝ a b, s • (b -ᵥ a)⟫ -
      ⟪p -ᵥ midpoint ℝ a b,
        HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (b -ᵥ a)⟫ =
    0
rw₇ :
  s * ⟪p -ᵥ midpoint ℝ a b, b -ᵥ a⟫ -
      ⟪p -ᵥ midpoint ℝ a b,
        HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (b -ᵥ a)⟫ =
    0
rw₈ :
  s * ⟪p -ᵥ midpoint ℝ a b, b -ᵥ a⟫ -
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ * ⟪p -ᵥ midpoint ℝ a b, b -ᵥ a⟫ =
    0
rw₉ : s * 0 - HMul.hMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) 0 = 0
⊢ ⟪p -ᵥ midpoint ℝ a b, (AffineMap.lineMap a b : (a : ℝ) → P) s -ᵥ midpoint ℝ a b⟫ = 0
have rw₁₀ : 0 - HMul.hMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) 0 = 0
Tactic: rw [← vsub_add_vsub_cancel (AffineMap.lineMap a b s) a, AffineMap.lineMap_vsub_left,
        left_vsub_midpoint, ← neg_vsub_eq_vsub_rev b a, smul_neg, ← sub_eq_add_neg,
        inner_sub_right, inner_smul_right, inner_smul_right,
        mem_perpBisector_iff_inner_eq_zero.mp hp, mul_zero, mul_zero, sub_self]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.PerpBisector (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b p : P
hab : a ≠ b
hp : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector a b) p
s : ℝ
h_wbtw : Wbtw ℝ a b ((AffineMap.lineMap a b : (a : ℝ) → P) s)
rw : ⟪p -ᵥ midpoint ℝ a b, (AffineMap.lineMap a b : (a : ℝ) → P) s -ᵥ a + (a -ᵥ midpoint ℝ a b)⟫ = 0
rw₁ : ⟪p -ᵥ midpoint ℝ a b, s • (b -ᵥ a) + (a -ᵥ midpoint ℝ a b)⟫ = 0
rw₂ :
  ⟪p -ᵥ midpoint ℝ a b,
      s • (b -ᵥ a) + HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (a -ᵥ b)⟫ =
    0
rw₃ :
  ⟪p -ᵥ midpoint ℝ a b,
      s • (b -ᵥ a) + HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (-(b -ᵥ a))⟫ =
    0
rw₄ :
  ⟪p -ᵥ midpoint ℝ a b,
      s • (b -ᵥ a) + -HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (b -ᵥ a)⟫ =
    0
rw₅ :
  ⟪p -ᵥ midpoint ℝ a b,
      s • (b -ᵥ a) - HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (b -ᵥ a)⟫ =
    0
rw₆ :
  ⟪p -ᵥ midpoint ℝ a b, s • (b -ᵥ a)⟫ -
      ⟪p -ᵥ midpoint ℝ a b,
        HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (b -ᵥ a)⟫ =
    0
rw₇ :
  s * ⟪p -ᵥ midpoint ℝ a b, b -ᵥ a⟫ -
      ⟪p -ᵥ midpoint ℝ a b,
        HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (b -ᵥ a)⟫ =
    0
rw₈ :
  s * ⟪p -ᵥ midpoint ℝ a b, b -ᵥ a⟫ -
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ * ⟪p -ᵥ midpoint ℝ a b, b -ᵥ a⟫ =
    0
rw₉ : s * 0 - HMul.hMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) 0 = 0
rw₁₀ : 0 - HMul.hMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) 0 = 0
⊢ ⟪p -ᵥ midpoint ℝ a b, (AffineMap.lineMap a b : (a : ℝ) → P) s -ᵥ midpoint ℝ a b⟫ = 0
have rw₁₁ : HSub.hSub (α := ℝ) 0 0 = 0
Tactic: rw [← vsub_add_vsub_cancel (AffineMap.lineMap a b s) a, AffineMap.lineMap_vsub_left,
        left_vsub_midpoint, ← neg_vsub_eq_vsub_rev b a, smul_neg, ← sub_eq_add_neg,
        inner_sub_right, inner_smul_right, inner_smul_right,
        mem_perpBisector_iff_inner_eq_zero.mp hp, mul_zero, mul_zero, sub_self]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.PerpBisector (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b p : P
hab : a ≠ b
hp : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector a b) p
s : ℝ
h_wbtw : Wbtw ℝ a b ((AffineMap.lineMap a b : (a : ℝ) → P) s)
rw : ⟪p -ᵥ midpoint ℝ a b, (AffineMap.lineMap a b : (a : ℝ) → P) s -ᵥ a + (a -ᵥ midpoint ℝ a b)⟫ = 0
rw₁ : ⟪p -ᵥ midpoint ℝ a b, s • (b -ᵥ a) + (a -ᵥ midpoint ℝ a b)⟫ = 0
rw₂ :
  ⟪p -ᵥ midpoint ℝ a b,
      s • (b -ᵥ a) + HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (a -ᵥ b)⟫ =
    0
rw₃ :
  ⟪p -ᵥ midpoint ℝ a b,
      s • (b -ᵥ a) + HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (-(b -ᵥ a))⟫ =
    0
rw₄ :
  ⟪p -ᵥ midpoint ℝ a b,
      s • (b -ᵥ a) + -HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (b -ᵥ a)⟫ =
    0
rw₅ :
  ⟪p -ᵥ midpoint ℝ a b,
      s • (b -ᵥ a) - HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (b -ᵥ a)⟫ =
    0
rw₆ :
  ⟪p -ᵥ midpoint ℝ a b, s • (b -ᵥ a)⟫ -
      ⟪p -ᵥ midpoint ℝ a b,
        HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (b -ᵥ a)⟫ =
    0
rw₇ :
  s * ⟪p -ᵥ midpoint ℝ a b, b -ᵥ a⟫ -
      ⟪p -ᵥ midpoint ℝ a b,
        HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (b -ᵥ a)⟫ =
    0
rw₈ :
  s * ⟪p -ᵥ midpoint ℝ a b, b -ᵥ a⟫ -
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ * ⟪p -ᵥ midpoint ℝ a b, b -ᵥ a⟫ =
    0
rw₉ : s * 0 - HMul.hMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) 0 = 0
rw₁₀ : 0 - HMul.hMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) 0 = 0
rw₁₁ : HSub.hSub (α := ℝ) 0 0 = 0
⊢ ⟪p -ᵥ midpoint ℝ a b, (AffineMap.lineMap a b : (a : ℝ) → P) s -ᵥ midpoint ℝ a b⟫ = 0
have rw₁₂ : Eq (α := ℝ) 0 0
Tactic: rw [← vsub_add_vsub_cancel (AffineMap.lineMap a b s) a, AffineMap.lineMap_vsub_left,
        left_vsub_midpoint, ← neg_vsub_eq_vsub_rev b a, smul_neg, ← sub_eq_add_neg,
        inner_sub_right, inner_smul_right, inner_smul_right,
        mem_perpBisector_iff_inner_eq_zero.mp hp, mul_zero, mul_zero, sub_self]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.PerpBisector (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
c₁ c₂ p₁ p₂ : P
hc₁ : dist p₁ c₁ = dist p₂ c₁
hc₂ : dist p₁ c₂ = dist p₂ c₂
⊢ ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫ = 0
have rw : Membership.mem (γ := Submodule ℝ V) (direction (perpBisector p₁ p₂)) (c₂ -ᵥ c₁)
Tactic: rw [← Submodule.mem_orthogonal_singleton_iff_inner_left, ← direction_perpBisector]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.PerpBisector (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
c₁ c₂ p₁ p₂ : P
hc₁ : dist p₁ c₁ = dist p₂ c₁
hc₂ : dist p₁ c₂ = dist p₂ c₂
⊢ Membership.mem (γ := Submodule ℝ V) (direction (perpBisector p₁ p₂)) (c₂ -ᵥ c₁)
have hp₁ : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c₂
Tactic: apply vsub_mem_direction
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.PerpBisector (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
c₁ c₂ p₁ p₂ : P
hc₁ : dist p₁ c₁ = dist p₂ c₁
hc₂ : dist p₁ c₂ = dist p₂ c₂
hp₁ : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c₂
⊢ Membership.mem (γ := Submodule ℝ V) (direction (perpBisector p₁ p₂)) (c₂ -ᵥ c₁)
have hp₂ : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c₁
Tactic: apply vsub_mem_direction
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.PerpBisector (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
V' : Type u_3
P' : Type u_4
inst_4 : NormedAddCommGroup V'
inst_5 : InnerProductSpace ℝ V'
inst_6 : MetricSpace P'
inst_7 : NormedAddTorsor V' P'
f : P → P'
h : Isometry f
p₁ p₂ : P
⊢ f ⁻¹' (↑(perpBisector (f p₁) (f p₂)) : Set P') = (↑(perpBisector p₁ p₂) : Set P)
have h₁ : ∀ (x : P), x ∈ f ⁻¹' (↑(perpBisector (f p₁) (f p₂)) : Set P') ↔ x ∈ (↑(perpBisector p₁ p₂) : Set P)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p x : P
hx : x ∈ s
⊢ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) =
    HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (↑((s.direction.orthogonalProjection : (a : V) → ↥s.direction) (p -ᵥ x)) : V) x
have rw : (↑(Classical.arbitrary ↥s) : P) -ᵥ x ∈ s.direction
Tactic: rw [orthogonalProjection_apply, coe_vadd, vadd_eq_vadd_iff_sub_eq_vsub, ← Submodule.coe_sub,
    ← map_sub, vsub_sub_vsub_cancel_left, Submodule.coe_orthogonalProjection_apply,
    Submodule.starProjection_eq_self_iff]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s₁ s₂ : AffineSubspace 𝕜 P
p₁ p₂ : P
inst_5 : Nonempty.{u_3 + 1} ↥s₁
inst_6 : s₁.direction.HasOrthogonalProjection
h : s₁ = s₂
hp : p₁ = p₂
⊢ Eq.{u_3 + 1} (α := P) (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p₁) : P)
    (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p₂) : P)
have subst : Eq.{u_3 + 1} (α := P) (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p₁) : P)
  (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p₁) : P)
Tactic: subst h hp
Cleared hypotheses: s₂, p₂, h, hp
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p : P
⊢ Membership.mem (γ := AffineSubspace 𝕜 P) (mk' p s.directionᗮ) (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
have rw : p -ᵥ (↑(Classical.arbitrary ↥s) : P) -
    (↑((s.direction.orthogonalProjection : (a : V) → ↥s.direction) (p -ᵥ (↑(Classical.arbitrary ↥s) : P))) : V) ∈
  s.directionᗮ
Tactic: rw [mem_mk', orthogonalProjection_apply, coe_vadd, vadd_vsub_eq_sub_vsub,
    ← Submodule.neg_mem_iff, neg_sub]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p : P
⊢ IsCompl s.direction (direction (mk' p s.directionᗮ))
have rw : IsCompl s.direction s.directionᗮ
Tactic: rw [direction_mk' p s.directionᗮ]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p : P
⊢ (↑s : Set P) ∩ (↑(mk' p s.directionᗮ) : Set P) = {(↑((orthogonalProjection s : (a : P) → ↥s) p) : P)}
have obtain : ∀ (q : P) (hq : (↑s : Set P) ∩ (↑(mk' p s.directionᗮ) : Set P) = {q}),
  (↑s : Set P) ∩ (↑(mk' p s.directionᗮ) : Set P) = {(↑((orthogonalProjection s : (a : P) → ↥s) p) : P)}
Tactic: obtain ⟨q, hq⟩ := inter_eq_singleton_of_nonempty_of_isCompl (nonempty_subtype.mp ‹_›)
    (mk'_nonempty p s.directionᗮ)
    (by
      rw [direction_mk' p s.directionᗮ]
      exact Submodule.isCompl_orthogonal_of_hasOrthogonalProjection)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p : P
⊢ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) = p ↔ p ∈ s
have mp : (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) = p → p ∈ s
Tactic: constructor