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
μ : 𝕜
inst_3 : CompleteSpace X
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h₁ : ¬HasEigenvalue (↑T : X →ₗ[𝕜] X) μ
S : X →L[𝕜] X := T - HSMul.hSMul (β := X →L[𝕜] X) μ 1
K : NNReal
hK : AntilipschitzWith (α := X) (β := X) K (⇑S : (a : X) → X)
h₂ : ¬Function.Surjective (α := X) (β := X) (⇑S : (a : X) → X)
c : 𝕜
hc : 1 < ‖c‖
f : ℕ → X
hf_norm_lower : ∀ (n : ℕ), 1 ≤ ‖f n‖
hf_norm_upper : ∀ (n : ℕ), ‖f n‖ ≤ ‖c‖ + 1
hf_far : ∀ (n : ℕ), ∀ y ∈ LinearMap.range ((↑S : X →ₗ[𝕜] X) ^ (n + 1)), 1 ≤ ‖f n - y‖
hf_mem : ∀ {n m : ℕ} (h : m ≤ n), f n ∈ ((↑S : X →ₗ[𝕜] X) ^ m).range
hf_mem' :
  ∀ {n m : ℕ} (h : m ≤ n), Membership.mem (α := X) ((↑S : X →ₗ[𝕜] X) ^ (m + 1)).range ((S : (a : X) → X) (f n) : X)
m n : ℕ
hmn : m < n
u : X := μ⁻¹ • (HSub.hSub (α := X) (β := X) ((S : (a : X) → X) (f n) : X) ((S : (a : X) → X) (f m) : X) + μ • f n)
hu : μ • (f m - u) = HSub.hSub (α := X) (β := X) ((T : (a : X) → X) (f m) : X) ((T : (a : X) → X) (f n) : X)
⊢ u ∈ ((↑S : X →ₗ[𝕜] X) ^ (m + 1)).range
have apply : HSub.hSub (α := X) (β := X) ((S : (a : X) → X) (f n) : X) ((S : (a : X) → X) (f m) : X) ∈
  ((↑S : X →ₗ[𝕜] X) ^ (m + 1)).range
Tactic: apply Submodule.smul_mem _ _ (Submodule.add_mem _ _ _)
-- 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
μ : 𝕜
inst_3 : CompleteSpace X
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h₁ : ¬HasEigenvalue (↑T : X →ₗ[𝕜] X) μ
S : X →L[𝕜] X := T - HSMul.hSMul (β := X →L[𝕜] X) μ 1
K : NNReal
hK : AntilipschitzWith (α := X) (β := X) K (⇑S : (a : X) → X)
h₂ : ¬Function.Surjective (α := X) (β := X) (⇑S : (a : X) → X)
c : 𝕜
hc : 1 < ‖c‖
f : ℕ → X
hf_norm_lower : ∀ (n : ℕ), 1 ≤ ‖f n‖
hf_norm_upper : ∀ (n : ℕ), ‖f n‖ ≤ ‖c‖ + 1
hf_far : ∀ (n : ℕ), ∀ y ∈ LinearMap.range ((↑S : X →ₗ[𝕜] X) ^ (n + 1)), 1 ≤ ‖f n - y‖
hf_mem : ∀ {n m : ℕ} (h : m ≤ n), f n ∈ ((↑S : X →ₗ[𝕜] X) ^ m).range
hf_mem' :
  ∀ {n m : ℕ} (h : m ≤ n), Membership.mem (α := X) ((↑S : X →ₗ[𝕜] X) ^ (m + 1)).range ((S : (a : X) → X) (f n) : X)
m n : ℕ
hmn : m < n
u : X := μ⁻¹ • (HSub.hSub (α := X) (β := X) ((S : (a : X) → X) (f n) : X) ((S : (a : X) → X) (f m) : X) + μ • f n)
hu : μ • (f m - u) = HSub.hSub (α := X) (β := X) ((T : (a : X) → X) (f m) : X) ((T : (a : X) → X) (f n) : X)
apply :
  HSub.hSub (α := X) (β := X) ((S : (a : X) → X) (f n) : X) ((S : (a : X) → X) (f m) : X) ∈
    ((↑S : X →ₗ[𝕜] X) ^ (m + 1)).range
