-- Lean 4 proof step from Mathlib.RingTheory.WittVector.TeichmullerSeries (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst : CommRing R
inst_1 : CharP R p
inst_2 : PerfectRing R p
S : Type u_2
inst_3 : CommRing S
f g : RingHom.{u_1, u_2} (𝕎 R) S
h :
  ∀ (x : R),
    Eq.{u_2 + 1} (α := S) ((f : (a : 𝕎 R) → S) ((teichmuller p : (a : R) → 𝕎 R) x : 𝕎 R) : S)
      ((g : (a : 𝕎 R) → S) ((teichmuller p : (a : R) → 𝕎 R) x : 𝕎 R) : S)
n : ℕ
hn : HPow.hPow (α := S) (↑p : S) n = 0
x c : 𝕎 R
hc :
  x -
      ∑ i ∈ Finset.Iic n,
        HMul.hMul (α := 𝕎 R)
          ((teichmuller p : (a : R) → 𝕎 R)
              ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) i : (a : R) → R) (x.coeff i) :
                R) :
            𝕎 R)
          (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i) =
    HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) (n + 1) * c
f₁ :
  (f : (a : 𝕎 R) → S) x =
    HAdd.hAdd (α := S) (β := S)
      ((f : (a : 𝕎 R) → S)
          (x -
            ∑ i ∈ Finset.Iic n,
              HMul.hMul (α := 𝕎 R)
                ((teichmuller p : (a : R) → 𝕎 R)
                    ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) i : (a : R) → R)
                        (x.coeff i) :
                      R) :
                  𝕎 R)
                (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)) :
        S)
      ((f : (a : 𝕎 R) → S)
          (∑ i ∈ Finset.Iic n,
            HMul.hMul (α := 𝕎 R)
              ((teichmuller p : (a : R) → 𝕎 R)
                  ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) i : (a : R) → R) (x.coeff i) :
                    R) :
                𝕎 R)
              (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)) :
        S)
f₂ :
  HAdd.hAdd (α := S) (β := S)
      ((f : (a : 𝕎 R) → S)
          (x -
            ∑ i ∈ Finset.Iic n,
              HMul.hMul (α := 𝕎 R)
                ((teichmuller p : (a : R) → 𝕎 R)
                    ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) i : (a : R) → R)
                        (x.coeff i) :
                      R) :
                  𝕎 R)
                (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)) :
        S)
      ((f : (a : 𝕎 R) → S)
          (∑ i ∈ Finset.Iic n,
            HMul.hMul (α := 𝕎 R)
              ((teichmuller p : (a : R) → 𝕎 R)
                  ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) i : (a : R) → R) (x.coeff i) :
                    R) :
                𝕎 R)
              (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)) :
        S) =
    ∑ i ∈ Finset.Iic n,
      HMul.hMul (α := S)
        ((f : (a : 𝕎 R) → S)
            ((teichmuller p : (a : R) → 𝕎 R)
                ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) i : (a : R) → R) (x.coeff i) :
                  R) :
              𝕎 R) :
          S)
        (HPow.hPow (α := S) (↑p : S) i)
f₃ :
  Eq.{u_2 + 1} (α := S)
    (∑ i ∈ Finset.Iic n,
      HMul.hMul (α := S)
        ((f : (a : 𝕎 R) → S)
            ((teichmuller p : (a : R) → 𝕎 R)
                ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) i : (a : R) → R) (x.coeff i) :
                  R) :
              𝕎 R) :
          S)
        (HPow.hPow (α := S) (↑p : S) i))
    (∑ i ∈ Finset.Iic n,
      HMul.hMul (α := S)
        ((g : (a : 𝕎 R) → S)
            ((teichmuller p : (a : R) → 𝕎 R)
                ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) i : (a : R) → R) (x.coeff i) :
                  R) :
              𝕎 R) :
          S)
        (HPow.hPow (α := S) (↑p : S) i))
⊢ Eq.{u_2 + 1} (α := S) ((f : (a : 𝕎 R) → S) x : S) ((g : (a : 𝕎 R) → S) x : S)
have f₄ : ∑ i ∈ Finset.Iic n,
    HMul.hMul (α := S)
      ((g : (a : 𝕎 R) → S)
          ((teichmuller p : (a : R) → 𝕎 R)
              ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) i : (a : R) → R) (x.coeff i) :
                R) :
            𝕎 R) :
        S)
      (HPow.hPow (α := S) (↑p : S) i) =
  HAdd.hAdd (α := S) (β := S)
    ((g : (a : 𝕎 R) → S)
        (x -
          ∑ i ∈ Finset.Iic n,
            HMul.hMul (α := 𝕎 R)
              ((teichmuller p : (a : R) → 𝕎 R)
                  ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) i : (a : R) → R) (x.coeff i) :
                    R) :
                𝕎 R)
              (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)) :
      S)
    ((g : (a : 𝕎 R) → S)
        (∑ i ∈ Finset.Iic n,
          HMul.hMul (α := 𝕎 R)
            ((teichmuller p : (a : R) → 𝕎 R)
                ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) i : (a : R) → R) (x.coeff i) :
                  R) :
              𝕎 R)
            (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)) :
      S)
Tactic: calc
    f x = f (x - ∑ (i ≤ n), teichmuller p (((_root_.frobeniusEquiv R p).symm ^ i)
        (x.coeff i)) * p ^ i) + f (∑ (i ≤ n), teichmuller p
        (((_root_.frobeniusEquiv R p).symm ^ i) (x.coeff i)) * p ^ i) := by simp
    _ = ∑ (i ≤ n), f (teichmuller p (((_root_.frobeniusEquiv R p).symm ^ i)
        (x.coeff i))) * p ^ i := by rw [hc]; simp [pow_succ, hn]
    _ = ∑ (i ≤ n), g (teichmuller p
        (((_root_.frobeniusEquiv R p).symm ^ i) (x.coeff i))) * p ^ i := by simp [h]
    _ = g (x - ∑ (i ≤ n), teichmuller p (((_root_.frobeniusEquiv R p).symm ^ i)
        (x.coeff i)) * p ^ i) + g (∑ (i ≤ n), teichmuller p (((_root_.frobeniusEquiv R p).symm ^ i)
        (x.coeff i)) * p ^ i) := by rw [hc]; simp [pow_succ, hn]
    _ = g x := by simp