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)
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)
hψy₁ : ∀ ε > 0, ∀ᶠ (x : ℕ) in atTop, ‖(y_ ∘ ψ) x‖ < ε
⊢ Eq (α := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) 0 : X) (0 : X)

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

Premises used: NormedAddGroup.tendsto_nhds_zero
-- 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 : ∀ ε > 0, ∀ᶠ (x : ℕ) in atTop, ‖(y_ ∘ ψ) x‖ < ε
hy_eigen' : Eq (α := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) 0 : X) (0 : X)
⊢ d > 0

Tactic:
positivity
-- 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 : ∀ ε > 0, ∀ᶠ (x : ℕ) in atTop, ‖(y_ ∘ ψ) x‖ < ε
hy_eigen' : Eq (α := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) 0 : X) (0 : X)
⊢ ∀ (a : ℕ), d ≤ ‖y_ (ψ a)‖ → ‖(y_ ∘ ψ) a‖ < d → False

Tactic:
grind
-- 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 : ∀ ε > 0, ∀ᶠ (x : ℕ) in atTop, ‖(y_ ∘ ψ) x‖ < ε
hy_eigen' : Eq (α := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) 0 : X) (0 : X)
h₁ :
  ∀ (a : ℕ),
    Membership.mem (γ := Set ℕ)
      {x : ℕ |
        Membership.mem (γ := Set ℕ) {x : ℕ | (fun (x : ℕ) ↦ d ≤ ‖y_ (ψ x)‖) x} x →
          Membership.mem (γ := Set ℕ)
            {x : ℕ |
              Membership.mem (γ := Set ℕ) {x : ℕ | (fun (x : ℕ) ↦ ‖(y_ ∘ ψ) x‖ < d) x} x →
                Membership.mem (γ := Set ℕ) {x : ℕ | (fun (n : ℕ) ↦ False) x} x}
            x}
      a
h₂ : ∀ (a : ℕ), d ≤ ‖y_ (ψ a)‖ → ‖(y_ ∘ ψ) a‖ < d → False
⊢ ∀ᶠ (n : ℕ) in atTop, False

Tactic:
filter_upwards [hψ.tendsto_atTop.eventually hd, hψy d (by positivity)] using by grind

Premises used: StrictMono.tendsto_atTop, Filter.Tendsto.eventually
-- 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)
⊢ y ≠ 0

Tactic:
have hy_ne : y ≠ 0 := by
    obtain ⟨d, hd₀, hd⟩ := hy_lower
    rintro rfl
    suffices ∀ᶠ n : ℕ in atTop, False by rwa [eventually_const] at this
    rw [NormedAddGroup.tendsto_nhds_zero] at hψy
    filter_upwards [hψ.tendsto_atTop.eventually hd, hψy d (by positivity)] using by grind
-- 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)
hy_ne : y ≠ 0
⊢ HasEigenvector (↑T : X →ₗ[𝕜] X) μ y

Tactic:
simpa [hasEigenvector_iff, mem_genEigenspace_one, hy_ne, sub_eq_zero] using hy_eigen'

Premises used: sub_eq_zero, Module.End.hasEigenvector_iff, Module.End.mem_genEigenspace_one
-- 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)
hy_ne : y ≠ 0
⊢ HasEigenvector (↑T : X →ₗ[𝕜] X) μ y

Tactic:
have : HasEigenvector (T : End 𝕜 X) μ y := by
    simpa [hasEigenvector_iff, mem_genEigenspace_one, hy_ne, sub_eq_zero] using hy_eigen'
-- 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)
hy_ne : y ≠ 0
this : HasEigenvector (↑T : X →ₗ[𝕜] X) μ y
⊢ HasEigenvalue (↑T : X →ₗ[𝕜] X) μ

Tactic:
hasEigenvalue_of_hasEigenvector this

Premises used: Module.End.hasEigenvalue_of_hasEigenvector
-- 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)
hy_ne : y ≠ 0
this : HasEigenvector (↑T : X →ₗ[𝕜] X) μ y
⊢ HasEigenvalue (↑T : X →ₗ[𝕜] X) μ

Tactic:
exact hasEigenvalue_of_hasEigenvector this

Premises used: Module.End.hasEigenvalue_of_hasEigenvector
-- 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
S : End 𝕜 X
hS_not_surj : ¬Function.Surjective (α := X) (β := X) (⇑S : (a : X) → X)
hS_anti : Topology.IsClosedEmbedding (X := X) (Y := X) (⇑S : (a : X) → X)
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
V : (n : ℕ) → Submodule 𝕜 X := fun (n : ℕ) ↦ (LinearMap.iterateRange S : (a : ℕ) → (Submodule 𝕜 X)ᵒᵈ) n
⊢ ∀ (n : ℕ), V (n + 1) = Submodule.map S (V n)

