-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem num_div_denom (x : RatFunc K) : algebraMap _ _ (num x) / algebraMap _ _ (denom x) = x

Proof state:
case f.hc
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
q_div_ne_zero : q / gcd p q ≠ 0
⊢ (algebraMap K[X] (RatFunc K)) (C (q / gcd p q).leadingCoeff⁻¹) ≠ 0

Tactic:
refine algebraMap_ne_zero (mt Polynomial.C_eq_zero.mp ?_)

Result:
case f.hc
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
q_div_ne_zero : q / gcd p q ≠ 0
⊢ ¬(q / gcd p q).leadingCoeff⁻¹ = 0

Proof state:
case f.h
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
q_div_ne_zero : q / gcd p q ≠ 0
⊢ gcd p q ∣ p

Tactic:
apply gcd_dvd_left

Result:
no goals

Proof state:
case f.hb
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
q_div_ne_zero : q / gcd p q ≠ 0
⊢ (algebraMap K[X] (RatFunc K)) (q / gcd p q) ≠ 0

Tactic:
exact algebraMap_ne_zero q_div_ne_zero

Result:
no goals

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

Tactic:
have q_div_ne_zero : q / gcd p q ≠ 0 := right_div_gcd_ne_zero hq

Result:
case f
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
q_div_ne_zero : q / gcd p q ≠ 0
⊢ (algebraMap K[X] (RatFunc K)) ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q).num /
      (algebraMap K[X] (RatFunc K)) ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q).denom =
    (algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q

Proof state:
K : Type u
inst✝ : Field K
x : RatFunc K
⊢ (algebraMap K[X] (RatFunc K)) x.num / (algebraMap K[X] (RatFunc K)) x.denom = x

Tactic:
induction' x using RatFunc.induction_on with p q hq

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

Proof state:
case f.h
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
q_div_ne_zero : q / gcd p q ≠ 0
⊢ gcd p q ∣ q

Tactic:
apply gcd_dvd_right

Result:
no goals

Proof state:
case f.hd
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
q_div_ne_zero : q / gcd p q ≠ 0
⊢ (algebraMap K[X] (RatFunc K)) q ≠ 0

Tactic:
exact algebraMap_ne_zero hq

Result:
no goals

Proof state:
case f
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
q_div_ne_zero : q / gcd p q ≠ 0
⊢ (algebraMap K[X] (RatFunc K)) ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q).num /
      (algebraMap K[X] (RatFunc K)) ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q).denom =
    (algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q

Tactic:
rw [num_div p q, denom_div p hq, RingHom.map_mul, RingHom.map_mul, mul_div_mul_left,
  div_eq_div_iff, ← RingHom.map_mul, ← RingHom.map_mul, mul_comm _ q, ←
  EuclideanDomain.mul_div_assoc, ← EuclideanDomain.mul_div_assoc, mul_comm]

Result:
case f.h
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
q_div_ne_zero : q / gcd p q ≠ 0
⊢ gcd p q ∣ q

case f.h
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
q_div_ne_zero : q / gcd p q ≠ 0
⊢ gcd p q ∣ p

case f.hb
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
q_div_ne_zero : q / gcd p q ≠ 0
⊢ (algebraMap K[X] (RatFunc K)) (q / gcd p q) ≠ 0

case f.hd
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
q_div_ne_zero : q / gcd p q ≠ 0
⊢ (algebraMap K[X] (RatFunc K)) q ≠ 0

case f.hc
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
q_div_ne_zero : q / gcd p q ≠ 0
⊢ (algebraMap K[X] (RatFunc K)) (C (q / gcd p q).leadingCoeff⁻¹) ≠ 0

Proof state:
case f.hc
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
q_div_ne_zero : q / gcd p q ≠ 0
⊢ ¬(q / gcd p q).leadingCoeff⁻¹ = 0

Tactic:
exact inv_ne_zero (Polynomial.leadingCoeff_ne_zero.mpr q_div_ne_zero)

Result:
no goals