cases y with | mk ny ky =>
let f : Quot r → Quot r' :=
  by
    apply Quot.lift (Quot.lift (Quot.mk r') _) _
    . intro a b h₃
      apply Quot.sound
      simp only
      rw [Quot.sound h₃]
      apply h₀
    . intro x; apply Quot.inductionOn (motive := _) x; clear x
      intro x y; apply Quot.inductionOn (motive := _) y; clear y
      intro y h
      apply Quot.sound
      apply h
have : f ∘ Quot.mk r ∘ Quot.mk (congr F) = Quot.mk r' := rfl
conv =>
  congr
  . rhs
    lhs
    intro i
    rw [←this]
    rfl
  . rhs
    lhs
    intro i
    rw [←this]
rw [Container.Map_spec, Container.Map_spec, Container.Map_spec, Container.Map_spec]
rw [inst.abs_map, inst.abs_map, inst.abs_map, inst.abs_map, inst.abs_map, inst.abs_map, h₂]
case a.a.mk
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝ y✝¹ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x y✝ : Container.M (C F)
h₂✝ : r' x y✝
y : Container.Obj (C F) (Container.M (C F))
nx : (C F).A
kx : Container.B (C F) nx → Container.M (C F)
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := nx, snd := kx } =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs y
⊢ abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) { fst := nx, snd := kx }) =
    abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) y)
no goals