IMO 2024 P1

Determine all real numbers \alpha such that, for every positive integer n, the integer \lfloor \alpha\rfloor + \lfloor2\alpha\rfloor + \cdots + \lfloor n\alpha\rfloor is a multiple of n. (Note that \lfloor z\rfloor denotes the greatest integer less than or equal to z. For example, \lfloor-\pi\rfloor = -4 and \lfloor2\rfloor = \lfloor2.9\rfloor = 2.)

Solution: \alpha is an even integer.

open scoped BigOperators

theorem imo_2024_p1 :
    {(α : ℝ) | ∀ (n : ℕ), 0 < n → (n : ℤ) ∣ (∑ i in Finset.Icc 1 n, ⌊i * α⌋)}
    = {α : ℝ | ∃ k : ℤ, Even k ∧ α = k} := by⊢ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋} = {α | ∃ k, Even k ∧ α = ↑k}
  rw [(Set.Subset.antisymm_iff ), (Set.subset_def), ]⊢ (∀ x ∈ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋}, x ∈ {α | ∃ k, Even k ∧ α = ↑k}) ∧
  {α | ∃ k, Even k ∧ α = ↑k} ⊆ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋}
  /- We introduce a variable that will be used
     in the second part of the proof (the hard direction),
     namely the integer `l` such that `2l = ⌊α⌋ + ⌊2α⌋`
     (this comes from the given divisibility condition with `n = 2`). -/
  existsλx L=>(L 2 two_pos).rec λl Y=>?_refine_1
⊢ {α | ∃ k, Even k ∧ α = ↑k} ⊆ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋}
refine_2
x : ℝ
L : x ∈ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋}
l : ℤ
Y : ∑ i ∈ Finset.Icc 1 2, ⌊↑i * x⌋ = ↑2 * l
⊢ x ∈ {α | ∃ k, Even k ∧ α = ↑k}
  useλy . x=>y.rec λS p=>?_refine_1
x✝¹ : ℝ
y : x✝¹ ∈ {α | ∃ k, Even k ∧ α = ↑k}
x✝ : ℕ
x : 0 < x✝
S : ℤ
p : Even S ∧ x✝¹ = ↑S
⊢ ↑x✝ ∣ ∑ i ∈ Finset.Icc 1 x✝, ⌊↑i * x✝¹⌋
refine_2
x : ℝ
L : x ∈ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋}
l : ℤ
Y : ∑ i ∈ Finset.Icc 1 2, ⌊↑i * x⌋ = ↑2 * l
⊢ x ∈ {α | ∃ k, Even k ∧ α = ↑k}
  ·refine_1
x✝¹ : ℝ
y : x✝¹ ∈ {α | ∃ k, Even k ∧ α = ↑k}
x✝ : ℕ
x : 0 < x✝
S : ℤ
p : Even S ∧ x✝¹ = ↑S
⊢ ↑x✝ ∣ ∑ i ∈ Finset.Icc 1 x✝, ⌊↑i * x✝¹⌋ /- We start by showing that every `α` of the form `2k` works.
       In this case, the sum simplifies to `kn(n+1)`),
       which is clearly divisible by `n`. -/
    simp_all[λL:ℕ=>(byx✝¹ : ℝ
y : x✝¹ ∈ {α | ∃ k, Even k ∧ α = ↑k}
x✝ : ℕ
x : 0 < x✝
S : ℤ
p : Even S ∧ x✝¹ = ↑S
L : ℕ
⊢ ⌊↑L * ↑S⌋ = ↑L * S norm_num[Int.floor_eq_iff]All goals completed! 🐙 :⌊(L:ℝ)*S⌋=L* S )]
    rw[p.2,Int.dvd_iff_emod_eq_zero,Nat.lt_iff_add_one_le,<-Finset.sum_mul,←Nat.cast_sum, S.even_iff, ←Nat.Ico_succ_right,@ .((( Finset.sum_Ico_eq_sum_range))),Finset.sum_add_distrib ]at*refine_1
x✝¹ : ℝ
x✝ : ℕ
x : 0 + 1 ≤ x✝
S : ℤ
p : S % 2 = 0 ∧ ↑S = ↑S
⊢ ↑(∑ x ∈ Finset.range (x✝.succ - 1), 1 + ∑ x ∈ Finset.range (x✝.succ - 1), x) * S % ↑x✝ = 0
    simp_all[Finset.sum_range_id]refine_1
x✝¹ : ℝ
x✝ : ℕ
S : ℤ
x : 1 ≤ x✝
p : 2 ∣ S
⊢ ↑x✝ ∣ (↑x✝ + ↑x✝ * (↑x✝ - 1) / 2) * S
    exact dvd_trans ⟨2+((_:ℕ)-1),byx✝¹ : ℝ
x✝ : ℕ
S : ℤ
x : 1 ≤ x✝
p : 2 ∣ S
⊢ (↑x✝ + ↑x✝ * (↑x✝ - 1) / 2) * 2 = ↑x✝ * (2 + (↑x✝ - 1)) linarith[((‹ℕ›:Int)*(‹Nat›-1)).ediv_mul_cancel$ Int.prime_two.dvd_mul.2<|byx✝¹ : ℝ
x✝ : ℕ
S : ℤ
x : 1 ≤ x✝
p : 2 ∣ S
⊢ 2 ∣ ↑x✝ ∨ 2 ∣ ↑x✝ - 1 ·x✝¹ : ℝ
x✝ : ℕ
S : ℤ
x : 1 ≤ x✝
p : 2 ∣ S
⊢ 2 ∣ ↑x✝ ∨ 2 ∣ ↑x✝ - 1omegaAll goals completed! 🐙]⟩ ↑↑(mul_dvd_mul_left @_ (p))
  /- Now let's prove the converse, i.e. that every `α` in the LHS
     is an even integer. We claim for all such `α` and `n ∈ ℕ`, we have
     `⌊(n+1)*α⌋ = ⌊α⌋+2n(l-⌊α⌋)`. -/
  suffices: ∀ (n : ℕ),⌊(n+1)*x⌋ =⌊ x⌋+2 * ↑ (n : ℕ) * (l-(⌊(x)⌋))refine_2
