Theorem: Int.mul_mul_mul_comm (Extra/Int/Lemmas.lean)

State before:
i₁ i₂ j₁ j₂ : Int
⊢ i₁ * i₂ * (j₁ * j₂) = i₁ * (i₂ * (j₁ * j₂))
Tactic:
rw [Int.mul_assoc]
State after:
no goals

State before:
i₁ i₂ j₁ j₂ : Int
⊢ i₁ * (i₂ * (j₁ * j₂)) = i₁ * (j₁ * (i₂ * j₂))
Tactic:
rw [Int.mul_left_comm i₂ j₁ j₂]
State after:
no goals

State before:
i₁ i₂ j₁ j₂ : Int
⊢ i₁ * (j₁ * (i₂ * j₂)) = i₁ * j₁ * (i₂ * j₂)
Tactic:
rw [Int.mul_assoc]
State after:
no goals