awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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 : Sphere P
as : AffineSubspace ℝ P
p : P
h : s.IsTangentAt p as
refine_1 : Metric.infDist s.center (↑as : Set P) ≤ s.radius
⊢ Metric.infDist s.center (↑as : Set P) = s.radius
have refine_2 : s.radius ≤ Metric.infDist s.center (↑as : Set P)
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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 : Sphere P
as : AffineSubspace ℝ P
p : P
h : s.IsTangentAt p as
⊢ Metric.infDist s.center (↑as : Set P) ≤ s.radius
have h₁ : s.radius = dist s.center p
Tactic: convert! Metric.infDist_le_dist_of_mem h.mem_space
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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 : Sphere P
as : AffineSubspace ℝ P
p : P
h : s.IsTangentAt p as
⊢ s.radius = dist s.center p
have h₁ : s.radius = s.radius
Tactic: rw [mem_sphere'.1 h.mem_sphere]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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 : Sphere P
as : AffineSubspace ℝ P
p : P
h : s.IsTangentAt p as
⊢ s.radius ≤ Metric.infDist s.center (↑as : Set P)
have refine_2 : s.radius ≤ ⨅ (y : (↑(↑as : Set P) : Type u_2)), dist s.center (↑y : P)
Tactic: rw [Metric.infDist_eq_iInf]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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 : Sphere P
as : AffineSubspace ℝ P
p : P
h : s.IsTangentAt p as
⊢ s.radius ≤ ⨅ (y : (↑(↑as : Set P) : Type u_2)), dist s.center (↑y : P)
have this : Nonempty.{u_2 + 1} ↥as
Tactic: have : Nonempty as := ⟨⟨p, h.mem_space⟩⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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 : Sphere P
as : AffineSubspace ℝ P
p : P
h : s.IsTangentAt p as
this : Nonempty.{u_2 + 1} ↥as
⊢ s.radius ≤ ⨅ (y : (↑(↑as : Set P) : Type u_2)), dist s.center (↑y : P)
have refine_2 : ∀ (x : (↑(↑as : Set P) : Type u_2)), s.radius ≤ dist s.center (↑x : P)
Tactic: refine le_ciInf fun x ↦ ?_
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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 : Sphere P
as : AffineSubspace ℝ P
p : P
h : s.IsTangentAt p as
this : Nonempty.{u_2 + 1} ↥as
x : (↑(↑as : Set P) : Type u_2)
⊢ s.radius ≤ dist s.center (↑x : P)
have refine_2 : s.radius ≤ dist (↑x : P) s.center
Tactic: rw [dist_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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 : Sphere P
as : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥as
inst_5 : as.direction.HasOrthogonalProjection
⊢ dist s.center (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) = s.radius ↔
    s.IsTangentAt (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) as
have refine_1 : ∀ (h : dist s.center (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) = s.radius),
  s.IsTangentAt (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) as
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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 : Sphere P
as : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥as
inst_5 : as.direction.HasOrthogonalProjection
refine_1 :
  ∀ (h : dist s.center (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) = s.radius),
    s.IsTangentAt (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) as
⊢ dist s.center (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) = s.radius ↔
    s.IsTangentAt (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) as
have refine_2 : ∀ (h : s.IsTangentAt (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) as),
  dist s.center (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) = s.radius
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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 : Sphere P
as : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥as
inst_5 : as.direction.HasOrthogonalProjection
h : dist s.center (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) = s.radius
⊢ s.IsTangentAt (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) as
have refine_1 : (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) ∈ s
Tactic: refine ⟨?_, orthogonalProjection_mem _, fun p hp ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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 : Sphere P
as : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥as
inst_5 : as.direction.HasOrthogonalProjection
h : dist s.center (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) = s.radius
refine_1 : (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) ∈ s
⊢ s.IsTangentAt (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) as
have refine_1₁ : ∀ (p : P) (hp : p ∈ as),
  Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P)) p
Tactic: refine ⟨?_, orthogonalProjection_mem _, fun p hp ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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 : Sphere P
as : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥as
inst_5 : as.direction.HasOrthogonalProjection
h : dist s.center (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) = s.radius
p : P
hp : p ∈ as
⊢ Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P)) p
have refine_1 : ⟪p -ᵥ (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P),
    (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) -ᵥ s.center⟫ =
  0
