awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Topology
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜 F
inst_7 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousConstSMul 𝕜 F
inst_10 : AddCommGroup G
inst_11 : Module 𝕜 G
inst_12 : TopologicalSpace G
inst_13 : IsTopologicalAddGroup G
inst_14 : ContinuousConstSMul 𝕜 G
x x_1 : F →L[𝕜] G
h :
  ∀ (x_2 : E [⋀^ι]→L[𝕜] F) (x_3 : ι → E),
    Eq.{u_4 + 1} (α := G)
      ((((let __LinearMap : E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G :=
                    (compContinuousAlternatingMapₗ 𝕜 E F G : (a : F →L[𝕜] G) → E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G)
                      (x + x_1);
                  { toLinearMap := __LinearMap, cont := ⋯ } :
                  (a : E [⋀^ι]→L[𝕜] F) → E [⋀^ι]→L[𝕜] G)
                x_2 :
              E [⋀^ι]→L[𝕜] G) :
            (a : ι → E) → G)
          x_3 :
        G)
      ((((HAdd.hAdd (α := E [⋀^ι]→L[𝕜] F →L[𝕜] E [⋀^ι]→L[𝕜] G)
                    (let __LinearMap : E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G :=
                      (compContinuousAlternatingMapₗ 𝕜 E F G : (a : F →L[𝕜] G) → E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G) x;
                    { toLinearMap := __LinearMap, cont := ⋯ : E [⋀^ι]→L[𝕜] F →L[𝕜] E [⋀^ι]→L[𝕜] G })
                    (let __LinearMap : E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G :=
                      (compContinuousAlternatingMapₗ 𝕜 E F G : (a : F →L[𝕜] G) → E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G)
                        x_1;
                    { toLinearMap := __LinearMap, cont := ⋯ : E [⋀^ι]→L[𝕜] F →L[𝕜] E [⋀^ι]→L[𝕜] G }) :
                  (a : E [⋀^ι]→L[𝕜] F) → E [⋀^ι]→L[𝕜] G)
                x_2 :
              E [⋀^ι]→L[𝕜] G) :
            (a : ι → E) → G)
          x_3 :
        G)
