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
suffices : TotallyBounded.{u_4} (α := M₂) (image.{u_3, u_4} (α := M₁) (⇑u : (a : M₁) → M₂) (closedBall 0 1))
⊢ Membership.mem (γ := Set (M₁ →SL[σ₁₂] M₂))
    {f : M₁ →SL[σ₁₂] M₂ | IsCompactOperator.{u_3, u_4} (M₁ := M₁) (M₂ := M₂) (⇑f : (a : M₁) → M₂)} u

Tactic:
suffices TotallyBounded (u '' Metric.closedBall 0 1) by
    change IsCompactOperator (u : M₁ →ₛₗ[σ₁₂] M₂)
    rw [isCompactOperator_iff_isCompact_closure_image_closedBall (u : M₁ →ₛₗ[σ₁₂] M₂) zero_lt_one]
    exact this.closure.isCompact_of_isClosed isClosed_closure
-- 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
rw :
  ∀ (U : Set M₂),
    Membership.mem (γ := Filter M₂) (𝓝 0) U →
      ∃ (t : Set M₂),
        t.Finite ∧
          Subset.{u_4} (α := Set M₂) (image.{u_3, u_4} (α := M₁) (⇑u : (a : M₁) → M₂) (closedBall 0 1))
            (⋃ y ∈ t, y +ᵥ U)
⊢ TotallyBounded.{u_4} (α := M₂) (image.{u_3, u_4} (α := M₁) (⇑u : (a : M₁) → M₂) (closedBall 0 1))

Tactic:
rw [totallyBounded_iff_subset_finite_iUnion_nhds_zero]

Premises used: totallyBounded_iff_subset_finite_iUnion_nhds_zero
-- 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
rcases :
  ∀ (V : Set M₂) (hV : Membership.mem (γ := Filter M₂) (𝓝 0) V) (hVU : ∀ v ∈ V, ∀ w ∈ V, v + w ∈ U),
    ∃ (t : Set M₂),
      t.Finite ∧
        Subset.{u_4} (α := Set M₂) (image.{u_3, u_4} (α := M₁) (⇑u : (a : M₁) → M₂) (closedBall 0 1)) (⋃ y ∈ t, y +ᵥ U)
⊢ ∃ (t : Set M₂),
    t.Finite ∧
      Subset.{u_4} (α := Set M₂) (image.{u_3, u_4} (α := M₁) (⇑u : (a : M₁) → M₂) (closedBall 0 1)) (⋃ y ∈ t, y +ᵥ U)

Tactic:
rcases exists_nhds_zero_half hU with ⟨V, hV, hVU⟩

Premises used: exists_nhds_zero_half
-- 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)
rcases :
  ∀ (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₂),
      t.Finite ∧
        Subset.{u_4} (α := Set M₂) (image.{u_3, u_4} (α := M₁) (⇑u : (a : M₁) → M₂) (closedBall 0 1)) (⋃ y ∈ t, y +ᵥ U)
⊢ ∃ (t : Set M₂),
    t.Finite ∧
      Subset.{u_4} (α := Set M₂) (image.{u_3, u_4} (α := M₁) (⇑u : (a : M₁) → M₂) (closedBall 0 1)) (⋃ y ∈ t, y +ᵥ U)

Tactic:
rcases hu { f | ∀ x ∈ SV.1, f x ∈ SV.2 }
      (ContinuousLinearMap.hasBasis_nhds_zero.mem_of_mem
        ⟨NormedSpace.isVonNBounded_closedBall _ _ _, neg_mem_nhds_zero M₂ hV⟩) with
    ⟨v, hv, huv⟩

Premises used: ContinuousLinearMap.hasBasis_nhds_zero, NormedSpace.isVonNBounded_closedBall, setOf, neg_mem_nhds_zero, And.intro, Filter.HasBasis.mem_of_mem
-- 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)
rcases :
  ∀ (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)),
    ∃ (t : Set M₂),
      t.Finite ∧
        Subset.{u_4} (α := Set M₂) (image.{u_3, u_4} (α := M₁) (⇑u : (a : M₁) → M₂) (closedBall 0 1)) (⋃ y ∈ t, y +ᵥ U)
⊢ ∃ (t : Set M₂),
    t.Finite ∧
      Subset.{u_4} (α := Set M₂) (image.{u_3, u_4} (α := M₁) (⇑u : (a : M₁) → M₂) (closedBall 0 1)) (⋃ y ∈ t, y +ᵥ U)

Tactic:
rcases totallyBounded_iff_subset_finite_iUnion_nhds_zero.mp
      (hv.isCompact_closure_image_closedBall 1).totallyBounded V hV with
    ⟨T, hT, hTv⟩

Premises used: IsCompact.totallyBounded, Iff.mp, OfNat.ofNat, totallyBounded_iff_subset_finite_iUnion_nhds_zero, IsCompactOperator.isCompact_closure_image_closedBall
-- 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)
⊢ Subset.{u_4} (α := Set M₂) (image.{u_3, u_4} (α := M₁) (⇑v : (a : M₁) → M₂) (closedBall 0 1)) (⋃ y ∈ T, y +ᵥ V)

Tactic:
have hTv : v '' closedBall 0 1 ⊆ _ := subset_closure.trans hTv
-- 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_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)
⊢ ∃ (t : Set M₂),
    t.Finite ∧
      Subset.{u_4} (α := Set M₂) (image.{u_3, u_4} (α := M₁) (⇑u : (a : M₁) → M₂) (closedBall 0 1)) (⋃ y ∈ t, y +ᵥ U)

Tactic:
⟨T, hT, ?_⟩

Premises used: And.intro, Exists.intro
-- 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_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)
refine : Subset.{u_4} (α := Set M₂) (image.{u_3, u_4} (α := M₁) (⇑u : (a : M₁) → M₂) (closedBall 0 1)) (⋃ y ∈ T, y +ᵥ U)
⊢ ∃ (t : Set M₂),
    t.Finite ∧
      Subset.{u_4} (α := Set M₂) (image.{u_3, u_4} (α := M₁) (⇑u : (a : M₁) → M₂) (closedBall 0 1)) (⋃ y ∈ t, y +ᵥ U)

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_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)
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))
⊢ Subset.{u_4} (α := Set M₂) (image.{u_3, u_4} (α := M₁) (⇑u : (a : M₁) → M₂) (closedBall 0 1)) (⋃ y ∈ T, y +ᵥ U)

Tactic:
rw [image_subset_iff, preimage_iUnion₂] at hTv ⊢

Premises used: Set.image_subset_iff, Set.preimage_iUnion₂
-- 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_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, (⇑v : (a : M₁) → M₂) ⁻¹' (i +ᵥ V)) x

Tactic:
specialize hTv 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_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
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
⊢ Membership.mem (γ := Set M₁) (⋃ i ∈ T, (⇑u : (a : M₁) → M₂) ⁻¹' (i +ᵥ U)) x

Tactic:
rw [mem_iUnion₂] at hTv ⊢

Premises used: Set.mem_iUnion₂
-- 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_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
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
⊢ ∃ (i : M₂) (_ : i ∈ T), Membership.mem (γ := Set M₁) ((⇑u : (a : M₁) → M₂) ⁻¹' (i +ᵥ U)) x

Tactic:
rcases hTv with ⟨t, ht, htx⟩
-- 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
⊢ ∃ (i : M₂) (_ : i ∈ T), Membership.mem (γ := Set M₁) ((⇑u : (a : M₁) → M₂) ⁻¹' (i +ᵥ U)) x

Tactic:
⟨t, ht, ?_⟩

Premises used: Exists.intro