F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x : Cofix F
⊢ ∀ (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 : Cofix F), r x x
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
intro x
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x : Cofix F
⊢ ∀ (a : PFunctor.M (P F)) (y : Cofix F), r (Quot.mk Mcongr a) y → Quot.mk Mcongr a = y
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x : Cofix F
⊢ ∀ (y : Cofix F), r x y → x = y
apply Quot.inductionOn (motive := _) x
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
⊢ ∀ (a : PFunctor.M (P F)) (y : Cofix F), r (Quot.mk Mcongr a) y → Quot.mk Mcongr a = y
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x : Cofix F
⊢ ∀ (a : PFunctor.M (P F)) (y : Cofix F), r (Quot.mk Mcongr a) y → Quot.mk Mcongr a = y
clear x
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x : PFunctor.M (P F)
y : Cofix F
⊢ r (Quot.mk Mcongr x) y → Quot.mk Mcongr x = y
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
⊢ ∀ (a : PFunctor.M (P F)) (y : Cofix F), r (Quot.mk Mcongr a) y → Quot.mk Mcongr a = y
intro x y
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x : PFunctor.M (P F)
y : Cofix F
⊢ ∀ (a : PFunctor.M (P F)), r (Quot.mk Mcongr x) (Quot.mk Mcongr a) → Quot.mk Mcongr x = Quot.mk Mcongr a
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x : PFunctor.M (P F)
y : Cofix F
⊢ r (Quot.mk Mcongr x) y → Quot.mk Mcongr x = y
apply Quot.inductionOn (motive := _) y
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x : PFunctor.M (P F)
⊢ ∀ (a : PFunctor.M (P F)), r (Quot.mk Mcongr x) (Quot.mk Mcongr a) → Quot.mk Mcongr x = Quot.mk Mcongr a
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x : PFunctor.M (P F)
y : Cofix F
⊢ ∀ (a : PFunctor.M (P F)), r (Quot.mk Mcongr x) (Quot.mk Mcongr a) → Quot.mk Mcongr x = Quot.mk Mcongr a
clear y
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x y : PFunctor.M (P F)
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
⊢ Quot.mk Mcongr x = Quot.mk Mcongr y
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x : PFunctor.M (P F)
⊢ ∀ (a : PFunctor.M (P F)), r (Quot.mk Mcongr x) (Quot.mk Mcongr a) → Quot.mk Mcongr x = Quot.mk Mcongr a
intro y rxy
case a
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x y : PFunctor.M (P F)
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
⊢ Mcongr x y
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x y : PFunctor.M (P F)
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
⊢ Quot.mk Mcongr x = Quot.mk Mcongr y
apply Quot.sound
case a
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x y : PFunctor.M (P F)
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : PFunctor.M (P F) → PFunctor.M (P F) → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
⊢ Mcongr x y
case a
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x y : PFunctor.M (P F)
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
⊢ Mcongr x y
let r' x y := r (Quot.mk _ x) (Quot.mk _ y)
case a
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x y : PFunctor.M (P F)
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : PFunctor.M (P F) → PFunctor.M (P F) → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
this : IsPrecongr r'
⊢ Mcongr x y
case a
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x y : PFunctor.M (P F)
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : PFunctor.M (P F) → PFunctor.M (P F) → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
⊢ Mcongr x y
have : IsPrecongr r' := by
  intro a b r'ab
  have h₀ :
    Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest a) =
      Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest b) :=
    h _ _ r'ab
  have h₁ : ∀ u v : q.P.M, Mcongr u v → Quot.mk r' u = Quot.mk r' v := by
    intro u v cuv
    apply Quot.sound
    simp only
    rw [Quot.sound cuv]
    apply h'
  let f : Quot r → Quot r' :=
    Quot.lift (Quot.lift (Quot.mk r') h₁)
      (by
        intro c; apply Quot.inductionOn (motive := _) c; clear c
        intro c d; apply Quot.inductionOn (motive := _) d; clear d
        intro d rcd; apply Quot.sound; apply rcd)
  have : f ∘ Quot.mk r ∘ Quot.mk Mcongr = Quot.mk r' := rfl
  rw [← this, PFunctor.comp_map _ _ f, PFunctor.comp_map _ _ (Quot.mk r), abs_map, abs_map,
    abs_map, h₀]
  rw [PFunctor.comp_map _ _ f, PFunctor.comp_map _ _ (Quot.mk r), abs_map, abs_map, abs_map]
no goals
case a
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x y : PFunctor.M (P F)
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : PFunctor.M (P F) → PFunctor.M (P F) → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
this : IsPrecongr r'
⊢ Mcongr x y
refine' ⟨r', this, rxy⟩
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x y : PFunctor.M (P F)
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : PFunctor.M (P F) → PFunctor.M (P F) → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : PFunctor.M (P F)
r'ab : r' a b
⊢ abs (Quot.mk r' <$> PFunctor.M.dest a) = abs (Quot.mk r' <$> PFunctor.M.dest b)
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x y : PFunctor.M (P F)
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : PFunctor.M (P F) → PFunctor.M (P F) → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
⊢ IsPrecongr r'
intro a b r'ab
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x y : PFunctor.M (P F)
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : PFunctor.M (P F) → PFunctor.M (P F) → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : PFunctor.M (P F)
r'ab : r' a b
h₀ : Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest a) = Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest b)
⊢ abs (Quot.mk r' <$> PFunctor.M.dest a) = abs (Quot.mk r' <$> PFunctor.M.dest b)
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x y : PFunctor.M (P F)
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : PFunctor.M (P F) → PFunctor.M (P F) → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : PFunctor.M (P F)
r'ab : r' a b
⊢ abs (Quot.mk r' <$> PFunctor.M.dest a) = abs (Quot.mk r' <$> PFunctor.M.dest b)
have h₀ :
  Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest a) =
    Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest b) :=
  h _ _ r'ab
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x y : PFunctor.M (P F)
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : PFunctor.M (P F) → PFunctor.M (P F) → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : PFunctor.M (P F)
r'ab : r' a b
h₀ : Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest a) = Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest b)
h₁ : ∀ (u v : PFunctor.M (P F)), Mcongr u v → Quot.mk r' u = Quot.mk r' v
⊢ abs (Quot.mk r' <$> PFunctor.M.dest a) = abs (Quot.mk r' <$> PFunctor.M.dest b)
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x y : PFunctor.M (P F)
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : PFunctor.M (P F) → PFunctor.M (P F) → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : PFunctor.M (P F)
r'ab : r' a b
h₀ : Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest a) = Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest b)
⊢ abs (Quot.mk r' <$> PFunctor.M.dest a) = abs (Quot.mk r' <$> PFunctor.M.dest b)
have h₁ : ∀ u v : q.P.M, Mcongr u v → Quot.mk r' u = Quot.mk r' v := by
  intro u v cuv
  apply Quot.sound
  simp only
  rw [Quot.sound cuv]
  apply h'
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x y : PFunctor.M (P F)
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : PFunctor.M (P F) → PFunctor.M (P F) → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : PFunctor.M (P F)
r'ab : r' a b
h₀ : Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest a) = Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest b)
h₁ : ∀ (u v : PFunctor.M (P F)), Mcongr u v → Quot.mk r' u = Quot.mk r' v
f : Quot r → Quot r' :=
  Quot.lift (Quot.lift (Quot.mk r') h₁)
    (_ : ∀ (c b : Cofix F), r c b → Quot.lift (Quot.mk r') h₁ c = Quot.lift (Quot.mk r') h₁ b)
⊢ abs (Quot.mk r' <$> PFunctor.M.dest a) = abs (Quot.mk r' <$> PFunctor.M.dest b)
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x y : PFunctor.M (P F)
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : PFunctor.M (P F) → PFunctor.M (P F) → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : PFunctor.M (P F)
r'ab : r' a b
h₀ : Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest a) = Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest b)
h₁ : ∀ (u v : PFunctor.M (P F)), Mcongr u v → Quot.mk r' u = Quot.mk r' v
⊢ abs (Quot.mk r' <$> PFunctor.M.dest a) = abs (Quot.mk r' <$> PFunctor.M.dest b)
let f : Quot r → Quot r' :=
  Quot.lift (Quot.lift (Quot.mk r') h₁)
    (by
      intro c; apply Quot.inductionOn (motive := _) c; clear c
      intro c d; apply Quot.inductionOn (motive := _) d; clear d
      intro d rcd; apply Quot.sound; apply rcd)
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x y : PFunctor.M (P F)
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : PFunctor.M (P F) → PFunctor.M (P F) → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : PFunctor.M (P F)
r'ab : r' a b
h₀ : Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest a) = Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest b)
h₁ : ∀ (u v : PFunctor.M (P F)), Mcongr u v → Quot.mk r' u = Quot.mk r' v
f : Quot r → Quot r' :=
  Quot.lift (Quot.lift (Quot.mk r') h₁)
    (_ : ∀ (c b : Cofix F), r c b → Quot.lift (Quot.mk r') h₁ c = Quot.lift (Quot.mk r') h₁ b)
this : f ∘ Quot.mk r ∘ Quot.mk Mcongr = Quot.mk r'
⊢ abs (Quot.mk r' <$> PFunctor.M.dest a) = abs (Quot.mk r' <$> PFunctor.M.dest b)
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x y : PFunctor.M (P F)
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : PFunctor.M (P F) → PFunctor.M (P F) → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : PFunctor.M (P F)
r'ab : r' a b
h₀ : Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest a) = Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest b)
h₁ : ∀ (u v : PFunctor.M (P F)), Mcongr u v → Quot.mk r' u = Quot.mk r' v
f : Quot r → Quot r' :=
  Quot.lift (Quot.lift (Quot.mk r') h₁)
    (_ : ∀ (c b : Cofix F), r c b → Quot.lift (Quot.mk r') h₁ c = Quot.lift (Quot.mk r') h₁ b)
⊢ abs (Quot.mk r' <$> PFunctor.M.dest a) = abs (Quot.mk r' <$> PFunctor.M.dest b)
have : f ∘ Quot.mk r ∘ Quot.mk Mcongr = Quot.mk r' := rfl
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x y : PFunctor.M (P F)
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : PFunctor.M (P F) → PFunctor.M (P F) → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : PFunctor.M (P F)
r'ab : r' a b
h₀ : Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest a) = Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest b)
h₁ : ∀ (u v : PFunctor.M (P F)), Mcongr u v → Quot.mk r' u = Quot.mk r' v
f : Quot r → Quot r' :=
  Quot.lift (Quot.lift (Quot.mk r') h₁)
    (_ : ∀ (c b : Cofix F), r c b → Quot.lift (Quot.mk r') h₁ c = Quot.lift (Quot.mk r') h₁ b)
this : f ∘ Quot.mk r ∘ Quot.mk Mcongr = Quot.mk r'
⊢ f <$> Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest b) =
    abs ((f ∘ Quot.mk r ∘ Quot.mk Mcongr) <$> PFunctor.M.dest b)
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x y : PFunctor.M (P F)
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : PFunctor.M (P F) → PFunctor.M (P F) → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : PFunctor.M (P F)
r'ab : r' a b
h₀ : Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest a) = Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest b)
h₁ : ∀ (u v : PFunctor.M (P F)), Mcongr u v → Quot.mk r' u = Quot.mk r' v
f : Quot r → Quot r' :=
  Quot.lift (Quot.lift (Quot.mk r') h₁)
    (_ : ∀ (c b : Cofix F), r c b → Quot.lift (Quot.mk r') h₁ c = Quot.lift (Quot.mk r') h₁ b)
this : f ∘ Quot.mk r ∘ Quot.mk Mcongr = Quot.mk r'
⊢ abs (Quot.mk r' <$> PFunctor.M.dest a) = abs (Quot.mk r' <$> PFunctor.M.dest b)
rw [← this, PFunctor.comp_map _ _ f, PFunctor.comp_map _ _ (Quot.mk r), abs_map, abs_map,
  abs_map, h₀]
no goals
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x y : PFunctor.M (P F)
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : PFunctor.M (P F) → PFunctor.M (P F) → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : PFunctor.M (P F)
r'ab : r' a b
h₀ : Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest a) = Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest b)
h₁ : ∀ (u v : PFunctor.M (P F)), Mcongr u v → Quot.mk r' u = Quot.mk r' v
f : Quot r → Quot r' :=
  Quot.lift (Quot.lift (Quot.mk r') h₁)
    (_ : ∀ (c b : Cofix F), r c b → Quot.lift (Quot.mk r') h₁ c = Quot.lift (Quot.mk r') h₁ b)
this : f ∘ Quot.mk r ∘ Quot.mk Mcongr = Quot.mk r'
⊢ f <$> Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest b) =
    abs ((f ∘ Quot.mk r ∘ Quot.mk Mcongr) <$> PFunctor.M.dest b)
rw [PFunctor.comp_map _ _ f, PFunctor.comp_map _ _ (Quot.mk r), abs_map, abs_map, abs_map]
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x y : PFunctor.M (P F)
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : PFunctor.M (P F) → PFunctor.M (P F) → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : PFunctor.M (P F)
r'ab : r' a b
h₀ : Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest a) = Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest b)
u v : PFunctor.M (P F)
cuv : Mcongr u v
⊢ Quot.mk r' u = Quot.mk r' v
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x y : PFunctor.M (P F)
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : PFunctor.M (P F) → PFunctor.M (P F) → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : PFunctor.M (P F)
r'ab : r' a b
h₀ : Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest a) = Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest b)
⊢ ∀ (u v : PFunctor.M (P F)), Mcongr u v → Quot.mk r' u = Quot.mk r' v
intro u v cuv
case a
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x y : PFunctor.M (P F)
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : PFunctor.M (P F) → PFunctor.M (P F) → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : PFunctor.M (P F)
r'ab : r' a b
h₀ : Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest a) = Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest b)
u v : PFunctor.M (P F)
cuv : Mcongr u v
⊢ r' u v
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x y : PFunctor.M (P F)
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : PFunctor.M (P F) → PFunctor.M (P F) → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : PFunctor.M (P F)
r'ab : r' a b
h₀ : Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest a) = Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest b)
u v : PFunctor.M (P F)
cuv : Mcongr u v
⊢ Quot.mk r' u = Quot.mk r' v
apply Quot.sound
case a
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x y : PFunctor.M (P F)
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : PFunctor.M (P F) → PFunctor.M (P F) → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : PFunctor.M (P F)
r'ab : r' a b
h₀ : Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest a) = Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest b)
u v : PFunctor.M (P F)
cuv : Mcongr u v
⊢ r (Quot.mk Mcongr u) (Quot.mk Mcongr v)
case a
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x y : PFunctor.M (P F)
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : PFunctor.M (P F) → PFunctor.M (P F) → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : PFunctor.M (P F)
r'ab : r' a b
h₀ : Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest a) = Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest b)
u v : PFunctor.M (P F)
cuv : Mcongr u v
⊢ r' u v
simp only
case a
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x y : PFunctor.M (P F)
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : PFunctor.M (P F) → PFunctor.M (P F) → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : PFunctor.M (P F)
r'ab : r' a b
h₀ : Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest a) = Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest b)
u v : PFunctor.M (P F)
cuv : Mcongr u v
⊢ r (Quot.mk Mcongr v) (Quot.mk Mcongr v)
case a
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x y : PFunctor.M (P F)
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : PFunctor.M (P F) → PFunctor.M (P F) → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : PFunctor.M (P F)
r'ab : r' a b
h₀ : Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest a) = Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest b)
u v : PFunctor.M (P F)
cuv : Mcongr u v
⊢ r (Quot.mk Mcongr u) (Quot.mk Mcongr v)
rw [Quot.sound cuv]
no goals
case a
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x y : PFunctor.M (P F)
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : PFunctor.M (P F) → PFunctor.M (P F) → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : PFunctor.M (P F)
r'ab : r' a b
h₀ : Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest a) = Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest b)
u v : PFunctor.M (P F)
cuv : Mcongr u v
⊢ r (Quot.mk Mcongr v) (Quot.mk Mcongr v)
apply h'
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x y : PFunctor.M (P F)
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : PFunctor.M (P F) → PFunctor.M (P F) → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : PFunctor.M (P F)
r'ab : r' a b
h₀ : Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest a) = Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest b)
h₁ : ∀ (u v : PFunctor.M (P F)), Mcongr u v → Quot.mk r' u = Quot.mk r' v
c : Cofix F
⊢ ∀ (b : Cofix F), r c b → Quot.lift (Quot.mk r') h₁ c = Quot.lift (Quot.mk r') h₁ b
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x y : PFunctor.M (P F)
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : PFunctor.M (P F) → PFunctor.M (P F) → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : PFunctor.M (P F)
r'ab : r' a b
h₀ : Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest a) = Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest b)
h₁ : ∀ (u v : PFunctor.M (P F)), Mcongr u v → Quot.mk r' u = Quot.mk r' v
⊢ ∀ (a b : Cofix F), r a b → Quot.lift (Quot.mk r') h₁ a = Quot.lift (Quot.mk r') h₁ b
intro c
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x y : PFunctor.M (P F)
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : PFunctor.M (P F) → PFunctor.M (P F) → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : PFunctor.M (P F)
r'ab : r' a b
h₀ : Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest a) = Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest b)
h₁ : ∀ (u v : PFunctor.M (P F)), Mcongr u v → Quot.mk r' u = Quot.mk r' v
c : Cofix F
⊢ ∀ (a : PFunctor.M (P F)) (b : Cofix F),
    r (Quot.mk Mcongr a) b → Quot.lift (Quot.mk r') h₁ (Quot.mk Mcongr a) = Quot.lift (Quot.mk r') h₁ b
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x y : PFunctor.M (P F)
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : PFunctor.M (P F) → PFunctor.M (P F) → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : PFunctor.M (P F)
r'ab : r' a b
h₀ : Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest a) = Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest b)
h₁ : ∀ (u v : PFunctor.M (P F)), Mcongr u v → Quot.mk r' u = Quot.mk r' v
c : Cofix F
⊢ ∀ (b : Cofix F), r c b → Quot.lift (Quot.mk r') h₁ c = Quot.lift (Quot.mk r') h₁ b
apply Quot.inductionOn (motive := _) c
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x y : PFunctor.M (P F)
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : PFunctor.M (P F) → PFunctor.M (P F) → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : PFunctor.M (P F)
r'ab : r' a b
h₀ : Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest a) = Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest b)
h₁ : ∀ (u v : PFunctor.M (P F)), Mcongr u v → Quot.mk r' u = Quot.mk r' v
⊢ ∀ (a : PFunctor.M (P F)) (b : Cofix F),
    r (Quot.mk Mcongr a) b → Quot.lift (Quot.mk r') h₁ (Quot.mk Mcongr a) = Quot.lift (Quot.mk r') h₁ b
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x y : PFunctor.M (P F)
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : PFunctor.M (P F) → PFunctor.M (P F) → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : PFunctor.M (P F)
r'ab : r' a b
h₀ : Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest a) = Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest b)
h₁ : ∀ (u v : PFunctor.M (P F)), Mcongr u v → Quot.mk r' u = Quot.mk r' v
c : Cofix F
⊢ ∀ (a : PFunctor.M (P F)) (b : Cofix F),
    r (Quot.mk Mcongr a) b → Quot.lift (Quot.mk r') h₁ (Quot.mk Mcongr a) = Quot.lift (Quot.mk r') h₁ b
