awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative
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
⊢ μ ∈ spectrum 𝕜 T → HasEigenvalue (↑T : X →ₗ[𝕜] X) μ

Tactic:
exact (hasEigenvalue_or_mem_resolventSet hT hμ).resolve_right

Premises used: IsCompactOperator.hasEigenvalue_or_mem_resolventSet, Or.resolve_right
-- Module: Mathlib.Analysis.Normed.Operator.CompleteCodomain
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

Tactic:
Metric.complete_of_cauchySeq_tendsto fun f hf => ?_

Premises used: Metric.complete_of_cauchySeq_tendsto
-- Module: Mathlib.Analysis.Normed.Operator.CompleteCodomain
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)
refine : ∀ (f : ℕ → F) (hf : CauchySeq f), ∃ (a : F), Tendsto f atTop (𝓝 a)
⊢ CompleteSpace F

Tactic:
refine Metric.complete_of_cauchySeq_tendsto fun f hf => ?_

Premises used: Metric.complete_of_cauchySeq_tendsto
-- Module: Mathlib.Analysis.Normed.Operator.CompleteCodomain
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), v ≠ 0

Tactic:
exists_ne 0

Premises used: exists_ne, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Operator.CompleteCodomain
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
obtain : ∀ (v : E) (hv : v ≠ 0), ∃ (a : F), Tendsto f atTop (𝓝 a)
⊢ ∃ (a : F), Tendsto f atTop (𝓝 a)

Tactic:
obtain ⟨v, hv⟩ : ∃ (v : E), v ≠ 0 := exists_ne 0

Premises used: exists_ne, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Operator.CompleteCodomain
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), Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : E) → 𝕜) v : 𝕜) (1 : 𝕜)

Tactic:
exists_eq_one hv

Premises used: SeparatingDual.exists_eq_one
-- Module: Mathlib.Analysis.Normed.Operator.CompleteCodomain
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
obtain :
  ∀ (φ : StrongDual 𝕜 E) (hφ : Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : E) → 𝕜) v : 𝕜) (1 : 𝕜)),
    ∃ (a : F), Tendsto f atTop (𝓝 a)
⊢ ∃ (a : F), Tendsto f atTop (𝓝 a)

Tactic:
obtain ⟨φ, hφ⟩ : ∃ φ : StrongDual 𝕜 E, φ v = 1 := exists_eq_one hv

Premises used: SeparatingDual.exists_eq_one, StrongDual
-- Module: Mathlib.Analysis.Normed.Operator.CompleteCodomain
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)
⊢ CauchySeq g

Tactic:
have : CauchySeq g := (ContinuousLinearMap.smulRightL 𝕜 E F φ).lipschitz.cauchySeq_comp hf
-- Module: Mathlib.Analysis.Normed.Operator.CompleteCodomain
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), 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
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
obtain : ∀ (a : E →L[𝕜] 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
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)

Tactic:
⟨a v, ?_⟩

Premises used: Exists.intro, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Operator.CompleteCodomain
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)
refine : Tendsto f atTop (𝓝 ((a : (a : E) → F) v))
⊢ ∃ (a : F), Tendsto f atTop (𝓝 a)

Tactic:
refine ⟨a v, ?_⟩
-- Module: Mathlib.Analysis.Normed.Operator.CompleteCodomain
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)
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (i : E →L[𝕜] F) ↦ (i : (a : E) → F) v

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Normed.Operator.CompleteCodomain
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)
⊢ 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
-- Module: Mathlib.Analysis.Normed.Operator.CompleteCodomain
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_1 : CauchySeq g
a : E →L[𝕜] F
ha : Tendsto g atTop (𝓝 a)
this : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (i : E →L[𝕜] F) ↦ (i : (a : E) → F) v
⊢ Tendsto.{0, u_3} (β := F) (fun (n : ℕ) ↦ ((g n : (a : E) → F) v : F)) atTop (𝓝 ((a : (a : E) → F) v) : Filter F)

Tactic:
(this.tendsto _).comp ha

Premises used: Continuous.tendsto, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Normed.Operator.CompleteCodomain
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_1 : CauchySeq g
a : E →L[𝕜] F
ha : Tendsto g atTop (𝓝 a)
this : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (i : E →L[𝕜] F) ↦ (i : (a : E) → F) v
⊢ Tendsto.{0, u_3} (β := F) (fun (n : ℕ) ↦ ((g n : (a : E) → F) v : F)) atTop (𝓝 ((a : (a : E) → F) v) : Filter F)

Tactic:
exact (this.tendsto _).comp ha

Premises used: Continuous.tendsto, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Normed.Operator.CompleteCodomain
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)

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
-- Module: Mathlib.Analysis.Normed.Operator.CompleteCodomain
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_1 : CauchySeq g
a : E →L[𝕜] F
ha : Tendsto g atTop (𝓝 a)
this : Tendsto.{0, u_3} (β := F) (fun (n : ℕ) ↦ ((g n : (a : E) → F) v : F)) atTop (𝓝 ((a : (a : E) → F) v) : Filter F)
⊢ Tendsto f atTop (𝓝 ((a : (a : E) → F) v))

Tactic:
simpa [g, ContinuousLinearMap.smulRightL, hφ]

Premises used: ContinuousLinearMap.smulRightL
-- Module: Mathlib.Analysis.Normed.Operator.CompleteCodomain
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
⊢ CompleteSpace (E →L[𝕜] F) ↔ CompleteSpace F

Tactic:
⟨fun _h ↦ completeSpace_of_completeSpace_continuousLinearMap 𝕜 E F, fun _h ↦ inferInstance⟩

Premises used: inferInstance, SeparatingDual.completeSpace_of_completeSpace_continuousLinearMap, Iff.intro
-- 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
⊢ CompleteSpace F

Tactic:
Metric.complete_of_cauchySeq_tendsto fun f hf => ?_

Premises used: Metric.complete_of_cauchySeq_tendsto
-- 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
refine : ∀ (f : ℕ → F) (hf : CauchySeq f), ∃ (a : F), Tendsto f atTop (𝓝 a)
⊢ CompleteSpace F

Tactic:
refine Metric.complete_of_cauchySeq_tendsto fun f hf => ?_

Premises used: Metric.complete_of_cauchySeq_tendsto
-- 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)), 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)
-- 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
this : ∀ (i : ι), ∃ (φ : StrongDual.{u_1, u_5} 𝕜 (M i)), Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : M i) → 𝕜) (m i) : 𝕜) (1 : 𝕜)
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)
⊢ ∃ (a : F), Tendsto f atTop (𝓝 a)

Tactic:
choose φ hφ using this
-- 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 : 𝕜)
intro : ∀ (val : Fintype ι), ∃ (a : F), Tendsto f atTop (𝓝 a)
⊢ ∃ (a : F), Tendsto f atTop (𝓝 a)

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- 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:
(ContinuousLinearMap.lipschitz _).cauchySeq_comp ?_

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))
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)
⊢ CauchySeq g

Tactic:
refine (ContinuousLinearMap.lipschitz _).cauchySeq_comp ?_

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 (α := 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:
(ContinuousLinearMap.lipschitz _).cauchySeq_comp hf

Premises used: ContinuousLinearMap.lipschitz, LipschitzWith.cauchySeq_comp