⊢ (let __LinearMap : E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G :=
      (compContinuousAlternatingMapₗ 𝕜 E F G : (a : F →L[𝕜] G) → E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G) (x + x_1);
    { toLinearMap := __LinearMap, cont := ⋯ }) =
    HAdd.hAdd (α := E [⋀^ι]→L[𝕜] F →L[𝕜] E [⋀^ι]→L[𝕜] G)
      (let __LinearMap : E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G :=
        (compContinuousAlternatingMapₗ 𝕜 E F G : (a : F →L[𝕜] G) → E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G) x;
      { toLinearMap := __LinearMap, cont := ⋯ : E [⋀^ι]→L[𝕜] F →L[𝕜] E [⋀^ι]→L[𝕜] G })
      (let __LinearMap : E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G :=
        (compContinuousAlternatingMapₗ 𝕜 E F G : (a : F →L[𝕜] G) → E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G) x_1;
      { toLinearMap := __LinearMap, cont := ⋯ : E [⋀^ι]→L[𝕜] F →L[𝕜] E [⋀^ι]→L[𝕜] G })

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Topology
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜 F
inst_7 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousConstSMul 𝕜 F
inst_10 : AddCommGroup G
inst_11 : Module 𝕜 G
inst_12 : TopologicalSpace G
inst_13 : IsTopologicalAddGroup G
inst_14 : ContinuousConstSMul 𝕜 G
x x_1 : F →L[𝕜] G
x_2 : E [⋀^ι]→L[𝕜] F
x_3 : ι → E
⊢ Eq.{u_4 + 1} (α := G)
    ((((let __LinearMap : E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G :=
                  (compContinuousAlternatingMapₗ 𝕜 E F G : (a : F →L[𝕜] G) → E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G)
                    (x + x_1);
                { toLinearMap := __LinearMap, cont := ⋯ } :
                (a : E [⋀^ι]→L[𝕜] F) → E [⋀^ι]→L[𝕜] G)
              x_2 :
            E [⋀^ι]→L[𝕜] G) :
          (a : ι → E) → G)
        x_3 :
      G)
    ((((HAdd.hAdd (α := E [⋀^ι]→L[𝕜] F →L[𝕜] E [⋀^ι]→L[𝕜] G)
                  (let __LinearMap : E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G :=
                    (compContinuousAlternatingMapₗ 𝕜 E F G : (a : F →L[𝕜] G) → E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G) x;
                  { toLinearMap := __LinearMap, cont := ⋯ : E [⋀^ι]→L[𝕜] F →L[𝕜] E [⋀^ι]→L[𝕜] G })
                  (let __LinearMap : E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G :=
                    (compContinuousAlternatingMapₗ 𝕜 E F G : (a : F →L[𝕜] G) → E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G) x_1;
                  { toLinearMap := __LinearMap, cont := ⋯ : E [⋀^ι]→L[𝕜] F →L[𝕜] E [⋀^ι]→L[𝕜] G }) :
                (a : E [⋀^ι]→L[𝕜] F) → E [⋀^ι]→L[𝕜] G)
              x_2 :
            E [⋀^ι]→L[𝕜] G) :
          (a : ι → E) → G)
        x_3 :
      G)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Topology
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜 F
inst_7 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousConstSMul 𝕜 F
inst_10 : AddCommGroup G
inst_11 : Module 𝕜 G
inst_12 : TopologicalSpace G
inst_13 : IsTopologicalAddGroup G
inst_14 : ContinuousConstSMul 𝕜 G
x : 𝕜
x_1 : F →L[𝕜] G
h :
  ∀ (x_2 : E [⋀^ι]→L[𝕜] F) (x_3 : ι → E),
    Eq.{u_4 + 1} (α := G)
      ((((let __LinearMap : E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G :=
                    (compContinuousAlternatingMapₗ 𝕜 E F G : (a : F →L[𝕜] G) → E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G)
                      (x • x_1);
                  { toLinearMap := __LinearMap, cont := ⋯ } :
                  (a : E [⋀^ι]→L[𝕜] F) → E [⋀^ι]→L[𝕜] G)
                x_2 :
              E [⋀^ι]→L[𝕜] G) :
            (a : ι → E) → G)
          x_3 :
        G)
      ((((HSMul.hSMul (α := 𝕜) (β := E [⋀^ι]→L[𝕜] F →L[𝕜] E [⋀^ι]→L[𝕜] G) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
                    (let __LinearMap : E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G :=
                      (compContinuousAlternatingMapₗ 𝕜 E F G : (a : F →L[𝕜] G) → E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G)
                        x_1;
                    { toLinearMap := __LinearMap, cont := ⋯ : E [⋀^ι]→L[𝕜] F →L[𝕜] E [⋀^ι]→L[𝕜] G }) :
                  (a : E [⋀^ι]→L[𝕜] F) → E [⋀^ι]→L[𝕜] G)
                x_2 :
              E [⋀^ι]→L[𝕜] G) :
            (a : ι → E) → G)
          x_3 :
        G)
