awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
ι : Sort u_1
inst : Nonempty ι
f : ι → ℝ≥0
n : ℕ
hn : n = 0
⊢ HPow.hPow (α := ℝ≥0) (⨆ (i : ι), f i) n = ⨆ (i : ι), f i ^ n

Tactic:
simp [hn]
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
ι : Sort u_1
inst : Nonempty ι
f : ι → ℝ≥0
n : ℕ
hn : ¬n = 0
⊢ HPow.hPow (α := ℝ≥0) (⨆ (i : ι), f i) n = ⨆ (i : ι), f i ^ n

Tactic:
iSup_pow_of_ne_zero hn _

Premises used: NNReal.iSup_pow_of_ne_zero
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
ι : Sort u_1
inst : Nonempty ι
f : ι → ℝ≥0
n : ℕ
hn : ¬n = 0
⊢ HPow.hPow (α := ℝ≥0) (⨆ (i : ι), f i) n = ⨆ (i : ι), f i ^ n

Tactic:
exact iSup_pow_of_ne_zero hn _

Premises used: NNReal.iSup_pow_of_ne_zero
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
ι : Sort u_1
n_1 n : ℕ
hn : n ≠ 0
zero :
  ∀ (hn : Ne (α := ℕ) 0 0),
    Eq (α := WithTop NNReal → WithTop NNReal) (fun (x : WithTop NNReal) ↦ HPow.hPow (β := ℕ) x 0)
      (⇑(NNReal.powOrderIso 0 hn).withTopCongr : (a : WithTop NNReal) → WithTop NNReal)
succ :
  ∀ (n : ℕ) (hn : n + 1 ≠ 0),
    Eq (α := WithTop NNReal → WithTop NNReal) (fun (x : WithTop NNReal) ↦ x ^ (n + 1))
      (⇑(NNReal.powOrderIso (n + 1) hn).withTopCongr : (a : WithTop NNReal) → WithTop NNReal)
⊢ Eq (α := WithTop NNReal → WithTop NNReal) (fun (x : WithTop NNReal) ↦ x ^ n)
    (⇑(NNReal.powOrderIso n hn).withTopCongr : (a : WithTop NNReal) → WithTop NNReal)

Tactic:
cases n
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
ι : Sort u_1
n : ℕ
hn : Ne (α := ℕ) 0 0
⊢ Eq (α := WithTop NNReal → WithTop NNReal) (fun (x : WithTop NNReal) ↦ HPow.hPow (β := ℕ) x 0)
    (⇑(NNReal.powOrderIso 0 hn).withTopCongr : (a : WithTop NNReal) → WithTop NNReal)

Tactic:
cases hn rfl

Premises used: rfl
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
ι : Sort u_1
n n_1 : ℕ
hn : n_1 + 1 ≠ 0
succ :
  HPow.hPow (α := WithTop NNReal) none (n_1 + 1) =
    ((NNReal.powOrderIso (n_1 + 1) hn).withTopCongr : (a : WithTop NNReal) → WithTop NNReal) none
succ₁ :
  ∀ (val : NNReal),
    some val ^ (n_1 + 1) =
      ((NNReal.powOrderIso (n_1 + 1) hn).withTopCongr : (a : WithTop NNReal) → WithTop NNReal) (some val)
⊢ Eq (α := WithTop NNReal → WithTop NNReal) (fun (x : WithTop NNReal) ↦ x ^ (n_1 + 1))
    (⇑(NNReal.powOrderIso (n_1 + 1) hn).withTopCongr : (a : WithTop NNReal) → WithTop NNReal)

Tactic:
ext (_ | _)
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
ι : Sort u_1
n n_1 : ℕ
hn : n_1 + 1 ≠ 0
⊢ HPow.hPow (α := WithTop NNReal) none (n_1 + 1) =
    ((NNReal.powOrderIso (n_1 + 1) hn).withTopCongr : (a : WithTop NNReal) → WithTop NNReal) none

Tactic:
rfl
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
ι : Sort u_1
n n_1 : ℕ
hn : n_1 + 1 ≠ 0
val : NNReal
⊢ some val ^ (n_1 + 1) =
    ((NNReal.powOrderIso (n_1 + 1) hn).withTopCongr : (a : WithTop NNReal) → WithTop NNReal) (some val)

Tactic:
rfl
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
ι : Sort u_1
n : ℕ
hn : n ≠ 0
f : ι → ℝ≥0∞
⊢ HPow.hPow (α := ℝ≥0∞) (⨆ (i : ι), f i) n = ⨆ (i : ι), f i ^ n

Tactic:
(powOrderIso n hn).map_iSup _