x : ℝ
L : x ∈ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋}
l : ℤ
Y : ∑ i ∈ Finset.Icc 1 2, ⌊↑i * x⌋ = ↑2 * l
this : ∀ (n : ℕ), ⌊(↑n + 1) * x⌋ = ⌊x⌋ + 2 * ↑n * (l - ⌊x⌋)
⊢ x ∈ {α | ∃ k, Even k ∧ α = ↑k}
this
x : ℝ
L : x ∈ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋}
l : ℤ
Y : ∑ i ∈ Finset.Icc 1 2, ⌊↑i * x⌋ = ↑2 * l
⊢ ∀ (n : ℕ), ⌊(↑n + 1) * x⌋ = ⌊x⌋ + 2 * ↑n * (l - ⌊x⌋)
  ·refine_2
x : ℝ
L : x ∈ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋}
l : ℤ
Y : ∑ i ∈ Finset.Icc 1 2, ⌊↑i * x⌋ = ↑2 * l
this : ∀ (n : ℕ), ⌊(↑n + 1) * x⌋ = ⌊x⌋ + 2 * ↑n * (l - ⌊x⌋)
⊢ x ∈ {α | ∃ k, Even k ∧ α = ↑k} /- Let's assume for now that the claim is true,
       and see how this is enough to finish our proof. -/
    zify[mul_comm,Int.floor_eq_iff] at thisrefine_2
x : ℝ
L : x ∈ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋}
l : ℤ
Y : ∑ i ∈ Finset.Icc 1 2, ⌊↑i * x⌋ = ↑2 * l
this : ∀ (n : ℕ), ↑⌊x⌋ + (↑l - ↑⌊x⌋) * (↑n * 2) ≤ x * (↑n + 1) ∧ x * (↑n + 1) < ↑⌊x⌋ + (↑l - ↑⌊x⌋) * (↑n * 2) + 1
⊢ x ∈ {α | ∃ k, Even k ∧ α = ↑k}
    -- We'll show that `α = 2(l-⌊α⌋)`, which is obviously even.
    use(l-⌊x⌋)*2h
x : ℝ
L : x ∈ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋}
l : ℤ
Y : ∑ i ∈ Finset.Icc 1 2, ⌊↑i * x⌋ = ↑2 * l
this : ∀ (n : ℕ), ↑⌊x⌋ + (↑l - ↑⌊x⌋) * (↑n * 2) ≤ x * (↑n + 1) ∧ x * (↑n + 1) < ↑⌊x⌋ + (↑l - ↑⌊x⌋) * (↑n * 2) + 1
⊢ Even ((l - ⌊x⌋) * 2) ∧ x = ↑((l - ⌊x⌋) * 2)
    norm_numh
x : ℝ
L : x ∈ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋}
l : ℤ
Y : ∑ i ∈ Finset.Icc 1 2, ⌊↑i * x⌋ = ↑2 * l
this : ∀ (n : ℕ), ↑⌊x⌋ + (↑l - ↑⌊x⌋) * (↑n * 2) ≤ x * (↑n + 1) ∧ x * (↑n + 1) < ↑⌊x⌋ + (↑l - ↑⌊x⌋) * (↑n * 2) + 1
⊢ x = (↑l - ↑⌊x⌋) * 2
    -- To do so, it suffices to show `α ≤ 2(l-⌊α⌋)` and `α ≥ 2(l-⌊α⌋)`.
    apply@le_antisymmh.a
x : ℝ
L : x ∈ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋}
l : ℤ
Y : ∑ i ∈ Finset.Icc 1 2, ⌊↑i * x⌋ = ↑2 * l
this : ∀ (n : ℕ), ↑⌊x⌋ + (↑l - ↑⌊x⌋) * (↑n * 2) ≤ x * (↑n + 1) ∧ x * (↑n + 1) < ↑⌊x⌋ + (↑l - ↑⌊x⌋) * (↑n * 2) + 1
⊢ x ≤ (↑l - ↑⌊x⌋) * 2
h.a
x : ℝ
L : x ∈ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋}
l : ℤ
Y : ∑ i ∈ Finset.Icc 1 2, ⌊↑i * x⌋ = ↑2 * l
this : ∀ (n : ℕ), ↑⌊x⌋ + (↑l - ↑⌊x⌋) * (↑n * 2) ≤ x * (↑n + 1) ∧ x * (↑n + 1) < ↑⌊x⌋ + (↑l - ↑⌊x⌋) * (↑n * 2) + 1
⊢ (↑l - ↑⌊x⌋) * 2 ≤ x
    /- To prove the first inequality, notice that if `α > 2(l-⌊α⌋)` then
       there exists an integer `N > 0` such that `N ≥ 1/(α - 2(l -⌊α⌋))`.
       By our assumed claim (with `n = N`), we have
       `⌊α⌋ + 2(l-⌊α⌋)N + 1 > (N+1)α`, i.e.
       `⌊α⌋ + (2(l-⌊α⌋) - α)N + 1 > α`,
       and this implies `⌊α⌋ > α`; contradiction. -/
    use not_lt.1 (by⊢ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋} = {α | ∃ k, Even k ∧ α = ↑k} cases exists_nat_ge (1/(x-_)) with|_ N =>nlinarith[ one_div_mul_cancel $ sub_ne_zero.2 ·.ne',9,Int.floor_le x, this N])
    /- Similarly, if `α < 2(l-⌊α⌋)` then we can find a positive natural `N`
       such that `N ≥ 1/(2(l-⌊α⌋) - α)`.
       By our claim (with `n = N`), we have
       `(N+1)α ≥ ⌊α⌋ + 2(l-⌊α⌋)N`, i.e.
       `α ≥ ⌊α⌋ + (2(l-⌊α⌋) - α)N`,
       and this implies `a ≥ ⌊α⌋ + 1`; contradiction. -/
    use not_lt.1 (by⊢ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋} = {α | ∃ k, Even k ∧ α = ↑k} cases exists_nat_ge (1/_:ℝ)with|_ A=>nlinarith[Int.lt_floor_add_one x,one_div_mul_cancel$ sub_ne_zero.2 ·.ne',this A])
  /- Now all that's left to do is to prove our claim
     `⌊(n + 1)α⌋ = ⌊α⌋ + 2n(l - ⌊α⌋)`. -/
  introthis
x : ℝ
L : x ∈ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋}
l : ℤ
Y : ∑ i ∈ Finset.Icc 1 2, ⌊↑i * x⌋ = ↑2 * l
n✝ : ℕ
⊢ ⌊(↑n✝ + 1) * x⌋ = ⌊x⌋ + 2 * ↑n✝ * (l - ⌊x⌋)
  -- We argue by strong induction on `n`.
  induction‹_› using@Nat.strongInductionOnthis.ind
x : ℝ
L : x ∈ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋}
l : ℤ
Y : ∑ i ∈ Finset.Icc 1 2, ⌊↑i * x⌋ = ↑2 * l
n✝ : ℕ
a✝ : ∀ m < n✝, ⌊(↑m + 1) * x⌋ = ⌊x⌋ + 2 * ↑m * (l - ⌊x⌋)
⊢ ⌊(↑n✝ + 1) * x⌋ = ⌊x⌋ + 2 * ↑n✝ * (l - ⌊x⌋)
  -- By our hypothesis on `α`, we know that `(n+1) | ∑_{i=1}^(n+1) ⌊iα⌋`
  specialize L$ ‹_›+1this.ind
