awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Compact.Basic (hypothesis)
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
M₁ : Type u_3
M₂ : Type u_4
inst_3 : TopologicalSpace M₁
inst_4 : AddCommGroup M₁
inst_5 : TopologicalSpace M₂
inst_6 : AddCommGroup M₂
inst_7 : Module 𝕜₁ M₁
inst_8 : Module 𝕜₂ M₂
inst_9 : IsTopologicalAddGroup M₁
inst_10 : ContinuousConstSMul 𝕜₁ M₁
inst_11 : IsTopologicalAddGroup M₂
inst_12 : ContinuousSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
U : Set M₂
hU : Membership.mem (γ := Filter M₂) (𝓝 0) U
K : Set M₂
hK : IsCompact K
hKf : Membership.mem (γ := Filter M₁) (𝓝 0) ((⇑f : (a : M₁) → M₂) ⁻¹' K)
r : ℝ
hr : r > 0
hrU : ∀ (c : 𝕜₂), r ≤ ‖c‖ → K ⊆ c • U
c : 𝕜₁
hc : r < ‖c‖
hcnz : c ≠ 0
this : HSMul.hSMul.{u_2, u_4, u_4} (α := 𝕜₂) ((σ₁₂ : (a : 𝕜₁) → 𝕜₂) c⁻¹ : 𝕜₂) K ⊆ U
⊢ Membership.mem (γ := Filter M₂) (map.{u_3, u_4} (α := M₁) (⇑f : (a : M₁) → M₂) (𝓝 0))
    (HSMul.hSMul.{u_2, u_4, u_4} (α := 𝕜₂) ((σ₁₂ : (a : 𝕜₁) → 𝕜₂) c⁻¹ : 𝕜₂) K)
have this₁ : IsUnit c⁻¹
Tactic: have : IsUnit c⁻¹ := hcnz.isUnit.inv
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Compact.Basic (goal)
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
M₁ : Type u_3
M₂ : Type u_4
inst_3 : TopologicalSpace M₁
inst_4 : AddCommGroup M₁
inst_5 : TopologicalSpace M₂
inst_6 : AddCommGroup M₂
inst_7 : Module 𝕜₁ M₁
inst_8 : Module 𝕜₂ M₂
inst_9 : IsTopologicalAddGroup M₁
inst_10 : ContinuousConstSMul 𝕜₁ M₁
inst_11 : IsTopologicalAddGroup M₂
inst_12 : ContinuousSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
U : Set M₂
hU : Membership.mem (γ := Filter M₂) (𝓝 0) U
K : Set M₂
hK : IsCompact K
hKf : Membership.mem (γ := Filter M₁) (𝓝 0) ((⇑f : (a : M₁) → M₂) ⁻¹' K)
r : ℝ
hr : r > 0
hrU : ∀ (c : 𝕜₂), r ≤ ‖c‖ → K ⊆ c • U
c : 𝕜₁
hc : r < ‖c‖
hcnz : c ≠ 0
this_1 : HSMul.hSMul.{u_2, u_4, u_4} (α := 𝕜₂) ((σ₁₂ : (a : 𝕜₁) → 𝕜₂) c⁻¹ : 𝕜₂) K ⊆ U
this : IsUnit c⁻¹
⊢ Membership.mem (γ := Filter M₂) (map.{u_3, u_4} (α := M₁) (⇑f : (a : M₁) → M₂) (𝓝 0))
    (HSMul.hSMul.{u_2, u_4, u_4} (α := 𝕜₂) ((σ₁₂ : (a : 𝕜₁) → 𝕜₂) c⁻¹ : 𝕜₂) K)
have rwa : Membership.mem (γ := Filter M₁) (𝓝 0)
  ((⇑f : (a : M₁) → M₂) ⁻¹' HSMul.hSMul.{u_2, u_4, u_4} (α := 𝕜₂) ((σ₁₂ : (a : 𝕜₁) → 𝕜₂) c⁻¹ : 𝕜₂) K)
Tactic: rwa [mem_map, this.preimage_smul_setₛₗ σ₁₂, set_smul_mem_nhds_zero_iff (inv_ne_zero hcnz)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Compact.Basic (goal)
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
M₁ : Type u_3
M₂ : Type u_4
inst_3 : TopologicalSpace M₁
inst_4 : AddCommGroup M₁
inst_5 : TopologicalSpace M₂
inst_6 : AddCommGroup M₂
inst_7 : Module 𝕜₁ M₁
inst_8 : Module 𝕜₂ M₂
inst_9 : IsTopologicalAddGroup M₁
inst_10 : ContinuousConstSMul 𝕜₁ M₁
inst_11 : IsTopologicalAddGroup M₂
inst_12 : ContinuousSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
U : Set M₂
hU : Membership.mem (γ := Filter M₂) (𝓝 0) U
K : Set M₂
hK : IsCompact K
hKf : Membership.mem (γ := Filter M₁) (𝓝 0) ((⇑f : (a : M₁) → M₂) ⁻¹' K)
r : ℝ
hr : r > 0
hrU : ∀ (c : 𝕜₂), r ≤ ‖c‖ → K ⊆ c • U
c : 𝕜₁
hc : r < ‖c‖
hcnz : c ≠ 0
this_1 : HSMul.hSMul.{u_2, u_4, u_4} (α := 𝕜₂) ((σ₁₂ : (a : 𝕜₁) → 𝕜₂) c⁻¹ : 𝕜₂) K ⊆ U
this : IsUnit c⁻¹
rwa :
  Membership.mem (γ := Filter M₁) (𝓝 0)
    ((⇑f : (a : M₁) → M₂) ⁻¹' HSMul.hSMul.{u_2, u_4, u_4} (α := 𝕜₂) ((σ₁₂ : (a : 𝕜₁) → 𝕜₂) c⁻¹ : 𝕜₂) K)
⊢ Membership.mem (γ := Filter M₂) (map.{u_3, u_4} (α := M₁) (⇑f : (a : M₁) → M₂) (𝓝 0))
    (HSMul.hSMul.{u_2, u_4, u_4} (α := 𝕜₂) ((σ₁₂ : (a : 𝕜₁) → 𝕜₂) c⁻¹ : 𝕜₂) K)
have rwa₁ : Membership.mem (γ := Filter M₁) (𝓝 0) (HSMul.hSMul (β := Set M₁) c⁻¹ ((⇑f : (a : M₁) → M₂) ⁻¹' K))
Tactic: rwa [mem_map, this.preimage_smul_setₛₗ σ₁₂, set_smul_mem_nhds_zero_iff (inv_ne_zero hcnz)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Compact.Basic (goal)
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
M₁ : Type u_3
M₂ : Type u_4
inst_3 : TopologicalSpace M₁
inst_4 : AddCommGroup M₁
inst_5 : TopologicalSpace M₂
inst_6 : AddCommGroup M₂
inst_7 : Module 𝕜₁ M₁
inst_8 : Module 𝕜₂ M₂
inst_9 : IsTopologicalAddGroup M₁
inst_10 : ContinuousConstSMul 𝕜₁ M₁
inst_11 : IsTopologicalAddGroup M₂
inst_12 : ContinuousSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
U : Set M₂
hU : Membership.mem (γ := Filter M₂) (𝓝 0) U
K : Set M₂
hK : IsCompact K
hKf : Membership.mem (γ := Filter M₁) (𝓝 0) ((⇑f : (a : M₁) → M₂) ⁻¹' K)
r : ℝ
hr : r > 0
hrU : ∀ (c : 𝕜₂), r ≤ ‖c‖ → K ⊆ c • U
c : 𝕜₁
hc : r < ‖c‖
hcnz : c ≠ 0
⊢ Membership.mem (γ := Filter M₂) (map.{u_3, u_4} (α := M₁) (⇑f : (a : M₁) → M₂) (𝓝 0)) U
have suffices : HSMul.hSMul.{u_2, u_4, u_4} (α := 𝕜₂) ((σ₁₂ : (a : 𝕜₁) → 𝕜₂) c⁻¹ : 𝕜₂) K ⊆ U
Tactic: suffices (σ₁₂ <| c⁻¹) • K ⊆ U by
    grw [← this]
    have : IsUnit c⁻¹ := hcnz.isUnit.inv
    rwa [mem_map, this.preimage_smul_setₛₗ σ₁₂, set_smul_mem_nhds_zero_iff (inv_ne_zero hcnz)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Compact.Basic (goal)
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
M₁ : Type u_3
M₂ : Type u_4
inst_3 : TopologicalSpace M₁
inst_4 : AddCommGroup M₁
inst_5 : TopologicalSpace M₂
inst_6 : AddCommGroup M₂
inst_7 : Module 𝕜₁ M₁
inst_8 : Module 𝕜₂ M₂
inst_9 : IsTopologicalAddGroup M₁
inst_10 : ContinuousConstSMul 𝕜₁ M₁
inst_11 : IsTopologicalAddGroup M₂
inst_12 : ContinuousSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
U : Set M₂
hU : Membership.mem (γ := Filter M₂) (𝓝 0) U
K : Set M₂
hK : IsCompact K
hKf : Membership.mem (γ := Filter M₁) (𝓝 0) ((⇑f : (a : M₁) → M₂) ⁻¹' K)
r : ℝ
hr : r > 0
hrU : ∀ (c : 𝕜₂), r ≤ ‖c‖ → K ⊆ c • U
c : 𝕜₁
hc : r < ‖c‖
hcnz : c ≠ 0
⊢ HSMul.hSMul.{u_2, u_4, u_4} (α := 𝕜₂) ((σ₁₂ : (a : 𝕜₁) → 𝕜₂) c⁻¹ : 𝕜₂) K ⊆ U
have rw : K ⊆ HSMul.hSMul.{u_2, u_4, u_4} (α := 𝕜₂) ((σ₁₂ : (a : 𝕜₁) → 𝕜₂) c : 𝕜₂) U
Tactic: rw [map_inv₀, ← subset_smul_set_iff₀ ((map_ne_zero σ₁₂).mpr hcnz)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Compact.Basic (goal)
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
M₁ : Type u_3
M₂ : Type u_4
inst_3 : TopologicalSpace M₁
inst_4 : AddCommGroup M₁
inst_5 : TopologicalSpace M₂
inst_6 : AddCommGroup M₂
inst_7 : Module 𝕜₁ M₁
inst_8 : Module 𝕜₂ M₂
inst_9 : IsTopologicalAddGroup M₁
inst_10 : ContinuousConstSMul 𝕜₁ M₁
inst_11 : IsTopologicalAddGroup M₂
inst_12 : ContinuousSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
U : Set M₂
hU : Membership.mem (γ := Filter M₂) (𝓝 0) U
K : Set M₂
hK : IsCompact K
hKf : Membership.mem (γ := Filter M₁) (𝓝 0) ((⇑f : (a : M₁) → M₂) ⁻¹' K)
r : ℝ
hr : r > 0
hrU : ∀ (c : 𝕜₂), r ≤ ‖c‖ → K ⊆ c • U
c : 𝕜₁
hc : r < ‖c‖
hcnz : c ≠ 0
⊢ K ⊆ HSMul.hSMul.{u_2, u_4, u_4} (α := 𝕜₂) ((σ₁₂ : (a : 𝕜₁) → 𝕜₂) c : 𝕜₂) U
have refine : r ≤ norm.{u_2} (E := 𝕜₂) ((σ₁₂ : (a : 𝕜₁) → 𝕜₂) c : 𝕜₂)
Tactic: refine hrU (σ₁₂ c) ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Compact.Basic (goal)
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
M₁ : Type u_3
M₂ : Type u_4
inst_3 : TopologicalSpace M₁
inst_4 : AddCommGroup M₁
inst_5 : TopologicalSpace M₂
inst_6 : AddCommGroup M₂
inst_7 : Module 𝕜₁ M₁
inst_8 : Module 𝕜₂ M₂
inst_9 : IsTopologicalAddGroup M₁
inst_10 : ContinuousConstSMul 𝕜₁ M₁
inst_11 : IsTopologicalAddGroup M₂
inst_12 : ContinuousSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
U : Set M₂
hU : Membership.mem (γ := Filter M₂) (𝓝 0) U
K : Set M₂
hK : IsCompact K
hKf : Membership.mem (γ := Filter M₁) (𝓝 0) ((⇑f : (a : M₁) → M₂) ⁻¹' K)
r : ℝ
hr : r > 0
hrU : ∀ (c : 𝕜₂), r ≤ ‖c‖ → K ⊆ c • U
c : 𝕜₁
hc : r < ‖c‖
hcnz : c ≠ 0
⊢ r ≤ norm.{u_2} (E := 𝕜₂) ((σ₁₂ : (a : 𝕜₁) → 𝕜₂) c : 𝕜₂)
have rw : r ≤ ‖c‖
Tactic: rw [RingHomIsometric.norm_map]
-- 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₂
⊢ IsClosed[ContinuousLinearMap.topologicalSpace]
    {f : M₁ →SL[σ₁₂] M₂ | IsCompactOperator.{u_3, u_4} (M₁ := M₁) (M₂ := M₂) (⇑f : (a : M₁) → M₂)}
have refine : Subset (α := Set (M₁ →SL[σ₁₂] M₂))
  (closure[ContinuousLinearMap.topologicalSpace]
    {f : M₁ →SL[σ₁₂] M₂ | IsCompactOperator.{u_3, u_4} (M₁ := M₁) (M₂ := M₂) (⇑f : (a : M₁) → M₂)})
  {f : M₁ →SL[σ₁₂] M₂ | IsCompactOperator.{u_3, u_4} (M₁ := M₁) (M₂ := M₂) (⇑f : (a : M₁) → M₂)}
Tactic: refine isClosed_of_closure_subset ?_
-- 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 :
  Membership.mem (γ := Set (M₁ →SL[σ₁₂] M₂))
    (closure[ContinuousLinearMap.topologicalSpace]
      {f : M₁ →SL[σ₁₂] M₂ | IsCompactOperator.{u_3, u_4} (M₁ := M₁) (M₂ := M₂) (⇑f : (a : M₁) → M₂)})
    u
⊢ Membership.mem (γ := Set (M₁ →SL[σ₁₂] M₂))
    {f : M₁ →SL[σ₁₂] M₂ | IsCompactOperator.{u_3, u_4} (M₁ := M₁) (M₂ := M₂) (⇑f : (a : M₁) → M₂)} u
have 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
Tactic: rw [mem_closure_iff_nhds_zero] at hu
Cleared hypotheses: hu
-- 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
this : 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
have change : IsCompactOperator.{u_3, u_4} (M₁ := M₁) (M₂ := M₂) (⇑(↑u : M₁ →ₛₗ[σ₁₂] M₂) : (a : M₁) → M₂)
Tactic: change IsCompactOperator (u : M₁ →ₛₗ[σ₁₂] M₂)
-- 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
this : TotallyBounded.{u_4} (α := M₂) (image.{u_3, u_4} (α := M₁) (⇑u : (a : M₁) → M₂) (closedBall 0 1))
⊢ IsCompactOperator.{u_3, u_4} (M₁ := M₁) (M₂ := M₂) (⇑(↑u : M₁ →ₛₗ[σ₁₂] M₂) : (a : M₁) → M₂)
have rw : IsCompact.{u_4} (X := M₂)
  (closure[inst_6.toTopologicalSpace]
    (image.{u_3, u_4} (α := M₁) (⇑(↑u : M₁ →ₛₗ[σ₁₂] M₂) : (a : M₁) → M₂) (closedBall 0 1)))
Tactic: rw [isCompactOperator_iff_isCompact_closure_image_closedBall (u : M₁ →ₛₗ[σ₁₂] M₂) zero_lt_one]
-- 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
⊢ Membership.mem (γ := Set (M₁ →SL[σ₁₂] M₂))
    {f : M₁ →SL[σ₁₂] M₂ | IsCompactOperator.{u_3, u_4} (M₁ := M₁) (M₂ := M₂) (⇑f : (a : M₁) → M₂)} u
have suffices : TotallyBounded.{u_4} (α := M₂) (image.{u_3, u_4} (α := M₁) (⇑u : (a : M₁) → M₂) (closedBall 0 1))
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
-- 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
⊢ TotallyBounded.{u_4} (α := M₂) (image.{u_3, u_4} (α := M₁) (⇑u : (a : M₁) → M₂) (closedBall 0 1))
have 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)
Tactic: rw [totallyBounded_iff_subset_finite_iUnion_nhds_zero]
-- 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
⊢ ∃ (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)
have 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)
Tactic: rcases exists_nhds_zero_half hU with ⟨V, hV, hVU⟩
-- 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)
⊢ ∃ (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)
have 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)
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⟩
-- 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₂),
    t.Finite ∧
      Subset.{u_4} (α := Set M₂) (image.{u_3, u_4} (α := M₁) (⇑u : (a : M₁) → M₂) (closedBall 0 1)) (⋃ y ∈ t, y +ᵥ U)
have 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)
Tactic: rcases totallyBounded_iff_subset_finite_iUnion_nhds_zero.mp
      (hv.isCompact_closure_image_closedBall 1).totallyBounded V hV with
    ⟨T, hT, 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 :
  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)
have hTv₁ : 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
-- 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)
⊢ ∃ (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)
have refine : 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, ?_⟩