awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
E : Type u_3
F : Type u_4
inst : MetricSpace E
inst_1 : MetricSpace F
f : E → F
hf : Isometry f
ps : Set E
c : E
r : ℝ
hc : ∀ p ∈ ps, dist p c = r
⊢ Cospherical (f '' ps)

Tactic:
⟨f c, r, ?_⟩

Premises used: EuclideanGeometry.Cospherical, Exists.intro
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
E : Type u_3
F : Type u_4
inst : MetricSpace E
inst_1 : MetricSpace F
f : E → F
hf : Isometry f
ps : Set E
c : E
r : ℝ
hc : ∀ p ∈ ps, dist p c = r
refine : ∀ p ∈ f '' ps, dist p (f c) = r
⊢ Cospherical (f '' ps)

Tactic:
refine ⟨f c, r, ?_⟩
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
E : Type u_3
F : Type u_4
inst : MetricSpace E
inst_1 : MetricSpace F
f : E → F
hf : Isometry f
ps : Set E
c : E
r : ℝ
hc : ∀ p ∈ ps, dist p c = r
p : E
hp : p ∈ ps
rw : dist p c = r
rw₁ rw₂ : r = r
⊢ dist (f p) (f c) = r

Tactic:
rw [hf.dist_eq, hc p hp]

Premises used: Isometry.dist_eq
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
S₁ S₂ : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥S₁
ps : Set ↥S₁
hps : Cospherical ps
hS : S₁ ≤ S₂
⊢ Cospherical (P := ↥S₂) ((⇑(AffineSubspace.inclusion hS) : (a : ↥S₁) → ↥S₂) '' ps)

Tactic:
Isometry.cospherical ?_ hps

Premises used: Isometry.cospherical
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
S₁ S₂ : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥S₁
ps : Set ↥S₁
hps : Cospherical ps
hS : S₁ ≤ S₂
refine : Isometry.{u_2, u_2} (α := ↥S₁) (β := ↥S₂) (⇑(AffineSubspace.inclusion hS) : (a : ↥S₁) → ↥S₂)
⊢ Cospherical (P := ↥S₂) ((⇑(AffineSubspace.inclusion hS) : (a : ↥S₁) → ↥S₂) '' ps)

Tactic:
refine Isometry.cospherical ?_ hps

Premises used: Isometry.cospherical
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
S₁ S₂ : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥S₁
ps : Set ↥S₁
hps : Cospherical ps
hS : S₁ ≤ S₂
⊢ Isometry.{u_2, u_2} (α := ↥S₁) (β := ↥S₂) (⇑(AffineSubspace.inclusion hS) : (a : ↥S₁) → ↥S₂)

Tactic:
S₁.subtypeₐᵢ.isometry

Premises used: Set.Mem, AffineIsometry.isometry, AffineSubspace.subtypeₐᵢ, Isometry
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
S₁ S₂ : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥S₁
ps : Set ↥S₁
hps : Cospherical ps
hS : S₁ ≤ S₂
⊢ Isometry.{u_2, u_2} (α := ↥S₁) (β := ↥S₂) (⇑(AffineSubspace.inclusion hS) : (a : ↥S₁) → ↥S₂)

Tactic:
exact S₁.subtypeₐᵢ.isometry

Premises used: AffineIsometry.isometry, AffineSubspace.subtypeₐᵢ
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
S : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥S
ps : Set ↥S
hps : Cospherical ps
⊢ Cospherical (Subtype.val (p := fun (x : P) ↦ x ∈ S) '' ps)

Tactic:
Isometry.cospherical S.subtypeₐᵢ.isometry hps

Premises used: Set.Mem, AffineIsometry.isometry, AffineSubspace.subtypeₐᵢ, Isometry.cospherical
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Nontrivial V
s : Sphere P
⊢ (Metric.sphere s.center s.radius).Nonempty ↔ 0 ≤ s.radius

Tactic:
⟨fun ⟨p, hp⟩ ↦ radius_nonneg_of_mem hp, fun h ↦ ?_⟩

Premises used: _private.0.EuclideanGeometry.Sphere.nonempty_iff.match_1, LE.le, EuclideanGeometry.Sphere.radius_nonneg_of_mem, Iff.intro, OfNat.ofNat, EuclideanGeometry.Sphere.radius
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Nontrivial V
s : Sphere P
refine : ∀ (h : 0 ≤ s.radius), (Metric.sphere s.center s.radius).Nonempty
⊢ (Metric.sphere s.center s.radius).Nonempty ↔ 0 ≤ s.radius

