-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
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 + 1)
j : Fin c.length
h :
  ∀ (hij : i < j.castSucc),
    LT.lt (α := Fin (n + 1))
      ((fun (m : Fin (c.length + 1)) ↦
          (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
              ⟨HSub.hSub (α := ℕ) (β := ℕ) (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize m : ℕ) 1, ⋯⟩ :
            Fin (n + 1)))
        i)
      ((fun (m : Fin (c.length + 1)) ↦
          (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
              ⟨HSub.hSub (α := ℕ) (β := ℕ) (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize m : ℕ) 1, ⋯⟩ :
            Fin (n + 1)))
        j.castSucc)
hij : i < j.succ
succ :
  (∀ (hij : 0 < j.castSucc),
      LT.lt (α := Fin (n + 1))
        ((fun (m : Fin (c.length + 1)) ↦
            (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
                ⟨HSub.hSub (α := ℕ) (β := ℕ) (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize m : ℕ) 1, ⋯⟩ :
              Fin (n + 1)))
          0)
        ((fun (m : Fin (c.length + 1)) ↦
            (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
                ⟨HSub.hSub (α := ℕ) (β := ℕ) (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize m : ℕ) 1, ⋯⟩ :
              Fin (n + 1)))
          j.castSucc)) →
    ∀ (hij : 0 < j.succ),
      LT.lt (α := Fin (n + 1))
        ((fun (m : Fin (c.length + 1)) ↦
            (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
                ⟨HSub.hSub (α := ℕ) (β := ℕ) (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize m : ℕ) 1, ⋯⟩ :
              Fin (n + 1)))
          0)
        ((fun (m : Fin (c.length + 1)) ↦
            (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
                ⟨HSub.hSub (α := ℕ) (β := ℕ) (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize m : ℕ) 1, ⋯⟩ :
              Fin (n + 1)))
          j.succ)
⊢ LT.lt (α := Fin (n + 1))
    ((fun (m : Fin (c.length + 1)) ↦
        (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
            ⟨HSub.hSub (α := ℕ) (β := ℕ) (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize m : ℕ) 1, ⋯⟩ :
          Fin (n + 1)))
      i)
    ((fun (m : Fin (c.length + 1)) ↦
        (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
            ⟨HSub.hSub (α := ℕ) (β := ℕ) (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize m : ℕ) 1, ⋯⟩ :
          Fin (n + 1)))
      j.succ)
have succ₁ : ∀ (i : Fin c.length),
  ((∀ (hij : i.castSucc < j.castSucc),
        LT.lt (α := Fin (n + 1))
          ((fun (m : Fin (c.length + 1)) ↦
              (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
                  ⟨HSub.hSub (α := ℕ) (β := ℕ) (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize m : ℕ) 1, sorry⟩ :
                Fin (n + 1)))
            i.castSucc)
          ((fun (m : Fin (c.length + 1)) ↦
              (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
                  ⟨HSub.hSub (α := ℕ) (β := ℕ) (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize m : ℕ) 1, sorry⟩ :
                Fin (n + 1)))
            j.castSucc)) →
      ∀ (hij : i.castSucc < j.succ),
        LT.lt (α := Fin (n + 1))
          ((fun (m : Fin (c.length + 1)) ↦
              (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
                  ⟨HSub.hSub (α := ℕ) (β := ℕ) (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize m : ℕ) 1, sorry⟩ :
                Fin (n + 1)))
            i.castSucc)
          ((fun (m : Fin (c.length + 1)) ↦
              (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
                  ⟨HSub.hSub (α := ℕ) (β := ℕ) (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize m : ℕ) 1, sorry⟩ :
                Fin (n + 1)))
            j.succ)) →
    (∀ (hij : i.succ < j.castSucc),
        LT.lt (α := Fin (n + 1))
          ((fun (m : Fin (c.length + 1)) ↦
              (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
                  ⟨HSub.hSub (α := ℕ) (β := ℕ) (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize m : ℕ) 1, sorry⟩ :
                Fin (n + 1)))
            i.succ)
          ((fun (m : Fin (c.length + 1)) ↦
              (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
                  ⟨HSub.hSub (α := ℕ) (β := ℕ) (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize m : ℕ) 1, sorry⟩ :
                Fin (n + 1)))
            j.castSucc)) →
      ∀ (hij : i.succ < j.succ),
        LT.lt (α := Fin (n + 1))
          ((fun (m : Fin (c.length + 1)) ↦
              (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
                  ⟨HSub.hSub (α := ℕ) (β := ℕ) (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize m : ℕ) 1, sorry⟩ :
                Fin (n + 1)))
            i.succ)
          ((fun (m : Fin (c.length + 1)) ↦
              (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
                  ⟨HSub.hSub (α := ℕ) (β := ℕ) (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize m : ℕ) 1, sorry⟩ :
                Fin (n + 1)))
            j.succ)
Tactic: induction i using Fin.induction with
      | zero => simp
      | succ i =>
        simp only [cons_succ, cases_succ, comp_apply, succ_lt_succ_iff]
        exact c.parts_strictMono (by simpa using hij)
Cleared hypotheses: i, h, hij