Theorem: Smt.Reconstruct.Arith.nonZeroEvenPow (Smt/Reconstruct/Arith/ArithMulSign/Lemmas.lean)

State before:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
⊢ ∀ {k : ℕ} {z : α}, z ≠ 0 → Even k → z ^ k > 0
Tactic:
intros k z h₁ h₂
State after:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
k : ℕ
z : α
h₁ : z ≠ 0
h₂ : Even k
⊢ z ^ k > 0

State before:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
k : ℕ
z : α
h₁ : z ≠ 0
h₂ : Even k
⊢ z ^ k > 0
Tactic:
match lt_trichotomy z 0 with
| Or.inl zNeg => exact powNegEven zNeg h₂
| Or.inr (Or.inl zZero) => rw [zZero] at h₁; simp at h₁
| Or.inr (Or.inr zPos)  => exact powPos zPos
State after:
no goals

State before:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
k : ℕ
z : α
h₁ : z ≠ 0
h₂ : Even k
zNeg : z < 0
⊢ z ^ k > 0
Tactic:
exact powNegEven zNeg h₂
State after:
no goals

State before:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
k : ℕ
z : α
h₁ : z ≠ 0
h₂ : Even k
zZero : z = 0
⊢ z ^ k > 0
Tactic:
rw [zZero] at h₁
State after:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
k : ℕ
z : α
h₁ : 0 ≠ 0
h₂ : Even k
zZero : z = 0
⊢ z ^ k > 0

State before:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
k : ℕ
z : α
h₁ : 0 ≠ 0
h₂ : Even k
zZero : z = 0
⊢ z ^ k > 0
Tactic:
simp at h₁
State after:
no goals

State before:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
k : ℕ
z : α
h₁ : z ≠ 0
h₂ : Even k
zPos : 0 < z
⊢ z ^ k > 0
Tactic:
exact powPos zPos
State after:
no goals