p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
⊢ x ∈ closure (Set.range Int.cast)
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
⊢ DenseRange Int.cast
intro x
case refine_1
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
⊢ IsClosed {b | b ∈ closure (Set.range Int.cast)}

case refine_2
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
⊢ ∀ (a : ℕ), ↑a ∈ closure (Set.range Int.cast)
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
⊢ x ∈ closure (Set.range Int.cast)
refine DenseRange.induction_on denseRange_nat_cast x ?_ ?_
no goals
case refine_1
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
⊢ IsClosed {b | b ∈ closure (Set.range Int.cast)}
exact isClosed_closure
case refine_2
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
a : ℕ
⊢ ↑a ∈ closure (Set.range Int.cast)
case refine_2
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
⊢ ∀ (a : ℕ), ↑a ∈ closure (Set.range Int.cast)
intro a
case refine_2.a
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
a : ℕ
⊢ ↑a ∈ Set.range Int.cast
case refine_2
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
a : ℕ
⊢ ↑a ∈ closure (Set.range Int.cast)
apply subset_closure
no goals
case refine_2.a
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
a : ℕ
⊢ ↑a ∈ Set.range Int.cast
exact Set.mem_range_self _