awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℕ
c_1 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
x : Fin n
j : Fin (c.partSize (c.index 0))
hij : c.emb (c.index 0) j = x.succ
j_ne : j ≠ 0
je_ne' : (↑j : ℕ) ≠ 0
⊢ ∃ (y :
    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 ⋯ y.succ)).pred ⋯ = x
have A : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)
Tactic: have A : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0) :=
        Nat.sub_add_cancel (c.partSize_pos _)
-- 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 : ℕ
c_1 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
x : Fin n
j : Fin (c.partSize (c.index 0))
hij : c.emb (c.index 0) j = x.succ
j_ne : j ≠ 0
je_ne' : (↑j : ℕ) ≠ 0
A : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)
⊢ ∃ (y :
    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 ⋯ y.succ)).pred ⋯ = x
have B : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0) =
  c.partSize (c.index 0) - 1
Tactic: have B : update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0) =
        c.partSize (c.index 0) - 1 := by simp
-- 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_1 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
x : Fin n
j : Fin (c.partSize (c.index 0))
hij : c.emb (c.index 0) j = x.succ
j_ne : j ≠ 0
je_ne' : (↑j : ℕ) ≠ 0
A : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)
B :
  update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0) =
    c.partSize (c.index 0) - 1
⊢ ∃ (y :
    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 ⋯ y.succ)).pred ⋯ = x
have inl : Fin.cast sorry j ≠ 0
Tactic: refine ⟨Fin.cast B.symm (pred (Fin.cast A.symm j) ?_), ?_⟩
-- 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_1 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
x : Fin n
j : Fin (c.partSize (c.index 0))
hij : c.emb (c.index 0) j = x.succ
j_ne : j ≠ 0
je_ne' : (↑j : ℕ) ≠ 0
A : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)
B :
  update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0) =
    c.partSize (c.index 0) - 1
inl : Fin.cast ⋯ j ≠ 0
⊢ ∃ (y :
    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 ⋯ y.succ)).pred ⋯ = x
have inl₁ : (c.emb (c.index 0) (Fin.cast sorry (Fin.cast sorry ((Fin.cast sorry j).pred sorry)).succ)).pred sorry = x
Tactic: refine ⟨Fin.cast B.symm (pred (Fin.cast A.symm j) ?_), ?_⟩
-- 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 : ℕ
c_1 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
x : Fin n
j : Fin (c.partSize (c.index 0))
hij : c.emb (c.index 0) j = x.succ
j_ne : j ≠ 0
je_ne' : (↑j : ℕ) ≠ 0
A : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)
B :
  update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0) =
    c.partSize (c.index 0) - 1
⊢ (c.emb (c.index 0) (Fin.cast ⋯ (Fin.cast ⋯ ((Fin.cast ⋯ j).pred ⋯)).succ)).pred ⋯ = x
have this : x = x.succ.pred sorry
Tactic: have : x = pred (succ x) (succ_ne_zero x) := rfl
-- 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_1 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
x : Fin n
j : Fin (c.partSize (c.index 0))
hij : c.emb (c.index 0) j = x.succ
j_ne : j ≠ 0
je_ne' : (↑j : ℕ) ≠ 0
A : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)
B :
  update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0) =
    c.partSize (c.index 0) - 1
this : x = x.succ.pred ⋯
⊢ (c.emb (c.index 0) (Fin.cast ⋯ (Fin.cast ⋯ ((Fin.cast ⋯ j).pred ⋯)).succ)).pred ⋯ = x
have inl : (c.emb (c.index 0) (Fin.cast sorry (Fin.cast sorry ((Fin.cast sorry j).pred sorry)).succ)).pred sorry = x.succ.pred sorry
Tactic: rw [this]
-- 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_1 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
x : Fin n
j : Fin (c.partSize (c.index 0))
hij : c.emb (c.index 0) j = x.succ
j_ne : j ≠ 0
je_ne' : (↑j : ℕ) ≠ 0
A : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)
B :
  update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0) =
    c.partSize (c.index 0) - 1
