Theorem: Nat.nonzero_iff_gt_zero (MLIR/Util/KDTensor.lean)

State before:
⊢ ∀ (n : ℕ), n ≠ 0 ↔ n > 0
Tactic:
intros n
State after:
n : ℕ
⊢ n ≠ 0 ↔ n > 0

State before:
n : ℕ
⊢ n ≠ 0 ↔ n > 0
Tactic:
constructor
State after:
case mp
n : ℕ
⊢ n ≠ 0 → n > 0

case mpr
n : ℕ
⊢ n > 0 → n ≠ 0

State before:
n : ℕ
⊢ n ≠ 0 → n > 0
Tactic:
case mp => {
intros NEQ_0;
cases n;
case zero => {
  contradiction;
}
case succ n' => { simp [Nat.succ_gt_zero]; }
}
State after:
no goals

State before:
n : ℕ
⊢ n > 0 → n ≠ 0
Tactic:
case mpr => {
 intros GT_ZERO;
 cases n;
 case zero => {
   simp at GT_ZERO;
 }
 case succ n' => { simp; }
}
State after:
no goals

State before:
n : ℕ
⊢ n ≠ 0 → n > 0
Tactic:
intros NEQ_0
State after:
n : ℕ
NEQ_0 : n ≠ 0
⊢ n > 0

State before:
n : ℕ
NEQ_0 : n ≠ 0
⊢ n > 0
Tactic:
cases n
State after:
case zero
NEQ_0 : zero ≠ 0
⊢ zero > 0

case succ
n✝ : ℕ
NEQ_0 : succ n✝ ≠ 0
⊢ succ n✝ > 0

State before:
NEQ_0 : zero ≠ 0
⊢ zero > 0
Tactic:
case zero => {
  contradiction;
}
State after:
no goals

State before:
n' : ℕ
NEQ_0 : succ n' ≠ 0
⊢ succ n' > 0
Tactic:
case succ n' => { simp [Nat.succ_gt_zero]; }
State after:
no goals

State before:
NEQ_0 : zero ≠ 0
⊢ zero > 0
Tactic:
contradiction
State after:
no goals

State before:
n' : ℕ
NEQ_0 : succ n' ≠ 0
⊢ succ n' > 0
Tactic:
simp [Nat.succ_gt_zero]
State after:
no goals

State before:
n : ℕ
⊢ n > 0 → n ≠ 0
Tactic:
intros GT_ZERO
State after:
n : ℕ
GT_ZERO : n > 0
⊢ n ≠ 0

State before:
n : ℕ
GT_ZERO : n > 0
⊢ n ≠ 0
Tactic:
cases n
State after:
case zero
GT_ZERO : zero > 0
⊢ zero ≠ 0

case succ
n✝ : ℕ
GT_ZERO : succ n✝ > 0
⊢ succ n✝ ≠ 0

State before:
GT_ZERO : zero > 0
⊢ zero ≠ 0
Tactic:
case zero => {
  simp at GT_ZERO;
}
State after:
no goals

State before:
n' : ℕ
GT_ZERO : succ n' > 0
⊢ succ n' ≠ 0
Tactic:
case succ n' => { simp; }
State after:
no goals

State before:
GT_ZERO : zero > 0
⊢ zero ≠ 0
Tactic:
simp at GT_ZERO
State after:
no goals

State before:
n' : ℕ
GT_ZERO : succ n' > 0
⊢ succ n' ≠ 0
Tactic:
simp
State after:
no goals