awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangePi
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
ι : Type u_3
N : ι → Type u_4
inst_3 : (i : ι) → AddCommMonoid (N i)
inst_4 : (i : ι) → Module.{u_1, u_4} R (N i)
P : ι → Type u_5
inst_5 : (i : ι) → AddCommMonoid (P i)
inst_6 : (i : ι) → Module.{u_1, u_5} R (P i)
inst_7 : (i : ι) → Module.{u_2, u_5} S (P i)
inst_8 : ∀ (i : ι), IsScalarTower.{u_1, u_2, u_5} R S (P i)
ε : (i : ι) → LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id R) (N i) (P i)
ibc : ∀ (i : ι), IsBaseChange S (ε i)
apply :
  ∀ (x : ⨁ (i : ι), N i),
    Eq (α := ⨁ (i : ι), P i)
      ((((directSumRight R S S N : (S ⊗[R] ⨁ (i : ι), N i) ≃ₗ[S] ⨁ (i : ι), TensorProduct.{u_1, u_2, u_4} R S (N i)) ≪≫ₗ
                (congrLinearEquiv (N := fun (i : ι) ↦ TensorProduct.{u_1, u_2, u_4} R S (N i)) (P := P) fun (i : ι) ↦
                    ⋯.equiv :
                  (⨁ (i : ι), TensorProduct.{u_1, u_2, u_4} R S (N i)) ≃ₗ[S] ⨁ (i : ι), P i) :
              (S ⊗[R] ⨁ (i : ι), N i) ≃ₗ[S] ⨁ (i : ι), P i) :
            (a : S ⊗[R] ⨁ (i : ι), N i) → ⨁ (i : ι), P i)
          (1 ⊗ₜ[R] x) :
        ⨁ (i : ι), P i)
      ((lmap (M := N) (N := P) ε : (a : ⨁ (i : ι), N i) → ⨁ (i : ι), P i) x : ⨁ (i : ι), P i)
⊢ IsBaseChange S (lmap (M := N) (N := P) ε)

Tactic:
apply of_equiv <| directSumRight R S S N ≪≫ₗ congrLinearEquiv fun i ↦ (ibc i).equiv

Premises used: TensorProduct.directSumRight, IsBaseChange.of_equiv, IsBaseChange.equiv, DirectSum.congrLinearEquiv
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangePi
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
ι : Type u_3
N : ι → Type u_4
inst_3 : (i : ι) → AddCommMonoid (N i)
inst_4 : (i : ι) → Module.{u_1, u_4} R (N i)
P : ι → Type u_5
inst_5 : (i : ι) → AddCommMonoid (P i)
inst_6 : (i : ι) → Module.{u_1, u_5} R (P i)
inst_7 : (i : ι) → Module.{u_2, u_5} S (P i)
inst_8 : ∀ (i : ι), IsScalarTower.{u_1, u_2, u_5} R S (P i)
ε : (i : ι) → LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id R) (N i) (P i)
ibc : ∀ (i : ι), IsBaseChange S (ε i)
x : ⨁ (i : ι), N i
w :
  ∀ (i : ι),
    (((((directSumRight R S S N : (S ⊗[R] ⨁ (i : ι), N i) ≃ₗ[S] ⨁ (i : ι), TensorProduct.{u_1, u_2, u_4} R S (N i)) ≪≫ₗ
                    (congrLinearEquiv (N := fun (i : ι) ↦ TensorProduct.{u_1, u_2, u_4} R S (N i)) (P := P)
                        fun (i : ι) ↦ ⋯.equiv :
                      (⨁ (i : ι), TensorProduct.{u_1, u_2, u_4} R S (N i)) ≃ₗ[S] ⨁ (i : ι), P i) :
                  (S ⊗[R] ⨁ (i : ι), N i) ≃ₗ[S] ⨁ (i : ι), P i) :
                (a : S ⊗[R] ⨁ (i : ι), N i) → ⨁ (i : ι), P i)
              (1 ⊗ₜ[R] x) :
            ⨁ (i : ι), P i) :
          (a : ι) → P a)
        i =
      (((lmap (M := N) (N := P) ε : (a : ⨁ (i : ι), N i) → ⨁ (i : ι), P i) x : ⨁ (i : ι), P i) : (a : ι) → P a) i