x : ℝ
l : ℤ
Y : ∑ i ∈ Finset.Icc 1 2, ⌊↑i * x⌋ = ↑2 * l
n✝ : ℕ
a✝ : ∀ m < n✝, ⌊(↑m + 1) * x⌋ = ⌊x⌋ + 2 * ↑m * (l - ⌊x⌋)
L : 0 < n✝ + 1 → ↑(n✝ + 1) ∣ ∑ i ∈ Finset.Icc 1 (n✝ + 1), ⌊↑i * x⌋
⊢ ⌊(↑n✝ + 1) * x⌋ = ⌊x⌋ + 2 * ↑n✝ * (l - ⌊x⌋)
  simp_all[add_comm,mul_assoc,Int.floor_eq_iff,<-Nat.Ico_succ_right, add_mul,(Finset.range_succ), Finset.sum_Ico_eq_sum_range]this.ind
x : ℝ
l : ℤ
n✝ : ℕ
Y : ⌊x⌋ + ⌊x + x⌋ = 2 * l
a✝ : ∀ m < n✝, ↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)))
L : ↑n✝ + 1 ∣ ⌊x + ↑n✝ * x⌋ + ∑ x_1 ∈ Finset.range n✝, ⌊x + ↑x_1 * x⌋
⊢ ↑⌊x⌋ + 2 * (↑n✝ * (↑l - ↑⌊x⌋)) ≤ x + ↑n✝ * x ∧ x + ↑n✝ * x < 1 + (↑⌊x⌋ + 2 * (↑n✝ * (↑l - ↑⌊x⌋)))
  revert‹ℕ›this.ind
x : ℝ
l : ℤ
Y : ⌊x⌋ + ⌊x + x⌋ = 2 * l
⊢ ∀ (n : ℕ),
  (∀ m < n, ↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)))) →
    ↑n + 1 ∣ ⌊x + ↑n * x⌋ + ∑ x_1 ∈ Finset.range n, ⌊x + ↑x_1 * x⌋ →
      ↑⌊x⌋ + 2 * (↑n * (↑l - ↑⌊x⌋)) ≤ x + ↑n * x ∧ x + ↑n * x < 1 + (↑⌊x⌋ + 2 * (↑n * (↑l - ↑⌊x⌋)))
  /- Thus, there exists `c` such that
     `(n+1)*c = ∑_{i=1}^{n+1} ⌊iα⌋ = ⌊nα+α⌋ + ∑_{i=1}^n ⌊iα⌋`. -/
  rintro A B@cthis.ind.intro
x : ℝ
l : ℤ
Y : ⌊x⌋ + ⌊x + x⌋ = 2 * l
A : ℕ
B : ∀ m < A, ↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)))
c : ℤ
h✝ : ⌊x + ↑A * x⌋ + ∑ x_1 ∈ Finset.range A, ⌊x + ↑x_1 * x⌋ = (↑A + 1) * c
⊢ ↑⌊x⌋ + 2 * (↑A * (↑l - ↑⌊x⌋)) ≤ x + ↑A * x ∧ x + ↑A * x < 1 + (↑⌊x⌋ + 2 * (↑A * (↑l - ↑⌊x⌋)))
  simp_all[ Finset.mem_range.mp _,←eq_sub_iff_add_eq',Int.floor_eq_iff]this.ind.intro
x : ℝ
l : ℤ
A : ℕ
c : ℤ
Y : 2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1
B : ∀ m < A, ↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)))
h✝ : ∑ x_1 ∈ Finset.range A, ⌊x + ↑x_1 * x⌋ = (↑A + 1) * c - ⌊x + ↑A * x⌋
⊢ ↑⌊x⌋ + 2 * (↑A * (↑l - ↑⌊x⌋)) ≤ x + ↑A * x ∧ x + ↑A * x < 1 + (↑⌊x⌋ + 2 * (↑A * (↑l - ↑⌊x⌋)))
  /- By the inductive hypothesis,
     `∑_{i=0}^{n-1}, ⌊α+iα⌋ = ∑_{i=0}^{n-1}, ⌊α⌋+2*i*(l-⌊α⌋)`. -/
  suffices:∑d in .range A,⌊x+d*x⌋=∑Q in .range A,(⌊x⌋+2*(Q * (l-.floor x)))this.ind.intro
