awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_1 : ℕ
c_1 : OrderedFinpartition n_1
n : ℕ
c : OrderedFinpartition (n + 1)
h : range (ι := Fin (c.partSize 0)) (c.emb 0) = {0}
A : c.length - 1 + 1 = c.length
h' : HEq (α := Fin (c.length - 1 + 1)) 0 (Fin.cast A 0)
⊢ cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1 (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast ⋯ i.succ)) 0 =
    c.partSize (Fin.cast A 0)

Tactic:
simp [c.partSize_eq_one_of_range_emb_eq_singleton h]

Premises used: OrderedFinpartition.partSize_eq_one_of_range_emb_eq_singleton
-- 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_1 : ℕ
c_1 : OrderedFinpartition n_1
n : ℕ
c : OrderedFinpartition (n + 1)
h : range (ι := Fin (c.partSize 0)) (c.emb 0) = {0}
A : c.length - 1 + 1 = c.length
i : Fin (c.length - 1)
h_1 :
  ∀ (h' : i.castSucc ≍ Fin.cast A i.castSucc),
    cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1 (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast ⋯ i.succ))
        i.castSucc =
      c.partSize (Fin.cast A i.castSucc)
h' : i.succ ≍ Fin.cast A i.succ
⊢ cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1 (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast ⋯ i.succ))
      i.succ =
    c.partSize (Fin.cast A i.succ)

Tactic:
simp
-- 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_1 : ℕ
c_1 : OrderedFinpartition n_1
n : ℕ
c : OrderedFinpartition (n + 1)
h : range (ι := Fin (c.partSize 0)) (c.emb 0) = {0}
A : c.length - 1 + 1 = c.length
i : Fin (c.length - 1 + 1)
h' : i ≍ Fin.cast A i
pos :
  ∀ (h' : HEq (α := Fin (c.length - 1 + 1)) 0 (Fin.cast A 0)),
    cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1 (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast ⋯ i.succ))
        0 =
      c.partSize (Fin.cast A 0)
pos₁ :
  ∀ (i : Fin (c.length - 1)),
    (∀ (h' : i.castSucc ≍ Fin.cast A i.castSucc),
        cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1
            (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast ⋯ i.succ)) i.castSucc =
          c.partSize (Fin.cast A i.castSucc)) →
      ∀ (h' : i.succ ≍ Fin.cast A i.succ),
        cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1
            (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast ⋯ i.succ)) i.succ =
          c.partSize (Fin.cast A i.succ)
⊢ cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1 (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast ⋯ i.succ)) i =
    c.partSize (Fin.cast A i)

Tactic:
induction i using Fin.induction with
          | zero => simp [c.partSize_eq_one_of_range_emb_eq_singleton h]
          | succ i => simp

Premises used: Fin.succ, OrderedFinpartition.partSize_eq_one_of_range_emb_eq_singleton
-- 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_1 : ℕ
c_1 : OrderedFinpartition n_1
n : ℕ
c : OrderedFinpartition (n + 1)
h : range (ι := Fin (c.partSize 0)) (c.emb 0) = {0}
A : c.length - 1 + 1 = c.length
h' : HEq (α := Fin (c.length - 1 + 1)) 0 (Fin.cast A 0)
j :
  Fin
    (cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1 (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast ⋯ i.succ))
      0)
pos : 0 = c.emb 0 (⟨0, ⋯⟩ : Fin (c.partSize 0))
⊢ cases (motive := fun (x : Fin (c.length - 1 + 1)) ↦
      Fin
          (cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1
            (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast ⋯ i.succ)) x) →
        Fin (n + 1))
      (fun
          (x :
            Fin
              (cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1
                (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast ⋯ i.succ)) 0)) ↦
        0)
      (fun (m : Fin (c.length - 1)) ↦
        succ ∘ fun (j : Fin (c.partSize (Fin.cast ⋯ m.succ))) ↦ (c.emb (Fin.cast ⋯ m.succ) j).pred ⋯)
      0 j =
    c.emb (Fin.cast A 0) (⟨(↑j : ℕ), ⋯⟩ : Fin (c.partSize (Fin.cast A 0)))

Tactic:
simp only [cases_zero, cast_zero, val_eq_zero]

