awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (goal)
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜₂ F
inst_7 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
𝔖 : Set (Set E)
ι : Type u_6
p : ι → Prop
b : ι → Set F
h : HasBasis (𝓝 0) p b
this_1 : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
⊢ Eq (α := Filter (UniformConvergenceCLM σ F 𝔖)) (𝓝 0)
    (⨅ s ∈ 𝔖, ⨅ (i : ι), ⨅ (_ : p i), 𝓟 {f : UniformConvergenceCLM σ F 𝔖 | MapsTo (⇑f : (a : E) → F) s (b i)})
have rw : Eq (α := Filter (UniformConvergenceCLM σ F 𝔖))
  (comap (β := E →ᵤ[𝔖] F)
    (comp (β := E → F) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → F) → E →ᵤ[𝔖] F) (DFunLike.coe (β := fun (a : E) ↦ F)))
    (⨅ s ∈ 𝔖,
      ⨅ (i : ι),
        ⨅ (_ : p i),
          𝓟
            {g : E →ᵤ[𝔖] F |
              ∀ x ∈ s,
                Membership.mem.{u_4, u_4} (α := F × F) (γ := Set (F × F)) {x : F × F | x.2 - x.1 ∈ b i}
                  (((UniformOnFun.toFun 𝔖 : (a : E →ᵤ[𝔖] F) → E → F)
                        (comp (α := UniformConvergenceCLM σ F 𝔖) (β := E → F)
                          (⇑(UniformOnFun.ofFun 𝔖) : (a : E → F) → E →ᵤ[𝔖] F) (DFunLike.coe (β := fun (a : E) ↦ F)) 0)
                        x,
                      (UniformOnFun.toFun 𝔖 : (a : E →ᵤ[𝔖] F) → E → F) g x) :
                    F × F)}))
  (⨅ s ∈ 𝔖, ⨅ (i : ι), ⨅ (_ : p i), 𝓟 {f : UniformConvergenceCLM σ F 𝔖 | MapsTo (⇑f : (a : E) → F) s (b i)})
