awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_5 : Module R M₂
inst_6 : Module R M₃
inst_7 : DistribSMul S M₂
inst_8 : DistribSMul S M₃
inst_9 : SMulCommClass R S M₂
inst_10 : SMulCommClass R S M₃
inst_11 : CompatibleSMul M₂ M₃ S R
g : M₂ →ₗ[R] M₃
s : S
f : MultilinearMap R M₁ M₂
⊢ g.compMultilinearMap (M₁ := M₁) (s • f) = s • g.compMultilinearMap (M₁ := M₁) f

Tactic:
MultilinearMap.ext fun _ => g.map_smul_of_tower _ _

Premises used: MultilinearMap.ext, LinearMap.map_smul_of_tower, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_5 : Module R M₂
inst_6 : Module R M₃
inst_7 : Monoid S
inst_8 : DistribMulAction S M₃
inst_9 : SMulCommClass R S M₃
g : M₂ →ₗ[R] M₃
s : S
f : MultilinearMap R M₁ M₂
⊢ (s • g).compMultilinearMap (M₁ := M₁) f = s • g.compMultilinearMap (M₁ := M₁) f

Tactic:
rfl

Premises used: LinearMap.compMultilinearMap, rfl
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_4 : Module R M₂
f : MultilinearMap R M₁ M₂
p : Submodule R M₂
h : ∀ (v : (i : ι) → M₁ i), Membership.mem (α := M₂) p ((f : (a : (i : ι) → M₁ i) → M₂) v : M₂)
⊢ p.subtype.compMultilinearMap (M₁ := M₁) (f.codRestrict (M₁ := M₁) p h) = f

Tactic:
rfl

Premises used: LinearMap.compMultilinearMap, rfl
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_5 : Module R M₂
inst_6 : Module R M₃
g : M₂ →ₗ[R] M₃
f : MultilinearMap R M₁ M₂
p : Submodule R M₃
h : ∀ (c : M₂), Membership.mem (α := M₃) p ((g : (a : M₂) → M₃) c : M₃)
⊢ (codRestrict p g h).compMultilinearMap (M₁ := M₁) f = (g.compMultilinearMap (M₁ := M₁) f).codRestrict (M₁ := M₁) p ⋯

Tactic:
rfl

