-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
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⟩)
⊢ (↑((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)) :
        ℕ)
have 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 := sorry, right_inv := sorry : 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 := sorry, right_inv := sorry : 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 := sorry, right_inv := sorry : 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 := sorry, right_inv := sorry : 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 := sorry, right_inv := sorry : 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 := sorry, right_inv := sorry : 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 := sorry, right_inv := sorry :
                Fin (∑ i : Fin m, n i.castSucc) ⊕ Fin (n (Fin.last m)) ≃
                  Fin (∑ i : Fin m, n i.castSucc + n (Fin.last m)) })
            (finCongr sorry) :
          (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 sorry 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