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‖
hK : ∀ K > 0, ∃ (x : X), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < K * ‖x‖
C : 𝕜
hC : 1 < ‖C‖
ε : ℝ
hε : ε > 0
x : X
hx : norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < ε * ‖x‖
this : x ≠ 0
η : 𝕜
hη : η ≠ 0
h₁ : ‖η • x‖ < 1
h₂ : 1 / ‖C‖ ≤ ‖η • x‖
h₃ : ‖η‖⁻¹ ≤ 1⁻¹ * ‖C‖ * ‖x‖
⊢ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (η • x) : X) < ε
have grw : ε * ‖η • x‖ < ε
Tactic: grw [map_smul, norm_smul, hx, mul_left_comm, ← norm_smul]
-- 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‖
hK : ∀ K > 0, ∃ (x : X), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < K * ‖x‖
⊢ HasEigenvalue (↑T : X →ₗ[𝕜] X) μ
have hK₁ : ∃ c > 0,
  ∀ ε > 0, ∃ (x : X), ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < ε
Tactic: replace hK : ∃ c > 0, ∀ ε > 0, ∃ x, ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ ‖(T - μ • 1) x‖ < ε := by
    obtain ⟨C, hC⟩ := NormedField.exists_one_lt_norm 𝕜
    refine ⟨‖C‖⁻¹, by positivity, fun ε hε ↦ ?_⟩
    obtain ⟨x, hx⟩ := hK ε (by positivity)
    have : x ≠ 0 := by aesop
    obtain ⟨η, hη, h₁, h₂, h₃⟩ := rescale_to_shell hC (ε := 1) (by simp) this
    refine ⟨η • x, h₁.le, by simpa using h₂, ?_⟩
    grw [map_smul, norm_smul, hx, mul_left_comm, ← norm_smul]
    linear_combination ε * h₁
Cleared hypotheses: hK
-- 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‖
hK :
  ∃ c > 0,
    ∀ ε > 0,
      ∃ (x : X), ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < ε
⊢ HasEigenvalue (↑T : X →ₗ[𝕜] X) μ
have obtain : ∀ (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) < ε),
  HasEigenvalue (↑T : X →ₗ[𝕜] X) μ
Tactic: obtain ⟨c, hc₀, hc⟩ := hK
Cleared hypotheses: hK
-- 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) < ε
⊢ HasEigenvalue (↑T : X →ₗ[𝕜] X) μ
have obtain : ∀ (φ : ℕ → ℝ) (hφ_anti : StrictAnti φ) (hφ_pos : ∀ (n : ℕ), 0 < φ n) (hφ : Tendsto φ atTop (𝓝 0)),
  HasEigenvalue (↑T : X →ₗ[𝕜] X) μ
Tactic: obtain ⟨φ, hφ_anti, hφ_pos, hφ⟩ := exists_seq_strictAnti_tendsto (0 : ℝ)
-- 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)
⊢ HasEigenvalue (↑T : X →ₗ[𝕜] X) μ
have this : ∀ (n : ℕ),
  ∃ (x : X), ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < φ n
Tactic: have (n : ℕ) : ∃ x, ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ ‖(T - μ • 1) x‖ < φ n := hc (φ n) (hφ_pos 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
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)
this :
  ∀ (n : ℕ),
    ∃ (x : X), ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < φ n
⊢ HasEigenvalue (↑T : X →ₗ[𝕜] X) μ
have choose : ∀ (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),
  HasEigenvalue (↑T : X →ₗ[𝕜] X) μ
