awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
h₁ : (↑j : ℝ) / r ≤ (↑k : ℝ) ∧ (↑k : ℝ) < HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r
m : ℤ
h₂ : (↑j : ℝ) / s < (↑m : ℝ) ∧ (↑m : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / s
h₃ : j < k + m
h₄ : k + m ≤ j
⊢ False

Tactic:
h₄.not_gt h₃

Premises used: LE.le.not_gt
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
h₁ : (↑j : ℝ) / r ≤ (↑k : ℝ) ∧ (↑k : ℝ) < HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r
m : ℤ
h₂ : (↑j : ℝ) / s < (↑m : ℝ) ∧ (↑m : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / s
h₃ : j < k + m
h₄ : k + m ≤ j
⊢ False

Tactic:
exact h₄.not_gt h₃

Premises used: LE.le.not_gt
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j k m : ℤ
h₁₁ : (↑k : ℝ) < (↑j : ℝ) / r
h₁₂ : HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r ≤ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1
h₂₁ : (↑m : ℝ) ≤ (↑j : ℝ) / s
h₂₂ : HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / s < HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
⊢ HAdd.hAdd (α := ℝ) (↑k : ℝ) (↑m : ℝ) < (↑j : ℝ) / r + (↑j : ℝ) / s

Tactic:
have h₃ := add_lt_add_of_lt_of_le h₁₁ h₂₁
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j k m : ℤ
h₁₁ : (↑k : ℝ) < (↑j : ℝ) / r
h₁₂ : HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r ≤ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1
h₂₁ : (↑m : ℝ) ≤ (↑j : ℝ) / s
h₂₂ : HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / s < HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
h₃ : HAdd.hAdd (α := ℝ) (↑k : ℝ) (↑m : ℝ) < (↑j : ℝ) / r + (↑j : ℝ) / s
⊢ HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r + HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / s <
    HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 + HAdd.hAdd (α := ℝ) (↑m : ℝ) 1

Tactic:
have h₄ := add_lt_add_of_le_of_lt h₁₂ h₂₂
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j k m : ℤ
h₁₁ : (↑k : ℝ) < (↑j : ℝ) / r
h₁₂ : HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r ≤ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1
h₂₁ : (↑m : ℝ) ≤ (↑j : ℝ) / s
h₂₂ : HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / s < HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
h₃ : HAdd.hAdd (α := ℝ) (↑k : ℝ) (↑m : ℝ) < (↑j : ℝ) / r + (↑j : ℝ) / s
h₄ :
  HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r + HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / s <
    HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 + HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
⊢ HAdd.hAdd (α := ℝ) (↑k : ℝ) (↑m : ℝ) < (↑j : ℝ)

Tactic:
simp_rw [div_eq_inv_mul, ← right_distrib, hrs.inv_add_inv_eq_one, one_mul] at h₃ h₄

Premises used: Real.HolderConjugate.inv_add_inv_eq_one, right_distrib, div_eq_inv_mul, one_mul
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j k m : ℤ
h₁₁ : (↑k : ℝ) < (↑j : ℝ) / r
h₁₂ : HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r ≤ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1
h₂₁ : (↑m : ℝ) ≤ (↑j : ℝ) / s
h₂₂ : HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / s < HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
h₃ : HAdd.hAdd (α := ℝ) (↑k : ℝ) (↑m : ℝ) < (↑j : ℝ) / r + (↑j : ℝ) / s
h₄ :
  HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r + HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / s <
    HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 + HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
h₅ : HAdd.hAdd (α := ℝ) (↑k : ℝ) (↑m : ℝ) < (↑j : ℝ)
⊢ HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 + HAdd.hAdd (α := ℝ) (↑m : ℝ) 1

Tactic:
simp_rw [div_eq_inv_mul, ← right_distrib, hrs.inv_add_inv_eq_one, one_mul] at h₃ h₄

Premises used: Real.HolderConjugate.inv_add_inv_eq_one, right_distrib, div_eq_inv_mul, one_mul
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j k m : ℤ
h₁₁ : (↑k : ℝ) < (↑j : ℝ) / r
h₁₂ : HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r ≤ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1
h₂₁ : (↑m : ℝ) ≤ (↑j : ℝ) / s
h₂₂ : HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / s < HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
h₃ : HAdd.hAdd (α := ℝ) (↑k : ℝ) (↑m : ℝ) < (↑j : ℝ)
h₄ : HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 + HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
⊢ (↑j : ℝ) < HAdd.hAdd (α := ℝ) (↑k : ℝ) (↑m : ℝ) + (↑1 : ℝ)

Tactic:
rw [← Int.cast_one, ← add_assoc, add_lt_add_iff_right, add_right_comm] at h₄

Premises used: add_assoc, add_right_comm, add_lt_add_iff_right, Int.cast_one
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j k m : ℤ
h₁₁ : (↑k : ℝ) < (↑j : ℝ) / r
h₁₂ : HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r ≤ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1
h₂₁ : (↑m : ℝ) ≤ (↑j : ℝ) / s
h₂₂ : HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / s < HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
h₃ : HAdd.hAdd (α := ℝ) (↑k : ℝ) (↑m : ℝ) < (↑j : ℝ)
h₄ : (↑j : ℝ) < HAdd.hAdd (α := ℝ) (↑k : ℝ) (↑m : ℝ) + (↑1 : ℝ)
⊢ k + m < j

Tactic:
simp_rw [← Int.cast_add, Int.cast_lt, Int.lt_add_one_iff] at h₃ h₄

Premises used: Int.cast_add, Int.cast_lt, Int.lt_add_one_iff
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j k m : ℤ
h₁₁ : (↑k : ℝ) < (↑j : ℝ) / r
h₁₂ : HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r ≤ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1
h₂₁ : (↑m : ℝ) ≤ (↑j : ℝ) / s
h₂₂ : HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / s < HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
h₃ : HAdd.hAdd (α := ℝ) (↑k : ℝ) (↑m : ℝ) < (↑j : ℝ)
h₄ : (↑j : ℝ) < HAdd.hAdd (α := ℝ) (↑k : ℝ) (↑m : ℝ) + (↑1 : ℝ)
h₅ : k + m < j
⊢ j ≤ k + m

Tactic:
simp_rw [← Int.cast_add, Int.cast_lt, Int.lt_add_one_iff] at h₃ h₄

Premises used: Int.cast_add, Int.cast_lt, Int.lt_add_one_iff
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j k m : ℤ
h₁₁ : (↑k : ℝ) < (↑j : ℝ) / r
h₁₂ : HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r ≤ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1
h₂₁ : (↑m : ℝ) ≤ (↑j : ℝ) / s
h₂₂ : HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / s < HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
h₃ : k + m < j
h₄ : j ≤ k + m
⊢ False

Tactic:
h₄.not_gt h₃

Premises used: LE.le.not_gt
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j k m : ℤ
h₁₁ : (↑k : ℝ) < (↑j : ℝ) / r
h₁₂ : HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r ≤ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1
h₂₁ : (↑m : ℝ) ≤ (↑j : ℝ) / s
h₂₂ : HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / s < HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
h₃ : k + m < j
h₄ : j ≤ k + m
⊢ False

Tactic:
exact h₄.not_gt h₃

Premises used: LE.le.not_gt
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r : ℝ
j : ℤ
h : r > 0
inl :
  HSub.hSub (α := ℝ) (↑⌈HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌉ : ℝ) 1 * r < (↑j : ℝ) →
    Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq r k = x} j ∨
      ∃ (k : ℤ), (↑k : ℝ) < (↑j : ℝ) / r ∧ HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r ≤ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1
inr :
  (↑j : ℝ) ≤ HSub.hSub (α := ℝ) (↑⌈HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌉ : ℝ) 1 * r →
    Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq r k = x} j ∨
      ∃ (k : ℤ), (↑k : ℝ) < (↑j : ℝ) / r ∧ HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r ≤ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1
