Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case refine_3.hAlg
R✝ : Type u_1
S✝ : Type u_2
T✝ : Type u_3
U✝ : Type u_4
K : Type u_5
R : Type u_6
S : Type u_7
T : Type u_8
U : Type u_9
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : CommRing U
inst✝ : Algebra R U
p✝ p : S[X]
q : (T ⊗[R] S)[X]
h : Polynomial.map includeRight.toRingHom p = q
x✝ : S
⊢ (((AlgHom.restrictScalars R
                ((liftAlgHom q
                      (Algebra.TensorProduct.map (AlgHom.id T T) (AlgHom.restrictScalars R (ofId S (AdjoinRoot p))))
                      (1 ⊗ₜ[R] root p) ⋯).comp
                  (Algebra.TensorProduct.lift (algHom T T (AdjoinRoot q)) (mapAlgHom includeRight p q ⋯) ⋯))).comp
            includeRight).comp
        (ofAlgHom R p))
      x✝ =
    (((AlgHom.restrictScalars R (AlgHom.id T (T ⊗[R] AdjoinRoot p))).comp includeRight).comp (ofAlgHom R p)) x✝

pp: case refine_3.hRoot
R✝ : Type u_1
S✝ : Type u_2
T✝ : Type u_3
U✝ : Type u_4
K : Type u_5
R : Type u_6
S : Type u_7
T : Type u_8
U : Type u_9
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : CommRing U
inst✝ : Algebra R U
p✝ p : S[X]
q : (T ⊗[R] S)[X]
h : Polynomial.map includeRight.toRingHom p = q
⊢ ((AlgHom.restrictScalars R
            ((liftAlgHom q
                  (Algebra.TensorProduct.map (AlgHom.id T T) (AlgHom.restrictScalars R (ofId S (AdjoinRoot p))))
                  (1 ⊗ₜ[R] root p) ⋯).comp
              (Algebra.TensorProduct.lift (algHom T T (AdjoinRoot q)) (mapAlgHom includeRight p q ⋯) ⋯))).comp
        includeRight)
      (root p) =
    ((AlgHom.restrictScalars R (AlgHom.id T (T ⊗[R] AdjoinRoot p))).comp includeRight) (root p)

Tactic:
<;>

Goal state after:
case refine_3.hAlg
R✝ : Type u_1
S✝ : Type u_2
T✝ : Type u_3
U✝ : Type u_4
K : Type u_5
R : Type u_6
S : Type u_7
T : Type u_8
U : Type u_9
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : CommRing U
inst✝ : Algebra R U
p✝ p : S[X]
q : (T ⊗[R] S)[X]
h : Polynomial.map includeRight.toRingHom p = q
x✝ : S
⊢ (((AlgHom.restrictScalars R
                ((liftAlgHom q
                      (Algebra.TensorProduct.map (AlgHom.id T T) (AlgHom.restrictScalars R (ofId S (AdjoinRoot p))))
                      (1 ⊗ₜ[R] root p) ⋯).comp
                  (Algebra.TensorProduct.lift (algHom T T (AdjoinRoot q)) (mapAlgHom includeRight p q ⋯) ⋯))).comp
            includeRight).comp
        (ofAlgHom R p))
      x✝ =
    (((AlgHom.restrictScalars R (AlgHom.id T (T ⊗[R] AdjoinRoot p))).comp includeRight).comp (ofAlgHom R p)) x✝

case refine_3.hRoot
R✝ : Type u_1
S✝ : Type u_2
T✝ : Type u_3
U✝ : Type u_4
K : Type u_5
R : Type u_6
S : Type u_7
T : Type u_8
U : Type u_9
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : CommRing U
inst✝ : Algebra R U
p✝ p : S[X]
q : (T ⊗[R] S)[X]
h : Polynomial.map includeRight.toRingHom p = q
⊢ ((AlgHom.restrictScalars R
            ((liftAlgHom q
                  (Algebra.TensorProduct.map (AlgHom.id T T) (AlgHom.restrictScalars R (ofId S (AdjoinRoot p))))
                  (1 ⊗ₜ[R] root p) ⋯).comp
              (Algebra.TensorProduct.lift (algHom T T (AdjoinRoot q)) (mapAlgHom includeRight p q ⋯) ⋯))).comp
        includeRight)
      (root p) =
    ((AlgHom.restrictScalars R (AlgHom.id T (T ⊗[R] AdjoinRoot p))).comp includeRight) (root p)