awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basis
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
ℬ : Basis ι R M
⊢ Function.Injective (α := ι →₀ N) (β := M ⊗[R] N)
    (⇑((Finsupp.lsum R : (a : ι → N →ₗ[R] M ⊗[R] N) → (ι →₀ N) →ₗ[R] M ⊗[R] N) fun (i : ι) ↦
          (mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) ((ℬ : (a : ι) → M) i)) :
      (a : ι →₀ N) → M ⊗[R] N)

Tactic:
have := Classical.decEq ι
  (equivFinsuppOfBasisLeft_symm (N := N) ℬ).symm ▸
    (TensorProduct.equivFinsuppOfBasisLeft ℬ).symm.injective

Premises used: LinearEquiv.symm, TensorProduct.equivFinsuppOfBasisLeft_symm, Eq.rec, TensorProduct.equivFinsuppOfBasisLeft, LinearEquiv.injective, Eq.symm, Classical.decEq
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basis
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
ℬ : Basis ι R M
b : ι →₀ N
h : Eq (α := M ⊗[R] N) (b.sum fun (i : ι) (n : N) ↦ (ℬ : (a : ι) → M) i ⊗ₜ[R] n) 0
this : DecidableEq ι
⊢ Eq (α := M ⊗[R] N) ((LinearEquiv.symm (equivFinsuppOfBasisLeft ℬ) : (a : ι →₀ N) → M ⊗[R] N) b : M ⊗[R] N)
    ((LinearEquiv.symm (equivFinsuppOfBasisLeft ℬ) : (a : ι →₀ N) → M ⊗[R] N) 0 : M ⊗[R] N)

Tactic:
simpa
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basis
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : AddCommMonoid N
inst_8 : Module R N
inst_9 : Free S M
inst_10 : Free R N
⊢ Free S (M ⊗[R] N)

Tactic:
let ⟨bM⟩ := exists_basis (R := S) (M := M)
  let ⟨bN⟩ := exists_basis (R := R) (M := N)
  of_basis (bM.2.tensorProduct bN.2)

Premises used: _private.0.Module.Free.tensor.match_1, Module.Free, Module.Free.of_basis, Module.Basis.tensorProduct, Module.Free.exists_basis, TensorProduct, Sigma.snd, _private.0.Module.Free.tensor.match_2
-- Module: Mathlib.LinearAlgebra.TensorProduct.Decomposition
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
S : Type u_4
inst : DecidableEq ι
inst_1 : CommSemiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
ℳ : ι → Submodule R M
inst_4 : CommSemiring S
inst_5 : Algebra R S
inst_6 : Decomposition ℳ
refine_1 :
  Eq (α := S ⊗[R] M →ₗ[S] S ⊗[R] M)
    ((coeLinearMap fun (i : ι) ↦ Submodule.baseChange S (ℳ i)) ∘ₗ
      (lmap (M := fun (x : ι) ↦ TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ x)) (N := fun (i : ι) ↦
            ↥(Submodule.baseChange S (ℳ i))) fun (x : ι) ↦ Submodule.toBaseChange S (ℳ x) :
          (⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) →ₗ[S] ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i))) ∘ₗ
        (((↑(directSumRight R S S fun (i : ι) ↦ ↥(ℳ i)) :
                (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) :
              (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) ∘ₗ
            ((↑(LinearEquiv.baseChange R S M (⨁ (i : ι), ↥(ℳ i)) (decomposeLinearEquiv ℳ)) :
                S ⊗[R] M →ₗ[S] S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) :
              S ⊗[R] M →ₗ[S] S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) :
          S ⊗[R] M →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)))
    LinearMap.id
refine_2 :
  Eq (α := (⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i))) →ₗ[S] ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i)))
    (((lmap (M := fun (x : ι) ↦ TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ x)) (N := fun (i : ι) ↦
            ↥(Submodule.baseChange S (ℳ i))) fun (x : ι) ↦ Submodule.toBaseChange S (ℳ x) :
          (⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) →ₗ[S] ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i))) ∘ₗ
        (((↑(directSumRight R S S fun (i : ι) ↦ ↥(ℳ i)) :
                (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) :
              (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) ∘ₗ
            ((↑(LinearEquiv.baseChange R S M (⨁ (i : ι), ↥(ℳ i)) (decomposeLinearEquiv ℳ)) :
                S ⊗[R] M →ₗ[S] S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) :
              S ⊗[R] M →ₗ[S] S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) :
          S ⊗[R] M →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i))) ∘ₗ
      coeLinearMap fun (i : ι) ↦ Submodule.baseChange S (ℳ i))
    LinearMap.id
