case intro
m t : ℕ
hl : m * m < t * t
hr : t * t < (m + 1) * (m + 1)
⊢ False
n m : ℕ
hl : m * m < n
hr : n < (m + 1) * (m + 1)
⊢ ¬∃ t, t * t = n
rintro ⟨t, rfl⟩
case intro
m t : ℕ
hl : m * m < t * t
hr : t * t < (m + 1) * (m + 1)
h1 : m < t
⊢ False
case intro
m t : ℕ
hl : m * m < t * t
hr : t * t < (m + 1) * (m + 1)
⊢ False
have h1 : m < t := Nat.mul_self_lt_mul_self_iff.mpr hl
case intro
m t : ℕ
hl : m * m < t * t
hr : t * t < (m + 1) * (m + 1)
h1 : m < t
h2 : t < m + 1
⊢ False
case intro
m t : ℕ
hl : m * m < t * t
hr : t * t < (m + 1) * (m + 1)
h1 : m < t
⊢ False
have h2 : t < m + 1 := Nat.mul_self_lt_mul_self_iff.mpr hr
no goals
case intro
m t : ℕ
hl : m * m < t * t
hr : t * t < (m + 1) * (m + 1)
h1 : m < t
h2 : t < m + 1
⊢ False
exact (not_lt_of_ge <| le_of_lt_succ h2) h1