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
o : Option (Fin c.length)
i a : Fin c.length
emb :
  HEq (c.emb a) (β :=
    Fin
        (update (β := fun (a : Fin (c.extendMiddle a).length) ↦ ℕ) (c.extendMiddle a).partSize
          ((c.extendMiddle a).index 0) ((c.extendMiddle a).partSize ((c.extendMiddle a).index 0) - 1) a) →
      Fin n)
    fun
      (j :
        Fin
          (update (β := fun (a : Fin (c.extendMiddle a).length) ↦ ℕ) (c.extendMiddle a).partSize
            ((c.extendMiddle a).index 0) ((c.extendMiddle a).partSize ((c.extendMiddle a).index 0) - 1) a)) ↦
    if h : a = a then ((c.extendMiddle a).emb a (Fin.cast ⋯ j.succ)).pred ⋯
    else ((c.extendMiddle a).emb a (Fin.cast ⋯ j)).pred ⋯
emb₁ :
  ∀ (hij : a ≠ i),
    HEq (c.emb a) (β :=
      Fin
          (update (β := fun (a : Fin (c.extendMiddle i).length) ↦ ℕ) (c.extendMiddle i).partSize
            ((c.extendMiddle i).index 0) ((c.extendMiddle i).partSize ((c.extendMiddle i).index 0) - 1) a) →
        Fin n)
      fun
        (j :
          Fin
            (update (β := fun (a : Fin (c.extendMiddle i).length) ↦ ℕ) (c.extendMiddle i).partSize
              ((c.extendMiddle i).index 0) ((c.extendMiddle i).partSize ((c.extendMiddle i).index 0) - 1) a)) ↦
      if h : a = i then ((c.extendMiddle i).emb a (Fin.cast ⋯ j.succ)).pred ⋯
      else ((c.extendMiddle i).emb a (Fin.cast ⋯ j)).pred ⋯
⊢ HEq (c.emb a) (β :=
    Fin
        (update (β := fun (a : Fin (c.extendMiddle i).length) ↦ ℕ) (c.extendMiddle i).partSize
          ((c.extendMiddle i).index 0) ((c.extendMiddle i).partSize ((c.extendMiddle i).index 0) - 1) a) →
      Fin n)
    fun
      (j :
        Fin
          (update (β := fun (a : Fin (c.extendMiddle i).length) ↦ ℕ) (c.extendMiddle i).partSize
            ((c.extendMiddle i).index 0) ((c.extendMiddle i).partSize ((c.extendMiddle i).index 0) - 1) a)) ↦
    if h : a = i then ((c.extendMiddle i).emb a (Fin.cast ⋯ j.succ)).pred ⋯
    else ((c.extendMiddle i).emb a (Fin.cast ⋯ j)).pred ⋯

Tactic:
rcases eq_or_ne a i with rfl | hij

Premises used: eq_or_ne, 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
o : Option (Fin c.length)
a : Fin c.length
⊢ HEq (c.emb a) (β :=
    Fin
        (update (β := fun (a : Fin (c.extendMiddle a).length) ↦ ℕ) (c.extendMiddle a).partSize
          ((c.extendMiddle a).index 0) ((c.extendMiddle a).partSize ((c.extendMiddle a).index 0) - 1) a) →
      Fin n)
    fun
      (j :
        Fin
          (update (β := fun (a : Fin (c.extendMiddle a).length) ↦ ℕ) (c.extendMiddle a).partSize
            ((c.extendMiddle a).index 0) ((c.extendMiddle a).partSize ((c.extendMiddle a).index 0) - 1) a)) ↦
    if h : a = a then ((c.extendMiddle a).emb a (Fin.cast ⋯ j.succ)).pred ⋯
    else ((c.extendMiddle a).emb a (Fin.cast ⋯ j)).pred ⋯

Tactic:
(Fin.heq_fun_iff ?_).mpr ?_

Premises used: Iff.mpr, Fin.heq_fun_iff
-- 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
o : Option (Fin c.length)
a : Fin c.length
emb :
  c.partSize a =
    update (β := fun (a : Fin (c.extendMiddle a).length) ↦ ℕ) (c.extendMiddle a).partSize ((c.extendMiddle a).index 0)
      ((c.extendMiddle a).partSize ((c.extendMiddle a).index 0) - 1) a
