-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
m : ℕ
ih :
  ∀ {n : Fin m → ℕ} (k : (i : Fin m) × Fin (n i)),
    (↑((finSigmaFinEquiv : (a : (i : Fin m) × Fin (n i)) → Fin (∑ i : Fin m, n i)) k) : ℕ) =
      ∑ i : Fin (↑k.fst : ℕ), n (Fin.castLE ⋯ i) + (↑(k.snd (β := fun (i : Fin m) ↦ Fin (n i))) : ℕ)
n : Fin (m + 1) → ℕ
iv : ℕ
hi : iv < m + 1
j : Fin (n ⟨iv, hi⟩)
succ :
  (↑(Sum.elim (Fin.castAdd (n (Fin.last m))) (Fin.natAdd (∑ i : Fin m, n i.castSucc))
          ((Equiv.sumCongr finSigmaFinEquiv
                (Equiv.uniqueSigma fun (i : Fin 1) ↦ Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) (Sum.inr i)))) :
              (a :
                  (i : Fin m) × Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) (Sum.inl i))) ⊕
                    (i : Fin 1) × Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) (Sum.inr i)))) →
                Fin (∑ i : Fin m, n i.castSucc) ⊕ Fin (n (Fin.last m)))
            ((Equiv.sumSigmaDistrib fun (a : Fin m ⊕ Fin 1) ↦ Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) a)) :
                  (a : (a : Fin m ⊕ Fin 1) × Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) a))) →
                    (i : Fin m) × Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) (Sum.inl i))) ⊕
                      (i : Fin 1) × Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) (Sum.inr i))))
                (Sigma.mk (β := fun (a : Fin m ⊕ Fin 1) ↦ Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) a)))
                    (Fin.addCases (motive := fun (x : Fin (m + 1)) ↦ Fin m ⊕ Fin 1) Sum.inl Sum.inr
                      (⟨iv, hi⟩ : Fin (m + 1)))
                    (@Eq.rec _ (⟨iv, hi⟩ : Fin (m + 1))
                      (fun (x : Fin (m + 1)) (h : (⟨iv, hi⟩ : Fin (m + 1)) = x) ↦ Fin (n x)) j
                      (Sum.elim (Fin.castAdd 1) (Fin.natAdd m)
                        (Fin.addCases (motive := fun (x : Fin (m + 1)) ↦ Fin m ⊕ Fin 1) Sum.inl Sum.inr
                          (⟨iv, hi⟩ : Fin (m + 1))))
                      ⋯) :
                  (a : Fin m ⊕ Fin 1) × Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) a))) :
              (i : Fin m) × Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) (Sum.inl i))) ⊕
                (i : Fin 1) × Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) (Sum.inr i)))))) :
      ℕ) =
    ∑ x : Fin iv, n (Fin.castLE ⋯ x) + (↑j : ℕ)
