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
μ : 𝕜
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h :
  ∀ (c : ℝ) (_ : c > 0), ∃ (x : X), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < c * ‖x‖
c : ℝ
hc₀ : c > 0
hc :
  ∀ ε > 0, ∃ (x : X), ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < ε
φ : ℕ → ℝ
hφ_anti : StrictAnti φ
hφ_pos : ∀ (n : ℕ), 0 < φ n
hφ : Tendsto φ atTop (𝓝 0)
x : (n : ℕ) → X
hx_norm_upper : ∀ (n : ℕ), ‖x n‖ ≤ 1
hx_norm_lower : ∀ (n : ℕ), c ≤ ‖x n‖
hx_bound : ∀ (n : ℕ), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n) : X) < φ n
hx_lim :
  Tendsto.{0, u_2} (β := X) (fun (n : ℕ) ↦ (T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n)) atTop (𝓝 0)
y_ : (n : ℕ) → X := fun (n : ℕ) ↦ (T : (a : X) → X) (x n)
hy_lower : ∃ d > 0, ∀ᶠ (n : ℕ) in atTop, d ≤ ‖y_ n‖
obtain :
  ∀ (K : Set X) (hK : IsCompact K)
    (hK' : Set.image (α := X) (⇑(↑T : X →ₗ[𝕜] X) : (a : X) → X) (Metric.closedBall 0 1) ⊆ K),
    HasEigenvalue (↑T : X →ₗ[𝕜] X) μ
⊢ HasEigenvalue (↑T : X →ₗ[𝕜] X) μ

Tactic:
obtain ⟨K, hK, hK'⟩ := hT.image_closedBall_subset_compact 1

Premises used: IsCompactOperator.image_closedBall_subset_compact, OfNat.ofNat
-- 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
μ : 𝕜
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h :
  ∀ (c : ℝ) (_ : c > 0), ∃ (x : X), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < c * ‖x‖
c : ℝ
hc₀ : c > 0
hc :
  ∀ ε > 0, ∃ (x : X), ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < ε
φ : ℕ → ℝ
hφ_anti : StrictAnti φ
hφ_pos : ∀ (n : ℕ), 0 < φ n
hφ : Tendsto φ atTop (𝓝 0)
x : (n : ℕ) → X
hx_norm_upper : ∀ (n : ℕ), ‖x n‖ ≤ 1
hx_norm_lower : ∀ (n : ℕ), c ≤ ‖x n‖
hx_bound : ∀ (n : ℕ), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n) : X) < φ n
hx_lim :
  Tendsto.{0, u_2} (β := X) (fun (n : ℕ) ↦ (T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n)) atTop (𝓝 0)
y_ : (n : ℕ) → X := fun (n : ℕ) ↦ (T : (a : X) → X) (x n)
hy_lower : ∃ d > 0, ∀ᶠ (n : ℕ) in atTop, d ≤ ‖y_ n‖
K : Set X
hK : IsCompact K
hK' : Set.image (α := X) (⇑(↑T : X →ₗ[𝕜] X) : (a : X) → X) (Metric.closedBall 0 1) ⊆ K
n : ℕ
⊢ Membership.mem (γ := Set X) (Metric.closedBall 0 1) (x n)

Tactic:
simp [*]
-- 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
μ : 𝕜
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h :
  ∀ (c : ℝ) (_ : c > 0), ∃ (x : X), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < c * ‖x‖
c : ℝ
hc₀ : c > 0
hc :
  ∀ ε > 0, ∃ (x : X), ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < ε
φ : ℕ → ℝ
hφ_anti : StrictAnti φ
hφ_pos : ∀ (n : ℕ), 0 < φ n
hφ : Tendsto φ atTop (𝓝 0)
x : (n : ℕ) → X
hx_norm_upper : ∀ (n : ℕ), ‖x n‖ ≤ 1
hx_norm_lower : ∀ (n : ℕ), c ≤ ‖x n‖
hx_bound : ∀ (n : ℕ), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n) : X) < φ n
hx_lim :
  Tendsto.{0, u_2} (β := X) (fun (n : ℕ) ↦ (T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n)) atTop (𝓝 0)
