internlm/Lean-Github huggingface dataset:
Theorem: Free.bind_pure.internal
Proof state before:
case h₀.refl
F : Type u → Type u
inst : QPF F
R : Type u
x y : QPF.M (FreeF F R)
⊢ (fun x => (↑x).fst) <$>
        (fun x =>
            { val := (x, x >>= pure),
              property := (_ : (x, x >>= pure).fst >>= pure = (x, x >>= pure).fst >>= pure) }) <$>
          destruct x =
      QPF.M.destruct x ∧
    (fun x => (↑x).snd) <$>
        (fun x =>
            { val := (x, x >>= pure),
              property := (_ : (x, x >>= pure).fst >>= pure = (x, x >>= pure).fst >>= pure) }) <$>
          destruct x =
      QPF.M.destruct (x >>= pure)
Tactic:
cases x using by_cases with
| pure r =>
  have : destruct (pure r) = .Pure r := by
    exact @destruct_construct F _ R (FreeF.Pure r)
  simp only [Functor.map, this, pure_bind r]
  constructor <;> rfl
| free f =>
  have : destruct (free f) = .Free f := by
    exact @destruct_construct F _ R (FreeF.Free f)
  simp only [Functor.map, this, free_bind, ←QPF.map_comp, Function.comp]
  constructor
  . conv =>
      rhs
      congr
      rw [←QPF.map_id f]
    rw [free, construct, QPF.M.destruct_construct]
    rfl
  . simp only [free, construct, QPF.M.destruct_construct]
    rfl
Proof state after:
no goals
Theorem: Free.bind_pure.internal
Proof state before:
F : Type u → Type u
inst : QPF F
R : Type u
x✝ y x : QPF.M (FreeF F R)
⊢ (fun x y => x >>= pure = y) (x, x >>= pure).fst (x, x >>= pure).snd
Tactic:
rfl
Proof state after:
no goals
Theorem: Free.bind_pure.internal
Proof state before:
case h₀.refl.pure
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
r : R
⊢ (fun x => (↑x).fst) <$>
        (fun x =>
            { val := (x, x >>= pure),
              property := (_ : (x, x >>= pure).fst >>= pure = (x, x >>= pure).fst >>= pure) }) <$>
          destruct (pure r) =
      QPF.M.destruct (pure r) ∧
    (fun x => (↑x).snd) <$>
        (fun x =>
            { val := (x, x >>= pure),
              property := (_ : (x, x >>= pure).fst >>= pure = (x, x >>= pure).fst >>= pure) }) <$>
          destruct (pure r) =
      QPF.M.destruct (pure r >>= pure)
Tactic:
have : destruct (pure r) = .Pure r := by
  exact @destruct_construct F _ R (FreeF.Pure r)
Proof state after:
case h₀.refl.pure
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
r : R
this : destruct (pure r) = FreeF.Pure r
⊢ (fun x => (↑x).fst) <$>
        (fun x =>
            { val := (x, x >>= pure),
              property := (_ : (x, x >>= pure).fst >>= pure = (x, x >>= pure).fst >>= pure) }) <$>
          destruct (pure r) =
      QPF.M.destruct (pure r) ∧
    (fun x => (↑x).snd) <$>
        (fun x =>
            { val := (x, x >>= pure),
              property := (_ : (x, x >>= pure).fst >>= pure = (x, x >>= pure).fst >>= pure) }) <$>
          destruct (pure r) =
      QPF.M.destruct (pure r >>= pure)
Theorem: Free.bind_pure.internal
Proof state before:
case h₀.refl.pure
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
r : R
this : destruct (pure r) = FreeF.Pure r
⊢ (fun x => (↑x).fst) <$>
        (fun x =>
            { val := (x, x >>= pure),
              property := (_ : (x, x >>= pure).fst >>= pure = (x, x >>= pure).fst >>= pure) }) <$>
          destruct (pure r) =
      QPF.M.destruct (pure r) ∧
    (fun x => (↑x).snd) <$>
        (fun x =>
            { val := (x, x >>= pure),
              property := (_ : (x, x >>= pure).fst >>= pure = (x, x >>= pure).fst >>= pure) }) <$>
          destruct (pure r) =
      QPF.M.destruct (pure r >>= pure)
