awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NontriviallyNormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst_2 : SeminormedAddCommGroup M₁
inst_3 : AddCommGroup M₂
inst_4 : NormedSpace 𝕜₁ M₁
inst_5 : Module 𝕜₂ M₂
inst_6 : UniformSpace M₂
inst_7 : IsUniformAddGroup M₂
inst_8 : ContinuousConstSMul 𝕜₂ M₂
inst_9 : T2Space M₂
inst_10 : CompleteSpace M₂
u : M₁ →SL[σ₁₂] M₂
hu :
  ∀ (U : Set (M₁ →SL[σ₁₂] M₂)),
    Membership.mem (γ := Filter (M₁ →SL[σ₁₂] M₂)) (𝓝 0) U →
      ∃ (y : M₁ →SL[σ₁₂] M₂),
        Membership.mem (γ := Set (M₁ →SL[σ₁₂] M₂))
            {f : M₁ →SL[σ₁₂] M₂ | IsCompactOperator.{u_3, u_4} (M₁ := M₁) (M₂ := M₂) (⇑f : (a : M₁) → M₂)} y ∧
          y - u ∈ U
U : Set M₂
hU : Membership.mem (γ := Filter M₂) (𝓝 0) U
V : Set M₂
hV : Membership.mem (γ := Filter M₂) (𝓝 0) V
hVU : ∀ v ∈ V, ∀ w ∈ V, v + w ∈ U
SV : Prod.{u_3, u_4} (Set M₁) (Set M₂) := (closedBall 0 1, -V)
v : M₁ →SL[σ₁₂] M₂
hv :
  Membership.mem (γ := Set (M₁ →SL[σ₁₂] M₂))
    {f : M₁ →SL[σ₁₂] M₂ | IsCompactOperator.{u_3, u_4} (M₁ := M₁) (M₂ := M₂) (⇑f : (a : M₁) → M₂)} v
huv :
  Membership.mem (γ := Set (M₁ →SL[σ₁₂] M₂))
    {f : M₁ →SL[σ₁₂] M₂ | ∀ x ∈ SV.1, Membership.mem (α := M₂) SV.2 ((f : (a : M₁) → M₂) x : M₂)} (v - u)
T : Set M₂
hT : T.Finite
hTv :
  Subset.{u_4} (α := Set M₂)
    (closure[inst_6.toTopologicalSpace]
      (image.{u_3, u_4} (α := M₁) (⇑(↑v : M₁ →ₛₗ[σ₁₂] M₂) : (a : M₁) → M₂) (closedBall 0 1)))
    (⋃ y ∈ T, y +ᵥ V)
