awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
X : Type u_5
inst_7 : TopologicalSpace X
f : X → E →L[𝕜] G
g : X → F →L[𝕜] G
hf : Continuous[inst_7, _] f
hg : Continuous[inst_7, _] g
apply : ContinuousOn (Y := E × F →L[𝕜] G) (fun (x : X) ↦ (f x).coprod (g x)) Set.univ
⊢ Continuous[inst_7, topologicalSpace] fun (x : X) ↦ (f x).coprod (g x)

Tactic:
apply continuousOn_univ.mp

Premises used: Iff.mp, continuousOn_univ
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
X : Type u_5
inst_7 : TopologicalSpace X
f : X → E →L[𝕜] G
g : X → F →L[𝕜] G
hf : Continuous[inst_7, _] f
hg : Continuous[inst_7, _] g
⊢ ContinuousOn (Y := E × F →L[𝕜] G) (fun (x : X) ↦ (f x).coprod (g x)) Set.univ

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace E
rw : ∀ (i : E ≃L[𝕜] F), range (ι := E ≃L[𝕜] F) toContinuousLinearMap ∈ 𝓝 (↑i : E →L[𝕜] F)
⊢ IsOpen (X := E →L[𝕜] F) (range (ι := E ≃L[𝕜] F) toContinuousLinearMap)

Tactic:
rw [isOpen_iff_mem_nhds, forall_mem_range]

Premises used: Set.forall_mem_range, isOpen_iff_mem_nhds
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace E
⊢ ∀ (i : E ≃L[𝕜] F), range (ι := E ≃L[𝕜] F) toContinuousLinearMap ∈ 𝓝 (↑i : E →L[𝕜] F)

Tactic:
fun e => IsOpen.mem_nhds ?_ (mem_range_self _)

Premises used: Set.mem_range_self, IsOpen.mem_nhds
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace E
refine : ∀ (e : E ≃L[𝕜] F), IsOpen (X := E →L[𝕜] F) (range (ι := E ≃L[𝕜] F) toContinuousLinearMap)
⊢ ∀ (i : E ≃L[𝕜] F), range (ι := E ≃L[𝕜] F) toContinuousLinearMap ∈ 𝓝 (↑i : E →L[𝕜] F)

Tactic:
refine fun e => IsOpen.mem_nhds ?_ (mem_range_self _)

Premises used: Set.mem_range_self, IsOpen.mem_nhds
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace E
e : E ≃L[𝕜] F
O : (E →L[𝕜] F) → E →L[𝕜] E := fun (f : E →L[𝕜] F) ↦ (↑e.symm : F →L[𝕜] E) ∘SL f
⊢ Continuous O

