awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative (goal)
Goal:
𝕜 : Type u_1
X : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
T : X →L[𝕜] X
μ : 𝕜
inst_3 : CompleteSpace X
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h₁ : ¬HasEigenvalue (↑T : X →ₗ[𝕜] X) μ
S : X →L[𝕜] X := T - HSMul.hSMul (β := X →L[𝕜] X) μ 1
K_1 : NNReal
hK_1 : AntilipschitzWith (α := X) (β := X) K_1 (⇑S : (a : X) → X)
h₂ : ¬Function.Surjective (α := X) (β := X) (⇑S : (a : X) → X)
c : 𝕜
hc : 1 < ‖c‖
f : ℕ → X
hf_norm_lower : ∀ (n : ℕ), 1 ≤ ‖f n‖
hf_norm_upper : ∀ (n : ℕ), ‖f n‖ ≤ ‖c‖ + 1
hf_far : ∀ (n : ℕ), ∀ y ∈ LinearMap.range ((↑S : X →ₗ[𝕜] X) ^ (n + 1)), 1 ≤ ‖f n - y‖
hf_mem : ∀ {n m : ℕ} (h : m ≤ n), f n ∈ ((↑S : X →ₗ[𝕜] X) ^ m).range
hf_mem' :
  ∀ {n m : ℕ} (h : m ≤ n), Membership.mem (α := X) ((↑S : X →ₗ[𝕜] X) ^ (m + 1)).range ((S : (a : X) → X) (f n) : X)
hp :
  Pairwise fun (x₁ x₂ : ℕ) ↦
    ‖μ‖ ≤ ‖HSub.hSub (α := X) (β := X) ((T : (a : X) → X) (f x₁) : X) ((T : (a : X) → X) (f x₂) : X)‖
K : Set X
hK : IsCompact K
hK' : Set.image (α := X) (⇑(↑T : X →ₗ[𝕜] X) : (a : X) → X) (Metric.closedBall 0 (‖c‖ + 1)) ⊆ K
y : X
hyK : y ∈ K
ψ : ℕ → ℕ
hψ : StrictMono ψ
hψy :
  ∀ ε > 0,
    ∃ (N : ℕ),
      ∀ n ≥ N,
        dist.{u_2} (α := X) (((fun (n : ℕ) ↦ ((↑T : X →ₗ[𝕜] X) : (a : X) → X) (f n)) ∘ ψ) n)
            (((fun (n : ℕ) ↦ ((↑T : X →ₗ[𝕜] X) : (a : X) → X) (f n)) ∘ ψ) N) <
          ε
N : ℕ
hN :
  ∀ n ≥ N,
    dist.{u_2} (α := X) (((fun (n : ℕ) ↦ ((↑T : X →ₗ[𝕜] X) : (a : X) → X) (f n)) ∘ ψ) n)
        (((fun (n : ℕ) ↦ ((↑T : X →ₗ[𝕜] X) : (a : X) → X) (f n)) ∘ ψ) N) <
      ‖μ‖
