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

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

State before:
i₁ i₂ j₁ j₂ : Int
⊢ i₁ + (i₂ + (j₁ + j₂)) = i₁ + (j₁ + (i₂ + j₂))
Tactic:
rw [Int.add_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.add_assoc]
State after:
no goals