-- Mathlib/Data/QPF/Multivariate/Constructions/Cofix.lean
theorem Cofix.dest_corec' {α : TypeVec.{u} n} {β : Type u}
    (g : β → F (α.append1 (Cofix F α ⊕ β))) (x : β) :
    Cofix.dest (Cofix.corec' g x) =
      appendFun id (Sum.elim _root_.id (Cofix.corec' g)) <$$> g x

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x : β
⊢ (corec' g x).dest = (TypeVec.id ::: Sum.elim _root_.id (corec' g)) <$$> g x

Tactic:
rw [Cofix.corec', Cofix.dest_corec]

Result:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x : β
⊢ (TypeVec.id ::: corec (Sum.elim (MvFunctor.map (TypeVec.id ::: Sum.inl) ∘ dest) g)) <$$>
      Sum.elim (MvFunctor.map (TypeVec.id ::: Sum.inl) ∘ dest) g (Sum.inr x) =
    (TypeVec.id ::: Sum.elim _root_.id (corec' g)) <$$> g x

Proof state:
case h.e'_6.h.e'_7.h.inl.intro.intro
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x✝ : β
i : Cofix F α
R : Cofix F α → Cofix F α → Prop :=
  fun a b =>
    ∃ x,
      a =
          corec
            (MvFunctor.map (TypeVec.id ::: fun x => x) ∘
              Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val => g val)
            (Sum.inl x) ∧
        b = x
a b x : Cofix F α
Ha :
  a =
    corec
      (MvFunctor.map (TypeVec.id ::: fun x => x) ∘
        Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val => g val)
      (Sum.inl x)
Hb : b = x
⊢ LiftR' (α.RelLast' R)
    ((TypeVec.id :::
        ((corec fun x =>
              (TypeVec.id ::: fun x => x) <$$>
                Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> val.dest) (fun val => g val) x) ∘
            fun x => x) ∘
          Sum.inl) <$$>
      x.dest)
    x.dest

Tactic:
apply liftR_map_last'

Result:
case h.e'_6.h.e'_7.h.inl.intro.intro.hh
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x✝ : β
i : Cofix F α
R : Cofix F α → Cofix F α → Prop :=
  fun a b =>
    ∃ x,
      a =
          corec
            (MvFunctor.map (TypeVec.id ::: fun x => x) ∘
              Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val => g val)
            (Sum.inl x) ∧
        b = x
a b x : Cofix F α
Ha :
  a =
    corec
      (MvFunctor.map (TypeVec.id ::: fun x => x) ∘
        Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val => g val)
      (Sum.inl x)
Hb : b = x
⊢ ∀ (x : Cofix F α),
    R
      ((((corec fun x =>
              (TypeVec.id ::: fun x => x) <$$>
                Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> val.dest) (fun val => g val) x) ∘
            fun x => x) ∘
          Sum.inl)
        x)
      x

Proof state:
case h.e'_6.h.e'_7.h.inr.e_g.h
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x i : β
y : Cofix F α ⊕ β
⊢ (MvFunctor.map (TypeVec.id ::: fun x => x) ∘
        Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val => g val)
      y =
    Sum.elim (MvFunctor.map (TypeVec.id ::: Sum.inl) ∘ dest) g y

Tactic:
erw [appendFun_id_id]

Result:
case h.e'_6.h.e'_7.h.inr.e_g.h
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x i : β
y : Cofix F α ⊕ β
⊢ (MvFunctor.map TypeVec.id ∘ Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val => g val) y =
    Sum.elim (MvFunctor.map (TypeVec.id ::: Sum.inl) ∘ dest) g y

Proof state:
case h.e'_6.h.e'_7.h.inr.e_g.h
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x i : β
y : Cofix F α ⊕ β
⊢ (MvFunctor.map TypeVec.id ∘ Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val => g val) y =
    Sum.elim (MvFunctor.map (TypeVec.id ::: Sum.inl) ∘ dest) g y

Tactic:
simp [MvFunctor.id_map, Sum.elim]

Result:
no goals

Proof state:
case h.e'_6.h.e'_7.h.inl.intro.intro.hh
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x✝ : β
i : Cofix F α
R : Cofix F α → Cofix F α → Prop :=
  fun a b =>
    ∃ x,
      a =
          corec
            (MvFunctor.map (TypeVec.id ::: fun x => x) ∘
              Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val => g val)
            (Sum.inl x) ∧
        b = x
a b x : Cofix F α
Ha :
  a =
    corec
      (MvFunctor.map (TypeVec.id ::: fun x => x) ∘
        Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val => g val)
      (Sum.inl x)
Hb : b = x
⊢ ∀ (x : Cofix F α),
    R
      (corec
        (fun x =>
          (TypeVec.id ::: fun x => x) <$$>
            Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> val.dest) (fun val => g val) x)
        (Sum.inl x))
      x

Tactic:
intros

Result:
case h.e'_6.h.e'_7.h.inl.intro.intro.hh
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x✝¹ : β
i : Cofix F α
R : Cofix F α → Cofix F α → Prop :=
  fun a b =>
    ∃ x,
      a =
          corec
            (MvFunctor.map (TypeVec.id ::: fun x => x) ∘
              Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val => g val)
            (Sum.inl x) ∧
        b = x
a b x : Cofix F α
Ha :
  a =
    corec
      (MvFunctor.map (TypeVec.id ::: fun x => x) ∘
        Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val => g val)
      (Sum.inl x)
Hb : b = x
x✝ : Cofix F α
⊢ R
    (corec
      (fun x =>
        (TypeVec.id ::: fun x => x) <$$>
          Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> val.dest) (fun val => g val) x)
      (Sum.inl x✝))
    x✝

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x : β
⊢ (TypeVec.id ::: corec (Sum.elim (MvFunctor.map (TypeVec.id ::: Sum.inl) ∘ dest) g)) <$$> g x =
    (TypeVec.id ::: Sum.elim _root_.id (corec' g)) <$$> g x

Tactic:
congr!

Result:
case h.e'_6.h.e'_7
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x : β
⊢ corec (Sum.elim (MvFunctor.map (TypeVec.id ::: Sum.inl) ∘ dest) g) = Sum.elim _root_.id (corec' g)

Proof state:
case h.e'_6.h.e'_7.h.inl
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x : β
i : Cofix F α
⊢ corec
      (MvFunctor.map (TypeVec.id ::: fun x => x) ∘
        Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val => g val)
      (Sum.inl i) =
    i

Tactic:
mv_bisim i with R a b x Ha Hb

Result:
case h.e'_6.h.e'_7.h.inl.intro.intro
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x✝ : β
i : Cofix F α
R : Cofix F α → Cofix F α → Prop :=
  fun a b =>
    ∃ x,
      a =
          corec
            (MvFunctor.map (TypeVec.id ::: fun x => x) ∘
              Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val => g val)
            (Sum.inl x) ∧
        b = x
a b x : Cofix F α
Ha :
  a =
    corec
      (MvFunctor.map (TypeVec.id ::: fun x => x) ∘
        Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val => g val)
      (Sum.inl x)
Hb : b = x
⊢ LiftR' (α.RelLast' R) a.dest b.dest