-- 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
i : Fin c.length
hi : Membership.mem (γ := Set (Fin (c.length + 1))) univ i.succ
j : Fin c.length
h_1 :
  ∀ (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
h_2 :
  ∀ (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
succ :
  ∀ (a : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize i.succ))
    (a_1 : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize j.succ)), ¬c.emb i a = c.emb j a_1
⊢ ∀ ⦃a : Fin (n + 1)⦄, a ∈ range (Fin.succ ∘ c.emb i) → ∀ ⦃b : Fin (n + 1)⦄, b ∈ range (Fin.succ ∘ c.emb j) → a ≠ b

Tactic:
simp only [mem_range, comp_apply, ne_eq, forall_exists_index, forall_apply_eq_imp_iff,
          succ_inj]

Premises used: Set.mem_range, forall_exists_index, Fin.succ_inj, ne_eq, Function.comp_apply, forall_apply_eq_imp_iff