case mk
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
⊢ ∀ (a : MvPFunctor.W (P F) α), g₁ (Quot.mk Setoid.r a) = g₂ (Quot.mk Setoid.r a)
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
⊢ ∀ (x : Fix F α), g₁ x = g₂ x
apply Quot.ind
case mk
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
x : MvPFunctor.W (P F) α
⊢ g₁ (Quot.mk Setoid.r x) = g₂ (Quot.mk Setoid.r x)
case mk
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
⊢ ∀ (a : MvPFunctor.W (P F) α), g₁ (Quot.mk Setoid.r a) = g₂ (Quot.mk Setoid.r a)
intro x
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
x : MvPFunctor.W (P F) α
⊢ ∀ (a : (P F).A) (f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α)
    (f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α),
    (∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), g₁ (Quot.mk Setoid.r (f i)) = g₂ (Quot.mk Setoid.r (f i))) →
      g₁ (Quot.mk Setoid.r (MvPFunctor.wMk (P F) a f' f)) = g₂ (Quot.mk Setoid.r (MvPFunctor.wMk (P F) a f' f))
case mk
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
x : MvPFunctor.W (P F) α
⊢ g₁ (Quot.mk Setoid.r x) = g₂ (Quot.mk Setoid.r x)
apply q.P.w_ind _ x
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
x : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
ih : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), g₁ (Quot.mk Setoid.r (f i)) = g₂ (Quot.mk Setoid.r (f i))
⊢ g₁ (Quot.mk Setoid.r (MvPFunctor.wMk (P F) a f' f)) = g₂ (Quot.mk Setoid.r (MvPFunctor.wMk (P F) a f' f))
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
x : MvPFunctor.W (P F) α
⊢ ∀ (a : (P F).A) (f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α)
    (f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α),
    (∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), g₁ (Quot.mk Setoid.r (f i)) = g₂ (Quot.mk Setoid.r (f i))) →
      g₁ (Quot.mk Setoid.r (MvPFunctor.wMk (P F) a f' f)) = g₂ (Quot.mk Setoid.r (MvPFunctor.wMk (P F) a f' f))
