Theorem: Array.size_pmap (Fifteen/Data/Array/Basic.lean)

State before:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
⊢ size (pmap f as h) = size as
Tactic:
rewrite [pmap_eq_nat_fold'_push]
State after:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
⊢ size (Nat.fold' (size as) (fun i x => push x (f as[i.val] (_ : p as[i.val]))) #[]) = size as

State before:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
⊢ size (Nat.fold' (size as) (fun i x => push x (f as[i.val] (_ : p as[i.val]))) #[]) = size as
Tactic:
refine Nat.fold'_induction (motive := fun k (x : Array β) => x.size = k) as.size _ #[] rfl ?_
State after:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
⊢ ∀ (i : Nat) (hi : i < size as) (a : Array β),
    (fun k x => size x = k) i a →
      (fun k x => size x = k) (i + 1)
        (push a (f as[{ val := i, isLt := hi }.val] (_ : p as[{ val := i, isLt := hi }.val])))

State before:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
⊢ ∀ (i : Nat) (hi : i < size as) (a : Array β),
    (fun k x => size x = k) i a →
      (fun k x => size x = k) (i + 1)
        (push a (f as[{ val := i, isLt := hi }.val] (_ : p as[{ val := i, isLt := hi }.val])))
Tactic:
intro i hi x hx
State after:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
i : Nat
hi : i < size as
x : Array β
hx : size x = i
⊢ size (push x (f as[{ val := i, isLt := hi }.val] (_ : p as[{ val := i, isLt := hi }.val]))) = i + 1

State before:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
i : Nat
hi : i < size as
x : Array β
hx : size x = i
⊢ size (push x (f as[{ val := i, isLt := hi }.val] (_ : p as[{ val := i, isLt := hi }.val]))) = i + 1
Tactic:
simp only [size_push, hx]
State after:
no goals