awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n_1 n : ℕ
x₀ : M
x : Fin n → M
ih :
  Eq (α := GradedMonoid fun (n : ℕ) ↦ ⨂[R]^n M)
    (List.prod
      (List.map
        (fun (a : Fin n) ↦
          GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) 1
            ((PiTensorProduct.tprod R (s := fun (x : Fin 1) ↦ M) : (a : (i : Fin 1) → M) → ⨂[R] (i : Fin 1), M)
              fun (x_1 : Fin 1) ↦ x a))
        (List.finRange n)))
    (GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) n
      ((PiTensorProduct.tprod R (s := fun (i : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) x))
⊢ Eq (α := ⨂[R]^(n + 1) M)
    ((PiTensorProduct.tprod R (s := fun (a : Fin (n + 1)) ↦ M) :
        (a : (i : Fin (n + 1)) → M) → ⨂[R] (i : Fin (n + 1)), M)
      fun (x_1 : Fin (n + 1)) ↦ Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) x₀ x (Fin.cast ⋯ (Fin.cast ⋯ x_1)))
    ((PiTensorProduct.tprod R (s := fun (a : Fin (n + 1)) ↦ M) :
        (a : (i : Fin (n + 1)) → M) → ⨂[R] (i : Fin (n + 1)), M)
      (Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) x₀ x))

