awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n plength : ℕ
psize : Fin plength → ℕ
partSize_pos : ∀ (m : Fin plength), 0 < psize m
pemb : (m : Fin plength) → Fin (psize m) → Fin n
emb_strictMono : ∀ (m : Fin plength), StrictMono (pemb m)
parts_strictMono : StrictMono (β := Fin n) fun (m : Fin plength) ↦ pemb m (⟨psize m - 1, ⋯⟩ : Fin (psize m))
disjoint : PairwiseDisjoint (α := Set (Fin n)) univ fun (m : Fin plength) ↦ range (pemb m)
cover : ∀ (x : Fin n), ∃ (m : Fin plength), x ∈ range (pemb m)
qlength : ℕ
qsize : Fin qlength → ℕ
partSize_pos_1 : ∀ (m : Fin qlength), 0 < qsize m
qemb : (m : Fin qlength) → Fin (qsize m) → Fin n
emb_strictMono_1 : ∀ (m : Fin qlength), StrictMono (qemb m)
parts_strictMono_1 : StrictMono (β := Fin n) fun (m : Fin qlength) ↦ qemb m (⟨qsize m - 1, ⋯⟩ : Fin (qsize m))
disjoint_1 : PairwiseDisjoint (α := Set (Fin n)) univ fun (m : Fin qlength) ↦ range (qemb m)
cover_1 : ∀ (x : Fin n), ∃ (m : Fin qlength), x ∈ range (qemb m)
hpq :
  plength = qlength ∧
    HEq (α := (p : Fin plength → Fin (n + 1)) × ((i : Fin plength) → Fin (↑(p i) : ℕ) → Fin n))
      (Sigma.mk (β := fun (p : Fin plength → Fin (n + 1)) ↦ (i : Fin plength) → Fin (↑(p i) : ℕ) → Fin n)
        (fun (m : Fin plength) ↦ ⟨psize m, ⋯⟩) fun (j : Fin plength) ↦ pemb j)
      (β := (p : Fin qlength → Fin (n + 1)) × ((i : Fin qlength) → Fin (↑(p i) : ℕ) → Fin n))
      (Sigma.mk (β := fun (p : Fin qlength → Fin (n + 1)) ↦ (i : Fin qlength) → Fin (↑(p i) : ℕ) → Fin n)
        (fun (m : Fin qlength) ↦ ⟨qsize m, ⋯⟩) fun (j : Fin qlength) ↦ qemb j)
⊢ plength = qlength

Tactic:
have : plength = qlength := hpq.1
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n plength : ℕ
psize : Fin plength → ℕ
partSize_pos : ∀ (m : Fin plength), 0 < psize m
pemb : (m : Fin plength) → Fin (psize m) → Fin n
emb_strictMono : ∀ (m : Fin plength), StrictMono (pemb m)
parts_strictMono : StrictMono (β := Fin n) fun (m : Fin plength) ↦ pemb m (⟨psize m - 1, ⋯⟩ : Fin (psize m))
disjoint : PairwiseDisjoint (α := Set (Fin n)) univ fun (m : Fin plength) ↦ range (pemb m)
cover : ∀ (x : Fin n), ∃ (m : Fin plength), x ∈ range (pemb m)
qlength : ℕ
qsize : Fin qlength → ℕ
partSize_pos_1 : ∀ (m : Fin qlength), 0 < qsize m
qemb : (m : Fin qlength) → Fin (qsize m) → Fin n
emb_strictMono_1 : ∀ (m : Fin qlength), StrictMono (qemb m)
parts_strictMono_1 : StrictMono (β := Fin n) fun (m : Fin qlength) ↦ qemb m (⟨qsize m - 1, ⋯⟩ : Fin (qsize m))
disjoint_1 : PairwiseDisjoint (α := Set (Fin n)) univ fun (m : Fin qlength) ↦ range (qemb m)
cover_1 : ∀ (x : Fin n), ∃ (m : Fin qlength), x ∈ range (qemb m)
hpq :
  plength = qlength ∧
    HEq (α := (p : Fin plength → Fin (n + 1)) × ((i : Fin plength) → Fin (↑(p i) : ℕ) → Fin n))
      (Sigma.mk (β := fun (p : Fin plength → Fin (n + 1)) ↦ (i : Fin plength) → Fin (↑(p i) : ℕ) → Fin n)
        (fun (m : Fin plength) ↦ ⟨psize m, ⋯⟩) fun (j : Fin plength) ↦ pemb j)
      (β := (p : Fin qlength → Fin (n + 1)) × ((i : Fin qlength) → Fin (↑(p i) : ℕ) → Fin n))
      (Sigma.mk (β := fun (p : Fin qlength → Fin (n + 1)) ↦ (i : Fin qlength) → Fin (↑(p i) : ℕ) → Fin n)
        (fun (m : Fin qlength) ↦ ⟨qsize m, ⋯⟩) fun (j : Fin qlength) ↦ qemb j)
