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 → 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
        (splitFun (α := (P F).B a) (α' := α ::: Quot r)
          (TypeVec.comp (α := ((P F).B a).drop) (β := α) (γ := (α ::: Quot r).drop) (TypeVec.id (α := α))
            (dropFun (α := (P F).B a) (β := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) f₀))
          (Quot.mk r ∘ 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
        (splitFun (α := (P F).B a) (α' := α ::: Quot r)
          (TypeVec.comp (α := ((P F).B a).drop) (β := α) (γ := (α ::: Quot r).drop) (TypeVec.id (α := α))
            (dropFun (α := (P F).B a) (β := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) f₁))
          (Quot.mk r ∘ 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))
          (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₁)))))

Tactic:
rw [appendFun_comp_splitFun, appendFun_comp_splitFun]

Premises used: TypeVec.appendFun_comp_splitFun
-- 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
        (splitFun (α := (P F).B a) (α' := α ::: Quot r)
          (dropFun (α := (P F).B a) (β := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) f₀)
          (Quot.mk r ∘ 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
        (splitFun (α := (P F).B a) (α' := α ::: Quot r)
          (dropFun (α := (P F).B a) (β := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) f₁)
          (Quot.mk r ∘ 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
        (splitFun (α := (P F).B a) (α' := α ::: Quot r)
          (TypeVec.comp (α := ((P F).B a).drop) (β := α) (γ := (α ::: Quot r).drop) (TypeVec.id (α := α))
            (dropFun (α := (P F).B a) (β := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) f₀))
          (Quot.mk r ∘ 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
        (splitFun (α := (P F).B a) (α' := α ::: Quot r)
          (TypeVec.comp (α := ((P F).B a).drop) (β := α) (γ := (α ::: Quot r).drop) (TypeVec.id (α := α))
            (dropFun (α := (P F).B a) (β := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) f₁))
          (Quot.mk r ∘ lastFun (α := (P F).B a) (β := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) f₁))))

Tactic:
rw [id_comp, id_comp]

Premises used: TypeVec.id_comp
-- 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₁ :
  ∀ (i : Fin2 (n + 1)) (j : (P F).B a i),
    splitFun (α := (P F).B a) (α' := α ::: Quot r)
        (dropFun (α := (P F).B a) (β := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) f₀)
        (Quot.mk r ∘ lastFun (α := (P F).B a) (β := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) f₀) i j =
      splitFun (α := (P F).B a) (α' := α ::: Quot r)
        (dropFun (α := (P F).B a) (β := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) f₁)
        (Quot.mk r ∘ lastFun (α := (P F).B a) (β := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) f₁) i j
⊢ Eq (α := F (α ::: Quot r))
    (MvQPF.abs (F := F) (α := α ::: Quot r)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Quot r) a
        (splitFun (α := (P F).B a) (α' := α ::: Quot r)
          (dropFun (α := (P F).B a) (β := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) f₀)
          (Quot.mk r ∘ 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
        (splitFun (α := (P F).B a) (α' := α ::: Quot r)
          (dropFun (α := (P F).B a) (β := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) f₁)
          (Quot.mk r ∘ lastFun (α := (P F).B a) (β := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) f₁))))

Tactic:
congr 2 with (i j)
-- 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)
i : Fin2 (n + 1)
j : (P F).B a i
h₁ :
  ∀ (j : (P F).B a Fin2.fz),
    splitFun (α := (P F).B a) (α' := α ::: Quot r)
        (dropFun (α := (P F).B a) (β := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) f₀)
        (Quot.mk r ∘ lastFun (α := (P F).B a) (β := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) f₀) Fin2.fz j =
      splitFun (α := (P F).B a) (α' := α ::: Quot r)
        (dropFun (α := (P F).B a) (β := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) f₁)
        (Quot.mk r ∘ lastFun (α := (P F).B a) (β := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) f₁) Fin2.fz j
h₂ :
  ∀ (i : Fin2 n) (j : (P F).B a i.fs),
    splitFun (α := (P F).B a) (α' := α ::: Quot r)
        (dropFun (α := (P F).B a) (β := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) f₀)
        (Quot.mk r ∘ lastFun (α := (P F).B a) (β := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) f₀) i.fs j =
      splitFun (α := (P F).B a) (α' := α ::: Quot r)
        (dropFun (α := (P F).B a) (β := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) f₁)
        (Quot.mk r ∘ lastFun (α := (P F).B a) (β := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) f₁) i.fs j
⊢ splitFun (α := (P F).B a) (α' := α ::: Quot r)
      (dropFun (α := (P F).B a) (β := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) f₀)
      (Quot.mk r ∘ lastFun (α := (P F).B a) (β := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) f₀) i j =
    splitFun (α := (P F).B a) (α' := α ::: Quot r)
      (dropFun (α := (P F).B a) (β := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) f₁)
      (Quot.mk r ∘ lastFun (α := (P F).B a) (β := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) f₁) i j

Tactic:
rcases i with - | i
-- 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)
j : (P F).B a Fin2.fz
h₁ :
  r (lastFun (α := (P F).B a) (β := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) f₀ j)
    (lastFun (α := (P F).B a) (β := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) f₁ j)
⊢ splitFun (α := (P F).B a) (α' := α ::: Quot r)
      (dropFun (α := (P F).B a) (β := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) f₀)
      (Quot.mk r ∘ lastFun (α := (P F).B a) (β := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) f₀) Fin2.fz j =
    splitFun (α := (P F).B a) (α' := α ::: Quot r)
      (dropFun (α := (P F).B a) (β := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) f₁)
      (Quot.mk r ∘ lastFun (α := (P F).B a) (β := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) f₁) Fin2.fz j

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 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)
j : (P F).B a Fin2.fz
⊢ r (lastFun (α := (P F).B a) (β := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) f₀ j)
    (lastFun (α := (P F).B a) (β := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) f₁ j)

Tactic:
apply h' _ j
-- 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)
i : Fin2 n
j : (P F).B a i.fs
h₁ : f₀ i.fs j = f₁ i.fs j
⊢ splitFun (α := (P F).B a) (α' := α ::: Quot r)
      (dropFun (α := (P F).B a) (β := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) f₀)
      (Quot.mk r ∘ lastFun (α := (P F).B a) (β := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) f₀) i.fs j =
    splitFun (α := (P F).B a) (α' := α ::: Quot r)
      (dropFun (α := (P F).B a) (β := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) f₁)
      (Quot.mk r ∘ lastFun (α := (P F).B a) (β := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) f₁) i.fs j

Tactic:
change f₀ _ j = f₁ _ j
-- 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)
i : Fin2 n
j : (P F).B a i.fs
⊢ f₀ i.fs j = f₁ i.fs j

Tactic:
apply h' _ j
-- 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' (α := α ::: Cofix F α) (F := F) (α.RelLast' r) (x.dest (F := F) (α := α)) (y.dest (F := F) (α := α))
x y : Cofix F α
h_1 : r x y
rw : LiftR' (α := α ::: Cofix F α) (F := F) (α.RelLast' r) (x.dest (F := F) (α := α)) (y.dest (F := F) (α := α))
⊢ LiftR (F := F) (α := α ::: Cofix F α) (α.RelLast r) (x.dest (F := F) (α := α)) (y.dest (F := F) (α := α))

Tactic:
rw [← LiftR_RelLast_iff]

Premises used: MvFunctor.LiftR_RelLast_iff
-- 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' (α := α ::: Cofix F α) (F := F) (α.RelLast' r) (x.dest (F := F) (α := α)) (y.dest (F := F) (α := α))
x y : Cofix F α
h_1 a : r x y
⊢ LiftR' (α := α ::: Cofix F α) (F := F) (α.RelLast' r) (x.dest (F := F) (α := α)) (y.dest (F := F) (α := α))

Tactic:
apply h
-- 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' (α := α ::: Cofix F α) (F := F) (α.RelLast' r) (x.dest (F := F) (α := α)) (y.dest (F := F) (α := α))
x y : Cofix F α
h_1 : r x y
⊢ r x y

Tactic:
assumption
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u_1
Q : β → Prop
u v : β → Cofix F α
h :
  ∀ (x : β),
    Q x →
      ∃ (a : (P F).A) (f' : (P F).drop.B a ⟹ α) (f₀ : (P F).last.B a → Cofix F α) (f₁ : (P F).last.B a → Cofix F α),
        (u x).dest (F := F) (α := α) =
            MvQPF.abs (F := F) (α := α ::: Cofix F α)
              (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Cofix F α) a
                ((P F).appendContents (α := α) f' f₀)) ∧
          (v x).dest (F := F) (α := α) =
              MvQPF.abs (F := F) (α := α ::: Cofix F α)
                (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Cofix F α) a
                  ((P F).appendContents (α := α) f' f₁)) ∧
            ∀ (i : (P F).last.B a), ∃ (x' : β), Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'
x_1 : β
Qx : Q x_1
R : (w z : Cofix F α) → Prop := fun (w z : Cofix F α) ↦ ∃ (x' : β), Q x' ∧ w = u x' ∧ z = v x'
x y : Cofix F α
h_1 : R x y
x' : β
Qx' : Q x'
xeq : x = u x'
yeq : y = v x'
rcases :
  ∀ (a : (P F).A) (f' : (P F).drop.B a ⟹ α) (f₀ f₁ : (P F).last.B a → Cofix F α)
    (ux'eq :
      (u x').dest (F := F) (α := α) =
        MvQPF.abs (F := F) (α := α ::: Cofix F α)
          (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Cofix F α) a ((P F).appendContents (α := α) f' f₀)))
    (vx'eq :
      (v x').dest (F := F) (α := α) =
        MvQPF.abs (F := F) (α := α ::: Cofix F α)
          (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Cofix F α) a ((P F).appendContents (α := α) f' f₁)))
    (h' : ∀ (i : (P F).last.B a), ∃ (x' : β), Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'),
    LiftR (F := F) (α := α ::: Cofix F α) (α.RelLast R) (x.dest (F := F) (α := α)) (y.dest (F := F) (α := α))
⊢ LiftR (F := F) (α := α ::: Cofix F α) (α.RelLast R) (x.dest (F := F) (α := α)) (y.dest (F := F) (α := α))

Tactic:
rcases h x' Qx' with ⟨a, f', f₀, f₁, ux'eq, vx'eq, h'⟩
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u_1
Q : β → Prop
u v : β → Cofix F α
h :
  ∀ (x : β),
    Q x →
      ∃ (a : (P F).A) (f' : (P F).drop.B a ⟹ α) (f₀ : (P F).last.B a → Cofix F α) (f₁ : (P F).last.B a → Cofix F α),
        (u x).dest (F := F) (α := α) =
            MvQPF.abs (F := F) (α := α ::: Cofix F α)
              (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Cofix F α) a
                ((P F).appendContents (α := α) f' f₀)) ∧
          (v x).dest (F := F) (α := α) =
              MvQPF.abs (F := F) (α := α ::: Cofix F α)
                (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Cofix F α) a
                  ((P F).appendContents (α := α) f' f₁)) ∧
            ∀ (i : (P F).last.B a), ∃ (x' : β), Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'
x_1 : β
Qx : Q x_1
R : (w z : Cofix F α) → Prop := fun (w z : Cofix F α) ↦ ∃ (x' : β), Q x' ∧ w = u x' ∧ z = v x'
x y : Cofix F α
h_1 : R x y
x' : β
Qx' : Q x'
xeq : x = u x'
yeq : y = v x'
a : (P F).A
f' : (P F).drop.B a ⟹ α
f₀ f₁ : (P F).last.B a → Cofix F α
ux'eq :
  (u x').dest (F := F) (α := α) =
    MvQPF.abs (F := F) (α := α ::: Cofix F α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Cofix F α) a ((P F).appendContents (α := α) f' f₀))
vx'eq :
  (v x').dest (F := F) (α := α) =
    MvQPF.abs (F := F) (α := α ::: Cofix F α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Cofix F α) a ((P F).appendContents (α := α) f' f₁))
h' : ∀ (i : (P F).last.B a), ∃ (x' : β), Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'
rw :
  ∃ (a : (P F).A) (f₀ : (P F).B a ⟹ α ::: Cofix F α) (f₁ : (P F).B a ⟹ α ::: Cofix F α),
    x.dest (F := F) (α := α) =
        MvQPF.abs (F := F) (α := α ::: Cofix F α)
          (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Cofix F α) a f₀) ∧
      y.dest (F := F) (α := α) =
          MvQPF.abs (F := F) (α := α ::: Cofix F α)
            (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Cofix F α) a f₁) ∧
        ∀ (i : Fin2 (n + 1)) (j : (P F).B a i), α.RelLast R (f₀ i j) (f₁ i j)
⊢ LiftR (F := F) (α := α ::: Cofix F α) (α.RelLast R) (x.dest (F := F) (α := α)) (y.dest (F := F) (α := α))

Tactic:
rw [liftR_iff]

Premises used: MvQPF.liftR_iff
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u_1
Q : β → Prop
u v : β → Cofix F α
h :
  ∀ (x : β),
    Q x →
      ∃ (a : (P F).A) (f' : (P F).drop.B a ⟹ α) (f₀ : (P F).last.B a → Cofix F α) (f₁ : (P F).last.B a → Cofix F α),
        (u x).dest (F := F) (α := α) =
            MvQPF.abs (F := F) (α := α ::: Cofix F α)
              (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Cofix F α) a
                ((P F).appendContents (α := α) f' f₀)) ∧
          (v x).dest (F := F) (α := α) =
              MvQPF.abs (F := F) (α := α ::: Cofix F α)
                (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Cofix F α) a
                  ((P F).appendContents (α := α) f' f₁)) ∧
            ∀ (i : (P F).last.B a), ∃ (x' : β), Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'
x_1 : β
Qx : Q x_1
R : (w z : Cofix F α) → Prop := fun (w z : Cofix F α) ↦ ∃ (x' : β), Q x' ∧ w = u x' ∧ z = v x'
x y : Cofix F α
h_1 : R x y
x' : β
Qx' : Q x'
xeq : x = u x'
yeq : y = v x'
a : (P F).A
f' : (P F).drop.B a ⟹ α
f₀ f₁ : (P F).last.B a → Cofix F α
ux'eq :
  (u x').dest (F := F) (α := α) =
    MvQPF.abs (F := F) (α := α ::: Cofix F α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Cofix F α) a ((P F).appendContents (α := α) f' f₀))
vx'eq :
  (v x').dest (F := F) (α := α) =
    MvQPF.abs (F := F) (α := α ::: Cofix F α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Cofix F α) a ((P F).appendContents (α := α) f' f₁))
h' : ∀ (i : (P F).last.B a), ∃ (x' : β), Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'
⊢ ∃ (a : (P F).A) (f₀ : (P F).B a ⟹ α ::: Cofix F α) (f₁ : (P F).B a ⟹ α ::: Cofix F α),
    x.dest (F := F) (α := α) =
        MvQPF.abs (F := F) (α := α ::: Cofix F α)
          (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Cofix F α) a f₀) ∧
      y.dest (F := F) (α := α) =
          MvQPF.abs (F := F) (α := α ::: Cofix F α)
            (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Cofix F α) a f₁) ∧
        ∀ (i : Fin2 (n + 1)) (j : (P F).B a i), α.RelLast R (f₀ i j) (f₁ i j)

Tactic:
⟨a, q.P.appendContents f' f₀, q.P.appendContents f' f₁, xeq.symm ▸ ux'eq,
          yeq.symm ▸ vx'eq, ?_⟩

Premises used: Eq.rec, MvPFunctor.appendContents, And.intro, Exists.intro, MvQPF.P, Eq.symm