internlm/Lean-Github huggingface dataset:
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₁
⊢ ∃ x, x >>= k₁ >>= k₂ = t >>= k₁ >>= k₂ ∧ x >>= flip bind k₂ ∘ k₁ = t >>= flip bind k₂ ∘ k₁
Tactic:
exists t
Proof state after:
no goals
Theorem: Free.equiv.coinduction
Proof state before:
C : _root_.Container
R S : Type u₁
eq : R → S → Prop
P : Free C R → Free C S → Prop
⊢ (∀ (x : Free C R) (y : Free C S), P x y → equivF eq (P ⊔ pequiv eq P) x y) →
    ∀ (x : Free C R) (y : Free C S), P x y → equiv eq x y
Tactic:
intro h x y h'
Proof state after:
C : _root_.Container
R S : Type u₁
eq : R → S → Prop
P : Free C R → Free C S → Prop
h : ∀ (x : Free C R) (y : Free C S), P x y → equivF eq (P ⊔ pequiv eq P) x y
x : Free C R
y : Free C S
h' : P x y
⊢ equiv eq x y
Theorem: Free.equiv.coinduction
Proof state before:
C : _root_.Container
R S : Type u₁
eq : R → S → Prop
P : Free C R → Free C S → Prop
h : ∀ (x : Free C R) (y : Free C S), P x y → equivF eq (P ⊔ pequiv eq P) x y
x : Free C R
y : Free C S
h' : P x y
⊢ equiv eq x y
Tactic:
apply (pgfp.coinduction (equivF' eq) P).2
Proof state after:
case a
C : _root_.Container
R S : Type u₁
eq : R → S → Prop
P : Free C R → Free C S → Prop
h : ∀ (x : Free C R) (y : Free C S), P x y → equivF eq (P ⊔ pequiv eq P) x y
x : Free C R
y : Free C S
h' : P x y
⊢ P ≤ ↑(equivF' eq) (P ⊔ ↑(pgfp (equivF' eq)) P)

case a
C : _root_.Container
R S : Type u₁
eq : R → S → Prop
P : Free C R → Free C S → Prop
h : ∀ (x : Free C R) (y : Free C S), P x y → equivF eq (P ⊔ pequiv eq P) x y
x : Free C R
y : Free C S
h' : P x y
⊢ P x y
Theorem: Free.equiv.coinduction
Proof state before:
case a
C : _root_.Container
R S : Type u₁
eq : R → S → Prop
P : Free C R → Free C S → Prop
h : ∀ (x : Free C R) (y : Free C S), P x y → equivF eq (P ⊔ pequiv eq P) x y
x : Free C R
y : Free C S
h' : P x y
⊢ P ≤ ↑(equivF' eq) (P ⊔ ↑(pgfp (equivF' eq)) P)

case a
C : _root_.Container
R S : Type u₁
eq : R → S → Prop
P : Free C R → Free C S → Prop
h : ∀ (x : Free C R) (y : Free C S), P x y → equivF eq (P ⊔ pequiv eq P) x y
x : Free C R
y : Free C S
h' : P x y
⊢ P x y
Tactic:
apply h
Proof state after:
case a
C : _root_.Container
R S : Type u₁
eq : R → S → Prop
P : Free C R → Free C S → Prop
h : ∀ (x : Free C R) (y : Free C S), P x y → equivF eq (P ⊔ pequiv eq P) x y
x : Free C R
y : Free C S
h' : P x y
⊢ P x y
Theorem: Free.equiv.coinduction
Proof state before:
case a
C : _root_.Container
R S : Type u₁
eq : R → S → Prop
P : Free C R → Free C S → Prop
h : ∀ (x : Free C R) (y : Free C S), P x y → equivF eq (P ⊔ pequiv eq P) x y
x : Free C R
y : Free C S
h' : P x y
⊢ P x y
Tactic:
apply h'
Proof state after:
no goals
Theorem: Free.eq.bisim
Proof state before:
C : _root_.Container
R : Type u₁
⊢ ∀ (x y : Free C R), eq x y → x = y
Tactic:
apply M.bisim
Proof state after:
case h₀
C : _root_.Container
R : Type u₁
⊢ ∀ (x y : M (Container C R)),
    eq x y →
      ∃ node k₁ k₂,
        M.destruct x = { fst := node, snd := k₁ } ∧
          M.destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : Container.B (Container C R) node), eq (k₁ i) (k₂ i)
