Theorem: Fitree.id_map (MLIR/Semantics/FitreeLaws.lean)

State before:
E : Type → Type
R : Type
t : Fitree E R
⊢ id <$> t = t
Tactic:
simp [Functor.map]
State after:
E : Type → Type
R : Type
t : Fitree E R
⊢ bind t (ret ∘ id) = t

State before:
E : Type → Type
R : Type
t : Fitree E R
⊢ bind t (ret ∘ id) = t
Tactic:
induction t with
| Ret _ => rfl
| Vis _ _ ih => simp [bind, ih]
State after:
no goals

State before:
case Ret
E : Type → Type
R : Type
r✝ : R
⊢ bind (Ret r✝) (ret ∘ id) = Ret r✝
Tactic:
rfl
State after:
no goals

State before:
case Vis
E : Type → Type
R T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E R
ih : ∀ (a : T✝), bind (k✝ a) (ret ∘ id) = k✝ a
⊢ bind (Vis e✝ k✝) (ret ∘ id) = Vis e✝ k✝
Tactic:
simp [bind, ih]
State after:
no goals