-- Mathlib/Algebra/BigOperators/Fin.lean
theorem finSigmaFinEquiv_apply {m : ℕ} {n : Fin m → ℕ} (k : (i : Fin m) × Fin (n i)) :
    (finSigmaFinEquiv k : ℕ) = ∑ i : Fin k.1, n (Fin.castLE k.1.2.le i) + k.2

Proof state:
case neg
m : ℕ
ih :
  ∀ {n : Fin m → ℕ} (k : (i : Fin m) × Fin (n i)), ↑(finSigmaFinEquiv k) = ∑ i : Fin ↑k.fst, n (Fin.castLE ⋯ i) + ↑k.snd
n : Fin (m + 1) → ℕ
iv : ℕ
hi : iv < m + 1
j : Fin (n ⟨iv, hi⟩)
him : iv = m
⊢ ↑(Sum.elim (Fin.castAdd (n (Fin.last m))) (Fin.natAdd (∑ i : Fin m, n i.castSucc))
        (Sum.map (⇑finSigmaFinEquiv)
          (⇑(Equiv.uniqueSigma fun i => Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) (Sum.inr i)))))
          ((Equiv.sumSigmaDistrib fun a => Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) a)))
            ⟨Fin.addCases Sum.inl Sum.inr ⟨iv, hi⟩, ⋯ ▸ j⟩))) =
    ∑ x : Fin iv, n (Fin.castLE ⋯ x) + ↑j

Tactic:
subst him

Result:
case neg
iv : ℕ
ih :
  ∀ {n : Fin iv → ℕ} (k : (i : Fin iv) × Fin (n i)),
    ↑(finSigmaFinEquiv k) = ∑ i : Fin ↑k.fst, n (Fin.castLE ⋯ i) + ↑k.snd
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))
        (Sum.map (⇑finSigmaFinEquiv)
          (⇑(Equiv.uniqueSigma fun i => Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) (Sum.inr i)))))
          ((Equiv.sumSigmaDistrib fun a => Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) a)))
            ⟨Fin.addCases Sum.inl Sum.inr ⟨iv, hi⟩, ⋯ ▸ j⟩))) =
    ∑ x : Fin iv, n (Fin.castLE ⋯ x) + ↑j

Proof state:
case succ.mk.mk
m : ℕ
ih :
  ∀ {n : Fin m → ℕ} (k : (i : Fin m) × Fin (n i)), ↑(finSigmaFinEquiv k) = ∑ i : Fin ↑k.fst, n (Fin.castLE ⋯ i) + ↑k.snd
n : Fin (m + 1) → ℕ
iv : ℕ
hi : iv < m + 1
j : Fin (n ⟨iv, hi⟩)
⊢ ↑(finSigmaFinEquiv ⟨⟨iv, hi⟩, j⟩) = ∑ i : Fin ↑⟨⟨iv, hi⟩, j⟩.fst, n (Fin.castLE ⋯ i) + ↑⟨⟨iv, hi⟩, j⟩.snd

Tactic:
rw [finSigmaFinEquiv]

Result:
case succ.mk.mk
m : ℕ
ih :
  ∀ {n : Fin m → ℕ} (k : (i : Fin m) × Fin (n i)), ↑(finSigmaFinEquiv k) = ∑ i : Fin ↑k.fst, n (Fin.castLE ⋯ i) + ↑k.snd
n : Fin (m + 1) → ℕ
iv : ℕ
hi : iv < m + 1
j : Fin (n ⟨iv, hi⟩)
⊢ ↑((Trans.trans
          (Trans.trans
            (Trans.trans
              (Trans.trans finSumFinEquiv.sigmaCongrLeft.symm
                (Equiv.sumSigmaDistrib fun a => Fin (n (finSumFinEquiv a))))
              (finSigmaFinEquiv.sumCongr (Equiv.uniqueSigma fun i => Fin (n (finSumFinEquiv (Sum.inr i))))))
            finSumFinEquiv)
          (finCongr ⋯))
        ⟨⟨iv, hi⟩, j⟩) =
    ∑ i : Fin ↑⟨⟨iv, hi⟩, j⟩.fst, n (Fin.castLE ⋯ i) + ↑⟨⟨iv, hi⟩, j⟩.snd

Proof state:
case neg
iv : ℕ
ih :
  ∀ {n : Fin iv → ℕ} (k : (i : Fin iv) × Fin (n i)),
    ↑(finSigmaFinEquiv k) = ∑ i : Fin ↑k.fst, n (Fin.castLE ⋯ i) + ↑k.snd
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))
        (Sum.map (⇑finSigmaFinEquiv)
          (⇑(Equiv.uniqueSigma fun i => Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) (Sum.inr i)))))
          ((Equiv.sumSigmaDistrib fun a => Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) a)))
            ⟨Fin.addCases Sum.inl Sum.inr ⟨iv, hi⟩, ⋯ ▸ j⟩))) =
    ∑ x : Fin iv, n (Fin.castLE ⋯ x) + ↑j

Tactic:
conv in Sigma.mk _ _ =>
  equals ⟨Sum.inr 0, j⟩ => simp [Fin.addCases, Fin.natAdd]

Result:
case neg
iv : ℕ
ih :
  ∀ {n : Fin iv → ℕ} (k : (i : Fin iv) × Fin (n i)),
    ↑(finSigmaFinEquiv k) = ∑ i : Fin ↑k.fst, n (Fin.castLE ⋯ i) + ↑k.snd
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))
        (Sum.map (⇑finSigmaFinEquiv)
          (⇑(Equiv.uniqueSigma fun i => Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) (Sum.inr i)))))
          ((Equiv.sumSigmaDistrib fun a => Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) a))) ⟨Sum.inr 0, j⟩))) =
    ∑ x : Fin iv, n (Fin.castLE ⋯ x) + ↑j