Tactic: rw [(isEmbedding_coeFn σ F 𝔖).isInducing.nhds_eq_comap,
    UniformOnFun.nhds_eq_of_basis _ _ h.uniformity_of_nhds_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (goal)
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜₂ F
inst_7 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
𝔖 : Set (Set E)
s : Set E
hs : s ∈ 𝔖
U : Set F
hu : Membership.mem (γ := Filter F) (𝓝 0) U
⊢ ∀ᶠ (f : UniformConvergenceCLM σ F 𝔖) in 𝓝 0, MapsTo (⇑f : (a : E) → F) s U
have rw : ∀ᶠ (f : UniformConvergenceCLM σ F 𝔖) in
  ⨅ s ∈ 𝔖,
    ⨅ (t : Set F),
      ⨅ (_ : Membership.mem (γ := Filter F) (𝓝 0) t),
        𝓟 {f : UniformConvergenceCLM σ F 𝔖 | MapsTo (⇑f : (a : E) → F) s t},
  MapsTo (⇑f : (a : E) → F) s U
Tactic: rw [nhds_zero_eq]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (goal)
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜₂ F
R : Type u_6
inst_7 : SeminormedRing R
inst_8 : TopologicalSpace F
inst_9 : IsTopologicalAddGroup F
inst_10 : DistribMulAction R F
inst_11 : ContinuousConstSMul R F
inst_12 : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
S : Set (UniformConvergenceCLM σ F 𝔖)
hS : IsVonNBounded R S
s : Set E
hs : s ∈ 𝔖
U : Set F
hU : Membership.mem (γ := Filter F) (𝓝 0) U
⊢ Absorbs R U (image2 (fun (f : UniformConvergenceCLM σ F 𝔖) (x : E) ↦ (f : (a : E) → F) x) S s)
have h : ∀ (c : R)
  (hc :
    S ⊆
      HSMul.hSMul (β := Set (UniformConvergenceCLM σ F 𝔖)) c
        {x : UniformConvergenceCLM σ F 𝔖 | MapsTo (⇑x : (a : E) → F) s U}),
  image2 (fun (f : UniformConvergenceCLM σ F 𝔖) (x : E) ↦ (f : (a : E) → F) x) S s ⊆ c • U
Tactic: filter_upwards [hS (eventually_nhds_zero_mapsTo σ hs hU)] with c hc
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (goal)
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜₂ F
R : Type u_6
inst_7 : SeminormedRing R
inst_8 : TopologicalSpace F
inst_9 : IsTopologicalAddGroup F
inst_10 : DistribMulAction R F
inst_11 : ContinuousConstSMul R F
inst_12 : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
S : Set (UniformConvergenceCLM σ F 𝔖)
hS : IsVonNBounded R S
s : Set E
hs : s ∈ 𝔖
U : Set F
hU : Membership.mem (γ := Filter F) (𝓝 0) U
c : R
hc :
  S ⊆
    HSMul.hSMul (β := Set (UniformConvergenceCLM σ F 𝔖)) c
      {x : UniformConvergenceCLM σ F 𝔖 | MapsTo (⇑x : (a : E) → F) s U}
⊢ image2 (fun (f : UniformConvergenceCLM σ F 𝔖) (x : E) ↦ (f : (a : E) → F) x) S s ⊆ c • U
have h : ∀ x ∈ S, ∀ y ∈ s, Membership.mem (α := F) (c • U) ((x : (a : E) → F) y : F)
Tactic: rw [image2_subset_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (goal)
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜₂ F
R : Type u_6
inst_7 : SeminormedRing R
inst_8 : TopologicalSpace F
inst_9 : IsTopologicalAddGroup F
inst_10 : DistribMulAction R F
inst_11 : ContinuousConstSMul R F
inst_12 : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
S : Set (UniformConvergenceCLM σ F 𝔖)
hS : IsVonNBounded R S
s : Set E
hs : s ∈ 𝔖
U : Set F
hU : Membership.mem (γ := Filter F) (𝓝 0) U
c : R
hc :
  S ⊆
    HSMul.hSMul (β := Set (UniformConvergenceCLM σ F 𝔖)) c
      {x : UniformConvergenceCLM σ F 𝔖 | MapsTo (⇑x : (a : E) → F) s U}
f : UniformConvergenceCLM σ F 𝔖
hf : f ∈ S
x : E
hx : x ∈ s
⊢ Membership.mem (α := F) (c • U) ((f : (a : E) → F) x : F)
have h : ∀ (g : UniformConvergenceCLM σ F 𝔖)
  (hg :
    Membership.mem (γ := Set (UniformConvergenceCLM σ F 𝔖))
      {x : UniformConvergenceCLM σ F 𝔖 | MapsTo (⇑x : (a : E) → F) s U} g)
  (hf : (fun (x : UniformConvergenceCLM σ F 𝔖) ↦ c • x) g ∈ S),
  Membership.mem (α := F) (c • U) (((fun (x : UniformConvergenceCLM σ F 𝔖) ↦ c • x) g : (a : E) → F) x : F)
Tactic: rcases hc hf with ⟨g, hg, rfl⟩
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (goal)
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜₂ F
R : Type u_6
inst_7 : NormedDivisionRing R
inst_8 : TopologicalSpace F
inst_9 : IsTopologicalAddGroup F
inst_10 : Module R F
inst_11 : ContinuousConstSMul R F
inst_12 : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
S : Set (UniformConvergenceCLM σ F 𝔖)
⊢ IsVonNBounded R S ↔
    ∀ s ∈ 𝔖,
      IsVonNBounded.{u_6, u_4} R (E := F)
        (image2 (fun (f : UniformConvergenceCLM σ F 𝔖) (x : E) ↦ (f : (a : E) → F) x) S s)
have refine : ∀
  (h :
    ∀ s ∈ 𝔖,
      IsVonNBounded.{u_6, u_4} R (E := F)
        (image2 (fun (f : UniformConvergenceCLM σ F 𝔖) (x : E) ↦ (f : (a : E) → F) x) S s)),
  IsVonNBounded R S
Tactic: refine ⟨fun hS s hs ↦ isVonNBounded_image2_apply hS hs, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (goal)
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜₂ F
R : Type u_6
inst_7 : NormedDivisionRing R
inst_8 : TopologicalSpace F
inst_9 : IsTopologicalAddGroup F
inst_10 : Module R F
inst_11 : ContinuousConstSMul R F
inst_12 : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
S : Set (UniformConvergenceCLM σ F 𝔖)
h :
  ∀ s ∈ 𝔖,
    IsVonNBounded.{u_6, u_4} R (E := F)
      (image2 (fun (f : UniformConvergenceCLM σ F 𝔖) (x : E) ↦ (f : (a : E) → F) x) S s)
⊢ IsVonNBounded R S
have simp_rw : ∀ (i : Set E) (i_1 : i ∈ 𝔖) (i_2 : Set F) (i_3 : Membership.mem (γ := Filter F) (𝓝 0) i_2),
  {f : UniformConvergenceCLM σ F 𝔖 | MapsTo (⇑f : (a : E) → F) i i_2} ∈ absorbing R S
Tactic: simp_rw [isVonNBounded_iff_absorbing_le, nhds_zero_eq, le_iInf_iff, le_principal_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (goal)
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜₂ F
R : Type u_6
inst_7 : NormedDivisionRing R
inst_8 : TopologicalSpace F
inst_9 : IsTopologicalAddGroup F
inst_10 : Module R F
inst_11 : ContinuousConstSMul R F
inst_12 : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
S : Set (UniformConvergenceCLM σ F 𝔖)
h :
  ∀ s ∈ 𝔖,
    IsVonNBounded.{u_6, u_4} R (E := F)
      (image2 (fun (f : UniformConvergenceCLM σ F 𝔖) (x : E) ↦ (f : (a : E) → F) x) S s)
s : Set E
hs : s ∈ 𝔖
U : Set F
hU : Membership.mem (γ := Filter F) (𝓝 0) U
⊢ {f : UniformConvergenceCLM σ F 𝔖 | MapsTo (⇑f : (a : E) → F) s U} ∈ absorbing R S
have rw : ∀ᶠ (a : R) in cobounded R,
  S ⊆
    HSMul.hSMul (β := Set (UniformConvergenceCLM σ F 𝔖)) a
      {f : UniformConvergenceCLM σ F 𝔖 | MapsTo (⇑f : (a : E) → F) s U}
Tactic: rw [Filter.mem_absorbing, Absorbs]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (goal)
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜₂ F
R : Type u_6
inst_7 : NormedDivisionRing R
inst_8 : TopologicalSpace F
inst_9 : IsTopologicalAddGroup F
inst_10 : Module R F
inst_11 : ContinuousConstSMul R F
inst_12 : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
S : Set (UniformConvergenceCLM σ F 𝔖)
h :
  ∀ s ∈ 𝔖,
    IsVonNBounded.{u_6, u_4} R (E := F)
      (image2 (fun (f : UniformConvergenceCLM σ F 𝔖) (x : E) ↦ (f : (a : E) → F) x) S s)
s : Set E
hs : s ∈ 𝔖
U : Set F
hU : Membership.mem (γ := Filter F) (𝓝 0) U
⊢ ∀ᶠ (a : R) in cobounded R,
    S ⊆
      HSMul.hSMul (β := Set (UniformConvergenceCLM σ F 𝔖)) a
        {f : UniformConvergenceCLM σ F 𝔖 | MapsTo (⇑f : (a : E) → F) s U}
have h₁ : ∀ (c : R) (hc : image2 (fun (f : UniformConvergenceCLM σ F 𝔖) (x : E) ↦ (f : (a : E) → F) x) S s ⊆ c • U) (hc₀ : c ≠ 0)
  ⦃f : UniformConvergenceCLM σ F 𝔖⦄ (hf : f ∈ S),
  f ∈
    HSMul.hSMul (β := Set (UniformConvergenceCLM σ F 𝔖)) c
      {f : UniformConvergenceCLM σ F 𝔖 | MapsTo (⇑f : (a : E) → F) s U}
Tactic: filter_upwards [h s hs hU, eventually_ne_cobounded 0] with c hc hc₀ f hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (goal)
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜₂ F
R : Type u_6
inst_7 : NormedDivisionRing R
inst_8 : TopologicalSpace F
inst_9 : IsTopologicalAddGroup F
inst_10 : Module R F
inst_11 : ContinuousConstSMul R F
inst_12 : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
S : Set (UniformConvergenceCLM σ F 𝔖)
h :
  ∀ s ∈ 𝔖,
    IsVonNBounded.{u_6, u_4} R (E := F)
      (image2 (fun (f : UniformConvergenceCLM σ F 𝔖) (x : E) ↦ (f : (a : E) → F) x) S s)
s : Set E
hs : s ∈ 𝔖
U : Set F
hU : Membership.mem (γ := Filter F) (𝓝 0) U
c : R
hc : image2 (fun (f : UniformConvergenceCLM σ F 𝔖) (x : E) ↦ (f : (a : E) → F) x) S s ⊆ c • U
hc₀ : c ≠ 0
f : UniformConvergenceCLM σ F 𝔖
hf : f ∈ S
⊢ f ∈
    HSMul.hSMul (β := Set (UniformConvergenceCLM σ F 𝔖)) c
      {f : UniformConvergenceCLM σ F 𝔖 | MapsTo (⇑f : (a : E) → F) s U}
have h₁ : Membership.mem (γ := Set (UniformConvergenceCLM σ F 𝔖))
  {f : UniformConvergenceCLM σ F 𝔖 | MapsTo (⇑f : (a : E) → F) s U} (c⁻¹ • f)
Tactic: rw [mem_smul_set_iff_inv_smul_mem₀ hc₀]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (goal)
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜₂ F
ι : Type u_6
p : Filter ι
inst_7 : UniformSpace F
inst_8 : IsUniformAddGroup F
𝔖 : Set (Set E)
a : ι → UniformConvergenceCLM σ F 𝔖
a₀ : UniformConvergenceCLM σ F 𝔖
⊢ Tendsto a p (𝓝 a₀) ↔
    ∀ s ∈ 𝔖,
      TendstoUniformlyOn.{u_3, u_4, u_6} (β := F) (fun (x1 : ι) (x2 : E) ↦ (a x1 : (a : E) → F) x2) (⇑a₀ : (a : E) → F)
        p s
have rw : (∀ s ∈ 𝔖,
    TendstoUniformlyOn.{u_3, u_4, u_6} (β := F)
      (comp (β := E →ᵤ[𝔖] F) (⇑(UniformOnFun.toFun 𝔖) : (a : E →ᵤ[𝔖] F) → E → F)
        (comp (β := E → F) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → F) → E →ᵤ[𝔖] F) (DFunLike.coe (β := fun (a : E) ↦ F)) ∘
          a))
      ((UniformOnFun.toFun 𝔖 : (a : E →ᵤ[𝔖] F) → E → F)
        (comp (β := E → F) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → F) → E →ᵤ[𝔖] F) (DFunLike.coe (β := fun (a : E) ↦ F))
          a₀))
      p s) ↔
  ∀ s ∈ 𝔖,
    TendstoUniformlyOn.{u_3, u_4, u_6} (β := F) (fun (x1 : ι) (x2 : E) ↦ (a x1 : (a : E) → F) x2) (⇑a₀ : (a : E) → F) p
      s
