Theorem: IQPF.M.imap_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 : F α i
⊢ IFunctor.imap (fun i => f i ∘ g i) x = IFunctor.imap f (IFunctor.imap g x)
Tactic:
conv =>
  congr
  <;> rw [←inst.abs_repr x]
State after:
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 : F α i
⊢ IFunctor.imap (fun i => f i ∘ g i) (abs (repr x)) = IFunctor.imap f (IFunctor.imap g (abs (repr x)))

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 : F α i
⊢ IFunctor.imap (fun i => f i ∘ g i) (abs (repr x)) = IFunctor.imap f (IFunctor.imap g (abs (repr x)))
Tactic:
cases repr 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
x : F α i
fst✝ : IContainer.A (C F) i
snd✝ : (y : IContainer.B (C F) i fst✝) → α (IContainer.N (C F) i fst✝ y)
⊢ IFunctor.imap (fun i => f i ∘ g i) (abs { fst := fst✝, snd := snd✝ }) =
    IFunctor.imap f (IFunctor.imap g (abs { 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
x : F α i
fst✝ : IContainer.A (C F) i
snd✝ : (y : IContainer.B (C F) i fst✝) → α (IContainer.N (C F) i fst✝ y)
⊢ IFunctor.imap (fun i => f i ∘ g i) (abs { fst := fst✝, snd := snd✝ }) =
    IFunctor.imap f (IFunctor.imap g (abs { fst := fst✝, snd := snd✝ }))
Tactic:
simp [←inst.abs_imap, IContainer.Map]
State after:
no goals