-- 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:
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:
exact ⟨_, rfl, rfl⟩

Result:
no goals

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
          (MvFunctor.map (TypeVec.id ::: fun x => x) ∘
            Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val => g val)) <$$>
      (MvFunctor.map (TypeVec.id ::: fun x => x) ∘
          Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val => g val)
        (Sum.inl x))
    x.dest

Tactic:
dsimp [Function.comp_def]

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)
    ((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) <$$>
      (TypeVec.id ::: fun x => x) <$$> (TypeVec.id ::: Sum.inl) <$$> x.dest)
    x.dest

Proof state:
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)

Tactic:
ext (i | i) <;> erw [corec_roll] <;> dsimp [Cofix.corec']

Result:
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

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

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)) <$$>
      Sum.elim (MvFunctor.map (TypeVec.id ::: Sum.inl) ∘ dest) g (Sum.inr x) =
    (TypeVec.id ::: Sum.elim _root_.id (corec' g)) <$$> g x

Tactic:
dsimp

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)) <$$> g x =
    (TypeVec.id ::: Sum.elim _root_.id (corec' g)) <$$> g x

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) ∘
            fun x => x) ∘
          Sum.inl)
        x)
      x

Tactic:
dsimp [Function.comp_def]

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

Tactic:
congr with y

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