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
r : Cofix F α → Cofix F α → Prop
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) (α := α))
r' : (x y : Cofix F α) → Prop := fun (x y : Cofix F α) ↦ x = y ∨ r x y
x_1 y_1 : Cofix F α
rxy : r x_1 y_1
x y : Cofix F α
r'xy : r x y
this : ∀ (x y : Cofix F α), r x y → r' x y
h₁ :
  MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r')
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r r' this ∘ Quot.mk r))
      (x.dest (F := F) (α := α)) =
    MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r')
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r r' this ∘ Quot.mk r))
      (y.dest (F := F) (α := α))
⊢ 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) (α := α))

Tactic:
rw [← Quot.factor_mk_eq _ _ this]

Premises used: Quot.factor_mk_eq
-- 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 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) (α := α))
r' : (x y : Cofix F α) → Prop := fun (x y : Cofix F α) ↦ x = y ∨ r x y
x_1 y_1 : Cofix F α
rxy : r x_1 y_1
x y : Cofix F α
r'xy : r x y
this : ∀ (x y : Cofix F α), r x y → r' x y
h₁ :
  MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot fun (x y : Cofix F α) ↦ x = y ∨ r x y)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
        (Quot.factor r (fun (x y : Cofix F α) ↦ x = y ∨ r x y) this ∘ Quot.mk r))
      (x.dest (F := F) (α := α)) =
    MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot fun (x y : Cofix F α) ↦ x = y ∨ r x y)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
        (Quot.factor r (fun (x y : Cofix F α) ↦ x = y ∨ r x y) this ∘ Quot.mk r))
      (y.dest (F := F) (α := α))
⊢ MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r')
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r r' this ∘ Quot.mk r))
      (x.dest (F := F) (α := α)) =
    MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r')
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r r' this ∘ Quot.mk r))
      (y.dest (F := F) (α := α))

Tactic:
dsimp [r']
-- 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 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) (α := α))
r' : (x y : Cofix F α) → Prop := fun (x y : Cofix F α) ↦ x = y ∨ r x y
x_1 y_1 : Cofix F α
rxy : r x_1 y_1
x y : Cofix F α
r'xy : r x y
this : ∀ (x y : Cofix F α), r x y → r' x y
h₁ :
  MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot fun (x y : Cofix F α) ↦ x = y ∨ r x y)
      (TypeVec.comp (α := α ::: Cofix F α) (β := α ::: Quot r) (γ := α ::: Quot fun (x y : Cofix F α) ↦ x = y ∨ r x y)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
          (Quot.factor r (fun (x y : Cofix F α) ↦ x = y ∨ r x y) this))
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)))
      (x.dest (F := F) (α := α)) =
    MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot fun (x y : Cofix F α) ↦ x = y ∨ r x y)
      (TypeVec.comp (α := α ::: Cofix F α) (β := α ::: Quot r) (γ := α ::: Quot fun (x y : Cofix F α) ↦ x = y ∨ r x y)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
          (Quot.factor r (fun (x y : Cofix F α) ↦ x = y ∨ r x y) this))
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)))
      (y.dest (F := F) (α := α))
⊢ MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot fun (x y : Cofix F α) ↦ x = y ∨ r x y)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
        (Quot.factor r (fun (x y : Cofix F α) ↦ x = y ∨ r x y) this ∘ Quot.mk r))
      (x.dest (F := F) (α := α)) =
    MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot fun (x y : Cofix F α) ↦ x = y ∨ r x y)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
        (Quot.factor r (fun (x y : Cofix F α) ↦ x = y ∨ r x y) this ∘ Quot.mk r))
      (y.dest (F := F) (α := α))

Tactic:
rw [appendFun_comp_id]

Premises used: 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 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) (α := α))
r' : (x y : Cofix F α) → Prop := fun (x y : Cofix F α) ↦ x = y ∨ r x y
x_1 y_1 : Cofix F α
rxy : r x_1 y_1
x y : Cofix F α
r'xy : r x y
this : ∀ (x y : Cofix F α), r x y → r' x y
h₁ :
  MvFunctor.map (F := F) (α := α ::: Quot r) (β := α ::: Quot fun (x y : Cofix F α) ↦ x = y ∨ r x y)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r (fun (x y : Cofix F α) ↦ x = y ∨ r x y) this))
      (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (x.dest (F := F) (α := α))) =
    MvFunctor.map (F := F) (α := α ::: Quot r) (β := α ::: Quot fun (x y : Cofix F α) ↦ x = y ∨ r x y)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r (fun (x y : Cofix F α) ↦ x = y ∨ r x y) this))
      (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (y.dest (F := F) (α := α)))