this : plength = qlength
subst :
  ∀ (qsize : Fin plength → ℕ) (partSize_pos_2 : ∀ (m : Fin plength), 0 < qsize m)
    (qemb : (m : Fin plength) → Fin (qsize m) → Fin n) (emb_strictMono_2 : ∀ (m : Fin plength), StrictMono (qemb m))
    (parts_strictMono_2 : StrictMono (β := Fin n) fun (m : Fin plength) ↦ qemb m (⟨qsize m - 1, ⋯⟩ : Fin (qsize m)))
    (disjoint_2 : PairwiseDisjoint (α := Set (Fin n)) univ fun (m : Fin plength) ↦ range (qemb m))
    (cover_2 : ∀ (x : Fin n), ∃ (m : Fin plength), x ∈ range (qemb m))
    (hpq :
      plength = plength ∧
        HEq (α := (p : Fin plength → Fin (n + 1)) × ((i : Fin plength) → Fin (↑(p i) : ℕ) → Fin n))
          (Sigma.mk (β := fun (p : Fin plength → Fin (n + 1)) ↦ (i : Fin plength) → Fin (↑(p i) : ℕ) → Fin n)
            (fun (m : Fin plength) ↦ ⟨psize m, ⋯⟩) fun (j : Fin plength) ↦ pemb j)
          (β := (p : Fin plength → Fin (n + 1)) × ((i : Fin plength) → Fin (↑(p i) : ℕ) → Fin n))
          (Sigma.mk (β := fun (p : Fin plength → Fin (n + 1)) ↦ (i : Fin plength) → Fin (↑(p i) : ℕ) → Fin n)
            (fun (m : Fin plength) ↦ ⟨qsize m, ⋯⟩) fun (j : Fin plength) ↦ qemb j)),
    psize ≍ qsize ∧ pemb ≍ qemb
⊢ psize ≍ qsize ∧ pemb ≍ qemb

Tactic:
subst this
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n plength : ℕ
psize : Fin plength → ℕ
partSize_pos : ∀ (m : Fin plength), 0 < psize m
pemb : (m : Fin plength) → Fin (psize m) → Fin n
emb_strictMono : ∀ (m : Fin plength), StrictMono (pemb m)
parts_strictMono : StrictMono (β := Fin n) fun (m : Fin plength) ↦ pemb m (⟨psize m - 1, ⋯⟩ : Fin (psize m))
disjoint : PairwiseDisjoint (α := Set (Fin n)) univ fun (m : Fin plength) ↦ range (pemb m)
cover : ∀ (x : Fin n), ∃ (m : Fin plength), x ∈ range (pemb m)
qsize : Fin plength → ℕ
partSize_pos_1 : ∀ (m : Fin plength), 0 < qsize m
qemb : (m : Fin plength) → Fin (qsize m) → Fin n
emb_strictMono_1 : ∀ (m : Fin plength), StrictMono (qemb m)
parts_strictMono_1 : StrictMono (β := Fin n) fun (m : Fin plength) ↦ qemb m (⟨qsize m - 1, ⋯⟩ : Fin (qsize m))
disjoint_1 : PairwiseDisjoint (α := Set (Fin n)) univ fun (m : Fin plength) ↦ range (qemb m)
cover_1 : ∀ (x : Fin n), ∃ (m : Fin plength), x ∈ range (qemb m)
hpq :
  plength = plength ∧
    HEq (α := (p : Fin plength → Fin (n + 1)) × ((i : Fin plength) → Fin (↑(p i) : ℕ) → Fin n))
      (Sigma.mk (β := fun (p : Fin plength → Fin (n + 1)) ↦ (i : Fin plength) → Fin (↑(p i) : ℕ) → Fin n)
        (fun (m : Fin plength) ↦ ⟨psize m, ⋯⟩) fun (j : Fin plength) ↦ pemb j)
      (β := (p : Fin plength → Fin (n + 1)) × ((i : Fin plength) → Fin (↑(p i) : ℕ) → Fin n))
      (Sigma.mk (β := fun (p : Fin plength → Fin (n + 1)) ↦ (i : Fin plength) → Fin (↑(p i) : ℕ) → Fin n)
        (fun (m : Fin plength) ↦ ⟨qsize m, ⋯⟩) fun (j : Fin plength) ↦ qemb j)