Premises used: Fin.cases_zero, Fin.val_eq_zero, Fin.cast_zero
-- 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_1 : ℕ
c_1 : OrderedFinpartition n_1
n : ℕ
c : OrderedFinpartition (n + 1)
h : range (ι := Fin (c.partSize 0)) (c.emb 0) = {0}
A : c.length - 1 + 1 = c.length
h' : HEq (α := Fin (c.length - 1 + 1)) 0 (Fin.cast A 0)
j :
  Fin
    (cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1 (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast ⋯ i.succ))
      0)
⊢ 0 = c.emb 0 (⟨0, ⋯⟩ : Fin (c.partSize 0))

Tactic:
(apply_eq_of_range_eq_singleton h _).symm

Premises used: Eq.symm, Function.apply_eq_of_range_eq_singleton
-- 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_1 : ℕ
c_1 : OrderedFinpartition n_1
n : ℕ
c : OrderedFinpartition (n + 1)
h : range (ι := Fin (c.partSize 0)) (c.emb 0) = {0}
A : c.length - 1 + 1 = c.length
h' : HEq (α := Fin (c.length - 1 + 1)) 0 (Fin.cast A 0)
j :
  Fin
    (cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1 (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast ⋯ i.succ))
      0)
⊢ 0 = c.emb 0 (⟨0, ⋯⟩ : Fin (c.partSize 0))

Tactic:
exact (apply_eq_of_range_eq_singleton h _).symm

Premises used: Eq.symm, Function.apply_eq_of_range_eq_singleton
-- 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_1 : ℕ
c_1 : OrderedFinpartition n_1
n : ℕ
c : OrderedFinpartition (n + 1)
h : range (ι := Fin (c.partSize 0)) (c.emb 0) = {0}
A : c.length - 1 + 1 = c.length
i : Fin (c.length - 1)
h_1 :
  ∀ (h' : i.castSucc ≍ Fin.cast A i.castSucc)
    (j :
      Fin
        (cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1
          (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast ⋯ i.succ)) i.castSucc)),
    cases (motive := fun (x : Fin (c.length - 1 + 1)) ↦
        Fin
            (cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1
              (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast ⋯ i.succ)) x) →
          Fin (n + 1))
        (fun
            (x :
              Fin
                (cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1
                  (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast ⋯ i.succ)) 0)) ↦
          0)
        (fun (m : Fin (c.length - 1)) ↦
          succ ∘ fun (j : Fin (c.partSize (Fin.cast ⋯ m.succ))) ↦ (c.emb (Fin.cast ⋯ m.succ) j).pred ⋯)
        i.castSucc j =
      c.emb (Fin.cast A i.castSucc) (⟨(↑j : ℕ), ⋯⟩ : Fin (c.partSize (Fin.cast A i.castSucc)))
h' : i.succ ≍ Fin.cast A i.succ
j :
  Fin
    (cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1 (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast ⋯ i.succ))
      i.succ)
⊢ cases (motive := fun (x : Fin (c.length - 1 + 1)) ↦
      Fin
          (cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1
            (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast ⋯ i.succ)) x) →
        Fin (n + 1))
      (fun
          (x :
            Fin
              (cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1
                (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast ⋯ i.succ)) 0)) ↦
        0)
      (fun (m : Fin (c.length - 1)) ↦
        succ ∘ fun (j : Fin (c.partSize (Fin.cast ⋯ m.succ))) ↦ (c.emb (Fin.cast ⋯ m.succ) j).pred ⋯)
      i.succ j =
    c.emb (Fin.cast A i.succ) (⟨(↑j : ℕ), ⋯⟩ : Fin (c.partSize (Fin.cast A i.succ)))

Tactic:
simp
-- 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_1 : ℕ
c_1 : OrderedFinpartition n_1
n : ℕ
c : OrderedFinpartition (n + 1)
h : ¬range (ι := Fin (c.partSize 0)) (c.emb 0) = {0}
neg :
  (Sigma.fst (β := fun (c : OrderedFinpartition n) ↦ Option (Fin c.length))
          (Sigma.mk (β := fun (c : OrderedFinpartition n) ↦ Option (Fin c.length)) (c.eraseMiddle h)
            (some (c.index 0)))).extend
      (Sigma.snd (β := fun (c : OrderedFinpartition n) ↦ Option (Fin c.length))
        (Sigma.mk (β := fun (c : OrderedFinpartition n) ↦ Option (Fin c.length)) (c.eraseMiddle h)
          (some (c.index 0)))) =
    c