Premises used: OrderIso.map_iSup, ENNReal.powOrderIso
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
ι : Sort u_1
inst : Nonempty ι
f : ι → ℝ≥0∞
n : ℕ
pos : ∀ (hn : n = 0), HPow.hPow (α := ℝ≥0∞) (⨆ (i : ι), f i) n = ⨆ (i : ι), f i ^ n
neg : ∀ (hn : ¬n = 0), HPow.hPow (α := ℝ≥0∞) (⨆ (i : ι), f i) n = ⨆ (i : ι), f i ^ n
⊢ HPow.hPow (α := ℝ≥0∞) (⨆ (i : ι), f i) n = ⨆ (i : ι), f i ^ n

Tactic:
by_cases hn : n = 0
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
ι : Sort u_1
inst : Nonempty ι
f : ι → ℝ≥0∞
n : ℕ
hn : n = 0
⊢ HPow.hPow (α := ℝ≥0∞) (⨆ (i : ι), f i) n = ⨆ (i : ι), f i ^ n

Tactic:
simp [hn]
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
ι : Sort u_1
inst : Nonempty ι
f : ι → ℝ≥0∞
n : ℕ
hn : ¬n = 0
⊢ HPow.hPow (α := ℝ≥0∞) (⨆ (i : ι), f i) n = ⨆ (i : ι), f i ^ n

Tactic:
iSup_pow_of_ne_zero hn _

Premises used: ENNReal.iSup_pow_of_ne_zero
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
ι : Sort u_1
inst : Nonempty ι
f : ι → ℝ≥0∞
n : ℕ
hn : ¬n = 0
⊢ HPow.hPow (α := ℝ≥0∞) (⨆ (i : ι), f i) n = ⨆ (i : ι), f i ^ n

Tactic:
exact iSup_pow_of_ne_zero hn _

Premises used: ENNReal.iSup_pow_of_ne_zero
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
ι : Sort u_1
κ : ι → Sort u_2
f : (i : ι) → κ i → ℝ≥0∞
n : ℕ
hn : n ≠ 0
⊢ HPow.hPow (α := ℝ≥0∞) (⨆ (i : ι), ⨆ (j : κ i), f i j) n = ⨆ (i : ι), ⨆ (j : κ i), f i j ^ n

Tactic:
(powOrderIso n hn).map_iSup₂ f

Premises used: ENNReal.powOrderIso, OrderIso.map_iSup₂
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
ι : Sort u_1
inst : Nonempty ι
f : ι → ℝ
hf : ∀ (i : ι), 0 ≤ f i
n : ℕ
⊢ ∀ (i : ι), 0 ≤ f i

Tactic:
hf
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
ι : Sort u_1
inst : Nonempty ι
f : ι → ℝ
hf : ∀ (i : ι), 0 ≤ f i
n : ℕ
lift :
  ∀ (f : (i : ι) → ℝ≥0),
    HPow.hPow (α := ℝ) (⨆ (i : ι), (fun (i : ι) ↦ (↑(f i) : ℝ)) i) n =
      ⨆ (i : ι), HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) n
⊢ HPow.hPow (α := ℝ) (⨆ (i : ι), f i) n = ⨆ (i : ι), f i ^ n

Tactic:
lift f to ι → ℝ≥0 using hf
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
ι : Sort u_1
inst : Nonempty ι
n : ℕ
f : (i : ι) → ℝ≥0
⊢ HPow.hPow (α := ℝ) (⨆ (i : ι), (↑(f i) : ℝ)) n = ⨆ (i : ι), (↑(f i) : ℝ) ^ n

Tactic:
mod_cast NNReal.iSup_pow f n

Premises used: NNReal.coe_iSup._simp_1, congrArg, cast, HPow.hPow, congr, congrFun', NNReal.coe_inj._simp_1, Eq.symm, Eq, NNReal.iSup_pow, Eq.trans
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
ι : Sort u_1
inst : Nonempty ι
n : ℕ
f : (i : ι) → ℝ≥0
⊢ HPow.hPow (α := ℝ) (⨆ (i : ι), (↑(f i) : ℝ)) n = ⨆ (i : ι), (↑(f i) : ℝ) ^ n

Tactic:
exact mod_cast NNReal.iSup_pow f n

Premises used: NNReal.iSup_pow
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
ι : Sort u_1
n : ℕ
f : ι → ℝ
hf : ∀ (i : ι), 0 ≤ f i
hn : n ≠ 0
inl : IsEmpty ι → HPow.hPow (α := ℝ) (⨆ (i : ι), f i) n = ⨆ (i : ι), f i ^ n
inr : Nonempty ι → HPow.hPow (α := ℝ) (⨆ (i : ι), f i) n = ⨆ (i : ι), f i ^ n
⊢ HPow.hPow (α := ℝ) (⨆ (i : ι), f i) n = ⨆ (i : ι), f i ^ n

