awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
Goal:
R : Type u
ι : Type v
n : ℕ
M : Fin n.succ → Type w
M₁ : ι → Type w₁
M₁' : ι → Type w₁'
M₂ : Type w₂
M₃ : Type w₃
M₄ : Type w₄
inst : Semiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : (i : ι) → AddCommMonoid (M₁ i)
inst_3 : (i : ι) → AddCommMonoid (M₁' i)
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : AddCommMonoid M₄
inst_7 : (i : Fin n.succ) → Module.{u, w} R (M i)
inst_8 : (i : ι) → Module.{u, w₁} R (M₁ i)
inst_9 : (i : ι) → Module.{u, w₁'} R (M₁' i)
inst_10 : Module R M₂
inst_11 : Module R M₃
inst_12 : Module R M₄
inst_13 : (i : Fin n.succ) → TopologicalSpace (M i)
inst_14 : (i : ι) → TopologicalSpace (M₁ i)
inst_15 : (i : ι) → TopologicalSpace (M₁' i)
inst_16 : TopologicalSpace M₂
inst_17 : TopologicalSpace M₃
inst_18 : TopologicalSpace M₄
f f' : ContinuousMultilinearMap R M₁ M₂
R' : Type u_1
R'' : Type u_2
A : Type u_3
inst_19 : Semiring A
inst_20 : (i : ι) → Module.{u_3, w₁} A (M₁ i)
inst_21 : Module A M₂
inst_22 : DistribSMul R' M₂
inst_23 : ContinuousConstSMul R' M₂
inst_24 : SMulCommClass A R' M₂
inst_25 : DistribSMul R'' M₂
inst_26 : ContinuousConstSMul R'' M₂
inst_27 : SMulCommClass A R'' M₂
inst_28 : SMul R' R''
inst_29 : IsScalarTower R' R'' M₂
⊢ IsScalarTower R' R'' (ContinuousMultilinearMap A M₁ M₂)

Tactic:
⟨fun _ _ _ => ext fun _ => smul_assoc _ _ _⟩

Premises used: smul_assoc, ContinuousMultilinearMap.ext, ContinuousMultilinearMap.toMultilinearMap, IsScalarTower.mk, DFunLike.coe
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
Goal:
R : Type u
ι : Type v
n : ℕ
M : Fin n.succ → Type w
M₁ : ι → Type w₁
M₁' : ι → Type w₁'
M₂ : Type w₂
M₃ : Type w₃
M₄ : Type w₄
inst : Semiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : (i : ι) → AddCommMonoid (M₁ i)
inst_3 : (i : ι) → AddCommMonoid (M₁' i)
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : AddCommMonoid M₄
inst_7 : (i : Fin n.succ) → Module.{u, w} R (M i)
inst_8 : (i : ι) → Module.{u, w₁} R (M₁ i)
inst_9 : (i : ι) → Module.{u, w₁'} R (M₁' i)
inst_10 : Module R M₂
inst_11 : Module R M₃
inst_12 : Module R M₄
inst_13 : (i : Fin n.succ) → TopologicalSpace (M i)
inst_14 : (i : ι) → TopologicalSpace (M₁ i)
inst_15 : (i : ι) → TopologicalSpace (M₁' i)
inst_16 : TopologicalSpace M₂
inst_17 : TopologicalSpace M₃
inst_18 : TopologicalSpace M₄
f f' : ContinuousMultilinearMap R M₁ M₂
R' : Type u_1
R'' : Type u_2
A : Type u_3
inst_19 : Semiring A
inst_20 : (i : ι) → Module.{u_3, w₁} A (M₁ i)
inst_21 : Module A M₂
inst_22 : DistribSMul R' M₂
inst_23 : ContinuousConstSMul R' M₂
inst_24 : SMulCommClass A R' M₂
inst_25 : DistribSMul R'' M₂
inst_26 : ContinuousConstSMul R'' M₂
inst_27 : SMulCommClass A R'' M₂
inst_28 : DistribSMul.{u_1, w₂} R'ᵐᵒᵖ M₂
inst_29 : IsCentralScalar R' M₂
⊢ IsCentralScalar R' (ContinuousMultilinearMap A M₁ M₂)

Tactic:
⟨fun _ _ => ext fun _ => op_smul_eq_smul _ _⟩

Premises used: ContinuousMultilinearMap.ext, ContinuousMultilinearMap.toMultilinearMap, IsCentralScalar.mk, DFunLike.coe, IsCentralScalar.op_smul_eq_smul
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
Goal:
R : Type u
ι : Type v
M₁ : ι → Type w₁
M₂ : Type w₂
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : ι) → Module.{u, w₁} R (M₁ i)
inst_4 : Module R M₂
inst_5 : (i : ι) → TopologicalSpace (M₁ i)
inst_6 : TopologicalSpace M₂
f f' : ContinuousMultilinearMap R M₁ M₂
inst_7 : ContinuousAdd M₂
m : (i : ι) → M₁ i
⊢ (f + f' : (a : (i : ι) → M₁ i) → M₂) m =
    HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) m : M₂) ((f' : (a : (i : ι) → M₁ i) → M₂) m : M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
Goal:
R : Type u
ι : Type v
M₁ : ι → Type w₁
M₂ : Type w₂
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : ι) → Module.{u, w₁} R (M₁ i)
inst_4 : Module R M₂
inst_5 : (i : ι) → TopologicalSpace (M₁ i)
inst_6 : TopologicalSpace M₂
inst_7 : ContinuousAdd M₂
f g : ContinuousMultilinearMap R M₁ M₂
⊢ (f + g).toMultilinearMap (M₁ := M₁) = f.toMultilinearMap (M₁ := M₁) + g.toMultilinearMap (M₁ := M₁)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
Goal:
R : Type u
ι : Type v
M₁ : ι → Type w₁
M₂ : Type w₂
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : ι) → Module.{u, w₁} R (M₁ i)
inst_4 : Module R M₂
inst_5 : (i : ι) → TopologicalSpace (M₁ i)
inst_6 : TopologicalSpace M₂
inst_7 : ContinuousAdd M₂
α : Type u_1
f : α → ContinuousMultilinearMap R M₁ M₂
m : (i : ι) → M₁ i
s : Finset α
⊢ Eq.{w₂ + 1} (α := M₂) ((∑ a ∈ s, f a : (a : (i : ι) → M₁ i) → M₂) m : M₂)
    (∑ a ∈ s, (f a : (a : (i : ι) → M₁ i) → M₂) m : M₂)

Tactic:
map_sum (applyAddHom m) f s

Premises used: map_sum, ContinuousMultilinearMap.applyAddHom
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
Goal:
R : Type u
ι : Type v
M₁ : ι → Type w₁
M₂ : Type w₂
M₃ : Type w₃
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : (i : ι) → Module.{u, w₁} R (M₁ i)
inst_5 : Module R M₂
inst_6 : Module R M₃
inst_7 : (i : ι) → TopologicalSpace (M₁ i)
inst_8 : TopologicalSpace M₂
inst_9 : TopologicalSpace M₃
f : ContinuousMultilinearMap R M₁ M₂
g : ContinuousMultilinearMap R M₁ M₃
m : (i : ι) → M₁ i
⊢ Eq (α := M₂ × M₃) ((f.prod (M₁ := M₁) g : (a : (i : ι) → M₁ i) → M₂ × M₃) m : M₂ × M₃)
    (((f : (a : (i : ι) → M₁ i) → M₂) m, (g : (a : (i : ι) → M₁ i) → M₃) m) : M₂ × M₃)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
Goal:
R : Type u
ι : Type v
M₁ : ι → Type w₁
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : (i : ι) → Module.{u, w₁} R (M₁ i)
inst_3 : (i : ι) → TopologicalSpace (M₁ i)
ι' : Type u_1
M' : ι' → Type u_2
inst_4 : (i : ι') → AddCommMonoid (M' i)
inst_5 : (i : ι') → TopologicalSpace (M' i)
inst_6 : (i : ι') → Module.{u, u_2} R (M' i)
f : (i : ι') → ContinuousMultilinearMap.{u, v, w₁, u_2} R M₁ (M' i)
⊢ Eq (α := (a : (i : ι) → M₁ i) → (i : ι') → M' i)
    (⇑(pi (M₁ := M₁) (M' := M') f) : (a : (i : ι) → M₁ i) → (i : ι') → M' i) fun (m : (i : ι) → M₁ i) (j : ι') ↦
    (f j : (a : (i : ι) → M₁ i) → M' j) m

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
Goal:
R : Type u
ι : Type v
M₁ : ι → Type w₁
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : (i : ι) → Module.{u, w₁} R (M₁ i)
inst_3 : (i : ι) → TopologicalSpace (M₁ i)
ι' : Type u_1
M' : ι' → Type u_2
inst_4 : (i : ι') → AddCommMonoid (M' i)
inst_5 : (i : ι') → TopologicalSpace (M' i)
inst_6 : (i : ι') → Module.{u, u_2} R (M' i)
f : (i : ι') → ContinuousMultilinearMap.{u, v, w₁, u_2} R M₁ (M' i)
m : (i : ι) → M₁ i
j : ι'
⊢ Eq.{u_2 + 1} (α := M' j) ((pi (M₁ := M₁) (M' := M') f : (a : (i : ι) → M₁ i) → (i : ι') → M' i) m j : M' j)
    ((f j : (a : (i : ι) → M₁ i) → M' j) m : M' j)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
Goal:
R : Type u
ι : Type v
M₁ : ι → Type w₁
M₁' : ι → Type w₁'
M₄ : Type w₄
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : (i : ι) → AddCommMonoid (M₁' i)
inst_3 : AddCommMonoid M₄
inst_4 : (i : ι) → Module.{u, w₁} R (M₁ i)
inst_5 : (i : ι) → Module.{u, w₁'} R (M₁' i)
inst_6 : Module R M₄
inst_7 : (i : ι) → TopologicalSpace (M₁ i)
inst_8 : (i : ι) → TopologicalSpace (M₁' i)
inst_9 : TopologicalSpace M₄
g : ContinuousMultilinearMap R M₁' M₄
f : (i : ι) → ContinuousLinearMap.{u, u, w₁, w₁'} (RingHom.id R) (M₁ i) (M₁' i)
m : (i : ι) → M₁ i
⊢ Eq.{w₄ + 1} (α := M₄) ((g.compContinuousLinearMap (M₁ := M₁) (M₁' := M₁') f : (a : (i : ι) → M₁ i) → M₄) m : M₄)
    ((g : (a : (i : ι) → M₁' i) → M₄) fun (i : ι) ↦ (f i : (a : M₁ i) → M₁' i) (m i) : M₄)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
Goal:
R : Type u
ι : Type v
M₁ : ι → Type w₁
M₂ : Type w₂
M₃ : Type w₃
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : (i : ι) → Module.{u, w₁} R (M₁ i)
inst_5 : Module R M₂
inst_6 : Module R M₃
inst_7 : (i : ι) → TopologicalSpace (M₁ i)
inst_8 : TopologicalSpace M₂
inst_9 : TopologicalSpace M₃
g : M₂ →L[R] M₃
f : ContinuousMultilinearMap R M₁ M₂
h :
  ∀ (m : (i : ι) → M₁ i),
    Eq.{w₃ + 1} (α := M₃) ((g.compContinuousMultilinearMap (M₁ := M₁) f : (a : (i : ι) → M₁ i) → M₃) m : M₃)
      (comp (β := M₂) (⇑g : (a : M₂) → M₃) (⇑f : (a : (i : ι) → M₁ i) → M₂) m : M₃)
⊢ Eq (α := (a : (i : ι) → M₁ i) → M₃) (⇑(g.compContinuousMultilinearMap (M₁ := M₁) f) : (a : (i : ι) → M₁ i) → M₃)
    (comp (β := M₂) (⇑g : (a : M₂) → M₃) (⇑f : (a : (i : ι) → M₁ i) → M₂))

Tactic:
ext m
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
Goal:
R : Type u
ι : Type v
M₁ : ι → Type w₁
M₂ : Type w₂
M₃ : Type w₃
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : (i : ι) → Module.{u, w₁} R (M₁ i)
inst_5 : Module R M₂
inst_6 : Module R M₃
inst_7 : (i : ι) → TopologicalSpace (M₁ i)
inst_8 : TopologicalSpace M₂
inst_9 : TopologicalSpace M₃
g : M₂ →L[R] M₃
f : ContinuousMultilinearMap R M₁ M₂
m : (i : ι) → M₁ i
⊢ Eq.{w₃ + 1} (α := M₃) ((g.compContinuousMultilinearMap (M₁ := M₁) f : (a : (i : ι) → M₁ i) → M₃) m : M₃)
    (comp (β := M₂) (⇑g : (a : M₂) → M₃) (⇑f : (a : (i : ι) → M₁ i) → M₂) m : M₃)

Tactic:
rfl
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
Goal:
R : Type u
ι : Type v
M₁ : ι → Type w₁
M₂ : Type w₂
M₃ : Type w₃
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : (i : ι) → Module.{u, w₁} R (M₁ i)
inst_5 : Module R M₂
inst_6 : Module R M₃
inst_7 : (i : ι) → TopologicalSpace (M₁ i)
inst_8 : TopologicalSpace M₂
inst_9 : TopologicalSpace M₃
f g : ContinuousMultilinearMap R M₁ (M₂ × M₃)
rw :
  f = g ↔
    (ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.fst R M₂ M₃) f,
        ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.snd R M₂ M₃) f) =
      (ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.fst R M₂ M₃) g,
        ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.snd R M₂ M₃) g)
rw₁ :
  f = g ↔
    (Equiv.symm (prodEquiv (M₁ := M₁)) :
          (a : ContinuousMultilinearMap R M₁ (M₂ × M₃)) →
            ContinuousMultilinearMap R M₁ M₂ × ContinuousMultilinearMap R M₁ M₃)
        f =
      (ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.fst R M₂ M₃) g,
        ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.snd R M₂ M₃) g)
rw₂ :
  f = g ↔
    Eq (α := ContinuousMultilinearMap R M₁ M₂ × ContinuousMultilinearMap R M₁ M₃)
      ((Equiv.symm (prodEquiv (M₁ := M₁)) :
            (a : ContinuousMultilinearMap R M₁ (M₂ × M₃)) →
              ContinuousMultilinearMap R M₁ M₂ × ContinuousMultilinearMap R M₁ M₃)
          f :
        ContinuousMultilinearMap R M₁ M₂ × ContinuousMultilinearMap R M₁ M₃)
      ((Equiv.symm (prodEquiv (M₁ := M₁)) :
            (a : ContinuousMultilinearMap R M₁ (M₂ × M₃)) →
              ContinuousMultilinearMap R M₁ M₂ × ContinuousMultilinearMap R M₁ M₃)
          g :
        ContinuousMultilinearMap R M₁ M₂ × ContinuousMultilinearMap R M₁ M₃)
rw₃ rw₄ : f = g ↔ f = g
⊢ f = g ↔
    ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.fst R M₂ M₃) f =
        ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.fst R M₂ M₃) g ∧
      ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.snd R M₂ M₃) f =
        ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.snd R M₂ M₃) g