clear c
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x y : PFunctor.M (P F)
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : PFunctor.M (P F) → PFunctor.M (P F) → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : PFunctor.M (P F)
r'ab : r' a b
h₀ : Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest a) = Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest b)
h₁ : ∀ (u v : PFunctor.M (P F)), Mcongr u v → Quot.mk r' u = Quot.mk r' v
c : PFunctor.M (P F)
d : Cofix F
⊢ r (Quot.mk Mcongr c) d → Quot.lift (Quot.mk r') h₁ (Quot.mk Mcongr c) = Quot.lift (Quot.mk r') h₁ d
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x y : PFunctor.M (P F)
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : PFunctor.M (P F) → PFunctor.M (P F) → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : PFunctor.M (P F)
r'ab : r' a b
h₀ : Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest a) = Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest b)
h₁ : ∀ (u v : PFunctor.M (P F)), Mcongr u v → Quot.mk r' u = Quot.mk r' v
⊢ ∀ (a : PFunctor.M (P F)) (b : Cofix F),
    r (Quot.mk Mcongr a) b → Quot.lift (Quot.mk r') h₁ (Quot.mk Mcongr a) = Quot.lift (Quot.mk r') h₁ b
intro c d
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x y : PFunctor.M (P F)
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : PFunctor.M (P F) → PFunctor.M (P F) → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : PFunctor.M (P F)
r'ab : r' a b
h₀ : Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest a) = Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest b)
h₁ : ∀ (u v : PFunctor.M (P F)), Mcongr u v → Quot.mk r' u = Quot.mk r' v
c : PFunctor.M (P F)
d : Cofix F
⊢ ∀ (a : PFunctor.M (P F)),
    r (Quot.mk Mcongr c) (Quot.mk Mcongr a) →
      Quot.lift (Quot.mk r') h₁ (Quot.mk Mcongr c) = Quot.lift (Quot.mk r') h₁ (Quot.mk Mcongr a)
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x y : PFunctor.M (P F)
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : PFunctor.M (P F) → PFunctor.M (P F) → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : PFunctor.M (P F)
r'ab : r' a b
h₀ : Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest a) = Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest b)
h₁ : ∀ (u v : PFunctor.M (P F)), Mcongr u v → Quot.mk r' u = Quot.mk r' v
c : PFunctor.M (P F)
d : Cofix F
⊢ r (Quot.mk Mcongr c) d → Quot.lift (Quot.mk r') h₁ (Quot.mk Mcongr c) = Quot.lift (Quot.mk r') h₁ d
apply Quot.inductionOn (motive := _) d
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x y : PFunctor.M (P F)
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : PFunctor.M (P F) → PFunctor.M (P F) → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : PFunctor.M (P F)
r'ab : r' a b
h₀ : Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest a) = Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest b)
h₁ : ∀ (u v : PFunctor.M (P F)), Mcongr u v → Quot.mk r' u = Quot.mk r' v
c : PFunctor.M (P F)
⊢ ∀ (a : PFunctor.M (P F)),
    r (Quot.mk Mcongr c) (Quot.mk Mcongr a) →
      Quot.lift (Quot.mk r') h₁ (Quot.mk Mcongr c) = Quot.lift (Quot.mk r') h₁ (Quot.mk Mcongr a)
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x y : PFunctor.M (P F)
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : PFunctor.M (P F) → PFunctor.M (P F) → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : PFunctor.M (P F)
r'ab : r' a b
h₀ : Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest a) = Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest b)
h₁ : ∀ (u v : PFunctor.M (P F)), Mcongr u v → Quot.mk r' u = Quot.mk r' v
c : PFunctor.M (P F)
d : Cofix F
⊢ ∀ (a : PFunctor.M (P F)),
    r (Quot.mk Mcongr c) (Quot.mk Mcongr a) →
      Quot.lift (Quot.mk r') h₁ (Quot.mk Mcongr c) = Quot.lift (Quot.mk r') h₁ (Quot.mk Mcongr a)
