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 : ℕ
c_1 c : OrderedFinpartition n
m : Fin c.length
a' : Fin (c.partSize m + 1)
b : Fin (c.partSize m)
h :
  ∀ (h' : a' < b.castSucc),
    LT.lt (α := Fin (n + 1))
      (cases (motive := fun (x : Fin (c.partSize m + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb m) a' : Fin (n + 1))
      (cases (motive := fun (x : Fin (c.partSize m + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb m) b.castSucc : Fin (n + 1))
h' : a' < b.succ
⊢ LT.lt (α := Fin (n + 1))
    (cases (motive := fun (x : Fin (c.partSize m + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb m) a' : Fin (n + 1))
    (cases (motive := fun (x : Fin (c.partSize m + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb m) b.succ : Fin (n + 1))
have inl : (∀ (h' : 0 < b.castSucc),
    LT.lt (α := Fin (n + 1))
      (cases (motive := fun (x : Fin (c.partSize m + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb m) 0 : Fin (n + 1))
      (cases (motive := fun (x : Fin (c.partSize m + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb m) b.castSucc : Fin (n + 1))) →
  ∀ (h' : 0 < b.succ),
    LT.lt (α := Fin (n + 1))
      (cases (motive := fun (x : Fin (c.partSize m + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb m) 0 : Fin (n + 1))
      (cases (motive := fun (x : Fin (c.partSize m + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb m) b.succ : Fin (n + 1))
Tactic: induction a' using Fin.induction with
        | zero => simp
        | succ a' =>
          simp only [cases_succ, comp_apply, succ_lt_succ_iff]
          exact c.emb_strictMono m (by simpa using h')
Cleared hypotheses: a', h, 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 c : OrderedFinpartition n
m : Fin c.length
a' b' : Fin (c.partSize m + 1)
h' : a' < b'
⊢ LT.lt (α := Fin (n + 1))
    (cases (motive := fun (x : Fin (c.partSize m + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb m) a' : Fin (n + 1))
    (cases (motive := fun (x : Fin (c.partSize m + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb m) b' : Fin (n + 1))
have inl : ∀ (h' : a' < 0),
  LT.lt (α := Fin (n + 1))
    (cases (motive := fun (x : Fin (c.partSize m + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb m) a' : Fin (n + 1))
    (cases (motive := fun (x : Fin (c.partSize m + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb m) 0 : Fin (n + 1))
Tactic: induction b' using Fin.induction with
      | zero => simp at h'
      | succ b =>
        induction a' using Fin.induction with
        | zero => simp
        | succ a' =>
          simp only [cases_succ, comp_apply, succ_lt_succ_iff]
          exact c.emb_strictMono m (by simpa using h')
Cleared hypotheses: b', 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 c : OrderedFinpartition n
m : Fin c.length
a' b' : Fin (c.partSize m + 1)
h' : a' < b'
inl :
  ∀ (h' : a' < 0),
    LT.lt (α := Fin (n + 1))
      (cases (motive := fun (x : Fin (c.partSize m + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb m) a' : Fin (n + 1))
      (cases (motive := fun (x : Fin (c.partSize m + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb m) 0 : Fin (n + 1))
⊢ LT.lt (α := Fin (n + 1))
    (cases (motive := fun (x : Fin (c.partSize m + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb m) a' : Fin (n + 1))
    (cases (motive := fun (x : Fin (c.partSize m + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb m) b' : Fin (n + 1))
have inl₁ : ∀ (b : Fin (c.partSize m)),
  (∀ (h' : a' < b.castSucc),
      LT.lt (α := Fin (n + 1))
        (cases (motive := fun (x : Fin (c.partSize m + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb m) a' : Fin (n + 1))
        (cases (motive := fun (x : Fin (c.partSize m + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb m) b.castSucc :
          Fin (n + 1))) →
    ∀ (h' : a' < b.succ),
      LT.lt (α := Fin (n + 1))
        (cases (motive := fun (x : Fin (c.partSize m + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb m) a' : Fin (n + 1))
        (cases (motive := fun (x : Fin (c.partSize m + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb m) b.succ : Fin (n + 1))
Tactic: induction b' using Fin.induction with
      | zero => simp at h'
      | succ b =>
        induction a' using Fin.induction with
        | zero => simp
        | succ a' =>
          simp only [cases_succ, comp_apply, succ_lt_succ_iff]
          exact c.emb_strictMono m (by simpa using h')
Cleared hypotheses: b', 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 c : OrderedFinpartition n
k m : Fin c.length
hm : m ≠ k
⊢ StrictMono (α := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m)) (β := Fin (n + 1))
    (if h : m = k then
      have this : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m = c.partSize k + 1 := ⋯;
      (fun (i : Fin (c.partSize k + 1)) ↦
          cases (motive := fun (x : Fin (c.partSize k + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb k) i) ∘
        Fin.cast this
    else
      have this : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m = c.partSize m := ⋯;
      succ ∘ c.emb m ∘ Fin.cast this)
have inr : StrictMono (α := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m))
  (succ ∘ c.emb m ∘ Fin.cast sorry)
Tactic: simp only [hm, ↓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 c : OrderedFinpartition n
k : Fin c.length
⊢ StrictMono (β := Fin (n + 1)) fun (m : Fin c.length) ↦
    (if h : m = k then
        have this : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m = c.partSize k + 1 := ⋯;
        (fun (i : Fin (c.partSize k + 1)) ↦
            cases (motive := fun (x : Fin (c.partSize k + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb k) i) ∘
          Fin.cast this
      else
        have this : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m = c.partSize m := ⋯;
        succ ∘ c.emb m ∘ Fin.cast this)
      ⟨update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m - 1, ⋯⟩
have h : ∀ (m : Fin c.length),
  Eq (α := Fin (n + 1))
    ((if h : m = k then
        have this : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m = c.partSize k + 1 := sorry;
        (fun (i : Fin (c.partSize k + 1)) ↦
            cases (motive := fun (x : Fin (c.partSize k + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb k) i) ∘
          Fin.cast this
      else
        have this : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m = c.partSize m := sorry;
        succ ∘ c.emb m ∘ Fin.cast this)
      ⟨update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m - 1, sorry⟩)
    ((succ ∘ fun (m : Fin c.length) ↦ c.emb m ⟨c.partSize m - 1, sorry⟩) m)
Tactic: convert! strictMono_succ.comp c.parts_strictMono with 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
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
k m : Fin c.length
⊢ Eq (α := Fin (n + 1))
    ((if h : m = k then
        have this : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m = c.partSize k + 1 := ⋯;
        (fun (i : Fin (c.partSize k + 1)) ↦
            cases (motive := fun (x : Fin (c.partSize k + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb k) i) ∘
          Fin.cast this
      else
        have this : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m = c.partSize m := ⋯;
        succ ∘ c.emb m ∘ Fin.cast this)
      ⟨update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m - 1, ⋯⟩)
    ((succ ∘ fun (m : Fin c.length) ↦ c.emb m ⟨c.partSize m - 1, ⋯⟩) m)
have h : Eq (α := Fin (n + 1))
  ((if h : m = m then
      have this : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize m (c.partSize m + 1) m = c.partSize m + 1 := sorry;
      (fun (i : Fin (c.partSize m + 1)) ↦
          cases (motive := fun (x : Fin (c.partSize m + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb m) i) ∘
        Fin.cast this
    else
      have this : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize m (c.partSize m + 1) m = c.partSize m := sorry;
      succ ∘ c.emb m ∘ Fin.cast this)
    ⟨update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize m (c.partSize m + 1) m - 1, sorry⟩)
  ((succ ∘ fun (m : Fin c.length) ↦ c.emb m ⟨c.partSize m - 1, sorry⟩) m)
Tactic: rcases eq_or_ne m k with rfl | hm
Cleared hypotheses: k
-- 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
k m : Fin c.length
h :
  Eq (α := Fin (n + 1))
    ((if h : m = m then
        have this : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize m (c.partSize m + 1) m = c.partSize m + 1 := ⋯;
        (fun (i : Fin (c.partSize m + 1)) ↦
            cases (motive := fun (x : Fin (c.partSize m + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb m) i) ∘
          Fin.cast this
      else
        have this : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize m (c.partSize m + 1) m = c.partSize m := ⋯;
        succ ∘ c.emb m ∘ Fin.cast this)
      ⟨update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize m (c.partSize m + 1) m - 1, ⋯⟩)
    ((succ ∘ fun (m : Fin c.length) ↦ c.emb m ⟨c.partSize m - 1, ⋯⟩) m)
⊢ Eq (α := Fin (n + 1))
    ((if h : m = k then
        have this : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m = c.partSize k + 1 := ⋯;
        (fun (i : Fin (c.partSize k + 1)) ↦
            cases (motive := fun (x : Fin (c.partSize k + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb k) i) ∘
          Fin.cast this
      else
        have this : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m = c.partSize m := ⋯;
        succ ∘ c.emb m ∘ Fin.cast this)
      ⟨update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m - 1, ⋯⟩)
    ((succ ∘ fun (m : Fin c.length) ↦ c.emb m ⟨c.partSize m - 1, ⋯⟩) m)
have h₁ : ∀ (hm : m ≠ k),
  Eq (α := Fin (n + 1))
    ((if h : m = k then
        have this : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m = c.partSize k + 1 := sorry;
        (fun (i : Fin (c.partSize k + 1)) ↦
            cases (motive := fun (x : Fin (c.partSize k + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb k) i) ∘
          Fin.cast this
      else
        have this : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m = c.partSize m := sorry;
        succ ∘ c.emb m ∘ Fin.cast this)
      ⟨update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m - 1, sorry⟩)
    ((succ ∘ fun (m : Fin c.length) ↦ c.emb m ⟨c.partSize m - 1, sorry⟩) m)
Tactic: rcases eq_or_ne m k with rfl | hm
-- 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
⊢ Eq (α := Fin (n + 1))
    ((if h : m = m then
        have this : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize m (c.partSize m + 1) m = c.partSize m + 1 := ⋯;
        (fun (i : Fin (c.partSize m + 1)) ↦
            cases (motive := fun (x : Fin (c.partSize m + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb m) i) ∘
          Fin.cast this
      else
        have this : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize m (c.partSize m + 1) m = c.partSize m := ⋯;
        succ ∘ c.emb m ∘ Fin.cast this)
      ⟨update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize m (c.partSize m + 1) m - 1, ⋯⟩)
    ((succ ∘ fun (m : Fin c.length) ↦ c.emb m ⟨c.partSize m - 1, ⋯⟩) m)
have h : cases (motive := fun (x : Fin (c.partSize m + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb m) ⟨c.partSize m, sorry⟩ =
  (c.emb m (⟨c.partSize m - 1, sorry⟩ : Fin (c.partSize m))).succ
Tactic: simp only [↓reduceDIte, update_self, add_tsub_cancel_right, comp_apply, cast_mk]
-- 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 c : OrderedFinpartition n
m : Fin c.length
a : Fin (c.partSize m + 1) := ⟨c.partSize m, ⋯⟩
b : Fin (c.partSize m) := ⟨c.partSize m - 1, ⋯⟩
⊢ cases (motive := fun (x : Fin (c.partSize m + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb m) a = (c.emb m b).succ
have this : a = b.succ
Tactic: have : a = succ b := by
        simpa [a, b, succ] using (Nat.sub_eq_iff_eq_add (c.partSize_pos m)).mp rfl
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c_1 c : OrderedFinpartition n
k i : Fin c.length
hi : Membership.mem (γ := Set (Fin c.length)) univ i
j : Fin c.length
hj : Membership.mem (γ := Set (Fin c.length)) univ j
hij : i ≠ j
⊢ onFun (β := Set (Fin (n + 1))) Disjoint
    (fun (m : Fin c.length) ↦
      range (ι := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m))
        (if h : m = k then
          have this : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m = c.partSize k + 1 :=
            ⋯;
          (fun (i : Fin (c.partSize k + 1)) ↦
              cases (motive := fun (x : Fin (c.partSize k + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb k) i) ∘
            Fin.cast this
        else
          have this : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m = c.partSize m := ⋯;
          succ ∘ c.emb m ∘ Fin.cast this))
    i j
have inr : ∀
  (this :
    ∀ (i : Fin c.length) (hi : Membership.mem (γ := Set (Fin c.length)) univ i) (j : Fin c.length)
      (hj : Membership.mem (γ := Set (Fin c.length)) univ j) (hij : i ≠ j) (h : i ≠ k),
      onFun (β := Set (Fin (n + 1))) Disjoint
        (fun (m : Fin c.length) ↦
          range (ι := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m))
            (if h : m = k then
              have this :
                update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m = c.partSize k + 1 := sorry;
              (fun (i : Fin (c.partSize k + 1)) ↦
                  cases (motive := fun (x : Fin (c.partSize k + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb k) i) ∘
                Fin.cast this
            else
              have this : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m = c.partSize m :=
                sorry;
              succ ∘ c.emb m ∘ Fin.cast this))
        i j)
  (h : ¬i ≠ k),
  onFun (β := Set (Fin (n + 1))) Disjoint
    (fun (m : Fin c.length) ↦
      range (ι := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m))
        (if h : m = k then
          have this : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m = c.partSize k + 1 :=
            sorry;
          (fun (i : Fin (c.partSize k + 1)) ↦
              cases (motive := fun (x : Fin (c.partSize k + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb k) i) ∘
            Fin.cast this
        else
          have this : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m = c.partSize m := sorry;
          succ ∘ c.emb m ∘ Fin.cast this))
    i j
Tactic: wlog h : i ≠ k 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
k i : Fin c.length
hi : Membership.mem (γ := Set (Fin c.length)) univ i
j : Fin c.length
hj : Membership.mem (γ := Set (Fin c.length)) univ j
hij : i ≠ j
this :
  ∀ (i : Fin c.length) (hi : Membership.mem (γ := Set (Fin c.length)) univ i) (j : Fin c.length)
    (hj : Membership.mem (γ := Set (Fin c.length)) univ j) (hij : i ≠ j) (h : i ≠ k),
    onFun (β := Set (Fin (n + 1))) Disjoint
      (fun (m : Fin c.length) ↦
        range (ι := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m))
          (if h : m = k then
            have this : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m = c.partSize k + 1 :=
              ⋯;
            (fun (i : Fin (c.partSize k + 1)) ↦
                cases (motive := fun (x : Fin (c.partSize k + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb k) i) ∘
              Fin.cast this
          else
            have this : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m = c.partSize m := ⋯;
            succ ∘ c.emb m ∘ Fin.cast this))
      i j
h : ¬i ≠ k
⊢ onFun (β := Set (Fin (n + 1))) Disjoint
    (fun (m : Fin c.length) ↦
      range (ι := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m))
        (if h : m = k then
          have this : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m = c.partSize k + 1 :=
            ⋯;
          (fun (i : Fin (c.partSize k + 1)) ↦
              cases (motive := fun (x : Fin (c.partSize k + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb k) i) ∘
            Fin.cast this
        else
          have this : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m = c.partSize m := ⋯;
          succ ∘ c.emb m ∘ Fin.cast this))
    i j
have apply : j ≠ k
Tactic: apply Disjoint.symm
        (this j (mem_univ j) i (mem_univ i) hij.symm ?_)
-- 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 c : OrderedFinpartition n
k i : Fin c.length
hi : Membership.mem (γ := Set (Fin c.length)) univ i
j : Fin c.length
hj : Membership.mem (γ := Set (Fin c.length)) univ j
hij : i ≠ j
this :
  ∀ (i : Fin c.length) (hi : Membership.mem (γ := Set (Fin c.length)) univ i) (j : Fin c.length)
    (hj : Membership.mem (γ := Set (Fin c.length)) univ j) (hij : i ≠ j) (h : i ≠ k),
    onFun (β := Set (Fin (n + 1))) Disjoint
      (fun (m : Fin c.length) ↦
        range (ι := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m))
          (if h : m = k then
            have this : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m = c.partSize k + 1 :=
              ⋯;
            (fun (i : Fin (c.partSize k + 1)) ↦
                cases (motive := fun (x : Fin (c.partSize k + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb k) i) ∘
              Fin.cast this
          else
            have this : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m = c.partSize m := ⋯;
            succ ∘ c.emb m ∘ Fin.cast this))
      i j
h : ¬i ≠ k
⊢ j ≠ k
have h₁ : i = k
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 c : OrderedFinpartition n
k i : Fin c.length
hi : Membership.mem (γ := Set (Fin c.length)) univ i
j : Fin c.length
hj : Membership.mem (γ := Set (Fin c.length)) univ j
hij : i ≠ j
h : i ≠ k
⊢ onFun (β := Set (Fin (n + 1))) Disjoint
    (fun (m : Fin c.length) ↦
      range (ι := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m))
        (if h : m = k then
          have this : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m = c.partSize k + 1 :=
            ⋯;
          (fun (i : Fin (c.partSize k + 1)) ↦
              cases (motive := fun (x : Fin (c.partSize k + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb k) i) ∘
            Fin.cast this
        else
          have this : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m = c.partSize m := ⋯;
          succ ∘ c.emb m ∘ Fin.cast this))
    i j
have inl : ∀ (h : i ≠ j),
  onFun (β := Set (Fin (n + 1))) Disjoint
    (fun (m : Fin c.length) ↦
      range (ι := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize j (c.partSize j + 1) m))
        (if h : m = j then
          have this : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize j (c.partSize j + 1) m = c.partSize j + 1 :=
            sorry;
          (fun (i : Fin (c.partSize j + 1)) ↦
              cases (motive := fun (x : Fin (c.partSize j + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb j) i) ∘
            Fin.cast this
        else
          have this : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize j (c.partSize j + 1) m = c.partSize m := sorry;
          succ ∘ c.emb m ∘ Fin.cast this))
    i j
Tactic: rcases eq_or_ne j k with rfl | hj
Cleared hypotheses: k, h