awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Module.RieszLemma
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
⊢ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x} ⊆
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s

Tactic:
exact closure_mono (singleton_subset_iff.2 hx)

Premises used: Iff.mpr, Set.singleton_subset_iff, closure_mono
-- Module: Mathlib.Analysis.Normed.Module.RieszLemma
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
inr :
  closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball x (infDist x sᶜ)) ⊆
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ closedBall x (infDist x sᶜ) ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s

Tactic:
rw [← closure_ball x h₀]

Premises used: closure_ball
-- Module: Mathlib.Analysis.Normed.Module.RieszLemma
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
⊢ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball x (infDist x sᶜ)) ⊆
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s

Tactic:
closure_mono ball_infDist_compl_subset

Premises used: Metric.ball_infDist_compl_subset, closure_mono
-- Module: Mathlib.Analysis.Normed.Module.RieszLemma
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
⊢ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball x (infDist x sᶜ)) ⊆
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s

Tactic:
exact closure_mono ball_infDist_compl_subset

Premises used: Metric.ball_infDist_compl_subset, closure_mono
-- Module: Mathlib.Analysis.Normed.Module.RieszLemma
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
obtain : ∀ (x₀ : E) (hx₀ : x₀ ∉ F) (h : ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖), ∃ x₀ ∉ F, ‖x₀‖ = 1 ∧ ∀ y ∈ F, r ≤ ‖x₀ - y‖
⊢ ∃ x₀ ∉ F, ‖x₀‖ = 1 ∧ ∀ y ∈ F, r ≤ ‖x₀ - y‖

Tactic:
obtain ⟨x₀, hx₀, h⟩ := riesz_lemma hFc hF hr

Premises used: riesz_lemma
-- Module: Mathlib.Analysis.Normed.Module.RieszLemma
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
hx₀ : 0 ∉ F
h : ∀ y ∈ F, r * norm.{u_5} (E := E) 0 ≤ ‖0 - y‖
⊢ False

Tactic:
simp at hx₀
-- Module: Mathlib.Analysis.Normed.Module.RieszLemma
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₀ ≠ 0

Tactic:
have hx₀' : x₀ ≠ 0 := by rintro rfl; simp at hx₀
-- Module: Mathlib.Analysis.Normed.Module.RieszLemma
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‖

Tactic:
⟨(‖x₀‖⁻¹ : 𝕜) • x₀, ?_, norm_smul_inv_norm hx₀', ?_⟩

Premises used: Norm.norm, norm_smul_inv_norm, RCLike.ofReal, Inv.inv, And.intro, Exists.intro, HSMul.hSMul
-- Module: Mathlib.Analysis.Normed.Module.RieszLemma
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
refine_2 : ∀ y ∈ F, r ≤ ‖HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜)⁻¹ x₀ - y‖
⊢ ∃ x₀ ∉ F, ‖x₀‖ = 1 ∧ ∀ y ∈ F, r ≤ ‖x₀ - y‖

Tactic:
refine ⟨(‖x₀‖⁻¹ : 𝕜) • x₀, ?_, norm_smul_inv_norm hx₀', ?_⟩
-- Module: Mathlib.Analysis.Normed.Module.RieszLemma
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 : Ne.{u_4 + 1} (α := 𝕜) (↑‖x₀‖ : 𝕜)⁻¹ 0
⊢ HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜)⁻¹ x₀ ∉ F

Tactic:
rwa [Submodule.smul_mem_iff]

Premises used: Submodule.smul_mem_iff
-- Module: Mathlib.Analysis.Normed.Module.RieszLemma
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
⊢ Ne.{u_4 + 1} (α := 𝕜) (↑‖x₀‖ : 𝕜)⁻¹ 0

Tactic:
simpa
-- Module: Mathlib.Analysis.Normed.Module.RieszLemma
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‖
rw₃ 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‖

