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 1
h₁ : c.length = 1
⊢ ∀ (i : Fin c.length), c.partSize i = 1

Tactic:
have h₂ (i) : c.partSize i = 1 := le_antisymm (c.partSize_le _) (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 1
h₁ : c.length = 1
h₂ : ∀ (i : Fin c.length), c.partSize i = 1
⊢ ∀ (i : Fin c.length) (j : Fin (c.partSize i)), c.emb i j = 0

Tactic:
have h₃ (i j) : c.emb i j = 0 := Subsingleton.elim _ _
-- 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 : OrderedFinpartition n
partSize : Fin 1 → ℕ
partSize_pos : ∀ (m : Fin 1), 0 < partSize m
emb : (m : Fin 1) → Fin (partSize m) → Fin 1
emb_strictMono : ∀ (m : Fin 1), StrictMono (emb m)
parts_strictMono : StrictMono (β := Fin 1) fun (m : Fin 1) ↦ emb m (⟨partSize m - 1, ⋯⟩ : Fin (partSize m))
disjoint : PairwiseDisjoint (α := Set (Fin 1)) univ fun (m : Fin 1) ↦ range (emb m)
cover : ∀ (x : Fin 1), ∃ (m : Fin 1), x ∈ range (emb m)
h₂ :
  ∀
    (i :
      Fin
        { length := 1, partSize := partSize, partSize_pos := partSize_pos, emb := emb, emb_strictMono := emb_strictMono,
            parts_strictMono := parts_strictMono, disjoint := disjoint, cover := cover :
            OrderedFinpartition 1 }.length),
    { length := 1, partSize := partSize, partSize_pos := partSize_pos, emb := emb, emb_strictMono := emb_strictMono,
            parts_strictMono := parts_strictMono, disjoint := disjoint, cover := cover :
            OrderedFinpartition 1 }.partSize
        i =
      1
h₃ :
  ∀
    (i :
      Fin
        { length := 1, partSize := partSize, partSize_pos := partSize_pos, emb := emb, emb_strictMono := emb_strictMono,
            parts_strictMono := parts_strictMono, disjoint := disjoint, cover := cover : OrderedFinpartition 1 }.length)
    (j :
      Fin
        ({ length := 1, partSize := partSize, partSize_pos := partSize_pos, emb := emb,
              emb_strictMono := emb_strictMono, parts_strictMono := parts_strictMono, disjoint := disjoint,
              cover := cover : OrderedFinpartition 1 }.partSize
          i)),
    { length := 1, partSize := partSize, partSize_pos := partSize_pos, emb := emb, emb_strictMono := emb_strictMono,
            parts_strictMono := parts_strictMono, disjoint := disjoint, cover := cover : OrderedFinpartition 1 }.emb
        i j =
      0
⊢ partSize = fun (x : Fin 1) ↦ 1

Tactic:
funext h₂

Premises used: funext
-- 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 : OrderedFinpartition n
partSize_pos : ∀ (m : Fin 1), LT.lt (α := ℕ) 0 ((fun (x : Fin 1) ↦ (1 : ℕ)) m)
emb : (m : Fin 1) → Fin ((fun (x : Fin 1) ↦ (1 : ℕ)) m) → Fin 1
emb_strictMono : ∀ (m : Fin 1), StrictMono (emb m)
parts_strictMono :
  StrictMono (β := Fin 1) fun (m : Fin 1) ↦
    emb m (⟨HSub.hSub (α := ℕ) ((fun (x : Fin 1) ↦ (1 : ℕ)) m) 1, ⋯⟩ : Fin ((fun (x : Fin 1) ↦ (1 : ℕ)) m))
disjoint : PairwiseDisjoint (α := Set (Fin 1)) univ fun (m : Fin 1) ↦ range (emb m)
cover : ∀ (x : Fin 1), ∃ (m : Fin 1), x ∈ range (emb m)
h₂ :
  ∀
    (i :
      Fin
        { length := 1, partSize := fun (x : Fin 1) ↦ 1, partSize_pos := partSize_pos, emb := emb,
            emb_strictMono := emb_strictMono, parts_strictMono := parts_strictMono, disjoint := disjoint,
            cover := cover : OrderedFinpartition 1 }.length),
    { length := 1, partSize := fun (x : Fin 1) ↦ 1, partSize_pos := partSize_pos, emb := emb,
            emb_strictMono := emb_strictMono, parts_strictMono := parts_strictMono, disjoint := disjoint,
            cover := cover : OrderedFinpartition 1 }.partSize
        i =
      1
h₃ :
  ∀
    (i :
      Fin
        { length := 1, partSize := fun (x : Fin 1) ↦ 1, partSize_pos := partSize_pos, emb := emb,
            emb_strictMono := emb_strictMono, parts_strictMono := parts_strictMono, disjoint := disjoint,
            cover := cover : OrderedFinpartition 1 }.length)
    (j :
      Fin
        ({ length := 1, partSize := fun (x : Fin 1) ↦ 1, partSize_pos := partSize_pos, emb := emb,
              emb_strictMono := emb_strictMono, parts_strictMono := parts_strictMono, disjoint := disjoint,
              cover := cover : OrderedFinpartition 1 }.partSize
          i)),
    { length := 1, partSize := fun (x : Fin 1) ↦ 1, partSize_pos := partSize_pos, emb := emb,
            emb_strictMono := emb_strictMono, parts_strictMono := parts_strictMono, disjoint := disjoint,
            cover := cover : OrderedFinpartition 1 }.emb
        i j =
      0
⊢ { length := 1, partSize := fun (x : Fin 1) ↦ 1, partSize_pos := partSize_pos, emb := emb,
      emb_strictMono := emb_strictMono, parts_strictMono := parts_strictMono, disjoint := disjoint, cover := cover :
      OrderedFinpartition 1 } =
    default

Tactic:
simpa [OrderedFinpartition.ext_iff, funext_iff, Fin.forall_fin_one] using h₃ _ _

Premises used: Fin.forall_fin_one, funext_iff, OrderedFinpartition.ext_iff
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition n
inst : NeZero n
apply : c.emb (c.index 0) 0 ≤ 0
⊢ c.emb (c.index 0) 0 = 0

Tactic:
apply le_antisymm _ (Fin.zero_le _)

Premises used: Fin.zero_le, le_antisymm
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition n
inst : NeZero n
rw : c.emb (c.index 0) (c.invEmbedding 0)
| 0

Tactic:
rw [← c.emb_invEmbedding 0]

Premises used: OrderedFinpartition.emb_invEmbedding, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition n
inst : NeZero n
conv_rhs : c.emb (c.index 0) 0 ≤ c.emb (c.index 0) (c.invEmbedding 0)
⊢ c.emb (c.index 0) 0 ≤ 0

Tactic:
conv_rhs => rw [← c.emb_invEmbedding 0]

Premises used: OrderedFinpartition.emb_invEmbedding, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition n
inst : NeZero n
⊢ c.emb (c.index 0) 0 ≤ c.emb (c.index 0) (c.invEmbedding 0)

Tactic:
apply (c.emb_strictMono _).monotone (Fin.zero_le _)

Premises used: StrictMono.monotone, Fin.zero_le, OrderedFinpartition.emb_strictMono
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition n
i : Fin c.length
j : Fin n
hc : range (c.emb i) = {j}
⊢ Fintype.card (↑(range (c.emb i)) : Type) = Fintype.card (Fin (c.partSize i))

Tactic:
have : Fintype.card (range (c.emb i)) = Fintype.card (Fin (c.partSize i)) :=
    card_range_of_injective (c.emb_strictMono i).injective
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition n
i : Fin c.length
j : Fin n
hc : range (c.emb i) = {j}
this : Fintype.card (↑(range (c.emb i)) : Type) = Fintype.card (Fin (c.partSize i))
⊢ c.partSize i = 1

Tactic:
simpa [hc] using this.symm

Premises used: Eq.symm
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
rw : c.partSize (c.index 0) = Nat.card (Fin (c.partSize (c.index 0)))
⊢ c.partSize (c.index 0) = Nat.card (↑(range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))) : Type)