⊢ Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq r k = x} j ∨
    ∃ (k : ℤ), (↑k : ℝ) < (↑j : ℝ) / r ∧ HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r ≤ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1

Tactic:
cases lt_or_ge ((⌈(j + 1) / r⌉ - 1) * r) j

Premises used: Int.cast, HMul.hMul, HSub.hSub, HDiv.hDiv, HAdd.hAdd, lt_or_ge, Int.ceil, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r : ℝ
j : ℤ
h : r > 0
h_1 : HSub.hSub (α := ℝ) (↑⌈HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌉ : ℝ) 1 * r < (↑j : ℝ)
⊢ Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq r k = x} j ∨
    ∃ (k : ℤ), (↑k : ℝ) < (↑j : ℝ) / r ∧ HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r ≤ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1

Tactic:
Or.inr ⟨⌈(j + 1) / r⌉ - 1, ?_⟩

Premises used: Int.cast, HSub.hSub, HDiv.hDiv, HAdd.hAdd, Exists.intro, Int.ceil, OfNat.ofNat, Or.inr
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r : ℝ
j : ℤ
h : r > 0
h_1 : HSub.hSub (α := ℝ) (↑⌈HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌉ : ℝ) 1 * r < (↑j : ℝ)
inl :
  (↑(⌈HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌉ - 1) : ℝ) < (↑j : ℝ) / r ∧
    HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r ≤ HAdd.hAdd (α := ℝ) (↑(⌈HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌉ - 1) : ℝ) 1
