-- Lean 4 proof step from Mathlib.RingTheory.FormalGroup.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
τ : Type u_4
σ : Type
F : FormalGroup R
f : R →+* S
this :
  ∀ (g₁ g₂ : MvPowerSeries (Fin 3) R),
    Eq.{u_2 + 1} (α := Fin (Nat.succ 0).succ → MvPowerSeries (Fin 3) S)
      (![((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 3) R) (MvPowerSeries (Fin 3) S)) :
              (a : MvPowerSeries (Fin 3) R) → MvPowerSeries (Fin 3) S)
            g₁,
          ((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 3) R) (MvPowerSeries (Fin 3) S)) :
              (a : MvPowerSeries (Fin 3) R) → MvPowerSeries (Fin 3) S)
            g₂] :
        Fin (Nat.succ 0).succ → MvPowerSeries (Fin 3) S)
      fun (i : Fin (Nat.succ 0).succ) ↦
      (((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 3) R) (MvPowerSeries (Fin 3) S)) :
            (a : MvPowerSeries (Fin 3) R) → MvPowerSeries (Fin 3) S)
          (![g₁, g₂] i) :
        MvPowerSeries (Fin 3) S)
simp_rw :
  Eq.{u_2 + 1} (α := MvPowerSeries (Fin 3) S)
    (subst (σ := Fin (Nat.succ 0).succ) (R := S)
      ![subst (σ := Fin (Nat.succ 0).succ) (R := S)
          ![((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 3) R) (MvPowerSeries (Fin 3) S)) :
                (a : MvPowerSeries (Fin 3) R) → MvPowerSeries (Fin 3) S)
              Y₀,
            ((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 3) R) (MvPowerSeries (Fin 3) S)) :
                (a : MvPowerSeries (Fin 3) R) → MvPowerSeries (Fin 3) S)
              Y₁]
          (((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 2) R) (MvPowerSeries (Fin 2) S)) :
              (a : MvPowerSeries (Fin 2) R) → MvPowerSeries (Fin 2) S)
            F.toPowerSeries),
        ((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 3) R) (MvPowerSeries (Fin 3) S)) :
            (a : MvPowerSeries (Fin 3) R) → MvPowerSeries (Fin 3) S)
          Y₂]
      (((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 2) R) (MvPowerSeries (Fin 2) S)) :
          (a : MvPowerSeries (Fin 2) R) → MvPowerSeries (Fin 2) S)
        F.toPowerSeries))
    (subst (σ := Fin (Nat.succ 0).succ) (R := S)
      ![((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 3) R) (MvPowerSeries (Fin 3) S)) :
            (a : MvPowerSeries (Fin 3) R) → MvPowerSeries (Fin 3) S)
          Y₀,
        subst (σ := Fin (Nat.succ 0).succ) (R := S)
          ![((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 3) R) (MvPowerSeries (Fin 3) S)) :
                (a : MvPowerSeries (Fin 3) R) → MvPowerSeries (Fin 3) S)
              Y₁,
            ((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 3) R) (MvPowerSeries (Fin 3) S)) :
                (a : MvPowerSeries (Fin 3) R) → MvPowerSeries (Fin 3) S)
              Y₂]
          (((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 2) R) (MvPowerSeries (Fin 2) S)) :
              (a : MvPowerSeries (Fin 2) R) → MvPowerSeries (Fin 2) S)
            F.toPowerSeries)]
      (((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 2) R) (MvPowerSeries (Fin 2) S)) :
          (a : MvPowerSeries (Fin 2) R) → MvPowerSeries (Fin 2) S)
        F.toPowerSeries))
