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)) 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'
a : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize j (c.partSize j + 1) i)
b : 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 ⋯ b)

Tactic:
apply 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
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 :
  ∀ (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'
⊢ 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:
suffices ∀ (a' : Fin (c.partSize i)) (b' : Fin (c.partSize j + 1)),
          succ (c.emb i a') ≠ cases (motive := fun _ ↦ Fin (n + 1)) 0 (succ ∘ c.emb j) b' by
        apply Set.disjoint_iff_forall_ne.2
        simp only [hij, ↓reduceDIte, mem_range, comp_apply, ne_eq, forall_exists_index,
          forall_apply_eq_imp_iff]
        intro a b
        apply 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
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
a' : Fin (c.partSize i)
⊢ (c.emb i a').succ ≠ cases (motive := fun (x : Fin (c.partSize j + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb j) 0

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
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
a' : Fin (c.partSize i)
b' : Fin (c.partSize j)
h_1 :
  (c.emb i a').succ ≠ cases (motive := fun (x : Fin (c.partSize j + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb j) b'.castSucc
inl : ¬c.emb i a' = c.emb j b'
⊢ (c.emb i a').succ ≠ cases (motive := fun (x : Fin (c.partSize j + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb j) b'.succ

Tactic:
simp only [cases_succ, comp_apply, ne_eq, succ_inj]

Premises used: Fin.succ_inj, ne_eq, 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
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
a' : Fin (c.partSize i)
b' : Fin (c.partSize j)
h_1 :
  (c.emb i a').succ ≠ cases (motive := fun (x : Fin (c.partSize j + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb j) b'.castSucc
⊢ ¬c.emb i a' = c.emb j b'

Tactic:
apply c.emb_ne_emb_of_ne 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
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
a' : Fin (c.partSize i)
b' : Fin (c.partSize j + 1)
inl : (c.emb i a').succ ≠ cases (motive := fun (x : Fin (c.partSize j + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb j) 0
inl₁ :
  ∀ (b' : Fin (c.partSize j)),
    (c.emb i a').succ ≠
        cases (motive := fun (x : Fin (c.partSize j + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb j) b'.castSucc →
      (c.emb i a').succ ≠ cases (motive := fun (x : Fin (c.partSize j + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb j) b'.succ
⊢ (c.emb i a').succ ≠ cases (motive := fun (x : Fin (c.partSize j + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb j) b'

Tactic:
induction b' using Fin.induction with
      | zero => simp
      | succ b' =>
        simp only [cases_succ, comp_apply, ne_eq, succ_inj]
        apply c.emb_ne_emb_of_ne hij

Premises used: Fin.succ, Fin.succ_inj, ne_eq, OrderedFinpartition.emb_ne_emb_of_ne, 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
k i : Fin c.length
hi : Membership.mem (γ := Set (Fin c.length)) univ i
j : Fin c.length
hj_1 : Membership.mem (γ := Set (Fin c.length)) univ j
hij : i ≠ j
h : i ≠ k
hj : j ≠ k
inr :
  Disjoint
    (range (ι := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) i))
      (succ ∘ c.emb i ∘ Fin.cast ⋯))
    (range (ι := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) j))
      (succ ∘ c.emb j ∘ Fin.cast ⋯))
⊢ 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:
simp only [onFun, h, ↓reduceDIte, hj]

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
k i : Fin c.length
hi : Membership.mem (γ := Set (Fin c.length)) univ i
j : Fin c.length
hj_1 : Membership.mem (γ := Set (Fin c.length)) univ j
hij : i ≠ j
h : i ≠ k
hj : j ≠ k
inr :
  ∀ ⦃a : Fin (n + 1)⦄,
    a ∈
        range (ι := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) i))
          (succ ∘ c.emb i ∘ Fin.cast ⋯) →
      ∀ ⦃b : Fin (n + 1)⦄,
        b ∈
            range (ι := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) j))
              (succ ∘ c.emb j ∘ Fin.cast ⋯) →
          a ≠ b
⊢ Disjoint
    (range (ι := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) i))
      (succ ∘ c.emb i ∘ Fin.cast ⋯))
    (range (ι := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) j))
      (succ ∘ c.emb j ∘ 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
k i : Fin c.length
hi : Membership.mem (γ := Set (Fin c.length)) univ i
j : Fin c.length
hj_1 : Membership.mem (γ := Set (Fin c.length)) univ j
hij : i ≠ j
h : i ≠ k
hj : j ≠ k
inr :
  ∀ (a : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) i))
    (a_1 : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) j)),
    ¬c.emb i (Fin.cast ⋯ a) = c.emb j (Fin.cast ⋯ a_1)
