-- Mathlib/Data/QPF/Multivariate/Constructions/Cofix.lean
theorem Cofix.mk_dest {α : TypeVec n} (x : Cofix F α) : Cofix.mk (Cofix.dest x) = x

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝ x y : Cofix F α
h : x = mk y.dest
⊢ (TypeVec.id ::: Quot.mk fun x y => x = mk y.dest) <$$>
      (TypeVec.id ::: corec fun x => (TypeVec.id ::: fun i => i.dest) <$$> x) <$$>
        (TypeVec.id ::: fun i => i.dest) <$$> y.dest =
    (TypeVec.id ::: Quot.mk fun x y => x = mk y.dest) <$$> y.dest

Tactic:
rw [← comp_map, ← appendFun_comp, id_comp]

Result:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝ x y : Cofix F α
h : x = mk y.dest
⊢ (TypeVec.id ::: (Quot.mk fun x y => x = mk y.dest) ∘ corec fun x => (TypeVec.id ::: fun i => i.dest) <$$> x) <$$>
      (TypeVec.id ::: fun i => i.dest) <$$> y.dest =
    (TypeVec.id ::: Quot.mk fun x y => x = mk y.dest) <$$> y.dest

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝ x y : Cofix F α
h : x = mk y.dest
⊢ (TypeVec.id ::: Quot.mk fun x y => x = mk y.dest) <$$> x.dest =
    (TypeVec.id ::: Quot.mk fun x y => x = mk y.dest) <$$> y.dest

Tactic:
rw [h]

Result:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝ x y : Cofix F α
h : x = mk y.dest
⊢ (TypeVec.id ::: Quot.mk fun x y => x = mk y.dest) <$$> (mk y.dest).dest =
    (TypeVec.id ::: Quot.mk fun x y => x = mk y.dest) <$$> y.dest

Proof state:
case e_a.h
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝ x y : Cofix F α
h : x = mk y.dest
⊢ (((Quot.mk fun x y => x = mk y.dest) ∘ mk) ∘ fun i => i.dest) = Quot.mk fun x y => x = mk y.dest

Tactic:
funext x

Result:
case e_a.h.h
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝¹ x✝ y : Cofix F α
h : x✝ = mk y.dest
x : Cofix F α
⊢ (((Quot.mk fun x y => x = mk y.dest) ∘ mk) ∘ fun i => i.dest) x = Quot.mk (fun x y => x = mk y.dest) x

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝ x y : Cofix F α
h : x = mk y.dest
⊢ (TypeVec.id ::: Quot.mk fun x y => x = mk y.dest) <$$> (mk y.dest).dest =
    (TypeVec.id ::: Quot.mk fun x y => x = mk y.dest) <$$> y.dest

Tactic:
conv =>
  lhs
  congr
  rfl
  rw [Cofix.mk]
  rw [Cofix.dest_corec]

Result:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝ x y : Cofix F α
h : x = mk y.dest
⊢ (TypeVec.id ::: Quot.mk fun x y => x = mk y.dest) <$$>
      (TypeVec.id ::: corec fun x => (TypeVec.id ::: fun i => i.dest) <$$> x) <$$>
        (TypeVec.id ::: fun i => i.dest) <$$> y.dest =
    (TypeVec.id ::: Quot.mk fun x y => x = mk y.dest) <$$> y.dest

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : Cofix F α
⊢ mk x.dest = x

Tactic:
apply Cofix.bisim_rel (fun x y : Cofix F α => x = Cofix.mk (Cofix.dest y)) _ _ _ rfl

Result:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : Cofix F α
⊢ ∀ (x y : Cofix F α),
    (fun x y => x = mk y.dest) x y →
      (TypeVec.id ::: Quot.mk fun x y => x = mk y.dest) <$$> x.dest =
        (TypeVec.id ::: Quot.mk fun x y => x = mk y.dest) <$$> y.dest

Proof state:
case e_a.h.h.a
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝¹ x✝ y : Cofix F α
h : x✝ = mk y.dest
x : Cofix F α
⊢ mk ((fun i => i.dest) x) = mk x.dest