Tactic:
rw [norm_smul, norm_inv, norm_algebraMap', norm_norm]

Premises used: norm_smul, norm_norm, norm_inv, norm_algebraMap'
-- Module: Mathlib.Analysis.Normed.Module.RieszLemma
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‖

Tactic:
have h₂ : ‖(‖x₀‖ : 𝕜)⁻¹ • (x₀ - (‖x₀‖ : 𝕜) • y)‖ = ‖x₀‖⁻¹ * ‖x₀ - (‖x₀‖ : 𝕜) • y‖ := by
    rw [norm_smul, norm_inv, norm_algebraMap', norm_norm]
-- Module: Mathlib.Analysis.Normed.Module.RieszLemma
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 * ‖x₀‖ ≤ ‖x₀ - HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜) y‖

Tactic:
have h₁ := h ((‖x₀‖ : 𝕜) • y) (F.smul_mem _ hy)
-- Module: Mathlib.Analysis.Normed.Module.RieszLemma
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‖
⊢ 0 < ‖x₀‖

Tactic:
simpa
-- Module: Mathlib.Analysis.Normed.Module.RieszLemma
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‖
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
⊢ r ≤ ‖HSMul.hSMul.{u_4, u_5, u_5} (α := 𝕜) (↑‖x₀‖ : 𝕜)⁻¹ x₀ - y‖

Tactic:
rwa [← le_inv_mul_iff₀' (by simpa), ← h₂, smul_sub, inv_smul_smul₀] at h₁

Premises used: inv_smul_smul₀, le_inv_mul_iff₀', smul_sub
-- Module: Mathlib.Analysis.Normed.Module.RieszLemma
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 ≤
    ‖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:
simpa using hx₀'
-- Module: Mathlib.Analysis.Normed.Module.Span
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 : 𝕜
rw : norm.{u_2} (E := E) ((toSpanSingleton 𝕜 E x : (a : 𝕜) → E) c : E) = ‖c‖ * ‖x‖
⊢ norm.{u_2} (E := E) ((toSpanSingleton 𝕜 E x : (a : 𝕜) → E) c : E) = ‖x‖ * ‖c‖

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Analysis.Normed.Module.Span
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) = ‖c‖ * ‖x‖

Tactic:
norm_smul _ _

Premises used: norm_smul
-- Module: Mathlib.Analysis.Normed.Module.Span
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) = ‖c‖ * ‖x‖

Tactic:
exact norm_smul _ _

Premises used: norm_smul
-- Module: Mathlib.Analysis.Normed.Module.Span
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
x : E
h : x ≠ 0
c : 𝕜
⊢ norm.{u_2} (E := ↥(𝕜 ∙ x))
      (((LinearEquiv.toSpanNonzeroSingleton 𝕜 E x h : LinearEquiv.{u_1, u_1, u_1, u_2} (RingHom.id 𝕜) 𝕜 ↥(𝕜 ∙ x)) :
            (a : 𝕜) → ↥(𝕜 ∙ x))
          c :
        ↥(𝕜 ∙ x)) =
    ‖x‖ * ‖c‖

Tactic:
LinearMap.toSpanSingleton_homothety _ _ _

Premises used: LinearMap.toSpanSingleton_homothety
-- Module: Mathlib.Analysis.Normed.Module.Span
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
h : x ≠ 0
⊢ Eq (α := (a : ↥(𝕜 ∙ x)) → 𝕜) (⇑(ContinuousLinearEquiv.symm (toSpanNonzeroSingleton 𝕜 x h)) : (a : ↥(𝕜 ∙ x)) → 𝕜)
    (⇑(coord 𝕜 x h) : (a : ↥(𝕜 ∙ x)) → 𝕜)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Module.Span
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
h : x ≠ 0
c : 𝕜
⊢ (coord 𝕜 x h : (a : ↥(𝕜 ∙ x)) → 𝕜)
      (((toSpanNonzeroSingleton 𝕜 x h : ContinuousLinearEquiv.{u_1, u_1, u_1, u_2} (RingHom.id 𝕜) 𝕜 ↥(𝕜 ∙ x)) :
            (a : 𝕜) → ↥(𝕜 ∙ x))
          c :
        ↥(𝕜 ∙ x)) =
    c

Tactic:
(toSpanNonzeroSingleton 𝕜 x h).symm_apply_apply c

