-- Mathlib/Analysis/Normed/Operator/Compact.lean
theorem IsCompactOperator.continuous {f : M₁ →ₛₗ[σ₁₂] M₂} (hf : IsCompactOperator f) :
    Continuous f

Proof state:
case intro.intro.intro.intro.intro
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹⁰ : RingHomIsometric σ₁₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁹ : TopologicalSpace M₁
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module 𝕜₁ M₁
inst✝⁴ : Module 𝕜₂ M₂
inst✝³ : IsTopologicalAddGroup M₁
inst✝² : ContinuousConstSMul 𝕜₁ M₁
inst✝¹ : IsTopologicalAddGroup M₂
inst✝ : ContinuousSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
this✝ : UniformSpace M₂ := IsTopologicalAddGroup.toUniformSpace M₂
this : UniformAddGroup M₂
U : Set M₂
hU : U ∈ 𝓝 0
K : Set M₂
hK : IsCompact K
hKf : ⇑f ⁻¹' K ∈ 𝓝 0
r : ℝ
hr : r > 0
hrU : ∀ (c : 𝕜₂), r ≤ ‖c‖ → K ⊆ c • U
c : 𝕜₁
hc : r < ‖c‖
hcnz : c ≠ 0
⊢ σ₁₂ c⁻¹ • K ⊆ U

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

Result:
case intro.intro.intro.intro.intro
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹⁰ : RingHomIsometric σ₁₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁹ : TopologicalSpace M₁
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module 𝕜₁ M₁
inst✝⁴ : Module 𝕜₂ M₂
inst✝³ : IsTopologicalAddGroup M₁
inst✝² : ContinuousConstSMul 𝕜₁ M₁
inst✝¹ : IsTopologicalAddGroup M₂
inst✝ : ContinuousSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
this✝ : UniformSpace M₂ := IsTopologicalAddGroup.toUniformSpace M₂
this : UniformAddGroup M₂
U : Set M₂
hU : U ∈ 𝓝 0
K : Set M₂
hK : IsCompact K
hKf : ⇑f ⁻¹' K ∈ 𝓝 0
r : ℝ
hr : r > 0
hrU : ∀ (c : 𝕜₂), r ≤ ‖c‖ → K ⊆ c • U
c : 𝕜₁
hc : r < ‖c‖
hcnz : c ≠ 0
⊢ K ⊆ σ₁₂ c • U

Proof state:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹⁰ : RingHomIsometric σ₁₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁹ : TopologicalSpace M₁
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module 𝕜₁ M₁
inst✝⁴ : Module 𝕜₂ M₂
inst✝³ : IsTopologicalAddGroup M₁
inst✝² : ContinuousConstSMul 𝕜₁ M₁
inst✝¹ : IsTopologicalAddGroup M₂
inst✝ : ContinuousSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
hf : IsCompactOperator ⇑f
this✝ : UniformSpace M₂ := IsTopologicalAddGroup.toUniformSpace M₂
this : UniformAddGroup M₂
U : Set M₂
hU : U ∈ 𝓝 0
⊢ U ∈ map (⇑f) (𝓝 0)

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

Result:
case intro.intro
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹⁰ : RingHomIsometric σ₁₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁹ : TopologicalSpace M₁
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module 𝕜₁ M₁
inst✝⁴ : Module 𝕜₂ M₂
inst✝³ : IsTopologicalAddGroup M₁
inst✝² : ContinuousConstSMul 𝕜₁ M₁
inst✝¹ : IsTopologicalAddGroup M₂
inst✝ : ContinuousSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
this✝ : UniformSpace M₂ := IsTopologicalAddGroup.toUniformSpace M₂
this : UniformAddGroup M₂
U : Set M₂
hU : U ∈ 𝓝 0
K : Set M₂
hK : IsCompact K
hKf : ⇑f ⁻¹' K ∈ 𝓝 0
⊢ U ∈ map (⇑f) (𝓝 0)

Proof state:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹⁰ : RingHomIsometric σ₁₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁹ : TopologicalSpace M₁
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module 𝕜₁ M₁
inst✝⁴ : Module 𝕜₂ M₂
inst✝³ : IsTopologicalAddGroup M₁
inst✝² : ContinuousConstSMul 𝕜₁ M₁
inst✝¹ : IsTopologicalAddGroup M₂
inst✝ : ContinuousSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
this✝² : UniformSpace M₂ := IsTopologicalAddGroup.toUniformSpace M₂
this✝¹ : UniformAddGroup M₂
U : Set M₂
hU : U ∈ 𝓝 0
K : Set M₂
hK : IsCompact K
hKf : ⇑f ⁻¹' K ∈ 𝓝 0
r : ℝ
hr : r > 0
hrU : ∀ (c : 𝕜₂), r ≤ ‖c‖ → K ⊆ c • U
c : 𝕜₁
hc : r < ‖c‖
hcnz : c ≠ 0
this✝ : σ₁₂ c⁻¹ • K ⊆ U
this : IsUnit c⁻¹
⊢ σ₁₂ c⁻¹ • K ∈ map (⇑f) (𝓝 0)