⊢ Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq r k = x} j ∨
    ∃ (k : ℤ), (↑k : ℝ) < (↑j : ℝ) / r ∧ HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r ≤ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1

Tactic:
refine Or.inr ⟨⌈(j + 1) / r⌉ - 1, ?_⟩

Premises used: Or.inr
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r : ℝ
j : ℤ
h : r > 0
h_1 : HSub.hSub (α := ℝ) (↑⌈HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌉ : ℝ) 1 * r < (↑j : ℝ)
inl :
  HSub.hSub (α := ℝ) (↑⌈HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌉ : ℝ) 1 * r < (↑j : ℝ) ∧
    HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r ≤ (↑⌈HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌉ : ℝ)
⊢ (↑(⌈HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌉ - 1) : ℝ) < (↑j : ℝ) / r ∧
    HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r ≤ HAdd.hAdd (α := ℝ) (↑(⌈HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌉ - 1) : ℝ) 1

Tactic:
rw [Int.cast_sub, Int.cast_one, lt_div_iff₀ h, sub_add_cancel]

Premises used: lt_div_iff₀, Int.cast_sub, sub_add_cancel, Int.cast_one
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r : ℝ
j : ℤ
h : r > 0
h_1 : HSub.hSub (α := ℝ) (↑⌈HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌉ : ℝ) 1 * r < (↑j : ℝ)
⊢ HSub.hSub (α := ℝ) (↑⌈HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌉ : ℝ) 1 * r < (↑j : ℝ) ∧
    HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r ≤ (↑⌈HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌉ : ℝ)

Tactic:
⟨‹_›, Int.le_ceil _⟩

Premises used: Int.le_ceil, And.intro
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r : ℝ
j : ℤ
h : r > 0
h_1 : HSub.hSub (α := ℝ) (↑⌈HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌉ : ℝ) 1 * r < (↑j : ℝ)
⊢ HSub.hSub (α := ℝ) (↑⌈HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌉ : ℝ) 1 * r < (↑j : ℝ) ∧
    HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r ≤ (↑⌈HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌉ : ℝ)