⊢ u ∈ ((↑S : X →ₗ[𝕜] X) ^ (m + 1)).range
have apply₁ : μ • f n ∈ ((↑S : X →ₗ[𝕜] X) ^ (m + 1)).range
Tactic: apply Submodule.smul_mem _ _ (Submodule.add_mem _ _ _)
-- 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
μ : 𝕜
inst_3 : CompleteSpace X
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h₁ : ¬HasEigenvalue (↑T : X →ₗ[𝕜] X) μ
S : X →L[𝕜] X := T - HSMul.hSMul (β := X →L[𝕜] X) μ 1
K : NNReal
hK : AntilipschitzWith (α := X) (β := X) K (⇑S : (a : X) → X)
h₂ : ¬Function.Surjective (α := X) (β := X) (⇑S : (a : X) → X)
c : 𝕜
hc : 1 < ‖c‖
f : ℕ → X
hf_norm_lower : ∀ (n : ℕ), 1 ≤ ‖f n‖
hf_norm_upper : ∀ (n : ℕ), ‖f n‖ ≤ ‖c‖ + 1
hf_far : ∀ (n : ℕ), ∀ y ∈ LinearMap.range ((↑S : X →ₗ[𝕜] X) ^ (n + 1)), 1 ≤ ‖f n - y‖
hf_mem : ∀ {n m : ℕ} (h : m ≤ n), f n ∈ ((↑S : X →ₗ[𝕜] X) ^ m).range
hf_mem' :
  ∀ {n m : ℕ} (h : m ≤ n), Membership.mem (α := X) ((↑S : X →ₗ[𝕜] X) ^ (m + 1)).range ((S : (a : X) → X) (f n) : X)
m n : ℕ
hmn : m < n
u : X := μ⁻¹ • (HSub.hSub (α := X) (β := X) ((S : (a : X) → X) (f n) : X) ((S : (a : X) → X) (f m) : X) + μ • f n)
hu : μ • (f m - u) = HSub.hSub (α := X) (β := X) ((T : (a : X) → X) (f m) : X) ((T : (a : X) → X) (f n) : X)
⊢ ‖μ‖ ≤ ‖HSub.hSub (α := X) (β := X) ((T : (a : X) → X) (f m) : X) ((T : (a : X) → X) (f n) : X)‖
have this : u ∈ ((↑S : X →ₗ[𝕜] X) ^ (m + 1)).range
Tactic: have : u ∈ ((S : End 𝕜 X) ^ (m + 1)).range := by
      apply Submodule.smul_mem _ _ (Submodule.add_mem _ _ _)
      · exact Submodule.sub_mem _ (hf_mem' hmn.le) (hf_mem' le_rfl)
      · exact Submodule.smul_mem _ μ (hf_mem hmn)
-- 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
μ : 𝕜
inst_3 : CompleteSpace X
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h₁ : ¬HasEigenvalue (↑T : X →ₗ[𝕜] X) μ
S : X →L[𝕜] X := T - HSMul.hSMul (β := X →L[𝕜] X) μ 1
K : NNReal
hK : AntilipschitzWith (α := X) (β := X) K (⇑S : (a : X) → X)
h₂ : ¬Function.Surjective (α := X) (β := X) (⇑S : (a : X) → X)
c : 𝕜
hc : 1 < ‖c‖
f : ℕ → X
hf_norm_lower : ∀ (n : ℕ), 1 ≤ ‖f n‖
hf_norm_upper : ∀ (n : ℕ), ‖f n‖ ≤ ‖c‖ + 1
hf_far : ∀ (n : ℕ), ∀ y ∈ LinearMap.range ((↑S : X →ₗ[𝕜] X) ^ (n + 1)), 1 ≤ ‖f n - y‖
hf_mem : ∀ {n m : ℕ} (h : m ≤ n), f n ∈ ((↑S : X →ₗ[𝕜] X) ^ m).range
hf_mem' :
  ∀ {n m : ℕ} (h : m ≤ n), Membership.mem (α := X) ((↑S : X →ₗ[𝕜] X) ^ (m + 1)).range ((S : (a : X) → X) (f n) : X)
m n : ℕ
hmn : m < n
u : X := μ⁻¹ • (HSub.hSub (α := X) (β := X) ((S : (a : X) → X) (f n) : X) ((S : (a : X) → X) (f m) : X) + μ • f n)
hu : μ • (f m - u) = HSub.hSub (α := X) (β := X) ((T : (a : X) → X) (f m) : X) ((T : (a : X) → X) (f n) : X)
this : u ∈ ((↑S : X →ₗ[𝕜] X) ^ (m + 1)).range
⊢ ‖μ‖ ≤ ‖HSub.hSub (α := X) (β := X) ((T : (a : X) → X) (f m) : X) ((T : (a : X) → X) (f n) : X)‖
have a : ‖μ‖ ≤ ‖μ • (f m - u)‖
Tactic: grw [← hu, norm_smul, mul_comm, ← hf_far _ u this, one_mul]
-- 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
μ : 𝕜
inst_3 : CompleteSpace X
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h₁ : ¬HasEigenvalue (↑T : X →ₗ[𝕜] X) μ
S : X →L[𝕜] X := T - HSMul.hSMul (β := X →L[𝕜] X) μ 1
K : NNReal
hK : AntilipschitzWith (α := X) (β := X) K (⇑S : (a : X) → X)
h₂ : ¬Function.Surjective (α := X) (β := X) (⇑S : (a : X) → X)
c : 𝕜
hc : 1 < ‖c‖
f : ℕ → X
hf_norm_lower : ∀ (n : ℕ), 1 ≤ ‖f n‖
hf_norm_upper : ∀ (n : ℕ), ‖f n‖ ≤ ‖c‖ + 1
hf_far : ∀ (n : ℕ), ∀ y ∈ LinearMap.range ((↑S : X →ₗ[𝕜] X) ^ (n + 1)), 1 ≤ ‖f n - y‖
hf_mem : ∀ {n m : ℕ} (h : m ≤ n), f n ∈ ((↑S : X →ₗ[𝕜] X) ^ m).range
hf_mem' :
  ∀ {n m : ℕ} (h : m ≤ n), Membership.mem (α := X) ((↑S : X →ₗ[𝕜] X) ^ (m + 1)).range ((S : (a : X) → X) (f n) : X)
