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

State before:
R₁ R₂ R₃ : Type
E : Type → Type
f : R₁ → R₂
g : R₂ → R₃
t : Fitree E R₁
⊢ (g ∘ f) <$> t = g <$> f <$> t
Tactic:
simp [Functor.map]
State after:
R₁ R₂ R₃ : Type
E : Type → Type
f : R₁ → R₂
g : R₂ → R₃
t : Fitree E R₁
⊢ bind t (ret ∘ g ∘ f) = bind t fun x => ret (g (f x))

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

State before:
case Ret
R₁ R₂ R₃ : Type
E : Type → Type
f : R₁ → R₂
g : R₂ → R₃
r✝ : R₁
⊢ bind (Ret r✝) (ret ∘ g ∘ f) = bind (Ret r✝) fun x => ret (g (f x))
Tactic:
rfl
State after:
no goals

State before:
case Vis
R₁ R₂ R₃ : Type
E : Type → Type
f : R₁ → R₂
g : R₂ → R₃
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E R₁
ih : ∀ (a : T✝), bind (k✝ a) (ret ∘ g ∘ f) = bind (k✝ a) fun x => ret (g (f x))
⊢ bind (Vis e✝ k✝) (ret ∘ g ∘ f) = bind (Vis e✝ k✝) fun x => ret (g (f x))
Tactic:
simp [bind, ih]
State after:
no goals