Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : 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 fun m ↦ emb m ⟨partSize m - 1, ⋯⟩
disjoint✝ : univ.PairwiseDisjoint fun m ↦ range (emb m)
cover✝ : ∀ (x : Fin 1), ∃ m, 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✝ }.length),
    { length := 1, partSize := partSize, partSize_pos := partSize_pos✝, emb := emb, emb_strictMono := emb_strictMono✝,
            parts_strictMono := parts_strictMono✝, disjoint := disjoint✝, cover := cover✝ }.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✝ }.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✝ }.partSize
          i)),
    { length := 1, partSize := partSize, partSize_pos := partSize_pos✝, emb := emb, emb_strictMono := emb_strictMono✝,
            parts_strictMono := parts_strictMono✝, disjoint := disjoint✝, cover := cover✝ }.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✝ } =
    default

Tactic:
obtain rfl : partSize = fun _ ↦ 1 := funext h₂

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c : OrderedFinpartition n
partSize_pos✝ : ∀ (m : Fin 1), 0 < (fun x ↦ 1) m
emb : (m : Fin 1) → Fin ((fun x ↦ 1) m) → Fin 1
emb_strictMono✝ : ∀ (m : Fin 1), StrictMono (emb m)
parts_strictMono✝ : StrictMono fun m ↦ emb m ⟨(fun x ↦ 1) m - 1, ⋯⟩
disjoint✝ : univ.PairwiseDisjoint fun m ↦ range (emb m)
cover✝ : ∀ (x : Fin 1), ∃ m, x ∈ range (emb m)
h₂ :
  ∀
    (i :
      Fin
        { length := 1, partSize := fun x ↦ 1, partSize_pos := partSize_pos✝, emb := emb,
            emb_strictMono := emb_strictMono✝, parts_strictMono := parts_strictMono✝, disjoint := disjoint✝,
            cover := cover✝ }.length),
    { length := 1, partSize := fun x ↦ 1, partSize_pos := partSize_pos✝, emb := emb, emb_strictMono := emb_strictMono✝,
            parts_strictMono := parts_strictMono✝, disjoint := disjoint✝, cover := cover✝ }.partSize
        i =
      1
h₃ :
  ∀
    (i :
      Fin
        { length := 1, partSize := fun x ↦ 1, partSize_pos := partSize_pos✝, emb := emb,
            emb_strictMono := emb_strictMono✝, parts_strictMono := parts_strictMono✝, disjoint := disjoint✝,
            cover := cover✝ }.length)
    (j :
      Fin
        ({ length := 1, partSize := fun x ↦ 1, partSize_pos := partSize_pos✝, emb := emb,
              emb_strictMono := emb_strictMono✝, parts_strictMono := parts_strictMono✝, disjoint := disjoint✝,
              cover := cover✝ }.partSize
          i)),
    { length := 1, partSize := fun x ↦ 1, partSize_pos := partSize_pos✝, emb := emb, emb_strictMono := emb_strictMono✝,
            parts_strictMono := parts_strictMono✝, disjoint := disjoint✝, cover := cover✝ }.emb
        i j =
      0
⊢ { length := 1, partSize := fun x ↦ 1, partSize_pos := partSize_pos✝, emb := emb, emb_strictMono := emb_strictMono✝,
      parts_strictMono := parts_strictMono✝, disjoint := disjoint✝, cover := cover✝ } =
    default