y_ : (n : ℕ) → X := fun (n : ℕ) ↦ (T : (a : X) → X) (x n)
hy_lower : ∃ d > 0, ∀ᶠ (n : ℕ) in atTop, d ≤ ‖y_ n‖
K : Set X
hK : IsCompact K
hK' : Set.image (α := X) (⇑(↑T : X →ₗ[𝕜] X) : (a : X) → X) (Metric.closedBall 0 1) ⊆ K
obtain :
  ∀ (y : X) (hyK : y ∈ K) (ψ : ℕ → ℕ) (hψ : StrictMono ψ) (hψy : Tendsto (y_ ∘ ψ) atTop (𝓝 y)),
    HasEigenvalue (↑T : X →ₗ[𝕜] X) μ
⊢ HasEigenvalue (↑T : X →ₗ[𝕜] X) μ

Tactic:
obtain ⟨y, hyK, ψ, hψ, hψy⟩ := hK.tendsto_subseq (x := y_) (fun n ↦ hK' ⟨x n, by simp [*], rfl⟩)

Premises used: And.intro, Exists.intro, rfl, IsCompact.tendsto_subseq
-- 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
μ : 𝕜
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h :
  ∀ (c : ℝ) (_ : c > 0), ∃ (x : X), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < c * ‖x‖
c : ℝ
hc₀ : c > 0
hc :
  ∀ ε > 0, ∃ (x : X), ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < ε
φ : ℕ → ℝ
hφ_anti : StrictAnti φ
hφ_pos : ∀ (n : ℕ), 0 < φ n
hφ : Tendsto φ atTop (𝓝 0)
x : (n : ℕ) → X
hx_norm_upper : ∀ (n : ℕ), ‖x n‖ ≤ 1
hx_norm_lower : ∀ (n : ℕ), c ≤ ‖x n‖
hx_bound : ∀ (n : ℕ), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n) : X) < φ n
hx_lim :
  Tendsto.{0, u_2} (β := X) (fun (n : ℕ) ↦ (T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n)) atTop (𝓝 0)
y_ : (n : ℕ) → X := fun (n : ℕ) ↦ (T : (a : X) → X) (x n)
hy_lower : ∃ d > 0, ∀ᶠ (n : ℕ) in atTop, d ≤ ‖y_ n‖
K : Set X
hK : IsCompact K
hK' : Set.image (α := X) (⇑(↑T : X →ₗ[𝕜] X) : (a : X) → X) (Metric.closedBall 0 1) ⊆ K
y : X
hyK : y ∈ K
ψ : ℕ → ℕ
hψ : StrictMono ψ
hψy : Tendsto (y_ ∘ ψ) atTop (𝓝 y)
⊢ Tendsto.{0, u_2} (β := X) (fun (n : ℕ) ↦ (T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (y_ n)) atTop (𝓝 0)

Tactic:
simpa [Function.comp_def] using T.continuous.continuousAt.tendsto.comp hx_lim

Premises used: Continuous.continuousAt, ContinuousLinearMap.continuous, Function.comp_def, ContinuousAt.tendsto, Filter.Tendsto.comp
-- 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
μ : 𝕜
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h :
  ∀ (c : ℝ) (_ : c > 0), ∃ (x : X), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < c * ‖x‖
c : ℝ
hc₀ : c > 0
hc :
  ∀ ε > 0, ∃ (x : X), ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < ε
φ : ℕ → ℝ
hφ_anti : StrictAnti φ
hφ_pos : ∀ (n : ℕ), 0 < φ n
hφ : Tendsto φ atTop (𝓝 0)
x : (n : ℕ) → X
hx_norm_upper : ∀ (n : ℕ), ‖x n‖ ≤ 1
hx_norm_lower : ∀ (n : ℕ), c ≤ ‖x n‖
hx_bound : ∀ (n : ℕ), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n) : X) < φ n
hx_lim :
  Tendsto.{0, u_2} (β := X) (fun (n : ℕ) ↦ (T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n)) atTop (𝓝 0)
