awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
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 : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : dist p₂ s.center < s.radius
h : ¬p₁ = p₂
⊢ 0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫

Tactic:
exact (inner_pos_or_eq_of_dist_le_radius hp₁ hp₂.le).resolve_right h

Premises used: EuclideanGeometry.inner_pos_or_eq_of_dist_le_radius, LT.lt.le, Or.resolve_right
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
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
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₁p₂ : p₁ ≠ p₂
rw : dist s.center p₁ = s.radius
⊢ ‖p₁ -ᵥ s.center‖ = s.radius

Tactic:
rw [← dist_eq_norm_vsub']

Premises used: dist_eq_norm_vsub'
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
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
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₁p₂ : p₁ ≠ p₂
⊢ dist s.center p₁ = s.radius

Tactic:
mem_sphere'.mp hp₁

Premises used: EuclideanGeometry.mem_sphere', Iff.mp
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
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
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₁p₂ : p₁ ≠ p₂
⊢ dist s.center p₁ = s.radius

Tactic:
exact mem_sphere'.mp hp₁

Premises used: EuclideanGeometry.mem_sphere', Iff.mp
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
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
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₁p₂ : p₁ ≠ p₂
⊢ ‖p₁ -ᵥ s.center‖ = s.radius

Tactic:
have hp₁' : ‖p₁ -ᵥ s.center‖ = s.radius := by rw [← dist_eq_norm_vsub']; exact mem_sphere'.mp hp₁
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
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
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₁p₂ : p₁ ≠ p₂
hp₁' : ‖p₁ -ᵥ s.center‖ = s.radius
rw : dist s.center p₂ = s.radius
⊢ ‖p₂ -ᵥ s.center‖ = s.radius

Tactic:
rw [← dist_eq_norm_vsub']

Premises used: dist_eq_norm_vsub'
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
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
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₁p₂ : p₁ ≠ p₂
hp₁' : ‖p₁ -ᵥ s.center‖ = s.radius
⊢ dist s.center p₂ = s.radius

Tactic:
mem_sphere'.mp hp₂

Premises used: EuclideanGeometry.mem_sphere', Iff.mp
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
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
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₁p₂ : p₁ ≠ p₂
hp₁' : ‖p₁ -ᵥ s.center‖ = s.radius
⊢ dist s.center p₂ = s.radius

Tactic:
exact mem_sphere'.mp hp₂

Premises used: EuclideanGeometry.mem_sphere', Iff.mp
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
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
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₁p₂ : p₁ ≠ p₂
hp₁' : ‖p₁ -ᵥ s.center‖ = s.radius
⊢ ‖p₂ -ᵥ s.center‖ = s.radius

Tactic:
have hp₂' : ‖p₂ -ᵥ s.center‖ = s.radius := by rw [← dist_eq_norm_vsub']; exact mem_sphere'.mp hp₂
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
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
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₁p₂ : p₁ ≠ p₂
hp₁' : ‖p₁ -ᵥ s.center‖ = s.radius
hp₂' : ‖p₂ -ᵥ s.center‖ = s.radius
rw :
  HPow.hPow (β := ℕ) ‖p₂ -ᵥ p₁ + (p₁ -ᵥ s.center)‖ 2 =
    HPow.hPow (β := ℕ) ‖p₂ -ᵥ p₁‖ 2 + 2 * ⟪p₂ -ᵥ p₁, p₁ -ᵥ s.center⟫ + HPow.hPow (β := ℕ) ‖p₁ -ᵥ s.center‖ 2
rw₁ rw₂ :
  HPow.hPow (β := ℕ) ‖p₂ -ᵥ p₁‖ 2 + 2 * ⟪p₂ -ᵥ p₁, p₁ -ᵥ s.center⟫ + HPow.hPow (β := ℕ) ‖p₁ -ᵥ s.center‖ 2 =
    HPow.hPow (β := ℕ) ‖p₂ -ᵥ p₁‖ 2 + 2 * ⟪p₂ -ᵥ p₁, p₁ -ᵥ s.center⟫ + HPow.hPow (β := ℕ) ‖p₁ -ᵥ s.center‖ 2
⊢ HPow.hPow (β := ℕ) ‖p₂ -ᵥ s.center‖ 2 =
    HPow.hPow (β := ℕ) ‖p₂ -ᵥ p₁‖ 2 + 2 * ⟪p₂ -ᵥ p₁, p₁ -ᵥ s.center⟫ + HPow.hPow (β := ℕ) ‖p₁ -ᵥ s.center‖ 2

