awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
Goal:
ι : Type u_1
ι₂ : Type u_2
R : Type u_4
inst : CommSemiring R
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
t : ι → Type u_11
inst_3 : (i : ι) → AddCommMonoid (t i)
inst_4 : (i : ι) → Module.{u_4, u_11} R (t i)
f : (i : ι) → LinearMap.{u_4, u_4, u_7, u_11} (RingHom.id R) (s i) (t i)
e : ι ≃ ι₂
x : ⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i)
⊢ Eq (α := ⨂[R] (i : ι), t i)
    ((map (s := s) (t := t) f : (a : ⨂[R] (i : ι), s i) → ⨂[R] (i : ι), t i)
        ((LinearEquiv.symm (reindex R s e) : (a : ⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i)) → ⨂[R] (i : ι), s i)
          x) :
      ⨂[R] (i : ι), t i)
    ((LinearEquiv.symm (reindex R t e) : (a : ⨂[R] (i : ι₂), t ((e.symm : (a : ι₂) → ι) i)) → ⨂[R] (i : ι), t i)
        ((map (s := fun (i : ι₂) ↦ s ((e.symm : (a : ι₂) → ι) i)) (t := fun (i : ι₂) ↦ t ((e.symm : (a : ι₂) → ι) i))
              fun (i : ι₂) ↦ f ((e.symm : (a : ι₂) → ι) i) :
            (a : ⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i)) → ⨂[R] (i : ι₂), t ((e.symm : (a : ι₂) → ι) i))
          x) :
      ⨂[R] (i : ι), t i)

Tactic:
DFunLike.congr_fun (map_comp_reindex_symm _ _) _

Premises used: DFunLike.congr_fun, Quotient.liftOn', AddCon.liftOn, PiTensorProduct.map_comp_reindex_symm
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
t : ι → Type u_11
inst_8 : (i : ι) → AddCommMonoid (t i)
inst_9 : (i : ι) → Module.{u_4, u_11} R (t i)
inst_10 : IsEmpty ι
x : ⨂[R] (i : ι), s i
⊢ (fun (r : R) ↦
        HSMul.hSMul (β := ⨂[R] (i : ι), s i) r
          ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (isEmptyElim (p := s))))
      ((((lift (s := s) : (a : MultilinearMap R s R) → (⨂[R] (i : ι), s i) →ₗ[R] R) (constOfIsEmpty R s 1) :
            (⨂[R] (i : ι), s i) →ₗ[R] R) :
          (a : ⨂[R] (i : ι), s i) → R)
        x) =
    x

Tactic:
x.induction_on ?_ ?_

Premises used: PiTensorProduct.induction_on
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
t : ι → Type u_11
inst_8 : (i : ι) → AddCommMonoid (t i)
inst_9 : (i : ι) → Module.{u_4, u_11} R (t i)
inst_10 : IsEmpty ι
x : ⨂[R] (i : ι), s i
refine_1 :
  ∀ (r : R) (f : (i : ι) → s i),
    (fun (r : R) ↦
          HSMul.hSMul (β := ⨂[R] (i : ι), s i) r
            ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (isEmptyElim (p := s))))
        ((((lift (s := s) : (a : MultilinearMap R s R) → (⨂[R] (i : ι), s i) →ₗ[R] R) (constOfIsEmpty R s 1) :
              (⨂[R] (i : ι), s i) →ₗ[R] R) :
            (a : ⨂[R] (i : ι), s i) → R)
          (HSMul.hSMul (β := ⨂[R] (i : ι), s i) r
            ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) f : ⨂[R] (i : ι), s i))) =
      HSMul.hSMul (β := ⨂[R] (i : ι), s i) r
        ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) f : ⨂[R] (i : ι), s i)
refine_2 :
  ∀ (x y : ⨂[R] (i : ι), s i),
    (fun (r : R) ↦
            HSMul.hSMul (β := ⨂[R] (i : ι), s i) r
              ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (isEmptyElim (p := s))))
          ((((lift (s := s) : (a : MultilinearMap R s R) → (⨂[R] (i : ι), s i) →ₗ[R] R) (constOfIsEmpty R s 1) :
                (⨂[R] (i : ι), s i) →ₗ[R] R) :
              (a : ⨂[R] (i : ι), s i) → R)
            x) =
        x →
      (fun (r : R) ↦
              HSMul.hSMul (β := ⨂[R] (i : ι), s i) r
                ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (isEmptyElim (p := s))))
            ((((lift (s := s) : (a : MultilinearMap R s R) → (⨂[R] (i : ι), s i) →ₗ[R] R) (constOfIsEmpty R s 1) :
                  (⨂[R] (i : ι), s i) →ₗ[R] R) :
                (a : ⨂[R] (i : ι), s i) → R)
              y) =
          y →
        (fun (r : R) ↦
              HSMul.hSMul (β := ⨂[R] (i : ι), s i) r
                ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (isEmptyElim (p := s))))
            ((((lift (s := s) : (a : MultilinearMap R s R) → (⨂[R] (i : ι), s i) →ₗ[R] R) (constOfIsEmpty R s 1) :
                  (⨂[R] (i : ι), s i) →ₗ[R] R) :
                (a : ⨂[R] (i : ι), s i) → R)
              (x + y)) =
          x + y
