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
hij : i < c.index 0
A : 1 < c.partSize (c.index 0)
⊢ LT.lt (α := Fin (c.partSize (c.index 0))) 0 ⟨c.partSize (c.index 0) - 1 - 1 + 1, ⋯⟩

Tactic:
simp [lt_def]

Premises used: Fin.lt_def
-- 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 j : Fin c.length
hij : i < j
hj : j ≠ c.index 0
h :
  (↑(c.emb j (⟨c.partSize j - 1, ⋯⟩ : Fin (c.partSize j))) : ℕ) - 1 + 1 =
    (↑(c.emb j (⟨c.partSize j - 1, ⋯⟩ : Fin (c.partSize j))) : ℕ)
⊢ (↑(if h : j = c.index 0 then
            (c.emb j
                  (Fin.cast ⋯
                    (⟨update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) j -
                            1,
                          ⋯⟩ :
                        Fin
                          (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                            j)).succ)).pred
              ⋯
          else
            (c.emb j
                  (Fin.cast ⋯
                    (⟨update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) j -
                          1,
                        ⋯⟩ :
                      Fin
                        (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                          j)))).pred
              ⋯) :
        ℕ) +
      1 =
    (↑((fun (m : Fin c.length) ↦ c.emb m (⟨c.partSize m - 1, ⋯⟩ : Fin (c.partSize m))) j) : ℕ)

Tactic:
simp only [hj, ↓reduceDIte, ne_eq, not_false_eq_true, update_of_ne, cast_mk, val_pred]

Premises used: Fin.val_pred, reduceDIte, ne_eq, Fin.cast_mk, not_false_eq_true, Function.update_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 j : Fin c.length
hij : i < j
hj : j ≠ c.index 0
h : 1 ≤ (↑(c.emb j (⟨c.partSize j - 1, ⋯⟩ : Fin (c.partSize j))) : ℕ)
⊢ (↑(c.emb j (⟨c.partSize j - 1, ⋯⟩ : Fin (c.partSize j))) : ℕ) - 1 + 1 =
    (↑(c.emb j (⟨c.partSize j - 1, ⋯⟩ : Fin (c.partSize j))) : ℕ)

Tactic:
apply Nat.sub_add_cancel

Premises used: Nat.sub_add_cancel
-- 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 j : Fin c.length
hij : i < j
hj : j ≠ c.index 0
⊢ c.emb j (⟨c.partSize j - 1, ⋯⟩ : Fin (c.partSize j)) ≠ c.emb (c.index 0) 0

Tactic:
have : c.emb j ⟨c.partSize j - 1, Nat.sub_one_lt_of_lt (c.partSize_pos j)⟩
            ≠ c.emb (c.index 0) 0 := c.emb_ne_emb_of_ne hj
-- 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 j : Fin c.length
hij : i < j
hj : j ≠ c.index 0
this : c.emb j (⟨c.partSize j - 1, ⋯⟩ : Fin (c.partSize j)) ≠ c.emb (c.index 0) 0
⊢ ¬(↑(c.emb j (⟨c.partSize j - 1, ⋯⟩ : Fin (c.partSize j))) : ℕ) = 0

Tactic:
simp only [c.emb_zero, ne_eq, ← val_eq_val, val_zero] at this

Premises used: OrderedFinpartition.emb_zero, ne_eq, Fin.val_zero, Fin.val_eq_val
-- 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 j : Fin c.length
hij : i < j
hj : j ≠ c.index 0
this : ¬(↑(c.emb j (⟨c.partSize j - 1, ⋯⟩ : Fin (c.partSize j))) : ℕ) = 0
⊢ 1 ≤ (↑(c.emb j (⟨c.partSize j - 1, ⋯⟩ : Fin (c.partSize j))) : ℕ)

Tactic:
lia
-- 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 : Membership.mem (γ := Set (Fin c.length)) univ i
j : Fin c.length
h_1 : Membership.mem (γ := Set (Fin c.length)) univ j
hij : i ≠ j
inr :
  ∀
    (this :
      ∀ (i : Fin c.length),
        Membership.mem (γ := Set (Fin c.length)) univ i →
          ∀ (j : Fin c.length),
            Membership.mem (γ := Set (Fin c.length)) univ j →
              ∀ (hij : i ≠ j) (h : i ≠ c.index 0),
                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)
    (h : ¬i ≠ c.index 0),
    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
