case mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
g₁ g₂ : Fix F → α
h : ∀ (x : F (Fix F)), g₁ <$> x = g₂ <$> x → g₁ (mk x) = g₂ (mk x)
⊢ ∀ (a : PFunctor.W (P F)), g₁ (Quot.mk Setoid.r a) = g₂ (Quot.mk Setoid.r a)
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
g₁ g₂ : Fix F → α
h : ∀ (x : F (Fix F)), g₁ <$> x = g₂ <$> x → g₁ (mk x) = g₂ (mk x)
⊢ ∀ (x : Fix F), g₁ x = g₂ x
apply Quot.ind
case mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
g₁ g₂ : Fix F → α
h : ∀ (x : F (Fix F)), g₁ <$> x = g₂ <$> x → g₁ (mk x) = g₂ (mk x)
x : PFunctor.W (P F)
⊢ g₁ (Quot.mk Setoid.r x) = g₂ (Quot.mk Setoid.r x)
case mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
g₁ g₂ : Fix F → α
h : ∀ (x : F (Fix F)), g₁ <$> x = g₂ <$> x → g₁ (mk x) = g₂ (mk x)
⊢ ∀ (a : PFunctor.W (P F)), g₁ (Quot.mk Setoid.r a) = g₂ (Quot.mk Setoid.r a)
intro x
case mk.mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
g₁ g₂ : Fix F → α
h : ∀ (x : F (Fix F)), g₁ <$> x = g₂ <$> x → g₁ (mk x) = g₂ (mk x)
a : (P F).A
f : PFunctor.B (P F) a → WType (P F).B
ih : ∀ (a : PFunctor.B (P F) a), g₁ (Quot.mk Setoid.r (f a)) = g₂ (Quot.mk Setoid.r (f a))
⊢ g₁ (Quot.mk Setoid.r (WType.mk a f)) = g₂ (Quot.mk Setoid.r (WType.mk a f))
case mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
g₁ g₂ : Fix F → α
h : ∀ (x : F (Fix F)), g₁ <$> x = g₂ <$> x → g₁ (mk x) = g₂ (mk x)
x : PFunctor.W (P F)
⊢ g₁ (Quot.mk Setoid.r x) = g₂ (Quot.mk Setoid.r x)
induction' x with a f ih
case mk.mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
g₁ g₂ : Fix F → α
h : ∀ (x : F (Fix F)), g₁ <$> x = g₂ <$> x → g₁ (mk x) = g₂ (mk x)
a : (P F).A
f : PFunctor.B (P F) a → WType (P F).B
ih : ∀ (a : PFunctor.B (P F) a), g₁ (Quot.mk Setoid.r (f a)) = g₂ (Quot.mk Setoid.r (f a))
⊢ g₁ (Quotient.mk Wsetoid (WType.mk a f)) = g₂ (Quotient.mk Wsetoid (WType.mk a f))
case mk.mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
g₁ g₂ : Fix F → α
h : ∀ (x : F (Fix F)), g₁ <$> x = g₂ <$> x → g₁ (mk x) = g₂ (mk x)
a : (P F).A
f : PFunctor.B (P F) a → WType (P F).B
ih : ∀ (a : PFunctor.B (P F) a), g₁ (Quot.mk Setoid.r (f a)) = g₂ (Quot.mk Setoid.r (f a))
⊢ g₁ (Quot.mk Setoid.r (WType.mk a f)) = g₂ (Quot.mk Setoid.r (WType.mk a f))
change g₁ ⟦⟨a, f⟩⟧ = g₂ ⟦⟨a, f⟩⟧
case mk.mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
g₁ g₂ : Fix F → α
h : ∀ (x : F (Fix F)), g₁ <$> x = g₂ <$> x → g₁ (mk x) = g₂ (mk x)
a : (P F).A
f : PFunctor.B (P F) a → WType (P F).B
ih : ∀ (a : PFunctor.B (P F) a), g₁ (Quot.mk Setoid.r (f a)) = g₂ (Quot.mk Setoid.r (f a))
⊢ g₁ (mk (abs { fst := a, snd := fun x => Quotient.mk Wsetoid (f x) })) =
    g₂ (mk (abs { fst := a, snd := fun x => Quotient.mk Wsetoid (f x) }))
case mk.mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
g₁ g₂ : Fix F → α
h : ∀ (x : F (Fix F)), g₁ <$> x = g₂ <$> x → g₁ (mk x) = g₂ (mk x)
a : (P F).A
f : PFunctor.B (P F) a → WType (P F).B
ih : ∀ (a : PFunctor.B (P F) a), g₁ (Quot.mk Setoid.r (f a)) = g₂ (Quot.mk Setoid.r (f a))
⊢ g₁ (Quotient.mk Wsetoid (WType.mk a f)) = g₂ (Quotient.mk Wsetoid (WType.mk a f))
rw [← Fix.ind_aux a f]
case mk.mk.a
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
g₁ g₂ : Fix F → α
h : ∀ (x : F (Fix F)), g₁ <$> x = g₂ <$> x → g₁ (mk x) = g₂ (mk x)
a : (P F).A
f : PFunctor.B (P F) a → WType (P F).B
ih : ∀ (a : PFunctor.B (P F) a), g₁ (Quot.mk Setoid.r (f a)) = g₂ (Quot.mk Setoid.r (f a))
⊢ g₁ <$> abs { fst := a, snd := fun x => Quotient.mk Wsetoid (f x) } =
    g₂ <$> abs { fst := a, snd := fun x => Quotient.mk Wsetoid (f x) }