Tactic:
rw [← Prod.mk_inj, ← prodEquiv_symm_apply, ← prodEquiv_symm_apply, Equiv.apply_eq_iff_eq]

Premises used: Prod.mk_inj, ContinuousMultilinearMap.prodEquiv_symm_apply, Equiv.apply_eq_iff_eq
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
Goal:
R : Type u
ι : Type v
M₁ : ι → Type w₁
M₂ : Type w₂
M₃ : Type w₃
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : (i : ι) → Module.{u, w₁} R (M₁ i)
inst_5 : Module R M₂
inst_6 : Module R M₃
inst_7 : (i : ι) → TopologicalSpace (M₁ i)
inst_8 : TopologicalSpace M₂
inst_9 : TopologicalSpace M₃
f g : ContinuousMultilinearMap R M₁ (M₂ × M₃)
h₁ :
  ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.fst R M₂ M₃) f =
    ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.fst R M₂ M₃) g
h₂ :
  ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.snd R M₂ M₃) f =
    ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.snd R M₂ M₃) g
⊢ f = g

Tactic:
prod_ext_iff.mpr ⟨h₁, h₂⟩

Premises used: Iff.mpr, ContinuousMultilinearMap.prod_ext_iff, And.intro
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
Goal:
R : Type u
ι : Type v
M₁ : ι → Type w₁
M₂ : Type w₂
M₃ : Type w₃
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : (i : ι) → Module.{u, w₁} R (M₁ i)
inst_5 : Module R M₂
inst_6 : Module R M₃
inst_7 : (i : ι) → TopologicalSpace (M₁ i)
inst_8 : TopologicalSpace M₂
inst_9 : TopologicalSpace M₃
f : ContinuousMultilinearMap R M₁ (M₂ × M₃)
g : ContinuousMultilinearMap R M₁ M₂
h : ContinuousMultilinearMap R M₁ M₃
⊢ f = g.prod (M₁ := M₁) h ↔
    ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.fst R M₂ M₃) f = g ∧
      ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.snd R M₂ M₃) f = h

