-- Mathlib/Algebra/BigOperators/Fin.lean
theorem finSigmaFinEquiv_apply {m : ℕ} {n : Fin m → ℕ} (k : (i : Fin m) × Fin (n i)) :
    (finSigmaFinEquiv k : ℕ) = ∑ i : Fin k.1, n (Fin.castLE k.1.2.le i) + k.2

Proof state:
case succ.mk.mk
m : ℕ
ih :
  ∀ {n : Fin m → ℕ} (k : (i : Fin m) × Fin (n i)), ↑(finSigmaFinEquiv k) = ∑ i : Fin ↑k.fst, n (Fin.castLE ⋯ i) + ↑k.snd
n : Fin (m + 1) → ℕ
iv : ℕ
hi : iv < m + 1
j : Fin (n ⟨iv, hi⟩)
⊢ ↑(Sum.elim (Fin.castAdd (n (Fin.last m))) (Fin.natAdd (∑ i : Fin m, n i.castSucc))
        ((finSigmaFinEquiv.sumCongr
            (Equiv.uniqueSigma fun i => Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) (Sum.inr i)))))
          ((Equiv.sumSigmaDistrib fun a => Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) a)))
            ⟨Fin.addCases Sum.inl Sum.inr ⟨iv, hi⟩, ⋯ ▸ j⟩))) =
    ∑ x : Fin iv, n (Fin.castLE ⋯ x) + ↑j

Tactic:
conv  =>
  enter [1,1,3]
  apply Equiv.sumCongr_apply

Result:
case succ.mk.mk
m : ℕ
ih :
  ∀ {n : Fin m → ℕ} (k : (i : Fin m) × Fin (n i)), ↑(finSigmaFinEquiv k) = ∑ i : Fin ↑k.fst, n (Fin.castLE ⋯ i) + ↑k.snd
n : Fin (m + 1) → ℕ
iv : ℕ
hi : iv < m + 1
j : Fin (n ⟨iv, hi⟩)
⊢ ↑(Sum.elim (Fin.castAdd (n (Fin.last m))) (Fin.natAdd (∑ i : Fin m, n i.castSucc))
        (Sum.map (⇑finSigmaFinEquiv)
          (⇑(Equiv.uniqueSigma fun i => Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) (Sum.inr i)))))
          ((Equiv.sumSigmaDistrib fun a => Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) a)))
            ⟨Fin.addCases Sum.inl Sum.inr ⟨iv, hi⟩, ⋯ ▸ j⟩))) =
    ∑ x : Fin iv, n (Fin.castLE ⋯ x) + ↑j

Proof state:
case succ.mk.mk
m : ℕ
ih :
  ∀ {n : Fin m → ℕ} (k : (i : Fin m) × Fin (n i)), ↑(finSigmaFinEquiv k) = ∑ i : Fin ↑k.fst, n (Fin.castLE ⋯ i) + ↑k.snd
n : Fin (m + 1) → ℕ
iv : ℕ
hi : iv < m + 1
j : Fin (n ⟨iv, hi⟩)
⊢ ↑((Trans.trans
          (Trans.trans
            (Trans.trans
              (Trans.trans
                { toFun := Sum.elim (Fin.castAdd 1) (Fin.natAdd m), invFun := fun i => Fin.addCases Sum.inl Sum.inr i,
                      left_inv := ⋯, right_inv := ⋯ }.sigmaCongrLeft.symm
                (Equiv.sumSigmaDistrib fun a =>
                  Fin
                    (n
                      ({ toFun := Sum.elim (Fin.castAdd 1) (Fin.natAdd m),
                          invFun := fun i => Fin.addCases Sum.inl Sum.inr i, left_inv := ⋯, right_inv := ⋯ }
                        a))))
              (finSigmaFinEquiv.sumCongr
                (Equiv.uniqueSigma fun i =>
                  Fin
                    (n
                      ({ toFun := Sum.elim (Fin.castAdd 1) (Fin.natAdd m),
                          invFun := fun i => Fin.addCases Sum.inl Sum.inr i, left_inv := ⋯, right_inv := ⋯ }
                        (Sum.inr i))))))
            { toFun := Sum.elim (Fin.castAdd (n (Fin.last m))) (Fin.natAdd (∑ i : Fin m, n i.castSucc)),
              invFun := fun i => Fin.addCases Sum.inl Sum.inr i, left_inv := ⋯, right_inv := ⋯ })
          (finCongr ⋯))
        ⟨⟨iv, hi⟩, j⟩) =
    ∑ i : Fin ↑⟨⟨iv, hi⟩, j⟩.fst, n (Fin.castLE ⋯ i) + ↑⟨⟨iv, hi⟩, j⟩.snd

Tactic:
simp only [Equiv.coe_fn_mk, Equiv.sigmaCongrLeft, Equiv.coe_fn_symm_mk, Equiv.instTrans_trans,
  Equiv.trans_apply, finCongr_apply, Fin.coe_cast]

Result:
case succ.mk.mk
m : ℕ
ih :
  ∀ {n : Fin m → ℕ} (k : (i : Fin m) × Fin (n i)), ↑(finSigmaFinEquiv k) = ∑ i : Fin ↑k.fst, n (Fin.castLE ⋯ i) + ↑k.snd
n : Fin (m + 1) → ℕ
iv : ℕ
hi : iv < m + 1
j : Fin (n ⟨iv, hi⟩)
⊢ ↑(Sum.elim (Fin.castAdd (n (Fin.last m))) (Fin.natAdd (∑ i : Fin m, n i.castSucc))
        ((finSigmaFinEquiv.sumCongr
            (Equiv.uniqueSigma fun i => Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) (Sum.inr i)))))
          ((Equiv.sumSigmaDistrib fun a => Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) a)))
            ⟨Fin.addCases Sum.inl Sum.inr ⟨iv, hi⟩, ⋯ ▸ j⟩))) =
    ∑ x : Fin iv, n (Fin.castLE ⋯ x) + ↑j