Tactic:
rw [← vsub_add_vsub_cancel p₂ p₁ s.center, norm_add_sq_real]

Premises used: vsub_add_vsub_cancel, EuclideanGeometry.Sphere.center, norm_add_sq_real
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
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
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₁p₂ : p₁ ≠ p₂
hp₁' : ‖p₁ -ᵥ s.center‖ = s.radius
hp₂' : ‖p₂ -ᵥ s.center‖ = s.radius
⊢ HPow.hPow (β := ℕ) ‖p₂ -ᵥ s.center‖ 2 =
    HPow.hPow (β := ℕ) ‖p₂ -ᵥ p₁‖ 2 + 2 * ⟪p₂ -ᵥ p₁, p₁ -ᵥ s.center⟫ + HPow.hPow (β := ℕ) ‖p₁ -ᵥ s.center‖ 2

Tactic:
have hd : ‖p₂ -ᵥ s.center‖ ^ 2 =
      ‖p₂ -ᵥ p₁‖ ^ 2 + 2 * ⟪p₂ -ᵥ p₁, p₁ -ᵥ s.center⟫ + ‖p₁ -ᵥ s.center‖ ^ 2 := by
    rw [← vsub_add_vsub_cancel p₂ p₁ s.center, norm_add_sq_real]
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
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
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₁p₂ : p₁ ≠ p₂
hp₁' : ‖p₁ -ᵥ s.center‖ = s.radius
hp₂' : ‖p₂ -ᵥ s.center‖ = s.radius
hd :
  HPow.hPow (β := ℕ) ‖p₂ -ᵥ s.center‖ 2 =
    HPow.hPow (β := ℕ) ‖p₂ -ᵥ p₁‖ 2 + 2 * ⟪p₂ -ᵥ p₁, p₁ -ᵥ s.center⟫ + HPow.hPow (β := ℕ) ‖p₁ -ᵥ s.center‖ 2
⊢ HPow.hPow (β := ℕ) s.radius 2 =
    HPow.hPow (β := ℕ) ‖p₂ -ᵥ p₁‖ 2 + 2 * -⟪p₂ -ᵥ p₁, s.center -ᵥ p₁⟫ + HPow.hPow (β := ℕ) s.radius 2

Tactic:
rw [hp₂', hp₁', ← neg_vsub_eq_vsub_rev s.center p₁, inner_neg_right] at hd

Premises used: inner_neg_right, EuclideanGeometry.Sphere.center, neg_vsub_eq_vsub_rev
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
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
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₁p₂ : p₁ ≠ p₂
hp₁' : ‖p₁ -ᵥ s.center‖ = s.radius
hp₂' : ‖p₂ -ᵥ s.center‖ = s.radius
hd :
  HPow.hPow (β := ℕ) s.radius 2 =
    HPow.hPow (β := ℕ) ‖p₂ -ᵥ p₁‖ 2 + 2 * -⟪p₂ -ᵥ p₁, s.center -ᵥ p₁⟫ + HPow.hPow (β := ℕ) s.radius 2
nlinarith :
  ⟪p₂ -ᵥ p₁, s.center -ᵥ p₁⟫ ≤ 0 →
    -(HPow.hPow (β := ℕ) s.radius 2 -
              (HPow.hPow (β := ℕ) ‖p₂ -ᵥ p₁‖ 2 + 2 * -⟪p₂ -ᵥ p₁, s.center -ᵥ p₁⟫ + HPow.hPow (β := ℕ) s.radius 2)) +
          2 * (⟪p₂ -ᵥ p₁, s.center -ᵥ p₁⟫ - 0) +
        (0 - HPow.hPow (β := ℕ) ‖p₂ -ᵥ p₁‖ 2) =
      0
nlinarith₁ : ⟪p₂ -ᵥ p₁, s.center -ᵥ p₁⟫ ≤ 0 → GT.gt (α := ℝ) 2 0
⊢ 0 < ⟪p₂ -ᵥ p₁, s.center -ᵥ p₁⟫

Tactic:
nlinarith [sq_pos_of_pos (norm_pos_iff.mpr (vsub_ne_zero.mpr hp₁p₂.symm))]

