awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x y : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr (F := F) (α := α) r
rxy : r x y
this : ∀ (x y : (P F).M α), r x y → Mcongr (F := F) (α := α) x y
conv :
  MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r (Mcongr (F := F) (α := α)) this ∘ Quot.mk r))
      (abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) x)) =
    MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r (Mcongr (F := F) (α := α)) this ∘ Quot.mk r))
      (abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) y))
conv₁ :
  MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r (Mcongr (F := F) (α := α)) this ∘ Quot.mk r))
      (abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) y)) =
    MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r (Mcongr (F := F) (α := α)) this ∘ Quot.mk r))
      (abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) y))
⊢ MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r (Mcongr (F := F) (α := α)) this ∘ Quot.mk r))
      (abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) x)) =
    MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r (Mcongr (F := F) (α := α)) this ∘ Quot.mk r))
      (abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) y))

Tactic:
conv =>
        lhs
        rw [appendFun_comp_id, comp_map, ← abs_map, pr rxy, abs_map, ← comp_map,
          ← appendFun_comp_id]

Premises used: MvQPF.comp_map, MvQPF.abs_map, TypeVec.appendFun_comp_id
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: β)
x : β
lhs : dest (F := F) (α := α) (corec (F := F) (α := α) g x)
| Eq (α := F (α ::: Cofix F α)) (dest (F := F) (α := α) (corec (F := F) (α := α) g x))
    (MvFunctor.map (F := F) (α := α ::: β) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (corec (F := F) (α := α) g)) (g x))

Tactic:
lhs
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: β)
x : β
rw :
  Quot.lift (r := Mcongr (F := F) (α := α))
    (fun (x : (P F).M α) ↦
      MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
        (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) x)))
    ⋯ (Quot.mk (Mcongr (F := F) (α := α)) (corecF (F := F) (α := α) g x))
| dest (F := F) (α := α) (corec (F := F) (α := α) g x)

Tactic:
rw [Cofix.dest, Cofix.corec]

Premises used: MvQPF.Cofix.corec, MvQPF.Cofix.dest
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: β)
x : β
rw :
  Quot.lift (r := Mcongr (F := F) (α := α))
    (fun (x : (P F).M α) ↦
      MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
        (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) x)))
    ⋯ (Quot.mk (Mcongr (F := F) (α := α)) (corecF (F := F) (α := α) g x))
| Eq (α := F (α ::: Cofix F α)) (dest (F := F) (α := α) (corec (F := F) (α := α) g x))
    (MvFunctor.map (F := F) (α := α ::: β) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (corec (F := F) (α := α) g)) (g x))

Tactic:
lhs
    rw [Cofix.dest, Cofix.corec]

Premises used: MvQPF.Cofix.corec, MvQPF.Cofix.dest
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: β)
x : β
conv :
  Eq (α := F (α ::: Cofix F α))
    (Quot.lift (r := Mcongr (F := F) (α := α))
      (fun (x : (P F).M α) ↦
        MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
          (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) x)))
      ⋯ (Quot.mk (Mcongr (F := F) (α := α)) (corecF (F := F) (α := α) g x)))
    (MvFunctor.map (F := F) (α := α ::: β) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (corec (F := F) (α := α) g)) (g x))
⊢ Eq (α := F (α ::: Cofix F α)) (dest (F := F) (α := α) (corec (F := F) (α := α) g x))
    (MvFunctor.map (F := F) (α := α ::: β) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (corec (F := F) (α := α) g)) (g x))

Tactic:
conv =>
    lhs
    rw [Cofix.dest, Cofix.corec]

Premises used: MvQPF.Cofix.corec, MvQPF.Cofix.dest
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: β)
x : β
dsimp :
  MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
      (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) (corecF (F := F) (α := α) g x))) =
    MvFunctor.map (F := F) (α := α ::: β) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (corec (F := F) (α := α) g)) (g x)
