awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
h₁ : Ne (α := EReal) (⊥, (↑a : EReal)).1 0 ∨ (⊥, (↑a : EReal)).2 ≠ ⊥
h₂ : Ne (α := EReal) (⊥, (↑a : EReal)).1 0 ∨ (⊥, (↑a : EReal)).2 ≠ ⊤
h₄ : Ne (α := EReal) (⊥, (↑a : EReal)).1 ⊤ ∨ (⊥, (↑a : EReal)).2 ≠ 0
h₃ : ¬a = 0
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (⊥, (↑a : EReal))

Tactic:
exact continuousAt_mul_symm1 (continuousAt_mul_top_ne_zero h₃)

Premises used: _private.0.EReal.continuousAt_mul_top_ne_zero, _private.0.EReal.continuousAt_mul_symm1
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
h₁ : Ne (α := EReal) (⊥, ⊤).1 0 ∨ Ne (α := EReal) (⊥, ⊤).2 ⊥
h₂ : Ne (α := EReal) (⊥, ⊤).1 0 ∨ Ne (α := EReal) (⊥, ⊤).2 ⊤
h₃ : Ne (α := EReal) (⊥, ⊤).1 ⊥ ∨ Ne (α := EReal) (⊥, ⊤).2 0
h₄ : Ne (α := EReal) (⊥, ⊤).1 ⊤ ∨ Ne (α := EReal) (⊥, ⊤).2 0
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (⊥, ⊤)

Tactic:
EReal.neg_top ▸ continuousAt_mul_symm1 continuousAt_mul_top_top

Premises used: _private.0.EReal.continuousAt_mul_top_top, Eq.rec, _private.0.EReal.continuousAt_mul_symm1, EReal.neg_top
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
h₁ : Ne (α := EReal) (⊥, ⊤).1 0 ∨ Ne (α := EReal) (⊥, ⊤).2 ⊥
h₂ : Ne (α := EReal) (⊥, ⊤).1 0 ∨ Ne (α := EReal) (⊥, ⊤).2 ⊤
h₃ : Ne (α := EReal) (⊥, ⊤).1 ⊥ ∨ Ne (α := EReal) (⊥, ⊤).2 0
h₄ : Ne (α := EReal) (⊥, ⊤).1 ⊤ ∨ Ne (α := EReal) (⊥, ⊤).2 0
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (⊥, ⊤)

Tactic:
exact EReal.neg_top ▸ continuousAt_mul_symm1 continuousAt_mul_top_top
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
h₁ : ((↑a : EReal), ⊥).1 ≠ 0 ∨ Ne (α := EReal) ((↑a : EReal), ⊥).2 ⊥
h₂ : ((↑a : EReal), ⊥).1 ≠ 0 ∨ Ne (α := EReal) ((↑a : EReal), ⊥).2 ⊤
h₃ : ((↑a : EReal), ⊥).1 ≠ ⊥ ∨ Ne (α := EReal) ((↑a : EReal), ⊥).2 0
h₄ : ((↑a : EReal), ⊥).1 ≠ ⊤ ∨ Ne (α := EReal) ((↑a : EReal), ⊥).2 0
⊢ ¬a = 0

Tactic:
simp only [ne_eq, EReal.coe_eq_zero, not_true_eq_false, or_false] at h₁

Premises used: not_true_eq_false, ne_eq, EReal.coe_eq_zero, or_false
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
h₂ : ((↑a : EReal), ⊥).1 ≠ 0 ∨ Ne (α := EReal) ((↑a : EReal), ⊥).2 ⊤
h₃ : ((↑a : EReal), ⊥).1 ≠ ⊥ ∨ Ne (α := EReal) ((↑a : EReal), ⊥).2 0
h₄ : ((↑a : EReal), ⊥).1 ≠ ⊤ ∨ Ne (α := EReal) ((↑a : EReal), ⊥).2 0
h₁ : ¬a = 0
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) ((↑a : EReal), ⊥)

Tactic:
continuousAt_mul_symm2 (continuousAt_mul_swap (continuousAt_mul_top_ne_zero h₁))

Premises used: _private.0.EReal.continuousAt_mul_swap, _private.0.EReal.continuousAt_mul_top_ne_zero, EReal.neg, _private.0.EReal.continuousAt_mul_symm2
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
h₂ : ((↑a : EReal), ⊥).1 ≠ 0 ∨ Ne (α := EReal) ((↑a : EReal), ⊥).2 ⊤
h₃ : ((↑a : EReal), ⊥).1 ≠ ⊥ ∨ Ne (α := EReal) ((↑a : EReal), ⊥).2 0
h₄ : ((↑a : EReal), ⊥).1 ≠ ⊤ ∨ Ne (α := EReal) ((↑a : EReal), ⊥).2 0
h₁ : ¬a = 0
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) ((↑a : EReal), ⊥)

