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 : 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₂) (closedBall 0 r) ⊆ K

Tactic:
⟨fun hf => hf.image_closedBall_subset_compact r, fun ⟨K, hK, hKr⟩ =>
    (isCompactOperator_iff_exists_mem_nhds_image_subset_compact f).mpr
      ⟨Metric.closedBall 0 r, closedBall_mem_nhds _ hr, K, hK, hKr⟩⟩

Premises used: Iff.mpr, Metric.closedBall_mem_nhds, _private.0.isCompactOperator_iff_image_closedBall_subset_compact.match_1, And.intro, Iff.intro, IsCompactOperator.image_closedBall_subset_compact, Exists.intro, Metric.closedBall, IsCompactOperator, OfNat.ofNat, DFunLike.coe, isCompactOperator_iff_exists_mem_nhds_image_subset_compact
-- 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₂
r : ℝ
hr : 0 < r
⊢ IsCompactOperator.{u_3, u_4} (M₁ := M₁) (M₂ := M₂) (⇑f : (a : M₁) → M₂) ↔
    IsCompact.{u_4} (X := M₂) (closure[inst_3] (image.{u_3, u_4} (α := M₁) (⇑f : (a : M₁) → M₂) (ball 0 r)))

Tactic:
⟨fun hf => hf.isCompact_closure_image_ball r, fun hf =>
    (isCompactOperator_iff_exists_mem_nhds_isCompact_closure_image f).mpr
      ⟨Metric.ball 0 r, ball_mem_nhds _ hr, hf⟩⟩

Premises used: Iff.mpr, Metric.ball, isCompactOperator_iff_exists_mem_nhds_isCompact_closure_image, Metric.ball_mem_nhds, And.intro, Iff.intro, Exists.intro, IsCompactOperator.isCompact_closure_image_ball, OfNat.ofNat, DFunLike.coe
-- 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₂
r : ℝ
hr : 0 < r
⊢ IsCompactOperator.{u_3, u_4} (M₁ := M₁) (M₂ := M₂) (⇑f : (a : M₁) → M₂) ↔
    IsCompact.{u_4} (X := M₂) (closure[inst_3] (image.{u_3, u_4} (α := M₁) (⇑f : (a : M₁) → M₂) (closedBall 0 r)))

Tactic:
⟨fun hf => hf.isCompact_closure_image_closedBall r, fun hf =>
    (isCompactOperator_iff_exists_mem_nhds_isCompact_closure_image f).mpr
      ⟨Metric.closedBall 0 r, closedBall_mem_nhds _ hr, hf⟩⟩

Premises used: Iff.mpr, Metric.closedBall_mem_nhds, isCompactOperator_iff_exists_mem_nhds_isCompact_closure_image, And.intro, Iff.intro, Exists.intro, Metric.closedBall, OfNat.ofNat, DFunLike.coe, IsCompactOperator.isCompact_closure_image_closedBall
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
Goal:
M₁ : Type u_3
M₂ : Type u_4
inst : TopologicalSpace M₁
inst_1 : AddCommMonoid M₁
inst_2 : TopologicalSpace M₂
inst_3 : AddCommMonoid M₂
S : Type u_6
inst_4 : Monoid S
inst_5 : DistribMulAction S M₂
inst_6 : ContinuousConstSMul S M₂
f : M₁ → M₂
hf : IsCompactOperator f
c : S
⊢ IsCompactOperator (c • f)

Tactic:
let ⟨K, hK, hKf⟩ := hf
  ⟨c • K, hK.image <| continuous_id.const_smul c,
    mem_of_superset hKf fun _ hx => smul_mem_smul_set hx⟩

Premises used: _private.0.isCompactOperator_iff_exists_mem_nhds_image_subset_compact.match_1, continuous_id, And.intro, Exists.intro, HSMul.hSMul, IsCompactOperator, IsCompact.image, Continuous.const_smul, Set.smul_mem_smul_set, Filter.mem_of_superset
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
Goal:
M₁ : Type u_3
M₂ : Type u_4
inst : TopologicalSpace M₁
inst_1 : AddCommMonoid M₁
inst_2 : TopologicalSpace M₂
inst_3 : AddCommMonoid M₂
S : Type u_6
inst_4 : Monoid S
inst_5 : DistribMulAction S M₂
inst_6 : ContinuousConstSMul S M₂
f : M₁ → M₂
c : Sˣ
h : IsCompactOperator (c • f)
⊢ IsCompactOperator f

Tactic:
simpa using h.smul c⁻¹

