awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.TensorPower.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
x : GradedMonoid fun (i : ℕ) ↦ ⨂[R]^i M
this :
  Eq (α := ⨂[R]^(x.fst (β := fun (i : ℕ) ↦ ⨂[R]^i M)) M)
    ((cast R M ⋯ : (a : ⨂[R]^(0 + x.fst) M) → ⨂[R]^x.fst M)
        (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ 0 (x.fst (β := fun (i : ℕ) ↦ ⨂[R]^i M))
          ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r) (x.snd (β := fun (i : ℕ) ↦ ⨂[R]^i M))) :
      ⨂[R]^(x.fst (β := fun (i : ℕ) ↦ ⨂[R]^i M)) M)
    ((cast R M ⋯ : (a : ⨂[R]^(x.fst + 0) M) → ⨂[R]^x.fst M)
        (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ (x.fst (β := fun (i : ℕ) ↦ ⨂[R]^i M)) 0
          (x.snd (β := fun (i : ℕ) ↦ ⨂[R]^i M)) ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r)) :
      ⨂[R]^(x.fst (β := fun (i : ℕ) ↦ ⨂[R]^i M)) M)
⊢ Eq (α := ⨂[R]^(0 + x.fst (β := fun (i : ℕ) ↦ ⨂[R]^i M)) M)
    (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ 0 (x.fst (β := fun (i : ℕ) ↦ ⨂[R]^i M))
        ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r) (x.snd (β := fun (i : ℕ) ↦ ⨂[R]^i M)) :
      ⨂[R]^(0 + x.fst (β := fun (i : ℕ) ↦ ⨂[R]^i M)) M)
    ((cast R M ⋯ : (a : ⨂[R]^(x.fst + 0) M) → ⨂[R]^(0 + x.fst) M)
        (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ (x.fst (β := fun (i : ℕ) ↦ ⨂[R]^i M)) 0
          (x.snd (β := fun (i : ℕ) ↦ ⨂[R]^i M)) ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r)) :
      ⨂[R]^(0 + x.fst (β := fun (i : ℕ) ↦ ⨂[R]^i M)) M)

Tactic:
rw [← LinearEquiv.eq_symm_apply, cast_symm, cast_cast] at this

Premises used: TensorPower.cast_cast, LinearEquiv.eq_symm_apply, TensorPower.cast_symm
-- Module: Mathlib.LinearAlgebra.TensorPower.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
x : GradedMonoid fun (i : ℕ) ↦ ⨂[R]^i M
this :
  Eq (α := ⨂[R]^(0 + x.fst (β := fun (i : ℕ) ↦ ⨂[R]^i M)) M)
    (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ 0 (x.fst (β := fun (i : ℕ) ↦ ⨂[R]^i M))
        ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r) (x.snd (β := fun (i : ℕ) ↦ ⨂[R]^i M)) :
      ⨂[R]^(0 + x.fst (β := fun (i : ℕ) ↦ ⨂[R]^i M)) M)
    ((cast R M ⋯ : (a : ⨂[R]^(x.fst + 0) M) → ⨂[R]^(0 + x.fst) M)
        (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ (x.fst (β := fun (i : ℕ) ↦ ⨂[R]^i M)) 0
          (x.snd (β := fun (i : ℕ) ↦ ⨂[R]^i M)) ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r)) :
      ⨂[R]^(0 + x.fst (β := fun (i : ℕ) ↦ ⨂[R]^i M)) M)
⊢ (GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) 0
            ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) r) *
          x).snd
      (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M) =
    (cast R M ⋯ :
        (a :
            ⨂[R]^(x * GradedMonoid.mk 0 (((↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M).toAddMonoidHom : (a : R) → ⨂[R]^0 M) r)).fst
              M) →
          ⨂[R]^(GradedMonoid.mk 0 (((↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M).toAddMonoidHom : (a : R) → ⨂[R]^0 M) r) * x).fst
            M)
      ((x *
            GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) 0
              ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) r)).snd
        (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M))

