awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (hypothesis)
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 : ℝ)
⊢ False
have h₆ : 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₄
Cleared hypotheses: h₃, h₄
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (hypothesis)
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
⊢ False
have h₅ : (↑j : ℝ) < HAdd.hAdd (α := ℝ) (↑k : ℝ) (↑m : ℝ) + (↑1 : ℝ)
Tactic: rw [← Int.cast_one, ← add_assoc, add_lt_add_iff_right, add_right_comm] at h₄
Cleared hypotheses: h₄
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (hypothesis)
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 : ℝ)
⊢ False
have h₅ : k + m < j
Tactic: simp_rw [← Int.cast_add, Int.cast_lt, Int.lt_add_one_iff] at h₃ h₄
Cleared hypotheses: h₃, h₄
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (hypothesis)
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
⊢ False
have h₆ : j ≤ k + m
Tactic: simp_rw [← Int.cast_add, Int.cast_lt, Int.lt_add_one_iff] at h₃ h₄
Cleared hypotheses: h₃, h₄
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (goal)
Goal:
r : ℝ
j : ℤ
h : r > 0
⊢ Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq r k = x} j ∨
    ∃ (k : ℤ), (↑k : ℝ) < (↑j : ℝ) / r ∧ HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r ≤ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1
have 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
Tactic: cases lt_or_ge ((⌈(j + 1) / r⌉ - 1) * r) j
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (goal)
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
⊢ Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq r k = x} j ∨
    ∃ (k : ℤ), (↑k : ℝ) < (↑j : ℝ) / r ∧ HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r ≤ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1
have 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
Tactic: cases lt_or_ge ((⌈(j + 1) / r⌉ - 1) * r) j
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (goal)
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
have inl : (↑(⌈HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌉ - 1) : ℝ) < (↑j : ℝ) / r ∧
  HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r ≤ HAdd.hAdd (α := ℝ) (↑(⌈HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌉ - 1) : ℝ) 1
Tactic: refine Or.inr ⟨⌈(j + 1) / r⌉ - 1, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (goal)
Goal:
r : ℝ
j : ℤ
h : r > 0
h_1 : HSub.hSub (α := ℝ) (↑⌈HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌉ : ℝ) 1 * r < (↑j : ℝ)
⊢ (↑(⌈HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌉ - 1) : ℝ) < (↑j : ℝ) / r ∧
    HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r ≤ HAdd.hAdd (α := ℝ) (↑(⌈HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌉ - 1) : ℝ) 1
have inl : HSub.hSub (α := ℝ) (↑⌈HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌉ : ℝ) 1 * r < (↑j : ℝ) ∧
  HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r ≤ (↑⌈HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌉ : ℝ)
Tactic: rw [Int.cast_sub, Int.cast_one, lt_div_iff₀ h, sub_add_cancel]
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (goal)
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
have inr : beattySeq r (⌈HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌉ - 1) = j
Tactic: refine Or.inl ⟨⌈(j + 1) / r⌉ - 1, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (goal)
Goal:
r : ℝ
j : ℤ
h : r > 0
h_1 : (↑j : ℝ) ≤ HSub.hSub (α := ℝ) (↑⌈HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌉ : ℝ) 1 * r
⊢ beattySeq r (⌈HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌉ - 1) = j
have inr : (↑j : ℝ) ≤ HSub.hSub (α := ℝ) (↑⌈HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌉ : ℝ) 1 * r ∧
  (↑⌈HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌉ : ℝ) < HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r + 1
Tactic: rw [beattySeq, Int.floor_eq_iff, Int.cast_sub, Int.cast_one, ← lt_div_iff₀ h, sub_lt_iff_lt_add]
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (goal)
Goal:
r : ℝ
j : ℤ
h : r > 0
⊢ Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq' r k = x} j ∨
    ∃ (k : ℤ), (↑k : ℝ) ≤ (↑j : ℝ) / r ∧ HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r < HAdd.hAdd (α := ℝ) (↑k : ℝ) 1
have 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
Tactic: cases le_or_gt (⌊(j + 1) / r⌋ * r) j
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (goal)
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
⊢ Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq' r k = x} j ∨
    ∃ (k : ℤ), (↑k : ℝ) ≤ (↑j : ℝ) / r ∧ HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r < HAdd.hAdd (α := ℝ) (↑k : ℝ) 1
have 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
Tactic: cases le_or_gt (⌊(j + 1) / r⌋ * r) j
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (goal)
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
have inr : beattySeq' r ⌊HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌋ = j
Tactic: refine Or.inl ⟨⌊(j + 1) / r⌋, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (goal)
Goal:
r : ℝ
j : ℤ
h : r > 0
h_1 : (↑j : ℝ) < (↑⌊HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌋ : ℝ) * r
⊢ beattySeq' r ⌊HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌋ = j
have inr : HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 - 1 < (↑⌊HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌋ : ℝ) * r ∧
  (↑⌊HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌋ : ℝ) * r ≤ HAdd.hAdd (α := ℝ) (↑j : ℝ) 1
