-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
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
j : Fin (c.length + 1)
hj : Membership.mem (γ := Set (Fin (c.length + 1))) univ j
i : Fin c.length
h_1 :
  ∀ (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) ↦ Fin.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
succ :
  ∀ (hj : Membership.mem (γ := Set (Fin (c.length + 1))) univ 0),
    (∀ (hi : Membership.mem (γ := Set (Fin (c.length + 1))) univ i.castSucc) (hij : i.castSucc ≠ 0)
        (h : 0 < 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) ↦ Fin.succ ∘ c.emb m) m))
          i.castSucc 0) →
      ∀ (hij : i.succ ≠ 0) (h : 0 < 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) ↦ Fin.succ ∘ c.emb m) m))
          i.succ 0
succ₁ :
  ∀ (j : Fin c.length),
    (∀ (hj : Membership.mem (γ := Set (Fin (c.length + 1))) univ j.castSucc),
        (∀ (hi : Membership.mem (γ := Set (Fin (c.length + 1))) univ i.castSucc) (hij : i.castSucc ≠ j.castSucc)
            (h : j.castSucc < 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) ↦ Fin.succ ∘ c.emb m) m))
              i.castSucc j.castSucc) →
          ∀ (hij : i.succ ≠ j.castSucc) (h : j.castSucc < 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) ↦ Fin.succ ∘ c.emb m) m))
              i.succ j.castSucc) →
      ∀ (hj : Membership.mem (γ := Set (Fin (c.length + 1))) univ j.succ),
        (∀ (hi : Membership.mem (γ := Set (Fin (c.length + 1))) univ i.castSucc) (hij : i.castSucc ≠ j.succ)
            (h : j.succ < 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) ↦ Fin.succ ∘ c.emb m) m))
              i.castSucc j.succ) →
          ∀ (hij : i.succ ≠ j.succ) (h : j.succ < 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) ↦ Fin.succ ∘ c.emb m) m))
              i.succ j.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) ↦ Fin.succ ∘ c.emb m) m))
    i.succ j

Tactic:
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)

Premises used: Iff.mpr, Set.mem_range, Function.onFun, Fin.succ, Nonempty.forall, and_imp, Fin.cases_zero, forall_exists_index, forall_eq', Fin.succ_inj, ne_eq, Set.disjoint_iff_forall_ne, Fin.succ_ne_zero, OrderedFinpartition.emb_ne_emb_of_ne, forall_const, Function.comp_apply, Fin.cases_succ, forall_apply_eq_imp_iff, Fin.cons_zero, exists_prop'