Theorem: Free.pure_bind (CoInd/QPF/FreeMonads.lean)

State before:
F : Type u → Type u
inst : QPF F
R S : Type u
x : R
k : R → Free F S
⊢ pure x >>= k = k x
Tactic:
simp only [pure, bind]
State after:
F : Type u → Type u
inst : QPF F
R S : Type u
x : R
k : R → Free F S
⊢ corec (bind.automaton k) (Sum.inl (construct (FreeF.Pure x))) = k x

State before:
F : Type u → Type u
inst : QPF F
R S : Type u
x : R
k : R → Free F S
⊢ corec (bind.automaton k) (Sum.inl (construct (FreeF.Pure x))) = k x
Tactic:
conv =>
  lhs
  rw [←construct_destruct (corec (bind.automaton k) (.inl (construct <| .Pure x)))]
  rw [destruct_corec]
  rhs
  rhs
  simp only [bind.automaton, destruct_construct]
State after:
F : Type u → Type u
inst : QPF F
R S : Type u
x : R
k : R → Free F S
⊢ construct (corec (bind.automaton k) <$> Sum.inr <$> destruct (k x)) = k x

State before:
F : Type u → Type u
inst : QPF F
R S : Type u
x : R
k : R → Free F S
⊢ construct (corec (bind.automaton k) <$> Sum.inr <$> destruct (k x)) = k x
Tactic:
simp only [←QPF.map_comp, Function.comp]
State after:
F : Type u → Type u
inst : QPF F
R S : Type u
x : R
k : R → Free F S
⊢ construct ((fun x => corec (bind.automaton k) (Sum.inr x)) <$> destruct (k x)) = k x

State before:
F : Type u → Type u
inst : QPF F
R S : Type u
x : R
k : R → Free F S
⊢ construct ((fun x => corec (bind.automaton k) (Sum.inr x)) <$> destruct (k x)) = k x
Tactic:
conv =>
  lhs
  congr
  lhs
  intro x
  rw [bind_inr]
State after:
F : Type u → Type u
inst : QPF F
R S : Type u
x : R
k : R → Free F S
⊢ construct ((fun x => x) <$> destruct (k x)) = k x

State before:
F : Type u → Type u
inst : QPF F
R S : Type u
x : R
k : R → Free F S
⊢ construct ((fun x => x) <$> destruct (k x)) = k x
Tactic:
have := QPF.map_id (destruct (k x))
State after:
F : Type u → Type u
inst : QPF F
R S : Type u
x : R
k : R → Free F S
this : id <$> destruct (k x) = destruct (k x)
⊢ construct ((fun x => x) <$> destruct (k x)) = k x

State before:
F : Type u → Type u
inst : QPF F
R S : Type u
x : R
k : R → Free F S
this : id <$> destruct (k x) = destruct (k x)
⊢ construct ((fun x => x) <$> destruct (k x)) = k x
Tactic:
simp only [id] at this
State after:
F : Type u → Type u
inst : QPF F
R S : Type u
x : R
k : R → Free F S
this : (fun a => a) <$> destruct (k x) = destruct (k x)
⊢ construct ((fun x => x) <$> destruct (k x)) = k x

State before:
F : Type u → Type u
inst : QPF F
R S : Type u
x : R
k : R → Free F S
this : (fun a => a) <$> destruct (k x) = destruct (k x)
⊢ construct ((fun x => x) <$> destruct (k x)) = k x
Tactic:
rw [this, construct_destruct]
State after:
no goals