awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
σ : ι ≃ ι'
c : S
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) (⇑(c • 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₂)
      ((HSMul.hSMul (α := S) (β :=
              MultilinearMap.{uR, u_1, v₁, v₂} R (fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) M₂)
              ((RingHom.id S : (a : S) → S) c : S)
              (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) (⇑(c • f) : (a : (i : ι) → M₁ i) → M₂)
        (⇑(Equiv.piCongrLeft' M₁ σ).symm : (a : (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b)) → (a : ι) → M₁ a))
      ⋯ ⋯ =
    HSMul.hSMul (α := S) (β := MultilinearMap.{uR, u_1, v₁, v₂} R (fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) M₂)
      ((RingHom.id S : (a : S) → S) c : S)
      (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
σ : ι ≃ ι'
c : S
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) (⇑(c • 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₂)
    ((HSMul.hSMul (α := S) (β := MultilinearMap.{uR, u_1, v₁, v₂} R (fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) M₂)
            ((RingHom.id S : (a : S) → S) c : S)
            (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, smul_apply, RingHom.id_apply]

Premises used: MultilinearMap.smul_apply, RingHom.id_apply, Function.comp, MultilinearMap.coe_mk
-- 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.{uR, u_1, v₁, v₂} R (fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) M₂
inst_12 : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
this : DecidableEq ι' := σ.symm.decidableEq
rw :
  ∀ (x y : M₁ ((σ.symm : (a : ι') → ι) ((σ : (a : ι) → ι') i : ι'))),
    comp (β := (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) (⇑f : (a : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) → M₂)
        (⇑(Equiv.piCongrLeft' M₁ σ) : (a : (a : ι) → M₁ a) → (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b))
        (update (β := M₁) m ((σ.symm : (a : ι') → ι) ((σ : (a : ι) → ι') i : ι')) (x + y)) =
      HAdd.hAdd (α := M₂)
        (comp (β := (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i))
          (⇑f : (a : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) → M₂)
          (⇑(Equiv.piCongrLeft' M₁ σ) : (a : (a : ι) → M₁ a) → (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b))
          (update (β := M₁) m ((σ.symm : (a : ι') → ι) ((σ : (a : ι) → ι') i : ι')) x))
        (comp (β := (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i))
          (⇑f : (a : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) → M₂)
          (⇑(Equiv.piCongrLeft' M₁ σ) : (a : (a : ι) → M₁ a) → (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b))
          (update (β := M₁) m ((σ.symm : (a : ι') → ι) ((σ : (a : ι) → ι') i : ι')) y))
⊢ ∀ (x y : M₁ i),
    comp (β := (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) (⇑f : (a : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) → M₂)
        (⇑(Equiv.piCongrLeft' M₁ σ) : (a : (a : ι) → M₁ a) → (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b))
        (update (β := M₁) m i (x + y)) =
      HAdd.hAdd (α := M₂)
        (comp (β := (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i))
          (⇑f : (a : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) → M₂)
          (⇑(Equiv.piCongrLeft' M₁ σ) : (a : (a : ι) → M₁ a) → (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b))
          (update (β := M₁) m i x))
        (comp (β := (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i))
          (⇑f : (a : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) → M₂)
          (⇑(Equiv.piCongrLeft' M₁ σ) : (a : (a : ι) → M₁ a) → (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b))
          (update (β := M₁) m i y))

Tactic:
rw [← σ.symm_apply_apply i]

Premises used: Equiv.symm_apply_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.{uR, u_1, v₁, v₂} R (fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) M₂
inst_12 : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
this : DecidableEq ι' := σ.symm.decidableEq
x y : M₁ ((σ.symm : (a : ι') → ι) ((σ : (a : ι) → ι') i : ι'))
⊢ comp (β := (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) (⇑f : (a : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) → M₂)
      (⇑(Equiv.piCongrLeft' M₁ σ) : (a : (a : ι) → M₁ a) → (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b))
      (update (β := M₁) m ((σ.symm : (a : ι') → ι) ((σ : (a : ι) → ι') i : ι')) (x + y)) =
    HAdd.hAdd (α := M₂)
      (comp (β := (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) (⇑f : (a : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) → M₂)
        (⇑(Equiv.piCongrLeft' M₁ σ) : (a : (a : ι) → M₁ a) → (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b))
        (update (β := M₁) m ((σ.symm : (a : ι') → ι) ((σ : (a : ι) → ι') i : ι')) x))
      (comp (β := (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) (⇑f : (a : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) → M₂)
        (⇑(Equiv.piCongrLeft' M₁ σ) : (a : (a : ι) → M₁ a) → (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b))
        (update (β := M₁) m ((σ.symm : (a : ι') → ι) ((σ : (a : ι) → ι') i : ι')) y))

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

Premises used: MultilinearMap.map_update_add, Function.piCongrLeft'_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.{uR, u_1, v₁, v₂} R (fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) M₂
inst_12 : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
c : R
this : DecidableEq ι' := σ.symm.decidableEq
rw :
  ∀ (x : M₁ ((σ.symm : (a : ι') → ι) ((σ : (a : ι) → ι') i : ι'))),
    comp (β := (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) (⇑f : (a : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) → M₂)
        (⇑(Equiv.piCongrLeft' M₁ σ) : (a : (a : ι) → M₁ a) → (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b))
        (update (β := M₁) m ((σ.symm : (a : ι') → ι) ((σ : (a : ι) → ι') i : ι')) (c • x)) =
      HSMul.hSMul (β := M₂) c
        (comp (β := (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i))
          (⇑f : (a : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) → M₂)
          (⇑(Equiv.piCongrLeft' M₁ σ) : (a : (a : ι) → M₁ a) → (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b))
          (update (β := M₁) m ((σ.symm : (a : ι') → ι) ((σ : (a : ι) → ι') i : ι')) x))
⊢ ∀ (x : M₁ i),
    comp (β := (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) (⇑f : (a : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) → M₂)
        (⇑(Equiv.piCongrLeft' M₁ σ) : (a : (a : ι) → M₁ a) → (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b))
        (update (β := M₁) m i (c • x)) =
      HSMul.hSMul (β := M₂) c
        (comp (β := (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i))
          (⇑f : (a : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) → M₂)
          (⇑(Equiv.piCongrLeft' M₁ σ) : (a : (a : ι) → M₁ a) → (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b))
          (update (β := M₁) m i x))

Tactic:
rw [← σ.symm_apply_apply i]

Premises used: Equiv.symm_apply_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.{uR, u_1, v₁, v₂} R (fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) M₂
inst_12 : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
c : R
this : DecidableEq ι' := σ.symm.decidableEq
x : M₁ ((σ.symm : (a : ι') → ι) ((σ : (a : ι) → ι') i : ι'))
⊢ comp (β := (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) (⇑f : (a : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) → M₂)
      (⇑(Equiv.piCongrLeft' M₁ σ) : (a : (a : ι) → M₁ a) → (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b))
      (update (β := M₁) m ((σ.symm : (a : ι') → ι) ((σ : (a : ι) → ι') i : ι')) (c • x)) =
    HSMul.hSMul (β := M₂) c
      (comp (β := (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) (⇑f : (a : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) → M₂)
        (⇑(Equiv.piCongrLeft' M₁ σ) : (a : (a : ι) → M₁ a) → (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b))
        (update (β := M₁) m ((σ.symm : (a : ι') → ι) ((σ : (a : ι) → ι') i : ι')) x))

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

Premises used: MultilinearMap.map_update_smul, Function.comp, Function.piCongrLeft'_update
-- 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₂
H :
  ∀ (x : (i : ι) → M₁ i),
    Eq.{v₂ + 1} (α := M₂)
      (((fun (f : MultilinearMap.{uR, u_1, v₁, v₂} R (fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) M₂) ↦
                (mk (M₁ := M₁)
                    (comp (β := (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i))
                      (⇑f : (a : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) → M₂)
                      (⇑(Equiv.piCongrLeft' M₁ σ) : (a : (a : ι) → M₁ a) → (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b)))
                    ⋯ ⋯ :
                  MultilinearMap R M₁ M₂))
              ((fun (f : MultilinearMap R M₁ 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))
                      ⋯ ⋯ :
                    MultilinearMap.{uR, u_1, v₁, v₂} R (fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) M₂))
                f) :
            (a : (i : ι) → M₁ i) → M₂)
          x :
        M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂)
⊢ (fun (f : MultilinearMap.{uR, u_1, v₁, v₂} R (fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) M₂) ↦
        (mk (M₁ := M₁)
            (comp (β := (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i))
              (⇑f : (a : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) → M₂)
              (⇑(Equiv.piCongrLeft' M₁ σ) : (a : (a : ι) → M₁ a) → (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b)))
            ⋯ ⋯ :
          MultilinearMap R M₁ M₂))
      ((fun (f : MultilinearMap R M₁ 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))
              ⋯ ⋯ :
            MultilinearMap.{uR, u_1, v₁, v₂} R (fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) M₂))
        f) =
    f

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 : MultilinearMap R M₁ M₂
x : (i : ι) → M₁ i
⊢ Eq.{v₂ + 1} (α := M₂)
    (((fun (f : MultilinearMap.{uR, u_1, v₁, v₂} R (fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) M₂) ↦
              (mk (M₁ := M₁)
                  (comp (β := (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i))
                    (⇑f : (a : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) → M₂)
                    (⇑(Equiv.piCongrLeft' M₁ σ) : (a : (a : ι) → M₁ a) → (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b)))
                  ⋯ ⋯ :
                MultilinearMap R M₁ M₂))
            ((fun (f : MultilinearMap R M₁ 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))
                    ⋯ ⋯ :
                  MultilinearMap.{uR, u_1, v₁, v₂} R (fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) M₂))
              f) :
          (a : (i : ι) → M₁ i) → M₂)
        x :
      M₂)
    ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂)

Tactic:
simp only [coe_mk, comp_apply, Equiv.symm_apply_apply]

Premises used: Equiv.symm_apply_apply, MultilinearMap.coe_mk, 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.{uR, u_1, v₁, v₂} R (fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) M₂
H :
  ∀ (x : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)),
    Eq.{v₂ + 1} (α := M₂)
      (((fun (f : MultilinearMap R M₁ 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))
                    ⋯ ⋯ :
                  MultilinearMap.{uR, u_1, v₁, v₂} R (fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) M₂))
              ((fun (f : MultilinearMap.{uR, u_1, v₁, v₂} R (fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) M₂) ↦
                  (mk (M₁ := M₁)
                      (comp (β := (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i))
                        (⇑f : (a : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) → M₂)
                        (⇑(Equiv.piCongrLeft' M₁ σ) : (a : (a : ι) → M₁ a) → (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b)))
                      ⋯ ⋯ :
                    MultilinearMap R M₁ M₂))
                f) :
            (a : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) → M₂)
          x :
        M₂)
      ((f : (a : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) → M₂) x : M₂)
⊢ (fun (f : MultilinearMap R M₁ 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))
            ⋯ ⋯ :
          MultilinearMap.{uR, u_1, v₁, v₂} R (fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) M₂))
      ((fun (f : MultilinearMap.{uR, u_1, v₁, v₂} R (fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) M₂) ↦
          (mk (M₁ := M₁)
              (comp (β := (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i))
                (⇑f : (a : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) → M₂)
                (⇑(Equiv.piCongrLeft' M₁ σ) : (a : (a : ι) → M₁ a) → (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b)))
              ⋯ ⋯ :
            MultilinearMap R M₁ M₂))
        f) =
    f

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 : MultilinearMap.{uR, u_1, v₁, v₂} R (fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) M₂
x : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)
⊢ Eq.{v₂ + 1} (α := M₂)
    (((fun (f : MultilinearMap R M₁ 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))
                  ⋯ ⋯ :
                MultilinearMap.{uR, u_1, v₁, v₂} R (fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) M₂))
            ((fun (f : MultilinearMap.{uR, u_1, v₁, v₂} R (fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) M₂) ↦
                (mk (M₁ := M₁)
                    (comp (β := (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i))
                      (⇑f : (a : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) → M₂)
                      (⇑(Equiv.piCongrLeft' M₁ σ) : (a : (a : ι) → M₁ a) → (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b)))
                    ⋯ ⋯ :
                  MultilinearMap R M₁ M₂))
              f) :
          (a : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) → M₂)
        x :
      M₂)
    ((f : (a : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) → M₂) x : M₂)

Tactic:
simp only [coe_mk, comp_apply, Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply, MultilinearMap.coe_mk, 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
ι₂ : Type u_2
σ : ι₁ ≃ ι₂
c : S
f : MultilinearMap.{uR, u_1, v₂, v₃} R (fun (x : ι₁) ↦ M₂) M₃
H :
  ∀ (x : (i : ι₂) → M₂),
    Eq.{v₃ + 1} (α := M₃)
      ((Equiv.toFun (AddEquiv.toEquiv (domDomCongrEquiv σ)) (c • f) : (a : (i : ι₂) → M₂) → M₃) x : M₃)
      ((HSMul.hSMul (α := S) ((RingHom.id S : (a : S) → S) c : S)
              (Equiv.toFun (AddEquiv.toEquiv (domDomCongrEquiv σ)) f) :
            (a : (i : ι₂) → M₂) → M₃)
          x :
        M₃)
⊢ Equiv.toFun (AddEquiv.toEquiv (domDomCongrEquiv σ)) (c • f) =
    HSMul.hSMul (α := S) ((RingHom.id S : (a : S) → S) c : S) (Equiv.toFun (AddEquiv.toEquiv (domDomCongrEquiv σ)) f)

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
ι₂ : Type u_2
σ : ι₁ ≃ ι₂
c : S
f : MultilinearMap.{uR, u_1, v₂, v₃} R (fun (x : ι₁) ↦ M₂) M₃
x : (i : ι₂) → M₂
⊢ Eq.{v₃ + 1} (α := M₃)
    ((Equiv.toFun (AddEquiv.toEquiv (domDomCongrEquiv σ)) (c • f) : (a : (i : ι₂) → M₂) → M₃) x : M₃)
    ((HSMul.hSMul (α := S) ((RingHom.id S : (a : S) → S) c : S)
            (Equiv.toFun (AddEquiv.toEquiv (domDomCongrEquiv σ)) f) :
          (a : (i : ι₂) → M₂) → M₃)
        x :
      M₃)

Tactic:
simp [MultilinearMap.domDomCongr]

Premises used: MultilinearMap.domDomCongr