Theorem: Free.bind_pure (CoInd/FreeMonads.lean)

State before:
C : _root_.Container
R S : Type u₁
r : R
k : R → Free C S
⊢ bind (pure r) k = k r
Tactic:
rw [←construct_destruct <| k r]
State after:
C : _root_.Container
R S : Type u₁
r : R
k : R → Free C S
⊢ bind (pure r) k = construct (destruct (k r))

State before:
C : _root_.Container
R S : Type u₁
r : R
k : R → Free C S
⊢ bind (pure r) k = construct (destruct (k r))
Tactic:
rw [←construct_destruct <| bind (pure r) k]
State after:
C : _root_.Container
R S : Type u₁
r : R
k : R → Free C S
⊢ construct (destruct (bind (pure r) k)) = construct (destruct (k r))

State before:
C : _root_.Container
R S : Type u₁
r : R
k : R → Free C S
⊢ construct (destruct (bind (pure r) k)) = construct (destruct (k r))
Tactic:
simp only [bind, pure, destruct_corec]
State after:
C : _root_.Container
R S : Type u₁
r : R
k : R → Free C S
⊢ construct (Map (corec (bind.automaton k)) (bind.automaton k (Sum.inl (construct (Functor.Pure r))))) =
    construct (destruct (k r))

State before:
C : _root_.Container
R S : Type u₁
r : R
k : R → Free C S
⊢ construct (Map (corec (bind.automaton k)) (bind.automaton k (Sum.inl (construct (Functor.Pure r))))) =
    construct (destruct (k r))
Tactic:
apply congrArg construct
State after:
C : _root_.Container
R S : Type u₁
r : R
k : R → Free C S
⊢ Map (corec (bind.automaton k)) (bind.automaton k (Sum.inl (construct (Functor.Pure r)))) = destruct (k r)

State before:
C : _root_.Container
R S : Type u₁
r : R
k : R → Free C S
⊢ Map (corec (bind.automaton k)) (bind.automaton k (Sum.inl (construct (Functor.Pure r)))) = destruct (k r)
Tactic:
conv =>
  lhs
  congr
  . rfl
  . simp only [bind.automaton, destruct_construct]
State after:
C : _root_.Container
R S : Type u₁
r : R
k : R → Free C S
⊢ Map (corec (bind.automaton k)) (Map Sum.inr (destruct (k r))) = destruct (k r)

State before:
C : _root_.Container
R S : Type u₁
r : R
k : R → Free C S
⊢ Map (corec (bind.automaton k)) (Map Sum.inr (destruct (k r))) = destruct (k r)
Tactic:
cases destruct (k r) with
| Pure r =>
  simp only [Map]
| Free n k =>
  simp only [Map]
  conv =>
    lhs
    congr
    simp only [Function.comp]
    intro x
    rw [bind_inr]
State after:
no goals

State before:
case Pure
C : _root_.Container
R S : Type u₁
r✝ : R
k : R → Free C S
r : S
⊢ Map (corec (bind.automaton k)) (Map Sum.inr (Functor.Pure r)) = Functor.Pure r
Tactic:
simp only [Map]
State after:
no goals

State before:
case Free
C : _root_.Container
R S : Type u₁
r : R
k✝ : R → Free C S
n : C.A
k : Container.B C n → Free C S
⊢ Map (corec (bind.automaton k✝)) (Map Sum.inr (Functor.Free n k)) = Functor.Free n k
Tactic:
simp only [Map]
State after:
case Free
C : _root_.Container
R S : Type u₁
r : R
k✝ : R → Free C S
n : C.A
k : Container.B C n → Free C S
⊢ Functor.Free n (corec (bind.automaton k✝) ∘ Sum.inr ∘ k) = Functor.Free n k

State before:
case Free
C : _root_.Container
R S : Type u₁
r : R
k✝ : R → Free C S
n : C.A
k : Container.B C n → Free C S
⊢ Functor.Free n (corec (bind.automaton k✝) ∘ Sum.inr ∘ k) = Functor.Free n k
Tactic:
conv =>
  lhs
  congr
  simp only [Function.comp]
  intro x
  rw [bind_inr]
State after:
no goals