-- 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_1 : ℕ
c_1 : OrderedFinpartition n_1
n : ℕ
c : OrderedFinpartition (n + 1)
h : range (ι := Fin (c.partSize 0)) (c.emb 0) = {0}
A : c.length - 1 + 1 = c.length
i : Fin (c.length - 1 + 1)
pos :
  partSize (n := n + 1)
      { length := c.length - 1 + 1,
        partSize :=
          cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1 fun (i : Fin (c.length - 1)) ↦
            c.partSize (Fin.cast ⋯ i.succ),
        partSize_pos := ⋯,
        emb := fun (i : Fin (c.length - 1 + 1)) ↦
          cases (motive := fun (x : Fin (c.length - 1 + 1)) ↦
            Fin
                (cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1
                  (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast ⋯ i.succ)) x) →
              Fin (n + 1))
            (fun
                (x :
                  Fin
                    (cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1
                      (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast ⋯ i.succ)) 0)) ↦
              0)
            (fun (m : Fin (c.length - 1)) ↦
              succ ∘ fun (j : Fin (c.partSize (Fin.cast ⋯ m.succ))) ↦ (c.emb (Fin.cast ⋯ m.succ) j).pred ⋯)
            i,
        emb_strictMono := ⋯, parts_strictMono := ⋯, disjoint := ⋯, cover := ⋯ : OrderedFinpartition (n + 1) }
      0 =
    c.partSize ⟨(↑0 : ℕ), ⋯⟩
pos₁ :
  ∀ (i : Fin (c.length - 1)),
    partSize (n := n + 1)
          { length := c.length - 1 + 1,
            partSize :=
              cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1 fun (i : Fin (c.length - 1)) ↦
                c.partSize (Fin.cast ⋯ i.succ),
            partSize_pos := ⋯,
            emb := fun (i : Fin (c.length - 1 + 1)) ↦
              cases (motive := fun (x : Fin (c.length - 1 + 1)) ↦
                Fin
                    (cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1
                      (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast ⋯ i.succ)) x) →
                  Fin (n + 1))
                (fun
                    (x :
                      Fin
                        (cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1
                          (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast ⋯ i.succ)) 0)) ↦
                  0)
                (fun (m : Fin (c.length - 1)) ↦
                  succ ∘ fun (j : Fin (c.partSize (Fin.cast ⋯ m.succ))) ↦ (c.emb (Fin.cast ⋯ m.succ) j).pred ⋯)
                i,
            emb_strictMono := ⋯, parts_strictMono := ⋯, disjoint := ⋯, cover := ⋯ : OrderedFinpartition (n + 1) }
          i.castSucc =
        c.partSize ⟨(↑i.castSucc : ℕ), ⋯⟩ →
      partSize (n := n + 1)
          { length := c.length - 1 + 1,
            partSize :=
              cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1 fun (i : Fin (c.length - 1)) ↦
                c.partSize (Fin.cast ⋯ i.succ),
            partSize_pos := ⋯,
            emb := fun (i : Fin (c.length - 1 + 1)) ↦
              cases (motive := fun (x : Fin (c.length - 1 + 1)) ↦
                Fin
                    (cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1
                      (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast ⋯ i.succ)) x) →
                  Fin (n + 1))
                (fun
                    (x :
                      Fin
                        (cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1
                          (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast ⋯ i.succ)) 0)) ↦
                  0)
                (fun (m : Fin (c.length - 1)) ↦
                  succ ∘ fun (j : Fin (c.partSize (Fin.cast ⋯ m.succ))) ↦ (c.emb (Fin.cast ⋯ m.succ) j).pred ⋯)
                i,
            emb_strictMono := ⋯, parts_strictMono := ⋯, disjoint := ⋯, cover := ⋯ : OrderedFinpartition (n + 1) }
          i.succ =
        c.partSize ⟨(↑i.succ : ℕ), ⋯⟩
⊢ partSize (n := n + 1)
      { length := c.length - 1 + 1,
        partSize :=
          cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1 fun (i : Fin (c.length - 1)) ↦
            c.partSize (Fin.cast ⋯ i.succ),
        partSize_pos := ⋯,
        emb := fun (i : Fin (c.length - 1 + 1)) ↦
          cases (motive := fun (x : Fin (c.length - 1 + 1)) ↦
            Fin
                (cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1
                  (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast ⋯ i.succ)) x) →
              Fin (n + 1))
            (fun
                (x :
                  Fin
                    (cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1
                      (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast ⋯ i.succ)) 0)) ↦
              0)
            (fun (m : Fin (c.length - 1)) ↦
              succ ∘ fun (j : Fin (c.partSize (Fin.cast ⋯ m.succ))) ↦ (c.emb (Fin.cast ⋯ m.succ) j).pred ⋯)
            i,
        emb_strictMono := ⋯, parts_strictMono := ⋯, disjoint := ⋯, cover := ⋯ : OrderedFinpartition (n + 1) }
      i =
    c.partSize ⟨(↑i : ℕ), ⋯⟩

Tactic:
induction i using Fin.induction with
        | zero => change 1 = c.partSize 0; simp [c.partSize_eq_one_of_range_emb_eq_singleton h]
        | succ i => simp only [cons_succ, val_succ]; rfl

Premises used: Fin.cons_succ, Fin.succ, Fin.val_succ, OrderedFinpartition.partSize, OrderedFinpartition.partSize_eq_one_of_range_emb_eq_singleton, OfNat.ofNat