Tactic:
refine ⟨fun ⟨p, hp⟩ ↦ radius_nonneg_of_mem hp, fun h ↦ ?_⟩
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Nontrivial V
s : Sphere P
h : 0 ≤ s.radius
obtain :
  ∀ (v : V) (hv : Membership.mem (γ := Set V) (Metric.sphere 0 s.radius) v), (Metric.sphere s.center s.radius).Nonempty
⊢ (Metric.sphere s.center s.radius).Nonempty

Tactic:
obtain ⟨v, hv⟩ := (NormedSpace.sphere_nonempty (x := (0 : V)) (r := s.radius)).2 h

Premises used: Iff.mpr, NormedSpace.sphere_nonempty
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Nontrivial V
s : Sphere P
h : 0 ≤ s.radius
v : V
hv : Membership.mem (γ := Set V) (Metric.sphere 0 s.radius) v
⊢ (Metric.sphere s.center s.radius).Nonempty

Tactic:
⟨v +ᵥ s.center, ?_⟩

Premises used: HVAdd.hVAdd, EuclideanGeometry.Sphere.center, Set.Nonempty, Exists.intro
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Nontrivial V
s : Sphere P
h : 0 ≤ s.radius
v : V
hv : Membership.mem (γ := Set V) (Metric.sphere 0 s.radius) v
refine : v +ᵥ s.center ∈ Metric.sphere s.center s.radius
⊢ (Metric.sphere s.center s.radius).Nonempty

Tactic:
refine ⟨v +ᵥ s.center, ?_⟩
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Nontrivial V
s : Sphere P
h : 0 ≤ s.radius
v : V
hv : Membership.mem (γ := Set V) (Metric.sphere 0 s.radius) v
⊢ v +ᵥ s.center ∈ Metric.sphere s.center s.radius

Tactic:
simpa [mem_sphere] using hv

Premises used: EuclideanGeometry.mem_sphere
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p₂ p : P
inl : dist (midpoint ℝ p p₂) p = (norm (E := ℝ) 2)⁻¹ * dist p p₂
inl₁ inl₂ : (norm (E := ℝ) 2)⁻¹ * dist p p₂ = (norm (E := ℝ) 2)⁻¹ * dist p p₂
⊢ dist p (midpoint ℝ p p₂) = (norm (E := ℝ) 2)⁻¹ * dist p p₂

Tactic:
rw [dist_comm, dist_midpoint_left (𝕜 := ℝ)]

Premises used: dist_comm, dist_midpoint_left
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p₁ p₂ : P
inr : dist (midpoint ℝ p₁ p₂) p₂ = (norm (E := ℝ) 2)⁻¹ * dist p₁ p₂
inr₁ inr₂ : (norm (E := ℝ) 2)⁻¹ * dist p₁ p₂ = (norm (E := ℝ) 2)⁻¹ * dist p₁ p₂
⊢ dist p₂ (midpoint ℝ p₁ p₂) = (norm (E := ℝ) 2)⁻¹ * dist p₁ p₂

Tactic:
rw [dist_comm, dist_midpoint_right (𝕜 := ℝ)]

Premises used: dist_midpoint_right, dist_comm
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
ps₁ ps₂ : Set P
hs : ps₁ ⊆ ps₂
h : Concyclic ps₂
⊢ Concyclic ps₁

Tactic:
⟨h.1.subset hs, h.2.subset hs⟩

Premises used: EuclideanGeometry.Cospherical.subset, EuclideanGeometry.Concyclic.Coplanar, EuclideanGeometry.Concyclic.Cospherical, EuclideanGeometry.Concyclic.mk, Coplanar.subset
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
⊢ Concyclic.{u_1, u_2} (P := P) ∅

Tactic:
⟨cospherical_empty, coplanar_empty ℝ P⟩

Premises used: coplanar_empty, Real, EuclideanGeometry.Concyclic.mk, EuclideanGeometry.cospherical_empty
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p : P
⊢ Concyclic (P := P) {p}

Tactic:
⟨cospherical_singleton p, coplanar_singleton ℝ p⟩

Premises used: Real, EuclideanGeometry.cospherical_singleton, EuclideanGeometry.Concyclic.mk, coplanar_singleton
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p₁ p₂ : P
⊢ Concyclic (P := P) {p₁, p₂}

Tactic:
⟨cospherical_pair p₁ p₂, coplanar_pair ℝ p₁ p₂⟩