Tactic:
rwa [mem_map, preimage_smul_setₛₗ _ _ _ f this, set_smul_mem_nhds_zero_iff (inv_ne_zero hcnz)]

Result:
no goals

Proof state:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹⁰ : RingHomIsometric σ₁₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁹ : TopologicalSpace M₁
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module 𝕜₁ M₁
inst✝⁴ : Module 𝕜₂ M₂
inst✝³ : IsTopologicalAddGroup M₁
inst✝² : ContinuousConstSMul 𝕜₁ M₁
inst✝¹ : IsTopologicalAddGroup M₂
inst✝ : ContinuousSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
hf : IsCompactOperator ⇑f
this✝ : UniformSpace M₂ := IsTopologicalAddGroup.toUniformSpace M₂
this : UniformAddGroup M₂
U : Set M₂
hU : U ∈ 𝓝 (f 0)
⊢ U ∈ map (⇑f) (𝓝 0)

Tactic:
rw [map_zero] at hU

Result:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹⁰ : RingHomIsometric σ₁₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁹ : TopologicalSpace M₁
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module 𝕜₁ M₁
inst✝⁴ : Module 𝕜₂ M₂
inst✝³ : IsTopologicalAddGroup M₁
inst✝² : ContinuousConstSMul 𝕜₁ M₁
inst✝¹ : IsTopologicalAddGroup M₂
inst✝ : ContinuousSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
hf : IsCompactOperator ⇑f
this✝ : UniformSpace M₂ := IsTopologicalAddGroup.toUniformSpace M₂
this : UniformAddGroup M₂
U : Set M₂
hU : U ∈ 𝓝 0
⊢ U ∈ map (⇑f) (𝓝 0)

Proof state:
case intro.intro.intro.intro.intro
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹⁰ : RingHomIsometric σ₁₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁹ : TopologicalSpace M₁
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module 𝕜₁ M₁
inst✝⁴ : Module 𝕜₂ M₂
inst✝³ : IsTopologicalAddGroup M₁
inst✝² : ContinuousConstSMul 𝕜₁ M₁
inst✝¹ : IsTopologicalAddGroup M₂
inst✝ : ContinuousSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
this✝ : UniformSpace M₂ := IsTopologicalAddGroup.toUniformSpace M₂
this : UniformAddGroup M₂
U : Set M₂
hU : U ∈ 𝓝 0
K : Set M₂
hK : IsCompact K
hKf : ⇑f ⁻¹' K ∈ 𝓝 0
r : ℝ
hr : r > 0
hrU : ∀ (c : 𝕜₂), r ≤ ‖c‖ → K ⊆ c • U
c : 𝕜₁
hc : r < ‖c‖
hcnz : c ≠ 0
⊢ r ≤ ‖c‖

Tactic:
exact hc.le

Result:
no goals

Proof state:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹⁰ : RingHomIsometric σ₁₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁹ : TopologicalSpace M₁
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module 𝕜₁ M₁
inst✝⁴ : Module 𝕜₂ M₂
inst✝³ : IsTopologicalAddGroup M₁
inst✝² : ContinuousConstSMul 𝕜₁ M₁
inst✝¹ : IsTopologicalAddGroup M₂
inst✝ : ContinuousSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
hf : IsCompactOperator ⇑f
⊢ Continuous ⇑f

Tactic:
letI : UniformSpace M₂ := IsTopologicalAddGroup.toUniformSpace _

Result:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹⁰ : RingHomIsometric σ₁₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁹ : TopologicalSpace M₁
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module 𝕜₁ M₁
inst✝⁴ : Module 𝕜₂ M₂
inst✝³ : IsTopologicalAddGroup M₁
inst✝² : ContinuousConstSMul 𝕜₁ M₁
inst✝¹ : IsTopologicalAddGroup M₂
inst✝ : ContinuousSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
hf : IsCompactOperator ⇑f
this : UniformSpace M₂ := IsTopologicalAddGroup.toUniformSpace M₂
⊢ Continuous ⇑f