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
hp : p ∈ s
q : P
hqs : q ∈ s
hrad : s.radius ≠ 0
hpar : s.orthRadius q ∥ s.orthRadius p
hqas : Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius q) q
hqo : LE.le (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius q)
hr : q = HSMul.hSMul (α := ℝ) (-1) (p -ᵥ s.center) +ᵥ s.center
hr0 : Ne (α := ℝ) (-1) 0
hr' : Eq (α := ℝ) |(-1)| 1
⊢ (Equiv.pointReflection s.center : (a : P) → P) p = HSMul.hSMul (α := ℝ) (-1) (p -ᵥ s.center) +ᵥ s.center

Tactic:
simp [Equiv.pointReflection_apply]

Premises used: Equiv.pointReflection_apply
-- 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
inst_4 : Nonempty.{u_2 + 1} ↥as
inst_5 : as.direction.HasOrthogonalProjection
h : s.IsTangentAt p as
⊢ p = (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P)

Tactic:
h.eq_of_isTangentAt ?_

Premises used: EuclideanGeometry.Sphere.IsTangentAt.eq_of_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
p : P
as : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥as
inst_5 : as.direction.HasOrthogonalProjection
h : s.IsTangentAt p as
refine : s.IsTangentAt (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) as
⊢ p = (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P)

Tactic:
refine h.eq_of_isTangentAt ?_

Premises used: EuclideanGeometry.Sphere.IsTangentAt.eq_of_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
p : P
as : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥as
inst_5 : as.direction.HasOrthogonalProjection
h : s.IsTangentAt p as
⊢ s.IsTangent as