emb₁ :
  ∀ (i : Fin (c.partSize a)),
    c.emb a i =
      if h : a = a then
        ((c.extendMiddle a).emb a
              (Fin.cast ⋯
                (succ
                  (⟨(↑i : ℕ), ⋯⟩ :
                    Fin
                      (update (β := fun (a : Fin (c.extendMiddle a).length) ↦ ℕ) (c.extendMiddle a).partSize
                        ((c.extendMiddle a).index 0) ((c.extendMiddle a).partSize ((c.extendMiddle a).index 0) - 1)
                        a))))).pred
          ⋯
      else
        ((c.extendMiddle a).emb a
              (Fin.cast ⋯
                (⟨(↑i : ℕ), ⋯⟩ :
                  Fin
                    (update (β := fun (a : Fin (c.extendMiddle a).length) ↦ ℕ) (c.extendMiddle a).partSize
                      ((c.extendMiddle a).index 0) ((c.extendMiddle a).partSize ((c.extendMiddle a).index 0) - 1)
                      a)))).pred
          ⋯
⊢ HEq (c.emb a) (β :=
    Fin
        (update (β := fun (a : Fin (c.extendMiddle a).length) ↦ ℕ) (c.extendMiddle a).partSize
          ((c.extendMiddle a).index 0) ((c.extendMiddle a).partSize ((c.extendMiddle a).index 0) - 1) a) →
      Fin n)
    fun
      (j :
        Fin
          (update (β := fun (a : Fin (c.extendMiddle a).length) ↦ ℕ) (c.extendMiddle a).partSize
            ((c.extendMiddle a).index 0) ((c.extendMiddle a).partSize ((c.extendMiddle a).index 0) - 1) a)) ↦
    if h : a = a then ((c.extendMiddle a).emb a (Fin.cast ⋯ j.succ)).pred ⋯
    else ((c.extendMiddle a).emb a (Fin.cast ⋯ j)).pred ⋯

Tactic:
refine (Fin.heq_fun_iff ?_).mpr ?_

Premises used: Iff.mpr, Fin.heq_fun_iff
-- 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
o : Option (Fin c.length)
a : Fin c.length
emb :
  c.partSize a =
    update (β := fun (a : Fin (c.extendMiddle a).length) ↦ ℕ) (c.extendMiddle a).partSize a
      ((c.extendMiddle a).partSize a - 1) a
⊢ c.partSize a =
    update (β := fun (a : Fin (c.extendMiddle a).length) ↦ ℕ) (c.extendMiddle a).partSize ((c.extendMiddle a).index 0)
      ((c.extendMiddle a).partSize ((c.extendMiddle a).index 0) - 1) a

Tactic:
rw [index_extendMiddle_zero]

Premises used: OrderedFinpartition.index_extendMiddle_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
o : Option (Fin c.length)
a : Fin c.length
⊢ c.partSize a =
    update (β := fun (a : Fin (c.extendMiddle a).length) ↦ ℕ) (c.extendMiddle a).partSize a
      ((c.extendMiddle a).partSize a - 1) a

Tactic:
simp [extendMiddle]

Premises used: 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
o : Option (Fin c.length)
a : Fin c.length
⊢ ∀ (i : Fin (c.partSize a)),
    c.emb a i =
      if h : a = a then
        ((c.extendMiddle a).emb a
              (Fin.cast ⋯
                (succ
                  (⟨(↑i : ℕ), ⋯⟩ :
                    Fin
                      (update (β := fun (a : Fin (c.extendMiddle a).length) ↦ ℕ) (c.extendMiddle a).partSize
                        ((c.extendMiddle a).index 0) ((c.extendMiddle a).partSize ((c.extendMiddle a).index 0) - 1)
                        a))))).pred
          ⋯
      else
        ((c.extendMiddle a).emb a
              (Fin.cast ⋯
                (⟨(↑i : ℕ), ⋯⟩ :
                  Fin
                    (update (β := fun (a : Fin (c.extendMiddle a).length) ↦ ℕ) (c.extendMiddle a).partSize
                      ((c.extendMiddle a).index 0) ((c.extendMiddle a).partSize ((c.extendMiddle a).index 0) - 1)
                      a)))).pred
          ⋯

Tactic:
simp [extendMiddle]

Premises used: 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
o : Option (Fin c.length)
i a : Fin c.length
hij : a ≠ i
⊢ HEq (c.emb a) (β :=
    Fin
        (update (β := fun (a : Fin (c.extendMiddle i).length) ↦ ℕ) (c.extendMiddle i).partSize
          ((c.extendMiddle i).index 0) ((c.extendMiddle i).partSize ((c.extendMiddle i).index 0) - 1) a) →
      Fin n)
    fun
      (j :
        Fin
          (update (β := fun (a : Fin (c.extendMiddle i).length) ↦ ℕ) (c.extendMiddle i).partSize
            ((c.extendMiddle i).index 0) ((c.extendMiddle i).partSize ((c.extendMiddle i).index 0) - 1) a)) ↦
    if h : a = i then ((c.extendMiddle i).emb a (Fin.cast ⋯ j.succ)).pred ⋯
    else ((c.extendMiddle i).emb a (Fin.cast ⋯ j)).pred ⋯