Tactic:
simp only [Functor.map, this, pure_bind r]
Proof state after:
case h₀.refl.pure
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
r : R
this : destruct (pure r) = FreeF.Pure r
⊢ FreeF.Pure r = QPF.M.destruct (pure r) ∧ FreeF.Pure r = QPF.M.destruct (pure r)
Theorem: Free.bind_pure.internal
Proof state before:
case h₀.refl.pure
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
r : R
this : destruct (pure r) = FreeF.Pure r
⊢ FreeF.Pure r = QPF.M.destruct (pure r) ∧ FreeF.Pure r = QPF.M.destruct (pure r)
Tactic:
constructor <;> rfl
Proof state after:
no goals
Theorem: Free.bind_pure.internal
Proof state before:
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
r : R
⊢ destruct (pure r) = FreeF.Pure r
Tactic:
exact @destruct_construct F _ R (FreeF.Pure r)
Proof state after:
no goals
Theorem: Free.bind_pure.internal
Proof state before:
case h₀.refl.free
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
f : F (Free F R)
⊢ (fun x => (↑x).fst) <$>
        (fun x =>
            { val := (x, x >>= pure),
              property := (_ : (x, x >>= pure).fst >>= pure = (x, x >>= pure).fst >>= pure) }) <$>
          destruct (free f) =
      QPF.M.destruct (free f) ∧
    (fun x => (↑x).snd) <$>
        (fun x =>
            { val := (x, x >>= pure),
              property := (_ : (x, x >>= pure).fst >>= pure = (x, x >>= pure).fst >>= pure) }) <$>
          destruct (free f) =
      QPF.M.destruct (free f >>= pure)
Tactic:
have : destruct (free f) = .Free f := by
  exact @destruct_construct F _ R (FreeF.Free f)
Proof state after:
case h₀.refl.free
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
f : F (Free F R)
this : destruct (free f) = FreeF.Free f
⊢ (fun x => (↑x).fst) <$>
        (fun x =>
            { val := (x, x >>= pure),
              property := (_ : (x, x >>= pure).fst >>= pure = (x, x >>= pure).fst >>= pure) }) <$>
          destruct (free f) =
      QPF.M.destruct (free f) ∧
    (fun x => (↑x).snd) <$>
        (fun x =>
            { val := (x, x >>= pure),
              property := (_ : (x, x >>= pure).fst >>= pure = (x, x >>= pure).fst >>= pure) }) <$>
          destruct (free f) =
      QPF.M.destruct (free f >>= pure)
Theorem: Free.bind_pure.internal
Proof state before:
case h₀.refl.free
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
f : F (Free F R)
this : destruct (free f) = FreeF.Free f
⊢ (fun x => (↑x).fst) <$>
        (fun x =>
            { val := (x, x >>= pure),
              property := (_ : (x, x >>= pure).fst >>= pure = (x, x >>= pure).fst >>= pure) }) <$>
          destruct (free f) =
      QPF.M.destruct (free f) ∧
    (fun x => (↑x).snd) <$>
        (fun x =>
            { val := (x, x >>= pure),
              property := (_ : (x, x >>= pure).fst >>= pure = (x, x >>= pure).fst >>= pure) }) <$>
          destruct (free f) =
      QPF.M.destruct (free f >>= pure)
Tactic:
simp only [Functor.map, this, free_bind, ←QPF.map_comp, Function.comp]
Proof state after:
case h₀.refl.free
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
f : F (Free F R)
this : destruct (free f) = FreeF.Free f
⊢ FreeF.Free ((fun x => x) <$> f) = QPF.M.destruct (free f) ∧
    FreeF.Free ((fun x => x >>= pure) <$> f) = QPF.M.destruct (free (flip bind pure <$> f))
Theorem: Free.bind_pure.internal
Proof state before:
case h₀.refl.free
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
f : F (Free F R)
this : destruct (free f) = FreeF.Free f
⊢ FreeF.Free ((fun x => x) <$> f) = QPF.M.destruct (free f) ∧
    FreeF.Free ((fun x => x >>= pure) <$> f) = QPF.M.destruct (free (flip bind pure <$> f))
Tactic:
constructor
Proof state after:
case h₀.refl.free.left
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
f : F (Free F R)
this : destruct (free f) = FreeF.Free f
⊢ FreeF.Free ((fun x => x) <$> f) = QPF.M.destruct (free f)

case h₀.refl.free.right
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
f : F (Free F R)
this : destruct (free f) = FreeF.Free f
⊢ FreeF.Free ((fun x => x >>= pure) <$> f) = QPF.M.destruct (free (flip bind pure <$> f))
Theorem: Free.bind_pure.internal
Proof state before:
case h₀.refl.free.left
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
f : F (Free F R)
this : destruct (free f) = FreeF.Free f
⊢ FreeF.Free ((fun x => x) <$> f) = QPF.M.destruct (free f)

case h₀.refl.free.right
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
f : F (Free F R)
this : destruct (free f) = FreeF.Free f
⊢ FreeF.Free ((fun x => x >>= pure) <$> f) = QPF.M.destruct (free (flip bind pure <$> f))
Tactic:
. conv =>
    rhs
    congr
    rw [←QPF.map_id f]
  rw [free, construct, QPF.M.destruct_construct]
  rfl
