Theorem: Array.push_induction (Algdata/Data/Array/Lemmas.lean)

State before:
α : Type u
motive : Array α → Prop
empty : motive #[]
push : ∀ (as : Array α) (a : α), motive as → motive (Array.push as a)
n : Nat
IH : ∀ (as : Array α), size as = n → motive as
as : Array α
hn : size as = Nat.succ n
⊢ motive as
Tactic:
rw [← as.push_pop_back' (hn ▸ n.zero_lt_succ)]
State after:
α : Type u
motive : Array α → Prop
empty : motive #[]
push : ∀ (as : Array α) (a : α), motive as → motive (Array.push as a)
n : Nat
IH : ∀ (as : Array α), size as = n → motive as
as : Array α
hn : size as = Nat.succ n
⊢ motive (Array.push (pop as) (back' as (_ : size as > 0)))

State before:
α : Type u
motive : Array α → Prop
empty : motive #[]
push : ∀ (as : Array α) (a : α), motive as → motive (Array.push as a)
n : Nat
IH : ∀ (as : Array α), size as = n → motive as
as : Array α
hn : size as = Nat.succ n
⊢ motive (Array.push (pop as) (back' as (_ : size as > 0)))
Tactic:
apply push
State after:
case a
α : Type u
motive : Array α → Prop
empty : motive #[]
push : ∀ (as : Array α) (a : α), motive as → motive (Array.push as a)
n : Nat
IH : ∀ (as : Array α), size as = n → motive as
as : Array α
hn : size as = Nat.succ n
⊢ motive (pop as)

State before:
case a
α : Type u
motive : Array α → Prop
empty : motive #[]
push : ∀ (as : Array α) (a : α), motive as → motive (Array.push as a)
n : Nat
IH : ∀ (as : Array α), size as = n → motive as
as : Array α
hn : size as = Nat.succ n
⊢ motive (pop as)
Tactic:
apply IH
State after:
case a.a
α : Type u
motive : Array α → Prop
empty : motive #[]
push : ∀ (as : Array α) (a : α), motive as → motive (Array.push as a)
n : Nat
IH : ∀ (as : Array α), size as = n → motive as
as : Array α
hn : size as = Nat.succ n
⊢ size (pop as) = n