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
c p₁ p₂ : P
rw :
  ⟪c -ᵥ midpoint ℝ p₁ ((Equiv.pointReflection p₂ : (a : P) → P) p₁),
        (Equiv.pointReflection p₂ : (a : P) → P) p₁ -ᵥ p₁⟫ =
      0 ↔
    ⟪c -ᵥ p₂, p₁ -ᵥ p₂⟫ = 0
rw₁ : ⟪c -ᵥ p₂, (Equiv.pointReflection p₂ : (a : P) → P) p₁ -ᵥ p₁⟫ = 0 ↔ ⟪c -ᵥ p₂, p₁ -ᵥ p₂⟫ = 0
rw₂ : ⟪c -ᵥ p₂, ((p₂ -ᵥ p₁) +ᵥ p₂) -ᵥ p₁⟫ = 0 ↔ ⟪c -ᵥ p₂, p₁ -ᵥ p₂⟫ = 0
rw₃ : ⟪c -ᵥ p₂, p₂ -ᵥ p₁ + (p₂ -ᵥ p₁)⟫ = 0 ↔ ⟪c -ᵥ p₂, p₁ -ᵥ p₂⟫ = 0
rw₄ : ⟪c -ᵥ p₂, p₂ -ᵥ p₁⟫ + ⟪c -ᵥ p₂, p₂ -ᵥ p₁⟫ = 0 ↔ ⟪c -ᵥ p₂, p₁ -ᵥ p₂⟫ = 0
rw₅ : ⟪c -ᵥ p₂, p₂ -ᵥ p₁⟫ = 0 ↔ ⟪c -ᵥ p₂, p₁ -ᵥ p₂⟫ = 0
rw₆ : -⟪c -ᵥ p₂, p₂ -ᵥ p₁⟫ = 0 ↔ ⟪c -ᵥ p₂, p₁ -ᵥ p₂⟫ = 0
rw₇ : ⟪c -ᵥ p₂, -(p₂ -ᵥ p₁)⟫ = 0 ↔ ⟪c -ᵥ p₂, p₁ -ᵥ p₂⟫ = 0
⊢ Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ ((Equiv.pointReflection p₂ : (a : P) → P) p₁)) c ↔
    ⟪c -ᵥ p₂, p₁ -ᵥ p₂⟫ = 0
have rw₈ : ⟪c -ᵥ p₂, p₁ -ᵥ p₂⟫ = 0 ↔ ⟪c -ᵥ p₂, p₁ -ᵥ p₂⟫ = 0
Tactic: rw [mem_perpBisector_iff_inner_eq_zero, midpoint_pointReflection_right,
    Equiv.pointReflection_apply, vadd_vsub_assoc, inner_add_right, add_self_eq_zero,
    ← neg_eq_zero, ← inner_neg_right, neg_vsub_eq_vsub_rev]
-- 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
p₁ p₂ : P
⊢ Eq (α := Submodule ℝ V) (direction (perpBisector p₁ p₂)) (ℝ ∙ (p₂ -ᵥ p₁))ᗮ
have rw : Eq (α := Submodule ℝ V)
  (LinearMap.ker (R₂ := ℝ) (M₂ := ℝ) (τ₁₂ := RingHom.id ℝ) ((innerₛₗ ℝ : (a : V) → V →ₗ[ℝ] ℝ) (p₂ -ᵥ p₁)))
  (ℝ ∙ (p₂ -ᵥ p₁))ᗮ
Tactic: rw [perpBisector, direction_mk']
-- 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
p₁ p₂ : P
⊢ Eq (α := Submodule ℝ V)
    (LinearMap.ker (R₂ := ℝ) (M₂ := ℝ) (τ₁₂ := RingHom.id ℝ) ((innerₛₗ ℝ : (a : V) → V →ₗ[ℝ] ℝ) (p₂ -ᵥ p₁)))
    (ℝ ∙ (p₂ -ᵥ p₁))ᗮ
have h : ∀ (x : V),
  Membership.mem (γ := Submodule ℝ V)
      (LinearMap.ker (R₂ := ℝ) (M₂ := ℝ) (τ₁₂ := RingHom.id ℝ) ((innerₛₗ ℝ : (a : V) → V →ₗ[ℝ] ℝ) (p₂ -ᵥ p₁))) x ↔
    Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p₂ -ᵥ p₁))ᗮ x
