[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : β → F (α ::: β)
x : β
⊢ M.dest (P F) (corecF g x) = (TypeVec.id ::: corecF g) <$$> repr (g x)
[PROOFSTEP]
rw [corecF, M.dest_corec]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α β : TypeVec n
g : α ⟹ β
⊢ ∀ (a b : M (P F) α), Mcongr a b → (fun x => Quot.mk Mcongr (g <$$> x)) a = (fun x => Quot.mk Mcongr (g <$$> x)) b
[PROOFSTEP]
rintro aa₁ aa₂ ⟨r, pr, ra₁a₂⟩
[GOAL]
case intro.intro
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α β : TypeVec n
g : α ⟹ β
aa₁ aa₂ : M (P F) α
r : M (P F) α → M (P F) α → Prop
pr : IsPrecongr r
ra₁a₂ : r aa₁ aa₂
⊢ (fun x => Quot.mk Mcongr (g <$$> x)) aa₁ = (fun x => Quot.mk Mcongr (g <$$> x)) aa₂
[PROOFSTEP]
apply Quot.sound
[GOAL]
case intro.intro.a
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α β : TypeVec n
g : α ⟹ β
aa₁ aa₂ : M (P F) α
r : M (P F) α → M (P F) α → Prop
pr : IsPrecongr r
ra₁a₂ : r aa₁ aa₂
⊢ Mcongr (g <$$> aa₁) (g <$$> aa₂)
[PROOFSTEP]
let r' b₁ b₂ := ∃ a₁ a₂ : q.P.M α, r a₁ a₂ ∧ b₁ = g <$$> a₁ ∧ b₂ = g <$$> a₂
[GOAL]
case intro.intro.a
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α β : TypeVec n
g : α ⟹ β
aa₁ aa₂ : M (P F) α
r : M (P F) α → M (P F) α → Prop
pr : IsPrecongr r
ra₁a₂ : r aa₁ aa₂
r' : M (P F) β → M (P F) β → Prop := fun b₁ b₂ => ∃ a₁ a₂, r a₁ a₂ ∧ b₁ = g <$$> a₁ ∧ b₂ = g <$$> a₂
⊢ Mcongr (g <$$> aa₁) (g <$$> aa₂)
[PROOFSTEP]
use r'
[GOAL]
case h
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α β : TypeVec n
g : α ⟹ β
aa₁ aa₂ : M (P F) α
r : M (P F) α → M (P F) α → Prop
pr : IsPrecongr r
ra₁a₂ : r aa₁ aa₂
r' : M (P F) β → M (P F) β → Prop := fun b₁ b₂ => ∃ a₁ a₂, r a₁ a₂ ∧ b₁ = g <$$> a₁ ∧ b₂ = g <$$> a₂
⊢ IsPrecongr r' ∧ r' (g <$$> aa₁) (g <$$> aa₂)
[PROOFSTEP]
constructor
[GOAL]
case h.left
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α β : TypeVec n
g : α ⟹ β
aa₁ aa₂ : M (P F) α
r : M (P F) α → M (P F) α → Prop
pr : IsPrecongr r
ra₁a₂ : r aa₁ aa₂
r' : M (P F) β → M (P F) β → Prop := fun b₁ b₂ => ∃ a₁ a₂, r a₁ a₂ ∧ b₁ = g <$$> a₁ ∧ b₂ = g <$$> a₂
⊢ IsPrecongr r'
[PROOFSTEP]
show IsPrecongr r'
[GOAL]
case h.left
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α β : TypeVec n
g : α ⟹ β
aa₁ aa₂ : M (P F) α
r : M (P F) α → M (P F) α → Prop
pr : IsPrecongr r
ra₁a₂ : r aa₁ aa₂
r' : M (P F) β → M (P F) β → Prop := fun b₁ b₂ => ∃ a₁ a₂, r a₁ a₂ ∧ b₁ = g <$$> a₁ ∧ b₂ = g <$$> a₂
⊢ IsPrecongr r'
[PROOFSTEP]
rintro b₁ b₂ ⟨a₁, a₂, ra₁a₂, b₁eq, b₂eq⟩
[GOAL]
case h.left.intro.intro.intro.intro
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α β : TypeVec n
g : α ⟹ β
aa₁ aa₂ : M (P F) α
r : M (P F) α → M (P F) α → Prop
pr : IsPrecongr r
ra₁a₂✝ : r aa₁ aa₂
r' : M (P F) β → M (P F) β → Prop := fun b₁ b₂ => ∃ a₁ a₂, r a₁ a₂ ∧ b₁ = g <$$> a₁ ∧ b₂ = g <$$> a₂
b₁ b₂ : M (P F) β
a₁ a₂ : M (P F) α
ra₁a₂ : r a₁ a₂
b₁eq : b₁ = g <$$> a₁
b₂eq : b₂ = g <$$> a₂
⊢ abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) b₁) = abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) b₂)
[PROOFSTEP]
let u : Quot r → Quot r' :=
  Quot.lift (fun x : q.P.M α => Quot.mk r' (g <$$> x))
    (by
      intro a₁ a₂ ra₁a₂
      apply Quot.sound
      exact ⟨a₁, a₂, ra₁a₂, rfl, rfl⟩)
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α β : TypeVec n
g : α ⟹ β
aa₁ aa₂ : M (P F) α
r : M (P F) α → M (P F) α → Prop
pr : IsPrecongr r
ra₁a₂✝ : r aa₁ aa₂
r' : M (P F) β → M (P F) β → Prop := fun b₁ b₂ => ∃ a₁ a₂, r a₁ a₂ ∧ b₁ = g <$$> a₁ ∧ b₂ = g <$$> a₂
b₁ b₂ : M (P F) β
a₁ a₂ : M (P F) α
ra₁a₂ : r a₁ a₂
b₁eq : b₁ = g <$$> a₁
b₂eq : b₂ = g <$$> a₂
⊢ ∀ (a b : M (P F) α), r a b → (fun x => Quot.mk r' (g <$$> x)) a = (fun x => Quot.mk r' (g <$$> x)) b
[PROOFSTEP]
intro a₁ a₂ ra₁a₂
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α β : TypeVec n
g : α ⟹ β
aa₁ aa₂ : M (P F) α
r : M (P F) α → M (P F) α → Prop
pr : IsPrecongr r
ra₁a₂✝¹ : r aa₁ aa₂
r' : M (P F) β → M (P F) β → Prop := fun b₁ b₂ => ∃ a₁ a₂, r a₁ a₂ ∧ b₁ = g <$$> a₁ ∧ b₂ = g <$$> a₂
b₁ b₂ : M (P F) β
a₁✝ a₂✝ : M (P F) α
ra₁a₂✝ : r a₁✝ a₂✝
b₁eq : b₁ = g <$$> a₁✝
b₂eq : b₂ = g <$$> a₂✝
a₁ a₂ : M (P F) α
ra₁a₂ : r a₁ a₂
⊢ (fun x => Quot.mk r' (g <$$> x)) a₁ = (fun x => Quot.mk r' (g <$$> x)) a₂
[PROOFSTEP]
apply Quot.sound
[GOAL]
case a
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α β : TypeVec n
g : α ⟹ β
aa₁ aa₂ : M (P F) α
r : M (P F) α → M (P F) α → Prop
pr : IsPrecongr r
ra₁a₂✝¹ : r aa₁ aa₂
r' : M (P F) β → M (P F) β → Prop := fun b₁ b₂ => ∃ a₁ a₂, r a₁ a₂ ∧ b₁ = g <$$> a₁ ∧ b₂ = g <$$> a₂
b₁ b₂ : M (P F) β
a₁✝ a₂✝ : M (P F) α
ra₁a₂✝ : r a₁✝ a₂✝
b₁eq : b₁ = g <$$> a₁✝
b₂eq : b₂ = g <$$> a₂✝
a₁ a₂ : M (P F) α
ra₁a₂ : r a₁ a₂
⊢ r' (g <$$> a₁) (g <$$> a₂)
[PROOFSTEP]
exact ⟨a₁, a₂, ra₁a₂, rfl, rfl⟩
[GOAL]
case h.left.intro.intro.intro.intro
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α β : TypeVec n
g : α ⟹ β
aa₁ aa₂ : M (P F) α
r : M (P F) α → M (P F) α → Prop
pr : IsPrecongr r
ra₁a₂✝ : r aa₁ aa₂
r' : M (P F) β → M (P F) β → Prop := fun b₁ b₂ => ∃ a₁ a₂, r a₁ a₂ ∧ b₁ = g <$$> a₁ ∧ b₂ = g <$$> a₂
b₁ b₂ : M (P F) β
a₁ a₂ : M (P F) α
ra₁a₂ : r a₁ a₂
b₁eq : b₁ = g <$$> a₁
b₂eq : b₂ = g <$$> a₂
u : Quot r → Quot r' :=
  Quot.lift (fun x => Quot.mk r' (g <$$> x))
    (_ : ∀ (a₁ a₂ : M (P F) α), r a₁ a₂ → Quot.mk r' (g <$$> a₁) = Quot.mk r' (g <$$> a₂))
⊢ abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) b₁) = abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) b₂)
[PROOFSTEP]
have hu : (Quot.mk r' ∘ fun x : q.P.M α => g <$$> x) = u ∘ Quot.mk r :=
  by
  ext x
  rfl
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α β : TypeVec n
g : α ⟹ β
aa₁ aa₂ : M (P F) α
r : M (P F) α → M (P F) α → Prop
pr : IsPrecongr r
ra₁a₂✝ : r aa₁ aa₂
r' : M (P F) β → M (P F) β → Prop := fun b₁ b₂ => ∃ a₁ a₂, r a₁ a₂ ∧ b₁ = g <$$> a₁ ∧ b₂ = g <$$> a₂
b₁ b₂ : M (P F) β
a₁ a₂ : M (P F) α
ra₁a₂ : r a₁ a₂
b₁eq : b₁ = g <$$> a₁
b₂eq : b₂ = g <$$> a₂
u : Quot r → Quot r' :=
  Quot.lift (fun x => Quot.mk r' (g <$$> x))
    (_ : ∀ (a₁ a₂ : M (P F) α), r a₁ a₂ → Quot.mk r' (g <$$> a₁) = Quot.mk r' (g <$$> a₂))
⊢ (Quot.mk r' ∘ fun x => g <$$> x) = u ∘ Quot.mk r
[PROOFSTEP]
ext x
[GOAL]
case h
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α β : TypeVec n
g : α ⟹ β
aa₁ aa₂ : M (P F) α
r : M (P F) α → M (P F) α → Prop
pr : IsPrecongr r
ra₁a₂✝ : r aa₁ aa₂
r' : M (P F) β → M (P F) β → Prop := fun b₁ b₂ => ∃ a₁ a₂, r a₁ a₂ ∧ b₁ = g <$$> a₁ ∧ b₂ = g <$$> a₂
b₁ b₂ : M (P F) β
a₁ a₂ : M (P F) α
ra₁a₂ : r a₁ a₂
b₁eq : b₁ = g <$$> a₁
b₂eq : b₂ = g <$$> a₂
u : Quot r → Quot r' :=
  Quot.lift (fun x => Quot.mk r' (g <$$> x))
    (_ : ∀ (a₁ a₂ : M (P F) α), r a₁ a₂ → Quot.mk r' (g <$$> a₁) = Quot.mk r' (g <$$> a₂))
x : M (P F) α
⊢ (Quot.mk r' ∘ fun x => g <$$> x) x = (u ∘ Quot.mk r) x
[PROOFSTEP]
rfl
[GOAL]
case h.left.intro.intro.intro.intro
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α β : TypeVec n
g : α ⟹ β
aa₁ aa₂ : M (P F) α
r : M (P F) α → M (P F) α → Prop
pr : IsPrecongr r
ra₁a₂✝ : r aa₁ aa₂
r' : M (P F) β → M (P F) β → Prop := fun b₁ b₂ => ∃ a₁ a₂, r a₁ a₂ ∧ b₁ = g <$$> a₁ ∧ b₂ = g <$$> a₂
b₁ b₂ : M (P F) β
a₁ a₂ : M (P F) α
ra₁a₂ : r a₁ a₂
b₁eq : b₁ = g <$$> a₁
b₂eq : b₂ = g <$$> a₂
u : Quot r → Quot r' :=
  Quot.lift (fun x => Quot.mk r' (g <$$> x))
    (_ : ∀ (a₁ a₂ : M (P F) α), r a₁ a₂ → Quot.mk r' (g <$$> a₁) = Quot.mk r' (g <$$> a₂))
hu : (Quot.mk r' ∘ fun x => g <$$> x) = u ∘ Quot.mk r
⊢ abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) b₁) = abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) b₂)
[PROOFSTEP]
rw [b₁eq, b₂eq, M.dest_map, M.dest_map, ← q.P.comp_map, ← q.P.comp_map]
[GOAL]
case h.left.intro.intro.intro.intro
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α β : TypeVec n
g : α ⟹ β
aa₁ aa₂ : M (P F) α
r : M (P F) α → M (P F) α → Prop
pr : IsPrecongr r
ra₁a₂✝ : r aa₁ aa₂
r' : M (P F) β → M (P F) β → Prop := fun b₁ b₂ => ∃ a₁ a₂, r a₁ a₂ ∧ b₁ = g <$$> a₁ ∧ b₂ = g <$$> a₂
b₁ b₂ : M (P F) β
a₁ a₂ : M (P F) α
ra₁a₂ : r a₁ a₂
b₁eq : b₁ = g <$$> a₁
b₂eq : b₂ = g <$$> a₂
u : Quot r → Quot r' :=
  Quot.lift (fun x => Quot.mk r' (g <$$> x))
    (_ : ∀ (a₁ a₂ : M (P F) α), r a₁ a₂ → Quot.mk r' (g <$$> a₁) = Quot.mk r' (g <$$> a₂))
hu : (Quot.mk r' ∘ fun x => g <$$> x) = u ∘ Quot.mk r
⊢ abs (((TypeVec.id ::: Quot.mk r') ⊚ (g ::: fun x => g <$$> x)) <$$> M.dest (P F) a₁) =
    abs (((TypeVec.id ::: Quot.mk r') ⊚ (g ::: fun x => g <$$> x)) <$$> M.dest (P F) a₂)
[PROOFSTEP]
rw [← appendFun_comp, id_comp, hu, ← comp_id g, appendFun_comp]
[GOAL]
case h.left.intro.intro.intro.intro
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α β : TypeVec n
g : α ⟹ β
aa₁ aa₂ : M (P F) α
r : M (P F) α → M (P F) α → Prop
pr : IsPrecongr r
ra₁a₂✝ : r aa₁ aa₂
r' : M (P F) β → M (P F) β → Prop := fun b₁ b₂ => ∃ a₁ a₂, r a₁ a₂ ∧ b₁ = g <$$> a₁ ∧ b₂ = g <$$> a₂
b₁ b₂ : M (P F) β
a₁ a₂ : M (P F) α
ra₁a₂ : r a₁ a₂
b₁eq : b₁ = g <$$> a₁
b₂eq : b₂ = g <$$> a₂
u : Quot r → Quot r' :=
  Quot.lift (fun x => Quot.mk r' (g <$$> x))
    (_ : ∀ (a₁ a₂ : M (P F) α), r a₁ a₂ → Quot.mk r' (g <$$> a₁) = Quot.mk r' (g <$$> a₂))
hu : (Quot.mk r' ∘ fun x => g <$$> x) = u ∘ Quot.mk r
⊢ abs (((g ::: u) ⊚ (TypeVec.id ::: Quot.mk r)) <$$> M.dest (P F) a₁) =
    abs (((g ::: u) ⊚ (TypeVec.id ::: Quot.mk r)) <$$> M.dest (P F) a₂)
[PROOFSTEP]
rw [q.P.comp_map, q.P.comp_map, abs_map, pr ra₁a₂, ← abs_map]
[GOAL]
case h.right
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α β : TypeVec n
g : α ⟹ β
aa₁ aa₂ : M (P F) α
r : M (P F) α → M (P F) α → Prop
pr : IsPrecongr r
ra₁a₂ : r aa₁ aa₂
r' : M (P F) β → M (P F) β → Prop := fun b₁ b₂ => ∃ a₁ a₂, r a₁ a₂ ∧ b₁ = g <$$> a₁ ∧ b₂ = g <$$> a₂
⊢ r' (g <$$> aa₁) (g <$$> aa₂)
[PROOFSTEP]
show r' (g <$$> aa₁) (g <$$> aa₂)
[GOAL]
case h.right
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α β : TypeVec n
g : α ⟹ β
aa₁ aa₂ : M (P F) α
r : M (P F) α → M (P F) α → Prop
pr : IsPrecongr r
ra₁a₂ : r aa₁ aa₂
r' : M (P F) β → M (P F) β → Prop := fun b₁ b₂ => ∃ a₁ a₂, r a₁ a₂ ∧ b₁ = g <$$> a₁ ∧ b₂ = g <$$> a₂
⊢ r' (g <$$> aa₁) (g <$$> aa₂)
[PROOFSTEP]
exact ⟨aa₁, aa₂, ra₁a₂, rfl, rfl⟩
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
⊢ ∀ (a b : M (P F) α),
    Mcongr a b →
      (fun x => (TypeVec.id ::: Quot.mk Mcongr) <$$> abs (M.dest (P F) x)) a =
        (fun x => (TypeVec.id ::: Quot.mk Mcongr) <$$> abs (M.dest (P F) x)) b
[PROOFSTEP]
rintro x y ⟨r, pr, rxy⟩
[GOAL]
case intro.intro
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
x y : M (P F) α
r : M (P F) α → M (P F) α → Prop
pr : IsPrecongr r
rxy : r x y
⊢ (fun x => (TypeVec.id ::: Quot.mk Mcongr) <$$> abs (M.dest (P F) x)) x =
    (fun x => (TypeVec.id ::: Quot.mk Mcongr) <$$> abs (M.dest (P F) x)) y
[PROOFSTEP]
dsimp
[GOAL]
case intro.intro
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
x y : M (P F) α
r : M (P F) α → M (P F) α → Prop
pr : IsPrecongr r
rxy : r x y
⊢ (TypeVec.id ::: Quot.mk Mcongr) <$$> abs (M.dest (P F) x) = (TypeVec.id ::: Quot.mk Mcongr) <$$> abs (M.dest (P F) y)
[PROOFSTEP]
have : ∀ x y, r x y → Mcongr x y := by
  intro x y h
  exact ⟨r, pr, h⟩
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
x y : M (P F) α
r : M (P F) α → M (P F) α → Prop
pr : IsPrecongr r
rxy : r x y
⊢ ∀ (x y : M (P F) α), r x y → Mcongr x y
[PROOFSTEP]
intro x y h
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
x✝ y✝ : M (P F) α
r : M (P F) α → M (P F) α → Prop
pr : IsPrecongr r
rxy : r x✝ y✝
x y : M (P F) α
h : r x y
⊢ Mcongr x y
[PROOFSTEP]
exact ⟨r, pr, h⟩
[GOAL]
case intro.intro
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
x y : M (P F) α
r : M (P F) α → M (P F) α → Prop
pr : IsPrecongr r
rxy : r x y
this : ∀ (x y : M (P F) α), r x y → Mcongr x y
⊢ (TypeVec.id ::: Quot.mk Mcongr) <$$> abs (M.dest (P F) x) = (TypeVec.id ::: Quot.mk Mcongr) <$$> abs (M.dest (P F) y)
[PROOFSTEP]
rw [← Quot.factor_mk_eq _ _ this]
[GOAL]
case intro.intro
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
x y : M (P F) α
r : M (P F) α → M (P F) α → Prop
pr : IsPrecongr r
rxy : r x y
this : ∀ (x y : M (P F) α), r x y → Mcongr x y
⊢ (TypeVec.id ::: Quot.factor (fun x y => r x y) (fun x y => Mcongr x y) this ∘ Quot.mk fun x y => r x y) <$$>
      abs (M.dest (P F) x) =
    (TypeVec.id ::: Quot.factor (fun x y => r x y) (fun x y => Mcongr x y) this ∘ Quot.mk fun x y => r x y) <$$>
      abs (M.dest (P F) y)
[PROOFSTEP]
conv =>
  lhs
  rw [appendFun_comp_id, comp_map, ← abs_map, pr rxy, abs_map, ← comp_map, ← appendFun_comp_id]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
x y : M (P F) α
r : M (P F) α → M (P F) α → Prop
pr : IsPrecongr r
rxy : r x y
this : ∀ (x y : M (P F) α), r x y → Mcongr x y
| (TypeVec.id ::: Quot.factor (fun x y => r x y) (fun x y => Mcongr x y) this ∘ Quot.mk fun x y => r x y) <$$>
      abs (M.dest (P F) x) =
    (TypeVec.id ::: Quot.factor (fun x y => r x y) (fun x y => Mcongr x y) this ∘ Quot.mk fun x y => r x y) <$$>
      abs (M.dest (P F) y)
[PROOFSTEP]
  lhs
  rw [appendFun_comp_id, comp_map, ← abs_map, pr rxy, abs_map, ← comp_map, ← appendFun_comp_id]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
x y : M (P F) α
r : M (P F) α → M (P F) α → Prop
pr : IsPrecongr r
rxy : r x y
this : ∀ (x y : M (P F) α), r x y → Mcongr x y
| (TypeVec.id ::: Quot.factor (fun x y => r x y) (fun x y => Mcongr x y) this ∘ Quot.mk fun x y => r x y) <$$>
      abs (M.dest (P F) x) =
    (TypeVec.id ::: Quot.factor (fun x y => r x y) (fun x y => Mcongr x y) this ∘ Quot.mk fun x y => r x y) <$$>
      abs (M.dest (P F) y)
[PROOFSTEP]
  lhs
  rw [appendFun_comp_id, comp_map, ← abs_map, pr rxy, abs_map, ← comp_map, ← appendFun_comp_id]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
x y : M (P F) α
r : M (P F) α → M (P F) α → Prop
pr : IsPrecongr r
rxy : r x y
this : ∀ (x y : M (P F) α), r x y → Mcongr x y
| (TypeVec.id ::: Quot.factor (fun x y => r x y) (fun x y => Mcongr x y) this ∘ Quot.mk fun x y => r x y) <$$>
      abs (M.dest (P F) x) =
    (TypeVec.id ::: Quot.factor (fun x y => r x y) (fun x y => Mcongr x y) this ∘ Quot.mk fun x y => r x y) <$$>
      abs (M.dest (P F) y)
[PROOFSTEP]
lhs
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
x y : M (P F) α
r : M (P F) α → M (P F) α → Prop
pr : IsPrecongr r
rxy : r x y
this : ∀ (x y : M (P F) α), r x y → Mcongr x y
| (TypeVec.id ::: Quot.factor (fun x y => r x y) (fun x y => Mcongr x y) this ∘ Quot.mk fun x y => r x y) <$$>
    abs (M.dest (P F) x)
[PROOFSTEP]
rw [appendFun_comp_id, comp_map, ← abs_map, pr rxy, abs_map, ← comp_map, ← appendFun_comp_id]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : β → F (α ::: β)
x : β
⊢ dest (corec g x) = (TypeVec.id ::: corec g) <$$> g x
[PROOFSTEP]
conv =>
  lhs
  rw [Cofix.dest, Cofix.corec];
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : β → F (α ::: β)
x : β
| dest (corec g x) = (TypeVec.id ::: corec g) <$$> g x
[PROOFSTEP]
  lhs
  rw [Cofix.dest, Cofix.corec];
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : β → F (α ::: β)
x : β
| dest (corec g x) = (TypeVec.id ::: corec g) <$$> g x
[PROOFSTEP]
  lhs
  rw [Cofix.dest, Cofix.corec];
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : β → F (α ::: β)
x : β
| dest (corec g x) = (TypeVec.id ::: corec g) <$$> g x
[PROOFSTEP]
lhs
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : β → F (α ::: β)
x : β
| dest (corec g x)
[PROOFSTEP]
rw [Cofix.dest, Cofix.corec]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : β → F (α ::: β)
x : β
⊢ Quot.lift (fun x => (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x))
      (_ :
        ∀ (x y : M (P F) α),
          Mcongr x y →
            (fun x => (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) x =
              (fun x => (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) y)
      (Quot.mk Mcongr (corecF g x)) =
    (TypeVec.id ::: corec g) <$$> g x
[PROOFSTEP]
dsimp
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : β → F (α ::: β)
x : β
⊢ (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) (corecF g x)) = (TypeVec.id ::: corec g) <$$> g x
[PROOFSTEP]
rw [corecF_eq, abs_map, abs_repr, ← comp_map, ← appendFun_comp]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : β → F (α ::: β)
x : β
⊢ (TypeVec.id ⊚ TypeVec.id ::: Quot.mk Mcongr ∘ corecF g) <$$> g x = (TypeVec.id ::: corec g) <$$> g x
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
⊢ ∀ (x y : Cofix F α), r x y → x = y
[PROOFSTEP]
intro x
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
x : Cofix F α
⊢ ∀ (y : Cofix F α), r x y → x = y
[PROOFSTEP]
rcases x
[GOAL]
case mk
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
x : Cofix F α
a✝ : M (P F) α
⊢ ∀ (y : Cofix F α), r (Quot.mk Mcongr a✝) y → Quot.mk Mcongr a✝ = y
[PROOFSTEP]
clear x
[GOAL]
case mk
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
a✝ : M (P F) α
⊢ ∀ (y : Cofix F α), r (Quot.mk Mcongr a✝) y → Quot.mk Mcongr a✝ = y
[PROOFSTEP]
rename M (P F) α => x
[GOAL]
case mk
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
x : M (P F) α
⊢ ∀ (y : Cofix F α), r (Quot.mk Mcongr x) y → Quot.mk Mcongr x = y
[PROOFSTEP]
intro y
[GOAL]
case mk
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
x : M (P F) α
y : Cofix F α
⊢ r (Quot.mk Mcongr x) y → Quot.mk Mcongr x = y
[PROOFSTEP]
rcases y
[GOAL]
case mk.mk
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
x : M (P F) α
y : Cofix F α
a✝ : M (P F) α
⊢ r (Quot.mk Mcongr x) (Quot.mk Mcongr a✝) → Quot.mk Mcongr x = Quot.mk Mcongr a✝
[PROOFSTEP]
clear y
[GOAL]
case mk.mk
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
x a✝ : M (P F) α
⊢ r (Quot.mk Mcongr x) (Quot.mk Mcongr a✝) → Quot.mk Mcongr x = Quot.mk Mcongr a✝
[PROOFSTEP]
rename M (P F) α => y
[GOAL]
case mk.mk
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
x y : M (P F) α
⊢ r (Quot.mk Mcongr x) (Quot.mk Mcongr y) → Quot.mk Mcongr x = Quot.mk Mcongr y
[PROOFSTEP]
intro rxy
[GOAL]
case mk.mk
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
x y : M (P F) α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
⊢ Quot.mk Mcongr x = Quot.mk Mcongr y
[PROOFSTEP]
apply Quot.sound
[GOAL]
case mk.mk.a
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
x y : M (P F) α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
⊢ Mcongr x y
[PROOFSTEP]
let r' := fun x y => r (Quot.mk _ x) (Quot.mk _ y)
[GOAL]
case mk.mk.a
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
x y : M (P F) α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : M (P F) α → M (P F) α → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
⊢ Mcongr x y
[PROOFSTEP]
have hr' : r' = fun x y => r (Quot.mk _ x) (Quot.mk _ y) := by rfl
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
x y : M (P F) α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : M (P F) α → M (P F) α → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
⊢ r' = fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
[PROOFSTEP]
rfl
[GOAL]
case mk.mk.a
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
x y : M (P F) α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : M (P F) α → M (P F) α → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
⊢ Mcongr x y
[PROOFSTEP]
have : IsPrecongr r' := by
  intro a b r'ab
  have h₀ :
    appendFun id (Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest q.P a) =
      appendFun id (Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest q.P b) :=
    by rw [appendFun_comp_id, comp_map, comp_map]; exact h _ _ r'ab
  have h₁ : ∀ u v : q.P.M α, Mcongr u v → Quot.mk r' u = Quot.mk r' v :=
    by
    intro u v cuv
    apply Quot.sound
    dsimp [hr']
    rw [Quot.sound cuv]
    apply h'
  let f : Quot r → Quot r' :=
    Quot.lift (Quot.lift (Quot.mk r') h₁)
      (by
        intro c
        apply
          Quot.inductionOn (motive := fun c => ∀ b, r c b → Quot.lift (Quot.mk r') h₁ c = Quot.lift (Quot.mk r') h₁ b) c
        clear c
        intro c d
        apply
          Quot.inductionOn (motive := fun d =>
            r (Quot.mk Mcongr c) d → Quot.lift (Quot.mk r') h₁ (Quot.mk Mcongr c) = Quot.lift (Quot.mk r') h₁ d) d
        clear d
        intro d rcd; apply Quot.sound; apply rcd)
  have : f ∘ Quot.mk r ∘ Quot.mk Mcongr = Quot.mk r' := rfl
  rw [← this, appendFun_comp_id, q.P.comp_map, q.P.comp_map, abs_map, abs_map, abs_map, abs_map, h₀]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
x y : M (P F) α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : M (P F) α → M (P F) α → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
⊢ IsPrecongr r'
[PROOFSTEP]
intro a b r'ab
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
x y : M (P F) α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : M (P F) α → M (P F) α → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : M (P F) α
r'ab : r' a b
⊢ MvQPF.abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) a) =
    MvQPF.abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) b)
[PROOFSTEP]
have h₀ :
  appendFun id (Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest q.P a) =
    appendFun id (Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest q.P b) :=
  by rw [appendFun_comp_id, comp_map, comp_map]; exact h _ _ r'ab
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
x y : M (P F) α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : M (P F) α → M (P F) α → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : M (P F) α
r'ab : r' a b
⊢ (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a) =
    (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) b)
[PROOFSTEP]
rw [appendFun_comp_id, comp_map, comp_map]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
x y : M (P F) α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : M (P F) α → M (P F) α → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : M (P F) α
r'ab : r' a b
⊢ (TypeVec.id ::: Quot.mk r) <$$> (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a) =
    (TypeVec.id ::: Quot.mk r) <$$> (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) b)
[PROOFSTEP]
exact h _ _ r'ab
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
x y : M (P F) α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : M (P F) α → M (P F) α → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : M (P F) α
r'ab : r' a b
h₀ :
  (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a) =
    (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) b)
⊢ MvQPF.abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) a) =
    MvQPF.abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) b)
[PROOFSTEP]
have h₁ : ∀ u v : q.P.M α, Mcongr u v → Quot.mk r' u = Quot.mk r' v :=
  by
  intro u v cuv
  apply Quot.sound
  dsimp [hr']
  rw [Quot.sound cuv]
  apply h'
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
x y : M (P F) α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : M (P F) α → M (P F) α → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : M (P F) α
r'ab : r' a b
h₀ :
  (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a) =
    (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) b)
⊢ ∀ (u v : M (P F) α), Mcongr u v → Quot.mk r' u = Quot.mk r' v
[PROOFSTEP]
intro u v cuv
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
x y : M (P F) α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : M (P F) α → M (P F) α → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : M (P F) α
r'ab : r' a b
h₀ :
  (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a) =
    (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) b)
u v : M (P F) α
cuv : Mcongr u v
⊢ Quot.mk r' u = Quot.mk r' v
[PROOFSTEP]
apply Quot.sound
[GOAL]
case a
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
x y : M (P F) α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : M (P F) α → M (P F) α → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : M (P F) α
r'ab : r' a b
h₀ :
  (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a) =
    (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) b)
u v : M (P F) α
cuv : Mcongr u v
⊢ r' u v
[PROOFSTEP]
dsimp [hr']
[GOAL]
case a
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
x y : M (P F) α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : M (P F) α → M (P F) α → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : M (P F) α
r'ab : r' a b
h₀ :
  (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a) =
    (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) b)
u v : M (P F) α
cuv : Mcongr u v
⊢ r (Quot.mk Mcongr u) (Quot.mk Mcongr v)
[PROOFSTEP]
rw [Quot.sound cuv]
[GOAL]
case a
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
x y : M (P F) α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : M (P F) α → M (P F) α → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : M (P F) α
r'ab : r' a b
h₀ :
  (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a) =
    (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) b)
u v : M (P F) α
cuv : Mcongr u v
⊢ r (Quot.mk Mcongr v) (Quot.mk Mcongr v)
[PROOFSTEP]
apply h'
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
x y : M (P F) α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : M (P F) α → M (P F) α → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : M (P F) α
r'ab : r' a b
h₀ :
  (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a) =
    (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) b)
h₁ : ∀ (u v : M (P F) α), Mcongr u v → Quot.mk r' u = Quot.mk r' v
⊢ MvQPF.abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) a) =
    MvQPF.abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) b)