Theorem: Free.eq.bisim
Proof state before:
case h₀
C : _root_.Container
R : Type u₁
⊢ ∀ (x y : M (Container C R)),
    eq x y →
      ∃ node k₁ k₂,
        M.destruct x = { fst := node, snd := k₁ } ∧
          M.destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : Container.B (Container C R) node), eq (k₁ i) (k₂ i)
Tactic:
intro x y h₁
Proof state after:
case h₀
C : _root_.Container
R : Type u₁
x y : M (Container C R)
h₁ : eq x y
⊢ ∃ node k₁ k₂,
    M.destruct x = { fst := node, snd := k₁ } ∧
      M.destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : Container.B (Container C R) node), eq (k₁ i) (k₂ i)
Theorem: Free.eq.bisim
Proof state before:
case h₀
C : _root_.Container
R : Type u₁
x y : M (Container C R)
h₁ : eq x y
⊢ ∃ node k₁ k₂,
    M.destruct x = { fst := node, snd := k₁ } ∧
      M.destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : Container.B (Container C R) node), eq (k₁ i) (k₂ i)
Tactic:
simp [eq, equiv, pequiv] at h₁
Proof state after:
case h₀
C : _root_.Container
R : Type u₁
x y : M (Container C R)
h₁ : ↑(pgfp (equivF' Eq)) ⊥ x y
⊢ ∃ node k₁ k₂,
    M.destruct x = { fst := node, snd := k₁ } ∧
      M.destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : Container.B (Container C R) node), eq (k₁ i) (k₂ i)
Theorem: Free.eq.bisim
Proof state before:
case h₀
C : _root_.Container
R : Type u₁
x y : M (Container C R)
h₁ : ↑(pgfp (equivF' Eq)) ⊥ x y
⊢ ∃ node k₁ k₂,
    M.destruct x = { fst := node, snd := k₁ } ∧
      M.destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : Container.B (Container C R) node), eq (k₁ i) (k₂ i)
Tactic:
rw [←pgfp.unfold] at h₁
Proof state after:
case h₀
C : _root_.Container
R : Type u₁
x y : M (Container C R)
h₁ : ↑(equivF' Eq) (⊥ ⊔ ↑(pgfp (equivF' Eq)) ⊥) x y
⊢ ∃ node k₁ k₂,
    M.destruct x = { fst := node, snd := k₁ } ∧
      M.destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : Container.B (Container C R) node), eq (k₁ i) (k₂ i)
Theorem: Free.eq.bisim
Proof state before:
case h₀
C : _root_.Container
R : Type u₁
x y : M (Container C R)
h₁ : ↑(equivF' Eq) (⊥ ⊔ ↑(pgfp (equivF' Eq)) ⊥) x y
⊢ ∃ node k₁ k₂,
    M.destruct x = { fst := node, snd := k₁ } ∧
      M.destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : Container.B (Container C R) node), eq (k₁ i) (k₂ i)
Tactic:
cases h₁ with
| Pure x y h₁ =>
  induction h₁
  exists (A.Pure x)
  exists (λ e => e.casesOn)
  exists (λ e => e.casesOn)
  simp only [construct, M.destruct_construct, inv, true_and]
  intro x
  apply x.elim
| Free node k₁ k₂ h =>
  exists (A.Free node)
  exists k₁
  exists k₂
  simp only [construct, M.destruct_construct, inv, true_and]
  intro x
  rw [CompleteLattice.bot_sup] at h
  apply h
Proof state after:
no goals
Theorem: Free.eq.bisim
Proof state before:
case h₀.Pure
C : _root_.Container
R : Type u₁
x y : R
h₁ : x = y
⊢ ∃ node k₁ k₂,
    M.destruct (construct (Functor.Pure x)) = { fst := node, snd := k₁ } ∧
      M.destruct (construct (Functor.Pure y)) = { fst := node, snd := k₂ } ∧
        ∀ (i : Container.B (Container C R) node), eq (k₁ i) (k₂ i)