Tactic:
congr 1 with i
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
x : Fin n → M
rw :
  Eq (α := ⨁ (n : ℕ), ⨂[R]^n M)
    (List.prod
        (List.ofFn (n := n)
          (Function.comp (β := TensorAlgebra R M) (⇑toDirectSum : (a : TensorAlgebra R M) → ⨁ (n : ℕ), ⨂[R]^n M)
            fun (i : Fin n) ↦ (ι R : (a : M) → TensorAlgebra R M) (x i))) :
      ⨁ (n : ℕ), ⨂[R]^n M)
    (((DirectSum.of (fun (i : ℕ) ↦ ⨂[R]^i M) n : ⨂[R]^n M →+ ⨁ (i : ℕ), ⨂[R]^i M) :
          (a : ⨂[R]^n M) → ⨁ (i : ℕ), ⨂[R]^i M)
        ((PiTensorProduct.tprod R (s := fun (i : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) x) :
      ⨁ (i : ℕ), ⨂[R]^i M)
⊢ Eq (α := ⨁ (n : ℕ), ⨂[R]^n M)
    ((toDirectSum : (a : TensorAlgebra R M) → ⨁ (n : ℕ), ⨂[R]^n M)
        ((tprod R M n : (a : (i : Fin n) → M) → TensorAlgebra R M) x) :
      ⨁ (n : ℕ), ⨂[R]^n M)
    (((DirectSum.of (fun (i : ℕ) ↦ ⨂[R]^i M) n : ⨂[R]^n M →+ ⨁ (i : ℕ), ⨂[R]^i M) :
          (a : ⨂[R]^n M) → ⨁ (i : ℕ), ⨂[R]^i M)
        ((PiTensorProduct.tprod R (s := fun (i : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) x) :
      ⨁ (i : ℕ), ⨂[R]^i M)

Tactic:
rw [tprod_apply, map_list_prod, List.map_ofFn]

Premises used: map_list_prod, List.map_ofFn, TensorAlgebra.tprod_apply
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
x : Fin n → M
simp_rw :
  Eq (α := ⨁ (n : ℕ), ⨂[R]^n M)
    (List.prod
        (List.ofFn (n := n) fun (x_1 : Fin n) ↦
          ((DirectSum.of (fun (n : ℕ) ↦ ⨂[R]^n M) 1 : ⨂[R]^1 M →+ ⨁ (i : ℕ), ⨂[R]^i M) :
              (a : ⨂[R]^1 M) → ⨁ (i : ℕ), ⨂[R]^i M)
            ((PiTensorProduct.tprod R (s := fun (x : Fin 1) ↦ M) : (a : (i : Fin 1) → M) → ⨂[R] (i : Fin 1), M)
              fun (x_2 : Fin 1) ↦ x x_1)) :
      ⨁ (n : ℕ), ⨂[R]^n M)
    (((DirectSum.of (fun (i : ℕ) ↦ ⨂[R]^i M) n : ⨂[R]^n M →+ ⨁ (i : ℕ), ⨂[R]^i M) :
          (a : ⨂[R]^n M) → ⨁ (i : ℕ), ⨂[R]^i M)
        ((PiTensorProduct.tprod R (s := fun (i : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) x) :
      ⨁ (i : ℕ), ⨂[R]^i M)
⊢ Eq (α := ⨁ (n : ℕ), ⨂[R]^n M)
    (List.prod
        (List.ofFn (n := n)
          (Function.comp (β := TensorAlgebra R M) (⇑toDirectSum : (a : TensorAlgebra R M) → ⨁ (n : ℕ), ⨂[R]^n M)
            fun (i : Fin n) ↦ (ι R : (a : M) → TensorAlgebra R M) (x i))) :
      ⨁ (n : ℕ), ⨂[R]^n M)
    (((DirectSum.of (fun (i : ℕ) ↦ ⨂[R]^i M) n : ⨂[R]^n M →+ ⨁ (i : ℕ), ⨂[R]^i M) :
          (a : ⨂[R]^n M) → ⨁ (i : ℕ), ⨂[R]^i M)
        ((PiTensorProduct.tprod R (s := fun (i : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) x) :
      ⨁ (i : ℕ), ⨂[R]^i M)

Tactic:
simp_rw [Function.comp_def, toDirectSum_ι]

Premises used: Function.comp_def, TensorAlgebra.toDirectSum_ι
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
x : Fin n → M
rw :
  Eq (α := ⨁ (n : ℕ), ⨂[R]^n M)
    (((DirectSum.of (fun (n : ℕ) ↦ ⨂[R]^n M) ((List.finRange n).dProdIndex fun (x : Fin n) ↦ 1) :
            ⨂[R]^((List.finRange n).dProdIndex fun (x : Fin n) ↦ 1) M →+ ⨁ (i : ℕ), ⨂[R]^i M) :
          (a : ⨂[R]^((List.finRange n).dProdIndex fun (x : Fin n) ↦ 1) M) → ⨁ (i : ℕ), ⨂[R]^i M)
        ((List.finRange n).dProd (A := fun (n : ℕ) ↦ ⨂[R]^n M) (fun (x : Fin n) ↦ 1) fun (x_1 : Fin n) ↦
          (PiTensorProduct.tprod R (s := fun (x : Fin 1) ↦ M) : (a : (i : Fin 1) → M) → ⨂[R] (i : Fin 1), M)
            fun (x_2 : Fin 1) ↦ x x_1) :
      ⨁ (i : ℕ), ⨂[R]^i M)
    (((DirectSum.of (fun (i : ℕ) ↦ ⨂[R]^i M) n : ⨂[R]^n M →+ ⨁ (i : ℕ), ⨂[R]^i M) :
          (a : ⨂[R]^n M) → ⨁ (i : ℕ), ⨂[R]^i M)
        ((PiTensorProduct.tprod R (s := fun (i : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) x) :
      ⨁ (i : ℕ), ⨂[R]^i M)
⊢ Eq (α := ⨁ (n : ℕ), ⨂[R]^n M)
    (List.prod
        (List.ofFn (n := n) fun (x_1 : Fin n) ↦
          ((DirectSum.of (fun (n : ℕ) ↦ ⨂[R]^n M) 1 : ⨂[R]^1 M →+ ⨁ (i : ℕ), ⨂[R]^i M) :
              (a : ⨂[R]^1 M) → ⨁ (i : ℕ), ⨂[R]^i M)
            ((PiTensorProduct.tprod R (s := fun (x : Fin 1) ↦ M) : (a : (i : Fin 1) → M) → ⨂[R] (i : Fin 1), M)
              fun (x_2 : Fin 1) ↦ x x_1)) :
      ⨁ (n : ℕ), ⨂[R]^n M)
    (((DirectSum.of (fun (i : ℕ) ↦ ⨂[R]^i M) n : ⨂[R]^n M →+ ⨁ (i : ℕ), ⨂[R]^i M) :
          (a : ⨂[R]^n M) → ⨁ (i : ℕ), ⨂[R]^i M)
        ((PiTensorProduct.tprod R (s := fun (i : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) x) :
      ⨁ (i : ℕ), ⨂[R]^i M)

Tactic:
rw [DirectSum.list_prod_ofFn_of_eq_dProd]

Premises used: DirectSum.list_prod_ofFn_of_eq_dProd
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
x : Fin n → M
h :
  Eq (α := GradedMonoid fun (n : ℕ) ↦ ⨂[R]^n M)
    (GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) ((List.finRange n).dProdIndex fun (x : Fin n) ↦ 1)
      ((List.finRange n).dProd (A := fun (n : ℕ) ↦ ⨂[R]^n M) (fun (x : Fin n) ↦ 1) fun (x_1 : Fin n) ↦
        (PiTensorProduct.tprod R (s := fun (x : Fin 1) ↦ M) : (a : (i : Fin 1) → M) → ⨂[R] (i : Fin 1), M)
          fun (x_2 : Fin 1) ↦ x x_1))
    (GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) n
      ((PiTensorProduct.tprod R (s := fun (i : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) x))
⊢ Eq (α := ⨁ (n : ℕ), ⨂[R]^n M)
    (((DirectSum.of (fun (n : ℕ) ↦ ⨂[R]^n M) ((List.finRange n).dProdIndex fun (x : Fin n) ↦ 1) :
            ⨂[R]^((List.finRange n).dProdIndex fun (x : Fin n) ↦ 1) M →+ ⨁ (i : ℕ), ⨂[R]^i M) :
          (a : ⨂[R]^((List.finRange n).dProdIndex fun (x : Fin n) ↦ 1) M) → ⨁ (i : ℕ), ⨂[R]^i M)
        ((List.finRange n).dProd (A := fun (n : ℕ) ↦ ⨂[R]^n M) (fun (x : Fin n) ↦ 1) fun (x_1 : Fin n) ↦
          (PiTensorProduct.tprod R (s := fun (x : Fin 1) ↦ M) : (a : (i : Fin 1) → M) → ⨂[R] (i : Fin 1), M)
            fun (x_2 : Fin 1) ↦ x x_1) :
      ⨁ (i : ℕ), ⨂[R]^i M)
    (((DirectSum.of (fun (i : ℕ) ↦ ⨂[R]^i M) n : ⨂[R]^n M →+ ⨁ (i : ℕ), ⨂[R]^i M) :
          (a : ⨂[R]^n M) → ⨁ (i : ℕ), ⨂[R]^i M)
        ((PiTensorProduct.tprod R (s := fun (i : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) x) :
      ⨁ (i : ℕ), ⨂[R]^i M)

Tactic:
apply DirectSum.of_eq_of_gradedMonoid_eq

Premises used: DirectSum.of_eq_of_gradedMonoid_eq
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
x : Fin n → M
h :
  Eq (α := GradedMonoid fun (n : ℕ) ↦ ⨂[R]^n M)
    (List.prod
      (List.map
        (fun (a : Fin n) ↦
          GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) 1
            ((PiTensorProduct.tprod R (s := fun (x : Fin 1) ↦ M) : (a : (i : Fin 1) → M) → ⨂[R] (i : Fin 1), M)
              fun (x_1 : Fin 1) ↦ x a))
        (List.finRange n)))
    (GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) n
      ((PiTensorProduct.tprod R (s := fun (i : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) x))
⊢ Eq (α := GradedMonoid fun (n : ℕ) ↦ ⨂[R]^n M)
    (GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) ((List.finRange n).dProdIndex fun (x : Fin n) ↦ 1)
      ((List.finRange n).dProd (A := fun (n : ℕ) ↦ ⨂[R]^n M) (fun (x : Fin n) ↦ 1) fun (x_1 : Fin n) ↦
        (PiTensorProduct.tprod R (s := fun (x : Fin 1) ↦ M) : (a : (i : Fin 1) → M) → ⨂[R] (i : Fin 1), M)
          fun (x_2 : Fin 1) ↦ x x_1))
    (GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) n
      ((PiTensorProduct.tprod R (s := fun (i : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) x))

Tactic:
rw [GradedMonoid.mk_list_dProd]

Premises used: GradedMonoid.mk_list_dProd
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
x : Fin n → M
h h₁ :
  Eq (α := GradedMonoid fun (n : ℕ) ↦ ⨂[R]^n M)
    (GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) n
      ((PiTensorProduct.tprod R (s := fun (i : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) x))
    (GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) n
      ((PiTensorProduct.tprod R (s := fun (i : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) x))
⊢ Eq (α := GradedMonoid fun (n : ℕ) ↦ ⨂[R]^n M)
    (List.prod
      (List.map
        (fun (a : Fin n) ↦
          GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) 1
            ((PiTensorProduct.tprod R (s := fun (x : Fin 1) ↦ M) : (a : (i : Fin 1) → M) → ⨂[R] (i : Fin 1), M)
              fun (x_1 : Fin 1) ↦ x a))
        (List.finRange n)))
    (GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) n
      ((PiTensorProduct.tprod R (s := fun (i : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) x))

Tactic:
rw [TensorPower.list_prod_gradedMonoid_mk_single]

Premises used: TensorPower.list_prod_gradedMonoid_mk_single
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
h :
  ∀ (i : ℕ) (x : (i : Fin i) → M) (i_1 : ℕ),
    (((LinearMap.compMultilinearMap (M₁ := fun (i : Fin i) ↦ M)
                  (AlgHom.toLinearMap (AlgHom.comp toDirectSum ofDirectSum) ∘ₗ
                    DirectSum.lof R ℕ (fun (i : ℕ) ↦ ⨂[R]^i M) i)
                  (PiTensorProduct.tprod R (s := fun (i : Fin i) ↦ M)) :
                (a : (i : Fin i) → M) → ⨁ (n : ℕ), ⨂[R]^n M)
              x :
            ⨁ (n : ℕ), ⨂[R]^n M) :
          (a : ℕ) → ⨂[R]^a M)
        i_1 =
      (((LinearMap.compMultilinearMap (M₁ := fun (i : Fin i) ↦ M)
                  (AlgHom.toLinearMap (AlgHom.id R (⨁ (n : ℕ), ⨂[R]^n M)) ∘ₗ
                    DirectSum.lof R ℕ (fun (i : ℕ) ↦ ⨂[R]^i M) i)
                  (PiTensorProduct.tprod R (s := fun (i : Fin i) ↦ M)) :
                (a : (i : Fin i) → M) → ⨁ (n : ℕ), ⨂[R]^n M)
              x :
            ⨁ (n : ℕ), ⨂[R]^n M) :
          (a : ℕ) → ⨂[R]^a M)
        i_1
⊢ Eq (α := (⨁ (n : ℕ), ⨂[R]^n M) →ₐ[R] ⨁ (n : ℕ), ⨂[R]^n M) (AlgHom.comp toDirectSum ofDirectSum)
    (AlgHom.id R (⨁ (n : ℕ), ⨂[R]^n M))

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
i : ℕ
x : (i : Fin i) → M
i_1 : ℕ
⊢ (((LinearMap.compMultilinearMap (M₁ := fun (i : Fin i) ↦ M)
                (AlgHom.toLinearMap (AlgHom.comp toDirectSum ofDirectSum) ∘ₗ
                  DirectSum.lof R ℕ (fun (i : ℕ) ↦ ⨂[R]^i M) i)
                (PiTensorProduct.tprod R (s := fun (i : Fin i) ↦ M)) :
              (a : (i : Fin i) → M) → ⨁ (n : ℕ), ⨂[R]^n M)
            x :
          ⨁ (n : ℕ), ⨂[R]^n M) :
        (a : ℕ) → ⨂[R]^a M)
      i_1 =
    (((LinearMap.compMultilinearMap (M₁ := fun (i : Fin i) ↦ M)
                (AlgHom.toLinearMap (AlgHom.id R (⨁ (n : ℕ), ⨂[R]^n M)) ∘ₗ DirectSum.lof R ℕ (fun (i : ℕ) ↦ ⨂[R]^i M) i)
                (PiTensorProduct.tprod R (s := fun (i : Fin i) ↦ M)) :
              (a : (i : Fin i) → M) → ⨁ (n : ℕ), ⨂[R]^n M)
            x :
          ⨁ (n : ℕ), ⨂[R]^n M) :
        (a : ℕ) → ⨂[R]^a M)
      i_1

Tactic:
simp [DirectSum.lof_eq_of, -tprod_apply, toDirectSum_tensorPower_tprod]

Premises used: TensorAlgebra.toDirectSum_tensorPower_tprod, DirectSum.lof_eq_of, TensorAlgebra.tprod_apply
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : ⨁ (n : ℕ), ⨂[R]^n M
⊢ (toDirectSum : (a : TensorAlgebra R M) → ⨁ (n : ℕ), ⨂[R]^n M)
      ((ofDirectSum : (a : ⨁ (n : ℕ), ⨂[R]^n M) → TensorAlgebra R M) x) =
    x

Tactic:
AlgHom.congr_fun toDirectSum_comp_ofDirectSum x

Premises used: TensorAlgebra.toDirectSum_comp_ofDirectSum, AlgHom.congr_fun, Trunc.lift
-- 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
ιι : Type u_3
ι : ιι → Type u_4
ai : ιι
a : ⨂[R] (x : ι ai), M
bi : ιι
b : ⨂[R] (x : ι bi), M
hi : ai = bi
h : (reindex R (fun (x : ι ai) ↦ M) (Equiv.cast ⋯) : (a : ⨂[R] (i : ι ai), M) → ⨂[R] (i : ι bi), M) a = b
subst :
  ∀ (b : ⨂[R] (x : ι ai), M)
    (h : (reindex R (fun (x : ι ai) ↦ M) (Equiv.cast ⋯) : (a : ⨂[R] (i : ι ai), M) → ⨂[R] (i : ι ai), M) a = b),
    Eq (α := GradedMonoid fun (ii : ιι) ↦ ⨂[R] (x : ι ii), M) (Sigma.mk (β := fun (ii : ιι) ↦ ⨂[R] (x : ι ii), M) ai a)
      (Sigma.mk (β := fun (ii : ιι) ↦ ⨂[R] (x : ι ii), M) ai b)
⊢ Eq (α := GradedMonoid fun (ii : ιι) ↦ ⨂[R] (x : ι ii), M) (Sigma.mk (β := fun (ii : ιι) ↦ ⨂[R] (x : ι ii), M) ai a)
    (Sigma.mk (β := fun (ii : ιι) ↦ ⨂[R] (x : ι ii), M) bi b)

Tactic:
subst hi
-- 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
ιι : Type u_3
ι : ιι → Type u_4
ai : ιι
a b : ⨂[R] (x : ι ai), M
h : (reindex R (fun (x : ι ai) ↦ M) (Equiv.cast ⋯) : (a : ⨂[R] (i : ι ai), M) → ⨂[R] (i : ι ai), M) a = b
⊢ Eq (α := GradedMonoid fun (ii : ιι) ↦ ⨂[R] (x : ι ii), M) (Sigma.mk (β := fun (ii : ιι) ↦ ⨂[R] (x : ι ii), M) ai a)
    (Sigma.mk (β := fun (ii : ιι) ↦ ⨂[R] (x : ι ii), M) ai b)

Tactic:
simp_all
-- 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
⊢ Eq (α := ⨂[R]^0 M) (@GradedMonoid.GOne.one _ (fun (i : ℕ) ↦ ⨂[R]^i M) MulZeroClass.toZero _ : ⨂[R]^0 M)
    ((tprod R (s := fun (i : Fin 0) ↦ M) : (a : (i : Fin 0) → M) → ⨂[R] (i : Fin 0), M) Fin.elim0 : ⨂[R] (i : Fin 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
i j : ℕ
a : ⨂[R]^i M
b : ⨂[R]^j M
⊢ Eq (α := ⨂[R]^(i + j) M) (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ _ _ a b : ⨂[R]^(i + j) M)
    ((mulEquiv : (a : ⨂[R]^i M ⊗[R] ⨂[R]^j M) → ⨂[R]^(i + j) M) (a ⊗ₜ[R] b) : ⨂[R]^(i + j) M)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, TensorProduct.tmul, AddCon.toQuotient, 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
i j : ℕ
a : ⨂[R]^i M
b : ⨂[R]^j M
⊢ Eq (α := ⨂[R]^(i + j) M) (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ _ _ a b : ⨂[R]^(i + j) M)
    ((((LinearMap.compr₂ (TensorProduct.mk R (⨂[R]^i M) (⨂[R]^j M))
                  (↑mulEquiv : ⨂[R]^i M ⊗[R] ⨂[R]^j M →ₗ[R] ⨂[R]^(i + j) M) :
                (a : ⨂[R]^i M) → ⨂[R]^j M →ₗ[R] ⨂[R]^(i + j) M)
              a :
            ⨂[R]^j M →ₗ[R] ⨂[R]^(i + j) M) :
          (a : ⨂[R]^j M) → ⨂[R]^(i + j) M)
        b :
      ⨂[R]^(i + j) 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
i j : ℕ
h : i = j
a : Fin i → M
⊢ Eq (α := ⨂[R]^j M)
    ((cast R M h : (a : ⨂[R]^i M) → ⨂[R]^j M)
        ((tprod R (s := fun (x : Fin i) ↦ M) : (a : (i : Fin i) → M) → ⨂[R] (i : Fin i), M) a) :
      ⨂[R]^j M)
    ((tprod R (s := fun (a : Fin j) ↦ M) : (a : (i : Fin j) → M) → ⨂[R] (i : Fin j), M) (a ∘ Fin.cast ⋯) :
      ⨂[R] (i : Fin j), M)

Tactic:
reindex_tprod _ _

Premises used: PiTensorProduct.reindex_tprod
-- 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
i : ℕ
h : i = i
⊢ Eq (α := ⨂[R]^i M ≃ₗ[R] ⨂[R]^i M) (cast R M h) (LinearEquiv.refl R (⨂[R]^i M))

Tactic:
(congr_arg (reindex R fun _ ↦ M) <| finCongr_refl h).trans reindex_refl

Premises used: PiTensorProduct.reindex_refl, PiTensorProduct.reindex, congr_arg, finCongr_refl, Eq.trans, TensorPower.cast
-- 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
i j : ℕ
h : i = j
⊢ Eq (α := ⨂[R]^j M ≃ₗ[R] ⨂[R]^i M) (LinearEquiv.symm (cast R M h)) (cast R M ⋯)

Tactic:
reindex_symm _

Premises used: finCongr, PiTensorProduct.reindex_symm, Equiv.symm, TensorPower.cast
-- 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
i j k : ℕ
h : i = j
h' : j = k
⊢ Eq (α := ⨂[R]^i M ≃ₗ[R] ⨂[R]^k M) (cast R M h ≪≫ₗ cast R M h') (cast R M ⋯)

Tactic:
reindex_trans _ _

Premises used: finCongr, PiTensorProduct.reindex_trans, TensorPower.cast
-- 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
i j k : ℕ
h : i = j
h' : j = k
a : ⨂[R]^i M
⊢ Eq (α := ⨂[R]^k M) ((cast R M h' : (a : ⨂[R]^j M) → ⨂[R]^k M) ((cast R M h : (a : ⨂[R]^i M) → ⨂[R]^j M) a) : ⨂[R]^k M)
    ((cast R M ⋯ : (a : ⨂[R]^i M) → ⨂[R]^k M) a : ⨂[R]^k M)

Tactic:
reindex_reindex _ _ _

Premises used: PiTensorProduct.reindex_reindex
-- 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
a b : GradedMonoid fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M
h : a.fst (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M) = b.fst (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)
h2 :
  (cast R M h : (a : ⨂[R]^a.fst M) → ⨂[R]^b.fst M) (a.snd (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)) =
    b.snd (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)
⊢ a = b

Tactic:
gradedMonoid_eq_of_reindex_cast h ?_

Premises used: PiTensorProduct.gradedMonoid_eq_of_reindex_cast
-- 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
a b : GradedMonoid fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M
h : a.fst (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M) = b.fst (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)
h2 :
  (cast R M h : (a : ⨂[R]^a.fst M) → ⨂[R]^b.fst M) (a.snd (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)) =
    b.snd (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)
refine :
  (reindex R (fun (x : Fin (a.fst (β := fun (ii : ℕ) ↦ ⨂[R] (x : Fin ii), M))) ↦ M) (Equiv.cast ⋯) :
        (a : ⨂[R] (i : Fin a.fst), M) → ⨂[R] (i : Fin b.fst), M)
      (a.snd (β := fun (ii : ℕ) ↦ ⨂[R] (x : Fin ii), M)) =
    b.snd (β := fun (ii : ℕ) ↦ ⨂[R] (x : Fin ii), M)
⊢ a = b

Tactic:
refine gradedMonoid_eq_of_reindex_cast h ?_

Premises used: PiTensorProduct.gradedMonoid_eq_of_reindex_cast
-- 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
a b : GradedMonoid fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M
h : a.fst (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M) = b.fst (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)
h2 :
  (cast R M h : (a : ⨂[R]^a.fst M) → ⨂[R]^b.fst M) (a.snd (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)) =
    b.snd (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)
⊢ (reindex R (fun (x : Fin (a.fst (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M))) ↦ M) (finCongr h) :
        (a : ⨂[R]^a.fst M) → ⨂[R]^b.fst M)
      (a.snd (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)) =
    b.snd (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)

Tactic:
rw [cast] at h2

Premises used: TensorPower.cast
-- 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
a b : GradedMonoid fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M
h : a.fst (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M) = b.fst (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)
h2 :
  (reindex R (fun (x : Fin (a.fst (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M))) ↦ M) (finCongr h) :
        (a : ⨂[R]^a.fst M) → ⨂[R]^b.fst M)
      (a.snd (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)) =
    b.snd (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)
rw :
  (reindex R (fun (x : Fin (a.fst (β := fun (ii : ℕ) ↦ ⨂[R] (x : Fin ii), M))) ↦ M) (finCongr h) :
        (a : ⨂[R] (i : Fin a.fst), M) → ⨂[R] (i : Fin b.fst), M)
      (a.snd (β := fun (ii : ℕ) ↦ ⨂[R] (x : Fin ii), M)) =
    b.snd (β := fun (ii : ℕ) ↦ ⨂[R] (x : Fin ii), M)
rw₁ : a.fst (β := fun (ii : ℕ) ↦ ⨂[R] (x : Fin ii), M) = b.fst (β := fun (ii : ℕ) ↦ ⨂[R] (x : Fin ii), M)
rw₂ :
  Eq (α := ⨂[R] (i : Fin (b.fst (β := fun (ii : ℕ) ↦ ⨂[R] (x : Fin ii), M))), M)
    ((reindex R (fun (x : Fin (a.fst (β := fun (ii : ℕ) ↦ ⨂[R] (x : Fin ii), M))) ↦ M) (finCongr h) :
          (a : ⨂[R] (i : Fin a.fst), M) → ⨂[R] (i : Fin b.fst), M)
        (a.snd (β := fun (ii : ℕ) ↦ ⨂[R] (x : Fin ii), M)) :
      ⨂[R] (i : Fin (b.fst (β := fun (ii : ℕ) ↦ ⨂[R] (x : Fin ii), M))), M)
    ((reindex R (fun (x : Fin (a.fst (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M))) ↦ M) (finCongr h) :
          (a : ⨂[R]^a.fst M) → ⨂[R]^b.fst M)
        (a.snd (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)) :
      ⨂[R]^(b.fst (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)) M)
rw₃ : a.fst (β := fun (ii : ℕ) ↦ ⨂[R] (x : Fin ii), M) = b.fst (β := fun (ii : ℕ) ↦ ⨂[R] (x : Fin ii), M)
rw₄ :
  Eq (α := ⨂[R] (i : Fin (b.fst (β := fun (ii : ℕ) ↦ ⨂[R] (x : Fin ii), M))), M)
    ((reindex R (fun (x : Fin (a.fst (β := fun (ii : ℕ) ↦ ⨂[R] (x : Fin ii), M))) ↦ M) (finCongr h) :
          (a : ⨂[R] (i : Fin a.fst), M) → ⨂[R] (i : Fin b.fst), M)
        (a.snd (β := fun (ii : ℕ) ↦ ⨂[R] (x : Fin ii), M)) :
      ⨂[R] (i : Fin (b.fst (β := fun (ii : ℕ) ↦ ⨂[R] (x : Fin ii), M))), M)
    ((reindex R (fun (x : Fin (a.fst (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M))) ↦ M) (finCongr h) :
          (a : ⨂[R]^a.fst M) → ⨂[R]^b.fst M)
        (a.snd (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)) :
      ⨂[R]^(b.fst (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)) M)
rw₅ : a.fst (β := fun (ii : ℕ) ↦ ⨂[R] (x : Fin ii), M) = b.fst (β := fun (ii : ℕ) ↦ ⨂[R] (x : Fin ii), M)
⊢ (reindex R (fun (x : Fin (a.fst (β := fun (ii : ℕ) ↦ ⨂[R] (x : Fin ii), M))) ↦ M) (Equiv.cast ⋯) :
        (a : ⨂[R] (i : Fin a.fst), M) → ⨂[R] (i : Fin b.fst), M)
      (a.snd (β := fun (ii : ℕ) ↦ ⨂[R] (x : Fin ii), M)) =
    b.snd (β := fun (ii : ℕ) ↦ ⨂[R] (x : Fin ii), M)

Tactic:
rw [← finCongr_eq_equivCast, ← h2]

Premises used: finCongr_eq_equivCast
-- 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
i j : ℕ
h : i = j
subst :
  Eq (α := (a : ⨂[R]^i M) → ⨂[R]^i M) ((⇑(cast R M ⋯) : (a : ⨂[R]^i M) → ⨂[R]^i M) : (a : ⨂[R]^i M) → ⨂[R]^i M)
    (_root_.cast ⋯ : (a : (fun (i : ℕ) ↦ ⨂[R]^i M) i) → (fun (i : ℕ) ↦ ⨂[R]^i M) i)
⊢ Eq (α := (a : ⨂[R]^i M) → ⨂[R]^j M) ((⇑(cast R M h) : (a : ⨂[R]^i M) → ⨂[R]^j M) : (a : ⨂[R]^i M) → ⨂[R]^j M)
    (_root_.cast ⋯ : (a : (fun (i : ℕ) ↦ ⨂[R]^i M) i) → (fun (i : ℕ) ↦ ⨂[R]^i M) j)

Tactic:
subst h