[PROOFSTEP]
let f : Quot r → Quot r' :=
  Quot.lift (Quot.lift (Quot.mk r') h₁)
    (by
      intro c
      apply
        Quot.inductionOn (motive := fun c => ∀ b, r c b → Quot.lift (Quot.mk r') h₁ c = Quot.lift (Quot.mk r') h₁ b) c
      clear c
      intro c d
      apply
        Quot.inductionOn (motive := fun d =>
          r (Quot.mk Mcongr c) d → Quot.lift (Quot.mk r') h₁ (Quot.mk Mcongr c) = Quot.lift (Quot.mk r') h₁ d) d
      clear d
      intro d rcd; apply Quot.sound; apply rcd)
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
x y : M (P F) α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : M (P F) α → M (P F) α → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : M (P F) α
r'ab : r' a b
h₀ :
  (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a) =
    (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) b)
h₁ : ∀ (u v : M (P F) α), Mcongr u v → Quot.mk r' u = Quot.mk r' v
⊢ ∀ (a b : Cofix F α), r a b → Quot.lift (Quot.mk r') h₁ a = Quot.lift (Quot.mk r') h₁ b
[PROOFSTEP]
intro c
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
x y : M (P F) α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : M (P F) α → M (P F) α → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : M (P F) α
r'ab : r' a b
h₀ :
  (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a) =
    (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) b)
