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

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

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

Tactic:
simp [← h, 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₁ s₂ : Sphere P
⊢ s₁.IsExtTangent s₂ ↔ dist s₁.center s₂.center = s₁.radius + s₂.radius ∧ 0 ≤ s₁.radius ∧ 0 ≤ s₂.radius

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

Premises used: EuclideanGeometry.Sphere.IsExtTangent.dist_center, And.intro, 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 : ∀ (h : s₁.IsExtTangent s₂), 0 ≤ s₁.radius ∧ 0 ≤ s₂.radius
refine_2 : dist s₁.center s₂.center = s₁.radius + s₂.radius ∧ 0 ≤ s₁.radius ∧ 0 ≤ s₂.radius → s₁.IsExtTangent s₂
⊢ s₁.IsExtTangent s₂ ↔ dist s₁.center s₂.center = s₁.radius + s₂.radius ∧ 0 ≤ s₁.radius ∧ 0 ≤ s₂.radius

Tactic:
refine ⟨fun h ↦ ⟨h.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₁ s₂ : Sphere P
h : s₁.IsExtTangent s₂
refine_1 : ∀ (p : P) (h₁ : p ∈ s₁) (h₂ : p ∈ s₂) (h : Wbtw ℝ s₁.center p s₂.center), 0 ≤ s₁.radius ∧ 0 ≤ s₂.radius
⊢ 0 ≤ s₁.radius ∧ 0 ≤ 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
⊢ 0 ≤ s₁.radius ∧ 0 ≤ s₂.radius

Tactic:
⟨radius_nonneg_of_mem h₁, radius_nonneg_of_mem h₂⟩

Premises used: EuclideanGeometry.Sphere.radius_nonneg_of_mem, 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
p : P
h₁ : p ∈ s₁
h₂ : p ∈ s₂
h : Wbtw ℝ s₁.center p s₂.center
⊢ 0 ≤ s₁.radius ∧ 0 ≤ s₂.radius

Tactic:
exact ⟨radius_nonneg_of_mem h₁, radius_nonneg_of_mem 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
h : dist s₁.center s₂.center = s₁.radius + s₂.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
⊢ s₁.IsExtTangent s₂

Tactic:
⟨AffineMap.lineMap s₁.center s₂.center (s₁.radius / (s₁.radius + s₂.radius)), ?_⟩

Premises used: EuclideanGeometry.Sphere.IsExtTangent, AffineMap.lineMap, HDiv.hDiv, EuclideanGeometry.Sphere.center, HAdd.hAdd, Exists.intro, DFunLike.coe, EuclideanGeometry.Sphere.radius
-- 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 : dist s₁.center s₂.center = s₁.radius + s₂.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
refine_2 :
  s₁.IsExtTangentAt s₂ ((AffineMap.lineMap s₁.center s₂.center : (a : ℝ) → P) (s₁.radius / (s₁.radius + s₂.radius)))
⊢ s₁.IsExtTangent s₂

Tactic:
refine ⟨AffineMap.lineMap s₁.center s₂.center (s₁.radius / (s₁.radius + s₂.radius)), ?_⟩
-- 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 : dist s₁.center s₂.center = s₁.radius + s₂.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
pos :
  ∀ (h0 : s₁.radius + s₂.radius = 0),
    s₁.IsExtTangentAt s₂ ((AffineMap.lineMap s₁.center s₂.center : (a : ℝ) → P) (s₁.radius / (s₁.radius + s₂.radius)))
neg :
  ∀ (h0 : ¬s₁.radius + s₂.radius = 0),
    s₁.IsExtTangentAt s₂ ((AffineMap.lineMap s₁.center s₂.center : (a : ℝ) → P) (s₁.radius / (s₁.radius + s₂.radius)))
⊢ s₁.IsExtTangentAt s₂ ((AffineMap.lineMap s₁.center s₂.center : (a : ℝ) → P) (s₁.radius / (s₁.radius + s₂.radius)))

Tactic:
by_cases h0 : s₁.radius + s₂.radius = 0

Premises used: EuclideanGeometry.Sphere.radius
-- 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 : dist s₁.center s₂.center = s₁.radius + s₂.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : s₁.radius + s₂.radius = 0
pos : s₁.radius = 0 ∧ dist s₁.center s₂.center = s₂.radius
⊢ s₁.IsExtTangentAt s₂ ((AffineMap.lineMap s₁.center s₂.center : (a : ℝ) → P) (s₁.radius / (s₁.radius + s₂.radius)))

Tactic:
simp only [h0, div_zero, AffineMap.lineMap_apply_zero, isExtTangentAt_center_iff, mem_sphere]

Premises used: EuclideanGeometry.Sphere.isExtTangentAt_center_iff, AffineMap.lineMap_apply_zero, EuclideanGeometry.mem_sphere, div_zero
-- 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 : dist s₁.center s₂.center = s₁.radius + s₂.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : s₁.radius + s₂.radius = 0
linarith : s₁.radius < 0 → 0 - s₁.radius + (s₁.radius - 0) = 0
linarith₁ : 0 < s₁.radius → 0 - s₂.radius + (s₁.radius + s₂.radius - 0) + (0 - s₁.radius) = 0
⊢ s₁.radius = 0

Tactic:
linarith
-- 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 : dist s₁.center s₂.center = s₁.radius + s₂.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : s₁.radius + s₂.radius = 0
linarith :
  dist s₁.center s₂.center < s₂.radius →
    -(dist s₁.center s₂.center - (s₁.radius + s₂.radius)) + (0 - s₁.radius) + (dist s₁.center s₂.center - s₂.radius) = 0
linarith₁ :
  s₂.radius < dist s₁.center s₂.center →
    dist s₁.center s₂.center - (s₁.radius + s₂.radius) + (0 - s₂.radius) + (s₁.radius + s₂.radius - 0) +
        (s₂.radius - dist s₁.center s₂.center) =
      0
⊢ dist s₁.center s₂.center = s₂.radius

Tactic:
linarith
-- 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 : dist s₁.center s₂.center = s₁.radius + s₂.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : s₁.radius + s₂.radius = 0
⊢ s₁.radius = 0 ∧ dist s₁.center s₂.center = s₂.radius

Tactic:
exact ⟨by linarith, by linarith⟩
-- 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 : dist s₁.center s₂.center = s₁.radius + s₂.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : ¬s₁.radius + s₂.radius = 0
⊢ s₁.IsExtTangentAt s₂ ((AffineMap.lineMap s₁.center s₂.center : (a : ℝ) → P) (s₁.radius / (s₁.radius + s₂.radius)))

Tactic:
⟨?_, ?_, ?_⟩

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
h : dist s₁.center s₂.center = s₁.radius + s₂.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : ¬s₁.radius + s₂.radius = 0
neg :
  Membership.mem (α := P) s₁
    ((AffineMap.lineMap s₁.center s₂.center : (a : ℝ) → P) (s₁.radius / (s₁.radius + s₂.radius)) : P)
neg₁ :
  Membership.mem (α := P) s₂
    ((AffineMap.lineMap s₁.center s₂.center : (a : ℝ) → P) (s₁.radius / (s₁.radius + s₂.radius)) : P)
neg₂ :
  Wbtw ℝ s₁.center ((AffineMap.lineMap s₁.center s₂.center : (a : ℝ) → P) (s₁.radius / (s₁.radius + s₂.radius)))
    s₂.center
⊢ s₁.IsExtTangentAt s₂ ((AffineMap.lineMap s₁.center s₂.center : (a : ℝ) → P) (s₁.radius / (s₁.radius + s₂.radius)))

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 : dist s₁.center s₂.center = s₁.radius + s₂.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : ¬s₁.radius + s₂.radius = 0
neg : s₁.radius / (s₁.radius + s₂.radius) * (s₁.radius + s₂.radius) = s₁.radius
⊢ Membership.mem (α := P) s₁
    ((AffineMap.lineMap s₁.center s₂.center : (a : ℝ) → P) (s₁.radius / (s₁.radius + s₂.radius)) : P)

Tactic:
simp only [mem_sphere, dist_lineMap_left, norm_div, Real.norm_eq_abs, h, abs_of_nonneg h₁,
          abs_of_nonneg (add_nonneg h₁ h₂)]

Premises used: dist_lineMap_left, add_nonneg, EuclideanGeometry.mem_sphere, norm_div, abs_of_nonneg, Real.norm_eq_abs
-- 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 : dist s₁.center s₂.center = s₁.radius + s₂.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : ¬s₁.radius + s₂.radius = 0
⊢ s₁.radius / (s₁.radius + s₂.radius) * (s₁.radius + s₂.radius) = s₁.radius

Tactic:
field
-- 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 : dist s₁.center s₂.center = s₁.radius + s₂.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : ¬s₁.radius + s₂.radius = 0
neg : |1 - s₁.radius / (s₁.radius + s₂.radius)| * (s₁.radius + s₂.radius) = s₂.radius
⊢ Membership.mem (α := P) s₂
    ((AffineMap.lineMap s₁.center s₂.center : (a : ℝ) → P) (s₁.radius / (s₁.radius + s₂.radius)) : P)

Tactic:
simp only [mem_sphere, dist_lineMap_right, Real.norm_eq_abs, h]

Premises used: dist_lineMap_right, EuclideanGeometry.mem_sphere, Real.norm_eq_abs
-- 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 : dist s₁.center s₂.center = s₁.radius + s₂.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : ¬s₁.radius + s₂.radius = 0
neg : s₂.radius / (s₁.radius + s₂.radius) * (s₁.radius + s₂.radius) = s₂.radius
⊢ |1 - s₁.radius / (s₁.radius + s₂.radius)| * (s₁.radius + s₂.radius) = s₂.radius

Tactic:
rw [one_sub_div h0, add_sub_cancel_left, abs_div, abs_of_nonneg h₂,
          abs_of_nonneg (add_nonneg h₁ h₂)]

Premises used: add_sub_cancel_left, abs_div, add_nonneg, abs_of_nonneg, one_sub_div
-- 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 : dist s₁.center s₂.center = s₁.radius + s₂.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : ¬s₁.radius + s₂.radius = 0
⊢ s₂.radius / (s₁.radius + s₂.radius) * (s₁.radius + s₂.radius) = s₂.radius

Tactic:
field
-- 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 : dist s₁.center s₂.center = s₁.radius + s₂.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : ¬s₁.radius + s₂.radius = 0
neg : s₁.center = s₂.center ∨ Membership.mem (γ := Set ℝ) (Set.Icc 0 1) (s₁.radius / (s₁.radius + s₂.radius))
⊢ Wbtw ℝ s₁.center ((AffineMap.lineMap s₁.center s₂.center : (a : ℝ) → P) (s₁.radius / (s₁.radius + s₂.radius)))
    s₂.center

Tactic:
simp only [wbtw_lineMap_iff]

Premises used: wbtw_lineMap_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 : dist s₁.center s₂.center = s₁.radius + s₂.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : ¬s₁.radius + s₂.radius = 0
⊢ s₁.center = s₂.center ∨ Membership.mem (γ := Set ℝ) (Set.Icc 0 1) (s₁.radius / (s₁.radius + s₂.radius))

Tactic:
.inr ⟨?_, ?_⟩

Premises used: And.intro, 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
h : dist s₁.center s₂.center = s₁.radius + s₂.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : ¬s₁.radius + s₂.radius = 0
neg : 0 ≤ s₁.radius / (s₁.radius + s₂.radius)
neg₁ : s₁.radius / (s₁.radius + s₂.radius) ≤ 1
⊢ s₁.center = s₂.center ∨ Membership.mem (γ := Set ℝ) (Set.Icc 0 1) (s₁.radius / (s₁.radius + s₂.radius))

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
h : dist s₁.center s₂.center = s₁.radius + s₂.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : ¬s₁.radius + s₂.radius = 0
⊢ 0 ≤ s₁.radius / (s₁.radius + s₂.radius)

Tactic:
positivity
-- 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 : dist s₁.center s₂.center = s₁.radius + s₂.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : ¬s₁.radius + s₂.radius = 0
⊢ 0 < s₁.radius + s₂.radius

Tactic:
positivity
-- 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 : dist s₁.center s₂.center = s₁.radius + s₂.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : ¬s₁.radius + s₂.radius = 0
neg : s₁.radius ≤ s₁.radius + s₂.radius
⊢ s₁.radius / (s₁.radius + s₂.radius) ≤ 1

Tactic:
rw [div_le_one (by positivity)]

Premises used: div_le_one
-- 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 : dist s₁.center s₂.center = s₁.radius + s₂.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : ¬s₁.radius + s₂.radius = 0
linarith : s₁.radius + s₂.radius < s₁.radius → 0 - s₂.radius + (s₁.radius + s₂.radius - s₁.radius) = 0
⊢ s₁.radius ≤ s₁.radius + s₂.radius

Tactic:
linarith
-- 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₁ s₂ : Sphere P
⊢ s₁.IsIntTangent s₂ ↔ dist s₁.center s₂.center = s₂.radius - s₁.radius ∧ 0 ≤ s₁.radius ∧ 0 ≤ s₂.radius

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

Premises used: And.intro, Iff.intro, EuclideanGeometry.Sphere.IsIntTangent.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
inst_4 : Nontrivial V
s₁ s₂ : Sphere P
refine_1 : ∀ (h : s₁.IsIntTangent s₂), 0 ≤ s₁.radius ∧ 0 ≤ s₂.radius
refine_2 : dist s₁.center s₂.center = s₂.radius - s₁.radius ∧ 0 ≤ s₁.radius ∧ 0 ≤ s₂.radius → s₁.IsIntTangent s₂
⊢ s₁.IsIntTangent s₂ ↔ dist s₁.center s₂.center = s₂.radius - s₁.radius ∧ 0 ≤ s₁.radius ∧ 0 ≤ s₂.radius

Tactic:
refine ⟨fun h ↦ ⟨h.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
inst_4 : Nontrivial V
s₁ s₂ : Sphere P
h : s₁.IsIntTangent s₂
refine_1 : ∀ (p : P) (h₁ : p ∈ s₁) (h₂ : p ∈ s₂) (h : Wbtw ℝ s₂.center s₁.center p), 0 ≤ s₁.radius ∧ 0 ≤ s₂.radius
⊢ 0 ≤ s₁.radius ∧ 0 ≤ 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
inst_4 : Nontrivial V
s₁ s₂ : Sphere P
p : P
h₁ : p ∈ s₁
h₂ : p ∈ s₂
h : Wbtw ℝ s₂.center s₁.center p
⊢ 0 ≤ s₁.radius ∧ 0 ≤ s₂.radius

Tactic:
⟨radius_nonneg_of_mem h₁, radius_nonneg_of_mem h₂⟩

Premises used: EuclideanGeometry.Sphere.radius_nonneg_of_mem, 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
inst_4 : Nontrivial V
s₁ s₂ : Sphere P
p : P
h₁ : p ∈ s₁
h₂ : p ∈ s₂
h : Wbtw ℝ s₂.center s₁.center p
⊢ 0 ≤ s₁.radius ∧ 0 ≤ s₂.radius

Tactic:
exact ⟨radius_nonneg_of_mem h₁, radius_nonneg_of_mem 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
inst_4 : Nontrivial V
s₁ s₂ : Sphere P
h : dist s₁.center s₂.center = s₂.radius - s₁.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
pos : ∀ (h0 : s₁.center = s₂.center), s₁.IsIntTangent s₂
neg : ∀ (h0 : ¬s₁.center = s₂.center), s₁.IsIntTangent s₂
⊢ s₁.IsIntTangent s₂

Tactic:
by_cases h0 : s₁.center = s₂.center

Premises used: EuclideanGeometry.Sphere.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
inst_4 : Nontrivial V
s₁ s₂ : Sphere P
h : dist s₁.center s₂.center = s₂.radius - s₁.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : s₁.center = s₂.center
⊢ s₁.radius = s₂.radius

Tactic:
rw [h0, dist_self, eq_comm, sub_eq_zero, eq_comm] at h

Premises used: sub_eq_zero, eq_comm, dist_self
-- 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₁ s₂ : Sphere P
h : dist s₁.center s₂.center = s₂.radius - s₁.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : s₁.center = s₂.center
h₃ : s₁.radius = s₂.radius
⊢ 0 ≤ s₁.radius

Tactic:
rw [h0, dist_self, eq_comm, sub_eq_zero, eq_comm] at h

Premises used: sub_eq_zero, eq_comm, dist_self
-- 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₁ s₂ : Sphere P
h : dist s₁.center s₂.center = s₂.radius - s₁.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : s₁.center = s₂.center
h₃ : s₁.radius = s₂.radius
h₄ : 0 ≤ s₁.radius
⊢ 0 ≤ s₂.radius

Tactic:
rw [h0, dist_self, eq_comm, sub_eq_zero, eq_comm] at h

Premises used: sub_eq_zero, eq_comm, dist_self
-- 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₁ s₂ : Sphere P
h : dist s₁.center s₂.center = s₂.radius - s₁.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : s₁.center = s₂.center
h₃ : s₁.radius = s₂.radius
h₄ : 0 ≤ s₁.radius
h₅ : 0 ≤ s₂.radius
⊢ s₁.center = s₂.center

Tactic:
rw [h0, dist_self, eq_comm, sub_eq_zero, eq_comm] at h

Premises used: sub_eq_zero, eq_comm, dist_self
-- 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₁ s₂ : Sphere P
h : s₁.radius = s₂.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 center : s₁.center = s₂.center
radius : s₁.radius = s₂.radius
⊢ s₁ = s₂

Tactic:
ext
-- 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₁ s₂ : Sphere P
h : s₁.radius = s₂.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : s₁.center = s₂.center
⊢ s₁.center = s₂.center

Tactic:
assumption
-- 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₁ s₂ : Sphere P
h : s₁.radius = s₂.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : s₁.center = s₂.center
⊢ s₁.radius = s₂.radius

Tactic:
assumption
-- 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₁ s₂ : Sphere P
h : s₁.radius = s₂.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : s₁.center = s₂.center
⊢ s₁ = s₂

Tactic:
have hs : s₁ = s₂ := by
        ext <;> assumption
-- 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₁ s₂ : Sphere P
h : s₁.radius = s₂.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : s₁.center = s₂.center
hs : s₁ = s₂
⊢ s₁.IsIntTangent s₂

Tactic:
simp [hs, 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
inst_4 : Nontrivial V
s₁ s₂ : Sphere P
h : dist s₁.center s₂.center = s₂.radius - s₁.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : ¬s₁.center = s₂.center
⊢ dist s₂.center s₁.center = s₂.radius - s₁.radius

Tactic:
rw [dist_comm] at h

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
inst_4 : Nontrivial V
s₁ s₂ : Sphere P
h : dist s₁.center s₂.center = s₂.radius - s₁.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : ¬s₁.center = s₂.center
h₃ : dist s₂.center s₁.center = s₂.radius - s₁.radius
⊢ 0 ≤ s₁.radius

Tactic:
rw [dist_comm] at h

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
inst_4 : Nontrivial V
s₁ s₂ : Sphere P
h : dist s₁.center s₂.center = s₂.radius - s₁.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : ¬s₁.center = s₂.center
h₃ : dist s₂.center s₁.center = s₂.radius - s₁.radius
h₄ : 0 ≤ s₁.radius
⊢ 0 ≤ s₂.radius

Tactic:
rw [dist_comm] at h

Premises used: dist_comm