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 :
  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)
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 :=
            ⋯;
          (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)
⊢ 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)

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
h :
  cases (motive := fun (x : Fin (c.partSize m + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb m) ⟨c.partSize m, ⋯⟩ =
    (c.emb m (⟨c.partSize m - 1, ⋯⟩ : Fin (c.partSize m))).succ
⊢ 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)

Tactic:
simp only [↓reduceDIte, update_self, add_tsub_cancel_right, comp_apply, cast_mk]

Premises used: reduceDIte, Fin.cast_mk, Function.comp_apply, add_tsub_cancel_right, Function.update_self
-- 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) := ⟨c.partSize m, ⋯⟩
b : Fin (c.partSize m) := ⟨c.partSize m - 1, ⋯⟩
h : cases (motive := fun (x : Fin (c.partSize m + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb m) a = (c.emb m b).succ
⊢ cases (motive := fun (x : Fin (c.partSize m + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb m) ⟨c.partSize m, ⋯⟩ =
    (c.emb m (⟨c.partSize m - 1, ⋯⟩ : Fin (c.partSize m))).succ

Tactic:
change (cases (motive := fun _ ↦ Fin (n + 1)) 0 (succ ∘ c.emb m)) a = succ (c.emb m b)

Premises used: Fin.succ, OrderedFinpartition.emb, Function.comp, Fin.cases, OfNat.ofNat
-- 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) := ⟨c.partSize m, ⋯⟩
b : Fin (c.partSize m) := ⟨c.partSize m - 1, ⋯⟩
⊢ a = b.succ

Tactic:
simpa [a, b, succ] using (Nat.sub_eq_iff_eq_add (c.partSize_pos m)).mp rfl

Premises used: OrderedFinpartition.partSize_pos, Fin.succ, Nat.sub_eq_iff_eq_add, Iff.mp, 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
a : Fin (c.partSize m + 1) := ⟨c.partSize m, ⋯⟩
b : Fin (c.partSize m) := ⟨c.partSize m - 1, ⋯⟩
⊢ 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
-- 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) := ⟨c.partSize m, ⋯⟩
b : Fin (c.partSize m) := ⟨c.partSize m - 1, ⋯⟩
this : a = b.succ
⊢ cases (motive := fun (x : Fin (c.partSize m + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb m) a = (c.emb m b).succ

Tactic:
simp [this]
-- 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
⊢ 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)

Tactic:
simp [hm]
-- 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 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
apply : j ≠ 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

Tactic:
apply Disjoint.symm
        (this j (mem_univ j) i (mem_univ i) hij.symm ?_)

Premises used: Ne.symm, Disjoint.symm, Set.mem_univ
-- 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 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
⊢ i = k

Tactic:
simp only [ne_eq, Decidable.not_not] at h

Premises used: ne_eq, Decidable.not_not
-- 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 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

Tactic:
simpa [h] using hij.symm

Premises used: Ne.symm
-- 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 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
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 :=
              ⋯;
            (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 := ⋯;
            succ ∘ c.emb m ∘ Fin.cast this))
      i j
inr :
  ∀ (hj : j ≠ 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
⊢ 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

Tactic:
rcases eq_or_ne j k with rfl | hj

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
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 h : i ≠ j
inl :
  Disjoint (α := Set (Fin (n + 1)))
    (range (ι := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize j (c.partSize j + 1) i))
      (if h : i = j then
        (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 ⋯
      else succ ∘ c.emb i ∘ Fin.cast ⋯))
    (range (ι := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize j (c.partSize j + 1) j))
      ((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 ⋯))
⊢ 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 :=
            ⋯;
          (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 := ⋯;
          succ ∘ c.emb m ∘ Fin.cast this))
    i j

Tactic:
simp only [onFun, ↓reduceDIte]

Premises used: Function.onFun, 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
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 h : i ≠ j
this :
  ∀ (a' : Fin (c.partSize i)) (b' : Fin (c.partSize j + 1)),
    (c.emb i a').succ ≠ cases (motive := fun (x : Fin (c.partSize j + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb j) b'
apply :
  ∀ ⦃a : Fin (n + 1)⦄,
    Membership.mem (γ := Set (Fin (n + 1)))
        (range (ι := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize j (c.partSize j + 1) i))
          (if h : i = j then
            (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 ⋯
          else succ ∘ c.emb i ∘ Fin.cast ⋯))
        a →
      ∀ ⦃b : Fin (n + 1)⦄,
        Membership.mem (γ := Set (Fin (n + 1)))
            (range (ι := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize j (c.partSize j + 1) j))
              ((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 ⋯))
            b →
          a ≠ b
⊢ Disjoint (α := Set (Fin (n + 1)))
    (range (ι := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize j (c.partSize j + 1) i))
      (if h : i = j then
        (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 ⋯
      else succ ∘ c.emb i ∘ Fin.cast ⋯))
    (range (ι := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize j (c.partSize j + 1) j))
      ((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 ⋯))

Tactic:
apply Set.disjoint_iff_forall_ne.2

Premises used: Iff.mpr, Set.disjoint_iff_forall_ne
-- 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
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 h : i ≠ j
this :
  ∀ (a' : Fin (c.partSize i)) (b' : Fin (c.partSize j + 1)),
    (c.emb i a').succ ≠ cases (motive := fun (x : Fin (c.partSize j + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb j) b'
simp :
  ∀ (a : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize j (c.partSize j + 1) i))
    (a_1 : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize j (c.partSize j + 1) j)),
    ¬(c.emb i (Fin.cast ⋯ a)).succ =
        cases (motive := fun (x : Fin (c.partSize j + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb j) (Fin.cast ⋯ a_1)
⊢ ∀ ⦃a : Fin (n + 1)⦄,
    Membership.mem (γ := Set (Fin (n + 1)))
        (range (ι := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize j (c.partSize j + 1) i))
          (if h : i = j then
            (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 ⋯
          else succ ∘ c.emb i ∘ Fin.cast ⋯))
        a →
      ∀ ⦃b : Fin (n + 1)⦄,
        Membership.mem (γ := Set (Fin (n + 1)))
            (range (ι := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize j (c.partSize j + 1) j))
              ((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 ⋯))
            b →
          a ≠ b

Tactic:
simp only [hij, ↓reduceDIte, mem_range, comp_apply, ne_eq, forall_exists_index,
          forall_apply_eq_imp_iff]

Premises used: Set.mem_range, forall_exists_index, reduceDIte, ne_eq, Function.comp_apply, forall_apply_eq_imp_iff