Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case ha
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
this : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
s : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R
i✝ : Fin m
⊢ ((((AlgHom.restrictScalars R (aeval (Sum.elim (fun x ↦ X x ⊗ₜ[R] 1) fun x ↦ 1 ⊗ₜ[R] X x))).comp
                (mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R)))).comp
            ↑(tensorEquivSum R (Fin m) (Fin k) R)).comp
        Algebra.TensorProduct.includeLeft)
      (X i✝) =
    ((AlgHom.id R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)).comp Algebra.TensorProduct.includeLeft) (X i✝)

pp: case hb
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
this : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
s : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R
i✝ : Fin k
⊢ ((AlgHom.restrictScalars R
            (((AlgHom.restrictScalars R (aeval (Sum.elim (fun x ↦ X x ⊗ₜ[R] 1) fun x ↦ 1 ⊗ₜ[R] X x))).comp
                  (mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R)))).comp
              ↑(tensorEquivSum R (Fin m) (Fin k) R))).comp
        Algebra.TensorProduct.includeRight)
      (X i✝) =
    ((AlgHom.restrictScalars R (AlgHom.id R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R))).comp
        Algebra.TensorProduct.includeRight)
      (X i✝)

Tactic:
<;>

Goal state after:
case ha
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
this : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
s : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R
i✝ : Fin m
⊢ ((((AlgHom.restrictScalars R (aeval (Sum.elim (fun x ↦ X x ⊗ₜ[R] 1) fun x ↦ 1 ⊗ₜ[R] X x))).comp
                (mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R)))).comp
            ↑(tensorEquivSum R (Fin m) (Fin k) R)).comp
        Algebra.TensorProduct.includeLeft)
      (X i✝) =
    ((AlgHom.id R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)).comp Algebra.TensorProduct.includeLeft) (X i✝)

case hb
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
this : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
s : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R
i✝ : Fin k
⊢ ((AlgHom.restrictScalars R
            (((AlgHom.restrictScalars R (aeval (Sum.elim (fun x ↦ X x ⊗ₜ[R] 1) fun x ↦ 1 ⊗ₜ[R] X x))).comp
                  (mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R)))).comp
              ↑(tensorEquivSum R (Fin m) (Fin k) R))).comp
        Algebra.TensorProduct.includeRight)
      (X i✝) =
    ((AlgHom.restrictScalars R (AlgHom.id R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R))).comp
        Algebra.TensorProduct.includeRight)
      (X i✝)