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

State before:
F : Type u₁ → Type u₁
inst : QPF F
α : Type u₁
f : α → F α
x₀ : α
⊢ destruct (corec f x₀) = (fun x => corec f x) <$> f x₀
Tactic:
simp only [destruct, corec, destruct.f, Container.M.destruct_corec, inst.abs_map, inst.abs_repr]
State after:
F : Type u₁ → Type u₁
inst : QPF F
α : Type u₁
f : α → F α
x₀ : α
⊢ (fun x => Quot.mk (congr F) x) <$> (Container.M.corec fun x => repr (f x)) <$> f x₀ =
    (fun x => Quot.mk (congr F) (Container.M.corec (fun x => repr (f x)) x)) <$> f x₀

State before:
F : Type u₁ → Type u₁
inst : QPF F
α : Type u₁
f : α → F α
x₀ : α
⊢ (fun x => Quot.mk (congr F) x) <$> (Container.M.corec fun x => repr (f x)) <$> f x₀ =
    (fun x => Quot.mk (congr F) (Container.M.corec (fun x => repr (f x)) x)) <$> f x₀
Tactic:
rw [←inst.abs_repr (f x₀)]
State after:
F : Type u₁ → Type u₁
inst : QPF F
α : Type u₁
f : α → F α
x₀ : α
⊢ (fun x => Quot.mk (congr F) x) <$> (Container.M.corec fun x => repr (f x)) <$> abs (repr (f x₀)) =
    (fun x => Quot.mk (congr F) (Container.M.corec (fun x => repr (f x)) x)) <$> abs (repr (f x₀))

State before:
F : Type u₁ → Type u₁
inst : QPF F
α : Type u₁
f : α → F α
x₀ : α
⊢ (fun x => Quot.mk (congr F) x) <$> (Container.M.corec fun x => repr (f x)) <$> abs (repr (f x₀)) =
    (fun x => Quot.mk (congr F) (Container.M.corec (fun x => repr (f x)) x)) <$> abs (repr (f x₀))
Tactic:
cases repr (f x₀) with
| mk n k =>
  simp only [←inst.abs_map, Container.Map]
  rfl
State after:
no goals

State before:
case mk
F : Type u₁ → Type u₁
inst : QPF F
α : Type u₁
f : α → F α
x₀ : α
n : (C F).A
k : Container.B (C F) n → α
⊢ (fun x => Quot.mk (congr F) x) <$> (Container.M.corec fun x => repr (f x)) <$> abs { fst := n, snd := k } =
    (fun x => Quot.mk (congr F) (Container.M.corec (fun x => repr (f x)) x)) <$> abs { fst := n, snd := k }
Tactic:
simp only [←inst.abs_map, Container.Map]
State after:
case mk
F : Type u₁ → Type u₁
inst : QPF F
α : Type u₁
f : α → F α
x₀ : α
n : (C F).A
k : Container.B (C F) n → α
⊢ abs { fst := n, snd := (fun x => Quot.mk (congr F) x) ∘ (Container.M.corec fun x => repr (f x)) ∘ k } =
    abs { fst := n, snd := (fun x => Quot.mk (congr F) (Container.M.corec (fun x => repr (f x)) x)) ∘ k }

State before:
case mk
F : Type u₁ → Type u₁
inst : QPF F
α : Type u₁
f : α → F α
x₀ : α
n : (C F).A
k : Container.B (C F) n → α
⊢ abs { fst := n, snd := (fun x => Quot.mk (congr F) x) ∘ (Container.M.corec fun x => repr (f x)) ∘ k } =
    abs { fst := n, snd := (fun x => Quot.mk (congr F) (Container.M.corec (fun x => repr (f x)) x)) ∘ k }
Tactic:
rfl
State after:
no goals