Premises used: Inv.inv, IsCompactOperator.smul
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
Goal:
M₁ : Type u_3
M₂ : Type u_4
inst : TopologicalSpace M₁
inst_1 : AddCommMonoid M₁
inst_2 : TopologicalSpace M₂
inst_3 : AddCommMonoid M₂
S : Type u_6
inst_4 : Monoid S
inst_5 : DistribMulAction S M₂
inst_6 : ContinuousConstSMul S M₂
f : M₁ → M₂
c : S
hc : IsUnit c
obtain : ∀ (c : Sˣ), IsCompactOperator ((↑c : S) • f) ↔ IsCompactOperator f
⊢ IsCompactOperator (c • f) ↔ IsCompactOperator f

Tactic:
obtain ⟨c, rfl⟩ := hc

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
Goal:
M₁ : Type u_3
M₂ : Type u_4
inst : TopologicalSpace M₁
inst_1 : AddCommMonoid M₁
inst_2 : TopologicalSpace M₂
inst_3 : AddCommMonoid M₂
S : Type u_6
inst_4 : Monoid S
inst_5 : DistribMulAction S M₂
inst_6 : ContinuousConstSMul S M₂
f : M₁ → M₂
c : Sˣ
⊢ IsCompactOperator ((↑c : S) • f) ↔ IsCompactOperator f

Tactic:
smul_unit_iff

Premises used: IsCompactOperator.smul_unit_iff
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
Goal:
M₁ : Type u_3
M₂ : Type u_4
inst : TopologicalSpace M₁
inst_1 : AddCommMonoid M₁
inst_2 : TopologicalSpace M₂
inst_3 : AddCommMonoid M₂
S : Type u_6
inst_4 : Monoid S
inst_5 : DistribMulAction S M₂
inst_6 : ContinuousConstSMul S M₂
f : M₁ → M₂
c : Sˣ
⊢ IsCompactOperator ((↑c : S) • f) ↔ IsCompactOperator f

Tactic:
exact smul_unit_iff

Premises used: IsCompactOperator.smul_unit_iff
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
Goal:
M₁ : Type u_3
M₂ : Type u_4
inst : TopologicalSpace M₁
inst_1 : AddCommMonoid M₁
inst_2 : TopologicalSpace M₂
inst_3 : AddCommMonoid M₂
S : Type u_6
inst_4 : Group S
inst_5 : DistribMulAction S M₂
inst_6 : ContinuousConstSMul S M₂
f : M₁ → M₂
c : S
⊢ IsCompactOperator (c • f) ↔ IsCompactOperator f

Tactic:
smul_isUnit_iff (Group.isUnit c)

Premises used: Group.isUnit, IsCompactOperator.smul_isUnit_iff
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
Goal:
M₁ : Type u_3
M₂ : Type u_4
inst : TopologicalSpace M₁
inst_1 : AddCommMonoid M₁
inst_2 : TopologicalSpace M₂
inst_3 : AddCommMonoid M₂
S : Type u_6
inst_4 : GroupWithZero S
inst_5 : DistribMulAction S M₂
inst_6 : ContinuousConstSMul S M₂
f : M₁ → M₂
c : S
hc : c ≠ 0
⊢ IsCompactOperator (c • f) ↔ IsCompactOperator f

Tactic:
smul_isUnit_iff hc.isUnit

Premises used: Ne.isUnit, IsCompactOperator.smul_isUnit_iff
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
Goal:
M₁ : Type u_3
M₂ : Type u_4
inst : TopologicalSpace M₁
inst_1 : AddCommMonoid M₁
inst_2 : TopologicalSpace M₂
inst_3 : AddCommMonoid M₂
inst_4 : ContinuousAdd M₂
f g : M₁ → M₂
hf : IsCompactOperator f
hg : IsCompactOperator g
⊢ IsCompactOperator (f + g)

Tactic:
let ⟨A, hA, hAf⟩ := hf
  let ⟨B, hB, hBg⟩ := hg
  ⟨A + B, hA.add hB,
    mem_of_superset (inter_mem hAf hBg) fun _ ⟨hxA, hxB⟩ => Set.add_mem_add hxA hxB⟩