Tactic:
cases isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
ι : Sort u_1
n : ℕ
f : ι → ℝ
hf : ∀ (i : ι), 0 ≤ f i
hn : n ≠ 0
h : IsEmpty ι
⊢ HPow.hPow (α := ℝ) (⨆ (i : ι), f i) n = ⨆ (i : ι), f i ^ n

Tactic:
simp [hn]
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
ι : Sort u_1
n : ℕ
f : ι → ℝ
hf : ∀ (i : ι), 0 ≤ f i
hn : n ≠ 0
h : Nonempty ι
⊢ HPow.hPow (α := ℝ) (⨆ (i : ι), f i) n = ⨆ (i : ι), f i ^ n

Tactic:
iSup_pow hf _

Premises used: Real.iSup_pow
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
ι : Sort u_1
n : ℕ
f : ι → ℝ
hf : ∀ (i : ι), 0 ≤ f i
hn : n ≠ 0
h : Nonempty ι
⊢ HPow.hPow (α := ℝ) (⨆ (i : ι), f i) n = ⨆ (i : ι), f i ^ n

Tactic:
exact iSup_pow hf _

Premises used: Real.iSup_pow
-- Module: Mathlib.Topology.Instances.Nat
Goal:
x y : ℕ
⊢ dist x y = |HSub.hSub (α := ℝ) (↑x : ℝ) (↑y : ℝ)|

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Instances.Nat
Goal:
x y : ℕ
⊢ dist (α := ℤ) (↑x : ℤ) (↑y : ℤ) = dist x y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Instances.Nat
Goal:
x y : ℕ
⊢ dist (α := ℝ) (↑x : ℝ) (↑y : ℝ) = dist x y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Instances.Nat
Goal:
⊢ Pairwise fun (m n : ℕ) ↦ 1 ≤ dist m n

Tactic:
fun _ _ hne =>
  Int.pairwise_one_le_dist <| mod_cast hne

Premises used: congrArg, cast, Pairwise, Nat.cast_inj._simp_1, Eq.symm, Not, Int.pairwise_one_le_dist
-- Module: Mathlib.Topology.Instances.Nat
Goal:
⊢ IsUniformEmbedding (β := ℝ) Nat.cast

Tactic:
isUniformEmbedding_bot_of_pairwise_le_dist zero_lt_one pairwise_one_le_dist

Premises used: Nat.pairwise_one_le_dist, zero_lt_one, Metric.isUniformEmbedding_bot_of_pairwise_le_dist
-- Module: Mathlib.Topology.Instances.Nat
Goal:
⊢ IsClosedEmbedding (Y := ℝ) Nat.cast

Tactic:
isClosedEmbedding_of_pairwise_le_dist zero_lt_one pairwise_one_le_dist

Premises used: Nat.pairwise_one_le_dist, zero_lt_one, Metric.isClosedEmbedding_of_pairwise_le_dist
-- Module: Mathlib.Topology.Instances.Nat
Goal:
x : ℕ
r : ℝ
⊢ preimage (β := ℝ) Nat.cast (ball (↑x : ℝ) r) = ball x r

Tactic:
rfl

Premises used: Set.Mem, setOf, Metric.ball, Set.preimage, rfl
-- Module: Mathlib.Topology.Instances.Nat
Goal:
x : ℕ
r : ℝ
⊢ preimage (β := ℝ) Nat.cast (closedBall (↑x : ℝ) r) = closedBall x r

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, Metric.closedBall, rfl
-- Module: Mathlib.Topology.Instances.Nat
Goal:
x : ℕ
r : ℝ
inl : ∀ (hr : 0 ≤ r), closedBall x r = Icc ⌈(↑x : ℝ) - r⌉₊ ⌊(↑x : ℝ) + r⌋₊
inr : ∀ (hr : r < 0), closedBall x r = Icc ⌈(↑x : ℝ) - r⌉₊ ⌊(↑x : ℝ) + r⌋₊
⊢ closedBall x r = Icc ⌈(↑x : ℝ) - r⌉₊ ⌊(↑x : ℝ) + r⌋₊

Tactic:
rcases le_or_gt 0 r with (hr | hr)

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.Topology.Instances.Nat
Goal:
x : ℕ
r : ℝ
hr : 0 ≤ r
inl : 0 ≤ (↑x : ℝ) + r
⊢ closedBall x r = Icc ⌈(↑x : ℝ) - r⌉₊ ⌊(↑x : ℝ) + r⌋₊

Tactic:
rw [← preimage_closedBall, Real.closedBall_eq_Icc, preimage_Icc]

Premises used: Real.closedBall_eq_Icc, Nat.preimage_Icc, Nat.preimage_closedBall
-- Module: Mathlib.Topology.Instances.Nat
Goal:
x : ℕ
r : ℝ
hr : 0 ≤ r
⊢ 0 ≤ (↑x : ℝ) + r