⊢ (fun (r : R) ↦
        HSMul.hSMul (β := ⨂[R] (i : ι), s i) r
          ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (isEmptyElim (p := s))))
      ((((lift (s := s) : (a : MultilinearMap R s R) → (⨂[R] (i : ι), s i) →ₗ[R] R) (constOfIsEmpty R s 1) :
            (⨂[R] (i : ι), s i) →ₗ[R] R) :
          (a : ⨂[R] (i : ι), s i) → R)
        x) =
    x

Tactic:
refine x.induction_on ?_ ?_
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
t : ι → Type u_11
inst_8 : (i : ι) → AddCommMonoid (t i)
inst_9 : (i : ι) → Module.{u_4, u_11} R (t i)
inst_10 : IsEmpty ι
x_1 : ⨂[R] (i : ι), s i
x : R
y : (i : ι) → s i
refine_1 :
  HSMul.hSMul (β := ⨂[R] (i : ι), s i) x
      ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (isEmptyElim (p := s))) =
    HSMul.hSMul (β := ⨂[R] (i : ι), s i) x
      ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) y : ⨂[R] (i : ι), s i)
⊢ (fun (r : R) ↦
        HSMul.hSMul (β := ⨂[R] (i : ι), s i) r
          ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (isEmptyElim (p := s))))
      ((((lift (s := s) : (a : MultilinearMap R s R) → (⨂[R] (i : ι), s i) →ₗ[R] R) (constOfIsEmpty R s 1) :
            (⨂[R] (i : ι), s i) →ₗ[R] R) :
          (a : ⨂[R] (i : ι), s i) → R)
        (HSMul.hSMul (β := ⨂[R] (i : ι), s i) x
          ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) y : ⨂[R] (i : ι), s i))) =
    HSMul.hSMul (β := ⨂[R] (i : ι), s i) x
      ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) y : ⨂[R] (i : ι), s i)

Tactic:
simp only [map_smulₛₗ, RingHom.id_apply, lift.tprod, constOfIsEmpty_apply, const_apply,
        smul_eq_mul, mul_one]

Premises used: Function.const_apply, PiTensorProduct.lift.tprod, RingHom.id_apply, MultilinearMap.constOfIsEmpty_apply, MulActionSemiHomClass.map_smulₛₗ, smul_eq_mul, mul_one
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
t : ι → Type u_11
inst_8 : (i : ι) → AddCommMonoid (t i)
inst_9 : (i : ι) → Module.{u_4, u_11} R (t i)
inst_10 : IsEmpty ι
x_1 : ⨂[R] (i : ι), s i
x : R
y : (i : ι) → s i
refine_1 : isEmptyElim (p := s) = y
⊢ HSMul.hSMul (β := ⨂[R] (i : ι), s i) x
      ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (isEmptyElim (p := s))) =
    HSMul.hSMul (β := ⨂[R] (i : ι), s i) x
      ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) y : ⨂[R] (i : ι), s i)

Tactic:
congr
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
t : ι → Type u_11
inst_8 : (i : ι) → AddCommMonoid (t i)
inst_9 : (i : ι) → Module.{u_4, u_11} R (t i)
inst_10 : IsEmpty ι
x_1 : ⨂[R] (i : ι), s i
x : R
y : (i : ι) → s i
⊢ isEmptyElim (p := s) = y

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
t_1 : ι → Type u_11
inst_8 : (i : ι) → AddCommMonoid (t_1 i)
inst_9 : (i : ι) → Module.{u_4, u_11} R (t_1 i)
inst_10 : IsEmpty ι
t : R
⊢ (((lift (s := s) : (a : MultilinearMap R s R) → (⨂[R] (i : ι), s i) →ₗ[R] R) (constOfIsEmpty R s 1) :
          (⨂[R] (i : ι), s i) →ₗ[R] R) :
        (a : ⨂[R] (i : ι), s i) → R)
      ((fun (r : R) ↦
          HSMul.hSMul (β := ⨂[R] (i : ι), s i) r
            ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (isEmptyElim (p := s))))
        t) =
    t

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
inst_3 : IsEmpty ι
f : (i : ι) → s i
⊢ Eq.{u_4 + 1} (α := R)
    ((isEmptyEquiv ι (s := s) : (a : ⨂[R] (i : ι), s i) → R)
        ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) f : ⨂[R] (i : ι), s i) :
      R)
    (1 : R)

