Theorem: book.irrational.Theorem_1 (FormalBook/Chapter_08.lean)

State before:
r : ℚ
h_r : r ≠ 0
⊢ irrational (↑r).exp
Tactic:
have : ∀ k : ℤ, k > 0 → irrational (exp k) := by
  sorry
State after:
r : ℚ
h_r : r ≠ 0
this : ∀ k > 0, irrational (↑k).exp
⊢ irrational (↑r).exp

State before:
r : ℚ
h_r : r ≠ 0
this : ∀ k > 0, irrational (↑k).exp
⊢ irrational (↑r).exp
Tactic:
sorry
State after:
no goals

State before:
r : ℚ
h_r : r ≠ 0
⊢ ∀ k > 0, irrational (↑k).exp
Tactic:
sorry
State after:
no goals