awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (hypothesis)
Goal:
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
this : c.partSize (c.index 0) = Nat.card (↑(range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))) : Type)
h : c.index 0 ≠ 0
⊢ 2 ≤ Nat.card (↑(range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))) : Type)
have this₁ : {c.emb (c.index 0) 0, c.emb (c.index 0) (⟨c.partSize (c.index 0) - 1, sorry⟩ : Fin (c.partSize (c.index 0)))} ⊆
  range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))
Tactic: have : {c.emb (c.index 0) 0,
        c.emb (c.index 0) ⟨c.partSize (c.index 0) - 1, Nat.sub_one_lt_of_lt (c.partSize_pos _)⟩}
          ⊆ range (c.emb (c.index 0)) := by simp [insert_subset]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (hypothesis)
Goal:
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
this_1 : c.partSize (c.index 0) = Nat.card (↑(range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))) : Type)
h : c.index 0 ≠ 0
this :
  {c.emb (c.index 0) 0, c.emb (c.index 0) (⟨c.partSize (c.index 0) - 1, ⋯⟩ : Fin (c.partSize (c.index 0)))} ⊆
    range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))
⊢ 2 ≤ Nat.card (↑(range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))) : Type)
have this₁ : {0, c.emb (c.index 0) (⟨c.partSize (c.index 0) - 1, sorry⟩ : Fin (c.partSize (c.index 0)))} ⊆
  range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))
Tactic: simp only [emb_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
Goal:
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
this_1 : c.partSize (c.index 0) = Nat.card (↑(range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))) : Type)
h : c.index 0 ≠ 0
this :
  {0, c.emb (c.index 0) (⟨c.partSize (c.index 0) - 1, ⋯⟩ : Fin (c.partSize (c.index 0)))} ⊆
    range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))
⊢ 2 ≤ Nat.card (↑(range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))) : Type)
have h₁ : 2 = Nat.card (↑{0, c.emb (c.index 0) (⟨c.partSize (c.index 0) - 1, sorry⟩ : Fin (c.partSize (c.index 0)))} : Type)
Tactic: convert! Nat.card_mono Subtype.finite this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
Goal:
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
this_1 : c.partSize (c.index 0) = Nat.card (↑(range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))) : Type)
h : c.index 0 ≠ 0
this :
  {0, c.emb (c.index 0) (⟨c.partSize (c.index 0) - 1, ⋯⟩ : Fin (c.partSize (c.index 0)))} ⊆
    range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))
⊢ 2 = Nat.card (↑{0, c.emb (c.index 0) (⟨c.partSize (c.index 0) - 1, ⋯⟩ : Fin (c.partSize (c.index 0)))} : Type)
have h₁ : 2 =
  Finset.card (α := Fin (n + 1)) {0, c.emb (c.index 0) (⟨c.partSize (c.index 0) - 1, sorry⟩ : Fin (c.partSize (c.index 0)))}
Tactic: simp only [Nat.card_eq_fintype_card, Fintype.card_ofFinset, toFinset_singleton]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
Goal:
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
this_1 : c.partSize (c.index 0) = Nat.card (↑(range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))) : Type)
h : c.index 0 ≠ 0
this :
  {0, c.emb (c.index 0) (⟨c.partSize (c.index 0) - 1, ⋯⟩ : Fin (c.partSize (c.index 0)))} ⊆
    range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))
⊢ 2 =
    Finset.card (α := Fin (n + 1))
      {0, c.emb (c.index 0) (⟨c.partSize (c.index 0) - 1, ⋯⟩ : Fin (c.partSize (c.index 0)))}
have apply : 0 ≠ c.emb (c.index 0) (⟨c.partSize (c.index 0) - 1, sorry⟩ : Fin (c.partSize (c.index 0)))
Tactic: apply (Finset.card_pair ?_).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 : ℕ
c_1 c : OrderedFinpartition n
⊢ ∀ (m : Fin (c.length + 1)),
    StrictMono (α := Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize m)) (β := Fin (n + 1))
      (cases (motive := fun (x : Fin (c.length + 1)) ↦
        Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize x) → Fin (n + 1))
        (fun (x : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize 0)) ↦ 0)
        (fun (m : Fin c.length) ↦ succ ∘ c.emb m) m)
