-- 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 : OrderedFinpartition n
c : OrderedFinpartition 1
h₁ : c.length = 1
h₂ : ∀ (i : Fin c.length), c.partSize i = 1
h₃ : ∀ (i : Fin c.length) (j : Fin (c.partSize i)), c.emb i j = 0
rcases :
  ∀ (length : ℕ) (partSize : Fin length → ℕ) (partSize_pos : ∀ (m : Fin length), 0 < partSize m)
    (emb : (m : Fin length) → Fin (partSize m) → Fin 1) (emb_strictMono : ∀ (m : Fin length), StrictMono (emb m))
    (parts_strictMono : StrictMono (β := Fin 1) fun (m : Fin length) ↦ emb m (⟨partSize m - 1, ⋯⟩ : Fin (partSize m)))
    (disjoint : PairwiseDisjoint (α := Set (Fin 1)) univ fun (m : Fin length) ↦ range (emb m))
    (cover : ∀ (x : Fin 1), ∃ (m : Fin length), x ∈ range (emb m))
    (h₁ :
      { length := length, partSize := partSize, partSize_pos := partSize_pos, emb := emb,
            emb_strictMono := emb_strictMono, parts_strictMono := parts_strictMono, disjoint := disjoint,
            cover := cover : OrderedFinpartition 1 }.length =
        1)
    (h₂ :
      ∀
        (i :
          Fin
            { length := length, partSize := partSize, partSize_pos := partSize_pos, emb := emb,
                emb_strictMono := emb_strictMono, parts_strictMono := parts_strictMono, disjoint := disjoint,
                cover := cover : OrderedFinpartition 1 }.length),
        { length := length, partSize := partSize, partSize_pos := partSize_pos, emb := emb,
                emb_strictMono := emb_strictMono, parts_strictMono := parts_strictMono, disjoint := disjoint,
                cover := cover : OrderedFinpartition 1 }.partSize
            i =
          1)
    (h₃ :
      ∀
        (i :
          Fin
            { length := length, partSize := partSize, partSize_pos := partSize_pos, emb := emb,
                emb_strictMono := emb_strictMono, parts_strictMono := parts_strictMono, disjoint := disjoint,
                cover := cover : OrderedFinpartition 1 }.length)
        (j :
          Fin
            ({ length := length, partSize := partSize, partSize_pos := partSize_pos, emb := emb,
                  emb_strictMono := emb_strictMono, parts_strictMono := parts_strictMono, disjoint := disjoint,
                  cover := cover : OrderedFinpartition 1 }.partSize
              i)),
        { length := length, partSize := partSize, partSize_pos := partSize_pos, emb := emb,
                emb_strictMono := emb_strictMono, parts_strictMono := parts_strictMono, disjoint := disjoint,
                cover := cover : OrderedFinpartition 1 }.emb
            i j =
          0),
    { length := length, partSize := partSize, partSize_pos := partSize_pos, emb := emb,
        emb_strictMono := emb_strictMono, parts_strictMono := parts_strictMono, disjoint := disjoint, cover := cover :
        OrderedFinpartition 1 } =
      default
⊢ c = default

Tactic:
rcases c with ⟨length, partSize, _, emb, _, _, _, _⟩

Premises used: OrderedFinpartition.emb, OrderedFinpartition.partSize, OrderedFinpartition.length