Tactic: rw [beattySeq', sub_eq_iff_eq_add, Int.ceil_eq_iff, Int.cast_add, Int.cast_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (goal)
Goal:
r : ℝ
j : ℤ
h : r > 0
h_1 : (↑j : ℝ) < (↑⌊HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌋ : ℝ) * r
⊢ HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 - 1 < (↑⌊HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌋ : ℝ) * r ∧
    (↑⌊HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌋ : ℝ) * r ≤ HAdd.hAdd (α := ℝ) (↑j : ℝ) 1
have inr : HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 - 1 < (↑⌊HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌋ : ℝ) * r
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (goal)
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 - 1 < (↑⌊HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌋ : ℝ) * r ∧
    (↑⌊HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌋ : ℝ) * r ≤ HAdd.hAdd (α := ℝ) (↑j : ℝ) 1
have inr₁ : (↑⌊HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r⌋ : ℝ) * r ≤ HAdd.hAdd (α := ℝ) (↑j : ℝ) 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (goal)
Goal:
r s : ℝ
hrs : r.HolderConjugate s
⊢ Eq (α := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq r k = x}ᶜ {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x}
have h : ∀ (j : ℤ),
  Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq r k = x}ᶜ j ↔
    Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x} j
Tactic: ext j
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (goal)
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
⊢ Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq r k = x}ᶜ j ↔
    Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x} j
have 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
Tactic: by_cases h₁ : j ∈ {beattySeq r k | k}
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (goal)
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
⊢ Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq r k = x}ᶜ j ↔
    Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x} j
have 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
Tactic: by_cases h₁ : j ∈ {beattySeq r k | k}
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (goal)
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
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
have 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
Tactic: by_cases h₂ : j ∈ {beattySeq' s k | k}
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (goal)
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
⊢ Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq r k = x}ᶜ j ↔
    Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x} j
have 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
Tactic: by_cases h₂ : j ∈ {beattySeq' s k | k}
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (goal)
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
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
have 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
Tactic: by_cases h₂ : j ∈ {beattySeq' s k | k}
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (goal)
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
⊢ Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq r k = x}ᶜ j ↔
    Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x} j
have 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
Tactic: by_cases h₂ : j ∈ {beattySeq' s k | k}
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (goal)
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
h₁ : j ∉ {x : ℤ | ∃ (k : ℤ), beattySeq r k = x}
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
have 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
Tactic: have ⟨k, h₁₁, h₁₂⟩ := (Beatty.hit_or_miss hrs.pos).resolve_left h₁
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (goal)
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
⊢ Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq r k = x}ᶜ j ↔
    Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x} j