m n : ℕ
hmn : m < n
u : X := μ⁻¹ • (HSub.hSub (α := X) (β := X) ((S : (a : X) → X) (f n) : X) ((S : (a : X) → X) (f m) : X) + μ • f n)
hu : μ • (f m - u) = HSub.hSub (α := X) (β := X) ((T : (a : X) → X) (f m) : X) ((T : (a : X) → X) (f n) : X)
this : u ∈ ((↑S : X →ₗ[𝕜] X) ^ (m + 1)).range
a : ‖μ‖ ≤ ‖μ • (f m - u)‖
⊢ ‖μ‖ ≤ ‖HSub.hSub (α := X) (β := X) ((T : (a : X) → X) (f m) : X) ((T : (a : X) → X) (f n) : X)‖
have a₁ : ‖μ‖ ≤ ‖μ‖ * ‖f m - u‖
Tactic: grw [← hu, norm_smul, mul_comm, ← hf_far _ u this, one_mul]
-- 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
μ : 𝕜
inst_3 : CompleteSpace X
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h₁ : ¬HasEigenvalue (↑T : X →ₗ[𝕜] X) μ
S : X →L[𝕜] X := T - HSMul.hSMul (β := X →L[𝕜] X) μ 1
K : NNReal
hK : AntilipschitzWith (α := X) (β := X) K (⇑S : (a : X) → X)
h₂ : ¬Function.Surjective (α := X) (β := X) (⇑S : (a : X) → X)
c : 𝕜
hc : 1 < ‖c‖
f : ℕ → X
hf_norm_lower : ∀ (n : ℕ), 1 ≤ ‖f n‖
hf_norm_upper : ∀ (n : ℕ), ‖f n‖ ≤ ‖c‖ + 1
hf_far : ∀ (n : ℕ), ∀ y ∈ LinearMap.range ((↑S : X →ₗ[𝕜] X) ^ (n + 1)), 1 ≤ ‖f n - y‖
hf_mem : ∀ {n m : ℕ} (h : m ≤ n), f n ∈ ((↑S : X →ₗ[𝕜] X) ^ m).range
hf_mem' :
  ∀ {n m : ℕ} (h : m ≤ n), Membership.mem (α := X) ((↑S : X →ₗ[𝕜] X) ^ (m + 1)).range ((S : (a : X) → X) (f n) : X)
m n : ℕ
hmn : m < n
u : X := μ⁻¹ • (HSub.hSub (α := X) (β := X) ((S : (a : X) → X) (f n) : X) ((S : (a : X) → X) (f m) : X) + μ • f n)
hu : μ • (f m - u) = HSub.hSub (α := X) (β := X) ((T : (a : X) → X) (f m) : X) ((T : (a : X) → X) (f n) : X)
this : u ∈ ((↑S : X →ₗ[𝕜] X) ^ (m + 1)).range
a : ‖μ‖ ≤ ‖μ • (f m - u)‖
a₁ : ‖μ‖ ≤ ‖μ‖ * ‖f m - u‖
⊢ ‖μ‖ ≤ ‖HSub.hSub (α := X) (β := X) ((T : (a : X) → X) (f m) : X) ((T : (a : X) → X) (f n) : X)‖
have a₂ : ‖μ‖ ≤ ‖f m - u‖ * ‖μ‖
Tactic: grw [← hu, norm_smul, mul_comm, ← hf_far _ u this, one_mul]
-- 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
μ : 𝕜
inst_3 : CompleteSpace X
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h₁ : ¬HasEigenvalue (↑T : X →ₗ[𝕜] X) μ
S : X →L[𝕜] X := T - HSMul.hSMul (β := X →L[𝕜] X) μ 1
K : NNReal
hK : AntilipschitzWith (α := X) (β := X) K (⇑S : (a : X) → X)
h₂ : ¬Function.Surjective (α := X) (β := X) (⇑S : (a : X) → X)
c : 𝕜
hc : 1 < ‖c‖
f : ℕ → X
hf_norm_lower : ∀ (n : ℕ), 1 ≤ ‖f n‖
hf_norm_upper : ∀ (n : ℕ), ‖f n‖ ≤ ‖c‖ + 1
hf_far : ∀ (n : ℕ), ∀ y ∈ LinearMap.range ((↑S : X →ₗ[𝕜] X) ^ (n + 1)), 1 ≤ ‖f n - y‖
hf_mem : ∀ {n m : ℕ} (h : m ≤ n), f n ∈ ((↑S : X →ₗ[𝕜] X) ^ m).range
hf_mem' :
  ∀ {n m : ℕ} (h : m ≤ n), Membership.mem (α := X) ((↑S : X →ₗ[𝕜] X) ^ (m + 1)).range ((S : (a : X) → X) (f n) : X)