Tactic:
exact continuousAt_mul_symm2 (continuousAt_mul_swap (continuousAt_mul_top_ne_zero h₁))

Premises used: _private.0.EReal.continuousAt_mul_swap, _private.0.EReal.continuousAt_mul_top_ne_zero, _private.0.EReal.continuousAt_mul_symm2
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a a_1 : ℝ
h₁ : ((↑a : EReal), (↑a_1 : EReal)).1 ≠ 0 ∨ ((↑a : EReal), (↑a_1 : EReal)).2 ≠ ⊥
h₂ : ((↑a : EReal), (↑a_1 : EReal)).1 ≠ 0 ∨ ((↑a : EReal), (↑a_1 : EReal)).2 ≠ ⊤
h₃ : ((↑a : EReal), (↑a_1 : EReal)).1 ≠ ⊥ ∨ ((↑a : EReal), (↑a_1 : EReal)).2 ≠ 0
h₄ : ((↑a : EReal), (↑a_1 : EReal)).1 ≠ ⊤ ∨ ((↑a : EReal), (↑a_1 : EReal)).2 ≠ 0
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) ((↑a : EReal), (↑a_1 : EReal))

Tactic:
continuousAt_mul_coe_coe _ _

Premises used: _private.0.EReal.continuousAt_mul_coe_coe
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a a_1 : ℝ
h₁ : ((↑a : EReal), (↑a_1 : EReal)).1 ≠ 0 ∨ ((↑a : EReal), (↑a_1 : EReal)).2 ≠ ⊥
h₂ : ((↑a : EReal), (↑a_1 : EReal)).1 ≠ 0 ∨ ((↑a : EReal), (↑a_1 : EReal)).2 ≠ ⊤
h₃ : ((↑a : EReal), (↑a_1 : EReal)).1 ≠ ⊥ ∨ ((↑a : EReal), (↑a_1 : EReal)).2 ≠ 0
h₄ : ((↑a : EReal), (↑a_1 : EReal)).1 ≠ ⊤ ∨ ((↑a : EReal), (↑a_1 : EReal)).2 ≠ 0
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) ((↑a : EReal), (↑a_1 : EReal))

Tactic:
exact continuousAt_mul_coe_coe _ _

Premises used: _private.0.EReal.continuousAt_mul_coe_coe
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
h₁ : ((↑a : EReal), ⊤).1 ≠ 0 ∨ Ne (α := EReal) ((↑a : EReal), ⊤).2 ⊥
h₂ : ((↑a : EReal), ⊤).1 ≠ 0 ∨ Ne (α := EReal) ((↑a : EReal), ⊤).2 ⊤
h₃ : ((↑a : EReal), ⊤).1 ≠ ⊥ ∨ Ne (α := EReal) ((↑a : EReal), ⊤).2 0
h₄ : ((↑a : EReal), ⊤).1 ≠ ⊤ ∨ Ne (α := EReal) ((↑a : EReal), ⊤).2 0
⊢ ¬a = 0

Tactic:
simp only [ne_eq, EReal.coe_eq_zero, not_true_eq_false, or_false] at h₂

Premises used: not_true_eq_false, ne_eq, EReal.coe_eq_zero, or_false
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
h₁ : ((↑a : EReal), ⊤).1 ≠ 0 ∨ Ne (α := EReal) ((↑a : EReal), ⊤).2 ⊥
h₃ : ((↑a : EReal), ⊤).1 ≠ ⊥ ∨ Ne (α := EReal) ((↑a : EReal), ⊤).2 0
h₄ : ((↑a : EReal), ⊤).1 ≠ ⊤ ∨ Ne (α := EReal) ((↑a : EReal), ⊤).2 0
h₂ : ¬a = 0
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) ((↑a : EReal), ⊤)

Tactic:
continuousAt_mul_swap (continuousAt_mul_top_ne_zero h₂)

Premises used: _private.0.EReal.continuousAt_mul_swap, _private.0.EReal.continuousAt_mul_top_ne_zero
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
h₁ : ((↑a : EReal), ⊤).1 ≠ 0 ∨ Ne (α := EReal) ((↑a : EReal), ⊤).2 ⊥
h₃ : ((↑a : EReal), ⊤).1 ≠ ⊥ ∨ Ne (α := EReal) ((↑a : EReal), ⊤).2 0
h₄ : ((↑a : EReal), ⊤).1 ≠ ⊤ ∨ Ne (α := EReal) ((↑a : EReal), ⊤).2 0
h₂ : ¬a = 0
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) ((↑a : EReal), ⊤)