Tactic:
rw [Nat.card_range_of_injective (c.emb_strictMono _).injective]

Premises used: StrictMono.injective, OrderedFinpartition.emb_strictMono, Nat.card_range_of_injective
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
⊢ c.partSize (c.index 0) = Nat.card (Fin (c.partSize (c.index 0)))

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
⊢ c.partSize (c.index 0) = Nat.card (↑(range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))) : Type)

Tactic:
have : c.partSize (c.index 0) = Nat.card (range (c.emb (c.index 0))) := by
    rw [Nat.card_range_of_injective (c.emb_strictMono _).injective]; simp
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
this : c.partSize (c.index 0) = Nat.card (↑(range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))) : Type)
rw : 1 < Nat.card (↑(range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))) : Type)
⊢ 1 < c.partSize (c.index 0)

Tactic:
rw [this]
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
this : c.partSize (c.index 0) = Nat.card (↑(range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))) : Type)
inl : ∀ (h : c.index 0 = 0), 1 < Nat.card (↑(range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))) : Type)
inr : ∀ (h : c.index 0 ≠ 0), 1 < Nat.card (↑(range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))) : Type)
⊢ 1 < Nat.card (↑(range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))) : Type)

Tactic:
rcases eq_or_ne (c.index 0) 0 with h | h

