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₁ 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
⊢ dist s₁.center s₂.center = s₁.radius + s₂.radius
have rw₂ : s₁.radius + s₂.radius = s₁.radius + s₂.radius
Tactic: rw [← h, mem_sphere'.1 h₁, 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₁ s₂ : Sphere P
h : s₁.IsIntTangent s₂
⊢ dist s₁.center s₂.center = s₂.radius - s₁.radius
have 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
Tactic: rcases h with ⟨p, h₁, h₂, h⟩
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₁ 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
have h₃ : 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
Cleared hypotheses: 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₁ s₂ : Sphere P
⊢ s₁.IsExtTangent s₂ ↔ dist s₁.center s₂.center = s₁.radius + s₂.radius ∧ 0 ≤ s₁.radius ∧ 0 ≤ s₂.radius
have refine_1 : ∀ (h : s₁.IsExtTangent s₂), 0 ≤ s₁.radius ∧ 0 ≤ s₂.radius
Tactic: refine ⟨fun h ↦ ⟨h.dist_center, ?_⟩, ?_⟩
-- 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₁ s₂ : Sphere P
refine_1 : ∀ (h : s₁.IsExtTangent s₂), 0 ≤ s₁.radius ∧ 0 ≤ s₂.radius
⊢ s₁.IsExtTangent s₂ ↔ dist s₁.center s₂.center = s₁.radius + s₂.radius ∧ 0 ≤ s₁.radius ∧ 0 ≤ s₂.radius
have refine_2 : dist s₁.center s₂.center = s₁.radius + s₂.radius ∧ 0 ≤ s₁.radius ∧ 0 ≤ s₂.radius → s₁.IsExtTangent s₂
Tactic: refine ⟨fun h ↦ ⟨h.dist_center, ?_⟩, ?_⟩
-- 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₁ s₂ : Sphere P
h : s₁.IsExtTangent s₂
⊢ 0 ≤ s₁.radius ∧ 0 ≤ s₂.radius
have refine_1 : ∀ (p : P) (h₁ : p ∈ s₁) (h₂ : p ∈ s₂) (h : Wbtw ℝ s₁.center p s₂.center), 0 ≤ s₁.radius ∧ 0 ≤ s₂.radius
Tactic: rcases h with ⟨p, h₁, h₂, h⟩
Cleared hypotheses: 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₁ s₂ : Sphere P
h : dist s₁.center s₂.center = s₁.radius + s₂.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
⊢ s₁.IsExtTangent s₂
have refine_2 : s₁.IsExtTangentAt s₂ ((AffineMap.lineMap s₁.center s₂.center : (a : ℝ) → P) (s₁.radius / (s₁.radius + s₂.radius)))
Tactic: refine ⟨AffineMap.lineMap s₁.center s₂.center (s₁.radius / (s₁.radius + s₂.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₁ s₂ : Sphere P
h : dist s₁.center s₂.center = s₁.radius + s₂.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
⊢ s₁.IsExtTangentAt s₂ ((AffineMap.lineMap s₁.center s₂.center : (a : ℝ) → P) (s₁.radius / (s₁.radius + s₂.radius)))
have pos : ∀ (h0 : s₁.radius + s₂.radius = 0),
  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
-- 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₁ 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)))
⊢ s₁.IsExtTangentAt s₂ ((AffineMap.lineMap s₁.center s₂.center : (a : ℝ) → P) (s₁.radius / (s₁.radius + s₂.radius)))
have neg : ∀ (h0 : ¬s₁.radius + s₂.radius = 0),
  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
-- 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₁ 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)))
have pos : s₁.radius = 0 ∧ dist s₁.center s₂.center = s₂.radius
Tactic: simp only [h0, div_zero, AffineMap.lineMap_apply_zero, isExtTangentAt_center_iff, 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₁ 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
have linarith : s₁.radius < 0 → 0 - s₁.radius + (s₁.radius - 0) = 0
Tactic: linarith
-- 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₁ 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
⊢ s₁.radius = 0
have linarith₁ : 0 < s₁.radius → 0 - s₂.radius + (s₁.radius + s₂.radius - 0) + (0 - s₁.radius) = 0
Tactic: linarith
-- 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₁ 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
⊢ dist s₁.center s₂.center = s₂.radius
have 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
Tactic: linarith
-- 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₁ 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
⊢ dist s₁.center s₂.center = s₂.radius
have 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
Tactic: linarith
-- 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₁ 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)))
have neg : Membership.mem (α := P) s₁
  ((AffineMap.lineMap s₁.center s₂.center : (a : ℝ) → P) (s₁.radius / (s₁.radius + s₂.radius)) : P)