⊢ Eq (α := F (α ::: Cofix F α))
    (Quot.lift (r := Mcongr (F := F) (α := α))
      (fun (x : (P F).M α) ↦
        MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
          (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) x)))
      ⋯ (Quot.mk (Mcongr (F := F) (α := α)) (corecF (F := F) (α := α) g x)))
    (MvFunctor.map (F := F) (α := α ::: β) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (corec (F := F) (α := α) g)) (g x))

Tactic:
dsimp
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: β)
x : β
rw :
  Eq (α := F (α ::: Cofix F α))
    (MvFunctor.map (F := F) (α := α ::: β) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α)
        (TypeVec.comp (α := α) (β := α) (γ := α) (TypeVec.id (α := α)) (TypeVec.id (α := α)))
        (Quot.mk (Mcongr (F := F) (α := α)) ∘ corecF (F := F) (α := α) g))
      (g x))
    (MvFunctor.map (F := F) (α := α ::: β) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (corec (F := F) (α := α) g)) (g x))
⊢ MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
      (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) (corecF (F := F) (α := α) g x))) =
    MvFunctor.map (F := F) (α := α ::: β) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (corec (F := F) (α := α) g)) (g x)

Tactic:
rw [corecF_eq, abs_map, abs_repr, ← comp_map, ← appendFun_comp]

Premises used: MvQPF.comp_map, MvQPF.abs_repr, TypeVec.appendFun_comp, MvQPF.abs_map, MvQPF.corecF_eq
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: β)
x : β
⊢ Eq (α := F (α ::: Cofix F α))
    (MvFunctor.map (F := F) (α := α ::: β) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α)
        (TypeVec.comp (α := α) (β := α) (γ := α) (TypeVec.id (α := α)) (TypeVec.id (α := α)))
        (Quot.mk (Mcongr (F := F) (α := α)) ∘ corecF (F := F) (α := α) g))
      (g x))
    (MvFunctor.map (F := F) (α := α ::: β) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (corec (F := F) (α := α) g)) (g x))

Tactic:
rfl
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
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 →
      MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (x.dest (F := F) (α := α)) =
        MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (y.dest (F := F) (α := α))
x : Cofix F α
mk :
  ∀ (a : (P F).M α) (y : Cofix F α),
    r (Quot.mk (Mcongr (F := F) (α := α)) a) y → Quot.mk (Mcongr (F := F) (α := α)) a = y
⊢ ∀ (y : Cofix F α), r x y → x = y

Tactic:
rcases x
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
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 →
      MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (x.dest (F := F) (α := α)) =
        MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (y.dest (F := F) (α := α))
x : (P F).M α
y : Cofix F α
mk :
  ∀ (a : (P F).M α),
    r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) a) →
      Eq (α := Cofix F α) (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) a)
⊢ r (Quot.mk (Mcongr (F := F) (α := α)) x) y → Quot.mk (Mcongr (F := F) (α := α)) x = y

Tactic:
rcases y
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
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 →
      MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (x.dest (F := F) (α := α)) =
        MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (y.dest (F := F) (α := α))
x y : (P F).M α
rxy : r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
mk : Mcongr (F := F) (α := α) x y
⊢ Eq (α := Cofix F α) (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)

Tactic:
apply Quot.sound

Premises used: Quot.sound
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
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 →
      MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (x.dest (F := F) (α := α)) =
        MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (y.dest (F := F) (α := α))
x y : (P F).M α
rxy : r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
r' : (x y : (P F).M α) → Prop :=
  fun (x y : (P F).M α) ↦ r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
⊢ r' = fun (x y : (P F).M α) ↦ r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)

Tactic:
have hr' : r' = fun x y => r (Quot.mk _ x) (Quot.mk _ y) := rfl
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
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 →
      MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (x.dest (F := F) (α := α)) =
        MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (y.dest (F := F) (α := α))
x y : (P F).M α
rxy : r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
r' : (x y : (P F).M α) → Prop :=
  fun (x y : (P F).M α) ↦ r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
hr' : r' = fun (x y : (P F).M α) ↦ r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
a b : (P F).M α
r'ab : r' a b
rw :
  MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r))
      (MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
        (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) a))) =
    MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r))
      (MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
        (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) b)))
