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
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
h₅ : 0 ≤ s₂.radius
⊢ ¬s₁.center = s₂.center

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
⊢ |s₂.radius - s₁.radius| = s₂.radius - s₁.radius

Tactic:
abs_of_nonneg ?_

Premises used: abs_of_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
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
refine : 0 ≤ s₂.radius - s₁.radius
⊢ |s₂.radius - s₁.radius| = s₂.radius - s₁.radius

Tactic:
refine abs_of_nonneg ?_

Premises used: abs_of_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
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
rw : 0 ≤ dist s₂.center s₁.center
⊢ 0 ≤ s₂.radius - s₁.radius

Tactic:
rw [← 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
⊢ 0 ≤ dist s₂.center s₁.center

Tactic:
dist_nonneg

Premises used: dist_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
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 ≤ dist s₂.center s₁.center

Tactic:
exact dist_nonneg

Premises used: dist_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
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

Tactic:
have ha : |s₂.radius - s₁.radius| = s₂.radius - s₁.radius := by
        refine abs_of_nonneg ?_
        rw [← h]
        exact dist_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
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₂.center = s₁.center

Tactic:
rw [hr0, dist_eq_zero] at h

Premises used: dist_eq_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
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
h₃ : s₂.center = s₁.center
⊢ 0 ≤ s₁.radius

Tactic:
rw [hr0, dist_eq_zero] at h

Premises used: dist_eq_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
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
h₃ : s₂.center = s₁.center
h₄ : 0 ≤ s₁.radius
⊢ 0 ≤ s₂.radius

Tactic:
rw [hr0, dist_eq_zero] at h

Premises used: dist_eq_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
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
h₃ : s₂.center = s₁.center
h₄ : 0 ≤ s₁.radius
h₅ : 0 ≤ s₂.radius
⊢ ¬s₁.center = s₂.center

Tactic:
rw [hr0, dist_eq_zero] at h

Premises used: dist_eq_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
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
h₃ : s₂.center = s₁.center
h₄ : 0 ≤ s₁.radius
h₅ : 0 ≤ s₂.radius
h0₁ : ¬s₁.center = s₂.center
⊢ |s₂.radius - s₁.radius| = s₂.radius - s₁.radius

Tactic:
rw [hr0, dist_eq_zero] at h

Premises used: dist_eq_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
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
h₃ : s₂.center = s₁.center
h₄ : 0 ≤ s₁.radius
h₅ : 0 ≤ s₂.radius
h0₁ : ¬s₁.center = s₂.center
ha₁ : |s₂.radius - s₁.radius| = s₂.radius - s₁.radius
⊢ s₂.radius - s₁.radius = 0

Tactic:
rw [hr0, dist_eq_zero] at h

Premises used: dist_eq_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
inst_4 : Nontrivial V
s₁ s₂ : Sphere P
h : s₂.center = s₁.center
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

Tactic:
h0 h.symm

Premises used: Eq.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
inst_4 : Nontrivial V
s₁ s₂ : Sphere P
h : s₂.center = s₁.center
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

Tactic:
exact h0 h.symm

Premises used: Eq.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
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₂.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
-- 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
ha : |s₂.radius - s₁.radius| = s₂.radius - s₁.radius
hr0 : s₂.radius - s₁.radius ≠ 0
⊢ s₁.IsIntTangent s₂

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

Premises used: AffineMap.lineMap, HSub.hSub, HDiv.hDiv, EuclideanGeometry.Sphere.center, Exists.intro, EuclideanGeometry.Sphere.IsIntTangent, DFunLike.coe, EuclideanGeometry.Sphere.IsIntTangentAt.mk, 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
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)
neg₁ :
  Membership.mem (α := P) s₂
    ((AffineMap.lineMap s₂.center s₁.center : (a : ℝ) → P) (s₂.radius / (s₂.radius - s₁.radius)) : P)
