-- 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 i : ℕ
hi : i < n + 1
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 ⋯)
      (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 ⋯)
⊢ ∀ (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)

Tactic:
refine fun n ↦ ⟨fun ⟨a, _, ha⟩ ⟨b, _, hb⟩ ↦ ?_⟩