Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: case ha
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra S A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R B
inst✝⁵ : CommRing C
inst✝⁴ : Algebra R C
inst✝³ : Algebra S C
inst✝² : IsScalarTower R S C
inst✝¹ : CommRing D
inst✝ : Algebra R D
f : A →ₐ[S] C
g : B →ₐ[R] D
hf : f.Flat
hg : g.Flat
heq :
  Algebra.TensorProduct.map f g =
    (Algebra.TensorProduct.map f (AlgHom.id R D)).comp (Algebra.TensorProduct.map (AlgHom.id S A) g)
x✝ : A
⊢ ((AlgHom.restrictScalars R (Algebra.TensorProduct.map f (AlgHom.id R D))).comp Algebra.TensorProduct.includeLeft) x✝ =
    (((↑(Algebra.TensorProduct.comm R D C)).comp
            ((Algebra.TensorProduct.lTensor D (AlgHom.restrictScalars R f)).comp
              ↑(Algebra.TensorProduct.comm R A D))).comp
        Algebra.TensorProduct.includeLeft)
      x✝

pp: case hb
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra S A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R B
inst✝⁵ : CommRing C
inst✝⁴ : Algebra R C
inst✝³ : Algebra S C
inst✝² : IsScalarTower R S C
inst✝¹ : CommRing D
inst✝ : Algebra R D
f : A →ₐ[S] C
g : B →ₐ[R] D
hf : f.Flat
hg : g.Flat
heq :
  Algebra.TensorProduct.map f g =
    (Algebra.TensorProduct.map f (AlgHom.id R D)).comp (Algebra.TensorProduct.map (AlgHom.id S A) g)
x✝ : D
⊢ ((AlgHom.restrictScalars R (AlgHom.restrictScalars R (Algebra.TensorProduct.map f (AlgHom.id R D)))).comp
        Algebra.TensorProduct.includeRight)
      x✝ =
    ((AlgHom.restrictScalars R
            ((↑(Algebra.TensorProduct.comm R D C)).comp
              ((Algebra.TensorProduct.lTensor D (AlgHom.restrictScalars R f)).comp
                ↑(Algebra.TensorProduct.comm R A D)))).comp
        Algebra.TensorProduct.includeRight)
      x✝

Tactic:
<;>

Goal state after:
case ha
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra S A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R B
inst✝⁵ : CommRing C
inst✝⁴ : Algebra R C
inst✝³ : Algebra S C
inst✝² : IsScalarTower R S C
inst✝¹ : CommRing D
inst✝ : Algebra R D
f : A →ₐ[S] C
g : B →ₐ[R] D
hf : f.Flat
hg : g.Flat
heq :
  Algebra.TensorProduct.map f g =
    (Algebra.TensorProduct.map f (AlgHom.id R D)).comp (Algebra.TensorProduct.map (AlgHom.id S A) g)
x✝ : A
⊢ ((AlgHom.restrictScalars R (Algebra.TensorProduct.map f (AlgHom.id R D))).comp Algebra.TensorProduct.includeLeft) x✝ =
    (((↑(Algebra.TensorProduct.comm R D C)).comp
            ((Algebra.TensorProduct.lTensor D (AlgHom.restrictScalars R f)).comp
              ↑(Algebra.TensorProduct.comm R A D))).comp
        Algebra.TensorProduct.includeLeft)
      x✝

case hb
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra S A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R B
inst✝⁵ : CommRing C
inst✝⁴ : Algebra R C
inst✝³ : Algebra S C
inst✝² : IsScalarTower R S C
inst✝¹ : CommRing D
inst✝ : Algebra R D
f : A →ₐ[S] C
g : B →ₐ[R] D
hf : f.Flat
hg : g.Flat
heq :
  Algebra.TensorProduct.map f g =
    (Algebra.TensorProduct.map f (AlgHom.id R D)).comp (Algebra.TensorProduct.map (AlgHom.id S A) g)
x✝ : D
⊢ ((AlgHom.restrictScalars R (AlgHom.restrictScalars R (Algebra.TensorProduct.map f (AlgHom.id R D)))).comp
        Algebra.TensorProduct.includeRight)
      x✝ =
    ((AlgHom.restrictScalars R
            ((↑(Algebra.TensorProduct.comm R D C)).comp
              ((Algebra.TensorProduct.lTensor D (AlgHom.restrictScalars R f)).comp
                ↑(Algebra.TensorProduct.comm R A D)))).comp
        Algebra.TensorProduct.includeRight)
      x✝