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

State before:
F : Type u → Type u
inst : QPF F
R : Type u
motive : Free F R → Sort u_1
pure : (r : R) → motive (Pure.pure r)
free : (f : F (Free F R)) → motive (Free.free f)
⊢ (x : Free F R) → motive x
Tactic:
intro x
State after:
F : Type u → Type u
inst : QPF F
R : Type u
motive : Free F R → Sort u_1
pure : (r : R) → motive (Pure.pure r)
free : (f : F (Free F R)) → motive (Free.free f)
x : Free F R
⊢ motive x

State before:
F : Type u → Type u
inst : QPF F
R : Type u
motive : Free F R → Sort u_1
pure : (r : R) → motive (Pure.pure r)
free : (f : F (Free F R)) → motive (Free.free f)
x : Free F R
⊢ motive x
Tactic:
rw [←construct_destruct x]
State after:
F : Type u → Type u
inst : QPF F
R : Type u
motive : Free F R → Sort u_1
pure : (r : R) → motive (Pure.pure r)
free : (f : F (Free F R)) → motive (Free.free f)
x : Free F R
⊢ motive (construct (destruct x))

State before:
F : Type u → Type u
inst : QPF F
R : Type u
motive : Free F R → Sort u_1
pure : (r : R) → motive (Pure.pure r)
free : (f : F (Free F R)) → motive (Free.free f)
x : Free F R
⊢ motive (construct (destruct x))
Tactic:
cases destruct x with
| Pure r =>
  exact pure r
| Free f =>
  exact free f
State after:
no goals

State before:
case Pure
F : Type u → Type u
inst : QPF F
R : Type u
motive : Free F R → Sort u_1
pure : (r : R) → motive (Pure.pure r)
free : (f : F (Free F R)) → motive (Free.free f)
x : Free F R
r : R
⊢ motive (construct (FreeF.Pure r))
Tactic:
exact pure r
State after:
no goals

State before:
case Free
F : Type u → Type u
inst : QPF F
R : Type u
motive : Free F R → Sort u_1
pure : (r : R) → motive (Pure.pure r)
free : (f : F (Free F R)) → motive (Free.free f)
x : Free F R
f : F (Free F R)
⊢ motive (construct (FreeF.Free f))
Tactic:
exact free f
State after:
no goals