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 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:
have A : update c.partSize (c.index i) (c.partSize (c.index i) + 1) (c.index i) =
          c.partSize (c.index i) + 1 := 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
A :
  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
⊢ (if h : c.index i = 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 (c.index i) ∘ Fin.cast ⋯)
      (Fin.cast ⋯ (c.invEmbedding i).succ) =
    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
A :
  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
⊢ ∃ (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

Tactic:
exact ⟨c.index i, (succ (c.invEmbedding i)).cast A.symm, 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
hi : c.index i ≠ k
⊢ update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) (c.index i) = c.partSize (c.index i)

Tactic:
simp [hi]
-- 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
hi : c.index i ≠ k
⊢ update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) (c.index i) = c.partSize (c.index i)

Tactic:
have A : update c.partSize k (c.partSize k + 1) (c.index i) = c.partSize (c.index i) := by
          simp [hi]
-- 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
hi : c.index i ≠ k
A : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) (c.index i) = c.partSize (c.index i)
⊢ (if h : c.index i = 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 (c.index i) ∘ Fin.cast ⋯)
      (Fin.cast ⋯ (c.invEmbedding i)) =
    i.succ

Tactic:
simp [hi]
-- 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
hi : c.index i ≠ k
A : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) (c.index i) = c.partSize (c.index i)
⊢ ∃ (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:
exact ⟨c.index i, (c.invEmbedding i).cast A.symm, by simp [hi]⟩
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition n
i : Fin c.length
⊢ (c.extendMiddle i).emb i 0 = 0

Tactic:
simp [extendMiddle]

Premises used: OrderedFinpartition.extendMiddle
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition n
i : Fin c.length
⊢ (c.extendMiddle i).emb i 0 = 0

Tactic:
have : (c.extendMiddle i).emb i 0 = 0 := by simp [extendMiddle]
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition n
i : Fin c.length
this : (c.extendMiddle i).emb i 0 = 0
rw : (c.extendMiddle i).emb ((c.extendMiddle i).index 0) ((c.extendMiddle i).invEmbedding 0)
| 0

Tactic:
rw [← (c.extendMiddle i).emb_invEmbedding 0]

Premises used: OrderedFinpartition.emb_invEmbedding, OrderedFinpartition.extendMiddle, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition n
i : Fin c.length
this : (c.extendMiddle i).emb i 0 = 0
⊢ (c.extendMiddle i).emb i 0 = (c.extendMiddle i).emb ((c.extendMiddle i).index 0) ((c.extendMiddle i).invEmbedding 0)

Tactic:
conv_rhs at this => rw [← (c.extendMiddle i).emb_invEmbedding 0]

Premises used: OrderedFinpartition.emb_invEmbedding, OrderedFinpartition.extendMiddle, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition n
i : Fin c.length
this :
  (c.extendMiddle i).emb i 0 = (c.extendMiddle i).emb ((c.extendMiddle i).index 0) ((c.extendMiddle i).invEmbedding 0)
contrapose! :
  ∀ (this : (c.extendMiddle i).index 0 ≠ i),
    (c.extendMiddle i).emb i 0 ≠ (c.extendMiddle i).emb ((c.extendMiddle i).index 0) ((c.extendMiddle i).invEmbedding 0)
⊢ (c.extendMiddle i).index 0 = i

Tactic:
contrapose! this
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition n
i : Fin c.length
this : (c.extendMiddle i).index 0 ≠ i
⊢ (c.extendMiddle i).emb i 0 ≠ (c.extendMiddle i).emb ((c.extendMiddle i).index 0) ((c.extendMiddle i).invEmbedding 0)

Tactic:
(c.extendMiddle i).emb_ne_emb_of_ne (Ne.symm this)

Premises used: Ne.symm, OrderedFinpartition.extendMiddle, OrderedFinpartition.emb_ne_emb_of_ne
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition n
i : Fin c.length
this : (c.extendMiddle i).index 0 ≠ i
⊢ (c.extendMiddle i).emb i 0 ≠ (c.extendMiddle i).emb ((c.extendMiddle i).index 0) ((c.extendMiddle i).invEmbedding 0)

Tactic:
exact (c.extendMiddle i).emb_ne_emb_of_ne (Ne.symm this)

Premises used: Ne.symm, OrderedFinpartition.extendMiddle, OrderedFinpartition.emb_ne_emb_of_ne
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition n
i j : Fin c.length
h : range ((c.extendMiddle i).emb j) = {0}
inl : ∀ (h : range ((c.extendMiddle j).emb j) = {0}), False
inr : ∀ (hij : j ≠ i), False
⊢ False

Tactic:
rcases eq_or_ne j i with rfl | hij

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition n
j : Fin c.length
h : range ((c.extendMiddle j).emb j) = {0}
rw : (c.emb j 0).succ ∈ range ((c.extendMiddle j).emb j)
⊢ Membership.mem (γ := Set (Fin n.succ)) {0} (c.emb j 0).succ

Tactic:
rw [← h]
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition n
j : Fin c.length
h : range ((c.extendMiddle j).emb j) = {0}
⊢ (c.extendMiddle j).partSize j = c.partSize j + 1

Tactic:
simp [extendMiddle]

Premises used: OrderedFinpartition.extendMiddle
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition n
j : Fin c.length
h : range ((c.extendMiddle j).emb j) = {0}
⊢ (c.extendMiddle j).partSize j = c.partSize j + 1

Tactic:
have A : (c.extendMiddle j).partSize j = c.partSize j + 1 := by simp [extendMiddle]
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition n
j : Fin c.length
h : range ((c.extendMiddle j).emb j) = {0}
A : (c.extendMiddle j).partSize j = c.partSize j + 1
⊢ ∃ (y : Fin ((c.extendMiddle j).partSize j)), (c.extendMiddle j).emb j y = (c.emb j 0).succ

Tactic:
⟨Fin.cast A.symm (succ 0), ?_⟩

Premises used: Fin.succ, Fin.cast, Exists.intro, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition n
j : Fin c.length
h : range ((c.extendMiddle j).emb j) = {0}
A : (c.extendMiddle j).partSize j = c.partSize j + 1
refine : (c.extendMiddle j).emb j (Fin.cast ⋯ (succ 0)) = (c.emb j 0).succ
⊢ ∃ (y : Fin ((c.extendMiddle j).partSize j)), (c.extendMiddle j).emb j y = (c.emb j 0).succ

Tactic:
refine ⟨Fin.cast A.symm (succ 0), ?_⟩
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition n
j : Fin c.length
h : range ((c.extendMiddle j).emb j) = {0}
A : (c.extendMiddle j).partSize j = c.partSize j + 1
⊢ (c.extendMiddle j).emb j (Fin.cast ⋯ (succ 0)) = (c.emb j 0).succ

Tactic:
simp only [extendMiddle, ↓reduceDIte, comp_apply, Fin.cast_cast, cast_eq_self, cases_succ]

Premises used: reduceDIte, Fin.cast_cast, Fin.cast_eq_self, OrderedFinpartition.extendMiddle, Function.comp_apply, Fin.cases_succ
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition n
j : Fin c.length
h : range ((c.extendMiddle j).emb j) = {0}
⊢ Membership.mem (γ := Set (Fin n.succ)) {0} (c.emb j 0).succ

Tactic:
have : Fin.succ (c.emb j 0) ∈ ({0} : Set (Fin n.succ)) := by
      rw [← h]
      simp only [Nat.succ_eq_add_one, mem_range]
      have A : (c.extendMiddle j).partSize j = c.partSize j + 1 := by simp [extendMiddle]
      refine ⟨Fin.cast A.symm (succ 0), ?_⟩
      simp only [extendMiddle, ↓reduceDIte, comp_apply, Fin.cast_cast, cast_eq_self, cases_succ]
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition n
j : Fin c.length
h : range ((c.extendMiddle j).emb j) = {0}
this : Membership.mem (γ := Set (Fin n.succ)) {0} (c.emb j 0).succ
⊢ (c.emb j 0).succ = 0

Tactic:
simp only [mem_singleton_iff] at this

Premises used: Set.mem_singleton_iff
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition n
j : Fin c.length
h : range ((c.extendMiddle j).emb j) = {0}
this : (c.emb j 0).succ = 0
⊢ False

Tactic:
Fin.succ_ne_zero _ this

Premises used: Fin.succ_ne_zero
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition n
j : Fin c.length
h : range ((c.extendMiddle j).emb j) = {0}
this : (c.emb j 0).succ = 0
⊢ False

Tactic:
exact Fin.succ_ne_zero _ this

Premises used: Fin.succ_ne_zero
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition n
i j : Fin c.length
h : range ((c.extendMiddle i).emb j) = {0}
hij : j ≠ i
⊢ (c.extendMiddle i).emb j 0 ∈ range ((c.extendMiddle i).emb j)

Tactic:
have : (c.extendMiddle i).emb j 0 ∈ range ((c.extendMiddle i).emb j) :=
      mem_range_self 0
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition n
i j : Fin c.length
h : range ((c.extendMiddle i).emb j) = {0}
hij : j ≠ i
this : (c.extendMiddle i).emb j 0 ∈ range ((c.extendMiddle i).emb j)
⊢ Membership.mem (γ := Set (Fin (n + 1))) {0} ((c.extendMiddle i).emb j 0)

Tactic:
rw [h] at this
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition n
i j : Fin c.length
h : range ((c.extendMiddle i).emb j) = {0}
hij : j ≠ i
this : Membership.mem (γ := Set (Fin (n + 1))) {0} ((c.extendMiddle i).emb j 0)
⊢ (c.emb j (Fin.cast ⋯ 0)).succ = 0

Tactic:
simp only [extendMiddle, hij, ↓reduceDIte, comp_apply, mem_singleton_iff] at this

Premises used: reduceDIte, Set.mem_singleton_iff, OrderedFinpartition.extendMiddle, Function.comp_apply
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition n
i j : Fin c.length
h : range ((c.extendMiddle i).emb j) = {0}
hij : j ≠ i
this : (c.emb j (Fin.cast ⋯ 0)).succ = 0
⊢ False

Tactic:
Fin.succ_ne_zero _ this

Premises used: Fin.succ_ne_zero
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition n
i j : Fin c.length
h : range ((c.extendMiddle i).emb j) = {0}
hij : j ≠ i
this : (c.emb j (Fin.cast ⋯ 0)).succ = 0
⊢ False

Tactic:
exact Fin.succ_ne_zero _ this

Premises used: Fin.succ_ne_zero
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition n
⊢ c.extend none = c.extendLeft

Tactic:
rfl

Premises used: OrderedFinpartition.extend, rfl
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition n
i : Fin c.length
⊢ c.extend (some i) = c.extendMiddle i

Tactic:
rfl

Premises used: OrderedFinpartition.extend, 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 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) = {0}
⊢ c.length - 1 + 1 = c.length