neg₂ :
  Wbtw ℝ s₂.center s₁.center
    ((AffineMap.lineMap s₂.center s₁.center : (a : ℝ) → P) (s₂.radius / (s₂.radius - s₁.radius)))
⊢ s₁.IsIntTangent 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
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 : 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, one_sub_div hr0, abs_div,
          sub_sub_cancel_left, abs_neg, abs_of_nonneg h₁, ha]

Premises used: abs_neg, abs_div, sub_sub_cancel_left, dist_lineMap_right, EuclideanGeometry.mem_sphere, abs_of_nonneg, one_sub_div, 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
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₁.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
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 : 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, ha,
          abs_of_nonneg h₂]

Premises used: dist_lineMap_left, 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
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₂.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
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 :
  s₂.center = s₁.center ∨
    Membership.mem.{u_2, u_2} (α := P) (γ := Set P)
      (Set.image (α := ℝ) (⇑(AffineMap.lineMap s₂.center s₁.center) : (a : ℝ) → P) (Set.Ici 1))
      ((AffineMap.lineMap s₂.center s₁.center : (a : ℝ) → P) (s₂.radius / (s₂.radius - s₁.radius)) : P)
⊢ Wbtw ℝ s₂.center s₁.center
    ((AffineMap.lineMap s₂.center s₁.center : (a : ℝ) → P) (s₂.radius / (s₂.radius - s₁.radius)))

Tactic:
rw [wbtw_iff_left_eq_or_right_mem_image_Ici]

Premises used: wbtw_iff_left_eq_or_right_mem_image_Ici
-- 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
ha : |s₂.radius - s₁.radius| = s₂.radius - s₁.radius
hr0 : s₂.radius - s₁.radius ≠ 0
neg : 1 ≤ s₂.radius / (s₂.radius - s₁.radius)
⊢ s₂.center = s₁.center ∨
    Membership.mem.{u_2, u_2} (α := P) (γ := Set P)
      (Set.image (α := ℝ) (⇑(AffineMap.lineMap s₂.center s₁.center) : (a : ℝ) → P) (Set.Ici 1))
      ((AffineMap.lineMap s₂.center s₁.center : (a : ℝ) → P) (s₂.radius / (s₂.radius - s₁.radius)) : P)

Tactic:
simp only [Ne.symm h0, Set.mem_image, Set.mem_Ici, AffineMap.lineMap_eq_lineMap_iff,
          false_or, exists_eq_right]

Premises used: Set.mem_image, exists_eq_right, Ne.symm, false_or, AffineMap.lineMap_eq_lineMap_iff, Set.mem_Ici
-- 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
ha : |s₂.radius - s₁.radius| = s₂.radius - s₁.radius
hr0 : s₂.radius - s₁.radius ≠ 0
neg : s₂.radius - s₁.radius ≤ s₂.radius
neg₁ : 0 < s₂.radius - s₁.radius
⊢ 1 ≤ s₂.radius / (s₂.radius - s₁.radius)

Tactic:
rw [one_le_div]

Premises used: one_le_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
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
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
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 : 0 < dist s₂.center s₁.center
⊢ 0 < s₂.radius - s₁.radius