Tactic:
exact continuousAt_mul_swap (continuousAt_mul_top_ne_zero h₂)

Premises used: _private.0.EReal.continuousAt_mul_swap, _private.0.EReal.continuousAt_mul_top_ne_zero
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
h₁ : Ne (α := EReal) (⊤, ⊥).1 0 ∨ Ne (α := EReal) (⊤, ⊥).2 ⊥
h₂ : Ne (α := EReal) (⊤, ⊥).1 0 ∨ Ne (α := EReal) (⊤, ⊥).2 ⊤
h₃ : Ne (α := EReal) (⊤, ⊥).1 ⊥ ∨ Ne (α := EReal) (⊤, ⊥).2 0
h₄ : Ne (α := EReal) (⊤, ⊥).1 ⊤ ∨ Ne (α := EReal) (⊤, ⊥).2 0
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (⊤, ⊥)

Tactic:
continuousAt_mul_symm2 continuousAt_mul_top_top

Premises used: _private.0.EReal.continuousAt_mul_top_top, EReal.neg, _private.0.EReal.continuousAt_mul_symm2
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
h₁ : Ne (α := EReal) (⊤, ⊥).1 0 ∨ Ne (α := EReal) (⊤, ⊥).2 ⊥
h₂ : Ne (α := EReal) (⊤, ⊥).1 0 ∨ Ne (α := EReal) (⊤, ⊥).2 ⊤
h₃ : Ne (α := EReal) (⊤, ⊥).1 ⊥ ∨ Ne (α := EReal) (⊤, ⊥).2 0
h₄ : Ne (α := EReal) (⊤, ⊥).1 ⊤ ∨ Ne (α := EReal) (⊤, ⊥).2 0
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (⊤, ⊥)

Tactic:
exact continuousAt_mul_symm2 continuousAt_mul_top_top

Premises used: _private.0.EReal.continuousAt_mul_top_top, _private.0.EReal.continuousAt_mul_symm2
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
h₁ : Ne (α := EReal) (⊤, (↑a : EReal)).1 0 ∨ (⊤, (↑a : EReal)).2 ≠ ⊥
h₂ : Ne (α := EReal) (⊤, (↑a : EReal)).1 0 ∨ (⊤, (↑a : EReal)).2 ≠ ⊤
h₃ : Ne (α := EReal) (⊤, (↑a : EReal)).1 ⊥ ∨ (⊤, (↑a : EReal)).2 ≠ 0
h₄ : Ne (α := EReal) (⊤, (↑a : EReal)).1 ⊤ ∨ (⊤, (↑a : EReal)).2 ≠ 0
⊢ ¬a = 0

Tactic:
simp only [ne_eq, not_true_eq_false, EReal.coe_eq_zero, false_or] at h₄

Premises used: not_true_eq_false, false_or, ne_eq, EReal.coe_eq_zero
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
h₁ : Ne (α := EReal) (⊤, (↑a : EReal)).1 0 ∨ (⊤, (↑a : EReal)).2 ≠ ⊥
h₂ : Ne (α := EReal) (⊤, (↑a : EReal)).1 0 ∨ (⊤, (↑a : EReal)).2 ≠ ⊤
h₃ : Ne (α := EReal) (⊤, (↑a : EReal)).1 ⊥ ∨ (⊤, (↑a : EReal)).2 ≠ 0
h₄ : ¬a = 0
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (⊤, (↑a : EReal))

Tactic:
continuousAt_mul_top_ne_zero h₄

Premises used: _private.0.EReal.continuousAt_mul_top_ne_zero
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
h₁ : Ne (α := EReal) (⊤, (↑a : EReal)).1 0 ∨ (⊤, (↑a : EReal)).2 ≠ ⊥
h₂ : Ne (α := EReal) (⊤, (↑a : EReal)).1 0 ∨ (⊤, (↑a : EReal)).2 ≠ ⊤
h₃ : Ne (α := EReal) (⊤, (↑a : EReal)).1 ⊥ ∨ (⊤, (↑a : EReal)).2 ≠ 0
h₄ : ¬a = 0
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (⊤, (↑a : EReal))

Tactic:
exact continuousAt_mul_top_ne_zero h₄