x : M₁
hx : Membership.mem (γ := Set M₁) (closedBall 0 1) x
t : M₂
ht : t ∈ T
htx : Membership.mem (γ := Set M₁) ((⇑v : (a : M₁) → M₂) ⁻¹' (t +ᵥ V)) x
refine : Membership.mem (γ := Set M₁) ((⇑u : (a : M₁) → M₂) ⁻¹' (t +ᵥ U)) x
⊢ ∃ (i : M₂) (_ : i ∈ T), Membership.mem (γ := Set M₁) ((⇑u : (a : M₁) → M₂) ⁻¹' (i +ᵥ U)) x

Tactic:
refine ⟨t, ht, ?_⟩
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NontriviallyNormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst_2 : SeminormedAddCommGroup M₁
inst_3 : AddCommGroup M₂
inst_4 : NormedSpace 𝕜₁ M₁
inst_5 : Module 𝕜₂ M₂
inst_6 : UniformSpace M₂
inst_7 : IsUniformAddGroup M₂
inst_8 : ContinuousConstSMul 𝕜₂ M₂
inst_9 : T2Space M₂
inst_10 : CompleteSpace M₂
u : M₁ →SL[σ₁₂] M₂
hu :
  ∀ (U : Set (M₁ →SL[σ₁₂] M₂)),
    Membership.mem (γ := Filter (M₁ →SL[σ₁₂] M₂)) (𝓝 0) U →
      ∃ (y : M₁ →SL[σ₁₂] M₂),
        Membership.mem (γ := Set (M₁ →SL[σ₁₂] M₂))
            {f : M₁ →SL[σ₁₂] M₂ | IsCompactOperator.{u_3, u_4} (M₁ := M₁) (M₂ := M₂) (⇑f : (a : M₁) → M₂)} y ∧
          y - u ∈ U
U : Set M₂
hU : Membership.mem (γ := Filter M₂) (𝓝 0) U
V : Set M₂
hV : Membership.mem (γ := Filter M₂) (𝓝 0) V
hVU : ∀ v ∈ V, ∀ w ∈ V, v + w ∈ U
SV : Prod.{u_3, u_4} (Set M₁) (Set M₂) := (closedBall 0 1, -V)
v : M₁ →SL[σ₁₂] M₂
hv :
  Membership.mem (γ := Set (M₁ →SL[σ₁₂] M₂))
    {f : M₁ →SL[σ₁₂] M₂ | IsCompactOperator.{u_3, u_4} (M₁ := M₁) (M₂ := M₂) (⇑f : (a : M₁) → M₂)} v
huv :
  Membership.mem (γ := Set (M₁ →SL[σ₁₂] M₂))
    {f : M₁ →SL[σ₁₂] M₂ | ∀ x ∈ SV.1, Membership.mem (α := M₂) SV.2 ((f : (a : M₁) → M₂) x : M₂)} (v - u)
T : Set M₂
hT : T.Finite
hTv :
  Subset.{u_4} (α := Set M₂)
    (closure[inst_6.toTopologicalSpace]
      (image.{u_3, u_4} (α := M₁) (⇑(↑v : M₁ →ₛₗ[σ₁₂] M₂) : (a : M₁) → M₂) (closedBall 0 1)))
    (⋃ y ∈ T, y +ᵥ V)
x : M₁
hx : Membership.mem (γ := Set M₁) (closedBall 0 1) x
t : M₂
ht : t ∈ T
htx : Membership.mem (γ := Set M₁) ((⇑v : (a : M₁) → M₂) ⁻¹' (t +ᵥ V)) x
rw :
  ∀ (htx : HSub.hSub (α := M₂) ((v : (a : M₁) → M₂) x : M₂) t ∈ V),
    HSub.hSub (α := M₂) ((u : (a : M₁) → M₂) x : M₂) t ∈ U
⊢ Membership.mem (γ := Set M₁) ((⇑u : (a : M₁) → M₂) ⁻¹' (t +ᵥ U)) x

Tactic:
rw [mem_preimage, mem_vadd_set_iff_neg_vadd_mem, vadd_eq_add, neg_add_eq_sub] at htx ⊢

Premises used: neg_add_eq_sub, vadd_eq_add, Set.mem_vadd_set_iff_neg_vadd_mem, Set.mem_preimage
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NontriviallyNormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst_2 : SeminormedAddCommGroup M₁
inst_3 : AddCommGroup M₂
inst_4 : NormedSpace 𝕜₁ M₁
inst_5 : Module 𝕜₂ M₂
inst_6 : UniformSpace M₂
inst_7 : IsUniformAddGroup M₂
inst_8 : ContinuousConstSMul 𝕜₂ M₂
inst_9 : T2Space M₂
inst_10 : CompleteSpace M₂
u : M₁ →SL[σ₁₂] M₂
hu :
  ∀ (U : Set (M₁ →SL[σ₁₂] M₂)),
    Membership.mem (γ := Filter (M₁ →SL[σ₁₂] M₂)) (𝓝 0) U →
      ∃ (y : M₁ →SL[σ₁₂] M₂),
        Membership.mem (γ := Set (M₁ →SL[σ₁₂] M₂))
            {f : M₁ →SL[σ₁₂] M₂ | IsCompactOperator.{u_3, u_4} (M₁ := M₁) (M₂ := M₂) (⇑f : (a : M₁) → M₂)} y ∧
          y - u ∈ U
U : Set M₂
hU : Membership.mem (γ := Filter M₂) (𝓝 0) U
V : Set M₂
hV : Membership.mem (γ := Filter M₂) (𝓝 0) V
hVU : ∀ v ∈ V, ∀ w ∈ V, v + w ∈ U
SV : Prod.{u_3, u_4} (Set M₁) (Set M₂) := (closedBall 0 1, -V)
v : M₁ →SL[σ₁₂] M₂
hv :
  Membership.mem (γ := Set (M₁ →SL[σ₁₂] M₂))
    {f : M₁ →SL[σ₁₂] M₂ | IsCompactOperator.{u_3, u_4} (M₁ := M₁) (M₂ := M₂) (⇑f : (a : M₁) → M₂)} v
huv :
  Membership.mem (γ := Set (M₁ →SL[σ₁₂] M₂))
    {f : M₁ →SL[σ₁₂] M₂ | ∀ x ∈ SV.1, Membership.mem (α := M₂) SV.2 ((f : (a : M₁) → M₂) x : M₂)} (v - u)
T : Set M₂
hT : T.Finite
hTv :
  Subset.{u_4} (α := Set M₂)
    (closure[inst_6.toTopologicalSpace]
      (image.{u_3, u_4} (α := M₁) (⇑(↑v : M₁ →ₛₗ[σ₁₂] M₂) : (a : M₁) → M₂) (closedBall 0 1)))
    (⋃ y ∈ T, y +ᵥ V)
x : M₁
hx : Membership.mem (γ := Set M₁) (closedBall 0 1) x
t : M₂
ht : t ∈ T
htx : HSub.hSub (α := M₂) ((v : (a : M₁) → M₂) x : M₂) t ∈ V
⊢ HAdd.hAdd (β := M₂) (HSub.hSub (α := M₂) ((v : (a : M₁) → M₂) x : M₂) t) (-(v - u : (a : M₁) → M₂) x : M₂) ∈ U

Tactic:
hVU _ htx _ (huv x hx)
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NontriviallyNormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst_2 : SeminormedAddCommGroup M₁
inst_3 : AddCommGroup M₂
inst_4 : NormedSpace 𝕜₁ M₁
inst_5 : Module 𝕜₂ M₂
inst_6 : UniformSpace M₂
inst_7 : IsUniformAddGroup M₂
inst_8 : ContinuousConstSMul 𝕜₂ M₂
inst_9 : T2Space M₂
inst_10 : CompleteSpace M₂
u : M₁ →SL[σ₁₂] M₂
hu :
  ∀ (U : Set (M₁ →SL[σ₁₂] M₂)),
    Membership.mem (γ := Filter (M₁ →SL[σ₁₂] M₂)) (𝓝 0) U →
      ∃ (y : M₁ →SL[σ₁₂] M₂),
        Membership.mem (γ := Set (M₁ →SL[σ₁₂] M₂))
            {f : M₁ →SL[σ₁₂] M₂ | IsCompactOperator.{u_3, u_4} (M₁ := M₁) (M₂ := M₂) (⇑f : (a : M₁) → M₂)} y ∧
          y - u ∈ U
U : Set M₂
hU : Membership.mem (γ := Filter M₂) (𝓝 0) U
V : Set M₂
hV : Membership.mem (γ := Filter M₂) (𝓝 0) V
hVU : ∀ v ∈ V, ∀ w ∈ V, v + w ∈ U
SV : Prod.{u_3, u_4} (Set M₁) (Set M₂) := (closedBall 0 1, -V)
v : M₁ →SL[σ₁₂] M₂
hv :
  Membership.mem (γ := Set (M₁ →SL[σ₁₂] M₂))
    {f : M₁ →SL[σ₁₂] M₂ | IsCompactOperator.{u_3, u_4} (M₁ := M₁) (M₂ := M₂) (⇑f : (a : M₁) → M₂)} v
huv :
  Membership.mem (γ := Set (M₁ →SL[σ₁₂] M₂))
    {f : M₁ →SL[σ₁₂] M₂ | ∀ x ∈ SV.1, Membership.mem (α := M₂) SV.2 ((f : (a : M₁) → M₂) x : M₂)} (v - u)
T : Set M₂
hT : T.Finite
hTv :
  Subset.{u_4} (α := Set M₂)
    (closure[inst_6.toTopologicalSpace]
      (image.{u_3, u_4} (α := M₁) (⇑(↑v : M₁ →ₛₗ[σ₁₂] M₂) : (a : M₁) → M₂) (closedBall 0 1)))
    (⋃ y ∈ T, y +ᵥ V)
x : M₁
hx : Membership.mem (γ := Set M₁) (closedBall 0 1) x
t : M₂
ht : t ∈ T
htx : HSub.hSub (α := M₂) ((v : (a : M₁) → M₂) x : M₂) t ∈ V
h :
  HSub.hSub (α := M₂) ((u : (a : M₁) → M₂) x : M₂) t =
    HAdd.hAdd (β := M₂) (HSub.hSub (α := M₂) ((v : (a : M₁) → M₂) x : M₂) t) (-(v - u : (a : M₁) → M₂) x : M₂)
⊢ HSub.hSub (α := M₂) ((u : (a : M₁) → M₂) x : M₂) t ∈ U

Tactic:
convert! hVU _ htx _ (huv x hx) using 1
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NontriviallyNormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst_2 : SeminormedAddCommGroup M₁
inst_3 : AddCommGroup M₂
inst_4 : NormedSpace 𝕜₁ M₁
inst_5 : Module 𝕜₂ M₂
inst_6 : UniformSpace M₂
inst_7 : IsUniformAddGroup M₂
inst_8 : ContinuousConstSMul 𝕜₂ M₂
inst_9 : T2Space M₂
inst_10 : CompleteSpace M₂
u : M₁ →SL[σ₁₂] M₂
hu :
  ∀ (U : Set (M₁ →SL[σ₁₂] M₂)),
    Membership.mem (γ := Filter (M₁ →SL[σ₁₂] M₂)) (𝓝 0) U →
      ∃ (y : M₁ →SL[σ₁₂] M₂),
        Membership.mem (γ := Set (M₁ →SL[σ₁₂] M₂))
            {f : M₁ →SL[σ₁₂] M₂ | IsCompactOperator.{u_3, u_4} (M₁ := M₁) (M₂ := M₂) (⇑f : (a : M₁) → M₂)} y ∧
          y - u ∈ U
U : Set M₂
hU : Membership.mem (γ := Filter M₂) (𝓝 0) U
V : Set M₂
hV : Membership.mem (γ := Filter M₂) (𝓝 0) V
hVU : ∀ v ∈ V, ∀ w ∈ V, v + w ∈ U
SV : Prod.{u_3, u_4} (Set M₁) (Set M₂) := (closedBall 0 1, -V)
v : M₁ →SL[σ₁₂] M₂
hv :
  Membership.mem (γ := Set (M₁ →SL[σ₁₂] M₂))
    {f : M₁ →SL[σ₁₂] M₂ | IsCompactOperator.{u_3, u_4} (M₁ := M₁) (M₂ := M₂) (⇑f : (a : M₁) → M₂)} v
huv :
  Membership.mem (γ := Set (M₁ →SL[σ₁₂] M₂))
    {f : M₁ →SL[σ₁₂] M₂ | ∀ x ∈ SV.1, Membership.mem (α := M₂) SV.2 ((f : (a : M₁) → M₂) x : M₂)} (v - u)
T : Set M₂
hT : T.Finite
hTv :
  Subset.{u_4} (α := Set M₂)
    (closure[inst_6.toTopologicalSpace]
      (image.{u_3, u_4} (α := M₁) (⇑(↑v : M₁ →ₛₗ[σ₁₂] M₂) : (a : M₁) → M₂) (closedBall 0 1)))
    (⋃ y ∈ T, y +ᵥ V)
x : M₁
hx : Membership.mem (γ := Set M₁) (closedBall 0 1) x
t : M₂
ht : t ∈ T
htx : HSub.hSub (α := M₂) ((v : (a : M₁) → M₂) x : M₂) t ∈ V
h :
  HSub.hSub (α := M₂) ((u : (a : M₁) → M₂) x : M₂) t =
    HSub.hSub (α := M₂) ((v : (a : M₁) → M₂) x : M₂) t +
      -HSub.hSub (α := M₂) (β := M₂) ((v : (a : M₁) → M₂) x : M₂) ((u : (a : M₁) → M₂) x : M₂)
⊢ HSub.hSub (α := M₂) ((u : (a : M₁) → M₂) x : M₂) t =
    HAdd.hAdd (β := M₂) (HSub.hSub (α := M₂) ((v : (a : M₁) → M₂) x : M₂) t) (-(v - u : (a : M₁) → M₂) x : M₂)

Tactic:
rw [ContinuousLinearMap.sub_apply]

Premises used: ContinuousLinearMap.sub_apply
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NontriviallyNormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst_2 : SeminormedAddCommGroup M₁
inst_3 : AddCommGroup M₂
inst_4 : NormedSpace 𝕜₁ M₁
inst_5 : Module 𝕜₂ M₂
inst_6 : UniformSpace M₂
inst_7 : IsUniformAddGroup M₂
inst_8 : ContinuousConstSMul 𝕜₂ M₂
inst_9 : T2Space M₂
inst_10 : CompleteSpace M₂
u : M₁ →SL[σ₁₂] M₂
hu :
  ∀ (U : Set (M₁ →SL[σ₁₂] M₂)),
    Membership.mem (γ := Filter (M₁ →SL[σ₁₂] M₂)) (𝓝 0) U →
      ∃ (y : M₁ →SL[σ₁₂] M₂),
        Membership.mem (γ := Set (M₁ →SL[σ₁₂] M₂))
            {f : M₁ →SL[σ₁₂] M₂ | IsCompactOperator.{u_3, u_4} (M₁ := M₁) (M₂ := M₂) (⇑f : (a : M₁) → M₂)} y ∧
          y - u ∈ U
U : Set M₂
hU : Membership.mem (γ := Filter M₂) (𝓝 0) U
V : Set M₂
hV : Membership.mem (γ := Filter M₂) (𝓝 0) V
hVU : ∀ v ∈ V, ∀ w ∈ V, v + w ∈ U
SV : Prod.{u_3, u_4} (Set M₁) (Set M₂) := (closedBall 0 1, -V)
v : M₁ →SL[σ₁₂] M₂
hv :
  Membership.mem (γ := Set (M₁ →SL[σ₁₂] M₂))
    {f : M₁ →SL[σ₁₂] M₂ | IsCompactOperator.{u_3, u_4} (M₁ := M₁) (M₂ := M₂) (⇑f : (a : M₁) → M₂)} v
huv :
  Membership.mem (γ := Set (M₁ →SL[σ₁₂] M₂))
    {f : M₁ →SL[σ₁₂] M₂ | ∀ x ∈ SV.1, Membership.mem (α := M₂) SV.2 ((f : (a : M₁) → M₂) x : M₂)} (v - u)
T : Set M₂
hT : T.Finite
hTv :
  Subset.{u_4} (α := Set M₂)
    (closure[inst_6.toTopologicalSpace]
      (image.{u_3, u_4} (α := M₁) (⇑(↑v : M₁ →ₛₗ[σ₁₂] M₂) : (a : M₁) → M₂) (closedBall 0 1)))
    (⋃ y ∈ T, y +ᵥ V)
x : M₁
hx : Membership.mem (γ := Set M₁) (closedBall 0 1) x
t : M₂
ht : t ∈ T
htx : HSub.hSub (α := M₂) ((v : (a : M₁) → M₂) x : M₂) t ∈ V
⊢ HSub.hSub (α := M₂) ((u : (a : M₁) → M₂) x : M₂) t =
    HSub.hSub (α := M₂) ((v : (a : M₁) → M₂) x : M₂) t +
      -HSub.hSub (α := M₂) (β := M₂) ((v : (a : M₁) → M₂) x : M₂) ((u : (a : M₁) → M₂) x : M₂)

Tactic:
abel
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NontriviallyNormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst_2 : SeminormedAddCommGroup M₁
inst_3 : AddCommGroup M₂
inst_4 : NormedSpace 𝕜₁ M₁
inst_5 : Module 𝕜₂ M₂
inst_6 : UniformSpace M₂
inst_7 : IsUniformAddGroup M₂
inst_8 : ContinuousConstSMul 𝕜₂ M₂
inst_9 : T2Space M₂
inst_10 : CompleteSpace M₂
⊢ Eq (α := Submodule 𝕜₂ (M₁ →SL[σ₁₂] M₂))
    (Submodule.topologicalClosure (compactOperator σ₁₂ M₁ M₂) : Submodule 𝕜₂ (M₁ →SL[σ₁₂] M₂))
    (compactOperator σ₁₂ M₁ M₂ : Submodule 𝕜₂ (M₁ →SL[σ₁₂] M₂))

Tactic:
SetLike.ext' isClosed_setOf_isCompactOperator.closure_eq

Premises used: IsClosed.closure_eq, SetLike.ext', isClosed_setOf_isCompactOperator
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
Goal:
ι : Type u_1
𝕜₁ : Type u_2
𝕜₂ : Type u_3
inst : NontriviallyNormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_4
M₂ : Type u_5
inst_2 : SeminormedAddCommGroup M₁
inst_3 : AddCommGroup M₂
inst_4 : NormedSpace 𝕜₁ M₁
inst_5 : Module 𝕜₂ M₂
inst_6 : UniformSpace M₂
inst_7 : IsUniformAddGroup M₂
inst_8 : ContinuousConstSMul 𝕜₂ M₂
inst_9 : T2Space M₂
inst_10 : CompleteSpace M₂
l : Filter ι
inst_11 : l.NeBot
F : ι → M₁ →SL[σ₁₂] M₂
f : M₁ →SL[σ₁₂] M₂
hf : Tendsto F l (𝓝 f)
hF : ∀ᶠ (i : ι) in l, IsCompactOperator.{u_4, u_5} (M₁ := M₁) (M₂ := M₂) (⇑(F i) : (a : M₁) → M₂)
⊢ IsCompactOperator.{u_4, u_5} (M₁ := M₁) (M₂ := M₂) (⇑f : (a : M₁) → M₂)

Tactic:
isClosed_setOf_isCompactOperator.mem_of_tendsto hf hF

Premises used: Set.Mem, setOf, IsClosed.mem_of_tendsto, IsCompactOperator, isClosed_setOf_isCompactOperator
-- Module: Mathlib.Analysis.Normed.Operator.Compact.FiniteDimension
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
E : Type u_2
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : T2Space E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyCompactSpace 𝕜
⊢ IsCompactOperator.{u_2, u_2} (M₁ := E) id ↔ FiniteDimensional 𝕜 E

Tactic:
isCompactOperator_id_iff_locallyCompactSpace.trans
    ⟨fun _ ↦ .of_locallyCompactSpace 𝕜, fun _ ↦ .of_finiteDimensional_of_complete 𝕜 E⟩

Premises used: FiniteDimensional.of_locallyCompactSpace, LocallyCompactSpace.of_finiteDimensional_of_complete, Iff.intro, Iff.trans, isCompactOperator_id_iff_locallyCompactSpace
-- Module: Mathlib.Analysis.Normed.Operator.Compact.FiniteDimension
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
E : Type u_2
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : T2Space E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
h : IsCompactOperator.{u_2, u_2} (M₁ := E) id
⊢ LocallyCompactSpace E

Tactic:
have := LocallyCompactSpace.of_isCompactOperator_id h
-- Module: Mathlib.Analysis.Normed.Operator.Compact.FiniteDimension
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
E : Type u_2
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : T2Space E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
h : IsCompactOperator.{u_2, u_2} (M₁ := E) id
this : LocallyCompactSpace E
⊢ FiniteDimensional 𝕜 E

Tactic:
FiniteDimensional.of_locallyCompactSpace 𝕜

Premises used: FiniteDimensional.of_locallyCompactSpace
-- Module: Mathlib.Analysis.Normed.Operator.Compact.FiniteDimension
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
E : Type u_2
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : T2Space E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
h : IsCompactOperator.{u_2, u_2} (M₁ := E) id
this : LocallyCompactSpace E
⊢ FiniteDimensional 𝕜 E

Tactic:
exact FiniteDimensional.of_locallyCompactSpace 𝕜

Premises used: FiniteDimensional.of_locallyCompactSpace
-- 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 : ¬HasEigenvalue (↑T : X →ₗ[𝕜] X) μ
rw : ∃ c > 0, ∀ (x : X), c * ‖x‖ ≤ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X)
⊢ ∃ (K : NNReal), AntilipschitzWith (α := X) (β := X) K (⇑(T - HSMul.hSMul (β := X →L[𝕜] X) μ 1) : (a : X) → X)

Tactic:
rw [antilipschitzWith_iff_exists_mul_le_norm]

Premises used: antilipschitzWith_iff_exists_mul_le_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
μ : 𝕜
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h : ¬HasEigenvalue (↑T : X →ₗ[𝕜] X) μ
contrapose! :
  ∀
    (h :
      ∀ (c : ℝ) (_ : c > 0),
        ∃ (x : X), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < c * ‖x‖),
    HasEigenvalue (↑T : X →ₗ[𝕜] X) μ
⊢ ∃ c > 0, ∀ (x : X), c * ‖x‖ ≤ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X)

Tactic:
contrapose! 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‖
⊢ ∀ K > 0, ∃ (x : X), norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < K * ‖x‖

Tactic:
replace hK : ∀ K > 0, ∃ x, ‖(T - μ • 1) x‖ < K * ‖x‖ := 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‖
obtain :
  ∀ (C : 𝕜) (hC : 1 < ‖C‖),
    ∃ c > 0,
      ∀ ε > 0,
        ∃ (x : X), ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : 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:
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
μ : 𝕜
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‖
⊢ ‖C‖⁻¹ > 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‖
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‖
refine :
  ∀ (ε : ℝ) (hε : ε > 0),
    ∃ (x : X), ‖x‖ ≤ 1 ∧ ‖C‖⁻¹ ≤ ‖x‖ ∧ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : 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:
refine ⟨‖C‖⁻¹, by positivity, fun ε 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
⊢ ε > 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‖
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
obtain :
  ∀ (x : X) (hx : norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → 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) < ε
⊢ ∃ (x : X), ‖x‖ ≤ 1 ∧ ‖C‖⁻¹ ≤ ‖x‖ ∧ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < ε

Tactic:
obtain ⟨x, hx⟩ := hK ε (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‖
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‖
⊢ x ≠ 0

Tactic:
aesop
-- 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‖
⊢ x ≠ 0

Tactic:
have : x ≠ 0 := by aesop
-- 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
⊢ LT.lt (α := ℝ) 0 1

Tactic:
simp