case pos
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
ha : a = 0
⊢ p / (↑C a * q) = ↑C a⁻¹ * (p / q)

case neg
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
ha : ¬a = 0
⊢ p / (↑C a * q) = ↑C a⁻¹ * (p / q)
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
⊢ p / (↑C a * q) = ↑C a⁻¹ * (p / q)
by_cases ha : a = 0
case neg
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
ha : ¬a = 0
⊢ ↑C a⁻¹ * (↑C (leadingCoeff q)⁻¹ * (p /ₘ (↑C a * (q * (↑C a⁻¹ * ↑C (leadingCoeff q)⁻¹))))) =
    ↑C a⁻¹ * (↑C (leadingCoeff q)⁻¹ * (p /ₘ (q * ↑C (leadingCoeff q)⁻¹)))
case neg
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
ha : ¬a = 0
⊢ p / (↑C a * q) = ↑C a⁻¹ * (p / q)
simp only [div_def, leadingCoeff_mul, mul_inv, leadingCoeff_C, C.map_mul, mul_assoc]
case neg.e_a.e_a.e_q
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
ha : ¬a = 0
⊢ ↑C a * (q * (↑C a⁻¹ * ↑C (leadingCoeff q)⁻¹)) = q * ↑C (leadingCoeff q)⁻¹
case neg
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
ha : ¬a = 0
⊢ ↑C a⁻¹ * (↑C (leadingCoeff q)⁻¹ * (p /ₘ (↑C a * (q * (↑C a⁻¹ * ↑C (leadingCoeff q)⁻¹))))) =
    ↑C a⁻¹ * (↑C (leadingCoeff q)⁻¹ * (p /ₘ (q * ↑C (leadingCoeff q)⁻¹)))
congr 3
no goals
case neg.e_a.e_a.e_q
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
ha : ¬a = 0
⊢ ↑C a * (q * (↑C a⁻¹ * ↑C (leadingCoeff q)⁻¹)) = q * ↑C (leadingCoeff q)⁻¹
rw [mul_left_comm q, ← mul_assoc, ← C.map_mul, mul_inv_cancel ha, C.map_one, one_mul]
no goals
case pos
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
ha : a = 0
⊢ p / (↑C a * q) = ↑C a⁻¹ * (p / q)
simp [ha]