Premises used: Iff.mpr, norm_pos_iff, vsub_ne_zero, sq_pos_of_pos, Ne.symm
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
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 : Sphere P
p₁ p₂ p₃ : P
h : Collinear ℝ (P := P) {p₁, p₂, p₃}
hp₁ : p₁ ∈ s
hp₂ : dist p₂ s.center ≤ s.radius
hp₃ : p₃ ∈ s
hp₁p₃ : p₁ ≠ p₃
⊢ Wbtw ℝ p₁ p₂ p₃

Tactic:
h.wbtw_of_dist_eq_of_dist_le hp₁ hp₂ hp₃ hp₁p₃

Premises used: Collinear.wbtw_of_dist_eq_of_dist_le
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
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 : Sphere P
p₁ p₂ p₃ : P
h : Collinear ℝ (P := P) {p₁, p₂, p₃}
hp₁ : p₁ ∈ s
hp₂ : dist p₂ s.center < s.radius
hp₃ : p₃ ∈ s
hp₁p₃ : p₁ ≠ p₃
⊢ Sbtw ℝ p₁ p₂ p₃

Tactic:
h.sbtw_of_dist_eq_of_dist_lt hp₁ hp₂ hp₃ hp₁p₃

Premises used: Collinear.sbtw_of_dist_eq_of_dist_lt
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
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 : Sphere P
p₁ p₂ : P
⊢ s.IsDiameter p₁ p₂ ↔ p₁ ∈ s ∧ p₂ ∈ s ∧ dist p₁ p₂ = 2 * s.radius

Tactic:
⟨fun h ↦ ⟨h.left_mem, h.right_mem, h.dist_left_right⟩, fun ⟨h₁, h₂, hr⟩ ↦ ⟨h₁, ?_⟩⟩

Premises used: EuclideanGeometry.Sphere.IsDiameter.dist_left_right, EuclideanGeometry.Sphere.IsDiameter.right_mem, EuclideanGeometry.Sphere.IsDiameter.left_mem, EuclideanGeometry.Sphere.IsDiameter.mk, EuclideanGeometry.Sphere.IsDiameter, And.intro, Iff.intro, _private.0.EuclideanGeometry.Sphere.isDiameter_iff_mem_and_mem_and_dist.match_1
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
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 : Sphere P
p₁ p₂ : P
refine :
  p₁ ∈ s ∧ p₂ ∈ s ∧ dist p₁ p₂ = 2 * s.radius →
    ∀ (h₁ : p₁ ∈ s) (h₂ : p₂ ∈ s) (hr : dist p₁ p₂ = 2 * s.radius), midpoint ℝ p₁ p₂ = s.center
⊢ s.IsDiameter p₁ p₂ ↔ p₁ ∈ s ∧ p₂ ∈ s ∧ dist p₁ p₂ = 2 * s.radius

Tactic:
refine ⟨fun h ↦ ⟨h.left_mem, h.right_mem, h.dist_left_right⟩, fun ⟨h₁, h₂, hr⟩ ↦ ⟨h₁, ?_⟩⟩
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
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 : Sphere P
p₁ p₂ : P
h : p₁ ∈ s ∧ p₂ ∈ s ∧ dist p₁ p₂ = 2 * s.radius
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
hr : dist p₁ p₂ = 2 * s.radius
rw : p₂ -ᵥ s.center = s.center -ᵥ p₁
⊢ midpoint ℝ p₁ p₂ = s.center

Tactic:
rw [midpoint_eq_iff, AffineEquiv.pointReflection_apply, eq_comm, eq_vadd_iff_vsub_eq]

Premises used: eq_comm, AffineEquiv.pointReflection_apply, midpoint_eq_iff, eq_vadd_iff_vsub_eq
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
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 : Sphere P
p₁ p₂ : P
h : p₁ ∈ s ∧ p₂ ∈ s ∧ dist p₁ p₂ = 2 * s.radius
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
hr : dist p₁ p₂ = 2 * s.radius
h₃ : ‖p₂ -ᵥ s.center‖ = ‖s.center -ᵥ p₁‖
h₄ : ‖p₂ -ᵥ s.center + (s.center -ᵥ p₁)‖ = ‖p₂ -ᵥ s.center‖ + ‖s.center -ᵥ p₁‖
⊢ p₂ -ᵥ s.center = s.center -ᵥ p₁

Tactic:
apply eq_of_norm_eq_of_norm_add_eq

