case intro.intro.intro.intro.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u_1
Q : α → Prop
u v : α → Cofix F
h :
  ∀ (x : α),
    Q x →
      ∃ a f f',
        dest (u x) = abs { fst := a, snd := f } ∧
          dest (v x) = abs { fst := a, snd := f' } ∧ ∀ (i : PFunctor.B (P F) a), ∃ x', Q x' ∧ f i = u x' ∧ f' i = v x'
x✝¹ : α
Qx : Q x✝¹
R : Cofix F → Cofix F → Prop := fun w z => ∃ x', Q x' ∧ w = u x' ∧ z = v x'
x y : Cofix F
x✝ : R x y
x' : α
Qx' : Q x'
xeq : x = u x'
yeq : y = v x'
a : (P F).A
f f' : PFunctor.B (P F) a → Cofix F
ux'eq : dest (u x') = abs { fst := a, snd := f }
vx'eq : dest (v x') = abs { fst := a, snd := f' }
h' : ∀ (i : PFunctor.B (P F) a), ∃ x', Q x' ∧ f i = u x' ∧ f' i = v x'
⊢ Liftr R (dest x) (dest y)
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u_1
Q : α → Prop
u v : α → Cofix F
h :
  ∀ (x : α),
    Q x →
      ∃ a f f',
        dest (u x) = abs { fst := a, snd := f } ∧
          dest (v x) = abs { fst := a, snd := f' } ∧ ∀ (i : PFunctor.B (P F) a), ∃ x', Q x' ∧ f i = u x' ∧ f' i = v x'
x✝¹ : α
Qx : Q x✝¹
R : Cofix F → Cofix F → Prop := fun w z => ∃ x', Q x' ∧ w = u x' ∧ z = v x'
x y : Cofix F
x✝ : R x y
x' : α
Qx' : Q x'
xeq : x = u x'
yeq : y = v x'
⊢ Liftr R (dest x) (dest y)
rcases h x' Qx' with ⟨a, f, f', ux'eq, vx'eq, h'⟩
case intro.intro.intro.intro.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u_1
Q : α → Prop
u v : α → Cofix F
h :
  ∀ (x : α),
    Q x →
      ∃ a f f',
        dest (u x) = abs { fst := a, snd := f } ∧
          dest (v x) = abs { fst := a, snd := f' } ∧ ∀ (i : PFunctor.B (P F) a), ∃ x', Q x' ∧ f i = u x' ∧ f' i = v x'
x✝¹ : α
Qx : Q x✝¹
R : Cofix F → Cofix F → Prop := fun w z => ∃ x', Q x' ∧ w = u x' ∧ z = v x'
x y : Cofix F
x✝ : R x y
x' : α
Qx' : Q x'
xeq : x = u x'
yeq : y = v x'
a : (P F).A
f f' : PFunctor.B (P F) a → Cofix F
ux'eq : dest (u x') = abs { fst := a, snd := f }
vx'eq : dest (v x') = abs { fst := a, snd := f' }
h' : ∀ (i : PFunctor.B (P F) a), ∃ x', Q x' ∧ f i = u x' ∧ f' i = v x'
⊢ ∃ a f₀ f₁,
    dest x = abs { fst := a, snd := f₀ } ∧
      dest y = abs { fst := a, snd := f₁ } ∧ ∀ (i : PFunctor.B (P F) a), R (f₀ i) (f₁ i)
case intro.intro.intro.intro.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u_1
Q : α → Prop
u v : α → Cofix F
h :
  ∀ (x : α),
    Q x →
      ∃ a f f',
        dest (u x) = abs { fst := a, snd := f } ∧
          dest (v x) = abs { fst := a, snd := f' } ∧ ∀ (i : PFunctor.B (P F) a), ∃ x', Q x' ∧ f i = u x' ∧ f' i = v x'
x✝¹ : α
Qx : Q x✝¹
R : Cofix F → Cofix F → Prop := fun w z => ∃ x', Q x' ∧ w = u x' ∧ z = v x'
x y : Cofix F
x✝ : R x y
x' : α
Qx' : Q x'
xeq : x = u x'
yeq : y = v x'
a : (P F).A
f f' : PFunctor.B (P F) a → Cofix F
ux'eq : dest (u x') = abs { fst := a, snd := f }
vx'eq : dest (v x') = abs { fst := a, snd := f' }
h' : ∀ (i : PFunctor.B (P F) a), ∃ x', Q x' ∧ f i = u x' ∧ f' i = v x'
⊢ Liftr R (dest x) (dest y)
rw [liftr_iff]
no goals
case intro.intro.intro.intro.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u_1
Q : α → Prop
u v : α → Cofix F
h :
  ∀ (x : α),
    Q x →
      ∃ a f f',
        dest (u x) = abs { fst := a, snd := f } ∧
          dest (v x) = abs { fst := a, snd := f' } ∧ ∀ (i : PFunctor.B (P F) a), ∃ x', Q x' ∧ f i = u x' ∧ f' i = v x'
x✝¹ : α
Qx : Q x✝¹
R : Cofix F → Cofix F → Prop := fun w z => ∃ x', Q x' ∧ w = u x' ∧ z = v x'
x y : Cofix F
x✝ : R x y
x' : α
Qx' : Q x'
xeq : x = u x'
yeq : y = v x'
a : (P F).A
f f' : PFunctor.B (P F) a → Cofix F
ux'eq : dest (u x') = abs { fst := a, snd := f }
vx'eq : dest (v x') = abs { fst := a, snd := f' }
h' : ∀ (i : PFunctor.B (P F) a), ∃ x', Q x' ∧ f i = u x' ∧ f' i = v x'
⊢ ∃ a f₀ f₁,
    dest x = abs { fst := a, snd := f₀ } ∧
      dest y = abs { fst := a, snd := f₁ } ∧ ∀ (i : PFunctor.B (P F) a), R (f₀ i) (f₁ i)
refine' ⟨a, f, f', xeq.symm ▸ ux'eq, yeq.symm ▸ vx'eq, h'⟩