awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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
p₁ p₂ p : P
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
o : P := s.center
t : ℝ
hpt : (AffineMap.lineMap p₁ p₂ : (a : ℝ) → P) t = p
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
hne₁ : p ≠ p₁
hne₂ : p ≠ p₂
ht₀' : 0 < t
ht₁' : t < 1
u : V := p₁ -ᵥ o
v : V := p₂ -ᵥ o
hu : ‖u‖ = s.radius
hv : ‖v‖ = s.radius
huv : u ≠ v
hpo : p -ᵥ o = (1 - t) • u + t • v
hmem : Membership.mem (γ := Set V) (interior (Metric.closedBall 0 s.radius)) ((1 - t) • u + t • v)
⊢ ‖(1 - t) • u + t • v‖ < s.radius
have rwa : ∀ (hmem : Membership.mem (γ := Set V) (Metric.ball 0 s.radius) ((1 - t) • u + t • v)), ‖(1 - t) • u + t • v‖ < s.radius
Tactic: rwa [interior_closedBall _ (fun h : s.radius = 0 => huv <|
      (norm_eq_zero.mp (hu.trans h)).trans (norm_eq_zero.mp (hv.trans h)).symm),
    Metric.mem_ball, dist_zero_right] at hmem
Cleared hypotheses: hmem
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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
p₁ p₂ p : P
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
o : P := s.center
t : ℝ
hpt : (AffineMap.lineMap p₁ p₂ : (a : ℝ) → P) t = p
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
hne₁ : p ≠ p₁
hne₂ : p ≠ p₂
ht₀' : 0 < t
ht₁' : t < 1
u : V := p₁ -ᵥ o
v : V := p₂ -ᵥ o
hu : ‖u‖ = s.radius
hv : ‖v‖ = s.radius
huv : u ≠ v
hpo : p -ᵥ o = (1 - t) • u + t • v
hmem : Membership.mem (γ := Set V) (interior (Metric.closedBall 0 s.radius)) ((1 - t) • u + t • v)
rwa :
  ∀ (hmem : Membership.mem (γ := Set V) (Metric.ball 0 s.radius) ((1 - t) • u + t • v)),
    ‖(1 - t) • u + t • v‖ < s.radius
⊢ ‖(1 - t) • u + t • v‖ < s.radius
have rwa₁ : ∀ (hmem : dist ((1 - t) • u + t • v) 0 < s.radius), ‖(1 - t) • u + t • v‖ < s.radius
Tactic: rwa [interior_closedBall _ (fun h : s.radius = 0 => huv <|
      (norm_eq_zero.mp (hu.trans h)).trans (norm_eq_zero.mp (hv.trans h)).symm),
    Metric.mem_ball, dist_zero_right] at hmem
Cleared hypotheses: hmem
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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
p₁ p₂ p : P
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
o : P := s.center
t : ℝ
hpt : (AffineMap.lineMap p₁ p₂ : (a : ℝ) → P) t = p
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
hne₁ : p ≠ p₁
hne₂ : p ≠ p₂
ht₀' : 0 < t
ht₁' : t < 1
u : V := p₁ -ᵥ o
v : V := p₂ -ᵥ o
hu : ‖u‖ = s.radius
hv : ‖v‖ = s.radius
huv : u ≠ v
hpo : p -ᵥ o = (1 - t) • u + t • v
hmem : Membership.mem (γ := Set V) (interior (Metric.closedBall 0 s.radius)) ((1 - t) • u + t • v)
rwa :
  ∀ (hmem : Membership.mem (γ := Set V) (Metric.ball 0 s.radius) ((1 - t) • u + t • v)),
    ‖(1 - t) • u + t • v‖ < s.radius
rwa₁ : ∀ (hmem : dist ((1 - t) • u + t • v) 0 < s.radius), ‖(1 - t) • u + t • v‖ < s.radius
⊢ ‖(1 - t) • u + t • v‖ < s.radius
have rwa₂ : ∀ (hmem : ‖(1 - t) • u + t • v‖ < s.radius), ‖(1 - t) • u + t • v‖ < s.radius
Tactic: rwa [interior_closedBall _ (fun h : s.radius = 0 => huv <|
      (norm_eq_zero.mp (hu.trans h)).trans (norm_eq_zero.mp (hv.trans h)).symm),
    Metric.mem_ball, dist_zero_right] at hmem