simp_rw₁ :
  Eq.{u_2 + 1} (α := MvPowerSeries (Fin 3) S)
    (subst (σ := Fin (Nat.succ 0).succ) (R := S)
      ![subst (R := S)
          (fun (i : Fin (Nat.succ 0).succ) ↦
            ((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 3) R) (MvPowerSeries (Fin 3) S)) :
                (a : MvPowerSeries (Fin 3) R) → MvPowerSeries (Fin 3) S)
              (![Y₀, Y₁] i))
          (((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 2) R) (MvPowerSeries (Fin 2) S)) :
              (a : MvPowerSeries (Fin 2) R) → MvPowerSeries (Fin 2) S)
            F.toPowerSeries),
        ((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 3) R) (MvPowerSeries (Fin 3) S)) :
            (a : MvPowerSeries (Fin 3) R) → MvPowerSeries (Fin 3) S)
          Y₂]
      (((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 2) R) (MvPowerSeries (Fin 2) S)) :
          (a : MvPowerSeries (Fin 2) R) → MvPowerSeries (Fin 2) S)
        F.toPowerSeries))
    (subst (σ := Fin (Nat.succ 0).succ) (R := S)
      ![((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 3) R) (MvPowerSeries (Fin 3) S)) :
            (a : MvPowerSeries (Fin 3) R) → MvPowerSeries (Fin 3) S)
          Y₀,
        subst (R := S)
          (fun (i : Fin (Nat.succ 0).succ) ↦
            ((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 3) R) (MvPowerSeries (Fin 3) S)) :
                (a : MvPowerSeries (Fin 3) R) → MvPowerSeries (Fin 3) S)
              (![Y₁, Y₂] i))
          (((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 2) R) (MvPowerSeries (Fin 2) S)) :
              (a : MvPowerSeries (Fin 2) R) → MvPowerSeries (Fin 2) S)
            F.toPowerSeries)]
      (((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 2) R) (MvPowerSeries (Fin 2) S)) :
          (a : MvPowerSeries (Fin 2) R) → MvPowerSeries (Fin 2) S)
        F.toPowerSeries))
⊢ Eq.{u_2 + 1} (α := MvPowerSeries (Fin 3) S)
    (subst (R := S)
      ![subst (R := S) ![X 0, X 1]
          (((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 2) R) (MvPowerSeries (Fin 2) S)) :
              (a : MvPowerSeries (Fin 2) R) → MvPowerSeries (Fin 2) S)
            F.toPowerSeries),
        X 2]
      (((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 2) R) (MvPowerSeries (Fin 2) S)) :
          (a : MvPowerSeries (Fin 2) R) → MvPowerSeries (Fin 2) S)
        F.toPowerSeries))
    (subst (R := S)
      ![X 0,
        subst (R := S) ![X 1, X 2]
          (((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 2) R) (MvPowerSeries (Fin 2) S)) :
              (a : MvPowerSeries (Fin 2) R) → MvPowerSeries (Fin 2) S)
            F.toPowerSeries)]
      (((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 2) R) (MvPowerSeries (Fin 2) S)) :
          (a : MvPowerSeries (Fin 2) R) → MvPowerSeries (Fin 2) S)
        F.toPowerSeries))
have simp_rw₂ : Eq.{u_2 + 1} (α := MvPowerSeries (Fin 3) S)
  (subst (σ := Fin (Nat.succ 0).succ) (R := S)
    ![((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 3) R) (MvPowerSeries (Fin 3) S)) :
          (a : MvPowerSeries (Fin 3) R) → MvPowerSeries (Fin 3) S)
        (subst ![Y₀, Y₁] F.toPowerSeries),
      ((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 3) R) (MvPowerSeries (Fin 3) S)) :
          (a : MvPowerSeries (Fin 3) R) → MvPowerSeries (Fin 3) S)
        Y₂]
    (((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 2) R) (MvPowerSeries (Fin 2) S)) :
        (a : MvPowerSeries (Fin 2) R) → MvPowerSeries (Fin 2) S)
      F.toPowerSeries))
  (subst (σ := Fin (Nat.succ 0).succ) (R := S)
    ![((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 3) R) (MvPowerSeries (Fin 3) S)) :
          (a : MvPowerSeries (Fin 3) R) → MvPowerSeries (Fin 3) S)
        Y₀,
      ((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 3) R) (MvPowerSeries (Fin 3) S)) :
          (a : MvPowerSeries (Fin 3) R) → MvPowerSeries (Fin 3) S)
        (subst ![Y₁, Y₂] F.toPowerSeries)]
    (((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 2) R) (MvPowerSeries (Fin 2) S)) :
        (a : MvPowerSeries (Fin 2) R) → MvPowerSeries (Fin 2) S)
      F.toPowerSeries))
Tactic: simp_rw [(map_X f _).symm, this, ← map_subst .X_X, this, ← map_subst
      (HasSubst.cons_subst_zero_left (0 : Fin 3) 1 2 F.zero_constantCoeff), F.assoc,
      ← map_subst (HasSubst.cons_subst_zero_right (0 : Fin 3) 1 2 F.zero_constantCoeff)]