Tactic:
exact ⟨‹_›, Int.le_ceil _⟩
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r : ℝ
j : ℤ
h : r > 0
h_1 : (↑j : ℝ) ≤ HSub.hSub (α := ℝ) (↑⌈HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌉ : ℝ) 1 * r
⊢ Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq r k = x} j ∨
    ∃ (k : ℤ), (↑k : ℝ) < (↑j : ℝ) / r ∧ HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r ≤ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1

Tactic:
Or.inl ⟨⌈(j + 1) / r⌉ - 1, ?_⟩

Premises used: Int.cast, HSub.hSub, HDiv.hDiv, HAdd.hAdd, Exists.intro, Or.inl, Int.ceil, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r : ℝ
j : ℤ
h : r > 0
h_1 : (↑j : ℝ) ≤ HSub.hSub (α := ℝ) (↑⌈HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌉ : ℝ) 1 * r
inr : beattySeq r (⌈HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌉ - 1) = j
⊢ Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq r k = x} j ∨
    ∃ (k : ℤ), (↑k : ℝ) < (↑j : ℝ) / r ∧ HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r ≤ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1

Tactic:
refine Or.inl ⟨⌈(j + 1) / r⌉ - 1, ?_⟩

Premises used: Or.inl
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r : ℝ
j : ℤ
h : r > 0
h_1 : (↑j : ℝ) ≤ HSub.hSub (α := ℝ) (↑⌈HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌉ : ℝ) 1 * r
inr :
  (↑j : ℝ) ≤ HSub.hSub (α := ℝ) (↑⌈HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌉ : ℝ) 1 * r ∧
    (↑⌈HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌉ : ℝ) < HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r + 1
⊢ beattySeq r (⌈HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌉ - 1) = j

Tactic:
rw [beattySeq, Int.floor_eq_iff, Int.cast_sub, Int.cast_one, ← lt_div_iff₀ h, sub_lt_iff_lt_add]

Premises used: lt_div_iff₀, Int.cast_sub, Int.floor_eq_iff, beattySeq, sub_lt_iff_lt_add, Int.cast_one
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r : ℝ
j : ℤ
h : r > 0
h_1 : (↑j : ℝ) ≤ HSub.hSub (α := ℝ) (↑⌈HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌉ : ℝ) 1 * r
⊢ (↑j : ℝ) ≤ HSub.hSub (α := ℝ) (↑⌈HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌉ : ℝ) 1 * r ∧
    (↑⌈HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌉ : ℝ) < HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r + 1

Tactic:
⟨‹_›, Int.ceil_lt_add_one _⟩

Premises used: Int.ceil_lt_add_one, And.intro
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r : ℝ
j : ℤ
h : r > 0
h_1 : (↑j : ℝ) ≤ HSub.hSub (α := ℝ) (↑⌈HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌉ : ℝ) 1 * r
⊢ (↑j : ℝ) ≤ HSub.hSub (α := ℝ) (↑⌈HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌉ : ℝ) 1 * r ∧
    (↑⌈HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌉ : ℝ) < HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r + 1

Tactic:
exact ⟨‹_›, Int.ceil_lt_add_one _⟩
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r : ℝ
j : ℤ
h : r > 0
inl :
  (↑⌊HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌋ : ℝ) * r ≤ (↑j : ℝ) →
    Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq' r k = x} j ∨
      ∃ (k : ℤ), (↑k : ℝ) ≤ (↑j : ℝ) / r ∧ HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r < HAdd.hAdd (α := ℝ) (↑k : ℝ) 1
inr :
  (↑j : ℝ) < (↑⌊HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌋ : ℝ) * r →
    Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq' r k = x} j ∨
      ∃ (k : ℤ), (↑k : ℝ) ≤ (↑j : ℝ) / r ∧ HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r < HAdd.hAdd (α := ℝ) (↑k : ℝ) 1
⊢ Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq' r k = x} j ∨
    ∃ (k : ℤ), (↑k : ℝ) ≤ (↑j : ℝ) / r ∧ HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r < HAdd.hAdd (α := ℝ) (↑k : ℝ) 1

