-- 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
m : Fin c.length
a' : Fin (c.partSize m + 1)
b : Fin (c.partSize m)
h :
  ∀ (h' : a' < b.castSucc),
    LT.lt (α := Fin (n + 1))
      (cases (motive := fun (x : Fin (c.partSize m + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb m) a' : Fin (n + 1))
      (cases (motive := fun (x : Fin (c.partSize m + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb m) b.castSucc : Fin (n + 1))
h' : a' < b.succ
inl :
  (∀ (h' : 0 < b.castSucc),
      LT.lt (α := Fin (n + 1))
        (cases (motive := fun (x : Fin (c.partSize m + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb m) 0 : Fin (n + 1))
        (cases (motive := fun (x : Fin (c.partSize m + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb m) b.castSucc :
          Fin (n + 1))) →
    ∀ (h' : 0 < b.succ),
      LT.lt (α := Fin (n + 1))
        (cases (motive := fun (x : Fin (c.partSize m + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb m) 0 : Fin (n + 1))
        (cases (motive := fun (x : Fin (c.partSize m + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb m) b.succ : Fin (n + 1))
inl₁ :
  ∀ (a' : Fin (c.partSize m)),
    ((∀ (h' : a'.castSucc < b.castSucc),
          LT.lt (α := Fin (n + 1))
            (cases (motive := fun (x : Fin (c.partSize m + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb m) a'.castSucc :
              Fin (n + 1))
            (cases (motive := fun (x : Fin (c.partSize m + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb m) b.castSucc :
              Fin (n + 1))) →
        ∀ (h' : a'.castSucc < b.succ),
          LT.lt (α := Fin (n + 1))
            (cases (motive := fun (x : Fin (c.partSize m + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb m) a'.castSucc :
              Fin (n + 1))
            (cases (motive := fun (x : Fin (c.partSize m + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb m) b.succ :
              Fin (n + 1))) →
      (∀ (h' : a'.succ < b.castSucc),
          LT.lt (α := Fin (n + 1))
            (cases (motive := fun (x : Fin (c.partSize m + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb m) a'.succ : Fin (n + 1))
            (cases (motive := fun (x : Fin (c.partSize m + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb m) b.castSucc :
              Fin (n + 1))) →
        ∀ (h' : a'.succ < b.succ),
          LT.lt (α := Fin (n + 1))
            (cases (motive := fun (x : Fin (c.partSize m + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb m) a'.succ : Fin (n + 1))
            (cases (motive := fun (x : Fin (c.partSize m + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb m) b.succ : Fin (n + 1))
⊢ LT.lt (α := Fin (n + 1))
    (cases (motive := fun (x : Fin (c.partSize m + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb m) a' : Fin (n + 1))
    (cases (motive := fun (x : Fin (c.partSize m + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb m) b.succ : Fin (n + 1))

Tactic:
induction a' using Fin.induction with
        | zero => simp
        | succ a' =>
          simp only [cases_succ, comp_apply, succ_lt_succ_iff]
          exact c.emb_strictMono m (by simpa using h')

Premises used: Fin.succ, Fin.succ_lt_succ_iff, Function.comp_apply, Fin.cases_succ, OrderedFinpartition.emb_strictMono