awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Operator.Completeness
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
Fₗ : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup Fₗ
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NontriviallyNormedField 𝕜₂
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedSpace 𝕜₂ F
inst_7 : NormedSpace 𝕜 Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
f_1 g_1 : E →SL[σ₁₂] F
E' : Type u_6
inst_8 : SeminormedAddCommGroup E'
inst_9 : NormedSpace 𝕜 E'
inst_10 : RingHomIsometric σ₁₂
f : E' → F
s : Set (E' →SL[σ₁₂] F)
hs : Bornology.IsBounded s
hf :
  Membership.mem (γ := Set ((a : E') → F)) (closure[Pi.topologicalSpace] (DFunLike.coe (β := fun (x : E') ↦ F) '' s)) f
C : ℝ
hC : ∀ x ∈ s, ‖x‖ ≤ C
this : ∀ (x : E'), IsClosed[Pi.topologicalSpace] {g : E' → F | ‖g x‖ ≤ C * ‖x‖}
x : E'
g : E' →SL[σ₁₂] F
hg : g ∈ s
⊢ Membership.mem (γ := Set (E' →SL[σ₁₂] F))
    (preimage (β := E' → F) (DFunLike.coe (β := fun (x : E') ↦ F)) {g : E' → F | ‖g x‖ ≤ C * ‖x‖}) g

Tactic:
g.le_of_opNorm_le (hC _ hg) _

Premises used: Set.Mem, setOf, ContinuousLinearMap.le_of_opNorm_le, Set.preimage
-- Module: Mathlib.Analysis.Normed.Operator.Completeness
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
Fₗ : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup Fₗ
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NontriviallyNormedField 𝕜₂
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedSpace 𝕜₂ F
inst_7 : NormedSpace 𝕜 Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
f_1 g_1 : E →SL[σ₁₂] F
E' : Type u_6
inst_8 : SeminormedAddCommGroup E'
inst_9 : NormedSpace 𝕜 E'
inst_10 : RingHomIsometric σ₁₂
f : E' → F
s : Set (E' →SL[σ₁₂] F)
hs : Bornology.IsBounded s
hf :
  Membership.mem (γ := Set ((a : E') → F)) (closure[Pi.topologicalSpace] (DFunLike.coe (β := fun (x : E') ↦ F) '' s)) f
C : ℝ
hC : ∀ x ∈ s, ‖x‖ ≤ C
this : ∀ (x : E'), IsClosed[Pi.topologicalSpace] {g : E' → F | ‖g x‖ ≤ C * ‖x‖}
x : E'
g : E' →SL[σ₁₂] F
hg : g ∈ s
⊢ Membership.mem (γ := Set (E' →SL[σ₁₂] F))
    (preimage (β := E' → F) (DFunLike.coe (β := fun (x : E') ↦ F)) {g : E' → F | ‖g x‖ ≤ C * ‖x‖}) g

Tactic:
exact g.le_of_opNorm_le (hC _ hg) _

Premises used: ContinuousLinearMap.le_of_opNorm_le
-- Module: Mathlib.Analysis.Normed.Operator.Completeness
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NontriviallyNormedField 𝕜₂
inst_3 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
E' : Type u_6
inst_4 : SeminormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : RingHomIsometric σ₁₂
f : ℕ → E' →SL[σ₁₂] F
g : E' →SL[σ₁₂] F
hg : Tendsto (β := (x : E') → F) (fun (n : ℕ) (x : E') ↦ (f n : (a : E') → F) x) atTop (𝓝 (⇑g : (a : E') → F))
hf : CauchySeq f
rcases :
  ∀ (b : ℕ → ℝ) (hb₀ : ∀ (n : ℕ), 0 ≤ b n) (hfb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) ≤ b N)
    (hb_lim : Tendsto b atTop (𝓝 0)), Tendsto f atTop (𝓝 g)
⊢ Tendsto f atTop (𝓝 g)

Tactic:
rcases cauchySeq_iff_le_tendsto_0.1 hf with ⟨b, hb₀, hfb, hb_lim⟩

Premises used: cauchySeq_iff_le_tendsto_0, Iff.mp
-- Module: Mathlib.Analysis.Normed.Operator.Completeness
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NontriviallyNormedField 𝕜₂
inst_3 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
E' : Type u_6
inst_4 : SeminormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : RingHomIsometric σ₁₂
f : ℕ → E' →SL[σ₁₂] F
g : E' →SL[σ₁₂] F
hg : Tendsto (β := (x : E') → F) (fun (n : ℕ) (x : E') ↦ (f n : (a : E') → F) x) atTop (𝓝 (⇑g : (a : E') → F))
hf : CauchySeq f
b : ℕ → ℝ
hb₀ : ∀ (n : ℕ), 0 ≤ b n
hfb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) ≤ b N
hb_lim : Tendsto b atTop (𝓝 0)
⊢ ∀ (n m N : ℕ), N ≤ n → N ≤ m → ‖f n - f m‖ ≤ b N

Tactic:
simp_rw [dist_eq_norm] at hfb

Premises used: dist_eq_norm
-- Module: Mathlib.Analysis.Normed.Operator.Completeness
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NontriviallyNormedField 𝕜₂
inst_3 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
E' : Type u_6
inst_4 : SeminormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : RingHomIsometric σ₁₂
f : ℕ → E' →SL[σ₁₂] F
g : E' →SL[σ₁₂] F
hg : Tendsto (β := (x : E') → F) (fun (n : ℕ) (x : E') ↦ (f n : (a : E') → F) x) atTop (𝓝 (⇑g : (a : E') → F))
hf : CauchySeq f
b : ℕ → ℝ
hb₀ : ∀ (n : ℕ), 0 ≤ b n
hb_lim : Tendsto b atTop (𝓝 0)
hfb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → ‖f n - f m‖ ≤ b N
suffices :
  ∀ (n : ℕ) (x : E'), ‖HSub.hSub (α := F) (β := F) ((f n : (a : E') → F) x : F) ((g : (a : E') → F) x : F)‖ ≤ b n * ‖x‖
⊢ Tendsto f atTop (𝓝 g)

Tactic:
suffices ∀ n x, ‖f n x - g x‖ ≤ b n * ‖x‖ from
    tendsto_iff_norm_sub_tendsto_zero.2
    (squeeze_zero (fun n => norm_nonneg _) (fun n => opNorm_le_bound _ (hb₀ n) (this n)) hb_lim)
-- Module: Mathlib.Analysis.Normed.Operator.Completeness
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NontriviallyNormedField 𝕜₂
inst_3 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
E' : Type u_6
inst_4 : SeminormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : RingHomIsometric σ₁₂
f : ℕ → E' →SL[σ₁₂] F
g : E' →SL[σ₁₂] F
hg : Tendsto (β := (x : E') → F) (fun (n : ℕ) (x : E') ↦ (f n : (a : E') → F) x) atTop (𝓝 (⇑g : (a : E') → F))
hf : CauchySeq f
b : ℕ → ℝ
hb₀ : ∀ (n : ℕ), 0 ≤ b n
hb_lim : Tendsto b atTop (𝓝 0)
hfb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → ‖f n - f m‖ ≤ b N
n : ℕ
x : E'
⊢ Tendsto (fun (m : ℕ) ↦ ‖HSub.hSub (α := F) (β := F) ((f n : (a : E') → F) x : F) ((f m : (a : E') → F) x : F)‖) atTop
    (𝓝 ‖HSub.hSub (α := F) (β := F) ((f n : (a : E') → F) x : F) ((g : (a : E') → F) x : F)‖)

Tactic:
have : Tendsto (fun m => ‖f n x - f m x‖) atTop (𝓝 ‖f n x - g x‖) :=
    (tendsto_const_nhds.sub <| tendsto_pi_nhds.1 hg _).norm
-- Module: Mathlib.Analysis.Normed.Operator.Completeness
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NontriviallyNormedField 𝕜₂
inst_3 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
E' : Type u_6
inst_4 : SeminormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : RingHomIsometric σ₁₂
f : ℕ → E' →SL[σ₁₂] F
g : E' →SL[σ₁₂] F
hg : Tendsto (β := (x : E') → F) (fun (n : ℕ) (x : E') ↦ (f n : (a : E') → F) x) atTop (𝓝 (⇑g : (a : E') → F))
hf : CauchySeq f
b : ℕ → ℝ
hb₀ : ∀ (n : ℕ), 0 ≤ b n
hb_lim : Tendsto b atTop (𝓝 0)
hfb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → ‖f n - f m‖ ≤ b N
n : ℕ
x : E'
this :
  Tendsto (fun (m : ℕ) ↦ ‖HSub.hSub (α := F) (β := F) ((f n : (a : E') → F) x : F) ((f m : (a : E') → F) x : F)‖) atTop
    (𝓝 ‖HSub.hSub (α := F) (β := F) ((f n : (a : E') → F) x : F) ((g : (a : E') → F) x : F)‖)
⊢ ‖HSub.hSub (α := F) (β := F) ((f n : (a : E') → F) x : F) ((g : (a : E') → F) x : F)‖ ≤ b n * ‖x‖

Tactic:
le_of_tendsto this (eventually_atTop.2 ⟨n, fun m hm => ?_⟩)

Premises used: Iff.mpr, le_of_tendsto, Exists.intro, Filter.eventually_atTop
-- Module: Mathlib.Analysis.Normed.Operator.Completeness
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NontriviallyNormedField 𝕜₂
inst_3 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
E' : Type u_6
inst_4 : SeminormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : RingHomIsometric σ₁₂
f : ℕ → E' →SL[σ₁₂] F
g : E' →SL[σ₁₂] F
hg : Tendsto (β := (x : E') → F) (fun (n : ℕ) (x : E') ↦ (f n : (a : E') → F) x) atTop (𝓝 (⇑g : (a : E') → F))
hf : CauchySeq f
b : ℕ → ℝ
hb₀ : ∀ (n : ℕ), 0 ≤ b n
hb_lim : Tendsto b atTop (𝓝 0)
hfb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → ‖f n - f m‖ ≤ b N
n : ℕ
x : E'
this :
  Tendsto (fun (m : ℕ) ↦ ‖HSub.hSub (α := F) (β := F) ((f n : (a : E') → F) x : F) ((f m : (a : E') → F) x : F)‖) atTop
    (𝓝 ‖HSub.hSub (α := F) (β := F) ((f n : (a : E') → F) x : F) ((g : (a : E') → F) x : F)‖)
refine :
  ∀ (m : ℕ) (hm : m ≥ n),
    ‖HSub.hSub (α := F) (β := F) ((f n : (a : E') → F) x : F) ((f m : (a : E') → F) x : F)‖ ≤ b n * ‖x‖
⊢ ‖HSub.hSub (α := F) (β := F) ((f n : (a : E') → F) x : F) ((g : (a : E') → F) x : F)‖ ≤ b n * ‖x‖

Tactic:
refine le_of_tendsto this (eventually_atTop.2 ⟨n, fun m hm => ?_⟩)

Premises used: Iff.mpr, le_of_tendsto, Exists.intro, Filter.eventually_atTop
-- Module: Mathlib.Analysis.Normed.Operator.Completeness
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NontriviallyNormedField 𝕜₂
inst_3 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
E' : Type u_6
inst_4 : SeminormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : RingHomIsometric σ₁₂
f : ℕ → E' →SL[σ₁₂] F
g : E' →SL[σ₁₂] F
hg : Tendsto (β := (x : E') → F) (fun (n : ℕ) (x : E') ↦ (f n : (a : E') → F) x) atTop (𝓝 (⇑g : (a : E') → F))
hf : CauchySeq f
b : ℕ → ℝ
hb₀ : ∀ (n : ℕ), 0 ≤ b n
hb_lim : Tendsto b atTop (𝓝 0)
hfb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → ‖f n - f m‖ ≤ b N
n : ℕ
x : E'
this :
  Tendsto (fun (m : ℕ) ↦ ‖HSub.hSub (α := F) (β := F) ((f n : (a : E') → F) x : F) ((f m : (a : E') → F) x : F)‖) atTop
    (𝓝 ‖HSub.hSub (α := F) (β := F) ((f n : (a : E') → F) x : F) ((g : (a : E') → F) x : F)‖)
m : ℕ
hm : m ≥ n
⊢ ‖HSub.hSub (α := F) (β := F) ((f n : (a : E') → F) x : F) ((f m : (a : E') → F) x : F)‖ ≤ b n * ‖x‖

Tactic:
(f n - f m).le_of_opNorm_le (hfb _ _ _ le_rfl hm) _

Premises used: le_rfl, HSub.hSub, ContinuousLinearMap.le_of_opNorm_le
-- Module: Mathlib.Analysis.Normed.Operator.Completeness
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NontriviallyNormedField 𝕜₂
inst_3 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
E' : Type u_6
inst_4 : SeminormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : RingHomIsometric σ₁₂
f : ℕ → E' →SL[σ₁₂] F
g : E' →SL[σ₁₂] F
hg : Tendsto (β := (x : E') → F) (fun (n : ℕ) (x : E') ↦ (f n : (a : E') → F) x) atTop (𝓝 (⇑g : (a : E') → F))
hf : CauchySeq f
b : ℕ → ℝ
hb₀ : ∀ (n : ℕ), 0 ≤ b n
hb_lim : Tendsto b atTop (𝓝 0)
hfb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → ‖f n - f m‖ ≤ b N
n : ℕ
x : E'
this :
  Tendsto (fun (m : ℕ) ↦ ‖HSub.hSub (α := F) (β := F) ((f n : (a : E') → F) x : F) ((f m : (a : E') → F) x : F)‖) atTop
    (𝓝 ‖HSub.hSub (α := F) (β := F) ((f n : (a : E') → F) x : F) ((g : (a : E') → F) x : F)‖)
m : ℕ
hm : m ≥ n
⊢ ‖HSub.hSub (α := F) (β := F) ((f n : (a : E') → F) x : F) ((f m : (a : E') → F) x : F)‖ ≤ b n * ‖x‖

Tactic:
exact (f n - f m).le_of_opNorm_le (hfb _ _ _ le_rfl hm) _

Premises used: le_rfl, HSub.hSub, ContinuousLinearMap.le_of_opNorm_le
-- Module: Mathlib.Analysis.Normed.Operator.Completeness
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NontriviallyNormedField 𝕜₂
inst_3 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
E' : Type u_6
inst_4 : SeminormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : RingHomIsometric σ₁₂
inst_7 : ProperSpace F
s : Set (E' →SL[σ₁₂] F)
hb : Bornology.IsBounded s
⊢ IsCompact (X := (a : E') → F) (closure[Pi.topologicalSpace] (DFunLike.coe (β := fun (x : E') ↦ F) '' s))

Tactic:
have : ∀ x, IsCompact (closure (apply' F σ₁₂ x '' s)) := fun x =>
    ((apply' F σ₁₂ x).lipschitz.isBounded_image hb).isCompact_closure
  (isCompact_pi_infinite this).closure_of_subset
    (image_subset_iff.2 fun _ hg _ => subset_closure <| mem_image_of_mem _ hg)

Premises used: Iff.mpr, subset_closure, ContinuousLinearMap.lipschitz, isCompact_pi_infinite, Bornology.IsBounded.isCompact_closure, LipschitzWith.isBounded_image, Set.mem_image_of_mem, Set.image_subset_iff, DFunLike.coe, IsCompact.closure_of_subset, ContinuousLinearMap.apply'
-- Module: Mathlib.Analysis.Normed.Operator.Completeness
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NontriviallyNormedField 𝕜₂
inst_3 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
E' : Type u_6
inst_4 : SeminormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : RingHomIsometric σ₁₂
inst_7 : ProperSpace F
s : Set (E' →SL[σ₁₂] F)
hb : Bornology.IsBounded s
hc : IsClosed[Pi.topologicalSpace] (DFunLike.coe (β := fun (x : E') ↦ F) '' s)
⊢ IsCompact (X := (a : E') → F) (DFunLike.coe (β := fun (x : E') ↦ F) '' s)

Tactic:
hc.closure_eq ▸ isCompact_closure_image_coe_of_bounded hb

Premises used: IsClosed.closure_eq, Eq.rec, ContinuousLinearMap.isCompact_closure_image_coe_of_bounded
-- Module: Mathlib.Analysis.Normed.Operator.Completeness
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NontriviallyNormedField 𝕜₂
inst_3 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
E' : Type u_6
inst_4 : SeminormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : RingHomIsometric σ₁₂
s : Set (E' →SL[σ₁₂] F)
hb : Bornology.IsBounded s
hc :
  ∀ (f : E' →SL[σ₁₂] F),
    Membership.mem (γ := Set ((a : E') → F)) (closure[Pi.topologicalSpace] (DFunLike.coe (β := fun (x : E') ↦ F) '' s))
        (⇑f : (a : E') → F) →
      f ∈ s
⊢ IsClosed[Pi.topologicalSpace] (DFunLike.coe (β := fun (x : E') ↦ F) '' s)

Tactic:
isClosed_of_closure_subset fun f hf =>
    ⟨ofMemClosureImageCoeBounded f hb hf, hc (ofMemClosureImageCoeBounded f hb hf) hf, rfl⟩

Premises used: ContinuousLinearMap.ofMemClosureImageCoeBounded, And.intro, Exists.intro, isClosed_of_closure_subset, rfl
-- Module: Mathlib.Analysis.Normed.Operator.Completeness
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NontriviallyNormedField 𝕜₂
inst_3 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
E' : Type u_6
inst_4 : SeminormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : RingHomIsometric σ₁₂
inst_7 : ProperSpace F
s : Set (E' →SL[σ₁₂] F)
hb : Bornology.IsBounded s
hc :
  ∀ (f : E' →SL[σ₁₂] F),
    Membership.mem (γ := Set ((a : E') → F)) (closure[Pi.topologicalSpace] (DFunLike.coe (β := fun (x : E') ↦ F) '' s))
        (⇑f : (a : E') → F) →
      f ∈ s
⊢ IsCompact (X := (a : E') → F) (DFunLike.coe (β := fun (x : E') ↦ F) '' s)

Tactic:
isCompact_image_coe_of_bounded_of_closed_image hb <|
    isClosed_image_coe_of_bounded_of_weak_closed hb hc

Premises used: ContinuousLinearMap.isCompact_image_coe_of_bounded_of_closed_image, ContinuousLinearMap.isClosed_image_coe_of_bounded_of_weak_closed
-- Module: Mathlib.Analysis.Normed.Operator.Completeness
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NontriviallyNormedField 𝕜₂
inst_3 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
E' : Type u_6
inst_4 : SeminormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : RingHomIsometric σ₁₂
f₀ : E' →SL[σ₁₂] F
r : ℝ
f : E' →SL[σ₁₂] F
hf :
  Membership.mem (γ := Set ((a : E') → F))
    (closure[Pi.topologicalSpace] (DFunLike.coe (β := fun (x : E') ↦ F) '' closedBall f₀ r)) (⇑f : (a : E') → F)
⊢ 0 ≤ r

Tactic:
have hr : 0 ≤ r := nonempty_closedBall.1 (closure_nonempty_iff.1 ⟨_, hf⟩).of_image
-- Module: Mathlib.Analysis.Normed.Operator.Completeness
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NontriviallyNormedField 𝕜₂
inst_3 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
E' : Type u_6
inst_4 : SeminormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : RingHomIsometric σ₁₂
f₀ : E' →SL[σ₁₂] F
r : ℝ
f : E' →SL[σ₁₂] F
hf :
  Membership.mem (γ := Set ((a : E') → F))
    (closure[Pi.topologicalSpace] (DFunLike.coe (β := fun (x : E') ↦ F) '' closedBall f₀ r)) (⇑f : (a : E') → F)
hr : 0 ≤ r
⊢ f ∈ closedBall f₀ r

Tactic:
mem_closedBall_iff_norm.2 (opNorm_le_bound _ hr fun x => ?_)

Premises used: Iff.mpr, Set.Mem, mem_closedBall_iff_norm, ContinuousLinearMap.opNorm_le_bound
-- Module: Mathlib.Analysis.Normed.Operator.Completeness
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NontriviallyNormedField 𝕜₂
inst_3 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
E' : Type u_6
inst_4 : SeminormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : RingHomIsometric σ₁₂
f₀ : E' →SL[σ₁₂] F
r : ℝ
f : E' →SL[σ₁₂] F
hf :
  Membership.mem (γ := Set ((a : E') → F))
    (closure[Pi.topologicalSpace] (DFunLike.coe (β := fun (x : E') ↦ F) '' closedBall f₀ r)) (⇑f : (a : E') → F)
hr : 0 ≤ r
refine : ∀ (x : E'), Norm.norm.{u_4} (E := F) ((f - f₀ : (a : E') → F) x : F) ≤ r * ‖x‖
⊢ f ∈ closedBall f₀ r

Tactic:
refine mem_closedBall_iff_norm.2 (opNorm_le_bound _ hr fun x => ?_)

Premises used: Iff.mpr, mem_closedBall_iff_norm
-- Module: Mathlib.Analysis.Normed.Operator.Completeness
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NontriviallyNormedField 𝕜₂
inst_3 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
E' : Type u_6
inst_4 : SeminormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : RingHomIsometric σ₁₂
f₀ : E' →SL[σ₁₂] F
r : ℝ
f : E' →SL[σ₁₂] F
hf :
  Membership.mem (γ := Set ((a : E') → F))
    (closure[Pi.topologicalSpace] (DFunLike.coe (β := fun (x : E') ↦ F) '' closedBall f₀ r)) (⇑f : (a : E') → F)
hr : 0 ≤ r
x : E'
⊢ IsClosed[Pi.topologicalSpace] {g : E' → F | ‖HSub.hSub (β := F) (g x) ((f₀ : (a : E') → F) x : F)‖ ≤ r * ‖x‖}

Tactic:
have : IsClosed { g : E' → F | ‖g x - f₀ x‖ ≤ r * ‖x‖ } :=
    isClosed_Iic.preimage ((@continuous_apply E' (fun _ => F) _ x).sub continuous_const).norm
-- Module: Mathlib.Analysis.Normed.Operator.Completeness
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NontriviallyNormedField 𝕜₂
inst_3 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
E' : Type u_6
inst_4 : SeminormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : RingHomIsometric σ₁₂
f₀ : E' →SL[σ₁₂] F
r : ℝ
f : E' →SL[σ₁₂] F
hf :
  Membership.mem (γ := Set ((a : E') → F))
    (closure[Pi.topologicalSpace] (DFunLike.coe (β := fun (x : E') ↦ F) '' closedBall f₀ r)) (⇑f : (a : E') → F)
hr : 0 ≤ r
x : E'
this : IsClosed[Pi.topologicalSpace] {g : E' → F | ‖HSub.hSub (β := F) (g x) ((f₀ : (a : E') → F) x : F)‖ ≤ r * ‖x‖}
⊢ Norm.norm.{u_4} (E := F) ((f - f₀ : (a : E') → F) x : F) ≤ r * ‖x‖

Tactic:
this.closure_subset_iff.2 (image_subset_iff.2 fun g hg => ?_) hf

Premises used: Iff.mpr, Set.Mem, IsClosed.closure_subset_iff, Set.image_subset_iff
-- Module: Mathlib.Analysis.Normed.Operator.Completeness
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NontriviallyNormedField 𝕜₂
inst_3 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
E' : Type u_6
inst_4 : SeminormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : RingHomIsometric σ₁₂
f₀ : E' →SL[σ₁₂] F
r : ℝ
f : E' →SL[σ₁₂] F
hf :
  Membership.mem (γ := Set ((a : E') → F))
    (closure[Pi.topologicalSpace] (DFunLike.coe (β := fun (x : E') ↦ F) '' closedBall f₀ r)) (⇑f : (a : E') → F)
hr : 0 ≤ r
x : E'
this : IsClosed[Pi.topologicalSpace] {g : E' → F | ‖HSub.hSub (β := F) (g x) ((f₀ : (a : E') → F) x : F)‖ ≤ r * ‖x‖}
refine :
  ∀ (g : E' →SL[σ₁₂] F) (hg : g ∈ closedBall f₀ r),
    Membership.mem (γ := Set (E' →SL[σ₁₂] F))
      (preimage (β := E' → F) (DFunLike.coe (β := fun (x : E') ↦ F))
        {g : E' → F | ‖HSub.hSub (β := F) (g x) ((f₀ : (a : E') → F) x : F)‖ ≤ r * ‖x‖})
      g
⊢ Norm.norm.{u_4} (E := F) ((f - f₀ : (a : E') → F) x : F) ≤ r * ‖x‖

Tactic:
refine this.closure_subset_iff.2 (image_subset_iff.2 fun g hg => ?_) hf

Premises used: Iff.mpr, IsClosed.closure_subset_iff, Set.image_subset_iff
-- Module: Mathlib.Analysis.Normed.Operator.Completeness
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NontriviallyNormedField 𝕜₂
inst_3 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
E' : Type u_6
inst_4 : SeminormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : RingHomIsometric σ₁₂
f₀ : E' →SL[σ₁₂] F
r : ℝ
f : E' →SL[σ₁₂] F
hf :
  Membership.mem (γ := Set ((a : E') → F))
    (closure[Pi.topologicalSpace] (DFunLike.coe (β := fun (x : E') ↦ F) '' closedBall f₀ r)) (⇑f : (a : E') → F)
hr : 0 ≤ r
x : E'
this : IsClosed[Pi.topologicalSpace] {g : E' → F | ‖HSub.hSub (β := F) (g x) ((f₀ : (a : E') → F) x : F)‖ ≤ r * ‖x‖}
g : E' →SL[σ₁₂] F
hg : g ∈ closedBall f₀ r
⊢ Membership.mem (γ := Set (E' →SL[σ₁₂] F))
    (preimage (β := E' → F) (DFunLike.coe (β := fun (x : E') ↦ F))
      {g : E' → F | ‖HSub.hSub (β := F) (g x) ((f₀ : (a : E') → F) x : F)‖ ≤ r * ‖x‖})
    g

Tactic:
(g - f₀).le_of_opNorm_le (mem_closedBall_iff_norm.1 hg) _

Premises used: Set.Mem, setOf, mem_closedBall_iff_norm, HSub.hSub, ContinuousLinearMap.le_of_opNorm_le, Set.preimage, Iff.mp
-- Module: Mathlib.Analysis.Normed.Operator.Completeness
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NontriviallyNormedField 𝕜₂
inst_3 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
E' : Type u_6
inst_4 : SeminormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : RingHomIsometric σ₁₂
f₀ : E' →SL[σ₁₂] F
r : ℝ
f : E' →SL[σ₁₂] F
hf :
  Membership.mem (γ := Set ((a : E') → F))
    (closure[Pi.topologicalSpace] (DFunLike.coe (β := fun (x : E') ↦ F) '' closedBall f₀ r)) (⇑f : (a : E') → F)
hr : 0 ≤ r
x : E'
this : IsClosed[Pi.topologicalSpace] {g : E' → F | ‖HSub.hSub (β := F) (g x) ((f₀ : (a : E') → F) x : F)‖ ≤ r * ‖x‖}
g : E' →SL[σ₁₂] F
hg : g ∈ closedBall f₀ r
⊢ Membership.mem (γ := Set (E' →SL[σ₁₂] F))
    (preimage (β := E' → F) (DFunLike.coe (β := fun (x : E') ↦ F))
      {g : E' → F | ‖HSub.hSub (β := F) (g x) ((f₀ : (a : E') → F) x : F)‖ ≤ r * ‖x‖})
    g

Tactic:
exact (g - f₀).le_of_opNorm_le (mem_closedBall_iff_norm.1 hg) _

Premises used: mem_closedBall_iff_norm, HSub.hSub, ContinuousLinearMap.le_of_opNorm_le, Iff.mp
-- Module: Mathlib.Analysis.Normed.Operator.Completeness
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f₀ : E →SL[σ₁₂] F
r : ℝ
⊢ IsClosed[Pi.topologicalSpace] (DFunLike.coe (β := fun (x : E) ↦ F) '' closedBall f₀ r)

Tactic:
isClosed_image_coe_of_bounded_of_weak_closed isBounded_closedBall (is_weak_closed_closedBall f₀ r)

Premises used: Metric.isBounded_closedBall, ContinuousLinearMap.isClosed_image_coe_of_bounded_of_weak_closed, ContinuousLinearMap.is_weak_closed_closedBall
-- Module: Mathlib.Analysis.Normed.Operator.Completeness
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
inst_7 : ProperSpace F
f₀ : E →SL[σ₁₂] F
r : ℝ
⊢ IsCompact (X := (a : E) → F) (DFunLike.coe (β := fun (x : E) ↦ F) '' closedBall f₀ r)

Tactic:
isCompact_image_coe_of_bounded_of_weak_closed isBounded_closedBall <|
    is_weak_closed_closedBall f₀ r

Premises used: Metric.isBounded_closedBall, ContinuousLinearMap.isCompact_image_coe_of_bounded_of_weak_closed, ContinuousLinearMap.is_weak_closed_closedBall
-- Module: Mathlib.Analysis.Normed.Operator.Conformal
Goal:
R : Type u_1
M : Type u_2
inst : NormedField R
inst_1 : SeminormedAddCommGroup M
inst_2 : NormedSpace R M
⊢ ContinuousLinearMap.id R M =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →L[R] M) 1 (toContinuousLinearMap LinearIsometry.id)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Operator.Conformal
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : NormedField R
inst_1 : SeminormedAddCommGroup M
inst_2 : SeminormedAddCommGroup N
inst_3 : NormedSpace R M
inst_4 : NormedSpace R N
f : M →L[R] N
hf : IsConformalMap f
c : R
hc : c ≠ 0
rcases : ∀ (c' : R) (hc' : c' ≠ 0) (li : M →ₗᵢ[R] N), IsConformalMap (c • c' • li.toContinuousLinearMap)
⊢ IsConformalMap (c • f)

Tactic:
rcases hf with ⟨c', hc', li, rfl⟩

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Operator.Conformal
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : NormedField R
inst_1 : SeminormedAddCommGroup M
inst_2 : SeminormedAddCommGroup N
inst_3 : NormedSpace R M
inst_4 : NormedSpace R N
c : R
hc : c ≠ 0
c' : R
hc' : c' ≠ 0
li : M →ₗᵢ[R] N
⊢ IsConformalMap (c • c' • li.toContinuousLinearMap)

Tactic:
⟨c * c', mul_ne_zero hc hc', li, smul_smul _ _ _⟩

Premises used: HMul.hMul, smul_smul, And.intro, Exists.intro, mul_ne_zero, IsConformalMap