-- Mathlib/Data/Real/Irrational.lean
theorem irrational_nrt_of_n_not_dvd_multiplicity {x : ℝ} (n : ℕ) {m : ℤ} (hm : m ≠ 0) (p : ℕ)
    [hp : Fact p.Prime] (hxr : x ^ n = m)
    (hv : multiplicity (p : ℤ) m % n ≠ 0) :
    Irrational x

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

Tactic:
rw [eq_comm, pow_zero, ← Int.cast_one, Int.cast_inj] at hxr

Result:
case inl
x : ℝ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hxr : m = 1
hv : multiplicity (↑p) m % 0 ≠ 0
⊢ Irrational x

Proof state:
n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
hm : 0 ^ n ≠ 0
hv : multiplicity (↑p) (0 ^ n) % n ≠ 0
⊢ False

Tactic:
rw [zero_pow hnpos.ne'] at hm

Result:
n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
hm : 0 ≠ 0
hv : multiplicity (↑p) (0 ^ n) % n ≠ 0
⊢ False

Proof state:
case inr.intro
n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
y : ℤ
hm : y ^ n ≠ 0
hv : multiplicity (↑p) (y ^ n) % n ≠ 0
this : y ≠ 0
⊢ False

Tactic:
rw [(Int.finiteMultiplicity_iff.2 ⟨by simp [hp.1.ne_one], this⟩).multiplicity_pow
  (Nat.prime_iff_prime_int.1 hp.1), Nat.mul_mod_right] at hv

Result:
case inr.intro
n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
y : ℤ
hm : y ^ n ≠ 0
hv : 0 ≠ 0
this : y ≠ 0
⊢ False

Proof state:
case inr.intro
n : ℕ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hv : multiplicity (↑p) m % n ≠ 0
hnpos : n > 0
y : ℤ
hxr : ↑y ^ n = ↑m
⊢ False

Tactic:
rw [← Int.cast_pow, Int.cast_inj] at hxr

Result:
case inr.intro
n : ℕ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hv : multiplicity (↑p) m % n ≠ 0
hnpos : n > 0
y : ℤ
hxr : y ^ n = m
⊢ False

Proof state:
case inr.intro
n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
y : ℤ
hm : y ^ n ≠ 0
hv : multiplicity (↑p) (y ^ n) % n ≠ 0
⊢ False

Tactic:
have : y ≠ 0 := by rintro rfl; rw [zero_pow hnpos.ne'] at hm; exact hm rfl

Result:
case inr.intro
n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
y : ℤ
hm : y ^ n ≠ 0
hv : multiplicity (↑p) (y ^ n) % n ≠ 0
this : y ≠ 0
⊢ False

Proof state:
case inl
x : ℝ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hxr : m = 1
hv : multiplicity (↑p) m % 0 ≠ 0
⊢ Irrational x

Tactic:
simp [hxr, multiplicity_of_one_right (mt isUnit_iff_dvd_one.1
  (mt Int.natCast_dvd_natCast.1 hp.1.not_dvd_one)), Nat.zero_mod] at hv

Result:
no goals

Proof state:
n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
y : ℤ
hm : y ^ n ≠ 0
hv : multiplicity (↑p) (y ^ n) % n ≠ 0
this : y ≠ 0
⊢ (↑p).natAbs ≠ 1

Tactic:
simp [hp.1.ne_one]

Result:
no goals

Proof state:
case inr.intro
n : ℕ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hv : multiplicity (↑p) m % n ≠ 0
hnpos : n > 0
y : ℤ
hxr : y ^ n = m
⊢ False

Tactic:
subst m

Result:
case inr.intro
n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
y : ℤ
hm : y ^ n ≠ 0
hv : multiplicity (↑p) (y ^ n) % n ≠ 0
⊢ False

Proof state:
case inr.intro
n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
y : ℤ
hm : y ^ n ≠ 0
hv : 0 ≠ 0
this : y ≠ 0
⊢ False

Tactic:
exact hv rfl

Result:
no goals

Proof state:
case inr
x : ℝ
n : ℕ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hxr : x ^ n = ↑m
hv : multiplicity (↑p) m % n ≠ 0
hnpos : n > 0
⊢ Irrational x

Tactic:
refine irrational_nrt_of_notint_nrt _ _ hxr ?_ hnpos

Result:
case inr
x : ℝ
n : ℕ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hxr : x ^ n = ↑m
hv : multiplicity (↑p) m % n ≠ 0
hnpos : n > 0
⊢ ¬∃ y, x = ↑y

Proof state:
n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
y : ℤ
hm : y ^ n ≠ 0
hv : multiplicity (↑p) (y ^ n) % n ≠ 0
⊢ y ≠ 0

Tactic:
rintro rfl

Result:
n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
hm : 0 ^ n ≠ 0
hv : multiplicity (↑p) (0 ^ n) % n ≠ 0
⊢ False

Proof state:
n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
hm : 0 ≠ 0
hv : multiplicity (↑p) (0 ^ n) % n ≠ 0
⊢ False

Tactic:
exact hm rfl

Result:
no goals

Proof state:
case inr
x : ℝ
n : ℕ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hxr : x ^ n = ↑m
hv : multiplicity (↑p) m % n ≠ 0
hnpos : n > 0
⊢ ¬∃ y, x = ↑y

Tactic:
rintro ⟨y, rfl⟩

Result:
case inr.intro
n : ℕ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hv : multiplicity (↑p) m % n ≠ 0
hnpos : n > 0
y : ℤ
hxr : ↑y ^ n = ↑m
⊢ False

Proof state:
x : ℝ
n : ℕ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hxr : x ^ n = ↑m
hv : multiplicity (↑p) m % n ≠ 0
⊢ Irrational x

Tactic:
rcases Nat.eq_zero_or_pos n with (rfl | hnpos)

Result:
case inl
x : ℝ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hxr : x ^ 0 = ↑m
hv : multiplicity (↑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 : multiplicity (↑p) m % n ≠ 0
hnpos : n > 0
⊢ Irrational x