Theorem: Free.bind_inr.internal (CoInd/QPF/FreeMonads.lean)

State before:
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
⊢ ∀ (x y : Free F S), corec (bind.automaton k) (Sum.inr x) = y → x = y
Tactic:
apply QPF.M.bisim (λ x y => corec (bind.automaton k) (.inr x) = y)
State after:
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
⊢ ∀ (x y : QPF.M (FreeF F S)),
    corec (bind.automaton k) (Sum.inr x) = y →
      QPF.M.liftr (FreeF F S) (fun x y => corec (bind.automaton k) (Sum.inr x) = y) (QPF.M.destruct x)
        (QPF.M.destruct y)

State before:
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
⊢ ∀ (x y : QPF.M (FreeF F S)),
    corec (bind.automaton k) (Sum.inr x) = y →
      QPF.M.liftr (FreeF F S) (fun x y => corec (bind.automaton k) (Sum.inr x) = y) (QPF.M.destruct x)
        (QPF.M.destruct y)
Tactic:
. intro x y h₁
  induction h₁
  rw [corec, QPF.M.destruct_corec]
  conv =>
    congr
    . skip
    . skip
    . rhs
      simp only [bind.automaton]
  exists (λ x => ⟨⟨x, corec (bind.automaton k) (.inr x)⟩, by rfl⟩) <$> destruct x
  rw [destruct]
  constructor
  . simp only [←QPF.map_comp, Function.comp]
    apply Eq.trans _ (QPF.map_id _)
    rfl
  . simp only [←QPF.map_comp, Function.comp]
    rfl
State after:
no goals

State before:
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
⊢ ∀ (x y : QPF.M (FreeF F S)),
    corec (bind.automaton k) (Sum.inr x) = y →
      QPF.M.liftr (FreeF F S) (fun x y => corec (bind.automaton k) (Sum.inr x) = y) (QPF.M.destruct x)
        (QPF.M.destruct y)
Tactic:
intro x y h₁
State after:
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
h₁ : corec (bind.automaton k) (Sum.inr x) = y
⊢ QPF.M.liftr (FreeF F S) (fun x y => corec (bind.automaton k) (Sum.inr x) = y) (QPF.M.destruct x) (QPF.M.destruct y)

State before:
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
h₁ : corec (bind.automaton k) (Sum.inr x) = y
⊢ QPF.M.liftr (FreeF F S) (fun x y => corec (bind.automaton k) (Sum.inr x) = y) (QPF.M.destruct x) (QPF.M.destruct y)
Tactic:
induction h₁
State after:
case refl
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
⊢ QPF.M.liftr (FreeF F S) (fun x y => corec (bind.automaton k) (Sum.inr x) = y) (QPF.M.destruct x)
    (QPF.M.destruct (corec (bind.automaton k) (Sum.inr x)))

State before:
case refl
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
⊢ QPF.M.liftr (FreeF F S) (fun x y => corec (bind.automaton k) (Sum.inr x) = y) (QPF.M.destruct x)
    (QPF.M.destruct (corec (bind.automaton k) (Sum.inr x)))
Tactic:
rw [corec, QPF.M.destruct_corec]
State after:
case refl
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
⊢ QPF.M.liftr (FreeF F S) (fun x y => QPF.M.corec (bind.automaton k) (Sum.inr x) = y) (QPF.M.destruct x)
    ((fun x => QPF.M.corec (bind.automaton k) x) <$> bind.automaton k (Sum.inr x))

State before:
case refl
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
⊢ QPF.M.liftr (FreeF F S) (fun x y => QPF.M.corec (bind.automaton k) (Sum.inr x) = y) (QPF.M.destruct x)
    ((fun x => QPF.M.corec (bind.automaton k) x) <$> bind.automaton k (Sum.inr x))
Tactic:
conv =>
  congr
  . skip
  . skip
  . rhs
    simp only [bind.automaton]
State after:
case refl
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
⊢ QPF.M.liftr (FreeF F S) (fun x y => QPF.M.corec (bind.automaton k) (Sum.inr x) = y) (QPF.M.destruct x)
    ((fun x => QPF.M.corec (bind.automaton k) x) <$> Sum.inr <$> destruct x)

