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
⊢ { 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 ⋯ i.succ),
      partSize_pos := ⋯,
      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 ⋯ 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,
      emb_strictMono := ⋯, parts_strictMono := ⋯, disjoint := ⋯, cover := ⋯ } =
    c
have pos : length (n := n + 1)
    { 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 : OrderedFinpartition (n + 1) } =
  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 + 1)
h : range (ι := Fin (c.partSize 0)) (c.emb 0) = {0}
A : c.length - 1 + 1 = c.length
⊢ partSize (n := n + 1)
      { 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 ⋯ i.succ),
        partSize_pos := ⋯,
        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 ⋯ 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,
        emb_strictMono := ⋯, parts_strictMono := ⋯, disjoint := ⋯, cover := ⋯ : OrderedFinpartition (n + 1) }
      0 =
    c.partSize ⟨(↑0 : ℕ), ⋯⟩
have pos : 1 = c.partSize 0
Tactic: change 1 = c.partSize 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}
A : c.length - 1 + 1 = c.length
i : Fin (c.length - 1)
h_1 :
  partSize (n := n + 1)
      { 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 ⋯ i.succ),
        partSize_pos := ⋯,
        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 ⋯ 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,
        emb_strictMono := ⋯, parts_strictMono := ⋯, disjoint := ⋯, cover := ⋯ : OrderedFinpartition (n + 1) }
      i.castSucc =
    c.partSize ⟨(↑i.castSucc : ℕ), ⋯⟩
⊢ partSize (n := n + 1)
      { 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 ⋯ i.succ),
        partSize_pos := ⋯,
        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 ⋯ 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,
        emb_strictMono := ⋯, parts_strictMono := ⋯, disjoint := ⋯, cover := ⋯ : OrderedFinpartition (n + 1) }
      i.succ =
    c.partSize ⟨(↑i.succ : ℕ), ⋯⟩
have pos : c.partSize (Fin.cast sorry i.succ) = c.partSize ⟨(↑i : ℕ) + 1, sorry⟩
Tactic: simp only [cons_succ, val_succ]
-- 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)
⊢ partSize (n := n + 1)
      { 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 ⋯ i.succ),
        partSize_pos := ⋯,
        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 ⋯ 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,
        emb_strictMono := ⋯, parts_strictMono := ⋯, disjoint := ⋯, cover := ⋯ : OrderedFinpartition (n + 1) }
      i =
    c.partSize ⟨(↑i : ℕ), ⋯⟩
have pos : partSize (n := n + 1)
    { 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 : OrderedFinpartition (n + 1) }
    0 =
  c.partSize ⟨(↑0 : ℕ), sorry⟩
Tactic: induction i using Fin.induction with
        | zero => change 1 = c.partSize 0; simp [c.partSize_eq_one_of_range_emb_eq_singleton h]
        | succ i => simp only [cons_succ, val_succ]; rfl
Cleared hypotheses: i
-- 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}
A : c.length - 1 + 1 = c.length
i : Fin (c.length - 1 + 1)
i' : Fin c.length
h' : i ≍ i'
⊢ HEq (α :=
    Fin
        (cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1
          (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast ⋯ i.succ)) i) →
      Fin (n + 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 ⋯ 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 :
      Fin
          (cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1
            (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast ⋯ i.succ)) i) →
        Fin (n + 1))
    (c.emb i')
have this : i' = Fin.cast A i
Tactic: have : i' = Fin.cast A i := eq_of_val_eq (by apply val_eq_val_of_heq h'.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}
A : c.length - 1 + 1 = c.length
i : Fin (c.length - 1 + 1)
i' : Fin c.length
h' : i ≍ i'
this : i' = Fin.cast A i
⊢ HEq (α :=
    Fin
        (cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1
          (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast ⋯ i.succ)) i) →
      Fin (n + 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 ⋯ 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 :
      Fin
          (cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1
            (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast ⋯ i.succ)) i) →
        Fin (n + 1))
    (c.emb i')
have pos : ∀ (h' : i ≍ Fin.cast A i),
  HEq (α :=
    Fin
        (cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1
          (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast sorry i.succ)) i) →
      Fin (n + 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 :
      Fin
          (cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1
            (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast sorry i.succ)) i) →
        Fin (n + 1))
    (β := Fin (c.partSize (Fin.cast A i)) → Fin (n + 1)) (c.emb (Fin.cast A i))
Tactic: subst this
Cleared hypotheses: i', h', 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_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
⊢ HEq (α :=
    Fin
        (cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1
          (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast ⋯ i.succ)) i) →
      Fin (n + 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 ⋯ 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 :
      Fin
          (cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1
            (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast ⋯ i.succ)) i) →
        Fin (n + 1))
    (β := Fin (c.partSize (Fin.cast A i)) → Fin (n + 1)) (c.emb (Fin.cast A i))
