awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Operator.CompleteCodomain
Goal:
𝕜 : Type u_1
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_4
inst_3 : Finite ι
M : ι → Type u_5
inst_4 : (i : ι) → NormedAddCommGroup (M i)
inst_5 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (M i)
inst_6 : ∀ (i : ι), SeparatingDual.{u_1, u_5} 𝕜 (M i)
inst_7 : CompleteSpace (ContinuousMultilinearMap 𝕜 M F)
m : (i : ι) → M i
hm : ∀ (i : ι), m i ≠ 0
f : ℕ → F
hf : CauchySeq f
φ : (i : ι) → StrongDual.{u_1, u_5} 𝕜 (M i)
hφ : ∀ (i : ι), Eq.{u_1 + 1} (α := 𝕜) ((φ i : (a : M i) → 𝕜) (m i) : 𝕜) (1 : 𝕜)
val : Fintype ι
g : ℕ → ContinuousMultilinearMap 𝕜 M F :=
  fun (n : ℕ) ↦
    ((compContinuousLinearMapL.{u_1, u_4, u_5, u_3, u_1} (𝕜 := 𝕜) (E := M) (F := F) (E₁ := fun (i : ι) ↦ 𝕜) φ :
          ContinuousMultilinearMap 𝕜 (fun (i : ι) ↦ 𝕜) F →L[𝕜] ContinuousMultilinearMap 𝕜 M F) :
        (a : ContinuousMultilinearMap 𝕜 (fun (i : ι) ↦ 𝕜) F) → ContinuousMultilinearMap 𝕜 M F)
      ((((smulRightL 𝕜 (fun (x : ι) ↦ 𝕜) F :
                (a : ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) 𝕜) →
                  F →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) F)
              (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι 𝕜) :
            F →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) F) :
          (a : F) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) F)
        (f n))
⊢ CauchySeq (α := ContinuousMultilinearMap 𝕜 (fun (i : ι) ↦ 𝕜) F) fun (n : ℕ) ↦
    (((smulRightL 𝕜 (fun (x : ι) ↦ 𝕜) F :
              (a : ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) 𝕜) →
                F →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) F)
            (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι 𝕜) :
          F →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) F) :
        (a : F) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) F)
      (f n)

Tactic:
exact (ContinuousLinearMap.lipschitz _).cauchySeq_comp hf

Premises used: ContinuousLinearMap.lipschitz, LipschitzWith.cauchySeq_comp
-- Module: Mathlib.Analysis.Normed.Operator.CompleteCodomain
Goal:
𝕜 : Type u_1
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_4
inst_3 : Finite ι
M : ι → Type u_5
inst_4 : (i : ι) → NormedAddCommGroup (M i)
inst_5 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (M i)
inst_6 : ∀ (i : ι), SeparatingDual.{u_1, u_5} 𝕜 (M i)
inst_7 : CompleteSpace (ContinuousMultilinearMap 𝕜 M F)
m : (i : ι) → M i
hm : ∀ (i : ι), m i ≠ 0
f : ℕ → F
hf : CauchySeq f
φ : (i : ι) → StrongDual.{u_1, u_5} 𝕜 (M i)
hφ : ∀ (i : ι), Eq.{u_1 + 1} (α := 𝕜) ((φ i : (a : M i) → 𝕜) (m i) : 𝕜) (1 : 𝕜)
val : Fintype ι
g : ℕ → ContinuousMultilinearMap 𝕜 M F :=
  fun (n : ℕ) ↦
    ((compContinuousLinearMapL.{u_1, u_4, u_5, u_3, u_1} (𝕜 := 𝕜) (E := M) (F := F) (E₁ := fun (i : ι) ↦ 𝕜) φ :
          ContinuousMultilinearMap 𝕜 (fun (i : ι) ↦ 𝕜) F →L[𝕜] ContinuousMultilinearMap 𝕜 M F) :
        (a : ContinuousMultilinearMap 𝕜 (fun (i : ι) ↦ 𝕜) F) → ContinuousMultilinearMap 𝕜 M F)
      ((((smulRightL 𝕜 (fun (x : ι) ↦ 𝕜) F :
                (a : ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) 𝕜) →
                  F →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) F)
              (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι 𝕜) :
            F →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) F) :
          (a : F) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) F)
        (f n))