this : ‖HSub.hSub (α := X) (β := X) ((T : (a : X) → X) (f (ψ (N + 1))) : X) ((T : (a : X) → X) (f (ψ N)) : X)‖ < ‖μ‖
⊢ False
have refine : ψ (N + 1) ≠ ψ N
Tactic: refine this.not_ge (hp ?_)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative (goal)
Goal:
𝕜 : Type u_1
X : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
T : X →L[𝕜] X
μ : 𝕜
inst_3 : CompleteSpace X
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
⊢ HasEigenvalue (↑T : X →ₗ[𝕜] X) μ ↔ μ ∈ spectrum 𝕜 T
have mp : HasEigenvalue (↑T : X →ₗ[𝕜] X) μ → μ ∈ spectrum 𝕜 T
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative (goal)
Goal:
𝕜 : Type u_1
X : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
T : X →L[𝕜] X
μ : 𝕜
inst_3 : CompleteSpace X
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
mp : HasEigenvalue (↑T : X →ₗ[𝕜] X) μ → μ ∈ spectrum 𝕜 T
⊢ HasEigenvalue (↑T : X →ₗ[𝕜] X) μ ↔ μ ∈ spectrum 𝕜 T
have mpr : μ ∈ spectrum 𝕜 T → HasEigenvalue (↑T : X →ₗ[𝕜] X) μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative (goal)
Goal:
𝕜 : Type u_1
X : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
T : X →L[𝕜] X
μ : 𝕜
inst_3 : CompleteSpace X
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
hμ' : HasEigenvalue (↑T : X →ₗ[𝕜] X) μ
⊢ μ ∈ spectrum 𝕜 T
have mp : μ ∈ spectrum 𝕜 (↑T : X →ₗ[𝕜] X)
Tactic: rw [ContinuousLinearMap.spectrum_eq]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.CompleteCodomain (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeparatingDual 𝕜 E
inst_6 : Nontrivial E
inst_7 : CompleteSpace (E →L[𝕜] F)
⊢ CompleteSpace F
have refine : ∀ (f : ℕ → F) (hf : CauchySeq f), ∃ (a : F), Tendsto f atTop (𝓝 a)
Tactic: refine Metric.complete_of_cauchySeq_tendsto fun f hf => ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.CompleteCodomain (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeparatingDual 𝕜 E
inst_6 : Nontrivial E
inst_7 : CompleteSpace (E →L[𝕜] F)
f : ℕ → F
hf : CauchySeq f
⊢ ∃ (a : F), Tendsto f atTop (𝓝 a)
have obtain : ∀ (v : E) (hv : v ≠ 0), ∃ (a : F), Tendsto f atTop (𝓝 a)
Tactic: obtain ⟨v, hv⟩ : ∃ (v : E), v ≠ 0 := exists_ne 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.CompleteCodomain (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeparatingDual 𝕜 E
inst_6 : Nontrivial E
inst_7 : CompleteSpace (E →L[𝕜] F)
f : ℕ → F
hf : CauchySeq f
v : E
hv : v ≠ 0
⊢ ∃ (a : F), Tendsto f atTop (𝓝 a)
have obtain : ∀ (φ : StrongDual 𝕜 E) (hφ : Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : E) → 𝕜) v : 𝕜) (1 : 𝕜)), ∃ (a : F), Tendsto f atTop (𝓝 a)
Tactic: obtain ⟨φ, hφ⟩ : ∃ φ : StrongDual 𝕜 E, φ v = 1 := exists_eq_one hv
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.CompleteCodomain (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeparatingDual 𝕜 E
inst_6 : Nontrivial E
inst_7 : CompleteSpace (E →L[𝕜] F)
f : ℕ → F
hf : CauchySeq f
v : E
hv : v ≠ 0
φ : StrongDual 𝕜 E
hφ : Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : E) → 𝕜) v : 𝕜) (1 : 𝕜)
g : ℕ → E →L[𝕜] F :=
  fun (n : ℕ) ↦
    (((ContinuousLinearMap.smulRightL 𝕜 E F : (a : StrongDual 𝕜 E) → F →L[𝕜] E →L[𝕜] F) φ : F →L[𝕜] E →L[𝕜] F) :
        (a : F) → E →L[𝕜] F)
      (f n)
⊢ ∃ (a : F), Tendsto f atTop (𝓝 a)
have this : CauchySeq g
Tactic: have : CauchySeq g := (ContinuousLinearMap.smulRightL 𝕜 E F φ).lipschitz.cauchySeq_comp hf
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.CompleteCodomain (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeparatingDual 𝕜 E
inst_6 : Nontrivial E
inst_7 : CompleteSpace (E →L[𝕜] F)
f : ℕ → F
hf : CauchySeq f
v : E
hv : v ≠ 0
φ : StrongDual 𝕜 E
hφ : Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : E) → 𝕜) v : 𝕜) (1 : 𝕜)
g : ℕ → E →L[𝕜] F :=
  fun (n : ℕ) ↦
    (((ContinuousLinearMap.smulRightL 𝕜 E F : (a : StrongDual 𝕜 E) → F →L[𝕜] E →L[𝕜] F) φ : F →L[𝕜] E →L[𝕜] F) :
        (a : F) → E →L[𝕜] F)
      (f n)
