Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this✝³ : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (MvPolynomial.universalFactorizationMap R n m k hn).toAlgebra
this✝² : Algebra (MvPolynomial (Fin n) R) R := ((MvPolynomial.mapEquivMonic R R n).symm p).toAlgebra
this✝¹ : Algebra (MvPolynomial (Fin n) R) S := Algebra.compHom S ((MvPolynomial.mapEquivMonic R R n).symm p).toRingHom
this✝ : IsScalarTower (MvPolynomial (Fin n) R) R S
this : IsScalarTower R (MvPolynomial (Fin n) R) S
⊢ (AlgHom.restrictScalars R
          (AlgHom.restrictScalars R
            ((AlgHom.restrictScalars (MvPolynomial (Fin n) R)
                  ((fun q ↦
                      Algebra.TensorProduct.lift (Algebra.ofId R S)
                        (let __RingHom :=
                          (↑((MvPolynomial.universalFactorizationMapLiftEquiv R S n m k hn
                                    (p.map (algebraMap R S))).symm
                                q)).toRingHom;
                        { toRingHom := __RingHom, commutes' := ⋯ })
                        ⋯)
                    ((fun f ↦ ⟨((factor₁ m k hn p).map ↑f, (factor₂ m k hn p).map ↑f), ⋯⟩) f))).comp
              Algebra.TensorProduct.includeRight))).comp
      Algebra.TensorProduct.includeRight =
    (AlgHom.restrictScalars R
          (AlgHom.restrictScalars R
            ((AlgHom.restrictScalars (MvPolynomial (Fin n) R) f).comp Algebra.TensorProduct.includeRight))).comp
      Algebra.TensorProduct.includeRight

Tactic:
ext

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this✝³ : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (MvPolynomial.universalFactorizationMap R n m k hn).toAlgebra
this✝² : Algebra (MvPolynomial (Fin n) R) R := ((MvPolynomial.mapEquivMonic R R n).symm p).toAlgebra
this✝¹ : Algebra (MvPolynomial (Fin n) R) S := Algebra.compHom S ((MvPolynomial.mapEquivMonic R R n).symm p).toRingHom
this✝ : IsScalarTower (MvPolynomial (Fin n) R) R S
this : IsScalarTower R (MvPolynomial (Fin n) R) S
i✝ : Fin k
⊢ ((AlgHom.restrictScalars R
            (AlgHom.restrictScalars R
              ((AlgHom.restrictScalars (MvPolynomial (Fin n) R)
                    ((fun q ↦
                        Algebra.TensorProduct.lift (Algebra.ofId R S)
                          (let __RingHom :=
                            (↑((MvPolynomial.universalFactorizationMapLiftEquiv R S n m k hn
                                      (p.map (algebraMap R S))).symm
                                  q)).toRingHom;
                          { toRingHom := __RingHom, commutes' := ⋯ })
                          ⋯)
                      ((fun f ↦ ⟨((factor₁ m k hn p).map ↑f, (factor₂ m k hn p).map ↑f), ⋯⟩) f))).comp
                Algebra.TensorProduct.includeRight))).comp
        Algebra.TensorProduct.includeRight)
      (MvPolynomial.X i✝) =
    ((AlgHom.restrictScalars R
            (AlgHom.restrictScalars R
              ((AlgHom.restrictScalars (MvPolynomial (Fin n) R) f).comp Algebra.TensorProduct.includeRight))).comp
        Algebra.TensorProduct.includeRight)
      (MvPolynomial.X i✝)