-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c_1 c : OrderedFinpartition n
k i : Fin c.length
hi : Membership.mem (γ := Set (Fin c.length)) univ i
j : Fin c.length
hj : Membership.mem (γ := Set (Fin c.length)) univ j
hij : i ≠ j
inr :
  ∀
    (this :
      ∀ (i : Fin c.length) (hi : Membership.mem (γ := Set (Fin c.length)) univ i) (j : Fin c.length)
        (hj : Membership.mem (γ := Set (Fin c.length)) univ j) (hij : i ≠ j) (h : i ≠ k),
        onFun (β := Set (Fin (n + 1))) Disjoint
          (fun (m : Fin c.length) ↦
            range (ι := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m))
              (if h : m = k then
                have this :
                  update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m = c.partSize k + 1 := ⋯;
                (fun (i : Fin (c.partSize k + 1)) ↦
                    cases (motive := fun (x : Fin (c.partSize k + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb k) i) ∘
                  Fin.cast this
              else
                have this : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m = c.partSize m :=
                  ⋯;
                succ ∘ c.emb m ∘ Fin.cast this))
          i j)
    (h : ¬i ≠ k),
    onFun (β := Set (Fin (n + 1))) Disjoint
      (fun (m : Fin c.length) ↦
        range (ι := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m))
          (if h : m = k then
            have this : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m = c.partSize k + 1 :=
              ⋯;
            (fun (i : Fin (c.partSize k + 1)) ↦
                cases (motive := fun (x : Fin (c.partSize k + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb k) i) ∘
              Fin.cast this
          else
            have this : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m = c.partSize m := ⋯;
            succ ∘ c.emb m ∘ Fin.cast this))
      i j
⊢ onFun (β := Set (Fin (n + 1))) Disjoint
    (fun (m : Fin c.length) ↦
      range (ι := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m))
        (if h : m = k then
          have this : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m = c.partSize k + 1 :=
            ⋯;
          (fun (i : Fin (c.partSize k + 1)) ↦
              cases (motive := fun (x : Fin (c.partSize k + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb k) i) ∘
            Fin.cast this
        else
          have this : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m = c.partSize m := ⋯;
          succ ∘ c.emb m ∘ Fin.cast this))
    i j
have wlog : ∀ (i : Fin c.length) (hi : Membership.mem (γ := Set (Fin c.length)) univ i) (j : Fin c.length)
  (hj : Membership.mem (γ := Set (Fin c.length)) univ j) (hij : i ≠ j) (h : i ≠ k),
  onFun (β := Set (Fin (n + 1))) Disjoint
    (fun (m : Fin c.length) ↦
      range (ι := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m))
        (if h : m = k then
          have this : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m = c.partSize k + 1 :=
            sorry;
          (fun (i : Fin (c.partSize k + 1)) ↦
              cases (motive := fun (x : Fin (c.partSize k + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb k) i) ∘
            Fin.cast this
        else
          have this : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m = c.partSize m := sorry;
          succ ∘ c.emb m ∘ Fin.cast this))
    i j
Tactic: wlog h : i ≠ k generalizing i j
Cleared hypotheses: i, hi, j, hj, hij