m n : ℕ
hmn : m < n
u : X := μ⁻¹ • (HSub.hSub (α := X) (β := X) ((S : (a : X) → X) (f n) : X) ((S : (a : X) → X) (f m) : X) + μ • f n)
hu : μ • (f m - u) = HSub.hSub (α := X) (β := X) ((T : (a : X) → X) (f m) : X) ((T : (a : X) → X) (f n) : X)
this : u ∈ ((↑S : X →ₗ[𝕜] X) ^ (m + 1)).range
a : ‖μ‖ ≤ ‖μ • (f m - u)‖
a₁ : ‖μ‖ ≤ ‖μ‖ * ‖f m - u‖
a₂ : ‖μ‖ ≤ ‖f m - u‖ * ‖μ‖
⊢ ‖μ‖ ≤ ‖HSub.hSub (α := X) (β := X) ((T : (a : X) → X) (f m) : X) ((T : (a : X) → X) (f n) : X)‖
have a₃ : ‖μ‖ ≤ 1 * ‖μ‖
Tactic: grw [← hu, norm_smul, mul_comm, ← hf_far _ u this, one_mul]
-- 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
μ : 𝕜
inst_3 : CompleteSpace X
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h₁ : ¬HasEigenvalue (↑T : X →ₗ[𝕜] X) μ
S : X →L[𝕜] X := T - HSMul.hSMul (β := X →L[𝕜] X) μ 1
K : NNReal
hK : AntilipschitzWith (α := X) (β := X) K (⇑S : (a : X) → X)
h₂ : ¬Function.Surjective (α := X) (β := X) (⇑S : (a : X) → X)
c : 𝕜
hc : 1 < ‖c‖
f : ℕ → X
hf_norm_lower : ∀ (n : ℕ), 1 ≤ ‖f n‖
hf_norm_upper : ∀ (n : ℕ), ‖f n‖ ≤ ‖c‖ + 1
hf_far : ∀ (n : ℕ), ∀ y ∈ LinearMap.range ((↑S : X →ₗ[𝕜] X) ^ (n + 1)), 1 ≤ ‖f n - y‖
hf_mem : ∀ {n m : ℕ} (h : m ≤ n), f n ∈ ((↑S : X →ₗ[𝕜] X) ^ m).range
hf_mem' :
  ∀ {n m : ℕ} (h : m ≤ n), Membership.mem (α := X) ((↑S : X →ₗ[𝕜] X) ^ (m + 1)).range ((S : (a : X) → X) (f n) : X)
