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 : 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)
rcases :
  ∀ (r : ℝ) (hr : r > 0) (hrU : ∀ (c : 𝕜₂), r ≤ ‖c‖ → K ⊆ c • U),
    Membership.mem (γ := Filter M₂) (map.{u_3, u_4} (α := M₁) (⇑f : (a : M₁) → M₂) (𝓝 0)) U
⊢ Membership.mem (γ := Filter M₂) (map.{u_3, u_4} (α := M₁) (⇑f : (a : M₁) → M₂) (𝓝 0)) U

Tactic:
rcases (hK.isVonNBounded 𝕜₂ hU).exists_pos with ⟨r, hr, hrU⟩

Premises used: IsCompact.isVonNBounded, Absorbs.exists_pos
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
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
rcases :
  ∀ (c : 𝕜₁) (hc : r < ‖c‖), Membership.mem (γ := Filter M₂) (map.{u_3, u_4} (α := M₁) (⇑f : (a : M₁) → M₂) (𝓝 0)) U
⊢ Membership.mem (γ := Filter M₂) (map.{u_3, u_4} (α := M₁) (⇑f : (a : M₁) → M₂) (𝓝 0)) U

Tactic:
rcases NormedField.exists_lt_norm 𝕜₁ r with ⟨c, hc⟩

Premises used: NormedField.exists_lt_norm
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
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‖
⊢ c ≠ 0

Tactic:
have hcnz : c ≠ 0 := ne_zero_of_norm_ne_zero (hr.trans hc).ne.symm
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
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
grw :
  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)
⊢ Membership.mem (γ := Filter M₂) (map.{u_3, u_4} (α := M₁) (⇑f : (a : M₁) → M₂) (𝓝 0)) U

Tactic:
grw [← this]
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
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
⊢ IsUnit c⁻¹

Tactic:
have : IsUnit c⁻¹ := hcnz.isUnit.inv
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
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)
rwa₁ : Membership.mem (γ := Filter M₁) (𝓝 0) (HSMul.hSMul (β := Set M₁) c⁻¹ ((⇑f : (a : M₁) → M₂) ⁻¹' K))
rwa₂ rwa₃ rwa₄ rwa₅ : Membership.mem (γ := Filter M₁) (𝓝 0) ((⇑f : (a : M₁) → M₂) ⁻¹' 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)

Tactic:
rwa [mem_map, this.preimage_smul_setₛₗ σ₁₂, set_smul_mem_nhds_zero_iff (inv_ne_zero hcnz)]

Premises used: set_smul_mem_nhds_zero_iff, inv_ne_zero, Filter.mem_map, IsUnit.preimage_smul_setₛₗ
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
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
suffices : 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)) 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)]
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
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
rw : K ⊆ HSMul.hSMul.{u_2, u_4, u_4} (α := 𝕜₂) ((σ₁₂ : (a : 𝕜₁) → 𝕜₂) c : 𝕜₂) U
⊢ HSMul.hSMul.{u_2, u_4, u_4} (α := 𝕜₂) ((σ₁₂ : (a : 𝕜₁) → 𝕜₂) c⁻¹ : 𝕜₂) K ⊆ U

Tactic:
rw [map_inv₀, ← subset_smul_set_iff₀ ((map_ne_zero σ₁₂).mpr hcnz)]

Premises used: Iff.mpr, map_inv₀, map_ne_zero, Set.subset_smul_set_iff₀
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
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

Tactic:
hrU (σ₁₂ c) ?_

Premises used: DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
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
refine : r ≤ norm.{u_2} (E := 𝕜₂) ((σ₁₂ : (a : 𝕜₁) → 𝕜₂) c : 𝕜₂)
⊢ K ⊆ HSMul.hSMul.{u_2, u_4, u_4} (α := 𝕜₂) ((σ₁₂ : (a : 𝕜₁) → 𝕜₂) c : 𝕜₂) U

Tactic:
refine hrU (σ₁₂ c) ?_

Premises used: DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
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
rw : r ≤ ‖c‖
⊢ r ≤ norm.{u_2} (E := 𝕜₂) ((σ₁₂ : (a : 𝕜₁) → 𝕜₂) c : 𝕜₂)

Tactic:
rw [RingHomIsometric.norm_map]

