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
μ : 𝕜
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h :
  ∀ (c : ℝ) (_ : c > 0), ∃ (x : X), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < c * ‖x‖
hK : ∀ K > 0, ∃ (x : X), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < K * ‖x‖
C : 𝕜
hC : 1 < ‖C‖
ε : ℝ
hε : ε > 0
x : X
hx : norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < ε * ‖x‖
this : x ≠ 0
obtain :
  ∀ (η : 𝕜) (hη : η ≠ 0) (h₁ : ‖η • x‖ < 1) (h₂ : 1 / ‖C‖ ≤ ‖η • x‖) (h₃ : ‖η‖⁻¹ ≤ 1⁻¹ * ‖C‖ * ‖x‖),
    ∃ (x : X), ‖x‖ ≤ 1 ∧ ‖C‖⁻¹ ≤ ‖x‖ ∧ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < ε
⊢ ∃ (x : X), ‖x‖ ≤ 1 ∧ ‖C‖⁻¹ ≤ ‖x‖ ∧ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < ε

Tactic:
obtain ⟨η, hη, h₁, h₂, h₃⟩ := rescale_to_shell hC (ε := 1) (by simp) this

Premises used: rescale_to_shell
-- 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
μ : 𝕜
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h :
  ∀ (c : ℝ) (_ : c > 0), ∃ (x : X), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < c * ‖x‖
hK : ∀ K > 0, ∃ (x : X), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < K * ‖x‖
C : 𝕜
hC : 1 < ‖C‖
ε : ℝ
hε : ε > 0
x : X
hx : norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < ε * ‖x‖
this : x ≠ 0
η : 𝕜
hη : η ≠ 0
h₁ : ‖η • x‖ < 1
h₂ : 1 / ‖C‖ ≤ ‖η • x‖
h₃ : ‖η‖⁻¹ ≤ 1⁻¹ * ‖C‖ * ‖x‖
⊢ ‖C‖⁻¹ ≤ ‖η • x‖

Tactic:
simpa using 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
μ : 𝕜
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h :
  ∀ (c : ℝ) (_ : c > 0), ∃ (x : X), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < c * ‖x‖
hK : ∀ K > 0, ∃ (x : X), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < K * ‖x‖
C : 𝕜
hC : 1 < ‖C‖
ε : ℝ
hε : ε > 0
x : X
hx : norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < ε * ‖x‖
this : x ≠ 0
η : 𝕜
hη : η ≠ 0
h₁ : ‖η • x‖ < 1
h₂ : 1 / ‖C‖ ≤ ‖η • x‖
h₃ : ‖η‖⁻¹ ≤ 1⁻¹ * ‖C‖ * ‖x‖
refine : norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (η • x) : X) < ε
⊢ ∃ (x : X), ‖x‖ ≤ 1 ∧ ‖C‖⁻¹ ≤ ‖x‖ ∧ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < ε

Tactic:
refine ⟨η • x, h₁.le, by simpa using 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
μ : 𝕜
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h :
  ∀ (c : ℝ) (_ : c > 0), ∃ (x : X), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < c * ‖x‖
hK : ∀ K > 0, ∃ (x : X), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < K * ‖x‖
C : 𝕜
hC : 1 < ‖C‖
ε : ℝ
hε : ε > 0
x : X
hx : norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < ε * ‖x‖
this : x ≠ 0
η : 𝕜
hη : η ≠ 0
h₁ : ‖η • x‖ < 1
h₂ : 1 / ‖C‖ ≤ ‖η • x‖
h₃ : ‖η‖⁻¹ ≤ 1⁻¹ * ‖C‖ * ‖x‖
grw : ε * ‖η • x‖ < ε
⊢ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (η • x) : X) < ε

Tactic:
grw [map_smul, norm_smul, hx, mul_left_comm, ← norm_smul]

Premises used: norm_smul, mul_left_comm, map_smul
-- 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
μ : 𝕜
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h :
  ∀ (c : ℝ) (_ : c > 0), ∃ (x : X), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < c * ‖x‖