Proof state after:
case h₀.refl.free.right
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
f : F (Free F R)
this : destruct (free f) = FreeF.Free f
⊢ FreeF.Free ((fun x => x >>= pure) <$> f) = QPF.M.destruct (free (flip bind pure <$> f))
Theorem: Free.bind_pure.internal
Proof state before:
case h₀.refl.free.right
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
f : F (Free F R)
this : destruct (free f) = FreeF.Free f
⊢ FreeF.Free ((fun x => x >>= pure) <$> f) = QPF.M.destruct (free (flip bind pure <$> f))
Tactic:
. simp only [free, construct, QPF.M.destruct_construct]
  rfl
Proof state after:
no goals
Theorem: Free.bind_pure.internal
Proof state before:
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
f : F (Free F R)
⊢ destruct (free f) = FreeF.Free f
Tactic:
exact @destruct_construct F _ R (FreeF.Free f)
Proof state after:
no goals
Theorem: Free.bind_pure.internal
Proof state before:
case h₀.refl.free.left
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
f : F (Free F R)
this : destruct (free f) = FreeF.Free f
⊢ FreeF.Free ((fun x => x) <$> f) = QPF.M.destruct (free f)
Tactic:
conv =>
  rhs
  congr
  rw [←QPF.map_id f]
Proof state after:
case h₀.refl.free.left
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
f : F (Free F R)
this : destruct (free f) = FreeF.Free f
⊢ FreeF.Free ((fun x => x) <$> f) = QPF.M.destruct (free (id <$> f))
Theorem: Free.bind_pure.internal
Proof state before:
case h₀.refl.free.left
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
f : F (Free F R)
this : destruct (free f) = FreeF.Free f
⊢ FreeF.Free ((fun x => x) <$> f) = QPF.M.destruct (free (id <$> f))
Tactic:
rw [free, construct, QPF.M.destruct_construct]
Proof state after:
case h₀.refl.free.left
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
f : F (Free F R)
this : destruct (free f) = FreeF.Free f
⊢ FreeF.Free ((fun x => x) <$> f) = FreeF.Free (id <$> f)
Theorem: Free.bind_pure.internal
Proof state before:
case h₀.refl.free.left
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
f : F (Free F R)
this : destruct (free f) = FreeF.Free f
⊢ FreeF.Free ((fun x => x) <$> f) = FreeF.Free (id <$> f)
Tactic:
rfl
Proof state after:
no goals
Theorem: Free.bind_pure.internal
Proof state before:
case h₀.refl.free.right
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
f : F (Free F R)
this : destruct (free f) = FreeF.Free f
⊢ FreeF.Free ((fun x => x >>= pure) <$> f) = QPF.M.destruct (free (flip bind pure <$> f))
Tactic:
simp only [free, construct, QPF.M.destruct_construct]
Proof state after:
case h₀.refl.free.right
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
f : F (Free F R)
this : destruct (free f) = FreeF.Free f
⊢ FreeF.Free ((fun x => x >>= pure) <$> f) = FreeF.Free (flip bind pure <$> f)
Theorem: Free.bind_pure.internal
Proof state before:
case h₀.refl.free.right
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
f : F (Free F R)
this : destruct (free f) = FreeF.Free f
⊢ FreeF.Free ((fun x => x >>= pure) <$> f) = FreeF.Free (flip bind pure <$> f)
Tactic:
rfl
Proof state after:
no goals
Theorem: Free.bind_pure
Proof state before:
F : Type u → Type u
inst : QPF F
R : Type u
x : Free F R
⊢ x >>= pure = x
Tactic:
conv =>
  rhs
  rw [bind_pure.internal x (bind x pure)]
  rfl
  rfl
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
⊢ (fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z) ≤ eq
Tactic:
simp only [Free.eq, Free.eqP, pgfp.coinduction]
Proof 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)
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
⊢ (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₂⟩
Proof 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
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
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₁
Proof 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
Theorem: Free.bind_bind.internal
Proof 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₂
Proof 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₁)
Theorem: Free.bind_bind.internal
Proof 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
Proof state after:
no goals
Theorem: Free.bind_bind.internal
Proof 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]
Proof 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₂)
Theorem: Free.bind_bind.internal
Proof 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
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
⊢ 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₂)
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
⊢ 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
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
⊢ 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
⊢ 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
Proof state after:
no goals
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
⊢ 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
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
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
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
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
Proof 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
Theorem: Free.bind_bind.internal
Proof 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⟩ ⊥
Proof 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
Theorem: Free.bind_bind.internal
Proof 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
Proof 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
Theorem: Free.bind_bind.internal
Proof 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
Proof state after:
no goals
Theorem: Free.bind_bind.internal
Proof 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
Proof 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
Theorem: Free.bind_bind.internal
Proof 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
Proof state after:
no goals
Theorem: Free.bind_bind.internal
Proof 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
Proof state after:
no goals