Tactic:
positivity
-- Module: Mathlib.Topology.Instances.Nat
Goal:
x : ℕ
r : ℝ
hr : r < 0
inr : ⌊(↑x : ℝ) + r⌋₊ < ⌈(↑x : ℝ) - r⌉₊
⊢ closedBall x r = Icc ⌈(↑x : ℝ) - r⌉₊ ⌊(↑x : ℝ) + r⌋₊

Tactic:
rw [closedBall_eq_empty.2 hr, Icc_eq_empty_of_lt]

Premises used: Iff.mpr, Metric.closedBall_eq_empty, Set.Icc_eq_empty_of_lt
-- Module: Mathlib.Topology.Instances.Nat
Goal:
x : ℕ
r : ℝ
hr : r < 0
linarith : (↑x : ℝ) < (↑x : ℝ) + r → r - 0 + ((↑x : ℝ) - ((↑x : ℝ) + r)) = 0
⊢ (↑x : ℝ) + r ≤ (↑x : ℝ)

Tactic:
linarith
-- Module: Mathlib.Topology.Instances.Nat
Goal:
x : ℕ
r : ℝ
hr : r < 0
rw : (↑x : ℝ) < (↑x : ℝ) - r
⊢ floor (α := ℝ) (↑x : ℝ) < ⌈(↑x : ℝ) - r⌉₊

Tactic:
rw [floor_natCast, Nat.lt_ceil]

Premises used: Nat.floor_natCast, Nat.lt_ceil
-- Module: Mathlib.Topology.Instances.Nat
Goal:
x : ℕ
r : ℝ
hr : r < 0
linarith : (↑x : ℝ) - r ≤ (↑x : ℝ) → r - 0 + ((↑x : ℝ) - r - (↑x : ℝ)) = 0
⊢ (↑x : ℝ) < (↑x : ℝ) - r

Tactic:
linarith
-- Module: Mathlib.Topology.Instances.Nat
Goal:
x : ℕ
r : ℝ
hr : r < 0
calc : floor (α := ℝ) (↑x : ℝ) < ⌈(↑x : ℝ) - r⌉₊
⊢ ⌊(↑x : ℝ) + r⌋₊ < ⌈(↑x : ℝ) - r⌉₊

Tactic:
calc ⌊(x : ℝ) + r⌋₊ ≤ ⌊(x : ℝ)⌋₊ := floor_mono <| by linarith
    _ < ⌈↑x - r⌉₊ := by
      rw [floor_natCast, Nat.lt_ceil]
      linarith

Premises used: Nat.cast, Nat.floor_mono
-- Module: Mathlib.Topology.Instances.Nat
Goal:
x : ℕ
r : ℝ
rw : IsCompact (Icc ⌈(↑x : ℝ) - r⌉₊ ⌊(↑x : ℝ) + r⌋₊)
⊢ IsCompact (closedBall x r)

Tactic:
rw [closedBall_eq_Icc]

Premises used: Nat.closedBall_eq_Icc
-- Module: Mathlib.Topology.Instances.Nat
Goal:
x : ℕ
r : ℝ
⊢ IsCompact (Icc ⌈(↑x : ℝ) - r⌉₊ ⌊(↑x : ℝ) + r⌋₊)

Tactic:
(Set.finite_Icc _ _).isCompact

Premises used: Set.Finite.isCompact, Set.finite_Icc
-- Module: Mathlib.Topology.Instances.Nat
Goal:
x : ℕ
r : ℝ
⊢ IsCompact (Icc ⌈(↑x : ℝ) - r⌉₊ ⌊(↑x : ℝ) + r⌋₊)

Tactic:
exact (Set.finite_Icc _ _).isCompact

Premises used: Set.Finite.isCompact, Set.finite_Icc
-- Module: Mathlib.Topology.Instances.Nat
Goal:
⊢ ∀ (r : ℝ), BddBelow (α := ℕ) (closedBall 0 r)

Tactic:
simp
-- Module: Mathlib.Topology.Instances.Nat
Goal:
⊢ ∀ (r : ℝ), BddAbove (α := ℕ) (closedBall 0 r)

Tactic:
simp [Nat.closedBall_eq_Icc]

Premises used: Nat.closedBall_eq_Icc
-- Module: Mathlib.Topology.Instances.Nat
Goal:
⊢ (cocompact ℕ).NeBot

Tactic:
simp only [Filter.cocompact_eq_cofinite, Filter.cofinite_neBot]

Premises used: Filter.cofinite_neBot, Filter.cocompact_eq_cofinite
-- Module: Mathlib.Topology.Instances.PNat
Goal:
x y : ℕ+
⊢ dist x y = |HSub.hSub (α := ℝ) (↑(↑x : ℕ) : ℝ) (↑(↑y : ℕ) : ℝ)|

Tactic:
rfl