Tactic:
have hV_succ (n : ℕ) : V (n + 1) = (V n).map (S : End 𝕜 X) := LinearMap.iterateRange_succ
-- 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
S : End 𝕜 X
hS_not_surj : ¬Function.Surjective (α := X) (β := X) (⇑S : (a : X) → X)
hS_anti : Topology.IsClosedEmbedding (X := X) (Y := X) (⇑S : (a : X) → X)
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
V : (n : ℕ) → Submodule 𝕜 X := fun (n : ℕ) ↦ (LinearMap.iterateRange S : (a : ℕ) → (Submodule 𝕜 X)ᵒᵈ) n
hV_succ : ∀ (n : ℕ), V (n + 1) = Submodule.map S (V n)
⊢ IsClosed (↑(V 0) : Set X)

Tactic:
simp [V, Module.End.one_eq_id]

Premises used: Module.End.one_eq_id
-- 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
S : End 𝕜 X
hS_not_surj : ¬Function.Surjective (α := X) (β := X) (⇑S : (a : X) → X)
hS_anti : Topology.IsClosedEmbedding (X := X) (Y := X) (⇑S : (a : X) → X)
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
V : (n : ℕ) → Submodule 𝕜 X := fun (n : ℕ) ↦ (LinearMap.iterateRange S : (a : ℕ) → (Submodule 𝕜 X)ᵒᵈ) n
hV_succ : ∀ (n : ℕ), V (n + 1) = Submodule.map S (V n)
n : ℕ
ih : IsClosed (↑(V n) : Set X)
succ : IsClosed (↑(Submodule.map S (V n)) : Set X)
⊢ IsClosed (↑(V (n + 1)) : Set X)

Tactic:
rw [hV_succ]
-- 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
S : End 𝕜 X
hS_not_surj : ¬Function.Surjective (α := X) (β := X) (⇑S : (a : X) → X)
hS_anti : Topology.IsClosedEmbedding (X := X) (Y := X) (⇑S : (a : X) → X)
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
V : (n : ℕ) → Submodule 𝕜 X := fun (n : ℕ) ↦ (LinearMap.iterateRange S : (a : ℕ) → (Submodule 𝕜 X)ᵒᵈ) n
hV_succ : ∀ (n : ℕ), V (n + 1) = Submodule.map S (V n)
n : ℕ
ih : IsClosed (↑(V n) : Set X)
⊢ IsClosed (↑(Submodule.map S (V n)) : Set X)

Tactic:
apply hS_anti.isClosedMap _ ih

Premises used: Topology.IsClosedEmbedding.isClosedMap
-- 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
S : End 𝕜 X
hS_not_surj : ¬Function.Surjective (α := X) (β := X) (⇑S : (a : X) → X)
hS_anti : Topology.IsClosedEmbedding (X := X) (Y := X) (⇑S : (a : X) → X)
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
V : (n : ℕ) → Submodule 𝕜 X := fun (n : ℕ) ↦ (LinearMap.iterateRange S : (a : ℕ) → (Submodule 𝕜 X)ᵒᵈ) n
hV_succ : ∀ (n : ℕ), V (n + 1) = Submodule.map S (V n)
n : ℕ
zero : IsClosed (↑(V 0) : Set X)
succ : ∀ (n : ℕ) (ih : IsClosed (↑(V n) : Set X)), IsClosed (↑(V (n + 1)) : Set X)
⊢ IsClosed (↑(V n) : Set X)

Tactic:
induction n with
    | zero => simp [V, Module.End.one_eq_id]
    | succ n ih =>
      rw [hV_succ]
      apply hS_anti.isClosedMap _ ih

Premises used: Module.End.one_eq_id
-- 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
S : End 𝕜 X
hS_not_surj : ¬Function.Surjective (α := X) (β := X) (⇑S : (a : X) → X)
hS_anti : Topology.IsClosedEmbedding (X := X) (Y := X) (⇑S : (a : X) → X)
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
V : (n : ℕ) → Submodule 𝕜 X := fun (n : ℕ) ↦ (LinearMap.iterateRange S : (a : ℕ) → (Submodule 𝕜 X)ᵒᵈ) n
hV_succ : ∀ (n : ℕ), V (n + 1) = Submodule.map S (V n)
⊢ ∀ (n : ℕ), IsClosed (↑(V n) : Set X)

