Theorem: Free.bind_bind.internal (CoInd/QPF/FreeMonads.lean)

State before:
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
⊢ (fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z) ≤ eq
Tactic:
simp only [Free.eq, Free.eqP, pgfp.coinduction]
State after:
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
⊢ (fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z) ≤
    eqF
      ((fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z) ⊔
        ↑(pgfp { toFun := eqF, monotone' := (_ : Monotone eqF) }) fun y z =>
          ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z)

State before:
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
⊢ (fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z) ≤
    eqF
      ((fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z) ⊔
        ↑(pgfp { toFun := eqF, monotone' := (_ : Monotone eqF) }) fun y z =>
          ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z)
Tactic:
intro y z ⟨x, h₁, h₂⟩
State after:
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y z : Free F T
x : Free F R
h₁ : x >>= k₁ >>= k₂ = y
h₂ : x >>= flip bind k₂ ∘ k₁ = z
⊢ eqF
    ((fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z) ⊔
      ↑(pgfp { toFun := eqF, monotone' := (_ : Monotone eqF) }) fun y z =>
        ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z)
    y z

State before:
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y z : Free F T
x : Free F R
h₁ : x >>= k₁ >>= k₂ = y
h₂ : x >>= flip bind k₂ ∘ k₁ = z
⊢ eqF
    ((fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z) ⊔
      ↑(pgfp { toFun := eqF, monotone' := (_ : Monotone eqF) }) fun y z =>
        ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z)
    y z
Tactic:
induction h₁
State after:
case refl
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y z : Free F T
x : Free F R
h₂ : x >>= flip bind k₂ ∘ k₁ = z
⊢ eqF
    ((fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z) ⊔
      ↑(pgfp { toFun := eqF, monotone' := (_ : Monotone eqF) }) fun y z =>
        ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z)
    (x >>= k₁ >>= k₂) z

State before:
case refl
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y z : Free F T
x : Free F R
h₂ : x >>= flip bind k₂ ∘ k₁ = z
⊢ eqF
    ((fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z) ⊔
      ↑(pgfp { toFun := eqF, monotone' := (_ : Monotone eqF) }) fun y z =>
        ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z)
    (x >>= k₁ >>= k₂) z
Tactic:
induction h₂
State after:
case refl.refl
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y z : Free F T
x : Free F R
⊢ eqF
    ((fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z) ⊔
      ↑(pgfp { toFun := eqF, monotone' := (_ : Monotone eqF) }) fun y z =>
        ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z)
    (x >>= k₁ >>= k₂) (x >>= flip bind k₂ ∘ k₁)

State before:
case refl.refl
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y z : Free F T
x : Free F R
⊢ eqF
    ((fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z) ⊔
      ↑(pgfp { toFun := eqF, monotone' := (_ : Monotone eqF) }) fun y z =>
        ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z)
    (x >>= k₁ >>= k₂) (x >>= flip bind k₂ ∘ k₁)
Tactic:
cases x using by_cases with
| pure r =>
  simp only [pure_bind, flip, Function.comp]
  apply @eqF.monotone F inst T eq
  . intro x y h
    apply Or.inr
    apply pgfp.monotone ⟨eqF, eqF.monotone⟩ ⊥
    . intro x y h
      cases h
    . exact h
  . have := eq.refl (k₁ r >>= k₂)
    rw [eq, eqP, ←pgfp.unfold, CompleteLattice.bot_sup] at this
    exact this
| free f =>
  simp only [←QPF.map_comp, free_bind]
  let P : Free F T → Free F T → Prop :=(λ y z:Free F T => ∃ x, (x >>= k₁ >>= k₂) = y ∧ x >>= (flip bind k₂ ∘ k₁) = z)
  apply @eqF.monotone F inst T P
  . intro x y h
    apply Or.inl
    exact h
  . apply eqF.Free
    exists inst.map (λ x => ⟨⟨x >>= k₁ >>= k₂, x >>= (flip bind k₂ ∘ k₁)⟩, by exists x⟩) f
    simp only [←QPF.map_comp]
    constructor
    . constructor
    . constructor
State after:
no goals

State before:
case refl.refl.pure
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y z : Free F T
r : R
⊢ eqF
    ((fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z) ⊔
      ↑(pgfp { toFun := eqF, monotone' := (_ : Monotone eqF) }) fun y z =>
        ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z)
    (pure r >>= k₁ >>= k₂) (pure r >>= flip bind k₂ ∘ k₁)
Tactic:
simp only [pure_bind, flip, Function.comp]
State after:
case refl.refl.pure
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y z : Free F T
r : R
⊢ eqF
    ((fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ (x >>= fun x => k₁ x >>= k₂) = z) ⊔
      ↑(pgfp { toFun := eqF, monotone' := (_ : Monotone eqF) }) fun y z =>
        ∃ x, x >>= k₁ >>= k₂ = y ∧ (x >>= fun x => k₁ x >>= k₂) = z)
    (k₁ r >>= k₂) (k₁ r >>= k₂)

State before:
case refl.refl.pure
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y z : Free F T
r : R
⊢ eqF
    ((fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ (x >>= fun x => k₁ x >>= k₂) = z) ⊔
      ↑(pgfp { toFun := eqF, monotone' := (_ : Monotone eqF) }) fun y z =>
        ∃ x, x >>= k₁ >>= k₂ = y ∧ (x >>= fun x => k₁ x >>= k₂) = z)
    (k₁ r >>= k₂) (k₁ r >>= k₂)
Tactic:
apply @eqF.monotone F inst T eq
State after:
case refl.refl.pure.a
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y z : Free F T
r : R
⊢ eq ≤
    (fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ (x >>= fun x => k₁ x >>= k₂) = z) ⊔
      ↑(pgfp { toFun := eqF, monotone' := (_ : Monotone eqF) }) fun y z =>
        ∃ x, x >>= k₁ >>= k₂ = y ∧ (x >>= fun x => k₁ x >>= k₂) = z

case refl.refl.pure.a
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y z : Free F T
r : R
⊢ eqF eq (k₁ r >>= k₂) (k₁ r >>= k₂)

State before:
case refl.refl.pure.a
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y z : Free F T
r : R
⊢ eq ≤
    (fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ (x >>= fun x => k₁ x >>= k₂) = z) ⊔
      ↑(pgfp { toFun := eqF, monotone' := (_ : Monotone eqF) }) fun y z =>
        ∃ x, x >>= k₁ >>= k₂ = y ∧ (x >>= fun x => k₁ x >>= k₂) = z

case refl.refl.pure.a
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y z : Free F T
r : R
⊢ eqF eq (k₁ r >>= k₂) (k₁ r >>= k₂)
Tactic:
. intro x y h
  apply Or.inr
  apply pgfp.monotone ⟨eqF, eqF.monotone⟩ ⊥
  . intro x y h
    cases h
  . exact h
State after:
case refl.refl.pure.a
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y z : Free F T
r : R
⊢ eqF eq (k₁ r >>= k₂) (k₁ r >>= k₂)

State before:
case refl.refl.pure.a
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y z : Free F T
r : R
⊢ eqF eq (k₁ r >>= k₂) (k₁ r >>= k₂)
Tactic:
. have := eq.refl (k₁ r >>= k₂)
  rw [eq, eqP, ←pgfp.unfold, CompleteLattice.bot_sup] at this
  exact this
State after:
no goals

State before:
case refl.refl.pure.a
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y z : Free F T
r : R
⊢ eq ≤
    (fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ (x >>= fun x => k₁ x >>= k₂) = z) ⊔
      ↑(pgfp { toFun := eqF, monotone' := (_ : Monotone eqF) }) fun y z =>
        ∃ x, x >>= k₁ >>= k₂ = y ∧ (x >>= fun x => k₁ x >>= k₂) = z
Tactic:
intro x y h
State after:
case refl.refl.pure.a
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y✝ z : Free F T
r : R
x y : Free F T
h : eq x y
⊢ ((fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ (x >>= fun x => k₁ x >>= k₂) = z) ⊔
      ↑(pgfp { toFun := eqF, monotone' := (_ : Monotone eqF) }) fun y z =>
        ∃ x, x >>= k₁ >>= k₂ = y ∧ (x >>= fun x => k₁ x >>= k₂) = z)
    x y

State before:
case refl.refl.pure.a
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y✝ z : Free F T
r : R
x y : Free F T
h : eq x y
⊢ ((fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ (x >>= fun x => k₁ x >>= k₂) = z) ⊔
      ↑(pgfp { toFun := eqF, monotone' := (_ : Monotone eqF) }) fun y z =>
        ∃ x, x >>= k₁ >>= k₂ = y ∧ (x >>= fun x => k₁ x >>= k₂) = z)
    x y
Tactic:
apply Or.inr
State after:
case refl.refl.pure.a.h
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y✝ z : Free F T
r : R
x y : Free F T
h : eq x y
⊢ ↑(pgfp { toFun := eqF, monotone' := (_ : Monotone eqF) })
    (fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ (x >>= fun x => k₁ x >>= k₂) = z) x y

State before:
case refl.refl.pure.a.h
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y✝ z : Free F T
r : R
x y : Free F T
h : eq x y
⊢ ↑(pgfp { toFun := eqF, monotone' := (_ : Monotone eqF) })
    (fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ (x >>= fun x => k₁ x >>= k₂) = z) x y
Tactic:
apply pgfp.monotone ⟨eqF, eqF.monotone⟩ ⊥
State after:
case refl.refl.pure.a.h.a
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y✝ z : Free F T
r : R
x y : Free F T
h : eq x y
⊢ ⊥ ≤ fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ (x >>= fun x => k₁ x >>= k₂) = z

case refl.refl.pure.a.h.a
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y✝ z : Free F T
r : R
x y : Free F T
h : eq x y
⊢ ↑(pgfp { toFun := eqF, monotone' := (_ : Monotone eqF) }) ⊥ x y

State before:
case refl.refl.pure.a.h.a
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y✝ z : Free F T
r : R
x y : Free F T
h : eq x y
⊢ ⊥ ≤ fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ (x >>= fun x => k₁ x >>= k₂) = z

case refl.refl.pure.a.h.a
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y✝ z : Free F T
r : R
x y : Free F T
h : eq x y
⊢ ↑(pgfp { toFun := eqF, monotone' := (_ : Monotone eqF) }) ⊥ x y
Tactic:
. intro x y h
  cases h
State after:
case refl.refl.pure.a.h.a
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y✝ z : Free F T
r : R
x y : Free F T
h : eq x y
⊢ ↑(pgfp { toFun := eqF, monotone' := (_ : Monotone eqF) }) ⊥ x y

State before:
case refl.refl.pure.a.h.a
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y✝ z : Free F T
r : R
x y : Free F T
h : eq x y
⊢ ↑(pgfp { toFun := eqF, monotone' := (_ : Monotone eqF) }) ⊥ x y
Tactic:
. exact h
State after:
no goals

State before:
case refl.refl.pure.a.h.a
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y✝ z : Free F T
r : R
x y : Free F T
h : eq x y
⊢ ⊥ ≤ fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ (x >>= fun x => k₁ x >>= k₂) = z
Tactic:
intro x y h
State after:
case refl.refl.pure.a.h.a
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y✝¹ z : Free F T
r : R
x✝ y✝ : Free F T
h✝ : eq x✝ y✝
x y : Free F T
h : ⊥ x y
⊢ ∃ x_1, x_1 >>= k₁ >>= k₂ = x ∧ (x_1 >>= fun x => k₁ x >>= k₂) = y

State before:
case refl.refl.pure.a.h.a
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y✝¹ z : Free F T
r : R
x✝ y✝ : Free F T
h✝ : eq x✝ y✝
x y : Free F T
h : ⊥ x y
⊢ ∃ x_1, x_1 >>= k₁ >>= k₂ = x ∧ (x_1 >>= fun x => k₁ x >>= k₂) = y
Tactic:
cases h
State after:
no goals

State before:
case refl.refl.pure.a.h.a
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y✝ z : Free F T
r : R
x y : Free F T
h : eq x y
⊢ ↑(pgfp { toFun := eqF, monotone' := (_ : Monotone eqF) }) ⊥ x y
Tactic:
exact h
State after:
no goals

State before:
case refl.refl.pure.a
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y z : Free F T
r : R
⊢ eqF eq (k₁ r >>= k₂) (k₁ r >>= k₂)
Tactic:
have := eq.refl (k₁ r >>= k₂)
State after:
case refl.refl.pure.a
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y z : Free F T
r : R
this : eq (k₁ r >>= k₂) (k₁ r >>= k₂)
⊢ eqF eq (k₁ r >>= k₂) (k₁ r >>= k₂)

State before:
case refl.refl.pure.a
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y z : Free F T
r : R
this : eq (k₁ r >>= k₂) (k₁ r >>= k₂)
⊢ eqF eq (k₁ r >>= k₂) (k₁ r >>= k₂)
Tactic:
rw [eq, eqP, ←pgfp.unfold, CompleteLattice.bot_sup] at this
State after:
case refl.refl.pure.a
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y z : Free F T
r : R
this :
  ↑{ toFun := eqF, monotone' := (_ : Monotone eqF) } (↑(pgfp { toFun := eqF, monotone' := (_ : Monotone eqF) }) ⊥)
    (k₁ r >>= k₂) (k₁ r >>= k₂)
⊢ eqF eq (k₁ r >>= k₂) (k₁ r >>= k₂)

State before:
case refl.refl.pure.a
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y z : Free F T
r : R
this :
  ↑{ toFun := eqF, monotone' := (_ : Monotone eqF) } (↑(pgfp { toFun := eqF, monotone' := (_ : Monotone eqF) }) ⊥)
    (k₁ r >>= k₂) (k₁ r >>= k₂)
⊢ eqF eq (k₁ r >>= k₂) (k₁ r >>= k₂)
Tactic:
exact this
State after:
no goals

State before:
case refl.refl.free
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y z : Free F T
f : F (Free F R)
⊢ eqF
    ((fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z) ⊔
      ↑(pgfp { toFun := eqF, monotone' := (_ : Monotone eqF) }) fun y z =>
        ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z)
    (free f >>= k₁ >>= k₂) (free f >>= flip bind k₂ ∘ k₁)
Tactic:
simp only [←QPF.map_comp, free_bind]
State after:
case refl.refl.free
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y z : Free F T
f : F (Free F R)
⊢ eqF
    ((fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z) ⊔
      ↑(pgfp { toFun := eqF, monotone' := (_ : Monotone eqF) }) fun y z =>
        ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z)
    (free ((flip bind k₂ ∘ flip bind k₁) <$> f)) (free (flip bind (flip bind k₂ ∘ k₁) <$> f))

State before:
case refl.refl.free
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y z : Free F T
f : F (Free F R)
⊢ eqF
    ((fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z) ⊔
      ↑(pgfp { toFun := eqF, monotone' := (_ : Monotone eqF) }) fun y z =>
        ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z)
    (free ((flip bind k₂ ∘ flip bind k₁) <$> f)) (free (flip bind (flip bind k₂ ∘ k₁) <$> f))
Tactic:
let P : Free F T → Free F T → Prop :=(λ y z:Free F T => ∃ x, (x >>= k₁ >>= k₂) = y ∧ x >>= (flip bind k₂ ∘ k₁) = z)
State after:
case refl.refl.free
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y z : Free F T
f : F (Free F R)
P : Free F T → Free F T → Prop := fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z
⊢ eqF
    ((fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z) ⊔
      ↑(pgfp { toFun := eqF, monotone' := (_ : Monotone eqF) }) fun y z =>
        ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z)
    (free ((flip bind k₂ ∘ flip bind k₁) <$> f)) (free (flip bind (flip bind k₂ ∘ k₁) <$> f))

State before:
case refl.refl.free
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y z : Free F T
f : F (Free F R)
P : Free F T → Free F T → Prop := fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z
⊢ eqF
    ((fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z) ⊔
      ↑(pgfp { toFun := eqF, monotone' := (_ : Monotone eqF) }) fun y z =>
        ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z)
    (free ((flip bind k₂ ∘ flip bind k₁) <$> f)) (free (flip bind (flip bind k₂ ∘ k₁) <$> f))
Tactic:
apply @eqF.monotone F inst T P
State after:
case refl.refl.free.a
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y z : Free F T
f : F (Free F R)
P : Free F T → Free F T → Prop := fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z
⊢ P ≤
    (fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z) ⊔
      ↑(pgfp { toFun := eqF, monotone' := (_ : Monotone eqF) }) fun y z =>
        ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z

case refl.refl.free.a
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y z : Free F T
f : F (Free F R)
P : Free F T → Free F T → Prop := fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z
⊢ eqF P (free ((flip bind k₂ ∘ flip bind k₁) <$> f)) (free (flip bind (flip bind k₂ ∘ k₁) <$> f))

State before:
case refl.refl.free.a
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y z : Free F T
f : F (Free F R)
P : Free F T → Free F T → Prop := fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z
⊢ P ≤
    (fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z) ⊔
      ↑(pgfp { toFun := eqF, monotone' := (_ : Monotone eqF) }) fun y z =>
        ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z

case refl.refl.free.a
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y z : Free F T
f : F (Free F R)
P : Free F T → Free F T → Prop := fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z
⊢ eqF P (free ((flip bind k₂ ∘ flip bind k₁) <$> f)) (free (flip bind (flip bind k₂ ∘ k₁) <$> f))
Tactic:
. intro x y h
  apply Or.inl
  exact h
State after:
case refl.refl.free.a
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y z : Free F T
f : F (Free F R)
P : Free F T → Free F T → Prop := fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z
⊢ eqF P (free ((flip bind k₂ ∘ flip bind k₁) <$> f)) (free (flip bind (flip bind k₂ ∘ k₁) <$> f))

State before:
case refl.refl.free.a
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y z : Free F T
f : F (Free F R)
P : Free F T → Free F T → Prop := fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z
⊢ eqF P (free ((flip bind k₂ ∘ flip bind k₁) <$> f)) (free (flip bind (flip bind k₂ ∘ k₁) <$> f))
Tactic:
. apply eqF.Free
  exists inst.map (λ x => ⟨⟨x >>= k₁ >>= k₂, x >>= (flip bind k₂ ∘ k₁)⟩, by exists x⟩) f
  simp only [←QPF.map_comp]
  constructor
  . constructor
  . constructor
State after:
no goals

State before:
case refl.refl.free.a
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y z : Free F T
f : F (Free F R)
P : Free F T → Free F T → Prop := fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z
⊢ P ≤
    (fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z) ⊔
      ↑(pgfp { toFun := eqF, monotone' := (_ : Monotone eqF) }) fun y z =>
        ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z
Tactic:
intro x y h
State after:
case refl.refl.free.a
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y✝ z : Free F T
f : F (Free F R)
P : Free F T → Free F T → Prop := fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z
x y : Free F T
h : P x y
⊢ ((fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z) ⊔
      ↑(pgfp { toFun := eqF, monotone' := (_ : Monotone eqF) }) fun y z =>
        ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z)
    x y

State before:
case refl.refl.free.a
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y✝ z : Free F T
f : F (Free F R)
P : Free F T → Free F T → Prop := fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z
x y : Free F T
h : P x y
⊢ ((fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z) ⊔
      ↑(pgfp { toFun := eqF, monotone' := (_ : Monotone eqF) }) fun y z =>
        ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z)
    x y
Tactic:
apply Or.inl
State after:
case refl.refl.free.a.h
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y✝ z : Free F T
f : F (Free F R)
P : Free F T → Free F T → Prop := fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z
x y : Free F T
h : P x y
⊢ (fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z) x y

State before:
case refl.refl.free.a.h
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y✝ z : Free F T
f : F (Free F R)
P : Free F T → Free F T → Prop := fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z
x y : Free F T
h : P x y
⊢ (fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z) x y
Tactic:
exact h
State after:
no goals

State before:
case refl.refl.free.a
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y z : Free F T
f : F (Free F R)
P : Free F T → Free F T → Prop := fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z
⊢ eqF P (free ((flip bind k₂ ∘ flip bind k₁) <$> f)) (free (flip bind (flip bind k₂ ∘ k₁) <$> f))
Tactic:
apply eqF.Free
State after:
case refl.refl.free.a.a
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y z : Free F T
f : F (Free F R)
P : Free F T → Free F T → Prop := fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z
⊢ QPF.M.liftr F P ((flip bind k₂ ∘ flip bind k₁) <$> f) (flip bind (flip bind k₂ ∘ k₁) <$> f)

State before:
case refl.refl.free.a.a
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y z : Free F T
f : F (Free F R)
P : Free F T → Free F T → Prop := fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z
⊢ QPF.M.liftr F P ((flip bind k₂ ∘ flip bind k₁) <$> f) (flip bind (flip bind k₂ ∘ k₁) <$> f)
Tactic:
exists inst.map (λ x => ⟨⟨x >>= k₁ >>= k₂, x >>= (flip bind k₂ ∘ k₁)⟩, by exists x⟩) f
State after:
case refl.refl.free.a.a
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y z : Free F T
f : F (Free F R)
P : Free F T → Free F T → Prop := fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z
⊢ (fun x => (↑x).fst) <$>
        (fun x =>
            { val := (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁),
              property :=
                (_ :
                  ∃ x_1,
                    x_1 >>= k₁ >>= k₂ = (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁).fst ∧
                      x_1 >>= flip bind k₂ ∘ k₁ = (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁).snd) }) <$>
          f =
      (flip bind k₂ ∘ flip bind k₁) <$> f ∧
    (fun x => (↑x).snd) <$>
        (fun x =>
            { val := (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁),
              property :=
                (_ :
                  ∃ x_1,
                    x_1 >>= k₁ >>= k₂ = (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁).fst ∧
                      x_1 >>= flip bind k₂ ∘ k₁ = (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁).snd) }) <$>
          f =
      flip bind (flip bind k₂ ∘ k₁) <$> f

State before:
case refl.refl.free.a.a
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y z : Free F T
f : F (Free F R)
P : Free F T → Free F T → Prop := fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z
⊢ (fun x => (↑x).fst) <$>
        (fun x =>
            { val := (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁),
              property :=
                (_ :
                  ∃ x_1,
                    x_1 >>= k₁ >>= k₂ = (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁).fst ∧
                      x_1 >>= flip bind k₂ ∘ k₁ = (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁).snd) }) <$>
          f =
      (flip bind k₂ ∘ flip bind k₁) <$> f ∧
    (fun x => (↑x).snd) <$>
        (fun x =>
            { val := (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁),
              property :=
                (_ :
                  ∃ x_1,
                    x_1 >>= k₁ >>= k₂ = (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁).fst ∧
                      x_1 >>= flip bind k₂ ∘ k₁ = (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁).snd) }) <$>
          f =
      flip bind (flip bind k₂ ∘ k₁) <$> f
Tactic:
simp only [←QPF.map_comp]
State after:
case refl.refl.free.a.a
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y z : Free F T
f : F (Free F R)
P : Free F T → Free F T → Prop := fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z
⊢ ((fun x => (↑x).fst) ∘ fun x =>
          { val := (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁),
            property :=
              (_ :
                ∃ x_1,
                  x_1 >>= k₁ >>= k₂ = (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁).fst ∧
                    x_1 >>= flip bind k₂ ∘ k₁ = (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁).snd) }) <$>
        f =
      (flip bind k₂ ∘ flip bind k₁) <$> f ∧
    ((fun x => (↑x).snd) ∘ fun x =>
          { val := (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁),
            property :=
              (_ :
                ∃ x_1,
                  x_1 >>= k₁ >>= k₂ = (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁).fst ∧
                    x_1 >>= flip bind k₂ ∘ k₁ = (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁).snd) }) <$>
        f =
      flip bind (flip bind k₂ ∘ k₁) <$> f

State before:
case refl.refl.free.a.a
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y z : Free F T
f : F (Free F R)
P : Free F T → Free F T → Prop := fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z
⊢ ((fun x => (↑x).fst) ∘ fun x =>
          { val := (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁),
            property :=
              (_ :
                ∃ x_1,
                  x_1 >>= k₁ >>= k₂ = (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁).fst ∧
                    x_1 >>= flip bind k₂ ∘ k₁ = (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁).snd) }) <$>
        f =
      (flip bind k₂ ∘ flip bind k₁) <$> f ∧
    ((fun x => (↑x).snd) ∘ fun x =>
          { val := (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁),
            property :=
              (_ :
                ∃ x_1,
                  x_1 >>= k₁ >>= k₂ = (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁).fst ∧
                    x_1 >>= flip bind k₂ ∘ k₁ = (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁).snd) }) <$>
        f =
      flip bind (flip bind k₂ ∘ k₁) <$> f
Tactic:
constructor
State after:
case refl.refl.free.a.a.left
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y z : Free F T
f : F (Free F R)
P : Free F T → Free F T → Prop := fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z
⊢ ((fun x => (↑x).fst) ∘ fun x =>
        { val := (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁),
          property :=
            (_ :
              ∃ x_1,
                x_1 >>= k₁ >>= k₂ = (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁).fst ∧
                  x_1 >>= flip bind k₂ ∘ k₁ = (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁).snd) }) <$>
      f =
    (flip bind k₂ ∘ flip bind k₁) <$> f

case refl.refl.free.a.a.right
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y z : Free F T
f : F (Free F R)
P : Free F T → Free F T → Prop := fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z
⊢ ((fun x => (↑x).snd) ∘ fun x =>
        { val := (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁),
          property :=
            (_ :
              ∃ x_1,
                x_1 >>= k₁ >>= k₂ = (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁).fst ∧
                  x_1 >>= flip bind k₂ ∘ k₁ = (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁).snd) }) <$>
      f =
    flip bind (flip bind k₂ ∘ k₁) <$> f

State before:
case refl.refl.free.a.a.left
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y z : Free F T
f : F (Free F R)
P : Free F T → Free F T → Prop := fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z
⊢ ((fun x => (↑x).fst) ∘ fun x =>
        { val := (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁),
          property :=
            (_ :
              ∃ x_1,
                x_1 >>= k₁ >>= k₂ = (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁).fst ∧
                  x_1 >>= flip bind k₂ ∘ k₁ = (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁).snd) }) <$>
      f =
    (flip bind k₂ ∘ flip bind k₁) <$> f

case refl.refl.free.a.a.right
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y z : Free F T
f : F (Free F R)
P : Free F T → Free F T → Prop := fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z
⊢ ((fun x => (↑x).snd) ∘ fun x =>
        { val := (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁),
          property :=
            (_ :
              ∃ x_1,
                x_1 >>= k₁ >>= k₂ = (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁).fst ∧
                  x_1 >>= flip bind k₂ ∘ k₁ = (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁).snd) }) <$>
      f =
    flip bind (flip bind k₂ ∘ k₁) <$> f
Tactic:
. constructor
State after:
case refl.refl.free.a.a.right
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y z : Free F T
f : F (Free F R)
P : Free F T → Free F T → Prop := fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z
⊢ ((fun x => (↑x).snd) ∘ fun x =>
        { val := (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁),
          property :=
            (_ :
              ∃ x_1,
                x_1 >>= k₁ >>= k₂ = (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁).fst ∧
                  x_1 >>= flip bind k₂ ∘ k₁ = (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁).snd) }) <$>
      f =
    flip bind (flip bind k₂ ∘ k₁) <$> f

State before:
case refl.refl.free.a.a.right
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y z : Free F T
f : F (Free F R)
P : Free F T → Free F T → Prop := fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z
⊢ ((fun x => (↑x).snd) ∘ fun x =>
        { val := (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁),
          property :=
            (_ :
              ∃ x_1,
                x_1 >>= k₁ >>= k₂ = (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁).fst ∧
                  x_1 >>= flip bind k₂ ∘ k₁ = (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁).snd) }) <$>
      f =
    flip bind (flip bind k₂ ∘ k₁) <$> f
Tactic:
. constructor
State after:
no goals

State before:
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y z : Free F T
f : F (Free F R)
P : Free F T → Free F T → Prop := fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z
x : Free F R
⊢ P (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁).fst (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁).snd
Tactic:
exists x
State after:
no goals

State before:
case refl.refl.free.a.a.left
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y z : Free F T
f : F (Free F R)
P : Free F T → Free F T → Prop := fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z
⊢ ((fun x => (↑x).fst) ∘ fun x =>
        { val := (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁),
          property :=
            (_ :
              ∃ x_1,
                x_1 >>= k₁ >>= k₂ = (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁).fst ∧
                  x_1 >>= flip bind k₂ ∘ k₁ = (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁).snd) }) <$>
      f =
    (flip bind k₂ ∘ flip bind k₁) <$> f
Tactic:
constructor
State after:
no goals

State before:
case refl.refl.free.a.a.right
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y z : Free F T
f : F (Free F R)
P : Free F T → Free F T → Prop := fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z
⊢ ((fun x => (↑x).snd) ∘ fun x =>
        { val := (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁),
          property :=
            (_ :
              ∃ x_1,
                x_1 >>= k₁ >>= k₂ = (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁).fst ∧
                  x_1 >>= flip bind k₂ ∘ k₁ = (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁).snd) }) <$>
      f =
    flip bind (flip bind k₂ ∘ k₁) <$> f
Tactic:
constructor
State after:
no goals