awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RieszLemma (goal)
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
hF : ∃ (x : E), x ∉ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : x ∉ F
hx : ∀ y ∈ F, ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
d : 𝕜
d0 : d ≠ 0
dxlt : ‖d • x‖ < R
ledx : R / ‖c‖ ≤ ‖d • x‖
y : E
hy : y ∈ F
y' : E := d⁻¹ • y
yy' : y = d • y'
rw : ‖d‖ * ‖x - y'‖ = ‖d • x - d • y'‖
rw₁ : ‖d‖ * ‖x - y'‖ = ‖d • (x - y')‖
⊢ ‖d‖ * ‖x - y'‖ = ‖d • x - y‖
have rw₂ : ‖d‖ * ‖x - y'‖ = ‖d‖ * ‖x - y'‖
Tactic: rw [yy', ← smul_sub, norm_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RieszLemma (goal)
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
hF : ∃ (x : E), x ∉ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : x ∉ F
hx : ∀ y ∈ F, ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
d : 𝕜
d0 : d ≠ 0
dxlt : ‖d • x‖ < R
ledx : R / ‖c‖ ≤ ‖d • x‖
y : E
hy : y ∈ F
y' : E := d⁻¹ • y
yy' : y = d • y'
⊢ 1 ≤ ‖d • x - y‖
have R₁ : 1 = ‖c‖ / R * (R / ‖c‖)
Tactic: calc
    1 = ‖c‖ / R * (R / ‖c‖) := by field
    _ ≤ ‖c‖ / R * ‖d • x‖ := by gcongr
    _ = ‖d‖ * (‖c‖ / R * ‖x‖) := by
      simp only [norm_smul]
      ring
    _ ≤ ‖d‖ * ‖x - y'‖ := by gcongr; exact hx y' (by simp [y', Submodule.smul_mem _ _ hy])
    _ = ‖d • x - y‖ := by rw [yy', ← smul_sub, norm_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RieszLemma (goal)
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
hF : ∃ (x : E), x ∉ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : x ∉ F
hx : ∀ y ∈ F, ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
d : 𝕜
d0 : d ≠ 0
dxlt : ‖d • x‖ < R
ledx : R / ‖c‖ ≤ ‖d • x‖
y : E
hy : y ∈ F
y' : E := d⁻¹ • y
yy' : y = d • y'
R₁ : 1 = ‖c‖ / R * (R / ‖c‖)
⊢ 1 ≤ ‖d • x - y‖
have R₂ : ‖c‖ / R * (R / ‖c‖) ≤ ‖c‖ / R * ‖d • x‖
Tactic: calc
    1 = ‖c‖ / R * (R / ‖c‖) := by field
    _ ≤ ‖c‖ / R * ‖d • x‖ := by gcongr
    _ = ‖d‖ * (‖c‖ / R * ‖x‖) := by
      simp only [norm_smul]
      ring
    _ ≤ ‖d‖ * ‖x - y'‖ := by gcongr; exact hx y' (by simp [y', Submodule.smul_mem _ _ hy])
    _ = ‖d • x - y‖ := by rw [yy', ← smul_sub, norm_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RieszLemma (goal)
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
hF : ∃ (x : E), x ∉ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : x ∉ F
hx : ∀ y ∈ F, ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
d : 𝕜
d0 : d ≠ 0
dxlt : ‖d • x‖ < R
ledx : R / ‖c‖ ≤ ‖d • x‖
y : E
hy : y ∈ F
y' : E := d⁻¹ • y
yy' : y = d • y'
R₁ : 1 = ‖c‖ / R * (R / ‖c‖)
R₂ : ‖c‖ / R * (R / ‖c‖) ≤ ‖c‖ / R * ‖d • x‖
⊢ 1 ≤ ‖d • x - y‖
have R₃ : ‖c‖ / R * ‖d • x‖ = ‖d‖ * (‖c‖ / R * ‖x‖)
Tactic: calc
    1 = ‖c‖ / R * (R / ‖c‖) := by field
    _ ≤ ‖c‖ / R * ‖d • x‖ := by gcongr
    _ = ‖d‖ * (‖c‖ / R * ‖x‖) := by
      simp only [norm_smul]
      ring
    _ ≤ ‖d‖ * ‖x - y'‖ := by gcongr; exact hx y' (by simp [y', Submodule.smul_mem _ _ hy])
    _ = ‖d • x - y‖ := by rw [yy', ← smul_sub, norm_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RieszLemma (goal)
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
hF : ∃ (x : E), x ∉ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : x ∉ F
hx : ∀ y ∈ F, ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
d : 𝕜
d0 : d ≠ 0
dxlt : ‖d • x‖ < R
ledx : R / ‖c‖ ≤ ‖d • x‖
y : E
hy : y ∈ F
y' : E := d⁻¹ • y
yy' : y = d • y'
R₁ : 1 = ‖c‖ / R * (R / ‖c‖)
R₂ : ‖c‖ / R * (R / ‖c‖) ≤ ‖c‖ / R * ‖d • x‖
R₃ : ‖c‖ / R * ‖d • x‖ = ‖d‖ * (‖c‖ / R * ‖x‖)
⊢ 1 ≤ ‖d • x - y‖
have R₄ : ‖d‖ * (‖c‖ / R * ‖x‖) ≤ ‖d‖ * ‖x - y'‖
Tactic: calc
    1 = ‖c‖ / R * (R / ‖c‖) := by field
    _ ≤ ‖c‖ / R * ‖d • x‖ := by gcongr
    _ = ‖d‖ * (‖c‖ / R * ‖x‖) := by
      simp only [norm_smul]
      ring
    _ ≤ ‖d‖ * ‖x - y'‖ := by gcongr; exact hx y' (by simp [y', Submodule.smul_mem _ _ hy])
    _ = ‖d • x - y‖ := by rw [yy', ← smul_sub, norm_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RieszLemma (goal)
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
hF : ∃ (x : E), x ∉ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : x ∉ F
hx : ∀ y ∈ F, ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
d : 𝕜
d0 : d ≠ 0
dxlt : ‖d • x‖ < R
ledx : R / ‖c‖ ≤ ‖d • x‖
y : E
hy : y ∈ F
y' : E := d⁻¹ • y
yy' : y = d • y'
R₁ : 1 = ‖c‖ / R * (R / ‖c‖)
R₂ : ‖c‖ / R * (R / ‖c‖) ≤ ‖c‖ / R * ‖d • x‖
R₃ : ‖c‖ / R * ‖d • x‖ = ‖d‖ * (‖c‖ / R * ‖x‖)
R₄ : ‖d‖ * (‖c‖ / R * ‖x‖) ≤ ‖d‖ * ‖x - y'‖
⊢ 1 ≤ ‖d • x - y‖
have R₅ : ‖d‖ * ‖x - y'‖ = ‖d • x - y‖
Tactic: calc
    1 = ‖c‖ / R * (R / ‖c‖) := by field
    _ ≤ ‖c‖ / R * ‖d • x‖ := by gcongr
    _ = ‖d‖ * (‖c‖ / R * ‖x‖) := by
      simp only [norm_smul]
      ring
    _ ≤ ‖d‖ * ‖x - y'‖ := by gcongr; exact hx y' (by simp [y', Submodule.smul_mem _ _ hy])
    _ = ‖d • x - y‖ := by rw [yy', ← smul_sub, norm_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RieszLemma (goal)
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : NormedSpace ℝ F
x : F
s : Set F
hx : x ∈ s
⊢ closedBall x (infDist x sᶜ) ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
have inl : ∀ (h₀ : infDist x sᶜ = 0), closedBall x (infDist x sᶜ) ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
Tactic: rcases eq_or_ne (infDist x sᶜ) 0 with h₀ | h₀
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RieszLemma (goal)
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : NormedSpace ℝ F
x : F
s : Set F
hx : x ∈ s
inl :
  ∀ (h₀ : infDist x sᶜ = 0),
    closedBall x (infDist x sᶜ) ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ closedBall x (infDist x sᶜ) ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
have inr : ∀ (h₀ : infDist x sᶜ ≠ 0), closedBall x (infDist x sᶜ) ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
Tactic: rcases eq_or_ne (infDist x sᶜ) 0 with h₀ | h₀
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RieszLemma (goal)
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : NormedSpace ℝ F
x : F
s : Set F
hx : x ∈ s
h₀ : infDist x sᶜ = 0
⊢ closedBall x (infDist x sᶜ) ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
have inl : closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x} ⊆
  closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
Tactic: rw [h₀, closedBall_zero']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RieszLemma (goal)
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : NormedSpace ℝ F
x : F
s : Set F
hx : x ∈ s
h₀ : infDist x sᶜ ≠ 0
⊢ closedBall x (infDist x sᶜ) ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
have inr : closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball x (infDist x sᶜ)) ⊆
  closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
Tactic: rw [← closure_ball x h₀]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RieszLemma (goal)
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
E : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
hF : ∃ (x : E), x ∉ F
r : ℝ
hr : r < 1
⊢ ∃ x₀ ∉ F, ‖x₀‖ = 1 ∧ ∀ y ∈ F, r ≤ ‖x₀ - y‖
have obtain : ∀ (x₀ : E) (hx₀ : x₀ ∉ F) (h : ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖), ∃ x₀ ∉ F, ‖x₀‖ = 1 ∧ ∀ y ∈ F, r ≤ ‖x₀ - y‖
Tactic: obtain ⟨x₀, hx₀, h⟩ := riesz_lemma hFc hF hr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RieszLemma (hypothesis)
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
E : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
hF : ∃ (x : E), x ∉ F
r : ℝ
hr : r < 1
x₀ : E
hx₀ : x₀ ∉ F
h : ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
⊢ ∃ x₀ ∉ F, ‖x₀‖ = 1 ∧ ∀ y ∈ F, r ≤ ‖x₀ - y‖
have hx₀' : x₀ ≠ 0
Tactic: have hx₀' : x₀ ≠ 0 := by rintro rfl; simp at hx₀
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RieszLemma (goal)
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
E : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
hF : ∃ (x : E), x ∉ F
r : ℝ
hr : r < 1
x₀ : E
hx₀ : x₀ ∉ F
h : ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
hx₀' : x₀ ≠ 0
⊢ ∃ x₀ ∉ F, ‖x₀‖ = 1 ∧ ∀ y ∈ F, r ≤ ‖x₀ - y‖
have refine_1 : HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜)⁻¹ x₀ ∉ F
Tactic: refine ⟨(‖x₀‖⁻¹ : 𝕜) • x₀, ?_, norm_smul_inv_norm hx₀', ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RieszLemma (goal)
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
E : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
hF : ∃ (x : E), x ∉ F
r : ℝ
hr : r < 1
x₀ : E
hx₀ : x₀ ∉ F
h : ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
hx₀' : x₀ ≠ 0
refine_1 : HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜)⁻¹ x₀ ∉ F
⊢ ∃ x₀ ∉ F, ‖x₀‖ = 1 ∧ ∀ y ∈ F, r ≤ ‖x₀ - y‖
have refine_2 : ∀ y ∈ F, r ≤ ‖HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜)⁻¹ x₀ - y‖
Tactic: refine ⟨(‖x₀‖⁻¹ : 𝕜) • x₀, ?_, norm_smul_inv_norm hx₀', ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RieszLemma (goal)
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
E : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
hF : ∃ (x : E), x ∉ F
r : ℝ
hr : r < 1
x₀ : E
hx₀ : x₀ ∉ F
h : ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
hx₀' : x₀ ≠ 0
⊢ HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜)⁻¹ x₀ ∉ F
have refine_1 : Ne.{u_4 + 1} (α := 𝕜) (↑‖x₀‖ : 𝕜)⁻¹ 0
Tactic: rwa [Submodule.smul_mem_iff]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RieszLemma (goal)
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
E : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
hF : ∃ (x : E), x ∉ F
r : ℝ
hr : r < 1
x₀ : E
hx₀ : x₀ ∉ F
h : ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
hx₀' : x₀ ≠ 0
y : E
hy : y ∈ F
⊢ ‖HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜)⁻¹ (x₀ - HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜) y)‖ =
    ‖x₀‖⁻¹ * ‖x₀ - HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜) y‖
have rw : norm.{u_4} (E := 𝕜) (↑‖x₀‖ : 𝕜)⁻¹ * ‖x₀ - HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜) y‖ =
  ‖x₀‖⁻¹ * ‖x₀ - HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜) y‖
Tactic: rw [norm_smul, norm_inv, norm_algebraMap', norm_norm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RieszLemma (goal)
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
E : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
hF : ∃ (x : E), x ∉ F
r : ℝ
hr : r < 1
x₀ : E
hx₀ : x₀ ∉ F
h : ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
hx₀' : x₀ ≠ 0
y : E
hy : y ∈ F
rw :
  norm.{u_4} (E := 𝕜) (↑‖x₀‖ : 𝕜)⁻¹ * ‖x₀ - HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜) y‖ =
    ‖x₀‖⁻¹ * ‖x₀ - HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜) y‖
⊢ ‖HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜)⁻¹ (x₀ - HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜) y)‖ =
    ‖x₀‖⁻¹ * ‖x₀ - HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜) y‖
have rw₁ : (norm.{u_4} (E := 𝕜) (↑‖x₀‖ : 𝕜))⁻¹ * ‖x₀ - HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜) y‖ =
  ‖x₀‖⁻¹ * ‖x₀ - HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜) y‖