y_ : (n : ℕ) → X := fun (n : ℕ) ↦ (T : (a : X) → X) (x n)
hy_lower : ∃ d > 0, ∀ᶠ (n : ℕ) in atTop, d ≤ ‖y_ n‖
K : Set X
hK : IsCompact K
hK' : Set.image (α := X) (⇑(↑T : X →ₗ[𝕜] X) : (a : X) → X) (Metric.closedBall 0 1) ⊆ K
y : X
hyK : y ∈ K
ψ : ℕ → ℕ
hψ : StrictMono ψ
hψy : Tendsto (y_ ∘ ψ) atTop (𝓝 y)
⊢ Tendsto.{0, u_2} (β := X) (fun (n : ℕ) ↦ (T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (y_ n)) atTop (𝓝 0)

Tactic:
have hy_lim : Tendsto (fun n ↦ (T - μ • 1) (y_ n)) atTop (𝓝 0) := by
    simpa [Function.comp_def] using T.continuous.continuousAt.tendsto.comp hx_lim
-- 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
μ : 𝕜
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h :
  ∀ (c : ℝ) (_ : c > 0), ∃ (x : X), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < c * ‖x‖
c : ℝ
hc₀ : c > 0
hc :
  ∀ ε > 0, ∃ (x : X), ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < ε
φ : ℕ → ℝ
hφ_anti : StrictAnti φ
hφ_pos : ∀ (n : ℕ), 0 < φ n
hφ : Tendsto φ atTop (𝓝 0)
x : (n : ℕ) → X
hx_norm_upper : ∀ (n : ℕ), ‖x n‖ ≤ 1
hx_norm_lower : ∀ (n : ℕ), c ≤ ‖x n‖
hx_bound : ∀ (n : ℕ), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n) : X) < φ n
hx_lim :
  Tendsto.{0, u_2} (β := X) (fun (n : ℕ) ↦ (T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n)) atTop (𝓝 0)
y_ : (n : ℕ) → X := fun (n : ℕ) ↦ (T : (a : X) → X) (x n)
hy_lower : ∃ d > 0, ∀ᶠ (n : ℕ) in atTop, d ≤ ‖y_ n‖
K : Set X
hK : IsCompact K
hK' : Set.image (α := X) (⇑(↑T : X →ₗ[𝕜] X) : (a : X) → X) (Metric.closedBall 0 1) ⊆ K
y : X
hyK : y ∈ K
ψ : ℕ → ℕ
hψ : StrictMono ψ
hψy : Tendsto (y_ ∘ ψ) atTop (𝓝 y)
hy_lim :
  Tendsto.{0, u_2} (β := X) (fun (n : ℕ) ↦ (T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (y_ n)) atTop (𝓝 0)
apply :
  Tendsto (β := X) ((fun (n : ℕ) ↦ (T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (y_ n)) ∘ ψ : ℕ → X) atTop
    (𝓝 ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) y) : Filter X)
⊢ Eq (α := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) y : X) (0 : X)

Tactic:
apply tendsto_nhds_unique _ (hy_lim.comp hψ.tendsto_atTop)

Premises used: StrictMono.tendsto_atTop, Filter.Tendsto.comp, tendsto_nhds_unique
-- 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
μ : 𝕜
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h :
  ∀ (c : ℝ) (_ : c > 0), ∃ (x : X), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < c * ‖x‖
c : ℝ
hc₀ : c > 0
hc :
  ∀ ε > 0, ∃ (x : X), ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < ε
φ : ℕ → ℝ
hφ_anti : StrictAnti φ
hφ_pos : ∀ (n : ℕ), 0 < φ n
hφ : Tendsto φ atTop (𝓝 0)
x : (n : ℕ) → X
hx_norm_upper : ∀ (n : ℕ), ‖x n‖ ≤ 1
hx_norm_lower : ∀ (n : ℕ), c ≤ ‖x n‖
hx_bound : ∀ (n : ℕ), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n) : X) < φ n
hx_lim :
  Tendsto.{0, u_2} (β := X) (fun (n : ℕ) ↦ (T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n)) atTop (𝓝 0)
