case intro.mk'
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : Nat.coprime (Int.natAbs N) D
hxr : ↑(mk' N D) ^ n = ↑m
hv : ¬∃ y, ↑(mk' N D) = ↑y
⊢ False
x : ℝ
n : ℕ
m : ℤ
hxr : x ^ n = ↑m
hv : ¬∃ y, x = ↑y
hnpos : 0 < n
⊢ Irrational x
rintro ⟨⟨N, D, P, C⟩, rfl⟩
case intro.mk'
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : Nat.coprime (Int.natAbs N) D
hxr : ↑(mk' N D ^ n) = ↑m
hv : ¬∃ y, ↑(mk' N D) = ↑y
⊢ False
case intro.mk'
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : Nat.coprime (Int.natAbs N) D
hxr : ↑(mk' N D) ^ n = ↑m
hv : ¬∃ y, ↑(mk' N D) = ↑y
⊢ False
rw [← cast_pow] at hxr
case intro.mk'
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : Nat.coprime (Int.natAbs N) D
hxr : ↑(mk' N D ^ n) = ↑m
hv : ¬∃ y, ↑(mk' N D) = ↑y
c1 : ↑↑D ≠ 0
⊢ False
case intro.mk'
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : Nat.coprime (Int.natAbs N) D
hxr : ↑(mk' N D ^ n) = ↑m
hv : ¬∃ y, ↑(mk' N D) = ↑y
⊢ False
have c1 : ((D : ℤ) : ℝ) ≠ 0 := by
  rw [Int.cast_ne_zero, Int.coe_nat_ne_zero]
  exact P
case intro.mk'
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : Nat.coprime (Int.natAbs N) D
hxr : ↑(mk' N D ^ n) = ↑m
hv : ¬∃ y, ↑(mk' N D) = ↑y
c1 : ↑↑D ≠ 0
c2 : ↑↑D ^ n ≠ 0
⊢ False
case intro.mk'
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : Nat.coprime (Int.natAbs N) D
hxr : ↑(mk' N D ^ n) = ↑m
hv : ¬∃ y, ↑(mk' N D) = ↑y
c1 : ↑↑D ≠ 0
⊢ False
have c2 : ((D : ℤ) : ℝ) ^ n ≠ 0 := pow_ne_zero _ c1
case intro.mk'
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : Nat.coprime (Int.natAbs N) D
hxr : m * ↑D ^ n = N ^ n
hv : ¬∃ y, ↑(mk' N D) = ↑y
c1 : ↑↑D ≠ 0
c2 : ↑↑D ^ n ≠ 0
⊢ False
case intro.mk'
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : Nat.coprime (Int.natAbs N) D
hxr : ↑(mk' N D ^ n) = ↑m
hv : ¬∃ y, ↑(mk' N D) = ↑y
c1 : ↑↑D ≠ 0
c2 : ↑↑D ^ n ≠ 0
⊢ False
rw [num_den', cast_pow, cast_mk, div_pow, div_eq_iff_mul_eq c2, ← Int.cast_pow, ← Int.cast_pow,
  ← Int.cast_mul, Int.cast_inj] at hxr
case intro.mk'
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : Nat.coprime (Int.natAbs N) D
hxr : m * ↑D ^ n = N ^ n
hv : ¬∃ y, ↑(mk' N D) = ↑y
c1 : ↑↑D ≠ 0
c2 : ↑↑D ^ n ≠ 0
hdivn : ↑D ^ n ∣ N ^ n
⊢ False
case intro.mk'
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : Nat.coprime (Int.natAbs N) D
hxr : m * ↑D ^ n = N ^ n
hv : ¬∃ y, ↑(mk' N D) = ↑y
c1 : ↑↑D ≠ 0
c2 : ↑↑D ^ n ≠ 0
⊢ False
have hdivn : (D : ℤ) ^ n ∣ N ^ n := Dvd.intro_left m hxr
case intro.mk'
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : Nat.coprime (Int.natAbs N) D
hxr : m * ↑D ^ n = N ^ n
hv : ¬∃ y, ↑(mk' N D) = ↑y
c1 : ↑↑D ≠ 0
c2 : ↑↑D ^ n ≠ 0
hdivn : D ∣ Int.natAbs N
⊢ False
case intro.mk'
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : Nat.coprime (Int.natAbs N) D
hxr : m * ↑D ^ n = N ^ n
hv : ¬∃ y, ↑(mk' N D) = ↑y
c1 : ↑↑D ≠ 0
c2 : ↑↑D ^ n ≠ 0
hdivn : ↑D ^ n ∣ N ^ n
⊢ False
rw [← Int.dvd_natAbs, ← Int.coe_nat_pow, Int.coe_nat_dvd, Int.natAbs_pow,
  Nat.pow_dvd_pow_iff hnpos] at hdivn
case intro.mk'
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
P : 1 ≠ 0
C : Nat.coprime (Int.natAbs N) 1
hxr : m * ↑1 ^ n = N ^ n
hv : ¬∃ y, ↑(mk' N 1) = ↑y
c1 : ↑↑1 ≠ 0
c2 : ↑↑1 ^ n ≠ 0
hdivn : 1 ∣ Int.natAbs N
⊢ False
case intro.mk'
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : Nat.coprime (Int.natAbs N) D
hxr : m * ↑D ^ n = N ^ n
hv : ¬∃ y, ↑(mk' N D) = ↑y
c1 : ↑↑D ≠ 0
c2 : ↑↑D ^ n ≠ 0
hdivn : D ∣ Int.natAbs N
⊢ False
obtain rfl : D = 1 := by rw [← Nat.gcd_eq_right hdivn, C.gcd_eq_one]
case intro.mk'
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
P : 1 ≠ 0
C : Nat.coprime (Int.natAbs N) 1
hxr : m * ↑1 ^ n = N ^ n
hv : ¬∃ y, ↑(mk' N 1) = ↑y
c1 : ↑↑1 ≠ 0
c2 : ↑↑1 ^ n ≠ 0
hdivn : 1 ∣ Int.natAbs N
⊢ ↑(mk' N 1) = ↑N
case intro.mk'
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
P : 1 ≠ 0
C : Nat.coprime (Int.natAbs N) 1
hxr : m * ↑1 ^ n = N ^ n
hv : ¬∃ y, ↑(mk' N 1) = ↑y
c1 : ↑↑1 ≠ 0
c2 : ↑↑1 ^ n ≠ 0
hdivn : 1 ∣ Int.natAbs N
⊢ False
refine' hv ⟨N, _⟩
no goals
case intro.mk'
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
P : 1 ≠ 0
C : Nat.coprime (Int.natAbs N) 1
hxr : m * ↑1 ^ n = N ^ n
hv : ¬∃ y, ↑(mk' N 1) = ↑y
c1 : ↑↑1 ≠ 0
c2 : ↑↑1 ^ n ≠ 0
hdivn : 1 ∣ Int.natAbs N
⊢ ↑(mk' N 1) = ↑N
rw [num_den', Int.ofNat_one, divInt_one, cast_coe_int]
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : Nat.coprime (Int.natAbs N) D
hxr : ↑(mk' N D ^ n) = ↑m
hv : ¬∃ y, ↑(mk' N D) = ↑y
⊢ D ≠ 0
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : Nat.coprime (Int.natAbs N) D
hxr : ↑(mk' N D ^ n) = ↑m
hv : ¬∃ y, ↑(mk' N D) = ↑y
⊢ ↑↑D ≠ 0
rw [Int.cast_ne_zero, Int.coe_nat_ne_zero]
no goals
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : Nat.coprime (Int.natAbs N) D
hxr : ↑(mk' N D ^ n) = ↑m
hv : ¬∃ y, ↑(mk' N D) = ↑y
⊢ D ≠ 0
exact P
no goals
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : Nat.coprime (Int.natAbs N) D
hxr : m * ↑D ^ n = N ^ n
hv : ¬∃ y, ↑(mk' N D) = ↑y
c1 : ↑↑D ≠ 0
c2 : ↑↑D ^ n ≠ 0
hdivn : D ∣ Int.natAbs N
⊢ D = 1
rw [← Nat.gcd_eq_right hdivn, C.gcd_eq_one]