awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Topology (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → TopologicalSpace (E i)
inst_2 : (i : ι) → AddCommGroup (E i)
inst_3 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : UniformSpace F
inst_7 : IsUniformAddGroup F
G : Type u_5
inst_8 : AddCommGroup G
inst_9 : UniformSpace G
inst_10 : IsUniformAddGroup G
inst_11 : Module 𝕜 G
g : F →L[𝕜] G
hg : IsUniformInducing.{u_4, u_5} (α := F) (β := G) (⇑g : (a : F) → G)
⊢ IsUniformInducing (α := ContinuousMultilinearMap 𝕜 E F) (g.compContinuousMultilinearMap (M₁ := E))
have rw : IsUniformInducing (α := ContinuousMultilinearMap 𝕜 E F)
  (toUniformOnFun (E := E) ∘ g.compContinuousMultilinearMap (M₁ := E))
Tactic: rw [← isUniformInducing_toUniformOnFun.of_comp_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Topology (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → TopologicalSpace (E i)
inst_2 : (i : ι) → AddCommGroup (E i)
inst_3 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : UniformSpace F
inst_7 : IsUniformAddGroup F
inst_8 : ∀ (i : ι), ContinuousSMul.{u_1, u_3} 𝕜 (E i)
inst_9 : ContinuousConstSMul 𝕜 F
inst_10 : CompleteSpace F
h : IsCoherentWith (X := (i : ι) → E i) {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}
⊢ CompleteSpace (ContinuousMultilinearMap 𝕜 E F)
have inr : ∀
  (this :
    ∀ {F : Type u_4} [inst_11 : AddCommGroup F] [inst_12 : Module 𝕜 F] [inst_13 : UniformSpace F]
      [inst_14 : IsUniformAddGroup F] [ContinuousConstSMul 𝕜 F] [CompleteSpace F] (hF : T2Space F),
      CompleteSpace (ContinuousMultilinearMap 𝕜 E F))
  (hF : ¬T2Space F), CompleteSpace (ContinuousMultilinearMap 𝕜 E F)
Tactic: wlog hF : T2Space F generalizing F
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Topology (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → TopologicalSpace (E i)
inst_2 : (i : ι) → AddCommGroup (E i)
inst_3 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : UniformSpace F
inst_7 : IsUniformAddGroup F
inst_8 : ∀ (i : ι), ContinuousSMul.{u_1, u_3} 𝕜 (E i)
inst_9 : ContinuousConstSMul 𝕜 F
inst_10 : CompleteSpace F
h : IsCoherentWith (X := (i : ι) → E i) {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}
inr :
  ∀
    (this :
      ∀ {F : Type u_4} [inst_11 : AddCommGroup F] [inst_12 : Module 𝕜 F] [inst_13 : UniformSpace F]
        [inst_14 : IsUniformAddGroup F] [ContinuousConstSMul 𝕜 F] [CompleteSpace F] (hF : T2Space F),
        CompleteSpace (ContinuousMultilinearMap 𝕜 E F))
    (hF : ¬T2Space F), CompleteSpace (ContinuousMultilinearMap 𝕜 E F)
⊢ CompleteSpace (ContinuousMultilinearMap 𝕜 E F)
have wlog : ∀ {F : Type u_4} [inst_11 : AddCommGroup F] [inst_12 : Module 𝕜 F] [inst_13 : UniformSpace F]
  [inst_14 : IsUniformAddGroup F] [ContinuousConstSMul 𝕜 F] [CompleteSpace F] (hF : T2Space F),
  CompleteSpace (ContinuousMultilinearMap 𝕜 E F)
Tactic: wlog hF : T2Space F generalizing F
Cleared hypotheses: inst_9, inst_10
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Topology (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → TopologicalSpace (E i)
inst_2 : (i : ι) → AddCommGroup (E i)
inst_3 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : UniformSpace F
inst_7 : IsUniformAddGroup F
inst_8 : ∀ (i : ι), ContinuousSMul.{u_1, u_3} 𝕜 (E i)
inst_9 : ContinuousConstSMul 𝕜 F
inst_10 : CompleteSpace F
h : IsCoherentWith (X := (i : ι) → E i) {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}
this :
  ∀ {F : Type u_4} [inst_11 : AddCommGroup F] [inst_12 : Module 𝕜 F] [inst_13 : UniformSpace F]
    [inst_14 : IsUniformAddGroup F] [ContinuousConstSMul 𝕜 F] [CompleteSpace F] (hF : T2Space F),
    CompleteSpace (ContinuousMultilinearMap 𝕜 E F)
hF : ¬T2Space F
⊢ CompleteSpace (ContinuousMultilinearMap 𝕜 E F)
have inr : CompleteSpace (ContinuousMultilinearMap.{u_1, u_2, u_3, u_4} 𝕜 E (SeparationQuotient F))
Tactic: rw [(isUniformInducing_postcomp (SeparationQuotient.mkCLM _ _)
      SeparationQuotient.isUniformInducing_mk).completeSpace_congr]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Topology (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → TopologicalSpace (E i)
inst_2 : (i : ι) → AddCommGroup (E i)
inst_3 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : UniformSpace F
inst_7 : IsUniformAddGroup F
inst_8 : ∀ (i : ι), ContinuousSMul.{u_1, u_3} 𝕜 (E i)
inst_9 : ContinuousConstSMul 𝕜 F
inst_10 : CompleteSpace F
h : IsCoherentWith (X := (i : ι) → E i) {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}
this :
  ∀ {F : Type u_4} [inst_11 : AddCommGroup F] [inst_12 : Module 𝕜 F] [inst_13 : UniformSpace F]
    [inst_14 : IsUniformAddGroup F] [ContinuousConstSMul 𝕜 F] [CompleteSpace F] (hF : T2Space F),
    CompleteSpace (ContinuousMultilinearMap 𝕜 E F)
hF : ¬T2Space F
inr : CompleteSpace (ContinuousMultilinearMap.{u_1, u_2, u_3, u_4} 𝕜 E (SeparationQuotient F))
⊢ CompleteSpace (ContinuousMultilinearMap 𝕜 E F)
have inr₁ : Surjective (α := ContinuousMultilinearMap 𝕜 E F) (β :=
  ContinuousMultilinearMap.{u_1, u_2, u_3, u_4} 𝕜 E (SeparationQuotient F))
  (ContinuousLinearMap.compContinuousMultilinearMap (M₁ := E) (SeparationQuotient.mkCLM 𝕜 F))
Tactic: rw [(isUniformInducing_postcomp (SeparationQuotient.mkCLM _ _)
      SeparationQuotient.isUniformInducing_mk).completeSpace_congr]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Topology (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → TopologicalSpace (E i)
inst_2 : (i : ι) → AddCommGroup (E i)
inst_3 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : UniformSpace F
inst_7 : IsUniformAddGroup F
inst_8 : ∀ (i : ι), ContinuousSMul.{u_1, u_3} 𝕜 (E i)
inst_9 : ContinuousConstSMul 𝕜 F
inst_10 : CompleteSpace F
h : IsCoherentWith (X := (i : ι) → E i) {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}
this :
  ∀ {F : Type u_4} [inst_11 : AddCommGroup F] [inst_12 : Module 𝕜 F] [inst_13 : UniformSpace F]
    [inst_14 : IsUniformAddGroup F] [ContinuousConstSMul 𝕜 F] [CompleteSpace F] (hF : T2Space F),
    CompleteSpace (ContinuousMultilinearMap 𝕜 E F)
hF : ¬T2Space F
f : ContinuousMultilinearMap.{u_1, u_2, u_3, u_4} 𝕜 E (SeparationQuotient F)
⊢ ∃ (a : ContinuousMultilinearMap 𝕜 E F),
    ContinuousLinearMap.compContinuousMultilinearMap (M₁ := E) (SeparationQuotient.mkCLM 𝕜 F) a = f
have h₁ : ContinuousLinearMap.compContinuousMultilinearMap (M₁ := E) (M₂ := F) (SeparationQuotient.mkCLM 𝕜 F)
    (ContinuousLinearMap.compContinuousMultilinearMap (M₁ := E) (SeparationQuotient.outCLM 𝕜 F) f) =
  f
Tactic: use (SeparationQuotient.outCLM _ _).compContinuousMultilinearMap f
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Topology (hypothesis)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F_1 : Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → TopologicalSpace (E i)
inst_2 : (i : ι) → AddCommGroup (E i)
inst_3 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_4 : AddCommGroup F_1
inst_5 : Module 𝕜 F_1
inst_6 : UniformSpace F_1
inst_7 : IsUniformAddGroup F_1
inst_8 : ∀ (i : ι), ContinuousSMul.{u_1, u_3} 𝕜 (E i)
h : IsCoherentWith (X := (i : ι) → E i) {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}
F : Type u_4
inst_9 : AddCommGroup F
inst_10 : Module 𝕜 F
inst_11 : UniformSpace F
inst_12 : IsUniformAddGroup F
inst_13 : ContinuousConstSMul 𝕜 F
inst_14 : CompleteSpace F
hF : T2Space F
⊢ CompleteSpace (ContinuousMultilinearMap 𝕜 E F)
have H : ∀ {m : (i : ι) → E i},
  Continuous[topologicalSpace ((i : ι) → E i) F {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s},
      inst_11.toTopologicalSpace]
    fun (f : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) ↦
    (toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
        (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
      f m
Tactic: have H : ∀ {m : Π i, E i},
      Continuous fun f : (Π i, E i) →ᵤ[{s | IsVonNBounded 𝕜 s}] F ↦ toFun _ f m :=
    (uniformContinuous_eval (sUnion_isVonNBounded_eq_univ) _).continuous
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Topology (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → TopologicalSpace (E i)
inst_2 : (i : ι) → AddCommGroup (E i)
inst_3 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : UniformSpace F
inst_7 : IsUniformAddGroup F
inst_8 : ∀ (i : ι), ContinuousSMul.{u_1, u_3} 𝕜 (E i)
inst_9 : ContinuousConstSMul 𝕜 F
inst_10 : CompleteSpace F
h : IsCoherentWith (X := (i : ι) → E i) {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}
⊢ CompleteSpace (ContinuousMultilinearMap 𝕜 E F)
have inr : ∀
  (this :
    ∀ {F : Type u_4} [inst_11 : AddCommGroup F] [inst_12 : Module 𝕜 F] [inst_13 : UniformSpace F]
      [inst_14 : IsUniformAddGroup F] [ContinuousConstSMul 𝕜 F] [CompleteSpace F] (hF : T2Space F),
      CompleteSpace (ContinuousMultilinearMap 𝕜 E F))
  (hF : ¬T2Space F), CompleteSpace (ContinuousMultilinearMap 𝕜 E F)
Tactic: classical
  wlog hF : T2Space F generalizing F
  · rw [(isUniformInducing_postcomp (SeparationQuotient.mkCLM _ _)
      SeparationQuotient.isUniformInducing_mk).completeSpace_congr]
    · exact this inferInstance
    · intro f
      use (SeparationQuotient.outCLM _ _).compContinuousMultilinearMap f
      simp [DFunLike.ext_iff]
  have H : ∀ {m : Π i, E i},
      Continuous fun f : (Π i, E i) →ᵤ[{s | IsVonNBounded 𝕜 s}] F ↦ toFun _ f m :=
    (uniformContinuous_eval (sUnion_isVonNBounded_eq_univ) _).continuous
  rw [completeSpace_iff_isComplete_range isUniformInducing_toUniformOnFun, range_toUniformOnFun]
  simp only [setOf_and, setOf_forall]
  apply_rules [IsClosed.isComplete, IsClosed.inter]
  · exact UniformOnFun.isClosed_setOf_continuous h
  · exact isClosed_iInter fun m ↦ isClosed_iInter fun i ↦
      isClosed_iInter fun x ↦ isClosed_iInter fun y ↦ isClosed_eq H (H.add H)
  · exact isClosed_iInter fun m ↦ isClosed_iInter fun i ↦
      isClosed_iInter fun c ↦ isClosed_iInter fun x ↦ isClosed_eq H (H.const_smul _)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Topology (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → TopologicalSpace (E i)
inst_2 : (i : ι) → AddCommGroup (E i)
inst_3 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : UniformSpace F
inst_7 : IsUniformAddGroup F
inst_8 : ∀ (i : ι), ContinuousSMul.{u_1, u_3} 𝕜 (E i)
inst_9 : ContinuousConstSMul 𝕜 F
inst_10 : CompleteSpace F
h : IsCoherentWith (X := (i : ι) → E i) {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}
inr :
  ∀
    (this :
      ∀ {F : Type u_4} [inst_11 : AddCommGroup F] [inst_12 : Module 𝕜 F] [inst_13 : UniformSpace F]
        [inst_14 : IsUniformAddGroup F] [ContinuousConstSMul 𝕜 F] [CompleteSpace F] (hF : T2Space F),
        CompleteSpace (ContinuousMultilinearMap 𝕜 E F))
    (hF : ¬T2Space F), CompleteSpace (ContinuousMultilinearMap 𝕜 E F)
⊢ CompleteSpace (ContinuousMultilinearMap 𝕜 E F)
have wlog : ∀ {F : Type u_4} [inst_11 : AddCommGroup F] [inst_12 : Module 𝕜 F] [inst_13 : UniformSpace F]
  [inst_14 : IsUniformAddGroup F] [ContinuousConstSMul 𝕜 F] [CompleteSpace F] (hF : T2Space F),
  CompleteSpace (ContinuousMultilinearMap 𝕜 E F)
Tactic: classical
  wlog hF : T2Space F generalizing F
  · rw [(isUniformInducing_postcomp (SeparationQuotient.mkCLM _ _)
      SeparationQuotient.isUniformInducing_mk).completeSpace_congr]
    · exact this inferInstance
    · intro f
      use (SeparationQuotient.outCLM _ _).compContinuousMultilinearMap f
      simp [DFunLike.ext_iff]
  have H : ∀ {m : Π i, E i},
      Continuous fun f : (Π i, E i) →ᵤ[{s | IsVonNBounded 𝕜 s}] F ↦ toFun _ f m :=
    (uniformContinuous_eval (sUnion_isVonNBounded_eq_univ) _).continuous
  rw [completeSpace_iff_isComplete_range isUniformInducing_toUniformOnFun, range_toUniformOnFun]
  simp only [setOf_and, setOf_forall]
  apply_rules [IsClosed.isComplete, IsClosed.inter]
  · exact UniformOnFun.isClosed_setOf_continuous h
  · exact isClosed_iInter fun m ↦ isClosed_iInter fun i ↦
      isClosed_iInter fun x ↦ isClosed_iInter fun y ↦ isClosed_eq H (H.add H)
  · exact isClosed_iInter fun m ↦ isClosed_iInter fun i ↦
      isClosed_iInter fun c ↦ isClosed_iInter fun x ↦ isClosed_eq H (H.const_smul _)
Cleared hypotheses: inst_9, inst_10
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Topology (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → TopologicalSpace (E i)
inst_2 : (i : ι) → AddCommGroup (E i)
inst_3 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : UniformSpace F
inst_7 : IsUniformAddGroup F
inst_8 : ∀ (i : ι), ContinuousSMul.{u_1, u_3} 𝕜 (E i)
inst_9 : ContinuousConstSMul 𝕜 F
inst_10 : CompleteSpace F
h : IsCoherentWith (X := (i : ι) → E i) {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}
inr :
  ∀
    (this :
      ∀ {F : Type u_4} [inst_11 : AddCommGroup F] [inst_12 : Module 𝕜 F] [inst_13 : UniformSpace F]
        [inst_14 : IsUniformAddGroup F] [ContinuousConstSMul 𝕜 F] [CompleteSpace F] (hF : T2Space F),
        CompleteSpace (ContinuousMultilinearMap 𝕜 E F))
    (hF : ¬T2Space F), CompleteSpace (ContinuousMultilinearMap 𝕜 E F)
wlog wlog₁ :
  ∀ {F : Type u_4} [inst_11 : AddCommGroup F] [inst_12 : Module 𝕜 F] [inst_13 : UniformSpace F]
    [inst_14 : IsUniformAddGroup F] [ContinuousConstSMul 𝕜 F] [CompleteSpace F] (hF : T2Space F),
    CompleteSpace (ContinuousMultilinearMap 𝕜 E F)
⊢ CompleteSpace (ContinuousMultilinearMap 𝕜 E F)
have wlog₂ : ∀ {F : Type u_4} [inst_11 : AddCommGroup F] [inst_12 : Module 𝕜 F] [inst_13 : UniformSpace F]
  [inst_14 : IsUniformAddGroup F] [ContinuousConstSMul 𝕜 F] [CompleteSpace F] (hF : T2Space F)
  (H :
    ∀ {m : (i : ι) → E i},
      Continuous (Y := F) fun (f : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) ↦
        (toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
            (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
          f m),
  CompleteSpace (ContinuousMultilinearMap 𝕜 E F)
Tactic: classical
  wlog hF : T2Space F generalizing F
  · rw [(isUniformInducing_postcomp (SeparationQuotient.mkCLM _ _)
      SeparationQuotient.isUniformInducing_mk).completeSpace_congr]
    · exact this inferInstance
    · intro f
      use (SeparationQuotient.outCLM _ _).compContinuousMultilinearMap f
      simp [DFunLike.ext_iff]
  have H : ∀ {m : Π i, E i},
      Continuous fun f : (Π i, E i) →ᵤ[{s | IsVonNBounded 𝕜 s}] F ↦ toFun _ f m :=
    (uniformContinuous_eval (sUnion_isVonNBounded_eq_univ) _).continuous
  rw [completeSpace_iff_isComplete_range isUniformInducing_toUniformOnFun, range_toUniformOnFun]
  simp only [setOf_and, setOf_forall]
  apply_rules [IsClosed.isComplete, IsClosed.inter]
  · exact UniformOnFun.isClosed_setOf_continuous h
  · exact isClosed_iInter fun m ↦ isClosed_iInter fun i ↦
      isClosed_iInter fun x ↦ isClosed_iInter fun y ↦ isClosed_eq H (H.add H)
  · exact isClosed_iInter fun m ↦ isClosed_iInter fun i ↦
      isClosed_iInter fun c ↦ isClosed_iInter fun x ↦ isClosed_eq H (H.const_smul _)
Cleared hypotheses: inst_9, inst_10
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Topology (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → TopologicalSpace (E i)
inst_2 : (i : ι) → AddCommGroup (E i)
inst_3 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : UniformSpace F
inst_7 : IsUniformAddGroup F
𝕜' : Type u_5
inst_8 : NontriviallyNormedField 𝕜'
inst_9 : NormedAlgebra 𝕜' 𝕜
inst_10 : (i : ι) → Module.{u_5, u_3} 𝕜' (E i)
inst_11 : ∀ (i : ι), IsScalarTower.{u_5, u_1, u_3} 𝕜' 𝕜 (E i)
inst_12 : Module 𝕜' F
inst_13 : IsScalarTower 𝕜' 𝕜 F
inst_14 : ∀ (i : ι), ContinuousSMul.{u_1, u_3} 𝕜 (E i)
this : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := ⋯ }
⊢ IsUniformEmbedding (α := ContinuousMultilinearMap 𝕜 E F) (β := ContinuousMultilinearMap 𝕜' E F)
    (restrictScalars 𝕜' (M₁ := E))
have rw : IsUniformEmbedding (α := ContinuousMultilinearMap 𝕜 E F) (β :=
  ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜' s}] F)
  (comp (β := ContinuousMultilinearMap 𝕜' E F) (toUniformOnFun (E := E)) (restrictScalars 𝕜' (M₁ := E)))
Tactic: rw [← isUniformEmbedding_toUniformOnFun.of_comp_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Topology (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → TopologicalSpace (E i)
inst_2 : (i : ι) → AddCommGroup (E i)
inst_3 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : UniformSpace F
inst_7 : IsUniformAddGroup F
𝕜' : Type u_5
inst_8 : NontriviallyNormedField 𝕜'
inst_9 : NormedAlgebra 𝕜' 𝕜
inst_10 : (i : ι) → Module.{u_5, u_3} 𝕜' (E i)
inst_11 : ∀ (i : ι), IsScalarTower.{u_5, u_1, u_3} 𝕜' 𝕜 (E i)
inst_12 : Module 𝕜' F
inst_13 : IsScalarTower 𝕜' 𝕜 F
inst_14 : ∀ (i : ι), ContinuousSMul.{u_1, u_3} 𝕜 (E i)
this : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := ⋯ }
⊢ IsUniformEmbedding (α := ContinuousMultilinearMap 𝕜 E F) (β :=
    ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜' s}] F)
    (comp (β := ContinuousMultilinearMap 𝕜' E F) (toUniformOnFun (E := E)) (restrictScalars 𝕜' (M₁ := E)))
have h : ∀ (s : Set ((i : ι) → E i)), IsVonNBounded 𝕜' s ↔ IsVonNBounded 𝕜 s
Tactic: convert! isUniformEmbedding_toUniformOnFun using 4 with s
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Topology (hypothesis)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → TopologicalSpace (E i)
inst_2 : (i : ι) → AddCommGroup (E i)
inst_3 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup F
M : Type u_5
inst_8 : Monoid M
inst_9 : DistribMulAction M F
inst_10 : SMulCommClass 𝕜 M F
inst_11 : ContinuousConstSMul M F
this : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
⊢ ContinuousConstSMul M (ContinuousMultilinearMap 𝕜 E F)
have this₁ : IsUniformAddGroup F
Tactic: haveI := isUniformAddGroup_of_addCommGroup (G := F)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Topology (hypothesis)
Goal:
𝕜 : Type u_1
ι_1 : Type u_2
E : ι_1 → Type u_3
F : Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι_1) → TopologicalSpace (E i)
inst_2 : (i : ι_1) → AddCommGroup (E i)
inst_3 : (i : ι_1) → Module.{u_1, u_3} 𝕜 (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup F
ι : Type u_5
p : ι → Prop
b : ι → Set F
h : Filter.HasBasis (𝓝 0) p b
this : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
⊢ Filter.HasBasis (α := ContinuousMultilinearMap 𝕜 E F) (𝓝 0)
    (fun (Si : Set ((i : ι_1) → E i) × ι) ↦ IsVonNBounded 𝕜 Si.1 ∧ p Si.2) fun (Si : Set ((i : ι_1) → E i) × ι) ↦
    {f : ContinuousMultilinearMap 𝕜 E F | MapsTo (⇑f : (a : (i : ι_1) → E i) → F) Si.1 (b Si.2)}
have this₁ : IsUniformAddGroup F
Tactic: haveI : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Topology (goal)
Goal:
𝕜 : Type u_1
ι_1 : Type u_2
E : ι_1 → Type u_3
F : Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι_1) → TopologicalSpace (E i)
inst_2 : (i : ι_1) → AddCommGroup (E i)
inst_3 : (i : ι_1) → Module.{u_1, u_3} 𝕜 (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup F
ι : Type u_5
p : ι → Prop
b : ι → Set F
h : Filter.HasBasis (𝓝 0) p b
this_1 : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
⊢ Filter.HasBasis (α := ContinuousMultilinearMap 𝕜 E F) (𝓝 0)
    (fun (Si : Set ((i : ι_1) → E i) × ι) ↦ IsVonNBounded 𝕜 Si.1 ∧ p Si.2) fun (Si : Set ((i : ι_1) → E i) × ι) ↦
    {f : ContinuousMultilinearMap 𝕜 E F | MapsTo (⇑f : (a : (i : ι_1) → E i) → F) Si.1 (b Si.2)}
have rw : Filter.HasBasis (α := ContinuousMultilinearMap 𝕜 E F)
  (Filter.comap (toUniformOnFun (E := E)) (𝓝 (toUniformOnFun (E := E) 0)))
  (fun (Si : Set ((i : ι_1) → E i) × ι) ↦ IsVonNBounded 𝕜 Si.1 ∧ p Si.2) fun (Si : Set ((i : ι_1) → E i) × ι) ↦
  {f : ContinuousMultilinearMap 𝕜 E F | MapsTo (⇑f : (a : (i : ι_1) → E i) → F) Si.1 (b Si.2)}
Tactic: rw [nhds_induced]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Topology (goal)
Goal:
𝕜 : Type u_1
ι_1 : Type u_2
E : ι_1 → Type u_3
F : Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι_1) → TopologicalSpace (E i)
inst_2 : (i : ι_1) → AddCommGroup (E i)
inst_3 : (i : ι_1) → Module.{u_1, u_3} 𝕜 (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup F
ι : Type u_5
p : ι → Prop
b : ι → Set F
h : Filter.HasBasis (𝓝 0) p b
this_1 : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
⊢ Filter.HasBasis (α := ContinuousMultilinearMap 𝕜 E F)
    (Filter.comap (toUniformOnFun (E := E)) (𝓝 (toUniformOnFun (E := E) 0)))
    (fun (Si : Set ((i : ι_1) → E i) × ι) ↦ IsVonNBounded 𝕜 Si.1 ∧ p Si.2) fun (Si : Set ((i : ι_1) → E i) × ι) ↦
    {f : ContinuousMultilinearMap 𝕜 E F | MapsTo (⇑f : (a : (i : ι_1) → E i) → F) Si.1 (b Si.2)}
have refine_1 : Set.Nonempty (α := Set ((i : ι_1) → E i)) {s : Set ((i : ι_1) → E i) | IsVonNBounded 𝕜 s}
Tactic: refine (UniformOnFun.hasBasis_nhds_zero_of_basis _ ?_ ?_ h).comap DFunLike.coe
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Topology (goal)
Goal:
𝕜 : Type u_1
ι_1 : Type u_2
E : ι_1 → Type u_3
F : Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι_1) → TopologicalSpace (E i)
inst_2 : (i : ι_1) → AddCommGroup (E i)
inst_3 : (i : ι_1) → Module.{u_1, u_3} 𝕜 (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup F
ι : Type u_5
p : ι → Prop
b : ι → Set F
h : Filter.HasBasis (𝓝 0) p b
this_1 : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
refine_1 : Set.Nonempty (α := Set ((i : ι_1) → E i)) {s : Set ((i : ι_1) → E i) | IsVonNBounded 𝕜 s}
⊢ Filter.HasBasis (α := ContinuousMultilinearMap 𝕜 E F)
    (Filter.comap (toUniformOnFun (E := E)) (𝓝 (toUniformOnFun (E := E) 0)))
    (fun (Si : Set ((i : ι_1) → E i) × ι) ↦ IsVonNBounded 𝕜 Si.1 ∧ p Si.2) fun (Si : Set ((i : ι_1) → E i) × ι) ↦
    {f : ContinuousMultilinearMap 𝕜 E F | MapsTo (⇑f : (a : (i : ι_1) → E i) → F) Si.1 (b Si.2)}
have refine_2 : DirectedOn (fun (x1 x2 : Set ((i : ι_1) → E i)) ↦ x1 ⊆ x2) {s : Set ((i : ι_1) → E i) | IsVonNBounded 𝕜 s}
Tactic: refine (UniformOnFun.hasBasis_nhds_zero_of_basis _ ?_ ?_ h).comap DFunLike.coe