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
μ : 𝕜
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)
⊢ 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]
-- 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
μ : 𝕜
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)‖
obtain :
  ∀ (K : Set X) (hK : IsCompact K)
    (hK' : Set.image (α := X) (⇑(↑T : X →ₗ[𝕜] X) : (a : X) → X) (Metric.closedBall 0 (‖c‖ + 1)) ⊆ K), False
⊢ False

Tactic:
obtain ⟨K, hK, hK'⟩ := hT.image_closedBall_subset_compact (‖c‖ + 1)

Premises used: Norm.norm, HAdd.hAdd, IsCompactOperator.image_closedBall_subset_compact, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative
Goal:
𝕜 : Type u_1
X : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
T : X →L[𝕜] X
μ : 𝕜
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
n : ℕ
⊢ Membership.mem (γ := Set X) (Metric.closedBall 0 (‖c‖ + 1)) (f n)

Tactic:
simp [*]
-- Module: Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative
Goal:
𝕜 : Type u_1
X : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
T : X →L[𝕜] X
μ : 𝕜
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
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
⊢ False

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

Premises used: And.intro, Exists.intro, rfl, IsCompact.tendsto_subseq
-- Module: Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative
Goal:
𝕜 : Type u_1
X : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
T : X →L[𝕜] X
μ : 𝕜
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)
⊢ CauchySeq.{u_2, 0} (α := X) ((fun (n : ℕ) ↦ ((↑T : X →ₗ[𝕜] X) : (a : X) → X) (f n)) ∘ ψ)

Tactic:
replace hψy := hψy.cauchySeq
-- 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
μ : 𝕜
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)) ∘ ψ)
⊢ ∀ ε > 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

Premises used: Metric.cauchySeq_iff'
-- 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
μ : 𝕜
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) <
          ε
⊢ ‖μ‖ > 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
μ : 𝕜
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) <
          ε
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
⊢ False

Tactic:
obtain ⟨N, hN⟩ := hψy ‖μ‖ (by positivity)

Premises used: Norm.norm
-- 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
μ : 𝕜
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) <
      ‖μ‖
⊢ ‖HSub.hSub (α := X) (β := X) ((T : (a : X) → X) (f (ψ (N + 1))) : X) ((T : (a : X) → X) (f (ψ N)) : X)‖ < ‖μ‖

Tactic:
simpa [dist_eq_norm_sub] using hN (N + 1)

Premises used: dist_eq_norm_sub, 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
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) <
      ‖μ‖
⊢ ‖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)
-- 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
μ : 𝕜
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) <
      ‖μ‖
this : ‖HSub.hSub (α := X) (β := X) ((T : (a : X) → X) (f (ψ (N + 1))) : X) ((T : (a : X) → X) (f (ψ N)) : X)‖ < ‖μ‖
⊢ False

Tactic:
this.not_ge (hp ?_)

Premises used: LT.lt.not_ge
-- 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
μ : 𝕜
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) <
      ‖μ‖
this : ‖HSub.hSub (α := X) (β := X) ((T : (a : X) → X) (f (ψ (N + 1))) : X) ((T : (a : X) → X) (f (ψ N)) : X)‖ < ‖μ‖
refine : ψ (N + 1) ≠ ψ N
⊢ False

Tactic:
refine this.not_ge (hp ?_)

Premises used: LT.lt.not_ge
-- 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
μ : 𝕜
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) <
      ‖μ‖
this : ‖HSub.hSub (α := X) (β := X) ((T : (a : X) → X) (f (ψ (N + 1))) : X) ((T : (a : X) → X) (f (ψ N)) : X)‖ < ‖μ‖
⊢ ψ (N + 1) ≠ ψ N

Tactic:
simp [hψ.injective.eq_iff]

Premises used: Function.Injective.eq_iff, StrictMono.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
T : X →L[𝕜] X
μ : 𝕜
inst_3 : CompleteSpace X
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
mp : HasEigenvalue (↑T : X →ₗ[𝕜] X) μ → μ ∈ spectrum 𝕜 T
mpr : μ ∈ spectrum 𝕜 T → HasEigenvalue (↑T : X →ₗ[𝕜] X) μ
⊢ HasEigenvalue (↑T : X →ₗ[𝕜] X) μ ↔ μ ∈ spectrum 𝕜 T

Tactic:
constructor
-- 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
μ : 𝕜
inst_3 : CompleteSpace X
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
hμ' : HasEigenvalue (↑T : X →ₗ[𝕜] X) μ
mp : μ ∈ spectrum 𝕜 (↑T : X →ₗ[𝕜] X)
⊢ μ ∈ spectrum 𝕜 T

Tactic:
rw [ContinuousLinearMap.spectrum_eq]

Premises used: ContinuousLinearMap.spectrum_eq
-- 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
μ : 𝕜
inst_3 : CompleteSpace X
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
hμ' : HasEigenvalue (↑T : X →ₗ[𝕜] X) μ
⊢ μ ∈ spectrum 𝕜 (↑T : X →ₗ[𝕜] X)

Tactic:
hμ'.mem_spectrum

Premises used: Module.End.HasEigenvalue.mem_spectrum, Set.Mem
-- 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
μ : 𝕜
inst_3 : CompleteSpace X
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
hμ' : HasEigenvalue (↑T : X →ₗ[𝕜] X) μ
⊢ μ ∈ spectrum 𝕜 (↑T : X →ₗ[𝕜] X)

Tactic:
exact hμ'.mem_spectrum

Premises used: Module.End.HasEigenvalue.mem_spectrum
-- 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
μ : 𝕜
inst_3 : CompleteSpace X
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
⊢ μ ∈ spectrum 𝕜 T → HasEigenvalue (↑T : X →ₗ[𝕜] X) μ

Tactic:
(hasEigenvalue_or_mem_resolventSet hT hμ).resolve_right

Premises used: spectrum, Set.Mem, setOf, IsCompactOperator.hasEigenvalue_or_mem_resolventSet, Or.resolve_right, Not