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 + 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
j :
  Fin
    (cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1 (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast ⋯ i.succ))
      i)
⊢ 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 j =
    c.emb (Fin.cast A i) (⟨(↑j : ℕ), ⋯⟩ : Fin (c.partSize (Fin.cast A i)))
have pos : ∀ (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 sorry i.succ)) 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 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)
      0 j =
    c.emb (Fin.cast A 0) (⟨(↑j : ℕ), sorry⟩ : Fin (c.partSize (Fin.cast A 0)))
Tactic: induction i using Fin.induction with
          | zero =>
            simp only [cases_zero, cast_zero, val_eq_zero]
            exact (apply_eq_of_range_eq_singleton h _).symm
          | succ i => simp
Cleared hypotheses: i, h', 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 + 1)
h : ¬range (ι := Fin (c.partSize 0)) (c.emb 0) = {0}
⊢ 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 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
Tactic: rw [dif_neg h]
-- 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}
⊢ (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
have B : 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))
-- 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}
B : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)
⊢ (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
have 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 := sorry,
    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 sorry j.succ)).pred sorry)
              i) ∘
          Fin.cast sorry
      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 sorry j.succ)).pred sorry else (c.emb m (Fin.cast sorry j)).pred sorry) ∘
            Fin.cast sorry,
    emb_strictMono := sorry, parts_strictMono := sorry, disjoint := sorry, cover := sorry : OrderedFinpartition (n + 1) } =
  c
Tactic: simp only [extend, extendMiddle, eraseMiddle, ↓reduceDIte]
-- 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}
B : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)
i : Fin c.length
⊢ HEq (α :=
    Fin
        (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)
          i) →
      Fin (n + 1))
    (if h_1 : i = 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) i)) ↦
            if h : i = c.index 0 then (c.emb i (Fin.cast ⋯ j.succ)).pred ⋯ else (c.emb i (Fin.cast ⋯ j)).pred ⋯) ∘
          Fin.cast ⋯)
    (c.emb i)
have neg : c.partSize i =
  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) i
Tactic: refine ((Fin.heq_fun_iff ?_).mpr ?_).symm
-- 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}
B : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)
j : Fin (c.partSize (c.index 0))
⊢ c.emb (c.index 0) j =
    (if h_1 : c.index 0 = 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)
                      (c.index 0))) ↦
              if h : c.index 0 = c.index 0 then (c.emb (c.index 0) (Fin.cast ⋯ j.succ)).pred ⋯
              else (c.emb (c.index 0) (Fin.cast ⋯ j)).pred ⋯) ∘
            Fin.cast ⋯)
      ⟨(↑j : ℕ), ⋯⟩
have neg : c.emb (c.index 0) j =
  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 sorry j.succ)).pred sorry)
    (Fin.cast sorry
      (⟨(↑j : ℕ), sorry⟩ :
        Fin
          (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)
            (c.index 0))))
Tactic: simp only [↓reduceDIte, comp_apply]
-- 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}
B : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)
j : Fin (c.partSize (c.index 0))
⊢ c.emb (c.index 0) j =
    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 ⋯)
      (Fin.cast ⋯
        (⟨(↑j : ℕ), ⋯⟩ :
          Fin
            (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)
              (c.index 0))))
have neg : c.emb (c.index 0) 0 =
  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 sorry j.succ)).pred sorry)
    (Fin.cast sorry
      (⟨(↑0 : ℕ), sorry⟩ :
        Fin
          (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)
            (c.index 0))))
Tactic: rcases eq_or_ne j 0 with rfl | hj
Cleared hypotheses: 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_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)
j : Fin (c.partSize (c.index 0))
hj : j ≠ 0
j' : Fin (c.partSize (c.index 0) - 1) := (Fin.cast ⋯ j).pred ⋯
⊢ c.emb (c.index 0) j =
    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 ⋯)
      (Fin.cast ⋯
        (⟨(↑j : ℕ), ⋯⟩ :
          Fin
            (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)
              (c.index 0))))
have this : j = Fin.cast B j'.succ
Tactic: have : j = (succ j').cast B := by simp [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 + 1)
h : ¬range (ι := Fin (c.partSize 0)) (c.emb 0) = {0}
B : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)
j : Fin (c.partSize (c.index 0))
hj : j ≠ 0
j' : Fin (c.partSize (c.index 0) - 1) := (Fin.cast ⋯ j).pred ⋯
this : j = Fin.cast B j'.succ
⊢ c.emb (c.index 0) j =
    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 ⋯)
      (Fin.cast ⋯
        (⟨(↑j : ℕ), ⋯⟩ :
          Fin
            (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)
              (c.index 0))))