x : ℝ
l : ℤ
A : ℕ
c : ℤ
Y : 2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1
B : ∀ m < A, ↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)))
h✝ : ∑ x_1 ∈ Finset.range A, ⌊x + ↑x_1 * x⌋ = (↑A + 1) * c - ⌊x + ↑A * x⌋
this : ∑ d ∈ Finset.range A, ⌊x + ↑d * x⌋ = ∑ Q ∈ Finset.range A, (⌊x⌋ + 2 * (↑Q * (l - ⌊x⌋)))
⊢ ↑⌊x⌋ + 2 * (↑A * (↑l - ↑⌊x⌋)) ≤ x + ↑A * x ∧ x + ↑A * x < 1 + (↑⌊x⌋ + 2 * (↑A * (↑l - ↑⌊x⌋)))
this
x : ℝ
l : ℤ
A : ℕ
c : ℤ
Y : 2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1
B : ∀ m < A, ↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)))
h✝ : ∑ x_1 ∈ Finset.range A, ⌊x + ↑x_1 * x⌋ = (↑A + 1) * c - ⌊x + ↑A * x⌋
⊢ ∑ d ∈ Finset.range A, ⌊x + ↑d * x⌋ = ∑ Q ∈ Finset.range A, (⌊x⌋ + 2 * (↑Q * (l - ⌊x⌋)))
  ·this.ind.intro
x : ℝ
l : ℤ
A : ℕ
c : ℤ
Y : 2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1
B : ∀ m < A, ↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)))
h✝ : ∑ x_1 ∈ Finset.range A, ⌊x + ↑x_1 * x⌋ = (↑A + 1) * c - ⌊x + ↑A * x⌋
this : ∑ d ∈ Finset.range A, ⌊x + ↑d * x⌋ = ∑ Q ∈ Finset.range A, (⌊x⌋ + 2 * (↑Q * (l - ⌊x⌋)))
⊢ ↑⌊x⌋ + 2 * (↑A * (↑l - ↑⌊x⌋)) ≤ x + ↑A * x ∧ x + ↑A * x < 1 + (↑⌊x⌋ + 2 * (↑A * (↑l - ↑⌊x⌋))) suffices:∑d in ( .range A),(((d)):ℤ) =A * ( A-1)/2this.ind.intro
x : ℝ
l : ℤ
A : ℕ
c : ℤ
Y : 2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1
B : ∀ m < A, ↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)))
h✝ : ∑ x_1 ∈ Finset.range A, ⌊x + ↑x_1 * x⌋ = (↑A + 1) * c - ⌊x + ↑A * x⌋
this✝ : ∑ d ∈ Finset.range A, ⌊x + ↑d * x⌋ = ∑ Q ∈ Finset.range A, (⌊x⌋ + 2 * (↑Q * (l - ⌊x⌋)))
this : ∑ d ∈ Finset.range A, ↑d = ↑A * (↑A - 1) / 2
⊢ ↑⌊x⌋ + 2 * (↑A * (↑l - ↑⌊x⌋)) ≤ x + ↑A * x ∧ x + ↑A * x < 1 + (↑⌊x⌋ + 2 * (↑A * (↑l - ↑⌊x⌋)))
this
x : ℝ
l : ℤ
A : ℕ
c : ℤ
Y : 2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1
B : ∀ m < A, ↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)))
h✝ : ∑ x_1 ∈ Finset.range A, ⌊x + ↑x_1 * x⌋ = (↑A + 1) * c - ⌊x + ↑A * x⌋
this : ∑ d ∈ Finset.range A, ⌊x + ↑d * x⌋ = ∑ Q ∈ Finset.range A, (⌊x⌋ + 2 * (↑Q * (l - ⌊x⌋)))
⊢ ∑ d ∈ Finset.range A, ↑d = ↑A * (↑A - 1) / 2
    ·this.ind.intro
x : ℝ
l : ℤ
A : ℕ
c : ℤ
Y : 2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1
B : ∀ m < A, ↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)))
h✝ : ∑ x_1 ∈ Finset.range A, ⌊x + ↑x_1 * x⌋ = (↑A + 1) * c - ⌊x + ↑A * x⌋
this✝ : ∑ d ∈ Finset.range A, ⌊x + ↑d * x⌋ = ∑ Q ∈ Finset.range A, (⌊x⌋ + 2 * (↑Q * (l - ⌊x⌋)))
this : ∑ d ∈ Finset.range A, ↑d = ↑A * (↑A - 1) / 2
⊢ ↑⌊x⌋ + 2 * (↑A * (↑l - ↑⌊x⌋)) ≤ x + ↑A * x ∧ x + ↑A * x < 1 + (↑⌊x⌋ + 2 * (↑A * (↑l - ↑⌊x⌋))) have:(A : ℤ) * (A-1)%2=0this
x : ℝ
l : ℤ
A : ℕ
c : ℤ
Y : 2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1
B : ∀ m < A, ↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)))
h✝ : ∑ x_1 ∈ Finset.range A, ⌊x + ↑x_1 * x⌋ = (↑A + 1) * c - ⌊x + ↑A * x⌋
this✝ : ∑ d ∈ Finset.range A, ⌊x + ↑d * x⌋ = ∑ Q ∈ Finset.range A, (⌊x⌋ + 2 * (↑Q * (l - ⌊x⌋)))
this : ∑ d ∈ Finset.range A, ↑d = ↑A * (↑A - 1) / 2
⊢ ↑A * (↑A - 1) % 2 = 0
this.ind.intro
x : ℝ
l : ℤ
A : ℕ
c : ℤ
Y : 2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1
B : ∀ m < A, ↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)))
h✝ : ∑ x_1 ∈ Finset.range A, ⌊x + ↑x_1 * x⌋ = (↑A + 1) * c - ⌊x + ↑A * x⌋
this✝¹ : ∑ d ∈ Finset.range A, ⌊x + ↑d * x⌋ = ∑ Q ∈ Finset.range A, (⌊x⌋ + 2 * (↑Q * (l - ⌊x⌋)))
this✝ : ∑ d ∈ Finset.range A, ↑d = ↑A * (↑A - 1) / 2
this : ↑A * (↑A - 1) % 2 = 0
⊢ ↑⌊x⌋ + 2 * (↑A * (↑l - ↑⌊x⌋)) ≤ x + ↑A * x ∧ x + ↑A * x < 1 + (↑⌊x⌋ + 2 * (↑A * (↑l - ↑⌊x⌋)))
      ·this