Cleared hypotheses: hmem
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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₂ : P
hp₁ : p₁ ∈ s
hp₂ : dist p₂ s.center ≤ s.radius
⊢ 0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫ ∨ p₁ = p₂
have pos : ∀ (h : p₁ = p₂), 0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫ ∨ p₁ = p₂
Tactic: by_cases h : p₁ = p₂
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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₂ : P
hp₁ : p₁ ∈ s
hp₂ : dist p₂ s.center ≤ s.radius
pos : ∀ (h : p₁ = p₂), 0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫ ∨ p₁ = p₂
⊢ 0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫ ∨ p₁ = p₂
have neg : ∀ (h : ¬p₁ = p₂), 0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫ ∨ p₁ = p₂
Tactic: by_cases h : p₁ = p₂
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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₂ : P
hp₁ : p₁ ∈ s
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
⊢ 0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫ ∨ p₁ = p₂
have neg : 0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫
Tactic: refine Or.inl ?_
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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₂ : P
hp₁ : p₁ ∈ s
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
⊢ 0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫
have hp₃ : dist p₁ s.center = s.radius
Tactic: rw [mem_sphere] at hp₁
Cleared hypotheses: hp₁, hp₂, h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
⊢ 0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫
have neg : ⟪p₂ -ᵥ s.center, p₁ -ᵥ s.center⟫ < ‖p₁ -ᵥ s.center‖ * ‖p₁ -ᵥ s.center‖
Tactic: rw [← vsub_sub_vsub_cancel_right p₁ p₂ s.center, inner_sub_left,
    real_inner_self_eq_norm_mul_norm, sub_pos]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