Tactic:
cases le_or_gt (⌊(j + 1) / r⌋ * r) j

Premises used: Int.cast, HMul.hMul, Int.floor, HDiv.hDiv, le_or_gt, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r : ℝ
j : ℤ
h : r > 0
h_1 : (↑⌊HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌋ : ℝ) * r ≤ (↑j : ℝ)
⊢ Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq' r k = x} j ∨
    ∃ (k : ℤ), (↑k : ℝ) ≤ (↑j : ℝ) / r ∧ HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r < HAdd.hAdd (α := ℝ) (↑k : ℝ) 1

Tactic:
Or.inr ⟨⌊(j + 1) / r⌋, (le_div_iff₀ h).2 ‹_›, Int.lt_floor_add_one _⟩

Premises used: Iff.mpr, Int.cast, Int.floor, Int.lt_floor_add_one, HDiv.hDiv, HAdd.hAdd, And.intro, Exists.intro, le_div_iff₀, OfNat.ofNat, Or.inr
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r : ℝ
j : ℤ
h : r > 0
h_1 : (↑⌊HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌋ : ℝ) * r ≤ (↑j : ℝ)
⊢ Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq' r k = x} j ∨
    ∃ (k : ℤ), (↑k : ℝ) ≤ (↑j : ℝ) / r ∧ HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r < HAdd.hAdd (α := ℝ) (↑k : ℝ) 1

Tactic:
exact Or.inr ⟨⌊(j + 1) / r⌋, (le_div_iff₀ h).2 ‹_›, Int.lt_floor_add_one _⟩

Premises used: Or.inr
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r : ℝ
j : ℤ
h : r > 0
h_1 : (↑j : ℝ) < (↑⌊HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌋ : ℝ) * r
⊢ Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq' r k = x} j ∨
    ∃ (k : ℤ), (↑k : ℝ) ≤ (↑j : ℝ) / r ∧ HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r < HAdd.hAdd (α := ℝ) (↑k : ℝ) 1

Tactic:
Or.inl ⟨⌊(j + 1) / r⌋, ?_⟩

Premises used: Int.cast, Int.floor, HDiv.hDiv, HAdd.hAdd, Exists.intro, Or.inl, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r : ℝ
j : ℤ
h : r > 0
h_1 : (↑j : ℝ) < (↑⌊HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌋ : ℝ) * r
inr : beattySeq' r ⌊HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌋ = j
⊢ Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq' r k = x} j ∨
    ∃ (k : ℤ), (↑k : ℝ) ≤ (↑j : ℝ) / r ∧ HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r < HAdd.hAdd (α := ℝ) (↑k : ℝ) 1

Tactic:
refine Or.inl ⟨⌊(j + 1) / r⌋, ?_⟩

Premises used: Or.inl
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r : ℝ
j : ℤ
h : r > 0
h_1 : (↑j : ℝ) < (↑⌊HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌋ : ℝ) * r
inr :
  HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 - 1 < (↑⌊HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌋ : ℝ) * r ∧
    (↑⌊HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌋ : ℝ) * r ≤ HAdd.hAdd (α := ℝ) (↑j : ℝ) 1
⊢ beattySeq' r ⌊HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌋ = j

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

Premises used: Int.ceil_eq_iff, Int.cast_add, sub_eq_iff_eq_add, beattySeq', Int.cast_one
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r : ℝ
j : ℤ
h : r > 0
h_1 : (↑j : ℝ) < (↑⌊HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌋ : ℝ) * r
inr : HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 - 1 < (↑⌊HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌋ : ℝ) * r
inr₁ : (↑⌊HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌋ : ℝ) * r ≤ HAdd.hAdd (α := ℝ) (↑j : ℝ) 1
⊢ HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 - 1 < (↑⌊HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌋ : ℝ) * r ∧
    (↑⌊HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌋ : ℝ) * r ≤ HAdd.hAdd (α := ℝ) (↑j : ℝ) 1