Premises used: Real, EuclideanGeometry.cospherical_pair, coplanar_pair, EuclideanGeometry.Concyclic.mk
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
rw : dist p₂ s.center = s.radius
rw₁ : dist p₂ s.center = dist p₁ s.center
rw₂ : dist p₂ (midpoint ℝ p₁ p₂) = dist p₁ (midpoint ℝ p₁ p₂)
rw₃ rw₄ : dist p₂ (midpoint ℝ p₁ p₂) = dist p₂ (midpoint ℝ p₁ p₂)
⊢ p₂ ∈ s

Tactic:
rw [mem_sphere, ← mem_sphere.1 h.left_mem, ← h.midpoint_eq_center,
    dist_left_midpoint_eq_dist_right_midpoint]

Premises used: dist_left_midpoint_eq_dist_right_midpoint, EuclideanGeometry.Sphere.IsDiameter.left_mem, EuclideanGeometry.mem_sphere, EuclideanGeometry.Sphere.IsDiameter.midpoint_eq_center, Iff.mp
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
⊢ s.IsDiameter p₂ p₁

Tactic:
⟨h.right_mem, midpoint_comm (R := ℝ) p₁ p₂ ▸ h.midpoint_eq_center⟩

Premises used: EuclideanGeometry.Sphere.IsDiameter.right_mem, EuclideanGeometry.Sphere.IsDiameter.mk, midpoint_comm, Eq.rec, EuclideanGeometry.Sphere.IsDiameter.midpoint_eq_center
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
⊢ s.IsDiameter p₁ p₂ ↔ s.IsDiameter p₂ p₁

Tactic:
⟨IsDiameter.symm, IsDiameter.symm⟩

Premises used: EuclideanGeometry.Sphere.IsDiameter.symm, Iff.intro
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
⊢ s.IsDiameter p₁ p₂ ↔ p₁ ∈ s ∧ midpoint ℝ p₁ p₂ = s.center

Tactic:
⟨fun h ↦ ⟨h.1, h.2⟩, fun h ↦ ⟨h.1, h.2⟩⟩

Premises used: EuclideanGeometry.Sphere.IsDiameter.left_mem, EuclideanGeometry.Sphere.IsDiameter.mk, And.right, And.left, EuclideanGeometry.Sphere.IsDiameter.midpoint_eq_center, And.intro, Iff.intro
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
⊢ s.IsDiameter p₁ p₂ ↔ p₂ ∈ s ∧ midpoint ℝ p₁ p₂ = s.center

Tactic:
⟨fun h ↦ ⟨h.right_mem, h.2⟩, fun h ↦ IsDiameter.symm ⟨h.1, midpoint_comm (R := ℝ) p₁ p₂ ▸ h.2⟩⟩

Premises used: EuclideanGeometry.Sphere.IsDiameter.symm, EuclideanGeometry.Sphere.IsDiameter.right_mem, EuclideanGeometry.Sphere.IsDiameter.mk, midpoint_comm, Eq.rec, And.right, And.left, EuclideanGeometry.Sphere.IsDiameter.midpoint_eq_center, And.intro, Iff.intro
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
rw : (Equiv.pointReflection (midpoint ℝ p₁ p₂) : (a : P) → P) p₁ = p₂
rw₁ rw₂ : p₂ = p₂
⊢ (Equiv.pointReflection s.center : (a : P) → P) p₁ = p₂

Tactic:
rw [← h.midpoint_eq_center, Equiv.pointReflection_midpoint_left]

Premises used: EuclideanGeometry.Sphere.IsDiameter.midpoint_eq_center, Equiv.pointReflection_midpoint_left
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
rw : (Equiv.pointReflection (midpoint ℝ p₁ p₂) : (a : P) → P) p₂ = p₁
rw₁ rw₂ : p₁ = p₁
⊢ (Equiv.pointReflection s.center : (a : P) → P) p₂ = p₁

Tactic:
rw [← h.midpoint_eq_center, Equiv.pointReflection_midpoint_right]

Premises used: Equiv.pointReflection_midpoint_right, EuclideanGeometry.Sphere.IsDiameter.midpoint_eq_center
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : p₁ ∈ s ∧ (Equiv.pointReflection s.center : (a : P) → P) p₁ = p₂
⊢ midpoint ℝ p₁ p₂ = s.center

Tactic:
simp [← h.2]

Premises used: And.right
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
rw : s.IsDiameter p₂ p₁ ↔ p₂ ∈ s ∧ (Equiv.pointReflection s.center : (a : P) → P) p₂ = p₁
rw₁ rw₂ :
  p₂ ∈ s ∧ (Equiv.pointReflection s.center : (a : P) → P) p₂ = p₁ ↔
    p₂ ∈ s ∧ (Equiv.pointReflection s.center : (a : P) → P) p₂ = p₁