⊢ Decomposition (σ := Submodule S (S ⊗[R] M)) fun (i : ι) ↦ Submodule.baseChange S (ℳ i)

Tactic:
refine .ofLinearMap _ (lmap (ℳ · |>.toBaseChange S) ∘ₗ
    (directSumRight R S S fun i ↦ ℳ i).toLinearMap ∘ₗ
    ((decomposeLinearEquiv ℳ).baseChange R S)) ?_ ?_
-- Module: Mathlib.LinearAlgebra.TensorProduct.Decomposition
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
S : Type u_4
inst : DecidableEq ι
inst_1 : CommSemiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
ℳ : ι → Submodule R M
inst_4 : CommSemiring S
inst_5 : Algebra R S
inst_6 : Decomposition ℳ
refine_1 :
  Eq (α := (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] S ⊗[R] M)
    (((coeLinearMap fun (i : ι) ↦ Submodule.baseChange S (ℳ i)) ∘ₗ
            lmap (M := fun (x : ι) ↦ TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ x)) (N := fun (i : ι) ↦
              ↥(Submodule.baseChange S (ℳ i))) fun (x : ι) ↦ Submodule.toBaseChange S (ℳ x) :
          (⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) →ₗ[S] S ⊗[R] M) ∘ₗ
        ((↑(directSumRight R S S fun (i : ι) ↦ ↥(ℳ i)) :
            (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) :
          (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) :
      (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] S ⊗[R] M)
    (LinearMap.id ∘ₗ
        (↑(LinearEquiv.symm (LinearEquiv.baseChange R S M (⨁ (i : ι), ↥(ℳ i)) (decomposeLinearEquiv ℳ))) :
          (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] S ⊗[R] M) :
      (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] S ⊗[R] M)
⊢ Eq (α := S ⊗[R] M →ₗ[S] S ⊗[R] M)
    ((((coeLinearMap fun (i : ι) ↦ Submodule.baseChange S (ℳ i)) ∘ₗ
              lmap (M := fun (x : ι) ↦ TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ x)) (N := fun (i : ι) ↦
                ↥(Submodule.baseChange S (ℳ i))) fun (x : ι) ↦ Submodule.toBaseChange S (ℳ x) :
            (⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) →ₗ[S] S ⊗[R] M) ∘ₗ
          ((↑(directSumRight R S S fun (i : ι) ↦ ↥(ℳ i)) :
              (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) :
            (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) :
        (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] S ⊗[R] M) ∘ₗ
      ((↑(LinearEquiv.baseChange R S M (⨁ (i : ι), ↥(ℳ i)) (decomposeLinearEquiv ℳ)) :
          S ⊗[R] M →ₗ[S] S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) :
        S ⊗[R] M →ₗ[S] S ⊗[R] ⨁ (i : ι), ↥(ℳ i)))
    LinearMap.id

Tactic:
rw [← LinearEquiv.eq_comp_toLinearMap_symm]

Premises used: LinearEquiv.eq_comp_toLinearMap_symm
-- Module: Mathlib.LinearAlgebra.TensorProduct.Decomposition
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
S : Type u_4
inst : DecidableEq ι
inst_1 : CommSemiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
ℳ : ι → Submodule R M
inst_4 : CommSemiring S
inst_5 : Algebra R S
inst_6 : Decomposition ℳ
refine_1 :
  ∀ (i : ι) (x : ↥(ℳ i)),
    Eq (α := S ⊗[R] M)
      (((((AlgebraTensorModule.curry
                        (((coeLinearMap fun (i : ι) ↦ Submodule.baseChange S (ℳ i)) ∘ₗ
                              lmap (M := fun (x : ι) ↦ TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ x)) (N := fun (i : ι) ↦
                                ↥(Submodule.baseChange S (ℳ i))) fun (x : ι) ↦ Submodule.toBaseChange S (ℳ x) :
                            (⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) →ₗ[S] S ⊗[R] M) ∘ₗ
                          ((↑(directSumRight R S S fun (i : ι) ↦ ↥(ℳ i)) :
                              (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) :
                            (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i))) :
                      S →ₗ[S] (⨁ (i : ι), ↥(ℳ i)) →ₗ[R] S ⊗[R] M) :
                    (a : S) → (⨁ (i : ι), ↥(ℳ i)) →ₗ[R] S ⊗[R] M)
                  1 ∘ₗ
                lof.{u_2, u_1, u_3} R ι (fun (i : ι) ↦ ↥(ℳ i)) i :
              ↥(ℳ i) →ₗ[R] S ⊗[R] M) :
            (a : ↥(ℳ i)) → S ⊗[R] M)
          x :
        S ⊗[R] M)
      (((((AlgebraTensorModule.curry
                        (LinearMap.id ∘ₗ
                          (↑(LinearEquiv.symm
                                (LinearEquiv.baseChange R S M (⨁ (i : ι), ↥(ℳ i)) (decomposeLinearEquiv ℳ))) :
                            (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] S ⊗[R] M)) :
                      S →ₗ[S] (⨁ (i : ι), ↥(ℳ i)) →ₗ[R] S ⊗[R] M) :
                    (a : S) → (⨁ (i : ι), ↥(ℳ i)) →ₗ[R] S ⊗[R] M)
                  1 ∘ₗ
                lof.{u_2, u_1, u_3} R ι (fun (i : ι) ↦ ↥(ℳ i)) i :
              ↥(ℳ i) →ₗ[R] S ⊗[R] M) :
            (a : ↥(ℳ i)) → S ⊗[R] M)
          x :
        S ⊗[R] M)
⊢ Eq (α := (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] S ⊗[R] M)
    (((coeLinearMap fun (i : ι) ↦ Submodule.baseChange S (ℳ i)) ∘ₗ
            lmap (M := fun (x : ι) ↦ TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ x)) (N := fun (i : ι) ↦
              ↥(Submodule.baseChange S (ℳ i))) fun (x : ι) ↦ Submodule.toBaseChange S (ℳ x) :
          (⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) →ₗ[S] S ⊗[R] M) ∘ₗ
        ((↑(directSumRight R S S fun (i : ι) ↦ ↥(ℳ i)) :
            (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) :
          (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) :
      (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] S ⊗[R] M)
    (LinearMap.id ∘ₗ
        (↑(LinearEquiv.symm (LinearEquiv.baseChange R S M (⨁ (i : ι), ↥(ℳ i)) (decomposeLinearEquiv ℳ))) :
          (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] S ⊗[R] M) :
      (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] S ⊗[R] M)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.TensorProduct.Decomposition
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
S : Type u_4
inst : DecidableEq ι
inst_1 : CommSemiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
ℳ : ι → Submodule R M
inst_4 : CommSemiring S
inst_5 : Algebra R S
inst_6 : Decomposition ℳ
i : ι
x : ↥(ℳ i)
⊢ Eq (α := S ⊗[R] M)
    (((((AlgebraTensorModule.curry
                      (((coeLinearMap fun (i : ι) ↦ Submodule.baseChange S (ℳ i)) ∘ₗ
                            lmap (M := fun (x : ι) ↦ TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ x)) (N := fun (i : ι) ↦
                              ↥(Submodule.baseChange S (ℳ i))) fun (x : ι) ↦ Submodule.toBaseChange S (ℳ x) :
                          (⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) →ₗ[S] S ⊗[R] M) ∘ₗ
                        ((↑(directSumRight R S S fun (i : ι) ↦ ↥(ℳ i)) :
                            (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) :
                          (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i))) :
                    S →ₗ[S] (⨁ (i : ι), ↥(ℳ i)) →ₗ[R] S ⊗[R] M) :
                  (a : S) → (⨁ (i : ι), ↥(ℳ i)) →ₗ[R] S ⊗[R] M)
                1 ∘ₗ
              lof.{u_2, u_1, u_3} R ι (fun (i : ι) ↦ ↥(ℳ i)) i :
            ↥(ℳ i) →ₗ[R] S ⊗[R] M) :
          (a : ↥(ℳ i)) → S ⊗[R] M)
        x :
      S ⊗[R] M)
    (((((AlgebraTensorModule.curry
                      (LinearMap.id ∘ₗ
                        (↑(LinearEquiv.symm
                              (LinearEquiv.baseChange R S M (⨁ (i : ι), ↥(ℳ i)) (decomposeLinearEquiv ℳ))) :
                          (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] S ⊗[R] M)) :
                    S →ₗ[S] (⨁ (i : ι), ↥(ℳ i)) →ₗ[R] S ⊗[R] M) :
                  (a : S) → (⨁ (i : ι), ↥(ℳ i)) →ₗ[R] S ⊗[R] M)
                1 ∘ₗ
              lof.{u_2, u_1, u_3} R ι (fun (i : ι) ↦ ↥(ℳ i)) i :
            ↥(ℳ i) →ₗ[R] S ⊗[R] M) :
          (a : ↥(ℳ i)) → S ⊗[R] M)
        x :
      S ⊗[R] M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Decomposition
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
S : Type u_4
inst : DecidableEq ι
inst_1 : CommSemiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
ℳ : ι → Submodule R M
inst_4 : CommSemiring S
inst_5 : Algebra R S
inst_6 : Decomposition ℳ
refine_2 :
  ∀ (i : ι),
    Eq (α := ↥(Submodule.baseChange S (ℳ i)) →ₗ[S] ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i)))
      ((((lmap (M := fun (x : ι) ↦ TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ x)) (N := fun (i : ι) ↦
                  ↥(Submodule.baseChange S (ℳ i))) fun (x : ι) ↦ Submodule.toBaseChange S (ℳ x) :
                (⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) →ₗ[S]
                  ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i))) ∘ₗ
              (((↑(directSumRight R S S fun (i : ι) ↦ ↥(ℳ i)) :
                      (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) :
                    (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) ∘ₗ
                  ((↑(LinearEquiv.baseChange R S M (⨁ (i : ι), ↥(ℳ i)) (decomposeLinearEquiv ℳ)) :
                      S ⊗[R] M →ₗ[S] S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) :
                    S ⊗[R] M →ₗ[S] S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) :
                S ⊗[R] M →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i))) ∘ₗ
            coeLinearMap fun (i : ι) ↦ Submodule.baseChange S (ℳ i)) ∘ₗ
          lof S ι (fun (i : ι) ↦ ↥(Submodule.baseChange S (ℳ i))) i :
        ↥(Submodule.baseChange S (ℳ i)) →ₗ[S] ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i)))
      (LinearMap.id ∘ₗ lof S ι (fun (i : ι) ↦ ↥(Submodule.baseChange S (ℳ i))) i :
        ↥(Submodule.baseChange S (ℳ i)) →ₗ[S] ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i)))