State before:
case refl
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
⊢ QPF.M.liftr (FreeF F S) (fun x y => QPF.M.corec (bind.automaton k) (Sum.inr x) = y) (QPF.M.destruct x)
    ((fun x => QPF.M.corec (bind.automaton k) x) <$> Sum.inr <$> destruct x)
Tactic:
exists (λ x => ⟨⟨x, corec (bind.automaton k) (.inr x)⟩, by rfl⟩) <$> destruct x
State after:
case refl
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
⊢ (fun x => (↑x).fst) <$>
        (fun x =>
            { val := (x, corec (bind.automaton k) (Sum.inr x)),
              property :=
                (_ :
                  QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst) =
                    QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst)) }) <$>
          destruct x =
      QPF.M.destruct x ∧
    (fun x => (↑x).snd) <$>
        (fun x =>
            { val := (x, corec (bind.automaton k) (Sum.inr x)),
              property :=
                (_ :
                  QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst) =
                    QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst)) }) <$>
          destruct x =
      (fun x => QPF.M.corec (bind.automaton k) x) <$> Sum.inr <$> destruct x

State before:
case refl
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
⊢ (fun x => (↑x).fst) <$>
        (fun x =>
            { val := (x, corec (bind.automaton k) (Sum.inr x)),
              property :=
                (_ :
                  QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst) =
                    QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst)) }) <$>
          destruct x =
      QPF.M.destruct x ∧
    (fun x => (↑x).snd) <$>
        (fun x =>
            { val := (x, corec (bind.automaton k) (Sum.inr x)),
              property :=
                (_ :
                  QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst) =
                    QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst)) }) <$>
          destruct x =
      (fun x => QPF.M.corec (bind.automaton k) x) <$> Sum.inr <$> destruct x
Tactic:
rw [destruct]
State after:
case refl
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
⊢ (fun x => (↑x).fst) <$>
        (fun x =>
            { val := (x, corec (bind.automaton k) (Sum.inr x)),
              property :=
                (_ :
                  QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst) =
                    QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst)) }) <$>
          QPF.M.destruct x =
      QPF.M.destruct x ∧
    (fun x => (↑x).snd) <$>
        (fun x =>
            { val := (x, corec (bind.automaton k) (Sum.inr x)),
              property :=
                (_ :
                  QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst) =
                    QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst)) }) <$>
          QPF.M.destruct x =
      (fun x => QPF.M.corec (bind.automaton k) x) <$> Sum.inr <$> QPF.M.destruct x

State before:
case refl
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
⊢ (fun x => (↑x).fst) <$>
        (fun x =>
            { val := (x, corec (bind.automaton k) (Sum.inr x)),
              property :=
                (_ :
                  QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst) =
                    QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst)) }) <$>
          QPF.M.destruct x =
      QPF.M.destruct x ∧
    (fun x => (↑x).snd) <$>
        (fun x =>
            { val := (x, corec (bind.automaton k) (Sum.inr x)),
              property :=
                (_ :
                  QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst) =
                    QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst)) }) <$>
          QPF.M.destruct x =
      (fun x => QPF.M.corec (bind.automaton k) x) <$> Sum.inr <$> QPF.M.destruct x
Tactic:
constructor
State after:
case refl.left
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
⊢ (fun x => (↑x).fst) <$>
      (fun x =>
          { val := (x, corec (bind.automaton k) (Sum.inr x)),
            property :=
              (_ :
                QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst) =
                  QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst)) }) <$>
        QPF.M.destruct x =
    QPF.M.destruct x

case refl.right
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
⊢ (fun x => (↑x).snd) <$>
      (fun x =>
          { val := (x, corec (bind.automaton k) (Sum.inr x)),
            property :=
              (_ :
                QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst) =
                  QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst)) }) <$>
        QPF.M.destruct x =
    (fun x => QPF.M.corec (bind.automaton k) x) <$> Sum.inr <$> QPF.M.destruct x