Premises used: ContinuousLinearEquiv.toSpanNonzeroSingleton, ContinuousLinearEquiv.symm_apply_apply
-- Module: Mathlib.Analysis.Normed.Module.Span
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
h : x ≠ 0
y : ↥(𝕜 ∙ x)
⊢ ((toSpanNonzeroSingleton 𝕜 x h : ContinuousLinearEquiv.{u_1, u_1, u_1, u_2} (RingHom.id 𝕜) 𝕜 ↥(𝕜 ∙ x)) :
        (a : 𝕜) → ↥(𝕜 ∙ x))
      ((coord 𝕜 x h : (a : ↥(𝕜 ∙ x)) → 𝕜) y) =
    y

Tactic:
(toSpanNonzeroSingleton 𝕜 x h).apply_symm_apply y

Premises used: ContinuousLinearEquiv.apply_symm_apply, ContinuousLinearEquiv.toSpanNonzeroSingleton
-- Module: Mathlib.Analysis.Normed.Module.Span
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
h : x ≠ 0
⊢ Eq.{u_1 + 1} (α := 𝕜)
    ((coord 𝕜 x h : (a : ↥(𝕜 ∙ x)) → 𝕜)
        (Subtype.mk (p := fun (x_1 : E) ↦ Membership.mem (γ := Submodule 𝕜 E) (𝕜 ∙ x) x_1) x ⋯) :
      𝕜)
    (1 : 𝕜)

Tactic:
LinearEquiv.coord_self 𝕜 E x h

Premises used: LinearEquiv.coord_self
-- Module: Mathlib.Analysis.Normed.Module.Span
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 ≠ 0

Tactic:
aesop
-- Module: Mathlib.Analysis.Normed.Module.Span
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‖
rw₂ rw₃ : ‖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‖

Tactic:
rw [LinearEquiv.toSpanNonzeroSingleton_homothety, hx, one_mul]

Premises used: LinearEquiv.toSpanNonzeroSingleton_homothety, one_mul
-- Module: Mathlib.Analysis.Normed.Module.Span
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
r : 𝕜
⊢ Membership.mem (γ := Submodule 𝕜 E) (𝕜 ∙ x) (r • x)

Tactic:
aesop
-- Module: Mathlib.Analysis.Normed.Module.Span
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
r : 𝕜
⊢ (toSpanUnitSingleton x hx : (a : 𝕜) → ↥(𝕜 ∙ x)) r =
    Subtype.mk (p := fun (x_1 : E) ↦ Membership.mem (γ := Submodule 𝕜 E) (𝕜 ∙ x) x_1) (r • x) ⋯

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Module.WeakDual
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set (StrongDual 𝕜 E)
⊢ Bornology.IsBounded (α := WeakDual 𝕜 E) ((⇑toStrongDual : (a : WeakDual 𝕜 E) → StrongDual 𝕜 E) ⁻¹' s) ↔
    Bornology.IsBounded s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, WeakBilin, Set.preimage, WeakDual
-- Module: Mathlib.Analysis.Normed.Module.WeakDual
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set (WeakDual 𝕜 E)
⊢ Bornology.IsBounded (α := StrongDual 𝕜 E) ((⇑StrongDual.toWeakDual : (a : StrongDual 𝕜 E) → WeakDual 𝕜 E) ⁻¹' s) ↔
    Bornology.IsBounded s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, WeakBilin, Set.preimage, WeakDual
-- Module: Mathlib.Analysis.Normed.Module.WeakDual
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
⊢ Continuous[ContinuousLinearMap.topologicalSpace, _] fun (x' : StrongDual 𝕜 E) ↦
    (StrongDual.toWeakDual : (a : StrongDual 𝕜 E) → WeakDual 𝕜 E) x'

Tactic:
WeakBilin.continuous_of_continuous_eval _ fun z => (ContinuousLinearMap.apply 𝕜 𝕜 z).continuous

Premises used: ContinuousLinearMap.continuous, ContinuousLinearMap.apply, WeakDual, WeakBilin.continuous_of_continuous_eval, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Module.WeakDual
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
⊢ NormedSpace 𝕜 E

Tactic:
assumption
-- Module: Mathlib.Analysis.Normed.Module.WeakDual
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
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))
⊢ LE.le (α := TopologicalSpace (StrongDual 𝕜 E)) (UniformSpace.toTopologicalSpace : TopologicalSpace (StrongDual 𝕜 E))
    (instTopologicalSpaceWeakDual 𝕜 E : TopologicalSpace (WeakDual 𝕜 E))

Tactic:
convert! (@toWeakDual_continuous _ _ _ _ (by assumption)).le_induced

Premises used: NormedSpace.Dual.toWeakDual_continuous, Continuous.le_induced
-- Module: Mathlib.Analysis.Normed.Module.WeakDual
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
⊢ 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:
induced_id.symm

Premises used: induced_id, WeakBilin, WeakDual, Eq.symm
-- Module: Mathlib.Analysis.Normed.Module.WeakDual
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
⊢ 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:
exact induced_id.symm

Premises used: induced_id, Eq.symm
-- Module: Mathlib.Analysis.Normed.Module.WeakDual
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
f : WeakDual 𝕜 E
⊢ (seminormFamily 𝕜 E x : (a : WeakDual 𝕜 E) → ℝ) f = norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) x : 𝕜)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Module.WeakDual
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
⊢ WithSeminorms (E := WeakDual 𝕜 E) (seminormFamily 𝕜 E)

