-- Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean
lemma injective_embSigma (n : ℕ) : Injective (embSigma n)

Proof state:
case mk.mk
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 fun m => pemb m ⟨psize m - 1, ⋯⟩
disjoint✝¹ : univ.PairwiseDisjoint fun m => range (pemb m)
cover✝¹ : ∀ (x : Fin n), ∃ m, x ∈ range (pemb m)
qlength : ℕ
qsize : Fin qlength → ℕ
partSize_pos✝ : ∀ (m : Fin qlength), 0 < qsize m
qemb : (m : Fin qlength) → Fin (qsize m) → Fin n
emb_strictMono✝ : ∀ (m : Fin qlength), StrictMono (qemb m)
parts_strictMono✝ : StrictMono fun m => qemb m ⟨qsize m - 1, ⋯⟩
disjoint✝ : univ.PairwiseDisjoint fun m => range (qemb m)
cover✝ : ∀ (x : Fin n), ∃ m, x ∈ range (qemb m)
hpq : plength = qlength ∧ HEq ⟨fun m => ⟨psize m, ⋯⟩, fun j => pemb j⟩ ⟨fun m => ⟨qsize m, ⋯⟩, fun j => qemb j⟩
this : plength = qlength
⊢ HEq psize qsize ∧ HEq pemb qemb

Tactic:
subst this

Result:
case mk.mk
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 fun m => pemb m ⟨psize m - 1, ⋯⟩
disjoint✝¹ : univ.PairwiseDisjoint fun m => range (pemb m)
cover✝¹ : ∀ (x : Fin n), ∃ m, x ∈ range (pemb m)
qsize : Fin plength → ℕ
partSize_pos✝ : ∀ (m : Fin plength), 0 < qsize m
qemb : (m : Fin plength) → Fin (qsize m) → Fin n
emb_strictMono✝ : ∀ (m : Fin plength), StrictMono (qemb m)
parts_strictMono✝ : StrictMono fun m => qemb m ⟨qsize m - 1, ⋯⟩
disjoint✝ : univ.PairwiseDisjoint fun m => range (qemb m)
cover✝ : ∀ (x : Fin n), ∃ m, x ∈ range (qemb m)
hpq : plength = plength ∧ HEq ⟨fun m => ⟨psize m, ⋯⟩, fun j => pemb j⟩ ⟨fun m => ⟨qsize m, ⋯⟩, fun j => qemb j⟩
⊢ HEq psize qsize ∧ HEq pemb qemb

Proof state:
n : ℕ
⊢ Injective (embSigma n)

Tactic:
rintro ⟨plength, psize, -, pemb, -, -, -, -⟩ ⟨qlength, qsize, -, qemb, -, -, -, -⟩

Result:
case mk.mk
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 fun m => pemb m ⟨psize m - 1, ⋯⟩
disjoint✝¹ : univ.PairwiseDisjoint fun m => range (pemb m)
cover✝¹ : ∀ (x : Fin n), ∃ m, x ∈ range (pemb m)
qlength : ℕ
qsize : Fin qlength → ℕ
partSize_pos✝ : ∀ (m : Fin qlength), 0 < qsize m
qemb : (m : Fin qlength) → Fin (qsize m) → Fin n
emb_strictMono✝ : ∀ (m : Fin qlength), StrictMono (qemb m)
parts_strictMono✝ : StrictMono fun m => qemb m ⟨qsize m - 1, ⋯⟩
disjoint✝ : univ.PairwiseDisjoint fun m => range (qemb m)
cover✝ : ∀ (x : Fin n), ∃ m, x ∈ range (qemb m)
⊢ embSigma n
        { length := plength, partSize := psize, partSize_pos := partSize_pos✝¹, emb := pemb,
          emb_strictMono := emb_strictMono✝¹, parts_strictMono := parts_strictMono✝¹, disjoint := disjoint✝¹,
          cover := cover✝¹ } =
      embSigma n
        { length := qlength, partSize := qsize, partSize_pos := partSize_pos✝, emb := qemb,
          emb_strictMono := emb_strictMono✝, parts_strictMono := parts_strictMono✝, disjoint := disjoint✝,
          cover := cover✝ } →
    { length := plength, partSize := psize, partSize_pos := partSize_pos✝¹, emb := pemb,
        emb_strictMono := emb_strictMono✝¹, parts_strictMono := parts_strictMono✝¹, disjoint := disjoint✝¹,
        cover := cover✝¹ } =
      { length := qlength, partSize := qsize, partSize_pos := partSize_pos✝, emb := qemb,
        emb_strictMono := emb_strictMono✝, parts_strictMono := parts_strictMono✝, disjoint := disjoint✝,
        cover := cover✝ }