⊢ (let __LinearMap : E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G :=
      (compContinuousAlternatingMapₗ 𝕜 E F G : (a : F →L[𝕜] G) → E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G) (x • x_1);
    { toLinearMap := __LinearMap, cont := ⋯ }) =
    HSMul.hSMul (α := 𝕜) (β := E [⋀^ι]→L[𝕜] F →L[𝕜] E [⋀^ι]→L[𝕜] G) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
      (let __LinearMap : E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G :=
        (compContinuousAlternatingMapₗ 𝕜 E F G : (a : F →L[𝕜] G) → E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G) x_1;
      { toLinearMap := __LinearMap, cont := ⋯ : E [⋀^ι]→L[𝕜] F →L[𝕜] E [⋀^ι]→L[𝕜] G })

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Topology
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜 F
inst_7 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousConstSMul 𝕜 F
inst_10 : AddCommGroup G
inst_11 : Module 𝕜 G
inst_12 : TopologicalSpace G
inst_13 : IsTopologicalAddGroup G
inst_14 : ContinuousConstSMul 𝕜 G
x : 𝕜
x_1 : F →L[𝕜] G
x_2 : E [⋀^ι]→L[𝕜] F
x_3 : ι → E
⊢ Eq.{u_4 + 1} (α := G)
    ((((let __LinearMap : E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G :=
                  (compContinuousAlternatingMapₗ 𝕜 E F G : (a : F →L[𝕜] G) → E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G)
                    (x • x_1);
                { toLinearMap := __LinearMap, cont := ⋯ } :
                (a : E [⋀^ι]→L[𝕜] F) → E [⋀^ι]→L[𝕜] G)
              x_2 :
            E [⋀^ι]→L[𝕜] G) :
          (a : ι → E) → G)
        x_3 :
      G)
    ((((HSMul.hSMul (α := 𝕜) (β := E [⋀^ι]→L[𝕜] F →L[𝕜] E [⋀^ι]→L[𝕜] G) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
                  (let __LinearMap : E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G :=
                    (compContinuousAlternatingMapₗ 𝕜 E F G : (a : F →L[𝕜] G) → E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G) x_1;
                  { toLinearMap := __LinearMap, cont := ⋯ : E [⋀^ι]→L[𝕜] F →L[𝕜] E [⋀^ι]→L[𝕜] G }) :
                (a : E [⋀^ι]→L[𝕜] F) → E [⋀^ι]→L[𝕜] G)
              x_2 :
            E [⋀^ι]→L[𝕜] G) :
          (a : ι → E) → G)
        x_3 :
      G)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Topology
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜 F
inst_7 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousConstSMul 𝕜 F
inst_10 : AddCommGroup G
inst_11 : Module 𝕜 G
inst_12 : TopologicalSpace G
inst_13 : IsTopologicalAddGroup G
inst_14 : ContinuousConstSMul 𝕜 G
rw :
  Continuous[topologicalSpace, topologicalSpace]
    (Function.comp (β := E [⋀^ι]→L[𝕜] F →L[𝕜] E [⋀^ι]→L[𝕜] G)
      (comp (ContinuousAlternatingMap.toContinuousMultilinearMapCLM 𝕜)) fun (g : F →L[𝕜] G) ↦
      let __LinearMap : E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G :=
        (compContinuousAlternatingMapₗ 𝕜 E F G : (a : F →L[𝕜] G) → E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G) g;
      { toLinearMap := __LinearMap, cont := ⋯ })
⊢ Continuous[topologicalSpace, topologicalSpace] fun (g : F →L[𝕜] G) ↦
    let __LinearMap : E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G :=
      (compContinuousAlternatingMapₗ 𝕜 E F G : (a : F →L[𝕜] G) → E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G) g;
    { toLinearMap := __LinearMap, cont := ⋯ }

Tactic:
rw [ContinuousLinearMap.isEmbedding_postcomp
      (ContinuousAlternatingMap.toContinuousMultilinearMapCLM 𝕜)
      ContinuousAlternatingMap.isEmbedding_toContinuousMultilinearMap |>.continuous_iff]

