-- 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)
h' : i ≍ Fin.cast A i
j :
  Fin
    (cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1 (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast ⋯ i.succ))
      i)
pos :
  ∀ (h' : HEq (α := Fin (c.length - 1 + 1)) 0 (Fin.cast A 0))
    (j :
      Fin
        (cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1
          (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast ⋯ i.succ)) 0)),
    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 ⋯)
        0 j =
      c.emb (Fin.cast A 0) (⟨(↑j : ℕ), ⋯⟩ : Fin (c.partSize (Fin.cast A 0)))
pos₁ :
  ∀ (i : Fin (c.length - 1)),
    (∀ (h' : i.castSucc ≍ Fin.cast A i.castSucc)
        (j :
          Fin
            (cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1
              (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast ⋯ i.succ)) i.castSucc)),
        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.castSucc j =
          c.emb (Fin.cast A i.castSucc) (⟨(↑j : ℕ), ⋯⟩ : Fin (c.partSize (Fin.cast A i.castSucc)))) →
      ∀ (h' : i.succ ≍ Fin.cast A i.succ)
        (j :
          Fin
            (cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1
              (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast ⋯ i.succ)) i.succ)),
        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.succ j =
          c.emb (Fin.cast A i.succ) (⟨(↑j : ℕ), ⋯⟩ : Fin (c.partSize (Fin.cast A i.succ)))
⊢ 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 j =
    c.emb (Fin.cast A i) (⟨(↑j : ℕ), ⋯⟩ : Fin (c.partSize (Fin.cast A i)))

Tactic:
induction i using Fin.induction with
          | zero =>
            simp only [cases_zero, cast_zero, val_eq_zero]
            exact (apply_eq_of_range_eq_singleton h _).symm
          | succ i => simp

Premises used: Fin.succ, Fin.cases_zero, Fin.val_eq_zero, Fin.cast_zero, Eq.symm, Function.apply_eq_of_range_eq_singleton