⊢ CauchySeq g

Tactic:
have : CauchySeq g := by
    refine (ContinuousLinearMap.lipschitz _).cauchySeq_comp ?_
    exact (ContinuousLinearMap.lipschitz _).cauchySeq_comp hf
-- Module: Mathlib.Analysis.Normed.Operator.CompleteCodomain
Goal:
𝕜 : Type u_1
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_4
inst_3 : Finite ι
M : ι → Type u_5
inst_4 : (i : ι) → NormedAddCommGroup (M i)
inst_5 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (M i)
inst_6 : ∀ (i : ι), SeparatingDual.{u_1, u_5} 𝕜 (M i)
inst_7 : CompleteSpace (ContinuousMultilinearMap 𝕜 M F)
m : (i : ι) → M i
hm : ∀ (i : ι), m i ≠ 0
f : ℕ → F
hf : CauchySeq f
φ : (i : ι) → StrongDual.{u_1, u_5} 𝕜 (M i)
hφ : ∀ (i : ι), Eq.{u_1 + 1} (α := 𝕜) ((φ i : (a : M i) → 𝕜) (m i) : 𝕜) (1 : 𝕜)
val : Fintype ι
g : ℕ → ContinuousMultilinearMap 𝕜 M F :=
  fun (n : ℕ) ↦
    ((compContinuousLinearMapL.{u_1, u_4, u_5, u_3, u_1} (𝕜 := 𝕜) (E := M) (F := F) (E₁ := fun (i : ι) ↦ 𝕜) φ :
          ContinuousMultilinearMap 𝕜 (fun (i : ι) ↦ 𝕜) F →L[𝕜] ContinuousMultilinearMap 𝕜 M F) :
        (a : ContinuousMultilinearMap 𝕜 (fun (i : ι) ↦ 𝕜) F) → ContinuousMultilinearMap 𝕜 M F)
      ((((smulRightL 𝕜 (fun (x : ι) ↦ 𝕜) F :
                (a : ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) 𝕜) →
                  F →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) F)
              (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι 𝕜) :
            F →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) F) :
          (a : F) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) F)
        (f n))
this : CauchySeq g
⊢ ∃ (a : ContinuousMultilinearMap 𝕜 M F), Tendsto g atTop (𝓝 a)

Tactic:
cauchy_iff_exists_le_nhds.mp this

Premises used: Set.Mem, cauchy_iff_exists_le_nhds, Filter.Tendsto, Iff.mp
-- Module: Mathlib.Analysis.Normed.Operator.CompleteCodomain
Goal:
𝕜 : Type u_1
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_4
inst_3 : Finite ι
M : ι → Type u_5
inst_4 : (i : ι) → NormedAddCommGroup (M i)
inst_5 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (M i)
inst_6 : ∀ (i : ι), SeparatingDual.{u_1, u_5} 𝕜 (M i)
inst_7 : CompleteSpace (ContinuousMultilinearMap 𝕜 M F)
m : (i : ι) → M i
hm : ∀ (i : ι), m i ≠ 0
f : ℕ → F
hf : CauchySeq f
φ : (i : ι) → StrongDual.{u_1, u_5} 𝕜 (M i)
hφ : ∀ (i : ι), Eq.{u_1 + 1} (α := 𝕜) ((φ i : (a : M i) → 𝕜) (m i) : 𝕜) (1 : 𝕜)
val : Fintype ι
g : ℕ → ContinuousMultilinearMap 𝕜 M F :=
  fun (n : ℕ) ↦
    ((compContinuousLinearMapL.{u_1, u_4, u_5, u_3, u_1} (𝕜 := 𝕜) (E := M) (F := F) (E₁ := fun (i : ι) ↦ 𝕜) φ :
          ContinuousMultilinearMap 𝕜 (fun (i : ι) ↦ 𝕜) F →L[𝕜] ContinuousMultilinearMap 𝕜 M F) :
        (a : ContinuousMultilinearMap 𝕜 (fun (i : ι) ↦ 𝕜) F) → ContinuousMultilinearMap 𝕜 M F)
      ((((smulRightL 𝕜 (fun (x : ι) ↦ 𝕜) F :
                (a : ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) 𝕜) →
                  F →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) F)
              (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι 𝕜) :
            F →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) F) :
          (a : F) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) F)
        (f n))