Tactic: rw [mem_orthRadius_iff_inner_left]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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 : Sphere P
as : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥as
inst_5 : as.direction.HasOrthogonalProjection
h : s.IsTangentAt (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) as
⊢ dist s.center (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) = s.radius
have refine_2 : Metric.infDist s.center (↑as : Set P) = s.radius
Tactic: rw [dist_orthogonalProjection_eq_infDist, h.isTangent.infDist_eq_radius]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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 : Sphere P
as : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥as
inst_5 : as.direction.HasOrthogonalProjection
h : s.IsTangentAt (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) as
refine_2 : Metric.infDist s.center (↑as : Set P) = s.radius
⊢ dist s.center (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) = s.radius
have refine_2₁ : s.radius = s.radius
Tactic: rw [dist_orthogonalProjection_eq_infDist, h.isTangent.infDist_eq_radius]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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 : Sphere P
as : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥as
inst_5 : as.direction.HasOrthogonalProjection
⊢ dist s.center (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) = s.radius ↔ s.IsTangent as
have refine : ∀ (h : s.IsTangent as), dist s.center (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) = s.radius
Tactic: refine ⟨fun h ↦ (dist_orthogonalProjection_eq_radius_iff_isTangentAt.1 h).isTangent, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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 : Sphere P
as : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥as
inst_5 : as.direction.HasOrthogonalProjection
h : s.IsTangent as
⊢ dist s.center (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) = s.radius
have rw : Metric.infDist s.center (↑as : Set P) = s.radius
Tactic: rw [dist_orthogonalProjection_eq_infDist, h.infDist_eq_radius]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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 : Sphere P
as : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥as
inst_5 : as.direction.HasOrthogonalProjection
h : s.IsTangent as
rw : Metric.infDist s.center (↑as : Set P) = s.radius
⊢ dist s.center (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) = s.radius
have rw₁ : s.radius = s.radius
Tactic: rw [dist_orthogonalProjection_eq_infDist, h.infDist_eq_radius]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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 : Sphere P
as : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥as
inst_5 : as.direction.HasOrthogonalProjection
⊢ Metric.infDist s.center (↑as : Set P) = s.radius ↔ s.IsTangent as
have rw : dist s.center (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) = s.radius ↔ s.IsTangent as
Tactic: rw [← dist_orthogonalProjection_eq_infDist, dist_orthogonalProjection_eq_radius_iff_isTangent]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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 : Sphere P
as : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥as
inst_5 : as.direction.HasOrthogonalProjection
rw : dist s.center (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) = s.radius ↔ s.IsTangent as
⊢ Metric.infDist s.center (↑as : Set P) = s.radius ↔ s.IsTangent as
have rw₁ : s.IsTangent as ↔ s.IsTangent as
Tactic: rw [← dist_orthogonalProjection_eq_infDist, dist_orthogonalProjection_eq_radius_iff_isTangent]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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 : Sphere P
as : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥as
inst_5 : as.direction.HasOrthogonalProjection
⊢ s.IsTangent as ↔ s.IsTangentAt (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) as
have rw : dist s.center (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) = s.radius ↔
  s.IsTangentAt (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) as
Tactic: rw [← dist_orthogonalProjection_eq_radius_iff_isTangent,
    dist_orthogonalProjection_eq_radius_iff_isTangentAt]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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 : Sphere P
as : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥as
inst_5 : as.direction.HasOrthogonalProjection
rw :
  dist s.center (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) = s.radius ↔
    s.IsTangentAt (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) as
⊢ s.IsTangent as ↔ s.IsTangentAt (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) as
have rw₁ : s.IsTangentAt (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) as ↔
  s.IsTangentAt (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) as
Tactic: rw [← dist_orthogonalProjection_eq_radius_iff_isTangent,
    dist_orthogonalProjection_eq_radius_iff_isTangentAt]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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 : Sphere P
as : AffineSubspace ℝ P
p : P
h : s.IsTangent as
hpar : as ∥ s.orthRadius p
hp : p ∈ s
⊢ as = s.orthRadius p ∨ as = s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p)
have rcases : ∀ (q : P) (hqs : q ∈ s) (hqas : q ∈ as) (hqo : as ≤ s.orthRadius q),
  as = s.orthRadius p ∨ as = s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p)
