awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
as : AffineSubspace ℝ P
h : s.IsTangentAt p as
⊢ s.IsTangent as

Tactic:
⟨p, h⟩

Premises used: Exists.intro, EuclideanGeometry.Sphere.IsTangent
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
⊢ s.IsTangent (s.orthRadius p) ↔ p ∈ s

Tactic:
⟨?_, fun h ↦ (isTangentAt_orthRadius_iff_mem.2 h).isTangent⟩

Premises used: Iff.mpr, EuclideanGeometry.Sphere.isTangentAt_orthRadius_iff_mem, Iff.intro, EuclideanGeometry.Sphere.IsTangentAt.isTangent
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
refine : s.IsTangent (s.orthRadius p) → p ∈ s
⊢ s.IsTangent (s.orthRadius p) ↔ p ∈ s

Tactic:
refine ⟨?_, fun h ↦ (isTangentAt_orthRadius_iff_mem.2 h).isTangent⟩
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
hs : q ∈ s
hsp : Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) q
hle : LE.le (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius q)
⊢ p = q ∨ q = s.center

Tactic:
rw [orthRadius_le_orthRadius_iff] at hle

Premises used: EuclideanGeometry.Sphere.orthRadius_le_orthRadius_iff
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
hs : q ∈ s
hsp : Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) q
hle : p = q ∨ q = s.center
inl : ∀ (hs : p ∈ s) (hsp : Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) p), p ∈ s
inr : ∀ (hs : s.center ∈ s) (hsp : Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) s.center), p ∈ s
⊢ p ∈ s

Tactic:
rcases hle with rfl | rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
hs : p ∈ s
hsp : Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) p
⊢ p ∈ s

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

Tactic:
exact hs
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
hs : s.center ∈ s
hsp : Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) s.center
⊢ p = s.center

Tactic:
rw [center_mem_orthRadius_iff] at hsp

Premises used: EuclideanGeometry.Sphere.center_mem_orthRadius_iff
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
hs : s.center ∈ s
hsp : p = s.center
inr inr₁ inr₂ inr₃ : ∀ (hs : p ∈ s) (hsp : p = s.center), p ∈ s
⊢ p ∈ s

Tactic:
rwa [← hsp] at hs
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
h : s.IsTangent as
p : P
hp : p ∈ as
obtain : ∀ (x : P) (h : s.IsTangentAt x as), s.radius ≤ dist p s.center
⊢ s.radius ≤ dist p s.center

Tactic:
obtain ⟨x, h⟩ := h
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
hp : p ∈ as
x : P
h : s.IsTangentAt x as
⊢ s.radius ≤ dist p s.center

Tactic:
le_of_sq_le_sq ?_ dist_nonneg

Premises used: dist_nonneg, le_of_sq_le_sq
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
hp : p ∈ as
x : P
h : s.IsTangentAt x as
refine : HPow.hPow (β := ℕ) s.radius 2 ≤ HPow.hPow (β := ℕ) (dist p s.center) 2
⊢ s.radius ≤ dist p s.center

Tactic:
refine le_of_sq_le_sq ?_ dist_nonneg

Premises used: dist_nonneg, le_of_sq_le_sq
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
hp : p ∈ as
x : P
h : s.IsTangentAt x as
rw : 0 ≤ HPow.hPow (β := ℕ) (dist p x) 2
⊢ HPow.hPow (β := ℕ) s.radius 2 ≤ HPow.hPow (β := ℕ) (dist p s.center) 2

Tactic:
rw [h.dist_sq_eq_of_mem hp, le_add_iff_nonneg_right]

Premises used: le_add_iff_nonneg_right, EuclideanGeometry.Sphere.IsTangentAt.dist_sq_eq_of_mem
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
hp : p ∈ as
x : P
h : s.IsTangentAt x as
⊢ 0 ≤ HPow.hPow (β := ℕ) (dist p x) 2

Tactic:
sq_nonneg _

Premises used: sq_nonneg
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
hp : p ∈ as
x : P
h : s.IsTangentAt x as
⊢ 0 ≤ HPow.hPow (β := ℕ) (dist p x) 2

Tactic:
exact sq_nonneg _

