awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.NinePointCircle (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
n : ℕ
hn : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
hn1 : ¬n = 1
hltn : 1 < n
hnsub1 : (↑(n - 1) : ℝ) = HSub.hSub (α := ℝ) (↑n : ℝ) 1
rw :
  HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) =
    (HAdd.hAdd (α := ℝ) 1 (↑n : ℝ) / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)
rw₁ :
  HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) =
    (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) + HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)
⊢ HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) =
    (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)
have rw₂ : HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) =
  (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) + 1) • (s.centroid -ᵥ s.circumcenter)
Tactic: rw [add_comm (n : ℝ) 1, add_div, div_self (by simpa using hn.out), add_smul, one_smul, one_div]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.NinePointCircle (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
n : ℕ
hn : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
hn1 : ¬n = 1
hltn : 1 < n
hnsub1 : (↑(n - 1) : ℝ) = HSub.hSub (α := ℝ) (↑n : ℝ) 1
rw :
  HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) =
    (HAdd.hAdd (α := ℝ) 1 (↑n : ℝ) / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)
rw₁ :
  HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) =
    (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) + HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)
rw₂ :
  HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) =
    (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) + 1) • (s.centroid -ᵥ s.circumcenter)
⊢ HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) =
    (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)
have rw₃ : HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) =
  HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) • (s.centroid -ᵥ s.circumcenter) + HSMul.hSMul (α := ℝ) 1 (s.centroid -ᵥ s.circumcenter)
Tactic: rw [add_comm (n : ℝ) 1, add_div, div_self (by simpa using hn.out), add_smul, one_smul, one_div]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.NinePointCircle (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
n : ℕ
hn : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
hn1 : ¬n = 1
hltn : 1 < n
hnsub1 : (↑(n - 1) : ℝ) = HSub.hSub (α := ℝ) (↑n : ℝ) 1
rw :
  HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) =
    (HAdd.hAdd (α := ℝ) 1 (↑n : ℝ) / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)
rw₁ :
  HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) =
    (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) + HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)
rw₂ :
  HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) =
    (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) + 1) • (s.centroid -ᵥ s.circumcenter)
rw₃ :
  HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) =
    HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) • (s.centroid -ᵥ s.circumcenter) +
      HSMul.hSMul (α := ℝ) 1 (s.centroid -ᵥ s.circumcenter)
⊢ HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) =
    (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)
have rw₄ : HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) =
  HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) • (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter)
Tactic: rw [add_comm (n : ℝ) 1, add_div, div_self (by simpa using hn.out), add_smul, one_smul, one_div]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.NinePointCircle (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
n : ℕ
hn : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
hn1 : ¬n = 1
hltn : 1 < n
hnsub1 : (↑(n - 1) : ℝ) = HSub.hSub (α := ℝ) (↑n : ℝ) 1
rw :
  HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) =
    (HAdd.hAdd (α := ℝ) 1 (↑n : ℝ) / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)
rw₁ :
  HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) =
    (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) + HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)
rw₂ :
  HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) =
    (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) + 1) • (s.centroid -ᵥ s.circumcenter)
rw₃ :
  HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) =
    HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) • (s.centroid -ᵥ s.circumcenter) +
      HSMul.hSMul (α := ℝ) 1 (s.centroid -ᵥ s.circumcenter)
rw₄ :
  HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) =
    HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) • (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter)
⊢ HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) =
    (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)
have rw₅ : HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) =
  HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter)
Tactic: rw [add_comm (n : ℝ) 1, add_div, div_self (by simpa using hn.out), add_smul, one_smul, one_div]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.NinePointCircle (hypothesis)
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
n : ℕ
hn : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
hn1 : ¬n = 1
hltn : 1 < n
hnsub1 : (↑(n - 1) : ℝ) = HSub.hSub (α := ℝ) (↑n : ℝ) 1
⊢ HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) +
        (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)) =
    (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)
have this : HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) =
  (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)
