-- 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)
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

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)
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 : ((fun m => ⟨psize m, ⋯⟩) = fun m => ⟨qsize m, ⋯⟩) ∧ HEq (fun j => pemb j) fun j => qemb j
⊢ psize = qsize

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⟩
⊢ HEq psize qsize ∧ HEq pemb qemb

Tactic:
have : plength = qlength := hpq.1

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⟩
this : plength = qlength
⊢ HEq psize qsize ∧ HEq pemb qemb