Theorem: QPF.M.construct_destruct (CoInd/Utils.lean)

State before:
F : Type u₁ → Type u₁
inst : QPF F
x : M F
⊢ construct (destruct x) = x
Tactic:
let R (x y: M F) := x = construct (destruct y)
State after:
F : Type u₁ → Type u₁
inst : QPF F
x : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
⊢ construct (destruct x) = x

State before:
F : Type u₁ → Type u₁
inst : QPF F
x : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
⊢ construct (destruct x) = x
Tactic:
apply bisim R
State after:
case h₀
F : Type u₁ → Type u₁
inst : QPF F
x : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
⊢ ∀ (x y : M F), R x y → liftr F R (destruct x) (destruct y)

case a
F : Type u₁ → Type u₁
inst : QPF F
x : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
⊢ R (construct (destruct x)) x

State before:
case h₀
F : Type u₁ → Type u₁
inst : QPF F
x : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
⊢ ∀ (x y : M F), R x y → liftr F R (destruct x) (destruct y)

case a
F : Type u₁ → Type u₁
inst : QPF F
x : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
⊢ R (construct (destruct x)) x
Tactic:
. intro x y h₀
  have h₀ := congrArg destruct h₀
  simp [liftr]
  simp only [construct, destruct_corec, construct.automaton] at h₀
  exists Functor.map (λ a => ⟨⟨construct <| destruct a, a⟩, by simp⟩) (destruct y)
  rw [h₀]
  constructor
  . simp only [←QPF.map_comp]
    rfl
  . rw [←QPF.M.map_comp]
    have : inst.map id (destruct y) = destruct y := by rw [QPF.map_id]
    apply Eq.trans _ this
    apply congrFun
    funext _
    rfl
State after:
case a
F : Type u₁ → Type u₁
inst : QPF F
x : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
⊢ R (construct (destruct x)) x

State before:
case a
F : Type u₁ → Type u₁
inst : QPF F
x : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
⊢ R (construct (destruct x)) x
Tactic:
. rfl
State after:
no goals

State before:
case h₀
F : Type u₁ → Type u₁
inst : QPF F
x : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
⊢ ∀ (x y : M F), R x y → liftr F R (destruct x) (destruct y)
Tactic:
intro x y h₀
State after:
case h₀
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀ : R x y
⊢ liftr F R (destruct x) (destruct y)

State before:
case h₀
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀ : R x y
⊢ liftr F R (destruct x) (destruct y)
Tactic:
have h₀ := congrArg destruct h₀
State after:
case h₀
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = destruct (construct (destruct y))
⊢ liftr F R (destruct x) (destruct y)

State before:
case h₀
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = destruct (construct (destruct y))
⊢ liftr F R (destruct x) (destruct y)
Tactic:
simp [liftr]
State after:
case h₀
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = destruct (construct (destruct y))
⊢ ∃ z, (fun x => (↑x).fst) <$> z = destruct x ∧ (fun x => (↑x).snd) <$> z = destruct y

State before:
case h₀
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = destruct (construct (destruct y))
⊢ ∃ z, (fun x => (↑x).fst) <$> z = destruct x ∧ (fun x => (↑x).snd) <$> z = destruct y
Tactic:
simp only [construct, destruct_corec, construct.automaton] at h₀
State after:
case h₀
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
⊢ ∃ z, (fun x => (↑x).fst) <$> z = destruct x ∧ (fun x => (↑x).snd) <$> z = destruct y

