-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Defs (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
n : ℕ
h₁ :
  ∀ (a : (_ : ℕ × ℕ) × ℕ × ℕ),
    Membership.mem (γ := Finset ((_ : ℕ × ℕ) × ℕ × ℕ))
        (n.divisorsAntidiagonal.sigma (α := fun (a : ℕ × ℕ) ↦ ℕ × ℕ) fun (a : ℕ × ℕ) ↦ a.1.divisorsAntidiagonal) a →
      Membership.mem (α := (_ : ℕ × ℕ) × ℕ × ℕ) (γ := Finset ((_ : ℕ × ℕ) × ℕ × ℕ))
        (n.divisorsAntidiagonal.sigma (α := fun (a : ℕ × ℕ) ↦ ℕ × ℕ) fun (a : ℕ × ℕ) ↦ a.2.divisorsAntidiagonal)
        (match (motive := (_ : ℕ × ℕ) × ℕ × ℕ → (_ : ℕ × ℕ) × ℕ × ℕ) a with
          | ⟨(_i, j), (k, l)⟩ => Sigma.mk (β := fun (i : ℕ × ℕ) ↦ ℕ × ℕ) (k, l * j) (l, j) :
          (_ : ℕ × ℕ) × ℕ × ℕ)
h₂ :
  ∀ (a : (_ : ℕ × ℕ) × ℕ × ℕ),
    Membership.mem (γ := Finset ((_ : ℕ × ℕ) × ℕ × ℕ))
        (n.divisorsAntidiagonal.sigma (α := fun (a : ℕ × ℕ) ↦ ℕ × ℕ) fun (a : ℕ × ℕ) ↦ a.2.divisorsAntidiagonal) a →
      Membership.mem (α := (_ : ℕ × ℕ) × ℕ × ℕ) (γ := Finset ((_ : ℕ × ℕ) × ℕ × ℕ))
        (n.divisorsAntidiagonal.sigma (α := fun (a : ℕ × ℕ) ↦ ℕ × ℕ) fun (a : ℕ × ℕ) ↦ a.1.divisorsAntidiagonal)
        (match (motive := (_ : ℕ × ℕ) × ℕ × ℕ → (_ : ℕ × ℕ) × ℕ × ℕ) a with
          | ⟨(i, _j), (k, l)⟩ => Sigma.mk (β := fun (i : ℕ × ℕ) ↦ ℕ × ℕ) (i * k, l) (i, k) :
          (_ : ℕ × ℕ) × ℕ × ℕ)
h₃ :
  ∀ (a : (_ : ℕ × ℕ) × ℕ × ℕ),
    Membership.mem (γ := Finset ((_ : ℕ × ℕ) × ℕ × ℕ))
        (n.divisorsAntidiagonal.sigma (α := fun (a : ℕ × ℕ) ↦ ℕ × ℕ) fun (a : ℕ × ℕ) ↦ a.1.divisorsAntidiagonal) a →
      (match (motive := (_ : ℕ × ℕ) × ℕ × ℕ → (_ : ℕ × ℕ) × ℕ × ℕ)
          match (motive := (_ : ℕ × ℕ) × ℕ × ℕ → (_ : ℕ × ℕ) × ℕ × ℕ) a with
          | ⟨(_i, j), (k, l)⟩ => Sigma.mk (β := fun (i : ℕ × ℕ) ↦ ℕ × ℕ) (k, l * j) (l, j) with
        | ⟨(i, _j), (k, l)⟩ => Sigma.mk (β := fun (i : ℕ × ℕ) ↦ ℕ × ℕ) (i * k, l) (i, k)) =
        a
h₄ :
  ∀ (a : (_ : ℕ × ℕ) × ℕ × ℕ),
    Membership.mem (γ := Finset ((_ : ℕ × ℕ) × ℕ × ℕ))
        (n.divisorsAntidiagonal.sigma (α := fun (a : ℕ × ℕ) ↦ ℕ × ℕ) fun (a : ℕ × ℕ) ↦ a.2.divisorsAntidiagonal) a →
      (match (motive := (_ : ℕ × ℕ) × ℕ × ℕ → (_ : ℕ × ℕ) × ℕ × ℕ)
          match (motive := (_ : ℕ × ℕ) × ℕ × ℕ → (_ : ℕ × ℕ) × ℕ × ℕ) a with
          | ⟨(i, _j), (k, l)⟩ => Sigma.mk (β := fun (i : ℕ × ℕ) ↦ ℕ × ℕ) (i * k, l) (i, k) with
        | ⟨(_i, j), (k, l)⟩ => Sigma.mk (β := fun (i : ℕ × ℕ) ↦ ℕ × ℕ) (k, l * j) (l, j)) =
        a
⊢ Eq.{u_2 + 1} (α := M)
    (∑ x ∈ n.divisorsAntidiagonal.sigma (α := fun (a : ℕ × ℕ) ↦ ℕ × ℕ) fun (a : ℕ × ℕ) ↦ a.1.divisorsAntidiagonal,
      HSMul.hSMul (α := R) ((f : (a : ℕ) → R) x.snd (β := fun (i : ℕ × ℕ) ↦ ℕ × ℕ).1 : R)
        (HSMul.hSMul (α := R) (β := M) ((g : (a : ℕ) → R) x.snd (β := fun (i : ℕ × ℕ) ↦ ℕ × ℕ).2 : R)
          ((h : (a : ℕ) → M) x.fst (β := fun (i : ℕ × ℕ) ↦ ℕ × ℕ).2 : M)))
    (∑ x ∈ n.divisorsAntidiagonal.sigma (α := fun (a : ℕ × ℕ) ↦ ℕ × ℕ) fun (a : ℕ × ℕ) ↦ a.2.divisorsAntidiagonal,
      HSMul.hSMul (α := R) ((f : (a : ℕ) → R) x.fst (β := fun (i : ℕ × ℕ) ↦ ℕ × ℕ).1 : R)
        (HSMul.hSMul (α := R) (β := M) ((g : (a : ℕ) → R) x.snd (β := fun (i : ℕ × ℕ) ↦ ℕ × ℕ).1 : R)
          ((h : (a : ℕ) → M) x.snd (β := fun (i : ℕ × ℕ) ↦ ℕ × ℕ).2 : M)))
have h₅ : ∀ (a : (_ : ℕ × ℕ) × ℕ × ℕ),
  Membership.mem (γ := Finset ((_ : ℕ × ℕ) × ℕ × ℕ))
      (n.divisorsAntidiagonal.sigma (α := fun (a : ℕ × ℕ) ↦ ℕ × ℕ) fun (a : ℕ × ℕ) ↦ a.1.divisorsAntidiagonal) a →
    HSMul.hSMul (α := R) ((f : (a : ℕ) → R) a.snd (β := fun (i : ℕ × ℕ) ↦ ℕ × ℕ).1 : R)
        (HSMul.hSMul (α := R) (β := M) ((g : (a : ℕ) → R) a.snd (β := fun (i : ℕ × ℕ) ↦ ℕ × ℕ).2 : R)
          ((h : (a : ℕ) → M) a.fst (β := fun (i : ℕ × ℕ) ↦ ℕ × ℕ).2 : M)) =
      HSMul.hSMul (α := R)
        ((f : (a : ℕ) → R)
            (Sigma.fst (β := fun (i : ℕ × ℕ) ↦ ℕ × ℕ)
                (match (motive := (_ : ℕ × ℕ) × ℕ × ℕ → (_ : ℕ × ℕ) × ℕ × ℕ) a with
                | ⟨(_i, j), (k, l)⟩ => Sigma.mk (β := fun (i : ℕ × ℕ) ↦ ℕ × ℕ) (k, l * j) (l, j))).1 :
          R)
        (HSMul.hSMul (α := R) (β := M)
          ((g : (a : ℕ) → R)
              (Sigma.snd (β := fun (i : ℕ × ℕ) ↦ ℕ × ℕ)
                  (match (motive := (_ : ℕ × ℕ) × ℕ × ℕ → (_ : ℕ × ℕ) × ℕ × ℕ) a with
                  | ⟨(_i, j), (k, l)⟩ => Sigma.mk (β := fun (i : ℕ × ℕ) ↦ ℕ × ℕ) (k, l * j) (l, j))).1 :
            R)
          ((h : (a : ℕ) → M)
              (Sigma.snd (β := fun (i : ℕ × ℕ) ↦ ℕ × ℕ)
                  (match (motive := (_ : ℕ × ℕ) × ℕ × ℕ → (_ : ℕ × ℕ) × ℕ × ℕ) a with
                  | ⟨(_i, j), (k, l)⟩ => Sigma.mk (β := fun (i : ℕ × ℕ) ↦ ℕ × ℕ) (k, l * j) (l, j))).2 :
            M))
Tactic: apply sum_nbij' (fun ⟨⟨_i, j⟩, ⟨k, l⟩⟩ ↦ ⟨(k, l * j), (l, j)⟩)
    (fun ⟨⟨i, _j⟩, ⟨k, l⟩⟩ ↦ ⟨(i * k, l), (i, k)⟩)