Tactic: rw [(isEmbedding_coeFn σ F 𝔖).tendsto_nhds_iff, UniformOnFun.tendsto_iff_tendstoUniformlyOn]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (goal)
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
G : Type u_5
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜₂ F
inst_7 : AddCommGroup G
inst_8 : UniformSpace G
inst_9 : IsUniformAddGroup G
𝕜₃ : Type u_6
inst_10 : NormedField 𝕜₃
inst_11 : Module 𝕜₃ G
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst_12 : RingHomCompTriple σ τ ρ
inst_13 : UniformSpace F
inst_14 : IsUniformAddGroup F
g : F →SL[τ] G
hg : IsUniformInducing.{u_4, u_5} (α := F) (β := G) (⇑g : (a : F) → G)
𝔖 : Set (Set E)
⊢ IsUniformInducing (α := UniformConvergenceCLM σ F 𝔖) g.comp
have rw : IsUniformInducing (α := UniformConvergenceCLM σ F 𝔖) (β := E →ᵤ[𝔖] G)
  (comp (β := E → G) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → G) → E →ᵤ[𝔖] G) (DFunLike.coe (β := fun (a : E) ↦ G)) ∘ g.comp)
Tactic: rw [← (isUniformInducing_coeFn _ _ _).of_comp_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (goal)
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜₂ F
inst_7 : UniformSpace F
inst_8 : IsUniformAddGroup F
inst_9 : ContinuousSMul 𝕜₂ F
inst_10 : CompleteSpace F
𝔖 : Set (Set E)
h𝔖 : IsCoherentWith 𝔖
h𝔖U : ⋃₀ 𝔖 = univ
⊢ CompleteSpace (UniformConvergenceCLM σ F 𝔖)
have inr : ∀
  (this :
    ∀ (F : Type u_4) [inst_11 : AddCommGroup F] [inst_12 : Module 𝕜₂ F] [inst_13 : UniformSpace F]
      [inst_14 : IsUniformAddGroup F] [ContinuousSMul 𝕜₂ F] [CompleteSpace F] (hF : T2Space F),
      CompleteSpace (UniformConvergenceCLM σ F 𝔖))
  (hF : ¬T2Space F), CompleteSpace (UniformConvergenceCLM σ F 𝔖)
Tactic: wlog hF : T2Space F generalizing F
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (goal)
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜₂ F
inst_7 : UniformSpace F
inst_8 : IsUniformAddGroup F
inst_9 : ContinuousSMul 𝕜₂ F
inst_10 : CompleteSpace F
𝔖 : Set (Set E)
h𝔖 : IsCoherentWith 𝔖
h𝔖U : ⋃₀ 𝔖 = univ
inr :
  ∀
    (this :
      ∀ (F : Type u_4) [inst_11 : AddCommGroup F] [inst_12 : Module 𝕜₂ F] [inst_13 : UniformSpace F]
        [inst_14 : IsUniformAddGroup F] [ContinuousSMul 𝕜₂ F] [CompleteSpace F] (hF : T2Space F),
        CompleteSpace (UniformConvergenceCLM σ F 𝔖))
    (hF : ¬T2Space F), CompleteSpace (UniformConvergenceCLM σ F 𝔖)
⊢ CompleteSpace (UniformConvergenceCLM σ F 𝔖)
have wlog : ∀ (F : Type u_4) [inst_11 : AddCommGroup F] [inst_12 : Module 𝕜₂ F] [inst_13 : UniformSpace F]
  [inst_14 : IsUniformAddGroup F] [ContinuousSMul 𝕜₂ F] [CompleteSpace F] (hF : T2Space F),
  CompleteSpace (UniformConvergenceCLM σ F 𝔖)
Tactic: wlog hF : T2Space F generalizing F
Cleared hypotheses: inst_7, inst_8, inst_9, inst_10
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (goal)
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜₂ F
inst_7 : UniformSpace F
inst_8 : IsUniformAddGroup F
inst_9 : ContinuousSMul 𝕜₂ F
inst_10 : CompleteSpace F
𝔖 : Set (Set E)
h𝔖 : IsCoherentWith 𝔖
h𝔖U : ⋃₀ 𝔖 = univ
this :
  ∀ (F : Type u_4) [inst_11 : AddCommGroup F] [inst_12 : Module 𝕜₂ F] [inst_13 : UniformSpace F]
    [inst_14 : IsUniformAddGroup F] [ContinuousSMul 𝕜₂ F] [CompleteSpace F] (hF : T2Space F),
    CompleteSpace (UniformConvergenceCLM σ F 𝔖)
hF : ¬T2Space F
⊢ CompleteSpace (UniformConvergenceCLM σ F 𝔖)
have inr : CompleteSpace (UniformConvergenceCLM.{u_1, u_2, u_3, u_4} σ (SeparationQuotient F) 𝔖)
Tactic: rw [(isUniformInducing_postcomp σ (SeparationQuotient.mkCLM 𝕜₂ F)
      SeparationQuotient.isUniformInducing_mk _).completeSpace_congr]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (goal)
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜₂ F
inst_7 : UniformSpace F
inst_8 : IsUniformAddGroup F
inst_9 : ContinuousSMul 𝕜₂ F
inst_10 : CompleteSpace F
𝔖 : Set (Set E)
h𝔖 : IsCoherentWith 𝔖
h𝔖U : ⋃₀ 𝔖 = univ
this :
  ∀ (F : Type u_4) [inst_11 : AddCommGroup F] [inst_12 : Module 𝕜₂ F] [inst_13 : UniformSpace F]
    [inst_14 : IsUniformAddGroup F] [ContinuousSMul 𝕜₂ F] [CompleteSpace F] (hF : T2Space F),
    CompleteSpace (UniformConvergenceCLM σ F 𝔖)
hF : ¬T2Space F
inr : CompleteSpace (UniformConvergenceCLM.{u_1, u_2, u_3, u_4} σ (SeparationQuotient F) 𝔖)
⊢ CompleteSpace (UniformConvergenceCLM σ F 𝔖)
have inr₁ : Surjective (α := UniformConvergenceCLM σ F 𝔖) (β :=
  UniformConvergenceCLM.{u_1, u_2, u_3, u_4} σ (SeparationQuotient F) 𝔖)
  (ContinuousLinearMap.comp (SeparationQuotient.mkCLM 𝕜₂ F))
Tactic: rw [(isUniformInducing_postcomp σ (SeparationQuotient.mkCLM 𝕜₂ F)
      SeparationQuotient.isUniformInducing_mk _).completeSpace_congr]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (goal)
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F_1 : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F_1
inst_6 : Module 𝕜₂ F_1
𝔖 : Set (Set E)
h𝔖 : IsCoherentWith 𝔖
h𝔖U : ⋃₀ 𝔖 = univ
F : Type u_4
inst_7 : AddCommGroup F
inst_8 : Module 𝕜₂ F
inst_9 : UniformSpace F
inst_10 : IsUniformAddGroup F
inst_11 : ContinuousSMul 𝕜₂ F
inst_12 : CompleteSpace F
hF : T2Space F
⊢ CompleteSpace (UniformConvergenceCLM σ F 𝔖)
have rw : IsComplete (α := E →ᵤ[𝔖] F)
  (range (ι := UniformConvergenceCLM σ F 𝔖)
    (comp (β := E → F) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → F) → E →ᵤ[𝔖] F) (DFunLike.coe (β := fun (a : E) ↦ F))))
