awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Cofix (goal)
Goal:
n : ℕ
α β : TypeVec.{u_1} n
F' : TypeVec.{u_1} n → Type u
inst : MvFunctor F'
inst_1 : LawfulMvFunctor F'
R : β ⊗ β ⟹ «repeat» n Prop
x : F' α
f g : α ⟹ β
h : α ⟹ Subtype_ (α := β ⊗ β) R
hh :
  TypeVec.comp (α := α) (β := Subtype_ (α := β ⊗ β) R) (γ := β ⊗ β) (subtypeVal (α := β ⊗ β) R) h =
    TypeVec.comp (α := α) (β := α ⊗ α) (γ := β ⊗ β) (prod.map (α := α) (α' := α) (β := β) (β' := β) f g)
      (prod.diag (α := α))
⊢ MvFunctor.map (F := F') (α := Subtype_ (α := β ⊗ β) R) (β := β)
        (TypeVec.comp (α := Subtype_ (α := β ⊗ β) R) (β := β ⊗ β) (γ := β) (prod.fst (α := β) (β := β))
          (subtypeVal (α := β ⊗ β) R))
        (MvFunctor.map (F := F') (α := α) (β := Subtype_ (α := β ⊗ β) R) h x) =
      MvFunctor.map (F := F') (α := α) (β := β) f x ∧
    MvFunctor.map (F := F') (α := Subtype_ (α := β ⊗ β) R) (β := β)
        (TypeVec.comp (α := Subtype_ (α := β ⊗ β) R) (β := β ⊗ β) (γ := β) (prod.snd (α := β) (β := β))
          (subtypeVal (α := β ⊗ β) R))
        (MvFunctor.map (F := F') (α := α) (β := Subtype_ (α := β ⊗ β) R) h x) =
      MvFunctor.map (F := F') (α := α) (β := β) g x
have rw : MvFunctor.map (F := F') (α := α) (β := β) (TypeVec.comp (α := α) (β := α) (γ := β) f (TypeVec.id (α := α))) x =
    MvFunctor.map (F := F') (α := α) (β := β) f x ∧
  MvFunctor.map (F := F') (α := Subtype_ (α := β ⊗ β) R) (β := β)
      (TypeVec.comp (α := Subtype_ (α := β ⊗ β) R) (β := β ⊗ β) (γ := β) (prod.snd (α := β) (β := β))
        (subtypeVal (α := β ⊗ β) R))
      (MvFunctor.map (F := F') (α := α) (β := Subtype_ (α := β ⊗ β) R) h x) =
    MvFunctor.map (F := F') (α := α) (β := β) g x
Tactic: rw [MvFunctor.map_map, comp_assoc, hh, ← comp_assoc, fst_prod_mk, comp_assoc, fst_diag]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Cofix (goal)
Goal:
n : ℕ
α β : TypeVec.{u_1} n
F' : TypeVec.{u_1} n → Type u
inst : MvFunctor F'
inst_1 : LawfulMvFunctor F'
R : β ⊗ β ⟹ «repeat» n Prop
x : F' α
f g : α ⟹ β
h : α ⟹ Subtype_ (α := β ⊗ β) R
hh :
  TypeVec.comp (α := α) (β := Subtype_ (α := β ⊗ β) R) (γ := β ⊗ β) (subtypeVal (α := β ⊗ β) R) h =
    TypeVec.comp (α := α) (β := α ⊗ α) (γ := β ⊗ β) (prod.map (α := α) (α' := α) (β := β) (β' := β) f g)
      (prod.diag (α := α))
⊢ MvFunctor.map (F := F') (α := α) (β := β) (TypeVec.comp (α := α) (β := α) (γ := β) f (TypeVec.id (α := α))) x =
      MvFunctor.map (F := F') (α := α) (β := β) f x ∧
    MvFunctor.map (F := F') (α := Subtype_ (α := β ⊗ β) R) (β := β)
        (TypeVec.comp (α := Subtype_ (α := β ⊗ β) R) (β := β ⊗ β) (γ := β) (prod.snd (α := β) (β := β))
          (subtypeVal (α := β ⊗ β) R))
        (MvFunctor.map (F := F') (α := α) (β := Subtype_ (α := β ⊗ β) R) h x) =
      MvFunctor.map (F := F') (α := α) (β := β) g x
have rw : MvFunctor.map (F := F') (α := α) (β := β) (TypeVec.comp (α := α) (β := α) (γ := β) f (TypeVec.id (α := α))) x =
    MvFunctor.map (F := F') (α := α) (β := β) f x ∧
  MvFunctor.map (F := F') (α := α) (β := β) (TypeVec.comp (α := α) (β := α) (γ := β) g (TypeVec.id (α := α))) x =
    MvFunctor.map (F := F') (α := α) (β := β) g x
Tactic: rw [MvFunctor.map_map, comp_assoc, hh, ← comp_assoc, snd_prod_mk, comp_assoc, snd_diag]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Cofix (goal)
Goal:
n : ℕ
α β : TypeVec.{u_1} n
F' : TypeVec.{u_1} n → Type u
inst : MvFunctor F'
inst_1 : LawfulMvFunctor F'
R : β ⊗ β ⟹ «repeat» n Prop
x : F' α
f g : α ⟹ β
h : α ⟹ Subtype_ (α := β ⊗ β) R
hh :
  TypeVec.comp (α := α) (β := Subtype_ (α := β ⊗ β) R) (γ := β ⊗ β) (subtypeVal (α := β ⊗ β) R) h =
    TypeVec.comp (α := α) (β := α ⊗ α) (γ := β ⊗ β) (prod.map (α := α) (α' := α) (β := β) (β' := β) f g)
      (prod.diag (α := α))
⊢ MvFunctor.map (F := F') (α := α) (β := β) (TypeVec.comp (α := α) (β := α) (γ := β) f (TypeVec.id (α := α))) x =
      MvFunctor.map (F := F') (α := α) (β := β) f x ∧
    MvFunctor.map (F := F') (α := α) (β := β) (TypeVec.comp (α := α) (β := α) (γ := β) g (TypeVec.id (α := α))) x =
      MvFunctor.map (F := F') (α := α) (β := β) g x
have dsimp : MvFunctor.map (F := F') (α := α) (β := β) f x = MvFunctor.map (F := F') (α := α) (β := β) f x ∧
  MvFunctor.map (F := F') (α := α) (β := β) g x = MvFunctor.map (F := F') (α := α) (β := β) g x
Tactic: dsimp [LiftR']
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Cofix (goal)
Goal:
n : ℕ
α β : TypeVec.{u_1} n
F' : TypeVec.{u_1} n → Type u
inst : MvFunctor F'
inst_1 : LawfulMvFunctor F'
R : β ⊗ β ⟹ «repeat» n Prop
x : F' α
f g : α ⟹ β
h : α ⟹ Subtype_ (α := β ⊗ β) R
hh :
  TypeVec.comp (α := α) (β := Subtype_ (α := β ⊗ β) R) (γ := β ⊗ β) (subtypeVal (α := β ⊗ β) R) h =
    TypeVec.comp (α := α) (β := α ⊗ α) (γ := β ⊗ β) (prod.map (α := α) (α' := α) (β := β) (β' := β) f g)
      (prod.diag (α := α))
⊢ MvFunctor.map (F := F') (α := α) (β := β) f x = MvFunctor.map (F := F') (α := α) (β := β) f x ∧
    MvFunctor.map (F := F') (α := α) (β := β) g x = MvFunctor.map (F := F') (α := α) (β := β) g x
have left : MvFunctor.map (F := F') (α := α) (β := β) f x = MvFunctor.map (F := F') (α := α) (β := β) f x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Cofix (goal)
Goal:
n : ℕ
α β : TypeVec.{u_1} n
F' : TypeVec.{u_1} n → Type u
inst : MvFunctor F'
inst_1 : LawfulMvFunctor F'
R : β ⊗ β ⟹ «repeat» n Prop
x : F' α
f g : α ⟹ β
h : α ⟹ Subtype_ (α := β ⊗ β) R
hh :
  TypeVec.comp (α := α) (β := Subtype_ (α := β ⊗ β) R) (γ := β ⊗ β) (subtypeVal (α := β ⊗ β) R) h =
    TypeVec.comp (α := α) (β := α ⊗ α) (γ := β ⊗ β) (prod.map (α := α) (α' := α) (β := β) (β' := β) f g)
      (prod.diag (α := α))
left : MvFunctor.map (F := F') (α := α) (β := β) f x = MvFunctor.map (F := F') (α := α) (β := β) f x
⊢ MvFunctor.map (F := F') (α := α) (β := β) f x = MvFunctor.map (F := F') (α := α) (β := β) f x ∧
    MvFunctor.map (F := F') (α := α) (β := β) g x = MvFunctor.map (F := F') (α := α) (β := β) g x
have right : MvFunctor.map (F := F') (α := α) (β := β) g x = MvFunctor.map (F := F') (α := α) (β := β) g x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Cofix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
lawful : LawfulMvFunctor F
α : TypeVec.{u} n
ι ι' : Type u
R : ι' → ι' → Prop
x : F (α ::: ι)
f g : ι → ι'
hh : ∀ (x : ι), R (f x) (g x)
h : ι → { x : ι' × ι' // uncurry R x } := fun (x : ι) ↦ Subtype.mk (p := fun (x : ι' × ι') ↦ uncurry R x) (f x, g x) ⋯
b : α ::: ι ⟹ Subtype_ (α := α ⊗ α) α.repeatEq ::: { x : ι' × ι' // uncurry R x } :=
  appendFun (α := α) (α' := Subtype_ (α := α ⊗ α) α.repeatEq) (diagSub (α := α)) h
c : Subtype_ (α := α ⊗ α) α.repeatEq ::: { x : ι' × ι' // uncurry R x } ⟹
  (fun (i : Fin2 n) ↦ { x : (α ::: ι' ⊗ α ::: ι') i.fs // ofRepeat (α.RelLast' R i.fs x) }) ::: Subtype (uncurry R) :=
  appendFun (α := Subtype_ (α := α ⊗ α) α.repeatEq) (α' := fun (i : Fin2 n) ↦
    { x : (α ::: ι' ⊗ α ::: ι') i.fs // ofRepeat (α.RelLast' R i.fs x) }) (ofSubtype (α := α ⊗ α) α.repeatEq) _root_.id
⊢ TypeVec.comp (α := (α ::: ι).drop) (β := (Subtype_ (α := α ::: ι' ⊗ α ::: ι') (α.RelLast' R)).drop) (γ :=
      (α ::: ι' ⊗ α ::: ι').drop) (subtypeVal (α := (α ::: ι' ⊗ α ::: ι').drop) α.repeatEq)
      (TypeVec.comp (α := (α ::: ι).drop) (β :=
        TypeVec.drop fun (i : Fin2 (n + 1)) ↦ { x : (α ::: ι' ⊗ α ::: ι') i // ofRepeat (α.RelLast' R i x) }) (γ :=
        (Subtype_ (α := α ::: ι' ⊗ α ::: ι') (α.RelLast' R)).drop)
        (toSubtype (α := fun (i : Fin2 n) ↦ (α ::: ι' ⊗ α ::: ι') i.fs) fun (i : Fin2 n) ↦ α.RelLast' R i.fs)
        (TypeVec.comp (α := (α ::: ι).drop) (β :=
          (Subtype_ (α := α ⊗ α) α.repeatEq ::: { x : ι' × ι' // uncurry R x }).drop) (γ :=
          TypeVec.drop
            ((TypeVec.drop fun (i : Fin2 (n + 1)) ↦ { x : (α ::: ι' ⊗ α ::: ι') i // ofRepeat (α.RelLast' R i x) }) :::
              TypeVec.last (n := n) fun (i : Fin2 (n + 1)) ↦
                { x : (α ::: ι' ⊗ α ::: ι') i // ofRepeat (α.RelLast' R i x) }))
          (dropFun (α := Subtype_ (α := α ⊗ α) α.repeatEq ::: { x : ι' × ι' // uncurry R x }) (β :=
            (TypeVec.drop fun (i : Fin2 (n + 1)) ↦ { x : (α ::: ι' ⊗ α ::: ι') i // ofRepeat (α.RelLast' R i x) }) :::
              TypeVec.last (n := n) fun (i : Fin2 (n + 1)) ↦
                { x : (α ::: ι' ⊗ α ::: ι') i // ofRepeat (α.RelLast' R i x) })
            c)
          (diagSub (α := α)))) =
    prod.diag (α := (α ::: ι).drop)
have h₀ : Eq.{u + 1} (α := (α ::: ι).drop ⟹ (α ::: ι' ⊗ α ::: ι').drop)
  (fun (i : Fin2 n) (x : (α ::: ι).drop i) ↦
    subtypeVal (α := (α ::: ι' ⊗ α ::: ι').drop) α.repeatEq i (diagSub (α := α) i x))
  (prod.diag (α := (α ::: ι).drop))
Tactic: erw [toSubtype_of_subtype_assoc, TypeVec.id_comp]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Cofix (goal)
Goal:
n : ℕ
α : TypeVec.{u} n
ι ι' : Type u
⊢ Eq.{u + 1} (α := (α ::: ι).drop ⟹ (α ::: ι' ⊗ α ::: ι').drop)
    (fun (i : Fin2 n) (x : (α ::: ι).drop i) ↦
      subtypeVal (α := (α ::: ι' ⊗ α ::: ι').drop) α.repeatEq i (diagSub (α := α) i x))
    (prod.diag (α := (α ::: ι).drop))
have h₀ : ∀ (i : Fin2 n) (x : (α ::: ι).drop i),
  subtypeVal (α := (α ::: ι' ⊗ α ::: ι').drop) α.repeatEq i (diagSub (α := α) i x) = prod.diag (α := (α ::: ι).drop) i x
Tactic: ext (i x) : 2
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Cofix (goal)
Goal:
n : ℕ
α : TypeVec.{u} n
ι ι' : Type u
i : Fin2 n
x : (α ::: ι).drop i
⊢ subtypeVal (α := (α ::: ι' ⊗ α ::: ι').drop) α.repeatEq i (diagSub (α := α) i x) = prod.diag (α := (α ::: ι).drop) i x
have h₀ : ∀ {n : ℕ} {α : TypeVec.{u} (n + 1)} (x : (α ::: ι).drop Fin2.fz),
  subtypeVal (α := (α ::: ι' ⊗ α ::: ι').drop) α.repeatEq Fin2.fz (diagSub (α := α) Fin2.fz x) =
    prod.diag (α := (α ::: ι).drop) Fin2.fz x
Tactic: induction i with
      | fz => rfl
      | fs _ ih =>
        apply ih
Cleared hypotheses: α, i, x
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Cofix (goal)
Goal:
n : ℕ
α : TypeVec.{u} n
ι ι' : Type u
i : Fin2 n
x : (α ::: ι).drop i
h₀ :
  ∀ {n : ℕ} {α : TypeVec.{u} (n + 1)} (x : (α ::: ι).drop Fin2.fz),
    subtypeVal (α := (α ::: ι' ⊗ α ::: ι').drop) α.repeatEq Fin2.fz (diagSub (α := α) Fin2.fz x) =
      prod.diag (α := (α ::: ι).drop) Fin2.fz x
⊢ subtypeVal (α := (α ::: ι' ⊗ α ::: ι').drop) α.repeatEq i (diagSub (α := α) i x) = prod.diag (α := (α ::: ι).drop) i x
have h₁ : ∀ {n : ℕ} (a : Fin2 n)
  (ih :
    ∀ {α : TypeVec.{u} n} (x : (α ::: ι).drop a),
      subtypeVal (α := (α ::: ι' ⊗ α ::: ι').drop) α.repeatEq a (diagSub (α := α) a x) =
        prod.diag (α := (α ::: ι).drop) a x)
  {α : TypeVec.{u} (n + 1)} (x : (α ::: ι).drop a.fs),
  subtypeVal (α := (α ::: ι' ⊗ α ::: ι').drop) α.repeatEq a.fs (diagSub (α := α) a.fs x) =
    prod.diag (α := (α ::: ι).drop) a.fs x
Tactic: induction i with
      | fz => rfl
      | fs _ ih =>
        apply ih
Cleared hypotheses: α, i, x
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Cofix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
lawful : LawfulMvFunctor F
α : TypeVec.{u} n
ι ι' : Type u
R : ι' → ι' → Prop
x : F (α ::: ι)
f g : ι → ι'
hh : ∀ (x : ι), R (f x) (g x)
h : ι → { x : ι' × ι' // uncurry R x } := fun (x : ι) ↦ Subtype.mk (p := fun (x : ι' × ι') ↦ uncurry R x) (f x, g x) ⋯
b : α ::: ι ⟹ Subtype_ (α := α ⊗ α) α.repeatEq ::: { x : ι' × ι' // uncurry R x } :=
  appendFun (α := α) (α' := Subtype_ (α := α ⊗ α) α.repeatEq) (diagSub (α := α)) h
c : Subtype_ (α := α ⊗ α) α.repeatEq ::: { x : ι' × ι' // uncurry R x } ⟹
  (fun (i : Fin2 n) ↦ { x : (α ::: ι' ⊗ α ::: ι') i.fs // ofRepeat (α.RelLast' R i.fs x) }) ::: Subtype (uncurry R) :=
  appendFun (α := Subtype_ (α := α ⊗ α) α.repeatEq) (α' := fun (i : Fin2 n) ↦
    { x : (α ::: ι' ⊗ α ::: ι') i.fs // ofRepeat (α.RelLast' R i.fs x) }) (ofSubtype (α := α ⊗ α) α.repeatEq) _root_.id
⊢ Subtype.val ∘
      lastFun (α := Subtype_ (α := α ⊗ α) α.repeatEq ::: { x : ι' × ι' // uncurry R x }) (β :=
          (TypeVec.drop fun (i : Fin2 (n + 1)) ↦ { x : (α ::: ι' ⊗ α ::: ι') i // ofRepeat (α.RelLast' R i x) }) :::
            TypeVec.last (n := n) fun (i : Fin2 (n + 1)) ↦
              { x : (α ::: ι' ⊗ α ::: ι') i // ofRepeat (α.RelLast' R i x) })
          c ∘
        h =
    Prod.map f g ∘ lastFun (α := α ::: ι) (β := α ::: ι ⊗ α ::: ι) (prod.diag (α := α ::: ι))
have h₁ : ∀ (x : (α ::: ι).last),
  (Subtype.val ∘
        lastFun (α := Subtype_ (α := α ⊗ α) α.repeatEq ::: { x : ι' × ι' // uncurry R x }) (β :=
            (TypeVec.drop fun (i : Fin2 (n + 1)) ↦ { x : (α ::: ι' ⊗ α ::: ι') i // ofRepeat (α.RelLast' R i x) }) :::
              TypeVec.last (n := n) fun (i : Fin2 (n + 1)) ↦
                { x : (α ::: ι' ⊗ α ::: ι') i // ofRepeat (α.RelLast' R i x) })
            c ∘
          h)
      x =
    (Prod.map f g ∘ lastFun (α := α ::: ι) (β := α ::: ι ⊗ α ::: ι) (prod.diag (α := α ::: ι))) x
Tactic: ext1
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Cofix (hypothesis)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
inst : LawfulMvFunctor F
α : TypeVec.{u} n
ι : Type u
R : ι → ι → Prop
x : F (α ::: ι)
f : ι → ι
hh : ∀ (x : ι), R (f x) x
⊢ LiftR' (α := α ::: ι) (F := F) (α.RelLast' R)
    (MvFunctor.map (F := F) (α := α ::: ι) (β := α ::: ι) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) f) x) x
have this : LiftR' (α := α ::: ι) (F := F) (α.RelLast' R)
  (MvFunctor.map (F := F) (α := α ::: ι) (β := α ::: ι) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) f) x)
  (MvFunctor.map (F := F) (α := α ::: ι) (β := α ::: ι) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) _root_.id)
    x)
Tactic: have := liftR_map_last R x f id hh
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Cofix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
inst : LawfulMvFunctor F
α : TypeVec.{u} n
ι : Type u
R : ι → ι → Prop
x : F (α ::: ι)
f : ι → ι
hh : ∀ (x : ι), R (f x) x
this :
  LiftR' (α := α ::: ι) (F := F) (α.RelLast' R)
    (MvFunctor.map (F := F) (α := α ::: ι) (β := α ::: ι) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) f) x)
    (MvFunctor.map (F := F) (α := α ::: ι) (β := α ::: ι) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) _root_.id)
      x)
⊢ LiftR' (α := α ::: ι) (F := F) (α.RelLast' R)
    (MvFunctor.map (F := F) (α := α ::: ι) (β := α ::: ι) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) f) x) x
have rwa : ∀
  (this :
    LiftR' (α := α ::: ι) (F := F) (α.RelLast' R)
      (MvFunctor.map (F := F) (α := α ::: ι) (β := α ::: ι) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) f) x)
      (MvFunctor.map (F := F) (α := α ::: ι) (β := α ::: ι) (TypeVec.id (α := α ::: ι)) x)),
  LiftR' (α := α ::: ι) (F := F) (α.RelLast' R)
    (MvFunctor.map (F := F) (α := α ::: ι) (β := α ::: ι) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) f) x) x
Tactic: rwa [appendFun_id_id, MvFunctor.id_map] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Cofix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
inst : LawfulMvFunctor F
α : TypeVec.{u} n
ι : Type u
R : ι → ι → Prop
x : F (α ::: ι)
f : ι → ι
hh : ∀ (x : ι), R (f x) x
this :
  LiftR' (α := α ::: ι) (F := F) (α.RelLast' R)
    (MvFunctor.map (F := F) (α := α ::: ι) (β := α ::: ι) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) f) x)
    (MvFunctor.map (F := F) (α := α ::: ι) (β := α ::: ι) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) _root_.id)
      x)
rwa :
  ∀
    (this :
      LiftR' (α := α ::: ι) (F := F) (α.RelLast' R)
        (MvFunctor.map (F := F) (α := α ::: ι) (β := α ::: ι) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) f) x)
        (MvFunctor.map (F := F) (α := α ::: ι) (β := α ::: ι) (TypeVec.id (α := α ::: ι)) x)),
    LiftR' (α := α ::: ι) (F := F) (α.RelLast' R)
      (MvFunctor.map (F := F) (α := α ::: ι) (β := α ::: ι) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) f) x) x
⊢ LiftR' (α := α ::: ι) (F := F) (α.RelLast' R)
    (MvFunctor.map (F := F) (α := α ::: ι) (β := α ::: ι) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) f) x) x
have rwa₁ : ∀
  (this :
    LiftR' (α := α ::: ι) (F := F) (α.RelLast' R)
      (MvFunctor.map (F := F) (α := α ::: ι) (β := α ::: ι) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) f) x)
      x),
  LiftR' (α := α ::: ι) (F := F) (α.RelLast' R)
    (MvFunctor.map (F := F) (α := α ::: ι) (β := α ::: ι) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) f) x) x
Tactic: rwa [appendFun_id_id, MvFunctor.id_map] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Cofix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : Cofix F α
R : (x y : Cofix F α) → Prop := fun (x y : Cofix F α) ↦ abs (F := F) (α := α) (y.repr (F := F) (α := α)) = x
⊢ Quot.mk (Mcongr (F := F) (α := α)) (x.repr (F := F) (α := α)) = x
have refine : ∀ (x y : Cofix F α),
  R x y → LiftR' (α := α ::: Cofix F α) (F := F) (α.RelLast' R) (x.dest (F := F) (α := α)) (y.dest (F := F) (α := α))
Tactic: refine Cofix.bisim₂ R ?_ _ _ rfl
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Cofix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
R : (x y : Cofix F α) → Prop := fun (x y : Cofix F α) ↦ abs (F := F) (α := α) (y.repr (F := F) (α := α)) = x
x y : Cofix F α
h : R x y
⊢ LiftR' (α := α ::: Cofix F α) (F := F) (α.RelLast' R) (x.dest (F := F) (α := α)) (y.dest (F := F) (α := α))
have subst : LiftR' (α := α ::: Cofix F α) (F := F) (α.RelLast' R)
  ((abs (F := F) (α := α) (y.repr (F := F) (α := α))).dest (F := F) (α := α)) (y.dest (F := F) (α := α))
Tactic: subst h
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Cofix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
R : (x y : Cofix F α) → Prop := fun (x y : Cofix F α) ↦ abs (F := F) (α := α) (y.repr (F := F) (α := α)) = x
y : Cofix F α
⊢ LiftR' (α := α ::: Cofix F α) (F := F) (α.RelLast' R)
    ((abs (F := F) (α := α) (y.repr (F := F) (α := α))).dest (F := F) (α := α)) (y.dest (F := F) (α := α))
have dsimp : LiftR' (α := α ::: Cofix F α) (F := F) (α.RelLast' 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) (α := α) (y.repr (F := 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)))
    sorry y)
Tactic: dsimp [Cofix.dest, Cofix.abs]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Cofix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
R : (x y : Cofix F α) → Prop := fun (x y : Cofix F α) ↦ abs (F := F) (α := α) (y.repr (F := F) (α := α)) = x
y : Cofix F α
⊢ LiftR' (α := α ::: Cofix F α) (F := F) (α.RelLast' 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) (α := α) (y.repr (F := 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)))
      ⋯ y)
have mk : ∀ (a : (P F).M α),
  LiftR' (α := α ::: Cofix F α) (F := F) (α.RelLast' 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) (α := α) (repr (F := F) (α := α) (Quot.mk (Mcongr (F := F) (α := α)) a)))))
    (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)))
      sorry (Quot.mk (Mcongr (F := F) (α := α)) a))
Tactic: induction y using Quot.ind
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Cofix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
R : (x y : Cofix F α) → Prop := fun (x y : Cofix F α) ↦ abs (F := F) (α := α) (y.repr (F := F) (α := α)) = x
a : (P F).M α
⊢ LiftR' (α := α ::: Cofix F α) (F := F) (α.RelLast' 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) (α := α) (repr (F := F) (α := α) (Quot.mk (Mcongr (F := F) (α := α)) a)))))
    (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) (α := α)) a))
have mk : LiftR' (α := α ::: Cofix F α) (F := F) (α.RelLast' R)
  (MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
    (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: (P F).M α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
        (M.corec (P F) (α := α) (MvQPF.repr (F := F) (α := α ::: Cofix F α) ∘ dest (F := F) (α := α))))
      (dest (F := F) (α := α) (Quot.mk (Mcongr (F := F) (α := α)) a))))
  (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)))
Tactic: simp only [Cofix.repr, M.dest_corec, abs_map, MvQPF.abs_repr, Function.comp]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Cofix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
R : (x y : Cofix F α) → Prop := fun (x y : Cofix F α) ↦ abs (F := F) (α := α) (y.repr (F := F) (α := α)) = x
a : (P F).M α
| LiftR' (α := α ::: Cofix F α) (F := F) (α.RelLast' R)
    (MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
      (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: (P F).M α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
          (M.corec (P F) (α := α) (MvQPF.repr (F := F) (α := α ::: Cofix F α) ∘ dest (F := F) (α := α))))
        (dest (F := F) (α := α) (Quot.mk (Mcongr (F := F) (α := α)) a))))
    (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)))
have R₁ : α.RelLast' R
Tactic: congr