Premises used: OrderedFinpartition.index, eq_or_ne, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
this : c.partSize (c.index 0) = Nat.card (↑(range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))) : Type)
h : c.index 0 = 0
⊢ range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0)) ≠ {0}

Tactic:
rw [← h] at hc
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
this : c.partSize (c.index 0) = Nat.card (↑(range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))) : Type)
h : c.index 0 = 0
hc₁ : range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0)) ≠ {0}
⊢ c.partSize (c.index 0) = Nat.card (↑(range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))) : Type)

Tactic:
rw [← h] at hc
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
this : c.partSize (c.index 0) = Nat.card (↑(range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))) : Type)
h : c.index 0 = 0
hc₁ : range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0)) ≠ {0}
this₁ : c.partSize (c.index 0) = Nat.card (↑(range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))) : Type)
⊢ c.index 0 = 0

Tactic:
rw [← h] at hc
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0)) ≠ {0}
this : c.partSize (c.index 0) = Nat.card (↑(range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))) : Type)
h : c.index 0 = 0
apply : {0} ⊆ range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))
⊢ {0} ⊂ range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))

Tactic:
apply ssubset_of_subset_of_ne ?_ hc.symm

Premises used: Ne.symm, ssubset_of_subset_of_ne
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0)) ≠ {0}
this : c.partSize (c.index 0) = Nat.card (↑(range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))) : Type)
h : c.index 0 = 0
⊢ {0} ⊆ range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))

Tactic:
simpa only [singleton_subset_iff, mem_range] using ⟨0, emb_zero c⟩

Premises used: Set.singleton_subset_iff, Set.mem_range
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0)) ≠ {0}
this : c.partSize (c.index 0) = Nat.card (↑(range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))) : Type)
h : c.index 0 = 0
⊢ {0} ⊂ range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))

Tactic:
have : {0} ⊂ range (c.emb (c.index 0)) := by
      apply ssubset_of_subset_of_ne ?_ hc.symm
      simpa only [singleton_subset_iff, mem_range] using ⟨0, emb_zero c⟩
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0)) ≠ {0}
this_1 : c.partSize (c.index 0) = Nat.card (↑(range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))) : Type)
h : c.index 0 = 0
this : {0} ⊂ range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))
⊢ 1 < Nat.card (↑(range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))) : Type)