Tactic: ext x
-- 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 p₁ p₂ : P
⊢ Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = ⟪c -ᵥ p₂, p₁ -ᵥ p₂⟫
have rw : ⟪c -ᵥ p₁ + (c -ᵥ p₂), p₂ -ᵥ p₁⟫ = 0 ↔ 2⁻¹ * ⟪c -ᵥ p₁ + (c -ᵥ p₂), p₂ -ᵥ p₁⟫ = 0
Tactic: rw [Iff.comm, mem_perpBisector_iff_inner_eq_zero, ← add_neg_eq_zero, ← inner_neg_right,
    neg_vsub_eq_vsub_rev, ← inner_add_left, vsub_midpoint, invOf_eq_inv, ← smul_add,
    real_inner_smul_left]
-- 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 p₁ p₂ : P
⊢ Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔
    ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
have rw : ⟪c -ᵥ midpoint ℝ p₁ p₂, p₂ -ᵥ p₁⟫ = 0 ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
Tactic: rw [mem_perpBisector_iff_inner_eq_zero, ← vsub_sub_vsub_cancel_right _ _ p₁, inner_sub_left,
    sub_eq_zero, midpoint_vsub_left, invOf_eq_inv, real_inner_smul_left, real_inner_self_eq_norm_sq,
    dist_eq_norm_vsub' V, div_eq_inv_mul]
-- 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 p₁ p₂ : P
rw : ⟪c -ᵥ midpoint ℝ p₁ p₂, p₂ -ᵥ p₁⟫ = 0 ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
⊢ Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔
    ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
have rw₁ : ⟪c -ᵥ p₁ - (midpoint ℝ p₁ p₂ -ᵥ p₁), p₂ -ᵥ p₁⟫ = 0 ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
Tactic: rw [mem_perpBisector_iff_inner_eq_zero, ← vsub_sub_vsub_cancel_right _ _ p₁, inner_sub_left,
    sub_eq_zero, midpoint_vsub_left, invOf_eq_inv, real_inner_smul_left, real_inner_self_eq_norm_sq,
    dist_eq_norm_vsub' V, div_eq_inv_mul]
-- 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 p₁ p₂ : P
rw : ⟪c -ᵥ midpoint ℝ p₁ p₂, p₂ -ᵥ p₁⟫ = 0 ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
rw₁ : ⟪c -ᵥ p₁ - (midpoint ℝ p₁ p₂ -ᵥ p₁), p₂ -ᵥ p₁⟫ = 0 ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
⊢ Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔
    ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
have rw₂ : ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ - ⟪midpoint ℝ p₁ p₂ -ᵥ p₁, p₂ -ᵥ p₁⟫ = 0 ↔
  ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
Tactic: rw [mem_perpBisector_iff_inner_eq_zero, ← vsub_sub_vsub_cancel_right _ _ p₁, inner_sub_left,
    sub_eq_zero, midpoint_vsub_left, invOf_eq_inv, real_inner_smul_left, real_inner_self_eq_norm_sq,
    dist_eq_norm_vsub' V, div_eq_inv_mul]
-- 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 p₁ p₂ : P
rw : ⟪c -ᵥ midpoint ℝ p₁ p₂, p₂ -ᵥ p₁⟫ = 0 ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
rw₁ : ⟪c -ᵥ p₁ - (midpoint ℝ p₁ p₂ -ᵥ p₁), p₂ -ᵥ p₁⟫ = 0 ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
rw₂ :
  ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ - ⟪midpoint ℝ p₁ p₂ -ᵥ p₁, p₂ -ᵥ p₁⟫ = 0 ↔
    ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
⊢ Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔
    ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
have rw₃ : ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = ⟪midpoint ℝ p₁ p₂ -ᵥ p₁, p₂ -ᵥ p₁⟫ ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
Tactic: rw [mem_perpBisector_iff_inner_eq_zero, ← vsub_sub_vsub_cancel_right _ _ p₁, inner_sub_left,
    sub_eq_zero, midpoint_vsub_left, invOf_eq_inv, real_inner_smul_left, real_inner_self_eq_norm_sq,
    dist_eq_norm_vsub' V, div_eq_inv_mul]
-- 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 p₁ p₂ : P
rw : ⟪c -ᵥ midpoint ℝ p₁ p₂, p₂ -ᵥ p₁⟫ = 0 ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
rw₁ : ⟪c -ᵥ p₁ - (midpoint ℝ p₁ p₂ -ᵥ p₁), p₂ -ᵥ p₁⟫ = 0 ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
rw₂ :
  ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ - ⟪midpoint ℝ p₁ p₂ -ᵥ p₁, p₂ -ᵥ p₁⟫ = 0 ↔
    ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
rw₃ :
  ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = ⟪midpoint ℝ p₁ p₂ -ᵥ p₁, p₂ -ᵥ p₁⟫ ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
⊢ Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔
    ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
have rw₄ : ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ =
    ⟪HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₂ -ᵥ p₁), p₂ -ᵥ p₁⟫ ↔
  ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
Tactic: rw [mem_perpBisector_iff_inner_eq_zero, ← vsub_sub_vsub_cancel_right _ _ p₁, inner_sub_left,
    sub_eq_zero, midpoint_vsub_left, invOf_eq_inv, real_inner_smul_left, real_inner_self_eq_norm_sq,
    dist_eq_norm_vsub' V, div_eq_inv_mul]
-- 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 p₁ p₂ : P
rw : ⟪c -ᵥ midpoint ℝ p₁ p₂, p₂ -ᵥ p₁⟫ = 0 ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
rw₁ : ⟪c -ᵥ p₁ - (midpoint ℝ p₁ p₂ -ᵥ p₁), p₂ -ᵥ p₁⟫ = 0 ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
rw₂ :
  ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ - ⟪midpoint ℝ p₁ p₂ -ᵥ p₁, p₂ -ᵥ p₁⟫ = 0 ↔
    ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
rw₃ :
  ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = ⟪midpoint ℝ p₁ p₂ -ᵥ p₁, p₂ -ᵥ p₁⟫ ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
rw₄ :
  ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ =
      ⟪HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₂ -ᵥ p₁), p₂ -ᵥ p₁⟫ ↔
    ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
⊢ Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔
    ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
have rw₅ : ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = ⟪HSMul.hSMul (α := ℝ) 2⁻¹ (p₂ -ᵥ p₁), p₂ -ᵥ p₁⟫ ↔
  ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
Tactic: rw [mem_perpBisector_iff_inner_eq_zero, ← vsub_sub_vsub_cancel_right _ _ p₁, inner_sub_left,
    sub_eq_zero, midpoint_vsub_left, invOf_eq_inv, real_inner_smul_left, real_inner_self_eq_norm_sq,
    dist_eq_norm_vsub' V, div_eq_inv_mul]
-- 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 p₁ p₂ : P
rw : ⟪c -ᵥ midpoint ℝ p₁ p₂, p₂ -ᵥ p₁⟫ = 0 ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
rw₁ : ⟪c -ᵥ p₁ - (midpoint ℝ p₁ p₂ -ᵥ p₁), p₂ -ᵥ p₁⟫ = 0 ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
rw₂ :
  ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ - ⟪midpoint ℝ p₁ p₂ -ᵥ p₁, p₂ -ᵥ p₁⟫ = 0 ↔
    ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
rw₃ :
  ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = ⟪midpoint ℝ p₁ p₂ -ᵥ p₁, p₂ -ᵥ p₁⟫ ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
rw₄ :
  ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ =
      ⟪HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₂ -ᵥ p₁), p₂ -ᵥ p₁⟫ ↔
    ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
rw₅ :
  ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = ⟪HSMul.hSMul (α := ℝ) 2⁻¹ (p₂ -ᵥ p₁), p₂ -ᵥ p₁⟫ ↔
    ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
⊢ Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔
    ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
have rw₆ : ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = 2⁻¹ * ⟪p₂ -ᵥ p₁, p₂ -ᵥ p₁⟫ ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
Tactic: rw [mem_perpBisector_iff_inner_eq_zero, ← vsub_sub_vsub_cancel_right _ _ p₁, inner_sub_left,
    sub_eq_zero, midpoint_vsub_left, invOf_eq_inv, real_inner_smul_left, real_inner_self_eq_norm_sq,
    dist_eq_norm_vsub' V, div_eq_inv_mul]
-- 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 p₁ p₂ : P
rw : ⟪c -ᵥ midpoint ℝ p₁ p₂, p₂ -ᵥ p₁⟫ = 0 ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
rw₁ : ⟪c -ᵥ p₁ - (midpoint ℝ p₁ p₂ -ᵥ p₁), p₂ -ᵥ p₁⟫ = 0 ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
rw₂ :
  ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ - ⟪midpoint ℝ p₁ p₂ -ᵥ p₁, p₂ -ᵥ p₁⟫ = 0 ↔
    ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
rw₃ :
  ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = ⟪midpoint ℝ p₁ p₂ -ᵥ p₁, p₂ -ᵥ p₁⟫ ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
rw₄ :
  ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ =
      ⟪HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₂ -ᵥ p₁), p₂ -ᵥ p₁⟫ ↔
    ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
rw₅ :
  ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = ⟪HSMul.hSMul (α := ℝ) 2⁻¹ (p₂ -ᵥ p₁), p₂ -ᵥ p₁⟫ ↔
    ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
rw₆ : ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = 2⁻¹ * ⟪p₂ -ᵥ p₁, p₂ -ᵥ p₁⟫ ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
⊢ Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔
    ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
have rw₇ : ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = 2⁻¹ * HPow.hPow (β := ℕ) ‖p₂ -ᵥ p₁‖ 2 ↔
  ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
Tactic: rw [mem_perpBisector_iff_inner_eq_zero, ← vsub_sub_vsub_cancel_right _ _ p₁, inner_sub_left,
    sub_eq_zero, midpoint_vsub_left, invOf_eq_inv, real_inner_smul_left, real_inner_self_eq_norm_sq,
    dist_eq_norm_vsub' V, div_eq_inv_mul]
-- 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 p₁ p₂ : P
rw : ⟪c -ᵥ midpoint ℝ p₁ p₂, p₂ -ᵥ p₁⟫ = 0 ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
rw₁ : ⟪c -ᵥ p₁ - (midpoint ℝ p₁ p₂ -ᵥ p₁), p₂ -ᵥ p₁⟫ = 0 ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
rw₂ :
  ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ - ⟪midpoint ℝ p₁ p₂ -ᵥ p₁, p₂ -ᵥ p₁⟫ = 0 ↔
    ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
rw₃ :
  ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = ⟪midpoint ℝ p₁ p₂ -ᵥ p₁, p₂ -ᵥ p₁⟫ ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
rw₄ :
  ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ =
      ⟪HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₂ -ᵥ p₁), p₂ -ᵥ p₁⟫ ↔
    ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
rw₅ :
  ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = ⟪HSMul.hSMul (α := ℝ) 2⁻¹ (p₂ -ᵥ p₁), p₂ -ᵥ p₁⟫ ↔
    ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
rw₆ : ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = 2⁻¹ * ⟪p₂ -ᵥ p₁, p₂ -ᵥ p₁⟫ ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
rw₇ :
  ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = 2⁻¹ * HPow.hPow (β := ℕ) ‖p₂ -ᵥ p₁‖ 2 ↔
    ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
⊢ Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔
    ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
have rw₈ : ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = 2⁻¹ * HPow.hPow (β := ℕ) ‖p₂ -ᵥ p₁‖ 2 ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) ‖p₂ -ᵥ p₁‖ 2 / 2
Tactic: rw [mem_perpBisector_iff_inner_eq_zero, ← vsub_sub_vsub_cancel_right _ _ p₁, inner_sub_left,
    sub_eq_zero, midpoint_vsub_left, invOf_eq_inv, real_inner_smul_left, real_inner_self_eq_norm_sq,
    dist_eq_norm_vsub' V, div_eq_inv_mul]
-- 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 p₁ p₂ : P
rw : ⟪c -ᵥ midpoint ℝ p₁ p₂, p₂ -ᵥ p₁⟫ = 0 ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
rw₁ : ⟪c -ᵥ p₁ - (midpoint ℝ p₁ p₂ -ᵥ p₁), p₂ -ᵥ p₁⟫ = 0 ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
rw₂ :
  ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ - ⟪midpoint ℝ p₁ p₂ -ᵥ p₁, p₂ -ᵥ p₁⟫ = 0 ↔
    ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
rw₃ :
  ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = ⟪midpoint ℝ p₁ p₂ -ᵥ p₁, p₂ -ᵥ p₁⟫ ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
rw₄ :
  ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ =
      ⟪HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₂ -ᵥ p₁), p₂ -ᵥ p₁⟫ ↔
    ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
rw₅ :
  ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = ⟪HSMul.hSMul (α := ℝ) 2⁻¹ (p₂ -ᵥ p₁), p₂ -ᵥ p₁⟫ ↔
    ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
rw₆ : ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = 2⁻¹ * ⟪p₂ -ᵥ p₁, p₂ -ᵥ p₁⟫ ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
rw₇ :
  ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = 2⁻¹ * HPow.hPow (β := ℕ) ‖p₂ -ᵥ p₁‖ 2 ↔
    ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
rw₈ :
  ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = 2⁻¹ * HPow.hPow (β := ℕ) ‖p₂ -ᵥ p₁‖ 2 ↔
    ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) ‖p₂ -ᵥ p₁‖ 2 / 2
⊢ Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔
    ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = HPow.hPow (β := ℕ) (dist p₁ p₂) 2 / 2
have rw₉ : ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = 2⁻¹ * HPow.hPow (β := ℕ) ‖p₂ -ᵥ p₁‖ 2 ↔
  ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = 2⁻¹ * HPow.hPow (β := ℕ) ‖p₂ -ᵥ p₁‖ 2
Tactic: rw [mem_perpBisector_iff_inner_eq_zero, ← vsub_sub_vsub_cancel_right _ _ p₁, inner_sub_left,
    sub_eq_zero, midpoint_vsub_left, invOf_eq_inv, real_inner_smul_left, real_inner_self_eq_norm_sq,
    dist_eq_norm_vsub' V, div_eq_inv_mul]
-- 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 p₁ p₂ : P
⊢ Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ dist c p₁ = dist c p₂
have rw : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ ‖c -ᵥ p₁‖ = dist c p₂
Tactic: rw [dist_eq_norm_vsub V, dist_eq_norm_vsub V, ← real_inner_add_sub_eq_zero_iff,
    vsub_sub_vsub_cancel_left, inner_add_left, add_eq_zero_iff_eq_neg, ← inner_neg_right,
    neg_vsub_eq_vsub_rev, mem_perpBisector_iff_inner_eq_inner]
-- 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 p₁ p₂ : P
rw : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ ‖c -ᵥ p₁‖ = dist c p₂
⊢ Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ dist c p₁ = dist c p₂
have rw₁ : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ ‖c -ᵥ p₁‖ = ‖c -ᵥ p₂‖
Tactic: rw [dist_eq_norm_vsub V, dist_eq_norm_vsub V, ← real_inner_add_sub_eq_zero_iff,
    vsub_sub_vsub_cancel_left, inner_add_left, add_eq_zero_iff_eq_neg, ← inner_neg_right,
    neg_vsub_eq_vsub_rev, mem_perpBisector_iff_inner_eq_inner]
-- 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 p₁ p₂ : P
rw : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ ‖c -ᵥ p₁‖ = dist c p₂
rw₁ : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ ‖c -ᵥ p₁‖ = ‖c -ᵥ p₂‖
⊢ Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ dist c p₁ = dist c p₂
have rw₂ : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ ⟪c -ᵥ p₁ + (c -ᵥ p₂), c -ᵥ p₁ - (c -ᵥ p₂)⟫ = 0
Tactic: rw [dist_eq_norm_vsub V, dist_eq_norm_vsub V, ← real_inner_add_sub_eq_zero_iff,
    vsub_sub_vsub_cancel_left, inner_add_left, add_eq_zero_iff_eq_neg, ← inner_neg_right,
    neg_vsub_eq_vsub_rev, mem_perpBisector_iff_inner_eq_inner]
-- 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 p₁ p₂ : P
rw : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ ‖c -ᵥ p₁‖ = dist c p₂
rw₁ : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ ‖c -ᵥ p₁‖ = ‖c -ᵥ p₂‖
rw₂ : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ ⟪c -ᵥ p₁ + (c -ᵥ p₂), c -ᵥ p₁ - (c -ᵥ p₂)⟫ = 0
⊢ Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ dist c p₁ = dist c p₂
have rw₃ : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ ⟪c -ᵥ p₁ + (c -ᵥ p₂), p₂ -ᵥ p₁⟫ = 0
Tactic: rw [dist_eq_norm_vsub V, dist_eq_norm_vsub V, ← real_inner_add_sub_eq_zero_iff,
    vsub_sub_vsub_cancel_left, inner_add_left, add_eq_zero_iff_eq_neg, ← inner_neg_right,
    neg_vsub_eq_vsub_rev, mem_perpBisector_iff_inner_eq_inner]
-- 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 p₁ p₂ : P
rw : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ ‖c -ᵥ p₁‖ = dist c p₂
rw₁ : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ ‖c -ᵥ p₁‖ = ‖c -ᵥ p₂‖
rw₂ : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ ⟪c -ᵥ p₁ + (c -ᵥ p₂), c -ᵥ p₁ - (c -ᵥ p₂)⟫ = 0
rw₃ : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ ⟪c -ᵥ p₁ + (c -ᵥ p₂), p₂ -ᵥ p₁⟫ = 0
⊢ Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ dist c p₁ = dist c p₂
have rw₄ : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ + ⟪c -ᵥ p₂, p₂ -ᵥ p₁⟫ = 0
Tactic: rw [dist_eq_norm_vsub V, dist_eq_norm_vsub V, ← real_inner_add_sub_eq_zero_iff,
    vsub_sub_vsub_cancel_left, inner_add_left, add_eq_zero_iff_eq_neg, ← inner_neg_right,
    neg_vsub_eq_vsub_rev, mem_perpBisector_iff_inner_eq_inner]
-- 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 p₁ p₂ : P
rw : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ ‖c -ᵥ p₁‖ = dist c p₂
rw₁ : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ ‖c -ᵥ p₁‖ = ‖c -ᵥ p₂‖
rw₂ : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ ⟪c -ᵥ p₁ + (c -ᵥ p₂), c -ᵥ p₁ - (c -ᵥ p₂)⟫ = 0
rw₃ : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ ⟪c -ᵥ p₁ + (c -ᵥ p₂), p₂ -ᵥ p₁⟫ = 0
rw₄ : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ + ⟪c -ᵥ p₂, p₂ -ᵥ p₁⟫ = 0
⊢ Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ dist c p₁ = dist c p₂
have rw₅ : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = -⟪c -ᵥ p₂, p₂ -ᵥ p₁⟫
Tactic: rw [dist_eq_norm_vsub V, dist_eq_norm_vsub V, ← real_inner_add_sub_eq_zero_iff,
    vsub_sub_vsub_cancel_left, inner_add_left, add_eq_zero_iff_eq_neg, ← inner_neg_right,
    neg_vsub_eq_vsub_rev, mem_perpBisector_iff_inner_eq_inner]
-- 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 p₁ p₂ : P
rw : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ ‖c -ᵥ p₁‖ = dist c p₂
rw₁ : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ ‖c -ᵥ p₁‖ = ‖c -ᵥ p₂‖
rw₂ : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ ⟪c -ᵥ p₁ + (c -ᵥ p₂), c -ᵥ p₁ - (c -ᵥ p₂)⟫ = 0
rw₃ : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ ⟪c -ᵥ p₁ + (c -ᵥ p₂), p₂ -ᵥ p₁⟫ = 0
rw₄ : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ + ⟪c -ᵥ p₂, p₂ -ᵥ p₁⟫ = 0
rw₅ : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = -⟪c -ᵥ p₂, p₂ -ᵥ p₁⟫
⊢ Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ dist c p₁ = dist c p₂
have rw₆ : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = ⟪c -ᵥ p₂, -(p₂ -ᵥ p₁)⟫
Tactic: rw [dist_eq_norm_vsub V, dist_eq_norm_vsub V, ← real_inner_add_sub_eq_zero_iff,
    vsub_sub_vsub_cancel_left, inner_add_left, add_eq_zero_iff_eq_neg, ← inner_neg_right,
    neg_vsub_eq_vsub_rev, mem_perpBisector_iff_inner_eq_inner]