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

Tactic:
ext i

Result:
case mk.mk.h
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
i : Fin plength
⊢ psize i = qsize i

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)
⊢ 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:
intro hpq

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 :
  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.h
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
i : Fin plength
⊢ psize i = qsize i

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

Result:
no goals