have refine_1 : StrictMono (α := Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize 0)) (β := Fin (n + 1))
  (cases (motive := fun (x : Fin (c.length + 1)) ↦
    Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize x) → Fin (n + 1))
    (fun (x : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize 0)) ↦ 0)
    (fun (m : Fin c.length) ↦ succ ∘ c.emb m) 0)
Tactic: refine Fin.cases ?_ (fun i ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c_1 c : OrderedFinpartition n
refine_1 :
  StrictMono (α := Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize 0)) (β := Fin (n + 1))
    (cases (motive := fun (x : Fin (c.length + 1)) ↦
      Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize x) → Fin (n + 1))
      (fun (x : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize 0)) ↦ 0)
      (fun (m : Fin c.length) ↦ succ ∘ c.emb m) 0)
⊢ ∀ (m : Fin (c.length + 1)),
    StrictMono (α := Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize m)) (β := Fin (n + 1))
      (cases (motive := fun (x : Fin (c.length + 1)) ↦
        Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize x) → Fin (n + 1))
        (fun (x : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize 0)) ↦ 0)
        (fun (m : Fin c.length) ↦ succ ∘ c.emb m) m)
have refine_2 : ∀ (i : Fin c.length),
  StrictMono (α := Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize i.succ)) (β := Fin (n + 1))
    (cases (motive := fun (x : Fin (c.length + 1)) ↦
      Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize x) → Fin (n + 1))
      (fun (x : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize 0)) ↦ 0)
      (fun (m : Fin c.length) ↦ succ ∘ c.emb m) i.succ)
Tactic: refine Fin.cases ?_ (fun i ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c_1 c : OrderedFinpartition n
i j : Fin (c.length + 1)
hij : i < j
⊢ LT.lt (α := Fin (n + 1))
    ((fun (m : Fin (c.length + 1)) ↦
        (cases (motive := fun (x : Fin (c.length + 1)) ↦
            Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize x) → Fin (n + 1))
            (fun (x : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize 0)) ↦ 0)
            (fun (m : Fin c.length) ↦ succ ∘ c.emb m) m
            ⟨HSub.hSub (α := ℕ) (β := ℕ) (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize m : ℕ) 1, ⋯⟩ :
          Fin (n + 1)))
      i)
    ((fun (m : Fin (c.length + 1)) ↦
        (cases (motive := fun (x : Fin (c.length + 1)) ↦
            Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize x) → Fin (n + 1))
            (fun (x : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize 0)) ↦ 0)
            (fun (m : Fin c.length) ↦ succ ∘ c.emb m) m
            ⟨HSub.hSub (α := ℕ) (β := ℕ) (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize m : ℕ) 1, ⋯⟩ :
          Fin (n + 1)))
      j)
have zero : ∀ (hij : i < 0),
  LT.lt (α := Fin (n + 1))
    ((fun (m : Fin (c.length + 1)) ↦
        (cases (motive := fun (x : Fin (c.length + 1)) ↦
            Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize x) → Fin (n + 1))
            (fun (x : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize 0)) ↦ 0)
            (fun (m : Fin c.length) ↦ succ ∘ c.emb m) m
            ⟨HSub.hSub (α := ℕ) (β := ℕ) (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize m : ℕ) 1, sorry⟩ :
          Fin (n + 1)))
      i)
    ((fun (m : Fin (c.length + 1)) ↦
        (cases (motive := fun (x : Fin (c.length + 1)) ↦
            Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize x) → Fin (n + 1))
            (fun (x : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize 0)) ↦ 0)
            (fun (m : Fin c.length) ↦ succ ∘ c.emb m) m
            ⟨HSub.hSub (α := ℕ) (β := ℕ) (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize m : ℕ) 1, sorry⟩ :
          Fin (n + 1)))
      0)