Premises used: _private.0.EReal.continuousAt_mul_top_ne_zero
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
h₁ : Ne (α := EReal) (⊤, ⊤).1 0 ∨ Ne (α := EReal) (⊤, ⊤).2 ⊥
h₂ : Ne (α := EReal) (⊤, ⊤).1 0 ∨ Ne (α := EReal) (⊤, ⊤).2 ⊤
h₃ : Ne (α := EReal) (⊤, ⊤).1 ⊥ ∨ Ne (α := EReal) (⊤, ⊤).2 0
h₄ : Ne (α := EReal) (⊤, ⊤).1 ⊤ ∨ Ne (α := EReal) (⊤, ⊤).2 0
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (⊤, ⊤)

Tactic:
continuousAt_mul_top_top

Premises used: _private.0.EReal.continuousAt_mul_top_top
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
h₁ : Ne (α := EReal) (⊤, ⊤).1 0 ∨ Ne (α := EReal) (⊤, ⊤).2 ⊥
h₂ : Ne (α := EReal) (⊤, ⊤).1 0 ∨ Ne (α := EReal) (⊤, ⊤).2 ⊤
h₃ : Ne (α := EReal) (⊤, ⊤).1 ⊥ ∨ Ne (α := EReal) (⊤, ⊤).2 0
h₄ : Ne (α := EReal) (⊤, ⊤).1 ⊤ ∨ Ne (α := EReal) (⊤, ⊤).2 0
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (⊤, ⊤)

Tactic:
exact continuousAt_mul_top_top

Premises used: _private.0.EReal.continuousAt_mul_top_top
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a b : EReal
h₁ : a ≠ 0 ∨ b ≠ ⊥
h₂ : a ≠ 0 ∨ b ≠ ⊤
h₃ : a ≠ ⊥ ∨ b ≠ 0
h₄ : a ≠ ⊤ ∨ b ≠ 0
⊢ Tendsto (fun (p : EReal × EReal) ↦ p.1 * p.2) (𝓝 (a, b)) (𝓝 (a * b))

Tactic:
(continuousAt_mul h₁ h₂ h₃ h₄).tendsto

Premises used: ContinuousAt.tendsto, EReal.continuousAt_mul
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_2
f : Filter α
ma mb : α → EReal
a b : EReal
hma : Tendsto ma f (𝓝 a)
hmb : Tendsto mb f (𝓝 b)
h₁ : a ≠ 0 ∨ b ≠ ⊥
h₂ : a ≠ 0 ∨ b ≠ ⊤
h₃ : a ≠ ⊥ ∨ b ≠ 0
h₄ : a ≠ ⊤ ∨ b ≠ 0
⊢ Tendsto (fun (x : α) ↦ ma x * mb x) f (𝓝 (a * b))

Tactic:
(EReal.tendsto_mul h₁ h₂ h₃ h₄).comp (hma.prodMk_nhds hmb)

Premises used: EReal.tendsto_mul, Filter.Tendsto.comp, Filter.Tendsto.prodMk_nhds
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_2
f : Filter α
m : α → EReal
a b : EReal
hm : Tendsto m f (𝓝 b)
h₁ : a ≠ ⊥ ∨ b ≠ 0
h₂ : a ≠ ⊤ ∨ b ≠ 0
this : a = 0
⊢ Tendsto (fun (b : α) ↦ a * m b) f (𝓝 (a * b))

Tactic:
simp [this, tendsto_const_nhds]

Premises used: tendsto_const_nhds
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_2
f : Filter α
m : α → EReal
a b : EReal
hm : Tendsto m f (𝓝 a)
h₁ : a ≠ 0 ∨ b ≠ ⊥
h₂ : a ≠ 0 ∨ b ≠ ⊤
⊢ Tendsto (fun (x : α) ↦ m x * b) f (𝓝 (a * b))

Tactic:
simpa only [mul_comm] using EReal.Tendsto.const_mul hm h₁.symm h₂.symm