⊢ Eq (α := ⨁ (i : ι), P i)
    ((((directSumRight R S S N : (S ⊗[R] ⨁ (i : ι), N i) ≃ₗ[S] ⨁ (i : ι), TensorProduct.{u_1, u_2, u_4} R S (N i)) ≪≫ₗ
              (congrLinearEquiv (N := fun (i : ι) ↦ TensorProduct.{u_1, u_2, u_4} R S (N i)) (P := P) fun (i : ι) ↦
                  ⋯.equiv :
                (⨁ (i : ι), TensorProduct.{u_1, u_2, u_4} R S (N i)) ≃ₗ[S] ⨁ (i : ι), P i) :
            (S ⊗[R] ⨁ (i : ι), N i) ≃ₗ[S] ⨁ (i : ι), P i) :
          (a : S ⊗[R] ⨁ (i : ι), N i) → ⨁ (i : ι), P i)
        (1 ⊗ₜ[R] x) :
      ⨁ (i : ι), P i)
    ((lmap (M := N) (N := P) ε : (a : ⨁ (i : ι), N i) → ⨁ (i : ι), P i) x : ⨁ (i : ι), P i)

Tactic:
ext
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangePi
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
ι : Type u_3
N : ι → Type u_4
inst_3 : (i : ι) → AddCommMonoid (N i)
inst_4 : (i : ι) → Module.{u_1, u_4} R (N i)
P : ι → Type u_5
inst_5 : (i : ι) → AddCommMonoid (P i)
inst_6 : (i : ι) → Module.{u_1, u_5} R (P i)
inst_7 : (i : ι) → Module.{u_2, u_5} S (P i)
inst_8 : ∀ (i : ι), IsScalarTower.{u_1, u_2, u_5} R S (P i)
ε : (i : ι) → LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id R) (N i) (P i)
ibc : ∀ (i : ι), IsBaseChange S (ε i)
x : ⨁ (i : ι), N i
i : ι
⊢ (((((directSumRight R S S N : (S ⊗[R] ⨁ (i : ι), N i) ≃ₗ[S] ⨁ (i : ι), TensorProduct.{u_1, u_2, u_4} R S (N i)) ≪≫ₗ
                  (congrLinearEquiv (N := fun (i : ι) ↦ TensorProduct.{u_1, u_2, u_4} R S (N i)) (P := P) fun (i : ι) ↦
                      ⋯.equiv :
                    (⨁ (i : ι), TensorProduct.{u_1, u_2, u_4} R S (N i)) ≃ₗ[S] ⨁ (i : ι), P i) :
                (S ⊗[R] ⨁ (i : ι), N i) ≃ₗ[S] ⨁ (i : ι), P i) :
              (a : S ⊗[R] ⨁ (i : ι), N i) → ⨁ (i : ι), P i)
            (1 ⊗ₜ[R] x) :
          ⨁ (i : ι), P i) :
        (a : ι) → P a)
      i =
    (((lmap (M := N) (N := P) ε : (a : ⨁ (i : ι), N i) → ⨁ (i : ι), P i) x : ⨁ (i : ι), P i) : (a : ι) → P a) i

Tactic:
simp [coe_directSumRight, coe_congrLinearEquiv, equiv_tmul]

