q : ℚ
x y : ℝ
h : Irrational 1
⊢ Irrational x
q : ℚ
x y : ℝ
h : Irrational (x ^ 0)
⊢ Irrational x
rw [pow_zero] at h
no goals
q : ℚ
x y : ℝ
h : Irrational 1
⊢ Irrational x
exact (h ⟨1, cast_one⟩).elim
q : ℚ
x y : ℝ
n : ℕ
h : Irrational (x * x ^ n)
⊢ Irrational x
q : ℚ
x y : ℝ
n : ℕ
h : Irrational (x ^ (n + 1))
⊢ Irrational x
rw [pow_succ] at h
no goals
q : ℚ
x y : ℝ
n : ℕ
h : Irrational (x * x ^ n)
⊢ Irrational x
exact h.mul_cases.elim id (of_pow n)