awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (hypothesis)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
y : E
hy : ‖y - x‖ ≤ r
this : ContinuousWithinAt.{0, u_1} (Y := E) (fun (c : ℝ) ↦ c • (y - x) + x) (Ico 0 1) 1
c : ℝ
hc0 : 0 ≤ c
hc1 : c < 1
⊢ ‖y - x‖ * c < r * 1
have hr₁ : 0 < r
Tactic: replace hr : 0 < r := ((norm_nonneg _).trans hy).lt_of_ne hr.symm
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ frontier (ball x r) = sphere x r
have rw : closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball x r) \ interior (ball x r) = sphere x r
Tactic: rw [frontier, closure_ball x hr, isOpen_ball.interior_eq, closedBall_diff_ball]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
rw : closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball x r) \ interior (ball x r) = sphere x r
⊢ frontier (ball x r) = sphere x r
have rw₁ : closedBall x r \ interior (ball x r) = sphere x r
Tactic: rw [frontier, closure_ball x hr, isOpen_ball.interior_eq, closedBall_diff_ball]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
rw : closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball x r) \ interior (ball x r) = sphere x r
rw₁ : closedBall x r \ interior (ball x r) = sphere x r
⊢ frontier (ball x r) = sphere x r
have rw₂ : closedBall x r \ ball x r = sphere x r
Tactic: rw [frontier, closure_ball x hr, isOpen_ball.interior_eq, closedBall_diff_ball]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
rw : closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball x r) \ interior (ball x r) = sphere x r
rw₁ : closedBall x r \ interior (ball x r) = sphere x r
rw₂ : closedBall x r \ ball x r = sphere x r
⊢ frontier (ball x r) = sphere x r
have rw₃ : sphere x r = sphere x r
Tactic: rw [frontier, closure_ball x hr, isOpen_ball.interior_eq, closedBall_diff_ball]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ interior (closedBall x r) = ball x r
have inl : ∀ (hr : r < 0), interior (closedBall x r) = ball x r
Tactic: rcases hr.lt_or_gt with hr | hr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
inl : ∀ (hr : r < 0), interior (closedBall x r) = ball x r
⊢ interior (closedBall x r) = ball x r
have inr : ∀ (hr : 0 < r), interior (closedBall x r) = ball x r
Tactic: rcases hr.lt_or_gt with hr | hr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr_1 : r ≠ 0
hr : r < 0
⊢ interior (closedBall x r) = ball x r
have inl : interior ∅ = ball x r
Tactic: rw [closedBall_eq_empty.2 hr, ball_eq_empty.2 hr.le, interior_empty]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr_1 : r ≠ 0
hr : r < 0
inl : interior ∅ = ball x r
⊢ interior (closedBall x r) = ball x r
have inl₁ : Eq.{u_1 + 1} (α := Set E) (interior ∅) ∅
Tactic: rw [closedBall_eq_empty.2 hr, ball_eq_empty.2 hr.le, interior_empty]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr_1 : r ≠ 0
hr : r < 0
inl : interior ∅ = ball x r
inl₁ : Eq.{u_1 + 1} (α := Set E) (interior ∅) ∅
⊢ interior (closedBall x r) = ball x r
have inl₂ : Eq.{u_1 + 1} (α := Set E) ∅ ∅
Tactic: rw [closedBall_eq_empty.2 hr, ball_eq_empty.2 hr.le, interior_empty]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr_1 : r ≠ 0
hr : 0 < r
⊢ interior (closedBall x r) = ball x r
have inr : interior (closedBall x r) ⊆ ball x r
Tactic: refine Subset.antisymm ?_ ball_subset_interior_closedBall
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr_1 : r ≠ 0
hr : 0 < r
y : E
hy : y ∈ interior (closedBall x r)
⊢ y ∈ ball x r
have inr : ∀ (hr : dist y x < r), y ∈ ball x r
Tactic: rcases (mem_closedBall.1 <| interior_subset hy).lt_or_eq with (hr | rfl)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr_1 : r ≠ 0
hr : 0 < r
y : E
hy : y ∈ interior (closedBall x r)
inr : ∀ (hr : dist y x < r), y ∈ ball x r
⊢ y ∈ ball x r
have inr₁ : ∀ (hr : dist y x ≠ 0) (hr : 0 < dist y x) (hy : y ∈ interior (closedBall x (dist y x))), y ∈ ball x (dist y x)
Tactic: rcases (mem_closedBall.1 <| interior_subset hy).lt_or_eq with (hr | rfl)
Cleared hypotheses: r, hr_1, hr, hy
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (hypothesis)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
hr_1 : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun (c : ℝ) ↦ c • (y - x) + x
this : f ⁻¹' closedBall x (dist y x) ⊆ Icc (-1) 1
⊢ y ∈ ball x (dist y x)
have h1 : Membership.mem (γ := Set ℝ) (interior (Icc (-1) 1)) 1
Tactic: have h1 : (1 : ℝ) ∈ interior (Icc (-1 : ℝ) 1) :=
      interior_mono this (preimage_interior_subset_interior_preimage (by fun_prop) (by simpa [f]))
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
hr_1 : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun (c : ℝ) ↦ c • (y - x) + x
⊢ y ∈ ball x (dist y x)
have inr : f ⁻¹' closedBall x (dist y x) ⊆ Icc (-1) 1
Tactic: suffices f ⁻¹' closedBall x (dist y x) ⊆ Icc (-1) 1 by
    have h1 : (1 : ℝ) ∈ interior (Icc (-1 : ℝ) 1) :=
      interior_mono this (preimage_interior_subset_interior_preimage (by fun_prop) (by simpa [f]))
    simp at h1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
