Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case refine_2
R : Type u_1
S : Type v₃
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
R' : Type u_6
S' : Type u_7
inst✝⁹ : CommSemiring R'
inst✝⁸ : CommSemiring S'
inst✝⁷ : Algebra R R'
inst✝⁶ : Algebra S S'
inst✝⁵ : Algebra R' S'
inst✝⁴ : Algebra R S'
inst✝³ : IsScalarTower R R' S'
inst✝² : IsScalarTower R S S'
H : IsPushout R S R' S'
A : Type u_8
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : S' →ₐ[R] A
h₁ : f.comp (toAlgHom R R' S') = g.comp (toAlgHom R R' S')
h₂ : f.comp (toAlgHom R S S') = g.comp (toAlgHom R S S')
x : S'
⊢ ∀ (m : R'), f ((toAlgHom R R' S').toLinearMap m) = g ((toAlgHom R R' S').toLinearMap m)

pp: case refine_3
R : Type u_1
S : Type v₃
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
R' : Type u_6
S' : Type u_7
inst✝⁹ : CommSemiring R'
inst✝⁸ : CommSemiring S'
inst✝⁷ : Algebra R R'
inst✝⁶ : Algebra S S'
inst✝⁵ : Algebra R' S'
inst✝⁴ : Algebra R S'
inst✝³ : IsScalarTower R R' S'
inst✝² : IsScalarTower R S S'
H : IsPushout R S R' S'
A : Type u_8
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : S' →ₐ[R] A
h₁ : f.comp (toAlgHom R R' S') = g.comp (toAlgHom R R' S')
h₂ : f.comp (toAlgHom R S S') = g.comp (toAlgHom R S S')
x : S'
⊢ ∀ (s : S) (n : S'), f n = g n → f (s • n) = g (s • n)

pp: case refine_4
R : Type u_1
S : Type v₃
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
R' : Type u_6
S' : Type u_7
inst✝⁹ : CommSemiring R'
inst✝⁸ : CommSemiring S'
inst✝⁷ : Algebra R R'
inst✝⁶ : Algebra S S'
inst✝⁵ : Algebra R' S'
inst✝⁴ : Algebra R S'
inst✝³ : IsScalarTower R R' S'
inst✝² : IsScalarTower R S S'
H : IsPushout R S R' S'
A : Type u_8
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : S' →ₐ[R] A
h₁ : f.comp (toAlgHom R R' S') = g.comp (toAlgHom R R' S')
h₂ : f.comp (toAlgHom R S S') = g.comp (toAlgHom R S S')
x : S'
⊢ ∀ (n₁ n₂ : S'), f n₁ = g n₁ → f n₂ = g n₂ → f (n₁ + n₂) = g (n₁ + n₂)

Tactic:
· exact AlgHom.congr_fun h₁

Goal state after:
case refine_3
R : Type u_1
S : Type v₃
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
R' : Type u_6
S' : Type u_7
inst✝⁹ : CommSemiring R'
inst✝⁸ : CommSemiring S'
inst✝⁷ : Algebra R R'
inst✝⁶ : Algebra S S'
inst✝⁵ : Algebra R' S'
inst✝⁴ : Algebra R S'
inst✝³ : IsScalarTower R R' S'
inst✝² : IsScalarTower R S S'
H : IsPushout R S R' S'
A : Type u_8
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : S' →ₐ[R] A
h₁ : f.comp (toAlgHom R R' S') = g.comp (toAlgHom R R' S')
h₂ : f.comp (toAlgHom R S S') = g.comp (toAlgHom R S S')
x : S'
⊢ ∀ (s : S) (n : S'), f n = g n → f (s • n) = g (s • n)

case refine_4
R : Type u_1
S : Type v₃
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
R' : Type u_6
S' : Type u_7
inst✝⁹ : CommSemiring R'
inst✝⁸ : CommSemiring S'
inst✝⁷ : Algebra R R'
inst✝⁶ : Algebra S S'
inst✝⁵ : Algebra R' S'
inst✝⁴ : Algebra R S'
inst✝³ : IsScalarTower R R' S'
inst✝² : IsScalarTower R S S'
H : IsPushout R S R' S'
A : Type u_8
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : S' →ₐ[R] A
h₁ : f.comp (toAlgHom R R' S') = g.comp (toAlgHom R R' S')
h₂ : f.comp (toAlgHom R S S') = g.comp (toAlgHom R S S')
x : S'
⊢ ∀ (n₁ n₂ : S'), f n₁ = g n₁ → f n₂ = g n₂ → f (n₁ + n₂) = g (n₁ + n₂)