⊢ MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Quot r)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r ∘ Quot.mk (Mcongr (F := F) (α := α))))
      (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) a)) =
    MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Quot r)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r ∘ Quot.mk (Mcongr (F := F) (α := α))))
      (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) b))

Tactic:
rw [appendFun_comp_id, comp_map, comp_map]

Premises used: MvQPF.comp_map, TypeVec.appendFun_comp_id
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
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 →
      MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (x.dest (F := F) (α := α)) =
        MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (y.dest (F := F) (α := α))
x y : (P F).M α
rxy : r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
r' : (x y : (P F).M α) → Prop :=
  fun (x y : (P F).M α) ↦ r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
hr' : r' = fun (x y : (P F).M α) ↦ r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
a b : (P F).M α
r'ab : r' a b
⊢ MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r))
      (MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
        (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) a))) =
    MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r))
      (MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
        (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) b)))

Tactic:
h _ _ r'ab

Premises used: MvQPF.Cofix.dest
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
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 →
      MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (x.dest (F := F) (α := α)) =
        MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (y.dest (F := F) (α := α))
x y : (P F).M α
rxy : r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
r' : (x y : (P F).M α) → Prop :=
  fun (x y : (P F).M α) ↦ r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
hr' : r' = fun (x y : (P F).M α) ↦ r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
a b : (P F).M α
r'ab : r' a b
⊢ MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r))
      (MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
        (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) a))) =
    MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r))
      (MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
        (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) b)))

Tactic:
exact h _ _ r'ab
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
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 →
      MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (x.dest (F := F) (α := α)) =
        MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (y.dest (F := F) (α := α))
x y : (P F).M α
rxy : r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
r' : (x y : (P F).M α) → Prop :=
  fun (x y : (P F).M α) ↦ r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
hr' : r' = fun (x y : (P F).M α) ↦ r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
a b : (P F).M α
r'ab : r' a b
⊢ MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Quot r)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r ∘ Quot.mk (Mcongr (F := F) (α := α))))
      (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) a)) =
    MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Quot r)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r ∘ Quot.mk (Mcongr (F := F) (α := α))))
      (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) b))

Tactic:
have h₀ :
      appendFun id (Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest q.P a) =
        appendFun id (Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest q.P b) := by
      rw [appendFun_comp_id, comp_map, comp_map]; exact h _ _ r'ab
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
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 →
      MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (x.dest (F := F) (α := α)) =
        MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (y.dest (F := F) (α := α))
x y : (P F).M α
rxy : r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
r' : (x y : (P F).M α) → Prop :=
  fun (x y : (P F).M α) ↦ r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
hr' : r' = fun (x y : (P F).M α) ↦ r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
a b : (P F).M α
r'ab : r' a b
h₀ :
  MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Quot r)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r ∘ Quot.mk (Mcongr (F := F) (α := α))))
      (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) a)) =
    MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Quot r)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r ∘ Quot.mk (Mcongr (F := F) (α := α))))
      (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) b))
u v : (P F).M α
cuv : Mcongr (F := F) (α := α) u v
a₁ : r' u v
⊢ Quot.mk r' u = Quot.mk r' v

Tactic:
apply Quot.sound

Premises used: Quot.sound
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
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 →
      MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (x.dest (F := F) (α := α)) =
        MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (y.dest (F := F) (α := α))
x y : (P F).M α
rxy : r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
r' : (x y : (P F).M α) → Prop :=
  fun (x y : (P F).M α) ↦ r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
hr' : r' = fun (x y : (P F).M α) ↦ r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
a b : (P F).M α
r'ab : r' a b
h₀ :
  MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Quot r)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r ∘ Quot.mk (Mcongr (F := F) (α := α))))
      (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) a)) =
    MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Quot r)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r ∘ Quot.mk (Mcongr (F := F) (α := α))))
      (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) b))
u v : (P F).M α
cuv : Mcongr (F := F) (α := α) u v
a₁ : r (Quot.mk (Mcongr (F := F) (α := α)) u) (Quot.mk (Mcongr (F := F) (α := α)) v)
⊢ r' u v

Tactic:
dsimp [r', hr']