case mp
K : Type u
inst✝ : Field K
x : RatFunc K
p : K[X]
hp : p ≠ 0
⊢ num x ∣ p → ∃ q hq, x = ↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q

case mpr
K : Type u
inst✝ : Field K
x : RatFunc K
p : K[X]
hp : p ≠ 0
⊢ (∃ q hq, x = ↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q) → num x ∣ p
K : Type u
inst✝ : Field K
x : RatFunc K
p : K[X]
hp : p ≠ 0
⊢ num x ∣ p ↔ ∃ q hq, x = ↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q
constructor
case mp.intro
K : Type u
inst✝ : Field K
x : RatFunc K
q : K[X]
hp : num x * q ≠ 0
⊢ ∃ q_1 hq, x = ↑(algebraMap K[X] (RatFunc K)) (num x * q) / ↑(algebraMap K[X] (RatFunc K)) q_1
case mp
K : Type u
inst✝ : Field K
x : RatFunc K
p : K[X]
hp : p ≠ 0
⊢ num x ∣ p → ∃ q hq, x = ↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q
rintro ⟨q, rfl⟩
case mp.intro.intro
K : Type u
inst✝ : Field K
x : RatFunc K
q : K[X]
hp : num x * q ≠ 0
_hx : num x ≠ 0
hq : q ≠ 0
⊢ ∃ q_1 hq, x = ↑(algebraMap K[X] (RatFunc K)) (num x * q) / ↑(algebraMap K[X] (RatFunc K)) q_1
case mp.intro
K : Type u
inst✝ : Field K
x : RatFunc K
q : K[X]
hp : num x * q ≠ 0
⊢ ∃ q_1 hq, x = ↑(algebraMap K[X] (RatFunc K)) (num x * q) / ↑(algebraMap K[X] (RatFunc K)) q_1
obtain ⟨_hx, hq⟩ := mul_ne_zero_iff.mp hp
case mp.intro.intro
K : Type u
inst✝ : Field K
x : RatFunc K
q : K[X]
hp : num x * q ≠ 0
_hx : num x ≠ 0
hq : q ≠ 0
⊢ ∃ hq, x = ↑(algebraMap K[X] (RatFunc K)) (num x * q) / ↑(algebraMap K[X] (RatFunc K)) (denom x * q)
case mp.intro.intro
K : Type u
inst✝ : Field K
x : RatFunc K
q : K[X]
hp : num x * q ≠ 0
_hx : num x ≠ 0
hq : q ≠ 0
⊢ ∃ q_1 hq, x = ↑(algebraMap K[X] (RatFunc K)) (num x * q) / ↑(algebraMap K[X] (RatFunc K)) q_1
use denom x * q
case mp.intro.intro
K : Type u
inst✝ : Field K
x : RatFunc K
q : K[X]
hp : num x * q ≠ 0
_hx : num x ≠ 0
hq : q ≠ 0
⊢ ∃ hq, x = x

case mp.intro.intro
K : Type u
inst✝ : Field K
x : RatFunc K
q : K[X]
hp : num x * q ≠ 0
_hx : num x ≠ 0
hq : q ≠ 0
⊢ ↑(algebraMap K[X] (RatFunc K)) q ≠ 0
case mp.intro.intro
K : Type u
inst✝ : Field K
x : RatFunc K
q : K[X]
hp : num x * q ≠ 0
_hx : num x ≠ 0
hq : q ≠ 0
⊢ ∃ hq, x = ↑(algebraMap K[X] (RatFunc K)) (num x * q) / ↑(algebraMap K[X] (RatFunc K)) (denom x * q)
rw [RingHom.map_mul, RingHom.map_mul, ← div_mul_div_comm, div_self, mul_one, num_div_denom]
no goals
case mp.intro.intro
K : Type u
inst✝ : Field K
x : RatFunc K
q : K[X]
hp : num x * q ≠ 0
_hx : num x ≠ 0
hq : q ≠ 0
⊢ ∃ hq, x = x
exact ⟨mul_ne_zero (denom_ne_zero x) hq, rfl⟩
no goals
case mp.intro.intro
K : Type u
inst✝ : Field K
x : RatFunc K
q : K[X]
hp : num x * q ≠ 0
_hx : num x ≠ 0
hq : q ≠ 0
⊢ ↑(algebraMap K[X] (RatFunc K)) q ≠ 0
exact algebraMap_ne_zero hq
case mpr.intro.intro
K : Type u
inst✝ : Field K
p : K[X]
hp : p ≠ 0
q : K[X]
hq : q ≠ 0
⊢ num (↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q) ∣ p
case mpr
K : Type u
inst✝ : Field K
x : RatFunc K
p : K[X]
hp : p ≠ 0
⊢ (∃ q hq, x = ↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q) → num x ∣ p
rintro ⟨q, hq, rfl⟩
no goals
case mpr.intro.intro
K : Type u
inst✝ : Field K
p : K[X]
hp : p ≠ 0
q : K[X]
hq : q ≠ 0
⊢ num (↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q) ∣ p
exact num_div_dvd p hq