Tactic: rw [norm_smul, norm_inv, norm_algebraMap', norm_norm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RieszLemma (goal)
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
E : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
hF : ∃ (x : E), x ∉ F
r : ℝ
hr : r < 1
x₀ : E
hx₀ : x₀ ∉ F
h : ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
hx₀' : x₀ ≠ 0
y : E
hy : y ∈ F
rw :
  norm.{u_4} (E := 𝕜) (↑‖x₀‖ : 𝕜)⁻¹ * ‖x₀ - HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜) y‖ =
    ‖x₀‖⁻¹ * ‖x₀ - HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜) y‖
rw₁ :
  (norm.{u_4} (E := 𝕜) (↑‖x₀‖ : 𝕜))⁻¹ * ‖x₀ - HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜) y‖ =
    ‖x₀‖⁻¹ * ‖x₀ - HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜) y‖
⊢ ‖HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜)⁻¹ (x₀ - HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜) y)‖ =
    ‖x₀‖⁻¹ * ‖x₀ - HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜) y‖
have rw₂ : ‖‖x₀‖‖⁻¹ * ‖x₀ - HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜) y‖ =
  ‖x₀‖⁻¹ * ‖x₀ - HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜) y‖
Tactic: rw [norm_smul, norm_inv, norm_algebraMap', norm_norm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RieszLemma (goal)
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
E : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
hF : ∃ (x : E), x ∉ F
r : ℝ
hr : r < 1
x₀ : E
hx₀ : x₀ ∉ F
h : ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
hx₀' : x₀ ≠ 0
y : E
hy : y ∈ F
rw :
  norm.{u_4} (E := 𝕜) (↑‖x₀‖ : 𝕜)⁻¹ * ‖x₀ - HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜) y‖ =
    ‖x₀‖⁻¹ * ‖x₀ - HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜) y‖