Tactic:
rfl

Result:
no goals

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : Cofix F α
⊢ ∀ (x y : Cofix F α),
    x = mk y.dest →
      (TypeVec.id ::: Quot.mk fun x y => x = mk y.dest) <$$> x.dest =
        (TypeVec.id ::: Quot.mk fun x y => x = mk y.dest) <$$> y.dest

Tactic:
intro x y h

Result:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝ x y : Cofix F α
h : x = mk y.dest
⊢ (TypeVec.id ::: Quot.mk fun x y => x = mk y.dest) <$$> x.dest =
    (TypeVec.id ::: Quot.mk fun x y => x = mk y.dest) <$$> y.dest

Proof state:
case e_a
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝ x y : Cofix F α
h : x = mk y.dest
⊢ (TypeVec.id ::: ((Quot.mk fun x y => x = mk y.dest) ∘ mk) ∘ fun i => i.dest) =
    (TypeVec.id ::: Quot.mk fun x y => x = mk y.dest)

Tactic:
apply congrArg

Result:
case e_a.h
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝ x y : Cofix F α
h : x = mk y.dest
⊢ (((Quot.mk fun x y => x = mk y.dest) ∘ mk) ∘ fun i => i.dest) = Quot.mk fun x y => x = mk y.dest

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝ x y : Cofix F α
h : x = mk y.dest
⊢ (TypeVec.id ::: ((Quot.mk fun x y => x = mk y.dest) ∘ mk) ∘ fun i => i.dest) <$$> y.dest =
    (TypeVec.id ::: Quot.mk fun x y => x = mk y.dest) <$$> y.dest

Tactic:
congr

Result:
case e_a
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝ x y : Cofix F α
h : x = mk y.dest
⊢ (TypeVec.id ::: ((Quot.mk fun x y => x = mk y.dest) ∘ mk) ∘ fun i => i.dest) =
    (TypeVec.id ::: Quot.mk fun x y => x = mk y.dest)

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : Cofix F α
⊢ ∀ (x y : Cofix F α),
    (fun x y => x = mk y.dest) x y →
      (TypeVec.id ::: Quot.mk fun x y => x = mk y.dest) <$$> x.dest =
        (TypeVec.id ::: Quot.mk fun x y => x = mk y.dest) <$$> y.dest

Tactic:
dsimp

Result:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : Cofix F α
⊢ ∀ (x y : Cofix F α),
    x = mk y.dest →
      (TypeVec.id ::: Quot.mk fun x y => x = mk y.dest) <$$> x.dest =
        (TypeVec.id ::: Quot.mk fun x y => x = mk y.dest) <$$> y.dest

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝ x y : Cofix F α
h : x = mk y.dest
⊢ (TypeVec.id ::: (Quot.mk fun x y => x = mk y.dest) ∘ corec fun x => (TypeVec.id ::: fun i => i.dest) <$$> x) <$$>
      (TypeVec.id ::: fun i => i.dest) <$$> y.dest =
    (TypeVec.id ::: Quot.mk fun x y => x = mk y.dest) <$$> y.dest

Tactic:
rw [← comp_map, ← appendFun_comp, id_comp, ← Cofix.mk]

Result:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝ x y : Cofix F α
h : x = mk y.dest
⊢ (TypeVec.id ::: ((Quot.mk fun x y => x = mk y.dest) ∘ mk) ∘ fun i => i.dest) <$$> y.dest =
    (TypeVec.id ::: Quot.mk fun x y => x = mk y.dest) <$$> y.dest

Proof state:
case e_a.h.h
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝¹ x✝ y : Cofix F α
h : x✝ = mk y.dest
x : Cofix F α
⊢ (((Quot.mk fun x y => x = mk y.dest) ∘ mk) ∘ fun i => i.dest) x = Quot.mk (fun x y => x = mk y.dest) x

Tactic:
apply Quot.sound

Result:
case e_a.h.h.a
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝¹ x✝ y : Cofix F α
h : x✝ = mk y.dest
x : Cofix F α
⊢ mk ((fun i => i.dest) x) = mk x.dest