Tactic:
have : c.length - 1 + 1 = c.length := Nat.sub_add_cancel (c.length_pos (Nat.zero_lt_succ n))
-- 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 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) = {0}
this : c.length - 1 + 1 = c.length
⊢ Fin (c.length - 1) → ℕ

Tactic:
exact fun i ↦ c.partSize (Fin.cast this (succ i))

Premises used: Fin.succ, Fin.cast, OrderedFinpartition.partSize
-- 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 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) = {0}
i : Fin (c.length - 1)
j : Fin (c.partSize (Fin.cast ⋯ i.succ))
⊢ c.length - 1 + 1 = c.length

Tactic:
have : c.length - 1 + 1 = c.length := Nat.sub_add_cancel (c.length_pos (Nat.zero_lt_succ n))
-- 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 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) = {0}
i : Fin (c.length - 1)
j : Fin (c.partSize (Fin.cast ⋯ i.succ))
this : c.length - 1 + 1 = c.length
refine : c.emb (Fin.cast this i.succ) j ≠ 0
⊢ Fin n

Tactic:
refine Fin.pred (c.emb (Fin.cast this (succ i)) j) ?_

Premises used: Fin.succ, Fin.pred, OrderedFinpartition.emb, Fin.cast
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c_1 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) = {0}
i : Fin (c.length - 1)
j : Fin (c.partSize (Fin.cast ⋯ i.succ))
this : c.length - 1 + 1 = c.length
⊢ onFun (β := Set (Fin (n + 1))) Disjoint (fun (m : Fin c.length) ↦ range (c.emb m)) (Fin.cast this i.succ) 0