Tactic:
rw [← 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
ha : |s₂.radius - s₁.radius| = s₂.radius - s₁.radius
hr0 : s₂.radius - s₁.radius ≠ 0
⊢ 0 < dist s₂.center s₁.center

Tactic:
simp [Ne.symm h0]

Premises used: Ne.symm
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
⊢ 2 * ‖x‖ * ‖y‖ * Real.cos (angle x y) = 2 * (Real.cos (angle x y) * (‖x‖ * ‖y‖))

Tactic:
ring
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
rw : ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - 2 * (Real.cos (angle x y) * (‖x‖ * ‖y‖))
rw₁ : ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - 2 * ⟪x, y⟫
rw₂ : ⟪x - y, x - y⟫ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - 2 * ⟪x, y⟫
rw₃ : ⟪x - y, x - y⟫ = ⟪x, x⟫ + ‖y‖ * ‖y‖ - 2 * ⟪x, y⟫
rw₄ : ⟪x - y, x - y⟫ = ⟪x, x⟫ + ⟪y, y⟫ - 2 * ⟪x, y⟫
rw₅ : ⟪x, x⟫ - 2 * ⟪x, y⟫ + ⟪y, y⟫ = ⟪x, x⟫ + ⟪y, y⟫ - 2 * ⟪x, y⟫
rw₆ rw₇ : ⟪x, x⟫ + ⟪y, y⟫ - 2 * ⟪x, y⟫ = ⟪x, x⟫ + ⟪y, y⟫ - 2 * ⟪x, y⟫
⊢ ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - 2 * ‖x‖ * ‖y‖ * Real.cos (angle x y)

Tactic:
rw [show 2 * ‖x‖ * ‖y‖ * Real.cos (angle x y) = 2 * (Real.cos (angle x y) * (‖x‖ * ‖y‖)) by ring,
    cos_angle_mul_norm_mul_norm, ← real_inner_self_eq_norm_mul_norm, ←
    real_inner_self_eq_norm_mul_norm, ← real_inner_self_eq_norm_mul_norm, real_inner_sub_sub_self,
    sub_add_eq_add_sub]

Premises used: InnerProductGeometry.cos_angle_mul_norm_mul_norm, real_inner_sub_sub_self, real_inner_self_eq_norm_mul_norm, sub_add_eq_add_sub
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
inl : Real.sin (angle x 0) * ‖x‖ = Real.sin (angle 0 (x - 0)) * ‖x - 0‖
inr : ∀ (hy : y ≠ 0), Real.sin (angle x y) * ‖x‖ = Real.sin (angle y (x - y)) * ‖x - y‖
⊢ Real.sin (angle x y) * ‖x‖ = Real.sin (angle y (x - y)) * ‖x - y‖

Tactic:
obtain rfl | hy := eq_or_ne y 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x : V
⊢ Real.sin (angle x 0) * ‖x‖ = Real.sin (angle 0 (x - 0)) * ‖x - 0‖

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
inr : Real.sin (angle 0 y) * norm.{u_1} (E := V) 0 = Real.sin (angle y (0 - y)) * ‖0 - y‖
inr₁ : ∀ (hx : x ≠ 0), Real.sin (angle x y) * ‖x‖ = Real.sin (angle y (x - y)) * ‖x - y‖
⊢ Real.sin (angle x y) * ‖x‖ = Real.sin (angle y (x - y)) * ‖x - y‖

Tactic:
obtain rfl | hx := eq_or_ne x 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
y : V
hy : y ≠ 0
⊢ Real.sin (angle 0 y) * norm.{u_1} (E := V) 0 = Real.sin (angle y (0 - y)) * ‖0 - y‖

Tactic:
simp [angle_neg_right, angle_self hy]

Premises used: InnerProductGeometry.angle_neg_right, InnerProductGeometry.angle_self
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
inr : ∀ (hy : x ≠ 0), Real.sin (angle x x) * ‖x‖ = Real.sin (angle x (x - x)) * ‖x - x‖
inr₁ : ∀ (hxy : x ≠ y), Real.sin (angle x y) * ‖x‖ = Real.sin (angle y (x - y)) * ‖x - y‖
⊢ Real.sin (angle x y) * ‖x‖ = Real.sin (angle y (x - y)) * ‖x - y‖

Tactic:
obtain rfl | hxy := eq_or_ne x y

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x : V
hx hy : x ≠ 0
⊢ Real.sin (angle x x) * ‖x‖ = Real.sin (angle x (x - x)) * ‖x - x‖

Tactic:
simp [angle_self hx]

Premises used: InnerProductGeometry.angle_self
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x_1 y_1 : V
hy_1 : y_1 ≠ 0
hx_1 : x_1 ≠ 0
hxy : x_1 ≠ y_1
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ Real.sin (angle x y) = √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖y‖)

