case intro
a : ℚ
tr : Transcendental ℚ ↑a
⊢ False
r : ℝ
tr : Transcendental ℚ r
⊢ Irrational r
rintro ⟨a, rfl⟩
no goals
case intro
a : ℚ
tr : Transcendental ℚ ↑a
⊢ False
exact tr (isAlgebraic_algebraMap a)