awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.BoundedLinearMaps (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : CommSemiring 𝕜
inst_1 : SeminormedRing A
inst_2 : Algebra 𝕜 A
E : Type u_3
inst_3 : SeminormedAddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : Module A E
inst_6 : IsBoundedSMul A E
inst_7 : IsScalarTower 𝕜 A E
x : A
y : E
⊢ ‖(x, y).1 • (x, y).2‖ ≤ 1 * ‖x‖ * ‖y‖
have grw : ‖(x, y).1 • (x, y).2‖ ≤ ‖x‖ * ‖y‖
Tactic: grw [one_mul, norm_smul_le]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.BoundedLinearMaps (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : CommSemiring 𝕜
inst_1 : SeminormedRing A
inst_2 : Algebra 𝕜 A
E : Type u_3
inst_3 : SeminormedAddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : Module A E
inst_6 : IsBoundedSMul A E
inst_7 : IsScalarTower 𝕜 A E
x : A
y : E
grw : ‖(x, y).1 • (x, y).2‖ ≤ ‖x‖ * ‖y‖
⊢ ‖(x, y).1 • (x, y).2‖ ≤ 1 * ‖x‖ * ‖y‖
have grw₁ : ‖(x, y).1‖ * ‖(x, y).2‖ ≤ ‖(x, y).1‖ * ‖(x, y).2‖
Tactic: grw [one_mul, norm_smul_le]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.BoundedLinearMaps (goal)
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
f : E →L[𝕜] F →L[𝕜] G
x : E
y : F
⊢ ‖f‖ * ‖x‖ * ‖y‖ ≤ max ‖f‖ 1 * ‖x‖ * ‖y‖
have hbc : ‖f‖ ≤ max ‖f‖ 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.BoundedLinearMaps (goal)
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
s : Set X
x : X
hf : ContinuousWithinAt f s x
hg : ContinuousWithinAt g s x
⊢ ContinuousWithinAt (Y := E × F →L[𝕜] G) (fun (x : X) ↦ (f x).coprod (g x)) s x
have simp : ContinuousWithinAt (Y := E × F →L[𝕜] G)
  (fun (x : X) ↦ f x ∘SL ContinuousLinearMap.fst 𝕜 E F + g x ∘SL ContinuousLinearMap.snd 𝕜 E F) s x
Tactic: simp only [← comp_fst_add_comp_snd]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.BoundedLinearMaps (goal)
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
x : X
hf : ContinuousAt f x
hg : ContinuousAt g x
⊢ ContinuousAt (Y := E × F →L[𝕜] G) (fun (x : X) ↦ (f x).coprod (g x)) x
have simp : ContinuousAt (Y := E × F →L[𝕜] G)
  (fun (x : X) ↦ f x ∘SL ContinuousLinearMap.fst 𝕜 E F + g x ∘SL ContinuousLinearMap.snd 𝕜 E F) x
Tactic: simp only [← comp_fst_add_comp_snd]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.BoundedLinearMaps (goal)
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
s : Set X
hf : ContinuousOn f s
hg : ContinuousOn g s
⊢ ContinuousOn (Y := E × F →L[𝕜] G) (fun (x : X) ↦ (f x).coprod (g x)) s
have simp : ContinuousOn (Y := E × F →L[𝕜] G)
  (fun (x : X) ↦ f x ∘SL ContinuousLinearMap.fst 𝕜 E F + g x ∘SL ContinuousLinearMap.snd 𝕜 E F) s
Tactic: simp only [← comp_fst_add_comp_snd]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.BoundedLinearMaps (goal)
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
⊢ Continuous[inst_7, topologicalSpace] fun (x : X) ↦ (f x).coprod (g x)
have apply : ContinuousOn (Y := E × F →L[𝕜] G) (fun (x : X) ↦ (f x).coprod (g x)) Set.univ
Tactic: apply continuousOn_univ.mp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.BoundedLinearMaps (goal)
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
⊢ IsOpen (X := E →L[𝕜] F) (range (ι := E ≃L[𝕜] F) toContinuousLinearMap)
have rw : ∀ (i : E ≃L[𝕜] F), range (ι := E ≃L[𝕜] F) toContinuousLinearMap ∈ 𝓝 (↑i : E →L[𝕜] F)
Tactic: rw [isOpen_iff_mem_nhds, forall_mem_range]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.BoundedLinearMaps (goal)
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)
have refine : ∀ (e : E ≃L[𝕜] F), IsOpen (X := E →L[𝕜] F) (range (ι := E ≃L[𝕜] F) toContinuousLinearMap)
Tactic: refine fun e => IsOpen.mem_nhds ?_ (mem_range_self _)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.BoundedLinearMaps (hypothesis)
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
⊢ IsOpen (X := E →L[𝕜] F) (range (ι := E ≃L[𝕜] F) toContinuousLinearMap)
have h_O : Continuous O
Tactic: have h_O : Continuous O := (isBoundedBilinearMap_comp (𝕜 := 𝕜) (F := F) (G := E)).continuous_right
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.BoundedLinearMaps (goal)
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 (X := E →L[𝕜] F) (range (ι := E ≃L[𝕜] F) toContinuousLinearMap)
have h : range (ι := E ≃L[𝕜] F) toContinuousLinearMap = O ⁻¹' {x : E →L[𝕜] E | IsUnit x}
Tactic: convert! show IsOpen (O ⁻¹' {x | IsUnit x}) from Units.isOpen.preimage h_O using 1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.BoundedLinearMaps (goal)
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
⊢ range (ι := E ≃L[𝕜] F) toContinuousLinearMap = O ⁻¹' {x : E →L[𝕜] E | IsUnit x}
have 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}
Tactic: ext f'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.BoundedLinearMaps (goal)
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
⊢ Membership.mem (γ := Set (E →L[𝕜] F)) (range (ι := E ≃L[𝕜] F) toContinuousLinearMap) f' ↔
    f' ∈ O ⁻¹' {x : E →L[𝕜] E | IsUnit x}
have h : Membership.mem (γ := Set (E →L[𝕜] F)) (range (ι := E ≃L[𝕜] F) toContinuousLinearMap) f' →
  f' ∈ O ⁻¹' {x : E →L[𝕜] E | IsUnit x}
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.BoundedLinearMaps (goal)
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}
⊢ Membership.mem (γ := Set (E →L[𝕜] F)) (range (ι := E ≃L[𝕜] F) toContinuousLinearMap) f' ↔
    f' ∈ O ⁻¹' {x : E →L[𝕜] E | IsUnit x}
