case inl
α : Type ?u.916813
β : Type ?u.916816
n d k : ℕ
x : Fin n → ℕ
⊢ ↑0 * exp (-4 * Real.sqrt (log ↑0)) ≤ ↑(↑rothNumberNat 0)

case inr
α : Type ?u.916813
β : Type ?u.916816
n d k N : ℕ
x : Fin n → ℕ
hN : N > 0
⊢ ↑N * exp (-4 * Real.sqrt (log ↑N)) ≤ ↑(↑rothNumberNat N)
α : Type ?u.916813
β : Type ?u.916816
n d k N : ℕ
x : Fin n → ℕ
⊢ ↑N * exp (-4 * Real.sqrt (log ↑N)) ≤ ↑(↑rothNumberNat N)
obtain rfl | hN := Nat.eq_zero_or_pos N
case inr.inl
α : Type ?u.916813
β : Type ?u.916816
n d k N : ℕ
x : Fin n → ℕ
hN : N > 0
h₁ : 4096 ≤ N
⊢ ↑N * exp (-4 * Real.sqrt (log ↑N)) ≤ ↑(↑rothNumberNat N)

case inr.inr
α : Type ?u.916813
β : Type ?u.916816
n d k N : ℕ
x : Fin n → ℕ
hN : N > 0
h₁ : N < 4096
⊢ ↑N * exp (-4 * Real.sqrt (log ↑N)) ≤ ↑(↑rothNumberNat N)
case inr
α : Type ?u.916813
β : Type ?u.916816
n d k N : ℕ
x : Fin n → ℕ
hN : N > 0
⊢ ↑N * exp (-4 * Real.sqrt (log ↑N)) ≤ ↑(↑rothNumberNat N)
obtain h₁ | h₁ := le_or_lt 4096 N
no goals
case inl
α : Type ?u.916813
β : Type ?u.916816
n d k : ℕ
x : Fin n → ℕ
⊢ ↑0 * exp (-4 * Real.sqrt (log ↑0)) ≤ ↑(↑rothNumberNat 0)
norm_num
no goals
case inr.inl
α : Type ?u.916813
β : Type ?u.916816
n d k N : ℕ
x : Fin n → ℕ
hN : N > 0
h₁ : 4096 ≤ N
⊢ ↑N * exp (-4 * Real.sqrt (log ↑N)) ≤ ↑(↑rothNumberNat N)
exact (roth_lower_bound_explicit h₁).le
case inr.inr
α : Type ?u.916813
β : Type ?u.916816
n d k N : ℕ
x : Fin n → ℕ
hN : N > 0
h₁ : N < 4096
⊢ 1 ≤ ↑(↑rothNumberNat N)
case inr.inr
α : Type ?u.916813
β : Type ?u.916816
n d k N : ℕ
x : Fin n → ℕ
hN : N > 0
h₁ : N < 4096
⊢ ↑N * exp (-4 * Real.sqrt (log ↑N)) ≤ ↑(↑rothNumberNat N)
apply (lower_bound_le_one hN h₁.le).trans
no goals
case inr.inr
α : Type ?u.916813
β : Type ?u.916816
n d k N : ℕ
x : Fin n → ℕ
hN : N > 0
h₁ : N < 4096
⊢ 1 ≤ ↑(↑rothNumberNat N)
simpa using rothNumberNat.monotone hN