-- 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
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
⊢ 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 ⋯)
have 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 sorry) :
    ℕ) =
  (↑(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 sorry) :
    ℕ)
Tactic: ext