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

State before:
F : Type u → Type u
inst : QPF F
R S T : Type u
t : Free F R
k₁ : R → Free F S
k₂ : S → Free F T
⊢ t >>= k₁ >>= k₂ = t >>= flip bind k₂ ∘ k₁
Tactic:
have h₁ := bind_bind.internal k₁ k₂ (t >>= k₁ >>= k₂) (t >>= (flip bind k₂ ∘ k₁))
State after:
F : Type u → Type u
inst : QPF F
R S T : Type u
t : Free F R
k₁ : R → Free F S
k₂ : S → Free F T
h₁ :
  (fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z) (t >>= k₁ >>= k₂) (t >>= flip bind k₂ ∘ k₁) ≤
    eq (t >>= k₁ >>= k₂) (t >>= flip bind k₂ ∘ k₁)
⊢ t >>= k₁ >>= k₂ = t >>= flip bind k₂ ∘ k₁

State before:
F : Type u → Type u
inst : QPF F
R S T : Type u
t : Free F R
k₁ : R → Free F S
k₂ : S → Free F T
h₁ :
  (fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z) (t >>= k₁ >>= k₂) (t >>= flip bind k₂ ∘ k₁) ≤
    eq (t >>= k₁ >>= k₂) (t >>= flip bind k₂ ∘ k₁)
⊢ t >>= k₁ >>= k₂ = t >>= flip bind k₂ ∘ k₁
Tactic:
have h₂ := Free.eq.bisim (t >>= k₁ >>= k₂) (t >>= (flip bind k₂ ∘ k₁))
State after:
F : Type u → Type u
inst : QPF F
R S T : Type u
t : Free F R
k₁ : R → Free F S
k₂ : S → Free F T
h₁ :
  (fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z) (t >>= k₁ >>= k₂) (t >>= flip bind k₂ ∘ k₁) ≤
    eq (t >>= k₁ >>= k₂) (t >>= flip bind k₂ ∘ k₁)
h₂ : eq (t >>= k₁ >>= k₂) (t >>= flip bind k₂ ∘ k₁) → t >>= k₁ >>= k₂ = t >>= flip bind k₂ ∘ k₁
⊢ t >>= k₁ >>= k₂ = t >>= flip bind k₂ ∘ k₁

State before:
F : Type u → Type u
inst : QPF F
R S T : Type u
t : Free F R
k₁ : R → Free F S
k₂ : S → Free F T
h₁ :
  (fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z) (t >>= k₁ >>= k₂) (t >>= flip bind k₂ ∘ k₁) ≤
    eq (t >>= k₁ >>= k₂) (t >>= flip bind k₂ ∘ k₁)
h₂ : eq (t >>= k₁ >>= k₂) (t >>= flip bind k₂ ∘ k₁) → t >>= k₁ >>= k₂ = t >>= flip bind k₂ ∘ k₁
⊢ t >>= k₁ >>= k₂ = t >>= flip bind k₂ ∘ k₁
Tactic:
apply h₂
State after:
F : Type u → Type u
inst : QPF F
R S T : Type u
t : Free F R
k₁ : R → Free F S
k₂ : S → Free F T
h₁ :
  (fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z) (t >>= k₁ >>= k₂) (t >>= flip bind k₂ ∘ k₁) ≤
    eq (t >>= k₁ >>= k₂) (t >>= flip bind k₂ ∘ k₁)
h₂ : eq (t >>= k₁ >>= k₂) (t >>= flip bind k₂ ∘ k₁) → t >>= k₁ >>= k₂ = t >>= flip bind k₂ ∘ k₁
⊢ eq (t >>= k₁ >>= k₂) (t >>= flip bind k₂ ∘ k₁)

State before:
F : Type u → Type u
inst : QPF F
R S T : Type u
t : Free F R
k₁ : R → Free F S
k₂ : S → Free F T
h₁ :
  (fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z) (t >>= k₁ >>= k₂) (t >>= flip bind k₂ ∘ k₁) ≤
    eq (t >>= k₁ >>= k₂) (t >>= flip bind k₂ ∘ k₁)
h₂ : eq (t >>= k₁ >>= k₂) (t >>= flip bind k₂ ∘ k₁) → t >>= k₁ >>= k₂ = t >>= flip bind k₂ ∘ k₁
⊢ eq (t >>= k₁ >>= k₂) (t >>= flip bind k₂ ∘ k₁)
Tactic:
apply h₁
State after:
F : Type u → Type u
inst : QPF F
R S T : Type u
t : Free F R
k₁ : R → Free F S
k₂ : S → Free F T
h₁ :
  (fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z) (t >>= k₁ >>= k₂) (t >>= flip bind k₂ ∘ k₁) ≤
    eq (t >>= k₁ >>= k₂) (t >>= flip bind k₂ ∘ k₁)
h₂ : eq (t >>= k₁ >>= k₂) (t >>= flip bind k₂ ∘ k₁) → t >>= k₁ >>= k₂ = t >>= flip bind k₂ ∘ k₁
⊢ ∃ x, x >>= k₁ >>= k₂ = t >>= k₁ >>= k₂ ∧ x >>= flip bind k₂ ∘ k₁ = t >>= flip bind k₂ ∘ k₁

State before:
F : Type u → Type u
inst : QPF F
R S T : Type u
t : Free F R
k₁ : R → Free F S
k₂ : S → Free F T
h₁ :
  (fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z) (t >>= k₁ >>= k₂) (t >>= flip bind k₂ ∘ k₁) ≤
    eq (t >>= k₁ >>= k₂) (t >>= flip bind k₂ ∘ k₁)
h₂ : eq (t >>= k₁ >>= k₂) (t >>= flip bind k₂ ∘ k₁) → t >>= k₁ >>= k₂ = t >>= flip bind k₂ ∘ k₁
⊢ ∃ x, x >>= k₁ >>= k₂ = t >>= k₁ >>= k₂ ∧ x >>= flip bind k₂ ∘ k₁ = t >>= flip bind k₂ ∘ k₁
Tactic:
exists t
State after:
no goals