awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
E₁ : ι → Type u_4
F : Type u_5
G : Type u_6
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 : (i : ι) → TopologicalSpace (E₁ i)
inst_5 : (i : ι) → AddCommGroup (E₁ i)
inst_6 : (i : ι) → Module.{u_1, u_4} 𝕜 (E₁ i)
inst_7 : AddCommGroup F
inst_8 : Module 𝕜 F
inst_9 : TopologicalSpace F
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousConstSMul 𝕜 F
inst_12 : AddCommGroup G
inst_13 : Module 𝕜 G
inst_14 : TopologicalSpace G
inst_15 : IsTopologicalAddGroup G
inst_16 : ContinuousConstSMul 𝕜 G
f : (i : ι) → ContinuousLinearEquiv.{u_1, u_1, u_3, u_4} (RingHom.id 𝕜) (E i) (E₁ i)
g : ContinuousMultilinearMap 𝕜 E F
H :
  ∀ (x : (i : ι) → E i),
    Eq.{u_5 + 1} (α := F)
      ((AddHom.toFun (M := ContinuousMultilinearMap 𝕜 E₁ F)
              (LinearMap.toAddHom
                  ((↑(ContinuousMultilinearMap.compContinuousLinearMapL (E := E) (E₁ := E₁) fun (i : ι) ↦
                          (↑(f i) : E i →L[𝕜] E₁ i)) :
                      ContinuousMultilinearMap 𝕜 E₁ F →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E F) :
                    ContinuousMultilinearMap 𝕜 E₁ F →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E F) :
                ContinuousMultilinearMap 𝕜 E₁ F →ₙ+ ContinuousMultilinearMap 𝕜 E F)
              ((ContinuousMultilinearMap.compContinuousLinearMapL (E := E₁) (E₁ := E) fun (i : ι) ↦
                    (↑(f i).symm : E₁ i →L[𝕜] E i) :
                  (a : ContinuousMultilinearMap 𝕜 E F) → ContinuousMultilinearMap 𝕜 E₁ F)
                g) :
            (a : (i : ι) → E i) → F)
          x :
        F)
      ((g : (a : (i : ι) → E i) → F) x : F)
⊢ AddHom.toFun (M := ContinuousMultilinearMap 𝕜 E₁ F)
      (LinearMap.toAddHom
          ((↑(ContinuousMultilinearMap.compContinuousLinearMapL (E := E) (E₁ := E₁) fun (i : ι) ↦
                  (↑(f i) : E i →L[𝕜] E₁ i)) :
              ContinuousMultilinearMap 𝕜 E₁ F →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E F) :
            ContinuousMultilinearMap 𝕜 E₁ F →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E F) :
        ContinuousMultilinearMap 𝕜 E₁ F →ₙ+ ContinuousMultilinearMap 𝕜 E F)
      ((ContinuousMultilinearMap.compContinuousLinearMapL (E := E₁) (E₁ := E) fun (i : ι) ↦
            (↑(f i).symm : E₁ i →L[𝕜] E i) :
          (a : ContinuousMultilinearMap 𝕜 E F) → ContinuousMultilinearMap 𝕜 E₁ F)
        g) =
    g

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
E₁ : ι → Type u_4
F : Type u_5
G : Type u_6
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 : (i : ι) → TopologicalSpace (E₁ i)
inst_5 : (i : ι) → AddCommGroup (E₁ i)
inst_6 : (i : ι) → Module.{u_1, u_4} 𝕜 (E₁ i)
inst_7 : AddCommGroup F
inst_8 : Module 𝕜 F
inst_9 : TopologicalSpace F
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousConstSMul 𝕜 F
inst_12 : AddCommGroup G
inst_13 : Module 𝕜 G
inst_14 : TopologicalSpace G
inst_15 : IsTopologicalAddGroup G
inst_16 : ContinuousConstSMul 𝕜 G
f : (i : ι) → ContinuousLinearEquiv.{u_1, u_1, u_3, u_4} (RingHom.id 𝕜) (E i) (E₁ i)
g : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
⊢ Eq.{u_5 + 1} (α := F)
    ((AddHom.toFun (M := ContinuousMultilinearMap 𝕜 E₁ F)
            (LinearMap.toAddHom
                ((↑(ContinuousMultilinearMap.compContinuousLinearMapL (E := E) (E₁ := E₁) fun (i : ι) ↦
                        (↑(f i) : E i →L[𝕜] E₁ i)) :
                    ContinuousMultilinearMap 𝕜 E₁ F →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E F) :
                  ContinuousMultilinearMap 𝕜 E₁ F →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E F) :
              ContinuousMultilinearMap 𝕜 E₁ F →ₙ+ ContinuousMultilinearMap 𝕜 E F)
            ((ContinuousMultilinearMap.compContinuousLinearMapL (E := E₁) (E₁ := E) fun (i : ι) ↦
                  (↑(f i).symm : E₁ i →L[𝕜] E i) :
                (a : ContinuousMultilinearMap 𝕜 E F) → ContinuousMultilinearMap 𝕜 E₁ F)
              g) :
          (a : (i : ι) → E i) → F)
        x :
      F)
    ((g : (a : (i : ι) → E i) → F) x : F)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