⊢ MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot fun (x y : Cofix F α) ↦ x = y ∨ r x y)
      (TypeVec.comp (α := α ::: Cofix F α) (β := α ::: Quot r) (γ := α ::: Quot fun (x y : Cofix F α) ↦ x = y ∨ r x y)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
          (Quot.factor r (fun (x y : Cofix F α) ↦ x = y ∨ r x y) this))
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)))
      (x.dest (F := F) (α := α)) =
    MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot fun (x y : Cofix F α) ↦ x = y ∨ r x y)
      (TypeVec.comp (α := α ::: Cofix F α) (β := α ::: Quot r) (γ := α ::: Quot fun (x y : Cofix F α) ↦ x = y ∨ r x y)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
          (Quot.factor r (fun (x y : Cofix F α) ↦ x = y ∨ r x y) this))
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)))
      (y.dest (F := F) (α := α))

Tactic:
rw [@comp_map _ _ q _ _ _ (appendFun id (Quot.mk r)),
        @comp_map _ _ q _ _ _ (appendFun id (Quot.mk r))]

Premises used: MvQPF.comp_map, TypeVec.appendFun, TypeVec.id, Quot.mk
-- 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 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) (α := α))
r' : (x y : Cofix F α) → Prop := fun (x y : Cofix F α) ↦ x = y ∨ r x y
x_1 y_1 : Cofix F α
rxy : r x_1 y_1
x y : Cofix F α
r'xy : r x y
this : ∀ (x y : Cofix F α), r x y → r' x y
h₁ h₂ :
  MvFunctor.map (F := F) (α := α ::: Quot r) (β := α ::: Quot fun (x y : Cofix F α) ↦ x = y ∨ r x y)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r (fun (x y : Cofix F α) ↦ x = y ∨ r x y) this))
      (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (y.dest (F := F) (α := α))) =
    MvFunctor.map (F := F) (α := α ::: Quot r) (β := α ::: Quot fun (x y : Cofix F α) ↦ x = y ∨ r x y)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r (fun (x y : Cofix F α) ↦ x = y ∨ r x y) this))
      (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (y.dest (F := F) (α := α)))
⊢ MvFunctor.map (F := F) (α := α ::: Quot r) (β := α ::: Quot fun (x y : Cofix F α) ↦ x = y ∨ r x y)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r (fun (x y : Cofix F α) ↦ x = y ∨ r x y) this))
      (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (x.dest (F := F) (α := α))) =
    MvFunctor.map (F := F) (α := α ::: Quot r) (β := α ::: Quot fun (x y : Cofix F α) ↦ x = y ∨ r x y)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r (fun (x y : Cofix F α) ↦ x = y ∨ r x y) this))
      (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (y.dest (F := F) (α := α)))

Tactic:
rw [h _ _ r'xy]
-- 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 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) (α := α))
r' : (x y : Cofix F α) → Prop := fun (x y : Cofix F α) ↦ x = y ∨ r x y
x_1 y_1 : Cofix F α
rxy : r x_1 y_1
x y : Cofix F α
r'xy : r' x y
h₁ :
  ∀ (h : 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) (α := α))
h₂ :
  ∀ (r'xy : 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) (α := α))
⊢ 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) (α := α))

Tactic:
cases r'xy with
    | inl h =>
      rw [h]
    | inr r'xy =>
      have : ∀ x y, r x y → r' x y := fun x y h => Or.inr h
      rw [← Quot.factor_mk_eq _ _ this]
      dsimp [r']
      rw [appendFun_comp_id]
      rw [@comp_map _ _ q _ _ _ (appendFun id (Quot.mk r)),
        @comp_map _ _ q _ _ _ (appendFun id (Quot.mk r))]
      rw [h _ _ r'xy]

Premises used: MvQPF.comp_map, TypeVec.appendFun, TypeVec.appendFun_comp_id, TypeVec.id, Quot.mk
-- 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 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) (α := α))
r' : (x y : Cofix F α) → Prop := fun (x y : Cofix F α) ↦ x = y ∨ r x y
x y : Cofix F α
rxy a : r x y
⊢ r' x y

Tactic:
right
-- 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 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) (α := α))
r' : (x y : Cofix F α) → Prop := fun (x y : Cofix F α) ↦ x = y ∨ r x y
x y : Cofix F α
rxy : r x y
⊢ r x y

Tactic:
rxy
-- 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 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) (α := α))
r' : (x y : Cofix F α) → Prop := fun (x y : Cofix F α) ↦ x = y ∨ r x y
x y : Cofix F α
rxy : r x y
⊢ r x y

Tactic:
exact rxy
-- 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 y : Cofix F α),
    r x y → LiftR (F := F) (α := α ::: Cofix F α) (α.RelLast r) (x.dest (F := F) (α := α)) (y.dest (F := F) (α := α))
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 : Cofix F α), r x y → x = y

Tactic:
apply Cofix.bisim_rel