Tactic: induction j using Fin.induction with
    | zero => simp at hij
    | succ j => induction i using Fin.induction with
      | zero => simp
      | succ i =>
        simp only [cons_succ, cases_succ, comp_apply, succ_lt_succ_iff]
        exact c.parts_strictMono (by simpa using hij)
Cleared hypotheses: 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 c : OrderedFinpartition n
i : Fin (c.length + 1)
hi : Membership.mem (γ := Set (Fin (c.length + 1))) univ i
j : Fin (c.length + 1)
hj : Membership.mem (γ := Set (Fin (c.length + 1))) univ j
hij : i ≠ j
⊢ onFun (β := Set (Fin (n + 1))) Disjoint
    (fun (m : Fin (c.length + 1)) ↦
      range (ι := Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize m))
        (cases (motive := fun (x : Fin (c.length + 1)) ↦
          Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize x) → Fin (n + 1))
          (fun (x : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize 0)) ↦ 0)
          (fun (m : Fin c.length) ↦ succ ∘ c.emb m) m))
    i j
have inr : ∀
  (this :
    ∀ (i : Fin (c.length + 1)) (hi : Membership.mem (γ := Set (Fin (c.length + 1))) univ i) (j : Fin (c.length + 1))
      (hj : Membership.mem (γ := Set (Fin (c.length + 1))) univ j) (hij : i ≠ j) (h : j < i),
      onFun (β := Set (Fin (n + 1))) Disjoint
        (fun (m : Fin (c.length + 1)) ↦
          range (ι := Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize m))
            (cases (motive := fun (x : Fin (c.length + 1)) ↦
              Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize x) → Fin (n + 1))
              (fun (x : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize 0)) ↦ 0)
              (fun (m : Fin c.length) ↦ succ ∘ c.emb m) m))
        i j)
  (h : i ≤ j),
  onFun (β := Set (Fin (n + 1))) Disjoint
    (fun (m : Fin (c.length + 1)) ↦
      range (ι := Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize m))
        (cases (motive := fun (x : Fin (c.length + 1)) ↦
          Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize x) → Fin (n + 1))
          (fun (x : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize 0)) ↦ 0)
          (fun (m : Fin c.length) ↦ succ ∘ c.emb m) m))
    i j
Tactic: wlog! h : j < i generalizing i 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 c : OrderedFinpartition n
i : Fin (c.length + 1)
hi : Membership.mem (γ := Set (Fin (c.length + 1))) univ i
j : Fin (c.length + 1)
hj : Membership.mem (γ := Set (Fin (c.length + 1))) univ j
hij : i ≠ j
inr :
  ∀
    (this :
      ∀ (i : Fin (c.length + 1)) (hi : Membership.mem (γ := Set (Fin (c.length + 1))) univ i) (j : Fin (c.length + 1))
        (hj : Membership.mem (γ := Set (Fin (c.length + 1))) univ j) (hij : i ≠ j) (h : j < i),
        onFun (β := Set (Fin (n + 1))) Disjoint
          (fun (m : Fin (c.length + 1)) ↦
            range (ι := Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize m))
              (cases (motive := fun (x : Fin (c.length + 1)) ↦
                Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize x) → Fin (n + 1))
                (fun (x : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize 0)) ↦ 0)
                (fun (m : Fin c.length) ↦ succ ∘ c.emb m) m))
          i j)
    (h : i ≤ j),
    onFun (β := Set (Fin (n + 1))) Disjoint
      (fun (m : Fin (c.length + 1)) ↦
        range (ι := Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize m))
          (cases (motive := fun (x : Fin (c.length + 1)) ↦
            Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize x) → Fin (n + 1))
            (fun (x : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize 0)) ↦ 0)
            (fun (m : Fin c.length) ↦ succ ∘ c.emb m) m))
      i j
⊢ onFun (β := Set (Fin (n + 1))) Disjoint
    (fun (m : Fin (c.length + 1)) ↦
      range (ι := Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize m))
        (cases (motive := fun (x : Fin (c.length + 1)) ↦
          Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize x) → Fin (n + 1))
          (fun (x : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize 0)) ↦ 0)
          (fun (m : Fin c.length) ↦ succ ∘ c.emb m) m))
    i j