h₁ : ∀ (u v : M (P F) α), Mcongr u v → Quot.mk r' u = Quot.mk r' v
c : Cofix F α
⊢ ∀ (b : Cofix F α), r c b → Quot.lift (Quot.mk r') h₁ c = Quot.lift (Quot.mk r') h₁ b
[PROOFSTEP]
apply Quot.inductionOn (motive := fun c => ∀ b, r c b → Quot.lift (Quot.mk r') h₁ c = Quot.lift (Quot.mk r') h₁ b) c
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
x y : M (P F) α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : M (P F) α → M (P F) α → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : M (P F) α
r'ab : r' a b
h₀ :
  (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a) =
    (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) b)
h₁ : ∀ (u v : M (P F) α), Mcongr u v → Quot.mk r' u = Quot.mk r' v
c : Cofix F α
⊢ ∀ (a : M (P F) α) (b : Cofix F α),
    r (Quot.mk Mcongr a) b → Quot.lift (Quot.mk r') h₁ (Quot.mk Mcongr a) = Quot.lift (Quot.mk r') h₁ b
[PROOFSTEP]
clear c
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
x y : M (P F) α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : M (P F) α → M (P F) α → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : M (P F) α
r'ab : r' a b
h₀ :
  (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a) =
    (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) b)
h₁ : ∀ (u v : M (P F) α), Mcongr u v → Quot.mk r' u = Quot.mk r' v
⊢ ∀ (a : M (P F) α) (b : Cofix F α),
    r (Quot.mk Mcongr a) b → Quot.lift (Quot.mk r') h₁ (Quot.mk Mcongr a) = Quot.lift (Quot.mk r') h₁ b
[PROOFSTEP]
intro c d
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
x y : M (P F) α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : M (P F) α → M (P F) α → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : M (P F) α
r'ab : r' a b
h₀ :
  (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a) =
    (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) b)
h₁ : ∀ (u v : M (P F) α), Mcongr u v → Quot.mk r' u = Quot.mk r' v
c : M (P F) α
d : Cofix F α
⊢ r (Quot.mk Mcongr c) d → Quot.lift (Quot.mk r') h₁ (Quot.mk Mcongr c) = Quot.lift (Quot.mk r') h₁ d
[PROOFSTEP]
apply
  Quot.inductionOn (motive := fun d =>
    r (Quot.mk Mcongr c) d → Quot.lift (Quot.mk r') h₁ (Quot.mk Mcongr c) = Quot.lift (Quot.mk r') h₁ d) d
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
x y : M (P F) α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : M (P F) α → M (P F) α → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : M (P F) α
r'ab : r' a b
h₀ :
  (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a) =
    (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) b)
h₁ : ∀ (u v : M (P F) α), Mcongr u v → Quot.mk r' u = Quot.mk r' v
c : M (P F) α
d : Cofix F α
⊢ ∀ (a : M (P F) α),
    r (Quot.mk Mcongr c) (Quot.mk Mcongr a) →
      Quot.lift (Quot.mk r') h₁ (Quot.mk Mcongr c) = Quot.lift (Quot.mk r') h₁ (Quot.mk Mcongr a)
[PROOFSTEP]
clear d
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
x y : M (P F) α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : M (P F) α → M (P F) α → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : M (P F) α
r'ab : r' a b
h₀ :
  (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a) =
    (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) b)
h₁ : ∀ (u v : M (P F) α), Mcongr u v → Quot.mk r' u = Quot.mk r' v
c : M (P F) α
⊢ ∀ (a : M (P F) α),
    r (Quot.mk Mcongr c) (Quot.mk Mcongr a) →
      Quot.lift (Quot.mk r') h₁ (Quot.mk Mcongr c) = Quot.lift (Quot.mk r') h₁ (Quot.mk Mcongr a)
[PROOFSTEP]
intro d rcd
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
x y : M (P F) α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : M (P F) α → M (P F) α → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : M (P F) α
r'ab : r' a b
h₀ :
  (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a) =
    (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) b)
h₁ : ∀ (u v : M (P F) α), Mcongr u v → Quot.mk r' u = Quot.mk r' v
c d : M (P F) α
rcd : r (Quot.mk Mcongr c) (Quot.mk Mcongr d)
⊢ Quot.lift (Quot.mk r') h₁ (Quot.mk Mcongr c) = Quot.lift (Quot.mk r') h₁ (Quot.mk Mcongr d)
[PROOFSTEP]
apply Quot.sound
[GOAL]
case a
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
x y : M (P F) α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : M (P F) α → M (P F) α → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : M (P F) α
r'ab : r' a b
h₀ :
  (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a) =
    (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) b)
h₁ : ∀ (u v : M (P F) α), Mcongr u v → Quot.mk r' u = Quot.mk r' v
c d : M (P F) α
rcd : r (Quot.mk Mcongr c) (Quot.mk Mcongr d)
⊢ r' c d
[PROOFSTEP]
apply rcd
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
x y : M (P F) α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : M (P F) α → M (P F) α → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : M (P F) α
r'ab : r' a b
h₀ :
  (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a) =
    (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) b)
h₁ : ∀ (u v : M (P F) α), Mcongr u v → Quot.mk r' u = Quot.mk r' v
f : Quot r → Quot r' :=
  Quot.lift (Quot.lift (Quot.mk r') h₁)
    (_ : ∀ (c b : Cofix F α), r c b → Quot.lift (Quot.mk r') h₁ c = Quot.lift (Quot.mk r') h₁ b)
⊢ MvQPF.abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) a) =
    MvQPF.abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) b)
[PROOFSTEP]
have : f ∘ Quot.mk r ∘ Quot.mk Mcongr = Quot.mk r' := rfl
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
x y : M (P F) α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : M (P F) α → M (P F) α → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : M (P F) α
r'ab : r' a b
h₀ :
  (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a) =
    (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) b)
h₁ : ∀ (u v : M (P F) α), Mcongr u v → Quot.mk r' u = Quot.mk r' v
f : Quot r → Quot r' :=
  Quot.lift (Quot.lift (Quot.mk r') h₁)
    (_ : ∀ (c b : Cofix F α), r c b → Quot.lift (Quot.mk r') h₁ c = Quot.lift (Quot.mk r') h₁ b)
this : f ∘ Quot.mk r ∘ Quot.mk Mcongr = Quot.mk r'
⊢ MvQPF.abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) a) =
    MvQPF.abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) b)