hr_1 : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun (c : ℝ) ↦ c • (y - x) + x
c : ℝ
hc : c ∈ f ⁻¹' closedBall x (dist y x)
⊢ Membership.mem (γ := Set ℝ) (Icc (-1) 1) c
have inr : ‖c‖ * dist y x ≤ 1 * dist y x
Tactic: rw [mem_Icc, ← abs_le, ← Real.norm_eq_abs, ← mul_le_mul_iff_left₀ hr]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ frontier (closedBall x r) = sphere x r
have rw : closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (closedBall x r) \ interior (closedBall x r) = sphere x r
Tactic: rw [frontier, closure_closedBall, interior_closedBall x hr, closedBall_diff_ball]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
rw :
  closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (closedBall x r) \ interior (closedBall x r) = sphere x r
⊢ frontier (closedBall x r) = sphere x r
have rw₁ : closedBall x r \ interior (closedBall x r) = sphere x r
Tactic: rw [frontier, closure_closedBall, interior_closedBall x hr, closedBall_diff_ball]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
rw :
  closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (closedBall x r) \ interior (closedBall x r) = sphere x r
rw₁ : closedBall x r \ interior (closedBall x r) = sphere x r
⊢ frontier (closedBall x r) = sphere x r
have rw₂ : closedBall x r \ ball x r = sphere x r
Tactic: rw [frontier, closure_closedBall, interior_closedBall x hr, closedBall_diff_ball]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
rw :
  closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (closedBall x r) \ interior (closedBall x r) = sphere x r
