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
n m : ℕ
h : m ≤ n
⊢ Membership.mem (α := X) (Submodule.map (↑S : X →ₗ[𝕜] X) (LinearMap.range ((↑S : X →ₗ[𝕜] X) ^ m)))
    ((S : (a : X) → X) (f n) : X)

Tactic:
⟨f n, hf_mem h, rfl⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image, rfl
-- 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
⊢ Membership.mem (α := X) (Submodule.map (↑S : X →ₗ[𝕜] X) (LinearMap.range ((↑S : X →ₗ[𝕜] X) ^ m)))
    ((S : (a : X) → X) (f n) : X)

Tactic:
exact ⟨f n, hf_mem h, rfl⟩
-- 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), Membership.mem (α := X) ((↑S : X →ₗ[𝕜] X) ^ (m + 1)).range ((S : (a : X) → X) (f n) : X)

Tactic:
have hf_mem' {n m : ℕ} (h : m ≤ n) : S (f n) ∈ ((S : End 𝕜 X) ^ (m + 1)).range := by
    rw [iterate_succ', LinearMap.range_comp]
    exact ⟨f n, hf_mem h, rfl⟩
-- 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 :
  Symmetric fun (x₁ x₂ : ℕ) ↦
    ‖μ‖ ≤ ‖HSub.hSub (α := X) (β := X) ((T : (a : X) → X) (f x₁) : X) ((T : (a : X) → X) (f x₂) : X)‖
a : ∀ ⦃a b : ℕ⦄, a < b → ‖μ‖ ≤ ‖HSub.hSub (α := X) (β := X) ((T : (a : X) → X) (f a) : X) ((T : (a : X) → X) (f b) : X)‖
⊢ Pairwise fun (x₁ x₂ : ℕ) ↦
    ‖μ‖ ≤ ‖HSub.hSub (α := X) (β := X) ((T : (a : X) → X) (f x₁) : X) ((T : (a : X) → X) (f x₂) : X)‖

Tactic:
apply Pairwise.of_lt

Premises used: Pairwise.of_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
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)
⊢ Symmetric fun (x₁ x₂ : ℕ) ↦
    ‖μ‖ ≤ ‖HSub.hSub (α := X) (β := X) ((T : (a : X) → X) (f x₁) : X) ((T : (a : X) → X) (f x₂) : X)‖

Tactic:
grind [Symmetric, norm_sub_rev]

Premises used: Symmetric, norm_sub_rev
-- 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)
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)
rw :
  μ • f m - (HSub.hSub (α := X) (β := X) ((S : (a : X) → X) (f n) : X) ((S : (a : X) → X) (f m) : X) + μ • f n) =
    HSub.hSub (α := X) (β := X) ((T : (a : X) → X) (f m) : X) ((T : (a : X) → X) (f n) : X)
⊢ μ • (f m - u) = HSub.hSub (α := X) (β := X) ((T : (a : X) → X) (f m) : X) ((T : (a : X) → X) (f n) : X)

Tactic:
rw [smul_sub, smul_inv_smul₀ hμ]

Premises used: smul_inv_smul₀, smul_sub
-- 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)
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)
simp :
  μ • f m -
      (HSub.hSub (α := X) ((T : (a : X) → X) (f n) : X) (μ • f n) -
          HSub.hSub (α := X) ((T : (a : X) → X) (f m) : X) (μ • f m) +
        μ • f n) =
    HSub.hSub (α := X) (β := X) ((T : (a : X) → X) (f m) : X) ((T : (a : X) → X) (f n) : X)
⊢ μ • f m - (HSub.hSub (α := X) (β := X) ((S : (a : X) → X) (f n) : X) ((S : (a : X) → X) (f m) : X) + μ • f n) =
    HSub.hSub (α := X) (β := X) ((T : (a : X) → X) (f m) : X) ((T : (a : X) → X) (f n) : 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) μ
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)
⊢ μ • f m -
          (HSub.hSub (α := X) ((T : (a : X) → X) (f n) : X) (μ • f n) -
              HSub.hSub (α := X) ((T : (a : X) → X) (f m) : X) (μ • f m) +
            μ • f n) +
        0 -
      (HSub.hSub (α := X) (β := X) ((T : (a : X) → X) (f m) : X) ((T : (a : X) → X) (f n) : X) + 0) =
    0

Tactic:
module
-- 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)
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)
a :
  μ • f m -
          (HSub.hSub (α := X) ((T : (a : X) → X) (f n) : X) (μ • f n) -
              HSub.hSub (α := X) ((T : (a : X) → X) (f m) : X) (μ • f m) +
            μ • f n) +
        0 -
      (HSub.hSub (α := X) (β := X) ((T : (a : X) → X) (f m) : X) ((T : (a : X) → X) (f n) : X) + 0) =
    0
⊢ μ • f m -
      (HSub.hSub (α := X) ((T : (a : X) → X) (f n) : X) (μ • f n) -
          HSub.hSub (α := X) ((T : (a : X) → X) (f m) : X) (μ • f m) +
        μ • f n) =
    HSub.hSub (α := X) (β := X) ((T : (a : X) → X) (f m) : X) ((T : (a : X) → X) (f n) : X)

Tactic:
linear_combination (norm := module)
-- 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)
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)
⊢ μ • (f m - u) = HSub.hSub (α := X) (β := X) ((T : (a : X) → X) (f m) : X) ((T : (a : X) → X) (f n) : X)

Tactic:
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)
-- 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)
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
apply₁ : μ • f n ∈ ((↑S : X →ₗ[𝕜] X) ^ (m + 1)).range
⊢ u ∈ ((↑S : X →ₗ[𝕜] X) ^ (m + 1)).range

Tactic:
apply Submodule.smul_mem _ _ (Submodule.add_mem _ _ _)

Premises used: Submodule.smul_mem, Submodule.add_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
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) ((S : (a : X) → X) (f n) : X) ((S : (a : X) → X) (f m) : X) ∈
    ((↑S : X →ₗ[𝕜] X) ^ (m + 1)).range

Tactic:
Submodule.sub_mem _ (hf_mem' hmn.le) (hf_mem' le_rfl)

Premises used: le_rfl, Set.Mem, LT.lt.le, Submodule.sub_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
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) ((S : (a : X) → X) (f n) : X) ((S : (a : X) → X) (f m) : X) ∈
    ((↑S : X →ₗ[𝕜] X) ^ (m + 1)).range

Tactic:
exact Submodule.sub_mem _ (hf_mem' hmn.le) (hf_mem' le_rfl)

Premises used: le_rfl, LT.lt.le, Submodule.sub_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
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)
⊢ μ • f n ∈ ((↑S : X →ₗ[𝕜] X) ^ (m + 1)).range

Tactic:
Submodule.smul_mem _ μ (hf_mem hmn)

Premises used: Set.Mem, Submodule.smul_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
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)
⊢ μ • f n ∈ ((↑S : X →ₗ[𝕜] X) ^ (m + 1)).range

Tactic:
exact Submodule.smul_mem _ μ (hf_mem hmn)

Premises used: Submodule.smul_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
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

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)
-- 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)
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 * ‖μ‖
a₄ a₅ : ‖μ‖ ≤ ‖μ‖
⊢ ‖μ‖ ≤ ‖HSub.hSub (α := X) (β := X) ((T : (a : X) → X) (f m) : X) ((T : (a : X) → X) (f n) : X)‖

Tactic:
grw [← hu, norm_smul, mul_comm, ← hf_far _ u this, one_mul]

Premises used: norm_smul, mul_comm, one_mul