this : CauchySeq g
intro : ∀ (a : ContinuousMultilinearMap 𝕜 M F) (ha : Tendsto g atTop (𝓝 a)), ∃ (a : F), Tendsto f atTop (𝓝 a)
⊢ ∃ (a : F), Tendsto f atTop (𝓝 a)

Tactic:
obtain ⟨a, ha⟩ : ∃ a, Tendsto g atTop (𝓝 a) := cauchy_iff_exists_le_nhds.mp this

Premises used: cauchy_iff_exists_le_nhds, Iff.mp
-- Module: Mathlib.Analysis.Normed.Operator.CompleteCodomain
Goal:
𝕜 : Type u_1
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_4
inst_3 : Finite ι
M : ι → Type u_5
inst_4 : (i : ι) → NormedAddCommGroup (M i)
inst_5 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (M i)
inst_6 : ∀ (i : ι), SeparatingDual.{u_1, u_5} 𝕜 (M i)
inst_7 : CompleteSpace (ContinuousMultilinearMap 𝕜 M F)
m : (i : ι) → M i
hm : ∀ (i : ι), m i ≠ 0
f : ℕ → F
hf : CauchySeq f
φ : (i : ι) → StrongDual.{u_1, u_5} 𝕜 (M i)
hφ : ∀ (i : ι), Eq.{u_1 + 1} (α := 𝕜) ((φ i : (a : M i) → 𝕜) (m i) : 𝕜) (1 : 𝕜)
val : Fintype ι
g : ℕ → ContinuousMultilinearMap 𝕜 M F :=
  fun (n : ℕ) ↦
    ((compContinuousLinearMapL.{u_1, u_4, u_5, u_3, u_1} (𝕜 := 𝕜) (E := M) (F := F) (E₁ := fun (i : ι) ↦ 𝕜) φ :
          ContinuousMultilinearMap 𝕜 (fun (i : ι) ↦ 𝕜) F →L[𝕜] ContinuousMultilinearMap 𝕜 M F) :
        (a : ContinuousMultilinearMap 𝕜 (fun (i : ι) ↦ 𝕜) F) → ContinuousMultilinearMap 𝕜 M F)
      ((((smulRightL 𝕜 (fun (x : ι) ↦ 𝕜) F :
                (a : ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) 𝕜) →
                  F →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) F)
              (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι 𝕜) :
            F →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) F) :
          (a : F) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) F)
        (f n))
this : CauchySeq g
a : ContinuousMultilinearMap 𝕜 M F
ha : Tendsto g atTop (𝓝 a)
⊢ ∃ (a : F), Tendsto f atTop (𝓝 a)

Tactic:
⟨a m, ?_⟩

Premises used: Exists.intro, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Operator.CompleteCodomain
Goal:
𝕜 : Type u_1
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_4
inst_3 : Finite ι
M : ι → Type u_5
inst_4 : (i : ι) → NormedAddCommGroup (M i)
inst_5 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (M i)
inst_6 : ∀ (i : ι), SeparatingDual.{u_1, u_5} 𝕜 (M i)
inst_7 : CompleteSpace (ContinuousMultilinearMap 𝕜 M F)
m : (i : ι) → M i
hm : ∀ (i : ι), m i ≠ 0
f : ℕ → F
hf : CauchySeq f
φ : (i : ι) → StrongDual.{u_1, u_5} 𝕜 (M i)
hφ : ∀ (i : ι), Eq.{u_1 + 1} (α := 𝕜) ((φ i : (a : M i) → 𝕜) (m i) : 𝕜) (1 : 𝕜)
val : Fintype ι
g : ℕ → ContinuousMultilinearMap 𝕜 M F :=
  fun (n : ℕ) ↦
    ((compContinuousLinearMapL.{u_1, u_4, u_5, u_3, u_1} (𝕜 := 𝕜) (E := M) (F := F) (E₁ := fun (i : ι) ↦ 𝕜) φ :
          ContinuousMultilinearMap 𝕜 (fun (i : ι) ↦ 𝕜) F →L[𝕜] ContinuousMultilinearMap 𝕜 M F) :
        (a : ContinuousMultilinearMap 𝕜 (fun (i : ι) ↦ 𝕜) F) → ContinuousMultilinearMap 𝕜 M F)
      ((((smulRightL 𝕜 (fun (x : ι) ↦ 𝕜) F :
                (a : ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) 𝕜) →
                  F →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) F)
              (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι 𝕜) :
            F →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) F) :
          (a : F) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) F)
        (f n))
