Theorem: Array.size_mapIdx' (Algdata/Data/Array/Lemmas.lean)

State before:
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
x✝ : Array α
f✝ : Fin (size x✝) → α → β
a : α
x : Array α
IH : ∀ (x_1 : Fin (size x) → α → β), size (mapIdx x x_1) = size x
f : Fin (size (cons a x)) → α → β
⊢ size (mapIdx (cons a x) f) = size (cons a x)
Tactic:
rw [mapIdx_cons]
State after:
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
x✝ : Array α
f✝ : Fin (size x✝) → α → β
a : α
x : Array α
IH : ∀ (x_1 : Fin (size x) → α → β), size (mapIdx x x_1) = size x
f : Fin (size (cons a x)) → α → β
⊢ size (cons (f { val := 0, isLt := (_ : 0 < Nat.succ (size x)) } a) (mapIdx x (f ∘ Fin.succ))) = size (cons a x)

State before:
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
x✝ : Array α
f✝ : Fin (size x✝) → α → β
a : α
x : Array α
IH : ∀ (x_1 : Fin (size x) → α → β), size (mapIdx x x_1) = size x
f : Fin (size (cons a x)) → α → β
⊢ size (cons (f { val := 0, isLt := (_ : 0 < Nat.succ (size x)) } a) (mapIdx x (f ∘ Fin.succ))) = size (cons a x)
Tactic:
dsimp [cons]
State after:
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
x✝ : Array α
f✝ : Fin (size x✝) → α → β
a : α
x : Array α
IH : ∀ (x_1 : Fin (size x) → α → β), size (mapIdx x x_1) = size x
f : Fin (size (cons a x)) → α → β
⊢ size { data := f 0 a :: (mapIdx x (f ∘ Fin.succ)).data } = size { data := a :: x.data }

State before:
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
x✝ : Array α
f✝ : Fin (size x✝) → α → β
a : α
x : Array α
IH : ∀ (x_1 : Fin (size x) → α → β), size (mapIdx x x_1) = size x
f : Fin (size (cons a x)) → α → β
⊢ size { data := f 0 a :: (mapIdx x (f ∘ Fin.succ)).data } = size { data := a :: x.data }
Tactic:
exact congrArg Nat.succ (IH (f ∘ Fin.succ))
State after:
no goals