Tactic:
prod_ext_iff

Premises used: ContinuousMultilinearMap.prod_ext_iff, ContinuousLinearMap.compContinuousMultilinearMap, LinearMap.compMultilinearMap
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
Goal:
R : Type u
ι : Type v
M₁ : ι → Type w₁
M₂ : Type w₂
M₃ : Type w₃
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : (i : ι) → Module.{u, w₁} R (M₁ i)
inst_5 : Module R M₂
inst_6 : Module R M₃
inst_7 : (i : ι) → TopologicalSpace (M₁ i)
inst_8 : TopologicalSpace M₂
inst_9 : TopologicalSpace M₃
inst_10 : ContinuousAdd M₂
inst_11 : ContinuousAdd M₃
f₁ f₂ : ContinuousMultilinearMap R M₁ M₂
g₁ g₂ : ContinuousMultilinearMap R M₁ M₃
⊢ (f₁ + f₂).prod (M₁ := M₁) (g₁ + g₂) = f₁.prod (M₁ := M₁) g₁ + f₂.prod (M₁ := M₁) g₂

Tactic:
rfl

Premises used: MultilinearMap.prod, ContinuousMultilinearMap.prod, rfl
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
Goal:
R : Type u
ι : Type v
M₁ : ι → Type w₁
M₂ : Type w₂
M₃ : Type w₃
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : (i : ι) → Module.{u, w₁} R (M₁ i)
inst_5 : Module R M₂
inst_6 : Module R M₃
inst_7 : (i : ι) → TopologicalSpace (M₁ i)
inst_8 : TopologicalSpace M₂
inst_9 : TopologicalSpace M₃
S : Type u_1
inst_10 : Monoid S
inst_11 : DistribMulAction S M₂
inst_12 : DistribMulAction S M₃
inst_13 : ContinuousConstSMul S M₂
inst_14 : SMulCommClass R S M₂
inst_15 : ContinuousConstSMul S M₃
inst_16 : SMulCommClass R S M₃
c : S
f : ContinuousMultilinearMap R M₁ M₂
g : ContinuousMultilinearMap R M₁ M₃
⊢ (c • f).prod (M₁ := M₁) (c • g) = c • f.prod (M₁ := M₁) g

