Theorem: Finset_coe_Nat_Int (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
f : ℤ → ℂ
m n : ℕ
⊢ ∑ x ∈ Finset.Ioc m n, f ↑x = ∑ x ∈ Finset.Ioc ↑m ↑n, f x
Tactic:
apply Finset.sum_nbij (i := (fun (x : ℕ) ↦ (x : ℤ))) ?_ ?_ ?_ fun _ _ ↦ rfl
State after:
f : ℤ → ℂ
m n : ℕ
⊢ ∀ a ∈ Finset.Ioc m n, (fun x => ↑x) a ∈ Finset.Ioc ↑m ↑n

f : ℤ → ℂ
m n : ℕ
⊢ InjOn (fun x => ↑x) ↑(Finset.Ioc m n)

f : ℤ → ℂ
m n : ℕ
⊢ SurjOn (fun x => ↑x) ↑(Finset.Ioc m n) ↑(Finset.Ioc ↑m ↑n)

State before:
f : ℤ → ℂ
m n : ℕ
⊢ ∀ a ∈ Finset.Ioc m n, (fun x => ↑x) a ∈ Finset.Ioc ↑m ↑n
Tactic:
intro x hx
State after:
f : ℤ → ℂ
m n x : ℕ
hx : x ∈ Finset.Ioc m n
⊢ (fun x => ↑x) x ∈ Finset.Ioc ↑m ↑n

State before:
f : ℤ → ℂ
m n x : ℕ
hx : x ∈ Finset.Ioc m n
⊢ (fun x => ↑x) x ∈ Finset.Ioc ↑m ↑n
Tactic:
simp only [Finset.mem_Ioc, Nat.cast_lt, Nat.cast_le] at hx ⊢
State after:
f : ℤ → ℂ
m n x : ℕ
hx : m < x ∧ x ≤ n
⊢ m < x ∧ x ≤ n

State before:
f : ℤ → ℂ
m n x : ℕ
hx : m < x ∧ x ≤ n
⊢ m < x ∧ x ≤ n
Tactic:
exact hx
State after:
no goals

State before:
f : ℤ → ℂ
m n : ℕ
⊢ InjOn (fun x => ↑x) ↑(Finset.Ioc m n)
Tactic:
intro x₁ _ x₂ _ h
State after:
f : ℤ → ℂ
m n x₁ : ℕ
a✝¹ : x₁ ∈ ↑(Finset.Ioc m n)
x₂ : ℕ
a✝ : x₂ ∈ ↑(Finset.Ioc m n)
h : (fun x => ↑x) x₁ = (fun x => ↑x) x₂
⊢ x₁ = x₂

State before:
f : ℤ → ℂ
m n x₁ : ℕ
a✝¹ : x₁ ∈ ↑(Finset.Ioc m n)
x₂ : ℕ
a✝ : x₂ ∈ ↑(Finset.Ioc m n)
h : (fun x => ↑x) x₁ = (fun x => ↑x) x₂
⊢ x₁ = x₂
Tactic:
simp only [Nat.cast_inj] at h
State after:
f : ℤ → ℂ
m n x₁ : ℕ
a✝¹ : x₁ ∈ ↑(Finset.Ioc m n)
x₂ : ℕ
a✝ : x₂ ∈ ↑(Finset.Ioc m n)
h : x₁ = x₂
⊢ x₁ = x₂

State before:
f : ℤ → ℂ
m n x₁ : ℕ
a✝¹ : x₁ ∈ ↑(Finset.Ioc m n)
x₂ : ℕ
a✝ : x₂ ∈ ↑(Finset.Ioc m n)
h : x₁ = x₂
⊢ x₁ = x₂
Tactic:
exact h
State after:
no goals

State before:
f : ℤ → ℂ
m n : ℕ
⊢ SurjOn (fun x => ↑x) ↑(Finset.Ioc m n) ↑(Finset.Ioc ↑m ↑n)
Tactic:
intro x hx
State after:
f : ℤ → ℂ
m n : ℕ
x : ℤ
hx : x ∈ ↑(Finset.Ioc ↑m ↑n)
⊢ x ∈ (fun x => ↑x) '' ↑(Finset.Ioc m n)

State before:
f : ℤ → ℂ
m n : ℕ
x : ℤ
hx : x ∈ ↑(Finset.Ioc ↑m ↑n)
⊢ x ∈ (fun x => ↑x) '' ↑(Finset.Ioc m n)
Tactic:
simp only [Finset.coe_Ioc, mem_image, mem_Ioc] at hx ⊢
State after:
f : ℤ → ℂ
m n : ℕ
x : ℤ
hx : ↑m < x ∧ x ≤ ↑n
⊢ ∃ x_1, (m < x_1 ∧ x_1 ≤ n) ∧ ↑x_1 = x

State before:
f : ℤ → ℂ
m n : ℕ
x : ℤ
hx : ↑m < x ∧ x ≤ ↑n
⊢ ∃ x_1, (m < x_1 ∧ x_1 ≤ n) ∧ ↑x_1 = x
Tactic:
lift x to ℕ using (by linarith)
State after:
case intro
f : ℤ → ℂ
m n x : ℕ
hx : ↑m < ↑x ∧ ↑x ≤ ↑n
⊢ ∃ x_1, (m < x_1 ∧ x_1 ≤ n) ∧ ↑x_1 = ↑x

State before:
case intro
f : ℤ → ℂ
m n x : ℕ
hx : ↑m < ↑x ∧ ↑x ≤ ↑n
⊢ ∃ x_1, (m < x_1 ∧ x_1 ≤ n) ∧ ↑x_1 = ↑x
Tactic:
exact ⟨x, by exact_mod_cast hx, rfl⟩
State after:
no goals

State before:
f : ℤ → ℂ
m n : ℕ
x : ℤ
hx : ↑m < x ∧ x ≤ ↑n
⊢ 0 ≤ x
Tactic:
linarith
State after:
no goals

State before:
f : ℤ → ℂ
m n x : ℕ
hx : ↑m < ↑x ∧ ↑x ≤ ↑n
⊢ m < x ∧ x ≤ n
Tactic:
exact_mod_cast hx
State after:
no goals