⊢ extend
      (Sigma.fst (β := fun (c : OrderedFinpartition n) ↦ Option (Fin c.length))
        (if h : range (ι := Fin (c.partSize 0)) (c.emb 0) = {0} then
          Sigma.mk (β := fun (c : OrderedFinpartition n) ↦ Option (Fin c.length)) (c.eraseLeft h) none
        else
          Sigma.mk (β := fun (c : OrderedFinpartition n) ↦ Option (Fin c.length)) (c.eraseMiddle h) (some (c.index 0))))
      (Sigma.snd (β := fun (c : OrderedFinpartition n) ↦ Option (Fin c.length))
        (if h : range (ι := Fin (c.partSize 0)) (c.emb 0) = {0} then
          Sigma.mk (β := fun (c : OrderedFinpartition n) ↦ Option (Fin c.length)) (c.eraseLeft h) none
        else
          Sigma.mk (β := fun (c : OrderedFinpartition n) ↦ Option (Fin c.length)) (c.eraseMiddle h)
            (some (c.index 0)))) =
    c

Tactic:
rw [dif_neg h]

Premises used: dif_neg
-- 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_1 : ℕ
c_1 : OrderedFinpartition n_1
n : ℕ
c : OrderedFinpartition (n + 1)
h : ¬range (ι := Fin (c.partSize 0)) (c.emb 0) = {0}
⊢ c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)

Tactic:
have B : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0) :=
        Nat.sub_add_cancel (c.partSize_pos (c.index 0))
-- 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_1 : ℕ
c_1 : OrderedFinpartition n_1
n : ℕ
c : OrderedFinpartition (n + 1)
h : ¬range (ι := Fin (c.partSize 0)) (c.emb 0) = {0}
B : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)
neg :
  { length := c.length,
      partSize :=
        update (β := fun (a : Fin c.length) ↦ ℕ)
          (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)) (c.index 0)
          (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0) +
            1),
      partSize_pos := ⋯,
      emb := fun (m : Fin c.length) ↦
        if h_1 : m = c.index 0 then
          (fun
                (i :
                  Fin
                    (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                        (c.index 0) +
                      1)) ↦
              cases (motive :=
                fun
                  (x :
                    Fin
                      (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                          (c.index 0) +
                        1)) ↦
                Fin (n + 1)) 0
                (succ ∘
                  fun
                    (j :
                      Fin
                        (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                          (c.index 0))) ↦
                  (c.emb (c.index 0) (Fin.cast ⋯ j.succ)).pred ⋯)
                i) ∘
            Fin.cast ⋯
        else
          succ ∘
            (fun
                  (j :
                    Fin
                      (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                        m)) ↦
                if h : m = c.index 0 then (c.emb m (Fin.cast ⋯ j.succ)).pred ⋯ else (c.emb m (Fin.cast ⋯ j)).pred ⋯) ∘
              Fin.cast ⋯,
      emb_strictMono := ⋯, parts_strictMono := ⋯, disjoint := ⋯, cover := ⋯ : OrderedFinpartition (n + 1) } =
    c
⊢ (Sigma.fst (β := fun (c : OrderedFinpartition n) ↦ Option (Fin c.length))
          (Sigma.mk (β := fun (c : OrderedFinpartition n) ↦ Option (Fin c.length)) (c.eraseMiddle h)
            (some (c.index 0)))).extend
      (Sigma.snd (β := fun (c : OrderedFinpartition n) ↦ Option (Fin c.length))
        (Sigma.mk (β := fun (c : OrderedFinpartition n) ↦ Option (Fin c.length)) (c.eraseMiddle h)
          (some (c.index 0)))) =
    c

Tactic:
simp only [extend, extendMiddle, eraseMiddle, ↓reduceDIte]

