Module: Mathlib.RingTheory.Etale.Weakly

Goal state before:
pp: case ha
R : Type u₁
S : Type u₂
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u₃
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : WeaklyEtale (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₂} S)
inst✝ : WeaklyEtale (ULift.{max u₁ u₂ u₃, u₂} S) (ULift.{max u₁ u₂ u₃, u₃} T)
x✝ : ULift.{max u₁ u₂ u₃, u₃} T
⊢ (((TensorProduct.lmul' (ULift.{max (max u₁ u₂) u₃, u₁} R)).comp TensorProduct.includeLeft) x✝).down =
    ((((AlgHom.restrictScalars (ULift.{max u₁ u₂ u₃, u₁} R) (TensorProduct.lmul' (ULift.{max u₁ u₂ u₃, u₂} S))).comp
              (TensorProduct.mapOfCompatibleSMul (ULift.{max u₁ u₂ u₃, u₂} S) (ULift.{max (max u₁ u₂) u₃, u₁} R)
                (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₃} T) (ULift.{max u₁ u₂ u₃, u₃} T))).comp
          TensorProduct.includeLeft)
        x✝).down

pp: case hb
R : Type u₁
S : Type u₂
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u₃
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : WeaklyEtale (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₂} S)
inst✝ : WeaklyEtale (ULift.{max u₁ u₂ u₃, u₂} S) (ULift.{max u₁ u₂ u₃, u₃} T)
x✝ : ULift.{max u₁ u₂ u₃, u₃} T
⊢ (((AlgHom.restrictScalars (ULift.{max (max u₁ u₂) u₃, u₁} R)
              (TensorProduct.lmul' (ULift.{max (max u₁ u₂) u₃, u₁} R))).comp
          TensorProduct.includeRight)
        x✝).down =
    (((AlgHom.restrictScalars (ULift.{max (max u₁ u₂) u₃, u₁} R)
              ((AlgHom.restrictScalars (ULift.{max u₁ u₂ u₃, u₁} R)
                    (TensorProduct.lmul' (ULift.{max u₁ u₂ u₃, u₂} S))).comp
                (TensorProduct.mapOfCompatibleSMul (ULift.{max u₁ u₂ u₃, u₂} S) (ULift.{max (max u₁ u₂) u₃, u₁} R)
                  (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₃} T) (ULift.{max u₁ u₂ u₃, u₃} T)))).comp
          TensorProduct.includeRight)
        x✝).down

Tactic:
<;>

Goal state after:
case ha
R : Type u₁
S : Type u₂
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u₃
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : WeaklyEtale (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₂} S)
inst✝ : WeaklyEtale (ULift.{max u₁ u₂ u₃, u₂} S) (ULift.{max u₁ u₂ u₃, u₃} T)
x✝ : ULift.{max u₁ u₂ u₃, u₃} T
⊢ (((TensorProduct.lmul' (ULift.{max (max u₁ u₂) u₃, u₁} R)).comp TensorProduct.includeLeft) x✝).down =
    ((((AlgHom.restrictScalars (ULift.{max u₁ u₂ u₃, u₁} R) (TensorProduct.lmul' (ULift.{max u₁ u₂ u₃, u₂} S))).comp
              (TensorProduct.mapOfCompatibleSMul (ULift.{max u₁ u₂ u₃, u₂} S) (ULift.{max (max u₁ u₂) u₃, u₁} R)
                (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₃} T) (ULift.{max u₁ u₂ u₃, u₃} T))).comp
          TensorProduct.includeLeft)
        x✝).down

case hb
R : Type u₁
S : Type u₂
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u₃
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : WeaklyEtale (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₂} S)
inst✝ : WeaklyEtale (ULift.{max u₁ u₂ u₃, u₂} S) (ULift.{max u₁ u₂ u₃, u₃} T)
x✝ : ULift.{max u₁ u₂ u₃, u₃} T
⊢ (((AlgHom.restrictScalars (ULift.{max (max u₁ u₂) u₃, u₁} R)
              (TensorProduct.lmul' (ULift.{max (max u₁ u₂) u₃, u₁} R))).comp
          TensorProduct.includeRight)
        x✝).down =
    (((AlgHom.restrictScalars (ULift.{max (max u₁ u₂) u₃, u₁} R)
              ((AlgHom.restrictScalars (ULift.{max u₁ u₂ u₃, u₁} R)
                    (TensorProduct.lmul' (ULift.{max u₁ u₂ u₃, u₂} S))).comp
                (TensorProduct.mapOfCompatibleSMul (ULift.{max u₁ u₂ u₃, u₂} S) (ULift.{max (max u₁ u₂) u₃, u₁} R)
                  (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₃} T) (ULift.{max u₁ u₂ u₃, u₃} T)))).comp
          TensorProduct.includeRight)
        x✝).down