Tactic:
induction h₁
Proof state after:
case h₀.Pure.refl
C : _root_.Container
R : Type u₁
x y : R
⊢ ∃ node k₁ k₂,
    M.destruct (construct (Functor.Pure x)) = { fst := node, snd := k₁ } ∧
      M.destruct (construct (Functor.Pure x)) = { fst := node, snd := k₂ } ∧
        ∀ (i : Container.B (Container C R) node), eq (k₁ i) (k₂ i)
Theorem: Free.eq.bisim
Proof state before:
case h₀.Pure.refl
C : _root_.Container
R : Type u₁
x y : R
⊢ ∃ node k₁ k₂,
    M.destruct (construct (Functor.Pure x)) = { fst := node, snd := k₁ } ∧
      M.destruct (construct (Functor.Pure x)) = { fst := node, snd := k₂ } ∧
        ∀ (i : Container.B (Container C R) node), eq (k₁ i) (k₂ i)
Tactic:
exists (A.Pure x)
Proof state after:
case h₀.Pure.refl
C : _root_.Container
R : Type u₁
x y : R
⊢ ∃ k₁ k₂,
    M.destruct (construct (Functor.Pure x)) = { fst := A.Pure x, snd := k₁ } ∧
      M.destruct (construct (Functor.Pure x)) = { fst := A.Pure x, snd := k₂ } ∧
        ∀ (i : Container.B (Container C R) (A.Pure x)), eq (k₁ i) (k₂ i)
Theorem: Free.eq.bisim
Proof state before:
case h₀.Pure.refl
C : _root_.Container
R : Type u₁
x y : R
⊢ ∃ k₁ k₂,
    M.destruct (construct (Functor.Pure x)) = { fst := A.Pure x, snd := k₁ } ∧
      M.destruct (construct (Functor.Pure x)) = { fst := A.Pure x, snd := k₂ } ∧
        ∀ (i : Container.B (Container C R) (A.Pure x)), eq (k₁ i) (k₂ i)
Tactic:
exists (λ e => e.casesOn)
Proof state after:
case h₀.Pure.refl
C : _root_.Container
R : Type u₁
x y : R
⊢ ∃ k₂,
    M.destruct (construct (Functor.Pure x)) =
        { fst := A.Pure x, snd := fun e => PEmpty.casesOn (fun x => M (Container C R)) e } ∧
      M.destruct (construct (Functor.Pure x)) = { fst := A.Pure x, snd := k₂ } ∧
        ∀ (i : Container.B (Container C R) (A.Pure x)),
          eq ((fun e => PEmpty.casesOn (fun x => M (Container C R)) e) i) (k₂ i)
Theorem: Free.eq.bisim
Proof state before:
case h₀.Pure.refl
C : _root_.Container
R : Type u₁
x y : R
⊢ ∃ k₂,
    M.destruct (construct (Functor.Pure x)) =
        { fst := A.Pure x, snd := fun e => PEmpty.casesOn (fun x => M (Container C R)) e } ∧
      M.destruct (construct (Functor.Pure x)) = { fst := A.Pure x, snd := k₂ } ∧
        ∀ (i : Container.B (Container C R) (A.Pure x)),
          eq ((fun e => PEmpty.casesOn (fun x => M (Container C R)) e) i) (k₂ i)
Tactic:
exists (λ e => e.casesOn)
Proof state after:
case h₀.Pure.refl
C : _root_.Container
R : Type u₁
x y : R
⊢ M.destruct (construct (Functor.Pure x)) =
      { fst := A.Pure x, snd := fun e => PEmpty.casesOn (fun x => M (Container C R)) e } ∧
    M.destruct (construct (Functor.Pure x)) =
        { fst := A.Pure x, snd := fun e => PEmpty.casesOn (fun x => M (Container C R)) e } ∧
      ∀ (i : Container.B (Container C R) (A.Pure x)),
        eq ((fun e => PEmpty.casesOn (fun x => M (Container C R)) e) i)
          ((fun e => PEmpty.casesOn (fun x => M (Container C R)) e) i)
