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

State before:
α : Type u
β : Type v
γ : Type w
n : Nat
f : α → β
g : β → γ
x✝ : SizedArray α n
n✝ : Nat
x : SizedArray α n✝
a : α
IH : map (g ∘ f) x = map g (map f x)
⊢ map (g ∘ f) (push x a) = map g (map f (push x a))
Tactic:
simp only [map_push, IH]
State after:
α : Type u
β : Type v
γ : Type w
n : Nat
f : α → β
g : β → γ
x✝ : SizedArray α n
n✝ : Nat
x : SizedArray α n✝
a : α
IH : map (g ∘ f) x = map g (map f x)
⊢ push (map g (map f x)) ((g ∘ f) a) = push (map g (map f x)) (g (f a))

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