Premises used: PNat.val, abs, rfl
-- Module: Mathlib.Topology.Instances.PNat
Goal:
x y : ℕ+
⊢ dist (↑x : ℕ) (↑y : ℕ) = dist x y

Tactic:
rfl

Premises used: PNat.val, rfl
-- Module: Mathlib.Topology.Instances.PNat
Goal:
⊢ IsUniformEmbedding val

Tactic:
isUniformEmbedding_subtype_val

Premises used: PNat.val, isUniformEmbedding_subtype_val, PNat
-- Module: Mathlib.Topology.Instances.PNat
Goal:
⊢ DiscreteTopology ℕ+

Tactic:
inferInstanceAs (DiscreteTopology { n : ℕ // 0 < n })

Premises used: _private.0.PNat.instDiscreteTopology._proof_1
-- Module: Mathlib.Topology.Instances.PNat
Goal:
n : ℕ+
r : ℝ
rw : IsCompact (val ⁻¹' Set.Icc ⌈(↑(↑n : ℕ) : ℝ) - r⌉₊ ⌊(↑(↑n : ℕ) : ℝ) + r⌋₊)
⊢ IsCompact (val ⁻¹' closedBall (↑n : ℕ) r)

Tactic:
rw [Nat.closedBall_eq_Icc]

Premises used: Nat.closedBall_eq_Icc
-- Module: Mathlib.Topology.Instances.PNat
Goal:
n : ℕ+
r : ℝ
⊢ IsCompact (val ⁻¹' Set.Icc ⌈(↑(↑n : ℕ) : ℝ) - r⌉₊ ⌊(↑(↑n : ℕ) : ℝ) + r⌋₊)

Tactic:
((Set.finite_Icc _ _).preimage PNat.coe_injective.injOn).isCompact

Premises used: Function.Injective.injOn, PNat.coe_injective, Set.Finite.isCompact, Set.finite_Icc, Set.Finite.preimage
-- Module: Mathlib.Topology.Instances.PNat
Goal:
n : ℕ+
r : ℝ
⊢ IsCompact (val ⁻¹' Set.Icc ⌈(↑(↑n : ℕ) : ℝ) - r⌉₊ ⌊(↑(↑n : ℕ) : ℝ) + r⌋₊)

Tactic:
exact ((Set.finite_Icc _ _).preimage PNat.coe_injective.injOn).isCompact

Premises used: Function.Injective.injOn, PNat.coe_injective, Set.Finite.isCompact, Set.finite_Icc, Set.Finite.preimage
-- Module: Mathlib.Topology.Instances.PNat
Goal:
⊢ (Filter.cocompact ℕ+).NeBot

Tactic:
simp only [Filter.cocompact_eq_cofinite, Filter.cofinite_neBot]

Premises used: Filter.cofinite_neBot, Filter.cocompact_eq_cofinite
-- Module: Mathlib.Topology.Instances.Rat
Goal:
x y : ℚ
⊢ dist x y = |HSub.hSub (α := ℝ) (↑x : ℝ) (↑y : ℝ)|

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Instances.Rat
Goal:
x y : ℚ
⊢ dist (α := ℝ) (↑x : ℝ) (↑y : ℝ) = dist x y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Instances.Rat
Goal:
⊢ UniformContinuous (β := ℝ) Rat.cast

Tactic:
uniformContinuous_comap

Premises used: uniformContinuous_comap
-- Module: Mathlib.Topology.Instances.Rat
Goal:
⊢ IsUniformEmbedding (β := ℝ) Rat.cast

Tactic:
isUniformEmbedding_comap Rat.cast_injective

Premises used: isUniformEmbedding_comap, Rat.cast_injective
-- Module: Mathlib.Topology.Instances.Rat
Goal:
⊢ IsDenseEmbedding (β := ℝ) Rat.cast

Tactic:
isUniformEmbedding_coe_real.isDenseEmbedding Rat.denseRange_cast

Premises used: IsUniformEmbedding.isDenseEmbedding, Rat.denseRange_cast, Rat.isUniformEmbedding_coe_real
-- Module: Mathlib.Topology.Instances.Rat
Goal:
⊢ IsEmbedding (Y := ℝ) Rat.cast

Tactic:
isDenseEmbedding_coe_real.isEmbedding

Premises used: Rat.isDenseEmbedding_coe_real, IsDenseEmbedding.isEmbedding
-- Module: Mathlib.Topology.Instances.Rat
Goal:
⊢ Continuous (Y := ℝ) Rat.cast

Tactic:
uniformContinuous_coe_real.continuous

Premises used: UniformContinuous.continuous, Rat.uniformContinuous_coe_real
-- Module: Mathlib.Topology.Instances.Rat
Goal:
x y : ℕ
⊢ dist (α := ℝ) (↑(↑x : ℚ) : ℝ) (↑(↑y : ℚ) : ℝ) = dist (α := ℝ) (↑x : ℝ) (↑y : ℝ)

Tactic:
congr
-- Module: Mathlib.Topology.Instances.Rat
Goal:
⊢ Pairwise fun (x y : ℕ) ↦ 1 ≤ dist (α := ℚ) (↑x : ℚ) (↑y : ℚ)

Tactic:
simpa using Nat.pairwise_one_le_dist

Premises used: Nat.pairwise_one_le_dist
-- Module: Mathlib.Topology.Instances.Rat
Goal:
x y : ℤ
⊢ dist (α := ℝ) (↑(↑x : ℚ) : ℝ) (↑(↑y : ℚ) : ℝ) = dist (α := ℝ) (↑x : ℝ) (↑y : ℝ)

Tactic:
congr
-- Module: Mathlib.Topology.Instances.Rat
Goal:
⊢ Pairwise fun (x y : ℤ) ↦ 1 ≤ dist (α := ℚ) (↑x : ℚ) (↑y : ℚ)

Tactic:
simpa using Int.pairwise_one_le_dist

Premises used: Int.pairwise_one_le_dist
-- Module: Mathlib.Topology.Instances.Rat
Goal:
⊢ NoncompactSpace ℚ

Tactic:
Int.isClosedEmbedding_coe_rat.noncompactSpace

Premises used: Topology.IsClosedEmbedding.noncompactSpace, Int.isClosedEmbedding_coe_rat
-- Module: Mathlib.Topology.Instances.Rat
Goal:
simp : UniformContinuous (β := ℝ) fun (x : ℚ × ℚ) ↦ HAdd.hAdd (α := ℝ) (↑x.1 : ℝ) (↑x.2 : ℝ)
⊢ UniformContinuous (α := ℚ × ℚ) (β := ℝ) (Rat.cast ∘ fun (p : ℚ × ℚ) ↦ p.1 + p.2)

Tactic:
simp only [Function.comp_def, Rat.cast_add]

Premises used: Function.comp_def, Rat.cast_add
-- Module: Mathlib.Topology.Instances.Rat
Goal:
⊢ UniformContinuous (β := ℝ) fun (x : ℚ × ℚ) ↦ HAdd.hAdd (α := ℝ) (↑x.1 : ℝ) (↑x.2 : ℝ)

Tactic:
Real.uniformContinuous_add.comp
      (Rat.uniformContinuous_coe_real.prodMap Rat.uniformContinuous_coe_real)

Premises used: UniformContinuous.prodMap, UniformContinuous.comp, Real.uniformContinuous_add, Rat.uniformContinuous_coe_real
-- Module: Mathlib.Topology.Instances.Rat
Goal:
⊢ UniformContinuous (β := ℝ) fun (x : ℚ × ℚ) ↦ HAdd.hAdd (α := ℝ) (↑x.1 : ℝ) (↑x.2 : ℝ)

Tactic:
exact Real.uniformContinuous_add.comp
      (Rat.uniformContinuous_coe_real.prodMap Rat.uniformContinuous_coe_real)

Premises used: UniformContinuous.prodMap, UniformContinuous.comp, Real.uniformContinuous_add, Rat.uniformContinuous_coe_real
-- Module: Mathlib.Topology.Instances.Rat
Goal:
ε : ℝ
ε0 : ε > 0
x x_1 : ℚ
h : dist x x_1 < ε
⊢ dist (-x) (-x_1) < ε

Tactic:
simpa only [abs_sub_comm, dist_eq, cast_neg, neg_sub_neg] using h

Premises used: Rat.dist_eq, neg_sub_neg, abs_sub_comm, Rat.cast_neg
-- Module: Mathlib.Topology.Instances.Rat
Goal:
⊢ IsUniformAddGroup ℚ

Tactic:
IsUniformAddGroup.mk' Rat.uniformContinuous_add Rat.uniformContinuous_neg

Premises used: Rat.uniformContinuous_neg, Rat.uniformContinuous_add, IsUniformAddGroup.mk'
-- Module: Mathlib.Topology.Instances.Rat
Goal:
⊢ IsTopologicalAddGroup ℚ

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.Instances.Rat
Goal:
⊢ OrderTopology ℚ

Tactic:
induced_orderTopology _ Rat.cast_lt exists_rat_btwn

Premises used: Rat.cast_lt, exists_rat_btwn, induced_orderTopology
-- Module: Mathlib.Topology.Instances.Rat
Goal:
ε : ℝ
ε0 : ε > 0
x x_1 : ℚ
h : dist x x_1 < ε
⊢ dist |x| |x_1| ≤ dist x x_1

Tactic:
simpa [Rat.dist_eq] using abs_abs_sub_abs_le_abs_sub _ _

Premises used: Rat.dist_eq, abs_abs_sub_abs_le_abs_sub
-- Module: Mathlib.Topology.Instances.Rat
Goal:
⊢ IsTopologicalRing ℚ

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.Instances.Rat
Goal:
a b : ℚ
⊢ TotallyBounded (Icc a b)

Tactic:
simpa only [preimage_cast_Icc]
    using totallyBounded_preimage Rat.isUniformEmbedding_coe_real.isUniformInducing
      (totallyBounded_Icc (a : ℝ) b)

Premises used: Rat.preimage_cast_Icc
-- Module: Mathlib.Topology.Instances.Rat
Goal:
p q : ℚ≥0
⊢ dist p q = dist (α := ℚ) (↑p : ℚ) (↑q : ℚ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Instances.Rat
Goal:
p q : ℚ≥0
⊢ nndist p q = nndist (α := ℚ) (↑p : ℚ) (↑q : ℚ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Instances.Rat
Goal:
⊢ Continuous (Y := ℚ) fun (p : ℚ≥0 × ℚ≥0) ↦ max ((↑p.1 : ℚ) - (↑p.2 : ℚ)) 0

Tactic:
fun_prop
-- Module: Mathlib.Topology.Instances.Rat
Goal:
⊢ OrderTopology ℚ≥0

Tactic:
orderTopology_of_ordConnected (t := Set.Ici 0)

Premises used: Set.Ici, Set.Mem, setOf, NNRat, orderTopology_of_ordConnected
-- Module: Mathlib.Topology.Instances.Rat
Goal:
⊢ ContinuousInv₀ ℚ≥0

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.Instances.Rat
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : MulAction ℚ R
inst_2 : MulAction ℚ≥0 R
inst_3 : IsScalarTower ℚ≥0 ℚ R
inst_4 : ContinuousSMul ℚ R
p : ℚ≥0 × R
rw : HSMul.hSMul (α := ℚ) (↑p.1 : ℚ) p.2
| p.1 • p.2

Tactic:
rw [← NNRat.cast_smul_eq_nnqsmul ℚ]

Premises used: Rat, NNRat.cast_smul_eq_nnqsmul
-- Module: Mathlib.Topology.Instances.Rat
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : MulAction ℚ R
inst_2 : MulAction ℚ≥0 R
inst_3 : IsScalarTower ℚ≥0 ℚ R
inst_4 : ContinuousSMul ℚ R
conv : Continuous[instTopologicalSpaceProd, inst] fun (p : ℚ≥0 × R) ↦ HSMul.hSMul (α := ℚ) (↑p.1 : ℚ) p.2
⊢ Continuous[instTopologicalSpaceProd, inst] fun (p : ℚ≥0 × R) ↦ p.1 • p.2

Tactic:
conv in _ • _ => rw [← NNRat.cast_smul_eq_nnqsmul ℚ]

Premises used: Rat, NNRat.cast_smul_eq_nnqsmul
-- Module: Mathlib.Topology.Instances.Rat
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : MulAction ℚ R
inst_2 : MulAction ℚ≥0 R
inst_3 : IsScalarTower ℚ≥0 ℚ R
inst_4 : ContinuousSMul ℚ R
⊢ Continuous[instTopologicalSpaceProd, inst] fun (p : ℚ≥0 × R) ↦ HSMul.hSMul (α := ℚ) (↑p.1 : ℚ) p.2

Tactic:
fun_prop
-- Module: Mathlib.Topology.Instances.Rat
Goal:
⊢ Continuous (Y := ℝ) fun (p : ℚ≥0 × NNReal) ↦ p.1 • (↑p.2 : ℝ)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Instances.RatLemmas
Goal:
s : Set ℚ
hs : IsCompact s
⊢ interior s = ∅

Tactic:
isDenseEmbedding_coe_real.isDenseInducing.interior_compact_eq_empty dense_irrational hs

Premises used: IsDenseEmbedding.isDenseInducing, Rat.isDenseEmbedding_coe_real, dense_irrational, IsDenseInducing.interior_compact_eq_empty
-- Module: Mathlib.Topology.Instances.RatLemmas
Goal:
s : Set ℚ
hs : IsCompact s
⊢ Dense sᶜ

Tactic:
interior_eq_empty_iff_dense_compl.1 (interior_compact_eq_empty hs)

Premises used: Rat.interior_compact_eq_empty, Iff.mp, interior_eq_empty_iff_dense_compl
-- Module: Mathlib.Topology.Instances.RatLemmas
Goal:
p : ℚ
s : Set ℚ
⊢ (cocompact ℚ ⊓ 𝓝 p).NeBot

Tactic:
(hasBasis_cocompact.inf (nhds_basis_opens _)).neBot_iff.2 ?_

Premises used: Iff.mpr, Filter.HasBasis.inf, Filter.HasBasis.neBot_iff, Filter.hasBasis_cocompact, nhds_basis_opens
-- Module: Mathlib.Topology.Instances.RatLemmas
Goal:
p : ℚ
s : Set ℚ
refine : ∀ {i : Set ℚ × Set ℚ}, IsCompact i.1 ∧ p ∈ i.2 ∧ IsOpen i.2 → (i.1ᶜ ∩ i.2).Nonempty
⊢ (cocompact ℚ ⊓ 𝓝 p).NeBot

Tactic:
refine (hasBasis_cocompact.inf (nhds_basis_opens _)).neBot_iff.2 ?_

Premises used: Iff.mpr, Filter.HasBasis.inf, Filter.HasBasis.neBot_iff, Filter.hasBasis_cocompact, nhds_basis_opens
-- Module: Mathlib.Topology.Instances.RatLemmas
Goal:
p : ℚ
s_1 s o : Set ℚ
hs : IsCompact (s, o).1
hpo : p ∈ (s, o).2
ho : IsOpen (s, o).2
rw : ((s, o).2 ∩ (s, o).1ᶜ).Nonempty
⊢ ((s, o).1ᶜ ∩ (s, o).2).Nonempty

Tactic:
rw [inter_comm]

Premises used: Set.inter_comm
-- Module: Mathlib.Topology.Instances.RatLemmas
Goal:
p : ℚ
s_1 s o : Set ℚ
hs : IsCompact (s, o).1
hpo : p ∈ (s, o).2
ho : IsOpen (s, o).2
⊢ ((s, o).2 ∩ (s, o).1ᶜ).Nonempty

Tactic:
(dense_compl_compact hs).inter_open_nonempty _ ho ⟨p, hpo⟩

Premises used: Dense.inter_open_nonempty, Rat.dense_compl_compact, Exists.intro
-- Module: Mathlib.Topology.Instances.RatLemmas
Goal:
p : ℚ
s_1 s o : Set ℚ
hs : IsCompact (s, o).1
hpo : p ∈ (s, o).2
ho : IsOpen (s, o).2
⊢ ((s, o).2 ∩ (s, o).1ᶜ).Nonempty

Tactic:
exact (dense_compl_compact hs).inter_open_nonempty _ ho ⟨p, hpo⟩

Premises used: Dense.inter_open_nonempty, Rat.dense_compl_compact, Exists.intro
-- Module: Mathlib.Topology.Instances.RatLemmas
Goal:
H : (cocompact ℚ).IsCountablyGenerated
rcases : ∀ (x : ℕ → ℚ) (hx : Tendsto x atTop (cocompact ℚ ⊓ 𝓝 0)), False
⊢ False

Tactic:
rcases exists_seq_tendsto (cocompact ℚ ⊓ 𝓝 0) with ⟨x, hx⟩

Premises used: Rat, nhds, Filter.cocompact, Filter.exists_seq_tendsto, OfNat.ofNat, Min.min
-- Module: Mathlib.Topology.Instances.RatLemmas
Goal:
H : (cocompact ℚ).IsCountablyGenerated
x : ℕ → ℚ
hx : Tendsto x atTop (cocompact ℚ ⊓ 𝓝 0)
⊢ Tendsto x atTop (cocompact ℚ) ∧ Tendsto x atTop (𝓝 0)

Tactic:
rw [tendsto_inf] at hx

Premises used: Filter.tendsto_inf
-- Module: Mathlib.Topology.Instances.RatLemmas
Goal:
H : (cocompact ℚ).IsCountablyGenerated
x : ℕ → ℚ
hx : Tendsto x atTop (cocompact ℚ) ∧ Tendsto x atTop (𝓝 0)
⊢ Tendsto x atTop (cocompact ℚ)

Tactic:
rcases hx with ⟨hxc, hx0⟩
-- Module: Mathlib.Topology.Instances.RatLemmas
Goal:
H : (cocompact ℚ).IsCountablyGenerated
x : ℕ → ℚ
hx : Tendsto x atTop (cocompact ℚ) ∧ Tendsto x atTop (𝓝 0)
hxc : Tendsto x atTop (cocompact ℚ)
⊢ Tendsto x atTop (𝓝 0)

Tactic:
rcases hx with ⟨hxc, hx0⟩
-- Module: Mathlib.Topology.Instances.RatLemmas
Goal:
H : (cocompact ℚ).IsCountablyGenerated
x : ℕ → ℚ
hxc : Tendsto x atTop (cocompact ℚ)
hx0 : Tendsto x atTop (𝓝 0)
⊢ ∃ (n : ℕ), x n ∉ insert 0 (range x)

Tactic:
(hxc.eventually hx0.isCompact_insert_range.compl_mem_cocompact).exists

Premises used: IsCompact.compl_mem_cocompact, Filter.Eventually.exists, Filter.Tendsto.eventually, Filter.Tendsto.isCompact_insert_range