-- Module: Mathlib.RingTheory.FormalGroup.Basic
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))
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))
simp_rw₃ :
  Eq.{u_2 + 1} (α := MvPowerSeries (Fin 3) 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)
          (![subst ![Y₀, Y₁] F.toPowerSeries, 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))
    (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₀, subst ![Y₁, Y₂] F.toPowerSeries] 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))
simp_rw₄ :
  Eq.{u_2 + 1} (α := 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)
        (subst ![subst ![Y₀, Y₁] F.toPowerSeries, Y₂] F.toPowerSeries) :
      MvPowerSeries (Fin 3) 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₀, subst ![Y₁, Y₂] F.toPowerSeries] 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 (Fin 3) S)
simp_rw₅ :
  Eq.{u_2 + 1} (α := 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)
        (subst ![Y₀, subst ![Y₁, Y₂] F.toPowerSeries] F.toPowerSeries) :
      MvPowerSeries (Fin 3) 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₀, subst ![Y₁, Y₂] F.toPowerSeries] 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 (Fin 3) S)
⊢ 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))

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)]

Premises used: FormalGroup.zero_constantCoeff, MvPowerSeries.map_subst, MvPowerSeries.HasSubst.X_X, MvPowerSeries.HasSubst.cons_subst_zero_left, FormalGroup.assoc, OfNat.ofNat, Eq.symm, MvPowerSeries.map_X, MvPowerSeries.HasSubst.cons_subst_zero_right