this : CauchySeq g
a : ContinuousMultilinearMap 𝕜 M F
ha : Tendsto g atTop (𝓝 a)
intro : Tendsto f atTop (𝓝 ((a : (a : (i : ι) → M i) → F) m))
⊢ ∃ (a : F), Tendsto f atTop (𝓝 a)

Tactic:
refine ⟨a m, ?_⟩
-- Module: Mathlib.Analysis.Normed.Operator.CompleteCodomain
Goal:
𝕜 : Type u_1
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_4
inst_3 : Finite ι
M : ι → Type u_5
inst_4 : (i : ι) → NormedAddCommGroup (M i)
inst_5 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (M i)
inst_6 : ∀ (i : ι), SeparatingDual.{u_1, u_5} 𝕜 (M i)
inst_7 : CompleteSpace (ContinuousMultilinearMap 𝕜 M F)
m : (i : ι) → M i
hm : ∀ (i : ι), m i ≠ 0
f : ℕ → F
hf : CauchySeq f
φ : (i : ι) → StrongDual.{u_1, u_5} 𝕜 (M i)
hφ : ∀ (i : ι), Eq.{u_1 + 1} (α := 𝕜) ((φ i : (a : M i) → 𝕜) (m i) : 𝕜) (1 : 𝕜)
val : Fintype ι
g : ℕ → ContinuousMultilinearMap 𝕜 M F :=
  fun (n : ℕ) ↦
    ((compContinuousLinearMapL.{u_1, u_4, u_5, u_3, u_1} (𝕜 := 𝕜) (E := M) (F := F) (E₁ := fun (i : ι) ↦ 𝕜) φ :
          ContinuousMultilinearMap 𝕜 (fun (i : ι) ↦ 𝕜) F →L[𝕜] ContinuousMultilinearMap 𝕜 M F) :
        (a : ContinuousMultilinearMap 𝕜 (fun (i : ι) ↦ 𝕜) F) → ContinuousMultilinearMap 𝕜 M F)
      ((((smulRightL 𝕜 (fun (x : ι) ↦ 𝕜) F :
                (a : ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) 𝕜) →
                  F →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) F)
              (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι 𝕜) :
            F →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) F) :
          (a : F) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) F)
        (f n))
this : CauchySeq g
a : ContinuousMultilinearMap 𝕜 M F
ha : Tendsto g atTop (𝓝 a)
⊢ Tendsto.{0, u_3} (β := F) (fun (n : ℕ) ↦ ((g n : (a : (i : ι) → M i) → F) m : F)) atTop
    (𝓝 ((a : (a : (i : ι) → M i) → F) m) : Filter F)

