-- 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⟩)
him : iv < m
pos :
  (↑(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)))
                  (Sum.inl (⟨iv, him⟩ : Fin m)) j) :
              (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 : ℕ)
⊢ (↑(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 : ℕ)

Tactic:
conv in Sigma.mk _ _ =>
      equals ⟨Sum.inl ⟨iv, him⟩, j⟩ => simp [Fin.addCases, him]

Premises used: Sigma.mk