Proof state:
case mk.mk
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 fun m => pemb m ⟨psize m - 1, ⋯⟩
disjoint✝¹ : univ.PairwiseDisjoint fun m => range (pemb m)
cover✝¹ : ∀ (x : Fin n), ∃ m, x ∈ range (pemb m)
qlength : ℕ
qsize : Fin qlength → ℕ
partSize_pos✝ : ∀ (m : Fin qlength), 0 < qsize m
qemb : (m : Fin qlength) → Fin (qsize m) → Fin n
emb_strictMono✝ : ∀ (m : Fin qlength), StrictMono (qemb m)
parts_strictMono✝ : StrictMono fun m => qemb m ⟨qsize m - 1, ⋯⟩
disjoint✝ : univ.PairwiseDisjoint fun m => range (qemb m)
cover✝ : ∀ (x : Fin n), ∃ m, x ∈ range (qemb m)
hpq :
  embSigma n
      { length := plength, partSize := psize, partSize_pos := partSize_pos✝¹, emb := pemb,
        emb_strictMono := emb_strictMono✝¹, parts_strictMono := parts_strictMono✝¹, disjoint := disjoint✝¹,
        cover := cover✝¹ } =
    embSigma n
      { length := qlength, partSize := qsize, partSize_pos := partSize_pos✝, emb := qemb,
        emb_strictMono := emb_strictMono✝, parts_strictMono := parts_strictMono✝, disjoint := disjoint✝,
        cover := cover✝ }
⊢ { length := plength, partSize := psize, partSize_pos := partSize_pos✝¹, emb := pemb,
      emb_strictMono := emb_strictMono✝¹, parts_strictMono := parts_strictMono✝¹, disjoint := disjoint✝¹,
      cover := cover✝¹ } =
    { length := qlength, partSize := qsize, partSize_pos := partSize_pos✝, emb := qemb,
      emb_strictMono := emb_strictMono✝, parts_strictMono := parts_strictMono✝, disjoint := disjoint✝, cover := cover✝ }

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

Result:
case mk.mk
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 fun m => pemb m ⟨psize m - 1, ⋯⟩
disjoint✝¹ : univ.PairwiseDisjoint fun m => range (pemb m)
cover✝¹ : ∀ (x : Fin n), ∃ m, x ∈ range (pemb m)
qlength : ℕ
qsize : Fin qlength → ℕ
partSize_pos✝ : ∀ (m : Fin qlength), 0 < qsize m
qemb : (m : Fin qlength) → Fin (qsize m) → Fin n
emb_strictMono✝ : ∀ (m : Fin qlength), StrictMono (qemb m)
parts_strictMono✝ : StrictMono fun m => qemb m ⟨qsize m - 1, ⋯⟩
disjoint✝ : univ.PairwiseDisjoint fun m => range (qemb m)
cover✝ : ∀ (x : Fin n), ∃ m, x ∈ range (qemb m)
hpq : plength = qlength ∧ HEq ⟨fun m => ⟨psize m, ⋯⟩, fun j => pemb j⟩ ⟨fun m => ⟨qsize m, ⋯⟩, fun j => qemb j⟩
⊢ HEq psize qsize ∧ HEq pemb qemb