Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: 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 (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 =
    (AlgHom.restrictScalars (MvPolynomial (Fin n) R) f).comp Algebra.TensorProduct.includeRight

Tactic:
refine AlgHom.restrictScalars_injective R (Algebra.TensorProduct.ext ?_ ?_)

Goal state after:
case refine_1
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 (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.includeLeft =
    (AlgHom.restrictScalars R
          ((AlgHom.restrictScalars (MvPolynomial (Fin n) R) f).comp Algebra.TensorProduct.includeRight)).comp
      Algebra.TensorProduct.includeLeft

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