-- Mathlib/NumberTheory/Rayleigh.lean
theorem no_collision (hrs : r.IsConjExponent s) :
    Disjoint {beattySeq r k | k} {beattySeq' s k | k}

Proof state:
r s : ℝ
hrs : r.IsConjExponent s
j k : ℤ
h₁ : ↑j / r ≤ ↑k ∧ ↑k < (↑j + 1) / r
m : ℤ
h₂ : ↑j / s < ↑m ∧ ↑m ≤ (↑j + 1) / s
⊢ False

Tactic:
have h₃ := add_lt_add_of_le_of_lt h₁.1 h₂.1

Result:
r s : ℝ
hrs : r.IsConjExponent s
j k : ℤ
h₁ : ↑j / r ≤ ↑k ∧ ↑k < (↑j + 1) / r
m : ℤ
h₂ : ↑j / s < ↑m ∧ ↑m ≤ (↑j + 1) / s
h₃ : ↑j / r + ↑j / s < ↑k + ↑m
⊢ False

Proof state:
r s : ℝ
hrs : r.IsConjExponent s
j k : ℤ
h₁ : ↑j / r ≤ ↑k ∧ ↑k < (↑j + 1) / r
m : ℤ
h₂ : ↑j / s < ↑m ∧ ↑m ≤ (↑j + 1) / s
h₃ : ↑j / r + ↑j / s < ↑k + ↑m
h₄ : ↑k + ↑m < (↑j + 1) / r + (↑j + 1) / s
⊢ False

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

Result:
r s : ℝ
hrs : r.IsConjExponent s
j k : ℤ
h₁ : ↑j / r ≤ ↑k ∧ ↑k < (↑j + 1) / r
m : ℤ
h₂ : ↑j / s < ↑m ∧ ↑m ≤ (↑j + 1) / s
h₃ : ↑j < ↑k + ↑m
h₄ : ↑k + ↑m < ↑j + 1
⊢ False

Proof state:
r s : ℝ
hrs : r.IsConjExponent s
j k : ℤ
h₁ : ↑j / r ≤ ↑k ∧ ↑k < (↑j + 1) / r
m : ℤ
h₂ : beattySeq' s m = j
⊢ False

Tactic:
rw [beattySeq', sub_eq_iff_eq_add, Int.ceil_eq_iff, Int.cast_add, Int.cast_one,
  add_sub_cancel_right, ← div_lt_iff₀ hrs.symm.pos, ← le_div_iff₀ hrs.symm.pos] at h₂

Result:
r s : ℝ
hrs : r.IsConjExponent s
j k : ℤ
h₁ : ↑j / r ≤ ↑k ∧ ↑k < (↑j + 1) / r
m : ℤ
h₂ : ↑j / s < ↑m ∧ ↑m ≤ (↑j + 1) / s
⊢ False

Proof state:
r s : ℝ
hrs : r.IsConjExponent s
j k : ℤ
h₁ : ↑j / r ≤ ↑k ∧ ↑k < (↑j + 1) / r
m : ℤ
h₂ : ↑j / s < ↑m ∧ ↑m ≤ (↑j + 1) / s
h₃ : ↑j < ↑k + ↑m
h₄ : ↑k + ↑m < ↑j + ↑1
⊢ False

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

Result:
r s : ℝ
hrs : r.IsConjExponent s
j k : ℤ
h₁ : ↑j / r ≤ ↑k ∧ ↑k < (↑j + 1) / r
m : ℤ
h₂ : ↑j / s < ↑m ∧ ↑m ≤ (↑j + 1) / s
h₃ : j < k + m
h₄ : k + m ≤ j
⊢ False

Proof state:
r s : ℝ
hrs : r.IsConjExponent s
⊢ ∀ ⦃a : ℤ⦄, a ∈ {x | ∃ k, beattySeq r k = x} → a ∉ {x | ∃ k, beattySeq' s k = x}

Tactic:
intro j ⟨k, h₁⟩ ⟨m, h₂⟩

Result:
r s : ℝ
hrs : r.IsConjExponent s
j k : ℤ
h₁ : beattySeq r k = j
m : ℤ
h₂ : beattySeq' s m = j
⊢ False

Proof state:
r s : ℝ
hrs : r.IsConjExponent s
j k : ℤ
h₁ : ↑j / r ≤ ↑k ∧ ↑k < (↑j + 1) / r
m : ℤ
h₂ : ↑j / s < ↑m ∧ ↑m ≤ (↑j + 1) / s
h₃ : ↑j < ↑k + ↑m
h₄ : ↑k + ↑m < ↑j + 1
⊢ False

Tactic:
rw [← Int.cast_one] at h₄

Result:
r s : ℝ
hrs : r.IsConjExponent s
j k : ℤ
h₁ : ↑j / r ≤ ↑k ∧ ↑k < (↑j + 1) / r
m : ℤ
h₂ : ↑j / s < ↑m ∧ ↑m ≤ (↑j + 1) / s
h₃ : ↑j < ↑k + ↑m
h₄ : ↑k + ↑m < ↑j + ↑1
⊢ False

Proof state:
r s : ℝ
hrs : r.IsConjExponent s
j k : ℤ
h₁ : ↑j / r ≤ ↑k ∧ ↑k < (↑j + 1) / r
m : ℤ
h₂ : ↑j / s < ↑m ∧ ↑m ≤ (↑j + 1) / s
h₃ : j < k + m
h₄ : k + m ≤ j
⊢ False

Tactic:
exact h₄.not_lt h₃

Result:
no goals

Proof state:
r s : ℝ
hrs : r.IsConjExponent s
j k : ℤ
h₁ : beattySeq r k = j
m : ℤ
h₂ : beattySeq' s m = j
⊢ False

Tactic:
rw [beattySeq, Int.floor_eq_iff, ← div_le_iff₀ hrs.pos, ← lt_div_iff₀ hrs.pos] at h₁

Result:
r s : ℝ
hrs : r.IsConjExponent s
j k : ℤ
h₁ : ↑j / r ≤ ↑k ∧ ↑k < (↑j + 1) / r
m : ℤ
h₂ : beattySeq' s m = j
⊢ False

Proof state:
r s : ℝ
hrs : r.IsConjExponent s
⊢ Disjoint {x | ∃ k, beattySeq r k = x} {x | ∃ k, beattySeq' s k = x}

Tactic:
rw [Set.disjoint_left]

Result:
r s : ℝ
hrs : r.IsConjExponent s
⊢ ∀ ⦃a : ℤ⦄, a ∈ {x | ∃ k, beattySeq r k = x} → a ∉ {x | ∃ k, beattySeq' s k = x}

Proof state:
r s : ℝ
hrs : r.IsConjExponent s
j k : ℤ
h₁ : ↑j / r ≤ ↑k ∧ ↑k < (↑j + 1) / r
m : ℤ
h₂ : ↑j / s < ↑m ∧ ↑m ≤ (↑j + 1) / s
h₃ : ↑j / r + ↑j / s < ↑k + ↑m
⊢ False

Tactic:
have h₄ := add_lt_add_of_lt_of_le h₁.2 h₂.2

Result:
r s : ℝ
hrs : r.IsConjExponent s
j k : ℤ
h₁ : ↑j / r ≤ ↑k ∧ ↑k < (↑j + 1) / r
m : ℤ
h₂ : ↑j / s < ↑m ∧ ↑m ≤ (↑j + 1) / s
h₃ : ↑j / r + ↑j / s < ↑k + ↑m
h₄ : ↑k + ↑m < (↑j + 1) / r + (↑j + 1) / s
⊢ False