awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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.faceOpposite s i).orthogonalProjectionSpan :
            (a : P) → ↥(affineSpan ℝ (Set.range (Simplex.faceOpposite s i).points)))
          (Simplex.eulerPoint s i)) :
      P) ∈
    Simplex.ninePointCircle s

Tactic:
s.orthogonalProjectionSpan_eulerPoint_mem_ninePointCircle i

Premises used: Affine.Simplex.orthogonalProjectionSpan_eulerPoint_mem_ninePointCircle
-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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
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)
⊢ Simplex.altitudeFoot s i ∈ Simplex.ninePointCircle s

Tactic:
convert! s.orthogonalProjectionSpan_eulerPoint_mem_ninePointCircle i

Premises used: Affine.Simplex.orthogonalProjectionSpan_eulerPoint_mem_ninePointCircle
-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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
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)
⊢ 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)

Tactic:
unfold Simplex.orthogonalProjectionSpan

Premises used: Affine.Simplex.orthogonalProjectionSpan
-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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
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)))
⊢ 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:
congr 1
-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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
⊢ HSub.hSub (α := ℝ) (↑2 : ℝ) 1 / (↑2 : ℝ) ≠ 0

Tactic:
norm_num
-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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
h : Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ (s.points i -ᵥ s.orthocenter)
⊢ 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:
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]

Premises used: direction_affineSpan, EuclideanGeometry.orthogonalProjection_eq_orthogonalProjection_iff_vsub_mem, Submodule.smul_mem_iff, Affine.Triangle.orthocenter_eq_mongePoint, Affine.Simplex.range_faceOpposite_points, Affine.Simplex.points_vsub_eulerPoint
-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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)

Tactic:
Set.mem_of_mem_of_subset ?_ (s.vectorSpan_isOrtho_altitude_direction i).ge

Premises used: Affine.Simplex.vectorSpan_isOrtho_altitude_direction, Set.mem_of_mem_of_subset, Submodule.IsOrtho.ge
-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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
h : s.points i -ᵥ s.orthocenter ∈ (↑(Simplex.altitude s i).direction : Set V)
⊢ Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ (s.points i -ᵥ s.orthocenter)

Tactic:
refine Set.mem_of_mem_of_subset ?_ (s.vectorSpan_isOrtho_altitude_direction i).ge

Premises used: Affine.Simplex.vectorSpan_isOrtho_altitude_direction, Set.mem_of_mem_of_subset, Submodule.IsOrtho.ge
-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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 -ᵥ s.orthocenter ∈ (↑(Simplex.altitude s i).direction : Set V)

Tactic:
vsub_mem_direction (s.mem_altitude i) (s.orthocenter_mem_altitude)

Premises used: Set.Mem, AffineSubspace.vsub_mem_direction, Affine.Triangle.orthocenter_mem_altitude, Affine.Simplex.mem_altitude
-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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 -ᵥ s.orthocenter ∈ (↑(Simplex.altitude s i).direction : Set V)

Tactic:
exact vsub_mem_direction (s.mem_altitude i) (s.orthocenter_mem_altitude)

Premises used: AffineSubspace.vsub_mem_direction, Affine.Triangle.orthocenter_mem_altitude, Affine.Simplex.mem_altitude
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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 ↔ ⟪p₂ -ᵥ p₁, c -ᵥ midpoint ℝ p₁ p₂⟫ = 0

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage, Set.singleton
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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 -ᵥ midpoint ℝ p₁ p₂, p₂ -ᵥ p₁⟫ = 0

Tactic:
inner_eq_zero_symm

Premises used: Set.Mem, setOf, Set.preimage, Set.singleton, inner_eq_zero_symm
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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 : 2⁻¹ * ⟪c -ᵥ p₁ + (c -ᵥ p₂), p₂ -ᵥ p₁⟫ = 0 ↔ ⟪c -ᵥ p₁ + (c -ᵥ p₂), p₂ -ᵥ p₁⟫ = 0
⊢ Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔
    ⟪(Equiv.pointReflection c : (a : P) → P) p₁ -ᵥ 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]