Premises used: eq_of_norm_eq_of_norm_add_eq
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
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 : Sphere P
p₁ p₂ : P
h : p₁ ∈ s ∧ p₂ ∈ s ∧ dist p₁ p₂ = 2 * s.radius
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
hr : dist p₁ p₂ = 2 * s.radius
h₃ : dist p₂ s.center = dist s.center p₁
h₄ : dist p₂ s.center = s.radius
⊢ ‖p₂ -ᵥ s.center‖ = ‖s.center -ᵥ p₁‖

Tactic:
simp_rw [← dist_eq_norm_vsub, mem_sphere'.1 h₁, mem_sphere.1 h₂]

Premises used: EuclideanGeometry.mem_sphere, EuclideanGeometry.mem_sphere', Iff.mp, dist_eq_norm_vsub
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
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 : Sphere P
p₁ p₂ : P
h : p₁ ∈ s ∧ p₂ ∈ s ∧ dist p₁ p₂ = 2 * s.radius
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
hr : dist p₁ p₂ = 2 * s.radius
h₃ : dist p₂ p₁ = s.radius + s.radius
⊢ ‖p₂ -ᵥ s.center + (s.center -ᵥ p₁)‖ = ‖p₂ -ᵥ s.center‖ + ‖s.center -ᵥ p₁‖

Tactic:
simp_rw [vsub_add_vsub_cancel, ← dist_eq_norm_vsub, mem_sphere'.1 h₁, mem_sphere.1 h₂]

Premises used: vsub_add_vsub_cancel, EuclideanGeometry.mem_sphere, EuclideanGeometry.mem_sphere', Iff.mp, dist_eq_norm_vsub
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
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 : Sphere P
p₁ p₂ : P
h : p₁ ∈ s ∧ p₂ ∈ s ∧ dist p₁ p₂ = 2 * s.radius
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
hr : dist p₁ p₂ = 2 * s.radius
h₃ : dist p₁ p₂ = s.radius + s.radius
h₄ : 2 * s.radius = s.radius + s.radius
h₅ h₆ : s.radius + s.radius = s.radius + s.radius
⊢ dist p₂ p₁ = s.radius + s.radius

Tactic:
rw [dist_comm, hr, two_mul]

Premises used: two_mul, dist_comm
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
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 : Sphere P
p₁ p₂ : P
⊢ s.IsDiameter p₁ p₂ ↔ p₁ ∈ s ∧ p₂ ∈ s ∧ Wbtw ℝ p₁ s.center p₂

Tactic:
⟨fun h ↦ ⟨h.left_mem, h.right_mem, h.wbtw⟩, fun ⟨h₁, h₂, hr⟩ ↦ ?_⟩

Premises used: EuclideanGeometry.Sphere.IsDiameter.right_mem, EuclideanGeometry.Sphere.IsDiameter.wbtw, EuclideanGeometry.Sphere.IsDiameter.left_mem, EuclideanGeometry.Sphere.IsDiameter, And.intro, Iff.intro, _private.0.EuclideanGeometry.Sphere.isDiameter_iff_mem_and_mem_and_wbtw.match_1
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
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 : Sphere P
p₁ p₂ : P
refine :
  p₁ ∈ s ∧ p₂ ∈ s ∧ Wbtw ℝ p₁ s.center p₂ →
    ∀ (h₁ : p₁ ∈ s) (h₂ : p₂ ∈ s) (hr : Wbtw ℝ p₁ s.center p₂), s.IsDiameter p₁ p₂
⊢ s.IsDiameter p₁ p₂ ↔ p₁ ∈ s ∧ p₂ ∈ s ∧ Wbtw ℝ p₁ s.center p₂

Tactic:
refine ⟨fun h ↦ ⟨h.left_mem, h.right_mem, h.wbtw⟩, fun ⟨h₁, h₂, hr⟩ ↦ ?_⟩
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
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 : Sphere P
p₁ p₂ : P
h : p₁ ∈ s ∧ p₂ ∈ s ∧ Wbtw ℝ p₁ s.center p₂
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
hr : Wbtw ℝ p₁ s.center p₂
⊢ dist p₁ s.center + dist s.center p₂ = dist p₁ p₂

Tactic:
have hd := hr.dist_add_dist
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
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 : Sphere P
p₁ p₂ : P
h : p₁ ∈ s ∧ p₂ ∈ s ∧ Wbtw ℝ p₁ s.center p₂
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
hr : Wbtw ℝ p₁ s.center p₂
hd : dist p₁ s.center + dist s.center p₂ = dist p₁ p₂
⊢ dist p₁ p₂ = 2 * s.radius

Tactic:
rw [mem_sphere.1 h₁, mem_sphere'.1 h₂, ← two_mul, eq_comm] at hd

Premises used: two_mul, eq_comm, EuclideanGeometry.mem_sphere, EuclideanGeometry.mem_sphere', Iff.mp
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
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 : Sphere P
p₁ p₂ : P
h : p₁ ∈ s ∧ p₂ ∈ s ∧ Wbtw ℝ p₁ s.center p₂
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
hr : Wbtw ℝ p₁ s.center p₂
hd : dist p₁ p₂ = 2 * s.radius
⊢ s.IsDiameter p₁ p₂

Tactic:
isDiameter_iff_mem_and_mem_and_dist.2 ⟨h₁, h₂, hd⟩

Premises used: Iff.mpr, EuclideanGeometry.Sphere.isDiameter_iff_mem_and_mem_and_dist, And.intro
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
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 : Sphere P
p₁ p₂ : P
h : p₁ ∈ s ∧ p₂ ∈ s ∧ Wbtw ℝ p₁ s.center p₂
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
hr : Wbtw ℝ p₁ s.center p₂
hd : dist p₁ p₂ = 2 * s.radius
⊢ s.IsDiameter p₁ p₂

Tactic:
exact isDiameter_iff_mem_and_mem_and_dist.2 ⟨h₁, h₂, hd⟩

Premises used: Iff.mpr, EuclideanGeometry.Sphere.isDiameter_iff_mem_and_mem_and_dist, And.intro
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
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 : Sphere P
p : P
⊢ Nonempty.{u_2 + 1} ↥(mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ)

Tactic:
infer_instance
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
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 : Sphere P
p : P
⊢ Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) p

Tactic:
self_mem_mk' _ _

Premises used: AffineSubspace.self_mem_mk', Set.Mem
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
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 : Sphere P
p x : P
rw : Membership.mem (γ := AffineSubspace ℝ P) (mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ) x ↔ ⟪x -ᵥ p, p -ᵥ s.center⟫ = 0
rw₁ : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (x -ᵥ p) ↔ ⟪x -ᵥ p, p -ᵥ s.center⟫ = 0
rw₂ rw₃ : ⟪x -ᵥ p, p -ᵥ s.center⟫ = 0 ↔ ⟪x -ᵥ p, p -ᵥ s.center⟫ = 0
⊢ Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) x ↔ ⟪x -ᵥ p, p -ᵥ s.center⟫ = 0

Tactic:
rw [orthRadius, mem_mk', Submodule.mem_orthogonal_singleton_iff_inner_left]

Premises used: EuclideanGeometry.Sphere.orthRadius, Submodule.mem_orthogonal_singleton_iff_inner_left, AffineSubspace.mem_mk'
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
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 : Sphere P
p x : P
rw : ⟪x -ᵥ p, p -ᵥ s.center⟫ = 0 ↔ ⟪p -ᵥ s.center, x -ᵥ p⟫ = 0
rw₁ rw₂ : ⟪p -ᵥ s.center, x -ᵥ p⟫ = 0 ↔ ⟪p -ᵥ s.center, x -ᵥ p⟫ = 0
⊢ Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) x ↔ ⟪p -ᵥ s.center, x -ᵥ p⟫ = 0

Tactic:
rw [mem_orthRadius_iff_inner_left, inner_eq_zero_symm]

Premises used: inner_eq_zero_symm, EuclideanGeometry.Sphere.mem_orthRadius_iff_inner_left
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
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 : Sphere P
p : P
rw : Eq (α := Submodule ℝ V) (direction (mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ)) (ℝ ∙ (p -ᵥ s.center))ᗮ
rw₁ rw₂ : Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (ℝ ∙ (p -ᵥ s.center))ᗮ
⊢ Eq (α := Submodule ℝ V) (direction (s.orthRadius p)) (ℝ ∙ (p -ᵥ s.center))ᗮ

Tactic:
rw [orthRadius, direction_mk']

Premises used: EuclideanGeometry.Sphere.orthRadius, AffineSubspace.direction_mk'
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
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 : Sphere P
p : P
rw : Submodule.HasOrthogonalProjection (E := V) (ℝ ∙ (p -ᵥ s.center))ᗮ
⊢ Submodule.HasOrthogonalProjection (direction (s.orthRadius p))

Tactic:
rw [direction_orthRadius]

Premises used: EuclideanGeometry.Sphere.direction_orthRadius
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
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 : Sphere P
p : P
⊢ Submodule.HasOrthogonalProjection (E := V) (ℝ ∙ (p -ᵥ s.center))ᗮ

Tactic:
infer_instance
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
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 : Sphere P
⊢ Eq (α := AffineSubspace ℝ P) (s.orthRadius s.center) ⊤

Tactic:
simp [orthRadius]

Premises used: EuclideanGeometry.Sphere.orthRadius
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
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 : Sphere P
p : P
rw : -⟪p -ᵥ s.center, p -ᵥ s.center⟫ = 0 ↔ p = s.center
⊢ Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) s.center ↔ p = s.center

Tactic:
rw [mem_orthRadius_iff_inner_left, ← neg_vsub_eq_vsub_rev, inner_neg_left]

Premises used: neg_vsub_eq_vsub_rev, EuclideanGeometry.Sphere.mem_orthRadius_iff_inner_left, inner_neg_left
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
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 : Sphere P
p : P
⊢ -⟪p -ᵥ s.center, p -ᵥ s.center⟫ = 0 ↔ p = s.center

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
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 : Sphere P
p : P
simp_rw :
  Membership.mem (γ := AffineSubspace ℝ P) (mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ) p ∧
    Membership.mem (γ := Submodule ℝ V) (direction (mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ))ᗮ (s.center -ᵥ p)
⊢ (↑((orthogonalProjection (s.orthRadius p) : (a : P) → ↥(s.orthRadius p)) s.center) : P) = p

Tactic:
simp_rw [orthRadius, coe_orthogonalProjection_eq_iff_mem]

Premises used: EuclideanGeometry.Sphere.orthRadius, EuclideanGeometry.coe_orthogonalProjection_eq_iff_mem
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
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 : Sphere P
p : P
rw :
  Membership.mem (γ := AffineSubspace ℝ P) (mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ) p ∧
    Membership.mem (γ := Submodule ℝ V) (direction (mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ))ᗮ (-(s.center -ᵥ p))
⊢ Membership.mem (γ := AffineSubspace ℝ P) (mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ) p ∧
    Membership.mem (γ := Submodule ℝ V) (direction (mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ))ᗮ (s.center -ᵥ p)

Tactic:
rw [← Submodule.neg_mem_iff]

Premises used: Submodule.neg_mem_iff
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
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 : Sphere P
p : P
⊢ Membership.mem (γ := AffineSubspace ℝ P) (mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ) p ∧
    Membership.mem (γ := Submodule ℝ V) (direction (mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ))ᗮ (-(s.center -ᵥ p))

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
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 : Sphere P
p q : P
⊢ LE.le (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius q) ↔ p = q ∨ q = s.center

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

Premises used: Iff.intro
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
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 : Sphere P
p q : P
refine_1 : ∀ (h : LE.le (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius q)), p = q ∨ q = s.center
refine_2 : ∀ (h : p = q ∨ q = s.center), LE.le (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius q)
⊢ LE.le (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius q) ↔ p = q ∨ q = s.center

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
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 : Sphere P
p q : P
h : LE.le (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius q)
⊢ LE.le (α := Submodule ℝ V) (direction (s.orthRadius p)) (direction (s.orthRadius q))

Tactic:
have h' := direction_le h
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
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 : Sphere P
p q : P
h : LE.le (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius q)
h' : LE.le (α := Submodule ℝ V) (direction (s.orthRadius p)) (direction (s.orthRadius q))
⊢ LE.le (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (ℝ ∙ (q -ᵥ s.center))ᗮ

Tactic:
simp only [direction_orthRadius] at h'

Premises used: EuclideanGeometry.Sphere.direction_orthRadius
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
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 : Sphere P
p q : P
h : LE.le (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius q)
h' : LE.le (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (ℝ ∙ (q -ᵥ s.center))ᗮ
⊢ LE.le (α := Submodule ℝ V) (ℝ ∙ (q -ᵥ s.center))ᗮᗮ (ℝ ∙ (p -ᵥ s.center))ᗮᗮ

Tactic:
have h'' := Submodule.orthogonal_le h'