Tactic: rw [completeSpace_iff_isComplete_range (isUniformInducing_coeFn _ _ _)]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (goal)
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F_1 : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F_1
inst_6 : Module 𝕜₂ F_1
𝔖 : Set (Set E)
h𝔖 : IsCoherentWith 𝔖
h𝔖U : ⋃₀ 𝔖 = univ
F : Type u_4
inst_7 : AddCommGroup F
inst_8 : Module 𝕜₂ F
inst_9 : UniformSpace F
inst_10 : IsUniformAddGroup F
inst_11 : ContinuousSMul 𝕜₂ F
inst_12 : CompleteSpace F
hF : T2Space F
⊢ IsComplete (α := E →ᵤ[𝔖] F)
    (range (ι := UniformConvergenceCLM σ F 𝔖)
      (comp (β := E → F) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → F) → E →ᵤ[𝔖] F) (DFunLike.coe (β := fun (a : E) ↦ F))))
have h : IsClosed[(UniformOnFun.uniformSpace E F 𝔖).toTopologicalSpace]
  (range (ι := UniformConvergenceCLM σ F 𝔖)
    (comp (β := E → F) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → F) → E →ᵤ[𝔖] F) (DFunLike.coe (β := fun (a : E) ↦ F))))
Tactic: apply IsClosed.isComplete
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (hypothesis)
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F_1 : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F_1
inst_6 : Module 𝕜₂ F_1
𝔖 : Set (Set E)
h𝔖 : IsCoherentWith 𝔖
h𝔖U : ⋃₀ 𝔖 = univ
F : Type u_4
inst_7 : AddCommGroup F
inst_8 : Module 𝕜₂ F
inst_9 : UniformSpace F
inst_10 : IsUniformAddGroup F
inst_11 : ContinuousSMul 𝕜₂ F
inst_12 : CompleteSpace F
hF : T2Space F
⊢ IsClosed[(UniformOnFun.uniformSpace E F 𝔖).toTopologicalSpace]
    (range (ι := UniformConvergenceCLM σ F 𝔖)
      (comp (β := E → F) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → F) → E →ᵤ[𝔖] F) (DFunLike.coe (β := fun (a : E) ↦ F))))
