[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
x : PFunctor.M (last P)
i : Fin2 n
inst✝ : Inhabited (B (drop P) (PFunctor.M.head x) i)
a : (last P).A := PFunctor.M.head x
f : PFunctor.B (last P) (PFunctor.M.head x) → PFunctor.M (last P) := PFunctor.M.children x
⊢ ∀ (a_1 : (last P).A) (f_1 : PFunctor.B (last P) a_1 → PFunctor.M (last P)),
    (fun x_1 => PFunctor.M.dest x = { fst := a, snd := f }) (PFunctor.M.mk { fst := a_1, snd := f_1 })
[PROOFSTEP]
intros
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
x : PFunctor.M (last P)
i : Fin2 n
inst✝ : Inhabited (B (drop P) (PFunctor.M.head x) i)
a : (last P).A := PFunctor.M.head x
f : PFunctor.B (last P) (PFunctor.M.head x) → PFunctor.M (last P) := PFunctor.M.children x
a✝ : (last P).A
f✝ : PFunctor.B (last P) a✝ → PFunctor.M (last P)
⊢ PFunctor.M.dest x = { fst := a, snd := f }
[PROOFSTEP]
simp [PFunctor.M.dest_mk, PFunctor.M.children_mk]
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
x : PFunctor.M (last P)
i : Fin2 n
inst✝ : Inhabited (B (drop P) (PFunctor.M.head x) i)
a : (last P).A := PFunctor.M.head x
f : PFunctor.B (last P) (PFunctor.M.head x) → PFunctor.M (last P) := PFunctor.M.children x
a✝ : (last P).A
f✝ : PFunctor.B (last P) a✝ → PFunctor.M (last P)
⊢ PFunctor.M.dest x = { fst := PFunctor.M.head x, snd := PFunctor.M.children x }
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
⊢ MvFunctor (M P)
[PROOFSTEP]
delta M
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
⊢ MvFunctor fun α => Obj (mp P) α
[PROOFSTEP]
infer_instance
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g₀ : β → P.A
g₁ : (b : β) → B (drop P) (g₀ b) ⟹ α
g₂ : (b : β) → PFunctor.B (last P) (g₀ b) → β
x✝ : PFunctor.M (last P)
b : β
x : PFunctor.M (last P)
i : Fin2 n
a : P.A
f : PFunctor.B (last P) a → PFunctor.M (last P)
h' : PFunctor.M.dest x = { fst := a, snd := f }
c : B (drop P) a i
h : x = corecShape P g₀ g₂ b
⊢ a = g₀ b
[PROOFSTEP]
rw [h, M.corecShape, PFunctor.M.dest_corec] at h' 
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g₀ : β → P.A
g₁ : (b : β) → B (drop P) (g₀ b) ⟹ α
g₂ : (b : β) → PFunctor.B (last P) (g₀ b) → β
x✝ : PFunctor.M (last P)
b : β
x : PFunctor.M (last P)
i : Fin2 n
a : P.A
f : PFunctor.B (last P) a → PFunctor.M (last P)
h' : (PFunctor.M.corec fun b => { fst := g₀ b, snd := g₂ b }) <$> { fst := g₀ b, snd := g₂ b } = { fst := a, snd := f }
c : B (drop P) a i
h : x = corecShape P g₀ g₂ b
⊢ a = g₀ b
[PROOFSTEP]
cases h'
[GOAL]
case refl
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g₀ : β → P.A
g₁ : (b : β) → B (drop P) (g₀ b) ⟹ α
g₂ : (b : β) → PFunctor.B (last P) (g₀ b) → β
x✝ : PFunctor.M (last P)
b : β
x : PFunctor.M (last P)
i : Fin2 n
h : x = corecShape P g₀ g₂ b
c : B (drop P) (g₀ b) i
⊢ g₀ b = g₀ b
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g₀ : β → P.A
g₁ : (b : β) → B (drop P) (g₀ b) ⟹ α
g₂ : (b : β) → PFunctor.B (last P) (g₀ b) → β
x✝ : PFunctor.M (last P)
b : β
x : PFunctor.M (last P)
i : Fin2 n
a : P.A
f : PFunctor.B (last P) a → PFunctor.M (last P)
h' : PFunctor.M.dest x = { fst := a, snd := f }
j : PFunctor.B (last P) a
c : Path P (f j) i
h : x = corecShape P g₀ g₂ b
⊢ a = g₀ b
[PROOFSTEP]
rw [h, M.corecShape, PFunctor.M.dest_corec] at h' 
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g₀ : β → P.A
g₁ : (b : β) → B (drop P) (g₀ b) ⟹ α
g₂ : (b : β) → PFunctor.B (last P) (g₀ b) → β
x✝ : PFunctor.M (last P)
b : β
x : PFunctor.M (last P)
i : Fin2 n
a : P.A
f : PFunctor.B (last P) a → PFunctor.M (last P)
h' : (PFunctor.M.corec fun b => { fst := g₀ b, snd := g₂ b }) <$> { fst := g₀ b, snd := g₂ b } = { fst := a, snd := f }
j : PFunctor.B (last P) a
c : Path P (f j) i
h : x = corecShape P g₀ g₂ b
⊢ a = g₀ b
[PROOFSTEP]
cases h'
[GOAL]
case refl
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g₀ : β → P.A
g₁ : (b : β) → B (drop P) (g₀ b) ⟹ α
g₂ : (b : β) → PFunctor.B (last P) (g₀ b) → β
x✝ : PFunctor.M (last P)
b : β
x : PFunctor.M (last P)
i : Fin2 n
h : x = corecShape P g₀ g₂ b
j : PFunctor.B (last P) (g₀ b)
c : Path P (((PFunctor.M.corec fun b => { fst := g₀ b, snd := g₂ b }) ∘ g₂ b) j) i
⊢ g₀ b = g₀ b
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g₀ : β → P.A
g₁ : (b : β) → B (drop P) (g₀ b) ⟹ α
g₂ : (b : β) → PFunctor.B (last P) (g₀ b) → β
x✝ : PFunctor.M (last P)
b : β
x : PFunctor.M (last P)
i : Fin2 n
a : P.A
f : PFunctor.B (last P) a → PFunctor.M (last P)
h' : PFunctor.M.dest x = { fst := a, snd := f }
j : PFunctor.B (last P) a
c : Path P (f j) i
h : x = corecShape P g₀ g₂ b
h₀ : a = g₀ b
⊢ f j = corecShape P g₀ g₂ (g₂ b (castLastB P h₀ j))
[PROOFSTEP]
rw [h, M.corecShape, PFunctor.M.dest_corec] at h' 
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g₀ : β → P.A
g₁ : (b : β) → B (drop P) (g₀ b) ⟹ α
g₂ : (b : β) → PFunctor.B (last P) (g₀ b) → β
x✝ : PFunctor.M (last P)
b : β
x : PFunctor.M (last P)
i : Fin2 n
a : P.A
f : PFunctor.B (last P) a → PFunctor.M (last P)
h' : (PFunctor.M.corec fun b => { fst := g₀ b, snd := g₂ b }) <$> { fst := g₀ b, snd := g₂ b } = { fst := a, snd := f }
j : PFunctor.B (last P) a
c : Path P (f j) i
h : x = corecShape P g₀ g₂ b
h₀ : a = g₀ b
⊢ f j = corecShape P g₀ g₂ (g₂ b (castLastB P h₀ j))
[PROOFSTEP]
cases h'
[GOAL]
case refl
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g₀ : β → P.A
g₁ : (b : β) → B (drop P) (g₀ b) ⟹ α
g₂ : (b : β) → PFunctor.B (last P) (g₀ b) → β
x✝ : PFunctor.M (last P)
b : β
x : PFunctor.M (last P)
i : Fin2 n
h : x = corecShape P g₀ g₂ b
j : PFunctor.B (last P) (g₀ b)
h₀ : g₀ b = g₀ b
c : Path P (((PFunctor.M.corec fun b => { fst := g₀ b, snd := g₂ b }) ∘ g₂ b) j) i
⊢ ((PFunctor.M.corec fun b => { fst := g₀ b, snd := g₂ b }) ∘ g₂ b) j = corecShape P g₀ g₂ (g₂ b (castLastB P h₀ j))
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
x : PFunctor.M (last P)
a₁ : P.A
f₁ : PFunctor.B (last P) a₁ → PFunctor.M (last P)
h₁ : PFunctor.M.dest x = { fst := a₁, snd := f₁ }
a₂ : P.A
f₂ : PFunctor.B (last P) a₂ → PFunctor.M (last P)
h₂ : PFunctor.M.dest x = { fst := a₂, snd := f₂ }
f' : Path P x ⟹ α
⊢ dest' P h₁ f' = dest' P h₂ f'
[PROOFSTEP]
cases h₁.symm.trans h₂
[GOAL]
case refl
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
x : PFunctor.M (last P)
a₁ : P.A
f₁ : PFunctor.B (last P) a₁ → PFunctor.M (last P)
h₁ : PFunctor.M.dest x = { fst := a₁, snd := f₁ }
f' : Path P x ⟹ α
h₂ : PFunctor.M.dest x = { fst := a₁, snd := f₁ }
⊢ dest' P h₁ f' = dest' P h₂ f'
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g : β → Obj P (α ::: β)
x : β
⊢ dest P (corec P g x) = (TypeVec.id ::: corec P g) <$$> g x
[PROOFSTEP]
trans
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g : β → Obj P (α ::: β)
x : β
⊢ dest P (corec P g x) = ?m.39771
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g : β → Obj P (α ::: β)
x : β
⊢ ?m.39771 = (TypeVec.id ::: corec P g) <$$> g x
n : ℕ P : MvPFunctor (n + 1) α : TypeVec n β : Type u g : β → Obj P (α ::: β) x : β ⊢ Obj P (α ::: M P α)
[PROOFSTEP]
apply M.dest_corec'
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g : β → Obj P (α ::: β)
x : β
⊢ { fst := (g x).fst,
      snd :=
        splitFun (dropFun (g x).snd)
          ((corec' P (fun b => (g b).fst) (fun b => dropFun (g b).snd) fun b => lastFun (g b).snd) ∘
            lastFun (g x).snd) } =
    (TypeVec.id ::: corec P g) <$$> g x
[PROOFSTEP]
cases' g x with a f
[GOAL]
case mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g : β → Obj P (α ::: β)
x : β
a : P.A
f : B P a ⟹ α ::: β
⊢ { fst := { fst := a, snd := f }.fst,
      snd :=
        splitFun (dropFun { fst := a, snd := f }.snd)
          ((corec' P (fun b => (g b).fst) (fun b => dropFun (g b).snd) fun b => lastFun (g b).snd) ∘
            lastFun { fst := a, snd := f }.snd) } =
    (TypeVec.id ::: corec P g) <$$> { fst := a, snd := f }
[PROOFSTEP]
dsimp
[GOAL]
case mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g : β → Obj P (α ::: β)
x : β
a : P.A
f : B P a ⟹ α ::: β
⊢ { fst := a,
      snd :=
        splitFun (dropFun f)
          ((corec' P (fun b => (g b).fst) (fun b => dropFun (g b).snd) fun b => lastFun (g b).snd) ∘ lastFun f) } =
    (TypeVec.id ::: corec P g) <$$> { fst := a, snd := f }
[PROOFSTEP]
rw [MvPFunctor.map_eq]
[GOAL]
case mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g : β → Obj P (α ::: β)
x : β
a : P.A
f : B P a ⟹ α ::: β
⊢ { fst := a,
      snd :=
        splitFun (dropFun f)
          ((corec' P (fun b => (g b).fst) (fun b => dropFun (g b).snd) fun b => lastFun (g b).snd) ∘ lastFun f) } =
    { fst := a, snd := (TypeVec.id ::: corec P g) ⊚ f }
[PROOFSTEP]
congr
[GOAL]
case mk.e_snd
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g : β → Obj P (α ::: β)
x : β
a : P.A
f : B P a ⟹ α ::: β
⊢ splitFun (dropFun f)
      ((corec' P (fun b => (g b).fst) (fun b => dropFun (g b).snd) fun b => lastFun (g b).snd) ∘ lastFun f) =
    (TypeVec.id ::: corec P g) ⊚ f
[PROOFSTEP]
conv =>
  rhs
  rw [← split_dropFun_lastFun f, appendFun_comp_splitFun]
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g : β → Obj P (α ::: β)
x : β
a : P.A
f : B P a ⟹ α ::: β
| splitFun (dropFun f)
      ((corec' P (fun b => (g b).fst) (fun b => dropFun (g b).snd) fun b => lastFun (g b).snd) ∘ lastFun f) =
    (TypeVec.id ::: corec P g) ⊚ f
[PROOFSTEP]
  rhs
  rw [← split_dropFun_lastFun f, appendFun_comp_splitFun]
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g : β → Obj P (α ::: β)
x : β
a : P.A
f : B P a ⟹ α ::: β
| splitFun (dropFun f)
      ((corec' P (fun b => (g b).fst) (fun b => dropFun (g b).snd) fun b => lastFun (g b).snd) ∘ lastFun f) =
    (TypeVec.id ::: corec P g) ⊚ f
[PROOFSTEP]
  rhs
  rw [← split_dropFun_lastFun f, appendFun_comp_splitFun]
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g : β → Obj P (α ::: β)
x : β
a : P.A
f : B P a ⟹ α ::: β
| splitFun (dropFun f)
      ((corec' P (fun b => (g b).fst) (fun b => dropFun (g b).snd) fun b => lastFun (g b).snd) ∘ lastFun f) =
    (TypeVec.id ::: corec P g) ⊚ f
[PROOFSTEP]
rhs
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g : β → Obj P (α ::: β)
x : β
a : P.A
f : B P a ⟹ α ::: β
| (TypeVec.id ::: corec P g) ⊚ f
[PROOFSTEP]
rw [← split_dropFun_lastFun f, appendFun_comp_splitFun]
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
a₁ : (mp P).A
f₁ : B (mp P) a₁ ⟹ α
a' : P.A
f' : TypeVec.drop (B P a') ⟹ α
f₁' : TypeVec.last (B P a') → M P α
e₁ : dest P { fst := a₁, snd := f₁ } = { fst := a', snd := splitFun f' f₁' }
⊢ ∃ g₁' e₁', f' = pathDestLeft P e₁' f₁ ∧ f₁' = fun x => { fst := g₁' x, snd := pathDestRight P e₁' f₁ x }
[PROOFSTEP]
generalize ef : @splitFun n _ (append1 α (M P α)) f' f₁' = ff at e₁ 
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
a₁ : (mp P).A
f₁ : B (mp P) a₁ ⟹ α
a' : P.A
f' : TypeVec.drop (B P a') ⟹ α
f₁' : TypeVec.last (B P a') → M P α
ff : B P a' ⟹ α ::: M P α
ef : splitFun f' f₁' = ff
e₁ : dest P { fst := a₁, snd := f₁ } = { fst := a', snd := ff }
⊢ ∃ g₁' e₁', f' = pathDestLeft P e₁' f₁ ∧ f₁' = fun x => { fst := g₁' x, snd := pathDestRight P e₁' f₁ x }
[PROOFSTEP]
let he₁' := PFunctor.M.dest a₁
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
a₁ : (mp P).A
f₁ : B (mp P) a₁ ⟹ α
a' : P.A
f' : TypeVec.drop (B P a') ⟹ α
f₁' : TypeVec.last (B P a') → M P α
ff : B P a' ⟹ α ::: M P α
ef : splitFun f' f₁' = ff
e₁ : dest P { fst := a₁, snd := f₁ } = { fst := a', snd := ff }
he₁' : PFunctor.Obj (last P) (PFunctor.M (last P)) := PFunctor.M.dest a₁
⊢ ∃ g₁' e₁', f' = pathDestLeft P e₁' f₁ ∧ f₁' = fun x => { fst := g₁' x, snd := pathDestRight P e₁' f₁ x }
[PROOFSTEP]
rcases e₁' : he₁' with ⟨a₁', g₁'⟩
[GOAL]
case mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
a₁ : (mp P).A
f₁ : B (mp P) a₁ ⟹ α
a' : P.A
f' : TypeVec.drop (B P a') ⟹ α
f₁' : TypeVec.last (B P a') → M P α
ff : B P a' ⟹ α ::: M P α
ef : splitFun f' f₁' = ff
e₁ : dest P { fst := a₁, snd := f₁ } = { fst := a', snd := ff }
he₁' : PFunctor.Obj (last P) (PFunctor.M (last P)) := PFunctor.M.dest a₁
a₁' : (last P).A
g₁' : PFunctor.B (last P) a₁' → PFunctor.M (last P)
e₁' : he₁' = { fst := a₁', snd := g₁' }
⊢ ∃ g₁' e₁', f' = pathDestLeft P e₁' f₁ ∧ f₁' = fun x => { fst := g₁' x, snd := pathDestRight P e₁' f₁ x }
[PROOFSTEP]
rw [M.dest_eq_dest' _ e₁'] at e₁ 
[GOAL]
case mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
a₁ : (mp P).A
f₁ : B (mp P) a₁ ⟹ α
a' : P.A
f' : TypeVec.drop (B P a') ⟹ α
f₁' : TypeVec.last (B P a') → M P α
ff : B P a' ⟹ α ::: M P α
ef : splitFun f' f₁' = ff
he₁' : PFunctor.Obj (last P) (PFunctor.M (last P)) := PFunctor.M.dest a₁
a₁' : (last P).A
g₁' : PFunctor.B (last P) a₁' → PFunctor.M (last P)
e₁' : he₁' = { fst := a₁', snd := g₁' }
e₁ : dest' P e₁' f₁ = { fst := a', snd := ff }
⊢ ∃ g₁' e₁', f' = pathDestLeft P e₁' f₁ ∧ f₁' = fun x => { fst := g₁' x, snd := pathDestRight P e₁' f₁ x }
[PROOFSTEP]
cases e₁
[GOAL]
case mk.refl
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
a₁ : (mp P).A
f₁ : B (mp P) a₁ ⟹ α
a' : P.A
f' : TypeVec.drop (B P a') ⟹ α
f₁' : TypeVec.last (B P a') → M P α
he₁' : PFunctor.Obj (last P) (PFunctor.M (last P)) := PFunctor.M.dest a₁
g₁' : PFunctor.B (last P) a' → PFunctor.M (last P)
e₁' : he₁' = { fst := a', snd := g₁' }
ef : splitFun f' f₁' = splitFun (pathDestLeft P e₁' f₁) fun x => { fst := g₁' x, snd := pathDestRight P e₁' f₁ x }
⊢ ∃ g₁' e₁', f' = pathDestLeft P e₁' f₁ ∧ f₁' = fun x => { fst := g₁' x, snd := pathDestRight P e₁' f₁ x }
[PROOFSTEP]
exact ⟨_, e₁', splitFun_inj ef⟩
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
x y : M P α
r : R x y
⊢ x = y
[PROOFSTEP]
cases' x with a₁ f₁
[GOAL]
case mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
y : M P α
a₁ : (mp P).A
f₁ : B (mp P) a₁ ⟹ α
r : R { fst := a₁, snd := f₁ } y
⊢ { fst := a₁, snd := f₁ } = y
[PROOFSTEP]
cases' y with a₂ f₂
[GOAL]
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
a₁ : (mp P).A
f₁ : B (mp P) a₁ ⟹ α
a₂ : (mp P).A
f₂ : B (mp P) a₂ ⟹ α
r : R { fst := a₁, snd := f₁ } { fst := a₂, snd := f₂ }
⊢ { fst := a₁, snd := f₁ } = { fst := a₂, snd := f₂ }
[PROOFSTEP]
dsimp [mp] at *
[GOAL]
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
a₁ : (mp P).A
f₁ : B (mp P) a₁ ⟹ α
a₂ : (mp P).A
f₂ : B (mp P) a₂ ⟹ α
r : R { fst := a₁, snd := f₁ } { fst := a₂, snd := f₂ }
⊢ { fst := a₁, snd := f₁ } = { fst := a₂, snd := f₂ }
[PROOFSTEP]
have : a₁ = a₂ :=
  by
  refine' PFunctor.M.bisim (fun a₁ a₂ => ∃ x y, R x y ∧ x.1 = a₁ ∧ y.1 = a₂) _ _ _ ⟨⟨a₁, f₁⟩, ⟨a₂, f₂⟩, r, rfl, rfl⟩
  rintro _ _ ⟨⟨a₁, f₁⟩, ⟨a₂, f₂⟩, r, rfl, rfl⟩
  rcases h _ _ r with ⟨a', f', f₁', f₂', e₁, e₂, h'⟩
  rcases M.bisim_lemma P e₁ with ⟨g₁', e₁', rfl, rfl⟩
  rcases M.bisim_lemma P e₂ with ⟨g₂', e₂', _, rfl⟩
  rw [e₁', e₂']
  exact ⟨_, _, _, rfl, rfl, fun b => ⟨_, _, h' b, rfl, rfl⟩⟩
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
a₁ : (mp P).A
f₁ : B (mp P) a₁ ⟹ α
a₂ : (mp P).A
f₂ : B (mp P) a₂ ⟹ α
r : R { fst := a₁, snd := f₁ } { fst := a₂, snd := f₂ }
⊢ a₁ = a₂
[PROOFSTEP]
refine' PFunctor.M.bisim (fun a₁ a₂ => ∃ x y, R x y ∧ x.1 = a₁ ∧ y.1 = a₂) _ _ _ ⟨⟨a₁, f₁⟩, ⟨a₂, f₂⟩, r, rfl, rfl⟩
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
a₁ : (mp P).A
f₁ : B (mp P) a₁ ⟹ α
a₂ : (mp P).A
f₂ : B (mp P) a₂ ⟹ α
r : R { fst := a₁, snd := f₁ } { fst := a₂, snd := f₂ }
⊢ ∀ (x y : PFunctor.M (last P)),
    (fun a₁ a₂ => ∃ x y, R x y ∧ x.fst = a₁ ∧ y.fst = a₂) x y →
      ∃ a f f',
        PFunctor.M.dest x = { fst := a, snd := f } ∧
          PFunctor.M.dest y = { fst := a, snd := f' } ∧
            ∀ (i : PFunctor.B (last P) a), (fun a₁ a₂ => ∃ x y, R x y ∧ x.fst = a₁ ∧ y.fst = a₂) (f i) (f' i)
[PROOFSTEP]
rintro _ _ ⟨⟨a₁, f₁⟩, ⟨a₂, f₂⟩, r, rfl, rfl⟩
[GOAL]
case intro.mk.intro.mk.intro.intro
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
a₁✝ : (mp P).A
f₁✝ : B (mp P) a₁✝ ⟹ α
a₂✝ : (mp P).A
f₂✝ : B (mp P) a₂✝ ⟹ α
r✝ : R { fst := a₁✝, snd := f₁✝ } { fst := a₂✝, snd := f₂✝ }
a₁ : (mp P).A
f₁ : B (mp P) a₁ ⟹ α
a₂ : (mp P).A
f₂ : B (mp P) a₂ ⟹ α
r : R { fst := a₁, snd := f₁ } { fst := a₂, snd := f₂ }
⊢ ∃ a f f',
    PFunctor.M.dest { fst := a₁, snd := f₁ }.fst = { fst := a, snd := f } ∧
      PFunctor.M.dest { fst := a₂, snd := f₂ }.fst = { fst := a, snd := f' } ∧
        ∀ (i : PFunctor.B (last P) a), (fun a₁ a₂ => ∃ x y, R x y ∧ x.fst = a₁ ∧ y.fst = a₂) (f i) (f' i)
[PROOFSTEP]
rcases h _ _ r with ⟨a', f', f₁', f₂', e₁, e₂, h'⟩
[GOAL]
case intro.mk.intro.mk.intro.intro.intro.intro.intro.intro.intro.intro
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
a₁✝ : (mp P).A
f₁✝ : B (mp P) a₁✝ ⟹ α
a₂✝ : (mp P).A
f₂✝ : B (mp P) a₂✝ ⟹ α
r✝ : R { fst := a₁✝, snd := f₁✝ } { fst := a₂✝, snd := f₂✝ }
a₁ : (mp P).A
f₁ : B (mp P) a₁ ⟹ α
a₂ : (mp P).A
f₂ : B (mp P) a₂ ⟹ α
r : R { fst := a₁, snd := f₁ } { fst := a₂, snd := f₂ }
a' : P.A
f' : TypeVec.drop (B P a') ⟹ TypeVec.drop (α ::: M P α)
f₁' f₂' : TypeVec.last (B P a') → TypeVec.last (α ::: M P α)
e₁ : dest P { fst := a₁, snd := f₁ } = { fst := a', snd := splitFun f' f₁' }
e₂ : dest P { fst := a₂, snd := f₂ } = { fst := a', snd := splitFun f' f₂' }
h' : ∀ (i : TypeVec.last (B P a')), R (f₁' i) (f₂' i)
⊢ ∃ a f f',
    PFunctor.M.dest { fst := a₁, snd := f₁ }.fst = { fst := a, snd := f } ∧
      PFunctor.M.dest { fst := a₂, snd := f₂ }.fst = { fst := a, snd := f' } ∧
        ∀ (i : PFunctor.B (last P) a), (fun a₁ a₂ => ∃ x y, R x y ∧ x.fst = a₁ ∧ y.fst = a₂) (f i) (f' i)
[PROOFSTEP]
rcases M.bisim_lemma P e₁ with ⟨g₁', e₁', rfl, rfl⟩
[GOAL]
case intro.mk.intro.mk.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
a₁✝ : (mp P).A
f₁✝ : B (mp P) a₁✝ ⟹ α
a₂✝ : (mp P).A
f₂✝ : B (mp P) a₂✝ ⟹ α
r✝ : R { fst := a₁✝, snd := f₁✝ } { fst := a₂✝, snd := f₂✝ }
a₁ : (mp P).A
f₁ : B (mp P) a₁ ⟹ α
a₂ : (mp P).A
f₂ : B (mp P) a₂ ⟹ α
r : R { fst := a₁, snd := f₁ } { fst := a₂, snd := f₂ }
a' : P.A
f₂' : TypeVec.last (B P a') → TypeVec.last (α ::: M P α)
g₁' : PFunctor.B (last P) a' → PFunctor.M (last P)
e₁' : PFunctor.M.dest a₁ = { fst := a', snd := g₁' }
e₂ : dest P { fst := a₂, snd := f₂ } = { fst := a', snd := splitFun (pathDestLeft P e₁' f₁) f₂' }
h' : ∀ (i : TypeVec.last (B P a')), R ((fun x => { fst := g₁' x, snd := pathDestRight P e₁' f₁ x }) i) (f₂' i)
e₁ :
  dest P { fst := a₁, snd := f₁ } =
    { fst := a', snd := splitFun (pathDestLeft P e₁' f₁) fun x => { fst := g₁' x, snd := pathDestRight P e₁' f₁ x } }
⊢ ∃ a f f',
    PFunctor.M.dest { fst := a₁, snd := f₁ }.fst = { fst := a, snd := f } ∧
      PFunctor.M.dest { fst := a₂, snd := f₂ }.fst = { fst := a, snd := f' } ∧
        ∀ (i : PFunctor.B (last P) a), (fun a₁ a₂ => ∃ x y, R x y ∧ x.fst = a₁ ∧ y.fst = a₂) (f i) (f' i)
[PROOFSTEP]
rcases M.bisim_lemma P e₂ with ⟨g₂', e₂', _, rfl⟩
[GOAL]
case intro.mk.intro.mk.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
a₁✝ : (mp P).A
f₁✝ : B (mp P) a₁✝ ⟹ α
a₂✝ : (mp P).A
f₂✝ : B (mp P) a₂✝ ⟹ α
r✝ : R { fst := a₁✝, snd := f₁✝ } { fst := a₂✝, snd := f₂✝ }
a₁ : (mp P).A
f₁ : B (mp P) a₁ ⟹ α
a₂ : (mp P).A
f₂ : B (mp P) a₂ ⟹ α
r : R { fst := a₁, snd := f₁ } { fst := a₂, snd := f₂ }
a' : P.A
g₁' : PFunctor.B (last P) a' → PFunctor.M (last P)
e₁' : PFunctor.M.dest a₁ = { fst := a', snd := g₁' }
e₁ :
  dest P { fst := a₁, snd := f₁ } =
    { fst := a', snd := splitFun (pathDestLeft P e₁' f₁) fun x => { fst := g₁' x, snd := pathDestRight P e₁' f₁ x } }
g₂' : PFunctor.B (last P) a' → PFunctor.M (last P)
e₂' : PFunctor.M.dest a₂ = { fst := a', snd := g₂' }
left✝ : pathDestLeft P e₁' f₁ = pathDestLeft P e₂' f₂
e₂ :
  dest P { fst := a₂, snd := f₂ } =
    { fst := a', snd := splitFun (pathDestLeft P e₁' f₁) fun x => { fst := g₂' x, snd := pathDestRight P e₂' f₂ x } }
h' :
  ∀ (i : TypeVec.last (B P a')),
    R ((fun x => { fst := g₁' x, snd := pathDestRight P e₁' f₁ x }) i)
      ((fun x => { fst := g₂' x, snd := pathDestRight P e₂' f₂ x }) i)
⊢ ∃ a f f',
    PFunctor.M.dest { fst := a₁, snd := f₁ }.fst = { fst := a, snd := f } ∧
      PFunctor.M.dest { fst := a₂, snd := f₂ }.fst = { fst := a, snd := f' } ∧
        ∀ (i : PFunctor.B (last P) a), (fun a₁ a₂ => ∃ x y, R x y ∧ x.fst = a₁ ∧ y.fst = a₂) (f i) (f' i)
[PROOFSTEP]
rw [e₁', e₂']
[GOAL]
case intro.mk.intro.mk.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
a₁✝ : (mp P).A
f₁✝ : B (mp P) a₁✝ ⟹ α
a₂✝ : (mp P).A
f₂✝ : B (mp P) a₂✝ ⟹ α
r✝ : R { fst := a₁✝, snd := f₁✝ } { fst := a₂✝, snd := f₂✝ }
a₁ : (mp P).A
f₁ : B (mp P) a₁ ⟹ α
a₂ : (mp P).A
f₂ : B (mp P) a₂ ⟹ α
r : R { fst := a₁, snd := f₁ } { fst := a₂, snd := f₂ }
a' : P.A
g₁' : PFunctor.B (last P) a' → PFunctor.M (last P)
e₁' : PFunctor.M.dest a₁ = { fst := a', snd := g₁' }
e₁ :
  dest P { fst := a₁, snd := f₁ } =
    { fst := a', snd := splitFun (pathDestLeft P e₁' f₁) fun x => { fst := g₁' x, snd := pathDestRight P e₁' f₁ x } }
g₂' : PFunctor.B (last P) a' → PFunctor.M (last P)
e₂' : PFunctor.M.dest a₂ = { fst := a', snd := g₂' }
left✝ : pathDestLeft P e₁' f₁ = pathDestLeft P e₂' f₂
e₂ :
  dest P { fst := a₂, snd := f₂ } =
    { fst := a', snd := splitFun (pathDestLeft P e₁' f₁) fun x => { fst := g₂' x, snd := pathDestRight P e₂' f₂ x } }
h' :
  ∀ (i : TypeVec.last (B P a')),
    R ((fun x => { fst := g₁' x, snd := pathDestRight P e₁' f₁ x }) i)
      ((fun x => { fst := g₂' x, snd := pathDestRight P e₂' f₂ x }) i)
⊢ ∃ a f f',
    { fst := a', snd := g₁' } = { fst := a, snd := f } ∧
      { fst := a', snd := g₂' } = { fst := a, snd := f' } ∧
        ∀ (i : PFunctor.B (last P) a), (fun a₁ a₂ => ∃ x y, R x y ∧ x.fst = a₁ ∧ y.fst = a₂) (f i) (f' i)
[PROOFSTEP]
exact ⟨_, _, _, rfl, rfl, fun b => ⟨_, _, h' b, rfl, rfl⟩⟩
[GOAL]
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
a₁ : (mp P).A
f₁ : B (mp P) a₁ ⟹ α
a₂ : (mp P).A
f₂ : B (mp P) a₂ ⟹ α
r : R { fst := a₁, snd := f₁ } { fst := a₂, snd := f₂ }
this : a₁ = a₂
⊢ { fst := a₁, snd := f₁ } = { fst := a₂, snd := f₂ }
[PROOFSTEP]
subst this
[GOAL]
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
a₁ : (mp P).A
f₁ f₂ : B (mp P) a₁ ⟹ α
r : R { fst := a₁, snd := f₁ } { fst := a₁, snd := f₂ }
⊢ { fst := a₁, snd := f₁ } = { fst := a₁, snd := f₂ }
[PROOFSTEP]
congr with (i p)
[GOAL]
case mk.mk.e_snd.a.h
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
a₁ : (mp P).A
f₁ f₂ : B (mp P) a₁ ⟹ α
r : R { fst := a₁, snd := f₁ } { fst := a₁, snd := f₂ }
i : Fin2 n
p : B (mp P) a₁ i
⊢ f₁ i p = f₂ i p
[PROOFSTEP]
induction' p with x a f h' i c x a f h' i c p IH
[GOAL]
case mk.mk.e_snd.a.h.root
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
a₁ : (mp P).A
f₁✝ f₂✝ : B (mp P) a₁ ⟹ α
r✝ : R { fst := a₁, snd := f₁✝ } { fst := a₁, snd := f₂✝ }
i✝ : Fin2 n
x : PFunctor.M (last P)
a : P.A
f : PFunctor.B (last P) a → PFunctor.M (last P)
h' : PFunctor.M.dest x = { fst := a, snd := f }
i : Fin2 n
c : B (drop P) a i
f₁ f₂ : B (mp P) x ⟹ α
r : R { fst := x, snd := f₁ } { fst := x, snd := f₂ }
⊢ f₁ i (Path.root x a f h' i c) = f₂ i (Path.root x a f h' i c)
[PROOFSTEP]
try
  rcases h _ _ r with ⟨a', f', f₁', f₂', e₁, e₂, h''⟩
  rcases M.bisim_lemma P e₁ with ⟨g₁', e₁', rfl, rfl⟩
  rcases M.bisim_lemma P e₂ with ⟨g₂', e₂', e₃, rfl⟩
  cases h'.symm.trans e₁'
  cases h'.symm.trans e₂'
[GOAL]
case mk.mk.e_snd.a.h.root
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
a₁ : (mp P).A
f₁✝ f₂✝ : B (mp P) a₁ ⟹ α
r✝ : R { fst := a₁, snd := f₁✝ } { fst := a₁, snd := f₂✝ }
i✝ : Fin2 n
x : PFunctor.M (last P)
a : P.A
f : PFunctor.B (last P) a → PFunctor.M (last P)
h' : PFunctor.M.dest x = { fst := a, snd := f }
i : Fin2 n
c : B (drop P) a i
f₁ f₂ : B (mp P) x ⟹ α
r : R { fst := x, snd := f₁ } { fst := x, snd := f₂ }
⊢ f₁ i (Path.root x a f h' i c) = f₂ i (Path.root x a f h' i c)
[PROOFSTEP]
rcases h _ _ r with ⟨a', f', f₁', f₂', e₁, e₂, h''⟩
[GOAL]
case mk.mk.e_snd.a.h.root.intro.intro.intro.intro.intro.intro
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
a₁ : (mp P).A
f₁✝ f₂✝ : B (mp P) a₁ ⟹ α
r✝ : R { fst := a₁, snd := f₁✝ } { fst := a₁, snd := f₂✝ }
i✝ : Fin2 n
x : PFunctor.M (last P)
a : P.A
f : PFunctor.B (last P) a → PFunctor.M (last P)
h' : PFunctor.M.dest x = { fst := a, snd := f }
i : Fin2 n
c : B (drop P) a i
f₁ f₂ : B (mp P) x ⟹ α
r : R { fst := x, snd := f₁ } { fst := x, snd := f₂ }
a' : P.A
f' : TypeVec.drop (B P a') ⟹ TypeVec.drop (α ::: M P α)
f₁' f₂' : TypeVec.last (B P a') → TypeVec.last (α ::: M P α)
e₁ : dest P { fst := x, snd := f₁ } = { fst := a', snd := splitFun f' f₁' }
e₂ : dest P { fst := x, snd := f₂ } = { fst := a', snd := splitFun f' f₂' }
h'' : ∀ (i : TypeVec.last (B P a')), R (f₁' i) (f₂' i)
⊢ f₁ i (Path.root x a f h' i c) = f₂ i (Path.root x a f h' i c)
[PROOFSTEP]
rcases M.bisim_lemma P e₁ with ⟨g₁', e₁', rfl, rfl⟩
[GOAL]
case mk.mk.e_snd.a.h.root.intro.intro.intro.intro.intro.intro.intro.intro.intro
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
a₁ : (mp P).A
f₁✝ f₂✝ : B (mp P) a₁ ⟹ α
r✝ : R { fst := a₁, snd := f₁✝ } { fst := a₁, snd := f₂✝ }
i✝ : Fin2 n
x : PFunctor.M (last P)
a : P.A
f : PFunctor.B (last P) a → PFunctor.M (last P)
h' : PFunctor.M.dest x = { fst := a, snd := f }
i : Fin2 n
c : B (drop P) a i
f₁ f₂ : B (mp P) x ⟹ α
r : R { fst := x, snd := f₁ } { fst := x, snd := f₂ }
a' : P.A
f₂' : TypeVec.last (B P a') → TypeVec.last (α ::: M P α)
g₁' : PFunctor.B (last P) a' → PFunctor.M (last P)
e₁' : PFunctor.M.dest x = { fst := a', snd := g₁' }
e₂ : dest P { fst := x, snd := f₂ } = { fst := a', snd := splitFun (pathDestLeft P e₁' f₁) f₂' }
h'' : ∀ (i : TypeVec.last (B P a')), R ((fun x_1 => { fst := g₁' x_1, snd := pathDestRight P e₁' f₁ x_1 }) i) (f₂' i)
e₁ :
  dest P { fst := x, snd := f₁ } =
    { fst := a',
      snd := splitFun (pathDestLeft P e₁' f₁) fun x_1 => { fst := g₁' x_1, snd := pathDestRight P e₁' f₁ x_1 } }
⊢ f₁ i (Path.root x a f h' i c) = f₂ i (Path.root x a f h' i c)
[PROOFSTEP]
rcases M.bisim_lemma P e₂ with ⟨g₂', e₂', e₃, rfl⟩
[GOAL]
case mk.mk.e_snd.a.h.root.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
a₁ : (mp P).A
f₁✝ f₂✝ : B (mp P) a₁ ⟹ α
r✝ : R { fst := a₁, snd := f₁✝ } { fst := a₁, snd := f₂✝ }
i✝ : Fin2 n
x : PFunctor.M (last P)
a : P.A
f : PFunctor.B (last P) a → PFunctor.M (last P)
h' : PFunctor.M.dest x = { fst := a, snd := f }
i : Fin2 n
c : B (drop P) a i
f₁ f₂ : B (mp P) x ⟹ α
r : R { fst := x, snd := f₁ } { fst := x, snd := f₂ }
a' : P.A
g₁' : PFunctor.B (last P) a' → PFunctor.M (last P)
e₁' : PFunctor.M.dest x = { fst := a', snd := g₁' }
e₁ :
  dest P { fst := x, snd := f₁ } =
    { fst := a',
      snd := splitFun (pathDestLeft P e₁' f₁) fun x_1 => { fst := g₁' x_1, snd := pathDestRight P e₁' f₁ x_1 } }
g₂' : PFunctor.B (last P) a' → PFunctor.M (last P)
e₂' : PFunctor.M.dest x = { fst := a', snd := g₂' }
e₃ : pathDestLeft P e₁' f₁ = pathDestLeft P e₂' f₂
e₂ :
  dest P { fst := x, snd := f₂ } =
    { fst := a',
      snd := splitFun (pathDestLeft P e₁' f₁) fun x_1 => { fst := g₂' x_1, snd := pathDestRight P e₂' f₂ x_1 } }
h'' :
  ∀ (i : TypeVec.last (B P a')),
    R ((fun x_1 => { fst := g₁' x_1, snd := pathDestRight P e₁' f₁ x_1 }) i)
      ((fun x_1 => { fst := g₂' x_1, snd := pathDestRight P e₂' f₂ x_1 }) i)
⊢ f₁ i (Path.root x a f h' i c) = f₂ i (Path.root x a f h' i c)
[PROOFSTEP]
cases h'.symm.trans e₁'
[GOAL]
case mk.mk.e_snd.a.h.root.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refl
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
a₁ : (mp P).A
f₁✝ f₂✝ : B (mp P) a₁ ⟹ α
r✝ : R { fst := a₁, snd := f₁✝ } { fst := a₁, snd := f₂✝ }
i✝ : Fin2 n
x : PFunctor.M (last P)
a : P.A
f : PFunctor.B (last P) a → PFunctor.M (last P)
h' : PFunctor.M.dest x = { fst := a, snd := f }
i : Fin2 n
c : B (drop P) a i
f₁ f₂ : B (mp P) x ⟹ α
r : R { fst := x, snd := f₁ } { fst := x, snd := f₂ }
g₂' : PFunctor.B (last P) a → PFunctor.M (last P)
e₂' : PFunctor.M.dest x = { fst := a, snd := g₂' }
e₁' : PFunctor.M.dest x = { fst := a, snd := f }
e₁ :
  dest P { fst := x, snd := f₁ } =
    { fst := a, snd := splitFun (pathDestLeft P e₁' f₁) fun x_1 => { fst := f x_1, snd := pathDestRight P e₁' f₁ x_1 } }
e₃ : pathDestLeft P e₁' f₁ = pathDestLeft P e₂' f₂
e₂ :
  dest P { fst := x, snd := f₂ } =
    { fst := a,
      snd := splitFun (pathDestLeft P e₁' f₁) fun x_1 => { fst := g₂' x_1, snd := pathDestRight P e₂' f₂ x_1 } }
h'' :
  ∀ (i : TypeVec.last (B P a)),
    R ((fun x_1 => { fst := f x_1, snd := pathDestRight P e₁' f₁ x_1 }) i)
      ((fun x_1 => { fst := g₂' x_1, snd := pathDestRight P e₂' f₂ x_1 }) i)
⊢ f₁ i (Path.root x a f h' i c) = f₂ i (Path.root x a f h' i c)
[PROOFSTEP]
cases h'.symm.trans e₂'
[GOAL]
case mk.mk.e_snd.a.h.child
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
a₁ : (mp P).A
f₁✝ f₂✝ : B (mp P) a₁ ⟹ α
r✝ : R { fst := a₁, snd := f₁✝ } { fst := a₁, snd := f₂✝ }
i✝ : Fin2 n
x : PFunctor.M (last P)
a : P.A
f : PFunctor.B (last P) a → PFunctor.M (last P)
h' : PFunctor.M.dest x = { fst := a, snd := f }
i : PFunctor.B (last P) a
c : Fin2 n
p : Path P (f i) c
IH : ∀ (f₁ f₂ : B (mp P) (f i) ⟹ α), R { fst := f i, snd := f₁ } { fst := f i, snd := f₂ } → f₁ c p = f₂ c p
f₁ f₂ : B (mp P) x ⟹ α
r : R { fst := x, snd := f₁ } { fst := x, snd := f₂ }
⊢ f₁ c (Path.child x a f h' i c p) = f₂ c (Path.child x a f h' i c p)
[PROOFSTEP]
try
  rcases h _ _ r with ⟨a', f', f₁', f₂', e₁, e₂, h''⟩
  rcases M.bisim_lemma P e₁ with ⟨g₁', e₁', rfl, rfl⟩
  rcases M.bisim_lemma P e₂ with ⟨g₂', e₂', e₃, rfl⟩
  cases h'.symm.trans e₁'
  cases h'.symm.trans e₂'
[GOAL]
case mk.mk.e_snd.a.h.child
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
a₁ : (mp P).A
f₁✝ f₂✝ : B (mp P) a₁ ⟹ α
r✝ : R { fst := a₁, snd := f₁✝ } { fst := a₁, snd := f₂✝ }
i✝ : Fin2 n
x : PFunctor.M (last P)
a : P.A
f : PFunctor.B (last P) a → PFunctor.M (last P)
h' : PFunctor.M.dest x = { fst := a, snd := f }
i : PFunctor.B (last P) a
c : Fin2 n
p : Path P (f i) c
IH : ∀ (f₁ f₂ : B (mp P) (f i) ⟹ α), R { fst := f i, snd := f₁ } { fst := f i, snd := f₂ } → f₁ c p = f₂ c p
f₁ f₂ : B (mp P) x ⟹ α
r : R { fst := x, snd := f₁ } { fst := x, snd := f₂ }
⊢ f₁ c (Path.child x a f h' i c p) = f₂ c (Path.child x a f h' i c p)
[PROOFSTEP]
rcases h _ _ r with ⟨a', f', f₁', f₂', e₁, e₂, h''⟩
[GOAL]
case mk.mk.e_snd.a.h.child.intro.intro.intro.intro.intro.intro
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
a₁ : (mp P).A
f₁✝ f₂✝ : B (mp P) a₁ ⟹ α
r✝ : R { fst := a₁, snd := f₁✝ } { fst := a₁, snd := f₂✝ }
i✝ : Fin2 n
x : PFunctor.M (last P)
a : P.A
f : PFunctor.B (last P) a → PFunctor.M (last P)
h' : PFunctor.M.dest x = { fst := a, snd := f }
i : PFunctor.B (last P) a
c : Fin2 n
p : Path P (f i) c
IH : ∀ (f₁ f₂ : B (mp P) (f i) ⟹ α), R { fst := f i, snd := f₁ } { fst := f i, snd := f₂ } → f₁ c p = f₂ c p
f₁ f₂ : B (mp P) x ⟹ α
r : R { fst := x, snd := f₁ } { fst := x, snd := f₂ }
a' : P.A
f' : TypeVec.drop (B P a') ⟹ TypeVec.drop (α ::: M P α)
f₁' f₂' : TypeVec.last (B P a') → TypeVec.last (α ::: M P α)
e₁ : dest P { fst := x, snd := f₁ } = { fst := a', snd := splitFun f' f₁' }
e₂ : dest P { fst := x, snd := f₂ } = { fst := a', snd := splitFun f' f₂' }
h'' : ∀ (i : TypeVec.last (B P a')), R (f₁' i) (f₂' i)
⊢ f₁ c (Path.child x a f h' i c p) = f₂ c (Path.child x a f h' i c p)
[PROOFSTEP]
rcases M.bisim_lemma P e₁ with ⟨g₁', e₁', rfl, rfl⟩
[GOAL]
case mk.mk.e_snd.a.h.child.intro.intro.intro.intro.intro.intro.intro.intro.intro
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
a₁ : (mp P).A
f₁✝ f₂✝ : B (mp P) a₁ ⟹ α
r✝ : R { fst := a₁, snd := f₁✝ } { fst := a₁, snd := f₂✝ }
i✝ : Fin2 n
x : PFunctor.M (last P)
a : P.A
f : PFunctor.B (last P) a → PFunctor.M (last P)
h' : PFunctor.M.dest x = { fst := a, snd := f }
i : PFunctor.B (last P) a
c : Fin2 n
p : Path P (f i) c
IH : ∀ (f₁ f₂ : B (mp P) (f i) ⟹ α), R { fst := f i, snd := f₁ } { fst := f i, snd := f₂ } → f₁ c p = f₂ c p
f₁ f₂ : B (mp P) x ⟹ α
r : R { fst := x, snd := f₁ } { fst := x, snd := f₂ }
a' : P.A
f₂' : TypeVec.last (B P a') → TypeVec.last (α ::: M P α)
g₁' : PFunctor.B (last P) a' → PFunctor.M (last P)
e₁' : PFunctor.M.dest x = { fst := a', snd := g₁' }
e₂ : dest P { fst := x, snd := f₂ } = { fst := a', snd := splitFun (pathDestLeft P e₁' f₁) f₂' }
h'' : ∀ (i : TypeVec.last (B P a')), R ((fun x_1 => { fst := g₁' x_1, snd := pathDestRight P e₁' f₁ x_1 }) i) (f₂' i)
e₁ :
  dest P { fst := x, snd := f₁ } =
    { fst := a',
      snd := splitFun (pathDestLeft P e₁' f₁) fun x_1 => { fst := g₁' x_1, snd := pathDestRight P e₁' f₁ x_1 } }
⊢ f₁ c (Path.child x a f h' i c p) = f₂ c (Path.child x a f h' i c p)
[PROOFSTEP]
rcases M.bisim_lemma P e₂ with ⟨g₂', e₂', e₃, rfl⟩
[GOAL]
case mk.mk.e_snd.a.h.child.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
a₁ : (mp P).A
f₁✝ f₂✝ : B (mp P) a₁ ⟹ α
r✝ : R { fst := a₁, snd := f₁✝ } { fst := a₁, snd := f₂✝ }
i✝ : Fin2 n
x : PFunctor.M (last P)
a : P.A
f : PFunctor.B (last P) a → PFunctor.M (last P)
h' : PFunctor.M.dest x = { fst := a, snd := f }
i : PFunctor.B (last P) a
c : Fin2 n
p : Path P (f i) c
IH : ∀ (f₁ f₂ : B (mp P) (f i) ⟹ α), R { fst := f i, snd := f₁ } { fst := f i, snd := f₂ } → f₁ c p = f₂ c p
f₁ f₂ : B (mp P) x ⟹ α
r : R { fst := x, snd := f₁ } { fst := x, snd := f₂ }
a' : P.A
g₁' : PFunctor.B (last P) a' → PFunctor.M (last P)
e₁' : PFunctor.M.dest x = { fst := a', snd := g₁' }
e₁ :
  dest P { fst := x, snd := f₁ } =
    { fst := a',
      snd := splitFun (pathDestLeft P e₁' f₁) fun x_1 => { fst := g₁' x_1, snd := pathDestRight P e₁' f₁ x_1 } }
g₂' : PFunctor.B (last P) a' → PFunctor.M (last P)
e₂' : PFunctor.M.dest x = { fst := a', snd := g₂' }
e₃ : pathDestLeft P e₁' f₁ = pathDestLeft P e₂' f₂
e₂ :
  dest P { fst := x, snd := f₂ } =
    { fst := a',
      snd := splitFun (pathDestLeft P e₁' f₁) fun x_1 => { fst := g₂' x_1, snd := pathDestRight P e₂' f₂ x_1 } }
h'' :
  ∀ (i : TypeVec.last (B P a')),
    R ((fun x_1 => { fst := g₁' x_1, snd := pathDestRight P e₁' f₁ x_1 }) i)
      ((fun x_1 => { fst := g₂' x_1, snd := pathDestRight P e₂' f₂ x_1 }) i)
⊢ f₁ c (Path.child x a f h' i c p) = f₂ c (Path.child x a f h' i c p)
[PROOFSTEP]
cases h'.symm.trans e₁'
[GOAL]
case mk.mk.e_snd.a.h.child.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refl
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
a₁ : (mp P).A
f₁✝ f₂✝ : B (mp P) a₁ ⟹ α
r✝ : R { fst := a₁, snd := f₁✝ } { fst := a₁, snd := f₂✝ }
i✝ : Fin2 n
x : PFunctor.M (last P)
a : P.A
f : PFunctor.B (last P) a → PFunctor.M (last P)
h' : PFunctor.M.dest x = { fst := a, snd := f }
i : PFunctor.B (last P) a
c : Fin2 n
p : Path P (f i) c
IH : ∀ (f₁ f₂ : B (mp P) (f i) ⟹ α), R { fst := f i, snd := f₁ } { fst := f i, snd := f₂ } → f₁ c p = f₂ c p
f₁ f₂ : B (mp P) x ⟹ α
r : R { fst := x, snd := f₁ } { fst := x, snd := f₂ }
g₂' : PFunctor.B (last P) a → PFunctor.M (last P)
e₂' : PFunctor.M.dest x = { fst := a, snd := g₂' }
e₁' : PFunctor.M.dest x = { fst := a, snd := f }
e₁ :
  dest P { fst := x, snd := f₁ } =
    { fst := a, snd := splitFun (pathDestLeft P e₁' f₁) fun x_1 => { fst := f x_1, snd := pathDestRight P e₁' f₁ x_1 } }
e₃ : pathDestLeft P e₁' f₁ = pathDestLeft P e₂' f₂
e₂ :
  dest P { fst := x, snd := f₂ } =
    { fst := a,
      snd := splitFun (pathDestLeft P e₁' f₁) fun x_1 => { fst := g₂' x_1, snd := pathDestRight P e₂' f₂ x_1 } }
h'' :
  ∀ (i : TypeVec.last (B P a)),
    R ((fun x_1 => { fst := f x_1, snd := pathDestRight P e₁' f₁ x_1 }) i)
      ((fun x_1 => { fst := g₂' x_1, snd := pathDestRight P e₂' f₂ x_1 }) i)
⊢ f₁ c (Path.child x a f h' i c p) = f₂ c (Path.child x a f h' i c p)
[PROOFSTEP]
cases h'.symm.trans e₂'
[GOAL]
case mk.mk.e_snd.a.h.root.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refl.refl
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
a₁ : (mp P).A
f₁✝ f₂✝ : B (mp P) a₁ ⟹ α
r✝ : R { fst := a₁, snd := f₁✝ } { fst := a₁, snd := f₂✝ }
i✝ : Fin2 n
x : PFunctor.M (last P)
a : P.A
f : PFunctor.B (last P) a → PFunctor.M (last P)
h' : PFunctor.M.dest x = { fst := a, snd := f }
i : Fin2 n
c : B (drop P) a i
f₁ f₂ : B (mp P) x ⟹ α
r : R { fst := x, snd := f₁ } { fst := x, snd := f₂ }
e₁' : PFunctor.M.dest x = { fst := a, snd := f }
e₁ :
  dest P { fst := x, snd := f₁ } =
    { fst := a, snd := splitFun (pathDestLeft P e₁' f₁) fun x_1 => { fst := f x_1, snd := pathDestRight P e₁' f₁ x_1 } }
e₂' : PFunctor.M.dest x = { fst := a, snd := f }
e₃ : pathDestLeft P e₁' f₁ = pathDestLeft P e₂' f₂
e₂ :
  dest P { fst := x, snd := f₂ } =
    { fst := a, snd := splitFun (pathDestLeft P e₁' f₁) fun x_1 => { fst := f x_1, snd := pathDestRight P e₂' f₂ x_1 } }
h'' :
  ∀ (i : TypeVec.last (B P a)),
    R ((fun x_1 => { fst := f x_1, snd := pathDestRight P e₁' f₁ x_1 }) i)
      ((fun x_1 => { fst := f x_1, snd := pathDestRight P e₂' f₂ x_1 }) i)
⊢ f₁ i (Path.root x a f h' i c) = f₂ i (Path.root x a f h' i c)
[PROOFSTEP]
exact (congr_fun (congr_fun e₃ i) c : _)
[GOAL]
case mk.mk.e_snd.a.h.child.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refl.refl
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
a₁ : (mp P).A
f₁✝ f₂✝ : B (mp P) a₁ ⟹ α
r✝ : R { fst := a₁, snd := f₁✝ } { fst := a₁, snd := f₂✝ }
i✝ : Fin2 n
x : PFunctor.M (last P)
a : P.A
f : PFunctor.B (last P) a → PFunctor.M (last P)
h' : PFunctor.M.dest x = { fst := a, snd := f }
i : PFunctor.B (last P) a
c : Fin2 n
p : Path P (f i) c
IH : ∀ (f₁ f₂ : B (mp P) (f i) ⟹ α), R { fst := f i, snd := f₁ } { fst := f i, snd := f₂ } → f₁ c p = f₂ c p
f₁ f₂ : B (mp P) x ⟹ α
r : R { fst := x, snd := f₁ } { fst := x, snd := f₂ }
e₁' : PFunctor.M.dest x = { fst := a, snd := f }
e₁ :
  dest P { fst := x, snd := f₁ } =
    { fst := a, snd := splitFun (pathDestLeft P e₁' f₁) fun x_1 => { fst := f x_1, snd := pathDestRight P e₁' f₁ x_1 } }
e₂' : PFunctor.M.dest x = { fst := a, snd := f }
e₃ : pathDestLeft P e₁' f₁ = pathDestLeft P e₂' f₂
e₂ :
  dest P { fst := x, snd := f₂ } =
    { fst := a, snd := splitFun (pathDestLeft P e₁' f₁) fun x_1 => { fst := f x_1, snd := pathDestRight P e₂' f₂ x_1 } }
h'' :
  ∀ (i : TypeVec.last (B P a)),
    R ((fun x_1 => { fst := f x_1, snd := pathDestRight P e₁' f₁ x_1 }) i)
      ((fun x_1 => { fst := f x_1, snd := pathDestRight P e₂' f₂ x_1 }) i)
⊢ f₁ c (Path.child x a f h' i c p) = f₂ c (Path.child x a f h' i c p)
[PROOFSTEP]
exact IH _ _ (h'' _)
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
h : ∀ (x y : M P α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : M P α
r : R x y
⊢ x = y
[PROOFSTEP]
apply M.bisim P R _ _ _ r
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
h : ∀ (x y : M P α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : M P α
r : R x y
⊢ ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
[PROOFSTEP]
clear r x y
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
h : ∀ (x y : M P α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
⊢ ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
[PROOFSTEP]
introv Hr
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
h : ∀ (x y : M P α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : M P α
Hr : R x y
⊢ ∃ a f f₁ f₂,
    dest P x = { fst := a, snd := splitFun f f₁ } ∧
      dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
[PROOFSTEP]
specialize h _ _ Hr
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
Hr : R x y
h : (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
⊢ ∃ a f f₁ f₂,
    dest P x = { fst := a, snd := splitFun f f₁ } ∧
      dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
[PROOFSTEP]
clear Hr
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
h : (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
⊢ ∃ a f f₁ f₂,
    dest P x = { fst := a, snd := splitFun f f₁ } ∧
      dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
[PROOFSTEP]
revert h
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
⊢ (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y →
    ∃ a f f₁ f₂,
      dest P x = { fst := a, snd := splitFun f f₁ } ∧
        dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
[PROOFSTEP]
rcases M.dest P x with ⟨ax, fx⟩
[GOAL]
case mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx : B P ax ⟹ α ::: M P α
⊢ (TypeVec.id ::: Quot.mk R) <$$> { fst := ax, snd := fx } = (TypeVec.id ::: Quot.mk R) <$$> dest P y →
    ∃ a f f₁ f₂,
      { fst := ax, snd := fx } = { fst := a, snd := splitFun f f₁ } ∧
        dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
[PROOFSTEP]
rcases M.dest P y with ⟨ay, fy⟩
[GOAL]
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx : B P ax ⟹ α ::: M P α
ay : P.A
fy : B P ay ⟹ α ::: M P α
⊢ (TypeVec.id ::: Quot.mk R) <$$> { fst := ax, snd := fx } = (TypeVec.id ::: Quot.mk R) <$$> { fst := ay, snd := fy } →
    ∃ a f f₁ f₂,
      { fst := ax, snd := fx } = { fst := a, snd := splitFun f f₁ } ∧
        { fst := ay, snd := fy } = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
[PROOFSTEP]
intro h
[GOAL]
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx : B P ax ⟹ α ::: M P α
ay : P.A
fy : B P ay ⟹ α ::: M P α
h : (TypeVec.id ::: Quot.mk R) <$$> { fst := ax, snd := fx } = (TypeVec.id ::: Quot.mk R) <$$> { fst := ay, snd := fy }
⊢ ∃ a f f₁ f₂,
    { fst := ax, snd := fx } = { fst := a, snd := splitFun f f₁ } ∧
      { fst := ay, snd := fy } = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
[PROOFSTEP]
rw [map_eq, map_eq] at h 
[GOAL]
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx : B P ax ⟹ α ::: M P α
ay : P.A
fy : B P ay ⟹ α ::: M P α
h : { fst := ax, snd := (TypeVec.id ::: Quot.mk R) ⊚ fx } = { fst := ay, snd := (TypeVec.id ::: Quot.mk R) ⊚ fy }
⊢ ∃ a f f₁ f₂,
    { fst := ax, snd := fx } = { fst := a, snd := splitFun f f₁ } ∧
      { fst := ay, snd := fy } = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
[PROOFSTEP]
injection h with h₀ h₁
[GOAL]
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀✝ : Equivalence R
x y : M P α
ax : P.A
fx : B P ax ⟹ α ::: M P α
ay : P.A
fy : B P ay ⟹ α ::: M P α
h₀ : ax = ay
h₁ : HEq ((TypeVec.id ::: Quot.mk R) ⊚ fx) ((TypeVec.id ::: Quot.mk R) ⊚ fy)
⊢ ∃ a f f₁ f₂,
    { fst := ax, snd := fx } = { fst := a, snd := splitFun f f₁ } ∧
      { fst := ay, snd := fy } = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
[PROOFSTEP]
subst ay
[GOAL]
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx fy : B P ax ⟹ α ::: M P α
h₁ : HEq ((TypeVec.id ::: Quot.mk R) ⊚ fx) ((TypeVec.id ::: Quot.mk R) ⊚ fy)
⊢ ∃ a f f₁ f₂,
    { fst := ax, snd := fx } = { fst := a, snd := splitFun f f₁ } ∧
      { fst := ax, snd := fy } = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
[PROOFSTEP]
simp at h₁ 
[GOAL]
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx fy : B P ax ⟹ α ::: M P α
h₁ : (TypeVec.id ::: Quot.mk R) ⊚ fx = (TypeVec.id ::: Quot.mk R) ⊚ fy
⊢ ∃ a f f₁ f₂,
    { fst := ax, snd := fx } = { fst := a, snd := splitFun f f₁ } ∧
      { fst := ax, snd := fy } = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
[PROOFSTEP]
have Hdrop : dropFun fx = dropFun fy := by
  replace h₁ := congr_arg dropFun h₁
  simpa using h₁
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx fy : B P ax ⟹ α ::: M P α
h₁ : (TypeVec.id ::: Quot.mk R) ⊚ fx = (TypeVec.id ::: Quot.mk R) ⊚ fy
⊢ dropFun fx = dropFun fy
[PROOFSTEP]
replace h₁ := congr_arg dropFun h₁
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx fy : B P ax ⟹ α ::: M P α
h₁ : dropFun ((TypeVec.id ::: Quot.mk R) ⊚ fx) = dropFun ((TypeVec.id ::: Quot.mk R) ⊚ fy)
⊢ dropFun fx = dropFun fy
[PROOFSTEP]
simpa using h₁
[GOAL]
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx fy : B P ax ⟹ α ::: M P α
h₁ : (TypeVec.id ::: Quot.mk R) ⊚ fx = (TypeVec.id ::: Quot.mk R) ⊚ fy
Hdrop : dropFun fx = dropFun fy
⊢ ∃ a f f₁ f₂,
    { fst := ax, snd := fx } = { fst := a, snd := splitFun f f₁ } ∧
      { fst := ax, snd := fy } = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
[PROOFSTEP]
exists ax, dropFun fx, lastFun fx, lastFun fy
[GOAL]
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx fy : B P ax ⟹ α ::: M P α
h₁ : (TypeVec.id ::: Quot.mk R) ⊚ fx = (TypeVec.id ::: Quot.mk R) ⊚ fy
Hdrop : dropFun fx = dropFun fy
⊢ { fst := ax, snd := fx } = { fst := ax, snd := splitFun (dropFun fx) (lastFun fx) } ∧
    { fst := ax, snd := fy } = { fst := ax, snd := splitFun (dropFun fx) (lastFun fy) } ∧
      ∀ (i : TypeVec.last (B P ax)), R (lastFun fx i) (lastFun fy i)
[PROOFSTEP]
rw [split_dropFun_lastFun, Hdrop, split_dropFun_lastFun]
[GOAL]
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx fy : B P ax ⟹ α ::: M P α
h₁ : (TypeVec.id ::: Quot.mk R) ⊚ fx = (TypeVec.id ::: Quot.mk R) ⊚ fy
Hdrop : dropFun fx = dropFun fy
⊢ { fst := ax, snd := fx } = { fst := ax, snd := fx } ∧
    { fst := ax, snd := fy } = { fst := ax, snd := fy } ∧ ∀ (i : TypeVec.last (B P ax)), R (lastFun fx i) (lastFun fy i)
[PROOFSTEP]
simp
[GOAL]
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx fy : B P ax ⟹ α ::: M P α
h₁ : (TypeVec.id ::: Quot.mk R) ⊚ fx = (TypeVec.id ::: Quot.mk R) ⊚ fy
Hdrop : dropFun fx = dropFun fy
⊢ ∀ (i : TypeVec.last (B P ax)), R (lastFun fx i) (lastFun fy i)
[PROOFSTEP]
intro i
[GOAL]
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx fy : B P ax ⟹ α ::: M P α
h₁ : (TypeVec.id ::: Quot.mk R) ⊚ fx = (TypeVec.id ::: Quot.mk R) ⊚ fy
Hdrop : dropFun fx = dropFun fy
i : TypeVec.last (B P ax)
⊢ R (lastFun fx i) (lastFun fy i)
[PROOFSTEP]
replace h₁ := congr_fun (congr_fun h₁ Fin2.fz) i
[GOAL]
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx fy : B P ax ⟹ α ::: M P α
Hdrop : dropFun fx = dropFun fy
i : TypeVec.last (B P ax)
h₁ : ((TypeVec.id ::: Quot.mk R) ⊚ fx) Fin2.fz i = ((TypeVec.id ::: Quot.mk R) ⊚ fy) Fin2.fz i
⊢ R (lastFun fx i) (lastFun fy i)
[PROOFSTEP]
simp [(· ⊚ ·), appendFun, splitFun] at h₁ 
[GOAL]
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx fy : B P ax ⟹ α ::: M P α
Hdrop : dropFun fx = dropFun fy
i : TypeVec.last (B P ax)
h₁ : Quot.mk R (fx Fin2.fz i) = Quot.mk R (fy Fin2.fz i)
⊢ R (lastFun fx i) (lastFun fy i)
[PROOFSTEP]
replace h₁ := Quot.exact _ h₁
[GOAL]
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx fy : B P ax ⟹ α ::: M P α
Hdrop : dropFun fx = dropFun fy
i : TypeVec.last (B P ax)
h₁ : EqvGen R (fx Fin2.fz i) (fy Fin2.fz i)
⊢ R (lastFun fx i) (lastFun fy i)
[PROOFSTEP]
rw [h₀.eqvGen_iff] at h₁ 
[GOAL]
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx fy : B P ax ⟹ α ::: M P α
Hdrop : dropFun fx = dropFun fy
i : TypeVec.last (B P ax)
h₁ : R (fx Fin2.fz i) (fy Fin2.fz i)
⊢ R (lastFun fx i) (lastFun fy i)
[PROOFSTEP]
exact h₁
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h : ∀ (x y : M P α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : M P α
r : R x y
⊢ x = y
[PROOFSTEP]
have := M.bisim₀ P (EqvGen R) ?_ ?_
[GOAL]
case refine_3
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h : ∀ (x y : M P α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : M P α
r : R x y
this : ∀ (x y : M P α), EqvGen R x y → x = y
⊢ x = y
[PROOFSTEP]
solve_by_elim [EqvGen.rel]
[GOAL]
case refine_1
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h : ∀ (x y : M P α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : M P α
r : R x y
⊢ Equivalence (EqvGen R)
[PROOFSTEP]
apply EqvGen.is_equivalence
[GOAL]
case refine_2
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h : ∀ (x y : M P α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : M P α
r : R x y
⊢ ∀ (x y : M P α),
    EqvGen R x y → (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P x = (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P y
[PROOFSTEP]
clear r x y
[GOAL]
case refine_2
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h : ∀ (x y : M P α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
⊢ ∀ (x y : M P α),
    EqvGen R x y → (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P x = (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P y
[PROOFSTEP]
introv Hr
[GOAL]
case refine_2
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h : ∀ (x y : M P α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : M P α
Hr : EqvGen R x y
⊢ (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P x = (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P y
[PROOFSTEP]
have : ∀ x y, R x y → EqvGen R x y := @EqvGen.rel _ R
[GOAL]
case refine_2
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h : ∀ (x y : M P α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : M P α
Hr : EqvGen R x y
this : ∀ (x y : M P α), R x y → EqvGen R x y
⊢ (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P x = (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P y
[PROOFSTEP]
induction Hr
[GOAL]
case refine_2.rel
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h : ∀ (x y : M P α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : M P α
this : ∀ (x y : M P α), R x y → EqvGen R x y
x✝ y✝ : M P α
a✝ : R x✝ y✝
⊢ (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P x✝ = (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P y✝
[PROOFSTEP]
rw [← Quot.factor_mk_eq R (EqvGen R) this]
[GOAL]
case refine_2.rel
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h : ∀ (x y : M P α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : M P α
this : ∀ (x y : M P α), R x y → EqvGen R x y
x✝ y✝ : M P α
a✝ : R x✝ y✝
⊢ (TypeVec.id ::: Quot.factor R (EqvGen R) this ∘ Quot.mk R) <$$> dest P x✝ =
    (TypeVec.id ::: Quot.factor R (EqvGen R) this ∘ Quot.mk R) <$$> dest P y✝
[PROOFSTEP]
rwa [appendFun_comp_id, ← MvFunctor.map_map, ← MvFunctor.map_map, h]
  -- porting note: `cc` was replaced with `aesop`, maybe there is a more light-weight solution?
[GOAL]
case refine_2.refl
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h : ∀ (x y : M P α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : M P α
this : ∀ (x y : M P α), R x y → EqvGen R x y
x✝ : M P α
⊢ (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P x✝ = (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P x✝
case refine_2.symm
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h : ∀ (x y : M P α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : M P α
this : ∀ (x y : M P α), R x y → EqvGen R x y
x✝ y✝ : M P α
a✝ : EqvGen R x✝ y✝
a_ih✝ : (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P x✝ = (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P y✝
⊢ (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P y✝ = (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P x✝
case refine_2.trans
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h : ∀ (x y : M P α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : M P α
this : ∀ (x y : M P α), R x y → EqvGen R x y
x✝ y✝ z✝ : M P α
a✝¹ : EqvGen R x✝ y✝
a✝ : EqvGen R y✝ z✝
a_ih✝¹ : (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P x✝ = (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P y✝
a_ih✝ : (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P y✝ = (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P z✝
⊢ (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P x✝ = (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P z✝
[PROOFSTEP]
all_goals aesop
[GOAL]
case refine_2.refl
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h : ∀ (x y : M P α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : M P α
this : ∀ (x y : M P α), R x y → EqvGen R x y
x✝ : M P α
⊢ (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P x✝ = (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P x✝
[PROOFSTEP]
aesop
[GOAL]
case refine_2.symm
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h : ∀ (x y : M P α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : M P α
this : ∀ (x y : M P α), R x y → EqvGen R x y
x✝ y✝ : M P α
a✝ : EqvGen R x✝ y✝
a_ih✝ : (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P x✝ = (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P y✝
⊢ (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P y✝ = (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P x✝
[PROOFSTEP]
aesop
[GOAL]
case refine_2.trans
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h : ∀ (x y : M P α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : M P α
this : ∀ (x y : M P α), R x y → EqvGen R x y
x✝ y✝ z✝ : M P α
a✝¹ : EqvGen R x✝ y✝
a✝ : EqvGen R y✝ z✝
a_ih✝¹ : (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P x✝ = (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P y✝
a_ih✝ : (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P y✝ = (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P z✝
⊢ (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P x✝ = (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P z✝
[PROOFSTEP]
aesop
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ⟹ β
x : M P α
⊢ dest P (g <$$> x) = (g ::: fun x => g <$$> x) <$$> dest P x
[PROOFSTEP]
cases' x with a f
[GOAL]
case mk
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ⟹ β
a : (mp P).A
f : B (mp P) a ⟹ α
⊢ dest P (g <$$> { fst := a, snd := f }) = (g ::: fun x => g <$$> x) <$$> dest P { fst := a, snd := f }
[PROOFSTEP]
rw [map_eq]
[GOAL]
case mk
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ⟹ β
a : (mp P).A
f : B (mp P) a ⟹ α
⊢ dest P { fst := a, snd := g ⊚ f } = (g ::: fun x => g <$$> x) <$$> dest P { fst := a, snd := f }
[PROOFSTEP]
conv =>
  rhs
  rw [M.dest, M.dest', map_eq, appendFun_comp_splitFun]
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ⟹ β
a : (mp P).A
f : B (mp P) a ⟹ α
| dest P { fst := a, snd := g ⊚ f } = (g ::: fun x => g <$$> x) <$$> dest P { fst := a, snd := f }
[PROOFSTEP]
  rhs
  rw [M.dest, M.dest', map_eq, appendFun_comp_splitFun]
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ⟹ β
a : (mp P).A
f : B (mp P) a ⟹ α
| dest P { fst := a, snd := g ⊚ f } = (g ::: fun x => g <$$> x) <$$> dest P { fst := a, snd := f }
[PROOFSTEP]
  rhs
  rw [M.dest, M.dest', map_eq, appendFun_comp_splitFun]
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ⟹ β
a : (mp P).A
f : B (mp P) a ⟹ α
| dest P { fst := a, snd := g ⊚ f } = (g ::: fun x => g <$$> x) <$$> dest P { fst := a, snd := f }
[PROOFSTEP]
rhs
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ⟹ β
a : (mp P).A
f : B (mp P) a ⟹ α
| (g ::: fun x => g <$$> x) <$$> dest P { fst := a, snd := f }
[PROOFSTEP]
rw [M.dest, M.dest', map_eq, appendFun_comp_splitFun]
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ::: M P α ⟹ β ::: M P β
x : M P α
h : ∀ (x : M P α), lastFun g x = dropFun g <$$> x
⊢ g <$$> dest P x = dest P (dropFun g <$$> x)
[PROOFSTEP]
rw [M.dest_map]
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ::: M P α ⟹ β ::: M P β
x : M P α
h : ∀ (x : M P α), lastFun g x = dropFun g <$$> x
⊢ g <$$> dest P x = (dropFun g ::: fun x => dropFun g <$$> x) <$$> dest P x
[PROOFSTEP]
congr
[GOAL]
case e_a
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ::: M P α ⟹ β ::: M P β
x : M P α
h : ∀ (x : M P α), lastFun g x = dropFun g <$$> x
⊢ g = (dropFun g ::: fun x => dropFun g <$$> x)
[PROOFSTEP]
apply eq_of_drop_last_eq
[GOAL]
case e_a.h₀
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ::: M P α ⟹ β ::: M P β
x : M P α
h : ∀ (x : M P α), lastFun g x = dropFun g <$$> x
⊢ dropFun g = dropFun (dropFun g ::: fun x => dropFun g <$$> x)
[PROOFSTEP]
simp
[GOAL]
case e_a.h₁
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ::: M P α ⟹ β ::: M P β
x : M P α
h : ∀ (x : M P α), lastFun g x = dropFun g <$$> x
⊢ lastFun g = lastFun (dropFun g ::: fun x => dropFun g <$$> x)
[PROOFSTEP]
simp
[GOAL]
case e_a.h₁
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ::: M P α ⟹ β ::: M P β
x : M P α
h : ∀ (x : M P α), lastFun g x = dropFun g <$$> x
⊢ lastFun g = fun x => dropFun g <$$> x
[PROOFSTEP]
ext1
[GOAL]
case e_a.h₁.h
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ::: M P α ⟹ β ::: M P β
x : M P α
h : ∀ (x : M P α), lastFun g x = dropFun g <$$> x
x✝ : TypeVec.last (α ::: M P α)
⊢ lastFun g x✝ = dropFun g <$$> x✝
[PROOFSTEP]
apply h