Proof state:
case neg
iv : ℕ
ih :
  ∀ {n : Fin iv → ℕ} (k : (i : Fin iv) × Fin (n i)),
    ↑(finSigmaFinEquiv k) = ∑ i : Fin ↑k.fst, n (Fin.castLE ⋯ i) + ↑k.snd
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))
        (Sum.map (⇑finSigmaFinEquiv) (⇑(Equiv.uniqueSigma fun i => Fin (n (Fin.natAdd iv i))))
          ((Equiv.sumSigmaDistrib fun a => Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) a))) ⟨Sum.inr 0, j⟩))) =
    ∑ x : Fin iv, n (Fin.castLE ⋯ x) + ↑j

Tactic:
rfl

Result:
no goals

Proof state:
case pos
m : ℕ
ih :
  ∀ {n : Fin m → ℕ} (k : (i : Fin m) × Fin (n i)), ↑(finSigmaFinEquiv k) = ∑ i : Fin ↑k.fst, n (Fin.castLE ⋯ i) + ↑k.snd
n : Fin (m + 1) → ℕ
iv : ℕ
hi : iv < m + 1
j : Fin (n ⟨iv, hi⟩)
him : iv < m
⊢ ↑(Sum.elim (Fin.castAdd (n (Fin.last m))) (Fin.natAdd (∑ i : Fin m, n i.castSucc))
        (Sum.map (⇑finSigmaFinEquiv)
          (⇑(Equiv.uniqueSigma fun i => Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) (Sum.inr i)))))
          ((Equiv.sumSigmaDistrib fun a => Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) a)))
            ⟨Fin.addCases Sum.inl Sum.inr ⟨iv, hi⟩, ⋯ ▸ j⟩))) =
    ∑ x : Fin iv, n (Fin.castLE ⋯ x) + ↑j

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

Result:
case pos
m : ℕ
ih :
  ∀ {n : Fin m → ℕ} (k : (i : Fin m) × Fin (n i)), ↑(finSigmaFinEquiv k) = ∑ i : Fin ↑k.fst, n (Fin.castLE ⋯ i) + ↑k.snd
n : Fin (m + 1) → ℕ
iv : ℕ
hi : iv < m + 1
j : Fin (n ⟨iv, hi⟩)
him : iv < m
⊢ ↑(Sum.elim (Fin.castAdd (n (Fin.last m))) (Fin.natAdd (∑ i : Fin m, n i.castSucc))
        (Sum.map (⇑finSigmaFinEquiv)
          (⇑(Equiv.uniqueSigma fun i => Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) (Sum.inr i)))))
          ((Equiv.sumSigmaDistrib fun a => Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) a)))
            ⟨Sum.inl ⟨iv, him⟩, j⟩))) =
    ∑ x : Fin iv, n (Fin.castLE ⋯ x) + ↑j

Proof state:
case neg
iv : ℕ
ih :
  ∀ {n : Fin iv → ℕ} (k : (i : Fin iv) × Fin (n i)),
    ↑(finSigmaFinEquiv k) = ∑ i : Fin ↑k.fst, n (Fin.castLE ⋯ i) + ↑k.snd
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))
        (Sum.map (⇑finSigmaFinEquiv)
          (⇑(Equiv.uniqueSigma fun i => Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) (Sum.inr i)))))
          ((Equiv.sumSigmaDistrib fun a => Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) a))) ⟨Sum.inr 0, j⟩))) =
    ∑ x : Fin iv, n (Fin.castLE ⋯ x) + ↑j

Tactic:
simp

Result:
case neg
iv : ℕ
ih :
  ∀ {n : Fin iv → ℕ} (k : (i : Fin iv) × Fin (n i)),
    ↑(finSigmaFinEquiv k) = ∑ i : Fin ↑k.fst, n (Fin.castLE ⋯ i) + ↑k.snd
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))
        (Sum.map (⇑finSigmaFinEquiv) (⇑(Equiv.uniqueSigma fun i => Fin (n (Fin.natAdd iv i))))
          ((Equiv.sumSigmaDistrib fun a => Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) a))) ⟨Sum.inr 0, j⟩))) =
    ∑ x : Fin iv, n (Fin.castLE ⋯ x) + ↑j

Proof state:
case zero
n : Fin 0 → ℕ
k : (i : Fin 0) × Fin (n i)
⊢ ↑(finSigmaFinEquiv k) = ∑ i : Fin ↑k.fst, n (Fin.castLE ⋯ i) + ↑k.snd

Tactic:
exact k.fst.elim0

Result:
no goals

Proof state:
m : ℕ
ih :
  ∀ {n : Fin m → ℕ} (k : (i : Fin m) × Fin (n i)), ↑(finSigmaFinEquiv k) = ∑ i : Fin ↑k.fst, n (Fin.castLE ⋯ i) + ↑k.snd
n : Fin (m + 1) → ℕ
iv : ℕ
hi : iv < m + 1
j : Fin (n ⟨iv, hi⟩)
him : iv < m
⊢ ⟨Fin.addCases Sum.inl Sum.inr ⟨iv, hi⟩, ⋯ ▸ j⟩ = ⟨Sum.inl ⟨iv, him⟩, j⟩

Tactic:
simp [Fin.addCases, him]

Result:
no goals