Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: 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

Goal state after:
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✝ }