[PROOFSTEP]
rw [← this, appendFun_comp_id, q.P.comp_map, q.P.comp_map, abs_map, abs_map, abs_map, abs_map, h₀]
[GOAL]
case mk.mk.a
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
x y : M (P F) α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : M (P F) α → M (P F) α → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
this : IsPrecongr r'
⊢ Mcongr x y
[PROOFSTEP]
refine' ⟨r', this, rxy⟩
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
⊢ ∀ (x y : Cofix F α), r x y → x = y
[PROOFSTEP]
let r' (x y) := x = y ∨ r x y
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
r' : Cofix F α → Cofix F α → Prop := fun x y => x = y ∨ r x y
⊢ ∀ (x y : Cofix F α), r x y → x = y
[PROOFSTEP]
intro x y rxy
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
r' : Cofix F α → Cofix F α → Prop := fun x y => x = y ∨ r x y
x y : Cofix F α
rxy : r x y
⊢ x = y
[PROOFSTEP]
apply Cofix.bisim_aux r'
[GOAL]
case h'
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
r' : Cofix F α → Cofix F α → Prop := fun x y => x = y ∨ r x y
x y : Cofix F α
rxy : r x y
⊢ ∀ (x : Cofix F α), r' x x
[PROOFSTEP]
intro x
[GOAL]
case h'
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
r' : Cofix F α → Cofix F α → Prop := fun x y => x = y ∨ r x y
x✝ y : Cofix F α
rxy : r x✝ y
x : Cofix F α
⊢ r' x x
[PROOFSTEP]
left
[GOAL]
case h'.h
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
r' : Cofix F α → Cofix F α → Prop := fun x y => x = y ∨ r x y
x✝ y : Cofix F α
rxy : r x✝ y
x : Cofix F α
⊢ x = x
[PROOFSTEP]
rfl
[GOAL]
case h
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
r' : Cofix F α → Cofix F α → Prop := fun x y => x = y ∨ r x y
x y : Cofix F α
rxy : r x y
⊢ ∀ (x y : Cofix F α), r' x y → (TypeVec.id ::: Quot.mk r') <$$> dest x = (TypeVec.id ::: Quot.mk r') <$$> dest y
[PROOFSTEP]
intro x y r'xy
[GOAL]
case h
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
r' : Cofix F α → Cofix F α → Prop := fun x y => x = y ∨ r x y
x✝ y✝ : Cofix F α
rxy : r x✝ y✝
x y : Cofix F α
r'xy : r' x y
⊢ (TypeVec.id ::: Quot.mk r') <$$> dest x = (TypeVec.id ::: Quot.mk r') <$$> dest y
[PROOFSTEP]
cases r'xy
[GOAL]
case h.inl
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
r' : Cofix F α → Cofix F α → Prop := fun x y => x = y ∨ r x y
x✝ y✝ : Cofix F α
rxy : r x✝ y✝
x y : Cofix F α
h✝ : x = y
⊢ (TypeVec.id ::: Quot.mk r') <$$> dest x = (TypeVec.id ::: Quot.mk r') <$$> dest y
case h.inr
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
r' : Cofix F α → Cofix F α → Prop := fun x y => x = y ∨ r x y
x✝ y✝ : Cofix F α
rxy : r x✝ y✝
x y : Cofix F α
h✝ : r x y
⊢ (TypeVec.id ::: Quot.mk r') <$$> dest x = (TypeVec.id ::: Quot.mk r') <$$> dest y
[PROOFSTEP]
case inl h => rw [h]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h✝ : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
r' : Cofix F α → Cofix F α → Prop := fun x y => x = y ∨ r x y
x✝ y✝ : Cofix F α
rxy : r x✝ y✝
x y : Cofix F α
h : x = y
⊢ (TypeVec.id ::: Quot.mk r') <$$> dest x = (TypeVec.id ::: Quot.mk r') <$$> dest y
[PROOFSTEP]
case inl h => rw [h]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h✝ : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
r' : Cofix F α → Cofix F α → Prop := fun x y => x = y ∨ r x y
x✝ y✝ : Cofix F α
rxy : r x✝ y✝
x y : Cofix F α
h : x = y
⊢ (TypeVec.id ::: Quot.mk r') <$$> dest x = (TypeVec.id ::: Quot.mk r') <$$> dest y
[PROOFSTEP]
rw [h]
[GOAL]
case h.inr
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
r' : Cofix F α → Cofix F α → Prop := fun x y => x = y ∨ r x y
x✝ y✝ : Cofix F α
rxy : r x✝ y✝
x y : Cofix F α
h✝ : r x y
⊢ (TypeVec.id ::: Quot.mk r') <$$> dest x = (TypeVec.id ::: Quot.mk r') <$$> dest y
[PROOFSTEP]
case inr r'xy =>
  have : ∀ x y, r x y → r' x y := fun x y h => Or.inr h
  rw [← Quot.factor_mk_eq _ _ this]
  dsimp
  rw [appendFun_comp_id]
  rw [@comp_map _ _ _ q _ _ _ (appendFun id (Quot.mk r)), @comp_map _ _ _ q _ _ _ (appendFun id (Quot.mk r))]
  rw [h _ _ r'xy]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
r' : Cofix F α → Cofix F α → Prop := fun x y => x = y ∨ r x y
x✝ y✝ : Cofix F α
rxy : r x✝ y✝
x y : Cofix F α
r'xy : r x y
⊢ (TypeVec.id ::: Quot.mk r') <$$> dest x = (TypeVec.id ::: Quot.mk r') <$$> dest y
[PROOFSTEP]
case inr r'xy =>
  have : ∀ x y, r x y → r' x y := fun x y h => Or.inr h
  rw [← Quot.factor_mk_eq _ _ this]
  dsimp
  rw [appendFun_comp_id]
  rw [@comp_map _ _ _ q _ _ _ (appendFun id (Quot.mk r)), @comp_map _ _ _ q _ _ _ (appendFun id (Quot.mk r))]
  rw [h _ _ r'xy]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
r' : Cofix F α → Cofix F α → Prop := fun x y => x = y ∨ r x y
x✝ y✝ : Cofix F α
rxy : r x✝ y✝
x y : Cofix F α
r'xy : r x y
⊢ (TypeVec.id ::: Quot.mk r') <$$> dest x = (TypeVec.id ::: Quot.mk r') <$$> dest y
[PROOFSTEP]
have : ∀ x y, r x y → r' x y := fun x y h => Or.inr h
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
r' : Cofix F α → Cofix F α → Prop := fun x y => x = y ∨ r x y
x✝ y✝ : Cofix F α
rxy : r x✝ y✝
x y : Cofix F α
r'xy : r x y
this : ∀ (x y : Cofix F α), r x y → r' x y
⊢ (TypeVec.id ::: Quot.mk r') <$$> dest x = (TypeVec.id ::: Quot.mk r') <$$> dest y
[PROOFSTEP]
rw [← Quot.factor_mk_eq _ _ this]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
r' : Cofix F α → Cofix F α → Prop := fun x y => x = y ∨ r x y
x✝ y✝ : Cofix F α
rxy : r x✝ y✝
x y : Cofix F α
r'xy : r x y
this : ∀ (x y : Cofix F α), r x y → r' x y
⊢ (TypeVec.id ::: Quot.factor (fun x y => r x y) (fun x y => r' x y) this ∘ Quot.mk fun x y => r x y) <$$> dest x =
    (TypeVec.id ::: Quot.factor (fun x y => r x y) (fun x y => r' x y) this ∘ Quot.mk fun x y => r x y) <$$> dest y
[PROOFSTEP]
dsimp
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
r' : Cofix F α → Cofix F α → Prop := fun x y => x = y ∨ r x y
x✝ y✝ : Cofix F α
rxy : r x✝ y✝
x y : Cofix F α
r'xy : r x y
this : ∀ (x y : Cofix F α), r x y → r' x y
⊢ (TypeVec.id ::: Quot.factor (fun x y => r x y) (fun x y => x = y ∨ r x y) this ∘ Quot.mk fun x y => r x y) <$$>
      dest x =
    (TypeVec.id ::: Quot.factor (fun x y => r x y) (fun x y => x = y ∨ r x y) this ∘ Quot.mk fun x y => r x y) <$$>
      dest y
[PROOFSTEP]
rw [appendFun_comp_id]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
r' : Cofix F α → Cofix F α → Prop := fun x y => x = y ∨ r x y
x✝ y✝ : Cofix F α
rxy : r x✝ y✝
x y : Cofix F α
r'xy : r x y
this : ∀ (x y : Cofix F α), r x y → r' x y
⊢ ((TypeVec.id ::: Quot.factor (fun x y => r x y) (fun x y => x = y ∨ r x y) this) ⊚
        (TypeVec.id ::: Quot.mk fun x y => r x y)) <$$>
      dest x =
    ((TypeVec.id ::: Quot.factor (fun x y => r x y) (fun x y => x = y ∨ r x y) this) ⊚
        (TypeVec.id ::: Quot.mk fun x y => r x y)) <$$>
      dest y
[PROOFSTEP]
rw [@comp_map _ _ _ q _ _ _ (appendFun id (Quot.mk r)), @comp_map _ _ _ q _ _ _ (appendFun id (Quot.mk r))]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
r' : Cofix F α → Cofix F α → Prop := fun x y => x = y ∨ r x y
x✝ y✝ : Cofix F α
rxy : r x✝ y✝
x y : Cofix F α
r'xy : r x y
this : ∀ (x y : Cofix F α), r x y → r' x y
⊢ (TypeVec.id ::: Quot.factor (fun x y => r x y) (fun x y => x = y ∨ r x y) this) <$$>
      (TypeVec.id ::: Quot.mk r) <$$> dest x =
    (TypeVec.id ::: Quot.factor (fun x y => r x y) (fun x y => x = y ∨ r x y) this) <$$>
      (TypeVec.id ::: Quot.mk r) <$$> dest y
[PROOFSTEP]
rw [h _ _ r'xy]
[GOAL]
case a
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
r' : Cofix F α → Cofix F α → Prop := fun x y => x = y ∨ r x y
x y : Cofix F α
rxy : r x y
⊢ r' x y
[PROOFSTEP]
right
[GOAL]
case a.h
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> dest x = (TypeVec.id ::: Quot.mk r) <$$> dest y
r' : Cofix F α → Cofix F α → Prop := fun x y => x = y ∨ r x y
x y : Cofix F α
rxy : r x y
⊢ r x y
[PROOFSTEP]
exact rxy
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR (fun {i} => RelLast α r) (dest x) (dest y)
⊢ ∀ (x y : Cofix F α), r x y → x = y
[PROOFSTEP]
apply Cofix.bisim_rel
[GOAL]
case h
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR (fun {i} => RelLast α r) (dest x) (dest y)
⊢ ∀ (x y : Cofix F α),
    r x y →
      (TypeVec.id ::: Quot.mk fun x y => r x y) <$$> dest x = (TypeVec.id ::: Quot.mk fun x y => r x y) <$$> dest y
[PROOFSTEP]
intro x y rxy
[GOAL]
case h
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR (fun {i} => RelLast α r) (dest x) (dest y)
x y : Cofix F α
rxy : r x y
⊢ (TypeVec.id ::: Quot.mk fun x y => r x y) <$$> dest x = (TypeVec.id ::: Quot.mk fun x y => r x y) <$$> dest y
[PROOFSTEP]
rcases(liftR_iff (fun a b => RelLast α r a b) (dest x) (dest y)).mp (h x y rxy) with ⟨a, f₀, f₁, dxeq, dyeq, h'⟩
[GOAL]
case h.intro.intro.intro.intro.intro
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR (fun {i} => RelLast α r) (dest x) (dest y)
x y : Cofix F α
rxy : r x y
a : (P F).A
f₀ f₁ : B (P F) a ⟹ fun {i} => (α ::: Cofix F α) i
dxeq : dest x = MvQPF.abs { fst := a, snd := f₀ }
dyeq : dest y = MvQPF.abs { fst := a, snd := f₁ }
h' : ∀ (i : Fin2 (n + 1)) (j : B (P F) a i), RelLast α r (f₀ i j) (f₁ i j)
⊢ (TypeVec.id ::: Quot.mk fun x y => r x y) <$$> dest x = (TypeVec.id ::: Quot.mk fun x y => r x y) <$$> dest y
[PROOFSTEP]
rw [dxeq, dyeq, ← abs_map, ← abs_map, MvPFunctor.map_eq, MvPFunctor.map_eq]
[GOAL]
case h.intro.intro.intro.intro.intro
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR (fun {i} => RelLast α r) (dest x) (dest y)
x y : Cofix F α
rxy : r x y
a : (P F).A
f₀ f₁ : B (P F) a ⟹ fun {i} => (α ::: Cofix F α) i
dxeq : dest x = MvQPF.abs { fst := a, snd := f₀ }
dyeq : dest y = MvQPF.abs { fst := a, snd := f₁ }
h' : ∀ (i : Fin2 (n + 1)) (j : B (P F) a i), RelLast α r (f₀ i j) (f₁ i j)
⊢ MvQPF.abs { fst := a, snd := (TypeVec.id ::: Quot.mk fun x y => r x y) ⊚ f₀ } =
    MvQPF.abs { fst := a, snd := (TypeVec.id ::: Quot.mk fun x y => r x y) ⊚ f₁ }
[PROOFSTEP]
rw [← split_dropFun_lastFun f₀, ← split_dropFun_lastFun f₁]
[GOAL]
case h.intro.intro.intro.intro.intro
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR (fun {i} => RelLast α r) (dest x) (dest y)
x y : Cofix F α
rxy : r x y
a : (P F).A
f₀ f₁ : B (P F) a ⟹ fun {i} => (α ::: Cofix F α) i
dxeq : dest x = MvQPF.abs { fst := a, snd := f₀ }
dyeq : dest y = MvQPF.abs { fst := a, snd := f₁ }
h' : ∀ (i : Fin2 (n + 1)) (j : B (P F) a i), RelLast α r (f₀ i j) (f₁ i j)
⊢ MvQPF.abs { fst := a, snd := (TypeVec.id ::: Quot.mk fun x y => r x y) ⊚ splitFun (dropFun f₀) (lastFun f₀) } =
    MvQPF.abs { fst := a, snd := (TypeVec.id ::: Quot.mk fun x y => r x y) ⊚ splitFun (dropFun f₁) (lastFun f₁) }
[PROOFSTEP]
rw [appendFun_comp_splitFun, appendFun_comp_splitFun]
[GOAL]
case h.intro.intro.intro.intro.intro
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR (fun {i} => RelLast α r) (dest x) (dest y)
x y : Cofix F α
rxy : r x y
a : (P F).A
f₀ f₁ : B (P F) a ⟹ fun {i} => (α ::: Cofix F α) i
dxeq : dest x = MvQPF.abs { fst := a, snd := f₀ }
dyeq : dest y = MvQPF.abs { fst := a, snd := f₁ }
h' : ∀ (i : Fin2 (n + 1)) (j : B (P F) a i), RelLast α r (f₀ i j) (f₁ i j)
⊢ MvQPF.abs { fst := a, snd := splitFun (TypeVec.id ⊚ dropFun f₀) ((Quot.mk fun x y => r x y) ∘ lastFun f₀) } =
    MvQPF.abs { fst := a, snd := splitFun (TypeVec.id ⊚ dropFun f₁) ((Quot.mk fun x y => r x y) ∘ lastFun f₁) }
[PROOFSTEP]
rw [id_comp, id_comp]
[GOAL]
case h.intro.intro.intro.intro.intro
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR (fun {i} => RelLast α r) (dest x) (dest y)
x y : Cofix F α
rxy : r x y
a : (P F).A
f₀ f₁ : B (P F) a ⟹ fun {i} => (α ::: Cofix F α) i
dxeq : dest x = MvQPF.abs { fst := a, snd := f₀ }
dyeq : dest y = MvQPF.abs { fst := a, snd := f₁ }
h' : ∀ (i : Fin2 (n + 1)) (j : B (P F) a i), RelLast α r (f₀ i j) (f₁ i j)
⊢ MvQPF.abs { fst := a, snd := splitFun (dropFun f₀) ((Quot.mk fun x y => r x y) ∘ lastFun f₀) } =
    MvQPF.abs { fst := a, snd := splitFun (dropFun f₁) ((Quot.mk fun x y => r x y) ∘ lastFun f₁) }
[PROOFSTEP]
congr 2 with (i j)
[GOAL]
case h.intro.intro.intro.intro.intro.e_a.e_snd.a.h
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR (fun {i} => RelLast α r) (dest x) (dest y)
x y : Cofix F α
rxy : r x y
a : (P F).A
f₀ f₁ : B (P F) a ⟹ fun {i} => (α ::: Cofix F α) i
dxeq : dest x = MvQPF.abs { fst := a, snd := f₀ }
dyeq : dest y = MvQPF.abs { fst := a, snd := f₁ }
h' : ∀ (i : Fin2 (n + 1)) (j : B (P F) a i), RelLast α r (f₀ i j) (f₁ i j)
i : Fin2 (n + 1)
j : B (P F) a i
⊢ splitFun (dropFun f₀) ((Quot.mk fun x y => r x y) ∘ lastFun f₀) i j =
    splitFun (dropFun f₁) ((Quot.mk fun x y => r x y) ∘ lastFun f₁) i j
[PROOFSTEP]
cases' i with _ i
[GOAL]
case h.intro.intro.intro.intro.intro.e_a.e_snd.a.h.fz
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR (fun {i} => RelLast α r) (dest x) (dest y)
x y : Cofix F α
rxy : r x y
a : (P F).A
f₀ f₁ : B (P F) a ⟹ fun {i} => (α ::: Cofix F α) i
dxeq : dest x = MvQPF.abs { fst := a, snd := f₀ }
dyeq : dest y = MvQPF.abs { fst := a, snd := f₁ }
h' : ∀ (i : Fin2 (n + 1)) (j : B (P F) a i), RelLast α r (f₀ i j) (f₁ i j)
j : B (P F) a Fin2.fz
⊢ splitFun (dropFun f₀) ((Quot.mk fun x y => r x y) ∘ lastFun f₀) Fin2.fz j =
    splitFun (dropFun f₁) ((Quot.mk fun x y => r x y) ∘ lastFun f₁) Fin2.fz j
[PROOFSTEP]
dsimp
[GOAL]
case h.intro.intro.intro.intro.intro.e_a.e_snd.a.h.fs
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR (fun {i} => RelLast α r) (dest x) (dest y)
x y : Cofix F α
rxy : r x y
a : (P F).A
f₀ f₁ : B (P F) a ⟹ fun {i} => (α ::: Cofix F α) i
dxeq : dest x = MvQPF.abs { fst := a, snd := f₀ }
dyeq : dest y = MvQPF.abs { fst := a, snd := f₁ }
h' : ∀ (i : Fin2 (n + 1)) (j : B (P F) a i), RelLast α r (f₀ i j) (f₁ i j)
a✝ : Fin2 (Nat.add n 0)
j : B (P F) a (Fin2.fs a✝)
⊢ splitFun (dropFun f₀) ((Quot.mk fun x y => r x y) ∘ lastFun f₀) (Fin2.fs a✝) j =
    splitFun (dropFun f₁) ((Quot.mk fun x y => r x y) ∘ lastFun f₁) (Fin2.fs a✝) j
[PROOFSTEP]
dsimp
[GOAL]
case h.intro.intro.intro.intro.intro.e_a.e_snd.a.h.fz
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR (fun {i} => RelLast α r) (dest x) (dest y)
x y : Cofix F α
rxy : r x y
a : (P F).A
f₀ f₁ : B (P F) a ⟹ fun {i} => (α ::: Cofix F α) i
dxeq : dest x = MvQPF.abs { fst := a, snd := f₀ }
dyeq : dest y = MvQPF.abs { fst := a, snd := f₁ }
h' : ∀ (i : Fin2 (n + 1)) (j : B (P F) a i), RelLast α r (f₀ i j) (f₁ i j)
j : B (P F) a Fin2.fz
⊢ splitFun (dropFun f₀) ((Quot.mk fun x y => r x y) ∘ lastFun f₀) Fin2.fz j =
    splitFun (dropFun f₁) ((Quot.mk fun x y => r x y) ∘ lastFun f₁) Fin2.fz j
[PROOFSTEP]
apply Quot.sound
[GOAL]
case h.intro.intro.intro.intro.intro.e_a.e_snd.a.h.fz.a
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR (fun {i} => RelLast α r) (dest x) (dest y)
x y : Cofix F α
rxy : r x y
a : (P F).A
f₀ f₁ : B (P F) a ⟹ fun {i} => (α ::: Cofix F α) i
dxeq : dest x = MvQPF.abs { fst := a, snd := f₀ }
dyeq : dest y = MvQPF.abs { fst := a, snd := f₁ }
h' : ∀ (i : Fin2 (n + 1)) (j : B (P F) a i), RelLast α r (f₀ i j) (f₁ i j)
j : B (P F) a Fin2.fz
⊢ r (lastFun f₀ j) (lastFun f₁ j)
[PROOFSTEP]
apply h' _ j
[GOAL]
case h.intro.intro.intro.intro.intro.e_a.e_snd.a.h.fs
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR (fun {i} => RelLast α r) (dest x) (dest y)
x y : Cofix F α
rxy : r x y
a : (P F).A
f₀ f₁ : B (P F) a ⟹ fun {i} => (α ::: Cofix F α) i
dxeq : dest x = MvQPF.abs { fst := a, snd := f₀ }
dyeq : dest y = MvQPF.abs { fst := a, snd := f₁ }
h' : ∀ (i : Fin2 (n + 1)) (j : B (P F) a i), RelLast α r (f₀ i j) (f₁ i j)
a✝ : Fin2 (Nat.add n 0)
j : B (P F) a (Fin2.fs a✝)
⊢ splitFun (dropFun f₀) ((Quot.mk fun x y => r x y) ∘ lastFun f₀) (Fin2.fs a✝) j =
    splitFun (dropFun f₁) ((Quot.mk fun x y => r x y) ∘ lastFun f₁) (Fin2.fs a✝) j
[PROOFSTEP]
change f₀ _ j = f₁ _ j
[GOAL]
case h.intro.intro.intro.intro.intro.e_a.e_snd.a.h.fs
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR (fun {i} => RelLast α r) (dest x) (dest y)
x y : Cofix F α
rxy : r x y
a : (P F).A
f₀ f₁ : B (P F) a ⟹ fun {i} => (α ::: Cofix F α) i
dxeq : dest x = MvQPF.abs { fst := a, snd := f₀ }
dyeq : dest y = MvQPF.abs { fst := a, snd := f₁ }
h' : ∀ (i : Fin2 (n + 1)) (j : B (P F) a i), RelLast α r (f₀ i j) (f₁ i j)
a✝ : Fin2 (Nat.add n 0)
j : B (P F) a (Fin2.fs a✝)
⊢ f₀ (Fin2.fs a✝) j = f₁ (Fin2.fs a✝) j
[PROOFSTEP]
apply h' _ j
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR' (RelLast' α r) (dest x) (dest y)
⊢ ∀ (x y : Cofix F α), r x y → LiftR (fun {i} => RelLast α r) (dest x) (dest y)
[PROOFSTEP]
intros
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR' (RelLast' α r) (dest x) (dest y)
x✝ y✝ : Cofix F α
a✝ : r x✝ y✝
⊢ LiftR (fun {i} => RelLast α r) (dest x✝) (dest y✝)
[PROOFSTEP]
rw [← LiftR_RelLast_iff]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR' (RelLast' α r) (dest x) (dest y)
x✝ y✝ : Cofix F α
a✝ : r x✝ y✝
⊢ LiftR' (RelLast' α r) (dest x✝) (dest y✝)
[PROOFSTEP]
apply h
[GOAL]
case a
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR' (RelLast' α r) (dest x) (dest y)
x✝ y✝ : Cofix F α
a✝ : r x✝ y✝
⊢ r x✝ y✝
[PROOFSTEP]
assumption
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u_1
Q : β → Prop
u v : β → Cofix F α
h :
  ∀ (x : β),
    Q x →
      ∃ a f' f₀ f₁,
        dest (u x) = MvQPF.abs { fst := a, snd := appendContents (P F) f' f₀ } ∧
          dest (v x) = MvQPF.abs { fst := a, snd := appendContents (P F) f' f₁ } ∧
            ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), ∃ x', Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'
x✝¹ : β
Qx : Q x✝¹
R : Cofix F α → Cofix F α → Prop := fun w z => ∃ x', Q x' ∧ w = u x' ∧ z = v x'
x y : Cofix F α
x✝ : R x y
x' : β
Qx' : Q x'
xeq : x = u x'
yeq : y = v x'
⊢ LiftR (fun {i} => RelLast α R) (dest x) (dest y)
[PROOFSTEP]
rcases h x' Qx' with ⟨a, f', f₀, f₁, ux'eq, vx'eq, h'⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u_1
Q : β → Prop
u v : β → Cofix F α
h :
  ∀ (x : β),
    Q x →
      ∃ a f' f₀ f₁,
        dest (u x) = MvQPF.abs { fst := a, snd := appendContents (P F) f' f₀ } ∧
          dest (v x) = MvQPF.abs { fst := a, snd := appendContents (P F) f' f₁ } ∧
            ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), ∃ x', Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'
x✝¹ : β
Qx : Q x✝¹
R : Cofix F α → Cofix F α → Prop := fun w z => ∃ x', Q x' ∧ w = u x' ∧ z = v x'
x y : Cofix F α
x✝ : R x y
x' : β
Qx' : Q x'
xeq : x = u x'
yeq : y = v x'
a : (P F).A
f' : B (MvPFunctor.drop (P F)) a ⟹ α
f₀ f₁ : PFunctor.B (MvPFunctor.last (P F)) a → Cofix F α
ux'eq : dest (u x') = MvQPF.abs { fst := a, snd := appendContents (P F) f' f₀ }
vx'eq : dest (v x') = MvQPF.abs { fst := a, snd := appendContents (P F) f' f₁ }
h' : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), ∃ x', Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'
⊢ LiftR (fun {i} => RelLast α R) (dest x) (dest y)
[PROOFSTEP]
rw [liftR_iff]
[GOAL]
case intro.intro.intro.intro.intro.intro
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u_1
Q : β → Prop
u v : β → Cofix F α
h :
  ∀ (x : β),
    Q x →
      ∃ a f' f₀ f₁,
        dest (u x) = MvQPF.abs { fst := a, snd := appendContents (P F) f' f₀ } ∧
          dest (v x) = MvQPF.abs { fst := a, snd := appendContents (P F) f' f₁ } ∧
            ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), ∃ x', Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'
x✝¹ : β
Qx : Q x✝¹
R : Cofix F α → Cofix F α → Prop := fun w z => ∃ x', Q x' ∧ w = u x' ∧ z = v x'
x y : Cofix F α
x✝ : R x y
x' : β
Qx' : Q x'
xeq : x = u x'
yeq : y = v x'
a : (P F).A
f' : B (MvPFunctor.drop (P F)) a ⟹ α
f₀ f₁ : PFunctor.B (MvPFunctor.last (P F)) a → Cofix F α
ux'eq : dest (u x') = MvQPF.abs { fst := a, snd := appendContents (P F) f' f₀ }
vx'eq : dest (v x') = MvQPF.abs { fst := a, snd := appendContents (P F) f' f₁ }
h' : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), ∃ x', Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'
⊢ ∃ a f₀ f₁,
    dest x = MvQPF.abs { fst := a, snd := f₀ } ∧
      dest y = MvQPF.abs { fst := a, snd := f₁ } ∧ ∀ (i : Fin2 (n + 1)) (j : B (P F) a i), RelLast α R (f₀ i j) (f₁ i j)
[PROOFSTEP]
refine' ⟨a, q.P.appendContents f' f₀, q.P.appendContents f' f₁, xeq.symm ▸ ux'eq, yeq.symm ▸ vx'eq, _⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u_1
Q : β → Prop
u v : β → Cofix F α
h :
  ∀ (x : β),
    Q x →
      ∃ a f' f₀ f₁,
        dest (u x) = MvQPF.abs { fst := a, snd := appendContents (P F) f' f₀ } ∧
          dest (v x) = MvQPF.abs { fst := a, snd := appendContents (P F) f' f₁ } ∧
            ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), ∃ x', Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'
x✝¹ : β
Qx : Q x✝¹
R : Cofix F α → Cofix F α → Prop := fun w z => ∃ x', Q x' ∧ w = u x' ∧ z = v x'
x y : Cofix F α
x✝ : R x y
x' : β
Qx' : Q x'
xeq : x = u x'
yeq : y = v x'
a : (P F).A
f' : B (MvPFunctor.drop (P F)) a ⟹ α
f₀ f₁ : PFunctor.B (MvPFunctor.last (P F)) a → Cofix F α
ux'eq : dest (u x') = MvQPF.abs { fst := a, snd := appendContents (P F) f' f₀ }
vx'eq : dest (v x') = MvQPF.abs { fst := a, snd := appendContents (P F) f' f₁ }
h' : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), ∃ x', Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'
⊢ ∀ (i : Fin2 (n + 1)) (j : B (P F) a i), RelLast α R (appendContents (P F) f' f₀ i j) (appendContents (P F) f' f₁ i j)
[PROOFSTEP]
intro i
[GOAL]
case intro.intro.intro.intro.intro.intro
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u_1
Q : β → Prop
u v : β → Cofix F α
h :
  ∀ (x : β),
    Q x →
      ∃ a f' f₀ f₁,
        dest (u x) = MvQPF.abs { fst := a, snd := appendContents (P F) f' f₀ } ∧
          dest (v x) = MvQPF.abs { fst := a, snd := appendContents (P F) f' f₁ } ∧
            ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), ∃ x', Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'
x✝¹ : β
Qx : Q x✝¹
R : Cofix F α → Cofix F α → Prop := fun w z => ∃ x', Q x' ∧ w = u x' ∧ z = v x'
x y : Cofix F α
x✝ : R x y
x' : β
Qx' : Q x'
xeq : x = u x'
yeq : y = v x'
a : (P F).A
f' : B (MvPFunctor.drop (P F)) a ⟹ α
f₀ f₁ : PFunctor.B (MvPFunctor.last (P F)) a → Cofix F α
ux'eq : dest (u x') = MvQPF.abs { fst := a, snd := appendContents (P F) f' f₀ }
vx'eq : dest (v x') = MvQPF.abs { fst := a, snd := appendContents (P F) f' f₁ }
h' : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), ∃ x', Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'
i : Fin2 (n + 1)
⊢ ∀ (j : B (P F) a i), RelLast α R (appendContents (P F) f' f₀ i j) (appendContents (P F) f' f₁ i j)
[PROOFSTEP]
cases i
[GOAL]
case intro.intro.intro.intro.intro.intro.fz
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u_1
Q : β → Prop
u v : β → Cofix F α
h :
  ∀ (x : β),
    Q x →
      ∃ a f' f₀ f₁,
        dest (u x) = MvQPF.abs { fst := a, snd := appendContents (P F) f' f₀ } ∧
          dest (v x) = MvQPF.abs { fst := a, snd := appendContents (P F) f' f₁ } ∧
            ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), ∃ x', Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'
x✝¹ : β
Qx : Q x✝¹
R : Cofix F α → Cofix F α → Prop := fun w z => ∃ x', Q x' ∧ w = u x' ∧ z = v x'
x y : Cofix F α
x✝ : R x y
x' : β
Qx' : Q x'
xeq : x = u x'
yeq : y = v x'
a : (P F).A
f' : B (MvPFunctor.drop (P F)) a ⟹ α
f₀ f₁ : PFunctor.B (MvPFunctor.last (P F)) a → Cofix F α
ux'eq : dest (u x') = MvQPF.abs { fst := a, snd := appendContents (P F) f' f₀ }
vx'eq : dest (v x') = MvQPF.abs { fst := a, snd := appendContents (P F) f' f₁ }
h' : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), ∃ x', Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'
⊢ ∀ (j : B (P F) a Fin2.fz), RelLast α R (appendContents (P F) f' f₀ Fin2.fz j) (appendContents (P F) f' f₁ Fin2.fz j)
[PROOFSTEP]
apply h'
[GOAL]
case intro.intro.intro.intro.intro.intro.fs
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u_1
Q : β → Prop
u v : β → Cofix F α
h :
  ∀ (x : β),
    Q x →
      ∃ a f' f₀ f₁,
        dest (u x) = MvQPF.abs { fst := a, snd := appendContents (P F) f' f₀ } ∧
          dest (v x) = MvQPF.abs { fst := a, snd := appendContents (P F) f' f₁ } ∧
            ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), ∃ x', Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'
x✝¹ : β
Qx : Q x✝¹
R : Cofix F α → Cofix F α → Prop := fun w z => ∃ x', Q x' ∧ w = u x' ∧ z = v x'
x y : Cofix F α
x✝ : R x y
x' : β
Qx' : Q x'
xeq : x = u x'
yeq : y = v x'
a : (P F).A
f' : B (MvPFunctor.drop (P F)) a ⟹ α
f₀ f₁ : PFunctor.B (MvPFunctor.last (P F)) a → Cofix F α
ux'eq : dest (u x') = MvQPF.abs { fst := a, snd := appendContents (P F) f' f₀ }
vx'eq : dest (v x') = MvQPF.abs { fst := a, snd := appendContents (P F) f' f₁ }
h' : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), ∃ x', Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'
a✝ : Fin2 (Nat.add n 0)
⊢ ∀ (j : B (P F) a (Fin2.fs a✝)),
    RelLast α R (appendContents (P F) f' f₀ (Fin2.fs a✝) j) (appendContents (P F) f' f₁ (Fin2.fs a✝) j)
[PROOFSTEP]
intro j
[GOAL]
case intro.intro.intro.intro.intro.intro.fs
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u_1
Q : β → Prop
u v : β → Cofix F α
h :
  ∀ (x : β),
    Q x →
      ∃ a f' f₀ f₁,
        dest (u x) = MvQPF.abs { fst := a, snd := appendContents (P F) f' f₀ } ∧
          dest (v x) = MvQPF.abs { fst := a, snd := appendContents (P F) f' f₁ } ∧
            ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), ∃ x', Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'
x✝¹ : β
Qx : Q x✝¹
R : Cofix F α → Cofix F α → Prop := fun w z => ∃ x', Q x' ∧ w = u x' ∧ z = v x'
x y : Cofix F α
x✝ : R x y
x' : β
Qx' : Q x'
xeq : x = u x'
yeq : y = v x'
a : (P F).A
f' : B (MvPFunctor.drop (P F)) a ⟹ α
f₀ f₁ : PFunctor.B (MvPFunctor.last (P F)) a → Cofix F α
ux'eq : dest (u x') = MvQPF.abs { fst := a, snd := appendContents (P F) f' f₀ }
vx'eq : dest (v x') = MvQPF.abs { fst := a, snd := appendContents (P F) f' f₁ }
h' : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), ∃ x', Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'
a✝ : Fin2 (Nat.add n 0)
j : B (P F) a (Fin2.fs a✝)
⊢ RelLast α R (appendContents (P F) f' f₀ (Fin2.fs a✝) j) (appendContents (P F) f' f₁ (Fin2.fs a✝) j)
[PROOFSTEP]
apply Eq.refl
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
x : Cofix F α
⊢ mk (dest x) = x
[PROOFSTEP]
apply Cofix.bisim_rel (fun x y : Cofix F α => x = Cofix.mk (Cofix.dest y)) _ _ _ rfl
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
x : Cofix F α
⊢ ∀ (x y : Cofix F α),
    (fun x y => x = mk (dest y)) x y →
      (TypeVec.id ::: Quot.mk fun x y => x = mk (dest y)) <$$> dest x =
        (TypeVec.id ::: Quot.mk fun x y => x = mk (dest y)) <$$> dest y
[PROOFSTEP]
dsimp
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
x : Cofix F α
⊢ ∀ (x y : Cofix F α),
    x = mk (dest y) →
      (TypeVec.id ::: Quot.mk fun x y => x = mk (dest y)) <$$> dest x =
        (TypeVec.id ::: Quot.mk fun x y => x = mk (dest y)) <$$> dest y
[PROOFSTEP]
intro x y h
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
x✝ x y : Cofix F α
h : x = mk (dest y)
⊢ (TypeVec.id ::: Quot.mk fun x y => x = mk (dest y)) <$$> dest x =
    (TypeVec.id ::: Quot.mk fun x y => x = mk (dest y)) <$$> dest y
[PROOFSTEP]
rw [h]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
x✝ x y : Cofix F α
h : x = mk (dest y)
⊢ (TypeVec.id ::: Quot.mk fun x y => x = mk (dest y)) <$$> dest (mk (dest y)) =
    (TypeVec.id ::: Quot.mk fun x y => x = mk (dest y)) <$$> dest y
[PROOFSTEP]
conv =>
  lhs
  congr
  rfl
  rw [Cofix.mk]
  rw [Cofix.dest_corec]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
x✝ x y : Cofix F α
h : x = mk (dest y)
| (TypeVec.id ::: Quot.mk fun x y => x = mk (dest y)) <$$> dest (mk (dest y)) =
    (TypeVec.id ::: Quot.mk fun x y => x = mk (dest y)) <$$> dest y
[PROOFSTEP]
  lhs
  congr
  rfl
  rw [Cofix.mk]
  rw [Cofix.dest_corec]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
x✝ x y : Cofix F α
h : x = mk (dest y)
| (TypeVec.id ::: Quot.mk fun x y => x = mk (dest y)) <$$> dest (mk (dest y)) =
    (TypeVec.id ::: Quot.mk fun x y => x = mk (dest y)) <$$> dest y
[PROOFSTEP]
  lhs
  congr
  rfl
  rw [Cofix.mk]
  rw [Cofix.dest_corec]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
x✝ x y : Cofix F α
h : x = mk (dest y)
| (TypeVec.id ::: Quot.mk fun x y => x = mk (dest y)) <$$> dest (mk (dest y)) =
    (TypeVec.id ::: Quot.mk fun x y => x = mk (dest y)) <$$> dest y
[PROOFSTEP]
lhs
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
x✝ x y : Cofix F α
h : x = mk (dest y)
| (TypeVec.id ::: Quot.mk fun x y => x = mk (dest y)) <$$> dest (mk (dest y))
[PROOFSTEP]
congr
[GOAL]
case a
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
x✝ x y : Cofix F α
h : x = mk (dest y)
| TypeVec.id ::: Quot.mk fun x y => x = mk (dest y)
case a
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
x✝ x y : Cofix F α
h : x = mk (dest y)
| dest (mk (dest y))
[PROOFSTEP]
rfl
[GOAL]
case a
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
x✝ x y : Cofix F α
h : x = mk (dest y)
| dest (mk (dest y))
[PROOFSTEP]
rw [Cofix.mk]
[GOAL]
case a
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
x✝ x y : Cofix F α
h : x = mk (dest y)
| dest (corec (fun x => (TypeVec.id ::: fun i => dest i) <$$> x) (dest y))
[PROOFSTEP]
rw [Cofix.dest_corec]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
x✝ x y : Cofix F α
h : x = mk (dest y)
⊢ (TypeVec.id ::: Quot.mk fun x y => x = mk (dest y)) <$$>
      (TypeVec.id ::: corec fun x => (TypeVec.id ::: fun i => dest i) <$$> x) <$$>
        (TypeVec.id ::: fun i => dest i) <$$> dest y =
    (TypeVec.id ::: Quot.mk fun x y => x = mk (dest y)) <$$> dest y
[PROOFSTEP]
rw [← comp_map, ← appendFun_comp, id_comp]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
x✝ x y : Cofix F α
h : x = mk (dest y)
⊢ (TypeVec.id ::: (Quot.mk fun x y => x = mk (dest y)) ∘ corec fun x => (TypeVec.id ::: fun i => dest i) <$$> x) <$$>
      (TypeVec.id ::: fun i => dest i) <$$> dest y =
    (TypeVec.id ::: Quot.mk fun x y => x = mk (dest y)) <$$> dest y
[PROOFSTEP]
rw [← comp_map, ← appendFun_comp, id_comp, ← Cofix.mk]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
x✝ x y : Cofix F α
h : x = mk (dest y)
⊢ (TypeVec.id ::: ((Quot.mk fun x y => x = mk (dest y)) ∘ mk) ∘ fun i => dest i) <$$> dest y =
    (TypeVec.id ::: Quot.mk fun x y => x = mk (dest y)) <$$> dest y
[PROOFSTEP]
congr
[GOAL]
case e_a
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
x✝ x y : Cofix F α
h : x = mk (dest y)
⊢ (TypeVec.id ::: ((Quot.mk fun x y => x = mk (dest y)) ∘ mk) ∘ fun i => dest i) =
    (TypeVec.id ::: Quot.mk fun x y => x = mk (dest y))
[PROOFSTEP]
apply congrArg
[GOAL]
case e_a.h
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
x✝ x y : Cofix F α
h : x = mk (dest y)
⊢ (((Quot.mk fun x y => x = mk (dest y)) ∘ mk) ∘ fun i => dest i) = Quot.mk fun x y => x = mk (dest y)
[PROOFSTEP]
funext x
[GOAL]
case e_a.h.h
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
x✝¹ x✝ y : Cofix F α
h : x✝ = mk (dest y)
x : Cofix F α
⊢ (((Quot.mk fun x y => x = mk (dest y)) ∘ mk) ∘ fun i => dest i) x = Quot.mk (fun x y => x = mk (dest y)) x
[PROOFSTEP]
apply Quot.sound
[GOAL]
case e_a.h.h.a
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
x✝¹ x✝ y : Cofix F α
h : x✝ = mk (dest y)
x : Cofix F α
⊢ mk ((fun i => dest i) x) = mk (dest x)
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F (α ::: Cofix F α)
⊢ dest (mk x) = x
[PROOFSTEP]
have : Cofix.mk ∘ Cofix.dest = @_root_.id (Cofix F α) := funext Cofix.mk_dest
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F (α ::: Cofix F α)
this : mk ∘ dest = _root_.id
⊢ dest (mk x) = x
[PROOFSTEP]
rw [Cofix.mk, Cofix.dest_corec, ← comp_map, ← Cofix.mk, ← appendFun_comp, this, id_comp, appendFun_id_id,
  MvFunctor.id_map]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
x y : Cofix F α
h : dest x = dest y
⊢ x = y
[PROOFSTEP]
rw [← Cofix.mk_dest x, h, Cofix.mk_dest]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
x y : F (α ::: Cofix F α)
h : mk x = mk y
⊢ x = y
[PROOFSTEP]
rw [← Cofix.dest_mk x, h, Cofix.dest_mk]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α β : TypeVec n
F' : TypeVec n → Type u
inst✝¹ : MvFunctor F'
inst✝ : LawfulMvFunctor F'
R : β ⊗ β ⟹ repeat n Prop
x : F' α
f g : α ⟹ β
h : α ⟹ Subtype_ R
hh : subtypeVal R ⊚ h = (f ⊗' g) ⊚ prod.diag
⊢ LiftR' R (f <$$> x) (g <$$> x)
[PROOFSTEP]
rw [LiftR_def]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α β : TypeVec n
F' : TypeVec n → Type u
inst✝¹ : MvFunctor F'
inst✝ : LawfulMvFunctor F'
R : β ⊗ β ⟹ repeat n Prop
x : F' α
f g : α ⟹ β
h : α ⟹ Subtype_ R
hh : subtypeVal R ⊚ h = (f ⊗' g) ⊚ prod.diag
⊢ ∃ u, (prod.fst ⊚ subtypeVal R) <$$> u = f <$$> x ∧ (prod.snd ⊚ subtypeVal R) <$$> u = g <$$> x
[PROOFSTEP]
exists h <$$> x
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α β : TypeVec n
F' : TypeVec n → Type u
inst✝¹ : MvFunctor F'
inst✝ : LawfulMvFunctor F'
R : β ⊗ β ⟹ repeat n Prop
x : F' α
f g : α ⟹ β
h : α ⟹ Subtype_ R
hh : subtypeVal R ⊚ h = (f ⊗' g) ⊚ prod.diag
⊢ (prod.fst ⊚ subtypeVal R) <$$> h <$$> x = f <$$> x ∧ (prod.snd ⊚ subtypeVal R) <$$> h <$$> x = g <$$> x
[PROOFSTEP]
rw [MvFunctor.map_map, comp_assoc, hh, ← comp_assoc, fst_prod_mk, comp_assoc, fst_diag]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α β : TypeVec n
F' : TypeVec n → Type u
inst✝¹ : MvFunctor F'
inst✝ : LawfulMvFunctor F'
R : β ⊗ β ⟹ repeat n Prop
x : F' α
f g : α ⟹ β
h : α ⟹ Subtype_ R
hh : subtypeVal R ⊚ h = (f ⊗' g) ⊚ prod.diag
⊢ (f ⊚ TypeVec.id) <$$> x = f <$$> x ∧ (prod.snd ⊚ subtypeVal R) <$$> h <$$> x = g <$$> x
[PROOFSTEP]
rw [MvFunctor.map_map, comp_assoc, hh, ← comp_assoc, snd_prod_mk, comp_assoc, snd_diag]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α β : TypeVec n
F' : TypeVec n → Type u
inst✝¹ : MvFunctor F'
inst✝ : LawfulMvFunctor F'
R : β ⊗ β ⟹ repeat n Prop
x : F' α
f g : α ⟹ β
h : α ⟹ Subtype_ R
hh : subtypeVal R ⊚ h = (f ⊗' g) ⊚ prod.diag
⊢ (f ⊚ TypeVec.id) <$$> x = f <$$> x ∧ (g ⊚ TypeVec.id) <$$> x = g <$$> x
[PROOFSTEP]
dsimp [LiftR']
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α β : TypeVec n
F' : TypeVec n → Type u
inst✝¹ : MvFunctor F'
inst✝ : LawfulMvFunctor F'
R : β ⊗ β ⟹ repeat n Prop
x : F' α
f g : α ⟹ β
h : α ⟹ Subtype_ R
hh : subtypeVal R ⊚ h = (f ⊗' g) ⊚ prod.diag
⊢ f <$$> x = f <$$> x ∧ g <$$> x = g <$$> x
[PROOFSTEP]
constructor
[GOAL]
case left
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α β : TypeVec n
F' : TypeVec n → Type u
inst✝¹ : MvFunctor F'
inst✝ : LawfulMvFunctor F'
R : β ⊗ β ⟹ repeat n Prop
x : F' α
f g : α ⟹ β
h : α ⟹ Subtype_ R
hh : subtypeVal R ⊚ h = (f ⊗' g) ⊚ prod.diag
⊢ f <$$> x = f <$$> x
[PROOFSTEP]
rfl
[GOAL]
case right
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α β : TypeVec n
F' : TypeVec n → Type u
inst✝¹ : MvFunctor F'
inst✝ : LawfulMvFunctor F'
R : β ⊗ β ⟹ repeat n Prop
x : F' α
f g : α ⟹ β
h : α ⟹ Subtype_ R
hh : subtypeVal R ⊚ h = (f ⊗' g) ⊚ prod.diag
⊢ g <$$> x = g <$$> x
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
lawful : LawfulMvFunctor F
α : TypeVec n
ι ι' : Type u
R : ι' → ι' → Prop
x : F (α ::: ι)
f g : ι → ι'
hh : ∀ (x : ι), R (f x) (g x)
h : ι → { x // uncurry R x } := fun x => { val := (f x, g x), property := (_ : R (f x) (g x)) }
b : α ::: ι ⟹ Subtype_ (repeatEq α) ::: { x // uncurry R x } := diagSub ::: h
c : Subtype_ (repeatEq α) ::: { x // uncurry R x } ⟹
  (fun i => { x // ofRepeat (RelLast' α R (Fin2.fs i) x) }) ::: Subtype (uncurry R) :=
  ofSubtype (repeatEq α) ::: _root_.id
⊢ subtypeVal (RelLast' α R) ⊚ toSubtype (RelLast' α R) ⊚ fromAppend1DropLast ⊚ c ⊚ b =
    ((TypeVec.id ::: f) ⊗' (TypeVec.id ::: g)) ⊚ prod.diag
[PROOFSTEP]
dsimp
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
lawful : LawfulMvFunctor F
α : TypeVec n
ι ι' : Type u
R : ι' → ι' → Prop
x : F (α ::: ι)
f g : ι → ι'
hh : ∀ (x : ι), R (f x) (g x)
h : ι → { x // uncurry R x } := fun x => { val := (f x, g x), property := (_ : R (f x) (g x)) }
b : α ::: ι ⟹ Subtype_ (repeatEq α) ::: { x // uncurry R x } := diagSub ::: h
c : Subtype_ (repeatEq α) ::: { x // uncurry R x } ⟹
  (fun i => { x // ofRepeat (RelLast' α R (Fin2.fs i) x) }) ::: Subtype (uncurry R) :=
  ofSubtype (repeatEq α) ::: _root_.id
⊢ subtypeVal (RelLast' α R) ⊚
      toSubtype (RelLast' α R) ⊚
        fromAppend1DropLast ⊚
          (ofSubtype (repeatEq α) ::: _root_.id) ⊚
            (diagSub ::: fun x => { val := (f x, g x), property := (_ : R (f x) (g x)) }) =
    ((TypeVec.id ::: f) ⊗' (TypeVec.id ::: g)) ⊚ prod.diag
[PROOFSTEP]
apply eq_of_drop_last_eq
[GOAL]
case h₀
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
lawful : LawfulMvFunctor F
α : TypeVec n
ι ι' : Type u
R : ι' → ι' → Prop
x : F (α ::: ι)
f g : ι → ι'
hh : ∀ (x : ι), R (f x) (g x)
h : ι → { x // uncurry R x } := fun x => { val := (f x, g x), property := (_ : R (f x) (g x)) }
b : α ::: ι ⟹ Subtype_ (repeatEq α) ::: { x // uncurry R x } := diagSub ::: h
c : Subtype_ (repeatEq α) ::: { x // uncurry R x } ⟹
  (fun i => { x // ofRepeat (RelLast' α R (Fin2.fs i) x) }) ::: Subtype (uncurry R) :=
  ofSubtype (repeatEq α) ::: _root_.id
⊢ dropFun
      (subtypeVal (RelLast' α R) ⊚
        toSubtype (RelLast' α R) ⊚
          fromAppend1DropLast ⊚
            (ofSubtype (repeatEq α) ::: _root_.id) ⊚
              (diagSub ::: fun x => { val := (f x, g x), property := (_ : R (f x) (g x)) })) =
    dropFun (((TypeVec.id ::: f) ⊗' (TypeVec.id ::: g)) ⊚ prod.diag)
[PROOFSTEP]
dsimp
[GOAL]
case h₀
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
lawful : LawfulMvFunctor F
α : TypeVec n
ι ι' : Type u
R : ι' → ι' → Prop
x : F (α ::: ι)
f g : ι → ι'
hh : ∀ (x : ι), R (f x) (g x)
h : ι → { x // uncurry R x } := fun x => { val := (f x, g x), property := (_ : R (f x) (g x)) }
b : α ::: ι ⟹ Subtype_ (repeatEq α) ::: { x // uncurry R x } := diagSub ::: h
c : Subtype_ (repeatEq α) ::: { x // uncurry R x } ⟹
  (fun i => { x // ofRepeat (RelLast' α R (Fin2.fs i) x) }) ::: Subtype (uncurry R) :=
  ofSubtype (repeatEq α) ::: _root_.id
⊢ subtypeVal (repeatEq α) ⊚ dropFun (toSubtype (RelLast' α R)) ⊚ ofSubtype (repeatEq α) ⊚ diagSub =
    dropFun ((TypeVec.id ::: f) ⊗' (TypeVec.id ::: g)) ⊚ dropFun prod.diag
[PROOFSTEP]
simp only [prod_map_id, dropFun_prod, dropFun_appendFun, dropFun_diag, id_comp, dropFun_toSubtype]
[GOAL]
case h₀
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
lawful : LawfulMvFunctor F
α : TypeVec n
ι ι' : Type u
R : ι' → ι' → Prop
x : F (α ::: ι)
f g : ι → ι'
hh : ∀ (x : ι), R (f x) (g x)
h : ι → { x // uncurry R x } := fun x => { val := (f x, g x), property := (_ : R (f x) (g x)) }
b : α ::: ι ⟹ Subtype_ (repeatEq α) ::: { x // uncurry R x } := diagSub ::: h
c : Subtype_ (repeatEq α) ::: { x // uncurry R x } ⟹
  (fun i => { x // ofRepeat (RelLast' α R (Fin2.fs i) x) }) ::: Subtype (uncurry R) :=
  ofSubtype (repeatEq α) ::: _root_.id
⊢ subtypeVal (repeatEq α) ⊚ (toSubtype fun i x => RelLast' α R (Fin2.fs i) x) ⊚ ofSubtype (repeatEq α) ⊚ diagSub =
    prod.diag
[PROOFSTEP]
erw [toSubtype_of_subtype_assoc, id_comp]
[GOAL]
case h₀
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
lawful : LawfulMvFunctor F
α : TypeVec n
ι ι' : Type u
R : ι' → ι' → Prop
x : F (α ::: ι)
f g : ι → ι'
hh : ∀ (x : ι), R (f x) (g x)
h : ι → { x // uncurry R x } := fun x => { val := (f x, g x), property := (_ : R (f x) (g x)) }
b : α ::: ι ⟹ Subtype_ (repeatEq α) ::: { x // uncurry R x } := diagSub ::: h
c : Subtype_ (repeatEq α) ::: { x // uncurry R x } ⟹
  (fun i => { x // ofRepeat (RelLast' α R (Fin2.fs i) x) }) ::: Subtype (uncurry R) :=
  ofSubtype (repeatEq α) ::: _root_.id
⊢ (fun i x => subtypeVal (repeatEq α) i (diagSub i x)) = prod.diag
[PROOFSTEP]
clear liftR_map_last q mvf lawful F x R f g hh h b c
[GOAL]
case h₀
n : ℕ
α : TypeVec n
ι ι' : Type u
⊢ (fun i x => subtypeVal (repeatEq α) i (diagSub i x)) = prod.diag
[PROOFSTEP]
ext (i x) : 2
[GOAL]
case h₀.a.h
n : ℕ
α : TypeVec n
ι ι' : Type u
i : Fin2 n
x : TypeVec.drop (α ::: ι) i
⊢ subtypeVal (repeatEq α) i (diagSub i x) = prod.diag i x
[PROOFSTEP]
induction i with
| fz => rfl
| fs _ ih => apply ih
[GOAL]
case h₀.a.h
n : ℕ
α : TypeVec n
ι ι' : Type u
i : Fin2 n
x : TypeVec.drop (α ::: ι) i
⊢ subtypeVal (repeatEq α) i (diagSub i x) = prod.diag i x
[PROOFSTEP]
induction i with
| fz => rfl
| fs _ ih => apply ih
[GOAL]
case h₀.a.h.fz
n : ℕ
ι ι' : Type u
n✝ : ℕ
α : TypeVec (Nat.succ n✝)
x : TypeVec.drop (α ::: ι) Fin2.fz
⊢ subtypeVal (repeatEq α) Fin2.fz (diagSub Fin2.fz x) = prod.diag Fin2.fz x
[PROOFSTEP]

| fz => rfl
[GOAL]
case h₀.a.h.fz
n : ℕ
ι ι' : Type u
n✝ : ℕ
α : TypeVec (Nat.succ n✝)
x : TypeVec.drop (α ::: ι) Fin2.fz
⊢ subtypeVal (repeatEq α) Fin2.fz (diagSub Fin2.fz x) = prod.diag Fin2.fz x
[PROOFSTEP]
rfl
[GOAL]
case h₀.a.h.fs
n : ℕ
ι ι' : Type u
n✝ : ℕ
a✝ : Fin2 n✝
ih : ∀ {α : TypeVec n✝} (x : TypeVec.drop (α ::: ι) a✝), subtypeVal (repeatEq α) a✝ (diagSub a✝ x) = prod.diag a✝ x
α : TypeVec (Nat.succ n✝)
x : TypeVec.drop (α ::: ι) (Fin2.fs a✝)
⊢ subtypeVal (repeatEq α) (Fin2.fs a✝) (diagSub (Fin2.fs a✝) x) = prod.diag (Fin2.fs a✝) x
[PROOFSTEP]

| fs _ ih => apply ih
[GOAL]
case h₀.a.h.fs
n : ℕ
ι ι' : Type u
n✝ : ℕ
a✝ : Fin2 n✝
ih : ∀ {α : TypeVec n✝} (x : TypeVec.drop (α ::: ι) a✝), subtypeVal (repeatEq α) a✝ (diagSub a✝ x) = prod.diag a✝ x
α : TypeVec (Nat.succ n✝)
x : TypeVec.drop (α ::: ι) (Fin2.fs a✝)
⊢ subtypeVal (repeatEq α) (Fin2.fs a✝) (diagSub (Fin2.fs a✝) x) = prod.diag (Fin2.fs a✝) x
[PROOFSTEP]
apply ih
[GOAL]
case h₁
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
lawful : LawfulMvFunctor F
α : TypeVec n
ι ι' : Type u
R : ι' → ι' → Prop
x : F (α ::: ι)
f g : ι → ι'
hh : ∀ (x : ι), R (f x) (g x)
h : ι → { x // uncurry R x } := fun x => { val := (f x, g x), property := (_ : R (f x) (g x)) }
b : α ::: ι ⟹ Subtype_ (repeatEq α) ::: { x // uncurry R x } := diagSub ::: h
c : Subtype_ (repeatEq α) ::: { x // uncurry R x } ⟹
  (fun i => { x // ofRepeat (RelLast' α R (Fin2.fs i) x) }) ::: Subtype (uncurry R) :=
  ofSubtype (repeatEq α) ::: _root_.id
⊢ lastFun
      (subtypeVal (RelLast' α R) ⊚
        toSubtype (RelLast' α R) ⊚
          fromAppend1DropLast ⊚
            (ofSubtype (repeatEq α) ::: _root_.id) ⊚
              (diagSub ::: fun x => { val := (f x, g x), property := (_ : R (f x) (g x)) })) =
    lastFun (((TypeVec.id ::: f) ⊗' (TypeVec.id ::: g)) ⊚ prod.diag)
[PROOFSTEP]
simp only [lastFun_from_append1_drop_last, lastFun_toSubtype, lastFun_appendFun, lastFun_subtypeVal, comp.left_id,
  lastFun_comp, lastFun_prod]
[GOAL]
case h₁
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
lawful : LawfulMvFunctor F
α : TypeVec n
ι ι' : Type u
R : ι' → ι' → Prop
x : F (α ::: ι)
f g : ι → ι'
hh : ∀ (x : ι), R (f x) (g x)
h : ι → { x // uncurry R x } := fun x => { val := (f x, g x), property := (_ : R (f x) (g x)) }
b : α ::: ι ⟹ Subtype_ (repeatEq α) ::: { x // uncurry R x } := diagSub ::: h
c : Subtype_ (repeatEq α) ::: { x // uncurry R x } ⟹
  (fun i => { x // ofRepeat (RelLast' α R (Fin2.fs i) x) }) ::: Subtype (uncurry R) :=
  ofSubtype (repeatEq α) ::: _root_.id
⊢ (Subtype.val ∘ fun x => { val := (f x, g x), property := (_ : R (f x) (g x)) }) = Prod.map f g ∘ lastFun prod.diag
[PROOFSTEP]
ext1
[GOAL]
case h₁.h
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
lawful : LawfulMvFunctor F
α : TypeVec n
ι ι' : Type u
R : ι' → ι' → Prop
x : F (α ::: ι)
f g : ι → ι'
hh : ∀ (x : ι), R (f x) (g x)
h : ι → { x // uncurry R x } := fun x => { val := (f x, g x), property := (_ : R (f x) (g x)) }
b : α ::: ι ⟹ Subtype_ (repeatEq α) ::: { x // uncurry R x } := diagSub ::: h
c : Subtype_ (repeatEq α) ::: { x // uncurry R x } ⟹
  (fun i => { x // ofRepeat (RelLast' α R (Fin2.fs i) x) }) ::: Subtype (uncurry R) :=
  ofSubtype (repeatEq α) ::: _root_.id
x✝ : TypeVec.last (α ::: ι)
⊢ (Subtype.val ∘ fun x => { val := (f x, g x), property := (_ : R (f x) (g x)) }) x✝ =
    (Prod.map f g ∘ lastFun prod.diag) x✝
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
inst✝ : LawfulMvFunctor F
α : TypeVec n
ι : Type u
R : ι → ι → Prop
x : F (α ::: ι)
f : ι → ι
hh : ∀ (x : ι), R (f x) x
⊢ LiftR' (RelLast' α R) ((TypeVec.id ::: f) <$$> x) x
[PROOFSTEP]
have := liftR_map_last R x f id hh
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
inst✝ : LawfulMvFunctor F
α : TypeVec n
ι : Type u
R : ι → ι → Prop
x : F (α ::: ι)
f : ι → ι
hh : ∀ (x : ι), R (f x) x
this : LiftR' (RelLast' α R) ((TypeVec.id ::: f) <$$> x) ((TypeVec.id ::: _root_.id) <$$> x)
⊢ LiftR' (RelLast' α R) ((TypeVec.id ::: f) <$$> x) x
[PROOFSTEP]
rwa [appendFun_id_id, MvFunctor.id_map] at this 
[GOAL]
n : ℕ
F✝ : TypeVec (n + 1) → Type u
mvf : MvFunctor F✝
q✝ : MvQPF F✝
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : Cofix F α
⊢ Quot.mk Mcongr (repr x) = x
[PROOFSTEP]
let R := fun x y : Cofix F α => abs (repr y) = x
[GOAL]
n : ℕ
F✝ : TypeVec (n + 1) → Type u
mvf : MvFunctor F✝
q✝ : MvQPF F✝
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : Cofix F α
R : Cofix F α → Cofix F α → Prop := fun x y => abs (repr y) = x
⊢ Quot.mk Mcongr (repr x) = x
[PROOFSTEP]
refine' Cofix.bisim₂ R _ _ _ rfl
[GOAL]
n : ℕ
F✝ : TypeVec (n + 1) → Type u
mvf : MvFunctor F✝
q✝ : MvQPF F✝
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : Cofix F α
R : Cofix F α → Cofix F α → Prop := fun x y => abs (repr y) = x
⊢ ∀ (x y : Cofix F α), R x y → LiftR' (RelLast' α R) (dest x) (dest y)
[PROOFSTEP]
clear x
[GOAL]
n : ℕ
F✝ : TypeVec (n + 1) → Type u
mvf : MvFunctor F✝
q✝ : MvQPF F✝
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
R : Cofix F α → Cofix F α → Prop := fun x y => abs (repr y) = x
⊢ ∀ (x y : Cofix F α), R x y → LiftR' (RelLast' α R) (dest x) (dest y)
[PROOFSTEP]
rintro x y h
[GOAL]
n : ℕ
F✝ : TypeVec (n + 1) → Type u
mvf : MvFunctor F✝
q✝ : MvQPF F✝
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
R : Cofix F α → Cofix F α → Prop := fun x y => abs (repr y) = x
x y : Cofix F α
h : R x y
⊢ LiftR' (RelLast' α R) (dest x) (dest y)
[PROOFSTEP]
subst h
[GOAL]
n : ℕ
F✝ : TypeVec (n + 1) → Type u
mvf : MvFunctor F✝
q✝ : MvQPF F✝
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
R : Cofix F α → Cofix F α → Prop := fun x y => abs (repr y) = x
y : Cofix F α
⊢ LiftR' (RelLast' α R) (dest (abs (repr y))) (dest y)
[PROOFSTEP]
dsimp [Cofix.dest, Cofix.abs]
[GOAL]
n : ℕ
F✝ : TypeVec (n + 1) → Type u
mvf : MvFunctor F✝
q✝ : MvQPF F✝
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
R : Cofix F α → Cofix F α → Prop := fun x y => abs (repr y) = x
y : Cofix F α
⊢ LiftR' (RelLast' α fun x y => Quot.mk Mcongr (repr y) = x)
    ((TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) (repr y)))
    (Quot.lift (fun x => (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x))
      (_ :
        ∀ (x y : M (P F) α),
          Mcongr x y →
            (fun x => (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) x =
              (fun x => (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) y)
      y)
[PROOFSTEP]
induction y using Quot.ind
[GOAL]
case mk
n : ℕ
F✝ : TypeVec (n + 1) → Type u
mvf : MvFunctor F✝
q✝ : MvQPF F✝
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
R : Cofix F α → Cofix F α → Prop := fun x y => abs (repr y) = x
a✝ : M (P F) α
⊢ LiftR' (RelLast' α fun x y => Quot.mk Mcongr (repr y) = x)
    ((TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) (repr (Quot.mk Mcongr a✝))))
    (Quot.lift (fun x => (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x))
      (_ :
        ∀ (x y : M (P F) α),
          Mcongr x y →
            (fun x => (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) x =
              (fun x => (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) y)
      (Quot.mk Mcongr a✝))
[PROOFSTEP]
simp only [Cofix.repr, M.dest_corec, abs_map, MvQPF.abs_repr, Function.comp]
[GOAL]
case mk
n : ℕ
F✝ : TypeVec (n + 1) → Type u
mvf : MvFunctor F✝
q✝ : MvQPF F✝
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
R : Cofix F α → Cofix F α → Prop := fun x y => abs (repr y) = x
a✝ : M (P F) α
⊢ LiftR' (RelLast' α fun x y => Quot.mk Mcongr (M.corec (P F) (fun x => MvQPF.repr (dest x)) y) = x)
    ((TypeVec.id ::: Quot.mk Mcongr) <$$>
      (TypeVec.id ::: M.corec (P F) fun x => MvQPF.repr (dest x)) <$$> dest (Quot.mk Mcongr a✝))
    ((TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a✝))
[PROOFSTEP]
conv =>
  congr
  rfl
  rw [Cofix.dest]
[GOAL]
n : ℕ
F✝ : TypeVec (n + 1) → Type u
mvf : MvFunctor F✝
q✝ : MvQPF F✝
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
R : Cofix F α → Cofix F α → Prop := fun x y => abs (repr y) = x
a✝ : M (P F) α
| LiftR' (RelLast' α fun x y => Quot.mk Mcongr (M.corec (P F) (fun x => MvQPF.repr (dest x)) y) = x)
    ((TypeVec.id ::: Quot.mk Mcongr) <$$>
      (TypeVec.id ::: M.corec (P F) fun x => MvQPF.repr (dest x)) <$$> dest (Quot.mk Mcongr a✝))
    ((TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a✝))
[PROOFSTEP]
  congr
  rfl
  rw [Cofix.dest]
[GOAL]
n : ℕ
F✝ : TypeVec (n + 1) → Type u
mvf : MvFunctor F✝
q✝ : MvQPF F✝
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
R : Cofix F α → Cofix F α → Prop := fun x y => abs (repr y) = x
a✝ : M (P F) α
| LiftR' (RelLast' α fun x y => Quot.mk Mcongr (M.corec (P F) (fun x => MvQPF.repr (dest x)) y) = x)
    ((TypeVec.id ::: Quot.mk Mcongr) <$$>
      (TypeVec.id ::: M.corec (P F) fun x => MvQPF.repr (dest x)) <$$> dest (Quot.mk Mcongr a✝))
    ((TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a✝))
[PROOFSTEP]
  congr
  rfl
  rw [Cofix.dest]
[GOAL]
n : ℕ
F✝ : TypeVec (n + 1) → Type u
mvf : MvFunctor F✝
q✝ : MvQPF F✝
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
R : Cofix F α → Cofix F α → Prop := fun x y => abs (repr y) = x
a✝ : M (P F) α
| LiftR' (RelLast' α fun x y => Quot.mk Mcongr (M.corec (P F) (fun x => MvQPF.repr (dest x)) y) = x)
    ((TypeVec.id ::: Quot.mk Mcongr) <$$>
      (TypeVec.id ::: M.corec (P F) fun x => MvQPF.repr (dest x)) <$$> dest (Quot.mk Mcongr a✝))
    ((TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a✝))
[PROOFSTEP]
congr
[GOAL]
case R
n : ℕ
F✝ : TypeVec (n + 1) → Type u
mvf : MvFunctor F✝
q✝ : MvQPF F✝
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
R : Cofix F α → Cofix F α → Prop := fun x y => abs (repr y) = x
a✝ : M (P F) α
| RelLast' α fun x y => Quot.mk Mcongr (M.corec (P F) (fun x => MvQPF.repr (dest x)) y) = x
case a
n : ℕ
F✝ : TypeVec (n + 1) → Type u
mvf : MvFunctor F✝
q✝ : MvQPF F✝
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
R : Cofix F α → Cofix F α → Prop := fun x y => abs (repr y) = x
a✝ : M (P F) α
| (TypeVec.id ::: Quot.mk Mcongr) <$$>
    (TypeVec.id ::: M.corec (P F) fun x => MvQPF.repr (dest x)) <$$> dest (Quot.mk Mcongr a✝)
case a
n : ℕ
F✝ : TypeVec (n + 1) → Type u
mvf : MvFunctor F✝
q✝ : MvQPF F✝
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
R : Cofix F α → Cofix F α → Prop := fun x y => abs (repr y) = x
a✝ : M (P F) α
| (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a✝)
[PROOFSTEP]
rfl
[GOAL]
case a
n : ℕ
F✝ : TypeVec (n + 1) → Type u
mvf : MvFunctor F✝
q✝ : MvQPF F✝
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
R : Cofix F α → Cofix F α → Prop := fun x y => abs (repr y) = x
a✝ : M (P F) α
| (TypeVec.id ::: Quot.mk Mcongr) <$$>
    (TypeVec.id ::: M.corec (P F) fun x => MvQPF.repr (dest x)) <$$> dest (Quot.mk Mcongr a✝)
case a
n : ℕ
F✝ : TypeVec (n + 1) → Type u
mvf : MvFunctor F✝
q✝ : MvQPF F✝
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
R : Cofix F α → Cofix F α → Prop := fun x y => abs (repr y) = x
a✝ : M (P F) α
| (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a✝)
[PROOFSTEP]
rw [Cofix.dest]
[GOAL]
case mk
n : ℕ
F✝ : TypeVec (n + 1) → Type u
mvf : MvFunctor F✝
q✝ : MvQPF F✝
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
R : Cofix F α → Cofix F α → Prop := fun x y => abs (repr y) = x
a✝ : M (P F) α
⊢ LiftR' (RelLast' α fun x y => Quot.mk Mcongr (M.corec (P F) (fun x => MvQPF.repr (dest x)) y) = x)
    ((TypeVec.id ::: Quot.mk Mcongr) <$$>
      (TypeVec.id :::
          M.corec (P F) fun x =>
            MvQPF.repr
              (Quot.lift (fun x => (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x))
                (_ :
                  ∀ (x y : M (P F) α),
                    Mcongr x y →
                      (fun x => (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) x =
                        (fun x => (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) y)
                x)) <$$>
        Quot.lift (fun x => (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x))
          (_ :
            ∀ (x y : M (P F) α),
              Mcongr x y →
                (fun x => (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) x =
                  (fun x => (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) y)
          (Quot.mk Mcongr a✝))
    ((TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a✝))
[PROOFSTEP]
rw [MvFunctor.map_map, MvFunctor.map_map, ← appendFun_comp_id, ← appendFun_comp_id]
[GOAL]
case mk
n : ℕ
F✝ : TypeVec (n + 1) → Type u
mvf : MvFunctor F✝
q✝ : MvQPF F✝
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
R : Cofix F α → Cofix F α → Prop := fun x y => abs (repr y) = x
a✝ : M (P F) α
⊢ LiftR' (RelLast' α fun x y => Quot.mk Mcongr (M.corec (P F) (fun x => MvQPF.repr (dest x)) y) = x)
    ((TypeVec.id :::
        (Quot.mk Mcongr ∘
            M.corec (P F) fun x =>
              MvQPF.repr
                (Quot.lift (fun x => (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x))
                  (_ :
                    ∀ (x y : M (P F) α),
                      Mcongr x y →
                        (fun x => (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) x =
                          (fun x => (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) y)
                  x)) ∘
          Quot.mk Mcongr) <$$>
      MvQPF.abs (M.dest (P F) a✝))
    ((TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a✝))
[PROOFSTEP]
apply liftR_map_last
[GOAL]
case mk.hh
n : ℕ
F✝ : TypeVec (n + 1) → Type u
mvf : MvFunctor F✝
q✝ : MvQPF F✝
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
R : Cofix F α → Cofix F α → Prop := fun x y => abs (repr y) = x
a✝ : M (P F) α
⊢ ∀ (x : M (P F) α),
    Quot.mk Mcongr (M.corec (P F) (fun x => MvQPF.repr (dest x)) (Quot.mk Mcongr x)) =
      ((Quot.mk Mcongr ∘
            M.corec (P F) fun x =>
              MvQPF.repr
                (Quot.lift (fun x => (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x))
                  (_ :
                    ∀ (x y : M (P F) α),
                      Mcongr x y →
                        (fun x => (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) x =
                          (fun x => (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) y)
                  x)) ∘
          Quot.mk Mcongr)
        x
[PROOFSTEP]
intros
[GOAL]
case mk.hh
n : ℕ
F✝ : TypeVec (n + 1) → Type u
mvf : MvFunctor F✝
q✝ : MvQPF F✝
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
R : Cofix F α → Cofix F α → Prop := fun x y => abs (repr y) = x
a✝ x✝ : M (P F) α
⊢ Quot.mk Mcongr (M.corec (P F) (fun x => MvQPF.repr (dest x)) (Quot.mk Mcongr x✝)) =
    ((Quot.mk Mcongr ∘
          M.corec (P F) fun x =>
            MvQPF.repr
              (Quot.lift (fun x => (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x))
                (_ :
                  ∀ (x y : M (P F) α),
                    Mcongr x y →
                      (fun x => (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) x =
                        (fun x => (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) y)
                x)) ∘
        Quot.mk Mcongr)
      x✝
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
X Y : Type u
x₀ : X
f : X → Y
g : Y → F (α ::: X)
⊢ Cofix.corec (g ∘ f) x₀ = Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) (f x₀)
[PROOFSTEP]
mv_bisim x₀ with R a b x Ha Hb
[GOAL]
case intro.intro
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
X Y : Type u
x₀ : X
f : X → Y
g : Y → F (α ::: X)
R : Cofix F α → Cofix F α → Prop :=
  fun a b => ∃ x, a = Cofix.corec (g ∘ f) x ∧ b = Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) (f x)
a b : Cofix F α
x : X
Ha : a = Cofix.corec (g ∘ f) x
Hb : b = Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) (f x)
⊢ LiftR' (RelLast' α R) (Cofix.dest a) (Cofix.dest b)
[PROOFSTEP]
rw [Ha, Hb, Cofix.dest_corec, Cofix.dest_corec, Function.comp_apply, Function.comp_apply]
[GOAL]
case intro.intro
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
X Y : Type u
x₀ : X
f : X → Y
g : Y → F (α ::: X)
R : Cofix F α → Cofix F α → Prop :=
  fun a b => ∃ x, a = Cofix.corec (g ∘ f) x ∧ b = Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) (f x)
a b : Cofix F α
x : X
Ha : a = Cofix.corec (g ∘ f) x
Hb : b = Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) (f x)
⊢ LiftR' (RelLast' α R) ((TypeVec.id ::: Cofix.corec (g ∘ f)) <$$> g (f x))
    ((TypeVec.id ::: Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g)) <$$> (TypeVec.id ::: f) <$$> g (f x))
[PROOFSTEP]
rw [MvFunctor.map_map, ← appendFun_comp_id]
[GOAL]
case intro.intro
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
X Y : Type u
x₀ : X
f : X → Y
g : Y → F (α ::: X)
R : Cofix F α → Cofix F α → Prop :=
  fun a b => ∃ x, a = Cofix.corec (g ∘ f) x ∧ b = Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) (f x)
a b : Cofix F α
x : X
Ha : a = Cofix.corec (g ∘ f) x
Hb : b = Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) (f x)
⊢ LiftR' (RelLast' α R) ((TypeVec.id ::: Cofix.corec (g ∘ f)) <$$> g (f x))
    ((TypeVec.id ::: Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) ∘ f) <$$> g (f x))
[PROOFSTEP]
refine' liftR_map_last _ _ _ _ _
[GOAL]
case intro.intro
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
X Y : Type u
x₀ : X
f : X → Y
g : Y → F (α ::: X)
R : Cofix F α → Cofix F α → Prop :=
  fun a b => ∃ x, a = Cofix.corec (g ∘ f) x ∧ b = Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) (f x)
a b : Cofix F α
x : X
Ha : a = Cofix.corec (g ∘ f) x
Hb : b = Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) (f x)
⊢ ∀ (x : X), R (Cofix.corec (g ∘ f) x) ((Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) ∘ f) x)
[PROOFSTEP]
intro a
[GOAL]
case intro.intro
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
X Y : Type u
x₀ : X
f : X → Y
g : Y → F (α ::: X)
R : Cofix F α → Cofix F α → Prop :=
  fun a b => ∃ x, a = Cofix.corec (g ∘ f) x ∧ b = Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) (f x)
a✝ b : Cofix F α
x : X
Ha : a✝ = Cofix.corec (g ∘ f) x
Hb : b = Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) (f x)
a : X
⊢ R (Cofix.corec (g ∘ f) a) ((Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) ∘ f) a)
[PROOFSTEP]
refine' ⟨a, rfl, rfl⟩
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x : β
⊢ dest (corec' g x) = (TypeVec.id ::: Sum.elim _root_.id (corec' g)) <$$> g x
[PROOFSTEP]
rw [Cofix.corec', Cofix.dest_corec]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec 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
[PROOFSTEP]
dsimp
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec 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
[PROOFSTEP]
congr!
[GOAL]
case h.e'_6.h.e'_7
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec 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)
[PROOFSTEP]
ext (i | i)
[GOAL]
case h.e'_6.h.e'_7.h.inl
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x : β
i : Cofix F α
⊢ corec (Sum.elim (MvFunctor.map (TypeVec.id ::: Sum.inl) ∘ dest) g) (Sum.inl i) =
    Sum.elim _root_.id (corec' g) (Sum.inl i)
[PROOFSTEP]
erw [corec_roll]
[GOAL]
case h.e'_6.h.e'_7.h.inr
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x i : β
⊢ corec (Sum.elim (MvFunctor.map (TypeVec.id ::: Sum.inl) ∘ dest) g) (Sum.inr i) =
    Sum.elim _root_.id (corec' g) (Sum.inr i)
[PROOFSTEP]
erw [corec_roll]
[GOAL]
case h.e'_6.h.e'_7.h.inl
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x : β
i : Cofix F α
⊢ corec
      (MvFunctor.map (TypeVec.id ::: fun x => x) ∘
        Sum.rec (fun val => (MvFunctor.map (TypeVec.id ::: Sum.inl) ∘ dest) val) fun val => g val)
      (Sum.inl i) =
    Sum.elim _root_.id (corec' g) (Sum.inl i)
[PROOFSTEP]
dsimp [Cofix.corec']
[GOAL]
case h.e'_6.h.e'_7.h.inr
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x i : β
⊢ corec
      (MvFunctor.map (TypeVec.id ::: fun x => x) ∘
        Sum.rec (fun val => (MvFunctor.map (TypeVec.id ::: Sum.inl) ∘ dest) val) fun val => g val)
      (Sum.inr i) =
    Sum.elim _root_.id (corec' g) (Sum.inr i)
[PROOFSTEP]
dsimp [Cofix.corec']
[GOAL]
case h.e'_6.h.e'_7.h.inl
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec 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) <$$> dest val) fun val => g val)
      (Sum.inl i) =
    i
[PROOFSTEP]
mv_bisim i with R a b x Ha Hb
[GOAL]
case h.e'_6.h.e'_7.h.inl.intro.intro
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec 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) <$$> dest val) 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) <$$> dest val) fun val => g val)
      (Sum.inl x)
Hb : b = x
⊢ LiftR' (RelLast' α R) (dest a) (dest b)
[PROOFSTEP]
rw [Ha, Hb, Cofix.dest_corec]
[GOAL]
case h.e'_6.h.e'_7.h.inl.intro.intro
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec 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) <$$> dest val) 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) <$$> dest val) 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) <$$> dest val) fun val => g val)) <$$>
      (MvFunctor.map (TypeVec.id ::: fun x => x) ∘
          Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> dest val) fun val => g val)
        (Sum.inl x))
    (dest x)
[PROOFSTEP]
dsimp [Function.comp]
[GOAL]
case h.e'_6.h.e'_7.h.inl.intro.intro
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec 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) <$$> dest val) 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) <$$> dest val) fun val => g val)
      (Sum.inl x)
Hb : b = x
⊢ LiftR'
    (RelLast' α fun a b =>
      ∃ x,
        a =
            corec
              (fun x =>
                (TypeVec.id ::: fun x => x) <$$>
                  Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> dest val) (fun val => g val) x)
              (Sum.inl x) ∧
          b = x)
    ((TypeVec.id :::
        corec fun x =>
          (TypeVec.id ::: fun x => x) <$$>
            Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> dest val) (fun val => g val) x) <$$>
      (TypeVec.id ::: fun x => x) <$$> (TypeVec.id ::: Sum.inl) <$$> dest x)
    (dest x)
[PROOFSTEP]
repeat rw [MvFunctor.map_map, ← appendFun_comp_id]
[GOAL]
case h.e'_6.h.e'_7.h.inl.intro.intro
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec 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) <$$> dest val) 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) <$$> dest val) fun val => g val)
      (Sum.inl x)
Hb : b = x
⊢ LiftR'
    (RelLast' α fun a b =>
      ∃ x,
        a =
            corec
              (fun x =>
                (TypeVec.id ::: fun x => x) <$$>
                  Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> dest val) (fun val => g val) x)
              (Sum.inl x) ∧
          b = x)
    ((TypeVec.id :::
        corec fun x =>
          (TypeVec.id ::: fun x => x) <$$>
            Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> dest val) (fun val => g val) x) <$$>
      (TypeVec.id ::: fun x => x) <$$> (TypeVec.id ::: Sum.inl) <$$> dest x)
    (dest x)
[PROOFSTEP]
rw [MvFunctor.map_map, ← appendFun_comp_id]
[GOAL]
case h.e'_6.h.e'_7.h.inl.intro.intro
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec 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) <$$> dest val) 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) <$$> dest val) fun val => g val)
      (Sum.inl x)
Hb : b = x
⊢ LiftR'
    (RelLast' α fun a b =>
      ∃ x,
        a =
            corec
              (fun x =>
                (TypeVec.id ::: fun x => x) <$$>
                  Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> dest val) (fun val => g val) x)
              (Sum.inl x) ∧
          b = x)
    ((TypeVec.id :::
        (corec fun x =>
            (TypeVec.id ::: fun x => x) <$$>
              Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> dest val) (fun val => g val) x) ∘
          fun x => x) <$$>
      (TypeVec.id ::: Sum.inl) <$$> dest x)
    (dest x)
[PROOFSTEP]
rw [MvFunctor.map_map, ← appendFun_comp_id]
[GOAL]
case h.e'_6.h.e'_7.h.inl.intro.intro
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec 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) <$$> dest val) 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) <$$> dest val) fun val => g val)
      (Sum.inl x)
Hb : b = x
⊢ LiftR'
    (RelLast' α fun a b =>
      ∃ x,
        a =
            corec
              (fun x =>
                (TypeVec.id ::: fun x => x) <$$>
                  Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> dest val) (fun val => g val) x)
              (Sum.inl x) ∧
          b = x)
    ((TypeVec.id :::
        ((corec fun x =>
              (TypeVec.id ::: fun x => x) <$$>
                Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> dest val) (fun val => g val) x) ∘
            fun x => x) ∘
          Sum.inl) <$$>
      dest x)
    (dest x)
[PROOFSTEP]
rw [MvFunctor.map_map, ← appendFun_comp_id]
[GOAL]
case h.e'_6.h.e'_7.h.inl.intro.intro
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec 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) <$$> dest val) 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) <$$> dest val) fun val => g val)
      (Sum.inl x)
Hb : b = x
⊢ LiftR'
    (RelLast' α fun a b =>
      ∃ x,
        a =
            corec
              (fun x =>
                (TypeVec.id ::: fun x => x) <$$>
                  Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> dest val) (fun val => g val) x)
              (Sum.inl x) ∧
          b = x)
    ((TypeVec.id :::
        ((corec fun x =>
              (TypeVec.id ::: fun x => x) <$$>
                Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> dest val) (fun val => g val) x) ∘
            fun x => x) ∘
          Sum.inl) <$$>
      dest x)
    (dest x)
[PROOFSTEP]
apply liftR_map_last'
[GOAL]
case h.e'_6.h.e'_7.h.inl.intro.intro.hh
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec 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) <$$> dest val) 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) <$$> dest val) fun val => g val)
      (Sum.inl x)
Hb : b = x
⊢ ∀ (x : Cofix F α),
    ∃ x_1,
      (((corec fun x =>
                  (TypeVec.id ::: fun x => x) <$$>
                    Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> dest val) (fun val => g val) x) ∘
                fun x => x) ∘
              Sum.inl)
            x =
          corec
            (fun x =>
              (TypeVec.id ::: fun x => x) <$$>
                Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> dest val) (fun val => g val) x)
            (Sum.inl x_1) ∧
        x = x_1
[PROOFSTEP]
dsimp [Function.comp]
[GOAL]
case h.e'_6.h.e'_7.h.inl.intro.intro.hh
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec 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) <$$> dest val) 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) <$$> dest val) fun val => g val)
      (Sum.inl x)
