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 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
i : Fin c.length
h_1 : Membership.mem (γ := Set (Fin c.length)) univ i
j : Fin c.length
h_2 : Membership.mem (γ := Set (Fin c.length)) univ j
hij : i ≠ j
h : i ≠ c.index 0
hj : j ≠ c.index 0
inr :
  Disjoint (α := Set (Fin n))
    (range
      fun (j : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i)) ↦
      (c.emb i (Fin.cast ⋯ j)).pred ⋯)
    (range
      fun (j_1 : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) j)) ↦
      (c.emb j (Fin.cast ⋯ j_1)).pred ⋯)
⊢ onFun (β := Set (Fin n)) Disjoint
    (fun (m : Fin c.length) ↦
      range
        fun (j : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) m)) ↦
        if h : m = c.index 0 then (c.emb m (Fin.cast ⋯ j.succ)).pred ⋯ else (c.emb m (Fin.cast ⋯ j)).pred ⋯)
    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 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
i : Fin c.length
h_1 : Membership.mem (γ := Set (Fin c.length)) univ i
j : Fin c.length
h_2 : Membership.mem (γ := Set (Fin c.length)) univ j
hij : i ≠ j
h : i ≠ c.index 0
hj : j ≠ c.index 0
inr :
  ∀ ⦃a : Fin n⦄,
    Membership.mem (γ := Set (Fin n))
        (range
          fun
            (j : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i)) ↦
          (c.emb i (Fin.cast ⋯ j)).pred ⋯)
        a →
      ∀ ⦃b : Fin n⦄,
        Membership.mem (γ := Set (Fin n))
            (range
              fun
                (j_1 :
                  Fin
                    (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) j)) ↦
              (c.emb j (Fin.cast ⋯ j_1)).pred ⋯)
            b →
          a ≠ b
⊢ Disjoint (α := Set (Fin n))
    (range
      fun (j : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i)) ↦
      (c.emb i (Fin.cast ⋯ j)).pred ⋯)
    (range
      fun (j_1 : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) j)) ↦
      (c.emb j (Fin.cast ⋯ j_1)).pred ⋯)

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 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
i : Fin c.length
h_1 : Membership.mem (γ := Set (Fin c.length)) univ i
j : Fin c.length
h_2 : Membership.mem (γ := Set (Fin c.length)) univ j
hij : i ≠ j
h : i ≠ c.index 0
hj : j ≠ c.index 0
inr :
  ∀ (a : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i))
    (a_1 : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) j)),
    ¬c.emb i (Fin.cast ⋯ a) = c.emb j (Fin.cast ⋯ a_1)
⊢ ∀ ⦃a : Fin n⦄,
    Membership.mem (γ := Set (Fin n))
        (range
          fun
            (j : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i)) ↦
          (c.emb i (Fin.cast ⋯ j)).pred ⋯)
        a →
      ∀ ⦃b : Fin n⦄,
        Membership.mem (γ := Set (Fin n))
            (range
              fun
                (j_1 :
                  Fin
                    (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) j)) ↦
              (c.emb j (Fin.cast ⋯ j_1)).pred ⋯)
            b →
          a ≠ b

Tactic:
simp only [mem_range, ne_eq, forall_exists_index, forall_apply_eq_imp_iff, pred_inj]

Premises used: Set.mem_range, Fin.pred_inj, forall_exists_index, ne_eq, 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 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
i : Fin c.length
h_1 : Membership.mem (γ := Set (Fin c.length)) univ i
j : Fin c.length
h_2 : Membership.mem (γ := Set (Fin c.length)) univ j
hij : i ≠ j
h : i ≠ c.index 0
hj : j ≠ c.index 0
a : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i)
b : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) j)
⊢ ¬c.emb i (Fin.cast ⋯ a) = c.emb j (Fin.cast ⋯ b)

Tactic:
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 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
i : Fin c.length
h_1 : Membership.mem (γ := Set (Fin c.length)) univ i
j : Fin c.length
h_2 : Membership.mem (γ := Set (Fin c.length)) univ j
hij : i ≠ j
h : i ≠ c.index 0
hj : j ≠ c.index 0
a : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i)
b : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) j)
⊢ ¬c.emb i (Fin.cast ⋯ a) = c.emb j (Fin.cast ⋯ b)