hK : ∀ K > 0, ∃ (x : X), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < K * ‖x‖
C : 𝕜
hC : 1 < ‖C‖
ε : ℝ
hε : ε > 0
x : X
hx : norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < ε * ‖x‖
this : x ≠ 0
η : 𝕜
hη : η ≠ 0
h₁ : ‖η • x‖ < 1
h₂ : 1 / ‖C‖ ≤ ‖η • x‖
h₃ : ‖η‖⁻¹ ≤ 1⁻¹ * ‖C‖ * ‖x‖
⊢ ε * ‖η • x‖ < ε

Tactic:
linear_combination ε * 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
μ : 𝕜
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h :
  ∀ (c : ℝ) (_ : c > 0), ∃ (x : X), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < c * ‖x‖
hK : ∀ K > 0, ∃ (x : X), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < K * ‖x‖
⊢ ∃ c > 0,
    ∀ ε > 0,
      ∃ (x : X), ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < ε

Tactic:
replace hK : ∃ c > 0, ∀ ε > 0, ∃ x, ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ ‖(T - μ • 1) x‖ < ε := by
    obtain ⟨C, hC⟩ := NormedField.exists_one_lt_norm 𝕜
    refine ⟨‖C‖⁻¹, by positivity, fun ε hε ↦ ?_⟩
    obtain ⟨x, hx⟩ := hK ε (by positivity)
    have : x ≠ 0 := by aesop
    obtain ⟨η, hη, h₁, h₂, h₃⟩ := rescale_to_shell hC (ε := 1) (by simp) this
    refine ⟨η • x, h₁.le, by simpa using h₂, ?_⟩
    grw [map_smul, norm_smul, hx, mul_left_comm, ← norm_smul]
    linear_combination ε * 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
μ : 𝕜
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h :
  ∀ (c : ℝ) (_ : c > 0), ∃ (x : X), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < c * ‖x‖
hK :
  ∃ c > 0,
    ∀ ε > 0,
      ∃ (x : X), ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < ε
obtain :
  ∀ (c : ℝ) (hc₀ : c > 0)
    (hc :
      ∀ ε > 0,
        ∃ (x : X), ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < ε),
    HasEigenvalue (↑T : X →ₗ[𝕜] X) μ
⊢ HasEigenvalue (↑T : X →ₗ[𝕜] X) μ

Tactic:
obtain ⟨c, hc₀, hc⟩ := hK
-- 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
μ : 𝕜
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h :
  ∀ (c : ℝ) (_ : c > 0), ∃ (x : X), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < c * ‖x‖
c : ℝ
hc₀ : c > 0
hc :
  ∀ ε > 0, ∃ (x : X), ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < ε
obtain :
  ∀ (φ : ℕ → ℝ) (hφ_anti : StrictAnti φ) (hφ_pos : ∀ (n : ℕ), 0 < φ n) (hφ : Tendsto φ atTop (𝓝 0)),
    HasEigenvalue (↑T : X →ₗ[𝕜] X) μ
⊢ HasEigenvalue (↑T : X →ₗ[𝕜] X) μ

Tactic:
obtain ⟨φ, hφ_anti, hφ_pos, hφ⟩ := exists_seq_strictAnti_tendsto (0 : ℝ)

Premises used: exists_seq_strictAnti_tendsto, 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
μ : 𝕜
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h :
  ∀ (c : ℝ) (_ : c > 0), ∃ (x : X), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < c * ‖x‖
c : ℝ
hc₀ : c > 0
hc :
  ∀ ε > 0, ∃ (x : X), ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < ε
φ : ℕ → ℝ
hφ_anti : StrictAnti φ
hφ_pos : ∀ (n : ℕ), 0 < φ n
hφ : Tendsto φ atTop (𝓝 0)
⊢ ∀ (n : ℕ),
    ∃ (x : X), ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < φ n

Tactic:
have (n : ℕ) : ∃ x, ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ ‖(T - μ • 1) x‖ < φ n := hc (φ n) (hφ_pos n)
-- 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
μ : 𝕜
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h :
  ∀ (c : ℝ) (_ : c > 0), ∃ (x : X), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < c * ‖x‖