Premises used: ContinuousLinearMap.isEmbedding_postcomp, Topology.IsEmbedding.continuous_iff
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Topology
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜 F
inst_7 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousConstSMul 𝕜 F
inst_10 : AddCommGroup G
inst_11 : Module 𝕜 G
inst_12 : TopologicalSpace G
inst_13 : IsTopologicalAddGroup G
inst_14 : ContinuousConstSMul 𝕜 G
⊢ Continuous[topologicalSpace, topologicalSpace]
    (Function.comp (β := E [⋀^ι]→L[𝕜] F →L[𝕜] E [⋀^ι]→L[𝕜] G)
      (comp (ContinuousAlternatingMap.toContinuousMultilinearMapCLM 𝕜)) fun (g : F →L[𝕜] G) ↦
      let __LinearMap : E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G :=
        (compContinuousAlternatingMapₗ 𝕜 E F G : (a : F →L[𝕜] G) → E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G) g;
      { toLinearMap := __LinearMap, cont := ⋯ })

Tactic:
map_continuous <|
      (precomp (ContinuousMultilinearMap 𝕜 (fun _ : ι ↦ E) G)
        ((ContinuousAlternatingMap.toContinuousMultilinearMapCLM 𝕜 : (E [⋀^ι]→L[𝕜] F) →L[𝕜] _))) ∘L
        (compContinuousMultilinearMapL 𝕜 (fun _ : ι ↦ E) F G)

Premises used: ContinuousLinearMap.comp, ContinuousAlternatingMap.toContinuousMultilinearMapLinear, ContinuousLinearMap.compContinuousMultilinearMap, ContinuousMultilinearMap, ContinuousLinearMap.precomp, ContinuousMapClass.map_continuous, ContinuousAlternatingMap.toContinuousMultilinearMapCLM, ContinuousLinearMap.compContinuousMultilinearMapL
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Topology
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜 F
inst_7 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousConstSMul 𝕜 F
inst_10 : AddCommGroup G
inst_11 : Module 𝕜 G
inst_12 : TopologicalSpace G
inst_13 : IsTopologicalAddGroup G
inst_14 : ContinuousConstSMul 𝕜 G
⊢ Continuous[topologicalSpace, topologicalSpace]
    (Function.comp (β := E [⋀^ι]→L[𝕜] F →L[𝕜] E [⋀^ι]→L[𝕜] G)
      (comp (ContinuousAlternatingMap.toContinuousMultilinearMapCLM 𝕜)) fun (g : F →L[𝕜] G) ↦
      let __LinearMap : E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G :=
        (compContinuousAlternatingMapₗ 𝕜 E F G : (a : F →L[𝕜] G) → E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G) g;
      { toLinearMap := __LinearMap, cont := ⋯ })

Tactic:
exact map_continuous <|
      (precomp (ContinuousMultilinearMap 𝕜 (fun _ : ι ↦ E) G)
        ((ContinuousAlternatingMap.toContinuousMultilinearMapCLM 𝕜 : (E [⋀^ι]→L[𝕜] F) →L[𝕜] _))) ∘L
        (compContinuousMultilinearMapL 𝕜 (fun _ : ι ↦ E) F G)

Premises used: ContinuousMultilinearMap, ContinuousLinearMap.precomp, ContinuousMapClass.map_continuous, ContinuousAlternatingMap.toContinuousMultilinearMapCLM, ContinuousLinearMap.compContinuousMultilinearMapL
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Topology
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_4
G : Type u_5
ι : Type u_6
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
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 (α := E [⋀^ι]→L[𝕜] G ≃L[𝕜] E [⋀^ι]→L[𝕜] F) (ContinuousLinearEquiv.symm g.continuousAlternatingMapCongrRight)
    g.symm.continuousAlternatingMapCongrRight

Tactic:
rfl