this : x = x.succ.pred ⋯
⊢ (c.emb (c.index 0) (Fin.cast ⋯ (Fin.cast ⋯ ((Fin.cast ⋯ j).pred ⋯)).succ)).pred ⋯ = x.succ.pred ⋯
have inl : c.emb (c.index 0) (Fin.cast sorry (Fin.cast sorry ((Fin.cast sorry j).pred sorry)).succ) = c.emb (c.index 0) j
Tactic: simp only [pred_inj, ← 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 : ℕ
c_1 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
x : Fin n
j : Fin (c.partSize (c.index 0))
hij : c.emb (c.index 0) j = x.succ
j_ne : j ≠ 0
je_ne' : (↑j : ℕ) ≠ 0
A : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)
B :
  update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0) =
    c.partSize (c.index 0) - 1
this : x = x.succ.pred ⋯
⊢ c.emb (c.index 0) (Fin.cast ⋯ (Fin.cast ⋯ ((Fin.cast ⋯ j).pred ⋯)).succ) = c.emb (c.index 0) j
have inl : Fin.cast sorry (Fin.cast sorry ((Fin.cast sorry j).pred sorry)).succ = j
Tactic: congr 1
-- 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_1 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
x : Fin n
j : Fin (c.partSize (c.index 0))
hij : c.emb (c.index 0) j = x.succ
j_ne : j ≠ 0
je_ne' : (↑j : ℕ) ≠ 0
A : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)
B :
  update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0) =
    c.partSize (c.index 0) - 1
this : x = x.succ.pred ⋯
⊢ Fin.cast ⋯ (Fin.cast ⋯ ((Fin.cast ⋯ j).pred ⋯)).succ = j
have inl : (↑(Fin.cast sorry (Fin.cast sorry ((Fin.cast sorry j).pred sorry)).succ) : ℕ) = (↑j : ℕ)
Tactic: rw [← val_eq_val]
-- 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_1 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
x : Fin n
j : Fin (c.partSize (c.index 0))
hij : c.emb (c.index 0) j = x.succ
j_ne : j ≠ 0
je_ne' : (↑j : ℕ) ≠ 0
A : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)
B :
  update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0) =
    c.partSize (c.index 0) - 1
this : x = x.succ.pred ⋯
⊢ (↑(Fin.cast ⋯ (Fin.cast ⋯ ((Fin.cast ⋯ j).pred ⋯)).succ) : ℕ) = (↑j : ℕ)
have inl : (↑j : ℕ) - 1 + 1 = (↑j : ℕ)
Tactic: simp only [val_cast, val_succ, val_pred]
-- 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 : ℕ
c_1 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
x : Fin n
i : Fin c.length
j : Fin (c.partSize i)
hij : c.emb i j = x.succ
hi : i ≠ c.index 0
⊢ ∃ (m : Fin c.length) (y :
    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 ⋯ y.succ)).pred ⋯ else (c.emb m (Fin.cast ⋯ y)).pred ⋯) = x
have A : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i = c.partSize i
Tactic: have A : update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i = c.partSize i := by
        simp [hi]
-- 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)
⊢ 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 none)))
    (Sigma.mk (β := fun (c : OrderedFinpartition n) ↦ Option (Fin c.length)) c none)
have simp : c.extendLeft.eraseLeft sorry = c
Tactic: simp only [extend, range_extendLeft_zero, ↓reduceDIte, Sigma.mk.inj_iff, heq_eq_eq,
        and_true]
-- 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 : 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 (some i))))
    (Sigma.mk (β := fun (c : OrderedFinpartition n) ↦ Option (Fin c.length)) c (some i))
have simp : { length := (c.extendMiddle i).length,
    partSize :=
      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),
    partSize_pos := sorry,
    emb :=
      fun (i_1 : Fin (c.extendMiddle i).length)
        (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) i_1)) ↦
      if h : i_1 = i then ((c.extendMiddle i).emb i_1 (Fin.cast sorry j.succ)).pred sorry
      else ((c.extendMiddle i).emb i_1 (Fin.cast sorry j)).pred sorry,
    emb_strictMono := sorry, parts_strictMono := sorry, disjoint := sorry, cover := sorry } =
  c
Tactic: simp only [extend, range_emb_extendMiddle_ne_singleton_zero, ↓reduceDIte,
        Sigma.mk.inj_iff, heq_eq_eq, and_true, eraseMiddle,
        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 : Fin c.length
⊢ { length := (c.extendMiddle i).length,
      partSize :=
        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),
      partSize_pos := ⋯,
      emb :=
        fun (i_1 : Fin (c.extendMiddle i).length)
          (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) i_1)) ↦
        if h : i_1 = i then ((c.extendMiddle i).emb i_1 (Fin.cast ⋯ j.succ)).pred ⋯
        else ((c.extendMiddle i).emb i_1 (Fin.cast ⋯ j)).pred ⋯,
      emb_strictMono := ⋯, parts_strictMono := ⋯, disjoint := ⋯, cover := ⋯ } =
    c