x : ℝ
l : ℤ
A : ℕ
c : ℤ
Y : 2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1
B : ∀ m < A, ↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)))
h✝ : ∑ x_1 ∈ Finset.range A, ⌊x + ↑x_1 * x⌋ = (↑A + 1) * c - ⌊x + ↑A * x⌋
this✝ : ∑ d ∈ Finset.range A, ⌊x + ↑d * x⌋ = ∑ Q ∈ Finset.range A, (⌊x⌋ + 2 * (↑Q * (l - ⌊x⌋)))
this : ∑ d ∈ Finset.range A, ↑d = ↑A * (↑A - 1) / 2
⊢ ↑A * (↑A - 1) % 2 = 0 cases@Int.emod_two_eq A with|_ B=>this.inr
x : ℝ
l : ℤ
A : ℕ
c : ℤ
Y : 2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1
B✝ : ∀ m < A, ↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)))
h✝ : ∑ x_1 ∈ Finset.range A, ⌊x + ↑x_1 * x⌋ = (↑A + 1) * c - ⌊x + ↑A * x⌋
this✝ : ∑ d ∈ Finset.range A, ⌊x + ↑d * x⌋ = ∑ Q ∈ Finset.range A, (⌊x⌋ + 2 * (↑Q * (l - ⌊x⌋)))
this : ∑ d ∈ Finset.range A, ↑d = ↑A * (↑A - 1) / 2
B : ↑A % 2 = 1
⊢ ↑A * (↑A - 1) % 2 = 0norm_num[B,Int.sub_emod,Int.mul_emod]All goals completed! 🐙
      norm_num at*this.ind.intro
x : ℝ
l : ℤ
A : ℕ
c : ℤ
Y : 2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1
B : ∀ m < A, ↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)))
h✝ : ∑ x_1 ∈ Finset.range A, ⌊x + ↑x_1 * x⌋ = (↑A + 1) * c - ⌊x + ↑A * x⌋
this✝¹ : ∑ d ∈ Finset.range A, ⌊x + ↑d * x⌋ = ∑ Q ∈ Finset.range A, (⌊x⌋ + 2 * (↑Q * (l - ⌊x⌋)))
this✝ : ∑ d ∈ Finset.range A, ↑d = ↑A * (↑A - 1) / 2
this : 2 ∣ ↑A * (↑A - 1)
⊢ ↑⌊x⌋ + 2 * (↑A * (↑l - ↑⌊x⌋)) ≤ x + ↑A * x ∧ x + ↑A * x < 1 + (↑⌊x⌋ + 2 * (↑A * (↑l - ↑⌊x⌋)))
      norm_num[ Finset.sum_add_distrib,<-Finset.sum_mul, ←Finset.mul_sum _ _] at*this.ind.intro
x : ℝ
l : ℤ
A : ℕ
c : ℤ
Y : 2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1
B : ∀ m < A, ↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)))
h✝ : ∑ x_1 ∈ Finset.range A, ⌊x + ↑x_1 * x⌋ = (↑A + 1) * c - ⌊x + ↑A * x⌋
this✝¹ : ∑ d ∈ Finset.range A, ↑d = ↑A * (↑A - 1) / 2
this✝ : 2 ∣ ↑A * (↑A - 1)
this : ∑ d ∈ Finset.range A, ⌊x + ↑d * x⌋ = ↑A * ⌊x⌋ + 2 * ((∑ i ∈ Finset.range A, ↑i) * (l - ⌊x⌋))
⊢ ↑⌊x⌋ + 2 * (↑A * (↑l - ↑⌊x⌋)) ≤ x + ↑A * x ∧ x + ↑A * x < 1 + (↑⌊x⌋ + 2 * (↑A * (↑l - ↑⌊x⌋)))
      rw[eq_sub_iff_add_eq]at*this.ind.intro
x : ℝ
l : ℤ
A : ℕ
c : ℤ
Y : 2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1
B : ∀ m < A, ↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)))
h✝ : ∑ x_1 ∈ Finset.range A, ⌊x + ↑x_1 * x⌋ + ⌊x + ↑A * x⌋ = (↑A + 1) * c
this✝¹ : ∑ d ∈ Finset.range A, ↑d = ↑A * (↑A - 1) / 2
this✝ : 2 ∣ ↑A * (↑A - 1)
this : ∑ d ∈ Finset.range A, ⌊x + ↑d * x⌋ = ↑A * ⌊x⌋ + 2 * ((∑ i ∈ Finset.range A, ↑i) * (l - ⌊x⌋))
⊢ ↑⌊x⌋ + 2 * (↑A * (↑l - ↑⌊x⌋)) ≤ x + ↑A * x ∧ x + ↑A * x < 1 + (↑⌊x⌋ + 2 * (↑A * (↑l - ↑⌊x⌋)))
      /- Combined with
         `∑_{i=0}^{n-1},⌊iα+α⌋ = (n+1)c - ⌊nα+α⌋`,
         we have `⌊nα+α⌋ = (n+1)c - n⌊α⌋ - n(n-1)(l-⌊α⌋)`, so
         `⌊nα+α⌋ ≥ (n+1)c - n⌊α⌋ - n(n-1)(l-⌊α⌋)`
         and
         `⌊nα+α⌋ < (n+1)c - n⌊α⌋ - n(n-1)(l-⌊α⌋) + 1`.
         Also, since `2*l = ⌊α⌋ + ⌊2α⌋`, we have
         `2α+⌊α⌋-1 < 2*l ≤ 2α+⌊α⌋.`-/
      zify[←mul_assoc, this,←eq_sub_iff_add_eq',‹_ =(@ _) /@_›,Int.floor_eq_iff] at *this.ind.intro
x : ℝ
l : ℤ
A : ℕ
c : ℤ
Y : 2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1
this✝¹ : 2 ∣ ↑A * (↑A - 1)
B : ∀ (m : ℕ), ↑m < ↑A → ↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋))
h✝ : (↑A + 1) * ↑c - (↑A * ↑⌊x⌋ + 2 * ↑(↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) ≤ x + ↑A * x ∧
  x + ↑A * x < (↑A + 1) * ↑c - (↑A * ↑⌊x⌋ + 2 * ↑(↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) + 1
this✝ : True
this : True
⊢ ↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋) ≤ x + ↑A * x ∧ x + ↑A * x < 1 + (↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋))
      zify[*]at*this.ind.intro