Tactic:
(Fin.heq_fun_iff ?_).mpr ?_

Premises used: Iff.mpr, Fin.heq_fun_iff
-- 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
o : Option (Fin c.length)
i a : Fin c.length
hij : a ≠ i
emb :
  c.partSize a =
    update (β := fun (a : Fin (c.extendMiddle i).length) ↦ ℕ) (c.extendMiddle i).partSize ((c.extendMiddle i).index 0)
      ((c.extendMiddle i).partSize ((c.extendMiddle i).index 0) - 1) a
emb₁ :
  ∀ (i_1 : Fin (c.partSize a)),
    c.emb a i_1 =
      if h : a = i then
        ((c.extendMiddle i).emb a
              (Fin.cast ⋯
                (succ
                  (⟨(↑i_1 : ℕ), ⋯⟩ :
                    Fin
                      (update (β := fun (a : Fin (c.extendMiddle i).length) ↦ ℕ) (c.extendMiddle i).partSize
                        ((c.extendMiddle i).index 0) ((c.extendMiddle i).partSize ((c.extendMiddle i).index 0) - 1)
                        a))))).pred
          ⋯
      else
        ((c.extendMiddle i).emb a
              (Fin.cast ⋯
                (⟨(↑i_1 : ℕ), ⋯⟩ :
                  Fin
                    (update (β := fun (a : Fin (c.extendMiddle i).length) ↦ ℕ) (c.extendMiddle i).partSize
                      ((c.extendMiddle i).index 0) ((c.extendMiddle i).partSize ((c.extendMiddle i).index 0) - 1)
                      a)))).pred
          ⋯
⊢ HEq (c.emb a) (β :=
    Fin
        (update (β := fun (a : Fin (c.extendMiddle i).length) ↦ ℕ) (c.extendMiddle i).partSize
          ((c.extendMiddle i).index 0) ((c.extendMiddle i).partSize ((c.extendMiddle i).index 0) - 1) a) →
      Fin n)
    fun
      (j :
        Fin
          (update (β := fun (a : Fin (c.extendMiddle i).length) ↦ ℕ) (c.extendMiddle i).partSize
            ((c.extendMiddle i).index 0) ((c.extendMiddle i).partSize ((c.extendMiddle i).index 0) - 1) a)) ↦
    if h : a = i then ((c.extendMiddle i).emb a (Fin.cast ⋯ j.succ)).pred ⋯
    else ((c.extendMiddle i).emb a (Fin.cast ⋯ j)).pred ⋯

Tactic:
refine (Fin.heq_fun_iff ?_).mpr ?_

Premises used: Iff.mpr, Fin.heq_fun_iff
-- 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
o : Option (Fin c.length)
i a : Fin c.length
hij : a ≠ i
emb :
  c.partSize a =
    update (β := fun (a : Fin (c.extendMiddle i).length) ↦ ℕ) (c.extendMiddle i).partSize i
      ((c.extendMiddle i).partSize i - 1) a
⊢ c.partSize a =
    update (β := fun (a : Fin (c.extendMiddle i).length) ↦ ℕ) (c.extendMiddle i).partSize ((c.extendMiddle i).index 0)
      ((c.extendMiddle i).partSize ((c.extendMiddle i).index 0) - 1) a

Tactic:
rw [index_extendMiddle_zero]

Premises used: OrderedFinpartition.index_extendMiddle_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
o : Option (Fin c.length)
i a : Fin c.length
hij : a ≠ i
⊢ c.partSize a =
    update (β := fun (a : Fin (c.extendMiddle i).length) ↦ ℕ) (c.extendMiddle i).partSize i
      ((c.extendMiddle i).partSize i - 1) a

Tactic:
simp [extendMiddle]

Premises used: 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
o : Option (Fin c.length)
i a : Fin c.length
hij : a ≠ i
⊢ ∀ (i_1 : Fin (c.partSize a)),
    c.emb a i_1 =
      if h : a = i then
        ((c.extendMiddle i).emb a
              (Fin.cast ⋯
                (succ
                  (⟨(↑i_1 : ℕ), ⋯⟩ :
                    Fin
                      (update (β := fun (a : Fin (c.extendMiddle i).length) ↦ ℕ) (c.extendMiddle i).partSize
                        ((c.extendMiddle i).index 0) ((c.extendMiddle i).partSize ((c.extendMiddle i).index 0) - 1)
                        a))))).pred
          ⋯
      else
        ((c.extendMiddle i).emb a
              (Fin.cast ⋯
                (⟨(↑i_1 : ℕ), ⋯⟩ :
                  Fin
                    (update (β := fun (a : Fin (c.extendMiddle i).length) ↦ ℕ) (c.extendMiddle i).partSize
                      ((c.extendMiddle i).index 0) ((c.extendMiddle i).partSize ((c.extendMiddle i).index 0) - 1)
                      a)))).pred
          ⋯

