-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem num_dvd {x : RatFunc K} {p : K[X]} (hp : p ≠ 0) :
    num x ∣ p ↔ ∃ q : K[X], q ≠ 0 ∧ x = algebraMap _ _ p / algebraMap _ _ q

Proof state:
case h
K : Type u
inst✝ : Field K
x : RatFunc K
q : K[X]
hp : x.num * q ≠ 0
_hx : x.num ≠ 0
hq : q ≠ 0
⊢ x.denom * q ≠ 0 ∧ x = (algebraMap K[X] (RatFunc K)) (x.num * q) / (algebraMap K[X] (RatFunc K)) (x.denom * q)

Tactic:
rw [RingHom.map_mul, RingHom.map_mul, ← div_mul_div_comm, div_self, mul_one, num_div_denom]

Result:
case h
K : Type u
inst✝ : Field K
x : RatFunc K
q : K[X]
hp : x.num * q ≠ 0
_hx : x.num ≠ 0
hq : q ≠ 0
⊢ x.denom * q ≠ 0 ∧ x = x

case h
K : Type u
inst✝ : Field K
x : RatFunc K
q : K[X]
hp : x.num * q ≠ 0
_hx : x.num ≠ 0
hq : q ≠ 0
⊢ (algebraMap K[X] (RatFunc K)) q ≠ 0

Proof state:
K : Type u
inst✝ : Field K
x : RatFunc K
p : K[X]
hp : p ≠ 0
⊢ x.num ∣ p ↔ ∃ q, q ≠ 0 ∧ x = (algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q

Tactic:
constructor

Result:
case mp
K : Type u
inst✝ : Field K
x : RatFunc K
p : K[X]
hp : p ≠ 0
⊢ x.num ∣ p → ∃ q, q ≠ 0 ∧ 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, q ≠ 0 ∧ x = (algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q) → x.num ∣ p

Proof state:
case mp.intro
K : Type u
inst✝ : Field K
x : RatFunc K
q : K[X]
hp : x.num * q ≠ 0
⊢ ∃ q_1, q_1 ≠ 0 ∧ x = (algebraMap K[X] (RatFunc K)) (x.num * q) / (algebraMap K[X] (RatFunc K)) q_1

Tactic:
obtain ⟨_hx, hq⟩ := mul_ne_zero_iff.mp hp

Result:
case mp.intro.intro
K : Type u
inst✝ : Field K
x : RatFunc K
q : K[X]
hp : x.num * q ≠ 0
_hx : x.num ≠ 0
hq : q ≠ 0
⊢ ∃ q_1, q_1 ≠ 0 ∧ x = (algebraMap K[X] (RatFunc K)) (x.num * q) / (algebraMap K[X] (RatFunc K)) q_1

Proof state:
case h
K : Type u
inst✝ : Field K
x : RatFunc K
q : K[X]
hp : x.num * q ≠ 0
_hx : x.num ≠ 0
hq : q ≠ 0
⊢ x.denom * q ≠ 0 ∧ x = x

Tactic:
exact ⟨mul_ne_zero (denom_ne_zero x) hq, rfl⟩

Result:
no goals

Proof state:
case mp.intro.intro
K : Type u
inst✝ : Field K
x : RatFunc K
q : K[X]
hp : x.num * q ≠ 0
_hx : x.num ≠ 0
hq : q ≠ 0
⊢ ∃ q_1, q_1 ≠ 0 ∧ x = (algebraMap K[X] (RatFunc K)) (x.num * q) / (algebraMap K[X] (RatFunc K)) q_1

Tactic:
use denom x * q

Result:
case h
K : Type u
inst✝ : Field K
x : RatFunc K
q : K[X]
hp : x.num * q ≠ 0
_hx : x.num ≠ 0
hq : q ≠ 0
⊢ x.denom * q ≠ 0 ∧ x = (algebraMap K[X] (RatFunc K)) (x.num * q) / (algebraMap K[X] (RatFunc K)) (x.denom * q)

Proof state:
case mpr.intro.intro
K : Type u
inst✝ : Field K
p : K[X]
hp : p ≠ 0
q : K[X]
hq : q ≠ 0
⊢ ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q).num ∣ p

Tactic:
exact num_div_dvd p hq

Result:
no goals

Proof state:
case h
K : Type u
inst✝ : Field K
x : RatFunc K
q : K[X]
hp : x.num * q ≠ 0
_hx : x.num ≠ 0
hq : q ≠ 0
⊢ (algebraMap K[X] (RatFunc K)) q ≠ 0

Tactic:
exact algebraMap_ne_zero hq

Result:
no goals

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

Tactic:
rintro ⟨q, rfl⟩

Result:
case mp.intro
K : Type u
inst✝ : Field K
x : RatFunc K
q : K[X]
hp : x.num * q ≠ 0
⊢ ∃ q_1, q_1 ≠ 0 ∧ x = (algebraMap K[X] (RatFunc K)) (x.num * q) / (algebraMap K[X] (RatFunc K)) q_1

Proof state:
case mpr
K : Type u
inst✝ : Field K
x : RatFunc K
p : K[X]
hp : p ≠ 0
⊢ (∃ q, q ≠ 0 ∧ x = (algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q) → x.num ∣ p

Tactic:
rintro ⟨q, hq, rfl⟩

Result:
case mpr.intro.intro
K : Type u
inst✝ : Field K
p : K[X]
hp : p ≠ 0
q : K[X]
hq : q ≠ 0
⊢ ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q).num ∣ p