Theorem: Int.mul_two (MLIR/Util/Arith.lean)

State before:
n : ℤ
⊢ n * 2 = n + n
Tactic:
have h: (2:Int) = 1 + 1 := rfl
State after:
n : ℤ
h : 2 = 1 + 1
⊢ n * 2 = n + n

State before:
n : ℤ
h : 2 = 1 + 1
⊢ n * 2 = n + n
Tactic:
rw [h]
State after:
n : ℤ
h : 2 = 1 + 1
⊢ n * (1 + 1) = n + n

State before:
n : ℤ
h : 2 = 1 + 1
⊢ n * (1 + 1) = n + n
Tactic:
rw [Int.mul_add]
State after:
n : ℤ
h : 2 = 1 + 1
⊢ n * 1 + n * 1 = n + n

State before:
n : ℤ
h : 2 = 1 + 1
⊢ n * 1 + n * 1 = n + n
Tactic:
simp [Int.mul_one]
State after:
no goals