awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
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
P : Type u_2
inst_9 : AddCommMonoid P
inst_10 : Module R P
A : Type u_4
inst_11 : CommSemiring A
inst_12 : Algebra R A
inst_13 : Algebra S A
inst_14 : IsScalarTower R S A
inst_15 : Module S M
inst_16 : IsScalarTower R S M
inst_17 : Module A N
inst_18 : IsScalarTower S A N
inst_19 : IsScalarTower R A N
f : M →ₗ[S] N
hf : IsBaseChange A f
e : A ⊗[S] (M ⊗[R] P) ≃ₗ[A] N ⊗[R] P :=
  (LinearEquiv.symm (AlgebraTensorModule.assoc R S A A M P) : A ⊗[S] (M ⊗[R] P) ≃ₗ[A] A ⊗[S] M ⊗[R] P) ≪≫ₗ
    (AlgebraTensorModule.congr hf.equiv (LinearEquiv.refl R P) : A ⊗[S] M ⊗[R] P ≃ₗ[A] N ⊗[R] P)
⊢ IsBaseChange (M := M ⊗[R] P) (N := N ⊗[R] P) A (AlgebraTensorModule.map f LinearMap.id : M ⊗[R] P →ₗ[S] N ⊗[R] P)
have refine : ∀ (x : M ⊗[R] P),
  Eq (α := N ⊗[R] P) ((e : (a : A ⊗[S] (M ⊗[R] P)) → N ⊗[R] P) (1 ⊗ₜ[S] x) : N ⊗[R] P)
    (((AlgebraTensorModule.map f LinearMap.id : M ⊗[R] P →ₗ[S] N ⊗[R] P) : (a : M ⊗[R] P) → N ⊗[R] P) x : N ⊗[R] P)