Tactic:
simpa using Set.Finite.card_lt_card (finite_range _) this

Premises used: Set.Finite.card_lt_card, Set.finite_range
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
this : c.partSize (c.index 0) = Nat.card (↑(range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))) : Type)
h : c.index 0 ≠ 0
⊢ {c.emb (c.index 0) 0, c.emb (c.index 0) (⟨c.partSize (c.index 0) - 1, ⋯⟩ : Fin (c.partSize (c.index 0)))} ⊆
    range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))

Tactic:
simp [insert_subset]

Premises used: Set.insert_subset
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
this : c.partSize (c.index 0) = Nat.card (↑(range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))) : Type)
h : c.index 0 ≠ 0
⊢ {c.emb (c.index 0) 0, c.emb (c.index 0) (⟨c.partSize (c.index 0) - 1, ⋯⟩ : Fin (c.partSize (c.index 0)))} ⊆
    range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))

Tactic:
have : {c.emb (c.index 0) 0,
        c.emb (c.index 0) ⟨c.partSize (c.index 0) - 1, Nat.sub_one_lt_of_lt (c.partSize_pos _)⟩}
          ⊆ range (c.emb (c.index 0)) := by simp [insert_subset]
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
this_1 : c.partSize (c.index 0) = Nat.card (↑(range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))) : Type)
h : c.index 0 ≠ 0
this :
  {c.emb (c.index 0) 0, c.emb (c.index 0) (⟨c.partSize (c.index 0) - 1, ⋯⟩ : Fin (c.partSize (c.index 0)))} ⊆
    range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))
⊢ {0, c.emb (c.index 0) (⟨c.partSize (c.index 0) - 1, ⋯⟩ : Fin (c.partSize (c.index 0)))} ⊆
    range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))

Tactic:
simp only [emb_zero] at this

Premises used: OrderedFinpartition.emb_zero
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
this_1 : c.partSize (c.index 0) = Nat.card (↑(range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))) : Type)
h : c.index 0 ≠ 0
this :
  {0, c.emb (c.index 0) (⟨c.partSize (c.index 0) - 1, ⋯⟩ : Fin (c.partSize (c.index 0)))} ⊆
    range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))
⊢ Nat.card (↑{0, c.emb (c.index 0) (⟨c.partSize (c.index 0) - 1, ⋯⟩ : Fin (c.partSize (c.index 0)))} : Type) ≤
    Nat.card (↑(range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))) : Type)

Tactic:
Nat.card_mono Subtype.finite this

Premises used: Subtype.finite, Nat.card_mono
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
this_1 : c.partSize (c.index 0) = Nat.card (↑(range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))) : Type)
h : c.index 0 ≠ 0
this :
  {0, c.emb (c.index 0) (⟨c.partSize (c.index 0) - 1, ⋯⟩ : Fin (c.partSize (c.index 0)))} ⊆
    range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))
h₁ : 2 = Nat.card (↑{0, c.emb (c.index 0) (⟨c.partSize (c.index 0) - 1, ⋯⟩ : Fin (c.partSize (c.index 0)))} : Type)
⊢ 2 ≤ Nat.card (↑(range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))) : Type)

Tactic:
convert! Nat.card_mono Subtype.finite this

Premises used: Subtype.finite, Nat.card_mono
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
this_1 : c.partSize (c.index 0) = Nat.card (↑(range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))) : Type)
h : c.index 0 ≠ 0
this :
  {0, c.emb (c.index 0) (⟨c.partSize (c.index 0) - 1, ⋯⟩ : Fin (c.partSize (c.index 0)))} ⊆
    range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))
h₁ :
  2 =
    Finset.card (α := Fin (n + 1))
      {0, c.emb (c.index 0) (⟨c.partSize (c.index 0) - 1, ⋯⟩ : Fin (c.partSize (c.index 0)))}