y_ : (n : ℕ) → X := fun (n : ℕ) ↦ (T : (a : X) → X) (x n)
hy_lower : ∃ d > 0, ∀ᶠ (n : ℕ) in atTop, d ≤ ‖y_ n‖
K : Set X
hK : IsCompact K
hK' : Set.image (α := X) (⇑(↑T : X →ₗ[𝕜] X) : (a : X) → X) (Metric.closedBall 0 1) ⊆ K
y : X
hyK : y ∈ K
ψ : ℕ → ℕ
hψ : StrictMono ψ
hψy : Tendsto (y_ ∘ ψ) atTop (𝓝 y)
hy_lim :
  Tendsto.{0, u_2} (β := X) (fun (n : ℕ) ↦ (T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (y_ n)) atTop (𝓝 0)
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑(T - HSMul.hSMul (β := X →L[𝕜] X) μ 1) : (a : X) → X)

Tactic:
fun_prop
-- 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
μ : 𝕜
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h :
  ∀ (c : ℝ) (_ : c > 0), ∃ (x : X), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < c * ‖x‖
c : ℝ
hc₀ : c > 0
hc :
  ∀ ε > 0, ∃ (x : X), ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < ε
φ : ℕ → ℝ
hφ_anti : StrictAnti φ
hφ_pos : ∀ (n : ℕ), 0 < φ n
hφ : Tendsto φ atTop (𝓝 0)
x : (n : ℕ) → X
hx_norm_upper : ∀ (n : ℕ), ‖x n‖ ≤ 1
hx_norm_lower : ∀ (n : ℕ), c ≤ ‖x n‖
hx_bound : ∀ (n : ℕ), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n) : X) < φ n
hx_lim :
  Tendsto.{0, u_2} (β := X) (fun (n : ℕ) ↦ (T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n)) atTop (𝓝 0)
y_ : (n : ℕ) → X := fun (n : ℕ) ↦ (T : (a : X) → X) (x n)
hy_lower : ∃ d > 0, ∀ᶠ (n : ℕ) in atTop, d ≤ ‖y_ n‖
K : Set X
hK : IsCompact K
hK' : Set.image (α := X) (⇑(↑T : X →ₗ[𝕜] X) : (a : X) → X) (Metric.closedBall 0 1) ⊆ K
y : X
hyK : y ∈ K
ψ : ℕ → ℕ
hψ : StrictMono ψ
hψy : Tendsto (y_ ∘ ψ) atTop (𝓝 y)
hy_lim :
  Tendsto.{0, u_2} (β := X) (fun (n : ℕ) ↦ (T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (y_ n)) atTop (𝓝 0)
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑(T - HSMul.hSMul (β := X →L[𝕜] X) μ 1) : (a : X) → X)

Tactic:
have : Continuous (T - μ • 1 : X →L[𝕜] X) := by fun_prop
-- 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
μ : 𝕜
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h :
  ∀ (c : ℝ) (_ : c > 0), ∃ (x : X), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < c * ‖x‖
c : ℝ
hc₀ : c > 0
hc :
  ∀ ε > 0, ∃ (x : X), ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < ε
φ : ℕ → ℝ
hφ_anti : StrictAnti φ
hφ_pos : ∀ (n : ℕ), 0 < φ n
hφ : Tendsto φ atTop (𝓝 0)
x : (n : ℕ) → X
hx_norm_upper : ∀ (n : ℕ), ‖x n‖ ≤ 1
hx_norm_lower : ∀ (n : ℕ), c ≤ ‖x n‖
hx_bound : ∀ (n : ℕ), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n) : X) < φ n
hx_lim :
  Tendsto.{0, u_2} (β := X) (fun (n : ℕ) ↦ (T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n)) atTop (𝓝 0)
y_ : (n : ℕ) → X := fun (n : ℕ) ↦ (T : (a : X) → X) (x n)
hy_lower : ∃ d > 0, ∀ᶠ (n : ℕ) in atTop, d ≤ ‖y_ n‖
K : Set X
hK : IsCompact K
hK' : Set.image (α := X) (⇑(↑T : X →ₗ[𝕜] X) : (a : X) → X) (Metric.closedBall 0 1) ⊆ K
y : X
hyK : y ∈ K
ψ : ℕ → ℕ
hψ : StrictMono ψ
hψy : Tendsto (y_ ∘ ψ) atTop (𝓝 y)
hy_lim :
  Tendsto.{0, u_2} (β := X) (fun (n : ℕ) ↦ (T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (y_ n)) atTop (𝓝 0)
this :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑(T - HSMul.hSMul (β := X →L[𝕜] X) μ 1) : (a : X) → X)
⊢ Tendsto (β := X) ((fun (n : ℕ) ↦ (T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (y_ n)) ∘ ψ : ℕ → X) atTop
    (𝓝 ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) y) : Filter X)