Premises used: vsub_midpoint, vadd_vsub_assoc, AffineSubspace.mem_perpBisector_iff_inner_eq_zero, invOf_eq_inv, real_inner_smul_left, smul_add, Equiv.pointReflection_apply
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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
⊢ 2⁻¹ * ⟪c -ᵥ p₁ + (c -ᵥ p₂), p₂ -ᵥ p₁⟫ = 0 ↔ ⟪c -ᵥ p₁ + (c -ᵥ p₂), p₂ -ᵥ p₁⟫ = 0

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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
rw₈ 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

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]

Premises used: vadd_vsub_assoc, AffineSubspace.mem_perpBisector_iff_inner_eq_zero, midpoint_pointReflection_right, add_self_eq_zero, inner_neg_right, neg_eq_zero, inner_add_right, neg_vsub_eq_vsub_rev, Equiv.pointReflection_apply
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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
⊢ Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) (midpoint ℝ p₁ p₂)

Tactic:
simp [mem_perpBisector_iff_inner_eq_zero]

Premises used: AffineSubspace.mem_perpBisector_iff_inner_eq_zero
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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
⊢ (↑(perpBisector p₁ p₂) : Set P).Nonempty

Tactic:
⟨_, midpoint_mem_perpBisector _ _⟩

Premises used: Set.Nonempty, AffineSubspace.midpoint_mem_perpBisector, Exists.intro
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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
rw :
  Eq (α := Submodule ℝ V)
    (LinearMap.ker (R₂ := ℝ) (M₂ := ℝ) (τ₁₂ := RingHom.id ℝ) ((innerₛₗ ℝ : (a : V) → V →ₗ[ℝ] ℝ) (p₂ -ᵥ p₁)))
    (ℝ ∙ (p₂ -ᵥ p₁))ᗮ
⊢ Eq (α := Submodule ℝ V) (direction (perpBisector p₁ p₂)) (ℝ ∙ (p₂ -ᵥ p₁))ᗮ

Tactic:
rw [perpBisector, direction_mk']

Premises used: AffineSubspace.perpBisector, AffineSubspace.direction_mk'
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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
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
⊢ Eq (α := Submodule ℝ V)
    (LinearMap.ker (R₂ := ℝ) (M₂ := ℝ) (τ₁₂ := RingHom.id ℝ) ((innerₛₗ ℝ : (a : V) → V →ₗ[ℝ] ℝ) (p₂ -ᵥ p₁)))
    (ℝ ∙ (p₂ -ᵥ p₁))ᗮ

Tactic:
ext x
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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
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:
Submodule.mem_orthogonal_singleton_iff_inner_right.symm

Premises used: Submodule.mem_orthogonal_singleton_iff_inner_right, Set.Mem, setOf, Set.preimage, Set.singleton, Iff.symm
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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
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:
exact Submodule.mem_orthogonal_singleton_iff_inner_right.symm

Premises used: Submodule.mem_orthogonal_singleton_iff_inner_right, Iff.symm
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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 -ᵥ p₁ + (c -ᵥ p₂), p₂ -ᵥ p₁⟫ = 0 ↔ 2⁻¹ * ⟪c -ᵥ p₁ + (c -ᵥ p₂), p₂ -ᵥ p₁⟫ = 0
⊢ Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = ⟪c -ᵥ p₂, p₁ -ᵥ p₂⟫

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]

Premises used: vsub_midpoint, add_neg_eq_zero, AffineSubspace.mem_perpBisector_iff_inner_eq_zero, inner_neg_right, inner_add_left, neg_vsub_eq_vsub_rev, Iff.comm, invOf_eq_inv, real_inner_smul_left, smul_add
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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
⊢ ⟪c -ᵥ p₁ + (c -ᵥ p₂), p₂ -ᵥ p₁⟫ = 0 ↔ 2⁻¹ * ⟪c -ᵥ p₁ + (c -ᵥ p₂), p₂ -ᵥ p₁⟫ = 0

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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
rw₉ rw₁₀ :
  ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = 2⁻¹ * HPow.hPow (β := ℕ) ‖p₂ -ᵥ p₁‖ 2 ↔
    ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = 2⁻¹ * HPow.hPow (β := ℕ) ‖p₂ -ᵥ p₁‖ 2
⊢ Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔
    ⟪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]