Premises used: EReal.Tendsto.const_mul, Or.symm, mul_comm
-- Module: Mathlib.Topology.Instances.Int
Goal:
x y : ℤ
⊢ dist x y = |HSub.hSub (α := ℝ) (↑x : ℝ) (↑y : ℝ)|

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Instances.Int
Goal:
m n : ℤ
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : |m - n| = |m - n|
⊢ |HSub.hSub (α := ℝ) (↑m : ℝ) (↑n : ℝ)| = (↑|m - n| : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.Topology.Instances.Int
Goal:
x y : ℤ
⊢ dist (α := ℝ) (↑x : ℝ) (↑y : ℝ) = dist x y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Instances.Int
Goal:
m n : ℤ
hne : m ≠ n
norm_cast : 1 ≤ |m - n|
⊢ 1 ≤ |HSub.hSub (α := ℝ) (↑m : ℝ) (↑n : ℝ)|

Tactic:
norm_cast
-- Module: Mathlib.Topology.Instances.Int
Goal:
m n : ℤ
hne : m ≠ n
rwa : HAdd.hAdd (α := ℤ) 0 1 ≤ |m - n|
rwa₁ : 0 < |m - n|
rwa₂ : m - n ≠ 0
rwa₃ rwa₄ rwa₅ rwa₆ : m ≠ n
⊢ 1 ≤ |m - n|

Tactic:
rwa [← zero_add (1 : ℤ), Int.add_one_le_iff, abs_pos, sub_ne_zero]

Premises used: sub_ne_zero, Int.add_one_le_iff, zero_add, abs_pos, OfNat.ofNat
-- Module: Mathlib.Topology.Instances.Int
Goal:
⊢ IsUniformEmbedding (β := ℝ) Int.cast

Tactic:
isUniformEmbedding_bot_of_pairwise_le_dist zero_lt_one pairwise_one_le_dist

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

Tactic:
isClosedEmbedding_of_pairwise_le_dist zero_lt_one pairwise_one_le_dist

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

Tactic:
rfl

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

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, Metric.closedBall, rfl
-- Module: Mathlib.Topology.Instances.Int
Goal:
x : ℤ
r : ℝ
rw : preimage (β := ℝ) Int.cast (ball (↑x : ℝ) r) = Ioo ⌊(↑x : ℝ) - r⌋ ⌈(↑x : ℝ) + r⌉
rw₁ : Int.cast ⁻¹' Ioo ((↑x : ℝ) - r) ((↑x : ℝ) + r) = Ioo ⌊(↑x : ℝ) - r⌋ ⌈(↑x : ℝ) + r⌉
rw₂ rw₃ : Ioo ⌊(↑x : ℝ) - r⌋ ⌈(↑x : ℝ) + r⌉ = Ioo ⌊(↑x : ℝ) - r⌋ ⌈(↑x : ℝ) + r⌉
⊢ ball x r = Ioo ⌊(↑x : ℝ) - r⌋ ⌈(↑x : ℝ) + r⌉

Tactic:
rw [← preimage_ball, Real.ball_eq_Ioo, preimage_Ioo]

Premises used: Real.ball_eq_Ioo, Int.preimage_Ioo, Int.preimage_ball
-- Module: Mathlib.Topology.Instances.Int
Goal:
x : ℤ
r : ℝ
rw : preimage (β := ℝ) Int.cast (closedBall (↑x : ℝ) r) = Icc ⌈(↑x : ℝ) - r⌉ ⌊(↑x : ℝ) + r⌋
rw₁ : Int.cast ⁻¹' Icc ((↑x : ℝ) - r) ((↑x : ℝ) + r) = Icc ⌈(↑x : ℝ) - r⌉ ⌊(↑x : ℝ) + r⌋
rw₂ rw₃ : Icc ⌈(↑x : ℝ) - r⌉ ⌊(↑x : ℝ) + r⌋ = Icc ⌈(↑x : ℝ) - r⌉ ⌊(↑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, Int.preimage_Icc, Int.preimage_closedBall
-- Module: Mathlib.Topology.Instances.Int
Goal:
x : ℤ
r : ℝ
rw : IsCompact (Icc ⌈(↑x : ℝ) - r⌉ ⌊(↑x : ℝ) + r⌋)
⊢ IsCompact (closedBall x r)

Tactic:
rw [closedBall_eq_Icc]

Premises used: Int.closedBall_eq_Icc
-- Module: Mathlib.Topology.Instances.Int
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.Int
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.Int
Goal:
⊢ ∀ (r : ℝ), BddBelow (α := ℤ) (closedBall 0 r)

Tactic:
simp [Int.closedBall_eq_Icc]

Premises used: Int.closedBall_eq_Icc
-- Module: Mathlib.Topology.Instances.Int
Goal:
⊢ ∀ (r : ℝ), BddAbove (α := ℤ) (closedBall 0 r)

Tactic:
simp [Int.closedBall_eq_Icc]

Premises used: Int.closedBall_eq_Icc
-- Module: Mathlib.Topology.Instances.Int
Goal:
rw : cocompact ℤ = atBot ⊔ atTop
rw₁ rw₂ : Eq (α := Filter ℤ) (atBot ⊔ atTop) (atBot ⊔ atTop)
⊢ Eq (α := Filter ℤ) cofinite (atBot ⊔ atTop)

Tactic:
rw [← cocompact_eq_cofinite, cocompact_eq_atBot_atTop]

Premises used: cocompact_eq_atBot_atTop, Filter.cocompact_eq_cofinite
-- Module: Mathlib.Topology.Instances.Irrational
Goal:
⊢ IsGδ (X := ℝ) {x : ℝ | Irrational x}

Tactic:
(countable_range _).isGδ_compl

Premises used: setOf, Set.countable_range, Irrational, Set.Countable.isGδ_compl
-- Module: Mathlib.Topology.Instances.Irrational
Goal:
⊢ Dense (X := ℝ) {x : ℝ | Irrational x}

Tactic:
Real.isTopologicalBasis_Ioo_rat.dense_iff.2 ?_

Premises used: Iff.mpr, Real.isTopologicalBasis_Ioo_rat, TopologicalSpace.IsTopologicalBasis.dense_iff
-- Module: Mathlib.Topology.Instances.Irrational
Goal:
refine :
  ∀ (o : Set ℝ),
    Membership.mem (γ := Set (Set ℝ)) (⋃ (a : ℚ), ⋃ (b : ℚ), ⋃ (_ : a < b), {Ioo (↑a : ℝ) (↑b : ℝ)}) o →
      o.Nonempty → (o ∩ {x : ℝ | Irrational x}).Nonempty
⊢ Dense (X := ℝ) {x : ℝ | Irrational x}

Tactic:
refine Real.isTopologicalBasis_Ioo_rat.dense_iff.2 ?_

Premises used: Iff.mpr, Real.isTopologicalBasis_Ioo_rat, TopologicalSpace.IsTopologicalBasis.dense_iff
-- Module: Mathlib.Topology.Instances.Irrational
Goal:
simp :
  ∀ (o : Set ℝ) (x x_1 : ℚ), x < x_1 → o = Ioo (↑x : ℝ) (↑x_1 : ℝ) → o.Nonempty → (o ∩ {x : ℝ | Irrational x}).Nonempty
⊢ ∀ (o : Set ℝ),
    Membership.mem (γ := Set (Set ℝ)) (⋃ (a : ℚ), ⋃ (b : ℚ), ⋃ (_ : a < b), {Ioo (↑a : ℝ) (↑b : ℝ)}) o →
      o.Nonempty → (o ∩ {x : ℝ | Irrational x}).Nonempty

Tactic:
simp only [mem_iUnion, mem_singleton_iff, exists_prop, forall_exists_index, and_imp]

Premises used: and_imp, Set.mem_iUnion, forall_exists_index, exists_prop, Set.mem_singleton_iff
-- Module: Mathlib.Topology.Instances.Irrational
Goal:
a b : ℚ
hlt : a < b
h : Set.Nonempty (α := ℝ) (Ioo (↑a : ℝ) (↑b : ℝ))
rw : Set.Nonempty (α := ℝ) ({x : ℝ | Irrational x} ∩ Ioo (↑a : ℝ) (↑b : ℝ))
⊢ Set.Nonempty (α := ℝ) (Ioo (↑a : ℝ) (↑b : ℝ) ∩ {x : ℝ | Irrational x})

Tactic:
rw [inter_comm]

Premises used: Set.inter_comm
-- Module: Mathlib.Topology.Instances.Irrational
Goal:
a b : ℚ
hlt : a < b
h : Set.Nonempty (α := ℝ) (Ioo (↑a : ℝ) (↑b : ℝ))
⊢ Set.Nonempty (α := ℝ) ({x : ℝ | Irrational x} ∩ Ioo (↑a : ℝ) (↑b : ℝ))

Tactic:
exists_irrational_btwn (Rat.cast_lt.2 hlt)

Premises used: Iff.mpr, Set.Mem, setOf, Rat.cast_lt, Set.inter, Set.Nonempty, Irrational, exists_irrational_btwn, Not, Set.Ioo
-- Module: Mathlib.Topology.Instances.Irrational
Goal:
a b : ℚ
hlt : a < b
h : Set.Nonempty (α := ℝ) (Ioo (↑a : ℝ) (↑b : ℝ))
⊢ Set.Nonempty (α := ℝ) ({x : ℝ | Irrational x} ∩ Ioo (↑a : ℝ) (↑b : ℝ))

Tactic:
exact exists_irrational_btwn (Rat.cast_lt.2 hlt)

Premises used: Iff.mpr, Rat.cast_lt, exists_irrational_btwn
-- Module: Mathlib.Topology.Instances.Irrational
Goal:
⊢ ∀ᶠ (x : ℝ) in residual ℝ, Irrational x

Tactic:
residual_of_dense_Gδ .setOf_irrational dense_irrational

Premises used: Filter.Eventually, dense_irrational, IsGδ.setOf_irrational, residual_of_dense_Gδ
-- Module: Mathlib.Topology.Instances.Irrational
Goal:
x : ℝ
⊢ OrderTopology { x : ℝ // Irrational x }

Tactic:
induced_orderTopology _ Iff.rfl <| @fun _ _ hlt =>
    let ⟨z, hz, hxz, hzy⟩ := exists_irrational_btwn hlt
    ⟨⟨z, hz⟩, hxz, hzy⟩

Premises used: Iff.rfl, Membership.mem, Exists, Subtype.mk, And.intro, Exists.intro, exists_irrational_btwn, _private.0.Irrational.instOrderTopologySubtypeReal.match_1, Subtype.val, Set.Ioo, induced_orderTopology
-- Module: Mathlib.Topology.Instances.Irrational
Goal:
x_1 : ℝ
x_2 : { x : ℝ // Irrational x }
x : ℝ
hx : Irrational x
⊢ Subtype.mk (p := fun (x : ℝ) ↦ Irrational x) x hx < Subtype.mk (p := fun (x : ℝ) ↦ Irrational x) (x + (↑1 : ℝ)) ⋯

Tactic:
simp
-- Module: Mathlib.Topology.Instances.Irrational
Goal:
x_1 : ℝ
x_2 : { x : ℝ // Irrational x }
x : ℝ
hx : Irrational x
⊢ Subtype.mk (p := fun (x : ℝ) ↦ Irrational x) (x - (↑1 : ℝ)) ⋯ < Subtype.mk (p := fun (x : ℝ) ↦ Irrational x) x hx

Tactic:
simp
-- Module: Mathlib.Topology.Instances.Irrational
Goal:
x : ℝ
⊢ DenselyOrdered { x : ℝ // Irrational x }

Tactic:
⟨fun _ _ hlt =>
    let ⟨z, hz, hxz, hzy⟩ := exists_irrational_btwn hlt
    ⟨⟨z, hz⟩, hxz, hzy⟩⟩

Premises used: Exists, DenselyOrdered.mk, Subtype.mk, And, And.intro, LT.lt, Exists.intro, exists_irrational_btwn, _private.0.Irrational.instDenselyOrderedSubtypeReal.match_1
-- Module: Mathlib.Topology.Instances.Irrational
Goal:
x : ℝ
hx : Irrational x
n : ℕ
⊢ IsClosed (X := ℝ) (range fun (m : ℤ) ↦ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑m : ℝ))

Tactic:
have A : IsClosed (range (fun m => (n : ℝ)⁻¹ * m : ℤ → ℝ)) :=
    ((isClosedMap_smul₀ (n⁻¹ : ℝ)).comp Int.isClosedEmbedding_coe_real.isClosedMap).isClosed_range
-- Module: Mathlib.Topology.Instances.Irrational
Goal:
n : ℕ
A : IsClosed (X := ℝ) (range fun (m : ℤ) ↦ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑m : ℝ))
m : ℤ
hx : Irrational ((fun (m : ℤ) ↦ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑m : ℝ)) m)
⊢ False

Tactic:
simp at hx
-- Module: Mathlib.Topology.Instances.Irrational
Goal:
x : ℝ
hx : Irrational x
n : ℕ
A : IsClosed (X := ℝ) (range fun (m : ℤ) ↦ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑m : ℝ))
⊢ x ∉ range fun (m : ℤ) ↦ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑m : ℝ)

Tactic:
have B : x ∉ range (fun m => (n : ℝ)⁻¹ * m : ℤ → ℝ) := by
    rintro ⟨m, rfl⟩
    simp at hx
-- Module: Mathlib.Topology.Instances.Irrational
Goal:
x : ℝ
hx : Irrational x
n : ℕ
A : IsClosed (X := ℝ) (range fun (m : ℤ) ↦ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑m : ℝ))
B : x ∉ range fun (m : ℤ) ↦ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑m : ℝ)
rcases :
  ∀ (ε : ℝ) (ε0 : ε > 0) (hε : ball x ε ⊆ (range fun (m : ℤ) ↦ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑m : ℝ))ᶜ),
    ∀ᶠ (ε : ℝ) in 𝓝 0, ∀ (m : ℤ), ε ≤ dist x (HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ))
