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

State before:
n : ℤ
m : ℕ
⊢ n > 0 → n ^ m > 0
Tactic:
revert n
State after:
m : ℕ
⊢ ∀ (n : ℤ), n > 0 → n ^ m > 0

State before:
m : ℕ
⊢ ∀ (n : ℤ), n > 0 → n ^ m > 0
Tactic:
induction m <;> intros n h <;> simp
State after:
case succ
n✝ : ℕ
n_ih✝ : ∀ (n : ℤ), n > 0 → n ^ n✝ > 0
n : ℤ
h : n > 0
⊢ 0 < n ^ Nat.succ n✝

State before:
acc : ℕ
ih : ∀ (n : ℤ), n > 0 → n ^ acc > 0
n : ℤ
h : n > 0
⊢ 0 < n ^ Nat.succ acc
Tactic:
case succ acc ih =>
  simp [pow_succ]; apply mul_gt_zero (ih _ h) h
State after:
no goals

State before:
acc : ℕ
ih : ∀ (n : ℤ), n > 0 → n ^ acc > 0
n : ℤ
h : n > 0
⊢ 0 < n ^ Nat.succ acc
Tactic:
simp [pow_succ]
State after:
acc : ℕ
ih : ∀ (n : ℤ), n > 0 → n ^ acc > 0
n : ℤ
h : n > 0
⊢ 0 < n ^ acc * n

State before:
acc : ℕ
ih : ∀ (n : ℤ), n > 0 → n ^ acc > 0
n : ℤ
h : n > 0
⊢ 0 < n ^ acc * n
Tactic:
apply mul_gt_zero (ih _ h) h
State after:
no goals