x : ℝ
l : ℤ
A : ℕ
c : ℤ
Y : 2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1
this✝¹ : 2 ∣ ↑A * (↑A - 1)
B : ∀ (m : ℕ), ↑m < ↑A → ↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋))
this✝ : True
this : True
h✝ : (↑A + 1) * ↑c - (↑A * ↑⌊x⌋ + 2 * (↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) ≤ x + ↑A * x ∧
  x + ↑A * x < (↑A + 1) * ↑c - (↑A * ↑⌊x⌋ + 2 * (↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) + 1
⊢ ↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋) ≤ x + ↑A * x ∧ x + ↑A * x < 1 + (↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋))
      -- We will now show that `c = n*(l-⌊α⌋) + ⌊α⌋`.
      cases unused variable `S5`
note: this linter can be disabled with `set_option linter.unusedVariables false`S5:lt_or_ge c (A * (l-.floor ↑x)+⌊x⌋ + 1)this.ind.intro.inl
x : ℝ
l : ℤ
A : ℕ
c : ℤ
Y : 2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1
this✝¹ : 2 ∣ ↑A * (↑A - 1)
B : ∀ (m : ℕ), ↑m < ↑A → ↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋))
this✝ : True
this : True
h✝¹ : (↑A + 1) * ↑c - (↑A * ↑⌊x⌋ + 2 * (↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) ≤ x + ↑A * x ∧
  x + ↑A * x < (↑A + 1) * ↑c - (↑A * ↑⌊x⌋ + 2 * (↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) + 1
h✝ : c < ↑A * (l - ⌊x⌋) + ⌊x⌋ + 1
S5 : ⋯ = ⋯
⊢ ↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋) ≤ x + ↑A * x ∧ x + ↑A * x < 1 + (↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋))
this.ind.intro.inr
x : ℝ
l : ℤ
A : ℕ
c : ℤ
Y : 2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1
this✝¹ : 2 ∣ ↑A * (↑A - 1)
B : ∀ (m : ℕ), ↑m < ↑A → ↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋))
this✝ : True
this : True
h✝¹ : (↑A + 1) * ↑c - (↑A * ↑⌊x⌋ + 2 * (↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) ≤ x + ↑A * x ∧
  x + ↑A * x < (↑A + 1) * ↑c - (↑A * ↑⌊x⌋ + 2 * (↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) + 1
h✝ : c ≥ ↑A * (l - ⌊x⌋) + ⌊x⌋ + 1
S5 : ⋯ = ⋯
⊢ ↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋) ≤ x + ↑A * x ∧ x + ↑A * x < 1 + (↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋))
      ·this.ind.intro.inl
x : ℝ
l : ℤ
A : ℕ
c : ℤ
Y : 2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1
this✝¹ : 2 ∣ ↑A * (↑A - 1)
B : ∀ (m : ℕ), ↑m < ↑A → ↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋))
this✝ : True
this : True
h✝¹ : (↑A + 1) * ↑c - (↑A * ↑⌊x⌋ + 2 * (↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) ≤ x + ↑A * x ∧
  x + ↑A * x < (↑A + 1) * ↑c - (↑A * ↑⌊x⌋ + 2 * (↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) + 1
h✝ : c < ↑A * (l - ⌊x⌋) + ⌊x⌋ + 1
S5 : ⋯ = ⋯
⊢ ↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋) ≤ x + ↑A * x ∧ x + ↑A * x < 1 + (↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋)) simp_allthis.ind.intro.inl
x : ℝ
l : ℤ
A : ℕ
c : ℤ
Y : 2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1
this : 2 ∣ ↑A * (↑A - 1)
h✝¹ : c < ↑A * (l - ⌊x⌋) + ⌊x⌋ + 1
B : ∀ m < A, ↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋))
h✝ : (↑A + 1) * ↑c ≤ x + ↑A * x + (↑A * ↑⌊x⌋ + 2 * (↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) ∧
  x + ↑A * x < (↑A + 1) * ↑c - (↑A * ↑⌊x⌋ + 2 * (↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) + 1
⊢ ↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋) ≤ x + ↑A * x ∧ x + ↑A * x < 1 + (↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋))
        have:(c+1:ℝ)<=A*(l-⌊x⌋)+⌊x⌋+1:=by⊢ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋} = {α | ∃ k, Even k ∧ α = ↑k} norm_castAll goals completed! 🐙
        simp_allthis.ind.intro.inl
