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
refine_1 :
  StrictMono (α := Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize 0)) (β := 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)
refine_2 :
  ∀ (i : Fin c.length),
    StrictMono (α := Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize i.succ)) (β := 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) i.succ)
⊢ ∀ (m : Fin (c.length + 1)),
    StrictMono (α := Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize m)) (β := 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)

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
⊢ Subsingleton (Fin 1)

Tactic:
infer_instance
-- 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
⊢ StrictMono (α := Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize 0)) (β := 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)

Tactic:
exact @Subsingleton.strictMono _ _ _ _ (by simp; infer_instance) _

Premises used: Subsingleton.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
i : Fin c.length
⊢ StrictMono (α := Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize i.succ)) (β := 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) i.succ)

Tactic:
strictMono_succ.comp (c.emb_strictMono i)

Premises used: Fin.induction.go, Fin.strictMono_succ, Fin.induction, Fin.cases, 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
i : Fin c.length
⊢ StrictMono (α := Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize i.succ)) (β := 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) i.succ)

Tactic:
exact strictMono_succ.comp (c.emb_strictMono i)

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
i : Fin (c.length + 1)
hij : i < 0
⊢ LT.lt (α := Fin (n + 1))
    ((fun (m : Fin (c.length + 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
            ⟨HSub.hSub (α := ℕ) (β := ℕ) (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize m : ℕ) 1, ⋯⟩ :
          Fin (n + 1)))
      i)
    ((fun (m : Fin (c.length + 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
            ⟨HSub.hSub (α := ℕ) (β := ℕ) (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize m : ℕ) 1, ⋯⟩ :
          Fin (n + 1)))
      0)

Tactic:
simp at 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
j : Fin c.length
h :
  ∀ (hij : 0 < j.castSucc),
    LT.lt (α := Fin (n + 1))
      ((fun (m : Fin (c.length + 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
              ⟨HSub.hSub (α := ℕ) (β := ℕ) (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize m : ℕ) 1, ⋯⟩ :
            Fin (n + 1)))
        0)
      ((fun (m : Fin (c.length + 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
              ⟨HSub.hSub (α := ℕ) (β := ℕ) (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize m : ℕ) 1, ⋯⟩ :
            Fin (n + 1)))
        j.castSucc)
hij : 0 < j.succ
⊢ LT.lt (α := Fin (n + 1))
    ((fun (m : Fin (c.length + 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
            ⟨HSub.hSub (α := ℕ) (β := ℕ) (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize m : ℕ) 1, ⋯⟩ :
          Fin (n + 1)))
      0)
    ((fun (m : Fin (c.length + 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
            ⟨HSub.hSub (α := ℕ) (β := ℕ) (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize m : ℕ) 1, ⋯⟩ :
          Fin (n + 1)))
      j.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 (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
inr :
  ∀
    (this :
      ∀ (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)
    (h : i ≤ j),
    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
wlog! :
  ∀ (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
⊢ 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

Tactic:
wlog! h : j < i generalizing i j
-- 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 + 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
this :
  ∀ (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
h : i ≤ j
⊢ 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

Tactic:
.symm
        (this j (mem_univ j) i (mem_univ i) hij.symm (lt_of_le_of_ne h hij))

Premises used: Ne.symm, Disjoint.symm, Set.mem_univ, lt_of_le_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
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
this :
  ∀ (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
h : i ≤ j
⊢ 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

Tactic:
exact .symm
        (this j (mem_univ j) i (mem_univ i) hij.symm (lt_of_le_of_ne h 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
j : Fin (c.length + 1)
hj : Membership.mem (γ := Set (Fin (c.length + 1))) univ j
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:
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
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) ↦ Fin.succ ∘ c.emb m) m))
      i.castSucc 0
hij : i.succ ≠ 0
h : 0 < i.succ
succ :
  Disjoint (range (Fin.succ ∘ c.emb i))
    (range fun (x : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize 0)) ↦ 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) ↦ Fin.succ ∘ c.emb m) m))
    i.succ 0

Tactic:
simp only [onFun, cases_succ, cases_zero]

Premises used: Function.onFun, Fin.cases_zero, 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
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) ↦ Fin.succ ∘ c.emb m) m))
      i.castSucc 0
hij : i.succ ≠ 0
h : 0 < i.succ
succ :
  ∀ ⦃a : Fin (n + 1)⦄,
    a ∈ range (Fin.succ ∘ c.emb i) →
      ∀ ⦃b : Fin (n + 1)⦄,
        Membership.mem (γ := Set (Fin (n + 1)))
            (range fun (x : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize 0)) ↦ 0) b →
          a ≠ b
⊢ Disjoint (range (Fin.succ ∘ c.emb i))
    (range fun (x : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize 0)) ↦ 0)

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
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) ↦ Fin.succ ∘ c.emb m) m))
      i.castSucc 0
hij : i.succ ≠ 0
h : 0 < i.succ
succ : ∀ (a : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize i.succ)), ¬(c.emb i a).succ = 0
⊢ ∀ ⦃a : Fin (n + 1)⦄,
    a ∈ range (Fin.succ ∘ c.emb i) →
      ∀ ⦃b : Fin (n + 1)⦄,
        Membership.mem (γ := Set (Fin (n + 1)))
            (range fun (x : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize 0)) ↦ 0) b →
          a ≠ b

Tactic:
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]

Premises used: Set.mem_range, Nonempty.forall, and_imp, forall_exists_index, forall_eq', ne_eq, forall_const, Function.comp_apply, forall_apply_eq_imp_iff, Fin.cons_zero, exists_prop'
-- 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:
fun _ ↦ succ_ne_zero _

Premises used: OrderedFinpartition.emb, Fin.succ_ne_zero