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

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

Tactic:
rintro ⟨p, rfl⟩

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

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

Tactic:
exact algebraMap_ne_zero hp

Result:
no goals

Proof state:
K : Type u
inst✝ : Field K
x : RatFunc K
q : K[X]
hq : q ≠ 0
⊢ x.denom ∣ q ↔ ∃ p, 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
q : K[X]
hq : q ≠ 0
⊢ x.denom ∣ q → ∃ p, x = (algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q

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

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

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
p : K[X]
hq : x.denom * p ≠ 0
_hx : x.denom ≠ 0
hp : p ≠ 0
⊢ (algebraMap K[X] (RatFunc K)) p ≠ 0

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

Tactic:
use num x * p

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

Proof state:
case mp.intro
K : Type u
inst✝ : Field K
x : RatFunc K
p : K[X]
hq : x.denom * p ≠ 0
⊢ ∃ p_1, x = (algebraMap K[X] (RatFunc K)) p_1 / (algebraMap K[X] (RatFunc K)) (x.denom * p)

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

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

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

Tactic:
rintro ⟨p, rfl⟩

Result:
case mp.intro
K : Type u
inst✝ : Field K
x : RatFunc K
p : K[X]
hq : x.denom * p ≠ 0
⊢ ∃ p_1, x = (algebraMap K[X] (RatFunc K)) p_1 / (algebraMap K[X] (RatFunc K)) (x.denom * p)

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

Tactic:
exact denom_div_dvd p q

Result:
no goals