⊢ s.IsDiameter p₁ p₂ ↔ p₂ ∈ s ∧ (Equiv.pointReflection s.center : (a : P) → P) p₂ = p₁

Tactic:
rw [isDiameter_comm, isDiameter_iff_left_mem_and_pointReflection_center_left]

Premises used: EuclideanGeometry.Sphere.isDiameter_comm, EuclideanGeometry.Sphere.isDiameter_iff_left_mem_and_pointReflection_center_left
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p₁ p₂ p₃ : P
h₁₂ : s.IsDiameter p₁ p₂
h₁₃ : s.IsDiameter p₁ p₃
rw : (Equiv.pointReflection s.center : (a : P) → P) p₁ = p₃
rw₁ rw₂ :
  Eq (α := P) ((Equiv.pointReflection s.center : (a : P) → P) p₁ : P)
    ((Equiv.pointReflection s.center : (a : P) → P) p₁ : P)
⊢ p₂ = p₃

Tactic:
rw [← h₁₂.pointReflection_center_left, ← h₁₃.pointReflection_center_left]

Premises used: EuclideanGeometry.Sphere.IsDiameter.pointReflection_center_left
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p₁ p₂ p₃ : P
h₁₃ : s.IsDiameter p₁ p₃
h₂₃ : s.IsDiameter p₂ p₃
rw : (Equiv.pointReflection s.center : (a : P) → P) p₃ = p₂
rw₁ rw₂ :
  Eq (α := P) ((Equiv.pointReflection s.center : (a : P) → P) p₃ : P)
    ((Equiv.pointReflection s.center : (a : P) → P) p₃ : P)
⊢ p₁ = p₂

Tactic:
rw [← h₁₃.pointReflection_center_right, ← h₂₃.pointReflection_center_right]

Premises used: EuclideanGeometry.Sphere.IsDiameter.pointReflection_center_right
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
rw : dist p₁ p₂ = 2 * ((norm (E := ℝ) 2)⁻¹ * dist p₁ p₂)
⊢ dist p₁ p₂ = 2 * s.radius

Tactic:
rw [← mem_sphere.1 h.left_mem, ← h.midpoint_eq_center, dist_left_midpoint]

Premises used: dist_left_midpoint, EuclideanGeometry.Sphere.IsDiameter.left_mem, EuclideanGeometry.mem_sphere, EuclideanGeometry.Sphere.IsDiameter.midpoint_eq_center, Iff.mp
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
⊢ dist p₁ p₂ = 2 * ((norm (E := ℝ) 2)⁻¹ * dist p₁ p₂)

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
⊢ dist p₁ p₂ / 2 = s.radius

Tactic:
simp [h.dist_left_right]

Premises used: EuclideanGeometry.Sphere.IsDiameter.dist_left_right
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
rw : 2 * s.radius = 0 ↔ s.radius = 0
⊢ p₁ = p₂ ↔ s.radius = 0

Tactic:
rw [← dist_eq_zero, h.dist_left_right]

Premises used: EuclideanGeometry.Sphere.IsDiameter.dist_left_right, dist_eq_zero
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
⊢ 2 * s.radius = 0 ↔ s.radius = 0

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
⊢ p₁ ≠ p₂ ↔ s.radius ≠ 0

Tactic:
h.left_eq_right_iff.not

Premises used: Iff.not, EuclideanGeometry.Sphere.IsDiameter.left_eq_right_iff
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
rw : s.radius ≠ 0 ↔ 0 ≤ s.radius ∧ 0 ≠ s.radius
⊢ p₁ ≠ p₂ ↔ 0 < s.radius

Tactic:
rw [h.left_ne_right_iff_radius_ne_zero, lt_iff_le_and_ne]

Premises used: lt_iff_le_and_ne, EuclideanGeometry.Sphere.IsDiameter.left_ne_right_iff_radius_ne_zero
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
⊢ s.radius ≠ 0 ↔ 0 ≤ s.radius ∧ 0 ≠ s.radius

Tactic:
simp [radius_nonneg_of_mem h.left_mem, eq_comm]

Premises used: EuclideanGeometry.Sphere.IsDiameter.left_mem, eq_comm, EuclideanGeometry.Sphere.radius_nonneg_of_mem
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
rw : Wbtw ℝ p₁ (midpoint ℝ p₁ p₂) p₂
⊢ Wbtw ℝ p₁ s.center p₂