have length : length (n := n)
    { length := (c.extendMiddle i).length,
      partSize :=
        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),
      partSize_pos := sorry,
      emb :=
        fun (i_1 : Fin (c.extendMiddle i).length)
          (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) i_1)) ↦
        if h : i_1 = i then ((c.extendMiddle i).emb i_1 (Fin.cast sorry j.succ)).pred sorry
        else ((c.extendMiddle i).emb i_1 (Fin.cast sorry j)).pred sorry,
      emb_strictMono := sorry, parts_strictMono := sorry, disjoint := sorry, cover := sorry : OrderedFinpartition n } =
  c.length
Tactic: ext
-- 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 : Fin c.length
⊢ HEq (α :=
    Fin
        (length (n := n)
          { length := (c.extendMiddle i).length,
            partSize :=
              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),
            partSize_pos := ⋯,
            emb :=
              fun (i_1 : Fin (c.extendMiddle i).length)
                (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)
                      i_1)) ↦
              if h : i_1 = i then ((c.extendMiddle i).emb i_1 (Fin.cast ⋯ j.succ)).pred ⋯
              else ((c.extendMiddle i).emb i_1 (Fin.cast ⋯ j)).pred ⋯,
            emb_strictMono := ⋯, parts_strictMono := ⋯, disjoint := ⋯, cover := ⋯ }) →
      ℕ)
    (partSize
      { length := (c.extendMiddle i).length,
        partSize :=
          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),
        partSize_pos := ⋯,
        emb :=
          fun (i_1 : Fin (c.extendMiddle i).length)
            (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) i_1)) ↦
          if h : i_1 = i then ((c.extendMiddle i).emb i_1 (Fin.cast ⋯ j.succ)).pred ⋯
          else ((c.extendMiddle i).emb i_1 (Fin.cast ⋯ j)).pred ⋯,
        emb_strictMono := ⋯, parts_strictMono := ⋯, disjoint := ⋯, cover := ⋯ })
    c.partSize
have partSize : update (β := fun (a : Fin (c.extendMiddle i).length) ↦ ℕ) (c.extendMiddle i).partSize i
    ((c.extendMiddle i).partSize i - 1) =
  c.partSize
Tactic: simp only [heq_eq_eq, 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 : Fin c.length
⊢ update (β := fun (a : Fin (c.extendMiddle i).length) ↦ ℕ) (c.extendMiddle i).partSize i
      ((c.extendMiddle i).partSize i - 1) =
    c.partSize
have partSize : ∀ (j : Fin (c.extendMiddle i).length),
  update (β := fun (a : Fin (c.extendMiddle i).length) ↦ ℕ) (c.extendMiddle i).partSize i
      ((c.extendMiddle i).partSize i - 1) j =
    c.partSize j
Tactic: ext j
-- 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 : Fin c.length
j : Fin (c.extendMiddle i).length
⊢ update (β := fun (a : Fin (c.extendMiddle i).length) ↦ ℕ) (c.extendMiddle i).partSize i
      ((c.extendMiddle i).partSize i - 1) j =
    c.partSize j
have partSize : update (β := fun (a : Fin (c.extendMiddle i).length) ↦ ℕ) (c.extendMiddle i).partSize i
    ((c.extendMiddle i).partSize i - 1) i =
  c.partSize i
Tactic: rcases eq_or_ne i j with rfl | hij
Cleared hypotheses: j
-- 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 : Fin c.length
j : Fin (c.extendMiddle i).length
partSize :
  update (β := fun (a : Fin (c.extendMiddle i).length) ↦ ℕ) (c.extendMiddle i).partSize i
      ((c.extendMiddle i).partSize i - 1) i =
    c.partSize i
⊢ update (β := fun (a : Fin (c.extendMiddle i).length) ↦ ℕ) (c.extendMiddle i).partSize i
      ((c.extendMiddle i).partSize i - 1) j =
    c.partSize j
have partSize₁ : ∀ (hij : i ≠ j),
  update (β := fun (a : Fin (c.extendMiddle i).length) ↦ ℕ) (c.extendMiddle i).partSize i
      ((c.extendMiddle i).partSize i - 1) j =
    c.partSize j
Tactic: rcases eq_or_ne i j with rfl | hij