Hb : b = x
⊢ ∀ (x : Cofix F α),
    ∃ x_1,
      corec
            (fun x =>
              (TypeVec.id ::: fun x => x) <$$>
                Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> dest val) (fun val => g val) x)
            (Sum.inl x) =
          corec
            (fun x =>
              (TypeVec.id ::: fun x => x) <$$>
                Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> dest val) (fun val => g val) x)
            (Sum.inl x_1) ∧
        x = x_1
[PROOFSTEP]
intros
[GOAL]
case h.e'_6.h.e'_7.h.inl.intro.intro.hh
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec 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) <$$> dest val) 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) <$$> dest val) fun val => g val)
      (Sum.inl x)
Hb : b = x
x✝ : Cofix F α
⊢ ∃ x,
    corec
          (fun x =>
            (TypeVec.id ::: fun x => x) <$$>
              Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> dest val) (fun val => g val) x)
          (Sum.inl x✝) =
        corec
          (fun x =>
            (TypeVec.id ::: fun x => x) <$$>
              Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> dest val) (fun val => g val) x)
          (Sum.inl x) ∧
      x✝ = x
[PROOFSTEP]
exact ⟨_, rfl, rfl⟩
[GOAL]
case h.e'_6.h.e'_7.h.inr
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec 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) <$$> dest val) fun val => g val)
      (Sum.inr i) =
    corec (Sum.elim (MvFunctor.map (TypeVec.id ::: Sum.inl) ∘ dest) g) (Sum.inr i)
