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
G : 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 : 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
aux : (F →L[𝕜] G) →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G :=
  {
    toFun := fun (g : F →L[𝕜] G) ↦
      { toFun := g.compContinuousMultilinearMap (M₁ := E), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ },
    map_add' := ⋯, map_smul' := ⋯ }
⊢ Filter.Tendsto (α := F →L[𝕜] G) (β := ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G)
    (⇑aux : (a : F →L[𝕜] G) → ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G) (𝓝 0) (𝓝 0)
have rw : ∀ (ib : Set (ContinuousMultilinearMap 𝕜 E F) × Set ((i : ι) → E i) × Set G),
  IsVonNBounded 𝕜 ib.1 ∧ IsVonNBounded 𝕜 ib.2.1 ∧ Membership.mem (γ := Filter G) (𝓝 0) ib.2.2 →
    ∃ (ia : Prod.{u_4, u_5} (Set F) (Set G)),
      (IsVonNBounded 𝕜 ia.1 ∧ Membership.mem (γ := Filter G) (𝓝 0) ia.2) ∧
        ∀ (x : F →L[𝕜] G),
          Membership.mem (γ := Set (F →L[𝕜] G))
              {f : F →L[𝕜] G | ∀ x ∈ ia.1, Membership.mem (α := G) ia.2 ((f : (a : F) → G) x : G)} x →
            Membership.mem (α := ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G) (γ :=
              Set (ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G))
              {f : ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G |
                ∀ x ∈ ib.1,
                  Membership.mem (α := ContinuousMultilinearMap 𝕜 E G) (γ := Set (ContinuousMultilinearMap 𝕜 E G))
                    {f : ContinuousMultilinearMap 𝕜 E G | MapsTo (⇑f : (a : (i : ι) → E i) → G) ib.2.1 ib.2.2}
                    ((f : (a : ContinuousMultilinearMap 𝕜 E F) → ContinuousMultilinearMap 𝕜 E G) x :
                      ContinuousMultilinearMap 𝕜 E G)}
              ((aux : (a : F →L[𝕜] G) → ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G) x :
                ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G)
Tactic: rw [ContinuousLinearMap.hasBasis_nhds_zero.tendsto_iff <|
        ContinuousLinearMap.hasBasis_nhds_zero_of_basis <|
        ContinuousMultilinearMap.hasBasis_nhds_zero]
-- 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
G : 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 : 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
aux : (F →L[𝕜] G) →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G :=
  {
    toFun := fun (g : F →L[𝕜] G) ↦
      { toFun := g.compContinuousMultilinearMap (M₁ := E), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ },
    map_add' := ⋯, map_smul' := ⋯ }
U : Set (ContinuousMultilinearMap 𝕜 E F)
V : Set ((i : ι) → E i)
W : Set G
hU : IsVonNBounded 𝕜 (U, V, W).1
hV : IsVonNBounded 𝕜 (U, V, W).2.1
hW : Membership.mem (γ := Filter G) (𝓝 0) (U, V, W).2.2
⊢ ∃ (ia : Prod.{u_4, u_5} (Set F) (Set G)),
    (IsVonNBounded 𝕜 ia.1 ∧ Membership.mem (γ := Filter G) (𝓝 0) ia.2) ∧
      ∀ (x : F →L[𝕜] G),
        Membership.mem (γ := Set (F →L[𝕜] G))
            {f : F →L[𝕜] G | ∀ x ∈ ia.1, Membership.mem (α := G) ia.2 ((f : (a : F) → G) x : G)} x →
          Membership.mem (α := ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G) (γ :=
            Set (ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G))
            {f : ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G |
              ∀ x ∈ (U, V, W).1,
                Membership.mem (α := ContinuousMultilinearMap 𝕜 E G) (γ := Set (ContinuousMultilinearMap 𝕜 E G))
                  {f : ContinuousMultilinearMap 𝕜 E G |
                    MapsTo (⇑f : (a : (i : ι) → E i) → G) (U, V, W).2.1 (U, V, W).2.2}
                  ((f : (a : ContinuousMultilinearMap 𝕜 E F) → ContinuousMultilinearMap 𝕜 E G) x :
                    ContinuousMultilinearMap 𝕜 E G)}
            ((aux : (a : F →L[𝕜] G) → ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G) x :
              ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G)
