case f
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
⊢ ↑(algebraMap K[X] (RatFunc K)) (num (↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q)) /
      ↑(algebraMap K[X] (RatFunc K)) (denom (↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q)) =
    ↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q
K : Type u
inst✝ : Field K
x : RatFunc K
⊢ ↑(algebraMap K[X] (RatFunc K)) (num x) / ↑(algebraMap K[X] (RatFunc K)) (denom x) = x
induction' x using RatFunc.induction_on with p q hq
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)) (num (↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q)) /
      ↑(algebraMap K[X] (RatFunc K)) (denom (↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q)) =
    ↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q
case f
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
⊢ ↑(algebraMap K[X] (RatFunc K)) (num (↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q)) /
      ↑(algebraMap K[X] (RatFunc K)) (denom (↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q)) =
    ↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q
have q_div_ne_zero : q / gcd p q ≠ 0 := right_div_gcd_ne_zero hq
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)) (num (↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q)) /
      ↑(algebraMap K[X] (RatFunc K)) (denom (↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q)) =
    ↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q
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)) (num (↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q)) /
      ↑(algebraMap K[X] (RatFunc K)) (denom (↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q)) =
    ↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q
dsimp only
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 (leadingCoeff (q / gcd p q))⁻¹) ≠ 0
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)) (num (↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q)) /
      ↑(algebraMap K[X] (RatFunc K)) (denom (↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q)) =
    ↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q
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]
no goals
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
apply gcd_dvd_right
no goals
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
apply gcd_dvd_left
no goals
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
exact algebraMap_ne_zero q_div_ne_zero
no goals
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
exact algebraMap_ne_zero hq
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
⊢ ¬(leadingCoeff (q / gcd p 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 (leadingCoeff (q / gcd p q))⁻¹) ≠ 0
refine' algebraMap_ne_zero (mt Polynomial.C_eq_zero.mp _)
no goals
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
⊢ ¬(leadingCoeff (q / gcd p q))⁻¹ = 0
exact inv_ne_zero (Polynomial.leadingCoeff_ne_zero.mpr q_div_ne_zero)