Premises used: sq_nonneg
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
h : s.IsTangent as
p : P
hp : dist p s.center < s.radius
contrapose! : ∀ (hp : p ∈ as), s.radius ≤ dist p s.center
⊢ p ∉ as

Tactic:
contrapose! hp
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
h : s.IsTangent as
p : P
hp : p ∈ as
⊢ s.radius ≤ dist p s.center

Tactic:
h.radius_le_dist_center hp

Premises used: EuclideanGeometry.Sphere.IsTangent.radius_le_dist_center
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
h : s.IsTangent as
p : P
hp : p ∈ as
⊢ s.radius ≤ dist p s.center

Tactic:
exact h.radius_le_dist_center hp

Premises used: EuclideanGeometry.Sphere.IsTangent.radius_le_dist_center
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
h : s.IsTangent as
obtain : ∀ (p : P) (h : s.IsTangentAt p as), Metric.infDist s.center (↑as : Set P) = s.radius
⊢ Metric.infDist s.center (↑as : Set P) = s.radius

Tactic:
obtain ⟨p, h⟩ := h
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
refine_2 : s.radius ≤ Metric.infDist s.center (↑as : Set P)
⊢ Metric.infDist s.center (↑as : Set P) = s.radius

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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) ≤ dist s.center p

Tactic:
Metric.infDist_le_dist_of_mem h.mem_space

Premises used: Metric.infDist_le_dist_of_mem, EuclideanGeometry.Sphere.IsTangentAt.mem_space
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
h₁ : s.radius = dist s.center p
⊢ Metric.infDist s.center (↑as : Set P) ≤ s.radius

Tactic:
convert! Metric.infDist_le_dist_of_mem h.mem_space

Premises used: Metric.infDist_le_dist_of_mem, EuclideanGeometry.Sphere.IsTangentAt.mem_space
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
h₁ h₂ : s.radius = s.radius
⊢ s.radius = dist s.center p

Tactic:
rw [mem_sphere'.1 h.mem_sphere]

Premises used: EuclideanGeometry.mem_sphere', EuclideanGeometry.Sphere.IsTangentAt.mem_sphere, Iff.mp
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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_2 : s.radius ≤ ⨅ (y : (↑(↑as : Set P) : Type u_2)), dist s.center (↑y : P)
⊢ s.radius ≤ Metric.infDist s.center (↑as : Set P)

Tactic:
rw [Metric.infDist_eq_iInf]

Premises used: Metric.infDist_eq_iInf
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
⊢ Nonempty.{u_2 + 1} ↥as

Tactic:
have : Nonempty as := ⟨⟨p, h.mem_space⟩⟩
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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)

Tactic:
le_ciInf fun x ↦ ?_

Premises used: le_ciInf
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
refine_2 : ∀ (x : (↑(↑as : Set P) : Type u_2)), s.radius ≤ dist s.center (↑x : P)
⊢ s.radius ≤ ⨅ (y : (↑(↑as : Set P) : Type u_2)), dist s.center (↑y : P)

Tactic:
refine le_ciInf fun x ↦ ?_

Premises used: le_ciInf
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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)
refine_2 : s.radius ≤ dist (↑x : P) s.center
⊢ s.radius ≤ dist s.center (↑x : P)

Tactic:
rw [dist_comm]

Premises used: dist_comm
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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 (↑x : P) s.center

Tactic:
h.isTangent.radius_le_dist_center x.property

Premises used: EuclideanGeometry.Sphere.IsTangent.radius_le_dist_center, EuclideanGeometry.Sphere.IsTangentAt.isTangent, Subtype.property
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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 (↑x : P) s.center

Tactic:
exact h.isTangent.radius_le_dist_center x.property

Premises used: EuclideanGeometry.Sphere.IsTangent.radius_le_dist_center, EuclideanGeometry.Sphere.IsTangentAt.isTangent, Subtype.property
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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

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

Premises used: Iff.intro
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
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
⊢ 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 ↦ ?_⟩
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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

Tactic:
⟨?_, orthogonalProjection_mem _, fun p hp ↦ ?_⟩

Premises used: EuclideanGeometry.orthogonalProjection_mem, EuclideanGeometry.Sphere.IsTangentAt.mk
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
refine_1₁ :
  ∀ (p : P) (hp : p ∈ as),
    Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P))
      p
⊢ s.IsTangentAt (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) as

