-- 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 i : ℕ
hi : i < n + 1
⊢ ∀ (n_1 : ℕ),
    Subsingleton
      (↑{r : ℕ |
            r ∈ Finset.Iic n ∧
              (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_1 ≠
                0} :
        Type)
have h : ∀ (n_1 : ℕ)
  (x_1 x_2 :
    (↑{r : ℕ |
          r ∈ Finset.Iic n ∧
            (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_1 ≠
              0} :
      Type))
  (a : ℕ) (left : a ∈ Finset.Iic n)
  (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_1 ≠
      0)
  (b : ℕ) (left_1 : b ∈ Finset.Iic n)
  (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_1 ≠
      0),
  Eq (α :=
    (↑{r : ℕ |
          r ∈ Finset.Iic n ∧
            (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_1 ≠
              0} :
      Type))
    (Subtype.mk (p := fun (x_3 : ℕ) ↦
      Membership.mem (γ := Set ℕ)
        {r : ℕ |
          r ∈ Finset.Iic n ∧
            (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_1 ≠
              0}
        x_3)
      a sorry)
    (Subtype.mk (p := fun (x_3 : ℕ) ↦
      Membership.mem (γ := Set ℕ)
        {r : ℕ |
          r ∈ Finset.Iic n ∧
            (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_1 ≠
              0}
        x_3)
      b sorry)
Tactic: refine fun n ↦ ⟨fun ⟨a, _, ha⟩ ⟨b, _, hb⟩ ↦ ?_⟩