Module: Mathlib.RingTheory.Smooth.IntegralClosure

Goal state before:
pp: case ha
R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : CommRing B
inst✝¹ : Algebra R B
M : Submonoid R
inst✝ : IsLocalization M S
φ : ↥(integralClosure R B) →ₐ[R] ↥(integralClosure S (S ⊗[R] B)) := ⋯
this✝² : Algebra ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B)) := ⋯
this✝¹ : IsScalarTower R ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B))
this✝ : IsScalarTower (↥(integralClosure R B)) (↥(integralClosure S (S ⊗[R] B))) (S ⊗[R] B)
this : IsLocalization (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M) ↥(integralClosure S (S ⊗[R] B))
⊢ (AlgHom.restrictScalars R (toIntegralClosure R S B)).comp Algebra.TensorProduct.includeLeft =
    (↑(AlgEquiv.restrictScalars R
            (IsLocalization.algEquiv (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M)
              (S ⊗[R] ↥(integralClosure R B)) ↥(integralClosure S (S ⊗[R] B))))).comp
      Algebra.TensorProduct.includeLeft

pp: case hb
R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : CommRing B
inst✝¹ : Algebra R B
M : Submonoid R
inst✝ : IsLocalization M S
φ : ↥(integralClosure R B) →ₐ[R] ↥(integralClosure S (S ⊗[R] B)) := ⋯
this✝² : Algebra ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B)) := ⋯
this✝¹ : IsScalarTower R ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B))
this✝ : IsScalarTower (↥(integralClosure R B)) (↥(integralClosure S (S ⊗[R] B))) (S ⊗[R] B)
this : IsLocalization (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M) ↥(integralClosure S (S ⊗[R] B))
⊢ (AlgHom.restrictScalars R (AlgHom.restrictScalars R (toIntegralClosure R S B))).comp
      Algebra.TensorProduct.includeRight =
    (AlgHom.restrictScalars R
          ↑(AlgEquiv.restrictScalars R
              (IsLocalization.algEquiv (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M)
                (S ⊗[R] ↥(integralClosure R B)) ↥(integralClosure S (S ⊗[R] B))))).comp
      Algebra.TensorProduct.includeRight

Tactic:
· apply IsLocalization.algHom_ext M; ext

Goal state after:
case hb
R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : CommRing B
inst✝¹ : Algebra R B
M : Submonoid R
inst✝ : IsLocalization M S
φ : ↥(integralClosure R B) →ₐ[R] ↥(integralClosure S (S ⊗[R] B)) := ⋯
this✝² : Algebra ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B)) := ⋯
this✝¹ : IsScalarTower R ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B))
this✝ : IsScalarTower (↥(integralClosure R B)) (↥(integralClosure S (S ⊗[R] B))) (S ⊗[R] B)
this : IsLocalization (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M) ↥(integralClosure S (S ⊗[R] B))
⊢ (AlgHom.restrictScalars R (AlgHom.restrictScalars R (toIntegralClosure R S B))).comp
      Algebra.TensorProduct.includeRight =
    (AlgHom.restrictScalars R
          ↑(AlgEquiv.restrictScalars R
              (IsLocalization.algEquiv (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M)
                (S ⊗[R] ↥(integralClosure R B)) ↥(integralClosure S (S ⊗[R] B))))).comp
      Algebra.TensorProduct.includeRight