⊢ ⟪p₂ -ᵥ s.center, p₁ -ᵥ s.center⟫ < ‖p₁ -ᵥ s.center‖ * ‖p₁ -ᵥ s.center‖
have neg : ‖p₂ -ᵥ s.center‖ ≤ ‖p₁ -ᵥ s.center‖
Tactic: refine lt_of_le_of_ne
    ((real_inner_le_norm _ _).trans (mul_le_mul_of_nonneg_right ?_ (norm_nonneg _))) ?_
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
neg : ‖p₂ -ᵥ s.center‖ ≤ ‖p₁ -ᵥ s.center‖
⊢ ⟪p₂ -ᵥ s.center, p₁ -ᵥ s.center⟫ < ‖p₁ -ᵥ s.center‖ * ‖p₁ -ᵥ s.center‖
have neg₁ : ⟪p₂ -ᵥ s.center, p₁ -ᵥ s.center⟫ ≠ ‖p₁ -ᵥ s.center‖ * ‖p₁ -ᵥ s.center‖
Tactic: refine lt_of_le_of_ne
    ((real_inner_le_norm _ _).trans (mul_le_mul_of_nonneg_right ?_ (norm_nonneg _))) ?_
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
⊢ ‖p₂ -ᵥ s.center‖ ≤ ‖p₁ -ᵥ s.center‖
have neg : dist p₂ s.center ≤ ‖p₁ -ᵥ s.center‖
Tactic: rwa [← dist_eq_norm_vsub, ← dist_eq_norm_vsub, hp₁]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
neg : dist p₂ s.center ≤ ‖p₁ -ᵥ s.center‖
⊢ ‖p₂ -ᵥ s.center‖ ≤ ‖p₁ -ᵥ s.center‖
have neg₁ : dist p₂ s.center ≤ dist p₁ s.center
Tactic: rwa [← dist_eq_norm_vsub, ← dist_eq_norm_vsub, hp₁]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
⊢ ⟪p₂ -ᵥ s.center, p₁ -ᵥ s.center⟫ ≠ ‖p₁ -ᵥ s.center‖ * ‖p₁ -ᵥ s.center‖
have neg : ∀ (hp₂' : dist p₂ s.center < s.radius), ⟪p₂ -ᵥ s.center, p₁ -ᵥ s.center⟫ ≠ ‖p₁ -ᵥ s.center‖ * ‖p₁ -ᵥ s.center‖
Tactic: rcases hp₂.lt_or_eq with (hp₂' | hp₂')
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
neg : ∀ (hp₂' : dist p₂ s.center < s.radius), ⟪p₂ -ᵥ s.center, p₁ -ᵥ s.center⟫ ≠ ‖p₁ -ᵥ s.center‖ * ‖p₁ -ᵥ s.center‖
⊢ ⟪p₂ -ᵥ s.center, p₁ -ᵥ s.center⟫ ≠ ‖p₁ -ᵥ s.center‖ * ‖p₁ -ᵥ s.center‖
have neg₁ : ∀ (hp₂' : dist p₂ s.center = s.radius), ⟪p₂ -ᵥ s.center, p₁ -ᵥ s.center⟫ ≠ ‖p₁ -ᵥ s.center‖ * ‖p₁ -ᵥ s.center‖
Tactic: rcases hp₂.lt_or_eq with (hp₂' | hp₂')
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
hp₂' : dist p₂ s.center < s.radius
⊢ ⟪p₂ -ᵥ s.center, p₁ -ᵥ s.center⟫ ≠ ‖p₁ -ᵥ s.center‖ * ‖p₁ -ᵥ s.center‖
have neg : ‖p₂ -ᵥ s.center‖ < ‖p₁ -ᵥ s.center‖
Tactic: refine ((real_inner_le_norm _ _).trans_lt (mul_lt_mul_of_pos_right ?_ ?_)).ne
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
hp₂' : dist p₂ s.center < s.radius
neg : ‖p₂ -ᵥ s.center‖ < ‖p₁ -ᵥ s.center‖
⊢ ⟪p₂ -ᵥ s.center, p₁ -ᵥ s.center⟫ ≠ ‖p₁ -ᵥ s.center‖ * ‖p₁ -ᵥ s.center‖
have neg₁ : 0 < ‖p₁ -ᵥ s.center‖
Tactic: refine ((real_inner_le_norm _ _).trans_lt (mul_lt_mul_of_pos_right ?_ ?_)).ne
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
hp₂' : dist p₂ s.center < s.radius
⊢ ‖p₂ -ᵥ s.center‖ < ‖p₁ -ᵥ s.center‖
have neg : ∀ (hp₂' : dist p₂ s.center < dist p₁ s.center), ‖p₂ -ᵥ s.center‖ < ‖p₁ -ᵥ s.center‖
Tactic: rwa [← hp₁, @dist_eq_norm_vsub V, @dist_eq_norm_vsub V] at hp₂'
Cleared hypotheses: hp₂'
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
hp₂' : dist p₂ s.center < s.radius
neg : ∀ (hp₂' : dist p₂ s.center < dist p₁ s.center), ‖p₂ -ᵥ s.center‖ < ‖p₁ -ᵥ s.center‖
⊢ ‖p₂ -ᵥ s.center‖ < ‖p₁ -ᵥ s.center‖
have neg₁ : ∀ (hp₂' : ‖p₂ -ᵥ s.center‖ < dist p₁ s.center), ‖p₂ -ᵥ s.center‖ < ‖p₁ -ᵥ s.center‖
Tactic: rwa [← hp₁, @dist_eq_norm_vsub V, @dist_eq_norm_vsub V] at hp₂'
Cleared hypotheses: hp₂'
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
hp₂' : dist p₂ s.center < s.radius
neg : ∀ (hp₂' : dist p₂ s.center < dist p₁ s.center), ‖p₂ -ᵥ s.center‖ < ‖p₁ -ᵥ s.center‖
neg₁ : ∀ (hp₂' : ‖p₂ -ᵥ s.center‖ < dist p₁ s.center), ‖p₂ -ᵥ s.center‖ < ‖p₁ -ᵥ s.center‖
⊢ ‖p₂ -ᵥ s.center‖ < ‖p₁ -ᵥ s.center‖
have neg₂ : ∀ (hp₂' : ‖p₂ -ᵥ s.center‖ < ‖p₁ -ᵥ s.center‖), ‖p₂ -ᵥ s.center‖ < ‖p₁ -ᵥ s.center‖
Tactic: rwa [← hp₁, @dist_eq_norm_vsub V, @dist_eq_norm_vsub V] at hp₂'
Cleared hypotheses: hp₂'
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
hp₂' : dist p₂ s.center < s.radius
⊢ 0 < ‖p₁ -ᵥ s.center‖
have neg : p₁ ≠ s.center
Tactic: rw [norm_pos_iff, vsub_ne_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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₂ : dist p₂ s.center ≤ s.radius
hp₂' : dist p₂ s.center < s.radius
hp₁ : dist s.center s.center = s.radius
h : ¬s.center = p₂
⊢ False
have hp₂'₁ : dist p₂ s.center < dist s.center s.center
Tactic: rw [← hp₁] at hp₂'
Cleared hypotheses: hp₂', hp₁, h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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₂ : dist p₂ s.center ≤ s.radius
hp₂' : dist p₂ s.center < dist s.center s.center
hp₁ : dist s.center s.center = s.radius
h : ¬s.center = p₂
⊢ False
have neg : dist p₂ s.center < 0
Tactic: refine (dist_nonneg.not_gt : ¬dist p₂ s.center < 0) ?_
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
hp₂' : dist p₂ s.center = s.radius
⊢ ⟪p₂ -ᵥ s.center, p₁ -ᵥ s.center⟫ ≠ ‖p₁ -ᵥ s.center‖ * ‖p₁ -ᵥ s.center‖
have hp₂'₁ : ‖p₂ -ᵥ s.center‖ = ‖p₁ -ᵥ s.center‖
Tactic: rw [← hp₁, @dist_eq_norm_vsub V, @dist_eq_norm_vsub V] at hp₂'
Cleared hypotheses: hp₂'
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
hp₂' : ‖p₂ -ᵥ s.center‖ = ‖p₁ -ᵥ s.center‖
⊢ ⟪p₂ -ᵥ s.center, p₁ -ᵥ s.center⟫ ≠ ‖p₁ -ᵥ s.center‖ * ‖p₁ -ᵥ s.center‖
have neg : ⟪p₂ -ᵥ s.center, p₁ -ᵥ s.center⟫ ≠ ‖p₂ -ᵥ s.center‖ * ‖p₁ -ᵥ s.center‖
Tactic: nth_rw 1 [← hp₂']
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
hp₂' : ‖p₂ -ᵥ s.center‖ = ‖p₁ -ᵥ s.center‖
⊢ ⟪p₂ -ᵥ s.center, p₁ -ᵥ s.center⟫ ≠ ‖p₂ -ᵥ s.center‖ * ‖p₁ -ᵥ s.center‖
have neg : p₁ ≠ s.center
Tactic: rw [Ne, inner_eq_norm_mul_iff_real, hp₂', ← sub_eq_zero, ← smul_sub,
        vsub_sub_vsub_cancel_right, ← Ne, smul_ne_zero_iff, vsub_ne_zero,
        and_iff_left (Ne.symm h), norm_ne_zero_iff, vsub_ne_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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₂ : dist p₂ s.center ≤ s.radius
hp₁ : dist s.center s.center = s.radius
h : ¬s.center = p₂
hp₂' : ‖p₂ -ᵥ s.center‖ = ‖s.center -ᵥ s.center‖
⊢ False
have neg : p₂ = s.center
Tactic: refine h (Eq.symm ?_)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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₂ : P
hp₁ : p₁ ∈ s
hp₂ : dist p₂ s.center ≤ s.radius
⊢ 0 ≤ ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫
have inl : ∀ (h : 0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫), 0 ≤ ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫
Tactic: rcases inner_pos_or_eq_of_dist_le_radius hp₁ hp₂ with (h | rfl)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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₂ : P
hp₁ : p₁ ∈ s
hp₂ : dist p₂ s.center ≤ s.radius
inl : ∀ (h : 0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫), 0 ≤ ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫
⊢ 0 ≤ ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫
have inr : ∀ (hp₂ : dist p₁ s.center ≤ s.radius), 0 ≤ ⟪p₁ -ᵥ p₁, p₁ -ᵥ s.center⟫
Tactic: rcases inner_pos_or_eq_of_dist_le_radius hp₁ hp₂ with (h | rfl)
Cleared hypotheses: p₂, hp₂
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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₂ : P
hp₁ : p₁ ∈ s
hp₂ : dist p₂ s.center < s.radius
⊢ 0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫
have pos : ∀ (h : p₁ = p₂), 0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫
Tactic: by_cases h : p₁ = p₂
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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₂ : P
hp₁ : p₁ ∈ s
hp₂ : dist p₂ s.center < s.radius
pos : ∀ (h : p₁ = p₂), 0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫
⊢ 0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫
have neg : ∀ (h : ¬p₁ = p₂), 0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫
Tactic: by_cases h : p₁ = p₂
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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₂ : P
hp₁ : p₁ ∈ s
hp₂ : dist p₂ s.center < s.radius
h : p₁ = p₂
⊢ 0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫
have hp₃ : dist p₂ s.center = s.radius
Tactic: rw [h, mem_sphere] at hp₁
Cleared hypotheses: hp₁, hp₂, h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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
p₁ p₂ : P
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₁p₂ : p₁ ≠ p₂
⊢ ‖p₁ -ᵥ s.center‖ = s.radius
have rw : dist s.center p₁ = s.radius
Tactic: rw [← dist_eq_norm_vsub']
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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
p₁ p₂ : P
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₁p₂ : p₁ ≠ p₂
⊢ 0 < ⟪p₂ -ᵥ p₁, s.center -ᵥ p₁⟫
have hp₁' : ‖p₁ -ᵥ s.center‖ = s.radius
Tactic: have hp₁' : ‖p₁ -ᵥ s.center‖ = s.radius := by rw [← dist_eq_norm_vsub']; exact mem_sphere'.mp hp₁
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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
p₁ p₂ : P
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₁p₂ : p₁ ≠ p₂
hp₁' : ‖p₁ -ᵥ s.center‖ = s.radius
⊢ ‖p₂ -ᵥ s.center‖ = s.radius
have rw : dist s.center p₂ = s.radius
Tactic: rw [← dist_eq_norm_vsub']
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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
p₁ p₂ : P
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₁p₂ : p₁ ≠ p₂
hp₁' : ‖p₁ -ᵥ s.center‖ = s.radius
⊢ 0 < ⟪p₂ -ᵥ p₁, s.center -ᵥ p₁⟫
have hp₂' : ‖p₂ -ᵥ s.center‖ = s.radius
Tactic: have hp₂' : ‖p₂ -ᵥ s.center‖ = s.radius := by rw [← dist_eq_norm_vsub']; exact mem_sphere'.mp hp₂
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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
p₁ p₂ : P
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₁p₂ : p₁ ≠ p₂
hp₁' : ‖p₁ -ᵥ s.center‖ = s.radius
hp₂' : ‖p₂ -ᵥ s.center‖ = s.radius
⊢ HPow.hPow (β := ℕ) ‖p₂ -ᵥ s.center‖ 2 =
    HPow.hPow (β := ℕ) ‖p₂ -ᵥ p₁‖ 2 + 2 * ⟪p₂ -ᵥ p₁, p₁ -ᵥ s.center⟫ + HPow.hPow (β := ℕ) ‖p₁ -ᵥ s.center‖ 2
have rw : HPow.hPow (β := ℕ) ‖p₂ -ᵥ p₁ + (p₁ -ᵥ s.center)‖ 2 =
  HPow.hPow (β := ℕ) ‖p₂ -ᵥ p₁‖ 2 + 2 * ⟪p₂ -ᵥ p₁, p₁ -ᵥ s.center⟫ + HPow.hPow (β := ℕ) ‖p₁ -ᵥ s.center‖ 2
Tactic: rw [← vsub_add_vsub_cancel p₂ p₁ s.center, norm_add_sq_real]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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
p₁ p₂ : P
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₁p₂ : p₁ ≠ p₂
hp₁' : ‖p₁ -ᵥ s.center‖ = s.radius
hp₂' : ‖p₂ -ᵥ s.center‖ = s.radius
rw :
  HPow.hPow (β := ℕ) ‖p₂ -ᵥ p₁ + (p₁ -ᵥ s.center)‖ 2 =
    HPow.hPow (β := ℕ) ‖p₂ -ᵥ p₁‖ 2 + 2 * ⟪p₂ -ᵥ p₁, p₁ -ᵥ s.center⟫ + HPow.hPow (β := ℕ) ‖p₁ -ᵥ s.center‖ 2
⊢ HPow.hPow (β := ℕ) ‖p₂ -ᵥ s.center‖ 2 =
    HPow.hPow (β := ℕ) ‖p₂ -ᵥ p₁‖ 2 + 2 * ⟪p₂ -ᵥ p₁, p₁ -ᵥ s.center⟫ + HPow.hPow (β := ℕ) ‖p₁ -ᵥ s.center‖ 2
have rw₁ : HPow.hPow (β := ℕ) ‖p₂ -ᵥ p₁‖ 2 + 2 * ⟪p₂ -ᵥ p₁, p₁ -ᵥ s.center⟫ + HPow.hPow (β := ℕ) ‖p₁ -ᵥ s.center‖ 2 =
  HPow.hPow (β := ℕ) ‖p₂ -ᵥ p₁‖ 2 + 2 * ⟪p₂ -ᵥ p₁, p₁ -ᵥ s.center⟫ + HPow.hPow (β := ℕ) ‖p₁ -ᵥ s.center‖ 2
Tactic: rw [← vsub_add_vsub_cancel p₂ p₁ s.center, norm_add_sq_real]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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
p₁ p₂ : P
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₁p₂ : p₁ ≠ p₂
hp₁' : ‖p₁ -ᵥ s.center‖ = s.radius
hp₂' : ‖p₂ -ᵥ s.center‖ = s.radius
⊢ 0 < ⟪p₂ -ᵥ p₁, s.center -ᵥ p₁⟫
have hd : HPow.hPow (β := ℕ) ‖p₂ -ᵥ s.center‖ 2 =
  HPow.hPow (β := ℕ) ‖p₂ -ᵥ p₁‖ 2 + 2 * ⟪p₂ -ᵥ p₁, p₁ -ᵥ s.center⟫ + HPow.hPow (β := ℕ) ‖p₁ -ᵥ s.center‖ 2
Tactic: have hd : ‖p₂ -ᵥ s.center‖ ^ 2 =
      ‖p₂ -ᵥ p₁‖ ^ 2 + 2 * ⟪p₂ -ᵥ p₁, p₁ -ᵥ s.center⟫ + ‖p₁ -ᵥ s.center‖ ^ 2 := by
    rw [← vsub_add_vsub_cancel p₂ p₁ s.center, norm_add_sq_real]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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
p₁ p₂ : P
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₁p₂ : p₁ ≠ p₂
hp₁' : ‖p₁ -ᵥ s.center‖ = s.radius
hp₂' : ‖p₂ -ᵥ s.center‖ = s.radius
hd :
  HPow.hPow (β := ℕ) ‖p₂ -ᵥ s.center‖ 2 =
    HPow.hPow (β := ℕ) ‖p₂ -ᵥ p₁‖ 2 + 2 * ⟪p₂ -ᵥ p₁, p₁ -ᵥ s.center⟫ + HPow.hPow (β := ℕ) ‖p₁ -ᵥ s.center‖ 2
⊢ 0 < ⟪p₂ -ᵥ p₁, s.center -ᵥ p₁⟫
have hd₁ : HPow.hPow (β := ℕ) s.radius 2 =
  HPow.hPow (β := ℕ) ‖p₂ -ᵥ p₁‖ 2 + 2 * -⟪p₂ -ᵥ p₁, s.center -ᵥ p₁⟫ + HPow.hPow (β := ℕ) s.radius 2
Tactic: rw [hp₂', hp₁', ← neg_vsub_eq_vsub_rev s.center p₁, inner_neg_right] at hd
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (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
p₁ p₂ : P
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₁p₂ : p₁ ≠ p₂
hp₁' : ‖p₁ -ᵥ s.center‖ = s.radius
hp₂' : ‖p₂ -ᵥ s.center‖ = s.radius
hd :
  HPow.hPow (β := ℕ) s.radius 2 =
    HPow.hPow (β := ℕ) ‖p₂ -ᵥ p₁‖ 2 + 2 * -⟪p₂ -ᵥ p₁, s.center -ᵥ p₁⟫ + HPow.hPow (β := ℕ) s.radius 2
⊢ 0 < ⟪p₂ -ᵥ p₁, s.center -ᵥ p₁⟫
have nlinarith : ⟪p₂ -ᵥ p₁, s.center -ᵥ p₁⟫ ≤ 0 →
  -(HPow.hPow (β := ℕ) s.radius 2 -
            (HPow.hPow (β := ℕ) ‖p₂ -ᵥ p₁‖ 2 + 2 * -⟪p₂ -ᵥ p₁, s.center -ᵥ p₁⟫ + HPow.hPow (β := ℕ) s.radius 2)) +
        2 * (⟪p₂ -ᵥ p₁, s.center -ᵥ p₁⟫ - 0) +
      (0 - HPow.hPow (β := ℕ) ‖p₂ -ᵥ p₁‖ 2) =
    0
Tactic: nlinarith [sq_pos_of_pos (norm_pos_iff.mpr (vsub_ne_zero.mpr hp₁p₂.symm))]