simp_all :
  ∀
    (hpq :
      (Eq (α := Fin plength → Fin (n + 1)) (fun (m : Fin plength) ↦ ⟨psize m, ⋯⟩) fun (m : Fin plength) ↦
          ⟨qsize m, ⋯⟩) ∧
        HEq (α := (i : Fin plength) → Fin (psize i) → Fin n) fun (j : Fin plength) ↦ pemb j (β :=
          (i : Fin plength) → Fin (qsize i) → Fin n) fun (j : Fin plength) ↦ qemb j),
    psize = qsize
⊢ psize ≍ qsize ∧ pemb ≍ qemb

Tactic:
simp_all only [Sigma.mk.inj_iff, heq_eq_eq, true_and, and_true]

Premises used: and_true, heq_eq_eq, Sigma.mk.inj_iff, true_and
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n plength : ℕ
psize : Fin plength → ℕ
partSize_pos : ∀ (m : Fin plength), 0 < psize m
pemb : (m : Fin plength) → Fin (psize m) → Fin n
emb_strictMono : ∀ (m : Fin plength), StrictMono (pemb m)
parts_strictMono : StrictMono (β := Fin n) fun (m : Fin plength) ↦ pemb m (⟨psize m - 1, ⋯⟩ : Fin (psize m))
disjoint : PairwiseDisjoint (α := Set (Fin n)) univ fun (m : Fin plength) ↦ range (pemb m)
cover : ∀ (x : Fin n), ∃ (m : Fin plength), x ∈ range (pemb m)
qsize : Fin plength → ℕ
partSize_pos_1 : ∀ (m : Fin plength), 0 < qsize m
qemb : (m : Fin plength) → Fin (qsize m) → Fin n
emb_strictMono_1 : ∀ (m : Fin plength), StrictMono (qemb m)
parts_strictMono_1 : StrictMono (β := Fin n) fun (m : Fin plength) ↦ qemb m (⟨qsize m - 1, ⋯⟩ : Fin (qsize m))
disjoint_1 : PairwiseDisjoint (α := Set (Fin n)) univ fun (m : Fin plength) ↦ range (qemb m)
cover_1 : ∀ (x : Fin n), ∃ (m : Fin plength), x ∈ range (qemb m)
hpq :
  (Eq (α := Fin plength → Fin (n + 1)) (fun (m : Fin plength) ↦ ⟨psize m, ⋯⟩) fun (m : Fin plength) ↦ ⟨qsize m, ⋯⟩) ∧
    HEq (α := (i : Fin plength) → Fin (psize i) → Fin n) fun (j : Fin plength) ↦ pemb j (β :=
      (i : Fin plength) → Fin (qsize i) → Fin n) fun (j : Fin plength) ↦ qemb j
h : ∀ (i : Fin plength), psize i = qsize i
⊢ psize = qsize