⊢ Eq (α := (⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i))) →ₗ[S] ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i)))
    (((lmap (M := fun (x : ι) ↦ TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ x)) (N := fun (i : ι) ↦
            ↥(Submodule.baseChange S (ℳ i))) fun (x : ι) ↦ Submodule.toBaseChange S (ℳ x) :
          (⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) →ₗ[S] ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i))) ∘ₗ
        (((↑(directSumRight R S S fun (i : ι) ↦ ↥(ℳ i)) :
                (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) :
              (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) ∘ₗ
            ((↑(LinearEquiv.baseChange R S M (⨁ (i : ι), ↥(ℳ i)) (decomposeLinearEquiv ℳ)) :
                S ⊗[R] M →ₗ[S] S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) :
              S ⊗[R] M →ₗ[S] S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) :
          S ⊗[R] M →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i))) ∘ₗ
      coeLinearMap fun (i : ι) ↦ Submodule.baseChange S (ℳ i))
    LinearMap.id

Tactic:
ext : 1
-- Module: Mathlib.LinearAlgebra.TensorProduct.Decomposition
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
S : Type u_4
inst : DecidableEq ι
inst_1 : CommSemiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
ℳ : ι → Submodule R M
inst_4 : CommSemiring S
inst_5 : Algebra R S
inst_6 : Decomposition ℳ
i : ι
x : ↥(ℳ i)
⊢ Eq (α := ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i)))
    ((((AlgebraTensorModule.curry
                  (((((lmap (M := fun (x : ι) ↦ TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ x)) (N := fun (i : ι) ↦
                                ↥(Submodule.baseChange S (ℳ i))) fun (x : ι) ↦ Submodule.toBaseChange S (ℳ x) :
                              (⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) →ₗ[S]
                                ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i))) ∘ₗ
                            (((↑(directSumRight R S S fun (i : ι) ↦ ↥(ℳ i)) :
                                    (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S]
                                      ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) :
                                  (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S]
                                    ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) ∘ₗ
                                ((↑(LinearEquiv.baseChange R S M (⨁ (i : ι), ↥(ℳ i)) (decomposeLinearEquiv ℳ)) :
                                    S ⊗[R] M →ₗ[S] S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) :
                                  S ⊗[R] M →ₗ[S] S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) :
                              S ⊗[R] M →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i))) ∘ₗ
                          coeLinearMap fun (i : ι) ↦ Submodule.baseChange S (ℳ i)) ∘ₗ
                        lof S ι (fun (i : ι) ↦ ↥(Submodule.baseChange S (ℳ i))) i :
                      ↥(Submodule.baseChange S (ℳ i)) →ₗ[S] ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i))) ∘ₗ
                    (Submodule.toBaseChange S (ℳ i) :
                      TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i) →ₗ[S] ↥(Submodule.baseChange S (ℳ i)))) :
                S →ₗ[S] ↥(ℳ i) →ₗ[R] ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i))) :
              (a : S) → ↥(ℳ i) →ₗ[R] ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i)))
            1 :
          (a : ↥(ℳ i)) → ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i)))
        x :
      ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i)))
    ((((AlgebraTensorModule.curry
                  ((LinearMap.id ∘ₗ lof S ι (fun (i : ι) ↦ ↥(Submodule.baseChange S (ℳ i))) i) ∘ₗ
                    Submodule.toBaseChange S (ℳ i)) :
                S →ₗ[S] ↥(ℳ i) →ₗ[R] ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i))) :
              (a : S) → ↥(ℳ i) →ₗ[R] ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i)))
            1 :
          (a : ↥(ℳ i)) → ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i)))
        x :
      ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i)))

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Decomposition
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
S : Type u_4
inst : DecidableEq ι
inst_1 : CommSemiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
ℳ : ι → Submodule R M
inst_4 : CommSemiring S
inst_5 : Algebra R S
inst_6 : Decomposition ℳ
i : ι
x y : TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)
h :
  Eq (α := ↥(Submodule.baseChange S (ℳ i)))
    ((Submodule.toBaseChange S (ℳ i) : (a : S ⊗[R] ↥(ℳ i)) → ↥(Submodule.baseChange S (ℳ i))) x :
      ↥(Submodule.baseChange S (ℳ i)))
    ((Submodule.toBaseChange S (ℳ i) : (a : S ⊗[R] ↥(ℳ i)) → ↥(Submodule.baseChange S (ℳ i))) y :
      ↥(Submodule.baseChange S (ℳ i)))
