Theorem: IContainer.Map_spec (CoInd/QPF/MIdx.lean)

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

State before:
case mk
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
i : I
α β γ : I → Type u₁
f : (i : I) → β i → γ i
g : (i : I) → α i → β i
fst✝ : A (IQPF.C F) i
snd✝ : (y : B (IQPF.C F) i fst✝) → α (N (IQPF.C F) i fst✝ y)
⊢ Map (fun i => f i ∘ g i) { fst := fst✝, snd := snd✝ } = Map f (Map g { fst := fst✝, snd := snd✝ })
Tactic:
simp [IContainer.Map]
State after:
no goals