Theorem: Container.Map_spec (CoInd/QPF/M.lean)

State before:
F : Type u₁ → Type u₁
inst : QPF F
α β γ : Type u₁
f : β → γ
g : α → β
x : Obj (QPF.C F) α
⊢ Map (f ∘ g) x = Map f (Map g x)
Tactic:
cases x
State after:
case mk
F : Type u₁ → Type u₁
inst : QPF F
α β γ : Type u₁
f : β → γ
g : α → β
fst✝ : (QPF.C F).A
snd✝ : B (QPF.C F) fst✝ → α
⊢ Map (f ∘ g) { fst := fst✝, snd := snd✝ } = Map f (Map g { fst := fst✝, snd := snd✝ })

State before:
case mk
F : Type u₁ → Type u₁
inst : QPF F
α β γ : Type u₁
f : β → γ
g : α → β
fst✝ : (QPF.C F).A
snd✝ : B (QPF.C F) fst✝ → α
⊢ Map (f ∘ g) { fst := fst✝, snd := snd✝ } = Map f (Map g { fst := fst✝, snd := snd✝ })
Tactic:
simp [Map]
State after:
case mk
F : Type u₁ → Type u₁
inst : QPF F
α β γ : Type u₁
f : β → γ
g : α → β
fst✝ : (QPF.C F).A
snd✝ : B (QPF.C F) fst✝ → α
⊢ (f ∘ g) ∘ snd✝ = f ∘ g ∘ snd✝

State before:
case mk
F : Type u₁ → Type u₁
inst : QPF F
α β γ : Type u₁
f : β → γ
g : α → β
fst✝ : (QPF.C F).A
snd✝ : B (QPF.C F) fst✝ → α
⊢ (f ∘ g) ∘ snd✝ = f ∘ g ∘ snd✝
Tactic:
rfl
State after:
no goals