-- Mathlib/Data/QPF/Multivariate/Constructions/Cofix.lean
theorem Cofix.bisim_aux {α : TypeVec n} (r : Cofix F α → Cofix F α → Prop) (h' : ∀ x, r x x)
    (h : ∀ x y, r x y →
      appendFun id (Quot.mk r) <$$> Cofix.dest x = appendFun id (Quot.mk r) <$$> Cofix.dest y) :
    ∀ x y, r x y → x = y

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
x y : (P F).M α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : (P F).M α → (P F).M α → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : (P F).M α
r'ab : r' a b
h₀ :
  (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a) =
    (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) b)
h₁ : ∀ (u v : (P F).M α), Mcongr u v → Quot.mk r' u = Quot.mk r' v
f : Quot r → Quot r' := Quot.lift (Quot.lift (Quot.mk r') h₁) ⋯
⊢ MvQPF.abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) a) =
    MvQPF.abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) b)

Tactic:
have : f ∘ Quot.mk r ∘ Quot.mk Mcongr = Quot.mk r' := rfl

Result:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
x y : (P F).M α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : (P F).M α → (P F).M α → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : (P F).M α
r'ab : r' a b
h₀ :
  (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a) =
    (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) b)
h₁ : ∀ (u v : (P F).M α), Mcongr u v → Quot.mk r' u = Quot.mk r' v
f : Quot r → Quot r' := Quot.lift (Quot.lift (Quot.mk r') h₁) ⋯
this : f ∘ Quot.mk r ∘ Quot.mk Mcongr = Quot.mk r'
⊢ MvQPF.abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) a) =
    MvQPF.abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) b)

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
x y : (P F).M α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : (P F).M α → (P F).M α → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : (P F).M α
r'ab : r' a b
h₀ :
  (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a) =
    (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) b)
h₁ : ∀ (u v : (P F).M α), Mcongr u v → Quot.mk r' u = Quot.mk r' v
c : (P F).M α
⊢ ∀ (a : (P F).M α),
    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)

Tactic:
intro d rcd

Result:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
x y : (P F).M α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : (P F).M α → (P F).M α → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : (P F).M α
r'ab : r' a b
h₀ :
  (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a) =
    (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) b)
h₁ : ∀ (u v : (P F).M α), Mcongr u v → Quot.mk r' u = Quot.mk r' v
c d : (P F).M α
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)