-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
iv : ℕ
ih :
  ∀ {n : Fin iv → ℕ} (k : (i : Fin iv) × Fin (n i)),
    (↑((finSigmaFinEquiv : (a : (i : Fin iv) × Fin (n i)) → Fin (∑ i : Fin iv, n i)) k) : ℕ) =
      ∑ i : Fin (↑k.fst : ℕ), n (Fin.castLE ⋯ i) + (↑(k.snd (β := fun (i : Fin iv) ↦ Fin (n i))) : ℕ)
n : Fin (iv + 1) → ℕ
hi : iv < iv + 1
j : Fin (n ⟨iv, hi⟩)
⊢ (↑(Sum.elim (Fin.castAdd (n (Fin.last iv))) (Fin.natAdd (∑ i : Fin iv, n i.castSucc))
          ((Equiv.sumCongr finSigmaFinEquiv
                (Equiv.uniqueSigma fun (i : Fin 1) ↦ Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) (Sum.inr i)))) :
              (a :
                  (i : Fin iv) × Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) (Sum.inl i))) ⊕
                    (i : Fin 1) × Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) (Sum.inr i)))) →
                Fin (∑ i : Fin iv, n i.castSucc) ⊕ Fin (n (Fin.last iv)))
            ((Equiv.sumSigmaDistrib fun (a : Fin iv ⊕ Fin 1) ↦ Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) a)) :
                  (a : (a : Fin iv ⊕ Fin 1) × Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) a))) →
                    (i : Fin iv) × Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) (Sum.inl i))) ⊕
                      (i : Fin 1) × Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) (Sum.inr i))))
                (Sigma.mk (β := fun (a : Fin iv ⊕ Fin 1) ↦ Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) a)))
                    (Fin.addCases (motive := fun (x : Fin (iv + 1)) ↦ Fin iv ⊕ Fin 1) Sum.inl Sum.inr
                      (⟨iv, hi⟩ : Fin (iv + 1)))
                    (@Eq.rec _ (⟨iv, hi⟩ : Fin (iv + 1))
                      (fun (x : Fin (iv + 1)) (h : (⟨iv, hi⟩ : Fin (iv + 1)) = x) ↦ Fin (n x)) j
                      (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv)
                        (Fin.addCases (motive := fun (x : Fin (iv + 1)) ↦ Fin iv ⊕ Fin 1) Sum.inl Sum.inr
                          (⟨iv, hi⟩ : Fin (iv + 1))))
                      ⋯) :
                  (a : Fin iv ⊕ Fin 1) × Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) a))) :
              (i : Fin iv) × Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) (Sum.inl i))) ⊕
                (i : Fin 1) × Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) (Sum.inr i)))))) :
      ℕ) =
    ∑ x : Fin iv, n (Fin.castLE ⋯ x) + (↑j : ℕ)
have neg : (↑(Sum.elim (Fin.castAdd (n (Fin.last iv))) (Fin.natAdd (∑ i : Fin iv, n i.castSucc))
        ((Equiv.sumCongr finSigmaFinEquiv
              (Equiv.uniqueSigma fun (i : Fin 1) ↦ Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) (Sum.inr i)))) :
            (a :
                (i : Fin iv) × Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) (Sum.inl i))) ⊕
                  (i : Fin 1) × Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) (Sum.inr i)))) →
              Fin (∑ i : Fin iv, n i.castSucc) ⊕ Fin (n (Fin.last iv)))
          ((Equiv.sumSigmaDistrib fun (a : Fin iv ⊕ Fin 1) ↦ Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) a)) :
                (a : (a : Fin iv ⊕ Fin 1) × Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) a))) →
                  (i : Fin iv) × Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) (Sum.inl i))) ⊕
                    (i : Fin 1) × Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) (Sum.inr i))))
              (Sigma.mk (β := fun (a : Fin iv ⊕ Fin 1) ↦ Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) a)))
                (Sum.inr 0) j) :
            (i : Fin iv) × Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) (Sum.inl i))) ⊕
              (i : Fin 1) × Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) (Sum.inr i)))))) :
    ℕ) =
  ∑ x : Fin iv, n (Fin.castLE sorry x) + (↑j : ℕ)
Tactic: conv in Sigma.mk _ _ =>
      equals ⟨Sum.inr 0, j⟩ => simp [Fin.addCases, Fin.natAdd]