intro a f' f ih
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
x : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
ih : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), g₁ (Quot.mk Setoid.r (f i)) = g₂ (Quot.mk Setoid.r (f i))
⊢ g₁ (Quotient.mk (wSetoid α) (MvPFunctor.wMk (P F) a f' f)) =
    g₂ (Quotient.mk (wSetoid α) (MvPFunctor.wMk (P F) a f' f))
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
x : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
ih : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), g₁ (Quot.mk Setoid.r (f i)) = g₂ (Quot.mk Setoid.r (f i))
⊢ g₁ (Quot.mk Setoid.r (MvPFunctor.wMk (P F) a f' f)) = g₂ (Quot.mk Setoid.r (MvPFunctor.wMk (P F) a f' f))
show g₁ ⟦q.P.wMk a f' f⟧ = g₂ ⟦q.P.wMk a f' f⟧
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
x : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
ih : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), g₁ (Quot.mk Setoid.r (f i)) = g₂ (Quot.mk Setoid.r (f i))
⊢ g₁ (mk (abs { fst := a, snd := MvPFunctor.appendContents (P F) f' fun x => Quotient.mk (wSetoid α) (f x) })) =
    g₂ (mk (abs { fst := a, snd := MvPFunctor.appendContents (P F) f' fun x => Quotient.mk (wSetoid α) (f x) }))
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
x : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
ih : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), g₁ (Quot.mk Setoid.r (f i)) = g₂ (Quot.mk Setoid.r (f i))
⊢ g₁ (Quotient.mk (wSetoid α) (MvPFunctor.wMk (P F) a f' f)) =
    g₂ (Quotient.mk (wSetoid α) (MvPFunctor.wMk (P F) a f' f))
rw [← Fix.ind_aux a f' f]
case a
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
x : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
ih : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), g₁ (Quot.mk Setoid.r (f i)) = g₂ (Quot.mk Setoid.r (f i))
⊢ (TypeVec.id ::: g₁) <$$>
      abs { fst := a, snd := MvPFunctor.appendContents (P F) f' fun x => Quotient.mk (wSetoid α) (f x) } =
    (TypeVec.id ::: g₂) <$$>
      abs { fst := a, snd := MvPFunctor.appendContents (P F) f' fun x => Quotient.mk (wSetoid α) (f x) }
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
x : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
ih : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), g₁ (Quot.mk Setoid.r (f i)) = g₂ (Quot.mk Setoid.r (f i))
⊢ g₁ (mk (abs { fst := a, snd := MvPFunctor.appendContents (P F) f' fun x => Quotient.mk (wSetoid α) (f x) })) =
    g₂ (mk (abs { fst := a, snd := MvPFunctor.appendContents (P F) f' fun x => Quotient.mk (wSetoid α) (f x) }))
apply h
case a
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
x : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
ih : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), g₁ (Quot.mk Setoid.r (f i)) = g₂ (Quot.mk Setoid.r (f i))
⊢ abs
      { fst := a,
        snd := (TypeVec.id ::: g₁) ⊚ MvPFunctor.appendContents (P F) f' fun x => Quotient.mk (wSetoid α) (f x) } =
    abs
      { fst := a,
        snd := (TypeVec.id ::: g₂) ⊚ MvPFunctor.appendContents (P F) f' fun x => Quotient.mk (wSetoid α) (f x) }
case a
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
x : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
ih : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), g₁ (Quot.mk Setoid.r (f i)) = g₂ (Quot.mk Setoid.r (f i))
⊢ (TypeVec.id ::: g₁) <$$>
      abs { fst := a, snd := MvPFunctor.appendContents (P F) f' fun x => Quotient.mk (wSetoid α) (f x) } =
    (TypeVec.id ::: g₂) <$$>
      abs { fst := a, snd := MvPFunctor.appendContents (P F) f' fun x => Quotient.mk (wSetoid α) (f x) }
rw [← abs_map, ← abs_map, MvPFunctor.map_eq, MvPFunctor.map_eq]
case a.e_a.e_snd
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
x : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
ih : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), g₁ (Quot.mk Setoid.r (f i)) = g₂ (Quot.mk Setoid.r (f i))
⊢ ((TypeVec.id ::: g₁) ⊚ MvPFunctor.appendContents (P F) f' fun x => Quotient.mk (wSetoid α) (f x)) =
    (TypeVec.id ::: g₂) ⊚ MvPFunctor.appendContents (P F) f' fun x => Quotient.mk (wSetoid α) (f x)
case a
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
x : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
ih : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), g₁ (Quot.mk Setoid.r (f i)) = g₂ (Quot.mk Setoid.r (f i))
⊢ abs
      { fst := a,
        snd := (TypeVec.id ::: g₁) ⊚ MvPFunctor.appendContents (P F) f' fun x => Quotient.mk (wSetoid α) (f x) } =
    abs
      { fst := a,
        snd := (TypeVec.id ::: g₂) ⊚ MvPFunctor.appendContents (P F) f' fun x => Quotient.mk (wSetoid α) (f x) }
congr 2
case a.e_a.e_snd
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
x : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
ih : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), g₁ (Quot.mk Setoid.r (f i)) = g₂ (Quot.mk Setoid.r (f i))
⊢ splitFun (TypeVec.id ⊚ f') (g₁ ∘ fun x => Quotient.mk (wSetoid α) (f x)) =
    splitFun (TypeVec.id ⊚ f') (g₂ ∘ fun x => Quotient.mk (wSetoid α) (f x))
case a.e_a.e_snd
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
x : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
ih : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), g₁ (Quot.mk Setoid.r (f i)) = g₂ (Quot.mk Setoid.r (f i))
⊢ ((TypeVec.id ::: g₁) ⊚ MvPFunctor.appendContents (P F) f' fun x => Quotient.mk (wSetoid α) (f x)) =
    (TypeVec.id ::: g₂) ⊚ MvPFunctor.appendContents (P F) f' fun x => Quotient.mk (wSetoid α) (f x)
rw [MvPFunctor.appendContents, appendFun, appendFun, ← splitFun_comp, ← splitFun_comp]
case a.e_a.e_snd
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
x : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
ih : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), g₁ (Quot.mk Setoid.r (f i)) = g₂ (Quot.mk Setoid.r (f i))
this : (g₁ ∘ fun x => Quotient.mk (wSetoid α) (f x)) = g₂ ∘ fun x => Quotient.mk (wSetoid α) (f x)
⊢ splitFun (TypeVec.id ⊚ f') (g₁ ∘ fun x => Quotient.mk (wSetoid α) (f x)) =
    splitFun (TypeVec.id ⊚ f') (g₂ ∘ fun x => Quotient.mk (wSetoid α) (f x))
case a.e_a.e_snd
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
x : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
ih : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), g₁ (Quot.mk Setoid.r (f i)) = g₂ (Quot.mk Setoid.r (f i))
⊢ splitFun (TypeVec.id ⊚ f') (g₁ ∘ fun x => Quotient.mk (wSetoid α) (f x)) =
    splitFun (TypeVec.id ⊚ f') (g₂ ∘ fun x => Quotient.mk (wSetoid α) (f x))
have : (g₁ ∘ fun x => ⟦f x⟧) = g₂ ∘ fun x => ⟦f x⟧ := by
  ext x
  exact ih x
no goals
case a.e_a.e_snd
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
x : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
ih : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), g₁ (Quot.mk Setoid.r (f i)) = g₂ (Quot.mk Setoid.r (f i))
this : (g₁ ∘ fun x => Quotient.mk (wSetoid α) (f x)) = g₂ ∘ fun x => Quotient.mk (wSetoid α) (f x)
⊢ splitFun (TypeVec.id ⊚ f') (g₁ ∘ fun x => Quotient.mk (wSetoid α) (f x)) =
    splitFun (TypeVec.id ⊚ f') (g₂ ∘ fun x => Quotient.mk (wSetoid α) (f x))
rw [this]
case h
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
x✝ : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
ih : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), g₁ (Quot.mk Setoid.r (f i)) = g₂ (Quot.mk Setoid.r (f i))
x : PFunctor.B (MvPFunctor.last (P F)) a
⊢ (g₁ ∘ fun x => Quotient.mk (wSetoid α) (f x)) x = (g₂ ∘ fun x => Quotient.mk (wSetoid α) (f x)) x
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
x : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
ih : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), g₁ (Quot.mk Setoid.r (f i)) = g₂ (Quot.mk Setoid.r (f i))
⊢ (g₁ ∘ fun x => Quotient.mk (wSetoid α) (f x)) = g₂ ∘ fun x => Quotient.mk (wSetoid α) (f x)
ext x
no goals
case h
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
x✝ : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
ih : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), g₁ (Quot.mk Setoid.r (f i)) = g₂ (Quot.mk Setoid.r (f i))
x : PFunctor.B (MvPFunctor.last (P F)) a
⊢ (g₁ ∘ fun x => Quotient.mk (wSetoid α) (f x)) x = (g₂ ∘ fun x => Quotient.mk (wSetoid α) (f x)) x
exact ih x