have H₁ : IsClosed[UniformOnFun.topologicalSpace E F 𝔖]
  {f : E →ᵤ[𝔖] F | Continuous[inst_4, inst_9.toTopologicalSpace] ((UniformOnFun.toFun 𝔖 : (a : E →ᵤ[𝔖] F) → E → F) f)}
Tactic: have H₁ : IsClosed {f : E →ᵤ[𝔖] F | Continuous ((UniformOnFun.toFun 𝔖) f)} :=
    UniformOnFun.isClosed_setOf_continuous h𝔖
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (goal)
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F_1 : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F_1
inst_6 : Module 𝕜₂ F_1
𝔖 : Set (Set E)
h𝔖 : IsCoherentWith 𝔖
h𝔖U : ⋃₀ 𝔖 = univ
F : Type u_4
inst_7 : AddCommGroup F
inst_8 : Module 𝕜₂ F
inst_9 : UniformSpace F
inst_10 : IsUniformAddGroup F
inst_11 : ContinuousSMul 𝕜₂ F
inst_12 : CompleteSpace F
hF : T2Space F
H₁ :
  IsClosed[UniformOnFun.topologicalSpace E F 𝔖]
    {f : E →ᵤ[𝔖] F | Continuous[inst_4, inst_9.toTopologicalSpace] ((UniformOnFun.toFun 𝔖 : (a : E →ᵤ[𝔖] F) → E → F) f)}