Tactic:
have : Tendsto (fun n ↦ g n m) atTop (𝓝 (a m)) := ((continuous_eval_const _).tendsto _).comp ha
-- Module: Mathlib.Analysis.Normed.Operator.CompleteCodomain
Goal:
𝕜 : Type u_1
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_4
inst_3 : Finite ι
M : ι → Type u_5
inst_4 : (i : ι) → NormedAddCommGroup (M i)
inst_5 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (M i)
inst_6 : ∀ (i : ι), SeparatingDual.{u_1, u_5} 𝕜 (M i)
inst_7 : CompleteSpace (ContinuousMultilinearMap 𝕜 M F)
m : (i : ι) → M i
hm : ∀ (i : ι), m i ≠ 0
f : ℕ → F
hf : CauchySeq f
φ : (i : ι) → StrongDual.{u_1, u_5} 𝕜 (M i)
hφ : ∀ (i : ι), Eq.{u_1 + 1} (α := 𝕜) ((φ i : (a : M i) → 𝕜) (m i) : 𝕜) (1 : 𝕜)
val : Fintype ι
g : ℕ → ContinuousMultilinearMap 𝕜 M F :=
  fun (n : ℕ) ↦
    ((compContinuousLinearMapL.{u_1, u_4, u_5, u_3, u_1} (𝕜 := 𝕜) (E := M) (F := F) (E₁ := fun (i : ι) ↦ 𝕜) φ :
          ContinuousMultilinearMap 𝕜 (fun (i : ι) ↦ 𝕜) F →L[𝕜] ContinuousMultilinearMap 𝕜 M F) :
        (a : ContinuousMultilinearMap 𝕜 (fun (i : ι) ↦ 𝕜) F) → ContinuousMultilinearMap 𝕜 M F)
      ((((smulRightL 𝕜 (fun (x : ι) ↦ 𝕜) F :
                (a : ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) 𝕜) →
                  F →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) F)
              (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι 𝕜) :
            F →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) F) :
          (a : F) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) F)
        (f n))
this_1 : CauchySeq g
a : ContinuousMultilinearMap 𝕜 M F
ha : Tendsto g atTop (𝓝 a)
this :
  Tendsto.{0, u_3} (β := F) (fun (n : ℕ) ↦ ((g n : (a : (i : ι) → M i) → F) m : F)) atTop
    (𝓝 ((a : (a : (i : ι) → M i) → F) m) : Filter F)
⊢ Tendsto f atTop (𝓝 ((a : (a : (i : ι) → M i) → F) m))

Tactic:
simpa [g, hφ]
-- Module: Mathlib.Analysis.Normed.Operator.CompleteCodomain
Goal:
𝕜 : Type u_1
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_4
inst_3 : Finite ι
M : ι → Type u_5
inst_4 : (i : ι) → NormedAddCommGroup (M i)
inst_5 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (M i)
inst_6 : ∀ (i : ι), SeparatingDual.{u_1, u_5} 𝕜 (M i)
m : (i : ι) → M i
hm : ∀ (i : ι), m i ≠ 0
⊢ CompleteSpace (ContinuousMultilinearMap 𝕜 M F) ↔ CompleteSpace F

Tactic:
⟨fun _h ↦ completeSpace_of_completeSpace_continuousMultilinearMap 𝕜 F hm, fun _h ↦ inferInstance⟩

Premises used: SeparatingDual.completeSpace_of_completeSpace_continuousMultilinearMap, inferInstance, Iff.intro
-- 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 : 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
refine_1 :
  Membership.mem (γ := Set ((a : E') → F))
    (closure[Pi.topologicalSpace] (range (ι := E' →ₛₗ[σ₁₂] F) (DFunLike.coe (β := fun (x : E') ↦ F)))) f
refine_2 :
  ∃ (C : ℝ), ∀ (x : E'), Norm.norm.{u_4} (E := F) ((linearMapOfMemClosureRangeCoe f ⋯ : (a : E') → F) x : F) ≤ C * ‖x‖
⊢ E' →SL[σ₁₂] F

Tactic:
refine (linearMapOfMemClosureRangeCoe f ?_).mkContinuousOfExistsBound ?_

Premises used: LinearMap.mkContinuousOfExistsBound, linearMapOfMemClosureRangeCoe
-- 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 : 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
⊢ Membership.mem (γ := Set ((a : E') → F))
    (closure[Pi.topologicalSpace] (range (ι := E' →ₛₗ[σ₁₂] F) (DFunLike.coe (β := fun (x : E') ↦ F)))) f

Tactic:
closure_mono (image_subset_iff.2 fun g _ => ?_) hf

Premises used: Iff.mpr, Set.Mem, closure_mono, Set.image_subset_iff
-- 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 : 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
refine_1 :
  ∀ g ∈ s,
    Membership.mem (γ := Set (E' →SL[σ₁₂] F))
      (preimage (β := E' → F) (DFunLike.coe (β := fun (x : E') ↦ F))
        (range (ι := E' →ₛₗ[σ₁₂] F) (DFunLike.coe (β := fun (x : E') ↦ F))))
      g
