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

State before:
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
⊢ 0 < a.size
Tactic:
apply Nat.zero_lt_of_ne_zero
State after:
case h
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
⊢ a.size ≠ 0

State before:
case h
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
⊢ a.size ≠ 0
Tactic:
intro heq
State after:
case h
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
heq : a.size = 0
⊢ False

State before:
case h
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
heq : a.size = 0
⊢ False
Tactic:
have : a = #[] := eq_empty_of_size_eq_zero heq
State after:
case h
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
heq : a.size = 0
this : a = #[]
⊢ False

State before:
case h
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
heq : a.size = 0
this : a = #[]
⊢ False
Tactic:
simp [this] at hemp
State after:
no goals