Tactic: have : (n : ℝ)⁻¹ • (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) =
      (((n + 1) / n : ℝ)) • (s.centroid -ᵥ s.circumcenter) := by
    rw [add_comm (n : ℝ) 1, add_div, div_self (by simpa using hn.out), add_smul, one_smul, one_div]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.NinePointCircle (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
n : ℕ
hn : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
hn1 : ¬n = 1
hltn : 1 < n
hnsub1 : (↑(n - 1) : ℝ) = HSub.hSub (α := ℝ) (↑n : ℝ) 1
this :
  HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) =
    (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)
⊢ HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) +
        (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)) =
    (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)
have neg : HMul.hMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) 2 •
    (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter) =
  (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)
Tactic: rw [this, ← two_smul ℝ, smul_smul]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.NinePointCircle (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
s : Triangle ℝ P
i : Fin 3
⊢ Simplex.eulerPoint s i = midpoint ℝ s.orthocenter (s.points i)
have apply : s.points i -ᵥ Simplex.eulerPoint s i = s.points i -ᵥ midpoint ℝ s.orthocenter (s.points i)
Tactic: apply vsub_right_cancel (p := s.points i)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.NinePointCircle (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
s : Triangle ℝ P
i : Fin 3
⊢ s.points i -ᵥ Simplex.eulerPoint s i = s.points i -ᵥ midpoint ℝ s.orthocenter (s.points i)
have rw : (HSub.hSub (α := ℝ) (↑2 : ℝ) 1 / (↑2 : ℝ)) • (s.points i -ᵥ Simplex.mongePoint s) =
  HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (s.points i -ᵥ Simplex.mongePoint s) +
    HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (s.points i -ᵥ s.points i)
Tactic: rw [orthocenter_eq_mongePoint, Simplex.points_vsub_eulerPoint, vsub_midpoint]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.NinePointCircle (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
s : Triangle ℝ P
i : Fin 3
⊢ Simplex.altitudeFoot s i ∈ Simplex.ninePointCircle s
have h : Simplex.altitudeFoot s i =
  (↑(((Simplex.faceOpposite s i).orthogonalProjectionSpan :
          (a : P) → ↥(affineSpan ℝ (Set.range (Simplex.faceOpposite s i).points)))
        (Simplex.eulerPoint s i)) :
    P)
Tactic: convert! s.orthogonalProjectionSpan_eulerPoint_mem_ninePointCircle i
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.NinePointCircle (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
s : Triangle ℝ P
i : Fin 3
⊢ Eq.{u_2 + 1} (α := P)
    (↑(((Simplex.faceOpposite s i).orthogonalProjectionSpan :
            (a : P) → ↥(affineSpan ℝ (Set.range (Simplex.faceOpposite s i).points)))
          (s.points i)) :
      P)
    (↑(((Simplex.faceOpposite s i).orthogonalProjectionSpan :
            (a : P) → ↥(affineSpan ℝ (Set.range (Simplex.faceOpposite s i).points)))
          (Simplex.eulerPoint s i)) :
      P)
have h : Eq.{u_2 + 1} (α := P)
  (↑((orthogonalProjection (affineSpan ℝ (Set.range (Simplex.faceOpposite s i).points)) :
          (a : P) → ↥(affineSpan ℝ (Set.range (Simplex.faceOpposite s i).points)))
        (s.points i)) :
    P)
  (↑((orthogonalProjection (affineSpan ℝ (Set.range (Simplex.faceOpposite s i).points)) :
          (a : P) → ↥(affineSpan ℝ (Set.range (Simplex.faceOpposite s i).points)))
        (Simplex.eulerPoint s i)) :
    P)
Tactic: unfold Simplex.orthogonalProjectionSpan
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.NinePointCircle (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
s : Triangle ℝ P
i : Fin 3
⊢ Eq.{u_2 + 1} (α := P)
    (↑((orthogonalProjection (affineSpan ℝ (Set.range (Simplex.faceOpposite s i).points)) :
            (a : P) → ↥(affineSpan ℝ (Set.range (Simplex.faceOpposite s i).points)))
          (s.points i)) :
      P)
    (↑((orthogonalProjection (affineSpan ℝ (Set.range (Simplex.faceOpposite s i).points)) :
            (a : P) → ↥(affineSpan ℝ (Set.range (Simplex.faceOpposite s i).points)))
          (Simplex.eulerPoint s i)) :
      P)
have h : Eq (α := ↥(affineSpan ℝ (Set.range (Simplex.faceOpposite s i).points)))
  ((orthogonalProjection (affineSpan ℝ (Set.range (Simplex.faceOpposite s i).points)) :
        (a : P) → ↥(affineSpan ℝ (Set.range (Simplex.faceOpposite s i).points)))
      (s.points i) :
    ↥(affineSpan ℝ (Set.range (Simplex.faceOpposite s i).points)))
  ((orthogonalProjection (affineSpan ℝ (Set.range (Simplex.faceOpposite s i).points)) :
        (a : P) → ↥(affineSpan ℝ (Set.range (Simplex.faceOpposite s i).points)))
      (Simplex.eulerPoint s i) :
    ↥(affineSpan ℝ (Set.range (Simplex.faceOpposite s i).points)))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.NinePointCircle (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
s : Triangle ℝ P
i : Fin 3
⊢ Eq (α := ↥(affineSpan ℝ (Set.range (Simplex.faceOpposite s i).points)))
    ((orthogonalProjection (affineSpan ℝ (Set.range (Simplex.faceOpposite s i).points)) :
          (a : P) → ↥(affineSpan ℝ (Set.range (Simplex.faceOpposite s i).points)))
        (s.points i) :
      ↥(affineSpan ℝ (Set.range (Simplex.faceOpposite s i).points)))
    ((orthogonalProjection (affineSpan ℝ (Set.range (Simplex.faceOpposite s i).points)) :
          (a : P) → ↥(affineSpan ℝ (Set.range (Simplex.faceOpposite s i).points)))
        (Simplex.eulerPoint s i) :
      ↥(affineSpan ℝ (Set.range (Simplex.faceOpposite s i).points)))
have h : Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ (s.points i -ᵥ s.orthocenter)
Tactic: rw [orthogonalProjection_eq_orthogonalProjection_iff_vsub_mem,
    Simplex.points_vsub_eulerPoint, Submodule.smul_mem_iff _ (by norm_num),
    ← orthocenter_eq_mongePoint, direction_affineSpan, Simplex.range_faceOpposite_points]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.NinePointCircle (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
s : Triangle ℝ P
i : Fin 3
⊢ Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ (s.points i -ᵥ s.orthocenter)
have h : s.points i -ᵥ s.orthocenter ∈ (↑(Simplex.altitude s i).direction : Set V)
Tactic: refine Set.mem_of_mem_of_subset ?_ (s.vectorSpan_isOrtho_altitude_direction i).ge
-- 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 ↔
    ⟪(Equiv.pointReflection c : (a : P) → P) p₁ -ᵥ p₂, p₂ -ᵥ p₁⟫ = 0
have rw : 2⁻¹ * ⟪c -ᵥ p₁ + (c -ᵥ p₂), p₂ -ᵥ p₁⟫ = 0 ↔ ⟪c -ᵥ p₁ + (c -ᵥ p₂), p₂ -ᵥ p₁⟫ = 0
Tactic: rw [mem_perpBisector_iff_inner_eq_zero, Equiv.pointReflection_apply,
    vsub_midpoint, invOf_eq_inv, ← smul_add, real_inner_smul_left, vadd_vsub_assoc]
-- 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₁ ((Equiv.pointReflection p₂ : (a : P) → P) p₁)) c ↔
    ⟪c -ᵥ p₂, p₁ -ᵥ p₂⟫ = 0
have 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
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
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
⊢ Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ ((Equiv.pointReflection p₂ : (a : P) → P) p₁)) c ↔
    ⟪c -ᵥ p₂, p₁ -ᵥ p₂⟫ = 0
have rw₁ : ⟪c -ᵥ p₂, (Equiv.pointReflection p₂ : (a : P) → 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
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
⊢ 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₁) +ᵥ 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
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
⊢ 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₁ + (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
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
⊢ 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₁⟫ + ⟪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
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
⊢ 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
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
⊢ 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
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
⊢ 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]