Tactic:
exact 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 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
x : Fin n
⊢ c.emb (c.index x.succ) (c.invEmbedding x.succ) = x.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 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
x : Fin n
obtain :
  ∀ (i : Fin c.length) (j : Fin (c.partSize i)) (hij : c.emb i j = x.succ),
    ∃ (m : Fin c.length) (y :
      Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) m)),
      (if h : m = c.index 0 then (c.emb m (Fin.cast ⋯ y.succ)).pred ⋯ else (c.emb m (Fin.cast ⋯ y)).pred ⋯) = x
⊢ ∃ (m : Fin c.length) (y :
    Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) m)),
    (if h : m = c.index 0 then (c.emb m (Fin.cast ⋯ y.succ)).pred ⋯ else (c.emb m (Fin.cast ⋯ y)).pred ⋯) = x

Tactic:
obtain ⟨i, j, hij⟩ : ∃ (i : Fin c.length), ∃ (j : Fin (c.partSize i)), c.emb i j = succ x :=
      ⟨c.index (succ x), c.invEmbedding (succ x), by simp⟩

Premises used: Fin.succ, Fin, OrderedFinpartition.length
-- 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}
x : Fin n
i : Fin c.length
j : Fin (c.partSize i)
hij : c.emb i j = x.succ
inl :
  ∀ (j : Fin (c.partSize (c.index 0))) (hij : c.emb (c.index 0) j = x.succ),
    ∃ (m : Fin c.length) (y :
      Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) m)),
      (if h : m = c.index 0 then (c.emb m (Fin.cast ⋯ y.succ)).pred ⋯ else (c.emb m (Fin.cast ⋯ y)).pred ⋯) = x
inr :
  ∀ (hi : i ≠ c.index 0),
    ∃ (m : Fin c.length) (y :
      Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) m)),
      (if h : m = c.index 0 then (c.emb m (Fin.cast ⋯ y.succ)).pred ⋯ else (c.emb m (Fin.cast ⋯ y)).pred ⋯) = x
⊢ ∃ (m : Fin c.length) (y :
    Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) m)),
    (if h : m = c.index 0 then (c.emb m (Fin.cast ⋯ y.succ)).pred ⋯ else (c.emb m (Fin.cast ⋯ y)).pred ⋯) = x

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

Premises used: OrderedFinpartition.index, eq_or_ne, OfNat.ofNat, 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}
x : Fin n
j : Fin (c.partSize (c.index 0))
hij : c.emb (c.index 0) j = x.succ
⊢ ∃ (m : Fin c.length) (y :
    Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) m)),
    (if h : m = c.index 0 then (c.emb m (Fin.cast ⋯ y.succ)).pred ⋯ else (c.emb m (Fin.cast ⋯ y)).pred ⋯) = x

Tactic:
⟨c.index 0, ?_⟩

Premises used: OrderedFinpartition.index, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c_1 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
x : Fin n
j : Fin (c.partSize (c.index 0))
hij : c.emb (c.index 0) j = x.succ
inl :
  ∃ (y :
    Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0))),
    (if h : c.index 0 = c.index 0 then (c.emb (c.index 0) (Fin.cast ⋯ y.succ)).pred ⋯
      else (c.emb (c.index 0) (Fin.cast ⋯ y)).pred ⋯) =
      x
⊢ ∃ (m : Fin c.length) (y :
    Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) m)),
    (if h : m = c.index 0 then (c.emb m (Fin.cast ⋯ y.succ)).pred ⋯ else (c.emb m (Fin.cast ⋯ y)).pred ⋯) = x

Tactic:
refine ⟨c.index 0, ?_⟩
-- 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}
x : Fin n
hij : c.emb (c.index 0) 0 = x.succ
⊢ 0 = x.succ

Tactic:
simp only [c.emb_zero] at hij

Premises used: OrderedFinpartition.emb_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 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
x : Fin n
hij : 0 = x.succ
⊢ False

Tactic:
(Fin.succ_ne_zero _).symm hij

Premises used: Ne.symm, 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 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
x : Fin n
hij : 0 = x.succ
⊢ False

Tactic:
exact (Fin.succ_ne_zero _).symm hij

Premises used: Ne.symm, 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 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
x : Fin n
j : Fin (c.partSize (c.index 0))
hij : c.emb (c.index 0) j = x.succ
⊢ j ≠ 0

