Theorem: Partial.map_map (ReactorModel/Extensions.lean)

State before:
α : Sort u_1
β γ δ : Type u_2
f : α ⇀ β
g₁ : β → γ
g₂ : γ → δ
⊢ map g₂ (map g₁ f) = map (g₂ ∘ g₁) f
Tactic:
unfold map
State after:
α : Sort u_1
β γ δ : Type u_2
f : α ⇀ β
g₁ : β → γ
g₂ : γ → δ
⊢ (fun a => g₂ <$> g₁ <$> f a) = fun a => (g₂ ∘ g₁) <$> f a

State before:
α : Sort u_1
β γ δ : Type u_2
f : α ⇀ β
g₁ : β → γ
g₂ : γ → δ
⊢ (fun a => g₂ <$> g₁ <$> f a) = fun a => (g₂ ∘ g₁) <$> f a
Tactic:
simp
State after:
no goals