-- Mathlib/RingTheory/IsTensorProduct.lean
/--
Let the following be a commutative diagram of rings
```
  R  →  S  →  T
  ↓     ↓     ↓
  R' →  S' →  T'
```
where the left-hand square is a pushout. Then the following are equivalent:
- the big rectangle is a pushout.
- the right-hand square is a pushout.

Note that this is essentially the isomorphism `T ⊗[S] (S ⊗[R] R') ≃ₐ[T] T ⊗[R] R'`.
-/
lemma Algebra.IsPushout.comp_iff {T' : Type*} [CommRing T'] [Algebra R T']
    [Algebra S' T'] [Algebra S T'] [Algebra T T'] [Algebra R' T']
    [IsScalarTower R T T'] [IsScalarTower S T T'] [IsScalarTower S S' T']
    [IsScalarTower R R' T'] [IsScalarTower R S' T'] [IsScalarTower R' S' T']
    [Algebra.IsPushout R S R' S'] :
    Algebra.IsPushout R T R' T' ↔ Algebra.IsPushout S T S' T'

Proof state:
R : Type u_1
S : Type v₃
inst✝²⁷ : CommSemiring R
inst✝²⁶ : CommSemiring S
inst✝²⁵ : Algebra R S
T : Type u_4
inst✝²⁴ : CommSemiring T
inst✝²³ : Algebra R T
inst✝²² : Algebra S T
inst✝²¹ : IsScalarTower R S T
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'
T' : Type u_8
inst✝¹² : CommRing T'
inst✝¹¹ : Algebra R T'
inst✝¹⁰ : Algebra S' T'
inst✝⁹ : Algebra S T'
inst✝⁸ : Algebra T T'
inst✝⁷ : Algebra R' T'
inst✝⁶ : IsScalarTower R T T'
inst✝⁵ : IsScalarTower S T T'
inst✝⁴ : IsScalarTower S S' T'
inst✝³ : IsScalarTower R R' T'
inst✝² : IsScalarTower R S' T'
inst✝¹ : IsScalarTower R' S' T'
inst✝ : IsPushout R S R' S'
⊢ IsPushout R T R' T' ↔ IsPushout S T S' T'

Tactic:
let f : R' →ₗ[R] S' := (IsScalarTower.toAlgHom R R' S').toLinearMap

Result:
R : Type u_1
S : Type v₃
inst✝²⁷ : CommSemiring R
inst✝²⁶ : CommSemiring S
inst✝²⁵ : Algebra R S
T : Type u_4
inst✝²⁴ : CommSemiring T
inst✝²³ : Algebra R T
inst✝²² : Algebra S T
inst✝²¹ : IsScalarTower R S T
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'
T' : Type u_8
inst✝¹² : CommRing T'
inst✝¹¹ : Algebra R T'
inst✝¹⁰ : Algebra S' T'
inst✝⁹ : Algebra S T'
inst✝⁸ : Algebra T T'
inst✝⁷ : Algebra R' T'
inst✝⁶ : IsScalarTower R T T'
inst✝⁵ : IsScalarTower S T T'
inst✝⁴ : IsScalarTower S S' T'
inst✝³ : IsScalarTower R R' T'
inst✝² : IsScalarTower R S' T'
inst✝¹ : IsScalarTower R' S' T'
inst✝ : IsPushout R S R' S'
f : R' →ₗ[R] S' := (toAlgHom R R' S').toLinearMap
⊢ IsPushout R T R' T' ↔ IsPushout S T S' T'

Proof state:
R : Type u_1
S : Type v₃
inst✝²⁷ : CommSemiring R
inst✝²⁶ : CommSemiring S
inst✝²⁵ : Algebra R S
T : Type u_4
inst✝²⁴ : CommSemiring T
inst✝²³ : Algebra R T
inst✝²² : Algebra S T
inst✝²¹ : IsScalarTower R S T
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'
T' : Type u_8
inst✝¹² : CommRing T'
inst✝¹¹ : Algebra R T'
inst✝¹⁰ : Algebra S' T'
inst✝⁹ : Algebra S T'
inst✝⁸ : Algebra T T'
inst✝⁷ : Algebra R' T'
inst✝⁶ : IsScalarTower R T T'
inst✝⁵ : IsScalarTower S T T'
inst✝⁴ : IsScalarTower S S' T'
inst✝³ : IsScalarTower R R' T'
inst✝² : IsScalarTower R S' T'
inst✝¹ : IsScalarTower R' S' T'
inst✝ : IsPushout R S R' S'
f : R' →ₗ[R] S' := (toAlgHom R R' S').toLinearMap
x : R
⊢ (algebraMap R T') x = (algebraMap S T') ((algebraMap R S) x)

Tactic:
rw [algebraMap_apply R S' T', algebraMap_apply R S S', ← algebraMap_apply S S' T']

Result:
no goals

Proof state:
case h
R : Type u_1
S : Type v₃
inst✝²⁷ : CommSemiring R
inst✝²⁶ : CommSemiring S
inst✝²⁵ : Algebra R S
T : Type u_4
inst✝²⁴ : CommSemiring T
inst✝²³ : Algebra R T
inst✝²² : Algebra S T
inst✝²¹ : IsScalarTower R S T
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'
T' : Type u_8
inst✝¹² : CommRing T'
inst✝¹¹ : Algebra R T'
inst✝¹⁰ : Algebra S' T'
inst✝⁹ : Algebra S T'
inst✝⁸ : Algebra T T'
inst✝⁷ : Algebra R' T'
inst✝⁶ : IsScalarTower R T T'
inst✝⁵ : IsScalarTower S T T'
inst✝⁴ : IsScalarTower S S' T'
inst✝³ : IsScalarTower R R' T'
inst✝² : IsScalarTower R S' T'
inst✝¹ : IsScalarTower R' S' T'
inst✝ : IsPushout R S R' S'
f : R' →ₗ[R] S' := (toAlgHom R R' S').toLinearMap
this : IsScalarTower R S T'
x : R'
⊢ (↑R (toAlgHom S S' T').toLinearMap ∘ₗ f) x = (toAlgHom R R' T').toLinearMap x

Tactic:
simp [f, ← IsScalarTower.algebraMap_apply]

Result:
no goals

Proof state:
R : Type u_1
S : Type v₃
inst✝²⁷ : CommSemiring R
inst✝²⁶ : CommSemiring S
inst✝²⁵ : Algebra R S
T : Type u_4
inst✝²⁴ : CommSemiring T
inst✝²³ : Algebra R T
inst✝²² : Algebra S T
inst✝²¹ : IsScalarTower R S T
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'
T' : Type u_8
inst✝¹² : CommRing T'
inst✝¹¹ : Algebra R T'
inst✝¹⁰ : Algebra S' T'
inst✝⁹ : Algebra S T'
inst✝⁸ : Algebra T T'
inst✝⁷ : Algebra R' T'
inst✝⁶ : IsScalarTower R T T'
inst✝⁵ : IsScalarTower S T T'
inst✝⁴ : IsScalarTower S S' T'
inst✝³ : IsScalarTower R R' T'
inst✝² : IsScalarTower R S' T'
inst✝¹ : IsScalarTower R' S' T'
inst✝ : IsPushout R S R' S'
f : R' →ₗ[R] S' := (toAlgHom R R' S').toLinearMap
this : IsScalarTower R S T'
⊢ IsPushout R T R' T' ↔ IsPushout S T S' T'

Tactic:
have heq : (toAlgHom S S' T').toLinearMap.restrictScalars R ∘ₗ f =
    (toAlgHom R R' T').toLinearMap := by
  ext x
  simp [f, ← IsScalarTower.algebraMap_apply]

Result:
R : Type u_1
S : Type v₃
inst✝²⁷ : CommSemiring R
inst✝²⁶ : CommSemiring S
inst✝²⁵ : Algebra R S
T : Type u_4
inst✝²⁴ : CommSemiring T
inst✝²³ : Algebra R T
inst✝²² : Algebra S T
inst✝²¹ : IsScalarTower R S T
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'
T' : Type u_8
inst✝¹² : CommRing T'
inst✝¹¹ : Algebra R T'
inst✝¹⁰ : Algebra S' T'
inst✝⁹ : Algebra S T'
inst✝⁸ : Algebra T T'
inst✝⁷ : Algebra R' T'
inst✝⁶ : IsScalarTower R T T'
inst✝⁵ : IsScalarTower S T T'
inst✝⁴ : IsScalarTower S S' T'
inst✝³ : IsScalarTower R R' T'
inst✝² : IsScalarTower R S' T'
inst✝¹ : IsScalarTower R' S' T'
inst✝ : IsPushout R S R' S'
f : R' →ₗ[R] S' := (toAlgHom R R' S').toLinearMap
this : IsScalarTower R S T'
heq : ↑R (toAlgHom S S' T').toLinearMap ∘ₗ f = (toAlgHom R R' T').toLinearMap
⊢ IsPushout R T R' T' ↔ IsPushout S T S' T'