m n : ℕ
hmn : m < n
u : X := μ⁻¹ • (HSub.hSub (α := X) (β := X) ((S : (a : X) → X) (f n) : X) ((S : (a : X) → X) (f m) : X) + μ • f n)
hu : μ • (f m - u) = HSub.hSub (α := X) (β := X) ((T : (a : X) → X) (f m) : X) ((T : (a : X) → X) (f n) : X)
this : u ∈ ((↑S : X →ₗ[𝕜] X) ^ (m + 1)).range
a : ‖μ‖ ≤ ‖μ • (f m - u)‖
a₁ : ‖μ‖ ≤ ‖μ‖ * ‖f m - u‖
a₂ : ‖μ‖ ≤ ‖f m - u‖ * ‖μ‖
a₃ : ‖μ‖ ≤ 1 * ‖μ‖
⊢ ‖μ‖ ≤ ‖HSub.hSub (α := X) (β := X) ((T : (a : X) → X) (f m) : X) ((T : (a : X) → X) (f n) : X)‖
have a₄ : ‖μ‖ ≤ ‖μ‖
Tactic: grw [← hu, norm_smul, mul_comm, ← hf_far _ u this, one_mul]
-- 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
μ : 𝕜
inst_3 : CompleteSpace X
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h₁ : ¬HasEigenvalue (↑T : X →ₗ[𝕜] X) μ
S : X →L[𝕜] X := T - HSMul.hSMul (β := X →L[𝕜] X) μ 1
K : NNReal
hK : AntilipschitzWith (α := X) (β := X) K (⇑S : (a : X) → X)
h₂ : ¬Function.Surjective (α := X) (β := X) (⇑S : (a : X) → X)
c : 𝕜
hc : 1 < ‖c‖
f : ℕ → X
hf_norm_lower : ∀ (n : ℕ), 1 ≤ ‖f n‖
hf_norm_upper : ∀ (n : ℕ), ‖f n‖ ≤ ‖c‖ + 1
hf_far : ∀ (n : ℕ), ∀ y ∈ LinearMap.range ((↑S : X →ₗ[𝕜] X) ^ (n + 1)), 1 ≤ ‖f n - y‖
hf_mem : ∀ {n m : ℕ} (h : m ≤ n), f n ∈ ((↑S : X →ₗ[𝕜] X) ^ m).range
hf_mem' :
  ∀ {n m : ℕ} (h : m ≤ n), Membership.mem (α := X) ((↑S : X →ₗ[𝕜] X) ^ (m + 1)).range ((S : (a : X) → X) (f n) : X)
⊢ False
have hp : Pairwise fun (x₁ x₂ : ℕ) ↦
  ‖μ‖ ≤ ‖HSub.hSub (α := X) (β := X) ((T : (a : X) → X) (f x₁) : X) ((T : (a : X) → X) (f x₂) : X)‖
Tactic: have hp : Pairwise fun x₁ x₂ ↦ ‖μ‖ ≤ ‖T (f x₁) - T (f x₂)‖ := by
    apply Pairwise.of_lt
    · grind [Symmetric, norm_sub_rev]
    intro m n hmn
    let u : X := μ⁻¹ • (S (f n) - S (f m) + μ • f n)
    have hu : μ • (f m - u) = T (f m) - T (f n) := by
      rw [smul_sub, smul_inv_smul₀ hμ]
      simp [S]
      linear_combination (norm := module)
    have : u ∈ ((S : End 𝕜 X) ^ (m + 1)).range := by
      apply Submodule.smul_mem _ _ (Submodule.add_mem _ _ _)
      · exact Submodule.sub_mem _ (hf_mem' hmn.le) (hf_mem' le_rfl)
      · exact Submodule.smul_mem _ μ (hf_mem hmn)
    grw [← hu, norm_smul, mul_comm, ← hf_far _ u this, one_mul]
-- 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
μ : 𝕜
inst_3 : CompleteSpace X
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h₁ : ¬HasEigenvalue (↑T : X →ₗ[𝕜] X) μ
S : X →L[𝕜] X := T - HSMul.hSMul (β := X →L[𝕜] X) μ 1
K : NNReal
hK : AntilipschitzWith (α := X) (β := X) K (⇑S : (a : X) → X)
h₂ : ¬Function.Surjective (α := X) (β := X) (⇑S : (a : X) → X)
c : 𝕜
hc : 1 < ‖c‖
f : ℕ → X
hf_norm_lower : ∀ (n : ℕ), 1 ≤ ‖f n‖
hf_norm_upper : ∀ (n : ℕ), ‖f n‖ ≤ ‖c‖ + 1
hf_far : ∀ (n : ℕ), ∀ y ∈ LinearMap.range ((↑S : X →ₗ[𝕜] X) ^ (n + 1)), 1 ≤ ‖f n - y‖
hf_mem : ∀ {n m : ℕ} (h : m ≤ n), f n ∈ ((↑S : X →ₗ[𝕜] X) ^ m).range
hf_mem' :
  ∀ {n m : ℕ} (h : m ≤ n), Membership.mem (α := X) ((↑S : X →ₗ[𝕜] X) ^ (m + 1)).range ((S : (a : X) → X) (f n) : X)
hp :
  Pairwise fun (x₁ x₂ : ℕ) ↦
    ‖μ‖ ≤ ‖HSub.hSub (α := X) (β := X) ((T : (a : X) → X) (f x₁) : X) ((T : (a : X) → X) (f x₂) : X)‖
