case h
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Liftr r (dest x) (dest y)
⊢ ∀ (x y : Cofix F), r x y → (Quot.mk fun x y => r x y) <$> dest x = (Quot.mk fun x y => r x y) <$> dest y
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Liftr r (dest x) (dest y)
⊢ ∀ (x y : Cofix F), r x y → x = y
apply Cofix.bisim_rel
case h
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Liftr r (dest x) (dest y)
x y : Cofix F
rxy : r x y
⊢ (Quot.mk fun x y => r x y) <$> dest x = (Quot.mk fun x y => r x y) <$> dest y
case h
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Liftr r (dest x) (dest y)
⊢ ∀ (x y : Cofix F), r x y → (Quot.mk fun x y => r x y) <$> dest x = (Quot.mk fun x y => r x y) <$> dest y
intro x y rxy
case h.intro.intro.intro.intro.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Liftr r (dest x) (dest y)
x y : Cofix F
rxy : r x y
a : (P F).A
f₀ f₁ : PFunctor.B (P F) a → Cofix F
dxeq : dest x = abs { fst := a, snd := f₀ }
dyeq : dest y = abs { fst := a, snd := f₁ }
h' : ∀ (i : PFunctor.B (P F) a), r (f₀ i) (f₁ i)
⊢ (Quot.mk fun x y => r x y) <$> dest x = (Quot.mk fun x y => r x y) <$> dest y
case h
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Liftr r (dest x) (dest y)
x y : Cofix F
rxy : r x y
⊢ (Quot.mk fun x y => r x y) <$> dest x = (Quot.mk fun x y => r x y) <$> dest y
rcases (liftr_iff r _ _).mp (h x y rxy) with ⟨a, f₀, f₁, dxeq, dyeq, h'⟩
case h.intro.intro.intro.intro.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Liftr r (dest x) (dest y)
x y : Cofix F
rxy : r x y
a : (P F).A
f₀ f₁ : PFunctor.B (P F) a → Cofix F
dxeq : dest x = abs { fst := a, snd := f₀ }
dyeq : dest y = abs { fst := a, snd := f₁ }
h' : ∀ (i : PFunctor.B (P F) a), r (f₀ i) (f₁ i)
⊢ abs { fst := a, snd := (Quot.mk fun x y => r x y) ∘ f₀ } = abs { fst := a, snd := (Quot.mk fun x y => r x y) ∘ f₁ }
case h.intro.intro.intro.intro.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Liftr r (dest x) (dest y)
x y : Cofix F
rxy : r x y
a : (P F).A
f₀ f₁ : PFunctor.B (P F) a → Cofix F
dxeq : dest x = abs { fst := a, snd := f₀ }
dyeq : dest y = abs { fst := a, snd := f₁ }
h' : ∀ (i : PFunctor.B (P F) a), r (f₀ i) (f₁ i)
⊢ (Quot.mk fun x y => r x y) <$> dest x = (Quot.mk fun x y => r x y) <$> dest y
rw [dxeq, dyeq, ← abs_map, ← abs_map, PFunctor.map_eq, PFunctor.map_eq]
case h.intro.intro.intro.intro.intro.e_a.e_snd.h
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Liftr r (dest x) (dest y)
x y : Cofix F
rxy : r x y
a : (P F).A
f₀ f₁ : PFunctor.B (P F) a → Cofix F
dxeq : dest x = abs { fst := a, snd := f₀ }
dyeq : dest y = abs { fst := a, snd := f₁ }
h' : ∀ (i : PFunctor.B (P F) a), r (f₀ i) (f₁ i)
i : PFunctor.B (P F) a
⊢ ((Quot.mk fun x y => r x y) ∘ f₀) i = ((Quot.mk fun x y => r x y) ∘ f₁) i
case h.intro.intro.intro.intro.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Liftr r (dest x) (dest y)
x y : Cofix F
rxy : r x y
a : (P F).A
f₀ f₁ : PFunctor.B (P F) a → Cofix F
dxeq : dest x = abs { fst := a, snd := f₀ }
dyeq : dest y = abs { fst := a, snd := f₁ }
h' : ∀ (i : PFunctor.B (P F) a), r (f₀ i) (f₁ i)
⊢ abs { fst := a, snd := (Quot.mk fun x y => r x y) ∘ f₀ } = abs { fst := a, snd := (Quot.mk fun x y => r x y) ∘ f₁ }
congr 2 with i
case h.intro.intro.intro.intro.intro.e_a.e_snd.h.a
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Liftr r (dest x) (dest y)
x y : Cofix F
rxy : r x y
a : (P F).A
f₀ f₁ : PFunctor.B (P F) a → Cofix F
dxeq : dest x = abs { fst := a, snd := f₀ }
dyeq : dest y = abs { fst := a, snd := f₁ }
h' : ∀ (i : PFunctor.B (P F) a), r (f₀ i) (f₁ i)
i : PFunctor.B (P F) a
⊢ r (f₀ i) (f₁ i)
case h.intro.intro.intro.intro.intro.e_a.e_snd.h
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Liftr r (dest x) (dest y)
x y : Cofix F
rxy : r x y
a : (P F).A
f₀ f₁ : PFunctor.B (P F) a → Cofix F
dxeq : dest x = abs { fst := a, snd := f₀ }
dyeq : dest y = abs { fst := a, snd := f₁ }
h' : ∀ (i : PFunctor.B (P F) a), r (f₀ i) (f₁ i)
i : PFunctor.B (P F) a
⊢ ((Quot.mk fun x y => r x y) ∘ f₀) i = ((Quot.mk fun x y => r x y) ∘ f₁) i
apply Quot.sound
no goals
case h.intro.intro.intro.intro.intro.e_a.e_snd.h.a
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Liftr r (dest x) (dest y)
x y : Cofix F
rxy : r x y
a : (P F).A
f₀ f₁ : PFunctor.B (P F) a → Cofix F
dxeq : dest x = abs { fst := a, snd := f₀ }
dyeq : dest y = abs { fst := a, snd := f₁ }
h' : ∀ (i : PFunctor.B (P F) a), r (f₀ i) (f₁ i)
i : PFunctor.B (P F) a
⊢ r (f₀ i) (f₁ i)
apply h'