internlm/Lean-Github huggingface dataset:
Theorem: Free.bind_bind.internal
Proof 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₂)
Proof 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₂)
Theorem: Free.bind_bind.internal
Proof 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
Proof 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₂)
Theorem: Free.bind_bind.internal
Proof 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
Proof state after:
no goals
Theorem: Free.bind_bind.internal
Proof 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]
Proof 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))
Theorem: Free.bind_bind.internal
Proof 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)
Proof 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))
Theorem: Free.bind_bind.internal
Proof 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
Proof 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))
Theorem: Free.bind_bind.internal
Proof 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
Proof 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))
Theorem: Free.bind_bind.internal
Proof 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
Proof state after:
no goals
Theorem: Free.bind_bind.internal
Proof 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
Proof 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
Theorem: Free.bind_bind.internal
Proof 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
Proof 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
Theorem: Free.bind_bind.internal
Proof 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
Proof state after:
no goals
Theorem: Free.bind_bind.internal
Proof 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
Proof 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)
Theorem: Free.bind_bind.internal
Proof 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
Proof 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
Theorem: Free.bind_bind.internal
Proof 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]
Proof 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
Theorem: Free.bind_bind.internal
Proof 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
Proof 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
Theorem: Free.bind_bind.internal
Proof 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
Proof 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
Theorem: Free.bind_bind.internal
Proof 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
Proof state after:
no goals
Theorem: Free.bind_bind.internal
Proof 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
Proof state after:
no goals
Theorem: Free.bind_bind.internal
Proof 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
Proof state after:
no goals
Theorem: Free.bind_bind.internal
Proof 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
Proof state after:
no goals
Theorem: Free.bind_bind
Proof 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₁))
Proof 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₁
Theorem: Free.bind_bind
Proof 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₁))
Proof 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₁
Theorem: Free.bind_bind
Proof 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₂
Proof 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₁)
Theorem: Free.bind_bind
Proof 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₁
Proof 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₁