-- Lean 4 proof step from Mathlib.Algebra.Colimit.Ring (goal)
Goal:
ι : Type u_1
inst : Preorder ι
G : ι → Type u_2
inst_1 : (i : ι) → CommRing (G i)
f' : (i j : ι) → i ≤ j → G i →+* G j
inst_2 : Nonempty ι
inst_3 : IsDirectedOrder ι
q : (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X]
n : ℕ
z : DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)
h_1 :
  ∃ (i : ι) (p : (G i)[X]),
    Polynomial.map (of G (fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) i) p =
      HMul.hMul (α := (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
        ((C :
              (a : DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) →
                (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
            z :
          (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
        (HPow.hPow (α := (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X]) X n)
i : ι
x : G i
h :
  (of G (fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) i :
        (a : G i) → DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))
      x =
    z
rw :
  HMul.hMul (α := (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
      (Polynomial.map (of G (fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) i)
        ((C : (a : G i) → (G i)[X]) x))
      (Polynomial.map (of G (fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) i)
        (HPow.hPow (α := (G i)[X]) X (n + 1))) =
    HMul.hMul (α := (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
      ((C :
            (a : DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) →
              (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
          z :
        (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
      (HPow.hPow (α := (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X]) X (n + 1))
rw₁ :
  HMul.hMul (α := (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X]) (β :=
      (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
      ((C :
            (a : DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) →
              (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
          ((of G (fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) i :
              (a : G i) → DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))
            x) :
        (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
      (Polynomial.map (of G (fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) i)
        (HPow.hPow (α := (G i)[X]) X (n + 1))) =
    HMul.hMul (α := (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
      ((C :
            (a : DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) →
              (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
          z :
        (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
      (HPow.hPow (α := (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X]) X (n + 1))
rw₂ :
  HMul.hMul (α := (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X]) (β :=
      (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
      ((C :
            (a : DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) →
              (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
          z :
        (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
      (Polynomial.map (of G (fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) i)
        (HPow.hPow (α := (G i)[X]) X (n + 1))) =
    HMul.hMul (α := (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
      ((C :
            (a : DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) →
              (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
          z :
        (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
      (HPow.hPow (α := (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X]) X (n + 1))
rw₃ :
  HMul.hMul (α := (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
      ((C :
            (a : DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) →
              (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
          z :
        (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
      (HPow.hPow (α := (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
        (Polynomial.map (of G (fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) i) X) (n + 1)) =
    HMul.hMul (α := (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
      ((C :
            (a : DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) →
              (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
          z :
        (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
      (HPow.hPow (α := (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X]) X (n + 1))
⊢ Polynomial.map (of G (fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) i)
      (HMul.hMul (α := (G i)[X]) ((C : (a : G i) → (G i)[X]) x : (G i)[X]) (HPow.hPow (α := (G i)[X]) X (n + 1))) =
    HMul.hMul (α := (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
      ((C :
            (a : DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) →
              (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
          z :
        (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
      (HPow.hPow (α := (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X]) X (n + 1))
have rw₄ : HMul.hMul (α := (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
    ((C :
          (a : DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) →
            (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
        z :
      (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
    (HPow.hPow (α := (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X]) X (n + 1)) =
  HMul.hMul (α := (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
    ((C :
          (a : DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) →
            (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
        z :
      (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
    (HPow.hPow (α := (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X]) X (n + 1))
Tactic: rw [Polynomial.map_mul, map_C, h, Polynomial.map_pow, map_X]