awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Compact.Basic (goal)
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_1 :
  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)
hTv : Subset.{u_4} (α := Set M₂) (image.{u_3, u_4} (α := M₁) (⇑v : (a : M₁) → M₂) (closedBall 0 1)) (⋃ y ∈ T, y +ᵥ V)
⊢ Subset.{u_4} (α := Set M₂) (image.{u_3, u_4} (α := M₁) (⇑u : (a : M₁) → M₂) (closedBall 0 1)) (⋃ y ∈ T, y +ᵥ U)
have rw : ∀ (hTv : Subset.{u_3} (α := Set M₁) (closedBall 0 1) (⋃ i ∈ T, (⇑v : (a : M₁) → M₂) ⁻¹' (i +ᵥ V))),
  Subset.{u_3} (α := Set M₁) (closedBall 0 1) (⋃ i ∈ T, (⇑u : (a : M₁) → M₂) ⁻¹' (i +ᵥ U))
Tactic: rw [image_subset_iff, preimage_iUnion₂] at hTv ⊢
Cleared hypotheses: hTv
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Compact.Basic (hypothesis)
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_1 :
  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)
hTv : Subset.{u_3} (α := Set M₁) (closedBall 0 1) (⋃ i ∈ T, (⇑v : (a : M₁) → M₂) ⁻¹' (i +ᵥ V))
x : M₁
hx : Membership.mem (γ := Set M₁) (closedBall 0 1) x
⊢ Membership.mem (γ := Set M₁) (⋃ i ∈ T, (⇑u : (a : M₁) → M₂) ⁻¹' (i +ᵥ U)) x
have hTv₁ : Membership.mem (γ := Set M₁) (⋃ i ∈ T, (⇑v : (a : M₁) → M₂) ⁻¹' (i +ᵥ V)) x
Tactic: specialize hTv hx
Cleared hypotheses: hTv
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Compact.Basic (goal)
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_1 :
  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
hTv : Membership.mem (γ := Set M₁) (⋃ i ∈ T, (⇑v : (a : M₁) → M₂) ⁻¹' (i +ᵥ V)) x
⊢ Membership.mem (γ := Set M₁) (⋃ i ∈ T, (⇑u : (a : M₁) → M₂) ⁻¹' (i +ᵥ U)) x
have rw : ∀ (hTv : ∃ (i : M₂) (_ : i ∈ T), Membership.mem (γ := Set M₁) ((⇑v : (a : M₁) → M₂) ⁻¹' (i +ᵥ V)) x),
  ∃ (i : M₂) (_ : i ∈ T), Membership.mem (γ := Set M₁) ((⇑u : (a : M₁) → M₂) ⁻¹' (i +ᵥ U)) x
Tactic: rw [mem_iUnion₂] at hTv ⊢
Cleared hypotheses: hTv
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Compact.Basic (goal)
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_1 :
  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
hTv : ∃ (i : M₂) (_ : i ∈ T), Membership.mem (γ := Set M₁) ((⇑v : (a : M₁) → M₂) ⁻¹' (i +ᵥ V)) x
⊢ ∃ (i : M₂) (_ : i ∈ T), Membership.mem (γ := Set M₁) ((⇑u : (a : M₁) → M₂) ⁻¹' (i +ᵥ U)) x
have rcases : ∀ (t : M₂) (ht : t ∈ T) (htx : Membership.mem (γ := Set M₁) ((⇑v : (a : M₁) → M₂) ⁻¹' (t +ᵥ V)) x),
  ∃ (i : M₂) (_ : i ∈ T), Membership.mem (γ := Set M₁) ((⇑u : (a : M₁) → M₂) ⁻¹' (i +ᵥ U)) x
Tactic: rcases hTv with ⟨t, ht, htx⟩
Cleared hypotheses: hTv
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Compact.Basic (goal)
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
⊢ ∃ (i : M₂) (_ : i ∈ T), Membership.mem (γ := Set M₁) ((⇑u : (a : M₁) → M₂) ⁻¹' (i +ᵥ U)) x
have refine : Membership.mem (γ := Set M₁) ((⇑u : (a : M₁) → M₂) ⁻¹' (t +ᵥ U)) x
Tactic: refine ⟨t, ht, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Compact.Basic (goal)
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
⊢ Membership.mem (γ := Set M₁) ((⇑u : (a : M₁) → M₂) ⁻¹' (t +ᵥ U)) x
have rw : ∀ (htx : HSub.hSub (α := M₂) ((v : (a : M₁) → M₂) x : M₂) t ∈ V), HSub.hSub (α := M₂) ((u : (a : M₁) → M₂) x : M₂) t ∈ U
Tactic: rw [mem_preimage, mem_vadd_set_iff_neg_vadd_mem, vadd_eq_add, neg_add_eq_sub] at htx ⊢
Cleared hypotheses: htx
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Compact.Basic (goal)
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 ∈ U
have 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₂)
Tactic: convert! hVU _ htx _ (huv x hx) using 1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Compact.Basic (goal)
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 =
    HAdd.hAdd (β := M₂) (HSub.hSub (α := M₂) ((v : (a : M₁) → M₂) x : M₂) t) (-(v - u : (a : M₁) → M₂) x : M₂)
have 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₂)
Tactic: rw [ContinuousLinearMap.sub_apply]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Compact.FiniteDimension (hypothesis)
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
⊢ FiniteDimensional 𝕜 E
have this : LocallyCompactSpace E
Tactic: have := LocallyCompactSpace.of_isCompactOperator_id 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
μ : 𝕜
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h : ¬HasEigenvalue (↑T : X →ₗ[𝕜] X) μ
⊢ ∃ (K : NNReal), AntilipschitzWith (α := X) (β := X) K (⇑(T - HSMul.hSMul (β := X →L[𝕜] X) μ 1) : (a : X) → X)
have rw : ∃ c > 0, ∀ (x : X), c * ‖x‖ ≤ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X)
Tactic: rw [antilipschitzWith_iff_exists_mul_le_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
μ : 𝕜
hT : IsCompactOperator (M₁ := X) (M₂ := X) (⇑T : (a : X) → X)
hμ : μ ≠ 0
h : ¬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)
have 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) μ
Tactic: contrapose! h
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
μ : 𝕜
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) < ε
have 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) < ε
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
μ : 𝕜
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,
    ∀ ε > 0,
      ∃ (x : X), ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < ε
have refine : ∀ (ε : ℝ) (hε : ε > 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ε ↦ ?_⟩
-- 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
μ : 𝕜
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), ‖x‖ ≤ 1 ∧ ‖C‖⁻¹ ≤ ‖x‖ ∧ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < ε
have 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) < ε
Tactic: obtain ⟨x, hx⟩ := hK ε (by positivity)
-- 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
μ : 𝕜
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 : X), ‖x‖ ≤ 1 ∧ ‖C‖⁻¹ ≤ ‖x‖ ∧ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < ε
have this : x ≠ 0
Tactic: have : x ≠ 0 := by aesop
-- 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
μ : 𝕜
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
⊢ ∃ (x : X), ‖x‖ ≤ 1 ∧ ‖C‖⁻¹ ≤ ‖x‖ ∧ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < ε
have 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) < ε
Tactic: obtain ⟨η, hη, h₁, h₂, h₃⟩ := rescale_to_shell hC (ε := 1) (by simp) 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
μ : 𝕜
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 : X), ‖x‖ ≤ 1 ∧ ‖C‖⁻¹ ≤ ‖x‖ ∧ norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) x : X) < ε
have refine : norm (E := X) ((T - HSMul.hSMul (β := X →L[𝕜] X) μ 1 : (a : X) → X) (η • x) : X) < ε
Tactic: refine ⟨η • x, h₁.le, by simpa using h₂, ?_⟩