Tactic:
this.continuousAt.tendsto.comp hψy

Premises used: Continuous.continuousAt, ContinuousAt.tendsto, Filter.Tendsto.comp
-- 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
μ : 𝕜
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h :
  ∀ (c : ℝ) (_ : c > 0), ∃ (x : X), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < c * ‖x‖
c : ℝ
hc₀ : c > 0
hc :
  ∀ ε > 0, ∃ (x : X), ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < ε
φ : ℕ → ℝ
hφ_anti : StrictAnti φ
hφ_pos : ∀ (n : ℕ), 0 < φ n
hφ : Tendsto φ atTop (𝓝 0)
x : (n : ℕ) → X
hx_norm_upper : ∀ (n : ℕ), ‖x n‖ ≤ 1
hx_norm_lower : ∀ (n : ℕ), c ≤ ‖x n‖
hx_bound : ∀ (n : ℕ), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n) : X) < φ n
hx_lim :
  Tendsto.{0, u_2} (β := X) (fun (n : ℕ) ↦ (T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n)) atTop (𝓝 0)
y_ : (n : ℕ) → X := fun (n : ℕ) ↦ (T : (a : X) → X) (x n)
hy_lower : ∃ d > 0, ∀ᶠ (n : ℕ) in atTop, d ≤ ‖y_ n‖
K : Set X
hK : IsCompact K
hK' : Set.image (α := X) (⇑(↑T : X →ₗ[𝕜] X) : (a : X) → X) (Metric.closedBall 0 1) ⊆ K
y : X
hyK : y ∈ K
ψ : ℕ → ℕ
hψ : StrictMono ψ
hψy : Tendsto (y_ ∘ ψ) atTop (𝓝 y)
hy_lim :
  Tendsto.{0, u_2} (β := X) (fun (n : ℕ) ↦ (T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (y_ n)) atTop (𝓝 0)
this :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑(T - HSMul.hSMul (β := X →L[𝕜] X) μ 1) : (a : X) → X)
⊢ Tendsto (β := X) ((fun (n : ℕ) ↦ (T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (y_ n)) ∘ ψ : ℕ → X) atTop
    (𝓝 ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) y) : Filter X)

Tactic:
exact this.continuousAt.tendsto.comp hψy

Premises used: Continuous.continuousAt, ContinuousAt.tendsto, Filter.Tendsto.comp
-- 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
μ : 𝕜
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h :
  ∀ (c : ℝ) (_ : c > 0), ∃ (x : X), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < c * ‖x‖
c : ℝ
hc₀ : c > 0
hc :
  ∀ ε > 0, ∃ (x : X), ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < ε
φ : ℕ → ℝ
hφ_anti : StrictAnti φ
hφ_pos : ∀ (n : ℕ), 0 < φ n
hφ : Tendsto φ atTop (𝓝 0)
x : (n : ℕ) → X
hx_norm_upper : ∀ (n : ℕ), ‖x n‖ ≤ 1
hx_norm_lower : ∀ (n : ℕ), c ≤ ‖x n‖
hx_bound : ∀ (n : ℕ), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n) : X) < φ n
hx_lim :
  Tendsto.{0, u_2} (β := X) (fun (n : ℕ) ↦ (T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n)) atTop (𝓝 0)
y_ : (n : ℕ) → X := fun (n : ℕ) ↦ (T : (a : X) → X) (x n)
hy_lower : ∃ d > 0, ∀ᶠ (n : ℕ) in atTop, d ≤ ‖y_ n‖
K : Set X
hK : IsCompact K
hK' : Set.image (α := X) (⇑(↑T : X →ₗ[𝕜] X) : (a : X) → X) (Metric.closedBall 0 1) ⊆ K
y : X
hyK : y ∈ K
ψ : ℕ → ℕ
hψ : StrictMono ψ
hψy : Tendsto (y_ ∘ ψ) atTop (𝓝 y)
hy_lim :
  Tendsto.{0, u_2} (β := X) (fun (n : ℕ) ↦ (T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (y_ n)) atTop (𝓝 0)
⊢ Eq (α := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) y : X) (0 : X)