have pos : cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1 (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast sorry i.succ)) i =
  c.partSize (Fin.cast A i)
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 + 1)
h : range (ι := Fin (c.partSize 0)) (c.emb 0) = {0}
A : c.length - 1 + 1 = c.length
i : Fin (c.length - 1 + 1)
h' : i ≍ Fin.cast A i
pos :
  cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1 (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast ⋯ i.succ)) i =
    c.partSize (Fin.cast A i)
⊢ HEq (α :=
    Fin
        (cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1
          (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast ⋯ i.succ)) i) →
      Fin (n + 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 ⋯ 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 :
      Fin
          (cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1
            (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast ⋯ i.succ)) i) →
        Fin (n + 1))
    (β := Fin (c.partSize (Fin.cast A i)) → Fin (n + 1)) (c.emb (Fin.cast A i))
have pos₁ : ∀
  (i_1 :
    Fin
      (cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1
        (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast sorry 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 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 i_1 =
    c.emb (Fin.cast A i) (⟨(↑i_1 : ℕ), sorry⟩ : Fin (c.partSize (Fin.cast A i)))
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 + 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
⊢ cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1 (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast ⋯ i.succ)) i =
    c.partSize (Fin.cast A i)
have pos : ∀ (h' : HEq (α := Fin (c.length - 1 + 1)) 0 (Fin.cast A 0)),
  cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1 (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast sorry i.succ)) 0 =
    c.partSize (Fin.cast A 0)
Tactic: induction i using Fin.induction with
          | zero => simp [c.partSize_eq_one_of_range_emb_eq_singleton h]
          | succ i => simp
Cleared hypotheses: i, 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
i : Fin (c.length - 1 + 1)
h' : i ≍ Fin.cast A i
pos :
  ∀ (h' : HEq (α := Fin (c.length - 1 + 1)) 0 (Fin.cast A 0)),
    cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1 (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast ⋯ i.succ))
        0 =
      c.partSize (Fin.cast A 0)
⊢ cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1 (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast ⋯ i.succ)) i =
    c.partSize (Fin.cast A i)
have pos₁ : ∀ (i : Fin (c.length - 1)),
  (∀ (h' : i.castSucc ≍ Fin.cast A i.castSucc),
      cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1 (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast sorry i.succ))
          i.castSucc =
        c.partSize (Fin.cast A i.castSucc)) →
    ∀ (h' : i.succ ≍ Fin.cast A i.succ),
      cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1 (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast sorry i.succ))
          i.succ =
        c.partSize (Fin.cast A i.succ)
Tactic: induction i using Fin.induction with
          | zero => simp [c.partSize_eq_one_of_range_emb_eq_singleton h]
          | succ i => simp
Cleared hypotheses: i, 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
h' : HEq (α := Fin (c.length - 1 + 1)) 0 (Fin.cast A 0)
j :
  Fin
    (cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1 (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast ⋯ i.succ))
      0)
⊢ cases (motive := fun (x : Fin (c.length - 1 + 1)) ↦
      Fin
          (cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1
            (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast ⋯ i.succ)) x) →
        Fin (n + 1))
      (fun
          (x :
            Fin
              (cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1
                (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast ⋯ i.succ)) 0)) ↦
        0)
      (fun (m : Fin (c.length - 1)) ↦
        succ ∘ fun (j : Fin (c.partSize (Fin.cast ⋯ m.succ))) ↦ (c.emb (Fin.cast ⋯ m.succ) j).pred ⋯)
      0 j =
    c.emb (Fin.cast A 0) (⟨(↑j : ℕ), ⋯⟩ : Fin (c.partSize (Fin.cast A 0)))
have pos : 0 = c.emb 0 (⟨0, sorry⟩ : Fin (c.partSize 0))
Tactic: simp only [cases_zero, cast_zero, val_eq_zero]