awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.DirectSum.TensorProduct (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Type u_1
inst_1 : Semiring S
inst_2 : Algebra R S
ι₁ : Type v₁
inst_3 : DecidableEq ι₁
M₁ : ι₁ → Type w₁
M₂' : Type w₂'
inst_4 : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst_5 : AddCommMonoid M₂'
inst_6 : (i₁ : ι₁) → Module.{u, w₁} R (M₁ i₁)
inst_7 : Module R M₂'
inst_8 : (i₁ : ι₁) → Module.{u_1, w₁} S (M₁ i₁)
inst_9 : ∀ (i₁ : ι₁), IsScalarTower.{u, u_1, w₁} R S (M₁ i₁)
i : ι₁
x : M₁ i
y : M₂'
⊢ Eq (α := (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] M₂')
    (((LinearEquiv.symm (directSumLeft R S M₁ M₂') :
            (⨁ (i : ι₁), TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') ≃ₗ[S] (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] M₂') :
          (a : ⨁ (i : ι₁), M₁ i ⊗[R] M₂') → (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] M₂')
        (((lof S ι₁ (fun (i : ι₁) ↦ TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') i :
              TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂' →ₗ[S] ⨁ (i : ι₁), TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') :
            (a : M₁ i ⊗[R] M₂') → ⨁ (i : ι₁), M₁ i ⊗[R] M₂')
          (x ⊗ₜ[R] y)) :
      (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] M₂')
    ((lof S ι₁ M₁ i : (a : M₁ i) → ⨁ (i : ι₁), M₁ i) x ⊗ₜ[R] y : (⨁ (i : ι₁), M₁ i) ⊗[R] M₂')
have rw : Eq (α := ⨁ (i : ι₁), TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂')
  (((lof S ι₁ (fun (i : ι₁) ↦ TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') i :
          TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂' →ₗ[S] ⨁ (i : ι₁), TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') :
        (a : M₁ i ⊗[R] M₂') → ⨁ (i : ι₁), M₁ i ⊗[R] M₂')
      (x ⊗ₜ[R] y) :
    ⨁ (i : ι₁), TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂')
  (((directSumLeft R S M₁ M₂' :
          (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] M₂' ≃ₗ[S] ⨁ (i : ι₁), TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') :
        (a : (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] M₂') → ⨁ (i : ι₁), M₁ i ⊗[R] M₂')
      ((lof S ι₁ M₁ i : (a : M₁ i) → ⨁ (i : ι₁), M₁ i) x ⊗ₜ[R] y) :
    ⨁ (i : ι₁), TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂')
Tactic: rw [LinearEquiv.symm_apply_eq, directSumLeft_tmul_lof]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DirectSum.TensorProduct (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Type u_1
inst_1 : Semiring S
inst_2 : Algebra R S
ι₁ : Type v₁
inst_3 : DecidableEq ι₁
M₁ : ι₁ → Type w₁
M₂' : Type w₂'
inst_4 : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst_5 : AddCommMonoid M₂'
inst_6 : (i₁ : ι₁) → Module.{u, w₁} R (M₁ i₁)
inst_7 : Module R M₂'
inst_8 : (i₁ : ι₁) → Module.{u_1, w₁} S (M₁ i₁)
inst_9 : ∀ (i₁ : ι₁), IsScalarTower.{u, u_1, w₁} R S (M₁ i₁)
i : ι₁
x : M₁ i
y : M₂'
rw :
  Eq (α := ⨁ (i : ι₁), TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂')
    (((lof S ι₁ (fun (i : ι₁) ↦ TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') i :
            TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂' →ₗ[S] ⨁ (i : ι₁), TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') :
          (a : M₁ i ⊗[R] M₂') → ⨁ (i : ι₁), M₁ i ⊗[R] M₂')
        (x ⊗ₜ[R] y) :
      ⨁ (i : ι₁), TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂')
    (((directSumLeft R S M₁ M₂' :
            (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] M₂' ≃ₗ[S] ⨁ (i : ι₁), TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') :
          (a : (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] M₂') → ⨁ (i : ι₁), M₁ i ⊗[R] M₂')
        ((lof S ι₁ M₁ i : (a : M₁ i) → ⨁ (i : ι₁), M₁ i) x ⊗ₜ[R] y) :
      ⨁ (i : ι₁), TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂')
⊢ Eq (α := (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] M₂')
    (((LinearEquiv.symm (directSumLeft R S M₁ M₂') :
            (⨁ (i : ι₁), TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') ≃ₗ[S] (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] M₂') :
          (a : ⨁ (i : ι₁), M₁ i ⊗[R] M₂') → (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] M₂')
        (((lof S ι₁ (fun (i : ι₁) ↦ TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') i :
              TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂' →ₗ[S] ⨁ (i : ι₁), TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') :
            (a : M₁ i ⊗[R] M₂') → ⨁ (i : ι₁), M₁ i ⊗[R] M₂')
          (x ⊗ₜ[R] y)) :
      (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] M₂')
    ((lof S ι₁ M₁ i : (a : M₁ i) → ⨁ (i : ι₁), M₁ i) x ⊗ₜ[R] y : (⨁ (i : ι₁), M₁ i) ⊗[R] M₂')
have rw₁ : Eq (α := ⨁ (i : ι₁), TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂')
  (((lof S ι₁ (fun (i : ι₁) ↦ TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') i :
          TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂' →ₗ[S] ⨁ (i : ι₁), TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') :
        (a : M₁ i ⊗[R] M₂') → ⨁ (i : ι₁), M₁ i ⊗[R] M₂')
      (x ⊗ₜ[R] y) :
    ⨁ (i : ι₁), TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂')
  (((lof S ι₁ (fun (i : ι₁) ↦ TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') i :
          TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂' →ₗ[S] ⨁ (i : ι₁), TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') :
        (a : M₁ i ⊗[R] M₂') → ⨁ (i : ι₁), M₁ i ⊗[R] M₂')
      (x ⊗ₜ[R] y) :
    ⨁ (i : ι₁), TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂')
Tactic: rw [LinearEquiv.symm_apply_eq, directSumLeft_tmul_lof]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DirectSum.TensorProduct (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Type u_1
inst_1 : Semiring S
inst_2 : Algebra R S
ι₁ : Type v₁
inst_3 : DecidableEq ι₁
M₁ : ι₁ → Type w₁
M₂' : Type w₂'
inst_4 : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst_5 : AddCommMonoid M₂'
inst_6 : (i₁ : ι₁) → Module.{u, w₁} R (M₁ i₁)
inst_7 : Module R M₂'
inst_8 : (i₁ : ι₁) → Module.{u_1, w₁} S (M₁ i₁)
inst_9 : ∀ (i₁ : ι₁), IsScalarTower.{u, u_1, w₁} R S (M₁ i₁)
m : ⨁ (i : ι₁), M₁ i
n : M₂'
i : ι₁
⊢ ((((directSumLeft R S M₁ M₂' :
                (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] M₂' ≃ₗ[S] ⨁ (i : ι₁), TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') :
              (a : (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] M₂') → ⨁ (i : ι₁), M₁ i ⊗[R] M₂')
            (m ⊗ₜ[R] n) :
          ⨁ (i : ι₁), TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') :
        (a : ι₁) → M₁ a ⊗[R] M₂')
      i =
    (m : (a : ι₁) → M₁ a) i ⊗ₜ[R] n
have suffices : Eq (α := (⨁ (i : ι₁), M₁ i) →ₗ[S] TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂')
  ((component S ι₁ (fun (i : ι₁) ↦ TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') i :
        (⨁ (i : ι₁), TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') →ₗ[S] TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') ∘ₗ
      (((↑(directSumLeft R S M₁ M₂') :
              (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] M₂' →ₗ[S] ⨁ (i : ι₁), TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') :
            (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] M₂' →ₗ[S] ⨁ (i : ι₁), TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') ∘ₗ
          ((LinearMap.flip (AlgebraTensorModule.mk R S (⨁ (i : ι₁), M₁ i) M₂') :
                (a : M₂') → (⨁ (i : ι₁), M₁ i) →ₗ[S] (⨁ (i : ι₁), M₁ i) ⊗[R] M₂')
              n :
            (⨁ (i : ι₁), M₁ i) →ₗ[S] (⨁ (i : ι₁), M₁ i) ⊗[R] M₂') :
        (⨁ (i : ι₁), M₁ i) →ₗ[S] ⨁ (i : ι₁), TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') :
    (⨁ (i : ι₁), M₁ i) →ₗ[S] TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂')
  ((LinearMap.flip (AlgebraTensorModule.mk R S (M₁ i) M₂') : (a : M₂') → M₁ i →ₗ[S] M₁ i ⊗[R] M₂') n ∘ₗ
      component S ι₁ M₁ i :
    (⨁ (i : ι₁), M₁ i) →ₗ[S] TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂')
Tactic: suffices (DirectSum.component S ι₁ _ i) ∘ₗ (directSumLeft R S M₁ M₂').toLinearMap ∘ₗ
      ((AlgebraTensorModule.mk R S (⨁ i, M₁ i) M₂').flip n) =
        ((AlgebraTensorModule.mk R S (M₁ i) M₂').flip n) ∘ₗ (DirectSum.component S ι₁ M₁ i) by
    simpa using LinearMap.congr_fun this m
-- Lean 4 proof step from Mathlib.LinearAlgebra.DirectSum.TensorProduct (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Type u_1
inst_1 : Semiring S
inst_2 : Algebra R S
ι₁ : Type v₁
inst_3 : DecidableEq ι₁
M₁ : ι₁ → Type w₁
M₂' : Type w₂'
inst_4 : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst_5 : AddCommMonoid M₂'
inst_6 : (i₁ : ι₁) → Module.{u, w₁} R (M₁ i₁)
inst_7 : Module R M₂'
inst_8 : (i₁ : ι₁) → Module.{u_1, w₁} S (M₁ i₁)
inst_9 : ∀ (i₁ : ι₁), IsScalarTower.{u, u_1, w₁} R S (M₁ i₁)
m : ⨁ (i : ι₁), M₁ i
n : M₂'
i : ι₁
⊢ Eq (α := (⨁ (i : ι₁), M₁ i) →ₗ[S] TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂')
    ((component S ι₁ (fun (i : ι₁) ↦ TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') i :
          (⨁ (i : ι₁), TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') →ₗ[S] TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') ∘ₗ
        (((↑(directSumLeft R S M₁ M₂') :
                (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] M₂' →ₗ[S] ⨁ (i : ι₁), TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') :
              (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] M₂' →ₗ[S] ⨁ (i : ι₁), TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') ∘ₗ
            ((LinearMap.flip (AlgebraTensorModule.mk R S (⨁ (i : ι₁), M₁ i) M₂') :
                  (a : M₂') → (⨁ (i : ι₁), M₁ i) →ₗ[S] (⨁ (i : ι₁), M₁ i) ⊗[R] M₂')
                n :
              (⨁ (i : ι₁), M₁ i) →ₗ[S] (⨁ (i : ι₁), M₁ i) ⊗[R] M₂') :
          (⨁ (i : ι₁), M₁ i) →ₗ[S] ⨁ (i : ι₁), TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') :
      (⨁ (i : ι₁), M₁ i) →ₗ[S] TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂')
    ((LinearMap.flip (AlgebraTensorModule.mk R S (M₁ i) M₂') : (a : M₂') → M₁ i →ₗ[S] M₁ i ⊗[R] M₂') n ∘ₗ
        component S ι₁ M₁ i :
      (⨁ (i : ι₁), M₁ i) →ₗ[S] TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂')
have H : ∀ (j : ι₁) (n_1 : M₁ j),
  Eq (α := TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂')
    (((((component S ι₁ (fun (i : ι₁) ↦ TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') i :
                  (⨁ (i : ι₁), TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') →ₗ[S]
                    TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') ∘ₗ
                (((↑(directSumLeft R S M₁ M₂') :
                        (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] M₂' →ₗ[S] ⨁ (i : ι₁), TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') :
                      (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] M₂' →ₗ[S] ⨁ (i : ι₁), TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') ∘ₗ
                    ((LinearMap.flip (AlgebraTensorModule.mk R S (⨁ (i : ι₁), M₁ i) M₂') :
                          (a : M₂') → (⨁ (i : ι₁), M₁ i) →ₗ[S] (⨁ (i : ι₁), M₁ i) ⊗[R] M₂')
                        n :
                      (⨁ (i : ι₁), M₁ i) →ₗ[S] (⨁ (i : ι₁), M₁ i) ⊗[R] M₂') :
                  (⨁ (i : ι₁), M₁ i) →ₗ[S] ⨁ (i : ι₁), TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂')) ∘ₗ
              lof S ι₁ M₁ j :
            M₁ j →ₗ[S] TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') :
          (a : M₁ j) → M₁ i ⊗[R] M₂')
        n_1 :
      TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂')
    ((((LinearMap.flip (AlgebraTensorModule.mk R S (M₁ i) M₂') : (a : M₂') → M₁ i →ₗ[S] M₁ i ⊗[R] M₂') n ∘ₗ
              component S ι₁ M₁ i) ∘ₗ
            lof S ι₁ M₁ j :
          (a : M₁ j) → M₁ i ⊗[R] M₂')
        n_1 :
      TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂')
Tactic: ext j n
-- Lean 4 proof step from Mathlib.LinearAlgebra.DirectSum.TensorProduct (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Type u_1
inst_1 : Semiring S
inst_2 : Algebra R S
ι₂ : Type v₂
inst_3 : DecidableEq ι₂
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
inst_4 : AddCommMonoid M₁'
inst_5 : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)
inst_6 : Module R M₁'
inst_7 : (i₂ : ι₂) → Module.{u, w₂} R (M₂ i₂)
inst_8 : Module S M₁'
inst_9 : IsScalarTower R S M₁'
x : M₁'
i : ι₂
y : M₂ i
⊢ Eq (α := M₁' ⊗[R] ⨁ (i : ι₂), M₂ i)
    (((LinearEquiv.symm (directSumRight R S M₁' M₂) :
            (⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) ≃ₗ[S] M₁' ⊗[R] ⨁ (i : ι₂), M₂ i) :
          (a : ⨁ (i : ι₂), M₁' ⊗[R] M₂ i) → M₁' ⊗[R] ⨁ (i : ι₂), M₂ i)
        (((lof S ι₂ (fun (i : ι₂) ↦ TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) i :
              TensorProduct.{u, w₁', w₂} R M₁' (M₂ i) →ₗ[S] ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) :
            (a : M₁' ⊗[R] M₂ i) → ⨁ (i : ι₂), M₁' ⊗[R] M₂ i)
          (x ⊗ₜ[R] y)) :
      M₁' ⊗[R] ⨁ (i : ι₂), M₂ i)
    (x ⊗ₜ[R] (lof R ι₂ M₂ i : (a : M₂ i) → ⨁ (i : ι₂), M₂ i) y : M₁' ⊗[R] ⨁ (i : ι₂), M₂ i)
have rw : Eq (α := ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i))
  (((lof S ι₂ (fun (i : ι₂) ↦ TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) i :
          TensorProduct.{u, w₁', w₂} R M₁' (M₂ i) →ₗ[S] ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) :
        (a : M₁' ⊗[R] M₂ i) → ⨁ (i : ι₂), M₁' ⊗[R] M₂ i)
      (x ⊗ₜ[R] y) :
    ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i))
  (((directSumRight R S M₁' M₂ :
          (M₁' ⊗[R] ⨁ (i : ι₂), M₂ i) ≃ₗ[S] ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) :
        (a : M₁' ⊗[R] ⨁ (i : ι₂), M₂ i) → ⨁ (i : ι₂), M₁' ⊗[R] M₂ i)
      (x ⊗ₜ[R] (lof R ι₂ M₂ i : (a : M₂ i) → ⨁ (i : ι₂), M₂ i) y) :
    ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i))
Tactic: rw [LinearEquiv.symm_apply_eq, directSumRight_tmul_lof]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DirectSum.TensorProduct (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Type u_1
inst_1 : Semiring S
inst_2 : Algebra R S
ι₂ : Type v₂
inst_3 : DecidableEq ι₂
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
inst_4 : AddCommMonoid M₁'
inst_5 : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)
inst_6 : Module R M₁'
inst_7 : (i₂ : ι₂) → Module.{u, w₂} R (M₂ i₂)
inst_8 : Module S M₁'
inst_9 : IsScalarTower R S M₁'
x : M₁'
i : ι₂
y : M₂ i
rw :
  Eq (α := ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i))
    (((lof S ι₂ (fun (i : ι₂) ↦ TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) i :
            TensorProduct.{u, w₁', w₂} R M₁' (M₂ i) →ₗ[S] ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) :
          (a : M₁' ⊗[R] M₂ i) → ⨁ (i : ι₂), M₁' ⊗[R] M₂ i)
        (x ⊗ₜ[R] y) :
      ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i))
    (((directSumRight R S M₁' M₂ :
            (M₁' ⊗[R] ⨁ (i : ι₂), M₂ i) ≃ₗ[S] ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) :
          (a : M₁' ⊗[R] ⨁ (i : ι₂), M₂ i) → ⨁ (i : ι₂), M₁' ⊗[R] M₂ i)
        (x ⊗ₜ[R] (lof R ι₂ M₂ i : (a : M₂ i) → ⨁ (i : ι₂), M₂ i) y) :
      ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i))
⊢ Eq (α := M₁' ⊗[R] ⨁ (i : ι₂), M₂ i)
    (((LinearEquiv.symm (directSumRight R S M₁' M₂) :
            (⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) ≃ₗ[S] M₁' ⊗[R] ⨁ (i : ι₂), M₂ i) :
          (a : ⨁ (i : ι₂), M₁' ⊗[R] M₂ i) → M₁' ⊗[R] ⨁ (i : ι₂), M₂ i)
        (((lof S ι₂ (fun (i : ι₂) ↦ TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) i :
              TensorProduct.{u, w₁', w₂} R M₁' (M₂ i) →ₗ[S] ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) :
            (a : M₁' ⊗[R] M₂ i) → ⨁ (i : ι₂), M₁' ⊗[R] M₂ i)
          (x ⊗ₜ[R] y)) :
      M₁' ⊗[R] ⨁ (i : ι₂), M₂ i)
    (x ⊗ₜ[R] (lof R ι₂ M₂ i : (a : M₂ i) → ⨁ (i : ι₂), M₂ i) y : M₁' ⊗[R] ⨁ (i : ι₂), M₂ i)
have rw₁ : Eq (α := ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i))
  (((lof S ι₂ (fun (i : ι₂) ↦ TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) i :
          TensorProduct.{u, w₁', w₂} R M₁' (M₂ i) →ₗ[S] ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) :
        (a : M₁' ⊗[R] M₂ i) → ⨁ (i : ι₂), M₁' ⊗[R] M₂ i)
      (x ⊗ₜ[R] y) :
    ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i))
  (((lof S ι₂ (fun (i : ι₂) ↦ TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) i :
          TensorProduct.{u, w₁', w₂} R M₁' (M₂ i) →ₗ[S] ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) :
        (a : M₁' ⊗[R] M₂ i) → ⨁ (i : ι₂), M₁' ⊗[R] M₂ i)
      (x ⊗ₜ[R] y) :
    ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i))
Tactic: rw [LinearEquiv.symm_apply_eq, directSumRight_tmul_lof]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DirectSum.TensorProduct (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Type u_1
inst_1 : Semiring S
inst_2 : Algebra R S
ι₂ : Type v₂
inst_3 : DecidableEq ι₂
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
inst_4 : AddCommMonoid M₁'
inst_5 : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)
inst_6 : Module R M₁'
inst_7 : (i₂ : ι₂) → Module.{u, w₂} R (M₂ i₂)
inst_8 : Module S M₁'
inst_9 : IsScalarTower R S M₁'
m : M₁'
n : ⨁ (i : ι₂), M₂ i
i : ι₂
⊢ ((((directSumRight R S M₁' M₂ :
                (M₁' ⊗[R] ⨁ (i : ι₂), M₂ i) ≃ₗ[S] ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) :
              (a : M₁' ⊗[R] ⨁ (i : ι₂), M₂ i) → ⨁ (i : ι₂), M₁' ⊗[R] M₂ i)
            (m ⊗ₜ[R] n) :
          ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) :
        (a : ι₂) → M₁' ⊗[R] M₂ a)
      i =
    m ⊗ₜ[R] (n : (a : ι₂) → M₂ a) i
have suffices : Eq (α := (⨁ (i : ι₂), M₂ i) →ₗ[R] TensorProduct.{u, w₁', w₂} R M₁' (M₂ i))
  ((↑R :
        {S : Type u_1} →
          {M : Type (max v₂ w₁' w₂)} →
            {M₂ : Type (max w₁' w₂)} →
              [inst : Semiring R] →
                [inst_10 : Semiring S] →
                  [inst_11 : AddCommMonoid M] →
                    [inst_12 : AddCommMonoid M₂] →
                      [inst_13 : Module R M] →
                        [inst_14 : Module R M₂] →
                          [inst_15 : Module S M] →
                            [inst_16 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (component S ι₂ (fun (i : ι₂) ↦ TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) i) ∘ₗ
    (↑R :
          {S : Type u_1} →
            {M M₂ : Type (max (max v₂ w₁') w₂)} →
              [inst : Semiring R] →
                [inst_10 : Semiring S] →
                  [inst_11 : AddCommMonoid M] →
                    [inst_12 : AddCommMonoid M₂] →
                      [inst_13 : Module R M] →
                        [inst_14 : Module R M₂] →
                          [inst_15 : Module S M] →
                            [inst_16 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        ((↑(directSumRight R S M₁' M₂) :
            (M₁' ⊗[R] ⨁ (i : ι₂), M₂ i) →ₗ[S] ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) :
          (M₁' ⊗[R] ⨁ (i : ι₂), M₂ i) →ₗ[S] ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) ∘ₗ
      (mk R M₁' (⨁ (i : ι₂), M₂ i) : (a : M₁') → (⨁ (i : ι₂), M₂ i) →ₗ[R] M₁' ⊗[R] ⨁ (i : ι₂), M₂ i) m)
  ((mk R M₁' (M₂ i) : (a : M₁') → M₂ i →ₗ[R] M₁' ⊗[R] M₂ i) m ∘ₗ component R ι₂ M₂ i)
Tactic: suffices (DirectSum.component S ι₂ _ i).restrictScalars R ∘ₗ
      (directSumRight R S M₁' M₂).toLinearMap.restrictScalars R ∘ₗ
        (TensorProduct.mk R M₁' (⨁ i, M₂ i) m) =
          (TensorProduct.mk R M₁' (M₂ i) m) ∘ₗ (DirectSum.component R ι₂ M₂ i) by
    simpa using LinearMap.congr_fun this n
-- Lean 4 proof step from Mathlib.LinearAlgebra.DirectSum.TensorProduct (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Type u_2
inst_1 : Semiring S
inst_2 : Algebra R S
ι₂ : Type v₂
inst_3 : DecidableEq ι₂
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
inst_4 : AddCommMonoid M₁'
inst_5 : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)
inst_6 : Module R M₁'
inst_7 : (i₂ : ι₂) → Module.{u, w₂} R (M₂ i₂)
inst_8 : Module S M₁'
inst_9 : IsScalarTower R S M₁'
S₀ : Type u_1
inst_10 : CommSemiring S₀
inst_11 : Algebra R S₀
inst_12 : Algebra S₀ S
inst_13 : Module S₀ M₁'
inst_14 : IsScalarTower R S₀ M₁'
inst_15 : IsScalarTower S₀ S M₁'
⊢ Eq (α := (M₁' ⊗[R] ⨁ (i : ι₂), M₂ i) →ₗ[R] ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i))
    (↑(LinearEquiv.restrictScalars R
          (LinearEquiv.restrictScalars S₀
            (directSumRight R S M₁' M₂ :
              (M₁' ⊗[R] ⨁ (i : ι₂), M₂ i) ≃ₗ[S] ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)))) :
      (M₁' ⊗[R] ⨁ (i : ι₂), M₂ i) →ₗ[R] ⨁ (i : ι₂), M₁' ⊗[R] M₂ i)
    (↑(LinearEquiv.restrictScalars R
          (directSumRight R S₀ M₁' M₂ :
            (M₁' ⊗[R] ⨁ (i : ι₂), M₂ i) ≃ₗ[S₀] ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i))) :
      (M₁' ⊗[R] ⨁ (i : ι₂), M₂ i) →ₗ[R] ⨁ (i : ι₂), M₁' ⊗[R] M₂ i)
have a : ∀ (x : M₁') (i : ι₂) (x_1 : M₂ i) (i_1 : ι₂),
  (((((AlgebraTensorModule.curry
                        (↑(LinearEquiv.restrictScalars R
                              (LinearEquiv.restrictScalars S₀
                                (directSumRight R S M₁' M₂ :
                                  (M₁' ⊗[R] ⨁ (i : ι₂), M₂ i) ≃ₗ[S]
                                    ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)))) :
                          (M₁' ⊗[R] ⨁ (i : ι₂), M₂ i) →ₗ[R] ⨁ (i : ι₂), M₁' ⊗[R] M₂ i) :
                      M₁' →ₗ[R] (⨁ (i : ι₂), M₂ i) →ₗ[R] ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) :
                    (a : M₁') → (⨁ (i : ι₂), M₂ i) →ₗ[R] ⨁ (i : ι₂), M₁' ⊗[R] M₂ i)
                  x ∘ₗ
                lof R ι₂ M₂ i :
              (a : M₂ i) → ⨁ (i : ι₂), M₁' ⊗[R] M₂ i)
            x_1 :
          ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) :
        (a : ι₂) → M₁' ⊗[R] M₂ a)
      i_1 =
    (((((AlgebraTensorModule.curry
                        (↑(LinearEquiv.restrictScalars R
                              (directSumRight R S₀ M₁' M₂ :
                                (M₁' ⊗[R] ⨁ (i : ι₂), M₂ i) ≃ₗ[S₀]
                                  ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i))) :
                          (M₁' ⊗[R] ⨁ (i : ι₂), M₂ i) →ₗ[R] ⨁ (i : ι₂), M₁' ⊗[R] M₂ i) :
                      M₁' →ₗ[R] (⨁ (i : ι₂), M₂ i) →ₗ[R] ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) :
                    (a : M₁') → (⨁ (i : ι₂), M₂ i) →ₗ[R] ⨁ (i : ι₂), M₁' ⊗[R] M₂ i)
                  x ∘ₗ
                lof R ι₂ M₂ i :
              (a : M₂ i) → ⨁ (i : ι₂), M₁' ⊗[R] M₂ i)
            x_1 :
          ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) :
        (a : ι₂) → M₁' ⊗[R] M₂ a)
      i_1
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.BaseChange (goal)
Goal:
R : Type u_1
inst : CommSemiring R
V : Type u_2
inst_1 : AddCommMonoid V
inst_2 : Module R V
A : Type u_4
inst_3 : CommSemiring A
inst_4 : Algebra R A
B : Type u_5
inst_5 : CommSemiring B
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : IsScalarTower R A B
f : Dual R V
⊢ Eq (α := Dual B (B ⊗[A] (A ⊗[R] V)))
    ((baseChange B : (a : Dual A (A ⊗[R] V)) → Dual B (B ⊗[A] (A ⊗[R] V)))
        ((baseChange A : (a : Dual R V) → Dual A (A ⊗[R] V)) f) :
      Dual B (B ⊗[A] (A ⊗[R] V)))
    (((LinearEquiv.symm (congr (cancelBaseChange R A B B V)) : Dual B (B ⊗[R] V) ≃ₗ[B] Dual B (B ⊗[A] (A ⊗[R] V))) :
          (a : Dual B (B ⊗[R] V)) → Dual B (B ⊗[A] (A ⊗[R] V)))
        ((baseChange B : (a : Dual R V) → Dual B (B ⊗[R] V)) f) :
      Dual B (B ⊗[A] (A ⊗[R] V)))
have a : ∀ (x : V),
  Eq.{u_5 + 1} (α := B)
    ((((AlgebraTensorModule.curry
                  (((AlgebraTensorModule.curry
                          ((baseChange B : (a : Dual A (A ⊗[R] V)) → Dual B (B ⊗[A] (A ⊗[R] V)))
                            ((baseChange A : (a : Dual R V) → Dual A (A ⊗[R] V)) f)) :
                        B →ₗ[B] A ⊗[R] V →ₗ[A] B) :
                      (a : B) → A ⊗[R] V →ₗ[A] B)
                    1) :
                A →ₗ[A] V →ₗ[R] B) :
              (a : A) → V →ₗ[R] B)
            1 :
          (a : V) → B)
        x :
      B)
    ((((AlgebraTensorModule.curry
                  (((AlgebraTensorModule.curry
                          (((LinearEquiv.symm (congr (cancelBaseChange R A B B V)) :
                                Dual B (B ⊗[R] V) ≃ₗ[B] Dual B (B ⊗[A] (A ⊗[R] V))) :
                              (a : Dual B (B ⊗[R] V)) → Dual B (B ⊗[A] (A ⊗[R] V)))
                            ((baseChange B : (a : Dual R V) → Dual B (B ⊗[R] V)) f)) :
                        B →ₗ[B] A ⊗[R] V →ₗ[A] B) :
                      (a : B) → A ⊗[R] V →ₗ[A] B)
                    1) :
                A →ₗ[A] V →ₗ[R] B) :
              (a : A) → V →ₗ[R] B)
            1 :
          (a : V) → B)
        x :
      B)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.BaseChange (goal)
Goal:
R : Type u_1
inst : CommSemiring R
V : Type u_2
inst_1 : AddCommMonoid V
inst_2 : Module R V
W : Type u_3
inst_3 : AddCommMonoid W
inst_4 : Module R W
A : Type u_4
inst_5 : CommSemiring A
inst_6 : Algebra R A
inst_7 : Module A W
inst_8 : IsScalarTower R A W
j : V →ₗ[R] W
ibc : IsBaseChange A j
f : Dual R V
⊢ Eq (α := Dual A W) ((ibc.toDual : (a : Dual R V) → Dual A W) f : Dual A W)
    ((Dual.congr ibc.equiv : (a : Dual A (A ⊗[R] V)) → Dual A W)
        ((Dual.baseChange A : (a : Dual R V) → Dual A (A ⊗[R] V)) f) :
      Dual A W)
have e : ∀ (x : V),
  Eq.{u_4 + 1} (α := A)
    ((((ibc.toDual : (a : Dual R V) → Dual A W) f : Dual A W) : (a : W) → A) ((j : (a : V) → W) x : W) : A)
    ((((Dual.congr ibc.equiv : (a : Dual A (A ⊗[R] V)) → Dual A W)
              ((Dual.baseChange A : (a : Dual R V) → Dual A (A ⊗[R] V)) f) :
            Dual A W) :
          (a : W) → A)
        ((j : (a : V) → W) x : W) :
      A)
Tactic: apply ibc.algHom_ext