awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : R'
⊢ Eq (α := S ⊗[R] R')
    ((AlgEquiv.symm (equiv R S R' S') : (a : S') → S ⊗[R] R') ((algebraMap R' S' : (a : R') → S') a) : S ⊗[R] R')
    (1 ⊗ₜ[R] a : S ⊗[R] R')
have rw : Eq.{u_7 + 1} (α := S') ((algebraMap R' S' : (a : R') → S') a : S')
  ((equiv R S R' S' : (a : S ⊗[R] R') → S') (1 ⊗ₜ[R] a) : S')
Tactic: rw [(equiv R S R' S').symm_apply_eq, equiv_tmul, map_one, one_mul]
-- 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 : R'
rw :
  Eq.{u_7 + 1} (α := S') ((algebraMap R' S' : (a : R') → S') a : S')
    ((equiv R S R' S' : (a : S ⊗[R] R') → S') (1 ⊗ₜ[R] a) : S')
⊢ Eq (α := S ⊗[R] R')
    ((AlgEquiv.symm (equiv R S R' S') : (a : S') → S ⊗[R] R') ((algebraMap R' S' : (a : R') → S') a) : S ⊗[R] R')
    (1 ⊗ₜ[R] a : S ⊗[R] R')
have rw₁ : (algebraMap R' S' : (a : R') → S') a =
  HMul.hMul (α := S') (β := S') ((algebraMap S S' : (a : S) → S') 1 : S') ((algebraMap R' S' : (a : R') → S') a : S')
Tactic: rw [(equiv R S R' S').symm_apply_eq, equiv_tmul, map_one, one_mul]
-- 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 : R'
rw :
  Eq.{u_7 + 1} (α := S') ((algebraMap R' S' : (a : R') → S') a : S')
    ((equiv R S R' S' : (a : S ⊗[R] R') → S') (1 ⊗ₜ[R] a) : S')
rw₁ :
  (algebraMap R' S' : (a : R') → S') a =
    HMul.hMul (α := S') (β := S') ((algebraMap S S' : (a : S) → S') 1 : S') ((algebraMap R' S' : (a : R') → S') a : S')
⊢ Eq (α := S ⊗[R] R')
    ((AlgEquiv.symm (equiv R S R' S') : (a : S') → S ⊗[R] R') ((algebraMap R' S' : (a : R') → S') a) : S ⊗[R] R')
    (1 ⊗ₜ[R] a : S ⊗[R] R')
have rw₂ : (algebraMap R' S' : (a : R') → S') a =
  HMul.hMul (α := S') (β := S') (1 : S') ((algebraMap R' S' : (a : R') → S') a : S')
Tactic: rw [(equiv R S R' S').symm_apply_eq, equiv_tmul, map_one, one_mul]
-- 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 : R'
rw :
  Eq.{u_7 + 1} (α := S') ((algebraMap R' S' : (a : R') → S') a : S')
    ((equiv R S R' S' : (a : S ⊗[R] R') → S') (1 ⊗ₜ[R] a) : S')
rw₁ :
  (algebraMap R' S' : (a : R') → S') a =
    HMul.hMul (α := S') (β := S') ((algebraMap S S' : (a : S) → S') 1 : S') ((algebraMap R' S' : (a : R') → S') a : S')
rw₂ :
  (algebraMap R' S' : (a : R') → S') a =
    HMul.hMul (α := S') (β := S') (1 : S') ((algebraMap R' S' : (a : R') → S') a : S')
⊢ Eq (α := S ⊗[R] R')
    ((AlgEquiv.symm (equiv R S R' S') : (a : S') → S ⊗[R] R') ((algebraMap R' S' : (a : R') → S') a) : S ⊗[R] R')
    (1 ⊗ₜ[R] a : S ⊗[R] R')
have rw₃ : Eq.{u_7 + 1} (α := S') ((algebraMap R' S' : (a : R') → S') a : S') ((algebraMap R' S' : (a : R') → S') a : S')
Tactic: rw [(equiv R S R' S').symm_apply_eq, equiv_tmul, map_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_8
S : Type u_9
A : Type u_10
B : Type u_11
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring A
inst_3 : CommSemiring B
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra A B
inst_7 : IsScalarTower R A B
inst_8 : Algebra R S
x : Algebra (A ⊗[R] S) (B ⊗[R] S)
h : IsScalarTower A (A ⊗[R] S) (B ⊗[R] S)
H :
  Eq (α := S →+* B ⊗[R] S)
    (@RingHom.comp _ (A ⊗[R] S) _ _ Semiring.toNonAssocSemiring _ (algebraMap (A ⊗[R] S) (B ⊗[R] S))
      (AlgHom.toRingHom TensorProduct.includeRight))
    (AlgHom.toRingHom TensorProduct.includeRight)
⊢ IsPushout A B (A ⊗[R] S) (B ⊗[R] S)
have out : IsBaseChange (M := A ⊗[R] S) (N := B ⊗[R] S) B (AlgHom.toLinearMap (toAlgHom A (A ⊗[R] S) (B ⊗[R] S)))
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_8
S : Type u_9
A : Type u_10
B : Type u_11
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring A
inst_3 : CommSemiring B
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra A B
inst_7 : IsScalarTower R A B
inst_8 : Algebra R S
x : Algebra (A ⊗[R] S) (B ⊗[R] S)
h : IsScalarTower A (A ⊗[R] S) (B ⊗[R] S)
H :
  Eq (α := S →+* B ⊗[R] S)
    (@RingHom.comp _ (A ⊗[R] S) _ _ Semiring.toNonAssocSemiring _ (algebraMap (A ⊗[R] S) (B ⊗[R] S))
      (AlgHom.toRingHom TensorProduct.includeRight))
    (AlgHom.toRingHom TensorProduct.includeRight)
⊢ IsBaseChange (M := A ⊗[R] S) (N := B ⊗[R] S) B (AlgHom.toLinearMap (toAlgHom A (A ⊗[R] S) (B ⊗[R] S)))
have h : Eq (α := AddCommMonoid (A ⊗[R] S)) NonUnitalNonAssocSemiring.toAddCommMonoid addCommMonoid →
  Eq (α := AddCommMonoid (B ⊗[R] S)) NonUnitalNonAssocSemiring.toAddCommMonoid addCommMonoid →
    HEq (α := Module A (A ⊗[R] S)) toModule (β := Module A (A ⊗[R] S)) leftModule →
      HEq (α := Module A (B ⊗[R] S)) toModule (β := Module A (B ⊗[R] S)) leftModule →
        Eq (α := A ⊗[R] S →ₗ[A] B ⊗[R] S) (AlgHom.toLinearMap (toAlgHom A (A ⊗[R] S) (B ⊗[R] S)))
          (AlgebraTensorModule.map (Algebra.linearMap A B) LinearMap.id)
Tactic: convert! isBaseChange_tensorProduct_map (R := R) (P := S) _ (IsBaseChange.linearMap A B)
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_8
S : Type u_9
A : Type u_10
B : Type u_11
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring A
inst_3 : CommSemiring B
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra A B
inst_7 : IsScalarTower R A B
inst_8 : Algebra R S
x : Algebra (A ⊗[R] S) (B ⊗[R] S)
h : IsScalarTower A (A ⊗[R] S) (B ⊗[R] S)
H :
  Eq (α := S →+* B ⊗[R] S)
    (@RingHom.comp _ (A ⊗[R] S) _ _ Semiring.toNonAssocSemiring _ (algebraMap (A ⊗[R] S) (B ⊗[R] S))
      (AlgHom.toRingHom TensorProduct.includeRight))
    (AlgHom.toRingHom TensorProduct.includeRight)
e_5 : Eq (α := AddCommMonoid (A ⊗[R] S)) NonUnitalNonAssocSemiring.toAddCommMonoid addCommMonoid
e_6 : Eq (α := AddCommMonoid (B ⊗[R] S)) NonUnitalNonAssocSemiring.toAddCommMonoid addCommMonoid
e_10 : HEq (α := Module A (A ⊗[R] S)) toModule (β := Module A (A ⊗[R] S)) leftModule
e_11 : HEq (α := Module A (B ⊗[R] S)) toModule (β := Module A (B ⊗[R] S)) leftModule
⊢ Eq (α := A ⊗[R] S →ₗ[A] B ⊗[R] S) (AlgHom.toLinearMap (toAlgHom A (A ⊗[R] S) (B ⊗[R] S)))
    (AlgebraTensorModule.map (Algebra.linearMap A B) LinearMap.id)
have h : ∀ (s : S),
  Eq (α := B ⊗[R] S)
    ((((AlgebraTensorModule.curry (AlgHom.toLinearMap (toAlgHom A (A ⊗[R] S) (B ⊗[R] S))) : A →ₗ[A] S →ₗ[R] B ⊗[R] S) :
              (a : A) → S →ₗ[R] B ⊗[R] S)
            1 :
          (a : S) → B ⊗[R] S)
        s :
      B ⊗[R] S)
    ((((AlgebraTensorModule.curry (AlgebraTensorModule.map (Algebra.linearMap A B) LinearMap.id) :
                A →ₗ[A] S →ₗ[R] B ⊗[R] S) :
              (a : A) → S →ₗ[R] B ⊗[R] S)
            1 :
          (a : S) → B ⊗[R] S)
        s :
      B ⊗[R] S)
Tactic: ext s
-- 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'
H : IsPushout R S R' S'
A : Type u_8
inst_11 : Semiring A
inst_12 : Algebra R A
f g : S' →ₐ[R] A
h₁ : Eq (α := R' →ₐ[R] A) (f.comp (toAlgHom R R' S')) (g.comp (toAlgHom R R' S'))
h₂ : Eq (α := S →ₐ[R] A) (f.comp (toAlgHom R S S')) (g.comp (toAlgHom R S S'))
⊢ f = g
have H₁ : ∀ (x : S'), Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) x : A) ((g : (a : S') → A) x : A)
Tactic: ext 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'
H : IsPushout R S R' S'
A : Type u_8
inst_11 : Semiring A
inst_12 : Algebra R A
f g : S' →ₐ[R] A
h₁ : Eq (α := R' →ₐ[R] A) (f.comp (toAlgHom R R' S')) (g.comp (toAlgHom R R' S'))
h₂ : Eq (α := S →ₐ[R] A) (f.comp (toAlgHom R S S')) (g.comp (toAlgHom R S S'))
x : S'
⊢ Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) x : A) ((g : (a : S') → A) x : A)
have H₁ : Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) 0 : A) ((g : (a : S') → A) 0 : A)
Tactic: refine H.1.inductionOn 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'
H : IsPushout R S R' S'
A : Type u_8
inst_11 : Semiring A
inst_12 : Algebra R A
f g : S' →ₐ[R] A
h₁ : Eq (α := R' →ₐ[R] A) (f.comp (toAlgHom R R' S')) (g.comp (toAlgHom R R' S'))
h₂ : Eq (α := S →ₐ[R] A) (f.comp (toAlgHom R S S')) (g.comp (toAlgHom R S S'))
x : S'
H₁ : Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) 0 : A) ((g : (a : S') → A) 0 : A)
⊢ Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) x : A) ((g : (a : S') → A) x : A)
have H₂ : ∀ (m : R'),
  Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) ((AlgHom.toLinearMap (toAlgHom R R' S') : (a : R') → S') m : S') : A)
    ((g : (a : S') → A) ((AlgHom.toLinearMap (toAlgHom R R' S') : (a : R') → S') m : S') : A)
Tactic: refine H.1.inductionOn 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'
H : IsPushout R S R' S'
A : Type u_8
inst_11 : Semiring A
inst_12 : Algebra R A
f g : S' →ₐ[R] A
h₁ : Eq (α := R' →ₐ[R] A) (f.comp (toAlgHom R R' S')) (g.comp (toAlgHom R R' S'))
h₂ : Eq (α := S →ₐ[R] A) (f.comp (toAlgHom R S S')) (g.comp (toAlgHom R S S'))
x : S'
H₁ : Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) 0 : A) ((g : (a : S') → A) 0 : A)
H₂ :
  ∀ (m : R'),
    Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) ((AlgHom.toLinearMap (toAlgHom R R' S') : (a : R') → S') m : S') : A)
      ((g : (a : S') → A) ((AlgHom.toLinearMap (toAlgHom R R' S') : (a : R') → S') m : S') : A)
⊢ Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) x : A) ((g : (a : S') → A) x : A)
have H₃ : ∀ (s : S) (n : S'),
  Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) n : A) ((g : (a : S') → A) n : A) →
    Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) (s • n) : A) ((g : (a : S') → A) (s • n) : A)
Tactic: refine H.1.inductionOn 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'
H : IsPushout R S R' S'
A : Type u_8
inst_11 : Semiring A
inst_12 : Algebra R A
f g : S' →ₐ[R] A
h₁ : Eq (α := R' →ₐ[R] A) (f.comp (toAlgHom R R' S')) (g.comp (toAlgHom R R' S'))
h₂ : Eq (α := S →ₐ[R] A) (f.comp (toAlgHom R S S')) (g.comp (toAlgHom R S S'))
x : S'
H₁ : Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) 0 : A) ((g : (a : S') → A) 0 : A)
H₂ :
  ∀ (m : R'),
    Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) ((AlgHom.toLinearMap (toAlgHom R R' S') : (a : R') → S') m : S') : A)
      ((g : (a : S') → A) ((AlgHom.toLinearMap (toAlgHom R R' S') : (a : R') → S') m : S') : A)
H₃ :
  ∀ (s : S) (n : S'),
    Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) n : A) ((g : (a : S') → A) n : A) →
      Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) (s • n) : A) ((g : (a : S') → A) (s • n) : A)
⊢ Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) x : A) ((g : (a : S') → A) x : A)
have H₄ : ∀ (n₁ n₂ : S'),
  Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) n₁ : A) ((g : (a : S') → A) n₁ : A) →
    Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) n₂ : A) ((g : (a : S') → A) n₂ : A) →
      Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) (n₁ + n₂) : A) ((g : (a : S') → A) (n₁ + n₂) : A)
Tactic: refine H.1.inductionOn 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'
H : IsPushout R S R' S'
A : Type u_8
inst_11 : Semiring A
inst_12 : Algebra R A
f g : S' →ₐ[R] A
h₁ : Eq (α := R' →ₐ[R] A) (f.comp (toAlgHom R R' S')) (g.comp (toAlgHom R R' S'))
h₂ : Eq (α := S →ₐ[R] A) (f.comp (toAlgHom R S S')) (g.comp (toAlgHom R S S'))
x : S'
s : S
s' : S'
e : Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) s' : A) ((g : (a : S') → A) s' : A)
⊢ Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) (s • s') : A) ((g : (a : S') → A) (s • s') : A)
have H₁ : HMul.hMul (α := A) (β := A) ((f : (a : S') → A) ((algebraMap S S' : (a : S) → S') s : S') : A)
    ((g : (a : S') → A) s' : A) =
  HMul.hMul (α := A) (β := A) ((g : (a : S') → A) ((algebraMap S S' : (a : S) → S') s : S') : A)
    ((g : (a : S') → A) s' : A)
Tactic: rw [Algebra.smul_def, map_mul, map_mul, e]
-- 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'
H : IsPushout R S R' S'
A : Type u_8
inst_11 : Semiring A
inst_12 : Algebra R A
f g : S' →ₐ[R] A
h₁ : Eq (α := R' →ₐ[R] A) (f.comp (toAlgHom R R' S')) (g.comp (toAlgHom R R' S'))
h₂ : Eq (α := S →ₐ[R] A) (f.comp (toAlgHom R S S')) (g.comp (toAlgHom R S S'))
x : S'
s : S
s' : S'
e : Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) s' : A) ((g : (a : S') → A) s' : A)
⊢ HMul.hMul (α := A) (β := A) ((f : (a : S') → A) ((algebraMap S S' : (a : S) → S') s : S') : A)
      ((g : (a : S') → A) s' : A) =
    HMul.hMul (α := A) (β := A) ((g : (a : S') → A) ((algebraMap S S' : (a : S) → S') s : S') : A)
      ((g : (a : S') → A) s' : A)
have H₁ : Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) ((algebraMap S S' : (a : S) → S') s : S') : A)
  ((g : (a : S') → A) ((algebraMap S S' : (a : S) → S') s : S') : A)
Tactic: congr 1
-- 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'
H : IsPushout R S R' S'
A : Type u_8
inst_11 : Semiring A
inst_12 : Algebra R A
f g : S' →ₐ[R] A
h₁ : Eq (α := R' →ₐ[R] A) (f.comp (toAlgHom R R' S')) (g.comp (toAlgHom R R' S'))
h₂ : Eq (α := S →ₐ[R] A) (f.comp (toAlgHom R S S')) (g.comp (toAlgHom R S S'))
x s₁ s₂ : S'
e₁ : Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) s₁ : A) ((g : (a : S') → A) s₁ : A)
e₂ : Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) s₂ : A) ((g : (a : S') → A) s₂ : A)
⊢ Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) (s₁ + s₂) : A) ((g : (a : S') → A) (s₁ + s₂) : A)
have H₁ : HAdd.hAdd (α := A) (β := A) ((f : (a : S') → A) s₁ : A) ((f : (a : S') → A) s₂ : A) = (g : (a : S') → A) (s₁ + s₂)
Tactic: rw [map_add, map_add, e₁, e₂]
-- 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'
H : IsPushout R S R' S'
A : Type u_8
inst_11 : Semiring A
inst_12 : Algebra R A
f g : S' →ₐ[R] A
h₁ : Eq (α := R' →ₐ[R] A) (f.comp (toAlgHom R R' S')) (g.comp (toAlgHom R R' S'))
h₂ : Eq (α := S →ₐ[R] A) (f.comp (toAlgHom R S S')) (g.comp (toAlgHom R S S'))
x s₁ s₂ : S'
e₁ : Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) s₁ : A) ((g : (a : S') → A) s₁ : A)
e₂ : Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) s₂ : A) ((g : (a : S') → A) s₂ : A)
H₁ : HAdd.hAdd (α := A) (β := A) ((f : (a : S') → A) s₁ : A) ((f : (a : S') → A) s₂ : A) = (g : (a : S') → A) (s₁ + s₂)
⊢ Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) (s₁ + s₂) : A) ((g : (a : S') → A) (s₁ + s₂) : A)
have H₂ : HAdd.hAdd (α := A) (β := A) ((f : (a : S') → A) s₁ : A) ((f : (a : S') → A) s₂ : A) =
  HAdd.hAdd (α := A) (β := A) ((g : (a : S') → A) s₁ : A) ((g : (a : S') → A) s₂ : A)
Tactic: rw [map_add, map_add, e₁, e₂]
-- 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'
H : IsPushout R S R' S'
A : Type u_8
inst_11 : Semiring A
inst_12 : Algebra R A
f g : S' →ₐ[R] A
h₁ : Eq (α := R' →ₐ[R] A) (f.comp (toAlgHom R R' S')) (g.comp (toAlgHom R R' S'))
h₂ : Eq (α := S →ₐ[R] A) (f.comp (toAlgHom R S S')) (g.comp (toAlgHom R S S'))
x s₁ s₂ : S'
e₁ : Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) s₁ : A) ((g : (a : S') → A) s₁ : A)
e₂ : Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) s₂ : A) ((g : (a : S') → A) s₂ : A)
H₁ : HAdd.hAdd (α := A) (β := A) ((f : (a : S') → A) s₁ : A) ((f : (a : S') → A) s₂ : A) = (g : (a : S') → A) (s₁ + s₂)
H₂ :
  HAdd.hAdd (α := A) (β := A) ((f : (a : S') → A) s₁ : A) ((f : (a : S') → A) s₂ : A) =
    HAdd.hAdd (α := A) (β := A) ((g : (a : S') → A) s₁ : A) ((g : (a : S') → A) s₂ : A)
⊢ Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) (s₁ + s₂) : A) ((g : (a : S') → A) (s₁ + s₂) : A)
have H₃ : HAdd.hAdd (α := A) (β := A) ((g : (a : S') → A) s₁ : A) ((f : (a : S') → A) s₂ : A) =
  HAdd.hAdd (α := A) (β := A) ((g : (a : S') → A) s₁ : A) ((g : (a : S') → A) s₂ : A)
Tactic: rw [map_add, map_add, e₁, e₂]
-- 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'
H : IsPushout R S R' S'
A : Type u_8
inst_11 : Semiring A
inst_12 : Algebra R A
f g : S' →ₐ[R] A
h₁ : Eq (α := R' →ₐ[R] A) (f.comp (toAlgHom R R' S')) (g.comp (toAlgHom R R' S'))
h₂ : Eq (α := S →ₐ[R] A) (f.comp (toAlgHom R S S')) (g.comp (toAlgHom R S S'))
x s₁ s₂ : S'
e₁ : Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) s₁ : A) ((g : (a : S') → A) s₁ : A)
e₂ : Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) s₂ : A) ((g : (a : S') → A) s₂ : A)
H₁ : HAdd.hAdd (α := A) (β := A) ((f : (a : S') → A) s₁ : A) ((f : (a : S') → A) s₂ : A) = (g : (a : S') → A) (s₁ + s₂)
H₂ :
  HAdd.hAdd (α := A) (β := A) ((f : (a : S') → A) s₁ : A) ((f : (a : S') → A) s₂ : A) =
    HAdd.hAdd (α := A) (β := A) ((g : (a : S') → A) s₁ : A) ((g : (a : S') → A) s₂ : A)
H₃ :
  HAdd.hAdd (α := A) (β := A) ((g : (a : S') → A) s₁ : A) ((f : (a : S') → A) s₂ : A) =
    HAdd.hAdd (α := A) (β := A) ((g : (a : S') → A) s₁ : A) ((g : (a : S') → A) s₂ : A)
⊢ Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) (s₁ + s₂) : A) ((g : (a : S') → A) (s₁ + s₂) : A)
have H₄ : HAdd.hAdd (α := A) (β := A) ((g : (a : S') → A) s₁ : A) ((g : (a : S') → A) s₂ : A) =
  HAdd.hAdd (α := A) (β := A) ((g : (a : S') → A) s₁ : A) ((g : (a : S') → A) s₂ : A)
Tactic: rw [map_add, map_add, e₁, e₂]
-- 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
T : Type u_4
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
R' : Type u_6
S' : Type u_7
inst_7 : CommSemiring R'
inst_8 : CommSemiring S'
inst_9 : Algebra R R'
inst_10 : Algebra S S'
inst_11 : Algebra R' S'
inst_12 : Algebra R S'
inst_13 : IsScalarTower R R' S'
inst_14 : IsScalarTower R S S'
T' : Type u_8
inst_15 : CommSemiring T'
inst_16 : Algebra R T'
inst_17 : Algebra S' T'
inst_18 : Algebra S T'
inst_19 : Algebra T T'
inst_20 : Algebra R' T'
inst_21 : IsScalarTower R T T'
inst_22 : IsScalarTower S T T'
inst_23 : IsScalarTower S S' T'
inst_24 : IsScalarTower R R' T'
inst_25 : IsScalarTower R S' T'
inst_26 : IsScalarTower R' S' T'
inst_27 : IsPushout R S R' S'
f : R' →ₗ[R] S' := AlgHom.toLinearMap (toAlgHom R R' S')
x : R
⊢ Eq.{u_8 + 1} (α := T') ((algebraMap R T' : (a : R) → T') x : T')
    ((algebraMap S T' : (a : S) → T') ((algebraMap R S : (a : R) → S) x : S) : T')
have rw : Eq.{u_8 + 1} (α := T') ((algebraMap S' T' : (a : S') → T') ((algebraMap R S' : (a : R) → S') x : S') : T')
  ((algebraMap S T' : (a : S) → T') ((algebraMap R S : (a : R) → S) x : S) : T')
Tactic: rw [algebraMap_apply R S' T', algebraMap_apply R S S', ← algebraMap_apply S S' T']