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 : Sphere P
as : AffineSubspace ℝ P
p : P
hpar : as ∥ s.orthRadius p
hp : p ∈ s
q : P
hqs : q ∈ s
hqas : q ∈ as
hqo : as ≤ s.orthRadius q
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
hrad : s.radius ≠ 0
⊢ as = s.orthRadius p ∨ as = s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p)
have inr : ∀ (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)),
  Eq (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius p) ∨
    Eq (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p))
Tactic: obtain rfl : as = s.orthRadius q := by
    refine eq_of_direction_eq_of_nonempty_of_le ?_ ⟨q, hqas⟩ hqo
    rw [hpar.direction_eq, direction_orthRadius, direction_orthRadius]
    congr 1
    rcases eq_or_ne r 0 with rfl | hr0
    · simp_all
    · rw [hr, Submodule.span_singleton_smul_eq hr0.isUnit]
Cleared hypotheses: as, hpar, hqas, hqo
-- 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 : Sphere P
p : P
hp : p ∈ s
q : P
hqs : q ∈ s
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
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)
⊢ Eq (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius p) ∨
    Eq (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p))
have inr : ∀ (hr : q -ᵥ s.center = HSMul.hSMul (α := ℝ) 0 (p -ᵥ s.center)),
  Eq (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius p) ∨
    Eq (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p))
Tactic: rcases eq_or_ne r 0 with rfl | hr0
Cleared hypotheses: r, hr
-- 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 : Sphere P
p : P
hp : p ∈ s
q : P
hqs : q ∈ s
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
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)
inr :
  ∀ (hr : q -ᵥ s.center = HSMul.hSMul (α := ℝ) 0 (p -ᵥ s.center)),
    Eq (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius p) ∨
      Eq (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p))
⊢ Eq (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius p) ∨
    Eq (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p))
have inr₁ : ∀ (hr0 : r ≠ 0),
  Eq (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius p) ∨
    Eq (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p))
Tactic: rcases eq_or_ne r 0 with rfl | hr0
-- 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 : Sphere P
p : P
hp : p ∈ s
q : P
hqs : q ∈ s
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
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)
hr0 : r ≠ 0
⊢ ‖q -ᵥ s.center‖ = ‖r • (p -ᵥ s.center)‖
have rw : ‖r • (p -ᵥ s.center)‖ = ‖r • (p -ᵥ s.center)‖
Tactic: rw [hr]
-- 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 : Sphere P
p : P
hp : p ∈ s
q : P
hqs : q ∈ s
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
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)
hr0 : r ≠ 0
⊢ Eq (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius p) ∨
    Eq (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p))
have hr' : ‖q -ᵥ s.center‖ = ‖r • (p -ᵥ s.center)‖
Tactic: have hr' : ‖q -ᵥ s.center‖ = ‖r • (p -ᵥ s.center)‖ := by
      rw [hr]
-- 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 : Sphere P
p : P
hp : p ∈ s
q : P
hqs : q ∈ s
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
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)
hr0 : r ≠ 0
hr' : ‖q -ᵥ s.center‖ = ‖r • (p -ᵥ s.center)‖
⊢ Eq (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius p) ∨
    Eq (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p))
have hr'₁ : |r| = 1
Tactic: simp_rw [norm_smul, Real.norm_eq_abs, ← dist_eq_norm_vsub, mem_sphere.1 hp,
      mem_sphere.1 hqs, right_eq_mul₀ hrad] at hr'
Cleared hypotheses: hr'
-- 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 : Sphere P
p : P
hp : p ∈ s
q : P
hqs : q ∈ s
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
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)
hr0 : r ≠ 0
hr' : |r| = 1
⊢ Eq (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius p) ∨
    Eq (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p))
have inr : ∀ (hr : q -ᵥ s.center = HSMul.hSMul (α := ℝ) 1 (p -ᵥ s.center)) (hr0 : Ne (α := ℝ) 1 0) (hr' : Eq (α := ℝ) |1| 1),
  Eq (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius p) ∨
    Eq (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p))
Tactic: rcases eq_or_eq_neg_of_abs_eq hr' with rfl | rfl
Cleared hypotheses: r, hr, hr0, hr'
-- 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 : Sphere P
p : P
hp : p ∈ s
q : P
hqs : q ∈ s
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
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)
hr0 : r ≠ 0
hr' : |r| = 1
inr :
  ∀ (hr : q -ᵥ s.center = HSMul.hSMul (α := ℝ) 1 (p -ᵥ s.center)) (hr0 : Ne (α := ℝ) 1 0) (hr' : Eq (α := ℝ) |1| 1),
    Eq (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius p) ∨
      Eq (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p))
⊢ Eq (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius p) ∨
    Eq (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p))
