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}
i : Fin c.length
h_1 : Membership.mem (γ := Set (Fin c.length)) univ i
j : Fin c.length
h_2 : Membership.mem (γ := Set (Fin c.length)) univ j
hij : i ≠ j
this :
  ∀ (i : Fin c.length),
    Membership.mem (γ := Set (Fin c.length)) univ i →
      ∀ (j : Fin c.length),
        Membership.mem (γ := Set (Fin c.length)) univ j →
          ∀ (hij : i ≠ j) (h : i ≠ c.index 0),
            onFun (β := Set (Fin n)) Disjoint
              (fun (m : Fin c.length) ↦
                range
                  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 ⋯ j.succ)).pred ⋯ else (c.emb m (Fin.cast ⋯ j)).pred ⋯)
              i j
h : ¬i ≠ c.index 0
⊢ j ≠ c.index 0
have h₁ : i = c.index 0
Tactic: simp only [ne_eq, Decidable.not_not] at h
Cleared hypotheses: 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 : ℕ
c_1 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
i : Fin c.length
h_1 : Membership.mem (γ := Set (Fin c.length)) univ i
j : Fin c.length
h_2 : Membership.mem (γ := Set (Fin c.length)) univ j
hij : i ≠ j
h : i ≠ c.index 0
⊢ onFun (β := Set (Fin n)) Disjoint
    (fun (m : Fin c.length) ↦
      range
        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 ⋯ j.succ)).pred ⋯ else (c.emb m (Fin.cast ⋯ j)).pred ⋯)
    i j
have inl : Membership.mem (γ := Set (Fin c.length)) univ (c.index 0) →
  ∀ (hij : i ≠ c.index 0),
    onFun (β := Set (Fin n)) Disjoint
      (fun (m : Fin c.length) ↦
        range
          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)
      i (c.index 0)
Tactic: rcases eq_or_ne j (c.index 0) with rfl | hj
Cleared hypotheses: j, h_2, 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}
i : Fin c.length
h_1 : Membership.mem (γ := Set (Fin c.length)) univ i
j : Fin c.length
h_2 : Membership.mem (γ := Set (Fin c.length)) univ j
hij : i ≠ j
h : i ≠ c.index 0
inl :
  Membership.mem (γ := Set (Fin c.length)) univ (c.index 0) →
    ∀ (hij : i ≠ c.index 0),
      onFun (β := Set (Fin n)) Disjoint
        (fun (m : Fin c.length) ↦
          range
            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 ⋯ j.succ)).pred ⋯ else (c.emb m (Fin.cast ⋯ j)).pred ⋯)
        i (c.index 0)
⊢ onFun (β := Set (Fin n)) Disjoint
    (fun (m : Fin c.length) ↦
      range
        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 ⋯ j.succ)).pred ⋯ else (c.emb m (Fin.cast ⋯ j)).pred ⋯)
    i j
have inr : ∀ (hj : j ≠ c.index 0),
  onFun (β := Set (Fin n)) Disjoint
    (fun (m : Fin c.length) ↦
      range
        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)
    i j
Tactic: rcases eq_or_ne j (c.index 0) with rfl | hj
-- 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}
i : Fin c.length
h_1 : Membership.mem (γ := Set (Fin c.length)) univ i
h : i ≠ c.index 0
h_2 : Membership.mem (γ := Set (Fin c.length)) univ (c.index 0)
hij : i ≠ c.index 0
⊢ onFun (β := Set (Fin n)) Disjoint
    (fun (m : Fin c.length) ↦
      range
        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 ⋯ j.succ)).pred ⋯ else (c.emb m (Fin.cast ⋯ j)).pred ⋯)
    i (c.index 0)
have inl : Disjoint (α := Set (Fin n))
  (range
    fun (j : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i)) ↦
    (c.emb i (Fin.cast sorry j)).pred sorry)
  (range
    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)