wlog :
  ∀ (i : Fin c.length),
    Membership.mem (γ := Set (Fin c.length)) univ i →
      ∀ (j : Fin c.length),
        Membership.mem (γ := Set (Fin c.length)) univ j →
          ∀ (hij : i ≠ j) (h : i ≠ c.index 0),
            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
⊢ 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:
wlog h : i ≠ c.index 0 generalizing i j

Premises used: OrderedFinpartition.index, 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}
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
this :
  ∀ (i : Fin c.length),
    Membership.mem (γ := Set (Fin c.length)) univ i →
      ∀ (j : Fin c.length),
        Membership.mem (γ := Set (Fin c.length)) univ j →
          ∀ (hij : i ≠ j) (h : i ≠ c.index 0),
            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
h : ¬i ≠ c.index 0
apply : j ≠ c.index 0
⊢ 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:
apply Disjoint.symm
        (this j (mem_univ j) i (mem_univ i) hij.symm ?_)

Premises used: Ne.symm, Disjoint.symm, Set.mem_univ
-- 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
this :
  ∀ (i : Fin c.length),
    Membership.mem (γ := Set (Fin c.length)) univ i →
      ∀ (j : Fin c.length),
        Membership.mem (γ := Set (Fin c.length)) univ j →
          ∀ (hij : i ≠ j) (h : i ≠ c.index 0),
            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
h : ¬i ≠ c.index 0
⊢ i = c.index 0

Tactic:
simp only [ne_eq, Decidable.not_not] at h

Premises used: ne_eq, Decidable.not_not
-- 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
this :
  ∀ (i : Fin c.length),
    Membership.mem (γ := Set (Fin c.length)) univ i →
      ∀ (j : Fin c.length),
        Membership.mem (γ := Set (Fin c.length)) univ j →
          ∀ (hij : i ≠ j) (h : i ≠ c.index 0),
            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
h : i = c.index 0
⊢ j ≠ c.index 0

Tactic:
simpa [h] using hij.symm

Premises used: Ne.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}
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
inl :
  Membership.mem (γ := Set (Fin c.length)) univ (c.index 0) →
    ∀ (hij : i ≠ c.index 0),
      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 (c.index 0)
inr :
  ∀ (hj : j ≠ c.index 0),
    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
⊢ 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:
rcases eq_or_ne j (c.index 0) with rfl | hj

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}
i : Fin c.length
h_1 : Membership.mem (γ := Set (Fin c.length)) univ i
h : i ≠ c.index 0
h_2 : Membership.mem (γ := Set (Fin c.length)) univ (c.index 0)
hij : i ≠ c.index 0
inl :
  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 :
          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 ⋯ j.succ)).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 (c.index 0)

Tactic:
simp only [onFun, hij, ↓reduceDIte]

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
h : i ≠ c.index 0
h_2 : Membership.mem (γ := Set (Fin c.length)) univ (c.index 0)
hij : i ≠ c.index 0
inl :
  ∀ ⦃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 :
                  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 ⋯ j.succ)).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 :
          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 ⋯ j.succ)).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
h : i ≠ c.index 0
h_2 : Membership.mem (γ := Set (Fin c.length)) univ (c.index 0)
hij : i ≠ c.index 0
inl :
  ∀ (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) (c.index 0))),
    ¬c.emb i (Fin.cast ⋯ a) = c.emb (c.index 0) (Fin.cast ⋯ a_1.succ)
⊢ ∀ ⦃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 :
                  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 ⋯ j.succ)).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
h : i ≠ c.index 0
h_2 : Membership.mem (γ := Set (Fin c.length)) univ (c.index 0)
hij : i ≠ 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) (c.index 0))
⊢ ¬c.emb i (Fin.cast ⋯ a) = c.emb (c.index 0) (Fin.cast ⋯ b.succ)

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
h : i ≠ c.index 0
h_2 : Membership.mem (γ := Set (Fin c.length)) univ (c.index 0)
hij : i ≠ 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) (c.index 0))
⊢ ¬c.emb i (Fin.cast ⋯ a) = c.emb (c.index 0) (Fin.cast ⋯ b.succ)

Tactic:
exact c.emb_ne_emb_of_ne hij

Premises used: OrderedFinpartition.emb_ne_emb_of_ne