Theorem: ℕplus.mul_def (meetings/ex6.lean)

State before:
a b : ℕplus
⊢ ↑a * ↑b ≠ 0
Tactic:
simp only [ne_eq, mul_eq_zero, not_or]
State after:
a b : ℕplus
⊢ ¬↑a = 0 ∧ ¬↑b = 0

State before:
a b : ℕplus
⊢ ¬↑a = 0 ∧ ¬↑b = 0
Tactic:
exact ⟨a.property, b.property⟩
State after:
no goals