case pos
R : Type u_1
inst✝¹ : Ring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : p = 0
⊢ mirror (p * q) = mirror p * mirror q

case neg
R : Type u_1
inst✝¹ : Ring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
⊢ mirror (p * q) = mirror p * mirror q
R : Type u_1
inst✝¹ : Ring R
p q : R[X]
inst✝ : NoZeroDivisors R
⊢ mirror (p * q) = mirror p * mirror q
by_cases hp : p = 0
case pos
R : Type u_1
inst✝¹ : Ring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : q = 0
⊢ mirror (p * q) = mirror p * mirror q

case neg
R : Type u_1
inst✝¹ : Ring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
⊢ mirror (p * q) = mirror p * mirror q
case neg
R : Type u_1
inst✝¹ : Ring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
⊢ mirror (p * q) = mirror p * mirror q
by_cases hq : q = 0
case neg
R : Type u_1
inst✝¹ : Ring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
⊢ reverse p * reverse q * (X ^ natTrailingDegree p * X ^ natTrailingDegree q) =
    reverse p * X ^ natTrailingDegree p * (reverse q * X ^ natTrailingDegree q)
case neg
R : Type u_1
inst✝¹ : Ring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
⊢ mirror (p * q) = mirror p * mirror q
rw [mirror, mirror, mirror, reverse_mul_of_domain, natTrailingDegree_mul hp hq, pow_add]
case neg
R : Type u_1
inst✝¹ : Ring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
⊢ reverse p * (X ^ natTrailingDegree p * reverse q * X ^ natTrailingDegree q) =
    reverse p * X ^ natTrailingDegree p * (reverse q * X ^ natTrailingDegree q)
case neg
R : Type u_1
inst✝¹ : Ring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
⊢ reverse p * reverse q * (X ^ natTrailingDegree p * X ^ natTrailingDegree q) =
    reverse p * X ^ natTrailingDegree p * (reverse q * X ^ natTrailingDegree q)
rw [mul_assoc, ← mul_assoc q.reverse, ← X_pow_mul (p := reverse q)]
no goals
case neg
R : Type u_1
inst✝¹ : Ring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
⊢ reverse p * (X ^ natTrailingDegree p * reverse q * X ^ natTrailingDegree q) =
    reverse p * X ^ natTrailingDegree p * (reverse q * X ^ natTrailingDegree q)
repeat' rw [mul_assoc]
no goals
case pos
R : Type u_1
inst✝¹ : Ring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : p = 0
⊢ mirror (p * q) = mirror p * mirror q
rw [hp, MulZeroClass.zero_mul, mirror_zero, MulZeroClass.zero_mul]
no goals
case pos
R : Type u_1
inst✝¹ : Ring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : q = 0
⊢ mirror (p * q) = mirror p * mirror q
rw [hq, MulZeroClass.mul_zero, mirror_zero, MulZeroClass.mul_zero]
no goals
case neg
R : Type u_1
inst✝¹ : Ring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
⊢ reverse p * (X ^ natTrailingDegree p * (reverse q * X ^ natTrailingDegree q)) =
    reverse p * X ^ natTrailingDegree p * (reverse q * X ^ natTrailingDegree q)
rw [mul_assoc]