have neg : c.emb (c.index 0) (Fin.cast B j'.succ) = c.emb (c.index 0) ⟨(↑j' : ℕ) + 1, sorry⟩
Tactic: simp only [this, val_cast, val_succ, cast_mk, cases_succ', comp_apply, succ_mk,
                succ_pred]
-- 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
n : ℕ
c : OrderedFinpartition n
p : (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F
j : Fin n
v : Fin n → E
z : E
⊢ c.applyOrderedFinpartition p (update (β := fun (a : Fin n) ↦ E) v j z) =
    update (β := fun (a : Fin c.length) ↦ F) (c.applyOrderedFinpartition p v) (c.index j)
      ((p (c.index j) : (a : (i : Fin (c.partSize (c.index j))) → E) → F)
        (update (β := fun (i : Fin (c.partSize (c.index j))) ↦ E) (v ∘ c.emb (c.index j)) (c.invEmbedding j) z))
have h : ∀ (m : Fin c.length),
  c.applyOrderedFinpartition p (update (β := fun (a : Fin n) ↦ E) v j z) m =
    update (β := fun (a : Fin c.length) ↦ F) (c.applyOrderedFinpartition p v) (c.index j)
      ((p (c.index j) : (a : (i : Fin (c.partSize (c.index j))) → E) → F)
        (update (β := fun (i : Fin (c.partSize (c.index j))) ↦ E) (v ∘ c.emb (c.index j)) (c.invEmbedding j) z))
      m
Tactic: ext m
-- 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
n : ℕ
c : OrderedFinpartition n
p : (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F
j : Fin n
v : Fin n → E
z : E
m : Fin c.length
⊢ c.applyOrderedFinpartition p (update (β := fun (a : Fin n) ↦ E) v j z) m =
    update (β := fun (a : Fin c.length) ↦ F) (c.applyOrderedFinpartition p v) (c.index j)
      ((p (c.index j) : (a : (i : Fin (c.partSize (c.index j))) → E) → F)
        (update (β := fun (i : Fin (c.partSize (c.index j))) ↦ E) (v ∘ c.emb (c.index j)) (c.invEmbedding j) z))
      m
have pos : ∀ (h : m = c.index j),
  c.applyOrderedFinpartition p (update (β := fun (a : Fin n) ↦ E) v j z) m =
    update (β := fun (a : Fin c.length) ↦ F) (c.applyOrderedFinpartition p v) (c.index j)
      ((p (c.index j) : (a : (i : Fin (c.partSize (c.index j))) → E) → F)
        (update (β := fun (i : Fin (c.partSize (c.index j))) ↦ E) (v ∘ c.emb (c.index j)) (c.invEmbedding j) z))
      m
Tactic: by_cases h : m = c.index 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
n : ℕ
c : OrderedFinpartition n
p : (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F
j : Fin n
v : Fin n → E
z : E
m : Fin c.length
pos :
  ∀ (h : m = c.index j),
    c.applyOrderedFinpartition p (update (β := fun (a : Fin n) ↦ E) v j z) m =
      update (β := fun (a : Fin c.length) ↦ F) (c.applyOrderedFinpartition p v) (c.index j)
        ((p (c.index j) : (a : (i : Fin (c.partSize (c.index j))) → E) → F)
          (update (β := fun (i : Fin (c.partSize (c.index j))) ↦ E) (v ∘ c.emb (c.index j)) (c.invEmbedding j) z))
        m
⊢ c.applyOrderedFinpartition p (update (β := fun (a : Fin n) ↦ E) v j z) m =
    update (β := fun (a : Fin c.length) ↦ F) (c.applyOrderedFinpartition p v) (c.index j)
      ((p (c.index j) : (a : (i : Fin (c.partSize (c.index j))) → E) → F)
        (update (β := fun (i : Fin (c.partSize (c.index j))) ↦ E) (v ∘ c.emb (c.index j)) (c.invEmbedding j) z))
      m
have neg : ∀ (h : ¬m = c.index j),
  c.applyOrderedFinpartition p (update (β := fun (a : Fin n) ↦ E) v j z) m =
    update (β := fun (a : Fin c.length) ↦ F) (c.applyOrderedFinpartition p v) (c.index j)
      ((p (c.index j) : (a : (i : Fin (c.partSize (c.index j))) → E) → F)
        (update (β := fun (i : Fin (c.partSize (c.index j))) ↦ E) (v ∘ c.emb (c.index j)) (c.invEmbedding j) z))
      m
Tactic: by_cases h : m = c.index j