c : ℝ
hc₀ : c > 0
hc :
  ∀ ε > 0, ∃ (x : X), ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < ε
φ : ℕ → ℝ
hφ_anti : StrictAnti φ
hφ_pos : ∀ (n : ℕ), 0 < φ n
hφ : Tendsto φ atTop (𝓝 0)
this :
  ∀ (n : ℕ),
    ∃ (x : X), ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < φ n
choose :
  ∀ (x : (n : ℕ) → X) (hx_norm_upper : ∀ (n : ℕ), ‖x n‖ ≤ 1) (hx_norm_lower : ∀ (n : ℕ), c ≤ ‖x n‖)
    (hx_bound : ∀ (n : ℕ), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n) : X) < φ n),
    HasEigenvalue (↑T : X →ₗ[𝕜] X) μ
⊢ HasEigenvalue (↑T : X →ₗ[𝕜] X) μ

Tactic:
choose x hx_norm_upper hx_norm_lower hx_bound using 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
μ : 𝕜
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h :
  ∀ (c : ℝ) (_ : c > 0), ∃ (x : X), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < c * ‖x‖
c : ℝ
hc₀ : c > 0
hc :
  ∀ ε > 0, ∃ (x : X), ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < ε
φ : ℕ → ℝ
hφ_anti : StrictAnti φ
hφ_pos : ∀ (n : ℕ), 0 < φ n
hφ : Tendsto φ atTop (𝓝 0)
x : (n : ℕ) → X
hx_norm_upper : ∀ (n : ℕ), ‖x n‖ ≤ 1
hx_norm_lower : ∀ (n : ℕ), c ≤ ‖x n‖
hx_bound : ∀ (n : ℕ), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n) : X) < φ n
⊢ ∀ (n : ℕ), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n) : X) ≤ φ n

Tactic:
grind
-- 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
μ : 𝕜
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h :
  ∀ (c : ℝ) (_ : c > 0), ∃ (x : X), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < c * ‖x‖
c : ℝ
hc₀ : c > 0
hc :
  ∀ ε > 0, ∃ (x : X), ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < ε
φ : ℕ → ℝ
hφ_anti : StrictAnti φ
hφ_pos : ∀ (n : ℕ), 0 < φ n
hφ : Tendsto φ atTop (𝓝 0)
x : (n : ℕ) → X
hx_norm_upper : ∀ (n : ℕ), ‖x n‖ ≤ 1
hx_norm_lower : ∀ (n : ℕ), c ≤ ‖x n‖
hx_bound : ∀ (n : ℕ), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n) : X) < φ n
⊢ Tendsto.{0, u_2} (β := X) (fun (n : ℕ) ↦ (T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n)) atTop (𝓝 0)

Tactic:
have hx_lim : Tendsto (fun n ↦ (T - μ • 1) (x n)) atTop (𝓝 0) := squeeze_zero_norm (by grind) 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
μ : 𝕜
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h :
  ∀ (c : ℝ) (_ : c > 0), ∃ (x : X), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < c * ‖x‖
c : ℝ
hc₀ : c > 0
hc :
  ∀ ε > 0, ∃ (x : X), ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < ε
φ : ℕ → ℝ
hφ_anti : StrictAnti φ
hφ_pos : ∀ (n : ℕ), 0 < φ n
hφ : Tendsto φ atTop (𝓝 0)
x : (n : ℕ) → X
hx_norm_upper : ∀ (n : ℕ), ‖x n‖ ≤ 1
hx_norm_lower : ∀ (n : ℕ), c ≤ ‖x n‖
hx_bound : ∀ (n : ℕ), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n) : X) < φ n
hx_lim :
  Tendsto.{0, u_2} (β := X) (fun (n : ℕ) ↦ (T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n)) atTop (𝓝 0)
y_ : (n : ℕ) → X := fun (n : ℕ) ↦ (T : (a : X) → X) (x n)
⊢ ‖μ‖ * c / 2 > 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
μ : 𝕜
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h :
  ∀ (c : ℝ) (_ : c > 0), ∃ (x : X), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < c * ‖x‖
c : ℝ
hc₀ : c > 0
hc :
  ∀ ε > 0, ∃ (x : X), ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < ε