Premises used: ContinuousLinearEquiv.symm, LinearEquiv.symm, ContinuousLinearMap.compContinuousAlternatingMap, ContinuousLinearEquiv.continuousAlternatingMapCongrRight, rfl
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Topology
Goal:
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
ι : Type u_6
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : AddCommGroup E'
inst_5 : Module 𝕜 E'
inst_6 : TopologicalSpace E'
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
e : E ≃L[𝕜] E'
e' : F ≃L[𝕜] G
⊢ Eq (α := E [⋀^ι]→L[𝕜] F →L[𝕜] E' [⋀^ι]→L[𝕜] G)
    (↑(e.continuousAlternatingMapCongr e') : E [⋀^ι]→L[𝕜] F →L[𝕜] E' [⋀^ι]→L[𝕜] G)
    (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
      ((ContinuousLinearMap.compContinuousAlternatingMapCLM 𝕜 E' F G ι :
          (a : F →L[𝕜] G) → E' [⋀^ι]→L[𝕜] F →L[𝕜] E' [⋀^ι]→L[𝕜] G)
        (↑e' : F →L[𝕜] G))
      (ContinuousAlternatingMap.compContinuousLinearMapCLM (↑e.symm : E' →L[𝕜] E)))

Tactic:
rfl

Premises used: ContinuousLinearMap.comp, ContinuousLinearMap.compContinuousAlternatingMap, rfl, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTopologicalRing R
inst_6 : IsTopologicalAddGroup M
hmul : Tendsto (β := M) (fun (p : R × M) ↦ p.1 • p.2) (SProd.sprod (α := Filter R) (β := Filter M) (𝓝 0) (𝓝 0)) (𝓝 0)
hmulleft : ∀ (m : M), Tendsto.{u_1, u_2} (β := M) (fun (a : R) ↦ a • m) (𝓝 0) (𝓝 0)
hmulright : ∀ (a : R), Tendsto (β := M) (fun (m : M) ↦ a • m) (𝓝 0) (𝓝 0)
⊢ Tendsto (β := M) (fun (p : R × M) ↦ p.1 • p.2) (𝓝 (0, 0)) (𝓝 0)

Tactic:
rw [← nhds_prod_eq] at hmul

Premises used: nhds_prod_eq
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTopologicalRing R
inst_6 : IsTopologicalAddGroup M
hmul : Tendsto (β := M) (fun (p : R × M) ↦ p.1 • p.2) (SProd.sprod (α := Filter R) (β := Filter M) (𝓝 0) (𝓝 0)) (𝓝 0)
hmulleft : ∀ (m : M), Tendsto.{u_1, u_2} (β := M) (fun (a : R) ↦ a • m) (𝓝 0) (𝓝 0)
hmulright : ∀ (a : R), Tendsto (β := M) (fun (m : M) ↦ a • m) (𝓝 0) (𝓝 0)
hmul₁ : Tendsto (β := M) (fun (p : R × M) ↦ p.1 • p.2) (𝓝 (0, 0)) (𝓝 0)
⊢ ∀ (m : M), Tendsto.{u_1, u_2} (β := M) (fun (a : R) ↦ a • m) (𝓝 0) (𝓝 0)

Tactic:
rw [← nhds_prod_eq] at hmul

Premises used: nhds_prod_eq
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTopologicalRing R
inst_6 : IsTopologicalAddGroup M
hmul : Tendsto (β := M) (fun (p : R × M) ↦ p.1 • p.2) (SProd.sprod (α := Filter R) (β := Filter M) (𝓝 0) (𝓝 0)) (𝓝 0)
hmulleft : ∀ (m : M), Tendsto.{u_1, u_2} (β := M) (fun (a : R) ↦ a • m) (𝓝 0) (𝓝 0)
hmulright : ∀ (a : R), Tendsto (β := M) (fun (m : M) ↦ a • m) (𝓝 0) (𝓝 0)
hmul₁ : Tendsto (β := M) (fun (p : R × M) ↦ p.1 • p.2) (𝓝 (0, 0)) (𝓝 0)
hmulleft₁ : ∀ (m : M), Tendsto.{u_1, u_2} (β := M) (fun (a : R) ↦ a • m) (𝓝 0) (𝓝 0)
⊢ ∀ (a : R), Tendsto (β := M) (fun (m : M) ↦ a • m) (𝓝 0) (𝓝 0)

Tactic:
rw [← nhds_prod_eq] at hmul

Premises used: nhds_prod_eq
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTopologicalRing R
inst_6 : IsTopologicalAddGroup M
hmul : Tendsto (β := M) (fun (p : R × M) ↦ p.1 • p.2) (𝓝 (0, 0)) (𝓝 0)
hmulleft : ∀ (m : M), Tendsto.{u_1, u_2} (β := M) (fun (a : R) ↦ a • m) (𝓝 0) (𝓝 0)
hmulright : ∀ (a : R), Tendsto (β := M) (fun (m : M) ↦ a • m) (𝓝 0) (𝓝 0)
⊢ Continuous[instTopologicalSpaceProd, inst_2] fun (p : R × M) ↦ p.1 • p.2

Tactic:
continuous_of_continuousAt_zero₂ (AddMonoidHom.smul : R →+ M →+ M) ?_ ?_ ?_

Premises used: AddMonoidHom.smul, continuous_of_continuousAt_zero₂
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTopologicalRing R
inst_6 : IsTopologicalAddGroup M
hmul : Tendsto (β := M) (fun (p : R × M) ↦ p.1 • p.2) (𝓝 (0, 0)) (𝓝 0)
hmulleft : ∀ (m : M), Tendsto.{u_1, u_2} (β := M) (fun (a : R) ↦ a • m) (𝓝 0) (𝓝 0)
hmulright : ∀ (a : R), Tendsto (β := M) (fun (m : M) ↦ a • m) (𝓝 0) (𝓝 0)
refine_1 :
  ContinuousAt (Y := M)
    (fun (x : R × M) ↦
      ((((AddMonoidHom.smul : AddMonoidHom.{u_1, u_2} R (M →+ M)) : (a : R) → M →+ M) x.1 : M →+ M) : (a : M) → M) x.2)
    (0, 0)
refine_2 :
  ∀ (x : R),
    ContinuousAt.{u_2, u_2} (X := M) (Y := M)
      (⇑(((AddMonoidHom.smul : AddMonoidHom.{u_1, u_2} R (M →+ M)) : (a : R) → M →+ M) x : M →+ M) : (a : M) → M) 0
refine_3 :
  ∀ (y : M),
    ContinuousAt.{u_1, u_2} (Y := M)
      (fun (x : R) ↦
        ((((AddMonoidHom.smul : AddMonoidHom.{u_1, u_2} R (M →+ M)) : (a : R) → M →+ M) x : M →+ M) : (a : M) → M) y)
      0
⊢ Continuous[instTopologicalSpaceProd, inst_2] fun (p : R × M) ↦ p.1 • p.2

Tactic:
refine continuous_of_continuousAt_zero₂ (AddMonoidHom.smul : R →+ M →+ M) ?_ ?_ ?_

Premises used: AddMonoidHom.smul, continuous_of_continuousAt_zero₂
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTopologicalRing R
inst_6 : IsTopologicalAddGroup M
hmul : Tendsto (β := M) (fun (p : R × M) ↦ p.1 • p.2) (𝓝 (0, 0)) (𝓝 0)
hmulleft : ∀ (m : M), Tendsto.{u_1, u_2} (β := M) (fun (a : R) ↦ a • m) (𝓝 0) (𝓝 0)
hmulright : ∀ (a : R), Tendsto (β := M) (fun (m : M) ↦ a • m) (𝓝 0) (𝓝 0)
⊢ ContinuousAt (Y := M)
    (fun (x : R × M) ↦
      ((((AddMonoidHom.smul : AddMonoidHom.{u_1, u_2} R (M →+ M)) : (a : R) → M →+ M) x.1 : M →+ M) : (a : M) → M) x.2)
    (0, 0)

Tactic:
simpa [ContinuousAt]

Premises used: ContinuousAt
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTopologicalRing R
inst_6 : IsTopologicalAddGroup M
hmul : Tendsto (β := M) (fun (p : R × M) ↦ p.1 • p.2) (𝓝 (0, 0)) (𝓝 0)
hmulleft : ∀ (m : M), Tendsto.{u_1, u_2} (β := M) (fun (a : R) ↦ a • m) (𝓝 0) (𝓝 0)
hmulright : ∀ (a : R), Tendsto (β := M) (fun (m : M) ↦ a • m) (𝓝 0) (𝓝 0)
⊢ ∀ (x : R),
    ContinuousAt.{u_2, u_2} (X := M) (Y := M)
      (⇑(((AddMonoidHom.smul : AddMonoidHom.{u_1, u_2} R (M →+ M)) : (a : R) → M →+ M) x : M →+ M) : (a : M) → M) 0

Tactic:
simpa [ContinuousAt]

Premises used: ContinuousAt
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTopologicalRing R
inst_6 : IsTopologicalAddGroup M
hmul : Tendsto (β := M) (fun (p : R × M) ↦ p.1 • p.2) (𝓝 (0, 0)) (𝓝 0)
hmulleft : ∀ (m : M), Tendsto.{u_1, u_2} (β := M) (fun (a : R) ↦ a • m) (𝓝 0) (𝓝 0)
hmulright : ∀ (a : R), Tendsto (β := M) (fun (m : M) ↦ a • m) (𝓝 0) (𝓝 0)
⊢ ∀ (y : M),
    ContinuousAt.{u_1, u_2} (Y := M)
      (fun (x : R) ↦
        ((((AddMonoidHom.smul : AddMonoidHom.{u_1, u_2} R (M →+ M)) : (a : R) → M →+ M) x : M →+ M) : (a : M) → M) y)
      0

Tactic:
simpa [ContinuousAt]

Premises used: ContinuousAt
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace M
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : ContinuousConstSMul R M
⊢ Continuous[inst_1, inst_1] fun (a : M) ↦ -a

Tactic:
simpa using continuous_const_smul (T := M) (-1 : R)

Premises used: ContinuousConstSMul.continuous_const_smul, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : ContinuousAdd M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : NeBot.{u_1} (α := R) (𝓝[{x : R | IsUnit x}] 0)
s : Submodule R M
hs : (interior (↑s : Set M)).Nonempty
rcases : ∀ (y : M) (hy : y ∈ interior (↑s : Set M)), s = ⊤
⊢ s = ⊤

Tactic:
rcases hs with ⟨y, hy⟩
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : ContinuousAdd M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : NeBot.{u_1} (α := R) (𝓝[{x : R | IsUnit x}] 0)
s : Submodule R M
y : M
hy : y ∈ interior (↑s : Set M)
⊢ s = ⊤

Tactic:
Submodule.eq_top_iff'.2 fun x => ?_

Premises used: Iff.mpr, Submodule.eq_top_iff'
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : ContinuousAdd M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : NeBot.{u_1} (α := R) (𝓝[{x : R | IsUnit x}] 0)
s : Submodule R M
y : M
hy : y ∈ interior (↑s : Set M)
refine : ∀ (x : M), x ∈ s
⊢ s = ⊤

Tactic:
refine Submodule.eq_top_iff'.2 fun x => ?_

Premises used: Iff.mpr, Submodule.eq_top_iff'
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : ContinuousAdd M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : NeBot.{u_1} (α := R) (𝓝[{x : R | IsUnit x}] 0)
s : Submodule R M
y : M
hy : y ∈ interior (↑s : Set M)
x : M
rw : ∀ (hy : (↑s : Set M) ∈ 𝓝 y) (x : M), x ∈ s
⊢ x ∈ s

Tactic:
rw [mem_interior_iff_mem_nhds] at hy

Premises used: mem_interior_iff_mem_nhds