this : CauchySeq g
⊢ ∃ (a : F), Tendsto f atTop (𝓝 a)
have obtain : ∀ (a : E →L[𝕜] F) (ha : Tendsto g atTop (𝓝 a)), ∃ (a : F), Tendsto f atTop (𝓝 a)
Tactic: obtain ⟨a, ha⟩ : ∃ a, Tendsto g atTop (𝓝 a) := cauchy_iff_exists_le_nhds.mp this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.CompleteCodomain (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeparatingDual 𝕜 E
inst_6 : Nontrivial E
inst_7 : CompleteSpace (E →L[𝕜] F)
f : ℕ → F
hf : CauchySeq f
v : E
hv : v ≠ 0
φ : StrongDual 𝕜 E
hφ : Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : E) → 𝕜) v : 𝕜) (1 : 𝕜)
g : ℕ → E →L[𝕜] F :=
  fun (n : ℕ) ↦
    (((ContinuousLinearMap.smulRightL 𝕜 E F : (a : StrongDual 𝕜 E) → F →L[𝕜] E →L[𝕜] F) φ : F →L[𝕜] E →L[𝕜] F) :
        (a : F) → E →L[𝕜] F)
      (f n)
this : CauchySeq g
a : E →L[𝕜] F
ha : Tendsto g atTop (𝓝 a)
⊢ ∃ (a : F), Tendsto f atTop (𝓝 a)
have refine : Tendsto f atTop (𝓝 ((a : (a : E) → F) v))
Tactic: refine ⟨a v, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.CompleteCodomain (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeparatingDual 𝕜 E
inst_6 : Nontrivial E
inst_7 : CompleteSpace (E →L[𝕜] F)
f : ℕ → F
hf : CauchySeq f
v : E
hv : v ≠ 0
φ : StrongDual 𝕜 E
hφ : Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : E) → 𝕜) v : 𝕜) (1 : 𝕜)
g : ℕ → E →L[𝕜] F :=
  fun (n : ℕ) ↦
    (((ContinuousLinearMap.smulRightL 𝕜 E F : (a : StrongDual 𝕜 E) → F →L[𝕜] E →L[𝕜] F) φ : F →L[𝕜] E →L[𝕜] F) :
        (a : F) → E →L[𝕜] F)
      (f n)
this : CauchySeq g
a : E →L[𝕜] F
ha : Tendsto g atTop (𝓝 a)
⊢ Tendsto.{0, u_3} (β := F) (fun (n : ℕ) ↦ ((g n : (a : E) → F) v : F)) atTop (𝓝 ((a : (a : E) → F) v) : Filter F)
have this₁ : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (i : E →L[𝕜] F) ↦ (i : (a : E) → F) v
Tactic: have : Continuous (fun (i : E →L[𝕜] F) ↦ i v) := by fun_prop
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.CompleteCodomain (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeparatingDual 𝕜 E
inst_6 : Nontrivial E
inst_7 : CompleteSpace (E →L[𝕜] F)
f : ℕ → F
hf : CauchySeq f
v : E
hv : v ≠ 0
φ : StrongDual 𝕜 E
hφ : Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : E) → 𝕜) v : 𝕜) (1 : 𝕜)
g : ℕ → E →L[𝕜] F :=
  fun (n : ℕ) ↦
    (((ContinuousLinearMap.smulRightL 𝕜 E F : (a : StrongDual 𝕜 E) → F →L[𝕜] E →L[𝕜] F) φ : F →L[𝕜] E →L[𝕜] F) :
        (a : F) → E →L[𝕜] F)
      (f n)
