-- 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
i : Fin (c.length + 1)
hi : Membership.mem (γ := Set (Fin (c.length + 1))) univ i
j : Fin (c.length + 1)
hj : Membership.mem (γ := Set (Fin (c.length + 1))) univ j
hij : i ≠ j
h : j < i
zero :
  ∀ (hi : Membership.mem (γ := Set (Fin (c.length + 1))) univ 0) (hij : 0 ≠ j) (h : j < 0),
    onFun (β := Set (Fin (n + 1))) Disjoint
      (fun (m : Fin (c.length + 1)) ↦
        range (ι := Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize m))
          (cases (motive := fun (x : Fin (c.length + 1)) ↦
            Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize x) → Fin (n + 1))
            (fun (x : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize 0)) ↦ 0)
            (fun (m : Fin c.length) ↦ succ ∘ c.emb m) m))
      0 j
⊢ onFun (β := Set (Fin (n + 1))) Disjoint
    (fun (m : Fin (c.length + 1)) ↦
      range (ι := Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize m))
        (cases (motive := fun (x : Fin (c.length + 1)) ↦
          Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize x) → Fin (n + 1))
          (fun (x : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize 0)) ↦ 0)
          (fun (m : Fin c.length) ↦ succ ∘ c.emb m) m))
    i j
have succ : ∀ (i : Fin c.length),
  (∀ (hi : Membership.mem (γ := Set (Fin (c.length + 1))) univ i.castSucc) (hij : i.castSucc ≠ j) (h : j < i.castSucc),
      onFun (β := Set (Fin (n + 1))) Disjoint
        (fun (m : Fin (c.length + 1)) ↦
          range (ι := Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize m))
            (cases (motive := fun (x : Fin (c.length + 1)) ↦
              Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize x) → Fin (n + 1))
              (fun (x : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize 0)) ↦ 0)
              (fun (m : Fin c.length) ↦ succ ∘ c.emb m) m))
        i.castSucc j) →
    ∀ (hi : Membership.mem (γ := Set (Fin (c.length + 1))) univ i.succ) (hij : i.succ ≠ j) (h : j < i.succ),
      onFun (β := Set (Fin (n + 1))) Disjoint
        (fun (m : Fin (c.length + 1)) ↦
          range (ι := Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize m))
            (cases (motive := fun (x : Fin (c.length + 1)) ↦
              Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize x) → Fin (n + 1))
              (fun (x : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize 0)) ↦ 0)
              (fun (m : Fin c.length) ↦ succ ∘ c.emb m) m))
        i.succ j
Tactic: induction i using Fin.induction with
    | zero => simp at h
    | succ i =>
      induction j using Fin.induction with
      | zero =>
        simp only [onFun, cases_succ, cases_zero]
        apply Set.disjoint_iff_forall_ne.2
        simp only [mem_range, comp_apply, exists_prop', cons_zero, ne_eq, and_imp,
          Nonempty.forall, forall_const, forall_eq', forall_exists_index, forall_apply_eq_imp_iff]
        exact fun _ ↦ succ_ne_zero _
      | succ j =>
        simp only [onFun, cases_succ]
        apply Set.disjoint_iff_forall_ne.2
        simp only [mem_range, comp_apply, ne_eq, forall_exists_index, forall_apply_eq_imp_iff,
          succ_inj]
        intro a b
        apply c.emb_ne_emb_of_ne (by simpa using hij)
Cleared hypotheses: i, hi, hij, h