[PROOFSTEP]
congr with y
[GOAL]
case h.e'_6.h.e'_7.h.inr.e_g.h
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec 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) <$$> dest val) fun val => g val)
      y =
    Sum.elim (MvFunctor.map (TypeVec.id ::: Sum.inl) ∘ dest) g y
[PROOFSTEP]
erw [appendFun_id_id]
[GOAL]
case h.e'_6.h.e'_7.h.inr.e_g.h
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x i : β
y : Cofix F α ⊕ β
⊢ (MvFunctor.map TypeVec.id ∘ Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> dest val) fun val => g val) y =
    Sum.elim (MvFunctor.map (TypeVec.id ::: Sum.inl) ∘ dest) g y
[PROOFSTEP]
simp [MvFunctor.id_map, Sum.elim]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : {X : Type u} → (Cofix F α → X) → (β → X) → β → F (α ::: X)
x : β
h :
  ∀ (X Y : Type u) (f : Cofix F α → X) (f' : β → X) (k : X → Y), g (k ∘ f) (k ∘ f') x = (TypeVec.id ::: k) <$$> g f f' x
⊢ dest (corec₁ g x) = g _root_.id (corec₁ g) x
[PROOFSTEP]
rw [Cofix.corec₁, Cofix.dest_corec', ← h]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : {X : Type u} → (Cofix F α → X) → (β → X) → β → F (α ::: X)
x : β
h :
  ∀ (X Y : Type u) (f : Cofix F α → X) (f' : β → X) (k : X → Y), g (k ∘ f) (k ∘ f') x = (TypeVec.id ::: k) <$$> g f f' x
⊢ g (Sum.elim _root_.id (corec' fun x => g Sum.inl Sum.inr x) ∘ Sum.inl)
      (Sum.elim _root_.id (corec' fun x => g Sum.inl Sum.inr x) ∘ Sum.inr) x =
    g _root_.id (corec₁ g) x
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
⊢ ∀ {α β : TypeVec n} (f : α ⟹ β) (p : Obj (mp (P F)) α),
    (fun {α} => Quot.mk Mcongr) (f <$$> p) = f <$$> (fun {α} => Quot.mk Mcongr) p
[PROOFSTEP]
intros
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
mvf : MvFunctor F
q : MvQPF F
α✝ β✝ : TypeVec n
f✝ : α✝ ⟹ β✝
p✝ : Obj (mp (P F)) α✝
⊢ (fun {α} => Quot.mk Mcongr) (f✝ <$$> p✝) = f✝ <$$> (fun {α} => Quot.mk Mcongr) p✝
[PROOFSTEP]
rfl