rw₁ :
  (norm.{u_4} (E := 𝕜) (↑‖x₀‖ : 𝕜))⁻¹ * ‖x₀ - HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜) y‖ =
    ‖x₀‖⁻¹ * ‖x₀ - HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜) y‖
rw₂ :
  ‖‖x₀‖‖⁻¹ * ‖x₀ - HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜) y‖ =
    ‖x₀‖⁻¹ * ‖x₀ - HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜) y‖
⊢ ‖HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜)⁻¹ (x₀ - HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜) y)‖ =
    ‖x₀‖⁻¹ * ‖x₀ - HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜) y‖
have rw₃ : ‖x₀‖⁻¹ * ‖x₀ - HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜) y‖ =
  ‖x₀‖⁻¹ * ‖x₀ - HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜) y‖
Tactic: rw [norm_smul, norm_inv, norm_algebraMap', norm_norm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RieszLemma (hypothesis)
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
E : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
hF : ∃ (x : E), x ∉ F
r : ℝ
hr : r < 1
x₀ : E
hx₀ : x₀ ∉ F
h : ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
hx₀' : x₀ ≠ 0
y : E
hy : y ∈ F
⊢ r ≤ ‖HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜)⁻¹ x₀ - y‖
have h₂ : ‖HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜)⁻¹ (x₀ - HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜) y)‖ =
  ‖x₀‖⁻¹ * ‖x₀ - HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜) y‖