Premises used: sub_eq_zero, AffineSubspace.mem_perpBisector_iff_inner_eq_zero, dist_eq_norm_vsub', midpoint_vsub_left, real_inner_self_eq_norm_sq, inner_sub_left, vsub_sub_vsub_cancel_right, invOf_eq_inv, real_inner_smul_left, div_eq_inv_mul
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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₁⟫
rw₆ : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = ⟪c -ᵥ p₂, -(p₂ -ᵥ p₁)⟫
rw₇ : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = ⟪c -ᵥ p₂, p₁ -ᵥ p₂⟫
rw₈ rw₉ : ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = ⟪c -ᵥ p₂, p₁ -ᵥ p₂⟫ ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = ⟪c -ᵥ p₂, p₁ -ᵥ p₂⟫
⊢ Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ dist 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]

Premises used: inner_neg_right, add_eq_zero_iff_eq_neg, inner_add_left, real_inner_add_sub_eq_zero_iff, AffineSubspace.mem_perpBisector_iff_inner_eq_inner, vsub_sub_vsub_cancel_left, neg_vsub_eq_vsub_rev, dist_eq_norm_vsub
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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 p₁ c = dist p₂ c

Tactic:
simp only [mem_perpBisector_iff_dist_eq, dist_comm]

Premises used: dist_comm, AffineSubspace.mem_perpBisector_iff_dist_eq
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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
h :
  ∀ (c : P),
    Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔
      Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₂ p₁) c
⊢ Eq (α := AffineSubspace ℝ P) (perpBisector p₁ p₂) (perpBisector p₂ p₁)

Tactic:
ext c
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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₂ c : P
⊢ Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔
    Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₂ p₁) c

Tactic:
simp only [mem_perpBisector_iff_dist_eq, eq_comm]

Premises used: eq_comm, AffineSubspace.mem_perpBisector_iff_dist_eq
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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
⊢ Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) p₂ ↔ p₁ = p₂

Tactic:
simpa [mem_perpBisector_iff_inner_eq_inner] using eq_comm

Premises used: eq_comm, AffineSubspace.mem_perpBisector_iff_inner_eq_inner
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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
rw : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₂ p₁) p₁ ↔ p₁ = p₂
rw₁ : p₂ = p₁ ↔ p₁ = p₂
rw₂ rw₃ : p₁ = p₂ ↔ p₁ = p₂
⊢ Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) p₁ ↔ p₁ = p₂

Tactic:
rw [perpBisector_comm, right_mem_perpBisector, eq_comm]

Premises used: eq_comm, AffineSubspace.perpBisector_comm, AffineSubspace.right_mem_perpBisector
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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 x : P
⊢ Membership.mem (γ := AffineSubspace ℝ P) ⊤ x → Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p p) x

Tactic:
simp [mem_perpBisector_iff_inner_eq_inner]

Premises used: AffineSubspace.mem_perpBisector_iff_inner_eq_inner
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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 (α := AffineSubspace ℝ P) (perpBisector p₁ p₂) ⊤ ↔ p₁ = p₂

Tactic:
⟨fun h ↦ ?_, fun h ↦ h ▸ perpBisector_self _⟩

Premises used: Eq.rec, AffineSubspace.perpBisector_self, Iff.intro
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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
refine : ∀ (h : Eq (α := AffineSubspace ℝ P) (perpBisector p₁ p₂) ⊤), p₁ = p₂
⊢ Eq (α := AffineSubspace ℝ P) (perpBisector p₁ p₂) ⊤ ↔ p₁ = p₂

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h ▸ perpBisector_self _⟩
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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
h : Eq (α := AffineSubspace ℝ P) (perpBisector p₁ p₂) ⊤
rw : Membership.mem (γ := AffineSubspace ℝ P) ⊤ p₁
⊢ p₁ = p₂

Tactic:
rw [← left_mem_perpBisector, h]

Premises used: AffineSubspace.left_mem_perpBisector
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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
h : Eq (α := AffineSubspace ℝ P) (perpBisector p₁ p₂) ⊤
⊢ Membership.mem (γ := AffineSubspace ℝ P) ⊤ p₁

Tactic:
trivial
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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
rw : (↑(perpBisector p₁ p₂) : Set P).Nonempty
⊢ Ne (α := AffineSubspace ℝ P) (perpBisector p₁ p₂) ⊥

Tactic:
rw [← nonempty_iff_ne_bot]

Premises used: AffineSubspace.nonempty_iff_ne_bot
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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
⊢ (↑(perpBisector p₁ p₂) : Set P).Nonempty

Tactic:
perpBisector_nonempty

Premises used: AffineSubspace.perpBisector_nonempty