⊢ Function.Bijective (α := S ⊗[R] M) (β := ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i))
    (⇑((↑(LinearEquiv.trans (LinearEquiv.baseChange R S M (⨁ (i : ι), ↥(ℳ i)) (decomposeLinearEquiv ℳ))
                (directSumRight R S S fun (i : ι) ↦ ↥(ℳ i))) :
            S ⊗[R] M →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) :
          S ⊗[R] M →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) :
      (a : S ⊗[R] M) → ⨁ (i : ι), S ⊗[R] ↥(ℳ i))

Tactic:
LinearEquiv.bijective _

Premises used: LinearEquiv.bijective
-- Module: Mathlib.LinearAlgebra.TensorProduct.Decomposition
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
S : Type u_4
inst : DecidableEq ι
inst_1 : CommSemiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
ℳ : ι → Submodule R M
inst_4 : CommSemiring S
inst_5 : Algebra R S
inst_6 : Decomposition ℳ
i : ι
x y : TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)
h :
  Eq (α := ↥(Submodule.baseChange S (ℳ i)))
    ((Submodule.toBaseChange S (ℳ i) : (a : S ⊗[R] ↥(ℳ i)) → ↥(Submodule.baseChange S (ℳ i))) x :
      ↥(Submodule.baseChange S (ℳ i)))
    ((Submodule.toBaseChange S (ℳ i) : (a : S ⊗[R] ↥(ℳ i)) → ↥(Submodule.baseChange S (ℳ i))) y :
      ↥(Submodule.baseChange S (ℳ i)))