have h₁ : f' ∈ O ⁻¹' {x : E →L[𝕜] E | IsUnit x} →
  Membership.mem (γ := Set (E →L[𝕜] F)) (range (ι := E ≃L[𝕜] F) toContinuousLinearMap) f'
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.BoundedLinearMaps (goal)
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'
⊢ Membership.mem (γ := Set (E →L[𝕜] F)) (range (ι := E ≃L[𝕜] F) toContinuousLinearMap) f'
have h : (↑(ContinuousLinearEquiv.trans ((unitsEquiv 𝕜 E : (a : (E →L[𝕜] E)ˣ) → E ≃L[𝕜] E) w) e) : E →L[𝕜] F) = f'
Tactic: use (unitsEquiv 𝕜 E w).trans e
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.BoundedLinearMaps (goal)
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'
⊢ (↑(ContinuousLinearEquiv.trans ((unitsEquiv 𝕜 E : (a : (E →L[𝕜] E)ˣ) → E ≃L[𝕜] E) w) e) : E →L[𝕜] F) = f'
have 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)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Compact.Basic (goal)
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₂
⊢ IsCompactOperator f ↔ ∃ (V : Set M₁), Membership.mem (γ := Filter M₁) (𝓝 0) V ∧ IsCompact (closure[inst_2] (f '' V))
have 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))
Tactic: rw [isCompactOperator_iff_exists_mem_nhds_image_subset_compact]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Compact.Basic (goal)
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 := ⋯
⊢ (⇑f : (a : M₁) → M₂) '' S ⊆ HSMul.hSMul.{u_2, u_4, u_4} (α := 𝕜₂) ((σ₁₂ : (a : 𝕜₁) → 𝕜₂) c : 𝕜₂) K
have rw : S ⊆ HSMul.hSMul (β := Set M₁) c ((⇑f : (a : M₁) → M₂) ⁻¹' K)
Tactic: rw [image_subset_iff, this.isUnit.preimage_smul_setₛₗ σ₁₂]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Compact.Basic (goal)
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
⊢ IsCompactOperator (c • f) ↔ IsCompactOperator f
have obtain : ∀ (c : Sˣ), IsCompactOperator ((↑c : S) • f) ↔ IsCompactOperator f
Tactic: obtain ⟨c, rfl⟩ := hc
Cleared hypotheses: c, hc
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Compact.Basic (goal)
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)
have rw : IsCompactOperator (f + -g)
Tactic: rw [sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Compact.Basic (hypothesis)
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₂
⊢ IsCompactOperator.{u_4, u_6} (M₁ := M₁) (f ∘ (⇑g : (a : M₁) → M₂))
have this : 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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Compact.Basic (hypothesis)
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₂)
⊢ IsCompactOperator.{u_4, u_6} (M₁ := M₁) (f ∘ (⇑g : (a : M₁) → M₂))
have this₁ : Tendsto.{u_4, u_5} (α := M₁) (β := M₂) (⇑g : (a : M₁) → M₂) (𝓝 0) (𝓝 0)
Tactic: rw [map_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Compact.Basic (goal)
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)
⊢ IsCompactOperator.{u_4, u_6} (M₁ := M₁) (f ∘ (⇑g : (a : M₁) → M₂))
have 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₂))
Tactic: rcases hf with ⟨K, hK, hKf⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Compact.Basic (goal)
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
⊢ IsCompactOperator (g ∘ f)
have rcases : ∀ (K : Set M₂) (hK : IsCompact K) (hKf : Membership.mem (γ := Filter M₁) (𝓝 0) (f ⁻¹' K)), IsCompactOperator (g ∘ f)
Tactic: rcases hf with ⟨K, hK, hKf⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Compact.Basic (goal)
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)
have refine : f ⁻¹' K ⊆ g ∘ f ⁻¹' g '' K
Tactic: refine ⟨g '' K, hK.image hg, mem_of_superset hKf ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Compact.Basic (goal)
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 ⊆ g ∘ f ⁻¹' g '' K
have rw : f ⁻¹' K ⊆ f ⁻¹' g ⁻¹' g '' K
Tactic: rw [preimage_comp]
-- 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₂
hf : IsCompactOperator.{u_3, u_4} (M₁ := M₁) (M₂ := M₂) (⇑f : (a : M₁) → M₂)
⊢ Continuous[inst_3, inst_5] (⇑f : (a : M₁) → M₂)
have 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
Tactic: refine continuous_of_continuousAt_zero f fun U hU => ?_
-- 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₂
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₂) (map.{u_3, u_4} (α := M₁) (⇑f : (a : M₁) → M₂) (𝓝 0)) U
have hU₁ : Membership.mem (γ := Filter M₂) (𝓝 0) U
Tactic: rw [map_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 : 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
⊢ Membership.mem (γ := Filter M₂) (map.{u_3, u_4} (α := M₁) (⇑f : (a : M₁) → M₂) (𝓝 0)) U
have 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
Tactic: rcases hf with ⟨K, hK, hKf⟩
Cleared hypotheses: hf
-- 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)
⊢ Membership.mem (γ := Filter M₂) (map.{u_3, u_4} (α := M₁) (⇑f : (a : M₁) → M₂) (𝓝 0)) U
have 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
Tactic: rcases (hK.isVonNBounded 𝕜₂ hU).exists_pos with ⟨r, hr, hrU⟩
-- 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
⊢ Membership.mem (γ := Filter M₂) (map.{u_3, u_4} (α := M₁) (⇑f : (a : M₁) → M₂) (𝓝 0)) U
have rcases : ∀ (c : 𝕜₁) (hc : r < ‖c‖), 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⟩
-- 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‖
⊢ Membership.mem (γ := Filter M₂) (map.{u_3, u_4} (α := M₁) (⇑f : (a : M₁) → M₂) (𝓝 0)) U
have hcnz : c ≠ 0
Tactic: have hcnz : c ≠ 0 := ne_zero_of_norm_ne_zero (hr.trans hc).ne.symm
-- 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 : 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
have 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)
Tactic: grw [← this]