-- 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}
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₂
⊢ 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_3 : ∀ b ∈ {n ∈ Ioc 0 ⌊x⌋₊ | IsPrimePow n},
  ∃ (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 =
      b
Tactic: refine (sum_bij (i := fun ⟨k, p⟩ _ ↦ p ^ k) ?_ ?_ ?_ ?_).symm