-- Mathlib/Data/QPF/Univariate/Basic.lean
theorem Cofix.bisim_rel (r : Cofix F → Cofix F → Prop)
    (h : ∀ x y, r x y → Quot.mk r <$> Cofix.dest x = Quot.mk r <$> Cofix.dest y) :
    ∀ x y, r x y → x = y

Proof state:
case h'
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
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

Tactic:
intro x

Result:
case h'
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
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

Proof state:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : Cofix F → Cofix F → Prop := fun x y => x = y ∨ r x y
⊢ ∀ (x y : Cofix F), r x y → x = y

Tactic:
intro x y rxy

Result:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : Cofix F → Cofix F → Prop := fun x y => x = y ∨ r x y
x y : Cofix F
rxy : r x y
⊢ x = y

Proof state:
case h
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
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' <$> x.dest = Quot.mk r' <$> y.dest

Tactic:
rcases r'xy with r'xy | r'xy

Result:
case h.inl
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
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' <$> x.dest = Quot.mk r' <$> y.dest

case h.inr
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
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' <$> x.dest = Quot.mk r' <$> y.dest

Proof state:
case h'
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
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

Tactic:
left

Result:
case h'.h
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
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

Proof state:
case h.inr
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
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 r (fun x y => x = y ∨ r x y) this <$> Quot.mk r <$> x.dest =
    Quot.factor r (fun x y => x = y ∨ r x y) this <$> Quot.mk r <$> y.dest

Tactic:
rw [h _ _ r'xy]

Result:
no goals

Proof state:
case a
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
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

Tactic:
right

Result:
case a.h
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
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

Proof state:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : Cofix F → Cofix F → Prop := fun x y => x = y ∨ r x y
x y : Cofix F
rxy : r x y
⊢ x = y

Tactic:
apply Cofix.bisim_aux r'

Result:
case h'
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
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
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
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' <$> x.dest = Quot.mk r' <$> y.dest

case a
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
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

Proof state:
case h.inr
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
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 r r' this ∘ Quot.mk r) <$> x.dest = (Quot.factor r r' this ∘ Quot.mk r) <$> y.dest

Tactic:
dsimp [r']

Result:
case h.inr
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
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 r (fun x y => x = y ∨ r x y) this ∘ Quot.mk r) <$> x.dest =
    (Quot.factor r (fun x y => x = y ∨ r x y) this ∘ Quot.mk r) <$> y.dest

Proof state:
case h.inr
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
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' <$> x.dest = Quot.mk r' <$> y.dest

Tactic:
rw [← Quot.factor_mk_eq _ _ this]

Result:
case h.inr
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
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 r r' this ∘ Quot.mk r) <$> x.dest = (Quot.factor r r' this ∘ Quot.mk r) <$> y.dest

Proof state:
case h.inl
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
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' <$> x.dest = Quot.mk r' <$> y.dest

Tactic:
rw [r'xy]

Result:
no goals

Proof state:
case a.h
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
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

Tactic:
exact rxy

Result:
no goals

Proof state:
case h.inr
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
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' <$> x.dest = Quot.mk r' <$> y.dest

Tactic:
have : ∀ x y, r x y → r' x y := fun x y h => Or.inr h

Result:
case h.inr
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
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' <$> x.dest = Quot.mk r' <$> y.dest