Premises used: _private.0.isCompactOperator_iff_exists_mem_nhds_image_subset_compact.match_1, Filter.inter_mem, Membership.mem, _private.0.IsCompactOperator.add.match_1, Set.add_mem_add, Set.preimage, HAdd.hAdd, And.intro, Exists.intro, IsCompactOperator, IsCompact.add, Filter.mem_of_superset
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
Goal:
M₁ : Type u_3
M₄ : Type u_5
inst : TopologicalSpace M₁
inst_1 : AddCommMonoid M₁
inst_2 : TopologicalSpace M₄
inst_3 : AddCommGroup M₄
inst_4 : ContinuousNeg M₄
f : M₁ → M₄
hf : IsCompactOperator f
⊢ IsCompactOperator (-f)

Tactic:
let ⟨K, hK, hKf⟩ := hf
  ⟨-K, hK.neg, mem_of_superset hKf fun x (hx : f x ∈ K) => Set.neg_mem_neg.mpr hx⟩

Premises used: Iff.mpr, _private.0.isCompactOperator_iff_exists_mem_nhds_image_subset_compact.match_1, IsCompact.neg, And.intro, Exists.intro, IsCompactOperator, Neg.neg, Set.neg_mem_neg, Filter.mem_of_superset
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
Goal:
M₁ : Type u_3
M₄ : Type u_5
inst : TopologicalSpace M₁
inst_1 : AddCommMonoid M₁
inst_2 : TopologicalSpace M₄
inst_3 : AddCommGroup M₄
inst_4 : IsTopologicalAddGroup M₄
f g : M₁ → M₄
hf : IsCompactOperator f
hg : IsCompactOperator g
rw : IsCompactOperator (f + -g)
⊢ IsCompactOperator (f - g)