Premises used: IsBaseChange.equiv_tmul, TensorProduct.coe_directSumRight, DirectSum.coe_congrLinearEquiv
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangePi
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
ι : Type u_3
N : ι → Type u_4
inst_3 : (i : ι) → AddCommMonoid (N i)
inst_4 : (i : ι) → Module.{u_1, u_4} R (N i)
P : ι → Type u_5
inst_5 : (i : ι) → AddCommMonoid (P i)
inst_6 : (i : ι) → Module.{u_1, u_5} R (P i)
inst_7 : (i : ι) → Module.{u_2, u_5} S (P i)
inst_8 : ∀ (i : ι), IsScalarTower.{u_1, u_2, u_5} R S (P i)
ε : (i : ι) → LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id R) (N i) (P i)
ibc : ∀ (i : ι), IsBaseChange S (ε i)
apply apply₁ apply₂ :
  ∀ (x : ⨁ (i : ι), N i),
    Eq (α := ⨁ (i : ι), P i)
      ((((directSumRight R S S N : (S ⊗[R] ⨁ (i : ι), N i) ≃ₗ[S] ⨁ (i : ι), TensorProduct.{u_1, u_2, u_4} R S (N i)) ≪≫ₗ
                (congrLinearEquiv (N := fun (i : ι) ↦ TensorProduct.{u_1, u_2, u_4} R S (N i)) (P := P) fun (i : ι) ↦
                    ⋯.equiv :
                  (⨁ (i : ι), TensorProduct.{u_1, u_2, u_4} R S (N i)) ≃ₗ[S] ⨁ (i : ι), P i) :
              (S ⊗[R] ⨁ (i : ι), N i) ≃ₗ[S] ⨁ (i : ι), P i) :
            (a : S ⊗[R] ⨁ (i : ι), N i) → ⨁ (i : ι), P i)
          (1 ⊗ₜ[R] x) :
        ⨁ (i : ι), P i)
      ((lmap (M := N) (N := P) ε : (a : ⨁ (i : ι), N i) → ⨁ (i : ι), P i) x : ⨁ (i : ι), P i)
w :
  ∀ (x : ⨁ (i : ι), N i) (i : ι),
    (((((directSumRight R S S N : (S ⊗[R] ⨁ (i : ι), N i) ≃ₗ[S] ⨁ (i : ι), TensorProduct.{u_1, u_2, u_4} R S (N i)) ≪≫ₗ
                    (congrLinearEquiv (N := fun (i : ι) ↦ TensorProduct.{u_1, u_2, u_4} R S (N i)) (P := P)
                        fun (i : ι) ↦ ⋯.equiv :
                      (⨁ (i : ι), TensorProduct.{u_1, u_2, u_4} R S (N i)) ≃ₗ[S] ⨁ (i : ι), P i) :
                  (S ⊗[R] ⨁ (i : ι), N i) ≃ₗ[S] ⨁ (i : ι), P i) :
                (a : S ⊗[R] ⨁ (i : ι), N i) → ⨁ (i : ι), P i)
              (1 ⊗ₜ[R] x) :
            ⨁ (i : ι), P i) :
          (a : ι) → P a)
        i =
      (((lmap (M := N) (N := P) ε : (a : ⨁ (i : ι), N i) → ⨁ (i : ι), P i) x : ⨁ (i : ι), P i) : (a : ι) → P a) i
⊢ IsBaseChange S (lmap (M := N) (N := P) ε)

Tactic:
classical
  apply of_equiv <| directSumRight R S S N ≪≫ₗ congrLinearEquiv fun i ↦ (ibc i).equiv
  intros; ext
  simp [coe_directSumRight, coe_congrLinearEquiv, equiv_tmul]

