-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
M : Type u_3
inst : CommMonoid M
n : ℕ
f : ℕ → ℕ → M
refine_1 :
  ∀ (a : (_ : ℕ) × ℕ),
    Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((range n).sigma (α := fun (a : ℕ) ↦ ℕ) fun (m : ℕ) ↦ range (m + 1)) a →
      Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((range n).sigma (α := fun (a : ℕ) ↦ ℕ) fun (m : ℕ) ↦ range (n - m))
        ((fun (a : (_ : ℕ) × ℕ) ↦
            (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (a.snd (β := fun (i : ℕ) ↦ ℕ))
                (a.fst (β := fun (i : ℕ) ↦ ℕ) - a.snd (β := fun (i : ℕ) ↦ ℕ)) :
              (_ : ℕ) × ℕ))
          a)
refine_2 :
  ∀ (a : (_ : ℕ) × ℕ),
    Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((range n).sigma (α := fun (a : ℕ) ↦ ℕ) fun (m : ℕ) ↦ range (n - m)) a →
      Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((range n).sigma (α := fun (a : ℕ) ↦ ℕ) fun (m : ℕ) ↦ range (m + 1))
        ((fun (a : (_ : ℕ) × ℕ) ↦
            (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (a.fst (β := fun (i : ℕ) ↦ ℕ) + a.snd (β := fun (i : ℕ) ↦ ℕ))
                (a.fst (β := fun (i : ℕ) ↦ ℕ)) :
              (_ : ℕ) × ℕ))
          a)
refine_3 :
  ∀ (a : (_ : ℕ) × ℕ),
    Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((range n).sigma (α := fun (a : ℕ) ↦ ℕ) fun (m : ℕ) ↦ range (m + 1)) a →
      (fun (a : (_ : ℕ) × ℕ) ↦
            (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (a.fst (β := fun (i : ℕ) ↦ ℕ) + a.snd (β := fun (i : ℕ) ↦ ℕ))
                (a.fst (β := fun (i : ℕ) ↦ ℕ)) :
              (_ : ℕ) × ℕ))
          ((fun (a : (_ : ℕ) × ℕ) ↦
              (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (a.snd (β := fun (i : ℕ) ↦ ℕ))
                  (a.fst (β := fun (i : ℕ) ↦ ℕ) - a.snd (β := fun (i : ℕ) ↦ ℕ)) :
                (_ : ℕ) × ℕ))
            a) =
        a
refine_4 :
  ∀ (a : (_ : ℕ) × ℕ),
    Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((range n).sigma (α := fun (a : ℕ) ↦ ℕ) fun (m : ℕ) ↦ range (n - m)) a →
      (fun (a : (_ : ℕ) × ℕ) ↦
            (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (a.snd (β := fun (i : ℕ) ↦ ℕ))
                (a.fst (β := fun (i : ℕ) ↦ ℕ) - a.snd (β := fun (i : ℕ) ↦ ℕ)) :
              (_ : ℕ) × ℕ))
          ((fun (a : (_ : ℕ) × ℕ) ↦
              (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (a.fst (β := fun (i : ℕ) ↦ ℕ) + a.snd (β := fun (i : ℕ) ↦ ℕ))
                  (a.fst (β := fun (i : ℕ) ↦ ℕ)) :
                (_ : ℕ) × ℕ))
            a) =
        a
⊢ Eq.{u_3 + 1} (α := M)
    (∏ x ∈ (range n).sigma (α := fun (a : ℕ) ↦ ℕ) fun (m : ℕ) ↦ range (m + 1),
      f (x.snd (β := fun (i : ℕ) ↦ ℕ)) (x.fst (β := fun (i : ℕ) ↦ ℕ) - x.snd (β := fun (i : ℕ) ↦ ℕ)))
    (∏ x ∈ (range n).sigma (α := fun (a : ℕ) ↦ ℕ) fun (m : ℕ) ↦ range (n - m),
      f (x.fst (β := fun (i : ℕ) ↦ ℕ)) (x.snd (β := fun (i : ℕ) ↦ ℕ)))
have refine_5 : ∀ (a : (_ : ℕ) × ℕ),
  Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((range n).sigma (α := fun (a : ℕ) ↦ ℕ) fun (m : ℕ) ↦ range (m + 1)) a →
    f (a.snd (β := fun (i : ℕ) ↦ ℕ)) (a.fst (β := fun (i : ℕ) ↦ ℕ) - a.snd (β := fun (i : ℕ) ↦ ℕ)) =
      f
        (Sigma.fst (β := fun (i : ℕ) ↦ ℕ)
          ((fun (a : (_ : ℕ) × ℕ) ↦
              (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (a.snd (β := fun (i : ℕ) ↦ ℕ))
                  (a.fst (β := fun (i : ℕ) ↦ ℕ) - a.snd (β := fun (i : ℕ) ↦ ℕ)) :
                (_ : ℕ) × ℕ))
            a))
        (Sigma.snd (β := fun (i : ℕ) ↦ ℕ)
          ((fun (a : (_ : ℕ) × ℕ) ↦
              (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (a.snd (β := fun (i : ℕ) ↦ ℕ))
                  (a.fst (β := fun (i : ℕ) ↦ ℕ) - a.snd (β := fun (i : ℕ) ↦ ℕ)) :
                (_ : ℕ) × ℕ))
            a))
Tactic: refine prod_nbij' (fun a ↦ ⟨a.2, a.1 - a.2⟩) (fun a ↦ ⟨a.1 + a.2, a.1⟩) ?_ ?_ ?_ ?_ ?_