awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_1 : ℕ
c_1 : OrderedFinpartition n_1
n : ℕ
c : OrderedFinpartition n
o : Option (Fin c.length)
i a : Fin c.length
⊢ 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 ⋯
have 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 sorry j.succ)).pred sorry
  else ((c.extendMiddle a).emb a (Fin.cast sorry j)).pred sorry
Tactic: rcases eq_or_ne a i with rfl | hij
Cleared hypotheses: i
-- 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_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 ⋯
⊢ 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 ⋯
have 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 sorry j.succ)).pred sorry
    else ((c.extendMiddle i).emb a (Fin.cast sorry j)).pred sorry
Tactic: rcases eq_or_ne a i with rfl | hij
-- 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_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 ⋯
have 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
Tactic: refine (Fin.heq_fun_iff ?_).mpr ?_
-- 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_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
⊢ 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 ⋯
have emb₁ : ∀ (i : Fin (c.partSize a)),
  c.emb a i =
    if h : a = a then
      ((c.extendMiddle a).emb a
            (Fin.cast sorry
              (succ
                (⟨(↑i : ℕ), sorry⟩ :
                  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
        sorry
    else
      ((c.extendMiddle a).emb a
            (Fin.cast sorry
              (⟨(↑i : ℕ), sorry⟩ :
                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
        sorry
Tactic: refine (Fin.heq_fun_iff ?_).mpr ?_
-- 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_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 ((c.extendMiddle a).index 0)
      ((c.extendMiddle a).partSize ((c.extendMiddle a).index 0) - 1) a
have emb : c.partSize a =
  update (β := fun (a : Fin (c.extendMiddle a).length) ↦ ℕ) (c.extendMiddle a).partSize a
    ((c.extendMiddle a).partSize a - 1) a
Tactic: rw [index_extendMiddle_zero]
-- 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_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 ⋯
have 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
Tactic: refine (Fin.heq_fun_iff ?_).mpr ?_
-- 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_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
⊢ 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 ⋯
have emb₁ : ∀ (i_1 : Fin (c.partSize a)),
  c.emb a i_1 =
    if h : a = i then
      ((c.extendMiddle i).emb a
            (Fin.cast sorry
              (succ
                (⟨(↑i_1 : ℕ), sorry⟩ :
                  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
        sorry
    else
      ((c.extendMiddle i).emb a
            (Fin.cast sorry
              (⟨(↑i_1 : ℕ), sorry⟩ :
                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
        sorry
Tactic: refine (Fin.heq_fun_iff ?_).mpr ?_
-- 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_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 ((c.extendMiddle i).index 0)
      ((c.extendMiddle i).partSize ((c.extendMiddle i).index 0) - 1) a
have emb : c.partSize a =
  update (β := fun (a : Fin (c.extendMiddle i).length) ↦ ℕ) (c.extendMiddle i).partSize i
    ((c.extendMiddle i).partSize i - 1) a
Tactic: rw [index_extendMiddle_zero]
-- 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_1 : ℕ
c_1 : OrderedFinpartition n_1
n : ℕ
c : OrderedFinpartition (n + 1)
⊢ (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
have 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
Tactic: by_cases h : range (c.emb 0) = {0}
-- 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_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
⊢ (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
have 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
Tactic: by_cases h : range (c.emb 0) = {0}
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (hypothesis)
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}
⊢ (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
have A : 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))
-- 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_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
⊢ 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
have 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
Tactic: rw [dif_pos h]
-- 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_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
⊢ (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
have pos : { length := c.length - 1 + 1,
    partSize :=
      cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1 fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast sorry i.succ),
    partSize_pos := sorry,
    emb := fun (i : Fin (c.length - 1 + 1)) ↦
      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 sorry 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 sorry i.succ)) 0)) ↦
          0)
        (fun (m : Fin (c.length - 1)) ↦
          succ ∘ fun (j : Fin (c.partSize (Fin.cast sorry m.succ))) ↦ (c.emb (Fin.cast sorry m.succ) j).pred sorry)
        i,
    emb_strictMono := sorry, parts_strictMono := sorry, disjoint := sorry, cover := sorry } =
  c
Tactic: simp only [extend, extendLeft, eraseLeft]