Theorem: Array.lt_size_of_pop_of_not_empty (Regex/Data/Array.lean)

State before:
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
⊢ a.pop.size < a.size
Tactic:
have : 0 < a.size := zero_lt_size_of_not_empty hemp
State after:
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
⊢ a.pop.size < a.size

State before:
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
⊢ a.pop.size < a.size
Tactic:
have : a.size - 1 < a.size := Nat.sub_lt_of_pos_le (by decide) this
State after:
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this✝ : 0 < a.size
this : a.size - 1 < a.size
⊢ a.pop.size < a.size

State before:
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this✝ : 0 < a.size
this : a.size - 1 < a.size
⊢ a.pop.size < a.size
Tactic:
simp [Array.pop]
State after:
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this✝ : 0 < a.size
this : a.size - 1 < a.size
⊢ a.size - 1 < a.size

State before:
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this✝ : 0 < a.size
this : a.size - 1 < a.size
⊢ a.size - 1 < a.size
Tactic:
exact this
State after:
no goals

State before:
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
⊢ 0 < 1
Tactic:
decide
State after:
no goals