Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
⊢ ∀ (a : ℕ × ℕ)
    (ha :
      a ∈
        {x_1 ∈ Icc 1 N ×ˢ filter Nat.Prime (Ioc 0 ⌊x⌋₊) |
          match x_1 with
          | (k, p) => p ≤ ⌊x ^ (↑k)⁻¹⌋₊}),
    (match a, ha with
      | (k, p), x => p ^ k) ∈
      {n ∈ Ioc 0 ⌊x⌋₊ | IsPrimePow n}

pp: case refine_2
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
⊢ ∀ (a₁ : ℕ × ℕ)
    (ha₁ :
      a₁ ∈
        {x_1 ∈ Icc 1 N ×ˢ filter Nat.Prime (Ioc 0 ⌊x⌋₊) |
          match x_1 with
          | (k, p) => p ≤ ⌊x ^ (↑k)⁻¹⌋₊})
    (a₂ : ℕ × ℕ)
    (ha₂ :
      a₂ ∈
        {x_1 ∈ Icc 1 N ×ˢ filter Nat.Prime (Ioc 0 ⌊x⌋₊) |
          match x_1 with
          | (k, p) => p ≤ ⌊x ^ (↑k)⁻¹⌋₊}),
    ((match a₁, ha₁ with
        | (k, p), x => p ^ k) =
        match a₂, ha₂ with
        | (k, p), x => p ^ k) →
      a₁ = a₂

pp: case refine_3
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
⊢ ∀ b ∈ {n ∈ Ioc 0 ⌊x⌋₊ | IsPrimePow n},
    ∃ a,
      ∃ (ha :
        a ∈
          {x_1 ∈ Icc 1 N ×ˢ filter Nat.Prime (Ioc 0 ⌊x⌋₊) |
            match x_1 with
            | (k, p) => p ≤ ⌊x ^ (↑k)⁻¹⌋₊}),
        (match a, ha with
          | (k, p), x => p ^ k) =
          b

pp: case refine_4
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
⊢ ∀ (a : ℕ × ℕ)
    (ha :
      a ∈
        {x_1 ∈ Icc 1 N ×ˢ filter Nat.Prime (Ioc 0 ⌊x⌋₊) |
          match x_1 with
          | (k, p) => p ≤ ⌊x ^ (↑k)⁻¹⌋₊}),
    (match a with
      | (k, p) => f (p ^ k)) =
      f
        (match a, ha with
        | (k, p), x => p ^ k)

Tactic:
· simp +contextual [hx, rpow_nonneg, le_floor_iff, ← pos_iff_ne_zero, Prime.isPrimePow,
        one_le_iff_ne_zero, le_rpow_inv_iff_of_pos, isPrimePow_pow_iff, prime_iff]

Goal state after:
case refine_2
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
⊢ ∀ (a₁ : ℕ × ℕ)
    (ha₁ :
      a₁ ∈
        {x_1 ∈ Icc 1 N ×ˢ filter Nat.Prime (Ioc 0 ⌊x⌋₊) |
          match x_1 with
          | (k, p) => p ≤ ⌊x ^ (↑k)⁻¹⌋₊})
    (a₂ : ℕ × ℕ)
    (ha₂ :
      a₂ ∈
        {x_1 ∈ Icc 1 N ×ˢ filter Nat.Prime (Ioc 0 ⌊x⌋₊) |
          match x_1 with
          | (k, p) => p ≤ ⌊x ^ (↑k)⁻¹⌋₊}),
    ((match a₁, ha₁ with
        | (k, p), x => p ^ k) =
        match a₂, ha₂ with
        | (k, p), x => p ^ k) →
      a₁ = a₂

case refine_3
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
⊢ ∀ b ∈ {n ∈ Ioc 0 ⌊x⌋₊ | IsPrimePow n},
    ∃ a,
      ∃ (ha :
        a ∈
          {x_1 ∈ Icc 1 N ×ˢ filter Nat.Prime (Ioc 0 ⌊x⌋₊) |
            match x_1 with
            | (k, p) => p ≤ ⌊x ^ (↑k)⁻¹⌋₊}),
        (match a, ha with
          | (k, p), x => p ^ k) =
          b

case refine_4
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
⊢ ∀ (a : ℕ × ℕ)
    (ha :
      a ∈
        {x_1 ∈ Icc 1 N ×ˢ filter Nat.Prime (Ioc 0 ⌊x⌋₊) |
          match x_1 with
          | (k, p) => p ≤ ⌊x ^ (↑k)⁻¹⌋₊}),
    (match a with
      | (k, p) => f (p ^ k)) =
      f
        (match a, ha with
        | (k, p), x => p ^ k)