Tactic:
rw [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
Goal:
M₁ : Type u_3
M₄ : Type u_5
inst : TopologicalSpace M₁
inst_1 : AddCommMonoid M₁
inst_2 : TopologicalSpace M₄
inst_3 : AddCommGroup M₄
inst_4 : IsTopologicalAddGroup M₄
f g : M₁ → M₄
hf : IsCompactOperator f
hg : IsCompactOperator g
⊢ IsCompactOperator (f + -g)

Tactic:
hf.add hg.neg

Premises used: IsCompactOperator.add, IsCompactOperator.neg
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
Goal:
M₁ : Type u_3
M₄ : Type u_5
inst : TopologicalSpace M₁
inst_1 : AddCommMonoid M₁
inst_2 : TopologicalSpace M₄
inst_3 : AddCommGroup M₄
inst_4 : IsTopologicalAddGroup M₄
f g : M₁ → M₄
hf : IsCompactOperator f
hg : IsCompactOperator g
⊢ IsCompactOperator (f + -g)

Tactic:
exact hf.add hg.neg

Premises used: IsCompactOperator.add, IsCompactOperator.neg
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst_2 : TopologicalSpace M₁
inst_3 : TopologicalSpace M₂
inst_4 : TopologicalSpace M₃
inst_5 : AddCommMonoid M₁
inst_6 : Module R₁ M₁
inst_7 : AddCommMonoid M₂
inst_8 : Module R₂ M₂
f : M₂ → M₃
hf : IsCompactOperator f
g : M₁ →SL[σ₁₂] M₂
⊢ Tendsto.{u_4, u_5} (α := M₁) (β := M₂) ((⇑g : (a : M₁) → M₂) : (a : M₁) → M₂) (𝓝 0)
    (𝓝 ((g : (a : M₁) → M₂) 0) : Filter M₂)

Tactic:
have := g.continuous.tendsto 0
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst_2 : TopologicalSpace M₁
inst_3 : TopologicalSpace M₂
inst_4 : TopologicalSpace M₃
inst_5 : AddCommMonoid M₁
inst_6 : Module R₁ M₁
inst_7 : AddCommMonoid M₂
inst_8 : Module R₂ M₂
f : M₂ → M₃
hf : IsCompactOperator f
g : M₁ →SL[σ₁₂] M₂
this :
  Tendsto.{u_4, u_5} (α := M₁) (β := M₂) ((⇑g : (a : M₁) → M₂) : (a : M₁) → M₂) (𝓝 0)
    (𝓝 ((g : (a : M₁) → M₂) 0) : Filter M₂)
⊢ Tendsto.{u_4, u_5} (α := M₁) (β := M₂) (⇑g : (a : M₁) → M₂) (𝓝 0) (𝓝 0)

Tactic:
rw [map_zero] at this

Premises used: map_zero
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst_2 : TopologicalSpace M₁
inst_3 : TopologicalSpace M₂
inst_4 : TopologicalSpace M₃
inst_5 : AddCommMonoid M₁
inst_6 : Module R₁ M₁
inst_7 : AddCommMonoid M₂
inst_8 : Module R₂ M₂
f : M₂ → M₃
hf : IsCompactOperator f
g : M₁ →SL[σ₁₂] M₂
this : Tendsto.{u_4, u_5} (α := M₁) (β := M₂) (⇑g : (a : M₁) → M₂) (𝓝 0) (𝓝 0)
rcases :
  ∀ (K : Set M₃) (hK : IsCompact K) (hKf : Membership.mem (γ := Filter M₂) (𝓝 0) (f ⁻¹' K)),
    IsCompactOperator.{u_4, u_6} (M₁ := M₁) (f ∘ (⇑g : (a : M₁) → M₂))
⊢ IsCompactOperator.{u_4, u_6} (M₁ := M₁) (f ∘ (⇑g : (a : M₁) → M₂))

Tactic:
rcases hf with ⟨K, hK, hKf⟩
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst_2 : TopologicalSpace M₁
inst_3 : TopologicalSpace M₂
inst_4 : TopologicalSpace M₃
inst_5 : AddCommMonoid M₁
inst_6 : Module R₁ M₁
inst_7 : AddCommMonoid M₂
inst_8 : Module R₂ M₂
f : M₂ → M₃
g : M₁ →SL[σ₁₂] M₂
this : Tendsto.{u_4, u_5} (α := M₁) (β := M₂) (⇑g : (a : M₁) → M₂) (𝓝 0) (𝓝 0)
K : Set M₃
hK : IsCompact K
hKf : Membership.mem (γ := Filter M₂) (𝓝 0) (f ⁻¹' K)
⊢ IsCompactOperator.{u_4, u_6} (M₁ := M₁) (f ∘ (⇑g : (a : M₁) → M₂))

Tactic:
⟨K, hK, this hKf⟩

Premises used: And.intro, Exists.intro, IsCompactOperator
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst_2 : TopologicalSpace M₁
inst_3 : TopologicalSpace M₂
inst_4 : TopologicalSpace M₃
inst_5 : AddCommMonoid M₁
inst_6 : Module R₁ M₁
inst_7 : AddCommMonoid M₂
inst_8 : Module R₂ M₂
f : M₂ → M₃
g : M₁ →SL[σ₁₂] M₂
this : Tendsto.{u_4, u_5} (α := M₁) (β := M₂) (⇑g : (a : M₁) → M₂) (𝓝 0) (𝓝 0)
K : Set M₃
hK : IsCompact K
hKf : Membership.mem (γ := Filter M₂) (𝓝 0) (f ⁻¹' K)
⊢ IsCompactOperator.{u_4, u_6} (M₁ := M₁) (f ∘ (⇑g : (a : M₁) → M₂))

Tactic:
exact ⟨K, hK, this hKf⟩
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
Goal:
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst : TopologicalSpace M₁
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : AddCommMonoid M₁
f : M₁ → M₂
hf : IsCompactOperator f
g : M₂ → M₃
hg : Continuous[inst_1, inst_2] g
rcases :
  ∀ (K : Set M₂) (hK : IsCompact K) (hKf : Membership.mem (γ := Filter M₁) (𝓝 0) (f ⁻¹' K)), IsCompactOperator (g ∘ f)
⊢ IsCompactOperator (g ∘ f)

Tactic:
rcases hf with ⟨K, hK, hKf⟩
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
Goal:
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst : TopologicalSpace M₁
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : AddCommMonoid M₁
f : M₁ → M₂
g : M₂ → M₃
hg : Continuous[inst_1, inst_2] g
K : Set M₂
hK : IsCompact K
hKf : Membership.mem (γ := Filter M₁) (𝓝 0) (f ⁻¹' K)
⊢ IsCompactOperator (g ∘ f)

Tactic:
⟨g '' K, hK.image hg, mem_of_superset hKf ?_⟩

Premises used: And.intro, Exists.intro, Set.image, IsCompactOperator, IsCompact.image, Filter.mem_of_superset
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
Goal:
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst : TopologicalSpace M₁
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : AddCommMonoid M₁
f : M₁ → M₂
g : M₂ → M₃
hg : Continuous[inst_1, inst_2] g
K : Set M₂
hK : IsCompact K
hKf : Membership.mem (γ := Filter M₁) (𝓝 0) (f ⁻¹' K)
refine : f ⁻¹' K ⊆ g ∘ f ⁻¹' g '' K
⊢ IsCompactOperator (g ∘ f)

Tactic:
refine ⟨g '' K, hK.image hg, mem_of_superset hKf ?_⟩
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
Goal:
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst : TopologicalSpace M₁
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : AddCommMonoid M₁
f : M₁ → M₂
g : M₂ → M₃
hg : Continuous[inst_1, inst_2] g
K : Set M₂
hK : IsCompact K
hKf : Membership.mem (γ := Filter M₁) (𝓝 0) (f ⁻¹' K)
rw : f ⁻¹' K ⊆ f ⁻¹' g ⁻¹' g '' K
⊢ f ⁻¹' K ⊆ g ∘ f ⁻¹' g '' K

Tactic:
rw [preimage_comp]

Premises used: Set.preimage_comp
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
Goal:
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst : TopologicalSpace M₁
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : AddCommMonoid M₁
f : M₁ → M₂
g : M₂ → M₃
hg : Continuous[inst_1, inst_2] g
K : Set M₂
hK : IsCompact K
hKf : Membership.mem (γ := Filter M₁) (𝓝 0) (f ⁻¹' K)
⊢ f ⁻¹' K ⊆ f ⁻¹' g ⁻¹' g '' K

Tactic:
preimage_mono (subset_preimage_image _ _)

Premises used: Set.preimage_mono, Set.subset_preimage_image
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
Goal:
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst : TopologicalSpace M₁
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : AddCommMonoid M₁
f : M₁ → M₂
g : M₂ → M₃
hg : Continuous[inst_1, inst_2] g
K : Set M₂
hK : IsCompact K
hKf : Membership.mem (γ := Filter M₁) (𝓝 0) (f ⁻¹' K)
⊢ f ⁻¹' K ⊆ f ⁻¹' g ⁻¹' g '' K

Tactic:
exact preimage_mono (subset_preimage_image _ _)

Premises used: Set.preimage_mono, Set.subset_preimage_image
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
Goal:
R₂ : Type u_2
R₃ : Type u_3
inst : Semiring R₂
inst_1 : Semiring R₃
σ₂₃ : R₂ →+* R₃
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst_2 : TopologicalSpace M₁
inst_3 : TopologicalSpace M₂
inst_4 : TopologicalSpace M₃
inst_5 : AddCommMonoid M₁
inst_6 : AddCommMonoid M₂
inst_7 : Module R₂ M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R₃ M₃
f : M₁ → M₂
hf : IsCompactOperator f
g : M₂ →SL[σ₂₃] M₃
⊢ IsCompactOperator.{u_4, u_6} (M₂ := M₃) ((⇑g : (a : M₂) → M₃) ∘ f)

Tactic:
hf.continuous_comp g.continuous

Premises used: IsCompactOperator.continuous_comp, ContinuousLinearMap.continuous
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
M₂ : Type u_5
inst_2 : TopologicalSpace M₁
inst_3 : TopologicalSpace M₂
inst_4 : AddCommMonoid M₁
inst_5 : Module R₁ M₁
inst_6 : AddCommGroup M₂
inst_7 : Module R₂ M₂
inst_8 : IsTopologicalAddGroup M₂
inst_9 : LocallyCompactSpace M₂
T : M₁ →SL[σ₁₂] M₂
⊢ IsCompactOperator.{u_4, u_5} (M₁ := M₁) (M₂ := M₂) (⇑T : (a : M₁) → M₂)

Tactic:
(isCompactOperator_id.comp_clm T :)

Premises used: IsCompactOperator.comp_clm
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
Goal:
R₂ : Type u_2
R₃ : Type u_3
inst : Semiring R₂
inst_1 : Semiring R₃
σ₂₃ : R₂ →+* R₃
M₂ : Type u_5
M₃ : Type u_6
inst_2 : TopologicalSpace M₂
inst_3 : TopologicalSpace M₃
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
inst_6 : IsTopologicalAddGroup M₂
inst_7 : LocallyCompactSpace M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R₃ M₃
T : M₂ →SL[σ₂₃] M₃
⊢ IsCompactOperator.{u_5, u_6} (M₁ := M₂) (M₂ := M₃) (⇑T : (a : M₂) → M₃)

Tactic:
isCompactOperator_id.clm_comp T

Premises used: IsCompactOperator.clm_comp
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
Goal:
R₂ : Type u_1
inst : Semiring R₂
M₁ : Type u_2
M₂ : Type u_3
inst_1 : TopologicalSpace M₁
inst_2 : TopologicalSpace M₂
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
f : M₁ → M₂
hf : IsCompactOperator f
V : Submodule R₂ M₂
hV : ∀ (x : M₁), f x ∈ V
h_closed : IsClosed[inst_2] (↑V : Set M₂)
⊢ IsCompactOperator (Set.codRestrict f (↑V : Set M₂) hV)

Tactic:
let ⟨_, hK, hKf⟩ := hf
  ⟨_, h_closed.isClosedEmbedding_subtypeVal.isCompact_preimage hK, hKf⟩

Premises used: _private.0.IsCompactOperator.codRestrict.match_1, SetLike.coe, Set.preimage, And.intro, Topology.IsClosedEmbedding.isCompact_preimage, Exists.intro, IsClosed.isClosedEmbedding_subtypeVal, Set.codRestrict, IsCompactOperator, Subtype.val
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
Goal:
R₁ : Type u_1
inst : Semiring R₁
M₁ : Type u_3
inst_1 : TopologicalSpace M₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R₁ M₁
f : M₁ →ₗ[R₁] M₁
hf : IsCompactOperator (M₁ := M₁) (M₂ := M₁) (⇑f : (a : M₁) → M₁)
V : Submodule R₁ M₁
hV : ∀ v ∈ V, Membership.mem (α := M₁) V ((f : (a : M₁) → M₁) v : M₁)
h_closed : IsClosed[inst_1] (↑V : Set M₁)
⊢ IsCompactOperator (M₁ := ↥V) (M₂ := ↥V) (⇑(f.restrict hV) : (a : ↥V) → ↥V)

Tactic:
(hf.comp_clm V.subtypeL).codRestrict (SetLike.forall.2 hV) h_closed

Premises used: Submodule.subtypeL, Iff.mpr, IsCompactOperator.codRestrict, SetLike.forall, IsCompactOperator.comp_clm, Set.codRestrict
-- Module: Mathlib.Analysis.Normed.Operator.Compact.Basic
Goal:
R₂ : Type u_2
inst : Semiring R₂
M₂ : Type u_4
inst_1 : UniformSpace M₂
inst_2 : AddCommMonoid M₂
inst_3 : Module R₂ M₂
inst_4 : T0Space M₂
f : M₂ →ₗ[R₂] M₂
hf : IsCompactOperator (M₁ := M₂) (M₂ := M₂) (⇑f : (a : M₂) → M₂)
V : Submodule R₂ M₂
hV : ∀ v ∈ V, Membership.mem (α := M₂) V ((f : (a : M₂) → M₂) v : M₂)
hcomplete : CompleteSpace.{u_4} ↥V
⊢ IsCompactOperator (M₁ := ↥V) (M₂ := ↥V) (⇑(f.restrict hV) : (a : ↥V) → ↥V)

Tactic:
hf.restrict hV (completeSpace_coe_iff_isComplete.mp hcomplete).isClosed

Premises used: IsComplete.isClosed, IsCompactOperator.restrict, Iff.mp, completeSpace_coe_iff_isComplete
-- 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₂)
⊢ Continuous[inst_3, inst_5] (⇑f : (a : M₁) → M₂)

Tactic:
continuous_of_continuousAt_zero f fun U hU => ?_

Premises used: continuous_of_continuousAt_zero
-- 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₂)
refine :
  ∀ (U : Set M₂) (hU : Membership.mem (γ := Filter M₂) (𝓝 ((f : (a : M₁) → M₂) 0) : Filter M₂) U),
    Membership.mem (γ := Filter M₂) (map.{u_3, u_4} (α := M₁) (⇑f : (a : M₁) → M₂) (𝓝 0)) U
⊢ Continuous[inst_3, inst_5] (⇑f : (a : M₁) → M₂)

Tactic:
refine continuous_of_continuousAt_zero f fun U hU => ?_

Premises used: continuous_of_continuousAt_zero
-- 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₂)
U : Set M₂
hU : Membership.mem (γ := Filter M₂) (𝓝 ((f : (a : M₁) → M₂) 0) : Filter M₂) U
⊢ Membership.mem (γ := Filter M₂) (𝓝 0) U

Tactic:
rw [map_zero] at hU

Premises used: map_zero
-- 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₂)
U : Set M₂
hU : Membership.mem (γ := Filter M₂) (𝓝 0) U
rcases :
  ∀ (K : Set M₂) (hK : IsCompact K) (hKf : 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)) U
⊢ Membership.mem (γ := Filter M₂) (map.{u_3, u_4} (α := M₁) (⇑f : (a : M₁) → M₂) (𝓝 0)) U

Tactic:
rcases hf with ⟨K, hK, hKf⟩