awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (goal)
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₂
⊢ dist p (midpoint ℝ p p₂) = (norm (E := ℝ) 2)⁻¹ * dist p p₂
have inl₁ : (norm (E := ℝ) 2)⁻¹ * dist p p₂ = (norm (E := ℝ) 2)⁻¹ * dist p p₂
Tactic: rw [dist_comm, dist_midpoint_left (𝕜 := ℝ)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (goal)
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
⊢ dist p₂ (midpoint ℝ p₁ p₂) = (norm (E := ℝ) 2)⁻¹ * dist p₁ p₂
have inr : dist (midpoint ℝ p₁ p₂) p₂ = (norm (E := ℝ) 2)⁻¹ * dist p₁ p₂
Tactic: rw [dist_comm, dist_midpoint_right (𝕜 := ℝ)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (goal)
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₂
⊢ dist p₂ (midpoint ℝ p₁ p₂) = (norm (E := ℝ) 2)⁻¹ * dist p₁ p₂
have inr₁ : (norm (E := ℝ) 2)⁻¹ * dist p₁ p₂ = (norm (E := ℝ) 2)⁻¹ * dist p₁ p₂
Tactic: rw [dist_comm, dist_midpoint_right (𝕜 := ℝ)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (goal)
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₂ ∈ s
have rw : dist p₂ s.center = s.radius
Tactic: rw [mem_sphere, ← mem_sphere.1 h.left_mem, ← h.midpoint_eq_center,
    dist_left_midpoint_eq_dist_right_midpoint]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (goal)
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
⊢ p₂ ∈ s
have rw₁ : dist p₂ s.center = dist p₁ s.center
Tactic: rw [mem_sphere, ← mem_sphere.1 h.left_mem, ← h.midpoint_eq_center,
    dist_left_midpoint_eq_dist_right_midpoint]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (goal)
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
⊢ p₂ ∈ s
have rw₂ : dist p₂ (midpoint ℝ p₁ p₂) = dist p₁ (midpoint ℝ p₁ p₂)
Tactic: rw [mem_sphere, ← mem_sphere.1 h.left_mem, ← h.midpoint_eq_center,
    dist_left_midpoint_eq_dist_right_midpoint]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (goal)
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₂)
⊢ p₂ ∈ s
have rw₃ : dist p₂ (midpoint ℝ p₁ p₂) = dist p₂ (midpoint ℝ p₁ p₂)
Tactic: rw [mem_sphere, ← mem_sphere.1 h.left_mem, ← h.midpoint_eq_center,
    dist_left_midpoint_eq_dist_right_midpoint]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (goal)
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₂
⊢ (Equiv.pointReflection s.center : (a : P) → P) p₁ = p₂
have rw : (Equiv.pointReflection (midpoint ℝ p₁ p₂) : (a : P) → P) p₁ = p₂
Tactic: rw [← h.midpoint_eq_center, Equiv.pointReflection_midpoint_left]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (goal)
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₂
⊢ (Equiv.pointReflection s.center : (a : P) → P) p₁ = p₂
have rw₁ : p₂ = p₂
Tactic: rw [← h.midpoint_eq_center, Equiv.pointReflection_midpoint_left]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (goal)
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₂
⊢ (Equiv.pointReflection s.center : (a : P) → P) p₂ = p₁
have rw : (Equiv.pointReflection (midpoint ℝ p₁ p₂) : (a : P) → P) p₂ = p₁
Tactic: rw [← h.midpoint_eq_center, Equiv.pointReflection_midpoint_right]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (goal)
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₁
⊢ (Equiv.pointReflection s.center : (a : P) → P) p₂ = p₁
have rw₁ : p₁ = p₁
Tactic: rw [← h.midpoint_eq_center, Equiv.pointReflection_midpoint_right]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (goal)
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 ∧ (Equiv.pointReflection s.center : (a : P) → P) p₂ = p₁
have rw : 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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (goal)
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₁
⊢ s.IsDiameter p₁ p₂ ↔ p₂ ∈ s ∧ (Equiv.pointReflection s.center : (a : P) → P) p₂ = p₁
have rw₁ : p₂ ∈ s ∧ (Equiv.pointReflection s.center : (a : P) → P) 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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (goal)
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₃
⊢ p₂ = p₃
have rw : (Equiv.pointReflection s.center : (a : P) → P) p₁ = p₃
Tactic: rw [← h₁₂.pointReflection_center_left, ← h₁₃.pointReflection_center_left]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (goal)
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₃
⊢ p₂ = p₃
have rw₁ : Eq (α := P) ((Equiv.pointReflection s.center : (a : P) → P) p₁ : P)
  ((Equiv.pointReflection s.center : (a : P) → P) p₁ : P)
Tactic: rw [← h₁₂.pointReflection_center_left, ← h₁₃.pointReflection_center_left]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (goal)
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₃
⊢ p₁ = p₂
have rw : (Equiv.pointReflection s.center : (a : P) → P) p₃ = p₂
Tactic: rw [← h₁₃.pointReflection_center_right, ← h₂₃.pointReflection_center_right]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (goal)
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₂
⊢ p₁ = p₂
have rw₁ : Eq (α := P) ((Equiv.pointReflection s.center : (a : P) → P) p₃ : P)
  ((Equiv.pointReflection s.center : (a : P) → P) p₃ : P)
Tactic: rw [← h₁₃.pointReflection_center_right, ← h₂₃.pointReflection_center_right]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (goal)
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
have rw : dist p₁ p₂ = 2 * ((norm (E := ℝ) 2)⁻¹ * dist p₁ p₂)
Tactic: rw [← mem_sphere.1 h.left_mem, ← h.midpoint_eq_center, dist_left_midpoint]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (goal)
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
have rw : 2 * s.radius = 0 ↔ s.radius = 0
Tactic: rw [← dist_eq_zero, h.dist_left_right]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (goal)
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₂ ↔ 0 < s.radius
have rw : s.radius ≠ 0 ↔ 0 ≤ s.radius ∧ 0 ≠ s.radius
Tactic: rw [h.left_ne_right_iff_radius_ne_zero, lt_iff_le_and_ne]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (goal)
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₁ s.center p₂
have rw : Wbtw ℝ p₁ (midpoint ℝ p₁ p₂) p₂
Tactic: rw [← h.midpoint_eq_center]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (goal)
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₁ s.center p₂
have rw : Sbtw ℝ p₁ (midpoint ℝ p₁ p₂) p₂
Tactic: rw [← h.midpoint_eq_center]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (goal)
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₂
⊢ Sphere.ofDiameter p₁ p₂ = s
have center : center (Sphere.ofDiameter p₁ p₂) = s.center
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (goal)
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
⊢ Sphere.ofDiameter p₁ p₂ = s
have radius : radius (Sphere.ofDiameter p₁ p₂) = s.radius
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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 : 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
have refine : ∀ (h : Cospherical (Subtype.val (p := fun (x : P) ↦ x ∈ S) '' ps)), Cospherical ps
Tactic: refine ⟨fun h => ?_, Cospherical.subtype_val⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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 : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥S
inst_5 : S.direction.HasOrthogonalProjection
ps : Set ↥S
h : Cospherical (Subtype.val (p := fun (x : P) ↦ x ∈ S) '' ps)
⊢ Cospherical ps
have inl : ∀ (h : Cospherical.{u_2} (P := P) (Set.image (α := ↥S) (Subtype.val (p := fun (x : P) ↦ x ∈ S)) ∅)),
  Cospherical.{u_2} (P := ↥S) ∅
Tactic: rcases ps.eq_empty_or_nonempty with rfl | ⟨p₀, hp₀⟩
Cleared hypotheses: ps, h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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 : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥S
inst_5 : S.direction.HasOrthogonalProjection
ps : Set ↥S
h : Cospherical (Subtype.val (p := fun (x : P) ↦ x ∈ S) '' ps)
inl :
  ∀ (h : Cospherical.{u_2} (P := P) (Set.image (α := ↥S) (Subtype.val (p := fun (x : P) ↦ x ∈ S)) ∅)),
    Cospherical.{u_2} (P := ↥S) ∅
⊢ Cospherical ps
have inr : ∀ (p₀ : ↥S) (hp₀ : p₀ ∈ ps), Cospherical ps
Tactic: rcases ps.eq_empty_or_nonempty with rfl | ⟨p₀, hp₀⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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 : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥S
inst_5 : S.direction.HasOrthogonalProjection
ps : Set ↥S
h : Cospherical (Subtype.val (p := fun (x : P) ↦ x ∈ S) '' ps)
p₀ : ↥S
hp₀ : p₀ ∈ ps
⊢ Cospherical ps
have inr : ∀ (c : P) (r : ℝ) (hr : ∀ p ∈ Subtype.val (p := fun (x : P) ↦ x ∈ S) '' ps, dist p c = r), Cospherical ps
Tactic: rcases h with ⟨c, r, hr⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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 : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥S
inst_5 : S.direction.HasOrthogonalProjection
ps : Set ↥S
p₀ : ↥S
hp₀ : p₀ ∈ ps
c : P
r : ℝ
hr : ∀ p ∈ Subtype.val (p := fun (x : P) ↦ x ∈ S) '' ps, dist p c = r
c' : ↥S := (orthogonalProjection S : (a : P) → ↥S) c
⊢ Cospherical ps
have inr : ∀ (p : ↥S) (hp : p ∈ ps), dist p c' = dist p₀ c'
Tactic: refine ⟨c', dist p₀ c', fun p hp => ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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
S : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥S
inst_5 : S.direction.HasOrthogonalProjection
ps : Set ↥S
p₀ : ↥S
hp₀ : p₀ ∈ ps
c : P
r : ℝ
hr : ∀ p ∈ Subtype.val (p := fun (x : P) ↦ x ∈ S) '' ps, dist p c = r
c' : ↥S := (orthogonalProjection S : (a : P) → ↥S) c
p : ↥S
hp : p ∈ ps
⊢ dist p c' = dist p₀ c'
have hp_dist : dist (↑p : P) c = r
Tactic: have hp_dist : dist (p : P) c = r := by grind
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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
S : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥S
inst_5 : S.direction.HasOrthogonalProjection
ps : Set ↥S
p₀ : ↥S
hp₀ : p₀ ∈ ps
c : P
r : ℝ
hr : ∀ p ∈ Subtype.val (p := fun (x : P) ↦ x ∈ S) '' ps, dist p c = r
c' : ↥S := (orthogonalProjection S : (a : P) → ↥S) c
p : ↥S
hp : p ∈ ps
hp_dist : dist (↑p : P) c = r
⊢ dist p c' = dist p₀ c'
have hp₀_dist : dist (↑p₀ : P) c = r
Tactic: have hp₀_dist : dist (p₀ : P) c = r := by grind
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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
S : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥S
inst_5 : S.direction.HasOrthogonalProjection
ps : Set ↥S
p₀ : ↥S
hp₀ : p₀ ∈ ps
c : P
r : ℝ
hr : ∀ p ∈ Subtype.val (p := fun (x : P) ↦ x ∈ S) '' ps, dist p c = r
c' : ↥S := (orthogonalProjection S : (a : P) → ↥S) c
p : ↥S
hp : p ∈ ps
hp_dist : dist (↑p : P) c = r
hp₀_dist : dist (↑p₀ : P) c = r
⊢ dist p c' = dist p₀ c'
have hpp₀ : dist (↑p : P) c = dist (↑p₀ : P) c
Tactic: have hpp₀ : dist (p : P) (c : P) = dist (p₀ : P) (c : P) := hp_dist.trans hp₀_dist.symm
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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₁ S₂ : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥S₁
ps : Set ↥S₁
inst_5 : S₁.direction.HasOrthogonalProjection
inst_6 : S₂.direction.HasOrthogonalProjection
hS : S₁ ≤ S₂
⊢ Nonempty.{u_2 + 1} ↥S₂
have obtain : ∀ (p : ↥S₁), Nonempty.{u_2 + 1} ↥S₂
Tactic: obtain ⟨p⟩ := ‹Nonempty S₁›
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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
S₁ S₂ : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥S₁
ps : Set ↥S₁
inst_5 : S₁.direction.HasOrthogonalProjection
inst_6 : S₂.direction.HasOrthogonalProjection
hS : S₁ ≤ S₂
⊢ Cospherical (P := ↥S₂) ((⇑(AffineSubspace.inclusion hS) : (a : ↥S₁) → ↥S₂) '' ps) ↔ Cospherical ps
have this : Nonempty.{u_2 + 1} ↥S₂
Tactic: haveI : Nonempty S₂ := by obtain ⟨p⟩ := ‹Nonempty S₁›; exact ⟨⟨p, hS p.property⟩⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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 : Set P
hs : Cospherical s
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
⊢ AffineIndependent ℝ p
have rw : ¬Collinear ℝ (Set.range p)
Tactic: rw [affineIndependent_iff_not_collinear]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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
s : Set P
hs : Cospherical s
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
hc : Collinear ℝ (Set.range p)
⊢ False
have hc₁ : ∃ (v : V), ∀ p_1 ∈ Set.range p, ∃ (r : ℝ), p_1 = r • v +ᵥ p 0
Tactic: rw [collinear_iff_of_mem (Set.mem_range_self (0 : Fin 3))] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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 : Set P
hs : Cospherical s
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
hc : ∃ (v : V), ∀ p_1 ∈ Set.range p, ∃ (r : ℝ), p_1 = r • v +ᵥ p 0
⊢ False
have rcases : ∀ (v : V) (hv : ∀ p_1 ∈ Set.range p, ∃ (r : ℝ), p_1 = r • v +ᵥ p 0), False
Tactic: rcases hc with ⟨v, hv⟩
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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
s : Set P
hs : Cospherical s
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
v : V
hv : ∀ p_1 ∈ Set.range p, ∃ (r : ℝ), p_1 = r • v +ᵥ p 0
⊢ False
have hv₁ : ∀ (i : Fin 3), ∃ (r : ℝ), p i = r • v +ᵥ p 0
Tactic: rw [Set.forall_mem_range] at hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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
s : Set P
hs : Cospherical s
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
v : V
hv : ∀ (i : Fin 3), ∃ (r : ℝ), p i = r • v +ᵥ p 0
h : v = 0
⊢ False
have he : p 1 = p 0
Tactic: have he : p 1 = p 0 := by simpa [h] using hv 1
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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
s : Set P
hs : Cospherical s
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
v : V
hv : ∀ (i : Fin 3), ∃ (r : ℝ), p i = r • v +ᵥ p 0
⊢ False
have hv0 : v ≠ 0
Tactic: have hv0 : v ≠ 0 := by
    intro h
    have he : p 1 = p 0 := by simpa [h] using hv 1
    exact (by decide : (1 : Fin 3) ≠ 0) (hpi he)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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 : Set P
hs : Cospherical s
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
v : V
hv : ∀ (i : Fin 3), ∃ (r : ℝ), p i = r • v +ᵥ p 0
hv0 : v ≠ 0
⊢ False
have rcases : ∀ (c : P) (r : ℝ) (hs : ∀ p ∈ s, dist p c = r), False
Tactic: rcases hs with ⟨c, r, hs⟩
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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
s : Set P
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
v : V
hv : ∀ (i : Fin 3), ∃ (r : ℝ), p i = r • v +ᵥ p 0
hv0 : v ≠ 0
c : P
r : ℝ
hs : ∀ p ∈ s, dist p c = r
⊢ False
have hs' : ∀ (i : Fin 3), dist (p i) c = r
Tactic: have hs' := fun i => hs (p i) (Set.mem_of_mem_of_subset (Set.mem_range_self _) hps)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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 : Set P
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
v : V
hv : ∀ (i : Fin 3), ∃ (r : ℝ), p i = r • v +ᵥ p 0
hv0 : v ≠ 0
c : P
r : ℝ
hs : ∀ p ∈ s, dist p c = r
hs' : ∀ (i : Fin 3), dist (p i) c = r
⊢ False
have choose : ∀ (f : (i : Fin 3) → ℝ) (hf : ∀ (i : Fin 3), p i = f i • v +ᵥ p 0), False
Tactic: choose f hf using hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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 : Set P
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
v : V
hv0 : v ≠ 0
c : P
r : ℝ
hs : ∀ p ∈ s, dist p c = r
hs' : ∀ (i : Fin 3), dist (p i) c = r
f : (i : Fin 3) → ℝ
hf : ∀ (i : Fin 3), p i = f i • v +ᵥ p 0
i : Fin 3
⊢ dist (f i • v +ᵥ p 0) c = r
have rw : dist (p i) c = r
Tactic: rw [← hf]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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
s : Set P
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
v : V
hv0 : v ≠ 0
c : P
r : ℝ
hs : ∀ p ∈ s, dist p c = r
hs' : ∀ (i : Fin 3), dist (p i) c = r
f : (i : Fin 3) → ℝ
hf : ∀ (i : Fin 3), p i = f i • v +ᵥ p 0
⊢ False
have hsd : ∀ (i : Fin 3), dist (f i • v +ᵥ p 0) c = r
Tactic: have hsd : ∀ i, dist (f i • v +ᵥ p 0) c = r := by
    intro i
    rw [← hf]
    exact hs' i
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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
s : Set P
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
v : V
hv0 : v ≠ 0
c : P
r : ℝ
hs : ∀ p ∈ s, dist p c = r
hs' : ∀ (i : Fin 3), dist (p i) c = r
f : (i : Fin 3) → ℝ
hf : ∀ (i : Fin 3), p i = f i • v +ᵥ p 0
hsd : ∀ (i : Fin 3), dist (f i • v +ᵥ p 0) c = r
⊢ f 0 = 0
have hf0' : p 0 = f 0 • v +ᵥ p 0
Tactic: have hf0' := hf 0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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
s : Set P
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
v : V
hv0 : v ≠ 0
c : P
r : ℝ
hs : ∀ p ∈ s, dist p c = r
hs' : ∀ (i : Fin 3), dist (p i) c = r
f : (i : Fin 3) → ℝ
hf : ∀ (i : Fin 3), p i = f i • v +ᵥ p 0
hsd : ∀ (i : Fin 3), dist (f i • v +ᵥ p 0) c = r
hf0' : p 0 = f 0 • v +ᵥ p 0
⊢ f 0 = 0
have hf0'₁ : f 0 = 0 ∨ v = 0
Tactic: rw [eq_comm, ← @vsub_eq_zero_iff_eq V, vadd_vsub, smul_eq_zero] at hf0'
Cleared hypotheses: hf0'