Tactic:
lift.tprod _

Premises used: PiTensorProduct.lift.tprod, Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
t : ι → Type u_11
inst_8 : (i : ι) → AddCommMonoid (t i)
inst_9 : (i : ι) → Module.{u_4, u_11} R (t i)
inst_10 : Subsingleton ι
i₀ : ι
inst_11 : DecidableEq ι
m : (i : ι) → s i
i : ι
rw : ∀ (x y : s i₀), update (β := s) m i₀ (x + y) i₀ = update (β := s) m i₀ x i₀ + update (β := s) m i₀ y i₀
⊢ ∀ (x y : s i), update (β := s) m i (x + y) i₀ = update (β := s) m i x i₀ + update (β := s) m i y i₀

Tactic:
rw [Subsingleton.elim i i₀]

Premises used: Subsingleton.elim
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
t : ι → Type u_11
inst_8 : (i : ι) → AddCommMonoid (t i)
inst_9 : (i : ι) → Module.{u_4, u_11} R (t i)
inst_10 : Subsingleton ι
i₀ : ι
inst_11 : DecidableEq ι
m : (i : ι) → s i
i : ι
⊢ ∀ (x y : s i₀), update (β := s) m i₀ (x + y) i₀ = update (β := s) m i₀ x i₀ + update (β := s) m i₀ y i₀

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
t : ι → Type u_11
inst_8 : (i : ι) → AddCommMonoid (t i)
inst_9 : (i : ι) → Module.{u_4, u_11} R (t i)
inst_10 : Subsingleton ι
i₀ : ι
inst_11 : DecidableEq ι
m : (i : ι) → s i
i : ι
rw : ∀ (c : R) (x : s i₀), update (β := s) m i₀ (c • x) i₀ = c • update (β := s) m i₀ x i₀
⊢ ∀ (c : R) (x : s i), update (β := s) m i (c • x) i₀ = c • update (β := s) m i x i₀

Tactic:
rw [Subsingleton.elim i i₀]

Premises used: Subsingleton.elim
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
t : ι → Type u_11
inst_8 : (i : ι) → AddCommMonoid (t i)
inst_9 : (i : ι) → Module.{u_4, u_11} R (t i)
inst_10 : Subsingleton ι
i₀ : ι
inst_11 : DecidableEq ι
m : (i : ι) → s i
i : ι
⊢ ∀ (c : R) (x : s i₀), update (β := s) m i₀ (c • x) i₀ = c • update (β := s) m i₀ x i₀

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
t : ι → Type u_11
inst_8 : (i : ι) → AddCommMonoid (t i)
inst_9 : (i : ι) → Module.{u_4, u_11} R (t i)
inst_10 : Subsingleton ι
i₀ : ι
⊢ ∀ (x y : s i₀),
    (tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (update (β := s) 0 i₀ (x + y)) =
      HAdd.hAdd (α := ⨂[R] (i : ι), s i) (β := ⨂[R] (i : ι), s i)
        ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (update (β := s) 0 i₀ x) : ⨂[R] (i : ι), s i)
        ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (update (β := s) 0 i₀ y) : ⨂[R] (i : ι), s i)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
t : ι → Type u_11
inst_8 : (i : ι) → AddCommMonoid (t i)
inst_9 : (i : ι) → Module.{u_4, u_11} R (t i)
inst_10 : Subsingleton ι
i₀ : ι
⊢ ∀ (m : R) (x : s i₀),
    (tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (update (β := s) 0 i₀ (m • x)) =
      HSMul.hSMul (α := R) (β := ⨂[R] (i : ι), s i) ((RingHom.id R : (a : R) → R) m : R)
        ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (update (β := s) 0 i₀ x) : ⨂[R] (i : ι), s i)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
