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
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))
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‖
⊢ ∃ 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₂

Premises used: riesz_lemma_of_norm_lt
-- Module: Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative
Goal:
𝕜 : Type u_1
X : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
S : End 𝕜 X
hS_not_surj : ¬Function.Surjective (α := X) (β := X) (⇑S : (a : X) → X)
hS_anti : Topology.IsClosedEmbedding (X := X) (Y := X) (⇑S : (a : X) → X)
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
V : (n : ℕ) → Submodule 𝕜 X := fun (n : ℕ) ↦ (LinearMap.iterateRange S : (a : ℕ) → (Submodule 𝕜 X)ᵒᵈ) n
hV_succ : ∀ (n : ℕ), V (n + 1) = Submodule.map S (V n)
hV_closed : ∀ (n : ℕ), IsClosed (↑(V n) : Set X)
n : ℕ
h₁ : IsClosed (↑(Submodule.comap (V n).subtype (V (n + 1))) : Set ↥(V n))
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‖
⊢ ∀ (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

Premises used: AddSubgroupClass.coe_sub, Submodule.subtype_apply, Submodule.mem_comap, Subtype.forall, AddSubgroupClass.coe_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
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 : ‖x‖ ≤ R
hxy : ∀ (a : X) (b : a ∈ V n), a ∈ V (n + 1) → 1 ≤ ‖x - a‖
⊢ 1 ≤ ‖x‖

Tactic:
simpa using hxy 0

Premises used: OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative
Goal:
𝕜 : Type u_1
X : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
S : End 𝕜 X
hS_not_surj : ¬Function.Surjective (α := X) (β := X) (⇑S : (a : X) → X)
hS_anti : Topology.IsClosedEmbedding (X := X) (Y := X) (⇑S : (a : X) → X)
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
V : (n : ℕ) → Submodule 𝕜 X := fun (n : ℕ) ↦ (LinearMap.iterateRange S : (a : ℕ) → (Submodule 𝕜 X)ᵒᵈ) n
hV_succ : ∀ (n : ℕ), V (n + 1) = Submodule.map S (V n)
hV_closed : ∀ (n : ℕ), IsClosed (↑(V n) : Set X)
n : ℕ
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 : ‖x‖ ≤ R
hxy : ∀ (a : X) (b : a ∈ V n), a ∈ V (n + 1) → 1 ≤ ‖x - a‖
y : X
hy : y ∈ V (n + 1)
⊢ n ≤ n + 1

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
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 : ‖x‖ ≤ R
hxy : ∀ (a : X) (b : a ∈ V n), a ∈ V (n + 1) → 1 ≤ ‖x - a‖
⊢ ∃ x ∈ V n, 1 ≤ ‖x‖ ∧ ‖x‖ ≤ R ∧ ∀ y ∈ V (n + 1), 1 ≤ ‖x - y‖

Tactic:
exact ⟨x, hx, by simpa using hxy 0, hxn,
      fun y hy ↦ hxy y (S.iterateRange.monotone (by simp) hy) hy⟩
-- Module: Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative
Goal:
𝕜 : Type u_1
X : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
S : End 𝕜 X
hS_not_surj : ¬Function.Surjective (α := X) (β := X) (⇑S : (a : X) → X)
hS_anti : Topology.IsClosedEmbedding (X := X) (Y := X) (⇑S : (a : X) → X)
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
V : (n : ℕ) → Submodule 𝕜 X := fun (n : ℕ) ↦ (LinearMap.iterateRange S : (a : ℕ) → (Submodule 𝕜 X)ᵒᵈ) n
hV_succ : ∀ (n : ℕ), V (n + 1) = Submodule.map S (V n)
hV_closed : ∀ (n : ℕ), IsClosed (↑(V n) : Set X)
⊢ ∀ (n : ℕ), ∃ x ∈ V n, 1 ≤ ‖x‖ ∧ ‖x‖ ≤ R ∧ ∀ y ∈ V (n + 1), 1 ≤ ‖x - y‖

Tactic:
have x (n : ℕ) : ∃ x ∈ V n, 1 ≤ ‖x‖ ∧ ‖x‖ ≤ R ∧ ∀ y ∈ V (n + 1), 1 ≤ ‖x - y‖ := by
    have h₁ : IsClosed ((V (n + 1)).comap (V n).subtype : Set (V n)) := by
      simpa using (hV_closed (n + 1)).preimage_val
    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
    obtain ⟨⟨x, hx⟩, hxn, hxy⟩ := riesz_lemma_of_norm_lt hc hR h₁ h₂
    simp only [Submodule.mem_comap, Submodule.subtype_apply, AddSubgroupClass.coe_norm,
      AddSubgroupClass.coe_sub, Subtype.forall] at hxn hxy
    exact ⟨x, hx, by simpa using hxy 0, hxn,
      fun y hy ↦ hxy y (S.iterateRange.monotone (by simp) hy) hy⟩
-- Module: Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative
Goal:
𝕜 : Type u_1
X : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
S : End 𝕜 X
hS_not_surj : ¬Function.Surjective (α := X) (β := X) (⇑S : (a : X) → X)
hS_anti : Topology.IsClosedEmbedding (X := X) (Y := X) (⇑S : (a : X) → X)
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
V : (n : ℕ) → Submodule 𝕜 X := fun (n : ℕ) ↦ (LinearMap.iterateRange S : (a : ℕ) → (Submodule 𝕜 X)ᵒᵈ) n
hV_succ : ∀ (n : ℕ), V (n + 1) = Submodule.map S (V n)
hV_closed : ∀ (n : ℕ), IsClosed (↑(V n) : Set X)
x : ∀ (n : ℕ), ∃ x ∈ V n, 1 ≤ ‖x‖ ∧ ‖x‖ ≤ R ∧ ∀ y ∈ V (n + 1), 1 ≤ ‖x - y‖
choose :
  ∀ (x : (n : ℕ) → X) (hxv : ∀ (n : ℕ), x n ∈ V n) (hxn : ∀ (n : ℕ), 1 ≤ ‖x n‖) (hxn' : ∀ (n : ℕ), ‖x n‖ ≤ R)
    (hxy : ∀ (n : ℕ), ∀ y ∈ V (n + 1), 1 ≤ ‖x n - y‖),
    ∃ (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‖
⊢ ∃ (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‖

Tactic:
choose x hxv hxn hxn' hxy using x
-- Module: Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative
Goal:
𝕜 : Type u_1
X : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
S : End 𝕜 X
hS_not_surj : ¬Function.Surjective (α := X) (β := X) (⇑S : (a : X) → X)
hS_anti : Topology.IsClosedEmbedding (X := X) (Y := X) (⇑S : (a : X) → X)
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
V : (n : ℕ) → Submodule 𝕜 X := fun (n : ℕ) ↦ (LinearMap.iterateRange S : (a : ℕ) → (Submodule 𝕜 X)ᵒᵈ) n
hV_succ : ∀ (n : ℕ), V (n + 1) = Submodule.map S (V n)
hV_closed : ∀ (n : ℕ), IsClosed (↑(V n) : Set X)
x : (n : ℕ) → X
hxv : ∀ (n : ℕ), x n ∈ V n
hxn : ∀ (n : ℕ), 1 ≤ ‖x n‖
hxn' : ∀ (n : ℕ), ‖x n‖ ≤ R
hxy : ∀ (n : ℕ), ∀ y ∈ V (n + 1), 1 ≤ ‖x n - y‖
⊢ ∃ (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‖

Tactic:
⟨x, hxn, hxn', hxv, hxy⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative
Goal:
𝕜 : Type u_1
X : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
S : End 𝕜 X
hS_not_surj : ¬Function.Surjective (α := X) (β := X) (⇑S : (a : X) → X)
hS_anti : Topology.IsClosedEmbedding (X := X) (Y := X) (⇑S : (a : X) → X)
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
V : (n : ℕ) → Submodule 𝕜 X := fun (n : ℕ) ↦ (LinearMap.iterateRange S : (a : ℕ) → (Submodule 𝕜 X)ᵒᵈ) n
hV_succ : ∀ (n : ℕ), V (n + 1) = Submodule.map S (V n)
hV_closed : ∀ (n : ℕ), IsClosed (↑(V n) : Set X)
x : (n : ℕ) → X
hxv : ∀ (n : ℕ), x n ∈ V n
hxn : ∀ (n : ℕ), 1 ≤ ‖x n‖
hxn' : ∀ (n : ℕ), ‖x n‖ ≤ R
hxy : ∀ (n : ℕ), ∀ y ∈ V (n + 1), 1 ≤ ‖x n - y‖
⊢ ∃ (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‖

Tactic:
exact ⟨x, hxn, hxn', hxv, hxy⟩
-- 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
by_contra! : ∀ (this : ¬HasEigenvalue (↑T : X →ₗ[𝕜] X) μ ∧ μ ∉ resolventSet 𝕜 T), False
⊢ HasEigenvalue (↑T : X →ₗ[𝕜] X) μ ∨ μ ∈ resolventSet 𝕜 T

Tactic:
by_contra!
-- 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
this : ¬HasEigenvalue (↑T : X →ₗ[𝕜] X) μ ∧ μ ∉ resolventSet 𝕜 T
⊢ ¬HasEigenvalue (↑T : X →ₗ[𝕜] X) μ

Tactic:
obtain ⟨h₁, h₂⟩ := this
-- 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
this : ¬HasEigenvalue (↑T : X →ₗ[𝕜] X) μ ∧ μ ∉ resolventSet 𝕜 T
h₁ : ¬HasEigenvalue (↑T : X →ₗ[𝕜] X) μ
⊢ μ ∉ resolventSet 𝕜 T

Tactic:
obtain ⟨h₁, h₂⟩ := this
-- 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) μ
h₂ : μ ∉ resolventSet 𝕜 T
S : X →L[𝕜] X := T - HSMul.hSMul (β := X →L[𝕜] X) μ 1
obtain : ∀ (K : NNReal) (hK : AntilipschitzWith (α := X) (β := X) K (⇑S : (a : X) → X)), False
⊢ False

Tactic:
obtain ⟨K, hK : AntilipschitzWith K S⟩ := antilipschitz_of_not_hasEigenvalue hT hμ h₁

Premises used: IsCompactOperator.antilipschitz_of_not_hasEigenvalue
-- 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) μ
h₂ : μ ∉ resolventSet 𝕜 T
S : X →L[𝕜] X := T - HSMul.hSMul (β := X →L[𝕜] X) μ 1
K : NNReal
hK : AntilipschitzWith (α := X) (β := X) K (⇑S : (a : X) → X)
rw :
  ∀
    (h₂ :
      ¬Function.Bijective (α := X) (β := X)
          (⇑(-HSub.hSub (α := X →L[𝕜] X) ((algebraMap 𝕜 (X →L[𝕜] X) : (a : 𝕜) → X →L[𝕜] X) μ : X →L[𝕜] X) T) :
            (a : X) → X)),
    let S := T - HSMul.hSMul (β := X →L[𝕜] X) μ 1;
    ∀ (K : NNReal) (hK : AntilipschitzWith (α := X) (β := X) K (⇑S : (a : X) → X)),
      ¬Function.Bijective (α := X) (β := X) (⇑S : (a : X) → X)
⊢ ¬Function.Bijective (α := X) (β := X) (⇑S : (a : X) → X)

Tactic:
rw [spectrum.mem_resolventSet_iff, ← IsUnit.neg_iff,
      ContinuousLinearMap.isUnit_iff_bijective] at h₂

Premises used: IsUnit.neg_iff, spectrum.mem_resolventSet_iff, ContinuousLinearMap.isUnit_iff_bijective
-- 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) μ
h₂ :
  ¬Function.Bijective (α := X) (β := X)
      (⇑(-HSub.hSub (α := X →L[𝕜] X) ((algebraMap 𝕜 (X →L[𝕜] X) : (a : 𝕜) → X →L[𝕜] X) μ : X →L[𝕜] X) T) : (a : X) → X)
S : X →L[𝕜] X := T - HSMul.hSMul (β := X →L[𝕜] X) μ 1
K : NNReal
hK : AntilipschitzWith (α := X) (β := X) K (⇑S : (a : X) → X)
⊢ ¬Function.Bijective (α := X) (β := X)
      (⇑(-HSub.hSub (α := X →L[𝕜] X) ((algebraMap 𝕜 (X →L[𝕜] X) : (a : 𝕜) → X →L[𝕜] X) μ : X →L[𝕜] X) T) : (a : X) → X)

Tactic:
h₂
-- 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) μ
h₂ :
  ¬Function.Bijective (α := X) (β := X)
      (⇑(-HSub.hSub (α := X →L[𝕜] X) ((algebraMap 𝕜 (X →L[𝕜] X) : (a : 𝕜) → X →L[𝕜] X) μ : X →L[𝕜] X) T) : (a : 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 : S = -HSub.hSub (α := X →L[𝕜] X) ((algebraMap 𝕜 (X →L[𝕜] X) : (a : 𝕜) → X →L[𝕜] X) μ : X →L[𝕜] X) T
⊢ ¬Function.Bijective (α := X) (β := X) (⇑S : (a : X) → X)

Tactic:
convert! h₂
-- 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) μ
h₂ :
  ¬Function.Bijective (α := X) (β := X)
      (⇑(-HSub.hSub (α := X →L[𝕜] X) ((algebraMap 𝕜 (X →L[𝕜] X) : (a : 𝕜) → X →L[𝕜] X) μ : X →L[𝕜] X) T) : (a : 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 :
  ∀ (x : X),
    Eq (α := X) ((S : (a : X) → X) x : X)
      ((-HSub.hSub (α := X →L[𝕜] X) ((algebraMap 𝕜 (X →L[𝕜] X) : (a : 𝕜) → X →L[𝕜] X) μ : X →L[𝕜] X) T : (a : X) → X)
          x :
        X)
⊢ S = -HSub.hSub (α := X →L[𝕜] X) ((algebraMap 𝕜 (X →L[𝕜] X) : (a : 𝕜) → X →L[𝕜] X) μ : X →L[𝕜] X) T

Tactic:
ext x
-- 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) μ
h₂ :
  ¬Function.Bijective (α := X) (β := X)
      (⇑(-HSub.hSub (α := X →L[𝕜] X) ((algebraMap 𝕜 (X →L[𝕜] X) : (a : 𝕜) → X →L[𝕜] X) μ : X →L[𝕜] X) T) : (a : X) → X)
S : X →L[𝕜] X := T - HSMul.hSMul (β := X →L[𝕜] X) μ 1
K : NNReal
hK : AntilipschitzWith (α := X) (β := X) K (⇑S : (a : X) → X)
x : X
⊢ Eq (α := X) ((S : (a : X) → X) x : X)
    ((-HSub.hSub (α := X →L[𝕜] X) ((algebraMap 𝕜 (X →L[𝕜] X) : (a : 𝕜) → X →L[𝕜] X) μ : X →L[𝕜] X) T : (a : X) → X) x :
      X)

Tactic:
simp [S]
-- 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) μ
h₂ : μ ∉ resolventSet 𝕜 T
S : X →L[𝕜] X := T - HSMul.hSMul (β := X →L[𝕜] X) μ 1
K : NNReal
hK : AntilipschitzWith (α := X) (β := X) K (⇑S : (a : X) → X)
⊢ ¬Function.Bijective (α := X) (β := X) (⇑S : (a : X) → X)

Tactic:
replace h₂ : ¬ (S : X → X).Bijective := by
    rw [spectrum.mem_resolventSet_iff, ← IsUnit.neg_iff,
      ContinuousLinearMap.isUnit_iff_bijective] at h₂
    convert! h₂
    ext x
    simp [S]
-- 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.Bijective (α := X) (β := X) (⇑S : (a : X) → X)
⊢ ¬Function.Surjective (α := X) (β := X) (⇑S : (a : X) → X)

Tactic:
grind [Function.Bijective, hK.injective]

Premises used: AntilipschitzWith.injective, Function.Bijective
-- 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.Bijective (α := X) (β := X) (⇑S : (a : X) → X)
⊢ ¬Function.Surjective (α := X) (β := X) (⇑S : (a : X) → X)

Tactic:
replace h₂ : ¬ (S : X → X).Surjective := by grind [Function.Bijective, hK.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
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)
obtain : ∀ (c : 𝕜) (hc : 1 < ‖c‖), False
⊢ False

Tactic:
obtain ⟨c, hc⟩ := NormedField.exists_one_lt_norm 𝕜

Premises used: NormedField.exists_one_lt_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 : NNReal
hK : AntilipschitzWith (α := X) (β := X) K (⇑S : (a : X) → X)
h₂ : ¬Function.Surjective (α := X) (β := X) (⇑S : (a : X) → X)
c : 𝕜
hc : 1 < ‖c‖
⊢ ‖c‖ < ‖c‖ + 1

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 : NNReal
hK : AntilipschitzWith (α := X) (β := X) K (⇑S : (a : X) → X)
h₂ : ¬Function.Surjective (α := X) (β := X) (⇑S : (a : X) → X)
c : 𝕜
hc : 1 < ‖c‖
obtain :
  ∀ (f : ℕ → X) (hf_norm_lower : ∀ (n : ℕ), 1 ≤ ‖f n‖) (hf_norm_upper : ∀ (n : ℕ), ‖f n‖ ≤ ‖c‖ + 1)
    (hf_mem : ∀ (n : ℕ), f n ∈ LinearMap.range ((↑S : X →ₗ[𝕜] X) ^ n))
    (hf_far : ∀ (n : ℕ), ∀ y ∈ LinearMap.range ((↑S : X →ₗ[𝕜] X) ^ (n + 1)), 1 ≤ ‖f n - y‖), False
⊢ False

Tactic:
obtain ⟨f, hf_norm_lower, hf_norm_upper, hf_mem, hf_far⟩ := exists_seq h₂
    (hK.isClosedEmbedding S.uniformContinuous) hc (R := ‖c‖ + 1) (by simp)

Premises used: ContinuousLinearMap.uniformContinuous, _private.0.IsCompactOperator.exists_seq, AntilipschitzWith.isClosedEmbedding
-- 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_mem : ∀ (n : ℕ), f n ∈ LinearMap.range ((↑S : X →ₗ[𝕜] X) ^ n)
hf_far : ∀ (n : ℕ), ∀ y ∈ LinearMap.range ((↑S : X →ₗ[𝕜] X) ^ (n + 1)), 1 ≤ ‖f n - y‖
n m : ℕ
h : m ≤ n
⊢ m ≤ n

Tactic:
lia
-- 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_mem : ∀ (n : ℕ), f n ∈ LinearMap.range ((↑S : X →ₗ[𝕜] X) ^ n)
hf_far : ∀ (n : ℕ), ∀ y ∈ LinearMap.range ((↑S : X →ₗ[𝕜] X) ^ (n + 1)), 1 ≤ ‖f n - y‖
⊢ ∀ {n m : ℕ} (h : m ≤ n), f n ∈ ((↑S : X →ₗ[𝕜] X) ^ m).range

Tactic:
replace hf_mem {n m : ℕ} (h : m ≤ n) : f n ∈ ((S : End 𝕜 X) ^ m).range :=
    (S : End 𝕜 X).iterateRange.monotone (by lia) (hf_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) μ
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
n m : ℕ
h : m ≤ n
rw :
  Membership.mem (α := X) (Submodule.map (↑S : X →ₗ[𝕜] X) (LinearMap.range ((↑S : X →ₗ[𝕜] X) ^ m)))
    ((S : (a : X) → X) (f n) : X)
⊢ Membership.mem (α := X) ((↑S : X →ₗ[𝕜] X) ^ (m + 1)).range ((S : (a : X) → X) (f n) : X)

Tactic:
rw [iterate_succ', LinearMap.range_comp]

Premises used: Module.End.iterate_succ', LinearMap.range_comp