Premises used: MvQPF.Cofix.bisim_rel
-- 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 y : Cofix F α),
    r x y → LiftR (F := F) (α := α ::: Cofix F α) (α.RelLast r) (x.dest (F := F) (α := α)) (y.dest (F := F) (α := α))
x y : Cofix F α
rxy : r x y
h₁ :
  ∀ (a : (P F).A) (f₀ f₁ : (P F).B a ⟹ fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a)
    (dxeq :
      x.dest (F := F) (α := α) =
        MvQPF.abs (F := F) (α := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a)
          (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) a f₀))
    (dyeq :
      y.dest (F := F) (α := α) =
        MvQPF.abs (F := F) (α := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a)
          (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) a f₁))
    (h' : ∀ (i : Fin2 (n + 1)) (j : (P F).B a i), α.RelLast r (f₀ i j) (f₁ i j)),
    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) (α := α))
⊢ 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) (α := α))

Tactic:
rcases (liftR_iff (fun a b => RelLast α r b) (dest x) (dest y)).mp (h x y rxy)
    with ⟨a, f₀, f₁, dxeq, dyeq, h'⟩

Premises used: TypeVec.RelLast, MvQPF.liftR_iff, Iff.mp, 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 y : Cofix F α),
    r x y → LiftR (F := F) (α := α ::: Cofix F α) (α.RelLast r) (x.dest (F := F) (α := α)) (y.dest (F := F) (α := α))
x y : Cofix F α
rxy : r x y
a : (P F).A
f₀ f₁ : (P F).B a ⟹ fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a
dxeq :
  x.dest (F := F) (α := α) =
    MvQPF.abs (F := F) (α := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) a f₀)
dyeq :
  y.dest (F := F) (α := α) =
    MvQPF.abs (F := F) (α := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) a f₁)
h' : ∀ (i : Fin2 (n + 1)) (j : (P F).B a i), α.RelLast r (f₀ i j) (f₁ i j)
h₁ :
  Eq (α := F (α ::: Quot r))
    (MvQPF.abs (F := F) (α := α ::: Quot r)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Quot r) a
        (TypeVec.comp (α := (P F).B a) (β := α ::: Cofix F α) (γ := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) f₀)))
    (MvQPF.abs (F := F) (α := α ::: Quot r)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Quot r) a
        (TypeVec.comp (α := (P F).B a) (β := α ::: Cofix F α) (γ := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) f₁)))
⊢ 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) (α := α))

Tactic:
rw [dxeq, dyeq, ← abs_map, ← abs_map, MvPFunctor.map_eq, MvPFunctor.map_eq]

Premises used: MvPFunctor.map_eq, MvQPF.abs_map
-- 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 y : Cofix F α),
    r x y → LiftR (F := F) (α := α ::: Cofix F α) (α.RelLast r) (x.dest (F := F) (α := α)) (y.dest (F := F) (α := α))
x y : Cofix F α
rxy : r x y
a : (P F).A
f₀ f₁ : (P F).B a ⟹ fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a
dxeq :
  x.dest (F := F) (α := α) =
    MvQPF.abs (F := F) (α := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) a f₀)
dyeq :
  y.dest (F := F) (α := α) =
    MvQPF.abs (F := F) (α := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) a f₁)
h' : ∀ (i : Fin2 (n + 1)) (j : (P F).B a i), α.RelLast r (f₀ i j) (f₁ i j)
h₁ :
  Eq (α := F (α ::: Quot r))
    (MvQPF.abs (F := F) (α := α ::: Quot r)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Quot r) a
        (TypeVec.comp (α := (P F).B a) (β := α ::: Cofix F α) (γ := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r))
          (splitFun (α := (P F).B a) (α' := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a)
            (dropFun (α := (P F).B a) (β := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) f₀)
            (lastFun (α := (P F).B a) (β := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) f₀)))))
    (MvQPF.abs (F := F) (α := α ::: Quot r)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Quot r) a
        (TypeVec.comp (α := (P F).B a) (β := α ::: Cofix F α) (γ := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r))
          (splitFun (α := (P F).B a) (α' := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a)
            (dropFun (α := (P F).B a) (β := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) f₁)
            (lastFun (α := (P F).B a) (β := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) f₁)))))
⊢ Eq (α := F (α ::: Quot r))
    (MvQPF.abs (F := F) (α := α ::: Quot r)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Quot r) a
        (TypeVec.comp (α := (P F).B a) (β := α ::: Cofix F α) (γ := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) f₀)))
    (MvQPF.abs (F := F) (α := α ::: Quot r)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Quot r) a
        (TypeVec.comp (α := (P F).B a) (β := α ::: Cofix F α) (γ := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) f₁)))

Tactic:
rw [← split_dropFun_lastFun f₀, ← split_dropFun_lastFun f₁]

Premises used: TypeVec.split_dropFun_lastFun