q : ℚ
x y : ℝ
⊢ ¬x * y ∈ Set.range Rat.cast → ¬x ∈ Set.range Rat.cast ∨ ¬y ∈ Set.range Rat.cast
q : ℚ
x y : ℝ
⊢ Irrational (x * y) → Irrational x ∨ Irrational y
delta Irrational
q : ℚ
x y : ℝ
⊢ x ∈ Set.range Rat.cast ∧ y ∈ Set.range Rat.cast → x * y ∈ Set.range Rat.cast
q : ℚ
x y : ℝ
⊢ ¬x * y ∈ Set.range Rat.cast → ¬x ∈ Set.range Rat.cast ∨ ¬y ∈ Set.range Rat.cast
contrapose!
case intro.intro.intro
q rx ry : ℚ
⊢ ↑rx * ↑ry ∈ Set.range Rat.cast
q : ℚ
x y : ℝ
⊢ x ∈ Set.range Rat.cast ∧ y ∈ Set.range Rat.cast → x * y ∈ Set.range Rat.cast
rintro ⟨⟨rx, rfl⟩, ⟨ry, rfl⟩⟩
no goals
case intro.intro.intro
q rx ry : ℚ
⊢ ↑rx * ↑ry ∈ Set.range Rat.cast
exact ⟨rx * ry, cast_mul rx ry⟩