Tactic:
this
-- Module: Mathlib.LinearAlgebra.TensorPower.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
x : GradedMonoid fun (i : ℕ) ↦ ⨂[R]^i M
this :
  Eq (α := ⨂[R]^(0 + x.fst (β := fun (i : ℕ) ↦ ⨂[R]^i M)) M)
    (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ 0 (x.fst (β := fun (i : ℕ) ↦ ⨂[R]^i M))
        ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r) (x.snd (β := fun (i : ℕ) ↦ ⨂[R]^i M)) :
      ⨂[R]^(0 + x.fst (β := fun (i : ℕ) ↦ ⨂[R]^i M)) M)
    ((cast R M ⋯ : (a : ⨂[R]^(x.fst + 0) M) → ⨂[R]^(0 + x.fst) M)
        (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ (x.fst (β := fun (i : ℕ) ↦ ⨂[R]^i M)) 0
          (x.snd (β := fun (i : ℕ) ↦ ⨂[R]^i M)) ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r)) :
      ⨂[R]^(0 + x.fst (β := fun (i : ℕ) ↦ ⨂[R]^i M)) M)
⊢ (GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) 0
            ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) r) *
          x).snd
      (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M) =
    (cast R M ⋯ :
        (a :
            ⨂[R]^(x * GradedMonoid.mk 0 (((↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M).toAddMonoidHom : (a : R) → ⨂[R]^0 M) r)).fst
              M) →
          ⨂[R]^(GradedMonoid.mk 0 (((↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M).toAddMonoidHom : (a : R) → ⨂[R]^0 M) r) * x).fst
            M)
      ((x *
            GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) 0
              ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) r)).snd
        (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M))

Tactic:
exact this
-- Module: Mathlib.LinearAlgebra.TensorPower.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
x : GradedMonoid fun (i : ℕ) ↦ ⨂[R]^i M
rw :
  (r • x).snd (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M) =
    (cast R M ⋯ :
        (a :
            ⨂[R]^(GradedMonoid.mk 0 (((↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M).toAddMonoidHom : (a : R) → ⨂[R]^0 M) r) * x).fst
              M) →
          ⨂[R]^(r • x).fst M)
      ((GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) 0
              ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) r) *
            x).snd
        (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M))
⊢ (cast R M ⋯ :
        (a : ⨂[R]^(r • x).fst M) →
          ⨂[R]^(GradedMonoid.mk 0 (((↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M).toAddMonoidHom : (a : R) → ⨂[R]^0 M) r) * x).fst
            M)
      ((r • x).snd (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)) =
    (GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) 0
            ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) r) *
          x).snd
      (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)

Tactic:
rw [← LinearEquiv.eq_symm_apply, cast_symm]

Premises used: LinearEquiv.eq_symm_apply, TensorPower.cast_symm
-- Module: Mathlib.LinearAlgebra.TensorPower.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
x : GradedMonoid fun (i : ℕ) ↦ ⨂[R]^i M
⊢ (r • x).snd (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M) =
    (cast R M ⋯ :
        (a :
            ⨂[R]^(GradedMonoid.mk 0 (((↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M).toAddMonoidHom : (a : R) → ⨂[R]^0 M) r) * x).fst
              M) →
          ⨂[R]^(r • x).fst M)
      ((GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) 0
              ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) r) *
            x).snd
        (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M))

Tactic:
(algebraMap₀_mul r x.snd).symm

Premises used: Quotient.liftOn', AddCon.liftOn, TensorPower.algebraMap₀_mul, GradedMonoid, Eq.symm, Sigma.snd
-- Module: Mathlib.LinearAlgebra.TensorPower.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
x : GradedMonoid fun (i : ℕ) ↦ ⨂[R]^i M
⊢ (r • x).snd (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M) =
    (cast R M ⋯ :
        (a :
            ⨂[R]^(GradedMonoid.mk 0 (((↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M).toAddMonoidHom : (a : R) → ⨂[R]^0 M) r) * x).fst
              M) →
          ⨂[R]^(r • x).fst M)
      ((GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) 0
              ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) r) *
            x).snd
        (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M))

Tactic:
exact (algebraMap₀_mul r x.snd).symm

Premises used: TensorPower.algebraMap₀_mul, Eq.symm, Sigma.snd
-- Module: Mathlib.LinearAlgebra.TensorPower.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
⊢ Eq (α := ⨂[R]^0 M)
    (((@DirectSum.GAlgebra.toFun _ R (fun (i : ℕ) ↦ ⨂[R]^i M) inst (fun (i : ℕ) ↦ instAddCommMonoid fun (x : Fin i) ↦ M)
              (fun (i : ℕ) ↦ instModule (s := fun (x : Fin i) ↦ M)) Nat.instAddMonoid gsemiring _ :
            R →+ ⨂[R]^0 M) :
          (a : R) → ⨂[R]^0 M)
        r :
      ⨂[R]^0 M)
    ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r : ⨂[R]^0 M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.TensorPower.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Algebra R (⨁ (n : ℕ), ⨂[R]^n M)