E₁ : ι → Type u_4
F : Type u_5
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 : (i : ι) → TopologicalSpace (E₁ i)
inst_5 : (i : ι) → AddCommGroup (E₁ i)
inst_6 : (i : ι) → Module.{u_1, u_4} 𝕜 (E₁ i)
inst_7 : AddCommGroup F
inst_8 : Module 𝕜 F
inst_9 : TopologicalSpace F
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousConstSMul 𝕜 F
f : (i : ι) → ContinuousLinearEquiv.{u_1, u_1, u_3, u_4} (RingHom.id 𝕜) (E i) (E₁ i)
⊢ Eq (α := ContinuousMultilinearMap 𝕜 E F ≃L[𝕜] ContinuousMultilinearMap 𝕜 E₁ F)
    (ContinuousLinearEquiv.symm (continuousMultilinearMapCongrLeft (E := E) (E₁ := E₁) F f))
    (continuousMultilinearMapCongrLeft (E := E₁) (E₁ := E) F fun (i : ι) ↦ (f i).symm)

Tactic:
rfl

Premises used: ContinuousLinearEquiv.symm, LinearEquiv.symm, ContinuousLinearEquiv.continuousMultilinearMapCongrLeft, ContinuousMultilinearMap.compContinuousLinearMap, rfl
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
E₁ : ι → Type u_4
F : Type u_5
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 : (i : ι) → TopologicalSpace (E₁ i)
inst_5 : (i : ι) → AddCommGroup (E₁ i)
inst_6 : (i : ι) → Module.{u_1, u_4} 𝕜 (E₁ i)
inst_7 : AddCommGroup F
inst_8 : Module 𝕜 F
inst_9 : TopologicalSpace F
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousConstSMul 𝕜 F
g : ContinuousMultilinearMap 𝕜 E₁ F
f : (i : ι) → ContinuousLinearEquiv.{u_1, u_1, u_3, u_4} (RingHom.id 𝕜) (E i) (E₁ i)
⊢ Eq (α := ContinuousMultilinearMap 𝕜 E F)
    ((continuousMultilinearMapCongrLeft (E := E) (E₁ := E₁) F f :
          (a : ContinuousMultilinearMap 𝕜 E₁ F) → ContinuousMultilinearMap 𝕜 E F)
        g :
      ContinuousMultilinearMap 𝕜 E F)
    (g.compContinuousLinearMap (M₁ := E) (M₁' := E₁) fun (i : ι) ↦ (↑(f i) : E i →L[𝕜] E₁ i) :
      ContinuousMultilinearMap 𝕜 E F)

Tactic:
rfl

Premises used: ContinuousMultilinearMap.compContinuousLinearMap, rfl
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
E₁ : ι → Type u_4
F : Type u_5
G : Type u_6
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 : (i : ι) → TopologicalSpace (E₁ i)
inst_5 : (i : ι) → AddCommGroup (E₁ i)
inst_6 : (i : ι) → Module.{u_1, u_4} 𝕜 (E₁ i)
inst_7 : AddCommGroup F
inst_8 : Module 𝕜 F
inst_9 : TopologicalSpace F
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousConstSMul 𝕜 F
inst_12 : AddCommGroup G
inst_13 : Module 𝕜 G
inst_14 : TopologicalSpace G
inst_15 : IsTopologicalAddGroup G
inst_16 : ContinuousConstSMul 𝕜 G
g : F ≃L[𝕜] G
x : ContinuousMultilinearMap 𝕜 E F
H :
  ∀ (x_1 : (i : ι) → E i),
    Eq.{u_5 + 1} (α := F)
      (((((ContinuousLinearMap.compContinuousMultilinearMapL 𝕜 E G F :
                      (a : G →L[𝕜] F) → ContinuousMultilinearMap 𝕜 E G →L[𝕜] ContinuousMultilinearMap 𝕜 E F)
                    (↑g.symm : G →L[𝕜] F) :
                  ContinuousMultilinearMap 𝕜 E G →L[𝕜] ContinuousMultilinearMap 𝕜 E F) :
                (a : ContinuousMultilinearMap 𝕜 E G) → ContinuousMultilinearMap 𝕜 E F)
              (AddHom.toFun
                (LinearMap.toAddHom (R := 𝕜) (S := 𝕜) (σ := RingHom.id 𝕜)
                  (↑((ContinuousLinearMap.compContinuousMultilinearMapL 𝕜 E F G :
                          (a : F →L[𝕜] G) → ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G)
                        (↑g : F →L[𝕜] G)) :
                    ContinuousMultilinearMap 𝕜 E F →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E G))
                x) :
            (a : (i : ι) → E i) → F)
          x_1 :
        F)
      ((x : (a : (i : ι) → E i) → F) x_1 : F)
⊢ (((ContinuousLinearMap.compContinuousMultilinearMapL 𝕜 E G F :
              (a : G →L[𝕜] F) → ContinuousMultilinearMap 𝕜 E G →L[𝕜] ContinuousMultilinearMap 𝕜 E F)
            (↑g.symm : G →L[𝕜] F) :
          ContinuousMultilinearMap 𝕜 E G →L[𝕜] ContinuousMultilinearMap 𝕜 E F) :
        (a : ContinuousMultilinearMap 𝕜 E G) → ContinuousMultilinearMap 𝕜 E F)
      (AddHom.toFun
        (LinearMap.toAddHom (R := 𝕜) (S := 𝕜) (σ := RingHom.id 𝕜)
          (↑((ContinuousLinearMap.compContinuousMultilinearMapL 𝕜 E F G :
                  (a : F →L[𝕜] G) → ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G)
                (↑g : F →L[𝕜] G)) :
            ContinuousMultilinearMap 𝕜 E F →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E G))
        x) =
    x

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
E₁ : ι → Type u_4
F : Type u_5
G : Type u_6
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 : (i : ι) → TopologicalSpace (E₁ i)
inst_5 : (i : ι) → AddCommGroup (E₁ i)
inst_6 : (i : ι) → Module.{u_1, u_4} 𝕜 (E₁ i)
inst_7 : AddCommGroup F
inst_8 : Module 𝕜 F
inst_9 : TopologicalSpace F
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousConstSMul 𝕜 F
inst_12 : AddCommGroup G
inst_13 : Module 𝕜 G
inst_14 : TopologicalSpace G
inst_15 : IsTopologicalAddGroup G
inst_16 : ContinuousConstSMul 𝕜 G
g : F ≃L[𝕜] G
x : ContinuousMultilinearMap 𝕜 E F
x_1 : (i : ι) → E i
⊢ Eq.{u_5 + 1} (α := F)
    (((((ContinuousLinearMap.compContinuousMultilinearMapL 𝕜 E G F :
                    (a : G →L[𝕜] F) → ContinuousMultilinearMap 𝕜 E G →L[𝕜] ContinuousMultilinearMap 𝕜 E F)
                  (↑g.symm : G →L[𝕜] F) :
                ContinuousMultilinearMap 𝕜 E G →L[𝕜] ContinuousMultilinearMap 𝕜 E F) :
              (a : ContinuousMultilinearMap 𝕜 E G) → ContinuousMultilinearMap 𝕜 E F)
            (AddHom.toFun
              (LinearMap.toAddHom (R := 𝕜) (S := 𝕜) (σ := RingHom.id 𝕜)
                (↑((ContinuousLinearMap.compContinuousMultilinearMapL 𝕜 E F G :
                        (a : F →L[𝕜] G) → ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G)
                      (↑g : F →L[𝕜] G)) :
                  ContinuousMultilinearMap 𝕜 E F →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E G))
              x) :
          (a : (i : ι) → E i) → F)
        x_1 :
      F)
    ((x : (a : (i : ι) → E i) → F) x_1 : F)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
E₁ : ι → Type u_4
F : Type u_5
G : Type u_6
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 : (i : ι) → TopologicalSpace (E₁ i)
inst_5 : (i : ι) → AddCommGroup (E₁ i)
inst_6 : (i : ι) → Module.{u_1, u_4} 𝕜 (E₁ i)
inst_7 : AddCommGroup F
inst_8 : Module 𝕜 F
inst_9 : TopologicalSpace F
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousConstSMul 𝕜 F
inst_12 : AddCommGroup G
inst_13 : Module 𝕜 G
inst_14 : TopologicalSpace G
inst_15 : IsTopologicalAddGroup G
inst_16 : ContinuousConstSMul 𝕜 G
g : F ≃L[𝕜] G
x : ContinuousMultilinearMap 𝕜 E G
H :
  ∀ (x_1 : (i : ι) → E i),
    Eq.{u_6 + 1} (α := G)
      ((AddHom.toFun (M := ContinuousMultilinearMap 𝕜 E F)
              (LinearMap.toAddHom (R := 𝕜) (S := 𝕜) (σ := RingHom.id 𝕜)
                  (↑((ContinuousLinearMap.compContinuousMultilinearMapL 𝕜 E F G :
                          (a : F →L[𝕜] G) → ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G)
                        (↑g : F →L[𝕜] G)) :
                    ContinuousMultilinearMap 𝕜 E F →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E G) :
                ContinuousMultilinearMap 𝕜 E F →ₙ+ ContinuousMultilinearMap 𝕜 E G)
              ((((ContinuousLinearMap.compContinuousMultilinearMapL 𝕜 E G F :
                          (a : G →L[𝕜] F) → ContinuousMultilinearMap 𝕜 E G →L[𝕜] ContinuousMultilinearMap 𝕜 E F)
                        (↑g.symm : G →L[𝕜] F) :
                      ContinuousMultilinearMap 𝕜 E G →L[𝕜] ContinuousMultilinearMap 𝕜 E F) :
                    (a : ContinuousMultilinearMap 𝕜 E G) → ContinuousMultilinearMap 𝕜 E F)
                  x :
                ContinuousMultilinearMap 𝕜 E F) :
            (a : (i : ι) → E i) → G)
          x_1 :
        G)
      ((x : (a : (i : ι) → E i) → G) x_1 : G)
⊢ AddHom.toFun (M := ContinuousMultilinearMap 𝕜 E F)
      (LinearMap.toAddHom (R := 𝕜) (S := 𝕜) (σ := RingHom.id 𝕜)
          (↑((ContinuousLinearMap.compContinuousMultilinearMapL 𝕜 E F G :
                  (a : F →L[𝕜] G) → ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G)
                (↑g : F →L[𝕜] G)) :
            ContinuousMultilinearMap 𝕜 E F →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E G) :
        ContinuousMultilinearMap 𝕜 E F →ₙ+ ContinuousMultilinearMap 𝕜 E G)
      ((((ContinuousLinearMap.compContinuousMultilinearMapL 𝕜 E G F :
                  (a : G →L[𝕜] F) → ContinuousMultilinearMap 𝕜 E G →L[𝕜] ContinuousMultilinearMap 𝕜 E F)
                (↑g.symm : G →L[𝕜] F) :
              ContinuousMultilinearMap 𝕜 E G →L[𝕜] ContinuousMultilinearMap 𝕜 E F) :
            (a : ContinuousMultilinearMap 𝕜 E G) → ContinuousMultilinearMap 𝕜 E F)
          x :
        ContinuousMultilinearMap 𝕜 E F) =
    x

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
E₁ : ι → Type u_4
F : Type u_5
G : Type u_6
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 : (i : ι) → TopologicalSpace (E₁ i)
inst_5 : (i : ι) → AddCommGroup (E₁ i)
inst_6 : (i : ι) → Module.{u_1, u_4} 𝕜 (E₁ i)
inst_7 : AddCommGroup F
inst_8 : Module 𝕜 F
inst_9 : TopologicalSpace F
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousConstSMul 𝕜 F
inst_12 : AddCommGroup G
inst_13 : Module 𝕜 G
inst_14 : TopologicalSpace G
inst_15 : IsTopologicalAddGroup G
inst_16 : ContinuousConstSMul 𝕜 G
g : F ≃L[𝕜] G
x : ContinuousMultilinearMap 𝕜 E G
x_1 : (i : ι) → E i
⊢ Eq.{u_6 + 1} (α := G)
    ((AddHom.toFun (M := ContinuousMultilinearMap 𝕜 E F)
            (LinearMap.toAddHom (R := 𝕜) (S := 𝕜) (σ := RingHom.id 𝕜)
                (↑((ContinuousLinearMap.compContinuousMultilinearMapL 𝕜 E F G :
                        (a : F →L[𝕜] G) → ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G)
                      (↑g : F →L[𝕜] G)) :
                  ContinuousMultilinearMap 𝕜 E F →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E G) :
              ContinuousMultilinearMap 𝕜 E F →ₙ+ ContinuousMultilinearMap 𝕜 E G)
            ((((ContinuousLinearMap.compContinuousMultilinearMapL 𝕜 E G F :
                        (a : G →L[𝕜] F) → ContinuousMultilinearMap 𝕜 E G →L[𝕜] ContinuousMultilinearMap 𝕜 E F)
                      (↑g.symm : G →L[𝕜] F) :
                    ContinuousMultilinearMap 𝕜 E G →L[𝕜] ContinuousMultilinearMap 𝕜 E F) :
                  (a : ContinuousMultilinearMap 𝕜 E G) → ContinuousMultilinearMap 𝕜 E F)
                x :
              ContinuousMultilinearMap 𝕜 E F) :
          (a : (i : ι) → E i) → G)
        x_1 :
      G)
    ((x : (a : (i : ι) → E i) → G) x_1 : G)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_5
G : Type u_6
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
inst_8 : ContinuousConstSMul 𝕜 F
inst_9 : AddCommGroup G
inst_10 : Module 𝕜 G
inst_11 : TopologicalSpace G
inst_12 : IsTopologicalAddGroup G
inst_13 : ContinuousConstSMul 𝕜 G
g : F ≃L[𝕜] G
⊢ Eq (α := ContinuousMultilinearMap 𝕜 E G ≃L[𝕜] ContinuousMultilinearMap 𝕜 E F)
    (ContinuousLinearEquiv.symm (continuousMultilinearMapCongrRight E g)) (continuousMultilinearMapCongrRight E g.symm)

Tactic:
rfl

Premises used: ContinuousLinearEquiv.symm, LinearEquiv.symm, ContinuousLinearMap.compContinuousMultilinearMap, rfl, ContinuousLinearEquiv.continuousMultilinearMapCongrRight
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_5
G : Type u_6
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
inst_8 : ContinuousConstSMul 𝕜 F
inst_9 : AddCommGroup G
inst_10 : Module 𝕜 G
inst_11 : TopologicalSpace G
inst_12 : IsTopologicalAddGroup G
inst_13 : ContinuousConstSMul 𝕜 G
g : F ≃L[𝕜] G
f : ContinuousMultilinearMap 𝕜 E F
⊢ (continuousMultilinearMapCongrRight E g : (a : ContinuousMultilinearMap 𝕜 E F) → ContinuousMultilinearMap 𝕜 E G) f =
    (↑g : F →L[𝕜] G).compContinuousMultilinearMap (M₁ := E) f

Tactic:
rfl

Premises used: ContinuousLinearMap.compContinuousMultilinearMap, rfl
-- Module: Mathlib.Topology.Algebra.Module.PerfectPairing
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : TopologicalSpace M
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
x : M
inst_8 : p.IsContPerfPair
⊢ Continuous.{u_3, u_1} (X := N) (Y := R) (⇑((p : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R)

Tactic:
p.continuous_uncurry_of_isContPerfPair.comp <| .prodMk_right x

Premises used: Continuous.comp, Continuous.prodMk_right, LinearMap.continuous_uncurry_of_isContPerfPair
-- Module: Mathlib.Topology.Algebra.Module.PerfectPairing
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : TopologicalSpace M
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
x_1 : M
y_1 : N
inst_8 : p.IsContPerfPair
inst_9 : IsTopologicalRing R
x y : M
h :
  ∀ (x_2 : N),
    Eq.{u_1 + 1} (α := R) (({ toLinearMap := (p : (a : M) → N →ₗ[R] R) (x + y), cont := ⋯ } : (a : N) → R) x_2 : R)
      ((HAdd.hAdd (α := StrongDual R N) { toLinearMap := (p : (a : M) → N →ₗ[R] R) x, cont := ⋯ : N →L[R] R }
              { toLinearMap := (p : (a : M) → N →ₗ[R] R) y, cont := ⋯ : N →L[R] R } :
            (a : N) → R)
          x_2 :
        R)
⊢ { toLinearMap := (p : (a : M) → N →ₗ[R] R) (x + y), cont := ⋯ } =
    HAdd.hAdd (α := StrongDual R N) { toLinearMap := (p : (a : M) → N →ₗ[R] R) x, cont := ⋯ : N →L[R] R }
      { toLinearMap := (p : (a : M) → N →ₗ[R] R) y, cont := ⋯ : N →L[R] R }

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.PerfectPairing
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : TopologicalSpace M
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
x_1 : M
y_1 : N
inst_8 : p.IsContPerfPair
inst_9 : IsTopologicalRing R
x y : M
x_2 : N
⊢ Eq.{u_1 + 1} (α := R) (({ toLinearMap := (p : (a : M) → N →ₗ[R] R) (x + y), cont := ⋯ } : (a : N) → R) x_2 : R)
    ((HAdd.hAdd (α := StrongDual R N) { toLinearMap := (p : (a : M) → N →ₗ[R] R) x, cont := ⋯ : N →L[R] R }
            { toLinearMap := (p : (a : M) → N →ₗ[R] R) y, cont := ⋯ : N →L[R] R } :
          (a : N) → R)
        x_2 :
      R)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.PerfectPairing
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : TopologicalSpace M
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
x_1 : M
y : N
inst_8 : p.IsContPerfPair
inst_9 : IsTopologicalRing R
r : R
x : M
h :
  ∀ (x_2 : N),
    Eq.{u_1 + 1} (α := R) (({ toLinearMap := (p : (a : M) → N →ₗ[R] R) (r • x), cont := ⋯ } : (a : N) → R) x_2 : R)
      ((HSMul.hSMul (α := R) (β := StrongDual R N) ((RingHom.id R : (a : R) → R) r : R)
              { toLinearMap := (p : (a : M) → N →ₗ[R] R) x, cont := ⋯ : N →L[R] R } :
            (a : N) → R)
          x_2 :
        R)
⊢ { toLinearMap := (p : (a : M) → N →ₗ[R] R) (r • x), cont := ⋯ } =
    HSMul.hSMul (α := R) (β := StrongDual R N) ((RingHom.id R : (a : R) → R) r : R)
      { toLinearMap := (p : (a : M) → N →ₗ[R] R) x, cont := ⋯ : N →L[R] R }

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.PerfectPairing
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : TopologicalSpace M
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
x_1 : M
y : N
inst_8 : p.IsContPerfPair
inst_9 : IsTopologicalRing R
r : R
x : M
x_2 : N
⊢ Eq.{u_1 + 1} (α := R) (({ toLinearMap := (p : (a : M) → N →ₗ[R] R) (r • x), cont := ⋯ } : (a : N) → R) x_2 : R)
    ((HSMul.hSMul (α := R) (β := StrongDual R N) ((RingHom.id R : (a : R) → R) r : R)
            { toLinearMap := (p : (a : M) → N →ₗ[R] R) x, cont := ⋯ : N →L[R] R } :
          (a : N) → R)
        x_2 :
      R)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.PerfectPairing
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : TopologicalSpace M
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
inst_8 : p.IsContPerfPair
inst_9 : IsTopologicalRing R
x : M
⊢ Eq (α := N →ₗ[R] R) (↑(((p.toContPerfPair : M ≃ₗ[R] StrongDual R N) : (a : M) → StrongDual R N) x) : N →ₗ[R] R)
    ((p : (a : M) → N →ₗ[R] R) x)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.PerfectPairing
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : TopologicalSpace M
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
inst_8 : p.IsContPerfPair
inst_9 : IsTopologicalRing R
x : M
y : N
⊢ Eq.{u_1 + 1} (α := R)
    (((((p.toContPerfPair : M ≃ₗ[R] StrongDual R N) : (a : M) → StrongDual R N) x : StrongDual R N) : (a : N) → R) y :
      R)
    ((((p : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) y : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.PerfectSpace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Nontrivial E
inst_4 : TopologicalSpace E
inst_5 : ContinuousAdd E
inst_6 : ContinuousSMul 𝕜 E
⊢ PerfectSpace E

Tactic:
⟨fun x hx ↦ ?_⟩

Premises used: PerfectSpace.mk
-- Module: Mathlib.Topology.Algebra.Module.PerfectSpace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Nontrivial E
inst_4 : TopologicalSpace E
inst_5 : ContinuousAdd E
inst_6 : ContinuousSMul 𝕜 E
refine : ∀ (x : E) (hx : Membership.mem (γ := Set E) univ x), AccPt x (𝓟 univ)
⊢ PerfectSpace E

Tactic:
refine ⟨fun x hx ↦ ?_⟩
-- Module: Mathlib.Topology.Algebra.Module.PerfectSpace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Nontrivial E
inst_4 : TopologicalSpace E
inst_5 : ContinuousAdd E
inst_6 : ContinuousSMul 𝕜 E
x : E
hx : Membership.mem (γ := Set E) univ x
let : ∀ (r : 𝕜) (hr₀ : 0 < ‖r‖) (hr : ‖r‖ < 1), AccPt x (𝓟 univ)
⊢ AccPt x (𝓟 univ)

Tactic:
let ⟨r, hr₀, hr⟩ := NormedField.exists_norm_lt_one 𝕜