Premises used: reduceDIte, OrderedFinpartition.eraseMiddle, OrderedFinpartition.extend, OrderedFinpartition.extendMiddle
-- 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_1 : ℕ
c_1 : OrderedFinpartition n_1
n : ℕ
c : OrderedFinpartition (n + 1)
h : ¬range (ι := Fin (c.partSize 0)) (c.emb 0) = {0}
B : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)
⊢ { length := c.length,
        partSize :=
          update (β := fun (a : Fin c.length) ↦ ℕ)
            (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)) (c.index 0)
            (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0) +
              1),
        partSize_pos := ⋯,
        emb := fun (m : Fin c.length) ↦
          if h_1 : m = c.index 0 then
            (fun
                  (i :
                    Fin
                      (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                          (c.index 0) +
                        1)) ↦
                cases (motive :=
                  fun
                    (x :
                      Fin
                        (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                            (c.index 0) +
                          1)) ↦
                  Fin (n + 1)) 0
                  (succ ∘
                    fun
                      (j :
                        Fin
                          (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                            (c.index 0))) ↦
                    (c.emb (c.index 0) (Fin.cast ⋯ j.succ)).pred ⋯)
                  i) ∘
              Fin.cast ⋯
          else
            succ ∘
              (fun
                    (j :
                      Fin
                        (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                          m)) ↦
                  if h : m = c.index 0 then (c.emb m (Fin.cast ⋯ j.succ)).pred ⋯ else (c.emb m (Fin.cast ⋯ j)).pred ⋯) ∘
                Fin.cast ⋯,
        emb_strictMono := ⋯, parts_strictMono := ⋯, disjoint := ⋯, cover := ⋯ : OrderedFinpartition (n + 1) }.length =
    c.length

Tactic:
rfl
-- 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_1 : ℕ
c_1 : OrderedFinpartition n_1
n : ℕ
c : OrderedFinpartition (n + 1)
h : ¬range (ι := Fin (c.partSize 0)) (c.emb 0) = {0}
B : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)
⊢ { length := c.length,
        partSize :=
          update (β := fun (a : Fin c.length) ↦ ℕ)
            (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)) (c.index 0)
            (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0) +
              1),
        partSize_pos := ⋯,
        emb := fun (m : Fin c.length) ↦
          if h_1 : m = c.index 0 then
            (fun
                  (i :
                    Fin
                      (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                          (c.index 0) +
                        1)) ↦
                cases (motive :=
                  fun
                    (x :
                      Fin
                        (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                            (c.index 0) +
                          1)) ↦
                  Fin (n + 1)) 0
                  (succ ∘
                    fun
                      (j :
                        Fin
                          (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                            (c.index 0))) ↦
                    (c.emb (c.index 0) (Fin.cast ⋯ j.succ)).pred ⋯)
                  i) ∘
              Fin.cast ⋯
          else
            succ ∘
              (fun
                    (j :
                      Fin
                        (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                          m)) ↦
                  if h : m = c.index 0 then (c.emb m (Fin.cast ⋯ j.succ)).pred ⋯ else (c.emb m (Fin.cast ⋯ j)).pred ⋯) ∘
                Fin.cast ⋯,
        emb_strictMono := ⋯, parts_strictMono := ⋯, disjoint := ⋯, cover := ⋯ : OrderedFinpartition (n + 1) }.partSize ≍
    c.partSize

Tactic:
simp only [update_self, update_idem, heq_eq_eq, update_eq_self_iff, B]

Premises used: heq_eq_eq, Function.update_idem, Function.update_eq_self_iff, Function.update_self
-- 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_1 : ℕ
c_1 : OrderedFinpartition n_1
n : ℕ
c : OrderedFinpartition (n + 1)
h : ¬range (ι := Fin (c.partSize 0)) (c.emb 0) = {0}
B : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)
⊢ { length := c.length,
        partSize :=
          update (β := fun (a : Fin c.length) ↦ ℕ)
            (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)) (c.index 0)
            (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0) +
              1),
        partSize_pos := ⋯,
        emb := fun (m : Fin c.length) ↦
          if h_1 : m = c.index 0 then
            (fun
                  (i :
                    Fin
                      (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                          (c.index 0) +
                        1)) ↦
                cases (motive :=
                  fun
                    (x :
                      Fin
                        (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                            (c.index 0) +
                          1)) ↦
                  Fin (n + 1)) 0
                  (succ ∘
                    fun
                      (j :
                        Fin
                          (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                            (c.index 0))) ↦
                    (c.emb (c.index 0) (Fin.cast ⋯ j.succ)).pred ⋯)
                  i) ∘
              Fin.cast ⋯
          else
            succ ∘
              (fun
                    (j :
                      Fin
                        (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                          m)) ↦
                  if h : m = c.index 0 then (c.emb m (Fin.cast ⋯ j.succ)).pred ⋯ else (c.emb m (Fin.cast ⋯ j)).pred ⋯) ∘
                Fin.cast ⋯,
        emb_strictMono := ⋯, parts_strictMono := ⋯, disjoint := ⋯, cover := ⋯ : OrderedFinpartition (n + 1) }.emb ≍
    c.emb

Tactic:
hfunext rfl ?_

Premises used: Function.hfunext, rfl