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 }
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 }
generalize ef : @splitFun n _ (append1 α (M P α)) f' f₁' = ff at e₁
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 }
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 }
let he₁' := PFunctor.M.dest a₁
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 }
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 }
rcases e₁' : he₁' with ⟨a₁', g₁'⟩
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 }
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 }
rw [M.dest_eq_dest' _ e₁'] at e₁
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 }
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 }
cases e₁
no goals
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 }
exact ⟨_, e₁', splitFun_inj ef⟩