Tactic: choose x hx_norm_upper hx_norm_lower hx_bound using this
Cleared hypotheses: 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
⊢ HasEigenvalue (↑T : X →ₗ[𝕜] X) μ
have hx_lim : Tendsto.{0, u_2} (β := X) (fun (n : ℕ) ↦ (T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n)) atTop (𝓝 0)
Tactic: have hx_lim : Tendsto (fun n ↦ (T - μ • 1) (x n)) atTop (𝓝 0) := squeeze_zero_norm (by grind) hφ
-- 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)
⊢ ∃ d > 0, ∀ᶠ (n : ℕ) in atTop, d ≤ ‖y_ n‖
have refine : ∀ᶠ (n : ℕ) in atTop, ‖μ‖ * c / 2 ≤ ‖y_ n‖
Tactic: refine ⟨(‖μ‖ * c) / 2, by positivity, ?_⟩
-- 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)
⊢ ∀ᶠ (n : ℕ) in atTop, ‖μ‖ * c / 2 ≤ ‖y_ n‖
have h₁ : ∀ (n : ℕ) (hn : φ n ≤ ‖μ‖ * c / 2), ‖μ‖ * c / 2 ≤ ‖y_ n‖
Tactic: filter_upwards [hφ.eventually_le_const (show (‖μ‖ * c) / 2 > 0 by positivity)] with n hn
-- 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)
n : ℕ
hn : φ n ≤ ‖μ‖ * c / 2
⊢ ‖μ‖ * c / 2 ≤ ‖y_ n‖
have h₁ : ‖HSub.hSub (α := X) ((T : (a : X) → X) (x n) : X) (μ • x n)‖ < φ n
Tactic: have h₁ : ‖T (x n) - μ • x n‖ < φ n := by simpa using hx_bound 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
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)
n : ℕ
hn : φ n ≤ ‖μ‖ * c / 2
h₁ : ‖HSub.hSub (α := X) ((T : (a : X) → X) (x n) : X) (μ • x n)‖ < φ n
⊢ ‖μ‖ * c / 2 ≤ ‖y_ n‖
have h₂ : ‖μ‖ * ‖x n‖ ≤ norm (E := X) ((T : (a : X) → X) (x n) : X) + ‖HSub.hSub (α := X) ((T : (a : X) → X) (x n) : X) (μ • x n)‖
Tactic: have h₂ : ‖μ‖ * ‖x n‖ ≤ ‖T (x n)‖ + ‖T (x n) - μ • x n‖ := by
      simpa [norm_smul] using norm_le_norm_add_norm_sub (T (x n)) (μ • x 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
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)
⊢ HasEigenvalue (↑T : X →ₗ[𝕜] X) μ
have hy_lower : ∃ d > 0, ∀ᶠ (n : ℕ) in atTop, d ≤ ‖y_ n‖
Tactic: have hy_lower : ∃ d > 0, ∀ᶠ n in atTop, d ≤ ‖y_ n‖ := by
    refine ⟨(‖μ‖ * c) / 2, by positivity, ?_⟩
    filter_upwards [hφ.eventually_le_const (show (‖μ‖ * c) / 2 > 0 by positivity)] with n hn
    have h₁ : ‖T (x n) - μ • x n‖ < φ n := by simpa using hx_bound n
    have h₂ : ‖μ‖ * ‖x n‖ ≤ ‖T (x n)‖ + ‖T (x n) - μ • x n‖ := by
      simpa [norm_smul] using norm_le_norm_add_norm_sub (T (x n)) (μ • x n)
    linear_combination h₂ + h₁ + hn + ‖μ‖ * hx_norm_lower 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
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‖
⊢ HasEigenvalue (↑T : X →ₗ[𝕜] X) μ
have 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) μ
Tactic: obtain ⟨K, hK, hK'⟩ := hT.image_closedBall_subset_compact 1
-- 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
⊢ HasEigenvalue (↑T : X →ₗ[𝕜] X) μ
have obtain : ∀ (y : X) (hyK : y ∈ K) (ψ : ℕ → ℕ) (hψ : StrictMono ψ) (hψy : Tendsto (y_ ∘ ψ) atTop (𝓝 y)),
  HasEigenvalue (↑T : X →ₗ[𝕜] X) μ
Tactic: obtain ⟨y, hyK, ψ, hψ, hψy⟩ := hK.tendsto_subseq (x := y_) (fun n ↦ hK' ⟨x n, by simp [*], rfl⟩)
-- 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)
⊢ HasEigenvalue (↑T : X →ₗ[𝕜] X) μ
have hy_lim : 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
-- 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)
⊢ Eq (α := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) y : X) (0 : X)
have 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)
Tactic: apply tendsto_nhds_unique _ (hy_lim.comp hψ.tendsto_atTop)
-- 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)
⊢ 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)
have this : 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
-- 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)
⊢ HasEigenvalue (↑T : X →ₗ[𝕜] X) μ
have hy_eigen' : 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