x : ℝ
l : ℤ
A : ℕ
c : ℤ
Y : 2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1
this✝ : 2 ∣ ↑A * (↑A - 1)
h✝¹ : c < ↑A * (l - ⌊x⌋) + ⌊x⌋ + 1
B : ∀ m < A, ↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋))
h✝ : (↑A + 1) * ↑c ≤ x + ↑A * x + (↑A * ↑⌊x⌋ + 2 * (↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) ∧
  x + ↑A * x < (↑A + 1) * ↑c - (↑A * ↑⌊x⌋ + 2 * (↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) + 1
this : ↑c ≤ ↑A * (↑l - ↑⌊x⌋) + ↑⌊x⌋
⊢ ↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋) ≤ x + ↑A * x ∧ x + ↑A * x < 1 + (↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋))
        cases this.eq_or_ltthis.ind.intro.inl.inl
x : ℝ
l : ℤ
A : ℕ
c : ℤ
Y : 2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1
this✝ : 2 ∣ ↑A * (↑A - 1)
h✝² : c < ↑A * (l - ⌊x⌋) + ⌊x⌋ + 1
B : ∀ m < A, ↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋))
h✝¹ : (↑A + 1) * ↑c ≤ x + ↑A * x + (↑A * ↑⌊x⌋ + 2 * (↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) ∧
  x + ↑A * x < (↑A + 1) * ↑c - (↑A * ↑⌊x⌋ + 2 * (↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) + 1
this : ↑c ≤ ↑A * (↑l - ↑⌊x⌋) + ↑⌊x⌋
h✝ : ↑c = ↑A * (↑l - ↑⌊x⌋) + ↑⌊x⌋
⊢ ↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋) ≤ x + ↑A * x ∧ x + ↑A * x < 1 + (↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋))
this.ind.intro.inl.inr
x : ℝ
l : ℤ
A : ℕ
c : ℤ
Y : 2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1
this✝ : 2 ∣ ↑A * (↑A - 1)
h✝² : c < ↑A * (l - ⌊x⌋) + ⌊x⌋ + 1
B : ∀ m < A, ↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋))
h✝¹ : (↑A + 1) * ↑c ≤ x + ↑A * x + (↑A * ↑⌊x⌋ + 2 * (↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) ∧
  x + ↑A * x < (↑A + 1) * ↑c - (↑A * ↑⌊x⌋ + 2 * (↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) + 1
this : ↑c ≤ ↑A * (↑l - ↑⌊x⌋) + ↑⌊x⌋
h✝ : ↑c < ↑A * (↑l - ↑⌊x⌋) + ↑⌊x⌋
⊢ ↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋) ≤ x + ↑A * x ∧ x + ↑A * x < 1 + (↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋))
        ·this.ind.intro.inl.inl
x : ℝ
l : ℤ
A : ℕ
c : ℤ
Y : 2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1
this✝ : 2 ∣ ↑A * (↑A - 1)
h✝² : c < ↑A * (l - ⌊x⌋) + ⌊x⌋ + 1
B : ∀ m < A, ↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋))
h✝¹ : (↑A + 1) * ↑c ≤ x + ↑A * x + (↑A * ↑⌊x⌋ + 2 * (↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) ∧
  x + ↑A * x < (↑A + 1) * ↑c - (↑A * ↑⌊x⌋ + 2 * (↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) + 1
this : ↑c ≤ ↑A * (↑l - ↑⌊x⌋) + ↑⌊x⌋
h✝ : ↑c = ↑A * (↑l - ↑⌊x⌋) + ↑⌊x⌋
⊢ ↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋) ≤ x + ↑A * x ∧ x + ↑A * x < 1 + (↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋)) /- For if `c = n*(l-⌊α⌋) + ⌊α⌋`, then
          $$`
          ⌊(n+1)α⌋ = (n+1)c - n⌊α⌋ - n(n-1)(l-⌊α⌋)
          = (n+1)(n(l - ⌊α⌋) + ⌊α⌋) - n⌊α⌋ - n(n-1)(l-⌊α⌋)
          = 2n(l-⌊α⌋) + ⌊α⌋
          `
          as desired. -/
          repeat use byx : ℝ