Tactic:
simp [extendMiddle, hij]

Premises used: 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
o : Option (Fin c.length)
⊢ Eq (α := (c : OrderedFinpartition n) × Option (Fin c.length))
    ((fun (c : OrderedFinpartition (n + 1)) ↦
        (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 : OrderedFinpartition n) × Option (Fin c.length)))
      ((fun (c : (c : OrderedFinpartition n) × Option (Fin c.length)) ↦
          c.fst (β := fun (c : OrderedFinpartition n) ↦ Option (Fin c.length)).extend
            (c.snd (β := fun (c : OrderedFinpartition n) ↦ Option (Fin c.length))))
        (Sigma.mk (β := fun (c : OrderedFinpartition n) ↦ Option (Fin c.length)) c o)))
    (Sigma.mk (β := fun (c : OrderedFinpartition n) ↦ Option (Fin c.length)) c o)

Tactic:
match o with
    | none =>
      simp only [extend, range_extendLeft_zero, ↓reduceDIte, Sigma.mk.inj_iff, heq_eq_eq,
        and_true]
      rfl
    | some i =>
      simp only [extend, range_emb_extendMiddle_ne_singleton_zero, ↓reduceDIte,
        Sigma.mk.inj_iff, heq_eq_eq, and_true, eraseMiddle,
        index_extendMiddle_zero]
      ext
      · rfl
      · simp only [heq_eq_eq, index_extendMiddle_zero]
        ext j
        rcases eq_or_ne i j with rfl | hij
        · simp [extendMiddle]
        · simp [hij.symm, extendMiddle]
      · refine HEq.symm (hfunext rfl ?_)
        simp only [heq_eq_eq, forall_eq']
        intro a
        rcases eq_or_ne a i with rfl | hij
        · refine (Fin.heq_fun_iff ?_).mpr ?_
          · rw [index_extendMiddle_zero]
            simp [extendMiddle]
          · simp [extendMiddle]
        · refine (Fin.heq_fun_iff ?_).mpr ?_
          · rw [index_extendMiddle_zero]
            simp [extendMiddle]
          · simp [extendMiddle, hij]
-- 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)
pos :
  ∀ (h : range (ι := Fin (c.partSize 0)) (c.emb 0) = {0}),
    (fun (c : (c : OrderedFinpartition n) × Option (Fin c.length)) ↦
          c.fst (β := fun (c : OrderedFinpartition n) ↦ Option (Fin c.length)).extend
            (c.snd (β := fun (c : OrderedFinpartition n) ↦ Option (Fin c.length))))
        ((fun (c : OrderedFinpartition (n + 1)) ↦
            (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 : OrderedFinpartition n) × Option (Fin c.length)))
          c) =
      c
neg :
  ∀ (h : ¬range (ι := Fin (c.partSize 0)) (c.emb 0) = {0}),
    (fun (c : (c : OrderedFinpartition n) × Option (Fin c.length)) ↦
          c.fst (β := fun (c : OrderedFinpartition n) ↦ Option (Fin c.length)).extend
            (c.snd (β := fun (c : OrderedFinpartition n) ↦ Option (Fin c.length))))
        ((fun (c : OrderedFinpartition (n + 1)) ↦
            (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 : OrderedFinpartition n) × Option (Fin c.length)))
          c) =
      c
⊢ (fun (c : (c : OrderedFinpartition n) × Option (Fin c.length)) ↦
        c.fst (β := fun (c : OrderedFinpartition n) ↦ Option (Fin c.length)).extend
          (c.snd (β := fun (c : OrderedFinpartition n) ↦ Option (Fin c.length))))
      ((fun (c : OrderedFinpartition (n + 1)) ↦
          (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 : OrderedFinpartition n) × Option (Fin c.length)))
        c) =
    c

Tactic:
by_cases h : range (c.emb 0) = {0}

Premises used: OrderedFinpartition.emb, Set.range, OfNat.ofNat
-- 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.length - 1 + 1 = c.length

Tactic:
have A : c.length - 1 + 1 = c.length := Nat.sub_add_cancel (c.length_pos (Nat.zero_lt_succ n))
-- 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
pos :
  (Sigma.fst (β := fun (c : OrderedFinpartition n) ↦ Option (Fin c.length))
          (Sigma.mk (β := fun (c : OrderedFinpartition n) ↦ Option (Fin c.length)) (c.eraseLeft h) none)).extend
      (Sigma.snd (β := fun (c : OrderedFinpartition n) ↦ Option (Fin c.length))
        (Sigma.mk (β := fun (c : OrderedFinpartition n) ↦ Option (Fin c.length)) (c.eraseLeft h) none)) =
    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_pos h]

Premises used: dif_pos