Premises used: RingHomIsometric.norm_map
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
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 ≤ ‖c‖

Tactic:
hc.le

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
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 ≤ ‖c‖

Tactic:
exact hc.le

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
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₂
hf : IsCompactOperator.{u_3, u_4} (M₁ := M₁) (M₂ := M₂) (⇑f : (a : M₁) → M₂)
⊢ (↑(mkOfIsCompactOperator hf) : M₁ →ₛₗ[σ₁₂] M₂) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
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₂
hf : IsCompactOperator.{u_3, u_4} (M₁ := M₁) (M₂ := M₂) (⇑f : (a : M₁) → M₂)
⊢ Eq (α := (a : M₁) → M₂) (⇑(mkOfIsCompactOperator hf) : (a : M₁) → M₂) (⇑f : (a : M₁) → M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
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₂
hf : IsCompactOperator.{u_3, u_4} (M₁ := M₁) (M₂ := M₂) (⇑f : (a : M₁) → M₂)
⊢ Membership.mem (γ := Submodule 𝕜₂ (M₁ →SL[σ₁₂] M₂)) (compactOperator σ₁₂ M₁ M₂ : Submodule 𝕜₂ (M₁ →SL[σ₁₂] M₂))
    (mkOfIsCompactOperator hf)

Tactic:
hf

Premises used: Set.Mem, setOf, IsCompactOperator
-- 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₂
⊢ IsClosed[ContinuousLinearMap.topologicalSpace]
    {f : M₁ →SL[σ₁₂] M₂ | IsCompactOperator.{u_3, u_4} (M₁ := M₁) (M₂ := M₂) (⇑f : (a : M₁) → M₂)}

Tactic:
isClosed_of_closure_subset ?_

Premises used: isClosed_of_closure_subset
-- 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₂
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₂)}
⊢ IsClosed[ContinuousLinearMap.topologicalSpace]
    {f : M₁ →SL[σ₁₂] M₂ | IsCompactOperator.{u_3, u_4} (M₁ := M₁) (M₂ := M₂) (⇑f : (a : M₁) → M₂)}

Tactic:
refine isClosed_of_closure_subset ?_

Premises used: isClosed_of_closure_subset
-- 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 :
  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
⊢ ∀ (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

Premises used: mem_closure_iff_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
this : TotallyBounded.{u_4} (α := M₂) (image.{u_3, u_4} (α := M₁) (⇑u : (a : M₁) → M₂) (closedBall 0 1))
change : IsCompactOperator.{u_3, u_4} (M₁ := M₁) (M₂ := M₂) (⇑(↑u : M₁ →ₛₗ[σ₁₂] M₂) : (a : M₁) → M₂)
⊢ 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:
change IsCompactOperator (u : M₁ →ₛₗ[σ₁₂] M₂)

Premises used: ContinuousLinearMap.toLinearMap, IsCompactOperator, DFunLike.coe
-- 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
this : TotallyBounded.{u_4} (α := M₂) (image.{u_3, u_4} (α := M₁) (⇑u : (a : M₁) → M₂) (closedBall 0 1))
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)))
⊢ IsCompactOperator.{u_3, u_4} (M₁ := M₁) (M₂ := M₂) (⇑(↑u : M₁ →ₛₗ[σ₁₂] M₂) : (a : M₁) → M₂)

Tactic:
rw [isCompactOperator_iff_isCompact_closure_image_closedBall (u : M₁ →ₛₗ[σ₁₂] M₂) zero_lt_one]

Premises used: ContinuousLinearMap.toLinearMap, zero_lt_one, isCompactOperator_iff_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
this : TotallyBounded.{u_4} (α := M₂) (image.{u_3, u_4} (α := M₁) (⇑u : (a : M₁) → M₂) (closedBall 0 1))
⊢ 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:
this.closure.isCompact_of_isClosed isClosed_closure

Premises used: TotallyBounded.isCompact_of_isClosed, TotallyBounded.closure, 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
this : TotallyBounded.{u_4} (α := M₂) (image.{u_3, u_4} (α := M₁) (⇑u : (a : M₁) → M₂) (closedBall 0 1))
⊢ 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:
exact this.closure.isCompact_of_isClosed isClosed_closure

Premises used: TotallyBounded.isCompact_of_isClosed, TotallyBounded.closure, isClosed_closure