clear d
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x y : PFunctor.M (P F)
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : PFunctor.M (P F) → PFunctor.M (P F) → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : PFunctor.M (P F)
r'ab : r' a b
h₀ : Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest a) = Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest b)
h₁ : ∀ (u v : PFunctor.M (P F)), Mcongr u v → Quot.mk r' u = Quot.mk r' v
c d : PFunctor.M (P F)
rcd : r (Quot.mk Mcongr c) (Quot.mk Mcongr d)
⊢ Quot.lift (Quot.mk r') h₁ (Quot.mk Mcongr c) = Quot.lift (Quot.mk r') h₁ (Quot.mk Mcongr d)
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x y : PFunctor.M (P F)
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : PFunctor.M (P F) → PFunctor.M (P F) → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : PFunctor.M (P F)
r'ab : r' a b
h₀ : Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest a) = Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest b)
h₁ : ∀ (u v : PFunctor.M (P F)), Mcongr u v → Quot.mk r' u = Quot.mk r' v
c : PFunctor.M (P F)
⊢ ∀ (a : PFunctor.M (P F)),
    r (Quot.mk Mcongr c) (Quot.mk Mcongr a) →
      Quot.lift (Quot.mk r') h₁ (Quot.mk Mcongr c) = Quot.lift (Quot.mk r') h₁ (Quot.mk Mcongr a)
