case inl
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.691467
p : R[X]
hp : Monic p
⊢ leadingCoeff (p * 0) = leadingCoeff 0

case inr
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.691467
p q : R[X]
hp : Monic p
H : q ≠ 0
⊢ leadingCoeff (p * q) = leadingCoeff q
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.691467
p q : R[X]
hp : Monic p
⊢ leadingCoeff (p * q) = leadingCoeff q
rcases eq_or_ne q 0 with (rfl | H)
no goals
case inl
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.691467
p : R[X]
hp : Monic p
⊢ leadingCoeff (p * 0) = leadingCoeff 0
simp
case inr
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.691467
p q : R[X]
hp : Monic p
H : q ≠ 0
⊢ leadingCoeff p * leadingCoeff q ≠ 0
case inr
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.691467
p q : R[X]
hp : Monic p
H : q ≠ 0
⊢ leadingCoeff (p * q) = leadingCoeff q
rw [leadingCoeff_mul', hp.leadingCoeff, one_mul]
no goals
case inr
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.691467
p q : R[X]
hp : Monic p
H : q ≠ 0
⊢ leadingCoeff p * leadingCoeff q ≠ 0
rwa [hp.leadingCoeff, one_mul, Ne.def, leadingCoeff_eq_zero]