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
i : Fin c.length
hi : Membership.mem (γ := Set (Fin (c.length + 1))) univ i.succ
hj : Membership.mem (γ := Set (Fin (c.length + 1))) univ 0
h_1 :
  ∀ (hi : Membership.mem (γ := Set (Fin (c.length + 1))) univ i.castSucc) (hij : i.castSucc ≠ 0) (h : 0 < i.castSucc),
    onFun (β := Set (Fin (n + 1))) Disjoint
      (fun (m : Fin (c.length + 1)) ↦
        range (ι := Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize m))
          (cases (motive := fun (x : Fin (c.length + 1)) ↦
            Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize x) → Fin (n + 1))
            (fun (x : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize 0)) ↦ 0)
            (fun (m : Fin c.length) ↦ succ ∘ c.emb m) m))
      i.castSucc 0
hij : i.succ ≠ 0
h : 0 < i.succ
⊢ ∀ (a : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize i.succ)), ¬(c.emb i a).succ = 0

Tactic:
exact fun _ ↦ succ_ne_zero _

Premises used: Fin.succ_ne_zero
-- 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 + 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) ↦ Fin.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) ↦ Fin.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) ↦ Fin.succ ∘ c.emb m) m))
      i.castSucc j.succ
hij : i.succ ≠ j.succ
h : j.succ < i.succ
succ : ∀ ⦃a : Fin (n + 1)⦄, a ∈ range (Fin.succ ∘ c.emb i) → ∀ ⦃b : Fin (n + 1)⦄, b ∈ range (Fin.succ ∘ c.emb j) → a ≠ b
⊢ Disjoint (range (Fin.succ ∘ c.emb i)) (range (Fin.succ ∘ c.emb j))

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 + 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 (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize i.succ)
b : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize j.succ)
⊢ i ≠ j

Tactic:
simpa using hij
-- 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 + 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 (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize i.succ)
b : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize j.succ)
⊢ ¬c.emb i a = c.emb j b

Tactic:
apply c.emb_ne_emb_of_ne (by simpa using hij)

Premises used: OrderedFinpartition.emb_ne_emb_of_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
⊢ ∀ (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

Tactic:
Fin.cases ?_ (fun i ↦ ?_)

Premises used: 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
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
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
⊢ ∀ (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

Tactic:
refine Fin.cases ?_ (fun i ↦ ?_)
-- 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
⊢ Eq (α := Fin (n + 1))
    (cases (motive := fun (x : Fin (c.length + 1)) ↦
        Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize x) → Fin (n + 1))
        (fun (x : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize 0)) ↦ 0)
        (fun (m : Fin c.length) ↦ succ ∘ c.emb m) 0 ⟨0, ⋯⟩ :
      Fin (n + 1))
    (0 : 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 + 1)) (y : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize m)),
    Eq (α := Fin (n + 1))
      (cases (motive := fun (x : Fin (c.length + 1)) ↦
          Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize x) → Fin (n + 1))
          (fun (x : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize 0)) ↦ 0)
          (fun (m : Fin c.length) ↦ succ ∘ c.emb m) m y :
        Fin (n + 1))
      (0 : Fin (n + 1))

Tactic:
exact ⟨0, ⟨0, by simp⟩, by 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
i : Fin n
⊢ c.partSize (c.index i) = cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize (c.index i).succ

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
i : Fin n
⊢ 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) (c.index i).succ (Fin.cast ⋯ (c.invEmbedding i)) =
    i.succ

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
i : Fin n
⊢ ∃ (m : Fin (c.length + 1)) (y : 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 y =
      i.succ

Tactic:
exact ⟨Fin.succ (c.index i), Fin.cast (by simp) (c.invEmbedding i), by simp⟩
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition n
⊢ Nonempty (Fin 1)

Tactic:
infer_instance
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition n
⊢ Eq (α := Set (Fin (n + 1))) (range fun (x : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize 0)) ↦ 0)
    {0}

Tactic:
apply @range_const _ _ (by simp; infer_instance)

Premises used: Set.range_const
-- 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 : 0 < update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize m (c.partSize m + 1) m
inr : ∀ (hm : m ≠ k), 0 < update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m
⊢ 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

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
⊢ 0 < update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize m (c.partSize m + 1) m

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
k m : Fin c.length
hm : m ≠ k
⊢ 0 < update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m

Tactic:
simpa [hm] using c.partSize_pos m

Premises used: OrderedFinpartition.partSize_pos
-- 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
pos : (h : m = k) → Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m) → Fin (n + 1)
neg : (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)

Tactic:
by_cases h : m = k
-- 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
rw : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) k = c.partSize k + 1
⊢ update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m = c.partSize k + 1

Tactic:
rw [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
h : m = k
⊢ update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) k = c.partSize k + 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
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

Tactic:
have : update c.partSize k (c.partSize k + 1) m = c.partSize k + 1 := by rw [h]; 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
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 k + 1
⊢ Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m) → Fin (n + 1)

Tactic:
exact Fin.cases 0 (succ ∘ c.emb k) ∘ Fin.cast this

Premises used: 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
h : ¬m = k
⊢ update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m = c.partSize m

Tactic:
simp [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
h : ¬m = k
⊢ 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]