Tactic:
rfl

Premises used: MultilinearMap.prod, ContinuousMultilinearMap.prod, rfl
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
Goal:
R : Type u
ι : Type v
M₁ : ι → Type w₁
M₂ : Type w₂
M₃ : Type w₃
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : (i : ι) → Module.{u, w₁} R (M₁ i)
inst_5 : Module R M₂
inst_6 : Module R M₃
inst_7 : (i : ι) → TopologicalSpace (M₁ i)
inst_8 : TopologicalSpace M₂
inst_9 : TopologicalSpace M₃
⊢ Eq (α := ContinuousMultilinearMap R M₁ (M₂ × M₃)) (prod (M₁ := M₁) 0 0) 0

Tactic:
rfl

Premises used: MultilinearMap.prod, ContinuousMultilinearMap.prod, rfl
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
Goal:
R : Type u
ι : Type v
n : ℕ
M : Fin n.succ → Type w
M₁ : ι → Type w₁
M₁' : ι → Type w₁'
M₂ : Type w₂
M₃ : Type w₃
M₄ : Type w₄
inst : Semiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : (i : ι) → AddCommMonoid (M₁ i)
inst_3 : (i : ι) → AddCommMonoid (M₁' i)
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : AddCommMonoid M₄
inst_7 : (i : Fin n.succ) → Module.{u, w} R (M i)
inst_8 : (i : ι) → Module.{u, w₁} R (M₁ i)
inst_9 : (i : ι) → Module.{u, w₁'} R (M₁' i)
inst_10 : Module R M₂
inst_11 : Module R M₃
inst_12 : Module R M₄
inst_13 : (i : Fin n.succ) → TopologicalSpace (M i)
inst_14 : (i : ι) → TopologicalSpace (M₁ i)
inst_15 : (i : ι) → TopologicalSpace (M₁' i)
inst_16 : TopologicalSpace M₂
inst_17 : TopologicalSpace M₃
inst_18 : TopologicalSpace M₄
f f' : ContinuousMultilinearMap R M₁ M₂
ι' : Type u_1
e : ι ≃ ι'
x : ContinuousMultilinearMap.{u, v, w₂, w₃} R (fun (x : ι) ↦ M₂) M₃
x_1 : (i : ι) → M₂
⊢ Eq.{w₃ + 1} (α := M₃) ((domDomCongr e.symm (domDomCongr e x) : (a : (i : ι) → M₂) → M₃) x_1 : M₃)
    ((x : (a : (i : ι) → M₂) → M₃) x_1 : M₃)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
Goal:
R : Type u
ι : Type v
n : ℕ
M : Fin n.succ → Type w
M₁ : ι → Type w₁
M₁' : ι → Type w₁'
M₂ : Type w₂
M₃ : Type w₃
M₄ : Type w₄
inst : Semiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : (i : ι) → AddCommMonoid (M₁ i)
inst_3 : (i : ι) → AddCommMonoid (M₁' i)
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : AddCommMonoid M₄
inst_7 : (i : Fin n.succ) → Module.{u, w} R (M i)
inst_8 : (i : ι) → Module.{u, w₁} R (M₁ i)
inst_9 : (i : ι) → Module.{u, w₁'} R (M₁' i)
inst_10 : Module R M₂
inst_11 : Module R M₃
inst_12 : Module R M₄
inst_13 : (i : Fin n.succ) → TopologicalSpace (M i)
inst_14 : (i : ι) → TopologicalSpace (M₁ i)
inst_15 : (i : ι) → TopologicalSpace (M₁' i)
inst_16 : TopologicalSpace M₂
inst_17 : TopologicalSpace M₃
inst_18 : TopologicalSpace M₄
f f' : ContinuousMultilinearMap R M₁ M₂
ι' : Type u_1
e : ι ≃ ι'
x : ContinuousMultilinearMap.{u, u_1, w₂, w₃} R (fun (x : ι') ↦ M₂) M₃
x_1 : (i : ι') → M₂
⊢ Eq.{w₃ + 1} (α := M₃) ((domDomCongr e (domDomCongr e.symm x) : (a : (i : ι') → M₂) → M₃) x_1 : M₃)
    ((x : (a : (i : ι') → M₂) → M₃) x_1 : M₃)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
Goal:
R : Type u
ι : Type v
M₁ : ι → Type w₁
M₂ : Type w₂
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : ι) → Module.{u, w₁} R (M₁ i)
inst_4 : Module R M₂
inst_5 : (i : ι) → TopologicalSpace (M₁ i)
inst_6 : TopologicalSpace M₂
f : ContinuousMultilinearMap R M₁ M₂
inst_7 : ContinuousAdd M₂
inst_8 : DecidableEq ι
inst_9 : Fintype ι
x y : (i : ι) → M₁ i
unfold :
  Eq.{w₂ + 1} (α := M₂)
    ((∑ i : ι,
            ContinuousLinearMap.comp (σ₂₃ := RingHom.id R)
              (let __src := f.toMultilinearMap (M₁ := M₁).toLinearMap (M₁ := M₁) x i;
              { toLinearMap := __src, cont := ⋯ })
              (ContinuousLinearMap.proj (φ := M₁) i) :
          (a : (i : ι) → M₁ i) → M₂)
        y :
      M₂)
    (∑ i : ι, (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) x i (y i)) : M₂)
⊢ Eq.{w₂ + 1} (α := M₂) ((f.linearDeriv (M₁ := M₁) x : (a : (i : ι) → M₁ i) → M₂) y : M₂)
    (∑ i : ι, (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) x i (y i)) : M₂)

Tactic:
unfold linearDeriv toContinuousLinearMap

Premises used: ContinuousMultilinearMap.linearDeriv, ContinuousMultilinearMap.toContinuousLinearMap
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
Goal:
R : Type u
ι : Type v
M₁ : ι → Type w₁
M₂ : Type w₂
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : ι) → Module.{u, w₁} R (M₁ i)
inst_4 : Module R M₂
inst_5 : (i : ι) → TopologicalSpace (M₁ i)
inst_6 : TopologicalSpace M₂
f : ContinuousMultilinearMap R M₁ M₂
inst_7 : ContinuousAdd M₂
inst_8 : DecidableEq ι
inst_9 : Fintype ι
x y : (i : ι) → M₁ i
simp :
  Eq.{w₂ + 1} (α := M₂)
    (∑ c : ι,
      comp (β := M₁ c) (⇑(f.toMultilinearMap (M₁ := M₁).toLinearMap (M₁ := M₁) x c) : (a : M₁ c) → M₂)
        (⇑(ContinuousLinearMap.proj (φ := M₁) c) : (a : (i : ι) → M₁ i) → M₁ c) y)
    (∑ i : ι, (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) x i (y i)))
⊢ Eq.{w₂ + 1} (α := M₂)
    ((∑ i : ι,
            ContinuousLinearMap.comp (σ₂₃ := RingHom.id R)
              (let __src := f.toMultilinearMap (M₁ := M₁).toLinearMap (M₁ := M₁) x i;
              { toLinearMap := __src, cont := ⋯ })
              (ContinuousLinearMap.proj (φ := M₁) i) :
          (a : (i : ι) → M₁ i) → M₂)
        y :
      M₂)
    (∑ i : ι, (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) x i (y i)) : M₂)

Tactic:
simp only [ContinuousLinearMap.coe_sum', ContinuousLinearMap.coe_comp',
    ContinuousLinearMap.coe_mk', Finset.sum_apply]

Premises used: ContinuousLinearMap.coe_comp', Finset.sum_apply, ContinuousLinearMap.coe_sum', ContinuousLinearMap.coe_mk'
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
Goal:
R : Type u
ι : Type v
M₁ : ι → Type w₁
M₂ : Type w₂
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : ι) → Module.{u, w₁} R (M₁ i)
inst_4 : Module R M₂
inst_5 : (i : ι) → TopologicalSpace (M₁ i)
inst_6 : TopologicalSpace M₂
f : ContinuousMultilinearMap R M₁ M₂
inst_7 : ContinuousAdd M₂
inst_8 : DecidableEq ι
inst_9 : Fintype ι
x y : (i : ι) → M₁ i
⊢ Eq.{w₂ + 1} (α := M₂)
    (∑ c : ι,
      comp (β := M₁ c) (⇑(f.toMultilinearMap (M₁ := M₁).toLinearMap (M₁ := M₁) x c) : (a : M₁ c) → M₂)
        (⇑(ContinuousLinearMap.proj (φ := M₁) c) : (a : (i : ι) → M₁ i) → M₁ c) y)
    (∑ i : ι, (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) x i (y i)))

Tactic:
rfl
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
Goal:
R : Type u
n : ℕ
M : Fin n.succ → Type w
M₂ : Type w₂
inst : Semiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : Fin n.succ) → Module.{u, w} R (M i)
inst_4 : Module R M₂
inst_5 : (i : Fin n.succ) → TopologicalSpace (M i)
inst_6 : TopologicalSpace M₂
f : ContinuousMultilinearMap R M M₂
m : (i : Fin n) → M i.succ
x y : M 0
⊢ (f : (a : (i : Fin n.succ) → M i) → M₂) (cons (α := M) (x + y) m) =
    HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : Fin n.succ) → M i) → M₂) (cons (α := M) x m) : M₂)
      ((f : (a : (i : Fin n.succ) → M i) → M₂) (cons (α := M) y m) : M₂)

Tactic:
f.toMultilinearMap.cons_add m x y

Premises used: MultilinearMap.cons_add, ContinuousMultilinearMap.toMultilinearMap
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
Goal:
R : Type u
n : ℕ
M : Fin n.succ → Type w
M₂ : Type w₂
inst : Semiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : Fin n.succ) → Module.{u, w} R (M i)
inst_4 : Module R M₂
inst_5 : (i : Fin n.succ) → TopologicalSpace (M i)
inst_6 : TopologicalSpace M₂
f : ContinuousMultilinearMap R M M₂
m : (i : Fin n) → M i.succ
c : R
x : M 0
⊢ (f : (a : (i : Fin n.succ) → M i) → M₂) (cons (α := M) (c • x) m) =
    HSMul.hSMul (β := M₂) c ((f : (a : (i : Fin n.succ) → M i) → M₂) (cons (α := M) x m) : M₂)

Tactic:
f.toMultilinearMap.cons_smul m c x

Premises used: MultilinearMap.cons_smul, ContinuousMultilinearMap.toMultilinearMap
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
Goal:
R : Type u
ι : Type v
M₁ : ι → Type w₁
M₂ : Type w₂
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : ι) → Module.{u, w₁} R (M₁ i)
inst_4 : Module R M₂
inst_5 : (i : ι) → TopologicalSpace (M₁ i)
inst_6 : TopologicalSpace M₂
f : ContinuousMultilinearMap R M₁ M₂
inst_7 : DecidableEq ι
m m' : (i : ι) → M₁ i
t : Finset ι
⊢ Eq.{w₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (t.piecewise (π := M₁) (m + m') m') : M₂)
    (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)

Tactic:
f.toMultilinearMap.map_piecewise_add _ _ _

Premises used: MultilinearMap.map_piecewise_add, ContinuousMultilinearMap.toMultilinearMap