Tactic: rcases h with ⟨q, hqs, hqas, hqo⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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 : Sphere P
as : AffineSubspace ℝ P
p : P
hpar : as ∥ s.orthRadius p
hp : p ∈ s
q : P
hqs : q ∈ s
hqas : q ∈ as
hqo : as ≤ s.orthRadius q
⊢ as = s.orthRadius p ∨ as = s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p)
have hd : as.direction ≤ direction (s.orthRadius q)
Tactic: have hd := direction_le hqo
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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 : Sphere P
as : AffineSubspace ℝ P
p : P
hpar : as ∥ s.orthRadius p
hp : p ∈ s
q : P
hqs : q ∈ s
hqas : q ∈ as
hqo : as ≤ s.orthRadius q
hd : as.direction ≤ direction (s.orthRadius q)
⊢ as = s.orthRadius p ∨ as = s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p)
have hd₁ : ∃ (r : ℝ), q -ᵥ s.center = r • (p -ᵥ s.center)
Tactic: rw [hpar.direction_eq, direction_orthRadius_le_iff] at hd
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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 : Sphere P
as : AffineSubspace ℝ P
p : P
hpar : as ∥ s.orthRadius p
hp : p ∈ s
q : P
hqs : q ∈ s
hqas : q ∈ as
hqo : as ≤ s.orthRadius q
hd : ∃ (r : ℝ), q -ᵥ s.center = r • (p -ᵥ s.center)
⊢ as = s.orthRadius p ∨ as = s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p)
have obtain : ∀ (r : ℝ) (hr : q -ᵥ s.center = r • (p -ᵥ s.center)),
  as = s.orthRadius p ∨ as = s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p)
Tactic: obtain ⟨r, hr⟩ := hd
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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 : Sphere P
as : AffineSubspace ℝ P
p : P
hpar : as ∥ s.orthRadius p
hp : p ∈ s
q : P
hqs : q ∈ s
hqas : q ∈ as
hqo : as ≤ s.orthRadius q
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
⊢ as = s.orthRadius p ∨ as = s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p)
have inl : ∀ (hrad : s.radius = 0), as = s.orthRadius p ∨ as = s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p)
Tactic: rcases eq_or_ne s.radius 0 with hrad | hrad
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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 : Sphere P
as : AffineSubspace ℝ P
p : P
hpar : as ∥ s.orthRadius p
hp : p ∈ s
q : P
hqs : q ∈ s
hqas : q ∈ as
hqo : as ≤ s.orthRadius q
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
inl :
  ∀ (hrad : s.radius = 0), as = s.orthRadius p ∨ as = s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p)
⊢ as = s.orthRadius p ∨ as = s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p)
have inr : ∀ (hrad : s.radius ≠ 0), as = s.orthRadius p ∨ as = s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p)
Tactic: rcases eq_or_ne s.radius 0 with hrad | hrad
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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 : Sphere P
as : AffineSubspace ℝ P
p : P
hpar : as ∥ s.orthRadius p
hp : p ∈ s
q : P
hqs : q ∈ s
hqas : q ∈ as
hqo : as ≤ s.orthRadius q
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
hrad : s.radius = 0
⊢ as = s.orthRadius p ∨ as = s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p)
have inl : ∀ (hp : p = s.center) (q : P) (hqs : q = s.center) (hqas : q ∈ as) (hqo : as ≤ s.orthRadius q) (r : ℝ)
  (hr : q -ᵥ s.center = r • (p -ᵥ s.center)) (hrad : s.radius = 0),
  as = s.orthRadius p ∨ as = s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p)
Tactic: rw [mem_sphere, hrad, dist_eq_zero] at hp hqs
Cleared hypotheses: hp, q, hqs, hqas, hqo, r, hr, hrad
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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 : Sphere P
as : AffineSubspace ℝ P
p : P
hpar : as ∥ s.orthRadius p
hp : p = s.center
q : P
hqs : q = s.center
hqas : q ∈ as
hqo : as ≤ s.orthRadius q
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
hrad : s.radius = 0
⊢ as = s.orthRadius p ∨ as = s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p)
have inl : ∀ (hpar : as ∥ ⊤) (hp : p = s.center) (q : P) (hqs : q = s.center) (hqas : q ∈ as) (hqo : as ≤ s.orthRadius q) (r : ℝ)
  (hr : q -ᵥ s.center = r • (p -ᵥ s.center)) (hrad : s.radius = 0),
  as = ⊤ ∨ as = s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) s.center)
Tactic: rw [hp, orthRadius_center] at hpar ⊢
Cleared hypotheses: hpar, hp, q, hqs, hqas, hqo, r, hr, hrad
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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 : Sphere P
as : AffineSubspace ℝ P
p : P
hpar : as ∥ ⊤
hp : p = s.center
q : P
hqs : q = s.center
hqas : q ∈ as
hqo : as ≤ s.orthRadius q
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
hrad : s.radius = 0
⊢ as = ⊤ ∨ as = s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) s.center)
have inl : ∀ (hqo : as ≤ ⊤) (r : ℝ) (hr : q -ᵥ s.center = r • (p -ᵥ s.center)) (hrad : s.radius = 0),
  as = ⊤ ∨ as = s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) s.center)