have wlog! : ∀ (i : Fin (c.length + 1)) (hi : Membership.mem (γ := Set (Fin (c.length + 1))) univ i) (j : Fin (c.length + 1))
  (hj : Membership.mem (γ := Set (Fin (c.length + 1))) univ j) (hij : i ≠ j) (h : j < i),
  onFun (β := Set (Fin (n + 1))) Disjoint
    (fun (m : Fin (c.length + 1)) ↦
      range (ι := Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize m))
        (cases (motive := fun (x : Fin (c.length + 1)) ↦
          Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize x) → Fin (n + 1))
          (fun (x : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize 0)) ↦ 0)
          (fun (m : Fin c.length) ↦ succ ∘ c.emb m) m))
    i j
Tactic: wlog! h : j < i generalizing i j
Cleared hypotheses: i, hi, j, hj, 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 c : OrderedFinpartition n
i : Fin c.length
hi : Membership.mem (γ := Set (Fin (c.length + 1))) univ i.succ
hj : Membership.mem (γ := Set (Fin (c.length + 1))) univ 0
h_1 :
  ∀ (hi : Membership.mem (γ := Set (Fin (c.length + 1))) univ i.castSucc) (hij : i.castSucc ≠ 0) (h : 0 < i.castSucc),
    onFun (β := Set (Fin (n + 1))) Disjoint
      (fun (m : Fin (c.length + 1)) ↦
        range (ι := Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize m))
          (cases (motive := fun (x : Fin (c.length + 1)) ↦
            Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize x) → Fin (n + 1))
            (fun (x : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize 0)) ↦ 0)
            (fun (m : Fin c.length) ↦ succ ∘ c.emb m) m))
      i.castSucc 0
hij : i.succ ≠ 0
h : 0 < i.succ
⊢ onFun (β := Set (Fin (n + 1))) Disjoint
    (fun (m : Fin (c.length + 1)) ↦
      range (ι := Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize m))
        (cases (motive := fun (x : Fin (c.length + 1)) ↦
          Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize x) → Fin (n + 1))
          (fun (x : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize 0)) ↦ 0)
          (fun (m : Fin c.length) ↦ succ ∘ c.emb m) m))
    i.succ 0
have succ : Disjoint (range (succ ∘ c.emb i))
  (range fun (x : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize 0)) ↦ 0)
Tactic: simp only [onFun, cases_succ, cases_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 : ℕ
c_1 c : OrderedFinpartition n
i : Fin c.length
hi : Membership.mem (γ := Set (Fin (c.length + 1))) univ i.succ
hj : Membership.mem (γ := Set (Fin (c.length + 1))) univ 0
h_1 :
  ∀ (hi : Membership.mem (γ := Set (Fin (c.length + 1))) univ i.castSucc) (hij : i.castSucc ≠ 0) (h : 0 < i.castSucc),
    onFun (β := Set (Fin (n + 1))) Disjoint
      (fun (m : Fin (c.length + 1)) ↦
        range (ι := Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize m))
          (cases (motive := fun (x : Fin (c.length + 1)) ↦
            Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize x) → Fin (n + 1))
            (fun (x : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize 0)) ↦ 0)
            (fun (m : Fin c.length) ↦ succ ∘ c.emb m) m))
      i.castSucc 0
hij : i.succ ≠ 0
h : 0 < i.succ
⊢ Disjoint (range (succ ∘ c.emb i))
    (range fun (x : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize 0)) ↦ 0)
have succ : ∀ ⦃a : Fin (n + 1)⦄,
  a ∈ range (succ ∘ c.emb i) →
    ∀ ⦃b : Fin (n + 1)⦄,
      Membership.mem (γ := Set (Fin (n + 1)))
          (range fun (x : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize 0)) ↦ 0) 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 c : OrderedFinpartition n