Tactic: refine ⟨?_, ?_, ?_⟩
-- 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₁ 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)
⊢ s₁.IsExtTangentAt s₂ ((AffineMap.lineMap s₁.center s₂.center : (a : ℝ) → P) (s₁.radius / (s₁.radius + s₂.radius)))
have neg₁ : Membership.mem (α := P) s₂
  ((AffineMap.lineMap s₁.center s₂.center : (a : ℝ) → P) (s₁.radius / (s₁.radius + s₂.radius)) : P)
Tactic: refine ⟨?_, ?_, ?_⟩
-- 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₁ 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)
⊢ s₁.IsExtTangentAt s₂ ((AffineMap.lineMap s₁.center s₂.center : (a : ℝ) → P) (s₁.radius / (s₁.radius + s₂.radius)))
have neg₂ : Wbtw ℝ s₁.center ((AffineMap.lineMap s₁.center s₂.center : (a : ℝ) → P) (s₁.radius / (s₁.radius + s₂.radius))) s₂.center
Tactic: refine ⟨?_, ?_, ?_⟩
-- 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₁ 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
⊢ Membership.mem (α := P) s₁
    ((AffineMap.lineMap s₁.center s₂.center : (a : ℝ) → P) (s₁.radius / (s₁.radius + s₂.radius)) : P)
have neg : s₁.radius / (s₁.radius + s₂.radius) * (s₁.radius + s₂.radius) = s₁.radius
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₂)]
-- 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₁ 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
⊢ Membership.mem (α := P) s₂
    ((AffineMap.lineMap s₁.center s₂.center : (a : ℝ) → P) (s₁.radius / (s₁.radius + s₂.radius)) : P)
have neg : |1 - s₁.radius / (s₁.radius + s₂.radius)| * (s₁.radius + s₂.radius) = s₂.radius
Tactic: simp only [mem_sphere, dist_lineMap_right, Real.norm_eq_abs, 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₁ 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
⊢ |1 - s₁.radius / (s₁.radius + s₂.radius)| * (s₁.radius + s₂.radius) = s₂.radius
have neg : 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₂)]
-- 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₁ 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
⊢ Wbtw ℝ s₁.center ((AffineMap.lineMap s₁.center s₂.center : (a : ℝ) → P) (s₁.radius / (s₁.radius + s₂.radius)))
    s₂.center
have neg : s₁.center = s₂.center ∨ Membership.mem (γ := Set ℝ) (Set.Icc 0 1) (s₁.radius / (s₁.radius + s₂.radius))
Tactic: simp only [wbtw_lineMap_iff]
-- 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₁ 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))
have neg : 0 ≤ s₁.radius / (s₁.radius + s₂.radius)
Tactic: refine .inr ⟨?_, ?_⟩
-- 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₁ 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)
⊢ s₁.center = s₂.center ∨ Membership.mem (γ := Set ℝ) (Set.Icc 0 1) (s₁.radius / (s₁.radius + s₂.radius))
have neg₁ : s₁.radius / (s₁.radius + s₂.radius) ≤ 1
Tactic: refine .inr ⟨?_, ?_⟩
-- 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₁ 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) ≤ 1
have neg : s₁.radius ≤ s₁.radius + s₂.radius
Tactic: rw [div_le_one (by positivity)]
-- 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₁ 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
have linarith : s₁.radius + s₂.radius < s₁.radius → 0 - s₂.radius + (s₁.radius + s₂.radius - s₁.radius) = 0
Tactic: linarith
-- 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
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
have refine_1 : ∀ (h : s₁.IsIntTangent s₂), 0 ≤ s₁.radius ∧ 0 ≤ s₂.radius
Tactic: refine ⟨fun h ↦ ⟨h.dist_center, ?_⟩, ?_⟩
-- 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
inst_4 : Nontrivial V
s₁ s₂ : Sphere P
refine_1 : ∀ (h : s₁.IsIntTangent s₂), 0 ≤ s₁.radius ∧ 0 ≤ s₂.radius
⊢ s₁.IsIntTangent s₂ ↔ dist s₁.center s₂.center = s₂.radius - s₁.radius ∧ 0 ≤ s₁.radius ∧ 0 ≤ s₂.radius
have refine_2 : dist s₁.center s₂.center = s₂.radius - s₁.radius ∧ 0 ≤ s₁.radius ∧ 0 ≤ s₂.radius → s₁.IsIntTangent s₂
Tactic: refine ⟨fun h ↦ ⟨h.dist_center, ?_⟩, ?_⟩
-- 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
inst_4 : Nontrivial V
s₁ s₂ : Sphere P
h : s₁.IsIntTangent s₂
⊢ 0 ≤ s₁.radius ∧ 0 ≤ s₂.radius
have refine_1 : ∀ (p : P) (h₁ : p ∈ s₁) (h₂ : p ∈ s₂) (h : Wbtw ℝ s₂.center s₁.center p), 0 ≤ s₁.radius ∧ 0 ≤ s₂.radius
Tactic: rcases h with ⟨p, h₁, h₂, h⟩
Cleared hypotheses: 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
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
⊢ s₁.IsIntTangent s₂
have pos : ∀ (h0 : s₁.center = s₂.center), s₁.IsIntTangent s₂
Tactic: by_cases h0 : s₁.center = s₂.center
-- 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
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₂
⊢ s₁.IsIntTangent s₂
have neg : ∀ (h0 : ¬s₁.center = s₂.center), s₁.IsIntTangent s₂
Tactic: by_cases h0 : s₁.center = s₂.center
-- 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
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₁.IsIntTangent s₂
have h₃ : s₁.radius = s₂.radius
Tactic: rw [h0, dist_self, eq_comm, sub_eq_zero, eq_comm] at h
Cleared hypotheses: h, h₁, h₂, h0
-- 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
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₁.IsIntTangent s₂
have hs : s₁ = s₂
Tactic: have hs : s₁ = s₂ := by
        ext <;> assumption