Tactic:
have h_O : Continuous O := (isBoundedBilinearMap_comp (𝕜 := 𝕜) (F := F) (G := E)).continuous_right
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace E
e : E ≃L[𝕜] F
O : (E →L[𝕜] F) → E →L[𝕜] E := fun (f : E →L[𝕜] F) ↦ (↑e.symm : F →L[𝕜] E) ∘SL f
h_O : Continuous O
⊢ IsOpen (O ⁻¹' {x : E →L[𝕜] E | IsUnit x})

Tactic:
show IsOpen (O ⁻¹' {x | IsUnit x}) from Units.isOpen.preimage h_O

Premises used: Units.isOpen, IsOpen.preimage
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace E
e : E ≃L[𝕜] F
O : (E →L[𝕜] F) → E →L[𝕜] E := fun (f : E →L[𝕜] F) ↦ (↑e.symm : F →L[𝕜] E) ∘SL f
h_O : Continuous O
h : range (ι := E ≃L[𝕜] F) toContinuousLinearMap = O ⁻¹' {x : E →L[𝕜] E | IsUnit x}
⊢ IsOpen (X := E →L[𝕜] F) (range (ι := E ≃L[𝕜] F) toContinuousLinearMap)

Tactic:
convert! show IsOpen (O ⁻¹' {x | IsUnit x}) from Units.isOpen.preimage h_O using 1

Premises used: Units.isOpen, IsOpen.preimage
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace E
e : E ≃L[𝕜] F
O : (E →L[𝕜] F) → E →L[𝕜] E := fun (f : E →L[𝕜] F) ↦ (↑e.symm : F →L[𝕜] E) ∘SL f
h_O : Continuous O
h :
  ∀ (f' : E →L[𝕜] F),
    Membership.mem (γ := Set (E →L[𝕜] F)) (range (ι := E ≃L[𝕜] F) toContinuousLinearMap) f' ↔
      f' ∈ O ⁻¹' {x : E →L[𝕜] E | IsUnit x}
⊢ range (ι := E ≃L[𝕜] F) toContinuousLinearMap = O ⁻¹' {x : E →L[𝕜] E | IsUnit x}

Tactic:
ext f'
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace E
e : E ≃L[𝕜] F
O : (E →L[𝕜] F) → E →L[𝕜] E := fun (f : E →L[𝕜] F) ↦ (↑e.symm : F →L[𝕜] E) ∘SL f
h_O : Continuous O
f' : E →L[𝕜] F
h :
  Membership.mem (γ := Set (E →L[𝕜] F)) (range (ι := E ≃L[𝕜] F) toContinuousLinearMap) f' →
    f' ∈ O ⁻¹' {x : E →L[𝕜] E | IsUnit x}
h₁ :
  f' ∈ O ⁻¹' {x : E →L[𝕜] E | IsUnit x} →
    Membership.mem (γ := Set (E →L[𝕜] F)) (range (ι := E ≃L[𝕜] F) toContinuousLinearMap) f'
⊢ Membership.mem (γ := Set (E →L[𝕜] F)) (range (ι := E ≃L[𝕜] F) toContinuousLinearMap) f' ↔
    f' ∈ O ⁻¹' {x : E →L[𝕜] E | IsUnit x}

Tactic:
constructor
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace E
e : E ≃L[𝕜] F
O : (E →L[𝕜] F) → E →L[𝕜] E := fun (f : E →L[𝕜] F) ↦ (↑e.symm : F →L[𝕜] E) ∘SL f
h_O : Continuous O
e' : E ≃L[𝕜] F
⊢ (↑e' : E →L[𝕜] F) ∈ O ⁻¹' {x : E →L[𝕜] E | IsUnit x}

Tactic:
⟨(e'.trans e.symm).toUnit, rfl⟩

Premises used: ContinuousLinearEquiv.symm, Set.Mem, setOf, IsUnit, ContinuousLinearEquiv.trans, Set.preimage, Exists.intro, ContinuousLinearEquiv.toUnit, rfl
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace E
e : E ≃L[𝕜] F
O : (E →L[𝕜] F) → E →L[𝕜] E := fun (f : E →L[𝕜] F) ↦ (↑e.symm : F →L[𝕜] E) ∘SL f
h_O : Continuous O
e' : E ≃L[𝕜] F
⊢ (↑e' : E →L[𝕜] F) ∈ O ⁻¹' {x : E →L[𝕜] E | IsUnit x}

Tactic:
exact ⟨(e'.trans e.symm).toUnit, rfl⟩
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace E
e : E ≃L[𝕜] F
O : (E →L[𝕜] F) → E →L[𝕜] E := fun (f : E →L[𝕜] F) ↦ (↑e.symm : F →L[𝕜] E) ∘SL f
h_O : Continuous O
f' : E →L[𝕜] F
w : (E →L[𝕜] E)ˣ
hw : (↑w : E →L[𝕜] E) = O f'
h : (↑(ContinuousLinearEquiv.trans ((unitsEquiv 𝕜 E : (a : (E →L[𝕜] E)ˣ) → E ≃L[𝕜] E) w) e) : E →L[𝕜] F) = f'
⊢ Membership.mem (γ := Set (E →L[𝕜] F)) (range (ι := E ≃L[𝕜] F) toContinuousLinearMap) f'

Tactic:
use (unitsEquiv 𝕜 E w).trans e

Premises used: ContinuousLinearEquiv.trans, ContinuousLinearEquiv.unitsEquiv, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace E
e : E ≃L[𝕜] F
O : (E →L[𝕜] F) → E →L[𝕜] E := fun (f : E →L[𝕜] F) ↦ (↑e.symm : F →L[𝕜] E) ∘SL f
h_O : Continuous O
f' : E →L[𝕜] F
w : (E →L[𝕜] E)ˣ
hw : (↑w : E →L[𝕜] E) = O f'
h :
  ∀ (x : E),
    Eq.{u_3 + 1} (α := F)
      (((↑(ContinuousLinearEquiv.trans ((unitsEquiv 𝕜 E : (a : (E →L[𝕜] E)ˣ) → E ≃L[𝕜] E) w) e) : E →L[𝕜] F) :
            (a : E) → F)
          x :
        F)
      ((f' : (a : E) → F) x : F)
⊢ (↑(ContinuousLinearEquiv.trans ((unitsEquiv 𝕜 E : (a : (E →L[𝕜] E)ˣ) → E ≃L[𝕜] E) w) e) : E →L[𝕜] F) = f'

Tactic:
ext x
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace E
e : E ≃L[𝕜] F
O : (E →L[𝕜] F) → E →L[𝕜] E := fun (f : E →L[𝕜] F) ↦ (↑e.symm : F →L[𝕜] E) ∘SL f
h_O : Continuous O
f' : E →L[𝕜] F
w : (E →L[𝕜] E)ˣ
hw : (↑w : E →L[𝕜] E) = O f'
x : E
⊢ Eq.{u_3 + 1} (α := F)
    (((↑(ContinuousLinearEquiv.trans ((unitsEquiv 𝕜 E : (a : (E →L[𝕜] E)ˣ) → E ≃L[𝕜] E) w) e) : E →L[𝕜] F) :
          (a : E) → F)
        x :
      F)
    ((f' : (a : E) → F) x : F)

Tactic:
simp [O, hw]
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace E
e : E ≃L[𝕜] F
⊢ Membership.mem (γ := Set (E →L[𝕜] F)) (range (ι := E ≃L[𝕜] F) toContinuousLinearMap) (↑e : E →L[𝕜] F)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Zero M₁
inst_1 : TopologicalSpace M₁
inst_2 : TopologicalSpace M₂
inst_3 : Zero M₂
⊢ IsCompactOperator.{u_1, u_2} (M₁ := M₁) (M₂ := M₂) 0

Tactic:
⟨{0}, isCompact_singleton, mem_of_superset univ_mem fun _ _ => rfl⟩

Premises used: isCompact_singleton, And.intro, Exists.intro, Filter.univ_mem, IsCompactOperator, Singleton.singleton, OfNat.ofNat, rfl, Filter.mem_of_superset
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
Goal:
E : Type u_1
inst : AddGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
⊢ IsCompactOperator.{u_1, u_1} (M₁ := E) id ↔ LocallyCompactSpace E

Tactic:
⟨fun ⟨_, hK, hK0⟩ ↦ hK.locallyCompactSpace_of_mem_nhds_of_addGroup hK0,
    fun _ ↦ exists_compact_mem_nhds 0⟩

Premises used: WeaklyLocallyCompactSpace.exists_compact_mem_nhds, Iff.intro, _private.0.isCompactOperator_id_iff_locallyCompactSpace.match_1, IsCompact.locallyCompactSpace_of_mem_nhds_of_addGroup, OfNat.ofNat, LocallyCompactSpace
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
Goal:
E : Type u_1
inst : AddGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : LocallyCompactSpace E
⊢ IsCompactOperator.{u_1, u_1} (M₁ := E) id

Tactic:
isCompactOperator_id_iff_locallyCompactSpace.2 ‹_›

Premises used: Iff.mpr, isCompactOperator_id_iff_locallyCompactSpace
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
Goal:
M₁ : Type u_2
M₂ : Type u_3
inst : TopologicalSpace M₁
inst_1 : AddCommMonoid M₁
inst_2 : TopologicalSpace M₂
f : M₁ → M₂
⊢ IsCompactOperator f ↔
    ∃ (V : Set M₁), Membership.mem (γ := Filter M₁) (𝓝 0) V ∧ ∃ (K : Set M₂), IsCompact K ∧ f '' V ⊆ K

Tactic:
⟨fun ⟨K, hK, hKf⟩ => ⟨f ⁻¹' K, hKf, K, hK, image_preimage_subset _ _⟩, fun ⟨_, hV, K, hK, hVK⟩ =>
    ⟨K, hK, mem_of_superset hV (image_subset_iff.mp hVK)⟩⟩

Premises used: _private.0.isCompactOperator_iff_exists_mem_nhds_image_subset_compact.match_1, _private.0.isCompactOperator_iff_exists_mem_nhds_image_subset_compact.match_2, Membership.mem, Exists, nhds, HasSubset.Subset, And, Set.preimage, And.intro, Iff.intro, Set.image_preimage_subset, Exists.intro, Iff.mp, Set.image, Set.image_subset_iff, IsCompactOperator, OfNat.ofNat, IsCompact, Filter.mem_of_superset
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
Goal:
M₁ : Type u_2
M₂ : Type u_3
inst : TopologicalSpace M₁
inst_1 : AddCommMonoid M₁
inst_2 : TopologicalSpace M₂
inst_3 : T2Space M₂
f : M₁ → M₂
rw :
  (∃ (V : Set M₁), Membership.mem (γ := Filter M₁) (𝓝 0) V ∧ ∃ (K : Set M₂), IsCompact K ∧ f '' V ⊆ K) ↔
    ∃ (V : Set M₁), Membership.mem (γ := Filter M₁) (𝓝 0) V ∧ IsCompact (closure[inst_2] (f '' V))
⊢ IsCompactOperator f ↔ ∃ (V : Set M₁), Membership.mem (γ := Filter M₁) (𝓝 0) V ∧ IsCompact (closure[inst_2] (f '' V))

Tactic:
rw [isCompactOperator_iff_exists_mem_nhds_image_subset_compact]

Premises used: isCompactOperator_iff_exists_mem_nhds_image_subset_compact
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
Goal:
M₁ : Type u_2
M₂ : Type u_3
inst : TopologicalSpace M₁
inst_1 : AddCommMonoid M₁
inst_2 : TopologicalSpace M₂
inst_3 : T2Space M₂
f : M₁ → M₂
⊢ (∃ (V : Set M₁), Membership.mem (γ := Filter M₁) (𝓝 0) V ∧ ∃ (K : Set M₂), IsCompact K ∧ f '' V ⊆ K) ↔
    ∃ (V : Set M₁), Membership.mem (γ := Filter M₁) (𝓝 0) V ∧ IsCompact (closure[inst_2] (f '' V))

Tactic:
⟨fun ⟨V, hV, K, hK, hKV⟩ => ⟨V, hV, hK.closure_of_subset hKV⟩,
      fun ⟨V, hV, hVc⟩ => ⟨V, hV, closure (f '' V), hVc, subset_closure⟩⟩

Premises used: _private.0.isCompactOperator_iff_exists_mem_nhds_isCompact_closure_image.match_2, _private.0.isCompactOperator_iff_exists_mem_nhds_isCompact_closure_image.match_1, subset_closure, Membership.mem, Exists, nhds, HasSubset.Subset, And, closure, And.intro, Iff.intro, Exists.intro, Set.image, OfNat.ofNat, IsCompact.closure_of_subset, IsCompact
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
Goal:
M₁ : Type u_2
M₂ : Type u_3
inst : TopologicalSpace M₁
inst_1 : AddCommMonoid M₁
inst_2 : TopologicalSpace M₂
inst_3 : T2Space M₂
f : M₁ → M₂
⊢ (∃ (V : Set M₁), Membership.mem (γ := Filter M₁) (𝓝 0) V ∧ ∃ (K : Set M₂), IsCompact K ∧ f '' V ⊆ K) ↔
    ∃ (V : Set M₁), Membership.mem (γ := Filter M₁) (𝓝 0) V ∧ IsCompact (closure[inst_2] (f '' V))

Tactic:
exact
    ⟨fun ⟨V, hV, K, hK, hKV⟩ => ⟨V, hV, hK.closure_of_subset hKV⟩,
      fun ⟨V, hV, hVc⟩ => ⟨V, hV, closure (f '' V), hVc, subset_closure⟩⟩
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NontriviallyNormedField 𝕜₁
inst_1 : SeminormedRing 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module 𝕜₁ M₁
inst_7 : Module 𝕜₂ M₂
inst_8 : ContinuousConstSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
hf : IsCompactOperator.{u_3, u_4} (M₁ := M₁) (M₂ := M₂) (⇑f : (a : M₁) → M₂)
S : Set M₁
hS : IsVonNBounded 𝕜₁ S
K : Set M₂
hK : IsCompact K
hKf : Membership.mem (γ := Filter M₁) (𝓝 0) ((⇑f : (a : M₁) → M₂) ⁻¹' K)
r : ℝ
hr : r > 0
hrS : ∀ (c : 𝕜₁), r ≤ ‖c‖ → S ⊆ HSMul.hSMul (β := Set M₁) c ((⇑f : (a : M₁) → M₂) ⁻¹' K)
c : 𝕜₁
hc : r < ‖c‖
this : c ≠ 0 := ⋯
rw : S ⊆ HSMul.hSMul (β := Set M₁) c ((⇑f : (a : M₁) → M₂) ⁻¹' K)
⊢ (⇑f : (a : M₁) → M₂) '' S ⊆ HSMul.hSMul.{u_2, u_4, u_4} (α := 𝕜₂) ((σ₁₂ : (a : 𝕜₁) → 𝕜₂) c : 𝕜₂) K

Tactic:
rw [image_subset_iff, this.isUnit.preimage_smul_setₛₗ σ₁₂]

Premises used: Ne.isUnit, Set.image_subset_iff, IsUnit.preimage_smul_setₛₗ
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NontriviallyNormedField 𝕜₁
inst_1 : SeminormedRing 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module 𝕜₁ M₁
inst_7 : Module 𝕜₂ M₂
inst_8 : ContinuousConstSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
hf : IsCompactOperator.{u_3, u_4} (M₁ := M₁) (M₂ := M₂) (⇑f : (a : M₁) → M₂)
S : Set M₁
hS : IsVonNBounded 𝕜₁ S
K : Set M₂
hK : IsCompact K
hKf : Membership.mem (γ := Filter M₁) (𝓝 0) ((⇑f : (a : M₁) → M₂) ⁻¹' K)
r : ℝ
hr : r > 0
hrS : ∀ (c : 𝕜₁), r ≤ ‖c‖ → S ⊆ HSMul.hSMul (β := Set M₁) c ((⇑f : (a : M₁) → M₂) ⁻¹' K)
c : 𝕜₁
hc : r < ‖c‖
this : c ≠ 0 := ⋯
⊢ S ⊆ HSMul.hSMul (β := Set M₁) c ((⇑f : (a : M₁) → M₂) ⁻¹' K)

Tactic:
hrS c 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 : SeminormedRing 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module 𝕜₁ M₁
inst_7 : Module 𝕜₂ M₂
inst_8 : ContinuousConstSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
hf : IsCompactOperator.{u_3, u_4} (M₁ := M₁) (M₂ := M₂) (⇑f : (a : M₁) → M₂)
S : Set M₁
hS : IsVonNBounded 𝕜₁ S
K : Set M₂
hK : IsCompact K
hKf : Membership.mem (γ := Filter M₁) (𝓝 0) ((⇑f : (a : M₁) → M₂) ⁻¹' K)
r : ℝ
hr : r > 0
hrS : ∀ (c : 𝕜₁), r ≤ ‖c‖ → S ⊆ HSMul.hSMul (β := Set M₁) c ((⇑f : (a : M₁) → M₂) ⁻¹' K)
c : 𝕜₁
hc : r < ‖c‖
this : c ≠ 0 := ⋯
⊢ S ⊆ HSMul.hSMul (β := Set M₁) c ((⇑f : (a : M₁) → M₂) ⁻¹' K)

Tactic:
exact hrS c 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 : SeminormedRing 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module 𝕜₁ M₁
inst_7 : Module 𝕜₂ M₂
inst_8 : ContinuousConstSMul 𝕜₂ M₂
inst_9 : T2Space M₂
f : M₁ →ₛₗ[σ₁₂] M₂
hf : IsCompactOperator.{u_3, u_4} (M₁ := M₁) (M₂ := M₂) (⇑f : (a : M₁) → M₂)
S : Set M₁
hS : IsVonNBounded 𝕜₁ S
⊢ IsCompact.{u_4} (X := M₂) (closure[inst_4] ((⇑f : (a : M₁) → M₂) '' S))

Tactic:
let ⟨_, hK, hKf⟩ := hf.image_subset_compact_of_isVonNBounded hS
  hK.closure_of_subset hKf

Premises used: IsCompactOperator.image_subset_compact_of_isVonNBounded, closure, Set.image, _private.0.IsCompactOperator.isCompact_closure_image_of_isVonNBounded.match_1, DFunLike.coe, IsCompact.closure_of_subset, IsCompact
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NontriviallyNormedField 𝕜₁
inst_1 : SeminormedRing 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst_2 : SeminormedAddCommGroup M₁
inst_3 : TopologicalSpace M₂
inst_4 : AddCommMonoid M₂
inst_5 : NormedSpace 𝕜₁ M₁
inst_6 : Module 𝕜₂ M₂
inst_7 : ContinuousConstSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
hf : IsCompactOperator.{u_3, u_4} (M₁ := M₁) (M₂ := M₂) (⇑f : (a : M₁) → M₂)
S : Set M₁
hS rwa rwa₁ rwa₂ rwa₃ : Bornology.IsBounded S
⊢ IsVonNBounded 𝕜₁ S

Tactic:
rwa [NormedSpace.isVonNBounded_iff]

Premises used: NormedSpace.isVonNBounded_iff
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NontriviallyNormedField 𝕜₁
inst_1 : SeminormedRing 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst_2 : SeminormedAddCommGroup M₁
inst_3 : TopologicalSpace M₂
inst_4 : AddCommMonoid M₂
inst_5 : NormedSpace 𝕜₁ M₁
inst_6 : Module 𝕜₂ M₂
inst_7 : ContinuousConstSMul 𝕜₂ M₂
inst_8 : T2Space M₂
f : M₁ →ₛₗ[σ₁₂] M₂
hf : IsCompactOperator.{u_3, u_4} (M₁ := M₁) (M₂ := M₂) (⇑f : (a : M₁) → M₂)
S : Set M₁
hS rwa rwa₁ rwa₂ rwa₃ : Bornology.IsBounded S
⊢ IsVonNBounded 𝕜₁ S

Tactic:
rwa [NormedSpace.isVonNBounded_iff]

Premises used: NormedSpace.isVonNBounded_iff
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NontriviallyNormedField 𝕜₁
inst_1 : SeminormedRing 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst_2 : SeminormedAddCommGroup M₁
inst_3 : TopologicalSpace M₂
inst_4 : AddCommMonoid M₂
inst_5 : NormedSpace 𝕜₁ M₁
inst_6 : Module 𝕜₂ M₂
inst_7 : ContinuousConstSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
hf : IsCompactOperator.{u_3, u_4} (M₁ := M₁) (M₂ := M₂) (⇑f : (a : M₁) → M₂)
r : ℝ
⊢ ∃ (K : Set M₂), IsCompact K ∧ image.{u_3, u_4} (α := M₁) (⇑f : (a : M₁) → M₂) (ball 0 r) ⊆ K

Tactic:
hf.image_subset_compact_of_isVonNBounded (NormedSpace.isVonNBounded_ball 𝕜₁ M₁ r)

Premises used: IsCompactOperator.image_subset_compact_of_isVonNBounded, NormedSpace.isVonNBounded_ball
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NontriviallyNormedField 𝕜₁
inst_1 : SeminormedRing 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst_2 : SeminormedAddCommGroup M₁
inst_3 : TopologicalSpace M₂
inst_4 : AddCommMonoid M₂
inst_5 : NormedSpace 𝕜₁ M₁
inst_6 : Module 𝕜₂ M₂
inst_7 : ContinuousConstSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
hf : IsCompactOperator.{u_3, u_4} (M₁ := M₁) (M₂ := M₂) (⇑f : (a : M₁) → M₂)
r : ℝ
⊢ ∃ (K : Set M₂), IsCompact K ∧ image.{u_3, u_4} (α := M₁) (⇑f : (a : M₁) → M₂) (closedBall 0 r) ⊆ K

Tactic:
hf.image_subset_compact_of_isVonNBounded (NormedSpace.isVonNBounded_closedBall 𝕜₁ M₁ r)

Premises used: IsCompactOperator.image_subset_compact_of_isVonNBounded, NormedSpace.isVonNBounded_closedBall
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NontriviallyNormedField 𝕜₁
inst_1 : SeminormedRing 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst_2 : SeminormedAddCommGroup M₁
inst_3 : TopologicalSpace M₂
inst_4 : AddCommMonoid M₂
inst_5 : NormedSpace 𝕜₁ M₁
inst_6 : Module 𝕜₂ M₂
inst_7 : ContinuousConstSMul 𝕜₂ M₂
inst_8 : T2Space M₂
f : M₁ →ₛₗ[σ₁₂] M₂
hf : IsCompactOperator.{u_3, u_4} (M₁ := M₁) (M₂ := M₂) (⇑f : (a : M₁) → M₂)
r : ℝ
⊢ IsCompact.{u_4} (X := M₂) (closure[inst_3] (image.{u_3, u_4} (α := M₁) (⇑f : (a : M₁) → M₂) (ball 0 r)))

Tactic:
hf.isCompact_closure_image_of_isVonNBounded (NormedSpace.isVonNBounded_ball 𝕜₁ M₁ r)

Premises used: NormedSpace.isVonNBounded_ball, IsCompactOperator.isCompact_closure_image_of_isVonNBounded
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NontriviallyNormedField 𝕜₁
inst_1 : SeminormedRing 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst_2 : SeminormedAddCommGroup M₁
inst_3 : TopologicalSpace M₂
inst_4 : AddCommMonoid M₂
inst_5 : NormedSpace 𝕜₁ M₁
inst_6 : Module 𝕜₂ M₂
inst_7 : ContinuousConstSMul 𝕜₂ M₂
inst_8 : T2Space M₂
f : M₁ →ₛₗ[σ₁₂] M₂
hf : IsCompactOperator.{u_3, u_4} (M₁ := M₁) (M₂ := M₂) (⇑f : (a : M₁) → M₂)
r : ℝ
⊢ IsCompact.{u_4} (X := M₂) (closure[inst_3] (image.{u_3, u_4} (α := M₁) (⇑f : (a : M₁) → M₂) (closedBall 0 r)))

Tactic:
hf.isCompact_closure_image_of_isVonNBounded (NormedSpace.isVonNBounded_closedBall 𝕜₁ M₁ r)

Premises used: NormedSpace.isVonNBounded_closedBall, IsCompactOperator.isCompact_closure_image_of_isVonNBounded
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NontriviallyNormedField 𝕜₁
inst_1 : SeminormedRing 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst_2 : SeminormedAddCommGroup M₁
inst_3 : TopologicalSpace M₂
inst_4 : AddCommMonoid M₂
inst_5 : NormedSpace 𝕜₁ M₁
inst_6 : Module 𝕜₂ M₂
inst_7 : ContinuousConstSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
r : ℝ
hr : 0 < r
⊢ IsCompactOperator.{u_3, u_4} (M₁ := M₁) (M₂ := M₂) (⇑f : (a : M₁) → M₂) ↔
    ∃ (K : Set M₂), IsCompact K ∧ image.{u_3, u_4} (α := M₁) (⇑f : (a : M₁) → M₂) (ball 0 r) ⊆ K

Tactic:
⟨fun hf => hf.image_ball_subset_compact r, fun ⟨K, hK, hKr⟩ =>
    (isCompactOperator_iff_exists_mem_nhds_image_subset_compact f).mpr
      ⟨Metric.ball 0 r, ball_mem_nhds _ hr, K, hK, hKr⟩⟩

Premises used: Iff.mpr, Metric.ball, Metric.ball_mem_nhds, _private.0.isCompactOperator_iff_image_ball_subset_compact.match_1, And.intro, Iff.intro, Exists.intro, IsCompactOperator.image_ball_subset_compact, IsCompactOperator, OfNat.ofNat, DFunLike.coe, isCompactOperator_iff_exists_mem_nhds_image_subset_compact