Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M✝ : Type v₁
N : Type v₂
S : Type v₃
inst✝⁵⁰ : AddCommMonoid M✝
inst✝⁴⁹ : AddCommMonoid N
inst✝⁴⁸ : CommSemiring R
inst✝⁴⁷ : CommSemiring S
inst✝⁴⁶ : Algebra R S
inst✝⁴⁵ : Module R M✝
inst✝⁴⁴ : Module R N
inst✝⁴³ : Module S N
inst✝⁴² : IsScalarTower R S N
f : M✝ →ₗ[R] N
h : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst✝⁴¹ : AddCommMonoid P
inst✝⁴⁰ : Module R P
inst✝³⁹ : AddCommMonoid Q
inst✝³⁸ : Module S Q
inst✝³⁷ : Module R Q
inst✝³⁶ : IsScalarTower R S Q
f' : P →ₗ[R] Q
T : Type u_4
O : Type u_5
inst✝³⁵ : CommSemiring T
inst✝³⁴ : Algebra R T
inst✝³³ : Algebra S T
inst✝³² : IsScalarTower R S T
inst✝³¹ : AddCommMonoid O
inst✝³⁰ : Module R O
inst✝²⁹ : Module S O
inst✝²⁸ : Module T O
inst✝²⁷ : IsScalarTower S T O
inst✝²⁶ : IsScalarTower R S O
inst✝²⁵ : IsScalarTower R T O
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'
A : Type u_8
B : Type u_9
inst✝¹⁶ : CommRing A
inst✝¹⁵ : CommRing B
inst✝¹⁴ : Algebra R A
inst✝¹³ : Algebra R B
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra S B
inst✝¹⁰ : IsScalarTower R A B
inst✝⁹ : IsScalarTower R S B
inst✝⁸ : IsPushout R S A B
M : Type u_10
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
C : Type u_11
inst✝³ : CommRing C
inst✝² : Algebra R C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower R A C
⊢ B ⊗[A] C ≃ₐ[S] S ⊗[R] C

Tactic:
refine AlgEquiv.symm
    (AlgEquiv.ofLinearEquiv (IsPushout.cancelBaseChange R S A B C).symm ?_ ?_)

Goal state after:
case refine_1
R : Type u_1
M✝ : Type v₁
N : Type v₂
S : Type v₃
inst✝⁵⁰ : AddCommMonoid M✝
inst✝⁴⁹ : AddCommMonoid N
inst✝⁴⁸ : CommSemiring R
inst✝⁴⁷ : CommSemiring S
inst✝⁴⁶ : Algebra R S
inst✝⁴⁵ : Module R M✝
inst✝⁴⁴ : Module R N
inst✝⁴³ : Module S N
inst✝⁴² : IsScalarTower R S N
f : M✝ →ₗ[R] N
h : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst✝⁴¹ : AddCommMonoid P
inst✝⁴⁰ : Module R P
inst✝³⁹ : AddCommMonoid Q
inst✝³⁸ : Module S Q
inst✝³⁷ : Module R Q
inst✝³⁶ : IsScalarTower R S Q
f' : P →ₗ[R] Q
T : Type u_4
O : Type u_5
inst✝³⁵ : CommSemiring T
inst✝³⁴ : Algebra R T
inst✝³³ : Algebra S T
inst✝³² : IsScalarTower R S T
inst✝³¹ : AddCommMonoid O
inst✝³⁰ : Module R O
inst✝²⁹ : Module S O
inst✝²⁸ : Module T O
inst✝²⁷ : IsScalarTower S T O
inst✝²⁶ : IsScalarTower R S O
inst✝²⁵ : IsScalarTower R T O
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'
A : Type u_8
B : Type u_9
inst✝¹⁶ : CommRing A
inst✝¹⁵ : CommRing B
inst✝¹⁴ : Algebra R A
inst✝¹³ : Algebra R B
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra S B
inst✝¹⁰ : IsScalarTower R A B
inst✝⁹ : IsScalarTower R S B
inst✝⁸ : IsPushout R S A B
M : Type u_10
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
C : Type u_11
inst✝³ : CommRing C
inst✝² : Algebra R C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower R A C
⊢ (cancelBaseChange R S A B C).symm 1 = 1

case refine_2
R : Type u_1
M✝ : Type v₁
N : Type v₂
S : Type v₃
inst✝⁵⁰ : AddCommMonoid M✝
inst✝⁴⁹ : AddCommMonoid N
inst✝⁴⁸ : CommSemiring R
inst✝⁴⁷ : CommSemiring S
inst✝⁴⁶ : Algebra R S
inst✝⁴⁵ : Module R M✝
inst✝⁴⁴ : Module R N
inst✝⁴³ : Module S N
inst✝⁴² : IsScalarTower R S N
f : M✝ →ₗ[R] N
h : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst✝⁴¹ : AddCommMonoid P
inst✝⁴⁰ : Module R P
inst✝³⁹ : AddCommMonoid Q
inst✝³⁸ : Module S Q
inst✝³⁷ : Module R Q
inst✝³⁶ : IsScalarTower R S Q
f' : P →ₗ[R] Q
T : Type u_4
O : Type u_5
inst✝³⁵ : CommSemiring T
inst✝³⁴ : Algebra R T
inst✝³³ : Algebra S T
inst✝³² : IsScalarTower R S T
inst✝³¹ : AddCommMonoid O
inst✝³⁰ : Module R O
inst✝²⁹ : Module S O
inst✝²⁸ : Module T O
inst✝²⁷ : IsScalarTower S T O
inst✝²⁶ : IsScalarTower R S O
inst✝²⁵ : IsScalarTower R T O
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'
A : Type u_8
B : Type u_9
inst✝¹⁶ : CommRing A
inst✝¹⁵ : CommRing B
inst✝¹⁴ : Algebra R A
inst✝¹³ : Algebra R B
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra S B
inst✝¹⁰ : IsScalarTower R A B
inst✝⁹ : IsScalarTower R S B
inst✝⁸ : IsPushout R S A B
M : Type u_10
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
C : Type u_11
inst✝³ : CommRing C
inst✝² : Algebra R C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower R A C
⊢ ∀ (x y : S ⊗[R] C),
    (cancelBaseChange R S A B C).symm (x * y) =
      (cancelBaseChange R S A B C).symm x * (cancelBaseChange R S A B C).symm y