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 → Quot.mk r <$> dest x = Quot.mk r <$> dest y
r' : Cofix F → Cofix F → Prop := fun x y => x = y ∨ r x y
⊢ ∀ (x y : Cofix F), r x y → x = 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 → Quot.mk r <$> dest x = Quot.mk r <$> dest y
⊢ ∀ (x y : Cofix F), r x y → x = y
let r' (x y) := x = y ∨ r x 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 → Quot.mk r <$> dest x = Quot.mk r <$> dest y
r' : Cofix F → Cofix F → Prop := fun x y => x = y ∨ r x y
x y : Cofix F
rxy : r x y
⊢ x = 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 → Quot.mk r <$> dest x = Quot.mk r <$> dest y
r' : Cofix F → Cofix F → Prop := fun x y => x = y ∨ r x y
⊢ ∀ (x y : Cofix F), r x y → x = y
intro x y rxy
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 → Quot.mk r <$> dest x = Quot.mk r <$> dest y
r' : Cofix F → Cofix F → Prop := fun x y => x = y ∨ r x y
x y : Cofix F
rxy : r x y
⊢ ∀ (x : Cofix F), r' x x

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 → Quot.mk r <$> dest x = Quot.mk r <$> dest y
r' : Cofix F → Cofix F → Prop := fun x y => x = y ∨ r x y
x y : Cofix F
rxy : r x y
⊢ ∀ (x y : Cofix F), r' x y → Quot.mk r' <$> dest x = Quot.mk r' <$> dest y

case 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 → Quot.mk r <$> dest x = Quot.mk r <$> dest y
r' : Cofix F → Cofix F → Prop := fun x y => x = y ∨ r x y
x y : Cofix F
rxy : r x y
⊢ r' x 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 → Quot.mk r <$> dest x = Quot.mk r <$> dest y
r' : Cofix F → Cofix F → Prop := fun x y => x = y ∨ r x y
x y : Cofix F
rxy : r x y
⊢ x = y
apply Cofix.bisim_aux r'
case a.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 → Quot.mk r <$> dest x = Quot.mk r <$> dest y
r' : Cofix F → Cofix F → Prop := fun x y => x = y ∨ r x y
x y : Cofix F
rxy : r x y
⊢ r x y
case 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 → Quot.mk r <$> dest x = Quot.mk r <$> dest y
r' : Cofix F → Cofix F → Prop := fun x y => x = y ∨ r x y
x y : Cofix F
rxy : r x y
⊢ r' x y
right
no goals
case a.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 → Quot.mk r <$> dest x = Quot.mk r <$> dest y
r' : Cofix F → Cofix F → Prop := fun x y => x = y ∨ r x y
x y : Cofix F
rxy : r x y
⊢ r x y
exact rxy
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 → Quot.mk r <$> dest x = Quot.mk r <$> dest y
r' : Cofix F → Cofix F → Prop := fun x y => x = y ∨ r x y
x✝ y : Cofix F
rxy : r x✝ y
x : Cofix F
⊢ r' x x
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 → Quot.mk r <$> dest x = Quot.mk r <$> dest y
r' : Cofix F → Cofix F → Prop := fun x y => x = y ∨ r x y
x y : Cofix F
rxy : r x y
⊢ ∀ (x : Cofix F), r' x x
intro x
case h'.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 → Quot.mk r <$> dest x = Quot.mk r <$> dest y
r' : Cofix F → Cofix F → Prop := fun x y => x = y ∨ r x y
x✝ y : Cofix F
rxy : r x✝ y
x : Cofix F
⊢ x = x
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 → Quot.mk r <$> dest x = Quot.mk r <$> dest y
r' : Cofix F → Cofix F → Prop := fun x y => x = y ∨ r x y
x✝ y : Cofix F
rxy : r x✝ y
x : Cofix F
⊢ r' x x
left
no goals
case h'.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 → Quot.mk r <$> dest x = Quot.mk r <$> dest y
r' : Cofix F → Cofix F → Prop := fun x y => x = y ∨ r x y
x✝ y : Cofix F
rxy : r x✝ y
x : Cofix F
⊢ x = x
rfl
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 → Quot.mk r <$> dest x = Quot.mk r <$> dest y
r' : Cofix F → Cofix F → Prop := fun x y => x = y ∨ r x y
x✝ y✝ : Cofix F
rxy : r x✝ y✝
x y : Cofix F
r'xy : r' x y
⊢ Quot.mk r' <$> dest x = Quot.mk r' <$> 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 → Quot.mk r <$> dest x = Quot.mk r <$> dest y
r' : Cofix F → Cofix F → Prop := fun x y => x = y ∨ r x y
x y : Cofix F
rxy : r x y
⊢ ∀ (x y : Cofix F), r' x y → Quot.mk r' <$> dest x = Quot.mk r' <$> dest y
intro x y r'xy
case h.inl
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 → Quot.mk r <$> dest x = Quot.mk r <$> dest y
r' : Cofix F → Cofix F → Prop := fun x y => x = y ∨ r x y
x✝ y✝ : Cofix F
rxy : r x✝ y✝
x y : Cofix F
r'xy : x = y
⊢ Quot.mk r' <$> dest x = Quot.mk r' <$> dest y