Tactic:
have hy_eigen' : (T - μ • 1) y = 0 := by
    apply tendsto_nhds_unique _ (hy_lim.comp hψ.tendsto_atTop)
    have : Continuous (T - μ • 1 : X →L[𝕜] X) := by fun_prop
    exact this.continuousAt.tendsto.comp hψy
-- 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
μ : 𝕜
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h :
  ∀ (c : ℝ) (_ : c > 0), ∃ (x : X), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < c * ‖x‖
c : ℝ
hc₀ : c > 0
hc :
  ∀ ε > 0, ∃ (x : X), ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < ε
φ : ℕ → ℝ
hφ_anti : StrictAnti φ
hφ_pos : ∀ (n : ℕ), 0 < φ n
hφ : Tendsto φ atTop (𝓝 0)
x : (n : ℕ) → X
hx_norm_upper : ∀ (n : ℕ), ‖x n‖ ≤ 1
hx_norm_lower : ∀ (n : ℕ), c ≤ ‖x n‖
hx_bound : ∀ (n : ℕ), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n) : X) < φ n
hx_lim :
  Tendsto.{0, u_2} (β := X) (fun (n : ℕ) ↦ (T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n)) atTop (𝓝 0)
y_ : (n : ℕ) → X := fun (n : ℕ) ↦ (T : (a : X) → X) (x n)
hy_lower : ∃ d > 0, ∀ᶠ (n : ℕ) in atTop, d ≤ ‖y_ n‖
K : Set X
hK : IsCompact K
hK' : Set.image (α := X) (⇑(↑T : X →ₗ[𝕜] X) : (a : X) → X) (Metric.closedBall 0 1) ⊆ K
y : X
hyK : y ∈ K
ψ : ℕ → ℕ
hψ : StrictMono ψ
hψy : Tendsto (y_ ∘ ψ) atTop (𝓝 y)
hy_lim :
  Tendsto.{0, u_2} (β := X) (fun (n : ℕ) ↦ (T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (y_ n)) atTop (𝓝 0)
hy_eigen' : Eq (α := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) y : X) (0 : X)
obtain : ∀ (d : ℝ) (hd₀ : d > 0) (hd : ∀ᶠ (n : ℕ) in atTop, d ≤ ‖y_ n‖), y ≠ 0
⊢ y ≠ 0

Tactic:
obtain ⟨d, hd₀, hd⟩ := hy_lower
-- 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
μ : 𝕜
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h :
  ∀ (c : ℝ) (_ : c > 0), ∃ (x : X), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < c * ‖x‖
c : ℝ
hc₀ : c > 0
hc :
  ∀ ε > 0, ∃ (x : X), ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < ε
φ : ℕ → ℝ
hφ_anti : StrictAnti φ
hφ_pos : ∀ (n : ℕ), 0 < φ n
hφ : Tendsto φ atTop (𝓝 0)
x : (n : ℕ) → X
hx_norm_upper : ∀ (n : ℕ), ‖x n‖ ≤ 1
hx_norm_lower : ∀ (n : ℕ), c ≤ ‖x n‖
hx_bound : ∀ (n : ℕ), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n) : X) < φ n
hx_lim :
  Tendsto.{0, u_2} (β := X) (fun (n : ℕ) ↦ (T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n)) atTop (𝓝 0)
y_ : (n : ℕ) → X := fun (n : ℕ) ↦ (T : (a : X) → X) (x n)
K : Set X
hK : IsCompact K
hK' : Set.image (α := X) (⇑(↑T : X →ₗ[𝕜] X) : (a : X) → X) (Metric.closedBall 0 1) ⊆ K
ψ : ℕ → ℕ
hψ : StrictMono ψ
hy_lim :
  Tendsto.{0, u_2} (β := X) (fun (n : ℕ) ↦ (T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (y_ n)) atTop (𝓝 0)
d : ℝ
hd₀ : d > 0
hd : ∀ᶠ (n : ℕ) in atTop, d ≤ ‖y_ n‖
hyK : 0 ∈ K
hψy : Tendsto (y_ ∘ ψ) atTop (𝓝 0)
hy_eigen' : Eq (α := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) 0 : X) (0 : X)
this : ∀ᶠ (n : ℕ) in atTop, False
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : False), False
⊢ False