Tactic:
simp [field, mul_assoc, sin_angle_mul_norm_mul_norm]

Premises used: mul_assoc, InnerProductGeometry.sin_angle_mul_norm_mul_norm
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
hxy : x ≠ y
⊢ ∀ (x y : V) (hx : x ≠ 0) (hy : y ≠ 0), Real.sin (angle x y) = √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖y‖)

Tactic:
have h_sin (x y : V) (hx : x ≠ 0) (hy : y ≠ 0) :
      Real.sin (angle x y) = √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖y‖) := by
    simp [field, mul_assoc, sin_angle_mul_norm_mul_norm]
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
hxy : x ≠ y
h_sin : ∀ (x y : V) (hx : x ≠ 0) (hy : y ≠ 0), Real.sin (angle x y) = √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖y‖)
inr :
  √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖y‖) * ‖x‖ =
    √(⟪y, y⟫ * ⟪x - y, x - y⟫ - ⟪y, x - y⟫ * ⟪y, x - y⟫) / (‖y‖ * ‖x - y‖) * ‖x - y‖
⊢ Real.sin (angle x y) * ‖x‖ = Real.sin (angle y (x - y)) * ‖x - y‖

Tactic:
rw [h_sin x y hx hy, h_sin y (x - y) hy (sub_ne_zero_of_ne hxy)]

Premises used: HSub.hSub, sub_ne_zero_of_ne
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
hxy : x ≠ y
h_sin : ∀ (x y : V) (hx : x ≠ 0) (hy : y ≠ 0), Real.sin (angle x y) = √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖y‖)
inr :
  √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖y‖) * ‖x‖ =
    √(⟪y, y⟫ * (⟪x, x⟫ - ⟪x, y⟫ - (⟪x, y⟫ - ⟪y, y⟫)) - (⟪x, y⟫ - ⟪y, y⟫) * (⟪x, y⟫ - ⟪y, y⟫)) / (‖y‖ * ‖x - y‖) *
      ‖x - y‖
⊢ √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖y‖) * ‖x‖ =
    √(⟪y, y⟫ * ⟪x - y, x - y⟫ - ⟪y, x - y⟫ * ⟪y, x - y⟫) / (‖y‖ * ‖x - y‖) * ‖x - y‖

Tactic:
simp only [inner_sub_left, inner_sub_right, real_inner_comm x y]

Premises used: inner_sub_left, inner_sub_right, real_inner_comm
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
hxy : x ≠ y
h_sin : ∀ (x y : V) (hx : x ≠ 0) (hy : y ≠ 0), Real.sin (angle x y) = √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖y‖)
⊢ x - y ≠ 0

Tactic:
have hsub : x - y ≠ 0 := sub_ne_zero_of_ne hxy
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
hxy : x ≠ y
h_sin : ∀ (x y : V) (hx : x ≠ 0) (hy : y ≠ 0), Real.sin (angle x y) = √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖y‖)
hsub : x - y ≠ 0
inr :
  √(⟪x, x⟫ * ⟪y, y⟫ - HPow.hPow (β := ℕ) ⟪x, y⟫ 2) =
    √(⟪y, y⟫ * (⟪x, x⟫ - ⟪x, y⟫ - (⟪x, y⟫ - ⟪y, y⟫)) - HPow.hPow (β := ℕ) (⟪x, y⟫ - ⟪y, y⟫) 2)
⊢ √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖y‖) * ‖x‖ =
    √(⟪y, y⟫ * (⟪x, x⟫ - ⟪x, y⟫ - (⟪x, y⟫ - ⟪y, y⟫)) - (⟪x, y⟫ - ⟪y, y⟫) * (⟪x, y⟫ - ⟪y, y⟫)) / (‖y‖ * ‖x - y‖) *
      ‖x - y‖

Tactic:
field_simp