awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
T : Type u_4
O : Type u_5
inst_9 : CommSemiring T
inst_10 : Algebra R T
inst_11 : Algebra S T
inst_12 : IsScalarTower R S T
inst_13 : AddCommMonoid O
inst_14 : Module R O
inst_15 : Module S O
inst_16 : Module T O
inst_17 : IsScalarTower S T O
inst_18 : IsScalarTower R S O
inst_19 : IsScalarTower R T O
f : M →ₗ[R] N
hf : IsBaseChange S f
h : N →ₗ[S] O
hc :
  IsBaseChange T
    ((↑R :
          {S : Type v₃} →
            {M : Type v₂} →
              {M₂ : Type u_5} →
                [inst : Semiring R] →
                  [inst_21 : Semiring S] →
                    [inst_22 : AddCommMonoid M] →
                      [inst_23 : AddCommMonoid M₂] →
                        [inst_24 : Module R M] →
                          [inst_25 : Module R M₂] →
                            [inst_26 : Module S M] →
                              [inst_27 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        h ∘ₗ
      f)
Q : Type (max v₂ u_5 u_4)
inst_20 : AddCommMonoid Q
h₁ :
  ∀ [inst : Module S Q] [inst_21 : Module T Q] [inst_22 : IsScalarTower S T Q] (g : N →ₗ[S] Q),
    ∃! g' : O →ₗ[T] Q,
      (↑S :
              {S_1 : Type u_4} →
                {M : Type u_5} →
                  {M₂ : Type (max (max v₂ u_5) u_4)} →
                    [inst : Semiring S] →
                      [inst_23 : Semiring S_1] →
                        [inst_24 : AddCommMonoid M] →
                          [inst_25 : AddCommMonoid M₂] →
                            [inst_26 : Module S M] →
                              [inst_27 : Module S M₂] →
                                [inst_28 : Module S_1 M] →
                                  [inst_29 : Module S_1 M₂] →
                                    [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
            g' ∘ₗ
          h =
        g
⊢ ∀ [inst : Module S Q] [inst_21 : Module T Q] [inst_22 : IsScalarTower S T Q] (g : N →ₗ[S] Q),
    ∃! g' : O →ₗ[T] Q,
      (↑S :
              {S_1 : Type u_4} →
                {M : Type u_5} →
                  {M₂ : Type (max (max v₂ u_5) u_4)} →
                    [inst : Semiring S] →
                      [inst_23 : Semiring S_1] →
                        [inst_24 : AddCommMonoid M] →
                          [inst_25 : AddCommMonoid M₂] →
                            [inst_26 : Module S M] →
                              [inst_27 : Module S M₂] →
                                [inst_28 : Module S_1 M] →
                                  [inst_29 : Module S_1 M₂] →
                                    [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
            g' ∘ₗ
          h =
        g

Tactic:
_
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
T : Type u_4
O : Type u_5
inst_9 : CommSemiring T
inst_10 : Algebra R T
inst_11 : Algebra S T
inst_12 : IsScalarTower R S T
inst_13 : AddCommMonoid O
inst_14 : Module R O
inst_15 : Module S O
inst_16 : Module T O
inst_17 : IsScalarTower S T O
inst_18 : IsScalarTower R S O
inst_19 : IsScalarTower R T O
f : M →ₗ[R] N
hf : IsBaseChange S f
h : N →ₗ[S] O
hc :
  IsBaseChange T
    ((↑R :
          {S : Type v₃} →
            {M : Type v₂} →
              {M₂ : Type u_5} →
                [inst : Semiring R] →
                  [inst_22 : Semiring S] →
                    [inst_23 : AddCommMonoid M] →
                      [inst_24 : AddCommMonoid M₂] →
                        [inst_25 : Module R M] →
                          [inst_26 : Module R M₂] →
                            [inst_27 : Module S M] →
                              [inst_28 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        h ∘ₗ
      f)
Q : Type (max v₂ u_5 u_4)
inst_20 : AddCommMonoid Q
inst_21 : Module S Q
h₁ :
  ∀ [inst : Module T Q] [inst_22 : IsScalarTower S T Q] (g : N →ₗ[S] Q),
    ∃! g' : O →ₗ[T] Q,
      (↑S :
              {S_1 : Type u_4} →
                {M : Type u_5} →
                  {M₂ : Type (max (max v₂ u_5) u_4)} →
                    [inst : Semiring S] →
                      [inst_23 : Semiring S_1] →
                        [inst_24 : AddCommMonoid M] →
                          [inst_25 : AddCommMonoid M₂] →
                            [inst_26 : Module S M] →
                              [inst_27 : Module S M₂] →
                                [inst_28 : Module S_1 M] →
                                  [inst_29 : Module S_1 M₂] →
                                    [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
            g' ∘ₗ
          h =
        g
⊢ ∀ [inst : Module T Q] [inst_22 : IsScalarTower S T Q] (g : N →ₗ[S] Q),
    ∃! g' : O →ₗ[T] Q,
      (↑S :
              {S_1 : Type u_4} →
                {M : Type u_5} →
                  {M₂ : Type (max (max v₂ u_5) u_4)} →
                    [inst : Semiring S] →
                      [inst_23 : Semiring S_1] →
                        [inst_24 : AddCommMonoid M] →
                          [inst_25 : AddCommMonoid M₂] →
                            [inst_26 : Module S M] →
                              [inst_27 : Module S M₂] →
                                [inst_28 : Module S_1 M] →
                                  [inst_29 : Module S_1 M₂] →
                                    [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
            g' ∘ₗ
          h =
        g

Tactic:
_
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
T : Type u_4
O : Type u_5
inst_9 : CommSemiring T
inst_10 : Algebra R T
inst_11 : Algebra S T
inst_12 : IsScalarTower R S T
inst_13 : AddCommMonoid O
inst_14 : Module R O
inst_15 : Module S O
inst_16 : Module T O
inst_17 : IsScalarTower S T O
inst_18 : IsScalarTower R S O
inst_19 : IsScalarTower R T O
f : M →ₗ[R] N
hf : IsBaseChange S f
h : N →ₗ[S] O
hc :
  IsBaseChange T
    ((↑R :
          {S : Type v₃} →
            {M : Type v₂} →
              {M₂ : Type u_5} →
                [inst : Semiring R] →
                  [inst_23 : Semiring S] →
                    [inst_24 : AddCommMonoid M] →
                      [inst_25 : AddCommMonoid M₂] →
                        [inst_26 : Module R M] →
                          [inst_27 : Module R M₂] →
                            [inst_28 : Module S M] →
                              [inst_29 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        h ∘ₗ
      f)
Q : Type (max v₂ u_5 u_4)
inst_20 : AddCommMonoid Q
inst_21 : Module S Q
inst_22 : Module T Q
h₁ :
  ∀ [inst : IsScalarTower S T Q] (g : N →ₗ[S] Q),
    ∃! g' : O →ₗ[T] Q,
      (↑S :
              {S_1 : Type u_4} →
                {M : Type u_5} →
                  {M₂ : Type (max (max v₂ u_5) u_4)} →
                    [inst : Semiring S] →
                      [inst_23 : Semiring S_1] →
                        [inst_24 : AddCommMonoid M] →
                          [inst_25 : AddCommMonoid M₂] →
                            [inst_26 : Module S M] →
                              [inst_27 : Module S M₂] →
                                [inst_28 : Module S_1 M] →
                                  [inst_29 : Module S_1 M₂] →
                                    [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
            g' ∘ₗ
          h =
        g
⊢ ∀ [inst : IsScalarTower S T Q] (g : N →ₗ[S] Q),
    ∃! g' : O →ₗ[T] Q,
      (↑S :
              {S_1 : Type u_4} →
                {M : Type u_5} →
                  {M₂ : Type (max (max v₂ u_5) u_4)} →
                    [inst : Semiring S] →
                      [inst_23 : Semiring S_1] →
                        [inst_24 : AddCommMonoid M] →
                          [inst_25 : AddCommMonoid M₂] →
                            [inst_26 : Module S M] →
                              [inst_27 : Module S M₂] →
                                [inst_28 : Module S_1 M] →
                                  [inst_29 : Module S_1 M₂] →
                                    [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
            g' ∘ₗ
          h =
        g

Tactic:
_
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
T : Type u_4
O : Type u_5
inst_9 : CommSemiring T
inst_10 : Algebra R T
inst_11 : Algebra S T
inst_12 : IsScalarTower R S T
inst_13 : AddCommMonoid O
inst_14 : Module R O
inst_15 : Module S O
inst_16 : Module T O
inst_17 : IsScalarTower S T O
inst_18 : IsScalarTower R S O
inst_19 : IsScalarTower R T O
f : M →ₗ[R] N
hf : IsBaseChange S f
h : N →ₗ[S] O
hc :
  IsBaseChange T
    ((↑R :
          {S : Type v₃} →
            {M : Type v₂} →
              {M₂ : Type u_5} →
                [inst : Semiring R] →
                  [inst_24 : Semiring S] →
                    [inst_25 : AddCommMonoid M] →
                      [inst_26 : AddCommMonoid M₂] →
                        [inst_27 : Module R M] →
                          [inst_28 : Module R M₂] →
                            [inst_29 : Module S M] →
                              [inst_30 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        h ∘ₗ
      f)
Q : Type (max v₂ u_5 u_4)
inst_20 : AddCommMonoid Q
inst_21 : Module S Q
inst_22 : Module T Q
inst_23 : IsScalarTower S T Q
r : N →ₗ[S] Q
this : Module R Q := Module.restrictScalars R S Q
⊢ IsScalarTower R S Q

Tactic:
haveI : IsScalarTower R S Q := .restrictScalars R S Q
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
T : Type u_4
O : Type u_5
inst_9 : CommSemiring T
inst_10 : Algebra R T
inst_11 : Algebra S T
inst_12 : IsScalarTower R S T
inst_13 : AddCommMonoid O
inst_14 : Module R O
inst_15 : Module S O
inst_16 : Module T O
inst_17 : IsScalarTower S T O
inst_18 : IsScalarTower R S O
inst_19 : IsScalarTower R T O
f : M →ₗ[R] N
hf : IsBaseChange S f
h : N →ₗ[S] O
hc :
  IsBaseChange T
    ((↑R :
          {S : Type v₃} →
            {M : Type v₂} →
              {M₂ : Type u_5} →
                [inst : Semiring R] →
                  [inst_24 : Semiring S] →
                    [inst_25 : AddCommMonoid M] →
                      [inst_26 : AddCommMonoid M₂] →
                        [inst_27 : Module R M] →
                          [inst_28 : Module R M₂] →
                            [inst_29 : Module S M] →
                              [inst_30 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        h ∘ₗ
      f)
Q : Type (max v₂ u_5 u_4)
inst_20 : AddCommMonoid Q
inst_21 : Module S Q
inst_22 : Module T Q
inst_23 : IsScalarTower S T Q
r_1 : N →ₗ[S] Q
this_1 : Module R Q := Module.restrictScalars R S Q
this : IsScalarTower R S Q
r : R
x : Q
⊢ HSMul.hSMul (α := T) ((algebraMap R T : (a : R) → T) r : T) x = r • x

Tactic:
simp [IsScalarTower.algebraMap_apply R S T]

Premises used: IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
T : Type u_4
O : Type u_5
inst_9 : CommSemiring T
inst_10 : Algebra R T
inst_11 : Algebra S T
inst_12 : IsScalarTower R S T
inst_13 : AddCommMonoid O
inst_14 : Module R O
inst_15 : Module S O
inst_16 : Module T O
inst_17 : IsScalarTower S T O
inst_18 : IsScalarTower R S O
inst_19 : IsScalarTower R T O
f : M →ₗ[R] N
hf : IsBaseChange S f
h : N →ₗ[S] O
hc :
  IsBaseChange T
    ((↑R :
          {S : Type v₃} →
            {M : Type v₂} →
              {M₂ : Type u_5} →
                [inst : Semiring R] →
                  [inst_24 : Semiring S] →
                    [inst_25 : AddCommMonoid M] →
                      [inst_26 : AddCommMonoid M₂] →
                        [inst_27 : Module R M] →
                          [inst_28 : Module R M₂] →
                            [inst_29 : Module S M] →
                              [inst_30 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        h ∘ₗ
      f)
Q : Type (max v₂ u_5 u_4)
inst_20 : AddCommMonoid Q
inst_21 : Module S Q
inst_22 : Module T Q
inst_23 : IsScalarTower S T Q
r : N →ₗ[S] Q
this_1 : Module R Q := Module.restrictScalars R S Q
this : IsScalarTower R S Q
⊢ IsScalarTower R T Q

Tactic:
haveI : IsScalarTower R T Q := IsScalarTower.of_algebraMap_smul fun r x ↦ by
    simp [IsScalarTower.algebraMap_apply R S T]
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
T : Type u_4
O : Type u_5
inst_9 : CommSemiring T
inst_10 : Algebra R T
inst_11 : Algebra S T
inst_12 : IsScalarTower R S T
inst_13 : AddCommMonoid O
inst_14 : Module R O
inst_15 : Module S O
inst_16 : Module T O
inst_17 : IsScalarTower S T O
inst_18 : IsScalarTower R S O
inst_19 : IsScalarTower R T O
f : M →ₗ[R] N
hf : IsBaseChange S f
h : N →ₗ[S] O
hc :
  IsBaseChange T
    ((↑R :
          {S : Type v₃} →
            {M : Type v₂} →
              {M₂ : Type u_5} →
                [inst : Semiring R] →
                  [inst_24 : Semiring S] →
                    [inst_25 : AddCommMonoid M] →
                      [inst_26 : AddCommMonoid M₂] →
                        [inst_27 : Module R M] →
                          [inst_28 : Module R M₂] →
                            [inst_29 : Module S M] →
                              [inst_30 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        h ∘ₗ
      f)
Q : Type (max v₂ u_5 u_4)
inst_20 : AddCommMonoid Q
inst_21 : Module S Q
inst_22 : Module T Q
inst_23 : IsScalarTower S T Q
r : N →ₗ[S] Q
this_1 : Module R Q := Module.restrictScalars R S Q
this_2 : IsScalarTower R S Q
this : IsScalarTower R T Q
r' : M →ₗ[R] Q :=
  (↑R :
        {S : Type v₃} →
          {M : Type v₂} →
            {M₂ : Type (max (max u_4 u_5) v₂)} →
              [inst : Semiring R] →
                [inst_24 : Semiring S] →
                  [inst_25 : AddCommMonoid M] →
                    [inst_26 : AddCommMonoid M₂] →
                      [inst_27 : Module R M] →
                        [inst_28 : Module R M₂] →
                          [inst_29 : Module S M] →
                            [inst_30 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      r ∘ₗ
    f
q : O →ₗ[T] Q := hc.lift r'
⊢ ∃! g' : O →ₗ[T] Q,
    (↑S :
            {S_1 : Type u_4} →
              {M : Type u_5} →
                {M₂ : Type (max (max v₂ u_5) u_4)} →
                  [inst : Semiring S] →
                    [inst_24 : Semiring S_1] →
                      [inst_25 : AddCommMonoid M] →
                        [inst_26 : AddCommMonoid M₂] →
                          [inst_27 : Module S M] →
                            [inst_28 : Module S M₂] →
                              [inst_29 : Module S_1 M] →
                                [inst_30 : Module S_1 M₂] →
                                  [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
          g' ∘ₗ
        h =
      r

Tactic:
⟨q, ?_, ?_⟩

Premises used: ExistsUnique, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
T : Type u_4
O : Type u_5
inst_9 : CommSemiring T
inst_10 : Algebra R T
inst_11 : Algebra S T
inst_12 : IsScalarTower R S T
inst_13 : AddCommMonoid O
inst_14 : Module R O
inst_15 : Module S O
inst_16 : Module T O
inst_17 : IsScalarTower S T O
inst_18 : IsScalarTower R S O
inst_19 : IsScalarTower R T O
f : M →ₗ[R] N
hf : IsBaseChange S f
h : N →ₗ[S] O
⊢ IsBaseChange T
      ((↑R :
            {S : Type v₃} →
              {M : Type v₂} →
                {M₂ : Type u_5} →
                  [inst : Semiring R] →
                    [inst_20 : Semiring S] →
                      [inst_21 : AddCommMonoid M] →
                        [inst_22 : AddCommMonoid M₂] →
                          [inst_23 : Module R M] →
                            [inst_24 : Module R M₂] →
                              [inst_25 : Module S M] →
                                [inst_26 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          h ∘ₗ
        f) ↔
    IsBaseChange T h

Tactic:
⟨fun hc ↦ IsBaseChange.of_comp hf hc, fun hh ↦ IsBaseChange.comp hf hh⟩

Premises used: IsBaseChange.of_comp, Iff.intro, IsBaseChange.comp
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
f : M →ₗ[R] N
hf : IsBaseChange S f
x : R
h :
  ∀ (y : N),
    Eq (α := N)
      ((IsTensorProduct.map hf hf LinearMap.id ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) x) : (a : N) → N) y : N)
      (((↑R :
                {S : Type v₃} →
                  {M M₂ : Type v₂} →
                    [inst : Semiring R] →
                      [inst_9 : Semiring S] →
                        [inst_10 : AddCommMonoid M] →
                          [inst_11 : AddCommMonoid M₂] →
                            [inst_12 : Module R M] →
                              [inst_13 : Module R M₂] →
                                [inst_14 : Module S M] →
                                  [inst_15 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              (S := S) ((LinearMap.lsmul S N : (a : S) → N →ₗ[S] N) ((algebraMap R S : (a : R) → S) x)) :
            (a : N) → N)
          y :
        N)
⊢ IsTensorProduct.map hf hf LinearMap.id ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) x) =
    (↑R :
        {S : Type v₃} →
          {M M₂ : Type v₂} →
            [inst : Semiring R] →
              [inst_9 : Semiring S] →
                [inst_10 : AddCommMonoid M] →
                  [inst_11 : AddCommMonoid M₂] →
                    [inst_12 : Module R M] →
                      [inst_13 : Module R M₂] →
                        [inst_14 : Module S M] →
                          [inst_15 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (S := S) ((LinearMap.lsmul S N : (a : S) → N →ₗ[S] N) ((algebraMap R S : (a : R) → S) x))

Tactic:
ext y
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
f : M →ₗ[R] N
hf : IsBaseChange S f
x : R
y : N
⊢ Eq (α := N)
    ((IsTensorProduct.map hf hf LinearMap.id ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) x) : (a : N) → N) 0 : N)
    (((↑R :
              {S : Type v₃} →
                {M M₂ : Type v₂} →
                  [inst : Semiring R] →
                    [inst_9 : Semiring S] →
                      [inst_10 : AddCommMonoid M] →
                        [inst_11 : AddCommMonoid M₂] →
                          [inst_12 : Module R M] →
                            [inst_13 : Module R M₂] →
                              [inst_14 : Module S M] →
                                [inst_15 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (S := S) ((LinearMap.lsmul S N : (a : S) → N →ₗ[S] N) ((algebraMap R S : (a : R) → S) x)) :
          (a : N) → N)
        0 :
      N)

Tactic:
simp