case inl
x : ℝ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hxr : x ^ 0 = ↑m
hv : Part.get (multiplicity (↑p) m) (_ : multiplicity.Finite (↑p) m) % 0 ≠ 0
⊢ Irrational x

case inr
x : ℝ
n : ℕ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hxr : x ^ n = ↑m
hv : Part.get (multiplicity (↑p) m) (_ : multiplicity.Finite (↑p) m) % n ≠ 0
hnpos : n > 0
⊢ Irrational x
x : ℝ
n : ℕ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hxr : x ^ n = ↑m
hv : Part.get (multiplicity (↑p) m) (_ : multiplicity.Finite (↑p) m) % n ≠ 0
⊢ Irrational x
rcases Nat.eq_zero_or_pos n with (rfl | hnpos)
case inr
x : ℝ
n : ℕ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hxr : x ^ n = ↑m
hv : Part.get (multiplicity (↑p) m) (_ : multiplicity.Finite (↑p) m) % n ≠ 0
hnpos : n > 0
⊢ ¬∃ y, x = ↑y
case inr
x : ℝ
n : ℕ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hxr : x ^ n = ↑m
hv : Part.get (multiplicity (↑p) m) (_ : multiplicity.Finite (↑p) m) % n ≠ 0
hnpos : n > 0
⊢ Irrational x
refine' irrational_nrt_of_notint_nrt _ _ hxr _ hnpos
case inr.intro
n : ℕ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hv : Part.get (multiplicity (↑p) m) (_ : multiplicity.Finite (↑p) m) % n ≠ 0
hnpos : n > 0
y : ℤ
hxr : ↑y ^ n = ↑m
⊢ False
case inr
x : ℝ
n : ℕ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hxr : x ^ n = ↑m
hv : Part.get (multiplicity (↑p) m) (_ : multiplicity.Finite (↑p) m) % n ≠ 0
hnpos : n > 0
⊢ ¬∃ y, x = ↑y
rintro ⟨y, rfl⟩
case inr.intro
n : ℕ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hv : Part.get (multiplicity (↑p) m) (_ : multiplicity.Finite (↑p) m) % n ≠ 0
hnpos : n > 0
y : ℤ
hxr : y ^ n = m
⊢ False
case inr.intro
n : ℕ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hv : Part.get (multiplicity (↑p) m) (_ : multiplicity.Finite (↑p) m) % n ≠ 0
hnpos : n > 0
y : ℤ
hxr : ↑y ^ n = ↑m
⊢ False
rw [← Int.cast_pow, Int.cast_inj] at hxr
case inr.intro
n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
y : ℤ
hm : y ^ n ≠ 0
hv : Part.get (multiplicity (↑p) (y ^ n)) (_ : multiplicity.Finite (↑p) (y ^ n)) % n ≠ 0
⊢ False
case inr.intro
n : ℕ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hv : Part.get (multiplicity (↑p) m) (_ : multiplicity.Finite (↑p) m) % n ≠ 0
hnpos : n > 0
y : ℤ
hxr : y ^ n = m
⊢ False
subst m
case inr.intro
n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
y : ℤ
hm : y ^ n ≠ 0
hv : Part.get (multiplicity (↑p) (y ^ n)) (_ : multiplicity.Finite (↑p) (y ^ n)) % n ≠ 0
this : y ≠ 0
⊢ False
case inr.intro
n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
y : ℤ
hm : y ^ n ≠ 0
hv : Part.get (multiplicity (↑p) (y ^ n)) (_ : multiplicity.Finite (↑p) (y ^ n)) % n ≠ 0
⊢ False
have : y ≠ 0 := by
  rintro rfl
  rw [zero_pow hnpos] at hm
  exact hm rfl
case inr.intro
n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
y : ℤ
hm : y ^ n ≠ 0
this : y ≠ 0
hv : 0 ≠ 0
⊢ False
case inr.intro
n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
y : ℤ
hm : y ^ n ≠ 0
hv : Part.get (multiplicity (↑p) (y ^ n)) (_ : multiplicity.Finite (↑p) (y ^ n)) % n ≠ 0
this : y ≠ 0
⊢ False
erw [multiplicity.pow' (Nat.prime_iff_prime_int.1 hp.1) (finite_int_iff.2 ⟨hp.1.ne_one, this⟩),
  Nat.mul_mod_right] at hv
no goals
case inr.intro
n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
y : ℤ
hm : y ^ n ≠ 0
this : y ≠ 0
hv : 0 ≠ 0
⊢ False
exact hv rfl
case inl
x : ℝ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hxr : m = 1
hv : Part.get (multiplicity (↑p) m) (_ : multiplicity.Finite (↑p) m) % 0 ≠ 0
⊢ Irrational x
case inl
x : ℝ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hxr : x ^ 0 = ↑m
hv : Part.get (multiplicity (↑p) m) (_ : multiplicity.Finite (↑p) m) % 0 ≠ 0
⊢ Irrational x
rw [eq_comm, pow_zero, ← Int.cast_one, Int.cast_inj] at hxr
no goals
case inl
x : ℝ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hxr : m = 1
hv : Part.get (multiplicity (↑p) m) (_ : multiplicity.Finite (↑p) m) % 0 ≠ 0
⊢ Irrational x
simp [hxr,
  multiplicity.one_right (mt isUnit_iff_dvd_one.1 (mt Int.coe_nat_dvd.1 hp.1.not_dvd_one)),
  Nat.zero_mod] at hv
n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
hm : 0 ^ n ≠ 0
hv : Part.get (multiplicity (↑p) (0 ^ n)) (_ : multiplicity.Finite (↑p) (0 ^ n)) % n ≠ 0
⊢ False
n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
y : ℤ
hm : y ^ n ≠ 0
hv : Part.get (multiplicity (↑p) (y ^ n)) (_ : multiplicity.Finite (↑p) (y ^ n)) % n ≠ 0
⊢ y ≠ 0
rintro rfl
n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
hm✝ : 0 ^ n ≠ 0
hm : 0 ≠ 0
hv : Part.get (multiplicity (↑p) (0 ^ n)) (_ : multiplicity.Finite (↑p) (0 ^ n)) % n ≠ 0
⊢ False
n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
hm : 0 ^ n ≠ 0
hv : Part.get (multiplicity (↑p) (0 ^ n)) (_ : multiplicity.Finite (↑p) (0 ^ n)) % n ≠ 0
⊢ False
rw [zero_pow hnpos] at hm
no goals
n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
hm✝ : 0 ^ n ≠ 0
hm : 0 ≠ 0
hv : Part.get (multiplicity (↑p) (0 ^ n)) (_ : multiplicity.Finite (↑p) (0 ^ n)) % n ≠ 0
⊢ False
exact hm rfl