Tactic:
constructor
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r : ℝ
j : ℤ
h : r > 0
h_1 : (↑j : ℝ) < (↑⌊HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌋ : ℝ) * r
inr inr₁ inr₂ inr₃ : (↑j : ℝ) < (↑⌊HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌋ : ℝ) * r
⊢ HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 - 1 < (↑⌊HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌋ : ℝ) * r

Tactic:
rwa [add_sub_cancel_right]

Premises used: add_sub_cancel_right
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r : ℝ
j : ℤ
h : r > 0
h_1 : (↑j : ℝ) < (↑⌊HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌋ : ℝ) * r
⊢ (↑⌊HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌋ : ℝ) * r ≤ HAdd.hAdd (α := ℝ) (↑j : ℝ) 1

Tactic:
sub_nonneg.1 (Int.sub_floor_div_mul_nonneg (j + 1 : ℝ) h)

Premises used: Int.cast, Int.sub_floor_div_mul_nonneg, HAdd.hAdd, Iff.mp, OfNat.ofNat, sub_nonneg
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r : ℝ
j : ℤ
h : r > 0
h_1 : (↑j : ℝ) < (↑⌊HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌋ : ℝ) * r
⊢ (↑⌊HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌋ : ℝ) * r ≤ HAdd.hAdd (α := ℝ) (↑j : ℝ) 1

Tactic:
exact sub_nonneg.1 (Int.sub_floor_div_mul_nonneg (j + 1 : ℝ) h)

Premises used: Int.cast, Int.sub_floor_div_mul_nonneg, HAdd.hAdd, Iff.mp, OfNat.ofNat, sub_nonneg
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r s : ℝ
hrs : r.HolderConjugate s
h :
  ∀ (j : ℤ),
    Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq r k = x}ᶜ j ↔
      Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x} j
⊢ Eq (α := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq r k = x}ᶜ {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x}

Tactic:
ext j
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
pos :
  ∀ (h₁ : Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq r k = x} j),
    Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq r k = x}ᶜ j ↔
      Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x} j
neg :
  ∀ (h₁ : j ∉ {x : ℤ | ∃ (k : ℤ), beattySeq r k = x}),
    Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq r k = x}ᶜ j ↔
      Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x} j
⊢ Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq r k = x}ᶜ j ↔
    Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x} j

Tactic:
by_cases h₁ : j ∈ {beattySeq r k | k}
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
h₁ : Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq r k = x} j
pos :
  ∀ (h₂ : Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x} j),
    Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq r k = x}ᶜ j ↔
      Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x} j
neg :
  ∀ (h₂ : j ∉ {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x}),
    Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq r k = x}ᶜ j ↔
      Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x} j
⊢ Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq r k = x}ᶜ j ↔
    Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x} j

Tactic:
by_cases h₂ : j ∈ {beattySeq' s k | k}
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
h₁ : j ∉ {x : ℤ | ∃ (k : ℤ), beattySeq r k = x}
pos :
  ∀ (h₂ : Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x} j),
    Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq r k = x}ᶜ j ↔
      Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x} j
neg :
  ∀ (h₂ : j ∉ {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x}),
    Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq r k = x}ᶜ j ↔
      Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x} j
⊢ Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq r k = x}ᶜ j ↔
    Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x} j

Tactic:
by_cases h₂ : j ∈ {beattySeq' s k | k}
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
h₁ : Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq r k = x} j
h₂ : Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x} j
⊢ Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq r k = x}ᶜ j ↔
    Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x} j

Tactic:
(Set.not_disjoint_iff.2 ⟨j, h₁, h₂⟩ (Beatty.no_collision hrs)).elim

Premises used: Iff.mpr, _private.0.Beatty.no_collision, False.elim, Set.not_disjoint_iff, And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
h₁ : Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq r k = x} j
h₂ : Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x} j
⊢ Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq r k = x}ᶜ j ↔
    Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x} j

