-- 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 : OrderedFinpartition n
partSize : Fin 1 → ℕ
partSize_pos : ∀ (m : Fin 1), 0 < partSize m
emb : (m : Fin 1) → Fin (partSize m) → Fin 1
emb_strictMono : ∀ (m : Fin 1), StrictMono (emb m)
parts_strictMono : StrictMono (β := Fin 1) fun (m : Fin 1) ↦ emb m (⟨partSize m - 1, ⋯⟩ : Fin (partSize m))
disjoint : PairwiseDisjoint (α := Set (Fin 1)) univ fun (m : Fin 1) ↦ range (emb m)
cover : ∀ (x : Fin 1), ∃ (m : Fin 1), x ∈ range (emb m)
h₂ :
  ∀
    (i :
      Fin
        { length := 1, partSize := partSize, partSize_pos := partSize_pos, emb := emb, emb_strictMono := emb_strictMono,
            parts_strictMono := parts_strictMono, disjoint := disjoint, cover := cover :
            OrderedFinpartition 1 }.length),
    { length := 1, 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 := 1, 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 := 1, 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 := 1, 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 := 1, partSize := partSize, partSize_pos := partSize_pos, emb := emb, emb_strictMono := emb_strictMono,
      parts_strictMono := parts_strictMono, disjoint := disjoint, cover := cover : OrderedFinpartition 1 } =
    default
have obtain : ∀ (partSize_pos : ∀ (m : Fin 1), LT.lt (α := ℕ) 0 ((fun (x : Fin 1) ↦ (1 : ℕ)) m))
  (emb : (m : Fin 1) → Fin ((fun (x : Fin 1) ↦ (1 : ℕ)) m) → Fin 1) (emb_strictMono : ∀ (m : Fin 1), StrictMono (emb m))
  (parts_strictMono :
    StrictMono (β := Fin 1) fun (m : Fin 1) ↦
      emb m (⟨HSub.hSub (α := ℕ) ((fun (x : Fin 1) ↦ (1 : ℕ)) m) 1, sorry⟩ : Fin ((fun (x : Fin 1) ↦ (1 : ℕ)) m)))
  (disjoint : PairwiseDisjoint (α := Set (Fin 1)) univ fun (m : Fin 1) ↦ range (emb m))
  (cover : ∀ (x : Fin 1), ∃ (m : Fin 1), x ∈ range (emb m))
  (h₂ :
    ∀
      (i :
        Fin
          { length := 1, partSize := fun (x : Fin 1) ↦ 1, partSize_pos := partSize_pos, emb := emb,
              emb_strictMono := emb_strictMono, parts_strictMono := parts_strictMono, disjoint := disjoint,
              cover := cover : OrderedFinpartition 1 }.length),
      { length := 1, partSize := fun (x : Fin 1) ↦ 1, 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 := 1, partSize := fun (x : Fin 1) ↦ 1, partSize_pos := partSize_pos, emb := emb,
              emb_strictMono := emb_strictMono, parts_strictMono := parts_strictMono, disjoint := disjoint,
              cover := cover : OrderedFinpartition 1 }.length)
      (j :
        Fin
          ({ length := 1, partSize := fun (x : Fin 1) ↦ 1, partSize_pos := partSize_pos, emb := emb,
                emb_strictMono := emb_strictMono, parts_strictMono := parts_strictMono, disjoint := disjoint,
                cover := cover : OrderedFinpartition 1 }.partSize
            i)),
      { length := 1, partSize := fun (x : Fin 1) ↦ 1, 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 := 1, partSize := fun (x : Fin 1) ↦ 1, partSize_pos := partSize_pos, emb := emb,
      emb_strictMono := emb_strictMono, parts_strictMono := parts_strictMono, disjoint := disjoint, cover := cover :
      OrderedFinpartition 1 } =
    default
Tactic: obtain rfl : partSize = fun _ ↦ 1 := funext h₂
Cleared hypotheses: partSize, partSize_pos, emb, emb_strictMono, parts_strictMono, disjoint, cover, h₂, h₃