awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜 : Type u_6
inst : NormedField 𝕜
E : Type u_7
ι : Type u_8
F : ι → Type u_9
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : (i : ι) → AddCommGroup (F i)
inst_5 : (i : ι) → Module.{u_6, u_9} 𝕜 (F i)
inst_6 : (i : ι) → TopologicalSpace (F i)
inst_7 : ∀ (i : ι), IsTopologicalAddGroup.{u_9} (F i)
inst_8 : ∀ (i : ι), ContinuousConstSMul.{u_6, u_9} 𝕜 (F i)
𝔖 : Set (Set E)
T : (i : ι) → UniformConvergenceCLM.{u_6, u_6, u_7, u_9} (RingHom.id 𝕜) (F i) 𝔖
e : E
i : ι
⊢ Eq.{u_9 + 1} (α := F i)
    ((((piEquivL 𝕜 F 𝔖 :
                (a : (i : ι) → UniformConvergenceCLM (RingHom.id 𝕜) (F i) 𝔖) →
                  UniformConvergenceCLM (RingHom.id 𝕜) ((i : ι) → F i) 𝔖)
              T :
            UniformConvergenceCLM (RingHom.id 𝕜) ((i : ι) → F i) 𝔖) :
          (a : E) → (i : ι) → F i)
        e i :
      F i)
    ((T i : (a : E) → F i) e : F i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜 : Type u_6
inst : NormedField 𝕜
E : Type u_7
ι : Type u_8
F : ι → Type u_9
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : (i : ι) → AddCommGroup (F i)
inst_5 : (i : ι) → Module.{u_6, u_9} 𝕜 (F i)
inst_6 : (i : ι) → TopologicalSpace (F i)
inst_7 : ∀ (i : ι), IsTopologicalAddGroup.{u_9} (F i)
inst_8 : ∀ (i : ι), ContinuousConstSMul.{u_6, u_9} 𝕜 (F i)
𝔖 : Set (Set E)
T : UniformConvergenceCLM (RingHom.id 𝕜) ((i : ι) → F i) 𝔖
e : E
i : ι
⊢ Eq.{u_9 + 1} (α := F i)
    ((((ContinuousLinearEquiv.symm (piEquivL 𝕜 F 𝔖) :
                (a : UniformConvergenceCLM (RingHom.id 𝕜) ((i : ι) → F i) 𝔖) →
                  (i : ι) → UniformConvergenceCLM (RingHom.id 𝕜) (F i) 𝔖)
              T i :
            UniformConvergenceCLM.{u_6, u_6, u_7, u_9} (RingHom.id 𝕜) (F i) 𝔖) :
          (a : E) → F i)
        e :
      F i)
    ((T : (a : E) → (i : ι) → F i) e i : F i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₁ : Type u_1
𝕜₂_1 : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂_1
σ : 𝕜₁ →+* 𝕜₂_1
E_1 : Type u_3
F_1 : Type u_4
G_1 : Type u_5
inst_2 : AddCommGroup E_1
inst_3 : Module 𝕜₁ E_1
inst_4 : TopologicalSpace E_1
inst_5 : AddCommGroup F_1
inst_6 : Module 𝕜₂_1 F_1
𝕜 : Type u_6
𝕜₂ : Type u_7
𝕜₃ : Type u_8
𝕜₄ : Type u_9
E : Type u_10
F : Type u_11
G : Type u_12
H : Type u_13
inst_7 : AddCommGroup E
inst_8 : AddCommGroup F
inst_9 : AddCommGroup G
inst_10 : AddCommGroup H
inst_11 : NormedField 𝕜
inst_12 : NormedField 𝕜₂
inst_13 : NormedField 𝕜₃
inst_14 : NormedField 𝕜₄
inst_15 : Module 𝕜 E
inst_16 : Module 𝕜₂ F
inst_17 : Module 𝕜₃ G
inst_18 : Module 𝕜₄ H
inst_19 : TopologicalSpace E
inst_20 : TopologicalSpace F
inst_21 : TopologicalSpace G
inst_22 : TopologicalSpace H
inst_23 : IsTopologicalAddGroup G
inst_24 : IsTopologicalAddGroup H
inst_25 : ContinuousConstSMul 𝕜₃ G
inst_26 : ContinuousConstSMul 𝕜₄ H
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
σ₃₄ : 𝕜₃ →+* 𝕜₄
σ₄₃ : 𝕜₄ →+* 𝕜₃
σ₂₄ : 𝕜₂ →+* 𝕜₄
σ₁₄ : 𝕜 →+* 𝕜₄
inst_27 : RingHomInvPair σ₁₂ σ₂₁
inst_28 : RingHomInvPair σ₂₁ σ₁₂
inst_29 : RingHomInvPair σ₃₄ σ₄₃
inst_30 : RingHomInvPair σ₄₃ σ₃₄
inst_31 : RingHomCompTriple σ₂₁ σ₁₄ σ₂₄
inst_32 : RingHomCompTriple σ₂₄ σ₄₃ σ₂₃
inst_33 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_34 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst_35 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst_36 : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
e₁₂ : E ≃SL[σ₁₂] F
e₄₃ : H ≃SL[σ₄₃] G
𝔖 : Set (Set E)
𝔗 : Set (Set F)
h : ∀ (t : Set F), t ∈ 𝔗 ↔ (⇑e₁₂ : (a : E) → F) ⁻¹' t ∈ 𝔖
s : Set E
⊢ s ∈ 𝔖 → (fun (x : Set E) ↦ ((⇑e₁₂ : (a : E) → F) '' x : Set F)) s ∈ 𝔗

Tactic:
simp [h, preimage_image_eq _ e₁₂.injective]

Premises used: ContinuousLinearEquiv.injective, Set.preimage_image_eq
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₁ : Type u_1
𝕜₂_1 : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂_1
σ : 𝕜₁ →+* 𝕜₂_1
E_1 : Type u_3
F_1 : Type u_4
G_1 : Type u_5
inst_2 : AddCommGroup E_1
inst_3 : Module 𝕜₁ E_1
inst_4 : TopologicalSpace E_1
inst_5 : AddCommGroup F_1
inst_6 : Module 𝕜₂_1 F_1
𝕜 : Type u_6
𝕜₂ : Type u_7
𝕜₃ : Type u_8
𝕜₄ : Type u_9
E : Type u_10
F : Type u_11
G : Type u_12
H : Type u_13
inst_7 : AddCommGroup E
inst_8 : AddCommGroup F
inst_9 : AddCommGroup G
inst_10 : AddCommGroup H
inst_11 : NormedField 𝕜
inst_12 : NormedField 𝕜₂
inst_13 : NormedField 𝕜₃
inst_14 : NormedField 𝕜₄
inst_15 : Module 𝕜 E
inst_16 : Module 𝕜₂ F
inst_17 : Module 𝕜₃ G
inst_18 : Module 𝕜₄ H
inst_19 : TopologicalSpace E
inst_20 : TopologicalSpace F
inst_21 : TopologicalSpace G
inst_22 : TopologicalSpace H
inst_23 : IsTopologicalAddGroup G
inst_24 : IsTopologicalAddGroup H
inst_25 : ContinuousConstSMul 𝕜₃ G
inst_26 : ContinuousConstSMul 𝕜₄ H
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
σ₃₄ : 𝕜₃ →+* 𝕜₄
σ₄₃ : 𝕜₄ →+* 𝕜₃
σ₂₄ : 𝕜₂ →+* 𝕜₄
σ₁₄ : 𝕜 →+* 𝕜₄
inst_27 : RingHomInvPair σ₁₂ σ₂₁
inst_28 : RingHomInvPair σ₂₁ σ₁₂
inst_29 : RingHomInvPair σ₃₄ σ₄₃
inst_30 : RingHomInvPair σ₄₃ σ₃₄
inst_31 : RingHomCompTriple σ₂₁ σ₁₄ σ₂₄
inst_32 : RingHomCompTriple σ₂₄ σ₄₃ σ₂₃
inst_33 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_34 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst_35 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst_36 : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
e₁₂ : E ≃SL[σ₁₂] F
e₄₃ : H ≃SL[σ₄₃] G
𝔖 : Set (Set E)
𝔗 : Set (Set F)
h : ∀ (t : Set F), t ∈ 𝔗 ↔ (⇑e₁₂ : (a : E) → F) ⁻¹' t ∈ 𝔖
mapsto₁ : MapsTo (fun (x : Set E) ↦ (⇑e₁₂ : (a : E) → F) '' x) 𝔖 𝔗
t : Set F
⊢ t ∈ 𝔗 → (fun (x : Set F) ↦ ((⇑e₁₂.symm : (a : F) → E) '' x : Set E)) t ∈ 𝔖

Tactic:
simp [h, e₁₂.image_symm_eq_preimage]

Premises used: ContinuousLinearEquiv.image_symm_eq_preimage
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜 : Type u_6
𝕜₂ : Type u_7
𝕜₃ : Type u_8
𝕜₄ : Type u_9
E : Type u_10
F : Type u_11
G : Type u_12
H : Type u_13
inst : AddCommGroup E
inst_1 : AddCommGroup F
inst_2 : AddCommGroup G
inst_3 : AddCommGroup H
inst_4 : NormedField 𝕜
inst_5 : NormedField 𝕜₂
inst_6 : NormedField 𝕜₃
inst_7 : NormedField 𝕜₄
inst_8 : Module 𝕜 E
inst_9 : Module 𝕜₂ F
inst_10 : Module 𝕜₃ G
inst_11 : Module 𝕜₄ H
inst_12 : TopologicalSpace E
inst_13 : TopologicalSpace F
inst_14 : TopologicalSpace G
inst_15 : TopologicalSpace H
inst_16 : IsTopologicalAddGroup G
inst_17 : IsTopologicalAddGroup H
inst_18 : ContinuousConstSMul 𝕜₃ G
inst_19 : ContinuousConstSMul 𝕜₄ H
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
σ₃₄ : 𝕜₃ →+* 𝕜₄
σ₄₃ : 𝕜₄ →+* 𝕜₃
σ₂₄ : 𝕜₂ →+* 𝕜₄
σ₁₄ : 𝕜 →+* 𝕜₄
inst_20 : RingHomInvPair σ₁₂ σ₂₁
inst_21 : RingHomInvPair σ₂₁ σ₁₂
inst_22 : RingHomInvPair σ₃₄ σ₄₃
inst_23 : RingHomInvPair σ₄₃ σ₃₄
inst_24 : RingHomCompTriple σ₂₁ σ₁₄ σ₂₄
inst_25 : RingHomCompTriple σ₂₄ σ₄₃ σ₂₃
inst_26 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_27 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst_28 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst_29 : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
e₁₂ : E ≃SL[σ₁₂] F
e₄₃ : H ≃SL[σ₄₃] G
𝔖 : Set (Set E)
𝔗 : Set (Set F)
h : ∀ (t : Set F), t ∈ 𝔗 ↔ (⇑e₁₂ : (a : E) → F) ⁻¹' t ∈ 𝔖
φ : UniformConvergenceCLM σ₁₄ H 𝔖
f : F
⊢ Eq.{u_12 + 1} (α := G)
    ((((e₁₂.uniformConvergenceCLMCongrSL e₄₃ 𝔖 𝔗 h :
                (a : UniformConvergenceCLM σ₁₄ H 𝔖) → UniformConvergenceCLM σ₂₃ G 𝔗)
              φ :
            UniformConvergenceCLM σ₂₃ G 𝔗) :
          (a : F) → G)
        f :
      G)
    ((e₄₃ : (a : H) → G) ((φ : (a : E) → H) ((e₁₂.symm : (a : F) → E) f : E) : H) : G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜 : Type u_6
𝕜₂ : Type u_7
𝕜₃ : Type u_8
𝕜₄ : Type u_9
E : Type u_10
F : Type u_11
G : Type u_12
H : Type u_13
inst : AddCommGroup E
inst_1 : AddCommGroup F
inst_2 : AddCommGroup G
inst_3 : AddCommGroup H
inst_4 : NormedField 𝕜
inst_5 : NormedField 𝕜₂
inst_6 : NormedField 𝕜₃
inst_7 : NormedField 𝕜₄
inst_8 : Module 𝕜 E
inst_9 : Module 𝕜₂ F
inst_10 : Module 𝕜₃ G
inst_11 : Module 𝕜₄ H
inst_12 : TopologicalSpace E
inst_13 : TopologicalSpace F
inst_14 : TopologicalSpace G
inst_15 : TopologicalSpace H
inst_16 : IsTopologicalAddGroup G
inst_17 : IsTopologicalAddGroup H
inst_18 : ContinuousConstSMul 𝕜₃ G
inst_19 : ContinuousConstSMul 𝕜₄ H
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
σ₃₄ : 𝕜₃ →+* 𝕜₄
σ₄₃ : 𝕜₄ →+* 𝕜₃
σ₂₄ : 𝕜₂ →+* 𝕜₄
σ₁₄ : 𝕜 →+* 𝕜₄
inst_20 : RingHomInvPair σ₁₂ σ₂₁
inst_21 : RingHomInvPair σ₂₁ σ₁₂
inst_22 : RingHomInvPair σ₃₄ σ₄₃
inst_23 : RingHomInvPair σ₄₃ σ₃₄
inst_24 : RingHomCompTriple σ₂₁ σ₁₄ σ₂₄
inst_25 : RingHomCompTriple σ₂₄ σ₄₃ σ₂₃
inst_26 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_27 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst_28 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst_29 : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
e₁₂ : E ≃SL[σ₁₂] F
e₄₃ : H ≃SL[σ₄₃] G
𝔖 : Set (Set E)
𝔗 : Set (Set F)
h : ∀ (t : Set F), t ∈ 𝔗 ↔ (⇑e₁₂ : (a : E) → F) ⁻¹' t ∈ 𝔖
φ : UniformConvergenceCLM σ₂₃ G 𝔗
e : E
⊢ Eq.{u_13 + 1} (α := H)
    ((((ContinuousLinearEquiv.symm (e₁₂.uniformConvergenceCLMCongrSL e₄₃ 𝔖 𝔗 h) :
                (a : UniformConvergenceCLM σ₂₃ G 𝔗) → UniformConvergenceCLM σ₁₄ H 𝔖)
              φ :
            UniformConvergenceCLM σ₁₄ H 𝔖) :
          (a : E) → H)
        e :
      H)
    ((e₄₃.symm : (a : G) → H) ((φ : (a : F) → G) ((e₁₂ : (a : E) → F) e : F) : G) : H)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜 : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
H : Type u_10
inst : AddCommGroup E
inst_1 : AddCommGroup F
inst_2 : AddCommGroup G
inst_3 : AddCommGroup H
inst_4 : NormedField 𝕜
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜 F
inst_7 : Module 𝕜 G
inst_8 : Module 𝕜 H
inst_9 : TopologicalSpace E
inst_10 : TopologicalSpace F
inst_11 : TopologicalSpace G
inst_12 : TopologicalSpace H
inst_13 : IsTopologicalAddGroup G
inst_14 : IsTopologicalAddGroup H
inst_15 : ContinuousConstSMul 𝕜 G
inst_16 : ContinuousConstSMul 𝕜 H
e₁ : E ≃L[𝕜] F
e₂ : H ≃L[𝕜] G
𝔖 : Set (Set E)
𝔗 : Set (Set F)
h : ∀ (t : Set F), t ∈ 𝔗 ↔ (⇑e₁ : (a : E) → F) ⁻¹' t ∈ 𝔖
φ : UniformConvergenceCLM (RingHom.id 𝕜) H 𝔖
f : F
⊢ Eq.{u_9 + 1} (α := G)
    ((((e₁.uniformConvergenceCLMCongr e₂ 𝔖 𝔗 h :
                (a : UniformConvergenceCLM (RingHom.id 𝕜) H 𝔖) → UniformConvergenceCLM (RingHom.id 𝕜) G 𝔗)
              φ :
            UniformConvergenceCLM (RingHom.id 𝕜) G 𝔗) :
          (a : F) → G)
        f :
      G)
    ((e₂ : (a : H) → G) ((φ : (a : E) → H) ((e₁.symm : (a : F) → E) f : E) : H) : G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜 : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
H : Type u_10
inst : AddCommGroup E
inst_1 : AddCommGroup F
inst_2 : AddCommGroup G
inst_3 : AddCommGroup H
inst_4 : NormedField 𝕜
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜 F
inst_7 : Module 𝕜 G
inst_8 : Module 𝕜 H
inst_9 : TopologicalSpace E
inst_10 : TopologicalSpace F
inst_11 : TopologicalSpace G
inst_12 : TopologicalSpace H
inst_13 : IsTopologicalAddGroup G
inst_14 : IsTopologicalAddGroup H
inst_15 : ContinuousConstSMul 𝕜 G
inst_16 : ContinuousConstSMul 𝕜 H
e₁ : E ≃L[𝕜] F
e₂ : H ≃L[𝕜] G
𝔖 : Set (Set E)
𝔗 : Set (Set F)
h : ∀ (t : Set F), t ∈ 𝔗 ↔ (⇑e₁ : (a : E) → F) ⁻¹' t ∈ 𝔖
φ : UniformConvergenceCLM (RingHom.id 𝕜) G 𝔗
e : E
⊢ Eq.{u_10 + 1} (α := H)
    ((((ContinuousLinearEquiv.symm (e₁.uniformConvergenceCLMCongr e₂ 𝔖 𝔗 h) :
                (a : UniformConvergenceCLM (RingHom.id 𝕜) G 𝔗) → UniformConvergenceCLM (RingHom.id 𝕜) H 𝔖)
              φ :
            UniformConvergenceCLM (RingHom.id 𝕜) H 𝔖) :
          (a : E) → H)
        e :
      H)
    ((e₂.symm : (a : G) → H) ((φ : (a : F) → G) ((e₁ : (a : E) → F) e : F) : G) : H)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
Goal:
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst : CommSemiring 𝕜
inst_1 : CommSemiring 𝕝
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : AddCommMonoid F
inst_5 : Module 𝕜 F
inst_6 : SMul 𝕝 𝕜
inst_7 : Module 𝕝 E
s : IsScalarTower 𝕝 𝕜 E
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
⊢ IsScalarTower.{u_3, u_2, u_4} 𝕝 𝕜 (WeakBilin B)

Tactic:
s

Premises used: instModuleWeakBilin._aux_1, WeakBilin
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
Goal:
𝕜 : Type u_2
E : Type u_4
F : Type u_5
inst : TopologicalSpace 𝕜
inst_1 : CommSemiring 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : AddCommMonoid F
inst_5 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
⊢ Continuous[instTopologicalSpace B, Pi.topologicalSpace] fun (x : WeakBilin B) (y : F) ↦
    (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y

Tactic:
continuous_induced_dom

Premises used: continuous_induced_dom
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
Goal:
𝕜 : Type u_2
E : Type u_4
F : Type u_5
inst : TopologicalSpace 𝕜
inst_1 : CommSemiring 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : AddCommMonoid F
inst_5 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
y : F
⊢ Continuous[instTopologicalSpace B, inst] fun (x : WeakBilin B) ↦
    (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y

Tactic:
(continuous_pi_iff.mp (coeFn_continuous B)) y

Premises used: continuous_pi_iff, WeakBilin.coeFn_continuous, Iff.mp
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
Goal:
α : Type u_1
𝕜 : Type u_2
E : Type u_4
F : Type u_5
inst : TopologicalSpace 𝕜
inst_1 : CommSemiring 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : AddCommMonoid F
inst_5 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst_6 : TopologicalSpace α
g : α → WeakBilin B
h : ∀ (y : F), Continuous[inst_6, inst] fun (a : α) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) (g a) : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y
⊢ Continuous[inst_6, instTopologicalSpace B] g

Tactic:
continuous_induced_rng.2 (continuous_pi_iff.mpr h)

Premises used: Iff.mpr, continuous_pi_iff, continuous_induced_rng
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
Goal:
𝕜 : Type u_2
E : Type u_4
F : Type u_5
inst : TopologicalSpace 𝕜
inst_1 : CommSemiring 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : AddCommMonoid F
inst_5 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
hB : Function.Injective (α := E) (β := F →ₗ[𝕜] 𝕜) (⇑B : (a : E) → F →ₗ[𝕜] 𝕜)
⊢ IsEmbedding (Y := (y : F) → 𝕜) fun (x : WeakBilin B) (y : F) ↦
    (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y

Tactic:
Function.Injective.isEmbedding_induced <| LinearMap.coe_injective.comp hB

Premises used: Function.Injective.comp, Function.Injective.isEmbedding_induced, LinearMap.coe_injective
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
Goal:
α : Type u_1
𝕜 : Type u_2
E : Type u_4
F : Type u_5
inst : TopologicalSpace 𝕜
inst_1 : CommSemiring 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : AddCommMonoid F
inst_5 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
l : Filter α
f : α → WeakBilin B
x : WeakBilin B
hB : Function.Injective (α := E) (β := F →ₗ[𝕜] 𝕜) (⇑B : (a : E) → F →ₗ[𝕜] 𝕜)
rw :
  Tendsto (β := (y : F) → 𝕜)
      ((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘ f) l
      (𝓝 fun (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ↔
    Tendsto (β := (i : F) → 𝕜) (fun (i : α) ↦ (⇑((B : (a : E) → F →ₗ[𝕜] 𝕜) (f i) : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜)) l
      (𝓝 (⇑((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜))
⊢ Tendsto f l (𝓝 x) ↔
    ∀ (y : F),
      Tendsto.{u_1, u_2} (β := 𝕜) (fun (i : α) ↦ ((((B : (a : E) → F →ₗ[𝕜] 𝕜) (f i) : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜))
        l (𝓝 ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) : Filter 𝕜)

Tactic:
rw [← tendsto_pi_nhds, (isEmbedding hB).tendsto_nhds_iff]

Premises used: WeakBilin.isEmbedding, tendsto_pi_nhds, Topology.IsEmbedding.tendsto_nhds_iff
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
Goal:
α : Type u_1
𝕜 : Type u_2
E : Type u_4
F : Type u_5
inst : TopologicalSpace 𝕜
inst_1 : CommSemiring 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : AddCommMonoid F
inst_5 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
l : Filter α
f : α → WeakBilin B
x : WeakBilin B
hB : Function.Injective (α := E) (β := F →ₗ[𝕜] 𝕜) (⇑B : (a : E) → F →ₗ[𝕜] 𝕜)
⊢ Tendsto (β := (y : F) → 𝕜)
      ((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘ f) l
      (𝓝 fun (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ↔
    Tendsto (β := (i : F) → 𝕜) (fun (i : α) ↦ (⇑((B : (a : E) → F →ₗ[𝕜] 𝕜) (f i) : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜)) l
      (𝓝 (⇑((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜))

Tactic:
rfl
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
Goal:
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst : TopologicalSpace 𝕜
inst_1 : CommSemiring 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : AddCommMonoid F
inst_5 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst_6 : ContinuousAdd 𝕜
⊢ ContinuousAdd.{u_4} (WeakBilin B)

Tactic:
⟨continuous_induced_rng.2 ?_⟩

Premises used: Iff.mpr, ContinuousAdd.mk, continuous_induced_rng
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
Goal:
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst : TopologicalSpace 𝕜
inst_1 : CommSemiring 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : AddCommMonoid F
inst_5 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst_6 : ContinuousAdd 𝕜
refine :
  Continuous[instTopologicalSpaceProd, Pi.topologicalSpace]
    ((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘
      fun (p : WeakBilin B × WeakBilin B) ↦ p.1 + p.2)
⊢ ContinuousAdd.{u_4} (WeakBilin B)

Tactic:
refine ⟨continuous_induced_rng.2 ?_⟩
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
Goal:
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst : TopologicalSpace 𝕜
inst_1 : CommSemiring 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : AddCommMonoid F
inst_5 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst_6 : ContinuousAdd 𝕜
⊢ Continuous[instTopologicalSpaceProd, Pi.topologicalSpace]
    ((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘
      fun (p : WeakBilin B × WeakBilin B) ↦ p.1 + p.2)

Tactic:
cast (congr_arg _ ?_)
      (((coeFn_continuous B).comp continuous_fst).add ((coeFn_continuous B).comp continuous_snd))

Premises used: Continuous.comp, cast, continuous_snd, continuous_fst, congr_arg, WeakBilin.coeFn_continuous, Continuous.add
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
Goal:
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst : TopologicalSpace 𝕜
inst_1 : CommSemiring 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : AddCommMonoid F
inst_5 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst_6 : ContinuousAdd 𝕜
cast :
  HAdd.hAdd (α := WeakBilin B × WeakBilin B → (y : F) → 𝕜)
      ((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘ Prod.fst)
      ((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘ Prod.snd) =
    (fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘
      fun (p : WeakBilin B × WeakBilin B) ↦ p.1 + p.2
⊢ Continuous[instTopologicalSpaceProd, Pi.topologicalSpace]
    ((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘
      fun (p : WeakBilin B × WeakBilin B) ↦ p.1 + p.2)

Tactic:
refine
    cast (congr_arg _ ?_)
      (((coeFn_continuous B).comp continuous_fst).add ((coeFn_continuous B).comp continuous_snd))

Premises used: Continuous.comp, cast, continuous_snd, continuous_fst, congr_arg, WeakBilin.coeFn_continuous, Continuous.add
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
Goal:
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst : TopologicalSpace 𝕜
inst_1 : CommSemiring 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : AddCommMonoid F
inst_5 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst_6 : ContinuousAdd 𝕜
h :
  ∀ (x : WeakBilin B × WeakBilin B) (x_1 : F),
    HAdd.hAdd (α := WeakBilin B × WeakBilin B → (y : F) → 𝕜) (β := WeakBilin B × WeakBilin B → (y : F) → 𝕜)
        ((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘ Prod.fst)
        ((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘ Prod.snd) x
        x_1 =
      ((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘
          fun (p : WeakBilin B × WeakBilin B) ↦ p.1 + p.2)
        x x_1
⊢ HAdd.hAdd (α := WeakBilin B × WeakBilin B → (y : F) → 𝕜)
      ((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘ Prod.fst)
      ((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘ Prod.snd) =
    (fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘
      fun (p : WeakBilin B × WeakBilin B) ↦ p.1 + p.2

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
Goal:
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst : TopologicalSpace 𝕜
inst_1 : CommSemiring 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : AddCommMonoid F
inst_5 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst_6 : ContinuousAdd 𝕜
x : WeakBilin B × WeakBilin B
x_1 : F
⊢ HAdd.hAdd (α := WeakBilin B × WeakBilin B → (y : F) → 𝕜) (β := WeakBilin B × WeakBilin B → (y : F) → 𝕜)
      ((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘ Prod.fst)
      ((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘ Prod.snd) x x_1 =
    ((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘
        fun (p : WeakBilin B × WeakBilin B) ↦ p.1 + p.2)
      x x_1

Tactic:
simp only [Function.comp_apply, Pi.add_apply, map_add, LinearMap.add_apply]

Premises used: LinearMap.add_apply, map_add, Pi.add_apply, Function.comp_apply
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
Goal:
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst : TopologicalSpace 𝕜
inst_1 : CommSemiring 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : AddCommMonoid F
inst_5 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst_6 : ContinuousSMul 𝕜 𝕜
⊢ ContinuousSMul.{u_2, u_4} 𝕜 (WeakBilin B)

Tactic:
⟨continuous_induced_rng.2 ?_⟩

Premises used: Iff.mpr, ContinuousSMul.mk, continuous_induced_rng
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
Goal:
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst : TopologicalSpace 𝕜
inst_1 : CommSemiring 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : AddCommMonoid F
inst_5 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst_6 : ContinuousSMul 𝕜 𝕜
refine :
  Continuous[instTopologicalSpaceProd, Pi.topologicalSpace]
    ((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘
      fun (p : Prod.{u_2, u_4} 𝕜 (WeakBilin B)) ↦ p.1 • p.2)
⊢ ContinuousSMul.{u_2, u_4} 𝕜 (WeakBilin B)

Tactic:
refine ⟨continuous_induced_rng.2 ?_⟩
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
Goal:
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst : TopologicalSpace 𝕜
inst_1 : CommSemiring 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : AddCommMonoid F
inst_5 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst_6 : ContinuousSMul 𝕜 𝕜
⊢ Continuous[instTopologicalSpaceProd, Pi.topologicalSpace]
    ((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘
      fun (p : Prod.{u_2, u_4} 𝕜 (WeakBilin B)) ↦ p.1 • p.2)

Tactic:
cast (congr_arg _ ?_) (continuous_fst.smul ((coeFn_continuous B).comp continuous_snd))

Premises used: Continuous.comp, cast, continuous_snd, continuous_fst, congr_arg, Continuous.smul, WeakBilin.coeFn_continuous