Tactic: have h₂ : ‖(‖x₀‖ : 𝕜)⁻¹ • (x₀ - (‖x₀‖ : 𝕜) • y)‖ = ‖x₀‖⁻¹ * ‖x₀ - (‖x₀‖ : 𝕜) • y‖ := by
    rw [norm_smul, norm_inv, norm_algebraMap', norm_norm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RieszLemma (hypothesis)
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
E : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
hF : ∃ (x : E), x ∉ F
r : ℝ
hr : r < 1
x₀ : E
hx₀ : x₀ ∉ F
h : ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
hx₀' : x₀ ≠ 0
y : E
hy : y ∈ F
h₂ :
  ‖HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜)⁻¹ (x₀ - HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜) y)‖ =
    ‖x₀‖⁻¹ * ‖x₀ - HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜) y‖
⊢ r ≤ ‖HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜)⁻¹ x₀ - y‖
have h₁ : r * ‖x₀‖ ≤ ‖x₀ - HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜) y‖
Tactic: have h₁ := h ((‖x₀‖ : 𝕜) • y) (F.smul_mem _ hy)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RieszLemma (goal)
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
E : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
hF : ∃ (x : E), x ∉ F
r : ℝ
hr : r < 1
x₀ : E
hx₀ : x₀ ∉ F
h : ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
hx₀' : x₀ ≠ 0
y : E
hy : y ∈ F
h₂ :
  ‖HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜)⁻¹ (x₀ - HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜) y)‖ =
    ‖x₀‖⁻¹ * ‖x₀ - HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜) y‖