Theorem: Free.eq.bisim
Proof state before:
case h₀.Pure.refl
C : _root_.Container
R : Type u₁
x y : R
⊢ M.destruct (construct (Functor.Pure x)) =
      { fst := A.Pure x, snd := fun e => PEmpty.casesOn (fun x => M (Container C R)) e } ∧
    M.destruct (construct (Functor.Pure x)) =
        { fst := A.Pure x, snd := fun e => PEmpty.casesOn (fun x => M (Container C R)) e } ∧
      ∀ (i : Container.B (Container C R) (A.Pure x)),
        eq ((fun e => PEmpty.casesOn (fun x => M (Container C R)) e) i)
          ((fun e => PEmpty.casesOn (fun x => M (Container C R)) e) i)
Tactic:
simp only [construct, M.destruct_construct, inv, true_and]
Proof state after:
case h₀.Pure.refl
C : _root_.Container
R : Type u₁
x y : R
⊢ ∀ (i : Container.B (Container C R) (A.Pure x)),
    eq (PEmpty.rec (fun x => M (Container C R)) i) (PEmpty.rec (fun x => M (Container C R)) i)
Theorem: Free.eq.bisim
Proof state before:
case h₀.Pure.refl
C : _root_.Container
R : Type u₁
x y : R
⊢ ∀ (i : Container.B (Container C R) (A.Pure x)),
    eq (PEmpty.rec (fun x => M (Container C R)) i) (PEmpty.rec (fun x => M (Container C R)) i)