φ : ℕ → ℝ
hφ_anti : StrictAnti φ
hφ_pos : ∀ (n : ℕ), 0 < φ n
hφ : Tendsto φ atTop (𝓝 0)
x : (n : ℕ) → X
hx_norm_upper : ∀ (n : ℕ), ‖x n‖ ≤ 1
hx_norm_lower : ∀ (n : ℕ), c ≤ ‖x n‖
hx_bound : ∀ (n : ℕ), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n) : X) < φ n
hx_lim :
  Tendsto.{0, u_2} (β := X) (fun (n : ℕ) ↦ (T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n)) atTop (𝓝 0)
y_ : (n : ℕ) → X := fun (n : ℕ) ↦ (T : (a : X) → X) (x n)
refine : ∀ᶠ (n : ℕ) in atTop, ‖μ‖ * c / 2 ≤ ‖y_ n‖
⊢ ∃ d > 0, ∀ᶠ (n : ℕ) in atTop, d ≤ ‖y_ n‖

Tactic:
refine ⟨(‖μ‖ * c) / 2, by 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
μ : 𝕜
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h :
  ∀ (c : ℝ) (_ : c > 0), ∃ (x : X), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < c * ‖x‖
c : ℝ
hc₀ : c > 0
hc :
  ∀ ε > 0, ∃ (x : X), ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < ε
φ : ℕ → ℝ
hφ_anti : StrictAnti φ
hφ_pos : ∀ (n : ℕ), 0 < φ n
hφ : Tendsto φ atTop (𝓝 0)
x : (n : ℕ) → X
hx_norm_upper : ∀ (n : ℕ), ‖x n‖ ≤ 1
hx_norm_lower : ∀ (n : ℕ), c ≤ ‖x n‖
hx_bound : ∀ (n : ℕ), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n) : X) < φ n
hx_lim :
  Tendsto.{0, u_2} (β := X) (fun (n : ℕ) ↦ (T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n)) atTop (𝓝 0)
y_ : (n : ℕ) → X := fun (n : ℕ) ↦ (T : (a : X) → X) (x n)
h₁ : ∀ (n : ℕ) (hn : φ n ≤ ‖μ‖ * c / 2), ‖μ‖ * c / 2 ≤ ‖y_ n‖
⊢ ∀ᶠ (n : ℕ) in atTop, ‖μ‖ * c / 2 ≤ ‖y_ n‖

Tactic:
filter_upwards [hφ.eventually_le_const (show (‖μ‖ * c) / 2 > 0 by positivity)] with n hn

Premises used: Filter.Tendsto.eventually_le_const
-- 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
μ : 𝕜
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h :
  ∀ (c : ℝ) (_ : c > 0), ∃ (x : X), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < c * ‖x‖
c : ℝ
hc₀ : c > 0
hc :
  ∀ ε > 0, ∃ (x : X), ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < ε
φ : ℕ → ℝ
hφ_anti : StrictAnti φ
hφ_pos : ∀ (n : ℕ), 0 < φ n
hφ : Tendsto φ atTop (𝓝 0)
x : (n : ℕ) → X
hx_norm_upper : ∀ (n : ℕ), ‖x n‖ ≤ 1
hx_norm_lower : ∀ (n : ℕ), c ≤ ‖x n‖
hx_bound : ∀ (n : ℕ), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n) : X) < φ n
hx_lim :
  Tendsto.{0, u_2} (β := X) (fun (n : ℕ) ↦ (T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n)) atTop (𝓝 0)
y_ : (n : ℕ) → X := fun (n : ℕ) ↦ (T : (a : X) → X) (x n)
n : ℕ
hn : φ n ≤ ‖μ‖ * c / 2
⊢ ‖HSub.hSub (α := X) ((T : (a : X) → X) (x n) : X) (μ • x n)‖ < φ n

Tactic:
simpa using hx_bound n
-- 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
μ : 𝕜
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h :
  ∀ (c : ℝ) (_ : c > 0), ∃ (x : X), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < c * ‖x‖
