awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
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
this : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m = c.partSize m
⊢ Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m) → Fin (n + 1)

Tactic:
exact succ ∘ c.emb m ∘ Fin.cast this

Premises used: Fin.succ, OrderedFinpartition.emb, Fin.cast
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
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)
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 := ⋯;
        (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)
⊢ 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)

Tactic:
rcases eq_or_ne m k with rfl | hm

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
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))
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 ⋯)
⊢ 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)

Tactic:
simp only [↓reduceDIte]

Premises used: reduceDIte
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
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))
a b : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize m (c.partSize m + 1) m)
hab : a < b
⊢ LT.lt (α := 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 ⋯)
      a)
    (((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 ⋯)
      b)

Tactic:
this _ _ hab

Premises used: Fin.induction, Fin.cases
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
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))
a b : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize m (c.partSize m + 1) m)
hab : a < b
⊢ LT.lt (α := 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 ⋯)
      a)
    (((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 ⋯)
      b)

Tactic:
exact this _ _ hab
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
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
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))
⊢ 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)

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
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
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)
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:
simp at h'
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
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 : Fin (c.partSize m)
h :
  ∀ (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:
simp
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
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
inl : c.emb m a' < c.emb m b
⊢ 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))

Tactic:
simp only [cases_succ, comp_apply, succ_lt_succ_iff]

Premises used: Fin.succ_lt_succ_iff, Function.comp_apply, Fin.cases_succ
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
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
⊢ a' < b

Tactic:
simpa using h'
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
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
⊢ c.emb m a' < c.emb m b

Tactic:
exact c.emb_strictMono m (by simpa using h')

Premises used: OrderedFinpartition.emb_strictMono
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
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))
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))
⊢ 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:
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')

Premises used: Fin.succ, Fin.succ_lt_succ_iff, Function.comp_apply, Fin.cases_succ, OrderedFinpartition.emb_strictMono
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
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
inr :
  StrictMono (α := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m))
    (succ ∘ c.emb m ∘ Fin.cast ⋯)
⊢ 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)

Tactic:
simp only [hm, ↓reduceDIte]

Premises used: reduceDIte
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
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.cast ⋯)

Tactic:
fun ⦃a b⦄ h ↦ h

Premises used: Function.update, StrictMono, dite
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
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.cast ⋯)

Tactic:
exact fun ⦃a b⦄ h ↦ h
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
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))
    (succ ∘ c.emb m ∘ Fin.cast ⋯)

Tactic:
exact strictMono_succ.comp ((c.emb_strictMono m).comp (by exact fun ⦃a b⦄ h ↦ h))

Premises used: Fin.strictMono_succ, OrderedFinpartition.emb_strictMono, StrictMono.comp
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
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 c.length) (β := Fin (n + 1)) (succ ∘ fun (m : Fin c.length) ↦ c.emb m ⟨c.partSize m - 1, ⋯⟩)

Tactic:
strictMono_succ.comp c.parts_strictMono

Premises used: Fin.strictMono_succ, OrderedFinpartition.parts_strictMono, StrictMono.comp
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
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
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 :=
            ⋯;
          (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)
⊢ 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, ⋯⟩

Tactic:
convert! strictMono_succ.comp c.parts_strictMono with m

Premises used: Fin.strictMono_succ, OrderedFinpartition.parts_strictMono, StrictMono.comp