Premises used: IsBaseChange.of_equiv, IsBaseChange.equiv_tmul, IsBaseChange.equiv, DirectSum.congrLinearEquiv, TensorProduct.coe_directSumRight, DirectSum.coe_congrLinearEquiv
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangePi
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
ι : Type u_3
M : Type u_6
M' : Type u_7
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M'
inst_5 : Module R M
inst_6 : Module R M'
inst_7 : Module S M'
inst_8 : IsScalarTower R S M'
ε : M →ₗ[R] M'
ibc : IsBaseChange S ε
⊢ IsBaseChange (R := R) (M := ⨁ (i : ι), M) (N := ⨁ (i : ι), M') S
    (lmap (M := fun (x : ι) ↦ M) (N := fun (x : ι) ↦ M') fun (x : ι) ↦ ε)

Tactic:
directSum (fun _ : ι ↦ ibc)

Premises used: IsBaseChange.directSum
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangePi
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
ι : Type u_3
M : Type u_6
M' : Type u_7
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M'
inst_5 : Module R M
inst_6 : Module R M'
inst_7 : Module S M'
inst_8 : IsScalarTower R S M'
ε : M →ₗ[R] M'
ibc : IsBaseChange S ε
apply :
  ∀ (x : ι →₀ M),
    Eq (α := ι →₀ M')
      ((LinearEquiv.baseChange R S (ι →₀ M) (⨁ (x : ι), M) (finsuppLEquivDirectSum R M ι) ≪≫ₗ
                equiv (f := lmap (M := fun (i : ι) ↦ M) (N := fun (i : ι) ↦ M') fun (x : ι) ↦ ε) ⋯ ≪≫ₗ
              LinearEquiv.symm (finsuppLEquivDirectSum S M' ι) :
            (a : S ⊗[R] (ι →₀ M)) → ι →₀ M')
          (1 ⊗ₜ[R] x) :
        ι →₀ M')
      ((Finsupp.mapRange.linearMap ε : (a : ι →₀ M) → ι →₀ M') x : ι →₀ M')
⊢ IsBaseChange (M := ι →₀ M) S (Finsupp.mapRange.linearMap ε)

Tactic:
apply of_equiv <|
    LinearEquiv.baseChange R S _ _ (finsuppLEquivDirectSum ..) ≪≫ₗ
      (directSum (fun _ ↦ ibc)).equiv ≪≫ₗ (finsuppLEquivDirectSum ..).symm

Premises used: LinearEquiv.symm, IsBaseChange.directSum, finsuppLEquivDirectSum, IsBaseChange.of_equiv, LinearEquiv.baseChange, IsBaseChange.equiv
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangePi
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
ι : Type u_3
M : Type u_6
M' : Type u_7
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M'
inst_5 : Module R M
inst_6 : Module R M'
inst_7 : Module S M'
inst_8 : IsScalarTower R S M'
ε : M →ₗ[R] M'
ibc : IsBaseChange S ε
x : ι →₀ M
rw :
  Eq (α := ⨁ (i : ι), M')
    ((LinearEquiv.baseChange R S (ι →₀ M) (⨁ (x : ι), M) (finsuppLEquivDirectSum R M ι) ≪≫ₗ
            equiv (f := lmap (M := fun (i : ι) ↦ M) (N := fun (i : ι) ↦ M') fun (x : ι) ↦ ε) ⋯ :
          (a : S ⊗[R] (ι →₀ M)) → ⨁ (i : ι), M')
        (1 ⊗ₜ[R] x) :
      ⨁ (i : ι), M')
    ((finsuppLEquivDirectSum S M' ι : (a : ι →₀ M') → ⨁ (i : ι), M') (Finsupp.mapRange (⇑ε : (a : M) → M') ⋯ x) :
      ⨁ (i : ι), M')
⊢ Eq (α := ι →₀ M')
    ((LinearEquiv.baseChange R S (ι →₀ M) (⨁ (x : ι), M) (finsuppLEquivDirectSum R M ι) ≪≫ₗ
              equiv (f := lmap (M := fun (i : ι) ↦ M) (N := fun (i : ι) ↦ M') fun (x : ι) ↦ ε) ⋯ ≪≫ₗ
            LinearEquiv.symm (finsuppLEquivDirectSum S M' ι) :
          (a : S ⊗[R] (ι →₀ M)) → ι →₀ M')
        (1 ⊗ₜ[R] x) :
      ι →₀ M')
    ((Finsupp.mapRange.linearMap ε : (a : ι →₀ M) → ι →₀ M') x : ι →₀ M')

Tactic:
rw [LinearEquiv.trans_apply, Finsupp.mapRange.linearMap_apply,
    LinearEquiv.symm_apply_eq]

Premises used: LinearEquiv.symm_apply_eq, LinearEquiv.trans_apply, Finsupp.mapRange.linearMap_apply
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangePi
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
ι : Type u_3
M : Type u_6
M' : Type u_7
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M'
inst_5 : Module R M
inst_6 : Module R M'
inst_7 : Module S M'
inst_8 : IsScalarTower R S M'
ε : M →ₗ[R] M'
ibc : IsBaseChange S ε
x : ι →₀ M
w :
  ∀ (i : ι),
    (((LinearEquiv.baseChange R S (ι →₀ M) (⨁ (x : ι), M) (finsuppLEquivDirectSum R M ι) ≪≫ₗ
                  equiv (f := lmap (M := fun (i : ι) ↦ M) (N := fun (i : ι) ↦ M') fun (x : ι) ↦ ε) ⋯ :
                (a : S ⊗[R] (ι →₀ M)) → ⨁ (i : ι), M')
              (1 ⊗ₜ[R] x) :
            ⨁ (i : ι), M') :
          (a : ι) → M')
        i =
      (((finsuppLEquivDirectSum S M' ι : (a : ι →₀ M') → ⨁ (i : ι), M') (Finsupp.mapRange (⇑ε : (a : M) → M') ⋯ x) :
            ⨁ (i : ι), M') :
          (a : ι) → M')
        i
⊢ Eq (α := ⨁ (i : ι), M')
    ((LinearEquiv.baseChange R S (ι →₀ M) (⨁ (x : ι), M) (finsuppLEquivDirectSum R M ι) ≪≫ₗ
            equiv (f := lmap (M := fun (i : ι) ↦ M) (N := fun (i : ι) ↦ M') fun (x : ι) ↦ ε) ⋯ :
          (a : S ⊗[R] (ι →₀ M)) → ⨁ (i : ι), M')
        (1 ⊗ₜ[R] x) :
      ⨁ (i : ι), M')
    ((finsuppLEquivDirectSum S M' ι : (a : ι →₀ M') → ⨁ (i : ι), M') (Finsupp.mapRange (⇑ε : (a : M) → M') ⋯ x) :
      ⨁ (i : ι), M')

Tactic:
ext
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangePi
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
ι : Type u_3
M : Type u_6
M' : Type u_7
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M'
inst_5 : Module R M
inst_6 : Module R M'
inst_7 : Module S M'
inst_8 : IsScalarTower R S M'
ε : M →ₗ[R] M'
ibc : IsBaseChange S ε
x : ι →₀ M
i : ι
⊢ (((LinearEquiv.baseChange R S (ι →₀ M) (⨁ (x : ι), M) (finsuppLEquivDirectSum R M ι) ≪≫ₗ
                equiv (f := lmap (M := fun (i : ι) ↦ M) (N := fun (i : ι) ↦ M') fun (x : ι) ↦ ε) ⋯ :
              (a : S ⊗[R] (ι →₀ M)) → ⨁ (i : ι), M')
            (1 ⊗ₜ[R] x) :
          ⨁ (i : ι), M') :
        (a : ι) → M')
      i =
    (((finsuppLEquivDirectSum S M' ι : (a : ι →₀ M') → ⨁ (i : ι), M') (Finsupp.mapRange (⇑ε : (a : M) → M') ⋯ x) :
          ⨁ (i : ι), M') :
        (a : ι) → M')
      i

Tactic:
simp [LinearEquiv.baseChange_tmul, IsBaseChange.equiv_tmul, lmap_finsuppLEquivDirectSum_eq]

Premises used: LinearEquiv.baseChange_tmul, IsBaseChange.equiv_tmul, lmap_finsuppLEquivDirectSum_eq
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangePi
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
ι : Type u_3
M : Type u_6
M' : Type u_7
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M'
inst_5 : Module R M
inst_6 : Module R M'
inst_7 : Module S M'
inst_8 : IsScalarTower R S M'
ε : M →ₗ[R] M'
ibc : IsBaseChange S ε
apply apply₁ :
  ∀ (x : ι →₀ M),
    Eq (α := ι →₀ M')
      ((LinearEquiv.baseChange R S (ι →₀ M) (⨁ (x : ι), M) (finsuppLEquivDirectSum R M ι) ≪≫ₗ
                equiv (f := lmap (M := fun (i : ι) ↦ M) (N := fun (i : ι) ↦ M') fun (x : ι) ↦ ε) ⋯ ≪≫ₗ
              LinearEquiv.symm (finsuppLEquivDirectSum S M' ι) :
            (a : S ⊗[R] (ι →₀ M)) → ι →₀ M')
          (1 ⊗ₜ[R] x) :
        ι →₀ M')
      ((Finsupp.mapRange.linearMap ε : (a : ι →₀ M) → ι →₀ M') x : ι →₀ M')
apply₂ :
  ∀ (x : ι →₀ M),
    Eq (α := ⨁ (i : ι), M')
      ((LinearEquiv.baseChange R S (ι →₀ M) (⨁ (x : ι), M) (finsuppLEquivDirectSum R M ι) ≪≫ₗ
              equiv (f := lmap (M := fun (i : ι) ↦ M) (N := fun (i : ι) ↦ M') fun (x : ι) ↦ ε) ⋯ :
            (a : S ⊗[R] (ι →₀ M)) → ⨁ (i : ι), M')
          (1 ⊗ₜ[R] x) :
        ⨁ (i : ι), M')
      ((finsuppLEquivDirectSum S M' ι : (a : ι →₀ M') → ⨁ (i : ι), M') (Finsupp.mapRange (⇑ε : (a : M) → M') ⋯ x) :
        ⨁ (i : ι), M')
w :
  ∀ (x : ι →₀ M) (i : ι),
    (((LinearEquiv.baseChange R S (ι →₀ M) (⨁ (x : ι), M) (finsuppLEquivDirectSum R M ι) ≪≫ₗ
                  equiv (f := lmap (M := fun (i : ι) ↦ M) (N := fun (i : ι) ↦ M') fun (x : ι) ↦ ε) ⋯ :
                (a : S ⊗[R] (ι →₀ M)) → ⨁ (i : ι), M')
              (1 ⊗ₜ[R] x) :
            ⨁ (i : ι), M') :
          (a : ι) → M')
        i =
      (((finsuppLEquivDirectSum S M' ι : (a : ι →₀ M') → ⨁ (i : ι), M') (Finsupp.mapRange (⇑ε : (a : M) → M') ⋯ x) :
            ⨁ (i : ι), M') :
          (a : ι) → M')
        i
⊢ IsBaseChange (M := ι →₀ M) S (Finsupp.mapRange.linearMap ε)

Tactic:
classical
  apply of_equiv <|
    LinearEquiv.baseChange R S _ _ (finsuppLEquivDirectSum ..) ≪≫ₗ
      (directSum (fun _ ↦ ibc)).equiv ≪≫ₗ (finsuppLEquivDirectSum ..).symm
  intro x
  rw [LinearEquiv.trans_apply, Finsupp.mapRange.linearMap_apply,
    LinearEquiv.symm_apply_eq]
  ext
  simp [LinearEquiv.baseChange_tmul, IsBaseChange.equiv_tmul, lmap_finsuppLEquivDirectSum_eq]

Premises used: LinearEquiv.symm, LinearEquiv.symm_apply_eq, IsBaseChange.directSum, LinearEquiv.trans_apply, Finsupp.mapRange.linearMap_apply, LinearEquiv.baseChange_tmul, finsuppLEquivDirectSum, IsBaseChange.of_equiv, LinearEquiv.baseChange, IsBaseChange.equiv_tmul, lmap_finsuppLEquivDirectSum_eq, IsBaseChange.equiv
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
C : Type uC
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Semiring B
inst_8 : Algebra R B
inst_9 : Semiring C
inst_10 : Algebra S C
f : A ⊗[R] B →ₗ[S] C
hf :
  ∀ (a₁ a₂ : A) (b₁ b₂ : B),
    (f : (a : A ⊗[R] B) → C) ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) =
      HMul.hMul (α := C) (β := C) ((f : (a : A ⊗[R] B) → C) (a₁ ⊗ₜ[R] b₁) : C)
        ((f : (a : A ⊗[R] B) → C) (a₂ ⊗ₜ[R] b₂) : C)
x y : A ⊗[R] B
this_1 : Algebra R C := restrictScalars R S C
this : IsScalarTower R S C := ⋯
a :
  ∀ (x : A) (x_1 : B) (x_2 : A) (x_3 : B),
    Eq.{uC + 1} (α := C)
      (((((AlgebraTensorModule.curry
                      (((((AlgebraTensorModule.curry (LinearMap.compr₂ (LinearMap.mul S (A ⊗[R] B)) f) :
                                  A →ₗ[S] B →ₗ[R] A ⊗[R] B →ₗ[S] C) :
                                (a : A) → B →ₗ[R] A ⊗[R] B →ₗ[S] C)
                              x :
                            B →ₗ[R] A ⊗[R] B →ₗ[S] C) :
                          (a : B) → A ⊗[R] B →ₗ[S] C)
                        x_1) :
                    A →ₗ[S] B →ₗ[R] C) :
                  (a : A) → B →ₗ[R] C)
                x_2 :
              B →ₗ[R] C) :
            (a : B) → C)
          x_3 :
        C)
      (((((AlgebraTensorModule.curry
                      (((((AlgebraTensorModule.curry ((LinearMap.mul S C ∘ₗ f).compl₂ f) :
                                  A →ₗ[S] B →ₗ[R] A ⊗[R] B →ₗ[S] C) :
                                (a : A) → B →ₗ[R] A ⊗[R] B →ₗ[S] C)
                              x :
                            B →ₗ[R] A ⊗[R] B →ₗ[S] C) :
                          (a : B) → A ⊗[R] B →ₗ[S] C)
                        x_1) :
                    A →ₗ[S] B →ₗ[R] C) :
                  (a : A) → B →ₗ[R] C)
                x_2 :
              B →ₗ[R] C) :
            (a : B) → C)
          x_3 :
        C)
⊢ LinearMap.compr₂ (LinearMap.mul S (A ⊗[R] B)) f = (LinearMap.mul S C ∘ₗ f).compl₂ f

Tactic:
ext
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
C : Type uC
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Semiring B
inst_8 : Algebra R B
inst_9 : Semiring C
inst_10 : Algebra S C
f : A ⊗[R] B →ₗ[S] C
hf :
  ∀ (a₁ a₂ : A) (b₁ b₂ : B),
    (f : (a : A ⊗[R] B) → C) ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) =
      HMul.hMul (α := C) (β := C) ((f : (a : A ⊗[R] B) → C) (a₁ ⊗ₜ[R] b₁) : C)
        ((f : (a : A ⊗[R] B) → C) (a₂ ⊗ₜ[R] b₂) : C)
x y : A ⊗[R] B
this_1 : Algebra R C := restrictScalars R S C
this : IsScalarTower R S C := ⋯
x_1 : A
x_2 : B
x_3 : A
x_4 : B
a :
  (f : (a : A ⊗[R] B) → C) ((x_1 * x_3) ⊗ₜ[R] (x_2 * x_4)) =
    HMul.hMul (α := C) (β := C) ((f : (a : A ⊗[R] B) → C) (x_1 ⊗ₜ[R] x_2) : C)
      ((f : (a : A ⊗[R] B) → C) (x_3 ⊗ₜ[R] x_4) : C)
⊢ Eq.{uC + 1} (α := C)
    (((((AlgebraTensorModule.curry
                    (((((AlgebraTensorModule.curry (LinearMap.compr₂ (LinearMap.mul S (A ⊗[R] B)) f) :
                                A →ₗ[S] B →ₗ[R] A ⊗[R] B →ₗ[S] C) :
                              (a : A) → B →ₗ[R] A ⊗[R] B →ₗ[S] C)
                            x_1 :
                          B →ₗ[R] A ⊗[R] B →ₗ[S] C) :
                        (a : B) → A ⊗[R] B →ₗ[S] C)
                      x_2) :
                  A →ₗ[S] B →ₗ[R] C) :
                (a : A) → B →ₗ[R] C)
              x_3 :
            B →ₗ[R] C) :
          (a : B) → C)
        x_4 :
      C)
    (((((AlgebraTensorModule.curry
                    (((((AlgebraTensorModule.curry ((LinearMap.mul S C ∘ₗ f).compl₂ f) :
                                A →ₗ[S] B →ₗ[R] A ⊗[R] B →ₗ[S] C) :
                              (a : A) → B →ₗ[R] A ⊗[R] B →ₗ[S] C)
                            x_1 :
                          B →ₗ[R] A ⊗[R] B →ₗ[S] C) :
                        (a : B) → A ⊗[R] B →ₗ[S] C)
                      x_2) :
                  A →ₗ[S] B →ₗ[R] C) :
                (a : A) → B →ₗ[R] C)
              x_3 :
            B →ₗ[R] C) :
          (a : B) → C)
        x_4 :
      C)

Tactic:
dsimp
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
C : Type uC
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Semiring B
inst_8 : Algebra R B
inst_9 : Semiring C
inst_10 : Algebra S C
f : A ⊗[R] B →ₗ[S] C
hf :
  ∀ (a₁ a₂ : A) (b₁ b₂ : B),
    (f : (a : A ⊗[R] B) → C) ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) =
      HMul.hMul (α := C) (β := C) ((f : (a : A ⊗[R] B) → C) (a₁ ⊗ₜ[R] b₁) : C)
        ((f : (a : A ⊗[R] B) → C) (a₂ ⊗ₜ[R] b₂) : C)
x y : A ⊗[R] B
this_1 : Algebra R C := restrictScalars R S C
this : IsScalarTower R S C := ⋯
x_1 : A
x_2 : B
x_3 : A
x_4 : B
⊢ (f : (a : A ⊗[R] B) → C) ((x_1 * x_3) ⊗ₜ[R] (x_2 * x_4)) =
    HMul.hMul (α := C) (β := C) ((f : (a : A ⊗[R] B) → C) (x_1 ⊗ₜ[R] x_2) : C)
      ((f : (a : A ⊗[R] B) → C) (x_3 ⊗ₜ[R] x_4) : C)

Tactic:
hf _ _ _ _
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
C : Type uC
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Semiring B
inst_8 : Algebra R B
inst_9 : Semiring C
inst_10 : Algebra S C
f : A ⊗[R] B →ₗ[S] C
hf :
  ∀ (a₁ a₂ : A) (b₁ b₂ : B),
    (f : (a : A ⊗[R] B) → C) ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) =
      HMul.hMul (α := C) (β := C) ((f : (a : A ⊗[R] B) → C) (a₁ ⊗ₜ[R] b₁) : C)
        ((f : (a : A ⊗[R] B) → C) (a₂ ⊗ₜ[R] b₂) : C)
x y : A ⊗[R] B
this_1 : Algebra R C := restrictScalars R S C
this : IsScalarTower R S C := ⋯
x_1 : A
x_2 : B
x_3 : A
x_4 : B
⊢ (f : (a : A ⊗[R] B) → C) ((x_1 * x_3) ⊗ₜ[R] (x_2 * x_4)) =
    HMul.hMul (α := C) (β := C) ((f : (a : A ⊗[R] B) → C) (x_1 ⊗ₜ[R] x_2) : C)
      ((f : (a : A ⊗[R] B) → C) (x_3 ⊗ₜ[R] x_4) : C)

Tactic:
exact hf _ _ _ _
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
C : Type uC
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Semiring B
inst_8 : Algebra R B
inst_9 : Semiring C
inst_10 : Algebra S C
f : A ⊗[R] B →ₗ[S] C
h_mul :
  ∀ (a₁ a₂ : A) (b₁ b₂ : B),
    (f : (a : A ⊗[R] B) → C) ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) =
      HMul.hMul (α := C) (β := C) ((f : (a : A ⊗[R] B) → C) (a₁ ⊗ₜ[R] b₁) : C)
        ((f : (a : A ⊗[R] B) → C) (a₂ ⊗ₜ[R] b₂) : C)
h_one : Eq.{uC + 1} (α := C) ((f : (a : A ⊗[R] B) → C) (1 ⊗ₜ[R] 1) : C) (1 : C)
x : A ⊗[R] B
⊢ Eq.{uC + 1} (α := C) (((algHomOfLinearMapTensorProduct f h_mul h_one : A ⊗[R] B →ₐ[S] C) : (a : A ⊗[R] B) → C) x : C)
    ((f : (a : A ⊗[R] B) → C) x : C)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
C : Type uC
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Semiring B
inst_8 : Algebra R B
inst_9 : Semiring C
inst_10 : Algebra S C
f : A ⊗[R] B ≃ₗ[S] C
h_mul :
  ∀ (a₁ a₂ : A) (b₁ b₂ : B),
    (f : (a : A ⊗[R] B) → C) ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) =
      HMul.hMul (α := C) (β := C) ((f : (a : A ⊗[R] B) → C) (a₁ ⊗ₜ[R] b₁) : C)
        ((f : (a : A ⊗[R] B) → C) (a₂ ⊗ₜ[R] b₂) : C)
h_one : Eq.{uC + 1} (α := C) ((f : (a : A ⊗[R] B) → C) (1 ⊗ₜ[R] 1) : C) (1 : C)
x : A ⊗[R] B
⊢ Eq.{uC + 1} (α := C)
    (((algEquivOfLinearEquivTensorProduct f h_mul h_one : A ⊗[R] B ≃ₐ[S] C) : (a : A ⊗[R] B) → C) x : C)
    ((f : (a : A ⊗[R] B) → C) x : C)

Tactic:
rfl

Premises used: rfl