have 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
Tactic: have ⟨m, h₂₁, h₂₂⟩ := (Beatty.hit_or_miss' hrs.symm.pos).resolve_left h₂
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (goal)
Goal:
r s : ℝ
hrs : r.HolderConjugate s
⊢ Eq (α := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq' r k = x}ᶜ {x : ℤ | ∃ (k : ℤ), beattySeq s k = x}
have rw : Eq (α := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq s k = x}ᶜᶜ {x : ℤ | ∃ (k : ℤ), beattySeq s k = x}
Tactic: rw [← compl_beattySeq hrs.symm, compl_compl]
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (goal)
Goal:
r s : ℝ
hrs : r.HolderConjugate s
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}
have rw₁ : Eq (α := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq s k = x} {x : ℤ | ∃ (k : ℤ), beattySeq s k = x}
Tactic: rw [← compl_beattySeq hrs.symm, compl_compl]
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (goal)
Goal:
r s : ℝ
hrs : r.HolderConjugate s
⊢ Eq (α := Set ℤ) ({x : ℤ | ∃ k > 0, beattySeq r k = x} ∆ {x : ℤ | ∃ k > 0, beattySeq' s k = x}) {n : ℤ | 0 < n}
have a : Subset (α := 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
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (goal)
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}
⊢ Eq (α := Set ℤ) ({x : ℤ | ∃ k > 0, beattySeq r k = x} ∆ {x : ℤ | ∃ k > 0, beattySeq' s k = x}) {n : ℤ | 0 < n}
have a₁ : Subset (α := Set ℤ) {n : ℤ | 0 < n} ({x : ℤ | ∃ k > 0, beattySeq r k = x} ∆ {x : ℤ | ∃ k > 0, beattySeq' s k = x})
Tactic: apply Set.eq_of_subset_of_subset
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (goal)
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
hk : k > 0
hjk : beattySeq r k = j
⊢ Membership.mem (γ := Set ℤ) {n : ℤ | 0 < n} j
have a : 1 ≤ (↑k : ℝ) * r
Tactic: rw [Set.mem_setOf_eq, ← hjk, beattySeq, Int.floor_pos]
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (goal)
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
hk : k > 0
hjk : beattySeq r k = j
⊢ LE.le (α := ℝ) 1 (↑k : ℝ)
have norm_cast : 1 ≤ k
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (goal)
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
hk : k > 0
hjk : beattySeq' s k = j
⊢ Membership.mem (γ := Set ℤ) {n : ℤ | 0 < n} j
have a : 1 < (↑k : ℝ) * s
Tactic: rw [Set.mem_setOf_eq, ← hjk, beattySeq', sub_pos, Int.lt_ceil, Int.cast_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (goal)
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
hk : k > 0
hjk : beattySeq' s k = j
⊢ LE.le (α := ℝ) 1 (↑k : ℝ)
have norm_cast : 1 ≤ k
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (goal)
Goal:
r s : ℝ
hrs : r.HolderConjugate s
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
have a : ∀ (hj : 0 < j),
  Membership.mem (γ := Set ℤ) ({x : ℤ | ∃ k > 0, beattySeq r k = x} ∆ {x : ℤ | ∃ k > 0, beattySeq' s k = x}) j
Tactic: (hj : 0 < j)
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (goal)
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
have refine : Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq s_1 k = x} j → ∀ (k : ℤ) (hk : beattySeq s_1 k = j), k > 0
Tactic: refine ⟨fun ⟨k, _, hk⟩ ↦ ⟨k, hk⟩, fun ⟨k, hk⟩ ↦ ⟨k, ?_, hk⟩⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (hypothesis)
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
⊢ k > 0
have hj₁ : 1 ≤ (↑k : ℝ) * s_1
Tactic: rw [← hk, beattySeq, Int.floor_pos] at hj
Cleared hypotheses: hj, hk
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (hypothesis)
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
hj : 0 < j
⊢ Membership.mem (γ := Set ℤ) ({x : ℤ | ∃ k > 0, beattySeq r k = x} ∆ {x : ℤ | ∃ k > 0, beattySeq' s k = x}) j
have hb₁ : ∀ 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
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (goal)
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
have refine : Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq' s_1 k = x} j → ∀ (k : ℤ) (hk : beattySeq' s_1 k = j), k > 0
Tactic: refine ⟨fun ⟨k, _, hk⟩ ↦ ⟨k, hk⟩, fun ⟨k, hk⟩ ↦ ⟨k, ?_, hk⟩⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (hypothesis)
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
⊢ k > 0
have hj₁ : 1 < (↑k : ℝ) * s_1
Tactic: rw [← hk, beattySeq', sub_pos, Int.lt_ceil, Int.cast_one] at hj
Cleared hypotheses: hj, hk
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (hypothesis)
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
⊢ Membership.mem (γ := Set ℤ) ({x : ℤ | ∃ k > 0, beattySeq r k = x} ∆ {x : ℤ | ∃ k > 0, beattySeq' s k = x}) j
have hb₂ : ∀ 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
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (goal)
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 > 0, beattySeq r k = x} ∆ {x : ℤ | ∃ k > 0, beattySeq' s k = x}) j
have a : Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq r k = x} j ∨ j ∉ {x : ℤ | ∃ (k : ℤ), beattySeq r k = x}
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]
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (goal)
Goal:
r s : ℝ
hrs : r.HolderConjugate s
⊢ Eq (α := Set ℤ) ({x : ℤ | ∃ k > 0, beattySeq' r k = x} ∆ {x : ℤ | ∃ k > 0, beattySeq s k = x}) {n : ℤ | 0 < n}
have rw : Eq (α := Set ℤ) ({x : ℤ | ∃ k > 0, beattySeq s k = x} ∆ {x : ℤ | ∃ k > 0, beattySeq' r k = x}) {n : ℤ | 0 < n}
Tactic: rw [symmDiff_comm, beattySeq_symmDiff_beattySeq'_pos hrs.symm]
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (goal)
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}
⊢ Eq (α := Set ℤ) ({x : ℤ | ∃ k > 0, beattySeq' r k = x} ∆ {x : ℤ | ∃ k > 0, beattySeq s k = x}) {n : ℤ | 0 < n}
have rw₁ : Eq (α := Set ℤ) {n : ℤ | 0 < n} {n : ℤ | 0 < n}
Tactic: rw [symmDiff_comm, beattySeq_symmDiff_beattySeq'_pos hrs.symm]
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (goal)
Goal:
r : ℝ
hr : Irrational r
⊢ Eq (α := Set ℤ) {x : ℤ | ∃ k > 0, ⌈(↑k : ℝ) * r⌉ - 1 = x} {x : ℤ | ∃ k > 0, ⌊(↑k : ℝ) * r⌋ = x}
have h : ∀ (x x_1 : ℤ), x_1 > 0 ∧ ⌈(↑x_1 : ℝ) * r⌉ - 1 = x ↔ x_1 > 0 ∧ ⌊(↑x_1 : ℝ) * r⌋ = x
Tactic: congr! 4