Theorem: Free.eq.bisim (CoInd/FreeMonads.lean)

State before:
C : _root_.Container
R : Type u₁
⊢ ∀ (x y : Free C R), eq x y → x = y
Tactic:
apply M.bisim
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)

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₁
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)

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₁
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)

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₁
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)

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
State after:
no goals

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₁
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)

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)
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)

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)
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)

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)
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)

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]
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)

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
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)

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
State after:
no goals

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)
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)

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₁
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)

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₂
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)

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]
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)

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
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)

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
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)

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
State after:
no goals