-- Mathlib/RingTheory/IsTensorProduct.lean
theorem Algebra.IsPushout.symm (h : Algebra.IsPushout R S R' S') : Algebra.IsPushout R R' S S'

Proof state:
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'
⊢ IsPushout R R' S S'

Tactic:
let _ := (Algebra.TensorProduct.includeRight : R' →ₐ[R] S ⊗ R').toRingHom.toAlgebra

Result:
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'
x✝ : Algebra R' (S ⊗[R] R') := TensorProduct.includeRight.toAlgebra
⊢ IsPushout R R' S S'

Proof state:
case out
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'
x✝ : Algebra R' (S ⊗[R] R') := TensorProduct.includeRight.toAlgebra
e : R' ⊗[R] S ≃ₗ[R'] S' :=
  let __src := _root_.TensorProduct.comm R R' S ≪≫ₗ LinearEquiv.restrictScalars R ⋯.equiv;
  { toAddHom := (↑__src).toAddHom, map_smul' := ⋯, invFun := __src.invFun, left_inv := ⋯, right_inv := ⋯ }
this : (toAlgHom R S S').toLinearMap = ↑R ↑e ∘ₗ (TensorProduct.mk R R' S) 1
⊢ IsBaseChange R' (↑R ↑e ∘ₗ (TensorProduct.mk R R' S) 1)

Tactic:
exact (TensorProduct.isBaseChange R S R').comp (IsBaseChange.ofEquiv e)

Result:
no goals

Proof state:
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'
x✝¹ : Algebra R' (S ⊗[R] R') := TensorProduct.includeRight.toAlgebra
r : R'
x✝ x y : R' ⊗[R] S
hx : ⋯.equiv ((TensorProduct.comm R R' S) (r • x)) = r • ⋯.equiv ((TensorProduct.comm R R' S) x)
hy : ⋯.equiv ((TensorProduct.comm R R' S) (r • y)) = r • ⋯.equiv ((TensorProduct.comm R R' S) y)
⊢ ⋯.equiv ((TensorProduct.comm R R' S) (r • (x + y))) = r • ⋯.equiv ((TensorProduct.comm R R' S) (x + y))

Tactic:
rw [map_add, map_add, smul_add, map_add, map_add, hx, hy, smul_add]

Result:
no goals

Proof state:
case out
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'
x✝ : Algebra R' (S ⊗[R] R') := TensorProduct.includeRight.toAlgebra
e : R' ⊗[R] S ≃ₗ[R'] S' :=
  let __src := _root_.TensorProduct.comm R R' S ≪≫ₗ LinearEquiv.restrictScalars R ⋯.equiv;
  { toAddHom := (↑__src).toAddHom, map_smul' := ⋯, invFun := __src.invFun, left_inv := ⋯, right_inv := ⋯ }
this : (toAlgHom R S S').toLinearMap = ↑R ↑e ∘ₗ (TensorProduct.mk R R' S) 1
⊢ IsBaseChange R' (toAlgHom R S S').toLinearMap

Tactic:
rw [this]

Result:
case out
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'
x✝ : Algebra R' (S ⊗[R] R') := TensorProduct.includeRight.toAlgebra
e : R' ⊗[R] S ≃ₗ[R'] S' :=
  let __src := _root_.TensorProduct.comm R R' S ≪≫ₗ LinearEquiv.restrictScalars R ⋯.equiv;
  { toAddHom := (↑__src).toAddHom, map_smul' := ⋯, invFun := __src.invFun, left_inv := ⋯, right_inv := ⋯ }
this : (toAlgHom R S S').toLinearMap = ↑R ↑e ∘ₗ (TensorProduct.mk R R' S) 1
⊢ IsBaseChange R' (↑R ↑e ∘ₗ (TensorProduct.mk R R' S) 1)

Proof state:
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'
x✝ : Algebra R' (S ⊗[R] R') := TensorProduct.includeRight.toAlgebra
r : R'
x : R' ⊗[R] S
⊢ (↑__src✝).toFun (r • x) = (RingHom.id R') r • (↑__src✝).toFun x

Tactic:
change
  h.1.equiv (TensorProduct.comm R R' S (r • x)) = r • h.1.equiv (TensorProduct.comm R R' S x)

Result:
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'
x✝ : Algebra R' (S ⊗[R] R') := TensorProduct.includeRight.toAlgebra
r : R'
x : R' ⊗[R] S
⊢ ⋯.equiv ((TensorProduct.comm R R' S) (r • x)) = r • ⋯.equiv ((TensorProduct.comm R R' S) x)

Proof state:
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'
x✝ : Algebra R' (S ⊗[R] R') := TensorProduct.includeRight.toAlgebra
r : R'
x : R' ⊗[R] S
⊢ ∀ (x y : R' ⊗[R] S),
    ⋯.equiv ((TensorProduct.comm R R' S) (r • x)) = r • ⋯.equiv ((TensorProduct.comm R R' S) x) →
      ⋯.equiv ((TensorProduct.comm R R' S) (r • y)) = r • ⋯.equiv ((TensorProduct.comm R R' S) y) →
        ⋯.equiv ((TensorProduct.comm R R' S) (r • (x + y))) = r • ⋯.equiv ((TensorProduct.comm R R' S) (x + y))

Tactic:
intro x y hx hy

Result:
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'
x✝¹ : Algebra R' (S ⊗[R] R') := TensorProduct.includeRight.toAlgebra
r : R'
x✝ x y : R' ⊗[R] S
hx : ⋯.equiv ((TensorProduct.comm R R' S) (r • x)) = r • ⋯.equiv ((TensorProduct.comm R R' S) x)
hy : ⋯.equiv ((TensorProduct.comm R R' S) (r • y)) = r • ⋯.equiv ((TensorProduct.comm R R' S) y)
⊢ ⋯.equiv ((TensorProduct.comm R R' S) (r • (x + y))) = r • ⋯.equiv ((TensorProduct.comm R R' S) (x + y))