Tactic: rw [hqs, orthRadius_center] at hqo
Cleared hypotheses: hqo, r, hr, hrad
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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 : Sphere P
as : AffineSubspace ℝ P
p : P
hpar : as ∥ s.orthRadius p
hp : p ∈ s
q : P
hqs : q ∈ s
hqas : q ∈ as
hqo : as ≤ s.orthRadius q
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
hrad : s.radius ≠ 0
⊢ as = s.orthRadius q
have refine : as.direction = direction (s.orthRadius q)
Tactic: refine eq_of_direction_eq_of_nonempty_of_le ?_ ⟨q, hqas⟩ hqo
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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 : Sphere P
as : AffineSubspace ℝ P
p : P
hpar : as ∥ s.orthRadius p
hp : p ∈ s
q : P
hqs : q ∈ s
hqas : q ∈ as
hqo : as ≤ s.orthRadius q
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
hrad : s.radius ≠ 0
⊢ as.direction = direction (s.orthRadius q)
have rw : Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (ℝ ∙ (q -ᵥ s.center))ᗮ
Tactic: rw [hpar.direction_eq, direction_orthRadius, direction_orthRadius]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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 : Sphere P
as : AffineSubspace ℝ P
p : P
hpar : as ∥ s.orthRadius p
hp : p ∈ s
q : P
hqs : q ∈ s
hqas : q ∈ as
hqo : as ≤ s.orthRadius q
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
hrad : s.radius ≠ 0
⊢ Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (ℝ ∙ (q -ᵥ s.center))ᗮ
have e_K : Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) (ℝ ∙ (q -ᵥ s.center))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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 : Sphere P
as : AffineSubspace ℝ P
p : P
hpar : as ∥ s.orthRadius p
hp : p ∈ s
q : P
hqs : q ∈ s
hqas : q ∈ as
hqo : as ≤ s.orthRadius q
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
hrad : s.radius ≠ 0
⊢ Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) (ℝ ∙ (q -ᵥ s.center))
have e_K : ∀ (hr : q -ᵥ s.center = HSMul.hSMul (α := ℝ) 0 (p -ᵥ s.center)),
  Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) (ℝ ∙ (q -ᵥ s.center))
Tactic: rcases eq_or_ne r 0 with rfl | hr0
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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 : Sphere P
as : AffineSubspace ℝ P
p : P
hpar : as ∥ s.orthRadius p
hp : p ∈ s
q : P
hqs : q ∈ s
hqas : q ∈ as
hqo : as ≤ s.orthRadius q
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
hrad : s.radius ≠ 0
e_K :
  ∀ (hr : q -ᵥ s.center = HSMul.hSMul (α := ℝ) 0 (p -ᵥ s.center)),
    Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) (ℝ ∙ (q -ᵥ s.center))
⊢ Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) (ℝ ∙ (q -ᵥ s.center))
have e_K₁ : ∀ (hr0 : r ≠ 0), Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) (ℝ ∙ (q -ᵥ s.center))
Tactic: rcases eq_or_ne r 0 with rfl | hr0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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 : Sphere P
as : AffineSubspace ℝ P
p : P
hpar : as ∥ s.orthRadius p
hp : p ∈ s
q : P
hqs : q ∈ s
hqas : q ∈ as
hqo : as ≤ s.orthRadius q
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
hrad : s.radius ≠ 0
hr0 : r ≠ 0
⊢ Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) (ℝ ∙ (q -ᵥ s.center))
have e_K : Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) (ℝ ∙ r • (p -ᵥ s.center))
Tactic: rw [hr, Submodule.span_singleton_smul_eq hr0.isUnit]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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 : Sphere P
as : AffineSubspace ℝ P
p : P
hpar : as ∥ s.orthRadius p
hp : p ∈ s
q : P
hqs : q ∈ s
hqas : q ∈ as
hqo : as ≤ s.orthRadius q
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
hrad : s.radius ≠ 0
hr0 : r ≠ 0
e_K : Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) (ℝ ∙ r • (p -ᵥ s.center))
⊢ Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) (ℝ ∙ (q -ᵥ s.center))
have e_K₁ : Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) (ℝ ∙ (p -ᵥ s.center))
Tactic: rw [hr, Submodule.span_singleton_smul_eq hr0.isUnit]