⊢ ∀ᶠ (ε : ℝ) in 𝓝 0, ∀ (m : ℤ), ε ≤ dist x (HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ))

Tactic:
rcases Metric.mem_nhds_iff.1 (A.isOpen_compl.mem_nhds B) with ⟨ε, ε0, hε⟩

Premises used: IsClosed.isOpen_compl, Metric.mem_nhds_iff, IsOpen.mem_nhds, Iff.mp
-- Module: Mathlib.Topology.Instances.Irrational
Goal:
x : ℝ
hx : Irrational x
n : ℕ
A : IsClosed (X := ℝ) (range fun (m : ℤ) ↦ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑m : ℝ))
B : x ∉ range fun (m : ℤ) ↦ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑m : ℝ)
ε : ℝ
ε0 : ε > 0
hε : ball x ε ⊆ (range fun (m : ℤ) ↦ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑m : ℝ))ᶜ
⊢ ∀ᶠ (ε : ℝ) in 𝓝 0, ∀ (m : ℤ), ε ≤ dist x (HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ))

Tactic:
(ge_mem_nhds ε0).mono fun δ hδ m => not_lt.1 fun hlt => ?_

Premises used: Filter.Eventually.mono, ge_mem_nhds, not_lt, Iff.mp
-- Module: Mathlib.Topology.Instances.Irrational
Goal:
x : ℝ
hx : Irrational x
n : ℕ
A : IsClosed (X := ℝ) (range fun (m : ℤ) ↦ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑m : ℝ))
B : x ∉ range fun (m : ℤ) ↦ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑m : ℝ)
ε : ℝ
ε0 : ε > 0
hε : ball x ε ⊆ (range fun (m : ℤ) ↦ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑m : ℝ))ᶜ
refine : ∀ (δ : ℝ) (hδ : δ ≤ ε) (m : ℤ) (hlt : dist x (HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)) < δ), False
⊢ ∀ᶠ (ε : ℝ) in 𝓝 0, ∀ (m : ℤ), ε ≤ dist x (HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ))