Premises used: MultilinearMap.codRestrict, LinearMap.compMultilinearMap, rfl
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M₂
inst_2 : AddCommMonoid M₃
inst_3 : AddCommMonoid M'
inst_4 : Module R M₂
inst_5 : Module R M₃
inst_6 : Module R M'
ι₁ : Type u_1
ι₂ : Type u_2
σ : ι₁ ≃ ι₂
g : M₂ →ₗ[R] M₃
f : MultilinearMap.{uR, u_1, v', v₂} R (fun (x : ι₁) ↦ M') M₂
H :
  ∀ (x : (i : ι₂) → M'),
    Eq.{v₃ + 1} (α := M₃)
      ((MultilinearMap.domDomCongr σ (g.compMultilinearMap (M₁ := fun (x : ι₁) ↦ M') f) : (a : (i : ι₂) → M') → M₃) x :
        M₃)
      ((g.compMultilinearMap (M₁ := fun (x : ι₂) ↦ M') (MultilinearMap.domDomCongr σ f) : (a : (i : ι₂) → M') → M₃) x :
        M₃)
⊢ MultilinearMap.domDomCongr σ (g.compMultilinearMap (M₁ := fun (x : ι₁) ↦ M') f) =
    g.compMultilinearMap (M₁ := fun (x : ι₂) ↦ M') (MultilinearMap.domDomCongr σ f)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M₂
inst_2 : AddCommMonoid M₃
inst_3 : AddCommMonoid M'
inst_4 : Module R M₂
inst_5 : Module R M₃
inst_6 : Module R M'
ι₁ : Type u_1
ι₂ : Type u_2
σ : ι₁ ≃ ι₂
g : M₂ →ₗ[R] M₃
f : MultilinearMap.{uR, u_1, v', v₂} R (fun (x : ι₁) ↦ M') M₂
x : (i : ι₂) → M'
⊢ Eq.{v₃ + 1} (α := M₃)
    ((MultilinearMap.domDomCongr σ (g.compMultilinearMap (M₁ := fun (x : ι₁) ↦ M') f) : (a : (i : ι₂) → M') → M₃) x :
      M₃)
    ((g.compMultilinearMap (M₁ := fun (x : ι₂) ↦ M') (MultilinearMap.domDomCongr σ f) : (a : (i : ι₂) → M') → M₃) x :
      M₃)

Tactic:
simp [MultilinearMap.domDomCongr]

Premises used: MultilinearMap.domDomCongr
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
inst_5 : Semiring S
inst_6 : Module S M₂
inst_7 : SMulCommClass R S M₂
inst_8 : Module.IsTorsionFree S M₂
⊢ Module.IsTorsionFree S (MultilinearMap R M₁ M₂)

Tactic:
coe_injective.moduleIsTorsionFree _ coe_smul

Premises used: MultilinearMap.coe_smul, Function.Injective.moduleIsTorsionFree, MultilinearMap.coe_injective
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
inst_5 : Semiring S
inst_6 : Module S M₂
inst_7 : SMulCommClass R S M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module S M₃
inst_10 : Module R M₃
inst_11 : SMulCommClass R S M₃
inst_12 : LinearMap.CompatibleSMul M₂ M₃ S R
inst_13 : LinearMap.CompatibleSMul M₃ M₂ S R
g : M₂ ≃ₗ[R] M₃
x : MultilinearMap R M₁ M₂
H :
  ∀ (x_1 : (i : ι) → M₁ i),
    Eq.{v₂ + 1} (α := M₂)
      ((((LinearMap.compMultilinearMapₗ S (M₁ := M₁) (↑g.symm : M₃ →ₗ[R] M₂) :
                  (a : MultilinearMap R M₁ M₃) → MultilinearMap R M₁ M₂)
                (AddHom.toFun (LinearMap.toAddHom (LinearMap.compMultilinearMapₗ S (M₁ := M₁) (↑g : M₂ →ₗ[R] M₃))) x) :
              MultilinearMap R M₁ M₂) :
            (a : (i : ι) → M₁ i) → M₂)
          x_1 :
        M₂)
      ((x : (a : (i : ι) → M₁ i) → M₂) x_1 : M₂)
⊢ (LinearMap.compMultilinearMapₗ S (M₁ := M₁) (↑g.symm : M₃ →ₗ[R] M₂) :
        (a : MultilinearMap R M₁ M₃) → MultilinearMap R M₁ M₂)
      (AddHom.toFun (LinearMap.toAddHom (LinearMap.compMultilinearMapₗ S (M₁ := M₁) (↑g : M₂ →ₗ[R] M₃))) x) =
    x

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
inst_5 : Semiring S
inst_6 : Module S M₂
inst_7 : SMulCommClass R S M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module S M₃
inst_10 : Module R M₃
inst_11 : SMulCommClass R S M₃
inst_12 : LinearMap.CompatibleSMul M₂ M₃ S R
inst_13 : LinearMap.CompatibleSMul M₃ M₂ S R
g : M₂ ≃ₗ[R] M₃
x : MultilinearMap R M₁ M₂
x_1 : (i : ι) → M₁ i
⊢ Eq.{v₂ + 1} (α := M₂)
    ((((LinearMap.compMultilinearMapₗ S (M₁ := M₁) (↑g.symm : M₃ →ₗ[R] M₂) :
                (a : MultilinearMap R M₁ M₃) → MultilinearMap R M₁ M₂)
              (AddHom.toFun (LinearMap.toAddHom (LinearMap.compMultilinearMapₗ S (M₁ := M₁) (↑g : M₂ →ₗ[R] M₃))) x) :
            MultilinearMap R M₁ M₂) :
          (a : (i : ι) → M₁ i) → M₂)
        x_1 :
      M₂)
    ((x : (a : (i : ι) → M₁ i) → M₂) x_1 : M₂)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
inst_5 : Semiring S
inst_6 : Module S M₂
inst_7 : SMulCommClass R S M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module S M₃
inst_10 : Module R M₃
inst_11 : SMulCommClass R S M₃
inst_12 : LinearMap.CompatibleSMul M₂ M₃ S R
inst_13 : LinearMap.CompatibleSMul M₃ M₂ S R
g : M₂ ≃ₗ[R] M₃
x : MultilinearMap R M₁ M₃
H :
  ∀ (x_1 : (i : ι) → M₁ i),
    Eq.{v₃ + 1} (α := M₃)
      ((AddHom.toFun (LinearMap.toAddHom (LinearMap.compMultilinearMapₗ S (M₁ := M₁) (↑g : M₂ →ₗ[R] M₃)))
              ((LinearMap.compMultilinearMapₗ S (M₁ := M₁) (↑g.symm : M₃ →ₗ[R] M₂) :
                  (a : MultilinearMap R M₁ M₃) → MultilinearMap R M₁ M₂)
                x) :
            (a : (i : ι) → M₁ i) → M₃)
          x_1 :
        M₃)
      ((x : (a : (i : ι) → M₁ i) → M₃) x_1 : M₃)
⊢ AddHom.toFun (LinearMap.toAddHom (LinearMap.compMultilinearMapₗ S (M₁ := M₁) (↑g : M₂ →ₗ[R] M₃)))
      ((LinearMap.compMultilinearMapₗ S (M₁ := M₁) (↑g.symm : M₃ →ₗ[R] M₂) :
          (a : MultilinearMap R M₁ M₃) → MultilinearMap R M₁ M₂)
        x) =
    x

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
inst_5 : Semiring S
inst_6 : Module S M₂
inst_7 : SMulCommClass R S M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module S M₃
inst_10 : Module R M₃
inst_11 : SMulCommClass R S M₃
inst_12 : LinearMap.CompatibleSMul M₂ M₃ S R
inst_13 : LinearMap.CompatibleSMul M₃ M₂ S R
g : M₂ ≃ₗ[R] M₃
x : MultilinearMap R M₁ M₃
x_1 : (i : ι) → M₁ i
⊢ Eq.{v₃ + 1} (α := M₃)
    ((AddHom.toFun (LinearMap.toAddHom (LinearMap.compMultilinearMapₗ S (M₁ := M₁) (↑g : M₂ →ₗ[R] M₃)))
            ((LinearMap.compMultilinearMapₗ S (M₁ := M₁) (↑g.symm : M₃ →ₗ[R] M₂) :
                (a : MultilinearMap R M₁ M₃) → MultilinearMap R M₁ M₂)
              x) :
          (a : (i : ι) → M₁ i) → M₃)
        x_1 :
      M₃)
    ((x : (a : (i : ι) → M₁ i) → M₃) x_1 : M₃)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
inst_5 : Semiring S
inst_6 : Module S M₂
inst_7 : SMulCommClass R S M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module S M₃
inst_10 : Module R M₃
inst_11 : SMulCommClass R S M₃
ι' : Type u_1
σ : ι ≃ ι'
f : MultilinearMap R M₁ M₂
inst_12 : DecidableEq ι'
m : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)
i : ι'
this : DecidableEq ι := σ.decidableEq
rw :
  ∀ (x y : M₁ ((σ.symm : (a : ι') → ι) ((σ : (a : ι) → ι') ((σ.symm : (a : ι') → ι) i : ι) : ι'))),
    comp (β := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂)
        (⇑(Equiv.piCongrLeft' M₁ σ).symm : (a : (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b)) → (a : ι) → M₁ a)
        (update (β := fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) m
          ((σ : (a : ι) → ι') ((σ.symm : (a : ι') → ι) i : ι)) (x + y)) =
      HAdd.hAdd (α := M₂)
        (comp (β := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂)
          (⇑(Equiv.piCongrLeft' M₁ σ).symm : (a : (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b)) → (a : ι) → M₁ a)
          (update (β := fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) m
            ((σ : (a : ι) → ι') ((σ.symm : (a : ι') → ι) i : ι)) x))
        (comp (β := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂)
          (⇑(Equiv.piCongrLeft' M₁ σ).symm : (a : (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b)) → (a : ι) → M₁ a)
          (update (β := fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) m
            ((σ : (a : ι) → ι') ((σ.symm : (a : ι') → ι) i : ι)) y))
⊢ ∀ (x y : M₁ ((σ.symm : (a : ι') → ι) i)),
    comp (β := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂)
        (⇑(Equiv.piCongrLeft' M₁ σ).symm : (a : (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b)) → (a : ι) → M₁ a)
        (update (β := fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) m i (x + y)) =
      HAdd.hAdd (α := M₂)
        (comp (β := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂)
          (⇑(Equiv.piCongrLeft' M₁ σ).symm : (a : (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b)) → (a : ι) → M₁ a)
          (update (β := fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) m i x))
        (comp (β := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂)
          (⇑(Equiv.piCongrLeft' M₁ σ).symm : (a : (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b)) → (a : ι) → M₁ a)
          (update (β := fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) m i y))

Tactic:
rw [← σ.apply_symm_apply i]

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
inst_5 : Semiring S
inst_6 : Module S M₂
inst_7 : SMulCommClass R S M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module S M₃
inst_10 : Module R M₃
inst_11 : SMulCommClass R S M₃
ι' : Type u_1
σ : ι ≃ ι'
f : MultilinearMap R M₁ M₂
inst_12 : DecidableEq ι'
m : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)
i : ι'
this : DecidableEq ι := σ.decidableEq
x y : M₁ ((σ.symm : (a : ι') → ι) ((σ : (a : ι) → ι') ((σ.symm : (a : ι') → ι) i : ι) : ι'))
⊢ comp (β := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂)
      (⇑(Equiv.piCongrLeft' M₁ σ).symm : (a : (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b)) → (a : ι) → M₁ a)
      (update (β := fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) m
        ((σ : (a : ι) → ι') ((σ.symm : (a : ι') → ι) i : ι)) (x + y)) =
    HAdd.hAdd (α := M₂)
      (comp (β := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂)
        (⇑(Equiv.piCongrLeft' M₁ σ).symm : (a : (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b)) → (a : ι) → M₁ a)
        (update (β := fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) m
          ((σ : (a : ι) → ι') ((σ.symm : (a : ι') → ι) i : ι)) x))
      (comp (β := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂)
        (⇑(Equiv.piCongrLeft' M₁ σ).symm : (a : (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b)) → (a : ι) → M₁ a)
        (update (β := fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) m
          ((σ : (a : ι) → ι') ((σ.symm : (a : ι') → ι) i : ι)) y))

Tactic:
simp only [comp_apply, piCongrLeft'_symm_update, f.map_update_add]

Premises used: MultilinearMap.map_update_add, Function.piCongrLeft'_symm_update, Function.comp_apply
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
inst_5 : Semiring S
inst_6 : Module S M₂
inst_7 : SMulCommClass R S M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module S M₃
inst_10 : Module R M₃
inst_11 : SMulCommClass R S M₃
ι' : Type u_1
σ : ι ≃ ι'
f : MultilinearMap R M₁ M₂
inst_12 : DecidableEq ι'
m : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)
i : ι'
c : R
this : DecidableEq ι := σ.decidableEq
rw :
  ∀ (x : M₁ ((σ.symm : (a : ι') → ι) ((σ : (a : ι) → ι') ((σ.symm : (a : ι') → ι) i : ι) : ι'))),
    comp (β := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂)
        (⇑(Equiv.piCongrLeft' M₁ σ).symm : (a : (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b)) → (a : ι) → M₁ a)
        (update (β := fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) m
          ((σ : (a : ι) → ι') ((σ.symm : (a : ι') → ι) i : ι)) (c • x)) =
      HSMul.hSMul (β := M₂) c
        (comp (β := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂)
          (⇑(Equiv.piCongrLeft' M₁ σ).symm : (a : (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b)) → (a : ι) → M₁ a)
          (update (β := fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) m
            ((σ : (a : ι) → ι') ((σ.symm : (a : ι') → ι) i : ι)) x))
⊢ ∀ (x : M₁ ((σ.symm : (a : ι') → ι) i)),
    comp (β := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂)
        (⇑(Equiv.piCongrLeft' M₁ σ).symm : (a : (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b)) → (a : ι) → M₁ a)
        (update (β := fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) m i (c • x)) =
      HSMul.hSMul (β := M₂) c
        (comp (β := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂)
          (⇑(Equiv.piCongrLeft' M₁ σ).symm : (a : (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b)) → (a : ι) → M₁ a)
          (update (β := fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) m i x))

Tactic:
rw [← σ.apply_symm_apply i]

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
inst_5 : Semiring S
inst_6 : Module S M₂
inst_7 : SMulCommClass R S M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module S M₃
inst_10 : Module R M₃
inst_11 : SMulCommClass R S M₃
ι' : Type u_1
σ : ι ≃ ι'
f : MultilinearMap R M₁ M₂
inst_12 : DecidableEq ι'
m : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)
i : ι'
c : R
this : DecidableEq ι := σ.decidableEq
x : M₁ ((σ.symm : (a : ι') → ι) ((σ : (a : ι) → ι') ((σ.symm : (a : ι') → ι) i : ι) : ι'))
⊢ comp (β := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂)
      (⇑(Equiv.piCongrLeft' M₁ σ).symm : (a : (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b)) → (a : ι) → M₁ a)
      (update (β := fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) m
        ((σ : (a : ι) → ι') ((σ.symm : (a : ι') → ι) i : ι)) (c • x)) =
    HSMul.hSMul (β := M₂) c
      (comp (β := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂)
        (⇑(Equiv.piCongrLeft' M₁ σ).symm : (a : (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b)) → (a : ι) → M₁ a)
        (update (β := fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) m
          ((σ : (a : ι) → ι') ((σ.symm : (a : ι') → ι) i : ι)) x))

Tactic:
simp only [Function.comp, piCongrLeft'_symm_update, f.map_update_smul]

Premises used: MultilinearMap.map_update_smul, Function.piCongrLeft'_symm_update, Function.comp
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
inst_5 : Semiring S
inst_6 : Module S M₂
inst_7 : SMulCommClass R S M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module S M₃
inst_10 : Module R M₃
inst_11 : SMulCommClass R S M₃
ι' : Type u_1
σ : ι ≃ ι'
f₁ f₂ : MultilinearMap R M₁ M₂
H :
  ∀ (x : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)),
    Eq.{v₂ + 1} (α := M₂)
      ((mk (M₁ := fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i))
              (comp (β := (i : ι) → M₁ i) (⇑(f₁ + f₂) : (a : (i : ι) → M₁ i) → M₂)
                (⇑(Equiv.piCongrLeft' M₁ σ).symm : (a : (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b)) → (a : ι) → M₁ a))
              ⋯ ⋯ :
            (a : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) → M₂)
          x :
        M₂)
      ((HAdd.hAdd (α := MultilinearMap.{uR, u_1, v₁, v₂} R (fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) M₂)
              (mk (M₁ := fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i))
                (comp (β := (i : ι) → M₁ i) (⇑f₁ : (a : (i : ι) → M₁ i) → M₂)
                  (⇑(Equiv.piCongrLeft' M₁ σ).symm : (a : (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b)) → (a : ι) → M₁ a))
                ⋯ ⋯)
              (mk (M₁ := fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i))
                (comp (β := (i : ι) → M₁ i) (⇑f₂ : (a : (i : ι) → M₁ i) → M₂)
                  (⇑(Equiv.piCongrLeft' M₁ σ).symm : (a : (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b)) → (a : ι) → M₁ a))
                ⋯ ⋯) :
            (a : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) → M₂)
          x :
        M₂)
⊢ mk (M₁ := fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i))
      (comp (β := (i : ι) → M₁ i) (⇑(f₁ + f₂) : (a : (i : ι) → M₁ i) → M₂)
        (⇑(Equiv.piCongrLeft' M₁ σ).symm : (a : (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b)) → (a : ι) → M₁ a))
      ⋯ ⋯ =
    HAdd.hAdd (α := MultilinearMap.{uR, u_1, v₁, v₂} R (fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) M₂)
      (mk (M₁ := fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i))
        (comp (β := (i : ι) → M₁ i) (⇑f₁ : (a : (i : ι) → M₁ i) → M₂)
          (⇑(Equiv.piCongrLeft' M₁ σ).symm : (a : (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b)) → (a : ι) → M₁ a))
        ⋯ ⋯)
      (mk (M₁ := fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i))
        (comp (β := (i : ι) → M₁ i) (⇑f₂ : (a : (i : ι) → M₁ i) → M₂)
          (⇑(Equiv.piCongrLeft' M₁ σ).symm : (a : (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b)) → (a : ι) → M₁ a))
        ⋯ ⋯)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
inst_5 : Semiring S
inst_6 : Module S M₂
inst_7 : SMulCommClass R S M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module S M₃
inst_10 : Module R M₃
inst_11 : SMulCommClass R S M₃
ι' : Type u_1
σ : ι ≃ ι'
f₁ f₂ : MultilinearMap R M₁ M₂
x : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)
⊢ Eq.{v₂ + 1} (α := M₂)
    ((mk (M₁ := fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i))
            (comp (β := (i : ι) → M₁ i) (⇑(f₁ + f₂) : (a : (i : ι) → M₁ i) → M₂)
              (⇑(Equiv.piCongrLeft' M₁ σ).symm : (a : (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b)) → (a : ι) → M₁ a))
            ⋯ ⋯ :
          (a : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) → M₂)
        x :
      M₂)
    ((HAdd.hAdd (α := MultilinearMap.{uR, u_1, v₁, v₂} R (fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) M₂)
            (mk (M₁ := fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i))
              (comp (β := (i : ι) → M₁ i) (⇑f₁ : (a : (i : ι) → M₁ i) → M₂)
                (⇑(Equiv.piCongrLeft' M₁ σ).symm : (a : (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b)) → (a : ι) → M₁ a))
              ⋯ ⋯)
            (mk (M₁ := fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i))
              (comp (β := (i : ι) → M₁ i) (⇑f₂ : (a : (i : ι) → M₁ i) → M₂)
                (⇑(Equiv.piCongrLeft' M₁ σ).symm : (a : (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b)) → (a : ι) → M₁ a))
              ⋯ ⋯) :
          (a : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) → M₂)
        x :
      M₂)

Tactic:
simp only [Function.comp, coe_mk, add_apply]

Premises used: MultilinearMap.add_apply, Function.comp, MultilinearMap.coe_mk