l : ℤ
A : ℕ
c : ℤ
Y : 2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1
this✝ : 2 ∣ ↑A * (↑A - 1)
h✝² : c < ↑A * (l - ⌊x⌋) + ⌊x⌋ + 1
B : ∀ m < A, ↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋))
h✝¹ : (↑A + 1) * ↑c ≤ x + ↑A * x + (↑A * ↑⌊x⌋ + 2 * (↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) ∧
  x + ↑A * x < (↑A + 1) * ↑c - (↑A * ↑⌊x⌋ + 2 * (↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) + 1
this : ↑c ≤ ↑A * (↑l - ↑⌊x⌋) + ↑⌊x⌋
h✝ : ↑c = ↑A * (↑l - ↑⌊x⌋) + ↑⌊x⌋
⊢ x + ↑A * x < 1 + (↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋)) nlinarithAll goals completed! 🐙
        /- Now, we show `c = n*(l-⌊α⌋) + ⌊α⌋` via contradiction
        split into two cases. First suppose `c ≤ n(l - ⌊α⌋) + ⌊α⌋ - 1`.
        $$`
        (n+1)α < (n+1)c - n⌊α⌋ - n(n-1)(l-⌊α⌋) + 1
        ≤ (n+1)(n(l-⌊α⌋) + ⌊α⌋ - 1) - n⌊α⌋ - n(n-1)(l-⌊α⌋) + 1
        = 2n(l-⌊α⌋) + ⌊α⌋ - n
        = 2ln - 2n⌊α⌋ + ⌊α⌋ - n
        ≤ (2α+⌊α⌋)n - 2n⌊α⌋ + ⌊α⌋ - n
        = nα + n(α-⌊α⌋-1) + ⌊α⌋
        n + α.
        `
        contradiction. -/
        nlinarith[(byx : ℝ
l : ℤ
A : ℕ
c : ℤ
Y : 2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1
this✝ : 2 ∣ ↑A * (↑A - 1)
h✝² : c < ↑A * (l - ⌊x⌋) + ⌊x⌋ + 1
B : ∀ m < A, ↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋))
h✝¹ : (↑A + 1) * ↑c ≤ x + ↑A * x + (↑A * ↑⌊x⌋ + 2 * (↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) ∧
  x + ↑A * x < (↑A + 1) * ↑c - (↑A * ↑⌊x⌋ + 2 * (↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) + 1
this : ↑c ≤ ↑A * (↑l - ↑⌊x⌋) + ↑⌊x⌋
h✝ : ↑c < ↑A * (↑l - ↑⌊x⌋) + ↑⌊x⌋
⊢ ↑A * (↑l - ↑⌊x⌋) + ↑⌊x⌋ ≥ ↑c + 1 norm_cast at*All goals completed! 🐙 :(A*(l -⌊x⌋):ℝ)+⌊(x)⌋ >=(c)+01),9,Int.add_emod ↑5,Int.floor_le (@x : ℝ),Int.lt_floor_add_one (x:)]
      /- Next, suppose `c ≥ n(l - ⌊α⌋) + ⌊α⌋ + 1`.
      $$`
      (n+1)α ≥ (n+1)c - n⌊α⌋ - n(n-1)(l-⌊α⌋)
      ≥ (n+1)(n(l-⌊α⌋) + ⌊α⌋ + 1) - n⌊α⌋ - n(n-1)(l-⌊α⌋)
      = 2n(l-⌊α⌋) + ⌊α⌋ + n + 1
      = 2ln - 2n⌊α⌋ + ⌊α⌋ + n + 1
      > (2α+⌊α⌋-1)n - 2n⌊α⌋ + ⌊α⌋ + n + 1
      = nα + n(α-⌊α⌋) + ⌊α⌋ + 1
      > n + α
      `
      contradiction. -/
      simp_allthis.ind.intro.inr
x : ℝ
l : ℤ
A : ℕ
c : ℤ
Y : 2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1
this : 2 ∣ ↑A * (↑A - 1)
h✝¹ : c ≥ ↑A * (l - ⌊x⌋) + ⌊x⌋ + 1
B : ∀ m < A, ↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋))
h✝ : (↑A + 1) * ↑c ≤ x + ↑A * x + (↑A * ↑⌊x⌋ + 2 * (↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) ∧
  x + ↑A * x < (↑A + 1) * ↑c - (↑A * ↑⌊x⌋ + 2 * (↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) + 1
⊢ ↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋) ≤ x + ↑A * x ∧ x + ↑A * x < 1 + (↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋))
      nlinarith[(byx : ℝ
l : ℤ
A : ℕ
c : ℤ
Y : 2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1
this : 2 ∣ ↑A * (↑A - 1)
h✝¹ : c ≥ ↑A * (l - ⌊x⌋) + ⌊x⌋ + 1
B : ∀ m < A, ↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋))
h✝ : (↑A + 1) * ↑c ≤ x + ↑A * x + (↑A * ↑⌊x⌋ + 2 * (↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) ∧
  x + ↑A * x < (↑A + 1) * ↑c - (↑A * ↑⌊x⌋ + 2 * (↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) + 1
⊢ ↑c ≥ ↑A * (↑l - ↑⌊x⌋) + ↑⌊x⌋ + 1 norm_castAll goals completed! 🐙:(c:ℝ)>=A*(l-⌊_⌋)+⌊_⌋+1),Int.floor_le x,Int.lt_floor_add_one x]
    rw [←Nat.cast_sum, mul_sub, Finset.sum_range_id]this
x : ℝ
l : ℤ
A : ℕ
c : ℤ
Y : 2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1
B : ∀ m < A, ↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)))
h✝ : ∑ x_1 ∈ Finset.range A, ⌊x + ↑x_1 * x⌋ = (↑A + 1) * c - ⌊x + ↑A * x⌋
this : ∑ d ∈ Finset.range A, ⌊x + ↑d * x⌋ = ∑ Q ∈ Finset.range A, (⌊x⌋ + 2 * (↑Q * (l - ⌊x⌋)))
⊢ ↑(A * (A - 1) / 2) = (↑A * ↑A - ↑A * 1) / 2
    cases A with|_=>this.succ
x : ℝ
l : ℤ
c : ℤ
Y : 2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1
n✝ : ℕ
B : ∀ m < n✝ + 1, ↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)))
h✝ : ∑ x_1 ∈ Finset.range (n✝ + 1), ⌊x + ↑x_1 * x⌋ = (↑(n✝ + 1) + 1) * c - ⌊x + ↑(n✝ + 1) * x⌋
this : ∑ d ∈ Finset.range (n✝ + 1), ⌊x + ↑d * x⌋ = ∑ Q ∈ Finset.range (n✝ + 1), (⌊x⌋ + 2 * (↑Q * (l - ⌊x⌋)))
⊢ ↑((n✝ + 1) * (n✝ + 1 - 1) / 2) = (↑(n✝ + 1) * ↑(n✝ + 1) - ↑(n✝ + 1) * 1) / 2norm_num[mul_add]All goals completed! 🐙
  use Finset.sum_congr rfl<|byx : ℝ
l : ℤ
A : ℕ
c : ℤ
Y : 2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1
B : ∀ m < A, ↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)))
h✝ : ∑ x_1 ∈ Finset.range A, ⌊x + ↑x_1 * x⌋ = (↑A + 1) * c - ⌊x + ↑A * x⌋
⊢ ∀ x_1 ∈ Finset.range A, ⌊x + ↑x_1 * x⌋ = ⌊x⌋ + 2 * (↑x_1 * (l - ⌊x⌋)) simp_all[add_comm,Int.floor_eq_iff]All goals completed! 🐙

The following command shows which axioms the proof relies upon:

'imo_2024_p1' depends on axioms: [propext, Classical.choice, Quot.sound]#print axioms imo_2024_p1

'imo_2024_p1' depends on axioms: [propext, Classical.choice, Quot.sound]

These are the standard built in axioms.