h₁ : r * ‖x₀‖ ≤ ‖x₀ - HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜) y‖
⊢ r ≤ ‖HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜)⁻¹ x₀ - y‖
have refine_2 : ∀
  (h₁ :
    r ≤
      ‖HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜)⁻¹ x₀ -
          HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜)⁻¹ (HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜) y)‖),
  Ne.{u_4 + 1} (α := 𝕜) (↑‖x₀‖ : 𝕜) 0
Tactic: rwa [← le_inv_mul_iff₀' (by simpa), ← h₂, smul_sub, inv_smul_smul₀] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Span (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
x : E
c : 𝕜
⊢ norm.{u_2} (E := E) ((toSpanSingleton 𝕜 E x : (a : 𝕜) → E) c : E) = ‖x‖ * ‖c‖
have rw : norm.{u_2} (E := E) ((toSpanSingleton 𝕜 E x : (a : 𝕜) → E) c : E) = ‖c‖ * ‖x‖
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Span (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
x : E
hx : ‖x‖ = 1
x_1 : 𝕜
⊢ norm.{u_2} (E := ↥(𝕜 ∙ x))
      (((LinearEquiv.toSpanNonzeroSingleton 𝕜 E x ⋯ : LinearEquiv.{u_1, u_1, u_1, u_2} (RingHom.id 𝕜) 𝕜 ↥(𝕜 ∙ x)) :
            (a : 𝕜) → ↥(𝕜 ∙ x))
          x_1 :
        ↥(𝕜 ∙ x)) =
    ‖x_1‖
have rw : ‖x‖ * ‖x_1‖ = ‖x_1‖
Tactic: rw [LinearEquiv.toSpanNonzeroSingleton_homothety, hx, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Span (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
x : E
hx : ‖x‖ = 1
x_1 : 𝕜
rw : ‖x‖ * ‖x_1‖ = ‖x_1‖
⊢ norm.{u_2} (E := ↥(𝕜 ∙ x))
      (((LinearEquiv.toSpanNonzeroSingleton 𝕜 E x ⋯ : LinearEquiv.{u_1, u_1, u_1, u_2} (RingHom.id 𝕜) 𝕜 ↥(𝕜 ∙ x)) :
            (a : 𝕜) → ↥(𝕜 ∙ x))
          x_1 :
        ↥(𝕜 ∙ x)) =
    ‖x_1‖
have rw₁ : 1 * ‖x_1‖ = ‖x_1‖
Tactic: rw [LinearEquiv.toSpanNonzeroSingleton_homothety, hx, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Span (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
x : E
hx : ‖x‖ = 1
x_1 : 𝕜
rw : ‖x‖ * ‖x_1‖ = ‖x_1‖
rw₁ : 1 * ‖x_1‖ = ‖x_1‖
⊢ norm.{u_2} (E := ↥(𝕜 ∙ x))
      (((LinearEquiv.toSpanNonzeroSingleton 𝕜 E x ⋯ : LinearEquiv.{u_1, u_1, u_1, u_2} (RingHom.id 𝕜) 𝕜 ↥(𝕜 ∙ x)) :
            (a : 𝕜) → ↥(𝕜 ∙ x))
          x_1 :
        ↥(𝕜 ∙ x)) =
    ‖x_1‖
have rw₂ : ‖x_1‖ = ‖x_1‖
Tactic: rw [LinearEquiv.toSpanNonzeroSingleton_homothety, hx, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.WeakDual (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
⊢ LE.le (α := TopologicalSpace (StrongDual 𝕜 E)) (UniformSpace.toTopologicalSpace : TopologicalSpace (StrongDual 𝕜 E))
    (instTopologicalSpaceWeakDual 𝕜 E : TopologicalSpace (WeakDual 𝕜 E))
have h : Eq (α := TopologicalSpace (StrongDual 𝕜 E)) (instTopologicalSpaceWeakDual 𝕜 E : TopologicalSpace (WeakDual 𝕜 E))
  (TopologicalSpace.induced (Y := WeakDual 𝕜 E)
    (fun (x' : StrongDual 𝕜 E) ↦ (StrongDual.toWeakDual : (a : StrongDual 𝕜 E) → WeakDual 𝕜 E) x')
    (instTopologicalSpaceWeakDual 𝕜 E))
Tactic: convert! (@toWeakDual_continuous _ _ _ _ (by assumption)).le_induced
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.WeakDual (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
s : Set (WeakDual 𝕜 E)
⊢ Bornology.IsBounded s ↔ IsVonNBounded 𝕜 s
have mp : Bornology.IsBounded s → IsVonNBounded 𝕜 s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.WeakDual (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
s : Set (WeakDual 𝕜 E)
mp : Bornology.IsBounded s → IsVonNBounded 𝕜 s
⊢ Bornology.IsBounded s ↔ IsVonNBounded 𝕜 s
have mpr : IsVonNBounded 𝕜 s → Bornology.IsBounded s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.WeakDual (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
s : Set (WeakDual 𝕜 E)
h_vN : IsVonNBounded 𝕜 s
⊢ Bornology.IsBounded s
have h_ptwise : ∀ (i : E), ∃ r > 0, ∀ x ∈ s, (seminormFamily 𝕜 E i : (a : WeakDual 𝕜 E) → ℝ) x < r
Tactic: have h_ptwise := (withSeminorms 𝕜 E).isVonNBounded_iff_seminorm_bounded.mp h_vN
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.WeakDual (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
s : Set (WeakDual 𝕜 E)
h_vN : IsVonNBounded 𝕜 s
h_ptwise : ∀ (i : E), ∃ r > 0, ∀ x ∈ s, (seminormFamily 𝕜 E i : (a : WeakDual 𝕜 E) → ℝ) x < r
⊢ Bornology.IsBounded s
have mpr : ∀ (C : ℝ)
  (hC :
    ∀ (i : (↑s : Type (max u_1 u_3))),
      norm (E := E →L[𝕜] 𝕜)
          ((toStrongDual : (a : WeakDual 𝕜 E) → StrongDual 𝕜 E) (↑i : WeakDual 𝕜 E) : StrongDual 𝕜 E) ≤
        C),
  Bornology.IsBounded s
Tactic: obtain ⟨C, hC⟩ := banach_steinhaus (g := fun i : s ↦ WeakDual.toStrongDual i.val) fun x ↦
      let ⟨M, _, hM⟩ := h_ptwise x
      ⟨M, fun i ↦ le_of_lt (hM i.val i.property)⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.WeakDual (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
s : Set (WeakDual 𝕜 E)
h_vN : IsVonNBounded 𝕜 s
h_ptwise : ∀ (i : E), ∃ r > 0, ∀ x ∈ s, (seminormFamily 𝕜 E i : (a : WeakDual 𝕜 E) → ℝ) x < r
C : ℝ
hC :
  ∀ (i : (↑s : Type (max u_1 u_3))),
    norm (E := E →L[𝕜] 𝕜) ((toStrongDual : (a : WeakDual 𝕜 E) → StrongDual 𝕜 E) (↑i : WeakDual 𝕜 E) : StrongDual 𝕜 E) ≤
      C
⊢ Bornology.IsBounded s
have mpr : ∃ (C : ℝ),
  ∀ (x : StrongDual 𝕜 E),
    Membership.mem (γ := Set (StrongDual 𝕜 E)) ((⇑StrongDual.toWeakDual : (a : StrongDual 𝕜 E) → WeakDual 𝕜 E) ⁻¹' s)
        x →
      ‖x‖ ≤ C
Tactic: rw [← isBounded_toWeakDual_preimage_iff_isBounded, isBounded_iff_forall_norm_le]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.WeakDual (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set (WeakDual 𝕜 E)
hb : Bornology.IsBounded s
⊢ Bornology.IsBounded (closure s)
have obtain : ∀ (R : ℝ) (hR : s ⊆ closedBall 0 R), Bornology.IsBounded (closure s)
Tactic: obtain ⟨R, hR⟩ := (Metric.isBounded_iff_subset_closedBall (0 : StrongDual 𝕜 E)).mp hb
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.WeakDual (goal)
Goal:
𝕜 : Type u_1
M : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup M
inst_2 : TopologicalSpace M
inst_3 : Module 𝕜 M
s : Set M
⊢ IsClosed (X := WeakDual 𝕜 M) (polar 𝕜 s)
have simp : IsClosed (X := WeakDual 𝕜 M) (⋂ i ∈ s, {x : WeakDual 𝕜 M | norm.{u_1} (E := 𝕜) ((x : (a : M) → 𝕜) i : 𝕜) ≤ 1})
Tactic: simp only [polar_def, setOf_forall]