t : ι → Type u_11
inst_8 : (i : ι) → AddCommMonoid (t i)
inst_9 : (i : ι) → Module.{u_4, u_11} R (t i)
inst_10 : Subsingleton ι
i₀ : ι
h :
  ∀ (x : s i₀),
    Eq (α := s i₀)
      (((lift (s := s) : (a : MultilinearMap R s (s i₀)) → (⨂[R] (i : ι), s i) →ₗ[R] s i₀)
                (MultilinearMap.mk (M₁ := s) (fun (f : (i : ι) → s i) ↦ f i₀) ⋯ ⋯) ∘ₗ
              {
                toFun := fun (x : s i₀) ↦
                  (tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (update (β := s) 0 i₀ x),
                map_add' := ⋯, map_smul' := ⋯ } :
            (a : s i₀) → s i₀)
          x :
        s i₀)
      ((LinearMap.id : (a : s i₀) → s i₀) x : s i₀)
⊢ Eq.{u_7 + 1} (α := s i₀ →ₗ[R] s i₀)
    ((lift (s := s) : (a : MultilinearMap R s (s i₀)) → (⨂[R] (i : ι), s i) →ₗ[R] s i₀)
        (MultilinearMap.mk (M₁ := s) (fun (f : (i : ι) → s i) ↦ f i₀) ⋯ ⋯) ∘ₗ
      { toFun := fun (x : s i₀) ↦ (tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (update (β := s) 0 i₀ x),
        map_add' := ⋯, map_smul' := ⋯ })
    LinearMap.id

Tactic:
ext _
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
t : ι → Type u_11
inst_8 : (i : ι) → AddCommMonoid (t i)
inst_9 : (i : ι) → Module.{u_4, u_11} R (t i)
inst_10 : Subsingleton ι
i₀ : ι
x : s i₀
⊢ Eq (α := s i₀)
    (((lift (s := s) : (a : MultilinearMap R s (s i₀)) → (⨂[R] (i : ι), s i) →ₗ[R] s i₀)
              (MultilinearMap.mk (M₁ := s) (fun (f : (i : ι) → s i) ↦ f i₀) ⋯ ⋯) ∘ₗ
            {
              toFun := fun (x : s i₀) ↦
                (tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (update (β := s) 0 i₀ x),
              map_add' := ⋯, map_smul' := ⋯ } :
          (a : s i₀) → s i₀)
        x :
      s i₀)
    ((LinearMap.id : (a : s i₀) → s i₀) x : s i₀)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
t : ι → Type u_11
inst_8 : (i : ι) → AddCommMonoid (t i)
inst_9 : (i : ι) → Module.{u_4, u_11} R (t i)
inst_10 : Subsingleton ι
i₀ : ι
H :
  ∀ (f : (i : ι) → s i),
    Eq (α := ⨂[R] (i : ι), s i)
      ((LinearMap.compMultilinearMap (M₁ := s)
              ({
                  toFun := fun (x : s i₀) ↦
                    (tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (update (β := s) 0 i₀ x),
                  map_add' := ⋯, map_smul' := ⋯ } ∘ₗ
                (lift (s := s) : (a : MultilinearMap R s (s i₀)) → (⨂[R] (i : ι), s i) →ₗ[R] s i₀)
                  (MultilinearMap.mk (M₁ := s) (fun (f : (i : ι) → s i) ↦ f i₀) ⋯ ⋯))
              (tprod R (s := s)) :
            (a : (i : ι) → s i) → ⨂[R] (i : ι), s i)
          f :
        ⨂[R] (i : ι), s i)
      ((LinearMap.compMultilinearMap (M₁ := s) LinearMap.id (tprod R (s := s)) :
            (a : (i : ι) → s i) → ⨂[R] (i : ι), s i)
          f :
        ⨂[R] (i : ι), s i)
⊢ Eq (α := (⨂[R] (i : ι), s i) →ₗ[R] ⨂[R] (i : ι), s i)
    ({ toFun := fun (x : s i₀) ↦ (tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (update (β := s) 0 i₀ x),
        map_add' := ⋯, map_smul' := ⋯ } ∘ₗ
      (lift (s := s) : (a : MultilinearMap R s (s i₀)) → (⨂[R] (i : ι), s i) →ₗ[R] s i₀)
        (MultilinearMap.mk (M₁ := s) (fun (f : (i : ι) → s i) ↦ f i₀) ⋯ ⋯))
    LinearMap.id

Tactic:
ext f
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
t : ι → Type u_11
inst_8 : (i : ι) → AddCommMonoid (t i)
inst_9 : (i : ι) → Module.{u_4, u_11} R (t i)
inst_10 : Subsingleton ι
i₀ : ι
f : (i : ι) → s i
⊢ update (β := s) 0 i₀ (f i₀) = f

Tactic:
have h : update (0 : (i : ι) → s i) i₀ (f i₀) = f := update_eq_self i₀ f
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
t : ι → Type u_11
inst_8 : (i : ι) → AddCommMonoid (t i)
inst_9 : (i : ι) → Module.{u_4, u_11} R (t i)
inst_10 : Subsingleton ι
i₀ : ι
f : (i : ι) → s i
h : update (β := s) 0 i₀ (f i₀) = f
⊢ Eq (α := ⨂[R] (i : ι), s i)
    ((LinearMap.compMultilinearMap (M₁ := s)
            ({
                toFun := fun (x : s i₀) ↦
                  (tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (update (β := s) 0 i₀ x),
                map_add' := ⋯, map_smul' := ⋯ } ∘ₗ
              (lift (s := s) : (a : MultilinearMap R s (s i₀)) → (⨂[R] (i : ι), s i) →ₗ[R] s i₀)
                (MultilinearMap.mk (M₁ := s) (fun (f : (i : ι) → s i) ↦ f i₀) ⋯ ⋯))
            (tprod R (s := s)) :
          (a : (i : ι) → s i) → ⨂[R] (i : ι), s i)
        f :
      ⨂[R] (i : ι), s i)
    ((LinearMap.compMultilinearMap (M₁ := s) LinearMap.id (tprod R (s := s)) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i)
        f :
      ⨂[R] (i : ι), s i)

Tactic:
simp [h]
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
inst_3 : Subsingleton ι
i₀ : ι
f : (i : ι) → s i
⊢ (subsingletonEquiv (s := s) i₀ : (a : ⨂[R] (i : ι), s i) → s i₀) (⨂ₜ[R] (i : ι), f i) = f i₀

Tactic:
lift.tprod _

Premises used: PiTensorProduct.lift.tprod
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
inst_3 : Subsingleton ι
i₀ : ι
x : s i₀
⊢ Eq (α := ⨂[R] (i : ι), s i)
    ((LinearEquiv.symm (subsingletonEquiv (s := s) i₀) : (a : s i₀) → ⨂[R] (i : ι), s i) x : ⨂[R] (i : ι), s i)
    (⨂ₜ[R] (i : ι), update (β := s) 0 i₀ x i : ⨂[R] (i : ι), s i)

Tactic:
rfl

Premises used: PiTensorProduct.tprodCoeff, AddCon.toQuotient, rfl
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
M : Type u_8
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Subsingleton ι
i₀ : ι
x : M
⊢ Eq (α := ⨂[R] (i : ι), M)
    (((LinearEquiv.symm (subsingletonEquiv (s := fun (x : ι) ↦ M) i₀) : M ≃ₗ[R] ⨂[R] (i : ι), M) :
          (a : M) → ⨂[R] (i : ι), M)
        x :
      ⨂[R] (i : ι), M)
    ((tprod R (s := fun (x : ι) ↦ M) : (a : (i : ι) → M) → ⨂[R] (i : ι), M) fun (x_1 : ι) ↦ x : ⨂[R] (i : ι), M)

Tactic:
simp [LinearEquiv.symm_apply_eq, subsingletonEquiv_apply_tprod]

Premises used: LinearEquiv.symm_apply_eq, PiTensorProduct.subsingletonEquiv_apply_tprod
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
t : ι → Type u_11
inst_8 : (i : ι) → AddCommMonoid (t i)
inst_9 : (i : ι) → Module.{u_4, u_11} R (t i)
N : ι ⊕ ι₂ → Type u_12
inst_10 : (i : ι ⊕ ι₂) → AddCommMonoid (N i)
inst_11 : (i : ι ⊕ ι₂) → Module.{u_4, u_12} R (N i)
x : (i : ι ⊕ ι₂) → N i
H :
  (fun (t : ι ⊕ ι₂) ↦
      Sum.rec (motive := fun (x : ι ⊕ ι₂) ↦ N x) (fun (i₁ : ι) ↦ x (Sum.inl i₁)) (fun (i₂ : ι₂) ↦ x (Sum.inr i₂)) t) =
    x
⊢ Eq (α := ⨂[R] (i : ι ⊕ ι₂), N i)
    (⨂ₜ[R] (t : ι ⊕ ι₂),
        Sum.rec (motive := fun (x : ι ⊕ ι₂) ↦ N x) (fun (i₁ : ι) ↦ x (Sum.inl i₁)) (fun (i₂ : ι₂) ↦ x (Sum.inr i₂)) t :
      ⨂[R] (i : ι ⊕ ι₂), N i)
    ((tprod R (s := N) : (a : (i : ι ⊕ ι₂) → N i) → ⨂[R] (i : ι ⊕ ι₂), N i) x : ⨂[R] (i : ι ⊕ ι₂), N i)

Tactic:
congr