Tactic:
exact (Set.not_disjoint_iff.2 ⟨j, h₁, h₂⟩ (Beatty.no_collision hrs)).elim

Premises used: Iff.mpr, _private.0.Beatty.no_collision, False.elim, Set.not_disjoint_iff, And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
h₁ : Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq r k = x} j
h₂ : j ∉ {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x}
⊢ Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq r k = x}ᶜ j ↔
    Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x} j

Tactic:
simp only [Set.mem_compl_iff, h₁, h₂, not_true_eq_false]

Premises used: not_true_eq_false, Set.mem_compl_iff
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
h₁ : j ∉ {x : ℤ | ∃ (k : ℤ), beattySeq r k = x}
h₂ : Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x} j
⊢ Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq r k = x}ᶜ j ↔
    Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x} j

Tactic:
simp only [Set.mem_compl_iff, h₁, h₂, not_false_eq_true]

Premises used: not_false_eq_true, Set.mem_compl_iff
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
h₁ : j ∉ {x : ℤ | ∃ (k : ℤ), beattySeq r k = x}
h₂ : j ∉ {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x}
neg :
  ∀ (k : ℤ) (h₁₁ : (↑k : ℝ) < (↑j : ℝ) / r) (h₁₂ : HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r ≤ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1),
    Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq r k = x}ᶜ j ↔
      Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x} j
⊢ Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq r k = x}ᶜ j ↔
    Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x} j

Tactic:
have ⟨k, h₁₁, h₁₂⟩ := (Beatty.hit_or_miss hrs.pos).resolve_left h₁
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
h₁ : j ∉ {x : ℤ | ∃ (k : ℤ), beattySeq r k = x}
h₂ : j ∉ {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x}
k : ℤ
h₁₁ : (↑k : ℝ) < (↑j : ℝ) / r
h₁₂ : HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r ≤ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1
neg :
  ∀ (m : ℤ) (h₂₁ : (↑m : ℝ) ≤ (↑j : ℝ) / s) (h₂₂ : HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / s < HAdd.hAdd (α := ℝ) (↑m : ℝ) 1),
    Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq r k = x}ᶜ j ↔
      Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x} j
⊢ Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq r k = x}ᶜ j ↔
    Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x} j

Tactic:
have ⟨m, h₂₁, h₂₂⟩ := (Beatty.hit_or_miss' hrs.symm.pos).resolve_left h₂
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
h₁ : j ∉ {x : ℤ | ∃ (k : ℤ), beattySeq r k = x}
h₂ : j ∉ {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x}
k : ℤ
h₁₁ : (↑k : ℝ) < (↑j : ℝ) / r
h₁₂ : HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r ≤ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1
m : ℤ
h₂₁ : (↑m : ℝ) ≤ (↑j : ℝ) / s
h₂₂ : HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / s < HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
⊢ Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq r k = x}ᶜ j ↔
    Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x} j

Tactic:
(Beatty.no_anticollision hrs ⟨j, k, m, h₁₁, h₁₂, h₂₁, h₂₂⟩).elim

Premises used: False.elim, _private.0.Beatty.no_anticollision, And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
h₁ : j ∉ {x : ℤ | ∃ (k : ℤ), beattySeq r k = x}
h₂ : j ∉ {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x}
k : ℤ
h₁₁ : (↑k : ℝ) < (↑j : ℝ) / r
h₁₂ : HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r ≤ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1
m : ℤ
h₂₁ : (↑m : ℝ) ≤ (↑j : ℝ) / s
h₂₂ : HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / s < HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
⊢ Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq r k = x}ᶜ j ↔
    Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x} j

Tactic:
exact (Beatty.no_anticollision hrs ⟨j, k, m, h₁₁, h₁₂, h₂₁, h₂₂⟩).elim

Premises used: False.elim, _private.0.Beatty.no_anticollision, And.intro, Exists.intro