case pos
R✝ : Type ?u.361245
inst✝² : Semiring R✝
f✝ : R✝[X]
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
f g : R[X]
f0 : f = 0
⊢ reverse (f * g) = reverse f * reverse g

case neg
R✝ : Type ?u.361245
inst✝² : Semiring R✝
f✝ : R✝[X]
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
f g : R[X]
f0 : ¬f = 0
⊢ reverse (f * g) = reverse f * reverse g
R✝ : Type ?u.361245
inst✝² : Semiring R✝
f✝ : R✝[X]
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
f g : R[X]
⊢ reverse (f * g) = reverse f * reverse g
by_cases f0 : f = 0
case pos
R✝ : Type ?u.361245
inst✝² : Semiring R✝
f✝ : R✝[X]
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
f g : R[X]
f0 : ¬f = 0
g0 : g = 0
⊢ reverse (f * g) = reverse f * reverse g

case neg
R✝ : Type ?u.361245
inst✝² : Semiring R✝
f✝ : R✝[X]
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
f g : R[X]
f0 : ¬f = 0
g0 : ¬g = 0
⊢ reverse (f * g) = reverse f * reverse g
case neg
R✝ : Type ?u.361245
inst✝² : Semiring R✝
f✝ : R✝[X]
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
f g : R[X]
f0 : ¬f = 0
⊢ reverse (f * g) = reverse f * reverse g
by_cases g0 : g = 0
no goals
case neg
R✝ : Type ?u.361245
inst✝² : Semiring R✝
f✝ : R✝[X]
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
f g : R[X]
f0 : ¬f = 0
g0 : ¬g = 0
⊢ reverse (f * g) = reverse f * reverse g
simp [reverse_mul, *]
no goals
case pos
R✝ : Type ?u.361245
inst✝² : Semiring R✝
f✝ : R✝[X]
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
f g : R[X]
f0 : f = 0
⊢ reverse (f * g) = reverse f * reverse g
simp only [f0, zero_mul, reverse_zero]
no goals
case pos
R✝ : Type ?u.361245
inst✝² : Semiring R✝
f✝ : R✝[X]
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
f g : R[X]
f0 : ¬f = 0
g0 : g = 0
⊢ reverse (f * g) = reverse f * reverse g
rw [g0, mul_zero, reverse_zero, mul_zero]