⊢ IsClosed[(UniformOnFun.uniformSpace E F 𝔖).toTopologicalSpace]
    (range (ι := UniformConvergenceCLM σ F 𝔖)
      (comp (β := E → F) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → F) → E →ᵤ[𝔖] F) (DFunLike.coe (β := fun (a : E) ↦ F))))
have h : Eq (α := Set (E →ᵤ[𝔖] F))
  (range (ι := UniformConvergenceCLM σ F 𝔖)
    (comp (β := E → F) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → F) → E →ᵤ[𝔖] F) (DFunLike.coe (β := fun (a : E) ↦ F))))
  ({f : E →ᵤ[𝔖] F |
      Continuous[inst_4, inst_9.toTopologicalSpace] ((UniformOnFun.toFun 𝔖 : (a : E →ᵤ[𝔖] F) → E → F) f)} ∩
    preimage (β := E → F) (⇑(UniformOnFun.toFun 𝔖) : (a : E →ᵤ[𝔖] F) → E → F)
      (range (ι := E →ₛₗ[σ] F) (DFunLike.coe (β := fun (x : E) ↦ F))))
Tactic: convert!
    H₁.inter <|
      (LinearMap.isClosed_range_coe E F σ).preimage
        (UniformOnFun.uniformContinuous_toFun h𝔖U).continuous
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (goal)
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜₂ F
𝔖₁ 𝔖₂ : Set (Set E)
inst_7 : UniformSpace F
inst_8 : IsUniformAddGroup F
h : 𝔖₂ ⊆ 𝔖₁
⊢ LE.le (α := UniformSpace (UniformConvergenceCLM σ F 𝔖₁)) (instUniformSpace σ F 𝔖₁) (instUniformSpace σ F 𝔖₂)
have simp_rw : LE.le (α := UniformSpace (UniformConvergenceCLM σ F 𝔖₁))
  (UniformSpace.comap
    (comp (β := E → F) (⇑(UniformOnFun.ofFun 𝔖₁) : (a : E → F) → E →ᵤ[𝔖₁] F) (DFunLike.coe (β := fun (a : E) ↦ F)))
    (UniformOnFun.uniformSpace E F 𝔖₁))
  (UniformSpace.comap
    (comp (β := E → F) (⇑(UniformOnFun.ofFun 𝔖₂) : (a : E → F) → E →ᵤ[𝔖₂] F) (DFunLike.coe (β := fun (a : E) ↦ F)))
    (UniformOnFun.uniformSpace E F 𝔖₂))
Tactic: simp_rw [uniformSpace_eq]