State before:
case refl.left
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
⊢ (fun x => (↑x).fst) <$>
      (fun x =>
          { val := (x, corec (bind.automaton k) (Sum.inr x)),
            property :=
              (_ :
                QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst) =
                  QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst)) }) <$>
        QPF.M.destruct x =
    QPF.M.destruct x

case refl.right
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
⊢ (fun x => (↑x).snd) <$>
      (fun x =>
          { val := (x, corec (bind.automaton k) (Sum.inr x)),
            property :=
              (_ :
                QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst) =
                  QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst)) }) <$>
        QPF.M.destruct x =
    (fun x => QPF.M.corec (bind.automaton k) x) <$> Sum.inr <$> QPF.M.destruct x
Tactic:
. simp only [←QPF.map_comp, Function.comp]
  apply Eq.trans _ (QPF.map_id _)
  rfl
State after:
case refl.right
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
⊢ (fun x => (↑x).snd) <$>
      (fun x =>
          { val := (x, corec (bind.automaton k) (Sum.inr x)),
            property :=
              (_ :
                QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst) =
                  QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst)) }) <$>
        QPF.M.destruct x =
    (fun x => QPF.M.corec (bind.automaton k) x) <$> Sum.inr <$> QPF.M.destruct x

State before:
case refl.right
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
⊢ (fun x => (↑x).snd) <$>
      (fun x =>
          { val := (x, corec (bind.automaton k) (Sum.inr x)),
            property :=
              (_ :
                QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst) =
                  QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst)) }) <$>
        QPF.M.destruct x =
    (fun x => QPF.M.corec (bind.automaton k) x) <$> Sum.inr <$> QPF.M.destruct x
Tactic:
. simp only [←QPF.map_comp, Function.comp]
  rfl
State after:
no goals

State before:
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x✝ y x : QPF.M (FreeF F S)
⊢ (fun x y => QPF.M.corec (bind.automaton k) (Sum.inr x) = y) (x, corec (bind.automaton k) (Sum.inr x)).fst
    (x, corec (bind.automaton k) (Sum.inr x)).snd
Tactic:
rfl
State after:
no goals

State before:
case refl.left
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
⊢ (fun x => (↑x).fst) <$>
      (fun x =>
          { val := (x, corec (bind.automaton k) (Sum.inr x)),
            property :=
              (_ :
                QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst) =
                  QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst)) }) <$>
        QPF.M.destruct x =
    QPF.M.destruct x
Tactic:
simp only [←QPF.map_comp, Function.comp]
State after:
case refl.left
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
⊢ (fun x => x) <$> QPF.M.destruct x = QPF.M.destruct x

State before:
case refl.left
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
⊢ (fun x => x) <$> QPF.M.destruct x = QPF.M.destruct x
Tactic:
apply Eq.trans _ (QPF.map_id _)
State after:
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
⊢ (fun x => x) <$> QPF.M.destruct x = id <$> QPF.M.destruct x

State before:
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
⊢ (fun x => x) <$> QPF.M.destruct x = id <$> QPF.M.destruct x
Tactic:
rfl
State after:
no goals

State before:
case refl.right
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
⊢ (fun x => (↑x).snd) <$>
      (fun x =>
          { val := (x, corec (bind.automaton k) (Sum.inr x)),
            property :=
              (_ :
                QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst) =
                  QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst)) }) <$>
        QPF.M.destruct x =
    (fun x => QPF.M.corec (bind.automaton k) x) <$> Sum.inr <$> QPF.M.destruct x
Tactic:
simp only [←QPF.map_comp, Function.comp]
State after:
case refl.right
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
⊢ (fun x => corec (bind.automaton k) (Sum.inr x)) <$> QPF.M.destruct x =
    (fun x => QPF.M.corec (bind.automaton k) (Sum.inr x)) <$> QPF.M.destruct x

State before:
case refl.right
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
⊢ (fun x => corec (bind.automaton k) (Sum.inr x)) <$> QPF.M.destruct x =
    (fun x => QPF.M.corec (bind.automaton k) (Sum.inr x)) <$> QPF.M.destruct x
Tactic:
rfl
State after:
no goals