Tactic:
have := c.disjoint (mem_univ (Fin.cast this (succ i))) (mem_univ 0) (ne_of_beq_false 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 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) = {0}
i : Fin (c.length - 1)
j : Fin (c.partSize (Fin.cast ⋯ i.succ))
this_1 : c.length - 1 + 1 = c.length
this : onFun (β := Set (Fin (n + 1))) Disjoint (fun (m : Fin c.length) ↦ range (c.emb m)) (Fin.cast this_1 i.succ) 0
⊢ Membership.mem (γ := Set (Fin (n + 1))) ((fun (m : Fin c.length) ↦ range (c.emb m)) (Fin.cast this_1 i.succ))
    (c.emb (Fin.cast this_1 i.succ) j)

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 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) = {0}
i : Fin (c.length - 1)
j : Fin (c.partSize (Fin.cast ⋯ i.succ))
this_1 : c.length - 1 + 1 = c.length
this : onFun (β := Set (Fin (n + 1))) Disjoint (fun (m : Fin c.length) ↦ range (c.emb m)) (Fin.cast this_1 i.succ) 0
⊢ Membership.mem (γ := Set (Fin (n + 1))) ((fun (m : Fin c.length) ↦ range (c.emb m)) 0) 0

Tactic:
simp only [mem_singleton_iff, hc]

