Theorem: SizedArray.map_id (Algdata/Data/Array/Sized.lean)

State before:
α : Type u
β : Type v
γ : Type w
n : Nat
x✝ : SizedArray α n
n✝ : Nat
x : SizedArray α n✝
a : α
IH : map id x = x
⊢ map id (push x a) = push x a
Tactic:
rw [map_push, IH]
State after:
α : Type u
β : Type v
γ : Type w
n : Nat
x✝ : SizedArray α n
n✝ : Nat
x : SizedArray α n✝
a : α
IH : map id x = x
⊢ push x (id a) = push x a

State before:
α : Type u
β : Type v
γ : Type w
n : Nat
x✝ : SizedArray α n
n✝ : Nat
x : SizedArray α n✝
a : α
IH : map id x = x
⊢ push x (id a) = push x a
Tactic:
rfl
State after:
no goals