Tactic: simp only [onFun, hij, ↓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 : ℕ
c_1 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
i : Fin c.length
h_1 : Membership.mem (γ := Set (Fin c.length)) univ i
h : i ≠ c.index 0
h_2 : Membership.mem (γ := Set (Fin c.length)) univ (c.index 0)
hij : i ≠ c.index 0
⊢ Disjoint (α := Set (Fin n))
    (range
      fun (j : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i)) ↦
      (c.emb i (Fin.cast ⋯ j)).pred ⋯)
    (range
      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 ⋯)
have inl : ∀ ⦃a : Fin n⦄,
  Membership.mem (γ := Set (Fin n))
      (range
        fun (j : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i)) ↦
        (c.emb i (Fin.cast sorry j)).pred sorry)
      a →
    ∀ ⦃b : Fin n⦄,
      Membership.mem (γ := Set (Fin n))
          (range
            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)
          b →
        a ≠ b
Tactic: apply Set.disjoint_iff_forall_ne.2
-- 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}
i : Fin c.length
h_1 : Membership.mem (γ := Set (Fin c.length)) univ i
h : i ≠ c.index 0
h_2 : Membership.mem (γ := Set (Fin c.length)) univ (c.index 0)
hij : i ≠ c.index 0
⊢ ∀ ⦃a : Fin n⦄,
    Membership.mem (γ := Set (Fin n))
        (range
          fun
            (j : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i)) ↦
          (c.emb i (Fin.cast ⋯ j)).pred ⋯)
        a →
      ∀ ⦃b : Fin n⦄,
        Membership.mem (γ := Set (Fin n))
            (range
              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 ⋯)
            b →
          a ≠ b
have inl : ∀ (a : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i))
  (a_1 :
    Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0))),
  ¬c.emb i (Fin.cast sorry a) = c.emb (c.index 0) (Fin.cast sorry a_1.succ)
Tactic: simp only [mem_range, ne_eq, forall_exists_index, forall_apply_eq_imp_iff, pred_inj]
-- 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}
i : Fin c.length
h_1 : Membership.mem (γ := Set (Fin c.length)) univ i
j : Fin c.length
h_2 : Membership.mem (γ := Set (Fin c.length)) univ j
hij : i ≠ j
h : i ≠ c.index 0
hj : j ≠ c.index 0
⊢ onFun (β := Set (Fin n)) Disjoint
    (fun (m : Fin c.length) ↦
      range
        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 ⋯ j.succ)).pred ⋯ else (c.emb m (Fin.cast ⋯ j)).pred ⋯)
    i j
have inr : Disjoint (α := Set (Fin n))
  (range
    fun (j : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i)) ↦
    (c.emb i (Fin.cast sorry j)).pred sorry)
  (range
    fun (j_1 : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) j)) ↦
    (c.emb j (Fin.cast sorry j_1)).pred sorry)
Tactic: simp only [onFun, h, ↓reduceDIte, hj]
-- 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}
i : Fin c.length
h_1 : Membership.mem (γ := Set (Fin c.length)) univ i
j : Fin c.length
h_2 : Membership.mem (γ := Set (Fin c.length)) univ j
hij : i ≠ j
h : i ≠ c.index 0
hj : j ≠ c.index 0
⊢ Disjoint (α := Set (Fin n))
    (range
      fun (j : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i)) ↦
      (c.emb i (Fin.cast ⋯ j)).pred ⋯)
    (range
      fun (j_1 : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) j)) ↦
      (c.emb j (Fin.cast ⋯ j_1)).pred ⋯)
have inr : ∀ ⦃a : Fin n⦄,
  Membership.mem (γ := Set (Fin n))
      (range
        fun (j : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i)) ↦
        (c.emb i (Fin.cast sorry j)).pred sorry)
      a →
    ∀ ⦃b : Fin n⦄,
      Membership.mem (γ := Set (Fin n))
          (range
            fun
              (j_1 :
                Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) j)) ↦
            (c.emb j (Fin.cast sorry j_1)).pred sorry)
          b →
        a ≠ b