Proof state:
iv : ℕ
ih :
  ∀ {n : Fin iv → ℕ} (k : (i : Fin iv) × Fin (n i)),
    ↑(finSigmaFinEquiv k) = ∑ i : Fin ↑k.fst, n (Fin.castLE ⋯ i) + ↑k.snd
n : Fin (iv + 1) → ℕ
hi : iv < iv + 1
j : Fin (n ⟨iv, hi⟩)
⊢ ⟨Fin.addCases Sum.inl Sum.inr ⟨iv, hi⟩, ⋯ ▸ j⟩ = ⟨Sum.inr 0, j⟩

Tactic:
simp [Fin.addCases, Fin.natAdd]

Result:
no goals

Proof state:
case succ
m : ℕ
ih :
  ∀ {n : Fin m → ℕ} (k : (i : Fin m) × Fin (n i)), ↑(finSigmaFinEquiv k) = ∑ i : Fin ↑k.fst, n (Fin.castLE ⋯ i) + ↑k.snd
n : Fin (m + 1) → ℕ
k : (i : Fin (m + 1)) × Fin (n i)
⊢ ↑(finSigmaFinEquiv k) = ∑ i : Fin ↑k.fst, n (Fin.castLE ⋯ i) + ↑k.snd

Tactic:
rcases k with ⟨⟨iv, hi⟩, j⟩

Result:
case succ.mk.mk
m : ℕ
ih :
  ∀ {n : Fin m → ℕ} (k : (i : Fin m) × Fin (n i)), ↑(finSigmaFinEquiv k) = ∑ i : Fin ↑k.fst, n (Fin.castLE ⋯ i) + ↑k.snd
n : Fin (m + 1) → ℕ
iv : ℕ
hi : iv < m + 1
j : Fin (n ⟨iv, hi⟩)
⊢ ↑(finSigmaFinEquiv ⟨⟨iv, hi⟩, j⟩) = ∑ i : Fin ↑⟨⟨iv, hi⟩, j⟩.fst, n (Fin.castLE ⋯ i) + ↑⟨⟨iv, hi⟩, j⟩.snd

Proof state:
case succ.mk.mk
m : ℕ
ih :
  ∀ {n : Fin m → ℕ} (k : (i : Fin m) × Fin (n i)), ↑(finSigmaFinEquiv k) = ∑ i : Fin ↑k.fst, n (Fin.castLE ⋯ i) + ↑k.snd
n : Fin (m + 1) → ℕ
iv : ℕ
hi : iv < m + 1
j : Fin (n ⟨iv, hi⟩)
⊢ ↑((Trans.trans
          (Trans.trans
            (Trans.trans
              (Trans.trans finSumFinEquiv.sigmaCongrLeft.symm
                (Equiv.sumSigmaDistrib fun a => Fin (n (finSumFinEquiv a))))
              (finSigmaFinEquiv.sumCongr (Equiv.uniqueSigma fun i => Fin (n (finSumFinEquiv (Sum.inr i))))))
            finSumFinEquiv)
          (finCongr ⋯))
        ⟨⟨iv, hi⟩, j⟩) =
    ∑ i : Fin ↑⟨⟨iv, hi⟩, j⟩.fst, n (Fin.castLE ⋯ i) + ↑⟨⟨iv, hi⟩, j⟩.snd

Tactic:
unfold finSumFinEquiv

Result:
case succ.mk.mk
m : ℕ
ih :
  ∀ {n : Fin m → ℕ} (k : (i : Fin m) × Fin (n i)), ↑(finSigmaFinEquiv k) = ∑ i : Fin ↑k.fst, n (Fin.castLE ⋯ i) + ↑k.snd
n : Fin (m + 1) → ℕ
iv : ℕ
hi : iv < m + 1
j : Fin (n ⟨iv, hi⟩)
⊢ ↑((Trans.trans
          (Trans.trans
            (Trans.trans
              (Trans.trans
                { toFun := Sum.elim (Fin.castAdd 1) (Fin.natAdd m), invFun := fun i => Fin.addCases Sum.inl Sum.inr i,
                      left_inv := ⋯, right_inv := ⋯ }.sigmaCongrLeft.symm
                (Equiv.sumSigmaDistrib fun a =>
                  Fin
                    (n
                      ({ toFun := Sum.elim (Fin.castAdd 1) (Fin.natAdd m),
                          invFun := fun i => Fin.addCases Sum.inl Sum.inr i, left_inv := ⋯, right_inv := ⋯ }
                        a))))
              (finSigmaFinEquiv.sumCongr
                (Equiv.uniqueSigma fun i =>
                  Fin
                    (n
                      ({ toFun := Sum.elim (Fin.castAdd 1) (Fin.natAdd m),
                          invFun := fun i => Fin.addCases Sum.inl Sum.inr i, left_inv := ⋯, right_inv := ⋯ }
                        (Sum.inr i))))))
            { toFun := Sum.elim (Fin.castAdd (n (Fin.last m))) (Fin.natAdd (∑ i : Fin m, n i.castSucc)),
              invFun := fun i => Fin.addCases Sum.inl Sum.inr i, left_inv := ⋯, right_inv := ⋯ })
          (finCongr ⋯))
        ⟨⟨iv, hi⟩, j⟩) =
    ∑ i : Fin ↑⟨⟨iv, hi⟩, j⟩.fst, n (Fin.castLE ⋯ i) + ↑⟨⟨iv, hi⟩, j⟩.snd