Tactic:
refine (ge_mem_nhds ε0).mono fun δ hδ m => not_lt.1 fun hlt => ?_

Premises used: Filter.Eventually.mono, ge_mem_nhds
-- Module: Mathlib.Topology.Instances.Irrational
Goal:
x : ℝ
hx : Irrational x
n : ℕ
A : IsClosed (X := ℝ) (range fun (m : ℤ) ↦ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑m : ℝ))
B : x ∉ range fun (m : ℤ) ↦ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑m : ℝ)
ε : ℝ
ε0 : ε > 0
hε : ball x ε ⊆ (range fun (m : ℤ) ↦ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑m : ℝ))ᶜ
δ : ℝ
hδ : δ ≤ ε
m : ℤ
hlt : dist x (HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)) < δ
⊢ dist (HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)) x < δ

Tactic:
rw [dist_comm] at hlt

Premises used: dist_comm
-- Module: Mathlib.Topology.Instances.Irrational
Goal:
x : ℝ
hx : Irrational x
n : ℕ
A : IsClosed (X := ℝ) (range fun (m : ℤ) ↦ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑m : ℝ))
B : x ∉ range fun (m : ℤ) ↦ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑m : ℝ)
ε : ℝ
ε0 : ε > 0
hε : ball x ε ⊆ (range fun (m : ℤ) ↦ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑m : ℝ))ᶜ
δ : ℝ
hδ : δ ≤ ε
m : ℤ
hlt : dist (HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)) x < δ
⊢ False