-- 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
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₁.IsIntTangent s₂
have h₃ : dist s₂.center s₁.center = s₂.radius - s₁.radius
Tactic: rw [dist_comm] at h
Cleared hypotheses: h, h₁, h₂, h0
-- 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
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| = s₂.radius - s₁.radius
have refine : 0 ≤ s₂.radius - s₁.radius
Tactic: refine abs_of_nonneg ?_
-- 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
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
⊢ 0 ≤ s₂.radius - s₁.radius
have rw : 0 ≤ dist s₂.center s₁.center
Tactic: rw [← 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
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₁.IsIntTangent s₂
have ha : |s₂.radius - s₁.radius| = s₂.radius - s₁.radius
Tactic: have ha : |s₂.radius - s₁.radius| = s₂.radius - s₁.radius := by
        refine abs_of_nonneg ?_
        rw [← h]
        exact dist_nonneg
-- 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
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
ha : |s₂.radius - s₁.radius| = s₂.radius - s₁.radius
hr0 : s₂.radius - s₁.radius = 0
⊢ False
have h₃ : s₂.center = s₁.center
Tactic: rw [hr0, dist_eq_zero] at h
Cleared hypotheses: h, h₁, h₂, h0, ha, hr0
-- 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
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
ha : |s₂.radius - s₁.radius| = s₂.radius - s₁.radius
⊢ s₁.IsIntTangent s₂
have hr0 : s₂.radius - s₁.radius ≠ 0
Tactic: have hr0 : s₂.radius - s₁.radius ≠ 0 := by
        intro hr0
        rw [hr0, dist_eq_zero] at h
        exact h0 h.symm
-- 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
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
ha : |s₂.radius - s₁.radius| = s₂.radius - s₁.radius
hr0 : s₂.radius - s₁.radius ≠ 0
⊢ s₁.IsIntTangent s₂
have neg : Membership.mem (α := P) s₁
  ((AffineMap.lineMap s₂.center s₁.center : (a : ℝ) → P) (s₂.radius / (s₂.radius - s₁.radius)) : P)
Tactic: refine ⟨AffineMap.lineMap s₂.center s₁.center (s₂.radius / (s₂.radius - s₁.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
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
ha : |s₂.radius - s₁.radius| = s₂.radius - s₁.radius
hr0 : 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)
⊢ s₁.IsIntTangent s₂
have neg₁ : Membership.mem (α := P) s₂
  ((AffineMap.lineMap s₂.center s₁.center : (a : ℝ) → P) (s₂.radius / (s₂.radius - s₁.radius)) : P)
Tactic: refine ⟨AffineMap.lineMap s₂.center s₁.center (s₂.radius / (s₂.radius - s₁.radius)),
              ?_, ?_, ?_⟩