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

State before:
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
⊢ ∀ (x : Free F S), corec (bind.automaton k) (Sum.inr x) = x
Tactic:
intro x
State after:
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x : Free F S
⊢ corec (bind.automaton k) (Sum.inr x) = x

State before:
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x : Free F S
⊢ corec (bind.automaton k) (Sum.inr x) = x
Tactic:
have := Free.bind_inr.internal k x (corec (bind.automaton k) (.inr x)) (by rfl)
State after:
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x : Free F S
this : x = corec (bind.automaton k) (Sum.inr x)
⊢ corec (bind.automaton k) (Sum.inr x) = x

State before:
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x : Free F S
this : x = corec (bind.automaton k) (Sum.inr x)
⊢ corec (bind.automaton k) (Sum.inr x) = x
Tactic:
conv =>
  rhs
  rw [this]
State after:
no goals

State before:
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x : Free F S
⊢ corec (bind.automaton k) (Sum.inr x) = corec (bind.automaton k) (Sum.inr x)
Tactic:
rfl
State after:
no goals