Tactic:
ext i
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n plength : ℕ
psize : Fin plength → ℕ
partSize_pos : ∀ (m : Fin plength), 0 < psize m
pemb : (m : Fin plength) → Fin (psize m) → Fin n
emb_strictMono : ∀ (m : Fin plength), StrictMono (pemb m)
parts_strictMono : StrictMono (β := Fin n) fun (m : Fin plength) ↦ pemb m (⟨psize m - 1, ⋯⟩ : Fin (psize m))
disjoint : PairwiseDisjoint (α := Set (Fin n)) univ fun (m : Fin plength) ↦ range (pemb m)
cover : ∀ (x : Fin n), ∃ (m : Fin plength), x ∈ range (pemb m)
qsize : Fin plength → ℕ
partSize_pos_1 : ∀ (m : Fin plength), 0 < qsize m
qemb : (m : Fin plength) → Fin (qsize m) → Fin n
emb_strictMono_1 : ∀ (m : Fin plength), StrictMono (qemb m)
parts_strictMono_1 : StrictMono (β := Fin n) fun (m : Fin plength) ↦ qemb m (⟨qsize m - 1, ⋯⟩ : Fin (qsize m))
disjoint_1 : PairwiseDisjoint (α := Set (Fin n)) univ fun (m : Fin plength) ↦ range (qemb m)
cover_1 : ∀ (x : Fin n), ∃ (m : Fin plength), x ∈ range (qemb m)
hpq :
  (Eq (α := Fin plength → Fin (n + 1)) (fun (m : Fin plength) ↦ ⟨psize m, ⋯⟩) fun (m : Fin plength) ↦ ⟨qsize m, ⋯⟩) ∧
    HEq (α := (i : Fin plength) → Fin (psize i) → Fin n) fun (j : Fin plength) ↦ pemb j (β :=
      (i : Fin plength) → Fin (qsize i) → Fin n) fun (j : Fin plength) ↦ qemb j
i : Fin plength
⊢ psize i = qsize i

Tactic:
mk.inj_iff.mp (congr_fun hpq.1 i)

Premises used: And.left, Iff.mp, congr_fun, Fin.mk.inj_iff
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n plength : ℕ
psize : Fin plength → ℕ
partSize_pos : ∀ (m : Fin plength), 0 < psize m
pemb : (m : Fin plength) → Fin (psize m) → Fin n
emb_strictMono : ∀ (m : Fin plength), StrictMono (pemb m)
parts_strictMono : StrictMono (β := Fin n) fun (m : Fin plength) ↦ pemb m (⟨psize m - 1, ⋯⟩ : Fin (psize m))
disjoint : PairwiseDisjoint (α := Set (Fin n)) univ fun (m : Fin plength) ↦ range (pemb m)
cover : ∀ (x : Fin n), ∃ (m : Fin plength), x ∈ range (pemb m)
qsize : Fin plength → ℕ
partSize_pos_1 : ∀ (m : Fin plength), 0 < qsize m
qemb : (m : Fin plength) → Fin (qsize m) → Fin n
emb_strictMono_1 : ∀ (m : Fin plength), StrictMono (qemb m)
parts_strictMono_1 : StrictMono (β := Fin n) fun (m : Fin plength) ↦ qemb m (⟨qsize m - 1, ⋯⟩ : Fin (qsize m))
disjoint_1 : PairwiseDisjoint (α := Set (Fin n)) univ fun (m : Fin plength) ↦ range (qemb m)
cover_1 : ∀ (x : Fin n), ∃ (m : Fin plength), x ∈ range (qemb m)
hpq :
  (Eq (α := Fin plength → Fin (n + 1)) (fun (m : Fin plength) ↦ ⟨psize m, ⋯⟩) fun (m : Fin plength) ↦ ⟨qsize m, ⋯⟩) ∧
    HEq (α := (i : Fin plength) → Fin (psize i) → Fin n) fun (j : Fin plength) ↦ pemb j (β :=
      (i : Fin plength) → Fin (qsize i) → Fin n) fun (j : Fin plength) ↦ qemb j
i : Fin plength
⊢ psize i = qsize i

Tactic:
exact mk.inj_iff.mp (congr_fun hpq.1 i)

Premises used: And.left, Iff.mp, congr_fun, Fin.mk.inj_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 : OrderedFinpartition n
⊢ Subsingleton (OrderedFinpartition 0)