Tactic:
rwa [eventually_const] at this

Premises used: Filter.eventually_const
-- 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
μ : 𝕜
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h :
  ∀ (c : ℝ) (_ : c > 0), ∃ (x : X), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < c * ‖x‖
c : ℝ
hc₀ : c > 0
hc :
  ∀ ε > 0, ∃ (x : X), ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < ε
φ : ℕ → ℝ
hφ_anti : StrictAnti φ
hφ_pos : ∀ (n : ℕ), 0 < φ n
hφ : Tendsto φ atTop (𝓝 0)
x : (n : ℕ) → X
hx_norm_upper : ∀ (n : ℕ), ‖x n‖ ≤ 1
hx_norm_lower : ∀ (n : ℕ), c ≤ ‖x n‖
hx_bound : ∀ (n : ℕ), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n) : X) < φ n
hx_lim :
  Tendsto.{0, u_2} (β := X) (fun (n : ℕ) ↦ (T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n)) atTop (𝓝 0)
y_ : (n : ℕ) → X := fun (n : ℕ) ↦ (T : (a : X) → X) (x n)
K : Set X
hK : IsCompact K
hK' : Set.image (α := X) (⇑(↑T : X →ₗ[𝕜] X) : (a : X) → X) (Metric.closedBall 0 1) ⊆ K
ψ : ℕ → ℕ
hψ : StrictMono ψ
hy_lim :
  Tendsto.{0, u_2} (β := X) (fun (n : ℕ) ↦ (T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (y_ n)) atTop (𝓝 0)
d : ℝ
hd₀ : d > 0
hd : ∀ᶠ (n : ℕ) in atTop, d ≤ ‖y_ n‖
hyK : 0 ∈ K
hψy : Tendsto (y_ ∘ ψ) atTop (𝓝 0)
hy_eigen' : Eq (α := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) 0 : X) (0 : X)
suffices : ∀ᶠ (n : ℕ) in atTop, False
⊢ False

Tactic:
suffices ∀ᶠ n : ℕ in atTop, False by rwa [eventually_const] at this
-- 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
μ : 𝕜
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h :
  ∀ (c : ℝ) (_ : c > 0), ∃ (x : X), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < c * ‖x‖
c : ℝ
hc₀ : c > 0
hc :
  ∀ ε > 0, ∃ (x : X), ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < ε
φ : ℕ → ℝ
hφ_anti : StrictAnti φ
hφ_pos : ∀ (n : ℕ), 0 < φ n
hφ : Tendsto φ atTop (𝓝 0)
x : (n : ℕ) → X
hx_norm_upper : ∀ (n : ℕ), ‖x n‖ ≤ 1
hx_norm_lower : ∀ (n : ℕ), c ≤ ‖x n‖
hx_bound : ∀ (n : ℕ), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n) : X) < φ n
hx_lim :
  Tendsto.{0, u_2} (β := X) (fun (n : ℕ) ↦ (T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n)) atTop (𝓝 0)
y_ : (n : ℕ) → X := fun (n : ℕ) ↦ (T : (a : X) → X) (x n)
K : Set X
hK : IsCompact K
hK' : Set.image (α := X) (⇑(↑T : X →ₗ[𝕜] X) : (a : X) → X) (Metric.closedBall 0 1) ⊆ K
ψ : ℕ → ℕ
hψ : StrictMono ψ
hy_lim :
  Tendsto.{0, u_2} (β := X) (fun (n : ℕ) ↦ (T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (y_ n)) atTop (𝓝 0)
d : ℝ
hd₀ : d > 0
hd : ∀ᶠ (n : ℕ) in atTop, d ≤ ‖y_ n‖
hyK : 0 ∈ K
hψy : Tendsto (y_ ∘ ψ) atTop (𝓝 0)
hy_eigen' : Eq (α := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) 0 : X) (0 : X)
⊢ ∀ ε > 0, ∀ᶠ (x : ℕ) in atTop, ‖(y_ ∘ ψ) x‖ < ε

Tactic:
rw [NormedAddGroup.tendsto_nhds_zero] at hψy

Premises used: NormedAddGroup.tendsto_nhds_zero