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
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
⊢ ∀ ⦃a : Fin (n + 1)⦄, a ∈ range (succ ∘ c.emb i) → ∀ ⦃b : Fin (n + 1)⦄, b ∈ range (succ ∘ c.emb j) → a ≠ b
have succ : ∀ (a : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize i.succ))
  (a_1 : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize j.succ)), ¬c.emb i a = c.emb j a_1
Tactic: simp only [mem_range, comp_apply, ne_eq, forall_exists_index, forall_apply_eq_imp_iff,
          succ_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 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
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
have zero : ∀ (hi : Membership.mem (γ := Set (Fin (c.length + 1))) univ 0) (hij : 0 ≠ j) (h : j < 0),
  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))
    0 j
Tactic: induction i using Fin.induction with
    | zero => simp at h
    | succ i =>
      induction j using Fin.induction with
      | zero =>
        simp only [onFun, cases_succ, cases_zero]
        apply Set.disjoint_iff_forall_ne.2
        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]
        exact fun _ ↦ succ_ne_zero _
      | succ j =>
        simp only [onFun, cases_succ]
        apply Set.disjoint_iff_forall_ne.2
        simp only [mem_range, comp_apply, ne_eq, forall_exists_index, forall_apply_eq_imp_iff,
          succ_inj]
        intro a b
        apply c.emb_ne_emb_of_ne (by simpa using hij)
Cleared hypotheses: i, hi, hij, 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
⊢ ∀ (x : Fin (n + 1)),
    ∃ (m : Fin (c.length + 1)),
      Membership.mem (γ := Set (Fin (n + 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))
        x
have refine_1 : ∃ (m : Fin (c.length + 1)),
  Membership.mem (γ := Set (Fin (n + 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))
    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 :
  ∃ (m : Fin (c.length + 1)),
    Membership.mem (γ := Set (Fin (n + 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))
      0
⊢ ∀ (x : Fin (n + 1)),
    ∃ (m : Fin (c.length + 1)),
      Membership.mem (γ := Set (Fin (n + 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))
        x
have refine_2 : ∀ (i : Fin n),
  ∃ (m : Fin (c.length + 1)),
    Membership.mem (γ := Set (Fin (n + 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
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
k m : Fin c.length
⊢ 0 < update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m
have inl : 0 < update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize m (c.partSize m + 1) 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
inl : 0 < update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize m (c.partSize m + 1) m
⊢ 0 < update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m
have inr : ∀ (hm : m ≠ k), 0 < update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) 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
k m : Fin c.length
⊢ Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m) → Fin (n + 1)
have pos : (h : m = k) → Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m) → Fin (n + 1)
Tactic: by_cases h : m = 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
pos : (h : m = k) → Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m) → Fin (n + 1)
⊢ Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m) → Fin (n + 1)
have neg : (h : ¬m = k) → Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m) → Fin (n + 1)
Tactic: by_cases h : m = 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 : m = k
⊢ update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m = c.partSize k + 1
have rw : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) k = c.partSize k + 1
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c_1 c : OrderedFinpartition n
k m : Fin c.length
h : m = k
⊢ Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m) → Fin (n + 1)
have this : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m = c.partSize k + 1
Tactic: have : update c.partSize k (c.partSize k + 1) m = c.partSize k + 1 := by rw [h]; simp
-- 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 m : Fin c.length
h : ¬m = k
⊢ Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m) → Fin (n + 1)
have this : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m = c.partSize m
Tactic: have : update c.partSize k (c.partSize k + 1) m = c.partSize m := by simp [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
⊢ 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 inl : StrictMono (α := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize m (c.partSize m + 1) m)) (β := 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)
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
inl :
  StrictMono (α := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize m (c.partSize m + 1) m)) (β := 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)
⊢ 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 : ∀ (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 := 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)
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
this :
  ∀ (a' b' : Fin (c.partSize m + 1)),
    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))
⊢ StrictMono (α := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize m (c.partSize m + 1) m)) (β := 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)
have simp : StrictMono (α := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize m (c.partSize m + 1) m)) (β := Fin (n + 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 sorry)
Tactic: simp only [↓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
m : Fin c.length
⊢ StrictMono (α := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize m (c.partSize m + 1) m)) (β := 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)
have inl : ∀ (a' b' : Fin (c.partSize m + 1)),
  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))
Tactic: suffices ∀ (a' b' : Fin (c.partSize m + 1)), a' < b' →
          (cases (motive := fun _ ↦ Fin (n + 1)) 0 (succ ∘ c.emb m)) a' <
          (cases (motive := fun _ ↦ Fin (n + 1)) 0 (succ ∘ c.emb m)) b' by
        simp only [↓reduceDIte]
        intro a b hab
        exact this _ _ hab
-- 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
b a' : Fin (c.partSize m)
h :
  (∀ (h' : a'.castSucc < 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'.castSucc : 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'.castSucc < 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'.castSucc : 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))
h_1 :
  ∀ (h' : a'.succ < 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'.succ : 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'.succ < 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'.succ : 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 : c.emb m a' < c.emb m b
Tactic: simp only [cases_succ, comp_apply, succ_lt_succ_iff]