Premises used: Set.mem_singleton_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 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) = {0}
i : Fin (c.length - 1)
j : Fin (c.partSize (Fin.cast ⋯ i.succ))
this_1 : c.length - 1 + 1 = c.length
this : onFun (β := Set (Fin (n + 1))) Disjoint (fun (m : Fin c.length) ↦ range (c.emb m)) (Fin.cast this_1 i.succ) 0
⊢ c.emb (Fin.cast this_1 i.succ) j ≠ 0

Tactic:
exact Set.disjoint_iff_forall_ne.1 this (by simp) (by simp only [mem_singleton_iff, hc])

Premises used: Set.disjoint_iff_forall_ne, Iff.mp
-- 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 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) = {0}
i : Fin (c.length - 1)
a b : Fin (c.partSize (Fin.cast ⋯ i.succ))
hab : a < b
simp : c.emb (Fin.cast ⋯ i.succ) a < c.emb (Fin.cast ⋯ i.succ) b
⊢ LT.lt (α := Fin n)
    ((fun (j : Fin (c.partSize (Fin.cast ⋯ i.succ))) ↦
        have this := ⋯;
        (c.emb (Fin.cast this i.succ) j).pred ⋯)
      a)
    ((fun (j : Fin (c.partSize (Fin.cast ⋯ i.succ))) ↦
        have this := ⋯;
        (c.emb (Fin.cast this i.succ) j).pred ⋯)
      b)

Tactic:
simp only [pred_lt_pred_iff, Nat.succ_eq_add_one]

Premises used: Nat.succ_eq_add_one, Fin.pred_lt_pred_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 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) = {0}
i : Fin (c.length - 1)
a b : Fin (c.partSize (Fin.cast ⋯ i.succ))
hab : a < b
⊢ c.emb (Fin.cast ⋯ i.succ) a < c.emb (Fin.cast ⋯ i.succ) b

Tactic:
apply c.emb_strictMono _ hab

Premises used: OrderedFinpartition.emb_strictMono