-- Module: Mathlib.RingTheory.Etale.Weakly
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : WeaklyEtale (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₂} S)
inst_8 : WeaklyEtale (ULift.{max u₁ u₂ u₃, u₂} S) (ULift.{max u₁ u₂ u₃, u₃} T)
ha :
  ∀ (x : ULift.{max u₁ u₂ u₃, u₃} T),
    Eq.{u₃ + 1} (α := T)
      (ULift.down
        ((AlgHom.comp (TensorProduct.lmul' (ULift.{max (max u₁ u₂) u₃, u₁} R)) TensorProduct.includeLeft :
            (a : ULift.{max u₁ u₂ u₃, u₃} T) → ULift.{max u₁ u₂ u₃, u₃} T)
          x))
      (ULift.down
        ((AlgHom.comp (B := ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max (max u₁ u₂) u₃, u₁} R] ULift.{max u₁ u₂ u₃, u₃} T)
              (AlgHom.comp (B := ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₂} S] ULift.{max u₁ u₂ u₃, u₃} T)
                (AlgHom.restrictScalars (ULift.{max u₁ u₂ u₃, u₁} R)
                    (TensorProduct.lmul' (ULift.{max u₁ u₂ u₃, u₂} S)) :
                  ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₂} S]
                      ULift.{max u₁ u₂ u₃, u₃} T →ₐ[ULift.{max u₁ u₂ u₃, u₁} R]
                    ULift.{max u₁ u₂ u₃, u₃} T)
                (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) :
                  ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max (max u₁ u₂) u₃, u₁} R]
                      ULift.{max u₁ u₂ u₃, u₃} T →ₐ[ULift.{max u₁ u₂ u₃, u₁} R]
                    ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₂} S] ULift.{max u₁ u₂ u₃, u₃} T))
              TensorProduct.includeLeft :
            (a : ULift.{max u₁ u₂ u₃, u₃} T) → ULift.{max u₁ u₂ u₃, u₃} T)
          x))
hb :
  ∀ (x : ULift.{max u₁ u₂ u₃, u₃} T),
    Eq.{u₃ + 1} (α := T)
      (ULift.down
        ((AlgHom.comp
              (AlgHom.restrictScalars (ULift.{max (max u₁ u₂) u₃, u₁} R) (S := ULift.{max (max u₁ u₂) u₃, u₁} R)
                (TensorProduct.lmul' (ULift.{max (max u₁ u₂) u₃, u₁} R)))
              TensorProduct.includeRight :
            (a : ULift.{max u₁ u₂ u₃, u₃} T) → ULift.{max u₁ u₂ u₃, u₃} T)
          x))
      (ULift.down
        ((AlgHom.comp (B := ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max (max u₁ u₂) u₃, u₁} R] ULift.{max u₁ u₂ u₃, u₃} T)
              (AlgHom.restrictScalars (ULift.{max (max u₁ u₂) u₃, u₁} R) (S := ULift.{max (max u₁ u₂) u₃, u₁} R)
                (AlgHom.comp (B := ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₂} S] ULift.{max u₁ u₂ u₃, u₃} T)
                  (AlgHom.restrictScalars (ULift.{max u₁ u₂ u₃, u₁} R)
                      (TensorProduct.lmul' (ULift.{max u₁ u₂ u₃, u₂} S)) :
                    ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₂} S]
                        ULift.{max u₁ u₂ u₃, u₃} T →ₐ[ULift.{max u₁ u₂ u₃, u₁} R]
                      ULift.{max u₁ u₂ u₃, u₃} T)
                  (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) :
                    ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max (max u₁ u₂) u₃, u₁} R]
                        ULift.{max u₁ u₂ u₃, u₃} T →ₐ[ULift.{max u₁ u₂ u₃, u₁} R]
                      ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₂} S] ULift.{max u₁ u₂ u₃, u₃} T)))
              TensorProduct.includeRight :
            (a : ULift.{max u₁ u₂ u₃, u₃} T) → ULift.{max u₁ u₂ u₃, u₃} T)
          x))
⊢ Eq (α :=
    ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max (max u₁ u₂) u₃, u₁} R]
        ULift.{max u₁ u₂ u₃, u₃} T →ₐ[ULift.{max (max u₁ u₂) u₃, u₁} R]
      ULift.{max u₁ u₂ u₃, u₃} T)
    (TensorProduct.lmul' (ULift.{max (max u₁ u₂) u₃, u₁} R))
    (AlgHom.comp (B := ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₂} S] ULift.{max u₁ u₂ u₃, u₃} T)
      (AlgHom.restrictScalars (ULift.{max u₁ u₂ u₃, u₁} R) (TensorProduct.lmul' (ULift.{max u₁ u₂ u₃, u₂} S)) :
        ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₂} S]
            ULift.{max u₁ u₂ u₃, u₃} T →ₐ[ULift.{max u₁ u₂ u₃, u₁} R]
          ULift.{max u₁ u₂ u₃, u₃} T)
      (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) :
        ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max (max u₁ u₂) u₃, u₁} R]
            ULift.{max u₁ u₂ u₃, u₃} T →ₐ[ULift.{max u₁ u₂ u₃, u₁} R]
          ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₂} S] ULift.{max u₁ u₂ u₃, u₃} T))

Tactic:
ext