⊢ Membership.mem (γ := Set ((a : E') → F))
    (closure[Pi.topologicalSpace] (range (ι := E' →ₛₗ[σ₁₂] F) (DFunLike.coe (β := fun (x : E') ↦ F)))) f

Tactic:
refine closure_mono (image_subset_iff.2 fun g _ => ?_) hf

Premises used: Iff.mpr, closure_mono, Set.image_subset_iff
-- 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
g : E' →SL[σ₁₂] F
h : g ∈ s
⊢ Membership.mem (γ := Set (E' →SL[σ₁₂] F))
    (preimage (β := E' → F) (DFunLike.coe (β := fun (x : E') ↦ F))
      (range (ι := E' →ₛₗ[σ₁₂] F) (DFunLike.coe (β := fun (x : E') ↦ F))))
    g

Tactic:
⟨g, rfl⟩

Premises used: Set.Mem, setOf, ContinuousLinearMap.toLinearMap, Set.preimage, Exists.intro, Set.range, rfl
-- 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
g : E' →SL[σ₁₂] F
h : g ∈ s
⊢ Membership.mem (γ := Set (E' →SL[σ₁₂] F))
    (preimage (β := E' → F) (DFunLike.coe (β := fun (x : E') ↦ F))
      (range (ι := E' →ₛₗ[σ₁₂] F) (DFunLike.coe (β := fun (x : E') ↦ F))))
    g

Tactic:
exact ⟨g, rfl⟩
-- 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 : 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
refine_2 :
  ∀ (C : ℝ) (hC : ∀ x ∈ s, ‖x‖ ≤ C),
    ∃ (C : ℝ), ∀ (x : E'), Norm.norm.{u_4} (E := F) ((linearMapOfMemClosureRangeCoe f ⋯ : (a : E') → F) x : F) ≤ C * ‖x‖
⊢ ∃ (C : ℝ), ∀ (x : E'), Norm.norm.{u_4} (E := F) ((linearMapOfMemClosureRangeCoe f ⋯ : (a : E') → F) x : F) ≤ C * ‖x‖

Tactic:
rcases isBounded_iff_forall_norm_le.1 hs with ⟨C, hC⟩

Premises used: isBounded_iff_forall_norm_le, Iff.mp
-- 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 : 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
⊢ ∀ (x : E'), IsClosed[Pi.topologicalSpace] {g : E' → F | ‖g x‖ ≤ C * ‖x‖}

Tactic:
have : ∀ x, IsClosed { g : E' → F | ‖g x‖ ≤ C * ‖x‖ } := fun x =>
      isClosed_Iic.preimage (@continuous_apply E' (fun _ => F) _ x).norm
-- 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 : 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‖}
⊢ ∃ (C : ℝ), ∀ (x : E'), Norm.norm.{u_4} (E := F) ((linearMapOfMemClosureRangeCoe f ⋯ : (a : E') → F) x : F) ≤ C * ‖x‖

Tactic:
⟨C, fun x => (this x).closure_subset_iff.2 (image_subset_iff.2 fun g hg => ?_) hf⟩

Premises used: Iff.mpr, IsClosed.closure_subset_iff, Exists.intro, Set.image_subset_iff
-- 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 : 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‖}
refine_2 :
  ∀ (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
⊢ ∃ (C : ℝ), ∀ (x : E'), Norm.norm.{u_4} (E := F) ((linearMapOfMemClosureRangeCoe f ⋯ : (a : E') → F) x : F) ≤ C * ‖x‖

Tactic:
refine ⟨C, fun x => (this x).closure_subset_iff.2 (image_subset_iff.2 fun g hg => ?_) hf⟩