Tactic:
have h' := 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 : P
as : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥as
inst_5 : as.direction.HasOrthogonalProjection
h : s.IsTangentAt p as
h' : s.IsTangent as
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (h' : s.IsTangentAt (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) as),
    s.IsTangentAt (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) as
⊢ s.IsTangentAt (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) as

Tactic:
rwa [isTangent_iff_isTangentAt_orthogonalProjection] at h'

Premises used: EuclideanGeometry.Sphere.isTangent_iff_isTangentAt_orthogonalProjection
-- 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
as : AffineSubspace ℝ P
s : Sphere P
⊢ Membership.mem (γ := Set (AffineSubspace ℝ P)) s.tangentSet as ↔ ∃ p ∈ s, s.orthRadius p = as

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, EuclideanGeometry.Sphere.tangentSet, Set.image
-- 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
as : AffineSubspace ℝ P
s : Sphere P
h : Membership.mem (γ := Set (AffineSubspace ℝ P)) s.tangentSet as
rcases : ∀ (p : P) (hps : p ∈ Metric.sphere s.center s.radius), s.IsTangent (s.orthRadius p)
⊢ s.IsTangent as

Tactic:
rcases h with ⟨p, hps, 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
hps : p ∈ Metric.sphere s.center s.radius
⊢ s.IsTangent (s.orthRadius p)

Tactic:
isTangent_orthRadius_iff_mem.2 hps

Premises used: Iff.mpr, EuclideanGeometry.Sphere.isTangent_orthRadius_iff_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
p : P
hps : p ∈ Metric.sphere s.center s.radius
⊢ s.IsTangent (s.orthRadius p)

Tactic:
exact isTangent_orthRadius_iff_mem.2 hps

Premises used: Iff.mpr, EuclideanGeometry.Sphere.isTangent_orthRadius_iff_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
as : AffineSubspace ℝ P
s : Sphere P
p : P
⊢ Membership.mem (γ := Set (AffineSubspace ℝ P)) (s.tangentsFrom p) as ↔
    Membership.mem (γ := Set (AffineSubspace ℝ P)) s.tangentSet as ∧ p ∈ as

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, EuclideanGeometry.Sphere.tangentsFrom
-- 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
as : AffineSubspace ℝ P
s : Sphere P
p : P
h : Membership.mem (γ := Set (AffineSubspace ℝ P)) (s.tangentsFrom p) as
⊢ Membership.mem (γ := Set (AffineSubspace ℝ P)) s.tangentSet as

Tactic:
h.1

Premises used: And.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
as : AffineSubspace ℝ P
s : Sphere P
p : P
h : Membership.mem (γ := Set (AffineSubspace ℝ P)) (s.tangentsFrom p) as
⊢ p ∈ as

Tactic:
h.2

Premises used: And.right
-- 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
as : AffineSubspace ℝ P
s : Sphere P
p : P
h : Membership.mem (γ := Set (AffineSubspace ℝ P)) (s.tangentsFrom p) as
⊢ s.IsTangent as

Tactic:
isTangent_of_mem_tangentSet h.1

Premises used: EuclideanGeometry.Sphere.isTangent_of_mem_tangentSet, And.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
as : AffineSubspace ℝ P
s₁ s₂ : Sphere P
⊢ Membership.mem (γ := Set (AffineSubspace ℝ P)) (s₁.commonTangents s₂) as ↔
    Membership.mem (γ := Set (AffineSubspace ℝ P)) s₁.tangentSet as ∧
      Membership.mem (γ := Set (AffineSubspace ℝ P)) s₂.tangentSet as

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.inter, EuclideanGeometry.Sphere.commonTangents
-- 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₁ s₂ : Sphere P
⊢ Eq (α := Set (AffineSubspace ℝ P)) (s₁.commonTangents s₂) (s₂.commonTangents s₁)

Tactic:
Set.inter_comm _ _

Premises used: Set.inter_comm, EuclideanGeometry.Sphere.commonTangents
-- 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
as : AffineSubspace ℝ P
s₁ s₂ : Sphere P
⊢ Membership.mem (γ := Set (AffineSubspace ℝ P)) (s₁.commonIntTangents s₂) as ↔
    Membership.mem (γ := Set (AffineSubspace ℝ P)) (s₁.commonTangents s₂) as ∧ ∃ p ∈ as, Wbtw ℝ s₁.center p s₂.center

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, EuclideanGeometry.Sphere.commonIntTangents
-- 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
as : AffineSubspace ℝ P
s₁ s₂ : Sphere P
⊢ Membership.mem (γ := Set (AffineSubspace ℝ P)) (s₁.commonExtTangents s₂) as ↔
    Membership.mem (γ := Set (AffineSubspace ℝ P)) (s₁.commonTangents s₂) as ∧ ∀ p ∈ as, ¬Sbtw ℝ s₁.center p s₂.center

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, EuclideanGeometry.Sphere.commonExtTangents
-- 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₁ s₂ : Sphere P
h :
  ∀ (as : AffineSubspace ℝ P),
    Membership.mem (γ := Set (AffineSubspace ℝ P)) (s₁.commonIntTangents s₂ ∪ s₁.commonExtTangents s₂) as ↔
      Membership.mem (γ := Set (AffineSubspace ℝ P)) (s₁.commonTangents s₂) as
⊢ Eq (α := Set (AffineSubspace ℝ P)) (s₁.commonIntTangents s₂ ∪ s₁.commonExtTangents s₂) (s₁.commonTangents s₂)

Tactic:
ext as
-- 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₁ s₂ : Sphere P
as : AffineSubspace ℝ P
h :
  Membership.mem (γ := Set (AffineSubspace ℝ P)) (s₁.commonTangents s₂) as →
    (∃ p ∈ as, Wbtw ℝ s₁.center p s₂.center) ∨ ∀ p ∈ as, ¬Sbtw ℝ s₁.center p s₂.center
⊢ Membership.mem (γ := Set (AffineSubspace ℝ P)) (s₁.commonIntTangents s₂ ∪ s₁.commonExtTangents s₂) as ↔
    Membership.mem (γ := Set (AffineSubspace ℝ P)) (s₁.commonTangents s₂) as

Tactic:
rw [Set.mem_union, mem_commonIntTangents_iff, mem_commonExtTangents_iff, ← and_or_left,
    and_iff_left_iff_imp]

Premises used: Set.mem_union, and_or_left, EuclideanGeometry.Sphere.mem_commonExtTangents_iff, EuclideanGeometry.Sphere.mem_commonIntTangents_iff, and_iff_left_iff_imp
-- 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₁ s₂ : Sphere P
as : AffineSubspace ℝ P
pos :
  ∀ (h : ∃ p ∈ as, Wbtw ℝ s₁.center p s₂.center),
    (∃ p ∈ as, Wbtw ℝ s₁.center p s₂.center) ∨ ∀ p ∈ as, ¬Sbtw ℝ s₁.center p s₂.center
neg :
  ∀ (h : ∀ (p : P) (_ : p ∈ as), ¬Wbtw ℝ s₁.center p s₂.center),
    (∃ p ∈ as, Wbtw ℝ s₁.center p s₂.center) ∨ ∀ p ∈ as, ¬Sbtw ℝ s₁.center p s₂.center
⊢ (∃ p ∈ as, Wbtw ℝ s₁.center p s₂.center) ∨ ∀ p ∈ as, ¬Sbtw ℝ s₁.center p s₂.center

Tactic:
by_cases! h : ∃ p ∈ as, Wbtw ℝ s₁.center p s₂.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₁ s₂ : Sphere P
as : AffineSubspace ℝ P
h : ∃ p ∈ as, Wbtw ℝ s₁.center p s₂.center
⊢ (∃ p ∈ as, Wbtw ℝ s₁.center p s₂.center) ∨ ∀ p ∈ as, ¬Sbtw ℝ s₁.center p s₂.center

Tactic:
.inl h

Premises used: Or.inl
-- 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₁ s₂ : Sphere P
as : AffineSubspace ℝ P
h : ∃ p ∈ as, Wbtw ℝ s₁.center p s₂.center
⊢ (∃ p ∈ as, Wbtw ℝ s₁.center p s₂.center) ∨ ∀ p ∈ as, ¬Sbtw ℝ s₁.center p s₂.center

Tactic:
exact .inl 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₁ s₂ : Sphere P
as : AffineSubspace ℝ P
h : ∀ (p : P) (_ : p ∈ as), ¬Wbtw ℝ s₁.center p s₂.center
⊢ (∃ p ∈ as, Wbtw ℝ s₁.center p s₂.center) ∨ ∀ p ∈ as, ¬Sbtw ℝ s₁.center p s₂.center

Tactic:
.inr ?_

Premises used: Or.inr
-- 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₁ s₂ : Sphere P
as : AffineSubspace ℝ P
h : ∀ (p : P) (_ : p ∈ as), ¬Wbtw ℝ s₁.center p s₂.center
neg : ∀ p ∈ as, ¬Sbtw ℝ s₁.center p s₂.center
⊢ (∃ p ∈ as, Wbtw ℝ s₁.center p s₂.center) ∨ ∀ p ∈ as, ¬Sbtw ℝ s₁.center p s₂.center

Tactic:
refine .inr ?_
-- 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₁ s₂ : Sphere P
as : AffineSubspace ℝ P
h : ∀ (p : P) (_ : p ∈ as), ¬Wbtw ℝ s₁.center p s₂.center
p : P
hp : p ∈ as
⊢ ¬Sbtw ℝ s₁.center p s₂.center

Tactic:
mt Sbtw.wbtw (h p hp)

Premises used: mt, Sbtw.wbtw
-- 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₁ s₂ : Sphere P
as : AffineSubspace ℝ P
h : ∀ (p : P) (_ : p ∈ as), ¬Wbtw ℝ s₁.center p s₂.center
p : P
hp : p ∈ as
⊢ ¬Sbtw ℝ s₁.center p s₂.center

Tactic:
exact mt Sbtw.wbtw (h p hp)

Premises used: mt, Sbtw.wbtw
-- 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₁ s₂ : Sphere P
p : P
⊢ s₁.IsExtTangentAt s₂ p ↔ s₂.IsExtTangentAt s₁ p

Tactic:
⟨IsExtTangentAt.symm, IsExtTangentAt.symm⟩

Premises used: Iff.intro, EuclideanGeometry.Sphere.IsExtTangentAt.symm
-- 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₁ s₂ : Sphere P
⊢ s₁.IsExtTangentAt s₂ s₁.center ↔ s₁.radius = 0 ∧ s₁.center ∈ s₂

Tactic:
⟨?_, ?_⟩

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₁ s₂ : Sphere P
refine_1 : s₁.IsExtTangentAt s₂ s₁.center → s₁.radius = 0 ∧ s₁.center ∈ s₂
refine_2 : s₁.radius = 0 ∧ s₁.center ∈ s₂ → s₁.IsExtTangentAt s₂ s₁.center
⊢ s₁.IsExtTangentAt s₂ s₁.center ↔ s₁.radius = 0 ∧ s₁.center ∈ s₂

Tactic:
refine ⟨?_, ?_⟩
-- 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₁ s₂ : Sphere P
h₁ : s₁.center ∈ s₁
h₂ : s₁.center ∈ s₂
⊢ s₁.radius = 0

Tactic:
rw [center_mem_iff] at h₁

Premises used: EuclideanGeometry.Sphere.center_mem_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₁ s₂ : Sphere P
h₁ : s₁.center ∈ s₁
h₂ : s₁.center ∈ s₂
h₃ : s₁.radius = 0
⊢ s₁.center ∈ s₂

Tactic:
rw [center_mem_iff] at h₁

Premises used: EuclideanGeometry.Sphere.center_mem_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₁ s₂ : Sphere P
h₁ : s₁.radius = 0
h₂ : s₁.center ∈ s₂
⊢ s₁.radius = 0 ∧ s₁.center ∈ s₂

Tactic:
⟨h₁, h₂⟩

Premises used: And.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₁ s₂ : Sphere P
h₁ : s₁.radius = 0
h₂ : s₁.center ∈ s₂
⊢ s₁.radius = 0 ∧ s₁.center ∈ s₂

Tactic:
exact ⟨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₁ s₂ : Sphere P
hr : s₁.radius = 0
hc : s₁.center ∈ s₂
⊢ s₁.IsExtTangentAt s₂ s₁.center

Tactic:
⟨?_, hc, ?_⟩

Premises used: EuclideanGeometry.Sphere.IsExtTangentAt.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₁ s₂ : Sphere P
hr : s₁.radius = 0
hc : s₁.center ∈ s₂
refine_2 : s₁.center ∈ s₁
refine_2₁ : Wbtw ℝ s₁.center s₁.center s₂.center
⊢ s₁.IsExtTangentAt s₂ s₁.center

Tactic:
refine ⟨?_, hc, ?_⟩
-- 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₁ s₂ : Sphere P
hr : s₁.radius = 0
hc : s₁.center ∈ s₂
refine_2 : s₁.radius = 0
refine_2₁ refine_2₂ : Eq (α := ℝ) 0 0
⊢ s₁.center ∈ s₁

Tactic:
rw [center_mem_iff, hr]

Premises used: EuclideanGeometry.Sphere.center_mem_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₁ s₂ : Sphere P
hr : s₁.radius = 0
hc : s₁.center ∈ s₂
⊢ Wbtw ℝ s₁.center s₁.center s₂.center

Tactic:
simp
-- 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₁ s₂ : Sphere P
⊢ s₁.IsIntTangentAt s₂ s₁.center ↔ s₁.radius = 0 ∧ s₁.center ∈ s₂

Tactic:
⟨?_, ?_⟩

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₁ s₂ : Sphere P
refine_1 : s₁.IsIntTangentAt s₂ s₁.center → s₁.radius = 0 ∧ s₁.center ∈ s₂
refine_2 : s₁.radius = 0 ∧ s₁.center ∈ s₂ → s₁.IsIntTangentAt s₂ s₁.center
⊢ s₁.IsIntTangentAt s₂ s₁.center ↔ s₁.radius = 0 ∧ s₁.center ∈ s₂

Tactic:
refine ⟨?_, ?_⟩
-- 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₁ s₂ : Sphere P
hr : s₁.radius = 0
hc : s₁.center ∈ s₂
⊢ s₁.IsIntTangentAt s₂ s₁.center

Tactic:
⟨?_, hc, ?_⟩

Premises used: EuclideanGeometry.Sphere.IsIntTangentAt.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₁ s₂ : Sphere P
hr : s₁.radius = 0
hc : s₁.center ∈ s₂
refine_2 : s₁.center ∈ s₁
refine_2₁ : Wbtw ℝ s₂.center s₁.center s₁.center
⊢ s₁.IsIntTangentAt s₂ s₁.center

Tactic:
refine ⟨?_, hc, ?_⟩
-- 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₁ s₂ : Sphere P
hr : s₁.radius = 0
hc : s₁.center ∈ s₂
⊢ Wbtw ℝ s₂.center s₁.center s₁.center

Tactic:
simp
-- 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
h : p ∈ s
⊢ Wbtw ℝ s.center s.center p

Tactic:
simp
-- 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₁ s₂ : Sphere P
h : s₁.IsExtTangent s₂
rcases : ∀ (p : P) (hp : s₁.IsExtTangentAt s₂ p), s₂.IsExtTangent s₁
⊢ s₂.IsExtTangent s₁

Tactic:
rcases h with ⟨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₁ s₂ : Sphere P
p : P
hp : s₁.IsExtTangentAt s₂ p
⊢ s₂.IsExtTangent s₁

Tactic:
⟨p, hp.symm⟩

Premises used: EuclideanGeometry.Sphere.IsExtTangent, Exists.intro, EuclideanGeometry.Sphere.IsExtTangentAt.symm
-- 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₁ s₂ : Sphere P
p : P
hp : s₁.IsExtTangentAt s₂ p
⊢ s₂.IsExtTangent s₁

Tactic:
exact ⟨p, hp.symm⟩
-- 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₁ s₂ : Sphere P
⊢ s₁.IsExtTangent s₂ ↔ s₂.IsExtTangent s₁

Tactic:
⟨IsExtTangent.symm, IsExtTangent.symm⟩

Premises used: EuclideanGeometry.Sphere.IsExtTangent.symm, 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₁ s₂ : Sphere P
p : P
h : s₁.IsExtTangentAt s₂ p
⊢ s₁.IsExtTangent s₂

Tactic:
⟨p, h⟩

Premises used: EuclideanGeometry.Sphere.IsExtTangent, Exists.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₁ s₂ : Sphere P
p : P
h : s₁.IsIntTangentAt s₂ p
⊢ s₁.IsIntTangent s₂

Tactic:
⟨p, h⟩

Premises used: Exists.intro, EuclideanGeometry.Sphere.IsIntTangent
-- 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
inst_4 : Nontrivial V
s : Sphere P
simp_rw : (∃ (p : P), p ∈ s) ↔ 0 ≤ s.radius
⊢ s.IsIntTangent s ↔ 0 ≤ s.radius

Tactic:
simp_rw [IsIntTangent, isIntTangentAt_self_iff_mem]

Premises used: EuclideanGeometry.Sphere.isIntTangentAt_self_iff_mem, EuclideanGeometry.Sphere.IsIntTangent
-- 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
inst_4 : Nontrivial V
s : Sphere P
rw : (∃ (p : P), p ∈ s) ↔ (Metric.sphere s.center s.radius).Nonempty
⊢ (∃ (p : P), p ∈ s) ↔ 0 ≤ s.radius

Tactic:
rw [← nonempty_iff]

Premises used: EuclideanGeometry.Sphere.nonempty_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
inst_4 : Nontrivial V
s : Sphere P
⊢ (∃ (p : P), p ∈ s) ↔ (Metric.sphere s.center s.radius).Nonempty

Tactic:
simp [Set.Nonempty]

Premises used: Set.Nonempty
-- 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₁ s₂ : Sphere P
h : s₁.IsExtTangent s₂
rcases :
  ∀ (p : P) (h₁ : p ∈ s₁) (h₂ : p ∈ s₂) (h : Wbtw ℝ s₁.center p s₂.center),
    dist s₁.center s₂.center = s₁.radius + s₂.radius
⊢ dist s₁.center s₂.center = s₁.radius + s₂.radius

Tactic:
rcases h with ⟨p, h₁, 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₁ s₂ : Sphere P
p : P
h₁ : p ∈ s₁
h₂ : p ∈ s₂
h : Wbtw ℝ s₁.center p s₂.center
⊢ dist s₁.center p + dist p s₂.center = dist s₁.center s₂.center

Tactic:
rw [← dist_add_dist_eq_iff] at h

Premises used: dist_add_dist_eq_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₁ s₂ : Sphere P
p : P
h₁ : p ∈ s₁
h₂ : p ∈ s₂
h : dist s₁.center p + dist p s₂.center = dist s₁.center s₂.center
rw : dist s₁.center p + dist p s₂.center = s₁.radius + s₂.radius
rw₁ : s₁.radius + dist p s₂.center = s₁.radius + s₂.radius
rw₂ rw₃ : s₁.radius + s₂.radius = s₁.radius + s₂.radius
⊢ dist s₁.center s₂.center = s₁.radius + s₂.radius

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

Premises used: EuclideanGeometry.mem_sphere', Iff.mp