awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r s : ℝ
hrs : r.HolderConjugate s
rw : Eq (α := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq s k = x}ᶜᶜ {x : ℤ | ∃ (k : ℤ), beattySeq s k = x}
rw₁ rw₂ : Eq (α := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq s k = x} {x : ℤ | ∃ (k : ℤ), beattySeq s k = x}
⊢ Eq (α := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq' r k = x}ᶜ {x : ℤ | ∃ (k : ℤ), beattySeq s k = x}

Tactic:
rw [← compl_beattySeq hrs.symm, compl_compl]

Premises used: compl_compl, Real.HolderConjugate.symm, compl_beattySeq
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r s : ℝ
hrs : r.HolderConjugate s
a : Subset (α := Set ℤ) ({x : ℤ | ∃ k > 0, beattySeq r k = x} ∆ {x : ℤ | ∃ k > 0, beattySeq' s k = x}) {n : ℤ | 0 < n}
a₁ : Subset (α := Set ℤ) {n : ℤ | 0 < n} ({x : ℤ | ∃ k > 0, beattySeq r k = x} ∆ {x : ℤ | ∃ k > 0, beattySeq' s k = x})
⊢ Eq (α := Set ℤ) ({x : ℤ | ∃ k > 0, beattySeq r k = x} ∆ {x : ℤ | ∃ k > 0, beattySeq' s k = x}) {n : ℤ | 0 < n}

Tactic:
apply Set.eq_of_subset_of_subset

Premises used: Set.eq_of_subset_of_subset
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
hk : k > 0
hjk : beattySeq r k = j
a : 1 ≤ (↑k : ℝ) * r
⊢ Membership.mem (γ := Set ℤ) {n : ℤ | 0 < n} j

Tactic:
rw [Set.mem_setOf_eq, ← hjk, beattySeq, Int.floor_pos]

Premises used: Set.mem_setOf_eq, beattySeq, Int.floor_pos
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
hk : k > 0
hjk : beattySeq r k = j
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : 1 ≤ k
⊢ LE.le (α := ℝ) 1 (↑k : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
hk : k > 0
hjk : beattySeq r k = j
⊢ 1 ≤ (↑k : ℝ) * r

Tactic:
exact one_le_mul_of_one_le_of_one_le (by norm_cast) hrs.lt.le

Premises used: LT.lt.le, Real.HolderTriple.lt, one_le_mul_of_one_le_of_one_le
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
hk : k > 0
hjk : beattySeq' s k = j
a : 1 < (↑k : ℝ) * s
⊢ Membership.mem (γ := Set ℤ) {n : ℤ | 0 < n} j

Tactic:
rw [Set.mem_setOf_eq, ← hjk, beattySeq', sub_pos, Int.lt_ceil, Int.cast_one]

Premises used: sub_pos, Int.lt_ceil, Set.mem_setOf_eq, beattySeq', Int.cast_one
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
hk : k > 0
hjk : beattySeq' s k = j
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : 1 ≤ k
⊢ LE.le (α := ℝ) 1 (↑k : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
hk : k > 0
hjk : beattySeq' s k = j
⊢ 1 < (↑k : ℝ) * s

Tactic:
exact one_lt_mul_of_le_of_lt (by norm_cast) hrs.symm.lt

Premises used: Real.HolderConjugate.symm, one_lt_mul_of_le_of_lt, Real.HolderTriple.lt
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
a :
  ∀ (hj : 0 < j),
    Membership.mem (γ := Set ℤ) ({x : ℤ | ∃ k > 0, beattySeq r k = x} ∆ {x : ℤ | ∃ k > 0, beattySeq' s k = x}) j
⊢ Membership.mem (γ := Set ℤ) {n : ℤ | 0 < n} j →
    Membership.mem (γ := Set ℤ) ({x : ℤ | ∃ k > 0, beattySeq r k = x} ∆ {x : ℤ | ∃ k > 0, beattySeq' s k = x}) j

Tactic:
(hj : 0 < j)
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
hj : 0 < j
s_1 : ℝ
hs : s_1 ≥ 0
⊢ Membership.mem (γ := Set ℤ) {x : ℤ | ∃ k > 0, beattySeq s_1 k = x} j ↔
    Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq s_1 k = x} j

Tactic:
⟨fun ⟨k, _, hk⟩ ↦ ⟨k, hk⟩, fun ⟨k, hk⟩ ↦ ⟨k, ?_, hk⟩⟩

Premises used: setOf, Membership.mem, Exists, _private.0.beattySeq_symmDiff_beattySeq'_pos.match_2, GT.gt, beattySeq, And, And.intro, Iff.intro, Exists.intro, _private.0.beattySeq_symmDiff_beattySeq'_pos.match_1, OfNat.ofNat, Eq
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
hj : 0 < j
s_1 : ℝ
hs : s_1 ≥ 0
refine :
  Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq s_1 k = x} j → ∀ (k : ℤ) (hk : beattySeq s_1 k = j), k > 0
⊢ Membership.mem (γ := Set ℤ) {x : ℤ | ∃ k > 0, beattySeq s_1 k = x} j ↔
    Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq s_1 k = x} j

Tactic:
refine ⟨fun ⟨k, _, hk⟩ ↦ ⟨k, hk⟩, fun ⟨k, hk⟩ ↦ ⟨k, ?_, hk⟩⟩
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
hj : 0 < j
s_1 : ℝ
hs : s_1 ≥ 0
h : Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq s_1 k = x} j
k : ℤ
hk : beattySeq s_1 k = j
⊢ 1 ≤ (↑k : ℝ) * s_1

Tactic:
rw [← hk, beattySeq, Int.floor_pos] at hj

Premises used: beattySeq, Int.floor_pos
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
hj : 0 < j
s_1 : ℝ
hs : s_1 ≥ 0
h : Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq s_1 k = x} j
k : ℤ
hk : beattySeq s_1 k = j
hj₁ : 1 ≤ (↑k : ℝ) * s_1
⊢ beattySeq s_1 k = j

Tactic:
rw [← hk, beattySeq, Int.floor_pos] at hj

Premises used: beattySeq, Int.floor_pos
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
s_1 : ℝ
hs : s_1 ≥ 0
h : Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq s_1 k = x} j
k : ℤ
hj : 1 ≤ (↑k : ℝ) * s_1
hk : beattySeq s_1 k = j
⊢ k > 0

Tactic:
exact_mod_cast pos_of_mul_pos_left (zero_lt_one.trans_le hj) hs

Premises used: pos_of_mul_pos_left, zero_lt_one, LT.lt.trans_le
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
hj : 0 < j
⊢ ∀ s ≥ 0,
    Membership.mem (γ := Set ℤ) {x : ℤ | ∃ k > 0, beattySeq s k = x} j ↔
      Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq s k = x} j

Tactic:
have hb₁ : ∀ s ≥ 0, j ∈ {beattySeq s k | k > 0} ↔ j ∈ {beattySeq s k | k} := by
    intro _ hs
    refine ⟨fun ⟨k, _, hk⟩ ↦ ⟨k, hk⟩, fun ⟨k, hk⟩ ↦ ⟨k, ?_, hk⟩⟩
    rw [← hk, beattySeq, Int.floor_pos] at hj
    exact_mod_cast pos_of_mul_pos_left (zero_lt_one.trans_le hj) hs
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
hj : 0 < j
hb₁ :
  ∀ s ≥ 0,
    Membership.mem (γ := Set ℤ) {x : ℤ | ∃ k > 0, beattySeq s k = x} j ↔
      Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq s k = x} j
s_1 : ℝ
hs : s_1 ≥ 0
⊢ Membership.mem (γ := Set ℤ) {x : ℤ | ∃ k > 0, beattySeq' s_1 k = x} j ↔
    Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq' s_1 k = x} j

Tactic:
⟨fun ⟨k, _, hk⟩ ↦ ⟨k, hk⟩, fun ⟨k, hk⟩ ↦ ⟨k, ?_, hk⟩⟩

Premises used: setOf, Membership.mem, Exists, _private.0.beattySeq_symmDiff_beattySeq'_pos.match_3, GT.gt, And, And.intro, Iff.intro, Exists.intro, beattySeq', OfNat.ofNat, Eq, _private.0.beattySeq_symmDiff_beattySeq'_pos.match_4
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
hj : 0 < j
hb₁ :
  ∀ s ≥ 0,
    Membership.mem (γ := Set ℤ) {x : ℤ | ∃ k > 0, beattySeq s k = x} j ↔
      Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq s k = x} j
s_1 : ℝ
hs : s_1 ≥ 0
refine :
  Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq' s_1 k = x} j → ∀ (k : ℤ) (hk : beattySeq' s_1 k = j), k > 0
⊢ Membership.mem (γ := Set ℤ) {x : ℤ | ∃ k > 0, beattySeq' s_1 k = x} j ↔
    Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq' s_1 k = x} j

Tactic:
refine ⟨fun ⟨k, _, hk⟩ ↦ ⟨k, hk⟩, fun ⟨k, hk⟩ ↦ ⟨k, ?_, hk⟩⟩
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
hj : 0 < j
hb₁ :
  ∀ s ≥ 0,
    Membership.mem (γ := Set ℤ) {x : ℤ | ∃ k > 0, beattySeq s k = x} j ↔
      Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq s k = x} j
s_1 : ℝ
hs : s_1 ≥ 0
h : Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq' s_1 k = x} j
k : ℤ
hk : beattySeq' s_1 k = j
⊢ 1 < (↑k : ℝ) * s_1

Tactic:
rw [← hk, beattySeq', sub_pos, Int.lt_ceil, Int.cast_one] at hj

Premises used: sub_pos, Int.lt_ceil, beattySeq', Int.cast_one
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
hj : 0 < j
hb₁ :
  ∀ s ≥ 0,
    Membership.mem (γ := Set ℤ) {x : ℤ | ∃ k > 0, beattySeq s k = x} j ↔
      Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq s k = x} j
s_1 : ℝ
hs : s_1 ≥ 0
h : Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq' s_1 k = x} j
k : ℤ
hk : beattySeq' s_1 k = j
hj₁ : 1 < (↑k : ℝ) * s_1
⊢ beattySeq' s_1 k = j

Tactic:
rw [← hk, beattySeq', sub_pos, Int.lt_ceil, Int.cast_one] at hj

Premises used: sub_pos, Int.lt_ceil, beattySeq', Int.cast_one
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
hb₁ :
  ∀ s ≥ 0,
    Membership.mem (γ := Set ℤ) {x : ℤ | ∃ k > 0, beattySeq s k = x} j ↔
      Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq s k = x} j
s_1 : ℝ
hs : s_1 ≥ 0
h : Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq' s_1 k = x} j
k : ℤ
hj : 1 < (↑k : ℝ) * s_1
hk : beattySeq' s_1 k = j
⊢ k > 0

Tactic:
exact_mod_cast pos_of_mul_pos_left (zero_lt_one.trans hj) hs

Premises used: pos_of_mul_pos_left, zero_lt_one, LT.lt.trans
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
hj : 0 < j
hb₁ :
  ∀ s ≥ 0,
    Membership.mem (γ := Set ℤ) {x : ℤ | ∃ k > 0, beattySeq s k = x} j ↔
      Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq s k = x} j
⊢ ∀ s ≥ 0,
    Membership.mem (γ := Set ℤ) {x : ℤ | ∃ k > 0, beattySeq' s k = x} j ↔
      Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x} j

Tactic:
have hb₂ : ∀ s ≥ 0, j ∈ {beattySeq' s k | k > 0} ↔ j ∈ {beattySeq' s k | k} := by
    intro _ hs
    refine ⟨fun ⟨k, _, hk⟩ ↦ ⟨k, hk⟩, fun ⟨k, hk⟩ ↦ ⟨k, ?_, hk⟩⟩
    rw [← hk, beattySeq', sub_pos, Int.lt_ceil, Int.cast_one] at hj
    exact_mod_cast pos_of_mul_pos_left (zero_lt_one.trans hj) hs
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
hj : 0 < j
hb₁ :
  ∀ s ≥ 0,
    Membership.mem (γ := Set ℤ) {x : ℤ | ∃ k > 0, beattySeq s k = x} j ↔
      Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq s k = x} j
hb₂ :
  ∀ s ≥ 0,
    Membership.mem (γ := Set ℤ) {x : ℤ | ∃ k > 0, beattySeq' s k = x} j ↔
      Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x} j
a : Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq r k = x} j ∨ j ∉ {x : ℤ | ∃ (k : ℤ), beattySeq r k = x}
⊢ Membership.mem (γ := Set ℤ) ({x : ℤ | ∃ k > 0, beattySeq r k = x} ∆ {x : ℤ | ∃ k > 0, beattySeq' s k = x}) j

Tactic:
rw [Set.mem_symmDiff, hb₁ _ hrs.nonneg, hb₂ _ hrs.symm.nonneg, ← compl_beattySeq hrs,
    Set.notMem_compl_iff, Set.mem_compl_iff, and_self, and_self]

Premises used: and_self, Set.mem_symmDiff, Real.HolderConjugate.symm, Set.notMem_compl_iff, compl_beattySeq, Real.HolderTriple.nonneg, Set.mem_compl_iff
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
hj : 0 < j
hb₁ :
  ∀ s ≥ 0,
    Membership.mem (γ := Set ℤ) {x : ℤ | ∃ k > 0, beattySeq s k = x} j ↔
      Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq s k = x} j
hb₂ :
  ∀ s ≥ 0,
    Membership.mem (γ := Set ℤ) {x : ℤ | ∃ k > 0, beattySeq' s k = x} j ↔
      Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x} j
⊢ Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq r k = x} j ∨ j ∉ {x : ℤ | ∃ (k : ℤ), beattySeq r k = x}

Tactic:
or_not

Premises used: or_not
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
hj : 0 < j
hb₁ :
  ∀ s ≥ 0,
    Membership.mem (γ := Set ℤ) {x : ℤ | ∃ k > 0, beattySeq s k = x} j ↔
      Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq s k = x} j
hb₂ :
  ∀ s ≥ 0,
    Membership.mem (γ := Set ℤ) {x : ℤ | ∃ k > 0, beattySeq' s k = x} j ↔
      Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x} j
⊢ Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq r k = x} j ∨ j ∉ {x : ℤ | ∃ (k : ℤ), beattySeq r k = x}

Tactic:
exact or_not

Premises used: or_not
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r s : ℝ
hrs : r.HolderConjugate s
rw : Eq (α := Set ℤ) ({x : ℤ | ∃ k > 0, beattySeq s k = x} ∆ {x : ℤ | ∃ k > 0, beattySeq' r k = x}) {n : ℤ | 0 < n}
rw₁ rw₂ : Eq (α := Set ℤ) {n : ℤ | 0 < n} {n : ℤ | 0 < n}
⊢ Eq (α := Set ℤ) ({x : ℤ | ∃ k > 0, beattySeq' r k = x} ∆ {x : ℤ | ∃ k > 0, beattySeq s k = x}) {n : ℤ | 0 < n}

Tactic:
rw [symmDiff_comm, beattySeq_symmDiff_beattySeq'_pos hrs.symm]

Premises used: symmDiff_comm, Real.HolderConjugate.symm, beattySeq_symmDiff_beattySeq'_pos
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r : ℝ
hr : Irrational r
h : ∀ (x x_1 : ℤ), x_1 > 0 ∧ ⌈(↑x_1 : ℝ) * r⌉ - 1 = x ↔ x_1 > 0 ∧ ⌊(↑x_1 : ℝ) * r⌋ = x
⊢ Eq (α := Set ℤ) {x : ℤ | ∃ k > 0, ⌈(↑k : ℝ) * r⌉ - 1 = x} {x : ℤ | ∃ k > 0, ⌊(↑k : ℝ) * r⌋ = x}

Tactic:
congr! 4
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r : ℝ
hr : Irrational r
x k : ℤ
h : k > 0 → (⌈(↑k : ℝ) * r⌉ - 1 = x ↔ ⌊(↑k : ℝ) * r⌋ = x)
⊢ k > 0 ∧ ⌈(↑k : ℝ) * r⌉ - 1 = x ↔ k > 0 ∧ ⌊(↑k : ℝ) * r⌋ = x

Tactic:
rw [and_congr_right_iff]

Premises used: and_congr_right_iff
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r : ℝ
hr : Irrational r
x k : ℤ
hk : k > 0
h : ⌈(↑k : ℝ) * r⌉ - 1 = ⌊(↑k : ℝ) * r⌋
⊢ ⌈(↑k : ℝ) * r⌉ - 1 = x ↔ ⌊(↑k : ℝ) * r⌋ = x

Tactic:
congr!
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r : ℝ
hr : Irrational r
x k : ℤ
hk : k > 0
h : (↑⌊(↑k : ℝ) * r⌋ : ℝ) < (↑k : ℝ) * r ∧ (↑k : ℝ) * r ≤ HAdd.hAdd (α := ℝ) (↑⌊(↑k : ℝ) * r⌋ : ℝ) 1
⊢ ⌈(↑k : ℝ) * r⌉ - 1 = ⌊(↑k : ℝ) * r⌋

Tactic:
rw [sub_eq_iff_eq_add, Int.ceil_eq_iff, Int.cast_add, Int.cast_one, add_sub_cancel_right]

Premises used: Int.ceil_eq_iff, Int.cast_add, sub_eq_iff_eq_add, add_sub_cancel_right, Int.cast_one
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r : ℝ
hr : Irrational r
x k : ℤ
hk : k > 0
⊢ (↑⌊(↑k : ℝ) * r⌋ : ℝ) < (↑k : ℝ) * r ∧ (↑k : ℝ) * r ≤ HAdd.hAdd (α := ℝ) (↑⌊(↑k : ℝ) * r⌋ : ℝ) 1

Tactic:
⟨(Int.floor_le _).lt_of_ne fun h ↦ ?_, (Int.lt_floor_add_one _).le⟩

Premises used: Int.lt_floor_add_one, LT.lt.le, LE.le.lt_of_ne, And.intro, Int.floor_le
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r : ℝ
hr : Irrational r
x k : ℤ
hk : k > 0
h : ∀ (h : (↑⌊(↑k : ℝ) * r⌋ : ℝ) = (↑k : ℝ) * r), False
⊢ (↑⌊(↑k : ℝ) * r⌋ : ℝ) < (↑k : ℝ) * r ∧ (↑k : ℝ) * r ≤ HAdd.hAdd (α := ℝ) (↑⌊(↑k : ℝ) * r⌋ : ℝ) 1

Tactic:
refine ⟨(Int.floor_le _).lt_of_ne fun h ↦ ?_, (Int.lt_floor_add_one _).le⟩
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r : ℝ
hr : Irrational r
x k : ℤ
hk : k > 0
h : (↑⌊(↑k : ℝ) * r⌋ : ℝ) = (↑k : ℝ) * r
⊢ False

Tactic:
(hr.intCast_mul hk.ne').ne_int ⌊k * r⌋ h.symm

Premises used: Int.cast, HMul.hMul, Int.floor, Irrational.intCast_mul, LT.lt.ne', Eq.symm, Irrational.ne_int
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r : ℝ
hr : Irrational r
x k : ℤ
hk : k > 0
h : (↑⌊(↑k : ℝ) * r⌋ : ℝ) = (↑k : ℝ) * r
⊢ False

Tactic:
exact (hr.intCast_mul hk.ne').ne_int ⌊k * r⌋ h.symm

Premises used: Int.cast, HMul.hMul, Int.floor, Irrational.intCast_mul, LT.lt.ne', Eq.symm, Irrational.ne_int
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r s : ℝ
hrs : r.HolderConjugate s
hr : Irrational r
rw : Eq (α := Set ℤ) ({x : ℤ | ∃ k > 0, beattySeq' r k = x} ∆ {x : ℤ | ∃ k > 0, beattySeq s k = x}) {n : ℤ | 0 < n}
rw₁ rw₂ : Eq (α := Set ℤ) {n : ℤ | 0 < n} {n : ℤ | 0 < n}
⊢ Eq (α := Set ℤ) ({x : ℤ | ∃ k > 0, beattySeq r k = x} ∆ {x : ℤ | ∃ k > 0, beattySeq s k = x}) {n : ℤ | 0 < n}

Tactic:
rw [← hr.beattySeq'_pos_eq, beattySeq'_symmDiff_beattySeq_pos hrs]

Premises used: beattySeq'_symmDiff_beattySeq_pos, Irrational.beattySeq'_pos_eq
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
⊢ Irrational x ↔ ∀ (a b : ℤ), b ≠ 0 → x ≠ HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)

Tactic:
simp [Irrational, Rat.forall, eq_comm]

Premises used: eq_comm, Irrational, Rat.forall
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
a b : ℤ
hx : Irrational (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ))
⊢ (↑(HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ)) : ℝ) = HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
a b : ℤ
hx : Irrational (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ))
⊢ False

Tactic:
exact hx ⟨a / b, by simp⟩

Premises used: Int.cast, HDiv.hDiv, Exists.intro
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
hx : ¬Irrational x
⊢ ∃ (q : ℚ), x = (↑q : ℝ)

Tactic:
grind [Irrational]

Premises used: Irrational
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
a : ℚ
tr : Transcendental ℚ (A := ℝ) (↑a : ℝ)
⊢ False

Tactic:
tr (isAlgebraic_algebraMap a)

Premises used: isAlgebraic_algebraMap
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
a : ℚ
tr : Transcendental ℚ (A := ℝ) (↑a : ℝ)
⊢ False

Tactic:
exact tr (isAlgebraic_algebraMap a)

Premises used: isAlgebraic_algebraMap
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : N.natAbs.Coprime D
hxr : HPow.hPow (α := ℝ) (↑{ num := N, den := D, den_nz := P, reduced := C : ℚ } : ℝ) n = (↑m : ℝ)
hv : ¬∃ (y : ℤ), Eq (α := ℝ) (↑{ num := N, den := D, den_nz := P, reduced := C } : ℝ) (↑y : ℝ)
⊢ Eq (α := ℝ) (↑({ num := N, den := D, den_nz := P, reduced := C : ℚ } ^ n) : ℝ) (↑m : ℝ)

Tactic:
rw [← cast_pow] at hxr

Premises used: Rat.cast_pow
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : N.natAbs.Coprime D
hxr : HPow.hPow (α := ℝ) (↑{ num := N, den := D, den_nz := P, reduced := C : ℚ } : ℝ) n = (↑m : ℝ)
hv : ¬∃ (y : ℤ), Eq (α := ℝ) (↑{ num := N, den := D, den_nz := P, reduced := C } : ℝ) (↑y : ℝ)
hxr₁ : Eq (α := ℝ) (↑({ num := N, den := D, den_nz := P, reduced := C : ℚ } ^ n) : ℝ) (↑m : ℝ)
⊢ ¬∃ (y : ℤ), Eq (α := ℝ) (↑{ num := N, den := D, den_nz := P, reduced := C } : ℝ) (↑y : ℝ)

Tactic:
rw [← cast_pow] at hxr

Premises used: Rat.cast_pow
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : N.natAbs.Coprime D
hxr : Eq (α := ℝ) (↑({ num := N, den := D, den_nz := P, reduced := C : ℚ } ^ n) : ℝ) (↑m : ℝ)
hv : ¬∃ (y : ℤ), Eq (α := ℝ) (↑{ num := N, den := D, den_nz := P, reduced := C } : ℝ) (↑y : ℝ)
rw : D ≠ 0
⊢ Ne (α := ℝ) (↑(↑D : ℤ) : ℝ) 0

Tactic:
rw [Int.cast_ne_zero, Int.natCast_ne_zero]

Premises used: Int.natCast_ne_zero, Int.cast_ne_zero
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : N.natAbs.Coprime D
hxr : Eq (α := ℝ) (↑({ num := N, den := D, den_nz := P, reduced := C : ℚ } ^ n) : ℝ) (↑m : ℝ)
hv : ¬∃ (y : ℤ), Eq (α := ℝ) (↑{ num := N, den := D, den_nz := P, reduced := C } : ℝ) (↑y : ℝ)
⊢ D ≠ 0

Tactic:
P
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : N.natAbs.Coprime D
hxr : Eq (α := ℝ) (↑({ num := N, den := D, den_nz := P, reduced := C : ℚ } ^ n) : ℝ) (↑m : ℝ)
hv : ¬∃ (y : ℤ), Eq (α := ℝ) (↑{ num := N, den := D, den_nz := P, reduced := C } : ℝ) (↑y : ℝ)
⊢ D ≠ 0

Tactic:
exact P
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : N.natAbs.Coprime D
hxr : Eq (α := ℝ) (↑({ num := N, den := D, den_nz := P, reduced := C : ℚ } ^ n) : ℝ) (↑m : ℝ)
hv : ¬∃ (y : ℤ), Eq (α := ℝ) (↑{ num := N, den := D, den_nz := P, reduced := C } : ℝ) (↑y : ℝ)
⊢ Ne (α := ℝ) (↑(↑D : ℤ) : ℝ) 0

Tactic:
have c1 : ((D : ℤ) : ℝ) ≠ 0 := by
    rw [Int.cast_ne_zero, Int.natCast_ne_zero]
    exact P
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : N.natAbs.Coprime D
hxr : Eq (α := ℝ) (↑({ num := N, den := D, den_nz := P, reduced := C : ℚ } ^ n) : ℝ) (↑m : ℝ)
hv : ¬∃ (y : ℤ), Eq (α := ℝ) (↑{ num := N, den := D, den_nz := P, reduced := C } : ℝ) (↑y : ℝ)
c1 : Ne (α := ℝ) (↑(↑D : ℤ) : ℝ) 0
⊢ HPow.hPow (α := ℝ) (↑(↑D : ℤ) : ℝ) n ≠ 0

Tactic:
have c2 : ((D : ℤ) : ℝ) ^ n ≠ 0 := pow_ne_zero _ c1
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : N.natAbs.Coprime D
hxr : Eq (α := ℝ) (↑({ num := N, den := D, den_nz := P, reduced := C : ℚ } ^ n) : ℝ) (↑m : ℝ)
hv : ¬∃ (y : ℤ), Eq (α := ℝ) (↑{ num := N, den := D, den_nz := P, reduced := C } : ℝ) (↑y : ℝ)
c1 : Ne (α := ℝ) (↑(↑D : ℤ) : ℝ) 0
c2 : HPow.hPow (α := ℝ) (↑(↑D : ℤ) : ℝ) n ≠ 0
⊢ m * HPow.hPow (α := ℤ) (↑D : ℤ) n = N ^ n

Tactic:
rw [mk_eq_divInt, cast_pow, cast_divInt, div_pow, div_eq_iff_mul_eq c2, ← Int.cast_pow,
    ← Int.cast_pow, ← Int.cast_mul, Int.cast_inj] at hxr

Premises used: Int.cast_inj, Rat.mk_eq_divInt, Int.cast_pow, div_eq_iff_mul_eq, Int.cast_mul, Rat.cast_divInt, div_pow, Rat.cast_pow
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : N.natAbs.Coprime D
hxr : Eq (α := ℝ) (↑({ num := N, den := D, den_nz := P, reduced := C : ℚ } ^ n) : ℝ) (↑m : ℝ)
hv : ¬∃ (y : ℤ), Eq (α := ℝ) (↑{ num := N, den := D, den_nz := P, reduced := C } : ℝ) (↑y : ℝ)
c1 : Ne (α := ℝ) (↑(↑D : ℤ) : ℝ) 0
c2 : HPow.hPow (α := ℝ) (↑(↑D : ℤ) : ℝ) n ≠ 0
hxr₁ : m * HPow.hPow (α := ℤ) (↑D : ℤ) n = N ^ n
⊢ ¬∃ (y : ℤ), Eq (α := ℝ) (↑{ num := N, den := D, den_nz := P, reduced := C } : ℝ) (↑y : ℝ)

Tactic:
rw [mk_eq_divInt, cast_pow, cast_divInt, div_pow, div_eq_iff_mul_eq c2, ← Int.cast_pow,
    ← Int.cast_pow, ← Int.cast_mul, Int.cast_inj] at hxr

Premises used: Int.cast_inj, Rat.mk_eq_divInt, Int.cast_pow, div_eq_iff_mul_eq, Int.cast_mul, Rat.cast_divInt, div_pow, Rat.cast_pow
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : N.natAbs.Coprime D
hxr : Eq (α := ℝ) (↑({ num := N, den := D, den_nz := P, reduced := C : ℚ } ^ n) : ℝ) (↑m : ℝ)
hv : ¬∃ (y : ℤ), Eq (α := ℝ) (↑{ num := N, den := D, den_nz := P, reduced := C } : ℝ) (↑y : ℝ)
c1 : Ne (α := ℝ) (↑(↑D : ℤ) : ℝ) 0
c2 : HPow.hPow (α := ℝ) (↑(↑D : ℤ) : ℝ) n ≠ 0
hxr₁ : m * HPow.hPow (α := ℤ) (↑D : ℤ) n = N ^ n
hv₁ : ¬∃ (y : ℤ), Eq (α := ℝ) (↑{ num := N, den := D, den_nz := P, reduced := C } : ℝ) (↑y : ℝ)
⊢ Ne (α := ℝ) (↑(↑D : ℤ) : ℝ) 0

Tactic:
rw [mk_eq_divInt, cast_pow, cast_divInt, div_pow, div_eq_iff_mul_eq c2, ← Int.cast_pow,
    ← Int.cast_pow, ← Int.cast_mul, Int.cast_inj] at hxr

Premises used: Int.cast_inj, Rat.mk_eq_divInt, Int.cast_pow, div_eq_iff_mul_eq, Int.cast_mul, Rat.cast_divInt, div_pow, Rat.cast_pow
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : N.natAbs.Coprime D
hxr : Eq (α := ℝ) (↑({ num := N, den := D, den_nz := P, reduced := C : ℚ } ^ n) : ℝ) (↑m : ℝ)
hv : ¬∃ (y : ℤ), Eq (α := ℝ) (↑{ num := N, den := D, den_nz := P, reduced := C } : ℝ) (↑y : ℝ)
c1 : Ne (α := ℝ) (↑(↑D : ℤ) : ℝ) 0
c2 : HPow.hPow (α := ℝ) (↑(↑D : ℤ) : ℝ) n ≠ 0
hxr₁ : m * HPow.hPow (α := ℤ) (↑D : ℤ) n = N ^ n
hv₁ : ¬∃ (y : ℤ), Eq (α := ℝ) (↑{ num := N, den := D, den_nz := P, reduced := C } : ℝ) (↑y : ℝ)
c1₁ : Ne (α := ℝ) (↑(↑D : ℤ) : ℝ) 0
⊢ HPow.hPow (α := ℝ) (↑(↑D : ℤ) : ℝ) n ≠ 0

Tactic:
rw [mk_eq_divInt, cast_pow, cast_divInt, div_pow, div_eq_iff_mul_eq c2, ← Int.cast_pow,
    ← Int.cast_pow, ← Int.cast_mul, Int.cast_inj] at hxr

Premises used: Int.cast_inj, Rat.mk_eq_divInt, Int.cast_pow, div_eq_iff_mul_eq, Int.cast_mul, Rat.cast_divInt, div_pow, Rat.cast_pow
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : N.natAbs.Coprime D
hxr : m * HPow.hPow (α := ℤ) (↑D : ℤ) n = N ^ n
hv : ¬∃ (y : ℤ), Eq (α := ℝ) (↑{ num := N, den := D, den_nz := P, reduced := C } : ℝ) (↑y : ℝ)
c1 : Ne (α := ℝ) (↑(↑D : ℤ) : ℝ) 0
c2 : HPow.hPow (α := ℝ) (↑(↑D : ℤ) : ℝ) n ≠ 0
⊢ HPow.hPow (α := ℤ) (↑D : ℤ) n ∣ N ^ n

Tactic:
have hdivn : (D : ℤ) ^ n ∣ N ^ n := Dvd.intro_left m hxr
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : N.natAbs.Coprime D
hxr : m * HPow.hPow (α := ℤ) (↑D : ℤ) n = N ^ n
hv : ¬∃ (y : ℤ), Eq (α := ℝ) (↑{ num := N, den := D, den_nz := P, reduced := C } : ℝ) (↑y : ℝ)
c1 : Ne (α := ℝ) (↑(↑D : ℤ) : ℝ) 0
c2 : HPow.hPow (α := ℝ) (↑(↑D : ℤ) : ℝ) n ≠ 0
hdivn : HPow.hPow (α := ℤ) (↑D : ℤ) n ∣ N ^ n
⊢ D ∣ N.natAbs

Tactic:
rw [← Int.dvd_natAbs, ← Int.natCast_pow, Int.natCast_dvd_natCast, Int.natAbs_pow,
    Nat.pow_dvd_pow_iff hnpos.ne'] at hdivn

Premises used: Int.dvd_natAbs, Int.natCast_pow, Int.natAbs_pow, Nat.pow_dvd_pow_iff, LT.lt.ne', Int.natCast_dvd_natCast