Theorem: Finset.mul_prod_Iio (LeanCamCombi/Mathlib/Algebra/Order/BigOperators/LocallyFinite.lean)

State before:
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : CommMonoid β
f : α → β
a✝ b : α
inst✝ : LocallyFiniteOrderBot α
a : α
⊢ f a * ∏ x ∈ Iio a, f x = ∏ x ∈ Iic a, f x
Tactic:
rw [Iic_eq_cons_Iio, prod_cons]
State after:
no goals