Tactic:
have : Subsingleton (OrderedFinpartition 0) :=
    Fintype.card_le_one_iff_subsingleton.mp (Fintype.card_le_of_injective _ (injective_embSigma 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 : OrderedFinpartition n
this : Subsingleton (OrderedFinpartition 0)
⊢ Unique (OrderedFinpartition 0)

Tactic:
exact Unique.mk' (OrderedFinpartition 0)

Premises used: OrderedFinpartition, Unique.mk', OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition n
j : Fin n
rcases :
  ∀ (m : Fin c.length) (r : Fin (c.partSize m)) (hmr : c.emb m r = j),
    ∃ (p : (m : Fin c.length) × Fin (c.partSize m)),
      c.emb (p.fst (β := fun (m : Fin c.length) ↦ Fin (c.partSize m)))
          (p.snd (β := fun (m : Fin c.length) ↦ Fin (c.partSize m))) =
        j
⊢ ∃ (p : (m : Fin c.length) × Fin (c.partSize m)),
    c.emb (p.fst (β := fun (m : Fin c.length) ↦ Fin (c.partSize m)))
        (p.snd (β := fun (m : Fin c.length) ↦ Fin (c.partSize m))) =
      j

Tactic:
rcases c.cover j with ⟨m, r, hmr⟩

Premises used: OrderedFinpartition.cover
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition n
j : Fin n
m : Fin c.length
r : Fin (c.partSize m)
hmr : c.emb m r = j
⊢ ∃ (p : (m : Fin c.length) × Fin (c.partSize m)),
    c.emb (p.fst (β := fun (m : Fin c.length) ↦ Fin (c.partSize m)))
        (p.snd (β := fun (m : Fin c.length) ↦ Fin (c.partSize m))) =
      j

Tactic:
⟨⟨m, r⟩, hmr⟩

Premises used: Exists.intro, Sigma.mk
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition n
j : Fin n
m : Fin c.length
r : Fin (c.partSize m)
hmr : c.emb m r = j
⊢ ∃ (p : (m : Fin c.length) × Fin (c.partSize m)),
    c.emb (p.fst (β := fun (m : Fin c.length) ↦ Fin (c.partSize m)))
        (p.snd (β := fun (m : Fin c.length) ↦ Fin (c.partSize m))) =
      j

Tactic:
exact ⟨⟨m, r⟩, hmr⟩
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition n
m : Fin c.length
r : Fin (c.partSize m)
m' : Fin c.length
r' : Fin (c.partSize m')
h : c.emb m r = c.emb m' r'
contrapose! : ∀ (h : m ≠ m'), c.emb m r ≠ c.emb m' r'
⊢ m = m'

Tactic:
contrapose! h
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition n
m : Fin c.length
r : Fin (c.partSize m)
m' : Fin c.length
r' : Fin (c.partSize m')
h : m ≠ m'
⊢ Disjoint (range (c.emb m)) (range (c.emb m'))

Tactic:
have A : Disjoint (range (c.emb m)) (range (c.emb m')) :=
      c.disjoint (mem_univ m) (mem_univ m') h
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition n
m : Fin c.length
r : Fin (c.partSize m)
m' : Fin c.length
r' : Fin (c.partSize m')
h : m ≠ m'
A : Disjoint (range (c.emb m)) (range (c.emb m'))
⊢ c.emb m r ≠ c.emb m' r'

Tactic:
apply disjoint_iff_forall_ne.1 A (mem_range_self r) (mem_range_self r')

Premises used: Set.mem_range_self, Set.disjoint_iff_forall_ne, Iff.mp
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition n
m : Fin c.length
r : Fin (c.partSize m)
m' : Fin c.length
r' : Fin (c.partSize m')
h : c.emb m r = c.emb m' r'
⊢ m = m'

Tactic:
have : m = m' := by
    contrapose! h
    have A : Disjoint (range (c.emb m)) (range (c.emb m')) :=
      c.disjoint (mem_univ m) (mem_univ m') h
    apply disjoint_iff_forall_ne.1 A (mem_range_self r) (mem_range_self r')
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition n
m : Fin c.length
r : Fin (c.partSize m)
m' : Fin c.length
r' : Fin (c.partSize m')
h : c.emb m r = c.emb m' r'
this : m = m'
subst :
  ∀ (r' : Fin (c.partSize m)) (h : c.emb m r = c.emb m r'),
    Eq (α := (m : Fin c.length) × Fin (c.partSize m)) (Sigma.mk (β := fun (m : Fin c.length) ↦ Fin (c.partSize m)) m r)
      (Sigma.mk (β := fun (m : Fin c.length) ↦ Fin (c.partSize m)) m r')
⊢ Eq (α := (m : Fin c.length) × Fin (c.partSize m)) (Sigma.mk (β := fun (m : Fin c.length) ↦ Fin (c.partSize m)) m r)
    (Sigma.mk (β := fun (m : Fin c.length) ↦ Fin (c.partSize m)) m' r')

Tactic:
subst this
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition n
m : Fin c.length
r r' : Fin (c.partSize m)
h : c.emb m r = c.emb m r'
⊢ Eq (α := (m : Fin c.length) × Fin (c.partSize m)) (Sigma.mk (β := fun (m : Fin c.length) ↦ Fin (c.partSize m)) m r)
    (Sigma.mk (β := fun (m : Fin c.length) ↦ Fin (c.partSize m)) m r')

Tactic:
simpa using (c.emb_strictMono m).injective h

Premises used: StrictMono.injective, OrderedFinpartition.emb_strictMono
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition n
i j : Fin c.length
a : Fin (c.partSize i)
b : Fin (c.partSize j)
h : i ≠ j
⊢ Ne (α := (m : Fin c.length) × Fin (c.partSize m)) (Sigma.mk (β := fun (m : Fin c.length) ↦ Fin (c.partSize m)) i a)
    (Sigma.mk (β := fun (m : Fin c.length) ↦ Fin (c.partSize m)) j b)

Tactic:
simp [h]
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition n
j : Fin n
⊢ c.emb (c.index j) (c.invEmbedding j) = j

Tactic:
(c.exists_inverse j).choose_spec

Premises used: Exists.choose_spec, OrderedFinpartition.invEmbedding, OrderedFinpartition.index, OrderedFinpartition.exists_inverse
-- 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
x : (i : Fin c.length) × Fin (c.partSize i)
a :
  Eq (α := Fin n)
    ((fun (p : (m : Fin c.length) × Fin (c.partSize m)) ↦
        c.emb (p.fst (β := fun (m : Fin c.length) ↦ Fin (c.partSize m)))
          (p.snd (β := fun (m : Fin c.length) ↦ Fin (c.partSize m))))
      ((fun (i : Fin n) ↦
          (Sigma.mk (β := fun (i : Fin c.length) ↦ Fin (c.partSize i)) (c.index i) (c.invEmbedding i) :
            (i : Fin c.length) × Fin (c.partSize i)))
        ((fun (p : (i : Fin c.length) × Fin (c.partSize i)) ↦
            c.emb (p.fst (β := fun (i : Fin c.length) ↦ Fin (c.partSize i)))
              (p.snd (β := fun (i : Fin c.length) ↦ Fin (c.partSize i))))
          x)))
    ((fun (p : (m : Fin c.length) × Fin (c.partSize m)) ↦
        c.emb (p.fst (β := fun (m : Fin c.length) ↦ Fin (c.partSize m)))
          (p.snd (β := fun (m : Fin c.length) ↦ Fin (c.partSize m))))
      x)
⊢ (fun (i : Fin n) ↦
        (Sigma.mk (β := fun (i : Fin c.length) ↦ Fin (c.partSize i)) (c.index i) (c.invEmbedding i) :
          (i : Fin c.length) × Fin (c.partSize i)))
      ((fun (p : (i : Fin c.length) × Fin (c.partSize i)) ↦
          c.emb (p.fst (β := fun (i : Fin c.length) ↦ Fin (c.partSize i)))
            (p.snd (β := fun (i : Fin c.length) ↦ Fin (c.partSize i))))
        x) =
    x

Tactic:
apply c.emb_injective

Premises used: OrderedFinpartition.emb_injective
-- 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
x : (i : Fin c.length) × Fin (c.partSize i)
⊢ Eq (α := Fin n)
    ((fun (p : (m : Fin c.length) × Fin (c.partSize m)) ↦
        c.emb (p.fst (β := fun (m : Fin c.length) ↦ Fin (c.partSize m)))
          (p.snd (β := fun (m : Fin c.length) ↦ Fin (c.partSize m))))
      ((fun (i : Fin n) ↦
          (Sigma.mk (β := fun (i : Fin c.length) ↦ Fin (c.partSize i)) (c.index i) (c.invEmbedding i) :
            (i : Fin c.length) × Fin (c.partSize i)))
        ((fun (p : (i : Fin c.length) × Fin (c.partSize i)) ↦
            c.emb (p.fst (β := fun (i : Fin c.length) ↦ Fin (c.partSize i)))
              (p.snd (β := fun (i : Fin c.length) ↦ Fin (c.partSize i))))
          x)))
    ((fun (p : (m : Fin c.length) × Fin (c.partSize m)) ↦
        c.emb (p.fst (β := fun (m : Fin c.length) ↦ Fin (c.partSize m)))
          (p.snd (β := fun (m : Fin c.length) ↦ Fin (c.partSize m))))
      x)

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 : OrderedFinpartition n
x : Fin n
⊢ (fun (p : (i : Fin c.length) × Fin (c.partSize i)) ↦
        c.emb (p.fst (β := fun (i : Fin c.length) ↦ Fin (c.partSize i)))
          (p.snd (β := fun (i : Fin c.length) ↦ Fin (c.partSize i))))
      ((fun (i : Fin n) ↦
          (Sigma.mk (β := fun (i : Fin c.length) ↦ Fin (c.partSize i)) (c.index i) (c.invEmbedding i) :
            (i : Fin c.length) × Fin (c.partSize i)))
        x) =
    x

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition n
α : Type u_5
inst : CommMonoid α
v : Fin n → α
rw :
  Eq.{u_5 + 1} (α := α)
    (∏
      x ∈
        Finset.sigma (α := fun (a : Fin c.length) ↦ Fin (c.partSize a)) Finset.univ fun (m : Fin c.length) ↦
          Finset.univ,
      v
        (c.emb (x.fst (β := fun (i : Fin c.length) ↦ Fin (c.partSize i)))
          (x.snd (β := fun (i : Fin c.length) ↦ Fin (c.partSize i)))))
    (∏ i : Fin n, v i)
⊢ Eq.{u_5 + 1} (α := α) (∏ m : Fin c.length, ∏ r : Fin (c.partSize m), v (c.emb m r)) (∏ i : Fin n, v i)

Tactic:
rw [Finset.prod_sigma']

Premises used: Finset.prod_sigma'
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition n
α : Type u_5
inst : CommMonoid α
v : Fin n → α
⊢ Eq.{u_5 + 1} (α := α)
    (∏
      x ∈
        Finset.sigma (α := fun (a : Fin c.length) ↦ Fin (c.partSize a)) Finset.univ fun (m : Fin c.length) ↦
          Finset.univ,
      v
        (c.emb (x.fst (β := fun (i : Fin c.length) ↦ Fin (c.partSize i)))
          (x.snd (β := fun (i : Fin c.length) ↦ Fin (c.partSize i)))))
    (∏ i : Fin n, v i)

Tactic:
Fintype.prod_equiv c.equivSigma _ _ (fun p ↦ rfl)

Premises used: Fintype.prod_equiv, Finset.univ, OrderedFinpartition.equivSigma, Finset.sigma, rfl
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition n
α : Type u_5
inst : CommMonoid α
v : Fin n → α
⊢ Eq.{u_5 + 1} (α := α)
    (∏
      x ∈
        Finset.sigma (α := fun (a : Fin c.length) ↦ Fin (c.partSize a)) Finset.univ fun (m : Fin c.length) ↦
          Finset.univ,
      v
        (c.emb (x.fst (β := fun (i : Fin c.length) ↦ Fin (c.partSize i)))
          (x.snd (β := fun (i : Fin c.length) ↦ Fin (c.partSize i)))))
    (∏ i : Fin n, v i)

Tactic:
exact Fintype.prod_equiv c.equivSigma _ _ (fun p ↦ rfl)

Premises used: Fintype.prod_equiv, OrderedFinpartition.equivSigma, rfl
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition n
h : 0 < n
⊢ 0 < c.length

Tactic:
Nat.zero_lt_of_lt (c.index ⟨0, h⟩).2

Premises used: OrderedFinpartition.index, Fin.isLt, Fin.mk, Nat.zero_lt_of_lt, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
inst : NeZero n
c : OrderedFinpartition n
⊢ NeZero c.length

Tactic:
⟨(c.length_pos pos').ne'⟩

Premises used: NeZero.mk, LT.lt.ne', OrderedFinpartition.length_pos, Fin.pos'
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition n
i : Fin c.length
⊢ NeZero (c.partSize i)

Tactic:
.of_pos (c.partSize_pos i)

Premises used: OrderedFinpartition.partSize_pos, NeZero.of_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
⊢ c.length = 1

Tactic:
have h₁ : c.length = 1 := le_antisymm c.length_le (c.length_pos Nat.zero_lt_one)