Tactic:
infer_instance
-- Module: Mathlib.LinearAlgebra.TensorPower.Pairing
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
x : DecidableEq (Fin n)
f : Fin n → Module.Dual R M
φ : Module.Dual R M
i j : Fin n
v : Fin n → M
pos :
  ∀ (h : j = i),
    Eq.{u_1 + 1} (α := R) ((Function.update (β := fun (a : Fin n) ↦ Module.Dual R M) f i φ j : (a : M) → R) (v j) : R)
      (Function.update (β := fun (j : Fin n) ↦ R) (fun (j : Fin n) ↦ (f j : (a : M) → R) (v j)) i
          ((φ : (a : M) → R) (v i)) j :
        R)
neg :
  ∀ (h : ¬j = i),
    Eq.{u_1 + 1} (α := R) ((Function.update (β := fun (a : Fin n) ↦ Module.Dual R M) f i φ j : (a : M) → R) (v j) : R)
      (Function.update (β := fun (j : Fin n) ↦ R) (fun (j : Fin n) ↦ (f j : (a : M) → R) (v j)) i
          ((φ : (a : M) → R) (v i)) j :
        R)
⊢ Eq.{u_1 + 1} (α := R) ((Function.update (β := fun (a : Fin n) ↦ Module.Dual R M) f i φ j : (a : M) → R) (v j) : R)
    (Function.update (β := fun (j : Fin n) ↦ R) (fun (j : Fin n) ↦ (f j : (a : M) → R) (v j)) i
        ((φ : (a : M) → R) (v i)) j :
      R)

Tactic:
by_cases h : j = i
-- Module: Mathlib.LinearAlgebra.TensorPower.Pairing
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
x : DecidableEq (Fin n)
f : Fin n → Module.Dual R M
φ : Module.Dual R M
i j : Fin n
v : Fin n → M
h : j = i
pos :
  Eq.{u_1 + 1} (α := R) ((Function.update (β := fun (a : Fin n) ↦ Module.Dual R M) f j φ j : (a : M) → R) (v j) : R)
    (Function.update (β := fun (j : Fin n) ↦ R) (fun (j : Fin n) ↦ (f j : (a : M) → R) (v j)) j
        ((φ : (a : M) → R) (v j)) j :
      R)
⊢ Eq.{u_1 + 1} (α := R) ((Function.update (β := fun (a : Fin n) ↦ Module.Dual R M) f i φ j : (a : M) → R) (v j) : R)
    (Function.update (β := fun (j : Fin n) ↦ R) (fun (j : Fin n) ↦ (f j : (a : M) → R) (v j)) i
        ((φ : (a : M) → R) (v i)) j :
      R)

Tactic:
subst h
-- Module: Mathlib.LinearAlgebra.TensorPower.Pairing
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
x : DecidableEq (Fin n)
f : Fin n → Module.Dual R M
φ : Module.Dual R M
j : Fin n
v : Fin n → M
⊢ Eq.{u_1 + 1} (α := R) ((Function.update (β := fun (a : Fin n) ↦ Module.Dual R M) f j φ j : (a : M) → R) (v j) : R)
    (Function.update (β := fun (j : Fin n) ↦ R) (fun (j : Fin n) ↦ (f j : (a : M) → R) (v j)) j
        ((φ : (a : M) → R) (v j)) j :
      R)

Tactic:
simp only [Function.update_self]

Premises used: Function.update_self
-- Module: Mathlib.LinearAlgebra.TensorPower.Pairing
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
x : DecidableEq (Fin n)
f : Fin n → Module.Dual R M
φ : Module.Dual R M
i j : Fin n
v : Fin n → M
h : ¬j = i
⊢ Eq.{u_1 + 1} (α := R) ((Function.update (β := fun (a : Fin n) ↦ Module.Dual R M) f i φ j : (a : M) → R) (v j) : R)
    (Function.update (β := fun (j : Fin n) ↦ R) (fun (j : Fin n) ↦ (f j : (a : M) → R) (v j)) i
        ((φ : (a : M) → R) (v i)) j :
      R)

