awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
⊢ ∃ (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‖
have 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⟩
-- 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
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‖
⊢ ∃ (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‖
have 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‖
Tactic: choose x hxv hxn hxn' hxy using x
Cleared hypotheses: x
-- 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
⊢ HasEigenvalue (↑T : X →ₗ[𝕜] X) μ ∨ μ ∈ resolventSet 𝕜 T
have by_contra! : ∀ (this : ¬HasEigenvalue (↑T : X →ₗ[𝕜] X) μ ∧ μ ∉ resolventSet 𝕜 T), False
Tactic: by_contra!
-- 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
this : ¬HasEigenvalue (↑T : X →ₗ[𝕜] X) μ ∧ μ ∉ resolventSet 𝕜 T
⊢ False
have h₁ : ¬HasEigenvalue (↑T : X →ₗ[𝕜] X) μ
Tactic: obtain ⟨h₁, h₂⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative (hypothesis)
Goal:
𝕜 : Type u_1
X : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
T : X →L[𝕜] X
μ : 𝕜
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) μ
⊢ False
have h₂ : μ ∉ resolventSet 𝕜 T
Tactic: obtain ⟨h₁, h₂⟩ := this
Cleared hypotheses: this
-- 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) μ
h₂ : μ ∉ resolventSet 𝕜 T
S : X →L[𝕜] X := T - HSMul.hSMul (β := X →L[𝕜] X) μ 1
⊢ False
have obtain : ∀ (K : NNReal) (hK : AntilipschitzWith (α := X) (β := X) K (⇑S : (a : X) → X)), False
Tactic: obtain ⟨K, hK : AntilipschitzWith K S⟩ := antilipschitz_of_not_hasEigenvalue hT hμ h₁
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative (goal)
Goal:
𝕜 : Type u_1
X : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
T : X →L[𝕜] X
μ : 𝕜
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)
have 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)
Tactic: rw [spectrum.mem_resolventSet_iff, ← IsUnit.neg_iff,
      ContinuousLinearMap.isUnit_iff_bijective] at h₂
Cleared hypotheses: h₂, S, K, hK
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative (goal)
Goal:
𝕜 : Type u_1
X : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
T : X →L[𝕜] X
μ : 𝕜
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) (⇑S : (a : X) → X)
have h : S = -HSub.hSub (α := X →L[𝕜] X) ((algebraMap 𝕜 (X →L[𝕜] X) : (a : 𝕜) → X →L[𝕜] X) μ : X →L[𝕜] X) T
Tactic: convert! h₂
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative (goal)
Goal:
𝕜 : Type u_1
X : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
T : X →L[𝕜] X
μ : 𝕜
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)
⊢ S = -HSub.hSub (α := X →L[𝕜] X) ((algebraMap 𝕜 (X →L[𝕜] X) : (a : 𝕜) → X →L[𝕜] X) μ : X →L[𝕜] X) T
have 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)
Tactic: ext x
-- 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) μ
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)
⊢ False
have h₃ : ¬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]
Cleared hypotheses: h₂
-- 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.Bijective (α := X) (β := X) (⇑S : (a : X) → X)
⊢ False
have h₃ : ¬Function.Surjective (α := X) (β := X) (⇑S : (a : X) → X)
Tactic: replace h₂ : ¬ (S : X → X).Surjective := by grind [Function.Bijective, hK.injective]
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative (goal)
Goal:
𝕜 : Type u_1
X : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
T : X →L[𝕜] X
μ : 𝕜
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)
⊢ False
have obtain : ∀ (c : 𝕜) (hc : 1 < ‖c‖), False
Tactic: obtain ⟨c, hc⟩ := NormedField.exists_one_lt_norm 𝕜
-- 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‖
⊢ False
have 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
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)
-- 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_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
have hf_mem₁ : ∀ {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 _)
Cleared hypotheses: hf_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
n m : ℕ
h : m ≤ n
⊢ Membership.mem (α := X) ((↑S : X →ₗ[𝕜] X) ^ (m + 1)).range ((S : (a : X) → X) (f n) : X)
have rw : Membership.mem (α := X) (Submodule.map (↑S : X →ₗ[𝕜] X) (LinearMap.range ((↑S : X →ₗ[𝕜] X) ^ m)))
  ((S : (a : X) → X) (f n) : X)
Tactic: rw [iterate_succ', LinearMap.range_comp]
-- 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
⊢ False
have hf_mem' : ∀ {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⟩
-- 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)
⊢ Pairwise fun (x₁ x₂ : ℕ) ↦
    ‖μ‖ ≤ ‖HSub.hSub (α := X) (β := X) ((T : (a : X) → X) (f x₁) : X) ((T : (a : X) → X) (f x₂) : X)‖
have hp : Symmetric 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
-- 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 :
  Symmetric fun (x₁ x₂ : ℕ) ↦
    ‖μ‖ ≤ ‖HSub.hSub (α := X) (β := X) ((T : (a : X) → X) (f x₁) : X) ((T : (a : X) → X) (f x₂) : X)‖
⊢ Pairwise fun (x₁ x₂ : ℕ) ↦
    ‖μ‖ ≤ ‖HSub.hSub (α := X) (β := X) ((T : (a : X) → X) (f x₁) : X) ((T : (a : X) → X) (f x₂) : X)‖
have a : ∀ ⦃a b : ℕ⦄, a < b → ‖μ‖ ≤ ‖HSub.hSub (α := X) (β := X) ((T : (a : X) → X) (f a) : X) ((T : (a : X) → X) (f b) : X)‖
Tactic: apply Pairwise.of_lt
-- 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)
⊢ μ • (f m - u) = HSub.hSub (α := X) (β := X) ((T : (a : X) → X) (f m) : X) ((T : (a : X) → X) (f n) : X)
have 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)
Tactic: rw [smul_sub, smul_inv_smul₀ hμ]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative (goal)
Goal:
𝕜 : Type u_1
X : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
T : X →L[𝕜] X
μ : 𝕜
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) (β := 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)
have 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)
Tactic: simp [S]
-- 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)
⊢ μ • 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)
have 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
Tactic: linear_combination (norm := module)
-- 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)
⊢ ‖μ‖ ≤ ‖HSub.hSub (α := X) (β := X) ((T : (a : X) → X) (f m) : X) ((T : (a : X) → X) (f n) : X)‖
have hu : μ • (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)