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
μ : 𝕜
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
have obtain : ∀ (d : ℝ) (hd₀ : d > 0) (hd : ∀ᶠ (n : ℕ) in atTop, d ≤ ‖y_ n‖), y ≠ 0
Tactic: obtain ⟨d, hd₀, hd⟩ := hy_lower
Cleared hypotheses: hy_lower
-- 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
μ : 𝕜
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
⊢ False
have rwa : ∀ (this : False), False
Tactic: rwa [eventually_const] at this
Cleared hypotheses: this
-- 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
μ : 𝕜
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)
⊢ False
have suffices : ∀ᶠ (n : ℕ) in atTop, False
Tactic: suffices ∀ᶠ n : ℕ in atTop, False by rwa [eventually_const] at this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative (hypothesis)
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)
⊢ ∀ᶠ (n : ℕ) in atTop, False
have hψy₁ : ∀ ε > 0, ∀ᶠ (x : ℕ) in atTop, ‖(y_ ∘ ψ) x‖ < ε
Tactic: rw [NormedAddGroup.tendsto_nhds_zero] at hψy
Cleared hypotheses: hψy, hy_eigen'
-- 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
μ : 𝕜
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)
⊢ ∀ᶠ (n : ℕ) in atTop, False
have 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
Tactic: filter_upwards [hψ.tendsto_atTop.eventually hd, hψy d (by positivity)] using by grind
-- 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
μ : 𝕜
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
⊢ ∀ᶠ (n : ℕ) in atTop, False
have h₂ : ∀ (a : ℕ), d ≤ ‖y_ (ψ a)‖ → ‖(y_ ∘ ψ) a‖ < d → False
Tactic: filter_upwards [hψ.tendsto_atTop.eventually hd, hψy d (by positivity)] using by grind
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative (hypothesis)
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)
⊢ HasEigenvalue (↑T : X →ₗ[𝕜] X) μ
have hy_ne : 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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative (hypothesis)
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
⊢ HasEigenvalue (↑T : X →ₗ[𝕜] X) μ
have this : 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'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative (hypothesis)
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
⊢ ∃ (f : ℕ → X),
    (∀ (n : ℕ), 1 ≤ ‖f n‖) ∧
      (∀ (n : ℕ), ‖f n‖ ≤ R) ∧
        (∀ (n : ℕ), f n ∈ LinearMap.range (S ^ n)) ∧ ∀ (n : ℕ), ∀ y ∈ LinearMap.range (S ^ (n + 1)), 1 ≤ ‖f n - y‖
have hV_succ : ∀ (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
-- 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
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 (↑(V (n + 1)) : Set X)
have succ : IsClosed (↑(Submodule.map S (V n)) : Set X)
Tactic: rw [hV_succ]
-- 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
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)
have zero : IsClosed (↑(V 0) : 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
Cleared hypotheses: n
-- 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
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)
⊢ IsClosed (↑(V n) : Set X)
have succ : ∀ (n : ℕ) (ih : IsClosed (↑(V n) : Set X)), IsClosed (↑(V (n + 1)) : 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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative (hypothesis)
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)
⊢ ∃ (f : ℕ → X),
    (∀ (n : ℕ), 1 ≤ ‖f n‖) ∧
      (∀ (n : ℕ), ‖f n‖ ≤ R) ∧
        (∀ (n : ℕ), f n ∈ LinearMap.range (S ^ n)) ∧ ∀ (n : ℕ), ∀ y ∈ LinearMap.range (S ^ (n + 1)), 1 ≤ ‖f n - y‖
have hV_closed : ∀ (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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative (hypothesis)
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 : ℕ
⊢ ∃ x ∈ V n, 1 ≤ ‖x‖ ∧ ‖x‖ ≤ R ∧ ∀ y ∈ V (n + 1), 1 ≤ ‖x - y‖
have h₁ : 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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative (hypothesis)
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, 1 ≤ ‖x‖ ∧ ‖x‖ ≤ R ∧ ∀ y ∈ V (n + 1), 1 ≤ ‖x - y‖
have h₂ : ∃ (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
-- 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
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))
h₂ : ∃ (x : ↥(V n)), x ∉ Submodule.comap (V n).subtype (V (n + 1))
⊢ ∃ x ∈ V n, 1 ≤ ‖x‖ ∧ ‖x‖ ≤ R ∧ ∀ y ∈ V (n + 1), 1 ≤ ‖x - y‖
have obtain : ∀ (x : X) (hx : x ∈ V n) (hxn : ‖Subtype.mk (p := fun (x : X) ↦ x ∈ V n) x hx‖ ≤ R)
  (hxy : ∀ y ∈ Submodule.comap (V n).subtype (V (n + 1)), 1 ≤ ‖Subtype.mk (p := fun (x : X) ↦ x ∈ V n) x hx - y‖),
  ∃ x ∈ V n, 1 ≤ ‖x‖ ∧ ‖x‖ ≤ R ∧ ∀ y ∈ V (n + 1), 1 ≤ ‖x - y‖
Tactic: obtain ⟨⟨x, hx⟩, hxn, hxy⟩ := riesz_lemma_of_norm_lt hc hR h₁ h₂
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative (hypothesis)
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))
h₂ : ∃ (x : ↥(V n)), x ∉ Submodule.comap (V n).subtype (V (n + 1))
x : X
hx : x ∈ V n
hxn : ‖Subtype.mk (p := fun (x : X) ↦ x ∈ V n) x hx‖ ≤ R
hxy : ∀ y ∈ Submodule.comap (V n).subtype (V (n + 1)), 1 ≤ ‖Subtype.mk (p := fun (x : X) ↦ x ∈ V n) x hx - y‖
⊢ ∃ x ∈ V n, 1 ≤ ‖x‖ ∧ ‖x‖ ≤ R ∧ ∀ y ∈ V (n + 1), 1 ≤ ‖x - y‖
have hxy₁ : ∀ (a : X) (b : a ∈ V n), a ∈ V (n + 1) → 1 ≤ ‖x - a‖
Tactic: simp only [Submodule.mem_comap, Submodule.subtype_apply, AddSubgroupClass.coe_norm,
      AddSubgroupClass.coe_sub, Subtype.forall] at hxn hxy
Cleared hypotheses: hxy