case f0
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
⊢ ∀ (p : K[X]),
    (if 0 = 0 then (0, 1)
      else
        let r := gcd p 0;
        (↑C (leadingCoeff (0 / r))⁻¹ * (p / r), ↑C (leadingCoeff (0 / r))⁻¹ * (0 / r))) =
      if 1 = 0 then (0, 1)
      else
        let r := gcd 0 1;
        (↑C (leadingCoeff (1 / r))⁻¹ * (0 / r), ↑C (leadingCoeff (1 / r))⁻¹ * (1 / r))
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
⊢ numDenom (↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q) =
    (↑C (leadingCoeff (q / gcd p q))⁻¹ * (p / gcd p q), ↑C (leadingCoeff (q / gcd p q))⁻¹ * (q / gcd p q))
rw [numDenom, liftOn'_div, if_neg hq]
case f0
K : Type u
inst✝ : Field K
p✝ q : K[X]
hq : q ≠ 0
p : K[X]
⊢ (if 0 = 0 then (0, 1)
    else
      let r := gcd p 0;
      (↑C (leadingCoeff (0 / r))⁻¹ * (p / r), ↑C (leadingCoeff (0 / r))⁻¹ * (0 / r))) =
    if 1 = 0 then (0, 1)
    else
      let r := gcd 0 1;
      (↑C (leadingCoeff (1 / r))⁻¹ * (0 / r), ↑C (leadingCoeff (1 / r))⁻¹ * (1 / r))
case f0
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
⊢ ∀ (p : K[X]),
    (if 0 = 0 then (0, 1)
      else
        let r := gcd p 0;
        (↑C (leadingCoeff (0 / r))⁻¹ * (p / r), ↑C (leadingCoeff (0 / r))⁻¹ * (0 / r))) =
      if 1 = 0 then (0, 1)
      else
        let r := gcd 0 1;
        (↑C (leadingCoeff (1 / r))⁻¹ * (0 / r), ↑C (leadingCoeff (1 / r))⁻¹ * (1 / r))
intro p
case f0
K : Type u
inst✝ : Field K
p✝ q : K[X]
hq : q ≠ 0
p : K[X]
⊢ (0, 1) =
    let r := gcd 0 1;
    (↑C (leadingCoeff (1 / r))⁻¹ * (0 / r), ↑C (leadingCoeff (1 / r))⁻¹ * (1 / r))
case f0
K : Type u
inst✝ : Field K
p✝ q : K[X]
hq : q ≠ 0
p : K[X]
⊢ (if 0 = 0 then (0, 1)
    else
      let r := gcd p 0;
      (↑C (leadingCoeff (0 / r))⁻¹ * (p / r), ↑C (leadingCoeff (0 / r))⁻¹ * (0 / r))) =
    if 1 = 0 then (0, 1)
    else
      let r := gcd 0 1;
      (↑C (leadingCoeff (1 / r))⁻¹ * (0 / r), ↑C (leadingCoeff (1 / r))⁻¹ * (1 / r))
rw [if_pos rfl, if_neg (one_ne_zero' K[X])]
no goals
case f0
K : Type u
inst✝ : Field K
p✝ q : K[X]
hq : q ≠ 0
p : K[X]
⊢ (0, 1) =
    let r := gcd 0 1;
    (↑C (leadingCoeff (1 / r))⁻¹ * (0 / r), ↑C (leadingCoeff (1 / r))⁻¹ * (1 / r))
simp