⊢ Function.Bijective (α := S ⊗[R] M) (β := ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i))
    (⇑((↑(LinearEquiv.trans (LinearEquiv.baseChange R S M (⨁ (i : ι), ↥(ℳ i)) (decomposeLinearEquiv ℳ))
                (directSumRight R S S fun (i : ι) ↦ ↥(ℳ i))) :
            S ⊗[R] M →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) :
          S ⊗[R] M →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) :
      (a : S ⊗[R] M) → ⨁ (i : ι), S ⊗[R] ↥(ℳ i))

Tactic:
exact LinearEquiv.bijective _

Premises used: LinearEquiv.bijective
-- Module: Mathlib.LinearAlgebra.TensorProduct.Decomposition
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
S : Type u_4
inst : DecidableEq ι
inst_1 : CommSemiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
ℳ : ι → Submodule R M
inst_4 : CommSemiring S
inst_5 : Algebra R S
inst_6 : Decomposition ℳ
i : ι
x y : TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)
h :
  Eq (α := ↥(Submodule.baseChange S (ℳ i)))
    ((Submodule.toBaseChange S (ℳ i) : (a : S ⊗[R] ↥(ℳ i)) → ↥(Submodule.baseChange S (ℳ i))) x :
      ↥(Submodule.baseChange S (ℳ i)))
    ((Submodule.toBaseChange S (ℳ i) : (a : S ⊗[R] ↥(ℳ i)) → ↥(Submodule.baseChange S (ℳ i))) y :
      ↥(Submodule.baseChange S (ℳ i)))
