-- Module: Mathlib.RingTheory.WittVector.TeichmullerSeries
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst : CommRing R
inst_1 : CharP R p
inst_2 : PerfectRing R p
x : 𝕎 R
n_1 i : ℕ
hi : i < n_1 + 1
n : ℕ
x_1 x_2 :
  (↑{r : ℕ |
        r ∈ Finset.Iic n_1 ∧
          (HMul.hMul (α := 𝕎 R)
                  ((teichmuller p : (a : R) → 𝕎 R)
                      ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) r : (a : R) → R)
                          (x.coeff r) :
                        R) :
                    𝕎 R)
                  (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) r)).coeff
              n ≠
            0} :
    Type)
a : ℕ
left : a ∈ Finset.Iic n_1
ha :
  (HMul.hMul (α := 𝕎 R)
          ((teichmuller p : (a : R) → 𝕎 R)
              ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) a : (a : R) → R) (x.coeff a) :
                R) :
            𝕎 R)
          (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) a)).coeff
      n ≠
    0
b : ℕ
left_1 : b ∈ Finset.Iic n_1
hb :
  (HMul.hMul (α := 𝕎 R)
          ((teichmuller p : (a : R) → 𝕎 R)
              ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) b : (a : R) → R) (x.coeff b) :
                R) :
            𝕎 R)
          (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) b)).coeff
      n ≠
    0
h :
  (↑(Subtype.mk (p := fun (x_3 : ℕ) ↦
          Membership.mem (γ := Set ℕ)
            {r : ℕ |
              r ∈ Finset.Iic n_1 ∧
                (HMul.hMul (α := 𝕎 R)
                        ((teichmuller p : (a : R) → 𝕎 R)
                            ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) r : (a : R) → R)
                                (x.coeff r) :
                              R) :
                          𝕎 R)
                        (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) r)).coeff
                    n ≠
                  0}
            x_3)
          a ⋯) :
      ℕ) =
    (↑(Subtype.mk (p := fun (x_3 : ℕ) ↦
          Membership.mem (γ := Set ℕ)
            {r : ℕ |
              r ∈ Finset.Iic n_1 ∧
                (HMul.hMul (α := 𝕎 R)
                        ((teichmuller p : (a : R) → 𝕎 R)
                            ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) r : (a : R) → R)
                                (x.coeff r) :
                              R) :
                          𝕎 R)
                        (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) r)).coeff
                    n ≠
                  0}
            x_3)
          b ⋯) :
      ℕ)
⊢ Eq (α :=
    (↑{r : ℕ |
          r ∈ Finset.Iic n_1 ∧
            (HMul.hMul (α := 𝕎 R)
                    ((teichmuller p : (a : R) → 𝕎 R)
                        ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) r : (a : R) → R)
                            (x.coeff r) :
                          R) :
                      𝕎 R)
                    (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) r)).coeff
                n ≠
              0} :
      Type))
    (Subtype.mk (p := fun (x_3 : ℕ) ↦
      Membership.mem (γ := Set ℕ)
        {r : ℕ |
          r ∈ Finset.Iic n_1 ∧
            (HMul.hMul (α := 𝕎 R)
                    ((teichmuller p : (a : R) → 𝕎 R)
                        ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) r : (a : R) → R)
                            (x.coeff r) :
                          R) :
                      𝕎 R)
                    (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) r)).coeff
                n ≠
              0}
        x_3)
      a ⋯)
    (Subtype.mk (p := fun (x_3 : ℕ) ↦
      Membership.mem (γ := Set ℕ)
        {r : ℕ |
          r ∈ Finset.Iic n_1 ∧
            (HMul.hMul (α := 𝕎 R)
                    ((teichmuller p : (a : R) → 𝕎 R)
                        ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) r : (a : R) → R)
                            (x.coeff r) :
                          R) :
                      𝕎 R)
                    (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) r)).coeff
                n ≠
              0}
        x_3)
      b ⋯)

Tactic:
ext