i : Fin c.length
hi : Membership.mem (γ := Set (Fin (c.length + 1))) univ i.succ
hj : Membership.mem (γ := Set (Fin (c.length + 1))) univ 0
h_1 :
  ∀ (hi : Membership.mem (γ := Set (Fin (c.length + 1))) univ i.castSucc) (hij : i.castSucc ≠ 0) (h : 0 < i.castSucc),
    onFun (β := Set (Fin (n + 1))) Disjoint
      (fun (m : Fin (c.length + 1)) ↦
        range (ι := Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize m))
          (cases (motive := fun (x : Fin (c.length + 1)) ↦
            Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize x) → Fin (n + 1))
            (fun (x : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize 0)) ↦ 0)
            (fun (m : Fin c.length) ↦ succ ∘ c.emb m) m))
      i.castSucc 0
hij : i.succ ≠ 0
h : 0 < i.succ
⊢ ∀ ⦃a : Fin (n + 1)⦄,
    a ∈ range (succ ∘ c.emb i) →
      ∀ ⦃b : Fin (n + 1)⦄,
        Membership.mem (γ := Set (Fin (n + 1)))
            (range fun (x : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize 0)) ↦ 0) b →
          a ≠ b
have succ : ∀ (a : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize i.succ)), ¬(c.emb i a).succ = 0
Tactic: simp only [mem_range, comp_apply, exists_prop', cons_zero, ne_eq, and_imp,
          Nonempty.forall, forall_const, forall_eq', forall_exists_index, forall_apply_eq_imp_iff]
-- 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 c : OrderedFinpartition n
i : Fin c.length
hi : Membership.mem (γ := Set (Fin (c.length + 1))) univ i.succ
j : Fin c.length
h_1 :
  ∀ (hj : Membership.mem (γ := Set (Fin (c.length + 1))) univ j.castSucc),
    (∀ (hi : Membership.mem (γ := Set (Fin (c.length + 1))) univ i.castSucc) (hij : i.castSucc ≠ j.castSucc)
        (h : j.castSucc < i.castSucc),
        onFun (β := Set (Fin (n + 1))) Disjoint
          (fun (m : Fin (c.length + 1)) ↦
            range (ι := Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize m))
              (cases (motive := fun (x : Fin (c.length + 1)) ↦
                Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize x) → Fin (n + 1))
                (fun (x : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize 0)) ↦ 0)
                (fun (m : Fin c.length) ↦ succ ∘ c.emb m) m))
          i.castSucc j.castSucc) →
      ∀ (hij : i.succ ≠ j.castSucc) (h : j.castSucc < i.succ),
        onFun (β := Set (Fin (n + 1))) Disjoint
          (fun (m : Fin (c.length + 1)) ↦
            range (ι := Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize m))
              (cases (motive := fun (x : Fin (c.length + 1)) ↦
                Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize x) → Fin (n + 1))
                (fun (x : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize 0)) ↦ 0)
                (fun (m : Fin c.length) ↦ succ ∘ c.emb m) m))
          i.succ j.castSucc
hj : Membership.mem (γ := Set (Fin (c.length + 1))) univ j.succ
h_2 :
  ∀ (hi : Membership.mem (γ := Set (Fin (c.length + 1))) univ i.castSucc) (hij : i.castSucc ≠ j.succ)
    (h : j.succ < i.castSucc),
    onFun (β := Set (Fin (n + 1))) Disjoint
      (fun (m : Fin (c.length + 1)) ↦
        range (ι := Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize m))
          (cases (motive := fun (x : Fin (c.length + 1)) ↦
            Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize x) → Fin (n + 1))
            (fun (x : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize 0)) ↦ 0)
            (fun (m : Fin c.length) ↦ succ ∘ c.emb m) m))
      i.castSucc j.succ
hij : i.succ ≠ j.succ
h : j.succ < i.succ
⊢ Disjoint (range (succ ∘ c.emb i)) (range (succ ∘ c.emb j))
have succ : ∀ ⦃a : Fin (n + 1)⦄, a ∈ range (succ ∘ c.emb i) → ∀ ⦃b : Fin (n + 1)⦄, b ∈ range (succ ∘ c.emb j) → a ≠ b
Tactic: apply Set.disjoint_iff_forall_ne.2