⊢ Function.Bijective (α := ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) (β :=
    ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i)))
    (⇑(lmap (M := fun (x : ι) ↦ TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ x)) (N := fun (x : ι) ↦
          ↥(Submodule.baseChange S (ℳ x))) fun (x : ι) ↦ Submodule.toBaseChange S (ℳ x)) :
      (a : ⨁ (i : ι), S ⊗[R] ↥(ℳ i)) → ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i)))

Tactic:
have := (Function.Bijective.of_comp_iff (lmap (ℳ · |>.toBaseChange S))
    (by rw [← LinearEquiv.coe_trans]; exact LinearEquiv.bijective _)).1
    (decompose (M := S ⊗[R] M) fun i ↦ (ℳ i).baseChange S).bijective
-- Module: Mathlib.LinearAlgebra.TensorProduct.Decomposition
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
S : Type u_4
inst : DecidableEq ι
inst_1 : CommSemiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
ℳ : ι → Submodule R M
inst_4 : CommSemiring S
inst_5 : Algebra R S
inst_6 : Decomposition ℳ
i : ι
x y : TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)
h :
  Eq (α := ↥(Submodule.baseChange S (ℳ i)))
    ((Submodule.toBaseChange S (ℳ i) : (a : S ⊗[R] ↥(ℳ i)) → ↥(Submodule.baseChange S (ℳ i))) x :
      ↥(Submodule.baseChange S (ℳ i)))
    ((Submodule.toBaseChange S (ℳ i) : (a : S ⊗[R] ↥(ℳ i)) → ↥(Submodule.baseChange S (ℳ i))) y :
      ↥(Submodule.baseChange S (ℳ i)))
this :
  Function.Bijective (α := ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) (β :=
    ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i)))
    (⇑(lmap (M := fun (x : ι) ↦ TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ x)) (N := fun (x : ι) ↦
          ↥(Submodule.baseChange S (ℳ x))) fun (x : ι) ↦ Submodule.toBaseChange S (ℳ x)) :
      (a : ⨁ (i : ι), S ⊗[R] ↥(ℳ i)) → ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i)))
⊢ x = y

Tactic:
of_injective (β := fun i ↦ S ⊗[R] ℳ i) i <| this.injective ?_

Premises used: Function.Bijective.injective, DirectSum.of_injective