this : CauchySeq g
a : E →L[𝕜] F
ha : Tendsto g atTop (𝓝 a)
⊢ Tendsto f atTop (𝓝 ((a : (a : E) → F) v))
have this₁ : Tendsto.{0, u_3} (β := F) (fun (n : ℕ) ↦ ((g n : (a : E) → F) v : F)) atTop (𝓝 ((a : (a : E) → F) v) : Filter F)
Tactic: have : Tendsto (fun n ↦ g n v) atTop (𝓝 (a v)) := by
    have : Continuous (fun (i : E →L[𝕜] F) ↦ i v) := by fun_prop
    exact (this.tendsto _).comp ha
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.CompleteCodomain (goal)
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
⊢ CompleteSpace F
have refine : ∀ (f : ℕ → F) (hf : CauchySeq f), ∃ (a : F), Tendsto f atTop (𝓝 a)
Tactic: refine Metric.complete_of_cauchySeq_tendsto fun f hf => ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.CompleteCodomain (hypothesis)
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
⊢ ∃ (a : F), Tendsto f atTop (𝓝 a)
have this : ∀ (i : ι), ∃ (φ : StrongDual.{u_1, u_5} 𝕜 (M i)), Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : M i) → 𝕜) (m i) : 𝕜) (1 : 𝕜)
Tactic: have : ∀ i, ∃ φ : StrongDual 𝕜 (M i), φ (m i) = 1 := fun i ↦ exists_eq_one (hm i)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.CompleteCodomain (goal)
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
this : ∀ (i : ι), ∃ (φ : StrongDual.{u_1, u_5} 𝕜 (M i)), Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : M i) → 𝕜) (m i) : 𝕜) (1 : 𝕜)
⊢ ∃ (a : F), Tendsto f atTop (𝓝 a)
have choose : ∀ (φ : (i : ι) → StrongDual.{u_1, u_5} 𝕜 (M i))
  (hφ : ∀ (i : ι), Eq.{u_1 + 1} (α := 𝕜) ((φ i : (a : M i) → 𝕜) (m i) : 𝕜) (1 : 𝕜)), ∃ (a : F), Tendsto f atTop (𝓝 a)
Tactic: choose φ hφ using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.CompleteCodomain (goal)
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 : 𝕜)
⊢ ∃ (a : F), Tendsto f atTop (𝓝 a)
have intro : ∀ (val : Fintype ι), ∃ (a : F), Tendsto f atTop (𝓝 a)
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.CompleteCodomain (goal)
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
have refine : 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: refine (ContinuousLinearMap.lipschitz _).cauchySeq_comp ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.CompleteCodomain (hypothesis)
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))
⊢ ∃ (a : F), Tendsto f atTop (𝓝 a)
have this : CauchySeq g
Tactic: have : CauchySeq g := by
    refine (ContinuousLinearMap.lipschitz _).cauchySeq_comp ?_
    exact (ContinuousLinearMap.lipschitz _).cauchySeq_comp hf
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.CompleteCodomain (goal)
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 : F), Tendsto f atTop (𝓝 a)
have intro : ∀ (a : ContinuousMultilinearMap 𝕜 M F) (ha : Tendsto g atTop (𝓝 a)), ∃ (a : F), Tendsto f atTop (𝓝 a)
Tactic: obtain ⟨a, ha⟩ : ∃ a, Tendsto g atTop (𝓝 a) := cauchy_iff_exists_le_nhds.mp this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.CompleteCodomain (goal)
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)
have intro : Tendsto f atTop (𝓝 ((a : (a : (i : ι) → M i) → F) m))
Tactic: refine ⟨a m, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.CompleteCodomain (hypothesis)
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 f atTop (𝓝 ((a : (a : (i : ι) → M i) → F) m))
have 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)
Tactic: have : Tendsto (fun n ↦ g n m) atTop (𝓝 (a m)) := ((continuous_eval_const _).tendsto _).comp ha
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Completeness (goal)
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
⊢ E' →SL[σ₁₂] F
have refine_1 : Membership.mem (γ := Set ((a : E') → F))
  (closure[Pi.topologicalSpace] (range (ι := E' →ₛₗ[σ₁₂] F) (DFunLike.coe (β := fun (x : E') ↦ F)))) f
Tactic: refine (linearMapOfMemClosureRangeCoe f ?_).mkContinuousOfExistsBound ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Completeness (goal)
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
⊢ E' →SL[σ₁₂] F
have refine_2 : ∃ (C : ℝ), ∀ (x : E'), Norm.norm.{u_4} (E := F) ((linearMapOfMemClosureRangeCoe f sorry : (a : E') → F) x : F) ≤ C * ‖x‖
Tactic: refine (linearMapOfMemClosureRangeCoe f ?_).mkContinuousOfExistsBound ?_