Tactic:
hε (ball_subset_ball hδ hlt) ⟨m, ?_⟩

Premises used: Metric.ball_subset_ball, Exists.intro
-- Module: Mathlib.Topology.Instances.Irrational
Goal:
x : ℝ
hx : Irrational x
n : ℕ
A : IsClosed (X := ℝ) (range fun (m : ℤ) ↦ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑m : ℝ))
B : x ∉ range fun (m : ℤ) ↦ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑m : ℝ)
ε : ℝ
ε0 : ε > 0
hε : ball x ε ⊆ (range fun (m : ℤ) ↦ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑m : ℝ))ᶜ
δ : ℝ
hδ : δ ≤ ε
m : ℤ
hlt : dist (HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)) x < δ
refine : (fun (m : ℤ) ↦ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑m : ℝ)) m = HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
⊢ False

Tactic:
refine hε (ball_subset_ball hδ hlt) ⟨m, ?_⟩

Premises used: Metric.ball_subset_ball, Exists.intro
-- Module: Mathlib.Topology.Instances.Irrational
Goal:
x : ℝ
hx : Irrational x
n : ℕ
A : IsClosed (X := ℝ) (range fun (m : ℤ) ↦ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑m : ℝ))
B : x ∉ range fun (m : ℤ) ↦ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑m : ℝ)
ε : ℝ
ε0 : ε > 0
hε : ball x ε ⊆ (range fun (m : ℤ) ↦ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑m : ℝ))ᶜ
δ : ℝ
hδ : δ ≤ ε
m : ℤ
hlt : dist (HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)) x < δ
⊢ (fun (m : ℤ) ↦ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑m : ℝ)) m = HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)

Tactic:
simp [div_eq_inv_mul]

Premises used: div_eq_inv_mul