Tactic:
refine ⟨?_, orthogonalProjection_mem _, fun p hp ↦ ?_⟩
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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 refine_1 refine_1₁ refine_1₂ refine_1₃ :
  dist s.center (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) = s.radius
⊢ (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) ∈ s

Tactic:
rwa [mem_sphere']

Premises used: EuclideanGeometry.mem_sphere'
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
refine_1 :
  ⟪p -ᵥ (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P),
      (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) -ᵥ s.center⟫ =
    0
⊢ Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P)) p

Tactic:
rw [mem_orthRadius_iff_inner_left]

Premises used: EuclideanGeometry.Sphere.mem_orthRadius_iff_inner_left
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
⊢ ⟪p -ᵥ (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P),
      (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) -ᵥ s.center⟫ =
    0

Tactic:
orthogonalProjection_vsub_mem_direction_orthogonal as s.center _
        (vsub_orthogonalProjection_mem_direction s.center hp)

Premises used: EuclideanGeometry.Sphere.center, EuclideanGeometry.vsub_orthogonalProjection_mem_direction, EuclideanGeometry.orthogonalProjection_vsub_mem_direction_orthogonal
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
⊢ ⟪p -ᵥ (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P),
      (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) -ᵥ s.center⟫ =
    0

Tactic:
exact orthogonalProjection_vsub_mem_direction_orthogonal as s.center _
        (vsub_orthogonalProjection_mem_direction s.center hp)

Premises used: EuclideanGeometry.Sphere.center, EuclideanGeometry.vsub_orthogonalProjection_mem_direction, EuclideanGeometry.orthogonalProjection_vsub_mem_direction_orthogonal
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
refine_2₁ refine_2₂ : s.radius = s.radius
⊢ dist s.center (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) = s.radius

Tactic:
rw [dist_orthogonalProjection_eq_infDist, h.isTangent.infDist_eq_radius]

Premises used: EuclideanGeometry.Sphere.IsTangent.infDist_eq_radius, EuclideanGeometry.dist_orthogonalProjection_eq_infDist, EuclideanGeometry.Sphere.IsTangentAt.isTangent
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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

Tactic:
⟨fun h ↦ (dist_orthogonalProjection_eq_radius_iff_isTangentAt.1 h).isTangent, fun h ↦ ?_⟩

Premises used: Iff.intro, Iff.mp, EuclideanGeometry.Sphere.IsTangentAt.isTangent, EuclideanGeometry.Sphere.dist_orthogonalProjection_eq_radius_iff_isTangentAt
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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 : ∀ (h : s.IsTangent as), dist s.center (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) = s.radius
⊢ dist s.center (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) = s.radius ↔ s.IsTangent as

Tactic:
refine ⟨fun h ↦ (dist_orthogonalProjection_eq_radius_iff_isTangentAt.1 h).isTangent, fun h ↦ ?_⟩
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
rw₁ rw₂ : s.radius = s.radius
⊢ dist s.center (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) = s.radius

Tactic:
rw [dist_orthogonalProjection_eq_infDist, h.infDist_eq_radius]

Premises used: EuclideanGeometry.Sphere.IsTangent.infDist_eq_radius, EuclideanGeometry.dist_orthogonalProjection_eq_infDist
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
rw₁ rw₂ : s.IsTangent as ↔ s.IsTangent as
⊢ Metric.infDist s.center (↑as : Set P) = s.radius ↔ s.IsTangent as

Tactic:
rw [← dist_orthogonalProjection_eq_infDist, dist_orthogonalProjection_eq_radius_iff_isTangent]

Premises used: EuclideanGeometry.Sphere.dist_orthogonalProjection_eq_radius_iff_isTangent, EuclideanGeometry.dist_orthogonalProjection_eq_infDist
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
rw₁ rw₂ :
  s.IsTangentAt (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) as ↔
    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

Tactic:
rw [← dist_orthogonalProjection_eq_radius_iff_isTangent,
    dist_orthogonalProjection_eq_radius_iff_isTangentAt]

Premises used: EuclideanGeometry.Sphere.dist_orthogonalProjection_eq_radius_iff_isTangent, EuclideanGeometry.Sphere.dist_orthogonalProjection_eq_radius_iff_isTangentAt