rw₁ : closedBall x r \ interior (closedBall x r) = sphere x r
rw₂ : closedBall x r \ ball x r = sphere x r
⊢ frontier (closedBall x r) = sphere x r
have rw₃ : sphere x r = sphere x r
Tactic: rw [frontier, closure_closedBall, interior_closedBall x hr, closedBall_diff_ball]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ interior (sphere x r) = ∅
have rw : interior (frontier (closedBall x r)) = ∅
Tactic: rw [← frontier_closedBall x hr, interior_frontier isClosed_closedBall]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
rw : interior (frontier (closedBall x r)) = ∅
⊢ interior (sphere x r) = ∅
have rw₁ : Eq.{u_1 + 1} (α := Set E) ∅ ∅
Tactic: rw [← frontier_closedBall x hr, interior_frontier isClosed_closedBall]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ frontier (sphere x r) = sphere x r
have rw : sphere x r \ interior (sphere x r) = sphere x r
Tactic: rw [isClosed_sphere.frontier_eq, interior_sphere x hr, diff_empty]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
rw : sphere x r \ interior (sphere x r) = sphere x r
⊢ frontier (sphere x r) = sphere x r
have rw₁ : sphere x r \ ∅ = sphere x r
Tactic: rw [isClosed_sphere.frontier_eq, interior_sphere x hr, diff_empty]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
rw : sphere x r \ interior (sphere x r) = sphere x r
rw₁ : sphere x r \ ∅ = sphere x r
⊢ frontier (sphere x r) = sphere x r
have rw₂ : sphere x r = sphere x r
Tactic: rw [isClosed_sphere.frontier_eq, interior_sphere x hr, diff_empty]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NontrivialTopology E
c : ℝ
hc : 0 ≤ c
⊢ ∃ (x : E), ‖x‖ = c
have rcases : ∀ (x : E) (hx : ‖x‖ ≠ 0), ∃ (x : E), ‖x‖ = c
Tactic: rcases exists_norm_ne_zero E with ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NontrivialTopology E
c : ℝ
hc : 0 ≤ c
x : E
hx : ‖x‖ ≠ 0
⊢ ∃ (x : E), ‖x‖ = c
have h : ‖c • ‖x‖⁻¹ • x‖ = c
Tactic: use c • ‖x‖⁻¹ • x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NontrivialTopology E
x : E
r : ℝ
⊢ (sphere x r).Nonempty ↔ 0 ≤ r
have refine : ∀ (hr : 0 ≤ r), (sphere x r).Nonempty
Tactic: refine ⟨fun h => nonempty_closedBall.1 (h.mono sphere_subset_closedBall), fun hr => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NontrivialTopology E
x : E
r : ℝ
hr : 0 ≤ r
⊢ (sphere x r).Nonempty
have obtain : ∀ (y : E) (hy : ‖y‖ = r), (sphere x r).Nonempty
Tactic: obtain ⟨y, hy⟩ := exists_norm_eq E hr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
r : ℝ
⊢ interior (closedBall x r) = ball x r
have inl : interior (closedBall x 0) = ball x 0
Tactic: rcases eq_or_ne r 0 with (rfl | hr)
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
r : ℝ
inl : interior (closedBall x 0) = ball x 0
⊢ interior (closedBall x r) = ball x r
have inr : ∀ (hr : r ≠ 0), interior (closedBall x r) = ball x r
Tactic: rcases eq_or_ne r 0 with (rfl | hr)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
⊢ interior (closedBall x 0) = ball x 0
have inl : interior {x} = ball x 0
Tactic: rw [closedBall_zero, ball_zero, interior_singleton]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
inl : interior {x} = ball x 0
⊢ interior (closedBall x 0) = ball x 0
have inl₁ : Eq (α := Set E) (interior {x}) ∅
Tactic: rw [closedBall_zero, ball_zero, interior_singleton]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
inl : interior {x} = ball x 0
inl₁ : Eq (α := Set E) (interior {x}) ∅
⊢ interior (closedBall x 0) = ball x 0
have inl₂ : Eq.{u_1 + 1} (α := Set E) ∅ ∅
Tactic: rw [closedBall_zero, ball_zero, interior_singleton]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
r : ℝ
⊢ frontier (closedBall x r) = sphere x r
have rw : closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (closedBall x r) \ interior (closedBall x r) = sphere x r
Tactic: rw [frontier, closure_closedBall, interior_closedBall' x r, closedBall_diff_ball]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
r : ℝ
rw :
  closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (closedBall x r) \ interior (closedBall x r) = sphere x r
⊢ frontier (closedBall x r) = sphere x r
have rw₁ : closedBall x r \ interior (closedBall x r) = sphere x r
Tactic: rw [frontier, closure_closedBall, interior_closedBall' x r, closedBall_diff_ball]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
r : ℝ
rw :
  closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (closedBall x r) \ interior (closedBall x r) = sphere x r
rw₁ : closedBall x r \ interior (closedBall x r) = sphere x r
⊢ frontier (closedBall x r) = sphere x r
have rw₂ : closedBall x r \ ball x r = sphere x r
Tactic: rw [frontier, closure_closedBall, interior_closedBall' x r, closedBall_diff_ball]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
r : ℝ
rw :
  closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (closedBall x r) \ interior (closedBall x r) = sphere x r
rw₁ : closedBall x r \ interior (closedBall x r) = sphere x r
rw₂ : closedBall x r \ ball x r = sphere x r
⊢ frontier (closedBall x r) = sphere x r
have rw₃ : sphere x r = sphere x r
Tactic: rw [frontier, closure_closedBall, interior_closedBall' x r, closedBall_diff_ball]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
r : ℝ
⊢ interior (sphere x r) = ∅
have rw : interior (frontier (closedBall x r)) = ∅
Tactic: rw [← frontier_closedBall' x, interior_frontier isClosed_closedBall]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
r : ℝ
rw : interior (frontier (closedBall x r)) = ∅
⊢ interior (sphere x r) = ∅
have rw₁ : Eq.{u_1 + 1} (α := Set E) ∅ ∅
Tactic: rw [← frontier_closedBall' x, interior_frontier isClosed_closedBall]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
r : ℝ
⊢ frontier (sphere x r) = sphere x r
have rw : sphere x r \ interior (sphere x r) = sphere x r
Tactic: rw [isClosed_sphere.frontier_eq, interior_sphere' x, diff_empty]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
r : ℝ
rw : sphere x r \ interior (sphere x r) = sphere x r
⊢ frontier (sphere x r) = sphere x r
have rw₁ : sphere x r \ ∅ = sphere x r
Tactic: rw [isClosed_sphere.frontier_eq, interior_sphere' x, diff_empty]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
r : ℝ
rw : sphere x r \ interior (sphere x r) = sphere x r
rw₁ : sphere x r \ ∅ = sphere x r
⊢ frontier (sphere x r) = sphere x r
have rw₂ : sphere x r = sphere x r
Tactic: rw [isClosed_sphere.frontier_eq, interior_sphere' x, diff_empty]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ray (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
h : SameRay ℝ x y
⊢ ‖x + y‖ = ‖x‖ + ‖y‖
have rcases : ∀ (u : E) (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (h : SameRay ℝ (a • u) (b • u)), ‖a • u + b • u‖ = ‖a • u‖ + ‖b • u‖
Tactic: rcases h.exists_eq_smul with ⟨u, a, b, ha, hb, -, rfl, rfl⟩
Cleared hypotheses: x, y, h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ray (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (a • u) (b • u)
⊢ ‖a • u + b • u‖ = ‖a • u‖ + ‖b • u‖
have rw : ‖(a + b) • u‖ = ‖a • u‖ + ‖b • u‖
Tactic: rw [← add_smul, norm_smul_of_nonneg (add_nonneg ha hb), norm_smul_of_nonneg ha,
    norm_smul_of_nonneg hb, add_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ray (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (a • u) (b • u)
rw : ‖(a + b) • u‖ = ‖a • u‖ + ‖b • u‖
⊢ ‖a • u + b • u‖ = ‖a • u‖ + ‖b • u‖
have rw₁ : (a + b) * ‖u‖ = ‖a • u‖ + ‖b • u‖
Tactic: rw [← add_smul, norm_smul_of_nonneg (add_nonneg ha hb), norm_smul_of_nonneg ha,
    norm_smul_of_nonneg hb, add_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ray (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (a • u) (b • u)
rw : ‖(a + b) • u‖ = ‖a • u‖ + ‖b • u‖
rw₁ : (a + b) * ‖u‖ = ‖a • u‖ + ‖b • u‖
⊢ ‖a • u + b • u‖ = ‖a • u‖ + ‖b • u‖
have rw₂ : (a + b) * ‖u‖ = a * ‖u‖ + ‖b • u‖
Tactic: rw [← add_smul, norm_smul_of_nonneg (add_nonneg ha hb), norm_smul_of_nonneg ha,
    norm_smul_of_nonneg hb, add_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ray (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (a • u) (b • u)
rw : ‖(a + b) • u‖ = ‖a • u‖ + ‖b • u‖
rw₁ : (a + b) * ‖u‖ = ‖a • u‖ + ‖b • u‖
rw₂ : (a + b) * ‖u‖ = a * ‖u‖ + ‖b • u‖
⊢ ‖a • u + b • u‖ = ‖a • u‖ + ‖b • u‖
have rw₃ : (a + b) * ‖u‖ = a * ‖u‖ + b * ‖u‖
Tactic: rw [← add_smul, norm_smul_of_nonneg (add_nonneg ha hb), norm_smul_of_nonneg ha,
    norm_smul_of_nonneg hb, add_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ray (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (a • u) (b • u)
rw : ‖(a + b) • u‖ = ‖a • u‖ + ‖b • u‖
rw₁ : (a + b) * ‖u‖ = ‖a • u‖ + ‖b • u‖
rw₂ : (a + b) * ‖u‖ = a * ‖u‖ + ‖b • u‖
rw₃ : (a + b) * ‖u‖ = a * ‖u‖ + b * ‖u‖
⊢ ‖a • u + b • u‖ = ‖a • u‖ + ‖b • u‖
have rw₄ : a * ‖u‖ + b * ‖u‖ = a * ‖u‖ + b * ‖u‖
Tactic: rw [← add_smul, norm_smul_of_nonneg (add_nonneg ha hb), norm_smul_of_nonneg ha,
    norm_smul_of_nonneg hb, add_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ray (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
h : SameRay ℝ x y
⊢ ‖x - y‖ = |‖x‖ - ‖y‖|
have rcases : ∀ (u : E) (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (h : SameRay ℝ (a • u) (b • u)), ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|
Tactic: rcases h.exists_eq_smul with ⟨u, a, b, ha, hb, -, rfl, rfl⟩
Cleared hypotheses: x, y, h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ray (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (a • u) (b • u)
⊢ ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|
have inr : ∀
  (H :
    ∀ (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (h : SameRay ℝ (a • u) (b • u)) (hab : b ≤ a),
      ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|)
  (hab : ¬b ≤ a), ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|
Tactic: wlog hab : b ≤ a generalizing a b with H
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ray (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (a • u) (b • u)
inr :
  ∀
    (H :
      ∀ (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (h : SameRay ℝ (a • u) (b • u)) (hab : b ≤ a),
        ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|)
    (hab : ¬b ≤ a), ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|
⊢ ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|
have wlog : ∀ (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (h : SameRay ℝ (a • u) (b • u)) (hab : b ≤ a),
  ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|
Tactic: wlog hab : b ≤ a generalizing a b with H
Cleared hypotheses: a, b, ha, hb, h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ray (hypothesis)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (a • u) (b • u)
H :
  ∀ (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (h : SameRay ℝ (a • u) (b • u)) (hab : b ≤ a),
    ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|
hab : ¬b ≤ a
⊢ ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|
have h₁ : SameRay ℝ (b • u) (a • u)
Tactic: rw [SameRay.sameRay_comm] at h
Cleared hypotheses: h, H, hab
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ray (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (b • u) (a • u)
H :
  ∀ (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (h : SameRay ℝ (a • u) (b • u)) (hab : b ≤ a),
    ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|
hab : ¬b ≤ a
⊢ ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|
have inr : ‖b • u - a • u‖ = |‖b • u‖ - ‖a • u‖|
Tactic: rw [norm_sub_rev, abs_sub_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ray (hypothesis)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (a • u) (b • u)
hab : b ≤ a
⊢ ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|
have hab₁ : 0 ≤ a - b
Tactic: rw [← sub_nonneg] at hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ray (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (a • u) (b • u)
hab : 0 ≤ a - b
⊢ ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|
have rw : ‖(a - b) • u‖ = |‖a • u‖ - ‖b • u‖|
Tactic: rw [← sub_smul, norm_smul_of_nonneg hab, norm_smul_of_nonneg ha, norm_smul_of_nonneg hb, ←
    sub_mul, abs_of_nonneg (mul_nonneg hab (norm_nonneg _))]