Tactic: refine IsBaseChange.of_equiv e (fun x ↦ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
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
P : Type u_2
inst_9 : AddCommMonoid P
inst_10 : Module R P
A : Type u_4
inst_11 : CommSemiring A
inst_12 : Algebra R A
inst_13 : Algebra S A
inst_14 : IsScalarTower R S A
inst_15 : Module S M
inst_16 : IsScalarTower R S M
inst_17 : Module A N
inst_18 : IsScalarTower S A N
inst_19 : IsScalarTower R A N
f : M →ₗ[S] N
hf : IsBaseChange A f
e : A ⊗[S] (M ⊗[R] P) ≃ₗ[A] N ⊗[R] P :=
  (LinearEquiv.symm (AlgebraTensorModule.assoc R S A A M P) : A ⊗[S] (M ⊗[R] P) ≃ₗ[A] A ⊗[S] M ⊗[R] P) ≪≫ₗ
    (AlgebraTensorModule.congr hf.equiv (LinearEquiv.refl R P) : A ⊗[S] M ⊗[R] P ≃ₗ[A] N ⊗[R] P)
x : M ⊗[R] P
⊢ Eq (α := N ⊗[R] P) ((e : (a : A ⊗[S] (M ⊗[R] P)) → N ⊗[R] P) (1 ⊗ₜ[S] x) : N ⊗[R] P)
    (((AlgebraTensorModule.map f LinearMap.id : M ⊗[R] P →ₗ[S] N ⊗[R] P) : (a : M ⊗[R] P) → N ⊗[R] P) x : N ⊗[R] P)
have zero : Eq (α := N ⊗[R] P) ((e : (a : A ⊗[S] (M ⊗[R] P)) → N ⊗[R] P) (1 ⊗ₜ[S] 0) : N ⊗[R] P)
  (((AlgebraTensorModule.map f LinearMap.id : M ⊗[R] P →ₗ[S] N ⊗[R] P) : (a : M ⊗[R] P) → N ⊗[R] P) 0 : N ⊗[R] P)
Tactic: induction x with
  | zero => simp
  | tmul => simp [e, IsBaseChange.equiv_tmul]
  | add _ _ h1 h2 => simp [tmul_add, h1, h2]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
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
P : Type u_2
inst_9 : AddCommMonoid P
inst_10 : Module R P
A : Type u_4
inst_11 : CommSemiring A
inst_12 : Algebra R A
inst_13 : Algebra S A
inst_14 : IsScalarTower R S A
inst_15 : Module S M
inst_16 : IsScalarTower R S M
inst_17 : Module A N
inst_18 : IsScalarTower S A N
inst_19 : IsScalarTower R A N
f : M →ₗ[S] N
hf : IsBaseChange A f
e : A ⊗[S] (M ⊗[R] P) ≃ₗ[A] N ⊗[R] P :=
  (LinearEquiv.symm (AlgebraTensorModule.assoc R S A A M P) : A ⊗[S] (M ⊗[R] P) ≃ₗ[A] A ⊗[S] M ⊗[R] P) ≪≫ₗ
    (AlgebraTensorModule.congr hf.equiv (LinearEquiv.refl R P) : A ⊗[S] M ⊗[R] P ≃ₗ[A] N ⊗[R] P)
x : M ⊗[R] P
zero :
  Eq (α := N ⊗[R] P) ((e : (a : A ⊗[S] (M ⊗[R] P)) → N ⊗[R] P) (1 ⊗ₜ[S] 0) : N ⊗[R] P)
    (((AlgebraTensorModule.map f LinearMap.id : M ⊗[R] P →ₗ[S] N ⊗[R] P) : (a : M ⊗[R] P) → N ⊗[R] P) 0 : N ⊗[R] P)
⊢ Eq (α := N ⊗[R] P) ((e : (a : A ⊗[S] (M ⊗[R] P)) → N ⊗[R] P) (1 ⊗ₜ[S] x) : N ⊗[R] P)
    (((AlgebraTensorModule.map f LinearMap.id : M ⊗[R] P →ₗ[S] N ⊗[R] P) : (a : M ⊗[R] P) → N ⊗[R] P) x : N ⊗[R] P)
have tmul : ∀ (x : M) (y : P),
  Eq (α := N ⊗[R] P) ((e : (a : A ⊗[S] (M ⊗[R] P)) → N ⊗[R] P) (1 ⊗ₜ[S] (x ⊗ₜ[R] y)) : N ⊗[R] P)
    (((AlgebraTensorModule.map f LinearMap.id : M ⊗[R] P →ₗ[S] N ⊗[R] P) : (a : M ⊗[R] P) → N ⊗[R] P) (x ⊗ₜ[R] y) :
      N ⊗[R] P)
Tactic: induction x with
  | zero => simp
  | tmul => simp [e, IsBaseChange.equiv_tmul]
  | add _ _ h1 h2 => simp [tmul_add, h1, h2]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
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
P : Type u_2
inst_9 : AddCommMonoid P
inst_10 : Module R P
A : Type u_4
inst_11 : CommSemiring A
inst_12 : Algebra R A
inst_13 : Algebra S A
inst_14 : IsScalarTower R S A
inst_15 : Module S M
inst_16 : IsScalarTower R S M
inst_17 : Module A N
inst_18 : IsScalarTower S A N
inst_19 : IsScalarTower R A N
f : M →ₗ[S] N
hf : IsBaseChange A f
e : A ⊗[S] (M ⊗[R] P) ≃ₗ[A] N ⊗[R] P :=
  (LinearEquiv.symm (AlgebraTensorModule.assoc R S A A M P) : A ⊗[S] (M ⊗[R] P) ≃ₗ[A] A ⊗[S] M ⊗[R] P) ≪≫ₗ
    (AlgebraTensorModule.congr hf.equiv (LinearEquiv.refl R P) : A ⊗[S] M ⊗[R] P ≃ₗ[A] N ⊗[R] P)
x : M ⊗[R] P
zero :
  Eq (α := N ⊗[R] P) ((e : (a : A ⊗[S] (M ⊗[R] P)) → N ⊗[R] P) (1 ⊗ₜ[S] 0) : N ⊗[R] P)
    (((AlgebraTensorModule.map f LinearMap.id : M ⊗[R] P →ₗ[S] N ⊗[R] P) : (a : M ⊗[R] P) → N ⊗[R] P) 0 : N ⊗[R] P)
tmul :
  ∀ (x : M) (y : P),
    Eq (α := N ⊗[R] P) ((e : (a : A ⊗[S] (M ⊗[R] P)) → N ⊗[R] P) (1 ⊗ₜ[S] (x ⊗ₜ[R] y)) : N ⊗[R] P)
      (((AlgebraTensorModule.map f LinearMap.id : M ⊗[R] P →ₗ[S] N ⊗[R] P) : (a : M ⊗[R] P) → N ⊗[R] P) (x ⊗ₜ[R] y) :
        N ⊗[R] P)
⊢ Eq (α := N ⊗[R] P) ((e : (a : A ⊗[S] (M ⊗[R] P)) → N ⊗[R] P) (1 ⊗ₜ[S] x) : N ⊗[R] P)
    (((AlgebraTensorModule.map f LinearMap.id : M ⊗[R] P →ₗ[S] N ⊗[R] P) : (a : M ⊗[R] P) → N ⊗[R] P) x : N ⊗[R] P)
have add : ∀ (x y : M ⊗[R] P)
  (h1 :
    Eq (α := N ⊗[R] P) ((e : (a : A ⊗[S] (M ⊗[R] P)) → N ⊗[R] P) (1 ⊗ₜ[S] x) : N ⊗[R] P)
      (((AlgebraTensorModule.map f LinearMap.id : M ⊗[R] P →ₗ[S] N ⊗[R] P) : (a : M ⊗[R] P) → N ⊗[R] P) x : N ⊗[R] P))
  (h2 :
    Eq (α := N ⊗[R] P) ((e : (a : A ⊗[S] (M ⊗[R] P)) → N ⊗[R] P) (1 ⊗ₜ[S] y) : N ⊗[R] P)
      (((AlgebraTensorModule.map f LinearMap.id : M ⊗[R] P →ₗ[S] N ⊗[R] P) : (a : M ⊗[R] P) → N ⊗[R] P) y : N ⊗[R] P)),
  Eq (α := N ⊗[R] P) ((e : (a : A ⊗[S] (M ⊗[R] P)) → N ⊗[R] P) (1 ⊗ₜ[S] (x + y)) : N ⊗[R] P)
    (((AlgebraTensorModule.map f LinearMap.id : M ⊗[R] P →ₗ[S] N ⊗[R] P) : (a : M ⊗[R] P) → N ⊗[R] P) (x + y) :
      N ⊗[R] P)
Tactic: induction x with
  | zero => simp
  | tmul => simp [e, IsBaseChange.equiv_tmul]
  | add _ _ h1 h2 => simp [tmul_add, h1, h2]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
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
h :
  ∀ (Q : Type (max v₁ v₂ v₃)) [inst_9 : AddCommMonoid Q] [inst_10 : Module R Q] [inst_11 : Module S Q]
    [inst_12 : IsScalarTower R S Q] (g : M →ₗ[R] Q),
    ∃! g' : N →ₗ[S] Q,
      (↑R :
              {S : Type v₃} →
                {M : Type v₂} →
                  {M₂ : Type (max (max v₁ v₂) v₃)} →
                    [inst : Semiring R] →
                      [inst_13 : Semiring S] →
                        [inst_14 : AddCommMonoid M] →
                          [inst_15 : AddCommMonoid M₂] →
                            [inst_16 : Module R M] →
                              [inst_17 : Module R M₂] →
                                [inst_18 : Module S M] →
                                  [inst_19 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            g' ∘ₗ
          f =
        g
⊢ IsBaseChange S f
have obtain : ∀ (g : N →ₗ[S] ULift.{v₂, max v₁ v₃} (S ⊗[R] M))
  (hg :
    Eq (α := M →ₗ[R] ULift.{v₂, max v₁ v₃} (S ⊗[R] M))
      ((↑R :
            {S : Type v₃} →
              {M : Type v₂} →
                {M₂ : Type (max (max v₁ v₂) 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₂)
          g ∘ₗ
        f)
      ((↑(LinearEquiv.symm ULift.moduleEquiv) : S ⊗[R] M →ₗ[R] ULift.{v₂, max v₁ v₃} (S ⊗[R] M)) ∘ₗ
        (mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) 1)),
  IsBaseChange S f
Tactic: obtain ⟨g, hg, -⟩ :=
    h (ULift.{v₂} <| S ⊗[R] M)
      (ULift.moduleEquiv.symm.toLinearMap.comp <| TensorProduct.mk R S M 1)
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
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
h :
  ∀ (Q : Type (max v₁ v₂ v₃)) [inst_9 : AddCommMonoid Q] [inst_10 : Module R Q] [inst_11 : Module S Q]
    [inst_12 : IsScalarTower R S Q] (g : M →ₗ[R] Q),
    ∃! g' : N →ₗ[S] Q,
      (↑R :
              {S : Type v₃} →
                {M : Type v₂} →
                  {M₂ : Type (max (max v₁ v₂) v₃)} →
                    [inst : Semiring R] →
                      [inst_13 : Semiring S] →
                        [inst_14 : AddCommMonoid M] →
                          [inst_15 : AddCommMonoid M₂] →
                            [inst_16 : Module R M] →
                              [inst_17 : Module R M₂] →
                                [inst_18 : Module S M] →
                                  [inst_19 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            g' ∘ₗ
          f =
        g
g : N →ₗ[S] ULift.{v₂, max v₁ v₃} (S ⊗[R] M)
hg :
  Eq (α := M →ₗ[R] ULift.{v₂, max v₁ v₃} (S ⊗[R] M))
    ((↑R :
          {S : Type v₃} →
            {M : Type v₂} →
              {M₂ : Type (max (max v₁ v₂) 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₂)
        g ∘ₗ
      f)
    ((↑(LinearEquiv.symm ULift.moduleEquiv) : S ⊗[R] M →ₗ[R] ULift.{v₂, max v₁ v₃} (S ⊗[R] M)) ∘ₗ
      (mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) 1)
f' : S ⊗[R] M →ₗ[R] N :=
  TensorProduct.lift
    ((↑R :
        {S M : Type v₃} →
          {M₂ : Type (max v₁ 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.flip (AlgHom.toLinearMap (Algebra.ofId S (Module.End S (M →ₗ[R] N)))) :
            (M →ₗ[R] N) →ₗ[S] S →ₗ[S] M →ₗ[R] N) :
          (a : M →ₗ[R] N) → S →ₗ[S] M →ₗ[R] N)
        f))
⊢ IsBaseChange S f
have change : Function.Bijective (α := S ⊗[R] M) (β := N) (⇑f' : (a : S ⊗[R] M) → N)
Tactic: change Function.Bijective f'
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
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
h :
  ∀ (Q : Type (max v₁ v₂ v₃)) [inst_9 : AddCommMonoid Q] [inst_10 : Module R Q] [inst_11 : Module S Q]
    [inst_12 : IsScalarTower R S Q] (g : M →ₗ[R] Q),
    ∃! g' : N →ₗ[S] Q,
      (↑R :
              {S : Type v₃} →
                {M : Type v₂} →
                  {M₂ : Type (max (max v₁ v₂) v₃)} →
                    [inst : Semiring R] →
                      [inst_13 : Semiring S] →
                        [inst_14 : AddCommMonoid M] →
                          [inst_15 : AddCommMonoid M₂] →
                            [inst_16 : Module R M] →
                              [inst_17 : Module R M₂] →
                                [inst_18 : Module S M] →
                                  [inst_19 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            g' ∘ₗ
          f =
        g
g : N →ₗ[S] ULift.{v₂, max v₁ v₃} (S ⊗[R] M)
hg :
  Eq (α := M →ₗ[R] ULift.{v₂, max v₁ v₃} (S ⊗[R] M))
    ((↑R :
          {S : Type v₃} →
            {M : Type v₂} →
              {M₂ : Type (max (max v₁ v₂) 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₂)
        g ∘ₗ
      f)
    ((↑(LinearEquiv.symm ULift.moduleEquiv) : S ⊗[R] M →ₗ[R] ULift.{v₂, max v₁ v₃} (S ⊗[R] M)) ∘ₗ
      (mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) 1)
f' : S ⊗[R] M →ₗ[R] N :=
  TensorProduct.lift
    ((↑R :
        {S M : Type v₃} →
          {M₂ : Type (max v₁ 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.flip (AlgHom.toLinearMap (Algebra.ofId S (Module.End S (M →ₗ[R] N)))) :
            (M →ₗ[R] N) →ₗ[S] S →ₗ[S] M →ₗ[R] N) :
          (a : M →ₗ[R] N) → S →ₗ[S] M →ₗ[R] N)
        f))
s : S
x : S ⊗[R] M
⊢ f'.toFun (HSMul.hSMul (β := S ⊗[R] M) s 0) = HSMul.hSMul (α := S) ((RingHom.id S : (a : S) → S) s : S) (f'.toFun 0)
have refine_1 : (f' : (a : S ⊗[R] M) → N) (HSMul.hSMul (β := S ⊗[R] M) s 0) = HSMul.hSMul (β := N) s ((f' : (a : S ⊗[R] M) → N) 0 : N)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
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
h :
  ∀ (Q : Type (max v₁ v₂ v₃)) [inst_9 : AddCommMonoid Q] [inst_10 : Module R Q] [inst_11 : Module S Q]
    [inst_12 : IsScalarTower R S Q] (g : M →ₗ[R] Q),
    ∃! g' : N →ₗ[S] Q,
      (↑R :
              {S : Type v₃} →
                {M : Type v₂} →
                  {M₂ : Type (max (max v₁ v₂) v₃)} →
                    [inst : Semiring R] →
                      [inst_13 : Semiring S] →
                        [inst_14 : AddCommMonoid M] →
                          [inst_15 : AddCommMonoid M₂] →
                            [inst_16 : Module R M] →
                              [inst_17 : Module R M₂] →
                                [inst_18 : Module S M] →
                                  [inst_19 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            g' ∘ₗ
          f =
        g
g : N →ₗ[S] ULift.{v₂, max v₁ v₃} (S ⊗[R] M)
hg :
  Eq (α := M →ₗ[R] ULift.{v₂, max v₁ v₃} (S ⊗[R] M))
    ((↑R :
          {S : Type v₃} →
            {M : Type v₂} →
              {M₂ : Type (max (max v₁ v₂) 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₂)
        g ∘ₗ
      f)
    ((↑(LinearEquiv.symm ULift.moduleEquiv) : S ⊗[R] M →ₗ[R] ULift.{v₂, max v₁ v₃} (S ⊗[R] M)) ∘ₗ
      (mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) 1)
f' : S ⊗[R] M →ₗ[R] N :=
  TensorProduct.lift
    ((↑R :
        {S M : Type v₃} →
          {M₂ : Type (max v₁ 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.flip (AlgHom.toLinearMap (Algebra.ofId S (Module.End S (M →ₗ[R] N)))) :
            (M →ₗ[R] N) →ₗ[S] S →ₗ[S] M →ₗ[R] N) :
          (a : M →ₗ[R] N) → S →ₗ[S] M →ₗ[R] N)
        f))
s : S
x : S ⊗[R] M
⊢ (f' : (a : S ⊗[R] M) → N) (HSMul.hSMul (β := S ⊗[R] M) s 0) = HSMul.hSMul (β := N) s ((f' : (a : S ⊗[R] M) → N) 0 : N)
have refine_1 : (f' : (a : S ⊗[R] M) → N) (HSMul.hSMul (β := S ⊗[R] M) s 0) = HSMul.hSMul (β := N) s 0
Tactic: rw [map_zero, smul_zero, map_zero, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
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
h :
  ∀ (Q : Type (max v₁ v₂ v₃)) [inst_9 : AddCommMonoid Q] [inst_10 : Module R Q] [inst_11 : Module S Q]
    [inst_12 : IsScalarTower R S Q] (g : M →ₗ[R] Q),
    ∃! g' : N →ₗ[S] Q,
      (↑R :
              {S : Type v₃} →
                {M : Type v₂} →
                  {M₂ : Type (max (max v₁ v₂) v₃)} →
                    [inst : Semiring R] →
                      [inst_13 : Semiring S] →
                        [inst_14 : AddCommMonoid M] →
                          [inst_15 : AddCommMonoid M₂] →
                            [inst_16 : Module R M] →
                              [inst_17 : Module R M₂] →
                                [inst_18 : Module S M] →
                                  [inst_19 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            g' ∘ₗ
          f =
        g
g : N →ₗ[S] ULift.{v₂, max v₁ v₃} (S ⊗[R] M)
f' : S ⊗[R] M →ₗ[R] N :=
  TensorProduct.lift
    ((↑R :
        {S M : Type v₃} →
          {M₂ : Type (max v₁ 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.flip (AlgHom.toLinearMap (Algebra.ofId S (Module.End S (M →ₗ[R] N)))) :
            (M →ₗ[R] N) →ₗ[S] S →ₗ[S] M →ₗ[R] N) :
          (a : M →ₗ[R] N) → S →ₗ[S] M →ₗ[R] N)
        f))
f'' : S ⊗[R] M →ₗ[S] N := { toAddHom := f'.toAddHom, map_smul' := ⋯ }
hg :
  ∀ (x : M),
    Eq (α := ULift.{v₂, max v₁ v₃} (S ⊗[R] M))
      ((g : (a : N) → ULift.{v₂, max v₁ v₃} (S ⊗[R] M)) ((f : (a : M) → N) x) : ULift.{v₂, max v₁ v₃} (S ⊗[R] M))
      (((↑(LinearEquiv.symm ULift.moduleEquiv) : S ⊗[R] M →ₗ[R] ULift.{v₂, max v₁ v₃} (S ⊗[R] M)) :
            (a : S ⊗[R] M) → ULift.{v₂, max v₁ v₃} (S ⊗[R] M))
          (((mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) 1 : (a : M) → S ⊗[R] M) x) :
        ULift.{v₂, max v₁ v₃} (S ⊗[R] M))
refine_3 : Function.Bijective (α := S ⊗[R] M) (β := N) (⇑f' : (a : S ⊗[R] M) → N)
⊢ Function.Bijective (α := S ⊗[R] M) (β := N) (⇑f' : (a : S ⊗[R] M) → N)
have refine_1 : f'' ∘ₗ (↑ULift.moduleEquiv : ULift.{v₂, max v₁ v₃} (S ⊗[R] M) →ₗ[S] S ⊗[R] M) ∘ₗ g = LinearMap.id
Tactic: let fe : S ⊗[R] M ≃ₗ[S] N :=
    LinearEquiv.ofLinear f'' (ULift.moduleEquiv.toLinearMap.comp g) ?_ ?_