intro d rcd
case a
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x y : PFunctor.M (P F)
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : PFunctor.M (P F) → PFunctor.M (P F) → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : PFunctor.M (P F)
r'ab : r' a b
h₀ : Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest a) = Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest b)
h₁ : ∀ (u v : PFunctor.M (P F)), Mcongr u v → Quot.mk r' u = Quot.mk r' v
c d : PFunctor.M (P F)
rcd : r (Quot.mk Mcongr c) (Quot.mk Mcongr d)
⊢ r' c d
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x y : PFunctor.M (P F)
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : PFunctor.M (P F) → PFunctor.M (P F) → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : PFunctor.M (P F)
r'ab : r' a b
h₀ : Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest a) = Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest b)
h₁ : ∀ (u v : PFunctor.M (P F)), Mcongr u v → Quot.mk r' u = Quot.mk r' v
c d : PFunctor.M (P F)
rcd : r (Quot.mk Mcongr c) (Quot.mk Mcongr d)
⊢ Quot.lift (Quot.mk r') h₁ (Quot.mk Mcongr c) = Quot.lift (Quot.mk r') h₁ (Quot.mk Mcongr d)
apply Quot.sound
no goals
case a
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> dest x = Quot.mk r <$> dest y
x y : PFunctor.M (P F)
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : PFunctor.M (P F) → PFunctor.M (P F) → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : PFunctor.M (P F)
r'ab : r' a b
h₀ : Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest a) = Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest b)
h₁ : ∀ (u v : PFunctor.M (P F)), Mcongr u v → Quot.mk r' u = Quot.mk r' v
c d : PFunctor.M (P F)
rcd : r (Quot.mk Mcongr c) (Quot.mk Mcongr d)
⊢ r' c d
apply rcd