⊢ ∀ ⦃a : Fin (n + 1)⦄,
    a ∈
        range (ι := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) i))
          (succ ∘ c.emb i ∘ Fin.cast ⋯) →
      ∀ ⦃b : Fin (n + 1)⦄,
        b ∈
            range (ι := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) j))
              (succ ∘ c.emb j ∘ Fin.cast ⋯) →
          a ≠ b

Tactic:
simp only [mem_range, comp_apply, ne_eq, forall_exists_index, forall_apply_eq_imp_iff,
        succ_inj]

Premises used: Set.mem_range, forall_exists_index, Fin.succ_inj, ne_eq, Function.comp_apply, forall_apply_eq_imp_iff
-- 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_1 : Membership.mem (γ := Set (Fin c.length)) univ j
hij : i ≠ j
h : i ≠ k
hj : j ≠ k
a : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) i)
b : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) j)
⊢ ¬c.emb i (Fin.cast ⋯ a) = c.emb j (Fin.cast ⋯ b)

Tactic:
apply c.emb_ne_emb_of_ne 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
k : Fin c.length
⊢ ∀ (x : Fin (n + 1)),
    ∃ (m : Fin c.length),
      Membership.mem (γ := Set (Fin (n + 1)))
        (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))
        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
k : Fin c.length
refine_1 :
  ∃ (m : Fin c.length),
    Membership.mem (γ := Set (Fin (n + 1)))
      (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))
      0
refine_2 :
  ∀ (i : Fin n),
    ∃ (m : Fin c.length),
      Membership.mem (γ := Set (Fin (n + 1)))
        (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.succ
⊢ ∀ (x : Fin (n + 1)),
    ∃ (m : Fin c.length),
      Membership.mem (γ := Set (Fin (n + 1)))
        (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))
        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
k : Fin c.length
refine_1 :
  ∃ (m : Fin c.length) (y : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m)),
    Eq (α := Fin (n + 1))
      ((if h : m = k then
          (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 ⋯
        else succ ∘ c.emb m ∘ Fin.cast ⋯)
        y)
      0
⊢ ∃ (m : Fin c.length),
    Membership.mem (γ := Set (Fin (n + 1)))
      (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))
      0

Tactic:
simp only [mem_range]

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

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 : Fin c.length
⊢ Eq (α := Fin (n + 1))
    ((if h : k = k then
        (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 ⋯
      else succ ∘ c.emb k ∘ Fin.cast ⋯)
      ⟨0, ⋯⟩)
    0

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 : Fin c.length
⊢ ∃ (m : Fin c.length) (y : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m)),
    Eq (α := Fin (n + 1))
      ((if h : m = k then
          (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 ⋯
        else succ ∘ c.emb m ∘ Fin.cast ⋯)
        y)
      0

Tactic:
exact ⟨k, ⟨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
k : Fin c.length
i : Fin n
refine_2 :
  ∃ (m : Fin c.length) (y : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m)),
    (if h : m = k then
          (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 ⋯
        else succ ∘ c.emb m ∘ Fin.cast ⋯)
        y =
      i.succ
⊢ ∃ (m : Fin c.length),
    Membership.mem (γ := Set (Fin (n + 1)))
      (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.succ

Tactic:
simp only [mem_range]

Premises used: Set.mem_range
-- 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
i : Fin n
refine_2 :
  ∃ (m : Fin c.length) (y :
    Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index i) (c.partSize (c.index i) + 1) m)),
    (if h : m = c.index i then
          (fun (i_1 : Fin (c.partSize (c.index i) + 1)) ↦
              cases (motive := fun (x : Fin (c.partSize (c.index i) + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb (c.index i))
                i_1) ∘
            Fin.cast ⋯
        else succ ∘ c.emb m ∘ Fin.cast ⋯)
        y =
      i.succ
refine_2₁ :
  ∀ (hi : c.index i ≠ k),
    ∃ (m : Fin c.length) (y : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m)),
      (if h : m = k then
            (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 ⋯
          else succ ∘ c.emb m ∘ Fin.cast ⋯)
          y =
        i.succ
⊢ ∃ (m : Fin c.length) (y : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m)),
    (if h : m = k then
          (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 ⋯
        else succ ∘ c.emb m ∘ Fin.cast ⋯)
        y =
      i.succ

Tactic:
rcases eq_or_ne (c.index i) k with rfl | hi

Premises used: OrderedFinpartition.index, 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 n
⊢ update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index i) (c.partSize (c.index i) + 1) (c.index i) =
    c.partSize (c.index i) + 1

Tactic:
simp