awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (hypothesis)
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
g : N →ₗ[S] O
hg : IsBaseChange T g
Q : Type (max v₁ u_5 u_4)
inst_20 : AddCommMonoid Q
inst_21 : Module R Q
inst_22 : Module T Q
inst_23 : IsScalarTower R T Q
i : M →ₗ[R] Q
this : Module S Q := Module.compHom Q (algebraMap S T)
⊢ ∃! g' : O →ₗ[T] Q,
    (↑R :
            {S : Type u_4} →
              {M : Type u_5} →
                {M₂ : Type (max (max v₁ u_5) u_4)} →
                  [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₂)
          g' ∘ₗ
        (↑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₂)
            g ∘ₗ
          f =
      i
have this₁ : IsScalarTower S T Q
Tactic: haveI : IsScalarTower S T Q :=
    ⟨fun x y z => by
      rw [Algebra.smul_def, mul_smul]
      rfl⟩
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (hypothesis)
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
g : N →ₗ[S] O
hg : IsBaseChange T g
Q : Type (max v₁ u_5 u_4)
inst_20 : AddCommMonoid Q
inst_21 : Module R Q
inst_22 : Module T Q
inst_23 : IsScalarTower R T Q
i : M →ₗ[R] Q
this_1 : Module S Q := Module.compHom Q (algebraMap S T)
this : IsScalarTower S T Q
⊢ ∃! g' : O →ₗ[T] Q,
    (↑R :
            {S : Type u_4} →
              {M : Type u_5} →
                {M₂ : Type (max (max v₁ u_5) u_4)} →
                  [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₂)
          g' ∘ₗ
        (↑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₂)
            g ∘ₗ
          f =
      i
have this₁ : IsScalarTower R S Q
Tactic: have : IsScalarTower R S Q := IsScalarTower.to₁₂₄ _ _ T _
-- 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
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_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
have h₁ : ∀ (Q : Type (max v₂ u_5 u_4)) [inst : AddCommMonoid Q] [inst_20 : 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: apply IsBaseChange.of_lift_unique
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (hypothesis)
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
⊢ ∃! 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
have this₁ : IsScalarTower R S Q
Tactic: haveI : IsScalarTower R S Q := .restrictScalars R S Q
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (hypothesis)
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
⊢ ∃! 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
have this₁ : 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]
-- 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
hf : IsBaseChange S f
x : R
⊢ 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))
have 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)
Tactic: ext y
-- 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_1 : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst_9 : AddCommMonoid P
inst_10 : Module R P
inst_11 : AddCommMonoid Q
inst_12 : Module S Q
inst_13 : Module R Q
inst_14 : IsScalarTower R S Q
f' : P →ₗ[R] Q
T : Type u_4
O : Type u_5
inst_15 : CommSemiring T
inst_16 : Algebra R T
inst_17 : Algebra S T
inst_18 : IsScalarTower R S T
inst_19 : AddCommMonoid O
inst_20 : Module R O
inst_21 : Module S O
inst_22 : Module T O
inst_23 : IsScalarTower S T O
inst_24 : IsScalarTower R S O
inst_25 : IsScalarTower R T O
R' : Type u_6
S' : Type u_7
inst_26 : CommSemiring R'
inst_27 : CommSemiring S'
inst_28 : Algebra R R'
inst_29 : Algebra S S'
inst_30 : Algebra R' S'
inst_31 : Algebra R S'
inst_32 : IsScalarTower R R' S'
inst_33 : IsScalarTower R S S'
h : IsPushout R S R' S'
x y : S ⊗[R] R'
⊢ AddHom.toFun
      (LinearMap.toAddHom (↑(IsBaseChange.equiv (f := AlgHom.toLinearMap (toAlgHom R R' S')) ⋯) : S ⊗[R] R' →ₗ[S] S'))
      (x * y) =
    HMul.hMul (α := S')
      (AddHom.toFun
        (LinearMap.toAddHom (↑(IsBaseChange.equiv (f := AlgHom.toLinearMap (toAlgHom R R' S')) ⋯) : S ⊗[R] R' →ₗ[S] S'))
        x)
      (AddHom.toFun
        (LinearMap.toAddHom (↑(IsBaseChange.equiv (f := AlgHom.toLinearMap (toAlgHom R R' S')) ⋯) : S ⊗[R] R' →ₗ[S] S'))
        y)
have dsimp : (IsBaseChange.equiv (f := AlgHom.toLinearMap (toAlgHom R R' S')) sorry : (a : S ⊗[R] R') → S') (x * y) =
  HMul.hMul (α := S') (β := S')
    ((IsBaseChange.equiv (f := AlgHom.toLinearMap (toAlgHom R R' S')) sorry : (a : S ⊗[R] R') → S') x : S')
    ((IsBaseChange.equiv (f := AlgHom.toLinearMap (toAlgHom R R' S')) sorry : (a : S ⊗[R] R') → S') y : S')
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_1 : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst_9 : AddCommMonoid P
inst_10 : Module R P
inst_11 : AddCommMonoid Q
inst_12 : Module S Q
inst_13 : Module R Q
inst_14 : IsScalarTower R S Q
f' : P →ₗ[R] Q
T : Type u_4
O : Type u_5
inst_15 : CommSemiring T
inst_16 : Algebra R T
inst_17 : Algebra S T
inst_18 : IsScalarTower R S T
inst_19 : AddCommMonoid O
inst_20 : Module R O
inst_21 : Module S O
inst_22 : Module T O
inst_23 : IsScalarTower S T O
inst_24 : IsScalarTower R S O
inst_25 : IsScalarTower R T O
R' : Type u_6
S' : Type u_7
inst_26 : CommSemiring R'
inst_27 : CommSemiring S'
inst_28 : Algebra R R'
inst_29 : Algebra S S'
inst_30 : Algebra R' S'
inst_31 : Algebra R S'
inst_32 : IsScalarTower R R' S'
inst_33 : IsScalarTower R S S'
h : IsPushout R S R' S'
y : S ⊗[R] R'
a : S
b : R'
⊢ (IsBaseChange.equiv (f := AlgHom.toLinearMap (toAlgHom R R' S')) ⋯ : (a : S ⊗[R] R') → S') (a ⊗ₜ[R] b * y) =
    HMul.hMul (α := S') (β := S')
      ((IsBaseChange.equiv (f := AlgHom.toLinearMap (toAlgHom R R' S')) ⋯ : (a : S ⊗[R] R') → S') (a ⊗ₜ[R] b) : S')
      ((IsBaseChange.equiv (f := AlgHom.toLinearMap (toAlgHom R R' S')) ⋯ : (a : S ⊗[R] R') → S') y : S')
have tmul : (IsBaseChange.equiv (f := AlgHom.toLinearMap (toAlgHom R R' S')) sorry : (a : S ⊗[R] R') → S')
    (HMul.hMul (α := S ⊗[R] R') (a ⊗ₜ[R] b) 0) =
  HMul.hMul (α := S') (β := S')
    ((IsBaseChange.equiv (f := AlgHom.toLinearMap (toAlgHom R R' S')) sorry : (a : S ⊗[R] R') → S') (a ⊗ₜ[R] b) : S')
    ((IsBaseChange.equiv (f := AlgHom.toLinearMap (toAlgHom R R' S')) sorry : (a : S ⊗[R] R') → S') 0 : S')
Tactic: induction y with
      | zero => simp
      | add x y _ _ => simp [*, mul_add]
      | tmul x y => simp [IsBaseChange.equiv_tmul, Algebra.smul_def, mul_mul_mul_comm]
Cleared hypotheses: y
-- 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_1 : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst_9 : AddCommMonoid P
inst_10 : Module R P
inst_11 : AddCommMonoid Q
inst_12 : Module S Q
inst_13 : Module R Q
inst_14 : IsScalarTower R S Q
f' : P →ₗ[R] Q
T : Type u_4
O : Type u_5
inst_15 : CommSemiring T
inst_16 : Algebra R T
inst_17 : Algebra S T
inst_18 : IsScalarTower R S T
inst_19 : AddCommMonoid O
inst_20 : Module R O
inst_21 : Module S O
inst_22 : Module T O
inst_23 : IsScalarTower S T O
inst_24 : IsScalarTower R S O
inst_25 : IsScalarTower R T O
R' : Type u_6
S' : Type u_7
inst_26 : CommSemiring R'
inst_27 : CommSemiring S'
inst_28 : Algebra R R'
inst_29 : Algebra S S'
inst_30 : Algebra R' S'
inst_31 : Algebra R S'
inst_32 : IsScalarTower R R' S'
inst_33 : IsScalarTower R S S'
h : IsPushout R S R' S'
x y : S ⊗[R] R'
⊢ (IsBaseChange.equiv (f := AlgHom.toLinearMap (toAlgHom R R' S')) ⋯ : (a : S ⊗[R] R') → S') (x * y) =
    HMul.hMul (α := S') (β := S')
      ((IsBaseChange.equiv (f := AlgHom.toLinearMap (toAlgHom R R' S')) ⋯ : (a : S ⊗[R] R') → S') x : S')
      ((IsBaseChange.equiv (f := AlgHom.toLinearMap (toAlgHom R R' S')) ⋯ : (a : S ⊗[R] R') → S') y : S')
have zero : (IsBaseChange.equiv (f := AlgHom.toLinearMap (toAlgHom R R' S')) sorry : (a : S ⊗[R] R') → S') (0 * y) =
  HMul.hMul (α := S') (β := S')
    ((IsBaseChange.equiv (f := AlgHom.toLinearMap (toAlgHom R R' S')) sorry : (a : S ⊗[R] R') → S') 0 : S')
    ((IsBaseChange.equiv (f := AlgHom.toLinearMap (toAlgHom R R' S')) sorry : (a : S ⊗[R] R') → S') y : S')
Tactic: induction x with
    | zero => simp
    | add x y _ _ => simp [*, add_mul]
    | tmul a b =>
      induction y with
      | zero => simp
      | add x y _ _ => simp [*, mul_add]
      | tmul x y => simp [IsBaseChange.equiv_tmul, Algebra.smul_def, mul_mul_mul_comm]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
S : Type v₃
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
R' : Type u_6
S' : Type u_7
inst_3 : CommSemiring R'
inst_4 : CommSemiring S'
inst_5 : Algebra R R'
inst_6 : Algebra S S'
inst_7 : Algebra R' S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
inst_11 : IsPushout R S R' S'
a : S
⊢ Eq (α := S ⊗[R] R')
    ((AlgEquiv.symm (equiv R S R' S') : (a : S') → S ⊗[R] R') ((algebraMap S S' : (a : S) → S') a) : S ⊗[R] R')
    (a ⊗ₜ[R] 1 : S ⊗[R] R')
have rw : Eq.{u_7 + 1} (α := S') ((algebraMap S S' : (a : S) → S') a : S')
  ((equiv R S R' S' : (a : S ⊗[R] R') → S') (a ⊗ₜ[R] 1) : S')
Tactic: rw [(equiv R S R' S').symm_apply_eq, equiv_tmul, map_one, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
S : Type v₃
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
R' : Type u_6
S' : Type u_7
inst_3 : CommSemiring R'
inst_4 : CommSemiring S'
inst_5 : Algebra R R'
inst_6 : Algebra S S'
inst_7 : Algebra R' S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
inst_11 : IsPushout R S R' S'
a : S
rw :
  Eq.{u_7 + 1} (α := S') ((algebraMap S S' : (a : S) → S') a : S')
    ((equiv R S R' S' : (a : S ⊗[R] R') → S') (a ⊗ₜ[R] 1) : S')
⊢ Eq (α := S ⊗[R] R')
    ((AlgEquiv.symm (equiv R S R' S') : (a : S') → S ⊗[R] R') ((algebraMap S S' : (a : S) → S') a) : S ⊗[R] R')
    (a ⊗ₜ[R] 1 : S ⊗[R] R')
have rw₁ : (algebraMap S S' : (a : S) → S') a =
  HMul.hMul (α := S') (β := S') ((algebraMap S S' : (a : S) → S') a : S') ((algebraMap R' S' : (a : R') → S') 1 : S')
Tactic: rw [(equiv R S R' S').symm_apply_eq, equiv_tmul, map_one, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
S : Type v₃
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
R' : Type u_6
S' : Type u_7
inst_3 : CommSemiring R'
inst_4 : CommSemiring S'
inst_5 : Algebra R R'
inst_6 : Algebra S S'
inst_7 : Algebra R' S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
inst_11 : IsPushout R S R' S'
a : S
rw :
  Eq.{u_7 + 1} (α := S') ((algebraMap S S' : (a : S) → S') a : S')
    ((equiv R S R' S' : (a : S ⊗[R] R') → S') (a ⊗ₜ[R] 1) : S')
rw₁ :
  (algebraMap S S' : (a : S) → S') a =
    HMul.hMul (α := S') (β := S') ((algebraMap S S' : (a : S) → S') a : S') ((algebraMap R' S' : (a : R') → S') 1 : S')
⊢ Eq (α := S ⊗[R] R')
    ((AlgEquiv.symm (equiv R S R' S') : (a : S') → S ⊗[R] R') ((algebraMap S S' : (a : S) → S') a) : S ⊗[R] R')
    (a ⊗ₜ[R] 1 : S ⊗[R] R')
have rw₂ : (algebraMap S S' : (a : S) → S') a = HMul.hMul (α := S') (β := S') ((algebraMap S S' : (a : S) → S') a : S') (1 : S')
Tactic: rw [(equiv R S R' S').symm_apply_eq, equiv_tmul, map_one, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
S : Type v₃
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
R' : Type u_6
S' : Type u_7
inst_3 : CommSemiring R'
inst_4 : CommSemiring S'
inst_5 : Algebra R R'
inst_6 : Algebra S S'
inst_7 : Algebra R' S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
inst_11 : IsPushout R S R' S'
a : S
rw :
  Eq.{u_7 + 1} (α := S') ((algebraMap S S' : (a : S) → S') a : S')
    ((equiv R S R' S' : (a : S ⊗[R] R') → S') (a ⊗ₜ[R] 1) : S')
rw₁ :
  (algebraMap S S' : (a : S) → S') a =
    HMul.hMul (α := S') (β := S') ((algebraMap S S' : (a : S) → S') a : S') ((algebraMap R' S' : (a : R') → S') 1 : S')
rw₂ :
  (algebraMap S S' : (a : S) → S') a = HMul.hMul (α := S') (β := S') ((algebraMap S S' : (a : S) → S') a : S') (1 : S')
⊢ Eq (α := S ⊗[R] R')
    ((AlgEquiv.symm (equiv R S R' S') : (a : S') → S ⊗[R] R') ((algebraMap S S' : (a : S) → S') a) : S ⊗[R] R')
    (a ⊗ₜ[R] 1 : S ⊗[R] R')
have rw₃ : Eq.{u_7 + 1} (α := S') ((algebraMap S S' : (a : S) → S') a : S') ((algebraMap S S' : (a : S) → S') a : S')
Tactic: rw [(equiv R S R' S').symm_apply_eq, equiv_tmul, map_one, mul_one]