-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
refine_1 :
  ∀ (a : ℕ × ℕ)
    (ha :
      a ∈
        {x_1 ∈ Icc 1 ⌊log x / log 2⌋₊ ×ˢ filter Nat.Prime (Ioc 0 ⌊x⌋₊) |
          match (motive := ℕ × ℕ → Prop) x_1 with
          | (k, p) => p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊}),
    (fun (x_1 : ℕ × ℕ)
            (x_2 :
              x_1 ∈
                {x_2 ∈ Icc 1 ⌊log x / log 2⌋₊ ×ˢ filter Nat.Prime (Ioc 0 ⌊x⌋₊) |
                  match (motive := ℕ × ℕ → Prop) x_2 with
                  | (k, p) => p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊}) ↦
          (match (motive :=
              (x_3 : ℕ × ℕ) →
                x_3 ∈
                    {x_4 ∈ Icc 1 ⌊log x / log 2⌋₊ ×ˢ filter Nat.Prime (Ioc 0 ⌊x⌋₊) |
                      match (motive := ℕ × ℕ → Prop) x_4 with
                      | (k, p) => p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊} →
                  ℕ)
              x_1, x_2 with
            | (k, p), x => p ^ k :
            ℕ))
        a ha ∈
      {n ∈ Ioc 0 ⌊x⌋₊ | IsPrimePow n}
⊢ Eq.{u_1 + 1} (α := R) (∑ n ∈ Ioc 0 ⌊x⌋₊ with IsPrimePow n, f n)
    (∑ x ∈ Icc 1 ⌊log x / log 2⌋₊ ×ˢ filter Nat.Prime (Ioc 0 ⌊x⌋₊) with
      match (motive := ℕ × ℕ → Prop) x with
      | (k, p) => p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊,
      match (motive := ℕ × ℕ → R) x with
      | (k, p) => f (p ^ k))
have refine_2 : ∀ (a₁ : ℕ × ℕ)
  (ha₁ :
    a₁ ∈
      {x_1 ∈ Icc 1 ⌊log x / log 2⌋₊ ×ˢ filter Nat.Prime (Ioc 0 ⌊x⌋₊) |
        match (motive := ℕ × ℕ → Prop) x_1 with
        | (k, p) => p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊})
  (a₂ : ℕ × ℕ)
  (ha₂ :
    a₂ ∈
      {x_1 ∈ Icc 1 ⌊log x / log 2⌋₊ ×ˢ filter Nat.Prime (Ioc 0 ⌊x⌋₊) |
        match (motive := ℕ × ℕ → Prop) x_1 with
        | (k, p) => p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊}),
  Eq (α := ℕ)
      ((fun (x_1 : ℕ × ℕ)
            (x_2 :
              x_1 ∈
                {x_2 ∈ Icc 1 ⌊log x / log 2⌋₊ ×ˢ filter Nat.Prime (Ioc 0 ⌊x⌋₊) |
                  match (motive := ℕ × ℕ → Prop) x_2 with
                  | (k, p) => p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊}) ↦
          (match (motive :=
              (x_3 : ℕ × ℕ) →
                x_3 ∈
                    {x_4 ∈ Icc 1 ⌊log x / log 2⌋₊ ×ˢ filter Nat.Prime (Ioc 0 ⌊x⌋₊) |
                      match (motive := ℕ × ℕ → Prop) x_4 with
                      | (k, p) => p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊} →
                  ℕ)
              x_1, x_2 with
            | (k, p), x => p ^ k :
            ℕ))
        a₁ ha₁)
      ((fun (x_1 : ℕ × ℕ)
            (x_2 :
              x_1 ∈
                {x_2 ∈ Icc 1 ⌊log x / log 2⌋₊ ×ˢ filter Nat.Prime (Ioc 0 ⌊x⌋₊) |
                  match (motive := ℕ × ℕ → Prop) x_2 with
                  | (k, p) => p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊}) ↦
          (match (motive :=
              (x_3 : ℕ × ℕ) →
                x_3 ∈
                    {x_4 ∈ Icc 1 ⌊log x / log 2⌋₊ ×ˢ filter Nat.Prime (Ioc 0 ⌊x⌋₊) |
                      match (motive := ℕ × ℕ → Prop) x_4 with
                      | (k, p) => p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊} →
                  ℕ)
              x_1, x_2 with
            | (k, p), x => p ^ k :
            ℕ))
        a₂ ha₂) →
    a₁ = a₂
Tactic: refine (sum_bij (i := fun ⟨k, p⟩ _ ↦ p ^ k) ?_ ?_ ?_ ?_).symm