| attribute [local simp] Nat.mul_comm Nat.mul_assoc Nat.mul_left_comm | |
| attribute [local simp] Nat.add_assoc Nat.add_comm Nat.add_left_comm | |
| example (w x y z : Nat) (p : Nat → Prop) | |
| (h : p (x * y + z * w * x)) : p (x * w * z + y * x) := by | |
| simp at *; assumption | |
| example (x y z : Nat) (p : Nat → Prop) | |
| (h₁ : p (1 * x + y)) (h₂ : p (x * z * 1)) | |
| : p (y + 0 + x) ∧ p (z * x) := by | |
| simp at * <;> constructor <;> assumption |