Theorem: IQPF.M.destruct_corec (CoInd/QPF/MIdx.lean)

State before:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
α : I → Type u₁
f : (i : I) → α i → F α i
i : I
x₀ : α i
⊢ destruct (corec f x₀) = IFunctor.imap (fun i x => corec f x) (f i x₀)
Tactic:
simp only [IQPF.M.destruct, IQPF.M.corec, destruct.f, IContainer.M.destruct_corec, inst.abs_imap, inst.abs_repr]
State after:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
α : I → Type u₁
f : (i : I) → α i → F α i
i : I
x₀ : α i
⊢ IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1)
      (IFunctor.imap (fun i => IContainer.M.corec fun i x => repr (f i x)) (f i x₀)) =
    IFunctor.imap (fun i x => Quot.mk (congr F i) (IContainer.M.corec (fun i x => repr (f i x)) x)) (f i x₀)

State before:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
α : I → Type u₁
f : (i : I) → α i → F α i
i : I
x₀ : α i
⊢ IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1)
      (IFunctor.imap (fun i => IContainer.M.corec fun i x => repr (f i x)) (f i x₀)) =
    IFunctor.imap (fun i x => Quot.mk (congr F i) (IContainer.M.corec (fun i x => repr (f i x)) x)) (f i x₀)
Tactic:
rw [←inst.abs_repr (f i x₀)]
State after:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
α : I → Type u₁
f : (i : I) → α i → F α i
i : I
x₀ : α i
⊢ IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1)
      (IFunctor.imap (fun i => IContainer.M.corec fun i x => repr (f i x)) (abs (repr (f i x₀)))) =
    IFunctor.imap (fun i x => Quot.mk (congr F i) (IContainer.M.corec (fun i x => repr (f i x)) x))
      (abs (repr (f i x₀)))

State before:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
α : I → Type u₁
f : (i : I) → α i → F α i
i : I
x₀ : α i
⊢ IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1)
      (IFunctor.imap (fun i => IContainer.M.corec fun i x => repr (f i x)) (abs (repr (f i x₀)))) =
    IFunctor.imap (fun i x => Quot.mk (congr F i) (IContainer.M.corec (fun i x => repr (f i x)) x))
      (abs (repr (f i x₀)))
Tactic:
cases repr (f i x₀) with
| mk n k =>
  simp only [←inst.abs_imap, IContainer.Map]
State after:
no goals

State before:
case mk
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
α : I → Type u₁
f : (i : I) → α i → F α i
i : I
x₀ : α i
n : IContainer.A (C F) i
k : (y : IContainer.B (C F) i n) → α (IContainer.N (C F) i n y)
⊢ IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1)
      (IFunctor.imap (fun i => IContainer.M.corec fun i x => repr (f i x)) (abs { fst := n, snd := k })) =
    IFunctor.imap (fun i x => Quot.mk (congr F i) (IContainer.M.corec (fun i x => repr (f i x)) x))
      (abs { fst := n, snd := k })
Tactic:
simp only [←inst.abs_imap, IContainer.Map]
State after:
no goals