Tactic:
have j_ne : j ≠ 0 := by
        rintro rfl
        simp only [c.emb_zero] at hij
        exact (Fin.succ_ne_zero _).symm 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 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
x : Fin n
j : Fin (c.partSize (c.index 0))
hij : c.emb (c.index 0) j = x.succ
j_ne : j ≠ 0
⊢ (↑j : ℕ) ≠ 0

Tactic:
simpa
-- 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}
x : Fin n
j : Fin (c.partSize (c.index 0))
hij : c.emb (c.index 0) j = x.succ
j_ne : j ≠ 0
⊢ (↑j : ℕ) ≠ 0

Tactic:
have je_ne' : (j : ℕ) ≠ 0 := by simpa
-- 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}
x : Fin n
j : Fin (c.partSize (c.index 0))
hij : c.emb (c.index 0) j = x.succ
j_ne : j ≠ 0
je_ne' : (↑j : ℕ) ≠ 0
inl :
  ∃ (y :
    Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0))),
    (c.emb (c.index 0) (Fin.cast ⋯ y.succ)).pred ⋯ = x
⊢ ∃ (y :
    Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0))),
    (if h : c.index 0 = c.index 0 then (c.emb (c.index 0) (Fin.cast ⋯ y.succ)).pred ⋯
      else (c.emb (c.index 0) (Fin.cast ⋯ y)).pred ⋯) =
      x

Tactic:
simp only [↓reduceDIte]

Premises used: 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 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
x : Fin n
j : Fin (c.partSize (c.index 0))
hij : c.emb (c.index 0) j = x.succ
j_ne : j ≠ 0
je_ne' : (↑j : ℕ) ≠ 0
⊢ c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)

Tactic:
have A : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0) :=
        Nat.sub_add_cancel (c.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 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
x : Fin n
j : Fin (c.partSize (c.index 0))
hij : c.emb (c.index 0) j = x.succ
j_ne : j ≠ 0
je_ne' : (↑j : ℕ) ≠ 0
A : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)
⊢ update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0) =
    c.partSize (c.index 0) - 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 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
x : Fin n
j : Fin (c.partSize (c.index 0))
hij : c.emb (c.index 0) j = x.succ
j_ne : j ≠ 0
je_ne' : (↑j : ℕ) ≠ 0
A : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)
⊢ update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0) =
    c.partSize (c.index 0) - 1

Tactic:
have B : update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0) =
        c.partSize (c.index 0) - 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 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
x : Fin n
j : Fin (c.partSize (c.index 0))
hij : c.emb (c.index 0) j = x.succ
j_ne : j ≠ 0
je_ne' : (↑j : ℕ) ≠ 0
A : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)
B :
  update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0) =
    c.partSize (c.index 0) - 1
⊢ ∃ (y :
    Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0))),
    (c.emb (c.index 0) (Fin.cast ⋯ y.succ)).pred ⋯ = x

Tactic:
⟨Fin.cast B.symm (pred (Fin.cast A.symm j) ?_), ?_⟩

Premises used: Fin.pred, Fin.cast, Exists.intro, Eq.symm
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c_1 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
x : Fin n
j : Fin (c.partSize (c.index 0))
hij : c.emb (c.index 0) j = x.succ
j_ne : j ≠ 0
je_ne' : (↑j : ℕ) ≠ 0
A : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)
B :
  update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0) =
    c.partSize (c.index 0) - 1
inl : Fin.cast ⋯ j ≠ 0
inl₁ : (c.emb (c.index 0) (Fin.cast ⋯ (Fin.cast ⋯ ((Fin.cast ⋯ j).pred ⋯)).succ)).pred ⋯ = x
⊢ ∃ (y :
    Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0))),
    (c.emb (c.index 0) (Fin.cast ⋯ y.succ)).pred ⋯ = x

Tactic:
refine ⟨Fin.cast B.symm (pred (Fin.cast A.symm 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 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
x : Fin n
j : Fin (c.partSize (c.index 0))
hij : c.emb (c.index 0) j = x.succ
j_ne : j ≠ 0
je_ne' : (↑j : ℕ) ≠ 0
A : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)
B :
  update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0) =
    c.partSize (c.index 0) - 1
⊢ Fin.cast ⋯ j ≠ 0

Tactic:
simpa using j_ne