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 j : Fin (c.length - 1)
hij : i < j
simp :
  c.emb (Fin.cast ⋯ i.succ) (⟨c.partSize (Fin.cast ⋯ i.succ) - 1, ⋯⟩ : Fin (c.partSize (Fin.cast ⋯ i.succ))) <
    c.emb (Fin.cast ⋯ j.succ) ⟨c.partSize (Fin.cast ⋯ j.succ) - 1, ⋯⟩
⊢ LT.lt (α := Fin n)
    ((fun (m : Fin (c.length - 1)) ↦
        have this := ⋯;
        (c.emb (Fin.cast this m.succ)
              (⟨c.partSize (Fin.cast ⋯ m.succ) - 1, ⋯⟩ : Fin (c.partSize (Fin.cast ⋯ m.succ)))).pred
          ⋯)
      i)
    ((fun (m : Fin (c.length - 1)) ↦
        have this := ⋯;
        (c.emb (Fin.cast this m.succ)
              (⟨c.partSize (Fin.cast ⋯ m.succ) - 1, ⋯⟩ : Fin (c.partSize (Fin.cast ⋯ m.succ)))).pred
          ⋯)
      j)

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 j : Fin (c.length - 1)
hij : i < j
⊢ c.emb (Fin.cast ⋯ i.succ) (⟨c.partSize (Fin.cast ⋯ i.succ) - 1, ⋯⟩ : Fin (c.partSize (Fin.cast ⋯ i.succ))) <
    c.emb (Fin.cast ⋯ j.succ) ⟨c.partSize (Fin.cast ⋯ j.succ) - 1, ⋯⟩

Tactic:
apply c.parts_strictMono (cast_strictMono _ (strictMono_succ hij))

Premises used: Fin.strictMono_succ, Fin.cast_strictMono, OrderedFinpartition.parts_strictMono
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c_1 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) = {0}
i : Fin (c.length - 1)
h : Membership.mem (γ := Set (Fin (c.length - 1))) univ i
j : Fin (c.length - 1)
h_1 : Membership.mem (γ := Set (Fin (c.length - 1))) univ j
hij : i ≠ j
apply :
  ∀ ⦃a : Fin n⦄,
    Membership.mem (γ := Set (Fin n))
        ((fun (m : Fin (c.length - 1)) ↦
            (range fun (j : Fin (c.partSize (Fin.cast ⋯ m.succ))) ↦
                have this := ⋯;
                (c.emb (Fin.cast this m.succ) j).pred ⋯ :
              Set (Fin n)))
          i)
        a →
      ∀ ⦃b : Fin n⦄,
        Membership.mem (γ := Set (Fin n))
            ((fun (m : Fin (c.length - 1)) ↦
                (range fun (j : Fin (c.partSize (Fin.cast ⋯ m.succ))) ↦
                    have this := ⋯;
                    (c.emb (Fin.cast this m.succ) j).pred ⋯ :
                  Set (Fin n)))
              j)
            b →
          a ≠ b
⊢ onFun (β := Set (Fin n)) Disjoint
    (fun (m : Fin (c.length - 1)) ↦
      range fun (j : Fin (c.partSize (Fin.cast ⋯ m.succ))) ↦
        have this := ⋯;
        (c.emb (Fin.cast this m.succ) j).pred ⋯)
    i j

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 - 1)
h : Membership.mem (γ := Set (Fin (c.length - 1))) univ i
j : Fin (c.length - 1)
h_1 : Membership.mem (γ := Set (Fin (c.length - 1))) univ j
hij : i ≠ j
simp :
  ∀ (a : Fin (c.partSize (Fin.cast ⋯ i.succ))) (a_1 : Fin (c.partSize (Fin.cast ⋯ j.succ))),
    ¬c.emb (Fin.cast ⋯ i.succ) a = c.emb (Fin.cast ⋯ j.succ) a_1
⊢ ∀ ⦃a : Fin n⦄,
    Membership.mem (γ := Set (Fin n))
        ((fun (m : Fin (c.length - 1)) ↦
            (range fun (j : Fin (c.partSize (Fin.cast ⋯ m.succ))) ↦
                have this := ⋯;
                (c.emb (Fin.cast this m.succ) j).pred ⋯ :
              Set (Fin n)))
          i)
        a →
      ∀ ⦃b : Fin n⦄,
        Membership.mem (γ := Set (Fin n))
            ((fun (m : Fin (c.length - 1)) ↦
                (range fun (j : Fin (c.partSize (Fin.cast ⋯ m.succ))) ↦
                    have this := ⋯;
                    (c.emb (Fin.cast this m.succ) j).pred ⋯ :
                  Set (Fin n)))
              j)
            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 - 1)