Tactic:
(topDualPairing 𝕜 E).weakBilin_withSeminorms

Premises used: instAddCommMonoidWeakDual._aux_1, instAddCommMonoidWeakBilin._aux_1, instAddCommMonoidWeakDual._aux_4, WeakDual.seminormFamily, instAddCommMonoidWeakBilin._aux_4, instModuleWeakBilin._aux_1, LinearMap.weakBilin_withSeminorms, topDualPairing, WeakBilin, WeakDual
-- Module: Mathlib.Analysis.Normed.Module.WeakDual
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
mpr : IsVonNBounded 𝕜 s → Bornology.IsBounded s
⊢ Bornology.IsBounded s ↔ IsVonNBounded 𝕜 s

Tactic:
constructor
-- Module: Mathlib.Analysis.Normed.Module.WeakDual
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

Tactic:
fun h => ((NormedSpace.isVonNBounded_iff 𝕜).mpr h).of_topologicalSpace_le
      Dual.dual_norm_topology_le_weak_dual_topology

Premises used: Iff.mpr, NormedSpace.isVonNBounded_iff, instAddCommMonoidWeakDual._aux_4, instAddCommMonoidWeakBilin._aux_4, WeakBilin, Bornology.IsVonNBounded.of_topologicalSpace_le, WeakDual, NormedSpace.Dual.dual_norm_topology_le_weak_dual_topology
-- Module: Mathlib.Analysis.Normed.Module.WeakDual
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

Tactic:
exact fun h => ((NormedSpace.isVonNBounded_iff 𝕜).mpr h).of_topologicalSpace_le
      Dual.dual_norm_topology_le_weak_dual_topology

Premises used: Bornology.IsVonNBounded.of_topologicalSpace_le, NormedSpace.Dual.dual_norm_topology_le_weak_dual_topology
-- Module: Mathlib.Analysis.Normed.Module.WeakDual
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
⊢ ∀ (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
-- Module: Mathlib.Analysis.Normed.Module.WeakDual
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
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
⊢ 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)⟩

Premises used: le_of_lt, Exists, banach_steinhaus, _private.0.WeakDual.isBounded_iff_isVonNBounded.match_1, Exists.intro, Subtype.val, Subtype.property
-- Module: Mathlib.Analysis.Normed.Module.WeakDual
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
mpr :
  ∃ (C : ℝ),
    ∀ (x : StrongDual 𝕜 E),
      Membership.mem (γ := Set (StrongDual 𝕜 E)) ((⇑StrongDual.toWeakDual : (a : StrongDual 𝕜 E) → WeakDual 𝕜 E) ⁻¹' s)
          x →
        ‖x‖ ≤ C
⊢ Bornology.IsBounded s

Tactic:
rw [← isBounded_toWeakDual_preimage_iff_isBounded, isBounded_iff_forall_norm_le]

Premises used: isBounded_iff_forall_norm_le, WeakDual.isBounded_toWeakDual_preimage_iff_isBounded