case mk.mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
g₁ g₂ : Fix F → α
h : ∀ (x : F (Fix F)), g₁ <$> x = g₂ <$> x → g₁ (mk x) = g₂ (mk x)
a : (P F).A
f : PFunctor.B (P F) a → WType (P F).B
ih : ∀ (a : PFunctor.B (P F) a), g₁ (Quot.mk Setoid.r (f a)) = g₂ (Quot.mk Setoid.r (f a))
⊢ g₁ (mk (abs { fst := a, snd := fun x => Quotient.mk Wsetoid (f x) })) =
    g₂ (mk (abs { fst := a, snd := fun x => Quotient.mk Wsetoid (f x) }))
apply h
case mk.mk.a
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
g₁ g₂ : Fix F → α
h : ∀ (x : F (Fix F)), g₁ <$> x = g₂ <$> x → g₁ (mk x) = g₂ (mk x)
a : (P F).A
f : PFunctor.B (P F) a → WType (P F).B
ih : ∀ (a : PFunctor.B (P F) a), g₁ (Quot.mk Setoid.r (f a)) = g₂ (Quot.mk Setoid.r (f a))
⊢ abs { fst := a, snd := g₁ ∘ fun x => Quotient.mk Wsetoid (f x) } =
    abs { fst := a, snd := g₂ ∘ fun x => Quotient.mk Wsetoid (f x) }
case mk.mk.a
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
g₁ g₂ : Fix F → α
h : ∀ (x : F (Fix F)), g₁ <$> x = g₂ <$> x → g₁ (mk x) = g₂ (mk x)
a : (P F).A
f : PFunctor.B (P F) a → WType (P F).B
ih : ∀ (a : PFunctor.B (P F) a), g₁ (Quot.mk Setoid.r (f a)) = g₂ (Quot.mk Setoid.r (f a))
⊢ g₁ <$> abs { fst := a, snd := fun x => Quotient.mk Wsetoid (f x) } =
    g₂ <$> abs { fst := a, snd := fun x => Quotient.mk Wsetoid (f x) }
rw [← abs_map, ← abs_map, PFunctor.map_eq, PFunctor.map_eq]
case mk.mk.a.e_a.e_snd.h
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
g₁ g₂ : Fix F → α
h : ∀ (x : F (Fix F)), g₁ <$> x = g₂ <$> x → g₁ (mk x) = g₂ (mk x)
a : (P F).A
f : PFunctor.B (P F) a → WType (P F).B
ih : ∀ (a : PFunctor.B (P F) a), g₁ (Quot.mk Setoid.r (f a)) = g₂ (Quot.mk Setoid.r (f a))
x : PFunctor.B (P F) a
⊢ (g₁ ∘ fun x => Quotient.mk Wsetoid (f x)) x = (g₂ ∘ fun x => Quotient.mk Wsetoid (f x)) x
case mk.mk.a
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
g₁ g₂ : Fix F → α
h : ∀ (x : F (Fix F)), g₁ <$> x = g₂ <$> x → g₁ (mk x) = g₂ (mk x)
a : (P F).A
f : PFunctor.B (P F) a → WType (P F).B
ih : ∀ (a : PFunctor.B (P F) a), g₁ (Quot.mk Setoid.r (f a)) = g₂ (Quot.mk Setoid.r (f a))
⊢ abs { fst := a, snd := g₁ ∘ fun x => Quotient.mk Wsetoid (f x) } =
    abs { fst := a, snd := g₂ ∘ fun x => Quotient.mk Wsetoid (f x) }
congr with x
no goals
case mk.mk.a.e_a.e_snd.h
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
g₁ g₂ : Fix F → α
h : ∀ (x : F (Fix F)), g₁ <$> x = g₂ <$> x → g₁ (mk x) = g₂ (mk x)
a : (P F).A
f : PFunctor.B (P F) a → WType (P F).B
ih : ∀ (a : PFunctor.B (P F) a), g₁ (Quot.mk Setoid.r (f a)) = g₂ (Quot.mk Setoid.r (f a))
x : PFunctor.B (P F) a
⊢ (g₁ ∘ fun x => Quotient.mk Wsetoid (f x)) x = (g₂ ∘ fun x => Quotient.mk Wsetoid (f x)) x
apply ih