have refine_1 : IsVonNBounded.{u_1, u_4} 𝕜 (E := F)
  (image2 (fun (f : ContinuousMultilinearMap 𝕜 E F) (v : (i : ι) → E i) ↦ (f : (a : (i : ι) → E i) → F) v) U V, W).1
Tactic: refine ⟨(.image2 (fun f v ↦ f v) U V, W), ⟨?_, hW⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Topology (goal)
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
⊢ (ContinuousMultilinearMap.compContinuousLinearMapL (E := E₁) (E₁ := E) fun (i : ι) ↦ (↑(f i).symm : E₁ i →L[𝕜] E i) :
        (a : ContinuousMultilinearMap 𝕜 E F) → ContinuousMultilinearMap 𝕜 E₁ F)
      (AddHom.toFun
        (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)
        g) =
    g
have H : ∀ (x : (i : ι) → E₁ i),
  Eq.{u_5 + 1} (α := F)
    ((((ContinuousMultilinearMap.compContinuousLinearMapL (E := E₁) (E₁ := E) fun (i : ι) ↦
                  (↑(f i).symm : E₁ i →L[𝕜] E i) :
                (a : ContinuousMultilinearMap 𝕜 E F) → ContinuousMultilinearMap 𝕜 E₁ F)
              (AddHom.toFun
                (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)
                g) :
            ContinuousMultilinearMap 𝕜 E₁ F) :
          (a : (i : ι) → E₁ i) → F)
        x :
      F)
    ((g : (a : (i : ι) → E₁ i) → F) x : F)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Topology (goal)
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
⊢ 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
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Topology (goal)
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
⊢ (((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
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Topology (goal)
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
⊢ 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
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.PerfectPairing (goal)
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
⊢ { 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 }
have h : ∀ (x_2 : N),
  Eq.{u_1 + 1} (α := R) (({ toLinearMap := (p : (a : M) → N →ₗ[R] R) (x + y), cont := sorry } : (a : N) → R) x_2 : R)
    ((HAdd.hAdd (α := StrongDual R N) { toLinearMap := (p : (a : M) → N →ₗ[R] R) x, cont := sorry : N →L[R] R }
            { toLinearMap := (p : (a : M) → N →ₗ[R] R) y, cont := sorry : N →L[R] R } :
          (a : N) → R)
        x_2 :
      R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.PerfectPairing (goal)
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
⊢ { 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 }
have h : ∀ (x_2 : N),
  Eq.{u_1 + 1} (α := R) (({ toLinearMap := (p : (a : M) → N →ₗ[R] R) (r • x), cont := sorry } : (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 := sorry : N →L[R] R } :
          (a : N) → R)
        x_2 :
      R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.PerfectSpace (goal)
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
have refine : ∀ (x : E) (hx : Membership.mem (γ := Set E) univ x), AccPt x (𝓟 univ)
Tactic: refine ⟨fun x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.PerfectSpace (goal)
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
⊢ AccPt x (𝓟 univ)
have let : ∀ (r : 𝕜) (hr₀ : 0 < ‖r‖) (hr : ‖r‖ < 1), AccPt x (𝓟 univ)
Tactic: let ⟨r, hr₀, hr⟩ := NormedField.exists_norm_lt_one 𝕜
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.PerfectSpace (goal)
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
r : 𝕜
hr₀ : 0 < ‖r‖
hr : ‖r‖ < 1
⊢ AccPt x (𝓟 univ)
have obtain : ∀ (c : E) (hc : c ≠ 0), AccPt x (𝓟 univ)
Tactic: obtain ⟨c, hc⟩ : ∃ (c : E), c ≠ 0 := exists_ne 0
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.PerfectSpace (goal)
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
r : 𝕜
hr₀ : 0 < ‖r‖
hr : ‖r‖ < 1
c : E
hc : c ≠ 0
⊢ Tendsto (fun (n : ℕ) ↦ x + r ^ n • c) atTop (𝓝 (x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 c))
have apply : Tendsto (fun (x : ℕ) ↦ r ^ x • c) atTop (𝓝 (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 c))
Tactic: apply Tendsto.add tendsto_const_nhds
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.PerfectSpace (hypothesis)
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
r : 𝕜
hr₀ : 0 < ‖r‖
hr : ‖r‖ < 1
c : E
hc : c ≠ 0
⊢ AccPt x (𝓟 univ)
have A : Tendsto (fun (n : ℕ) ↦ x + r ^ n • c) atTop (𝓝 (x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 c))
Tactic: have A : Tendsto (fun (n : ℕ) ↦ x + r ^ n • c) atTop (𝓝 (x + (0 : 𝕜) • c)) := by
    apply Tendsto.add tendsto_const_nhds
    exact (tendsto_pow_atTop_nhds_zero_of_norm_lt_one hr).smul tendsto_const_nhds
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.PerfectSpace (hypothesis)
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
r : 𝕜
hr₀ : 0 < ‖r‖
hr : ‖r‖ < 1
c : E
hc : c ≠ 0
A : Tendsto (fun (n : ℕ) ↦ x + r ^ n • c) atTop (𝓝 (x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 c))
⊢ Tendsto (fun (n : ℕ) ↦ x + r ^ n • c) atTop (𝓝[univ \ {x}] x)
have A₁ : Tendsto (fun (n : ℕ) ↦ x + r ^ n • c) atTop (𝓝 x)
Tactic: simp only [zero_smul, add_zero] at A
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.PerfectSpace (hypothesis)
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
r : 𝕜
hr₀ : 0 < ‖r‖
hr : ‖r‖ < 1
c : E
hc : c ≠ 0
A : Tendsto (fun (n : ℕ) ↦ x + r ^ n • c) atTop (𝓝 (x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 c))
⊢ AccPt x (𝓟 univ)
have B : Tendsto (fun (n : ℕ) ↦ x + r ^ n • c) atTop (𝓝[univ \ {x}] x)
Tactic: have B : Tendsto (fun (n : ℕ) ↦ x + r ^ n • c) atTop (𝓝[univ \ {x}] x) := by
    simp only [zero_smul, add_zero] at A
    simp [tendsto_nhdsWithin_iff, A, hc, norm_pos_iff.mp hr₀]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Simple (goal)
Goal:
R : Type u
M : Type v
N : Type w
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : Module R N
inst_8 : ContinuousAdd M
inst_9 : IsSimpleModule R N
l : M →ₗ[R] N
⊢ IsClosed (↑l.ker : Set M) ∨ Dense (↑l.ker : Set M)
have inl : ∀ (hl : Function.Surjective.{v + 1, w + 1} (α := M) (β := N) (⇑l : (a : M) → N)),
  IsClosed (↑l.ker : Set M) ∨ Dense (↑l.ker : Set M)
Tactic: rcases l.surjective_or_eq_zero with (hl | rfl)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Simple (goal)
Goal:
R : Type u
M : Type v
N : Type w
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : Module R N
inst_8 : ContinuousAdd M
inst_9 : IsSimpleModule R N
l : M →ₗ[R] N
inl :
  ∀ (hl : Function.Surjective.{v + 1, w + 1} (α := M) (β := N) (⇑l : (a : M) → N)),
    IsClosed (↑l.ker : Set M) ∨ Dense (↑l.ker : Set M)
⊢ IsClosed (↑l.ker : Set M) ∨ Dense (↑l.ker : Set M)
have inr : IsClosed (↑(ker.{u, u, v, w} (R₂ := R) (M₂ := N) (τ₁₂ := RingHom.id R) 0) : Set M) ∨
  Dense (↑(ker.{u, u, v, w} (R₂ := R) (M₂ := N) (τ₁₂ := RingHom.id R) 0) : Set M)
Tactic: rcases l.surjective_or_eq_zero with (hl | rfl)
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Simple (goal)
Goal:
R : Type u
M : Type v
N : Type w
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : Module R N
inst_8 : ContinuousAdd M
inst_9 : IsSimpleModule R N
⊢ IsClosed (↑(ker.{u, u, v, w} (R₂ := R) (M₂ := N) (τ₁₂ := RingHom.id R) 0) : Set M) ∨
    Dense (↑(ker.{u, u, v, w} (R₂ := R) (M₂ := N) (τ₁₂ := RingHom.id R) 0) : Set M)
have inr : IsClosed (↑⊤ : Set M) ∨ Dense (↑⊤ : Set M)
Tactic: rw [LinearMap.ker_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Simple (goal)
Goal:
R : Type u
M : Type v
N : Type w
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : Module R N
inst_8 : ContinuousAdd M
inst_9 : IsSimpleModule R N
⊢ IsClosed (↑⊤ : Set M) ∨ Dense (↑⊤ : Set M)
have inr : IsClosed (↑⊤ : Set M)
Tactic: left