Theorem: Nat.and_pos_iff (Logic/Vorspiel/Arith.lean)

State before:
n m : ℕ
⊢ 0 < n.and m ↔ 0 < n ∧ 0 < m
Tactic:
simp[and_eq]
State after:
n m : ℕ
⊢ (0 < if 0 < n ∧ 0 < m then 1 else 0) ↔ 0 < n ∧ 0 < m

State before:
n m : ℕ
⊢ (0 < if 0 < n ∧ 0 < m then 1 else 0) ↔ 0 < n ∧ 0 < m
Tactic:
by_cases 0 < n ∧ 0 < m <;> simp[*]
State after:
no goals