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

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

State before:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
k : ℕ
z : α
h : z > 0
⊢ z ^ k > 0
Tactic:
cases k with
| zero    => simp
| succ k' =>
  have ih := @powPos k' z h
  rw [pow_succ]
  have h₂ := arith_mul_pos_lt ⟨h, ih⟩
  simp at h₂
  rw [mul_comm]
  exact h₂
State after:
no goals

State before:
case zero
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h : z > 0
⊢ z ^ 0 > 0
Tactic:
simp
State after:
no goals

State before:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h : z > 0
k' : ℕ
⊢ z ^ (k' + 1) > 0
Tactic:
have ih := @powPos k' z h
State after:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h : z > 0
k' : ℕ
ih : z ^ k' > 0
⊢ z ^ (k' + 1) > 0

State before:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h : z > 0
k' : ℕ
ih : z ^ k' > 0
⊢ z ^ (k' + 1) > 0
Tactic:
rw [pow_succ]
State after:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h : z > 0
k' : ℕ
ih : z ^ k' > 0
⊢ z ^ k' * z > 0

State before:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h : z > 0
k' : ℕ
ih : z ^ k' > 0
⊢ z ^ k' * z > 0
Tactic:
have h₂ := arith_mul_pos_lt ⟨h, ih⟩
State after:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h : z > 0
k' : ℕ
ih : z ^ k' > 0
h₂ : z * 0 < z * z ^ k'
⊢ z ^ k' * z > 0

State before:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h : z > 0
k' : ℕ
ih : z ^ k' > 0
h₂ : z * 0 < z * z ^ k'
⊢ z ^ k' * z > 0
Tactic:
simp at h₂
State after:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h : z > 0
k' : ℕ
ih : z ^ k' > 0
h₂ : 0 < z * z ^ k'
⊢ z ^ k' * z > 0

State before:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h : z > 0
k' : ℕ
ih : z ^ k' > 0
h₂ : 0 < z * z ^ k'
⊢ z ^ k' * z > 0
Tactic:
rw [mul_comm]
State after:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h : z > 0
k' : ℕ
ih : z ^ k' > 0
h₂ : 0 < z * z ^ k'
⊢ z * z ^ k' > 0

State before:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h : z > 0
k' : ℕ
ih : z ^ k' > 0
h₂ : 0 < z * z ^ k'
⊢ z * z ^ k' > 0
Tactic:
exact h₂
State after:
no goals