Theorem: Measurable.square (Ray/Hartogs/FubiniBall.lean)

State before:
r0 r1 : ℝ
⊢ MeasurableSet (_root_.square r0 r1)
Tactic:
apply_rules [MeasurableSet.prod, measurableSet_Ioc]
State after:
no goals