Tactic:
have hV_closed (n : ℕ) : IsClosed (V n : Set X) := by
    induction n with
    | zero => simp [V, Module.End.one_eq_id]
    | succ n ih =>
      rw [hV_succ]
      apply hS_anti.isClosedMap _ ih
-- 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
S : End 𝕜 X
hS_not_surj : ¬Function.Surjective (α := X) (β := X) (⇑S : (a : X) → X)
hS_anti : Topology.IsClosedEmbedding (X := X) (Y := X) (⇑S : (a : X) → X)
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
V : (n : ℕ) → Submodule 𝕜 X := fun (n : ℕ) ↦ (LinearMap.iterateRange S : (a : ℕ) → (Submodule 𝕜 X)ᵒᵈ) n
hV_succ : ∀ (n : ℕ), V (n + 1) = Submodule.map S (V n)
hV_closed : ∀ (n : ℕ), IsClosed (↑(V n) : Set X)
n : ℕ
⊢ IsClosed (↑(Submodule.comap (V n).subtype (V (n + 1))) : Set ↥(V n))

Tactic:
simpa using (hV_closed (n + 1)).preimage_val

Premises used: IsClosed.preimage_val, HAdd.hAdd, 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
S : End 𝕜 X
hS_not_surj : ¬Function.Surjective (α := X) (β := X) (⇑S : (a : X) → X)
hS_anti : Topology.IsClosedEmbedding (X := X) (Y := X) (⇑S : (a : X) → X)
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
V : (n : ℕ) → Submodule 𝕜 X := fun (n : ℕ) ↦ (LinearMap.iterateRange S : (a : ℕ) → (Submodule 𝕜 X)ᵒᵈ) n
hV_succ : ∀ (n : ℕ), V (n + 1) = Submodule.map S (V n)
hV_closed : ∀ (n : ℕ), IsClosed (↑(V n) : Set X)
n : ℕ
⊢ IsClosed (↑(Submodule.comap (V n).subtype (V (n + 1))) : Set ↥(V n))

Tactic:
have h₁ : IsClosed ((V (n + 1)).comap (V n).subtype : Set (V n)) := by
      simpa using (hV_closed (n + 1)).preimage_val
-- 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
S : End 𝕜 X
hS_not_surj : ¬Function.Surjective (α := X) (β := X) (⇑S : (a : X) → X)
hS_anti : Topology.IsClosedEmbedding (X := X) (Y := X) (⇑S : (a : X) → X)
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
V : (n : ℕ) → Submodule 𝕜 X := fun (n : ℕ) ↦ (LinearMap.iterateRange S : (a : ℕ) → (Submodule 𝕜 X)ᵒᵈ) n
hV_succ : ∀ (n : ℕ), V (n + 1) = Submodule.map S (V n)
hV_closed : ∀ (n : ℕ), IsClosed (↑(V n) : Set X)
n : ℕ
h₁ : IsClosed (↑(Submodule.comap (V n).subtype (V (n + 1))) : Set ↥(V n))
⊢ ∃ (x : ↥(V n)), x ∉ Submodule.comap (V n).subtype (V (n + 1))

Tactic:
simpa [iterate_succ, V, (iterate_injective hS_anti.injective n).eq_iff,
        Function.Surjective] using hS_not_surj

Premises used: Function.Injective.eq_iff, Topology.IsClosedEmbedding.toIsEmbedding, Topology.IsEmbedding.injective, Module.End.iterate_succ, Function.Surjective, Module.End.iterate_injective
-- 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
S : End 𝕜 X
hS_not_surj : ¬Function.Surjective (α := X) (β := X) (⇑S : (a : X) → X)
hS_anti : Topology.IsClosedEmbedding (X := X) (Y := X) (⇑S : (a : X) → X)
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
V : (n : ℕ) → Submodule 𝕜 X := fun (n : ℕ) ↦ (LinearMap.iterateRange S : (a : ℕ) → (Submodule 𝕜 X)ᵒᵈ) n
hV_succ : ∀ (n : ℕ), V (n + 1) = Submodule.map S (V n)
hV_closed : ∀ (n : ℕ), IsClosed (↑(V n) : Set X)
n : ℕ
h₁ : IsClosed (↑(Submodule.comap (V n).subtype (V (n + 1))) : Set ↥(V n))
⊢ ∃ (x : ↥(V n)), x ∉ Submodule.comap (V n).subtype (V (n + 1))

Tactic:
have h₂ : ∃ x : V n, x ∉ (V (n + 1)).comap (V n).subtype := by
      simpa [iterate_succ, V, (iterate_injective hS_anti.injective n).eq_iff,
        Function.Surjective] using hS_not_surj