case intro
p q y : ℝ
r✝ : ℚ
m : ℤ
n : ℕ
hp : 1 < p
r : ℚ
h : LiouvilleWith p ↑r
⊢ False
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
h : LiouvilleWith p x
hp : 1 < p
⊢ Irrational x
rintro ⟨r, rfl⟩
case intro.inl
p q y : ℝ
r : ℚ
m : ℤ
n : ℕ
hp : 1 < p
h : LiouvilleWith p ↑0
⊢ False

case intro.inr
p q y : ℝ
r✝ : ℚ
m : ℤ
n : ℕ
hp : 1 < p
r : ℚ
h : LiouvilleWith p ↑r
h0 : r ≠ 0
⊢ False
case intro
p q y : ℝ
r✝ : ℚ
m : ℤ
n : ℕ
hp : 1 < p
r : ℚ
h : LiouvilleWith p ↑r
⊢ False
rcases eq_or_ne r 0 with (rfl | h0)
case intro.inl
p q y : ℝ
r : ℚ
m : ℤ
n : ℕ
hp : 1 < p
h : LiouvilleWith p ↑0
⊢ ↑0 = ↑0
case intro.inl
p q y : ℝ
r : ℚ
m : ℤ
n : ℕ
hp : 1 < p
h : LiouvilleWith p ↑0
⊢ False
refine h.ne_cast_int hp 0 ?_
no goals
case intro.inl
p q y : ℝ
r : ℚ
m : ℤ
n : ℕ
hp : 1 < p
h : LiouvilleWith p ↑0
⊢ ↑0 = ↑0
rw [Rat.cast_zero, Int.cast_zero]
case intro.inr
p q y : ℝ
r✝ : ℚ
m : ℤ
n : ℕ
hp : 1 < p
r : ℚ
h : LiouvilleWith p ↑r
h0 : r ≠ 0
⊢ ↑r * ↑r⁻¹ = ↑1
case intro.inr
p q y : ℝ
r✝ : ℚ
m : ℤ
n : ℕ
hp : 1 < p
r : ℚ
h : LiouvilleWith p ↑r
h0 : r ≠ 0
⊢ False
refine (h.mul_rat (inv_ne_zero h0)).ne_cast_int hp 1 ?_
case intro.inr
p q y : ℝ
r✝ : ℚ
m : ℤ
n : ℕ
hp : 1 < p
r : ℚ
h : LiouvilleWith p ↑r
h0 : r ≠ 0
⊢ 1 = ↑1

case intro.inr
p q y : ℝ
r✝ : ℚ
m : ℤ
n : ℕ
hp : 1 < p
r : ℚ
h : LiouvilleWith p ↑r
h0 : r ≠ 0
⊢ ↑r ≠ 0
case intro.inr
p q y : ℝ
r✝ : ℚ
m : ℤ
n : ℕ
hp : 1 < p
r : ℚ
h : LiouvilleWith p ↑r
h0 : r ≠ 0
⊢ ↑r * ↑r⁻¹ = ↑1
rw [Rat.cast_inv, mul_inv_cancel]
no goals
case intro.inr
p q y : ℝ
r✝ : ℚ
m : ℤ
n : ℕ
hp : 1 < p
r : ℚ
h : LiouvilleWith p ↑r
h0 : r ≠ 0
⊢ 1 = ↑1

case intro.inr
p q y : ℝ
r✝ : ℚ
m : ℤ
n : ℕ
hp : 1 < p
r : ℚ
h : LiouvilleWith p ↑r
h0 : r ≠ 0
⊢ ↑r ≠ 0
exacts [Int.cast_one.symm, Rat.cast_ne_zero.mpr h0]