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
p : MonicDegreeEq S n
f : { f // f.comp (universalFactorizationMap R n m k hn) = (mapEquivMonic R S n).symm p }
i✝ : Fin m
⊢ ((↑((fun q ↦
                ⟨Algebra.TensorProduct.lift ((mapEquivMonic R S m).symm (↑q).1) ((mapEquivMonic R S k).symm (↑q).2) ⋯,
                  ⋯⟩)
              ((fun f ↦
                  ⟨((mapEquivMonic R S m) ((↑f).comp Algebra.TensorProduct.includeLeft),
                      (mapEquivMonic R S k) ((↑f).comp Algebra.TensorProduct.includeRight)),
                    ⋯⟩)
                f))).comp
        Algebra.TensorProduct.includeLeft)
      (X i✝) =
    ((↑f).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
p : MonicDegreeEq S n
f : { f // f.comp (universalFactorizationMap R n m k hn) = (mapEquivMonic R S n).symm p }
i✝ : Fin k
⊢ ((AlgHom.restrictScalars R
            ↑((fun q ↦
                  ⟨Algebra.TensorProduct.lift ((mapEquivMonic R S m).symm (↑q).1) ((mapEquivMonic R S k).symm (↑q).2) ⋯,
                    ⋯⟩)
                ((fun f ↦
                    ⟨((mapEquivMonic R S m) ((↑f).comp Algebra.TensorProduct.includeLeft),
                        (mapEquivMonic R S k) ((↑f).comp Algebra.TensorProduct.includeRight)),
                      ⋯⟩)
                  f))).comp
        Algebra.TensorProduct.includeRight)
      (X i✝) =
    ((AlgHom.restrictScalars R ↑f).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
p : MonicDegreeEq S n
f : { f // f.comp (universalFactorizationMap R n m k hn) = (mapEquivMonic R S n).symm p }
i✝ : Fin m
⊢ ((↑((fun q ↦
                ⟨Algebra.TensorProduct.lift ((mapEquivMonic R S m).symm (↑q).1) ((mapEquivMonic R S k).symm (↑q).2) ⋯,
                  ⋯⟩)
              ((fun f ↦
                  ⟨((mapEquivMonic R S m) ((↑f).comp Algebra.TensorProduct.includeLeft),
                      (mapEquivMonic R S k) ((↑f).comp Algebra.TensorProduct.includeRight)),
                    ⋯⟩)
                f))).comp
        Algebra.TensorProduct.includeLeft)
      (X i✝) =
    ((↑f).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
p : MonicDegreeEq S n
f : { f // f.comp (universalFactorizationMap R n m k hn) = (mapEquivMonic R S n).symm p }
i✝ : Fin k
⊢ ((AlgHom.restrictScalars R
            ↑((fun q ↦
                  ⟨Algebra.TensorProduct.lift ((mapEquivMonic R S m).symm (↑q).1) ((mapEquivMonic R S k).symm (↑q).2) ⋯,
                    ⋯⟩)
                ((fun f ↦
                    ⟨((mapEquivMonic R S m) ((↑f).comp Algebra.TensorProduct.includeLeft),
                        (mapEquivMonic R S k) ((↑f).comp Algebra.TensorProduct.includeRight)),
                      ⋯⟩)
                  f))).comp
        Algebra.TensorProduct.includeRight)
      (X i✝) =
    ((AlgHom.restrictScalars R ↑f).comp Algebra.TensorProduct.includeRight) (X i✝)