⊢ 2 = Nat.card (↑{0, c.emb (c.index 0) (⟨c.partSize (c.index 0) - 1, ⋯⟩ : Fin (c.partSize (c.index 0)))} : Type)

Tactic:
simp only [Nat.card_eq_fintype_card, Fintype.card_ofFinset, toFinset_singleton]

Premises used: Fintype.card_ofFinset, Set.toFinset_singleton, Nat.card_eq_fintype_card
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
this_1 : c.partSize (c.index 0) = Nat.card (↑(range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))) : Type)
h : c.index 0 ≠ 0
this :
  {0, c.emb (c.index 0) (⟨c.partSize (c.index 0) - 1, ⋯⟩ : Fin (c.partSize (c.index 0)))} ⊆
    range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))
apply : 0 ≠ c.emb (c.index 0) (⟨c.partSize (c.index 0) - 1, ⋯⟩ : Fin (c.partSize (c.index 0)))
⊢ 2 =
    Finset.card (α := Fin (n + 1))
      {0, c.emb (c.index 0) (⟨c.partSize (c.index 0) - 1, ⋯⟩ : Fin (c.partSize (c.index 0)))}

Tactic:
apply (Finset.card_pair ?_).symm

Premises used: Finset.card_pair, Eq.symm
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
this_1 : c.partSize (c.index 0) = Nat.card (↑(range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))) : Type)
h : c.index 0 ≠ 0
this :
  {0, c.emb (c.index 0) (⟨c.partSize (c.index 0) - 1, ⋯⟩ : Fin (c.partSize (c.index 0)))} ⊆
    range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))
⊢ 0 ≠ c.emb (c.index 0) (⟨c.partSize (c.index 0) - 1, ⋯⟩ : Fin (c.partSize (c.index 0)))

Tactic:
((Fin.zero_le _).trans_lt (c.parts_strictMono ((pos_iff_ne_zero' (c.index 0)).mpr h))).ne

Premises used: Iff.mpr, OrderedFinpartition.index, Fin.zero_le, OrderedFinpartition.parts_strictMono, OfNat.ofNat, LE.le.trans_lt, Fin.pos_iff_ne_zero', LT.lt.ne
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
this_1 : c.partSize (c.index 0) = Nat.card (↑(range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))) : Type)
h : c.index 0 ≠ 0
this :
  {0, c.emb (c.index 0) (⟨c.partSize (c.index 0) - 1, ⋯⟩ : Fin (c.partSize (c.index 0)))} ⊆
    range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))
⊢ 0 ≠ c.emb (c.index 0) (⟨c.partSize (c.index 0) - 1, ⋯⟩ : Fin (c.partSize (c.index 0)))

Tactic:
exact ((Fin.zero_le _).trans_lt (c.parts_strictMono ((pos_iff_ne_zero' (c.index 0)).mpr h))).ne

Premises used: Iff.mpr, OrderedFinpartition.index, Fin.zero_le, OrderedFinpartition.parts_strictMono, OfNat.ofNat, LE.le.trans_lt, Fin.pos_iff_ne_zero', LT.lt.ne
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c_1 c : OrderedFinpartition n
⊢ LT.lt (α := ℕ) (0 : ℕ) (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize 0 : ℕ)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c_1 c : OrderedFinpartition n
⊢ ∀ (i : Fin c.length), LT.lt (α := ℕ) (0 : ℕ) (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize i.succ : ℕ)

Tactic:
simp [c.partSize_pos]

Premises used: OrderedFinpartition.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 c : OrderedFinpartition n
⊢ ∀ (m : Fin (c.length + 1)),
    StrictMono (α := Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize m)) (β := Fin (n + 1))
      (cases (motive := fun (x : Fin (c.length + 1)) ↦
        Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize x) → Fin (n + 1))
        (fun (x : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize 0)) ↦ 0)
        (fun (m : Fin c.length) ↦ succ ∘ c.emb m) m)

Tactic:
Fin.cases ?_ (fun i ↦ ?_)

Premises used: Fin.cases