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

State before:
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
⊢ a.pop.push (a.back' hemp) = a
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.push (a.back' hemp) = a

State before:
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
⊢ a.pop.push (a.back' hemp) = a
Tactic:
apply Array.ext
State after:
case h₁
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
⊢ (a.pop.push (a.back' hemp)).size = a.size

case h₂
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
⊢ ∀ (i : Nat) (hi₁ : i < (a.pop.push (a.back' hemp)).size) (hi₂ : i < a.size), (a.pop.push (a.back' hemp))[i] = a[i]

State before:
case h₁
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
⊢ (a.pop.push (a.back' hemp)).size = a.size

case h₂
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
⊢ ∀ (i : Nat) (hi₁ : i < (a.pop.push (a.back' hemp)).size) (hi₂ : i < a.size), (a.pop.push (a.back' hemp))[i] = a[i]
Tactic:
. simp [Nat.sub_add_cancel this]
State after:
case h₂
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
⊢ ∀ (i : Nat) (hi₁ : i < (a.pop.push (a.back' hemp)).size) (hi₂ : i < a.size), (a.pop.push (a.back' hemp))[i] = a[i]

State before:
case h₂
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
⊢ ∀ (i : Nat) (hi₁ : i < (a.pop.push (a.back' hemp)).size) (hi₂ : i < a.size), (a.pop.push (a.back' hemp))[i] = a[i]
Tactic:
. simp [Nat.sub_add_cancel this]
  intro i h _
  rw [Array.get_push]
  split
  case inl h' => rw [Array.getElem_pop]
  case inr h' =>
    simp at h'
    have : i + 1 - 1 ≤ a.size - 1 := Nat.sub_le_sub_right h _
    simp at this
    have : i = a.size - 1 := Nat.le_antisymm this h'
    simp [back', this]
State after:
no goals

State before:
case h₁
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
⊢ (a.pop.push (a.back' hemp)).size = a.size
Tactic:
simp [Nat.sub_add_cancel this]
State after:
no goals

State before:
case h₂
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
⊢ ∀ (i : Nat) (hi₁ : i < (a.pop.push (a.back' hemp)).size) (hi₂ : i < a.size), (a.pop.push (a.back' hemp))[i] = a[i]
Tactic:
simp [Nat.sub_add_cancel this]
State after:
case h₂
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
⊢ ∀ (i : Nat) (hi₁ hi₂ : i < a.size), (a.pop.push (a.back' hemp))[i] = a[i]

State before:
case h₂
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
⊢ ∀ (i : Nat) (hi₁ hi₂ : i < a.size), (a.pop.push (a.back' hemp))[i] = a[i]
Tactic:
intro i h _
State after:
case h₂
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
i : Nat
h hi₂✝ : i < a.size
⊢ (a.pop.push (a.back' hemp))[i] = a[i]

State before:
case h₂
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
i : Nat
h hi₂✝ : i < a.size
⊢ (a.pop.push (a.back' hemp))[i] = a[i]
Tactic:
rw [Array.get_push]
State after:
case h₂
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
i : Nat
h hi₂✝ : i < a.size
⊢ (if h : i < a.pop.size then a.pop[i] else a.back' hemp) = a[i]

State before:
case h₂
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
i : Nat
h hi₂✝ : i < a.size
⊢ (if h : i < a.pop.size then a.pop[i] else a.back' hemp) = a[i]
Tactic:
split
State after:
case h₂.inl
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
i : Nat
h hi₂✝ : i < a.size
h✝ : i < a.pop.size
⊢ a.pop[i] = a[i]

case h₂.inr
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
i : Nat
h hi₂✝ : i < a.size
h✝ : ¬i < a.pop.size
⊢ a.back' hemp = a[i]

State before:
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
i : Nat
h hi₂✝ : i < a.size
h' : i < a.pop.size
⊢ a.pop[i] = a[i]
Tactic:
case inl h' => rw [Array.getElem_pop]
State after:
no goals

State before:
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
i : Nat
h hi₂✝ : i < a.size
h' : ¬i < a.pop.size
⊢ a.back' hemp = a[i]
Tactic:
case inr h' =>
  simp at h'
  have : i + 1 - 1 ≤ a.size - 1 := Nat.sub_le_sub_right h _
  simp at this
  have : i = a.size - 1 := Nat.le_antisymm this h'
  simp [back', this]
State after:
no goals

State before:
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
i : Nat
h hi₂✝ : i < a.size
h' : i < a.pop.size
⊢ a.pop[i] = a[i]
Tactic:
rw [Array.getElem_pop]
State after:
no goals

State before:
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
i : Nat
h hi₂✝ : i < a.size
h' : ¬i < a.pop.size
⊢ a.back' hemp = a[i]
Tactic:
simp at h'
State after:
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
i : Nat
h hi₂✝ : i < a.size
h' : a.size - 1 ≤ i
⊢ a.back' hemp = a[i]

State before:
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
i : Nat
h hi₂✝ : i < a.size
h' : a.size - 1 ≤ i
⊢ a.back' hemp = a[i]
Tactic:
have : i + 1 - 1 ≤ a.size - 1 := Nat.sub_le_sub_right h _
State after:
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this✝ : 0 < a.size
i : Nat
h hi₂✝ : i < a.size
h' : a.size - 1 ≤ i
this : i + 1 - 1 ≤ a.size - 1
⊢ a.back' hemp = a[i]

State before:
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this✝ : 0 < a.size
i : Nat
h hi₂✝ : i < a.size
h' : a.size - 1 ≤ i
this : i + 1 - 1 ≤ a.size - 1
⊢ a.back' hemp = a[i]
Tactic:
simp at this
State after:
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this✝ : 0 < a.size
i : Nat
h hi₂✝ : i < a.size
h' : a.size - 1 ≤ i
this : i ≤ a.size - 1
⊢ a.back' hemp = a[i]

State before:
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this✝ : 0 < a.size
i : Nat
h hi₂✝ : i < a.size
h' : a.size - 1 ≤ i
this : i ≤ a.size - 1
⊢ a.back' hemp = a[i]
Tactic:
have : i = a.size - 1 := Nat.le_antisymm this h'
State after:
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this✝¹ : 0 < a.size
i : Nat
h hi₂✝ : i < a.size
h' : a.size - 1 ≤ i
this✝ : i ≤ a.size - 1
this : i = a.size - 1
⊢ a.back' hemp = a[i]

State before:
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this✝¹ : 0 < a.size
i : Nat
h hi₂✝ : i < a.size
h' : a.size - 1 ≤ i
this✝ : i ≤ a.size - 1
this : i = a.size - 1
⊢ a.back' hemp = a[i]
Tactic:
simp [back', this]
State after:
no goals