-- 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 :
  (↑((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)) :
        ℕ)
⊢ (↑((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 ((finSumFinEquiv : (a : Fin m ⊕ Fin 1) → Fin (m + 1)) (Sum.inl i))) ⊕
                    (i : Fin 1) × Fin (n ((finSumFinEquiv : (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 ((finSumFinEquiv : (a : Fin m ⊕ Fin 1) → Fin (m + 1)) a)))
                    (Equiv.symm (Equiv.sigmaCongrLeft (β := fun (a : Fin (m + 1)) ↦ Fin (n a)) finSumFinEquiv))
                    (Equiv.sumSigmaDistrib fun (a : Fin m ⊕ Fin 1) ↦
                      Fin (n ((finSumFinEquiv : (a : Fin m ⊕ Fin 1) → Fin (m + 1)) a))))
                  (Equiv.sumCongr finSigmaFinEquiv
                    (Equiv.uniqueSigma fun (i : Fin 1) ↦
                      Fin (n ((finSumFinEquiv : (a : Fin m ⊕ Fin 1) → Fin (m + 1)) (Sum.inr i))))))
                finSumFinEquiv)
              (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:
unfold finSumFinEquiv

Premises used: finSumFinEquiv