Tactic:
rw [← h.midpoint_eq_center]

Premises used: EuclideanGeometry.Sphere.IsDiameter.midpoint_eq_center
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
⊢ Wbtw ℝ p₁ (midpoint ℝ p₁ p₂) p₂

Tactic:
wbtw_midpoint _ _ _

Premises used: wbtw_midpoint
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
⊢ Wbtw ℝ p₁ (midpoint ℝ p₁ p₂) p₂

Tactic:
exact wbtw_midpoint _ _ _

Premises used: wbtw_midpoint
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
hr : s.radius ≠ 0
rw : Sbtw ℝ p₁ (midpoint ℝ p₁ p₂) p₂
⊢ Sbtw ℝ p₁ s.center p₂

Tactic:
rw [← h.midpoint_eq_center]

Premises used: EuclideanGeometry.Sphere.IsDiameter.midpoint_eq_center
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
hr : s.radius ≠ 0
⊢ Sbtw ℝ p₁ (midpoint ℝ p₁ p₂) p₂

Tactic:
sbtw_midpoint_of_ne _ (h.left_ne_right_iff_radius_ne_zero.2 hr)

Premises used: Iff.mpr, sbtw_midpoint_of_ne, EuclideanGeometry.Sphere.IsDiameter.left_ne_right_iff_radius_ne_zero
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
hr : s.radius ≠ 0
⊢ Sbtw ℝ p₁ (midpoint ℝ p₁ p₂) p₂

Tactic:
exact sbtw_midpoint_of_ne _ (h.left_ne_right_iff_radius_ne_zero.2 hr)

Premises used: Iff.mpr, sbtw_midpoint_of_ne, EuclideanGeometry.Sphere.IsDiameter.left_ne_right_iff_radius_ne_zero
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p₁ p₂ : P
⊢ Membership.mem (γ := Sphere P) (Sphere.ofDiameter p₁ p₂) p₁

Tactic:
simp [Sphere.ofDiameter, mem_sphere, inv_mul_eq_div]

Premises used: EuclideanGeometry.Sphere.ofDiameter, inv_mul_eq_div, EuclideanGeometry.mem_sphere
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
center : Sphere.center (Sphere.ofDiameter p₁ p₂) = s.center
radius : Sphere.radius (Sphere.ofDiameter p₁ p₂) = s.radius
⊢ Sphere.ofDiameter p₁ p₂ = s

Tactic:
ext
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
⊢ center (Sphere.ofDiameter p₁ p₂) = s.center

Tactic:
simp [Sphere.ofDiameter, h.midpoint_eq_center]

Premises used: EuclideanGeometry.Sphere.ofDiameter, EuclideanGeometry.Sphere.IsDiameter.midpoint_eq_center
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
⊢ radius (Sphere.ofDiameter p₁ p₂) = s.radius

Tactic:
simp [Sphere.ofDiameter, ← h.dist_left_right_div_two]

Premises used: EuclideanGeometry.Sphere.ofDiameter, EuclideanGeometry.Sphere.IsDiameter.dist_left_right_div_two
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p₁ p₂ : P
⊢ IsDiameter (Sphere.ofDiameter p₁ p₂) p₁ p₂

Tactic:
isDiameter_ofDiameter _ _

Premises used: EuclideanGeometry.Sphere.isDiameter_ofDiameter
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p₁ p₂ : P
⊢ IsDiameter (Sphere.ofDiameter p₁ p₂) p₁ p₂

Tactic:
exact isDiameter_ofDiameter _ _

Premises used: EuclideanGeometry.Sphere.isDiameter_ofDiameter
-- 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 : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥S
inst_5 : S.direction.HasOrthogonalProjection
ps : Set ↥S
⊢ Cospherical (Subtype.val (p := fun (x : P) ↦ x ∈ S) '' ps) ↔ Cospherical ps

Tactic:
⟨fun h => ?_, Cospherical.subtype_val⟩

Premises used: Iff.intro, EuclideanGeometry.Cospherical.subtype_val
-- 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 : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥S
inst_5 : S.direction.HasOrthogonalProjection
ps : Set ↥S
refine : ∀ (h : Cospherical (Subtype.val (p := fun (x : P) ↦ x ∈ S) '' ps)), Cospherical ps
⊢ Cospherical (Subtype.val (p := fun (x : P) ↦ x ∈ S) '' ps) ↔ Cospherical ps

Tactic:
refine ⟨fun h => ?_, Cospherical.subtype_val⟩