State before:
case h₀
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
⊢ ∃ z, (fun x => (↑x).fst) <$> z = destruct x ∧ (fun x => (↑x).snd) <$> z = destruct y
Tactic:
exists Functor.map (λ a => ⟨⟨construct <| destruct a, a⟩, by simp⟩) (destruct y)
State after:
case h₀
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
⊢ (fun x => (↑x).fst) <$>
        (fun a =>
            { val := (construct (destruct a), a),
              property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
          destruct y =
      destruct x ∧
    (fun x => (↑x).snd) <$>
        (fun a =>
            { val := (construct (destruct a), a),
              property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
          destruct y =
      destruct y

State before:
case h₀
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
⊢ (fun x => (↑x).fst) <$>
        (fun a =>
            { val := (construct (destruct a), a),
              property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
          destruct y =
      destruct x ∧
    (fun x => (↑x).snd) <$>
        (fun a =>
            { val := (construct (destruct a), a),
              property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
          destruct y =
      destruct y
Tactic:
rw [h₀]
State after:
case h₀
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
⊢ (fun x => (↑x).fst) <$>
        (fun a =>
            { val := (construct (destruct a), a),
              property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
          destruct y =
      (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y ∧
    (fun x => (↑x).snd) <$>
        (fun a =>
            { val := (construct (destruct a), a),
              property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
          destruct y =
      destruct y

State before:
case h₀
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
⊢ (fun x => (↑x).fst) <$>
        (fun a =>
            { val := (construct (destruct a), a),
              property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
          destruct y =
      (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y ∧
    (fun x => (↑x).snd) <$>
        (fun a =>
            { val := (construct (destruct a), a),
              property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
          destruct y =
      destruct y
Tactic:
constructor
State after:
case h₀.left
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
⊢ (fun x => (↑x).fst) <$>
      (fun a =>
          { val := (construct (destruct a), a), property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
        destruct y =
    (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y

case h₀.right
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
⊢ (fun x => (↑x).snd) <$>
      (fun a =>
          { val := (construct (destruct a), a), property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
        destruct y =
    destruct y

State before:
case h₀.left
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
⊢ (fun x => (↑x).fst) <$>
      (fun a =>
          { val := (construct (destruct a), a), property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
        destruct y =
    (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y

case h₀.right
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
⊢ (fun x => (↑x).snd) <$>
      (fun a =>
          { val := (construct (destruct a), a), property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
        destruct y =
    destruct y
Tactic:
. simp only [←QPF.map_comp]
  rfl
State after:
case h₀.right
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
⊢ (fun x => (↑x).snd) <$>
      (fun a =>
          { val := (construct (destruct a), a), property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
        destruct y =
    destruct y

State before:
case h₀.right
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
⊢ (fun x => (↑x).snd) <$>
      (fun a =>
          { val := (construct (destruct a), a), property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
        destruct y =
    destruct y
Tactic:
. rw [←QPF.M.map_comp]
  have : inst.map id (destruct y) = destruct y := by rw [QPF.map_id]
  apply Eq.trans _ this
  apply congrFun
  funext _
  rfl
State after:
no goals

State before:
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
a : M F
⊢ (construct (destruct a), a).fst = construct (destruct (construct (destruct a), a).snd)
Tactic:
simp
State after:
no goals

State before:
case h₀.left
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
⊢ (fun x => (↑x).fst) <$>
      (fun a =>
          { val := (construct (destruct a), a), property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
        destruct y =
    (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
Tactic:
simp only [←QPF.map_comp]
State after:
case h₀.left
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
⊢ ((fun x => (↑x).fst) ∘ fun a =>
        { val := (construct (destruct a), a), property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
      destruct y =
    ((fun x => corec (Functor.map destruct) x) ∘ destruct) <$> destruct y

State before:
case h₀.left
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
⊢ ((fun x => (↑x).fst) ∘ fun a =>
        { val := (construct (destruct a), a), property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
      destruct y =
    ((fun x => corec (Functor.map destruct) x) ∘ destruct) <$> destruct y
Tactic:
rfl
State after:
no goals

State before:
case h₀.right
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
⊢ (fun x => (↑x).snd) <$>
      (fun a =>
          { val := (construct (destruct a), a), property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
        destruct y =
    destruct y
Tactic:
rw [←QPF.M.map_comp]
State after:
case h₀.right
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
⊢ ((fun x => (↑x).snd) ∘ fun a =>
        { val := (construct (destruct a), a), property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
      destruct y =
    destruct y

State before:
case h₀.right
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
⊢ ((fun x => (↑x).snd) ∘ fun a =>
        { val := (construct (destruct a), a), property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
      destruct y =
    destruct y
Tactic:
have : inst.map id (destruct y) = destruct y := by rw [QPF.map_id]
State after:
case h₀.right
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
this : id <$> destruct y = destruct y
⊢ ((fun x => (↑x).snd) ∘ fun a =>
        { val := (construct (destruct a), a), property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
      destruct y =
    destruct y

State before:
case h₀.right
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
this : id <$> destruct y = destruct y
⊢ ((fun x => (↑x).snd) ∘ fun a =>
        { val := (construct (destruct a), a), property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
      destruct y =
    destruct y
Tactic:
apply Eq.trans _ this
State after:
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
this : id <$> destruct y = destruct y
⊢ ((fun x => (↑x).snd) ∘ fun a =>
        { val := (construct (destruct a), a), property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
      destruct y =
    id <$> destruct y

State before:
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
this : id <$> destruct y = destruct y
⊢ ((fun x => (↑x).snd) ∘ fun a =>
        { val := (construct (destruct a), a), property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
      destruct y =
    id <$> destruct y
Tactic:
apply congrFun
State after:
case h
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
this : id <$> destruct y = destruct y
⊢ Functor.map
      ((fun x => (↑x).snd) ∘ fun a =>
        { val := (construct (destruct a), a), property := (_ : construct (destruct a) = construct (destruct a)) }) =
    Functor.map id

State before:
case h
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
this : id <$> destruct y = destruct y
⊢ Functor.map
      ((fun x => (↑x).snd) ∘ fun a =>
        { val := (construct (destruct a), a), property := (_ : construct (destruct a) = construct (destruct a)) }) =
    Functor.map id
Tactic:
funext _
State after:
case h.h
F : Type u₁ → Type u₁
inst : QPF F
x✝¹ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
this : id <$> destruct y = destruct y
x✝ : F (M F)
⊢ ((fun x => (↑x).snd) ∘ fun a =>
        { val := (construct (destruct a), a), property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
      x✝ =
    id <$> x✝

State before:
case h.h
F : Type u₁ → Type u₁
inst : QPF F
x✝¹ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
this : id <$> destruct y = destruct y
x✝ : F (M F)
⊢ ((fun x => (↑x).snd) ∘ fun a =>
        { val := (construct (destruct a), a), property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
      x✝ =
    id <$> x✝
Tactic:
rfl
State after:
no goals

State before:
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
⊢ id <$> destruct y = destruct y
Tactic:
rw [QPF.map_id]
State after:
no goals

State before:
case a
F : Type u₁ → Type u₁
inst : QPF F
x : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
⊢ R (construct (destruct x)) x
Tactic:
rfl
State after:
no goals