Tactic:
simp only [Function.update_of_ne h]

Premises used: Function.update_of_ne
-- Module: Mathlib.LinearAlgebra.TensorPower.Pairing
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
this :
  ∀ (x : DecidableEq (Fin n)) (f : Fin n → Module.Dual R M) (φ : Module.Dual R M) (i j : Fin n) (v : Fin n → M),
    Eq.{u_1 + 1} (α := R) ((Function.update (β := fun (a : Fin n) ↦ Module.Dual R M) f i φ j : (a : M) → R) (v j) : R)
      (Function.update (β := fun (j : Fin n) ↦ R) (fun (j : Fin n) ↦ (f j : (a : M) → R) (v j)) i
          ((φ : (a : M) → R) (v i)) j :
        R)
inst_3 : DecidableEq (Fin n)
f : (i : Fin n) → Module.Dual R M
i : Fin n
φ₁ φ₂ : Module.Dual R M
v : (i : Fin n) → M
⊢ (((PiTensorProduct.lift (s := fun (x : Fin n) ↦ M) :
              (a : MultilinearMap R (fun (x : Fin n) ↦ M) R) → (⨂[R] (i : Fin n), M) →ₗ[R] R)
            (MultilinearMap.compLinearMap (M₁ := fun (x : Fin n) ↦ M) (M₁' := fun (x : Fin n) ↦ R)
              (MultilinearMap.mkPiRing R (Fin n) 1)
              (Function.update (β := fun (x : Fin n) ↦ Module.Dual R M) f i (φ₁ + φ₂))) :
          (⨂[R] (i : Fin n), M) →ₗ[R] R) :
        (a : ⨂[R] (i : Fin n), M) → R)
      ((tprod R (s := fun (i : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) v : ⨂[R] (i : Fin n), M) =
    HAdd.hAdd (α := R) (β := R)
      ((((PiTensorProduct.lift (s := fun (x : Fin n) ↦ M) :
                  (a : MultilinearMap R (fun (x : Fin n) ↦ M) R) → (⨂[R] (i : Fin n), M) →ₗ[R] R)
                (MultilinearMap.compLinearMap (M₁ := fun (x : Fin n) ↦ M) (M₁' := fun (x : Fin n) ↦ R)
                  (MultilinearMap.mkPiRing R (Fin n) 1)
                  (Function.update (β := fun (x : Fin n) ↦ Module.Dual R M) f i φ₁)) :
              (⨂[R] (i : Fin n), M) →ₗ[R] R) :
            (a : ⨂[R] (i : Fin n), M) → R)
          ((tprod R (s := fun (i : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) v : ⨂[R] (i : Fin n), M) :
        R)
      ((((PiTensorProduct.lift (s := fun (x : Fin n) ↦ M) :
                  (a : MultilinearMap R (fun (x : Fin n) ↦ M) R) → (⨂[R] (i : Fin n), M) →ₗ[R] R)
                (MultilinearMap.compLinearMap (M₁ := fun (x : Fin n) ↦ M) (M₁' := fun (x : Fin n) ↦ R)
                  (MultilinearMap.mkPiRing R (Fin n) 1)
                  (Function.update (β := fun (x : Fin n) ↦ Module.Dual R M) f i φ₂)) :
              (⨂[R] (i : Fin n), M) →ₗ[R] R) :
            (a : ⨂[R] (i : Fin n), M) → R)
          ((tprod R (s := fun (i : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) v : ⨂[R] (i : Fin n), M) :
        R)

Tactic:
simp only [lift.tprod, MultilinearMap.compLinearMap_apply, this,
        LinearMap.add_apply, MultilinearMap.map_update_add]

Premises used: PiTensorProduct.lift.tprod, MultilinearMap.map_update_add, LinearMap.add_apply, MultilinearMap.compLinearMap_apply
-- Module: Mathlib.LinearAlgebra.TensorPower.Pairing
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
this :
  ∀ (x : DecidableEq (Fin n)) (f : Fin n → Module.Dual R M) (φ : Module.Dual R M) (i j : Fin n) (v : Fin n → M),
    Eq.{u_1 + 1} (α := R) ((Function.update (β := fun (a : Fin n) ↦ Module.Dual R M) f i φ j : (a : M) → R) (v j) : R)
      (Function.update (β := fun (j : Fin n) ↦ R) (fun (j : Fin n) ↦ (f j : (a : M) → R) (v j)) i
          ((φ : (a : M) → R) (v i)) j :
        R)
inst_3 : DecidableEq (Fin n)
f : (i : Fin n) → Module.Dual R M
i : Fin n
a : R
φ : Module.Dual R M
H :
  ∀ (v : (i : Fin n) → M),
    Eq.{u_1 + 1} (α := R)
      ((LinearMap.compMultilinearMap (M₁ := fun (i : Fin n) ↦ M)
              ((PiTensorProduct.lift (s := fun (x : Fin n) ↦ M) :
                  (a : MultilinearMap R (fun (x : Fin n) ↦ M) R) → (⨂[R] (i : Fin n), M) →ₗ[R] R)
                (MultilinearMap.compLinearMap (M₁ := fun (x : Fin n) ↦ M) (M₁' := fun (x : Fin n) ↦ R)
                  (MultilinearMap.mkPiRing R (Fin n) 1)
                  (Function.update (β := fun (x : Fin n) ↦ Module.Dual R M) f i (a • φ))))
              (tprod R (s := fun (i : Fin n) ↦ M)) :
            (a : (i : Fin n) → M) → R)
          v :
        R)
      ((LinearMap.compMultilinearMap (M₁ := fun (i : Fin n) ↦ M)
              (HSMul.hSMul (β := Module.Dual R (⨂[R]^n M)) a
                ((PiTensorProduct.lift (s := fun (x : Fin n) ↦ M) :
                      (a : MultilinearMap R (fun (x : Fin n) ↦ M) R) → (⨂[R] (i : Fin n), M) →ₗ[R] R)
                    (MultilinearMap.compLinearMap (M₁ := fun (x : Fin n) ↦ M) (M₁' := fun (x : Fin n) ↦ R)
                      (MultilinearMap.mkPiRing R (Fin n) 1)
                      (Function.update (β := fun (x : Fin n) ↦ Module.Dual R M) f i φ)) :
                  (⨂[R] (i : Fin n), M) →ₗ[R] R))
              (tprod R (s := fun (i : Fin n) ↦ M)) :
            (a : (i : Fin n) → M) → R)
          v :
        R)
⊢ (PiTensorProduct.lift (s := fun (x : Fin n) ↦ M) :
        (a : MultilinearMap R (fun (x : Fin n) ↦ M) R) → (⨂[R] (i : Fin n), M) →ₗ[R] R)
      (MultilinearMap.compLinearMap (M₁ := fun (x : Fin n) ↦ M) (M₁' := fun (x : Fin n) ↦ R)
        (MultilinearMap.mkPiRing R (Fin n) 1) (Function.update (β := fun (x : Fin n) ↦ Module.Dual R M) f i (a • φ))) =
    HSMul.hSMul (β := Module.Dual R (⨂[R]^n M)) a
      ((PiTensorProduct.lift (s := fun (x : Fin n) ↦ M) :
            (a : MultilinearMap R (fun (x : Fin n) ↦ M) R) → (⨂[R] (i : Fin n), M) →ₗ[R] R)
          (MultilinearMap.compLinearMap (M₁ := fun (x : Fin n) ↦ M) (M₁' := fun (x : Fin n) ↦ R)
            (MultilinearMap.mkPiRing R (Fin n) 1) (Function.update (β := fun (x : Fin n) ↦ Module.Dual R M) f i φ)) :
        (⨂[R] (i : Fin n), M) →ₗ[R] R)

Tactic:
ext v
-- Module: Mathlib.LinearAlgebra.TensorPower.Pairing
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
this :
  ∀ (x : DecidableEq (Fin n)) (f : Fin n → Module.Dual R M) (φ : Module.Dual R M) (i j : Fin n) (v : Fin n → M),
    Eq.{u_1 + 1} (α := R) ((Function.update (β := fun (a : Fin n) ↦ Module.Dual R M) f i φ j : (a : M) → R) (v j) : R)
      (Function.update (β := fun (j : Fin n) ↦ R) (fun (j : Fin n) ↦ (f j : (a : M) → R) (v j)) i
          ((φ : (a : M) → R) (v i)) j :
        R)
inst_3 : DecidableEq (Fin n)
f : (i : Fin n) → Module.Dual R M
i : Fin n
a : R
φ : Module.Dual R M
v : (i : Fin n) → M
H :
  HSMul.hSMul (β := R) a
      ((MultilinearMap.mkPiRing R (Fin n) 1 : (a : (i : Fin n) → R) → R)
          (Function.update (β := fun (x : Fin n) ↦ R) (fun (j : Fin n) ↦ (f j : (a : M) → R) (v j)) i
            ((φ : (a : M) → R) (v i))) :
        R) =
    HMul.hMul (β := R) a
      ((MultilinearMap.mkPiRing R (Fin n) 1 : (a : (i : Fin n) → R) → R) fun (i_1 : Fin n) ↦
          Function.update (β := fun (j : Fin n) ↦ R) (fun (j : Fin n) ↦ (f j : (a : M) → R) (v j)) i
            ((φ : (a : M) → R) (v i)) i_1 :
        R)
⊢ (((PiTensorProduct.lift (s := fun (x : Fin n) ↦ M) :
              (a : MultilinearMap R (fun (x : Fin n) ↦ M) R) → (⨂[R] (i : Fin n), M) →ₗ[R] R)
            (MultilinearMap.compLinearMap (M₁ := fun (x : Fin n) ↦ M) (M₁' := fun (x : Fin n) ↦ R)
              (MultilinearMap.mkPiRing R (Fin n) 1)
              (Function.update (β := fun (x : Fin n) ↦ Module.Dual R M) f i (a • φ))) :
          (⨂[R] (i : Fin n), M) →ₗ[R] R) :
        (a : ⨂[R] (i : Fin n), M) → R)
      ((tprod R (s := fun (i : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) v : ⨂[R] (i : Fin n), M) =
    HMul.hMul (β := R) a
      ((((PiTensorProduct.lift (s := fun (x : Fin n) ↦ M) :
                  (a : MultilinearMap R (fun (x : Fin n) ↦ M) R) → (⨂[R] (i : Fin n), M) →ₗ[R] R)
                (MultilinearMap.compLinearMap (M₁ := fun (x : Fin n) ↦ M) (M₁' := fun (x : Fin n) ↦ R)
                  (MultilinearMap.mkPiRing R (Fin n) 1)
                  (Function.update (β := fun (x : Fin n) ↦ Module.Dual R M) f i φ)) :
              (⨂[R] (i : Fin n), M) →ₗ[R] R) :
            (a : ⨂[R] (i : Fin n), M) → R)
          ((tprod R (s := fun (i : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) v : ⨂[R] (i : Fin n), M) :
        R)

Tactic:
simp only [lift.tprod, MultilinearMap.compLinearMap_apply, this,
         LinearMap.smul_apply, MultilinearMap.map_update_smul]

Premises used: PiTensorProduct.lift.tprod, MultilinearMap.map_update_smul, LinearMap.smul_apply, MultilinearMap.compLinearMap_apply
-- Module: Mathlib.LinearAlgebra.TensorPower.Pairing
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
this :
  ∀ (x : DecidableEq (Fin n)) (f : Fin n → Module.Dual R M) (φ : Module.Dual R M) (i j : Fin n) (v : Fin n → M),
    Eq.{u_1 + 1} (α := R) ((Function.update (β := fun (a : Fin n) ↦ Module.Dual R M) f i φ j : (a : M) → R) (v j) : R)
      (Function.update (β := fun (j : Fin n) ↦ R) (fun (j : Fin n) ↦ (f j : (a : M) → R) (v j)) i
          ((φ : (a : M) → R) (v i)) j :
        R)
inst_3 : DecidableEq (Fin n)
f : (i : Fin n) → Module.Dual R M
i : Fin n
a : R
φ : Module.Dual R M
v : (i : Fin n) → M
⊢ HSMul.hSMul (β := R) a
      ((MultilinearMap.mkPiRing R (Fin n) 1 : (a : (i : Fin n) → R) → R)
          (Function.update (β := fun (x : Fin n) ↦ R) (fun (j : Fin n) ↦ (f j : (a : M) → R) (v j)) i
            ((φ : (a : M) → R) (v i))) :
        R) =
    HMul.hMul (β := R) a
      ((MultilinearMap.mkPiRing R (Fin n) 1 : (a : (i : Fin n) → R) → R) fun (i_1 : Fin n) ↦
          Function.update (β := fun (j : Fin n) ↦ R) (fun (j : Fin n) ↦ (f j : (a : M) → R) (v j)) i
            ((φ : (a : M) → R) (v i)) i_1 :
        R)

Tactic:
dsimp
-- Module: Mathlib.LinearAlgebra.TensorPower.Pairing
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
f : Fin n → Module.Dual R M
v : Fin n → M
⊢ Eq.{u_1 + 1} (α := R)
    ((((multilinearMapToDual R M n : (a : (i : Fin n) → Module.Dual R M) → Module.Dual R (⨂[R]^n M)) f :
            Module.Dual R (⨂[R]^n M)) :
          (a : ⨂[R]^n M) → R)
        ((tprod R (s := fun (x : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) v : ⨂[R] (i : Fin n), M) :
      R)
    (∏ i : Fin n, (f i : (a : M) → R) (v i) : R)

Tactic:
simp [multilinearMapToDual]

Premises used: TensorPower.multilinearMapToDual
-- Module: Mathlib.LinearAlgebra.TensorPower.Pairing
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
f : Fin n → Module.Dual R M
v : Fin n → M
⊢ Eq.{u_1 + 1} (α := R)
    ((((pairingDual R M n : (a : ⨂[R]^n (Module.Dual R M)) → Module.Dual R (⨂[R]^n M))
              ((tprod R (s := fun (x : Fin n) ↦ Module.Dual R M) :
                  (a : (i : Fin n) → Module.Dual R M) → ⨂[R] (i : Fin n), Module.Dual R M)
                f) :
            Module.Dual R (⨂[R]^n M)) :
          (a : ⨂[R]^n M) → R)
        ((tprod R (s := fun (x : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) v : ⨂[R] (i : Fin n), M) :
      R)
    (∏ i : Fin n, (f i : (a : M) → R) (v i) : R)

Tactic:
simp [pairingDual]

Premises used: TensorPower.pairingDual
-- Module: Mathlib.LinearAlgebra.TensorPower.Symmetric
Goal:
R ι : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
x y : ⨂[R] (x : ι), M
e : Perm ι
f : ι → M
of :
  IsEmpty ι →
    (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop)
      (HSMul.hSMul (β := ⨂[R] (x : ι), M) r
        ((PiTensorProduct.tprod R (s := fun (x : ι) ↦ M) : (a : (i : ι) → M) → ⨂[R] (i : ι), M) fun (i : ι) ↦ f i))
      (HSMul.hSMul (β := ⨂[R] (x : ι), M) r
        ((PiTensorProduct.tprod R (s := fun (x : ι) ↦ M) : (a : (i : ι) → M) → ⨂[R] (i : ι), M) fun (i : ι) ↦
          f ((e : (a : ι) → ι) i)))
of₁ :
  Nonempty ι →
    (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop)
      (HSMul.hSMul (β := ⨂[R] (x : ι), M) r
        ((PiTensorProduct.tprod R (s := fun (x : ι) ↦ M) : (a : (i : ι) → M) → ⨂[R] (i : ι), M) fun (i : ι) ↦ f i))
      (HSMul.hSMul (β := ⨂[R] (x : ι), M) r
        ((PiTensorProduct.tprod R (s := fun (x : ι) ↦ M) : (a : (i : ι) → M) → ⨂[R] (i : ι), M) fun (i : ι) ↦
          f ((e : (a : ι) → ι) i)))
⊢ (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop)
    (HSMul.hSMul (β := ⨂[R] (x : ι), M) r
      ((PiTensorProduct.tprod R (s := fun (x : ι) ↦ M) : (a : (i : ι) → M) → ⨂[R] (i : ι), M) fun (i : ι) ↦ f i))
    (HSMul.hSMul (β := ⨂[R] (x : ι), M) r
      ((PiTensorProduct.tprod R (s := fun (x : ι) ↦ M) : (a : (i : ι) → M) → ⨂[R] (i : ι), M) fun (i : ι) ↦
        f ((e : (a : ι) → ι) i)))

Tactic:
apply isEmpty_or_nonempty ι |>.elim

Premises used: isEmpty_or_nonempty, Or.elim