Theorem: inversions_mul (Bruhat/Goal.lean)

State before:
f g : Equiv.Perm ℕ
⊢ Inversions (f * g) = Prod.map ⇑g.symm ⇑g.symm '' Inversions f ∩ Inversions g
Tactic:
sorry
State after:
no goals