case h.inr
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 → Quot.mk r <$> dest x = Quot.mk r <$> dest y
r' : Cofix F → Cofix F → Prop := fun x y => x = y ∨ r x y
x✝ y✝ : Cofix F
rxy : r x✝ y✝
x y : Cofix F
r'xy : r x y
⊢ Quot.mk r' <$> dest x = Quot.mk r' <$> 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 → Quot.mk r <$> dest x = Quot.mk r <$> dest y
r' : Cofix F → Cofix F → Prop := fun x y => x = y ∨ r x y
x✝ y✝ : Cofix F
rxy : r x✝ y✝
x y : Cofix F
r'xy : r' x y
⊢ Quot.mk r' <$> dest x = Quot.mk r' <$> dest y
cases' r'xy with r'xy r'xy
case h.inr
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 → Quot.mk r <$> dest x = Quot.mk r <$> dest y
r' : Cofix F → Cofix F → Prop := fun x y => x = y ∨ r x y
x✝ y✝ : Cofix F
rxy : r x✝ y✝
x y : Cofix F
r'xy : r x y
this : ∀ (x y : Cofix F), r x y → r' x y
⊢ Quot.mk r' <$> dest x = Quot.mk r' <$> dest y
case h.inr
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 → Quot.mk r <$> dest x = Quot.mk r <$> dest y
r' : Cofix F → Cofix F → Prop := fun x y => x = y ∨ r x y
x✝ y✝ : Cofix F
rxy : r x✝ y✝
x y : Cofix F
r'xy : r x y
⊢ Quot.mk r' <$> dest x = Quot.mk r' <$> dest y
have : ∀ x y, r x y → r' x y := fun x y h => Or.inr h
case h.inr
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 → Quot.mk r <$> dest x = Quot.mk r <$> dest y
r' : Cofix F → Cofix F → Prop := fun x y => x = y ∨ r x y
x✝ y✝ : Cofix F
rxy : r x✝ y✝
x y : Cofix F
r'xy : r x y
this : ∀ (x y : Cofix F), r x y → r' x y
⊢ (Quot.factor (fun x y => r x y) (fun x y => r' x y) this ∘ Quot.mk fun x y => r x y) <$> dest x =
    (Quot.factor (fun x y => r x y) (fun x y => r' x y) this ∘ Quot.mk fun x y => r x y) <$> dest y
case h.inr
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 → Quot.mk r <$> dest x = Quot.mk r <$> dest y
r' : Cofix F → Cofix F → Prop := fun x y => x = y ∨ r x y
x✝ y✝ : Cofix F
rxy : r x✝ y✝
x y : Cofix F
r'xy : r x y
this : ∀ (x y : Cofix F), r x y → r' x y
⊢ Quot.mk r' <$> dest x = Quot.mk r' <$> dest y
rw [← Quot.factor_mk_eq _ _ this]
case h.inr
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 → Quot.mk r <$> dest x = Quot.mk r <$> dest y
r' : Cofix F → Cofix F → Prop := fun x y => x = y ∨ r x y
x✝ y✝ : Cofix F
rxy : r x✝ y✝
x y : Cofix F
r'xy : r x y
this : ∀ (x y : Cofix F), r x y → r' x y
⊢ (Quot.factor (fun x y => r x y) (fun x y => x = y ∨ r x y) this ∘ Quot.mk fun x y => r x y) <$> dest x =
    (Quot.factor (fun x y => r x y) (fun x y => x = y ∨ r x y) this ∘ Quot.mk fun x y => r x y) <$> dest y
case h.inr
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 → Quot.mk r <$> dest x = Quot.mk r <$> dest y
r' : Cofix F → Cofix F → Prop := fun x y => x = y ∨ r x y
x✝ y✝ : Cofix F
rxy : r x✝ y✝
x y : Cofix F
r'xy : r x y
this : ∀ (x y : Cofix F), r x y → r' x y
⊢ (Quot.factor (fun x y => r x y) (fun x y => r' x y) this ∘ Quot.mk fun x y => r x y) <$> dest x =
    (Quot.factor (fun x y => r x y) (fun x y => r' x y) this ∘ Quot.mk fun x y => r x y) <$> dest y
dsimp
case h.inr
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 → Quot.mk r <$> dest x = Quot.mk r <$> dest y
r' : Cofix F → Cofix F → Prop := fun x y => x = y ∨ r x y
x✝ y✝ : Cofix F
rxy : r x✝ y✝
x y : Cofix F
r'xy : r x y
this : ∀ (x y : Cofix F), r x y → r' x y
⊢ Quot.factor (fun x y => r x y) (fun x y => x = y ∨ r x y) this <$> Quot.mk r <$> dest x =
    Quot.factor (fun x y => r x y) (fun x y => x = y ∨ r x y) this <$> Quot.mk r <$> dest y
case h.inr
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 → Quot.mk r <$> dest x = Quot.mk r <$> dest y
r' : Cofix F → Cofix F → Prop := fun x y => x = y ∨ r x y
x✝ y✝ : Cofix F
rxy : r x✝ y✝
x y : Cofix F
r'xy : r x y
this : ∀ (x y : Cofix F), r x y → r' x y
⊢ (Quot.factor (fun x y => r x y) (fun x y => x = y ∨ r x y) this ∘ Quot.mk fun x y => r x y) <$> dest x =
    (Quot.factor (fun x y => r x y) (fun x y => x = y ∨ r x y) this ∘ Quot.mk fun x y => r x y) <$> dest y
rw [@comp_map _ _ q _ _ _ (Quot.mk r), @comp_map _ _ q _ _ _ (Quot.mk r)]
no goals
case h.inr
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 → Quot.mk r <$> dest x = Quot.mk r <$> dest y
r' : Cofix F → Cofix F → Prop := fun x y => x = y ∨ r x y
x✝ y✝ : Cofix F
rxy : r x✝ y✝
x y : Cofix F
r'xy : r x y
this : ∀ (x y : Cofix F), r x y → r' x y
⊢ Quot.factor (fun x y => r x y) (fun x y => x = y ∨ r x y) this <$> Quot.mk r <$> dest x =
    Quot.factor (fun x y => r x y) (fun x y => x = y ∨ r x y) this <$> Quot.mk r <$> dest y
rw [h _ _ r'xy]
no goals
case h.inl
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 → Quot.mk r <$> dest x = Quot.mk r <$> dest y
r' : Cofix F → Cofix F → Prop := fun x y => x = y ∨ r x y
x✝ y✝ : Cofix F
rxy : r x✝ y✝
x y : Cofix F
r'xy : x = y
⊢ Quot.mk r' <$> dest x = Quot.mk r' <$> dest y
rw [r'xy]