have inr₁ : ∀ (hr : q -ᵥ s.center = HSMul.hSMul (α := ℝ) (-1) (p -ᵥ s.center)) (hr0 : Ne (α := ℝ) (-1) 0)
  (hr' : Eq (α := ℝ) |(-1)| 1),
  Eq (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius p) ∨
    Eq (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p))
Tactic: rcases eq_or_eq_neg_of_abs_eq hr' with rfl | rfl
Cleared hypotheses: r, hr, hr0, hr'
-- 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 : 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 -ᵥ s.center = HSMul.hSMul (α := ℝ) (-1) (p -ᵥ s.center)
hr0 : Ne (α := ℝ) (-1) 0
hr' : Eq (α := ℝ) |(-1)| 1
⊢ Eq (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius p) ∨
    Eq (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p))
have inr : Eq (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p))
Tactic: right
-- 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 : 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 -ᵥ s.center = HSMul.hSMul (α := ℝ) (-1) (p -ᵥ s.center)
hr0 : Ne (α := ℝ) (-1) 0
hr' : Eq (α := ℝ) |(-1)| 1
⊢ Eq (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p))
have h : (Equiv.pointReflection s.center : (a : P) → P) p = q
Tactic: convert! rfl
-- 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 : 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 -ᵥ s.center = HSMul.hSMul (α := ℝ) (-1) (p -ᵥ s.center)
hr0 : Ne (α := ℝ) (-1) 0
hr' : Eq (α := ℝ) |(-1)| 1
⊢ (Equiv.pointReflection s.center : (a : P) → P) p = q
have hr₁ : q = HSMul.hSMul (α := ℝ) (-1) (p -ᵥ s.center) +ᵥ s.center
Tactic: rw [← eq_vadd_iff_vsub_eq] at hr
Cleared hypotheses: hr, hr0, hr'
-- 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 : 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 = q
have h : (Equiv.pointReflection s.center : (a : P) → P) p = HSMul.hSMul (α := ℝ) (-1) (p -ᵥ s.center) +ᵥ s.center
Tactic: rw [hr]
-- 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 : 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)
have refine : s.IsTangentAt (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) as
Tactic: refine h.eq_of_isTangentAt ?_
-- 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 : 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.IsTangentAt (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) as
have h' : s.IsTangent as
Tactic: have h' := h.isTangent
-- 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 : 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
⊢ s.IsTangentAt (↑((orthogonalProjection as : (a : P) → ↥as) s.center) : P) as
have rwa : ∀ (h' : 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'
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
as : AffineSubspace ℝ P
s : Sphere P
h : Membership.mem (γ := Set (AffineSubspace ℝ P)) s.tangentSet as
⊢ s.IsTangent as
have rcases : ∀ (p : P) (hps : p ∈ Metric.sphere s.center s.radius), s.IsTangent (s.orthRadius p)
Tactic: rcases h with ⟨p, hps, rfl⟩
Cleared hypotheses: as, 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
⊢ Eq (α := Set (AffineSubspace ℝ P)) (s₁.commonIntTangents s₂ ∪ s₁.commonExtTangents s₂) (s₁.commonTangents s₂)
have 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
Tactic: ext as
-- 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
as : AffineSubspace ℝ P
⊢ Membership.mem (γ := Set (AffineSubspace ℝ P)) (s₁.commonIntTangents s₂ ∪ s₁.commonExtTangents s₂) as ↔
    Membership.mem (γ := Set (AffineSubspace ℝ P)) (s₁.commonTangents s₂) as
have 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
Tactic: rw [Set.mem_union, mem_commonIntTangents_iff, mem_commonExtTangents_iff, ← and_or_left,
    and_iff_left_iff_imp]
-- 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
as : AffineSubspace ℝ P
⊢ (∃ p ∈ as, Wbtw ℝ s₁.center p s₂.center) ∨ ∀ p ∈ as, ¬Sbtw ℝ s₁.center p s₂.center
have 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
Tactic: by_cases! h : ∃ p ∈ as, Wbtw ℝ s₁.center p 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
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
⊢ (∃ p ∈ as, Wbtw ℝ s₁.center p s₂.center) ∨ ∀ p ∈ as, ¬Sbtw ℝ s₁.center p s₂.center
have 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
Tactic: by_cases! h : ∃ p ∈ as, Wbtw ℝ s₁.center p 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
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
have neg : ∀ p ∈ as, ¬Sbtw ℝ s₁.center p s₂.center
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
⊢ s₁.IsExtTangentAt s₂ s₁.center ↔ s₁.radius = 0 ∧ s₁.center ∈ s₂
have refine_1 : s₁.IsExtTangentAt s₂ s₁.center → s₁.radius = 0 ∧ s₁.center ∈ s₂
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
refine_1 : s₁.IsExtTangentAt s₂ s₁.center → s₁.radius = 0 ∧ s₁.center ∈ s₂
⊢ s₁.IsExtTangentAt s₂ s₁.center ↔ s₁.radius = 0 ∧ s₁.center ∈ s₂
have refine_2 : s₁.radius = 0 ∧ s₁.center ∈ s₂ → s₁.IsExtTangentAt s₂ s₁.center
Tactic: refine ⟨?_, ?_⟩
-- 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
h₁ : s₁.center ∈ s₁
h₂ : s₁.center ∈ s₂
⊢ s₁.radius = 0 ∧ s₁.center ∈ s₂
have h₃ : s₁.radius = 0
Tactic: rw [center_mem_iff] at h₁
Cleared hypotheses: 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
hr : s₁.radius = 0
hc : s₁.center ∈ s₂
⊢ s₁.IsExtTangentAt s₂ s₁.center
have refine_2 : s₁.center ∈ s₁
Tactic: refine ⟨?_, hc, ?_⟩
-- 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
hr : s₁.radius = 0
hc : s₁.center ∈ s₂
refine_2 : s₁.center ∈ s₁
⊢ s₁.IsExtTangentAt s₂ s₁.center
have refine_2₁ : Wbtw ℝ s₁.center s₁.center s₂.center
Tactic: refine ⟨?_, hc, ?_⟩
-- 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
hr : s₁.radius = 0
hc : s₁.center ∈ s₂
refine_2 : s₁.radius = 0
⊢ s₁.center ∈ s₁
have refine_2₁ : Eq (α := ℝ) 0 0
Tactic: rw [center_mem_iff, hr]
-- 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₁.IsIntTangentAt s₂ s₁.center ↔ s₁.radius = 0 ∧ s₁.center ∈ s₂
have refine_1 : s₁.IsIntTangentAt s₂ s₁.center → s₁.radius = 0 ∧ s₁.center ∈ s₂
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
refine_1 : s₁.IsIntTangentAt s₂ s₁.center → s₁.radius = 0 ∧ s₁.center ∈ s₂
⊢ s₁.IsIntTangentAt s₂ s₁.center ↔ s₁.radius = 0 ∧ s₁.center ∈ s₂
have refine_2 : s₁.radius = 0 ∧ s₁.center ∈ s₂ → s₁.IsIntTangentAt s₂ 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
hr : s₁.radius = 0
hc : s₁.center ∈ s₂
⊢ s₁.IsIntTangentAt s₂ s₁.center
have refine_2 : s₁.center ∈ s₁
Tactic: refine ⟨?_, hc, ?_⟩
-- 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
hr : s₁.radius = 0
hc : s₁.center ∈ s₂
refine_2 : s₁.center ∈ s₁
⊢ s₁.IsIntTangentAt s₂ s₁.center
have refine_2₁ : Wbtw ℝ s₂.center s₁.center s₁.center
Tactic: refine ⟨?_, hc, ?_⟩
-- 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₂
⊢ s₂.IsExtTangent s₁
have rcases : ∀ (p : P) (hp : s₁.IsExtTangentAt s₂ p), s₂.IsExtTangent s₁
Tactic: rcases h with ⟨p, hp⟩
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 : Sphere P
⊢ s.IsIntTangent s ↔ 0 ≤ s.radius
have simp_rw : (∃ (p : P), p ∈ s) ↔ 0 ≤ s.radius
Tactic: simp_rw [IsIntTangent, isIntTangentAt_self_iff_mem]
-- 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 : Sphere P
⊢ (∃ (p : P), p ∈ s) ↔ 0 ≤ s.radius
have rw : (∃ (p : P), p ∈ s) ↔ (Metric.sphere s.center s.radius).Nonempty
Tactic: rw [← nonempty_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 : s₁.IsExtTangent s₂
⊢ dist s₁.center s₂.center = s₁.radius + s₂.radius
have 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
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 p s₂.center
⊢ dist s₁.center s₂.center = s₁.radius + s₂.radius
have h₃ : dist s₁.center p + dist p s₂.center = dist s₁.center s₂.center
Tactic: rw [← dist_add_dist_eq_iff] 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
p : P
h₁ : p ∈ s₁
h₂ : p ∈ s₂
h : dist s₁.center p + dist p s₂.center = dist s₁.center s₂.center
⊢ dist s₁.center s₂.center = s₁.radius + s₂.radius
have rw : dist s₁.center p + dist p s₂.center = 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
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
⊢ dist s₁.center s₂.center = s₁.radius + s₂.radius
have rw₁ : s₁.radius + dist p s₂.center = s₁.radius + s₂.radius
Tactic: rw [← h, mem_sphere'.1 h₁, h₂]