⊢ False
have obtain : ∀ (K : Set X) (hK : IsCompact K)
  (hK' : Set.image (α := X) (⇑(↑T : X →ₗ[𝕜] X) : (a : X) → X) (Metric.closedBall 0 (‖c‖ + 1)) ⊆ K), False
Tactic: obtain ⟨K, hK, hK'⟩ := hT.image_closedBall_subset_compact (‖c‖ + 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
μ : 𝕜
inst_3 : CompleteSpace X
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h₁ : ¬HasEigenvalue (↑T : X →ₗ[𝕜] X) μ
S : X →L[𝕜] X := T - HSMul.hSMul (β := X →L[𝕜] X) μ 1
K_1 : NNReal
hK_1 : AntilipschitzWith (α := X) (β := X) K_1 (⇑S : (a : X) → X)
h₂ : ¬Function.Surjective (α := X) (β := X) (⇑S : (a : X) → X)
c : 𝕜
hc : 1 < ‖c‖
f : ℕ → X
hf_norm_lower : ∀ (n : ℕ), 1 ≤ ‖f n‖
hf_norm_upper : ∀ (n : ℕ), ‖f n‖ ≤ ‖c‖ + 1
hf_far : ∀ (n : ℕ), ∀ y ∈ LinearMap.range ((↑S : X →ₗ[𝕜] X) ^ (n + 1)), 1 ≤ ‖f n - y‖
hf_mem : ∀ {n m : ℕ} (h : m ≤ n), f n ∈ ((↑S : X →ₗ[𝕜] X) ^ m).range
hf_mem' :
  ∀ {n m : ℕ} (h : m ≤ n), Membership.mem (α := X) ((↑S : X →ₗ[𝕜] X) ^ (m + 1)).range ((S : (a : X) → X) (f n) : X)
hp :
  Pairwise fun (x₁ x₂ : ℕ) ↦
    ‖μ‖ ≤ ‖HSub.hSub (α := X) (β := X) ((T : (a : X) → X) (f x₁) : X) ((T : (a : X) → X) (f x₂) : X)‖
K : Set X
hK : IsCompact K
hK' : Set.image (α := X) (⇑(↑T : X →ₗ[𝕜] X) : (a : X) → X) (Metric.closedBall 0 (‖c‖ + 1)) ⊆ K
⊢ False
have obtain : ∀ (y : X) (hyK : y ∈ K) (ψ : ℕ → ℕ) (hψ : StrictMono ψ)
  (hψy : Filter.Tendsto ((fun (n : ℕ) ↦ ((↑T : X →ₗ[𝕜] X) : (a : X) → X) (f n)) ∘ ψ) Filter.atTop (nhds y)), False
Tactic: obtain ⟨y, hyK, ψ, hψ, hψy⟩ := hK.tendsto_subseq (fun n ↦ hK' ⟨f 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
μ : 𝕜
inst_3 : CompleteSpace X
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h₁ : ¬HasEigenvalue (↑T : X →ₗ[𝕜] X) μ
S : X →L[𝕜] X := T - HSMul.hSMul (β := X →L[𝕜] X) μ 1
K_1 : NNReal
hK_1 : AntilipschitzWith (α := X) (β := X) K_1 (⇑S : (a : X) → X)
h₂ : ¬Function.Surjective (α := X) (β := X) (⇑S : (a : X) → X)
c : 𝕜
hc : 1 < ‖c‖
f : ℕ → X
hf_norm_lower : ∀ (n : ℕ), 1 ≤ ‖f n‖
hf_norm_upper : ∀ (n : ℕ), ‖f n‖ ≤ ‖c‖ + 1
hf_far : ∀ (n : ℕ), ∀ y ∈ LinearMap.range ((↑S : X →ₗ[𝕜] X) ^ (n + 1)), 1 ≤ ‖f n - y‖
hf_mem : ∀ {n m : ℕ} (h : m ≤ n), f n ∈ ((↑S : X →ₗ[𝕜] X) ^ m).range
hf_mem' :
  ∀ {n m : ℕ} (h : m ≤ n), Membership.mem (α := X) ((↑S : X →ₗ[𝕜] X) ^ (m + 1)).range ((S : (a : X) → X) (f n) : X)
hp :
  Pairwise fun (x₁ x₂ : ℕ) ↦
    ‖μ‖ ≤ ‖HSub.hSub (α := X) (β := X) ((T : (a : X) → X) (f x₁) : X) ((T : (a : X) → X) (f x₂) : X)‖
K : Set X
hK : IsCompact K
hK' : Set.image (α := X) (⇑(↑T : X →ₗ[𝕜] X) : (a : X) → X) (Metric.closedBall 0 (‖c‖ + 1)) ⊆ K
y : X
hyK : y ∈ K
ψ : ℕ → ℕ
hψ : StrictMono ψ
hψy : Filter.Tendsto ((fun (n : ℕ) ↦ ((↑T : X →ₗ[𝕜] X) : (a : X) → X) (f n)) ∘ ψ) Filter.atTop (nhds y)
⊢ False
have hψy₁ : CauchySeq.{u_2, 0} (α := X) ((fun (n : ℕ) ↦ ((↑T : X →ₗ[𝕜] X) : (a : X) → X) (f n)) ∘ ψ)
Tactic: replace hψy := hψy.cauchySeq
Cleared hypotheses: hψy
-- 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
μ : 𝕜
inst_3 : CompleteSpace X
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h₁ : ¬HasEigenvalue (↑T : X →ₗ[𝕜] X) μ
S : X →L[𝕜] X := T - HSMul.hSMul (β := X →L[𝕜] X) μ 1
K_1 : NNReal
hK_1 : AntilipschitzWith (α := X) (β := X) K_1 (⇑S : (a : X) → X)
h₂ : ¬Function.Surjective (α := X) (β := X) (⇑S : (a : X) → X)
c : 𝕜
hc : 1 < ‖c‖
f : ℕ → X
hf_norm_lower : ∀ (n : ℕ), 1 ≤ ‖f n‖
hf_norm_upper : ∀ (n : ℕ), ‖f n‖ ≤ ‖c‖ + 1
hf_far : ∀ (n : ℕ), ∀ y ∈ LinearMap.range ((↑S : X →ₗ[𝕜] X) ^ (n + 1)), 1 ≤ ‖f n - y‖
hf_mem : ∀ {n m : ℕ} (h : m ≤ n), f n ∈ ((↑S : X →ₗ[𝕜] X) ^ m).range
hf_mem' :
  ∀ {n m : ℕ} (h : m ≤ n), Membership.mem (α := X) ((↑S : X →ₗ[𝕜] X) ^ (m + 1)).range ((S : (a : X) → X) (f n) : X)
hp :
  Pairwise fun (x₁ x₂ : ℕ) ↦
    ‖μ‖ ≤ ‖HSub.hSub (α := X) (β := X) ((T : (a : X) → X) (f x₁) : X) ((T : (a : X) → X) (f x₂) : X)‖
K : Set X
hK : IsCompact K
hK' : Set.image (α := X) (⇑(↑T : X →ₗ[𝕜] X) : (a : X) → X) (Metric.closedBall 0 (‖c‖ + 1)) ⊆ K
y : X
hyK : y ∈ K
ψ : ℕ → ℕ
hψ : StrictMono ψ
hψy : CauchySeq.{u_2, 0} (α := X) ((fun (n : ℕ) ↦ ((↑T : X →ₗ[𝕜] X) : (a : X) → X) (f n)) ∘ ψ)
⊢ False
have hψy₁ : ∀ ε > 0,
  ∃ (N : ℕ),
    ∀ n ≥ N,
      dist.{u_2} (α := X) (((fun (n : ℕ) ↦ ((↑T : X →ₗ[𝕜] X) : (a : X) → X) (f n)) ∘ ψ) n)
          (((fun (n : ℕ) ↦ ((↑T : X →ₗ[𝕜] X) : (a : X) → X) (f n)) ∘ ψ) N) <
        ε
Tactic: rw [Metric.cauchySeq_iff'] at hψy
Cleared hypotheses: hψy
-- 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
μ : 𝕜
inst_3 : CompleteSpace X
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h₁ : ¬HasEigenvalue (↑T : X →ₗ[𝕜] X) μ
S : X →L[𝕜] X := T - HSMul.hSMul (β := X →L[𝕜] X) μ 1
K_1 : NNReal
hK_1 : AntilipschitzWith (α := X) (β := X) K_1 (⇑S : (a : X) → X)
h₂ : ¬Function.Surjective (α := X) (β := X) (⇑S : (a : X) → X)
c : 𝕜
hc : 1 < ‖c‖
f : ℕ → X
hf_norm_lower : ∀ (n : ℕ), 1 ≤ ‖f n‖
hf_norm_upper : ∀ (n : ℕ), ‖f n‖ ≤ ‖c‖ + 1
hf_far : ∀ (n : ℕ), ∀ y ∈ LinearMap.range ((↑S : X →ₗ[𝕜] X) ^ (n + 1)), 1 ≤ ‖f n - y‖
hf_mem : ∀ {n m : ℕ} (h : m ≤ n), f n ∈ ((↑S : X →ₗ[𝕜] X) ^ m).range
hf_mem' :
  ∀ {n m : ℕ} (h : m ≤ n), Membership.mem (α := X) ((↑S : X →ₗ[𝕜] X) ^ (m + 1)).range ((S : (a : X) → X) (f n) : X)
hp :
  Pairwise fun (x₁ x₂ : ℕ) ↦
    ‖μ‖ ≤ ‖HSub.hSub (α := X) (β := X) ((T : (a : X) → X) (f x₁) : X) ((T : (a : X) → X) (f x₂) : X)‖
K : Set X
hK : IsCompact K
hK' : Set.image (α := X) (⇑(↑T : X →ₗ[𝕜] X) : (a : X) → X) (Metric.closedBall 0 (‖c‖ + 1)) ⊆ K
y : X
hyK : y ∈ K
ψ : ℕ → ℕ
hψ : StrictMono ψ
hψy :
  ∀ ε > 0,
    ∃ (N : ℕ),
      ∀ n ≥ N,
        dist.{u_2} (α := X) (((fun (n : ℕ) ↦ ((↑T : X →ₗ[𝕜] X) : (a : X) → X) (f n)) ∘ ψ) n)
            (((fun (n : ℕ) ↦ ((↑T : X →ₗ[𝕜] X) : (a : X) → X) (f n)) ∘ ψ) N) <
          ε
⊢ False
have obtain : ∀ (N : ℕ)
  (hN :
    ∀ n ≥ N,
      dist.{u_2} (α := X) (((fun (n : ℕ) ↦ ((↑T : X →ₗ[𝕜] X) : (a : X) → X) (f n)) ∘ ψ) n)
          (((fun (n : ℕ) ↦ ((↑T : X →ₗ[𝕜] X) : (a : X) → X) (f n)) ∘ ψ) N) <
        ‖μ‖),
  False
Tactic: obtain ⟨N, hN⟩ := hψy ‖μ‖ (by positivity)
-- 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
μ : 𝕜
inst_3 : CompleteSpace X
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h₁ : ¬HasEigenvalue (↑T : X →ₗ[𝕜] X) μ
S : X →L[𝕜] X := T - HSMul.hSMul (β := X →L[𝕜] X) μ 1
K_1 : NNReal
hK_1 : AntilipschitzWith (α := X) (β := X) K_1 (⇑S : (a : X) → X)
h₂ : ¬Function.Surjective (α := X) (β := X) (⇑S : (a : X) → X)
c : 𝕜
hc : 1 < ‖c‖
f : ℕ → X
hf_norm_lower : ∀ (n : ℕ), 1 ≤ ‖f n‖
hf_norm_upper : ∀ (n : ℕ), ‖f n‖ ≤ ‖c‖ + 1
hf_far : ∀ (n : ℕ), ∀ y ∈ LinearMap.range ((↑S : X →ₗ[𝕜] X) ^ (n + 1)), 1 ≤ ‖f n - y‖
hf_mem : ∀ {n m : ℕ} (h : m ≤ n), f n ∈ ((↑S : X →ₗ[𝕜] X) ^ m).range
hf_mem' :
  ∀ {n m : ℕ} (h : m ≤ n), Membership.mem (α := X) ((↑S : X →ₗ[𝕜] X) ^ (m + 1)).range ((S : (a : X) → X) (f n) : X)
hp :
  Pairwise fun (x₁ x₂ : ℕ) ↦
    ‖μ‖ ≤ ‖HSub.hSub (α := X) (β := X) ((T : (a : X) → X) (f x₁) : X) ((T : (a : X) → X) (f x₂) : X)‖
K : Set X
hK : IsCompact K
hK' : Set.image (α := X) (⇑(↑T : X →ₗ[𝕜] X) : (a : X) → X) (Metric.closedBall 0 (‖c‖ + 1)) ⊆ K
y : X
hyK : y ∈ K
ψ : ℕ → ℕ
hψ : StrictMono ψ
hψy :
  ∀ ε > 0,
    ∃ (N : ℕ),
      ∀ n ≥ N,
        dist.{u_2} (α := X) (((fun (n : ℕ) ↦ ((↑T : X →ₗ[𝕜] X) : (a : X) → X) (f n)) ∘ ψ) n)
            (((fun (n : ℕ) ↦ ((↑T : X →ₗ[𝕜] X) : (a : X) → X) (f n)) ∘ ψ) N) <
          ε
N : ℕ
hN :
  ∀ n ≥ N,
    dist.{u_2} (α := X) (((fun (n : ℕ) ↦ ((↑T : X →ₗ[𝕜] X) : (a : X) → X) (f n)) ∘ ψ) n)
        (((fun (n : ℕ) ↦ ((↑T : X →ₗ[𝕜] X) : (a : X) → X) (f n)) ∘ ψ) N) <
      ‖μ‖
⊢ False
have this : ‖HSub.hSub (α := X) (β := X) ((T : (a : X) → X) (f (ψ (N + 1))) : X) ((T : (a : X) → X) (f (ψ N)) : X)‖ < ‖μ‖
Tactic: have : ‖T (f (ψ (N + 1))) - T (f (ψ N))‖ < ‖μ‖ := by simpa [dist_eq_norm_sub] using hN (N + 1)