Tactic:
intro x
Proof state after:
case h₀.Pure.refl
C : _root_.Container
R : Type u₁
x✝ y : R
x : Container.B (Container C R) (A.Pure x✝)
⊢ eq (PEmpty.rec (fun x => M (Container C R)) x) (PEmpty.rec (fun x => M (Container C R)) x)
Theorem: Free.eq.bisim
Proof state before:
case h₀.Pure.refl
C : _root_.Container
R : Type u₁
x✝ y : R
x : Container.B (Container C R) (A.Pure x✝)
⊢ eq (PEmpty.rec (fun x => M (Container C R)) x) (PEmpty.rec (fun x => M (Container C R)) x)
Tactic:
apply x.elim
Proof state after:
no goals
Theorem: Free.eq.bisim
Proof state before:
case h₀.Free
C : _root_.Container
R : Type u₁
node : C.A
k₁ k₂ : Container.B C node → Free C R
h : ∀ (x : Container.B C node), (⊥ ⊔ ↑(pgfp (equivF' Eq)) ⊥) (k₁ x) (k₂ x)
⊢ ∃ node_1 k₁_1 k₂_1,
    M.destruct (construct (Functor.Free node k₁)) = { fst := node_1, snd := k₁_1 } ∧
      M.destruct (construct (Functor.Free node k₂)) = { fst := node_1, snd := k₂_1 } ∧
        ∀ (i : Container.B (Container C R) node_1), eq (k₁_1 i) (k₂_1 i)
Tactic:
exists (A.Free node)
Proof state after:
case h₀.Free
C : _root_.Container
R : Type u₁
node : C.A
k₁ k₂ : Container.B C node → Free C R
h : ∀ (x : Container.B C node), (⊥ ⊔ ↑(pgfp (equivF' Eq)) ⊥) (k₁ x) (k₂ x)
⊢ ∃ k₁_1 k₂_1,
    M.destruct (construct (Functor.Free node k₁)) = { fst := A.Free node, snd := k₁_1 } ∧
      M.destruct (construct (Functor.Free node k₂)) = { fst := A.Free node, snd := k₂_1 } ∧
        ∀ (i : Container.B (Container C R) (A.Free node)), eq (k₁_1 i) (k₂_1 i)
Theorem: Free.eq.bisim
Proof state before:
case h₀.Free
C : _root_.Container
R : Type u₁
node : C.A
k₁ k₂ : Container.B C node → Free C R
h : ∀ (x : Container.B C node), (⊥ ⊔ ↑(pgfp (equivF' Eq)) ⊥) (k₁ x) (k₂ x)
⊢ ∃ k₁_1 k₂_1,
    M.destruct (construct (Functor.Free node k₁)) = { fst := A.Free node, snd := k₁_1 } ∧
      M.destruct (construct (Functor.Free node k₂)) = { fst := A.Free node, snd := k₂_1 } ∧
        ∀ (i : Container.B (Container C R) (A.Free node)), eq (k₁_1 i) (k₂_1 i)
Tactic:
exists k₁
Proof state after:
case h₀.Free
C : _root_.Container
R : Type u₁
node : C.A
k₁ k₂ : Container.B C node → Free C R
h : ∀ (x : Container.B C node), (⊥ ⊔ ↑(pgfp (equivF' Eq)) ⊥) (k₁ x) (k₂ x)
⊢ ∃ k₂_1,
    M.destruct (construct (Functor.Free node k₁)) = { fst := A.Free node, snd := k₁ } ∧
      M.destruct (construct (Functor.Free node k₂)) = { fst := A.Free node, snd := k₂_1 } ∧
        ∀ (i : Container.B (Container C R) (A.Free node)), eq (k₁ i) (k₂_1 i)
Theorem: Free.eq.bisim
Proof state before:
case h₀.Free
C : _root_.Container
R : Type u₁
node : C.A
k₁ k₂ : Container.B C node → Free C R
h : ∀ (x : Container.B C node), (⊥ ⊔ ↑(pgfp (equivF' Eq)) ⊥) (k₁ x) (k₂ x)
⊢ ∃ k₂_1,
    M.destruct (construct (Functor.Free node k₁)) = { fst := A.Free node, snd := k₁ } ∧
      M.destruct (construct (Functor.Free node k₂)) = { fst := A.Free node, snd := k₂_1 } ∧
        ∀ (i : Container.B (Container C R) (A.Free node)), eq (k₁ i) (k₂_1 i)
Tactic:
exists k₂
Proof state after:
case h₀.Free
C : _root_.Container
R : Type u₁
node : C.A
k₁ k₂ : Container.B C node → Free C R
h : ∀ (x : Container.B C node), (⊥ ⊔ ↑(pgfp (equivF' Eq)) ⊥) (k₁ x) (k₂ x)
⊢ M.destruct (construct (Functor.Free node k₁)) = { fst := A.Free node, snd := k₁ } ∧
    M.destruct (construct (Functor.Free node k₂)) = { fst := A.Free node, snd := k₂ } ∧
      ∀ (i : Container.B (Container C R) (A.Free node)), eq (k₁ i) (k₂ i)
Theorem: Free.eq.bisim
Proof state before:
case h₀.Free
C : _root_.Container
R : Type u₁
node : C.A
k₁ k₂ : Container.B C node → Free C R
h : ∀ (x : Container.B C node), (⊥ ⊔ ↑(pgfp (equivF' Eq)) ⊥) (k₁ x) (k₂ x)
⊢ M.destruct (construct (Functor.Free node k₁)) = { fst := A.Free node, snd := k₁ } ∧
    M.destruct (construct (Functor.Free node k₂)) = { fst := A.Free node, snd := k₂ } ∧
      ∀ (i : Container.B (Container C R) (A.Free node)), eq (k₁ i) (k₂ i)
Tactic:
simp only [construct, M.destruct_construct, inv, true_and]
Proof state after:
case h₀.Free
C : _root_.Container
R : Type u₁
node : C.A
k₁ k₂ : Container.B C node → Free C R
h : ∀ (x : Container.B C node), (⊥ ⊔ ↑(pgfp (equivF' Eq)) ⊥) (k₁ x) (k₂ x)
⊢ ∀ (i : Container.B (Container C R) (A.Free node)), eq (k₁ i) (k₂ i)
Theorem: Free.eq.bisim
Proof state before:
case h₀.Free
C : _root_.Container
R : Type u₁
node : C.A
k₁ k₂ : Container.B C node → Free C R
h : ∀ (x : Container.B C node), (⊥ ⊔ ↑(pgfp (equivF' Eq)) ⊥) (k₁ x) (k₂ x)
⊢ ∀ (i : Container.B (Container C R) (A.Free node)), eq (k₁ i) (k₂ i)
Tactic:
intro x
Proof state after:
case h₀.Free
C : _root_.Container
R : Type u₁
node : C.A
k₁ k₂ : Container.B C node → Free C R
h : ∀ (x : Container.B C node), (⊥ ⊔ ↑(pgfp (equivF' Eq)) ⊥) (k₁ x) (k₂ x)
x : Container.B (Container C R) (A.Free node)
⊢ eq (k₁ x) (k₂ x)
Theorem: Free.eq.bisim
Proof state before:
case h₀.Free
C : _root_.Container
R : Type u₁
node : C.A
k₁ k₂ : Container.B C node → Free C R
h : ∀ (x : Container.B C node), (⊥ ⊔ ↑(pgfp (equivF' Eq)) ⊥) (k₁ x) (k₂ x)
x : Container.B (Container C R) (A.Free node)
⊢ eq (k₁ x) (k₂ x)
Tactic:
rw [CompleteLattice.bot_sup] at h
Proof state after:
case h₀.Free
C : _root_.Container
R : Type u₁
node : C.A
k₁ k₂ : Container.B C node → Free C R
h : ∀ (x : Container.B C node), ↑(pgfp (equivF' Eq)) ⊥ (k₁ x) (k₂ x)
x : Container.B (Container C R) (A.Free node)
⊢ eq (k₁ x) (k₂ x)
Theorem: Free.eq.bisim
Proof state before:
case h₀.Free
C : _root_.Container
R : Type u₁
node : C.A
k₁ k₂ : Container.B C node → Free C R
h : ∀ (x : Container.B C node), ↑(pgfp (equivF' Eq)) ⊥ (k₁ x) (k₂ x)
x : Container.B (Container C R) (A.Free node)
⊢ eq (k₁ x) (k₂ x)
Tactic:
apply h
Proof state after:
no goals
Theorem: Free.eq.rfl
Proof state before:
C : _root_.Container
R : Type u₁
⊢ ∀ (x : Free C R), eq x x
Tactic:
have : ∀ (x y:Free C R), x = y → Free.eq x y := by
  apply Free.equiv.coinduction
  intro x y h
  cases h
  conv =>
    congr
    . rfl
    . rfl
    . rw [←construct_destruct x]
    . rw [←construct_destruct x]
  cases destruct x with
  | Pure r =>
    apply equivF.Pure
    rfl
  | Free node k =>
    apply equivF.Free
    intro y
    left
    rfl
Proof state after:
C : _root_.Container
R : Type u₁
this : ∀ (x y : Free C R), x = y → eq x y
⊢ ∀ (x : Free C R), eq x x
Theorem: Free.eq.rfl
Proof state before:
C : _root_.Container
R : Type u₁
this : ∀ (x y : Free C R), x = y → eq x y
⊢ ∀ (x : Free C R), eq x x
Tactic:
intro x
Proof state after:
C : _root_.Container
R : Type u₁
this : ∀ (x y : Free C R), x = y → eq x y
x : Free C R
⊢ eq x x
Theorem: Free.eq.rfl
Proof state before:
C : _root_.Container
R : Type u₁
this : ∀ (x y : Free C R), x = y → eq x y
x : Free C R
⊢ eq x x
Tactic:
apply this
Proof state after:
case a
C : _root_.Container
R : Type u₁
this : ∀ (x y : Free C R), x = y → eq x y
x : Free C R
⊢ x = x
Theorem: Free.eq.rfl
Proof state before:
case a
C : _root_.Container
R : Type u₁
this : ∀ (x y : Free C R), x = y → eq x y
x : Free C R
⊢ x = x
Tactic:
rfl
Proof state after:
no goals
Theorem: Free.eq.rfl
Proof state before:
C : _root_.Container
R : Type u₁
⊢ ∀ (x y : Free C R), x = y → eq x y
Tactic:
apply Free.equiv.coinduction
Proof state after:
case a
C : _root_.Container
R : Type u₁
⊢ ∀ (x y : Free C R), x = y → equivF Eq ((fun x y => x = y) ⊔ pequiv Eq fun x y => x = y) x y
Theorem: Free.eq.rfl
Proof state before:
case a
C : _root_.Container
R : Type u₁
⊢ ∀ (x y : Free C R), x = y → equivF Eq ((fun x y => x = y) ⊔ pequiv Eq fun x y => x = y) x y
Tactic:
intro x y h
Proof state after:
case a
C : _root_.Container
R : Type u₁
x y : Free C R
h : x = y
⊢ equivF Eq ((fun x y => x = y) ⊔ pequiv Eq fun x y => x = y) x y
Theorem: Free.eq.rfl
Proof state before:
case a
C : _root_.Container
R : Type u₁
x y : Free C R
h : x = y
⊢ equivF Eq ((fun x y => x = y) ⊔ pequiv Eq fun x y => x = y) x y
Tactic:
cases h
Proof state after:
case a.refl
C : _root_.Container
R : Type u₁
x : Free C R
⊢ equivF Eq ((fun x y => x = y) ⊔ pequiv Eq fun x y => x = y) x x
Theorem: Free.eq.rfl
Proof state before:
case a.refl
C : _root_.Container
R : Type u₁
x : Free C R
⊢ equivF Eq ((fun x y => x = y) ⊔ pequiv Eq fun x y => x = y) x x
Tactic:
conv =>
  congr
  . rfl
  . rfl
  . rw [←construct_destruct x]
  . rw [←construct_destruct x]
Proof state after:
case a.refl
C : _root_.Container
R : Type u₁
x : Free C R
⊢ equivF Eq ((fun x y => x = y) ⊔ pequiv Eq fun x y => x = y) (construct (destruct x)) (construct (destruct x))
Theorem: Free.eq.rfl
Proof state before:
case a.refl
C : _root_.Container
R : Type u₁
x : Free C R
⊢ equivF Eq ((fun x y => x = y) ⊔ pequiv Eq fun x y => x = y) (construct (destruct x)) (construct (destruct x))
Tactic:
cases destruct x with
| Pure r =>
  apply equivF.Pure
  rfl
| Free node k =>
  apply equivF.Free
  intro y
  left
  rfl
Proof state after:
no goals
Theorem: Free.eq.rfl
Proof state before:
case a.refl.Pure
C : _root_.Container
R : Type u₁
x : Free C R
r : R
⊢ equivF Eq ((fun x y => x = y) ⊔ pequiv Eq fun x y => x = y) (construct (Functor.Pure r)) (construct (Functor.Pure r))
Tactic:
apply equivF.Pure
Proof state after:
case a.refl.Pure.a
C : _root_.Container
R : Type u₁
x : Free C R
r : R
⊢ r = r
Theorem: Free.eq.rfl
Proof state before:
case a.refl.Pure.a
C : _root_.Container
R : Type u₁
x : Free C R
r : R
⊢ r = r
Tactic:
rfl
Proof state after:
no goals
Theorem: Free.eq.rfl
Proof state before:
case a.refl.Free
C : _root_.Container
R : Type u₁
x : Free C R
node : C.A
k : Container.B C node → Free C R
⊢ equivF Eq ((fun x y => x = y) ⊔ pequiv Eq fun x y => x = y) (construct (Functor.Free node k))
    (construct (Functor.Free node k))
Tactic:
apply equivF.Free
Proof state after:
case a.refl.Free.a
C : _root_.Container
R : Type u₁
x : Free C R
node : C.A
k : Container.B C node → Free C R
⊢ ∀ (x : Container.B C node), ((fun x y => x = y) ⊔ pequiv Eq fun x y => x = y) (k x) (k x)
Theorem: Free.eq.rfl
Proof state before:
case a.refl.Free.a
C : _root_.Container
R : Type u₁
x : Free C R
node : C.A
k : Container.B C node → Free C R
⊢ ∀ (x : Container.B C node), ((fun x y => x = y) ⊔ pequiv Eq fun x y => x = y) (k x) (k x)
Tactic:
intro y
Proof state after:
case a.refl.Free.a
C : _root_.Container
R : Type u₁
x : Free C R
node : C.A
k : Container.B C node → Free C R
y : Container.B C node
⊢ ((fun x y => x = y) ⊔ pequiv Eq fun x y => x = y) (k y) (k y)
Theorem: Free.eq.rfl
Proof state before:
case a.refl.Free.a
C : _root_.Container
R : Type u₁
x : Free C R
node : C.A
k : Container.B C node → Free C R
y : Container.B C node
⊢ ((fun x y => x = y) ⊔ pequiv Eq fun x y => x = y) (k y) (k y)
Tactic:
left
Proof state after:
case a.refl.Free.a.h
C : _root_.Container
R : Type u₁
x : Free C R
node : C.A
k : Container.B C node → Free C R
y : Container.B C node
⊢ (fun x y => x = y) (k y) (k y)
Theorem: Free.eq.rfl
Proof state before:
case a.refl.Free.a.h
C : _root_.Container
R : Type u₁
x : Free C R
node : C.A
k : Container.B C node → Free C R
y : Container.B C node
⊢ (fun x y => x = y) (k y) (k y)
Tactic:
rfl
Proof state after:
no goals
Theorem: Free.bind_inr
Proof state before:
C : _root_.Container
R S : Type u₁
f : R → Free C S
x : Free C S
⊢ corec (bind.automaton f) (Sum.inr x) = x
Tactic:
apply Free.eq.bisim
Proof state after:
case a
C : _root_.Container
R S : Type u₁
f : R → Free C S
x : Free C S
⊢ eq (corec (bind.automaton f) (Sum.inr x)) x
Theorem: Free.bind_inr
Proof state before:
case a
C : _root_.Container
R S : Type u₁
f : R → Free C S
x : Free C S
⊢ eq (corec (bind.automaton f) (Sum.inr x)) x
Tactic:
have : ∀ x y, x = corec (bind.automaton f) (.inr y) → eq x y := by
  apply Free.equiv.coinduction
  intro x y h₁
  conv =>
    congr
    . rfl
    . rfl
    . rw [←construct_destruct x]
    . rw [←construct_destruct y]
  have h₂ := congrArg destruct h₁
  clear h₁
  rw [destruct_corec] at h₂
  cases hy: destruct y with
  | Pure r =>
    simp only [Map, hy, bind.automaton] at h₂
    rw [h₂]
    apply equivF.Pure
    rfl
  | Free n k =>
    simp only [Map, bind.automaton, hy] at h₂
    rw [h₂]
    apply equivF.Free
    intro y
    left
    rfl
Proof state after:
case a
C : _root_.Container
R S : Type u₁
f : R → Free C S
x : Free C S
this : ∀ (x y : Free C S), x = corec (bind.automaton f) (Sum.inr y) → eq x y
⊢ eq (corec (bind.automaton f) (Sum.inr x)) x
Theorem: Free.bind_inr
Proof state before:
case a
C : _root_.Container
R S : Type u₁
f : R → Free C S
x : Free C S
this : ∀ (x y : Free C S), x = corec (bind.automaton f) (Sum.inr y) → eq x y
⊢ eq (corec (bind.automaton f) (Sum.inr x)) x
Tactic:
apply this
Proof state after:
case a.a
C : _root_.Container
R S : Type u₁
f : R → Free C S
x : Free C S
this : ∀ (x y : Free C S), x = corec (bind.automaton f) (Sum.inr y) → eq x y
⊢ corec (bind.automaton f) (Sum.inr x) = corec (bind.automaton f) (Sum.inr x)
Theorem: Free.bind_inr
Proof state before:
case a.a
C : _root_.Container
R S : Type u₁
f : R → Free C S
x : Free C S
this : ∀ (x y : Free C S), x = corec (bind.automaton f) (Sum.inr y) → eq x y
⊢ corec (bind.automaton f) (Sum.inr x) = corec (bind.automaton f) (Sum.inr x)
Tactic:
rfl
Proof state after:
no goals
Theorem: Free.bind_inr
Proof state before:
C : _root_.Container
R S : Type u₁
f : R → Free C S
x : Free C S
⊢ ∀ (x y : Free C S), x = corec (bind.automaton f) (Sum.inr y) → eq x y
Tactic:
apply Free.equiv.coinduction
Proof state after:
case a
C : _root_.Container
R S : Type u₁
f : R → Free C S
x : Free C S
⊢ ∀ (x y : Free C S),
    x = corec (bind.automaton f) (Sum.inr y) →
      equivF Eq
        ((fun x y => x = corec (bind.automaton f) (Sum.inr y)) ⊔
          pequiv Eq fun x y => x = corec (bind.automaton f) (Sum.inr y))
        x y