Theorem: Array.isEmpty_iff (RegexCorrectness/Data/Array.lean)

State before:
α : Type u_1
a : Array α
⊢ a.isEmpty = true ↔ a = #[]
Tactic:
simp [Array.isEmpty]
State after:
α : Type u_1
a : Array α
⊢ a.data = [] ↔ a = #[]

State before:
α : Type u_1
a : Array α
⊢ a.data = [] ↔ a = #[]
Tactic:
apply Iff.intro
State after:
case mp
α : Type u_1
a : Array α
⊢ a.data = [] → a = #[]

case mpr
α : Type u_1
a : Array α
⊢ a = #[] → a.data = []

State before:
case mp
α : Type u_1
a : Array α
⊢ a.data = [] → a = #[]

case mpr
α : Type u_1
a : Array α
⊢ a = #[] → a.data = []
Tactic:
. exact ext'
State after:
case mpr
α : Type u_1
a : Array α
⊢ a = #[] → a.data = []

State before:
case mpr
α : Type u_1
a : Array α
⊢ a = #[] → a.data = []
Tactic:
. intro h
  simp [h]
State after:
no goals

State before:
case mp
α : Type u_1
a : Array α
⊢ a.data = [] → a = #[]
Tactic:
exact ext'
State after:
no goals

State before:
case mpr
α : Type u_1
a : Array α
⊢ a = #[] → a.data = []
Tactic:
intro h
State after:
case mpr
α : Type u_1
a : Array α
h : a = #[]
⊢ a.data = []

State before:
case mpr
α : Type u_1
a : Array α
h : a = #[]
⊢ a.data = []
Tactic:
simp [h]
State after:
no goals