c : ℝ
hc₀ : c > 0
hc :
  ∀ ε > 0, ∃ (x : X), ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < ε
φ : ℕ → ℝ
hφ_anti : StrictAnti φ
hφ_pos : ∀ (n : ℕ), 0 < φ n
hφ : Tendsto φ atTop (𝓝 0)
x : (n : ℕ) → X
hx_norm_upper : ∀ (n : ℕ), ‖x n‖ ≤ 1
hx_norm_lower : ∀ (n : ℕ), c ≤ ‖x n‖
hx_bound : ∀ (n : ℕ), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n) : X) < φ n
hx_lim :
  Tendsto.{0, u_2} (β := X) (fun (n : ℕ) ↦ (T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n)) atTop (𝓝 0)
y_ : (n : ℕ) → X := fun (n : ℕ) ↦ (T : (a : X) → X) (x n)
n : ℕ
hn : φ n ≤ ‖μ‖ * c / 2
⊢ ‖HSub.hSub (α := X) ((T : (a : X) → X) (x n) : X) (μ • x n)‖ < φ n

Tactic:
have h₁ : ‖T (x n) - μ • x n‖ < φ n := by simpa using hx_bound n
-- 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
μ : 𝕜
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h :
  ∀ (c : ℝ) (_ : c > 0), ∃ (x : X), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < c * ‖x‖
c : ℝ
hc₀ : c > 0
hc :
  ∀ ε > 0, ∃ (x : X), ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < ε
φ : ℕ → ℝ
hφ_anti : StrictAnti φ
hφ_pos : ∀ (n : ℕ), 0 < φ n
hφ : Tendsto φ atTop (𝓝 0)
x : (n : ℕ) → X
hx_norm_upper : ∀ (n : ℕ), ‖x n‖ ≤ 1
hx_norm_lower : ∀ (n : ℕ), c ≤ ‖x n‖
hx_bound : ∀ (n : ℕ), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n) : X) < φ n
hx_lim :
  Tendsto.{0, u_2} (β := X) (fun (n : ℕ) ↦ (T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n)) atTop (𝓝 0)
y_ : (n : ℕ) → X := fun (n : ℕ) ↦ (T : (a : X) → X) (x n)
n : ℕ
hn : φ n ≤ ‖μ‖ * c / 2
h₁ : ‖HSub.hSub (α := X) ((T : (a : X) → X) (x n) : X) (μ • x n)‖ < φ n
⊢ ‖μ‖ * ‖x n‖ ≤
    norm (E := X) ((T : (a : X) → X) (x n) : X) + ‖HSub.hSub (α := X) ((T : (a : X) → X) (x n) : X) (μ • x n)‖

Tactic:
simpa [norm_smul] using norm_le_norm_add_norm_sub (T (x n)) (μ • x n)

Premises used: norm_smul, norm_le_norm_add_norm_sub, HSMul.hSMul, DFunLike.coe
-- 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
μ : 𝕜
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h :
  ∀ (c : ℝ) (_ : c > 0), ∃ (x : X), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < c * ‖x‖
c : ℝ
hc₀ : c > 0
hc :
  ∀ ε > 0, ∃ (x : X), ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < ε
φ : ℕ → ℝ
hφ_anti : StrictAnti φ
hφ_pos : ∀ (n : ℕ), 0 < φ n
hφ : Tendsto φ atTop (𝓝 0)
x : (n : ℕ) → X
hx_norm_upper : ∀ (n : ℕ), ‖x n‖ ≤ 1
hx_norm_lower : ∀ (n : ℕ), c ≤ ‖x n‖
hx_bound : ∀ (n : ℕ), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n) : X) < φ n
hx_lim :
  Tendsto.{0, u_2} (β := X) (fun (n : ℕ) ↦ (T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n)) atTop (𝓝 0)
y_ : (n : ℕ) → X := fun (n : ℕ) ↦ (T : (a : X) → X) (x n)
n : ℕ
hn : φ n ≤ ‖μ‖ * c / 2
h₁ : ‖HSub.hSub (α := X) ((T : (a : X) → X) (x n) : X) (μ • x n)‖ < φ n
⊢ ‖μ‖ * ‖x n‖ ≤
    norm (E := X) ((T : (a : X) → X) (x n) : X) + ‖HSub.hSub (α := X) ((T : (a : X) → X) (x n) : X) (μ • x n)‖