h : Membership.mem (γ := Set (Fin (c.length - 1))) univ i
j : Fin (c.length - 1)
h_1 : Membership.mem (γ := Set (Fin (c.length - 1))) univ j
hij : i ≠ j
a : Fin (c.partSize (Fin.cast ⋯ i.succ))
b : Fin (c.partSize (Fin.cast ⋯ j.succ))
⊢ i.succ ≠ j.succ

Tactic:
simpa using 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}
i : Fin (c.length - 1)
h : Membership.mem (γ := Set (Fin (c.length - 1))) univ i
j : Fin (c.length - 1)
h_1 : Membership.mem (γ := Set (Fin (c.length - 1))) univ j
hij : i ≠ j
a : Fin (c.partSize (Fin.cast ⋯ i.succ))
b : Fin (c.partSize (Fin.cast ⋯ j.succ))
⊢ ¬c.emb (Fin.cast ⋯ i.succ) a = c.emb (Fin.cast ⋯ j.succ) b

Tactic:
exact c.emb_ne_emb_of_ne ((cast_injective _).ne (by simpa using hij))

Premises used: Function.Injective.ne, Fin.cast_injective, 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 - 1)) (y : Fin (c.partSize (Fin.cast ⋯ m.succ))), (c.emb (Fin.cast ⋯ m.succ) y).pred ⋯ = x
⊢ ∃ (m : Fin (c.length - 1)) (y : Fin (c.partSize (Fin.cast ⋯ m.succ))), (c.emb (Fin.cast ⋯ m.succ) 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
⊢ c.length = c.length - 1 + 1

Tactic:
have A : c.length = c.length - 1 + 1 :=
      (Nat.sub_add_cancel (c.length_pos (Nat.zero_lt_succ n))).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
i : Fin c.length
j : Fin (c.partSize i)
hij : c.emb i j = x.succ
A : c.length = c.length - 1 + 1
h : i = 0
rw : c.emb i j ∈ range (c.emb i)
⊢ x.succ ∈ range (c.emb i)

Tactic:
rw [← 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
i : Fin c.length
j : Fin (c.partSize i)
hij : c.emb i j = x.succ
A : c.length = c.length - 1 + 1
h : i = 0
⊢ c.emb i j ∈ range (c.emb i)

Tactic:
apply mem_range_self

Premises used: Set.mem_range_self
-- 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
A : c.length = c.length - 1 + 1
h : i = 0
⊢ x.succ ∈ range (c.emb i)

Tactic:
have : succ x ∈ range (c.emb i) := by rw [← hij]; apply mem_range_self
-- 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
A : c.length = c.length - 1 + 1
h : i = 0
this : x.succ ∈ range (c.emb i)
⊢ x.succ = 0

Tactic:
rw [h, hc, mem_singleton_iff] at this

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}
x : Fin n
i : Fin c.length
j : Fin (c.partSize i)
hij : c.emb i j = x.succ
A : c.length = c.length - 1 + 1
h : i = 0
this : x.succ = 0
⊢ False

Tactic:
Fin.succ_ne_zero _ this

Premises used: 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
i : Fin c.length
j : Fin (c.partSize i)
hij : c.emb i j = x.succ
A : c.length = c.length - 1 + 1
h : i = 0
this : x.succ = 0
⊢ False

Tactic:
exact Fin.succ_ne_zero _ this

Premises used: 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
i : Fin c.length
j : Fin (c.partSize i)
hij : c.emb i j = x.succ
A : c.length = c.length - 1 + 1
⊢ i ≠ 0

Tactic:
have i_ne : i ≠ 0 := by
      intro h
      have : succ x ∈ range (c.emb i) := by rw [← hij]; apply mem_range_self
      rw [h, hc, mem_singleton_iff] at this
      exact Fin.succ_ne_zero _ 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 : 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
A : c.length = c.length - 1 + 1
i_ne : i ≠ 0
⊢ Fin.cast A i ≠ 0

Tactic:
simpa using i_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
i : Fin c.length
j : Fin (c.partSize i)
hij : c.emb i j = x.succ
A : c.length = c.length - 1 + 1
i_ne : i ≠ 0
⊢ c.partSize i = c.partSize (Fin.cast ⋯ ((Fin.cast A i).pred ⋯).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
i : Fin c.length
j : Fin (c.partSize i)
hij : c.emb i j = x.succ
A : c.length = c.length - 1 + 1
i_ne : i ≠ 0
refine : (c.emb (Fin.cast ⋯ ((Fin.cast A i).pred ⋯).succ) (Fin.cast ⋯ j)).pred ⋯ = x
⊢ ∃ (m : Fin (c.length - 1)) (y : Fin (c.partSize (Fin.cast ⋯ m.succ))), (c.emb (Fin.cast ⋯ m.succ) y).pred ⋯ = x

Tactic:
refine ⟨pred (Fin.cast A i) (by simpa using i_ne), Fin.cast (by simp) 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
i : Fin c.length
j : Fin (c.partSize i)
hij : c.emb i j = x.succ
A : c.length = c.length - 1 + 1
i_ne : i ≠ 0
⊢ x = x.succ.pred ⋯

Tactic:
have : x = pred (succ x) (succ_ne_zero x) := 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
i : Fin c.length
j : Fin (c.partSize i)
hij : c.emb i j = x.succ
A : c.length = c.length - 1 + 1
i_ne : i ≠ 0
this : x = x.succ.pred ⋯
rw : (c.emb (Fin.cast ⋯ ((Fin.cast A i).pred ⋯).succ) (Fin.cast ⋯ j)).pred ⋯ = x.succ.pred ⋯
⊢ (c.emb (Fin.cast ⋯ ((Fin.cast A i).pred ⋯).succ) (Fin.cast ⋯ j)).pred ⋯ = x

Tactic:
rw [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 : 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
A : c.length = c.length - 1 + 1
i_ne : i ≠ 0
this : x = x.succ.pred ⋯
e_i : c.emb (Fin.cast ⋯ ((Fin.cast A i).pred ⋯).succ) (Fin.cast ⋯ j) = x.succ
⊢ (c.emb (Fin.cast ⋯ ((Fin.cast A i).pred ⋯).succ) (Fin.cast ⋯ j)).pred ⋯ = x.succ.pred ⋯

Tactic:
congr
-- 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
A : c.length = c.length - 1 + 1
i_ne : i ≠ 0
this : x = x.succ.pred ⋯
e_i : c.emb (Fin.cast ⋯ ((Fin.cast A i).pred ⋯).succ) (Fin.cast ⋯ j) = c.emb i j
⊢ c.emb (Fin.cast ⋯ ((Fin.cast A i).pred ⋯).succ) (Fin.cast ⋯ j) = x.succ

Tactic:
rw [← 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
i : Fin c.length
j : Fin (c.partSize i)
hij : c.emb i j = x.succ
A : c.length = c.length - 1 + 1
i_ne : i ≠ 0
this : x = x.succ.pred ⋯
e_i : Fin.cast ⋯ ((Fin.cast A i).pred ⋯).succ = i
e_i₁ : HEq (α := Fin (c.partSize (Fin.cast ⋯ ((Fin.cast A i).pred ⋯).succ))) (Fin.cast ⋯ j) j
⊢ c.emb (Fin.cast ⋯ ((Fin.cast A i).pred ⋯).succ) (Fin.cast ⋯ j) = c.emb i j

Tactic:
congr 1
-- 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
A : c.length = c.length - 1 + 1
i_ne : i ≠ 0
this : x = x.succ.pred ⋯
⊢ Fin.cast ⋯ ((Fin.cast A i).pred ⋯).succ = i

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
i : Fin c.length
j : Fin (c.partSize i)
hij : c.emb i j = x.succ
A : c.length = c.length - 1 + 1
i_ne : i ≠ 0
this : x = x.succ.pred ⋯
⊢ HEq (α := Fin (c.partSize (Fin.cast ⋯ ((Fin.cast A i).pred ⋯).succ))) (Fin.cast ⋯ j) j

Tactic:
simp [Fin.heq_ext_iff]

Premises used: Fin.heq_ext_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
inl : 0 < update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0)
inr :
  ∀ (hi : i ≠ c.index 0),
    0 < update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i
⊢ 0 < update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i

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

Premises used: OrderedFinpartition.index, eq_or_ne, OfNat.ofNat, rfl