Tactic: apply Set.disjoint_iff_forall_ne.2
-- 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}
i : Fin c.length
h_1 : Membership.mem (γ := Set (Fin c.length)) univ i
j : Fin c.length
h_2 : Membership.mem (γ := Set (Fin c.length)) univ j
hij : i ≠ j
h : i ≠ c.index 0
hj : j ≠ c.index 0
⊢ ∀ ⦃a : Fin n⦄,
    Membership.mem (γ := Set (Fin n))
        (range
          fun
            (j : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i)) ↦
          (c.emb i (Fin.cast ⋯ j)).pred ⋯)
        a →
      ∀ ⦃b : Fin n⦄,
        Membership.mem (γ := Set (Fin n))
            (range
              fun
                (j_1 :
                  Fin
                    (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) j)) ↦
              (c.emb j (Fin.cast ⋯ j_1)).pred ⋯)
            b →
          a ≠ b
have inr : ∀ (a : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i))
  (a_1 : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) j)),
  ¬c.emb i (Fin.cast sorry a) = c.emb j (Fin.cast sorry a_1)
Tactic: simp only [mem_range, ne_eq, forall_exists_index, forall_apply_eq_imp_iff, pred_inj]
-- 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
⊢ ∃ (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 obtain : ∀ (i : Fin c.length) (j : Fin (c.partSize i)) (hij : c.emb i j = x.succ),
  ∃ (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 sorry y.succ)).pred sorry else (c.emb m (Fin.cast sorry y)).pred sorry) = x
Tactic: obtain ⟨i, j, hij⟩ : ∃ (i : Fin c.length), ∃ (j : Fin (c.partSize i)), c.emb i j = succ x :=
      ⟨c.index (succ x), c.invEmbedding (succ x), 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
i : Fin c.length
j : Fin (c.partSize i)
hij : c.emb i j = x.succ
⊢ ∃ (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 inl : ∀ (j : Fin (c.partSize (c.index 0))) (hij : c.emb (c.index 0) j = x.succ),
  ∃ (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 sorry y.succ)).pred sorry else (c.emb m (Fin.cast sorry y)).pred sorry) = x
Tactic: rcases eq_or_ne i (c.index 0) with rfl | hi
Cleared hypotheses: i, j, 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
i : Fin c.length
j : Fin (c.partSize i)
hij : c.emb i j = x.succ
inl :
  ∀ (j : Fin (c.partSize (c.index 0))) (hij : c.emb (c.index 0) j = x.succ),
    ∃ (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
⊢ ∃ (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 inr : ∀ (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 sorry y.succ)).pred sorry else (c.emb m (Fin.cast sorry y)).pred sorry) = x
Tactic: rcases eq_or_ne i (c.index 0) with rfl | 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 : ℕ
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
⊢ ∃ (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 inl : ∃ (y : 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 sorry y.succ)).pred sorry
    else (c.emb (c.index 0) (Fin.cast sorry y)).pred sorry) =
    x
Tactic: refine ⟨c.index 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 : ℕ
c_1 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
x : Fin n
hij : c.emb (c.index 0) 0 = x.succ
⊢ False
have hij₁ : 0 = x.succ
Tactic: simp only [c.emb_zero] at hij
Cleared hypotheses: hij
-- 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
⊢ ∃ (y :
    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 ⋯ y.succ)).pred ⋯
      else (c.emb (c.index 0) (Fin.cast ⋯ y)).pred ⋯) =
      x
have j_ne : j ≠ 0
Tactic: have j_ne : j ≠ 0 := by
        rintro rfl
        simp only [c.emb_zero] at hij
        exact (Fin.succ_ne_zero _).symm hij
-- 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
⊢ ∃ (y :
    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 ⋯ y.succ)).pred ⋯
      else (c.emb (c.index 0) (Fin.cast ⋯ y)).pred ⋯) =
      x
have je_ne' : (↑j : ℕ) ≠ 0
Tactic: have je_ne' : (j : ℕ) ≠ 0 := by simpa
-- 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
⊢ ∃ (y :
    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 ⋯ y.succ)).pred ⋯
      else (c.emb (c.index 0) (Fin.cast ⋯ y)).pred ⋯) =
      x
have inl : ∃ (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 sorry y.succ)).pred sorry = x
Tactic: simp only [↓reduceDIte]