Tactic:
have h₂ : ‖μ‖ * ‖x n‖ ≤ ‖T (x n)‖ + ‖T (x n) - μ • x n‖ := by
      simpa [norm_smul] using norm_le_norm_add_norm_sub (T (x n)) (μ • x n)
-- 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
μ : 𝕜
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h :
  ∀ (c : ℝ) (_ : c > 0), ∃ (x : X), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < c * ‖x‖
c : ℝ
hc₀ : c > 0
hc :
  ∀ ε > 0, ∃ (x : X), ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < ε
φ : ℕ → ℝ
hφ_anti : StrictAnti φ
hφ_pos : ∀ (n : ℕ), 0 < φ n
hφ : Tendsto φ atTop (𝓝 0)
x : (n : ℕ) → X
hx_norm_upper : ∀ (n : ℕ), ‖x n‖ ≤ 1
hx_norm_lower : ∀ (n : ℕ), c ≤ ‖x n‖
hx_bound : ∀ (n : ℕ), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n) : X) < φ n
hx_lim :
  Tendsto.{0, u_2} (β := X) (fun (n : ℕ) ↦ (T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n)) atTop (𝓝 0)
y_ : (n : ℕ) → X := fun (n : ℕ) ↦ (T : (a : X) → X) (x n)
n : ℕ
hn : φ n ≤ ‖μ‖ * c / 2
h₁ : ‖HSub.hSub (α := X) ((T : (a : X) → X) (x n) : X) (μ • x n)‖ < φ n
h₂ :
  ‖μ‖ * ‖x n‖ ≤
    norm (E := X) ((T : (a : X) → X) (x n) : X) + ‖HSub.hSub (α := X) ((T : (a : X) → X) (x n) : X) (μ • x n)‖
⊢ ‖μ‖ * c / 2 ≤ ‖y_ n‖

Tactic:
linear_combination h₂ + h₁ + hn + ‖μ‖ * hx_norm_lower n
-- 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
μ : 𝕜
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h :
  ∀ (c : ℝ) (_ : c > 0), ∃ (x : X), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < c * ‖x‖
c : ℝ
hc₀ : c > 0
hc :
  ∀ ε > 0, ∃ (x : X), ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < ε
φ : ℕ → ℝ
hφ_anti : StrictAnti φ
hφ_pos : ∀ (n : ℕ), 0 < φ n
hφ : Tendsto φ atTop (𝓝 0)
x : (n : ℕ) → X
hx_norm_upper : ∀ (n : ℕ), ‖x n‖ ≤ 1
hx_norm_lower : ∀ (n : ℕ), c ≤ ‖x n‖
hx_bound : ∀ (n : ℕ), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n) : X) < φ n
hx_lim :
  Tendsto.{0, u_2} (β := X) (fun (n : ℕ) ↦ (T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (x n)) atTop (𝓝 0)
y_ : (n : ℕ) → X := fun (n : ℕ) ↦ (T : (a : X) → X) (x n)
⊢ ∃ d > 0, ∀ᶠ (n : ℕ) in atTop, d ≤ ‖y_ n‖

Tactic:
have hy_lower : ∃ d > 0, ∀ᶠ n in atTop, d ≤ ‖y_ n‖ := by
    refine ⟨(‖μ‖ * c) / 2, by positivity, ?_⟩
    filter_upwards [hφ.eventually_le_const (show (‖μ‖ * c) / 2 > 0 by positivity)] with n hn
    have h₁ : ‖T (x n) - μ • x n‖ < φ n := by simpa using hx_bound n
    have h₂ : ‖μ‖ * ‖x n‖ ≤ ‖T (x n)‖ + ‖T (x n) - μ • x n‖ := by
      simpa [norm_smul] using norm_le_norm_add_norm_sub (T (x n)) (μ • x n)
    linear_combination h₂ + h₁ + hn + ‖μ‖ * hx_norm_lower n