⊢ (↑((Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
              (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
                (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv) (b :=
                  (i : Fin m) ×
                      Fin
                        (n
                          (({ toFun := Sum.elim (Fin.castAdd 1) (Fin.natAdd m),
                                invFun := fun (i : Fin (m + 1)) ↦
                                  Fin.addCases (motive := fun (x : Fin (m + 1)) ↦ Fin m ⊕ Fin 1) Sum.inl Sum.inr i,
                                left_inv := ⋯, right_inv := ⋯ : Fin m ⊕ Fin 1 ≃ Fin (m + 1) } :
                              (a : Fin m ⊕ Fin 1) → Fin (m + 1))
                            (Sum.inl i))) ⊕
                    (i : Fin 1) ×
                      Fin
                        (n
                          (({ toFun := Sum.elim (Fin.castAdd 1) (Fin.natAdd m),
                                invFun := fun (i : Fin (m + 1)) ↦
                                  Fin.addCases (motive := fun (x : Fin (m + 1)) ↦ Fin m ⊕ Fin 1) Sum.inl Sum.inr i,
                                left_inv := ⋯, right_inv := ⋯ : Fin m ⊕ Fin 1 ≃ Fin (m + 1) } :
                              (a : Fin m ⊕ Fin 1) → Fin (m + 1))
                            (Sum.inr i))))
                  (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv) (b :=
                    (a : Fin m ⊕ Fin 1) ×
                      Fin
                        (n
                          (({ toFun := Sum.elim (Fin.castAdd 1) (Fin.natAdd m),
                                invFun := fun (i : Fin (m + 1)) ↦
                                  Fin.addCases (motive := fun (x : Fin (m + 1)) ↦ Fin m ⊕ Fin 1) Sum.inl Sum.inr i,
                                left_inv := ⋯, right_inv := ⋯ : Fin m ⊕ Fin 1 ≃ Fin (m + 1) } :
                              (a : Fin m ⊕ Fin 1) → Fin (m + 1))
                            a)))
                    (Equiv.symm
                      (Equiv.sigmaCongrLeft (β := fun (a : Fin (m + 1)) ↦ Fin (n a))
                        { toFun := Sum.elim (Fin.castAdd 1) (Fin.natAdd m),
                          invFun := fun (i : Fin (m + 1)) ↦
                            Fin.addCases (motive := fun (x : Fin (m + 1)) ↦ Fin m ⊕ Fin 1) Sum.inl Sum.inr i,
                          left_inv := ⋯, right_inv := ⋯ : Fin m ⊕ Fin 1 ≃ Fin (m + 1) }))
                    (Equiv.sumSigmaDistrib fun (a : Fin m ⊕ Fin 1) ↦
                      Fin
                        (n
                          (({ toFun := Sum.elim (Fin.castAdd 1) (Fin.natAdd m),
                                invFun := fun (i : Fin (m + 1)) ↦
                                  Fin.addCases (motive := fun (x : Fin (m + 1)) ↦ Fin m ⊕ Fin 1) Sum.inl Sum.inr i,
                                left_inv := ⋯, right_inv := ⋯ : Fin m ⊕ Fin 1 ≃ Fin (m + 1) } :
                              (a : Fin m ⊕ Fin 1) → Fin (m + 1))
                            a))))
                  (Equiv.sumCongr finSigmaFinEquiv
                    (Equiv.uniqueSigma fun (i : Fin 1) ↦
                      Fin
                        (n
                          (({ toFun := Sum.elim (Fin.castAdd 1) (Fin.natAdd m),
                                invFun := fun (i : Fin (m + 1)) ↦
                                  Fin.addCases (motive := fun (x : Fin (m + 1)) ↦ Fin m ⊕ Fin 1) Sum.inl Sum.inr i,
                                left_inv := ⋯, right_inv := ⋯ : Fin m ⊕ Fin 1 ≃ Fin (m + 1) } :
                              (a : Fin m ⊕ Fin 1) → Fin (m + 1))
                            (Sum.inr i))))))
                { toFun := Sum.elim (Fin.castAdd (n (Fin.last m))) (Fin.natAdd (∑ i : Fin m, n i.castSucc)),
                  invFun := fun (i : Fin (∑ i : Fin m, n i.castSucc + n (Fin.last m))) ↦
                    Fin.addCases (motive := fun (x : Fin (∑ i : Fin m, n i.castSucc + n (Fin.last m))) ↦
                      Fin (∑ i : Fin m, n i.castSucc) ⊕ Fin (n (Fin.last m))) Sum.inl Sum.inr i,
                  left_inv := ⋯, right_inv := ⋯ :
                  Fin (∑ i : Fin m, n i.castSucc) ⊕ Fin (n (Fin.last m)) ≃
                    Fin (∑ i : Fin m, n i.castSucc + n (Fin.last m)) })
              (finCongr ⋯) :
            (a : (i : Fin (m + 1)) × Fin (n i)) → Fin (∑ i : Fin (m + 1), n i))
          (Sigma.mk (β := fun (i : Fin (m + 1)) ↦ Fin (n i)) (⟨iv, hi⟩ : Fin (m + 1)) j)) :
      ℕ) =
    ∑ i : Fin (↑⟨⟨iv, hi⟩, j⟩.fst : ℕ), n (Fin.castLE ⋯ i) +
      (↑(Sigma.snd (β := fun (i : Fin (m + 1)) ↦ Fin (n i))
            (Sigma.mk (β := fun (i : Fin (m + 1)) ↦ Fin (n i)) (⟨iv, hi⟩ : Fin (m + 1)) j)) :
        ℕ)

Tactic:
simp only [Equiv.coe_fn_mk, Equiv.sigmaCongrLeft, Equiv.coe_fn_symm_mk, Equiv.trans_def,
    Equiv.trans_apply, finCongr_apply, Fin.val_cast]

Premises used: finCongr_apply, Equiv.coe_fn_symm_mk, Equiv.trans_apply, Equiv.sigmaCongrLeft, Equiv.trans_def, Equiv.coe_fn_mk, Fin.val_cast