awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_1 x y : Cofix F α
h : x = mk (F := F) (α := α) (y.dest (F := F) (α := α))
⊢ Eq.{u + 1} (α :=
    α ::: Cofix F α ⟹ α ::: Quot fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α)))
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
      (((Quot.mk fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α))) ∘ mk (F := F) (α := α)) ∘
        fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)))
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
      (Quot.mk fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α))))
have e_a : Eq.{u + 1} (α := Cofix F α → Quot fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α)))
  (((Quot.mk fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α))) ∘ mk (F := F) (α := α)) ∘
    fun (i : Cofix F α) ↦ i.dest (F := F) (α := α))
  (Quot.mk fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α)))
Tactic: apply congrArg
-- 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_1 x y : Cofix F α
h : x = mk (F := F) (α := α) (y.dest (F := F) (α := α))
⊢ Eq.{u + 1} (α := Cofix F α → Quot fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α)))
    (((Quot.mk fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α))) ∘ mk (F := F) (α := α)) ∘
      fun (i : Cofix F α) ↦ i.dest (F := F) (α := α))
    (Quot.mk fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α)))
have e_a : ∀ (x : Cofix F α),
  Eq (α := Quot fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α)))
    ((((Quot.mk fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α))) ∘ mk (F := F) (α := α)) ∘
        fun (i : Cofix F α) ↦ i.dest (F := F) (α := α))
      x)
    (Quot.mk (fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α))) x)
Tactic: funext 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
α : TypeVec.{u} n
x_1 x_2 y : Cofix F α
h : x_2 = mk (F := F) (α := α) (y.dest (F := F) (α := α))
x : Cofix F α
⊢ Eq (α := Quot fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α)))
    ((((Quot.mk fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α))) ∘ mk (F := F) (α := α)) ∘
        fun (i : Cofix F α) ↦ i.dest (F := F) (α := α))
      x)
    (Quot.mk (fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α))) x)
have e_a : mk (F := F) (α := α) ((fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)) x) =
  mk (F := F) (α := α) (x.dest (F := F) (α := α))
Tactic: apply Quot.sound
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Cofix (hypothesis)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Cofix F α)
⊢ (mk (F := F) (α := α) x).dest (F := F) (α := α) = x
have this : Eq.{u + 1} (α := Cofix F α → Cofix F α) (mk (F := F) (α := α) ∘ dest (F := F) (α := α)) _root_.id
Tactic: have : Cofix.mk ∘ Cofix.dest = @_root_.id (Cofix F α) := funext Cofix.mk_dest
-- 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 : F (α ::: Cofix F α)
this : Eq.{u + 1} (α := Cofix F α → Cofix F α) (mk (F := F) (α := α) ∘ dest (F := F) (α := α)) _root_.id
⊢ (mk (F := F) (α := α) x).dest (F := F) (α := α) = x
have rw : dest (F := F) (α := α)
    (corec (F := F) (α := α)
      (fun (x : F (α ::: Cofix F α)) ↦
        MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: F (α ::: Cofix F α))
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)) x)
      x) =
  x
Tactic: rw [Cofix.mk, Cofix.dest_corec, ← comp_map, ← Cofix.mk, ← appendFun_comp, this, id_comp,
    appendFun_id_id, MvFunctor.id_map]
-- 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 : F (α ::: Cofix F α)
this : Eq.{u + 1} (α := Cofix F α → Cofix F α) (mk (F := F) (α := α) ∘ dest (F := F) (α := α)) _root_.id
rw :
  dest (F := F) (α := α)
      (corec (F := F) (α := α)
        (fun (x : F (α ::: Cofix F α)) ↦
          MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: F (α ::: Cofix F α))
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)) x)
        x) =
    x
⊢ (mk (F := F) (α := α) x).dest (F := F) (α := α) = x
have rw₁ : MvFunctor.map (F := F) (α := α ::: F (α ::: Cofix F α)) (β := α ::: Cofix F α)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
      (corec (F := F) (α := α) fun (x : F (α ::: Cofix F α)) ↦
        MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: F (α ::: Cofix F α))
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)) x))
    (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: F (α ::: Cofix F α))
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)) x) =
  x
Tactic: rw [Cofix.mk, Cofix.dest_corec, ← comp_map, ← Cofix.mk, ← appendFun_comp, this, id_comp,
    appendFun_id_id, MvFunctor.id_map]
-- 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 : F (α ::: Cofix F α)
this : Eq.{u + 1} (α := Cofix F α → Cofix F α) (mk (F := F) (α := α) ∘ dest (F := F) (α := α)) _root_.id
rw :
  dest (F := F) (α := α)
      (corec (F := F) (α := α)
        (fun (x : F (α ::: Cofix F α)) ↦
          MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: F (α ::: Cofix F α))
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)) x)
        x) =
    x
rw₁ :
  MvFunctor.map (F := F) (α := α ::: F (α ::: Cofix F α)) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
        (corec (F := F) (α := α) fun (x : F (α ::: Cofix F α)) ↦
          MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: F (α ::: Cofix F α))
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)) x))
      (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: F (α ::: Cofix F α))
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)) x) =
    x
⊢ (mk (F := F) (α := α) x).dest (F := F) (α := α) = x
have rw₂ : MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Cofix F α)
    (TypeVec.comp (α := α ::: Cofix F α) (β := α ::: F (α ::: Cofix F α)) (γ := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
        (corec (F := F) (α := α) fun (x : F (α ::: Cofix F α)) ↦
          MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: F (α ::: Cofix F α))
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)) x))
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)))
    x =
  x
Tactic: rw [Cofix.mk, Cofix.dest_corec, ← comp_map, ← Cofix.mk, ← appendFun_comp, this, id_comp,
    appendFun_id_id, MvFunctor.id_map]
-- 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 : F (α ::: Cofix F α)
this : Eq.{u + 1} (α := Cofix F α → Cofix F α) (mk (F := F) (α := α) ∘ dest (F := F) (α := α)) _root_.id
rw :
  dest (F := F) (α := α)
      (corec (F := F) (α := α)
        (fun (x : F (α ::: Cofix F α)) ↦
          MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: F (α ::: Cofix F α))
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)) x)
        x) =
    x
rw₁ :
  MvFunctor.map (F := F) (α := α ::: F (α ::: Cofix F α)) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
        (corec (F := F) (α := α) fun (x : F (α ::: Cofix F α)) ↦
          MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: F (α ::: Cofix F α))
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)) x))
      (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: F (α ::: Cofix F α))
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)) x) =
    x
rw₂ :
  MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Cofix F α)
      (TypeVec.comp (α := α ::: Cofix F α) (β := α ::: F (α ::: Cofix F α)) (γ := α ::: Cofix F α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
          (corec (F := F) (α := α) fun (x : F (α ::: Cofix F α)) ↦
            MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: F (α ::: Cofix F α))
              (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)) x))
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)))
      x =
    x
⊢ (mk (F := F) (α := α) x).dest (F := F) (α := α) = x
have rw₃ : MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Cofix F α)
    (TypeVec.comp (α := α ::: Cofix F α) (β := α ::: F (α ::: Cofix F α)) (γ := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (mk (F := F) (α := α)))
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)))
    x =
  x
Tactic: rw [Cofix.mk, Cofix.dest_corec, ← comp_map, ← Cofix.mk, ← appendFun_comp, this, id_comp,
    appendFun_id_id, MvFunctor.id_map]
-- 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 : F (α ::: Cofix F α)
this : Eq.{u + 1} (α := Cofix F α → Cofix F α) (mk (F := F) (α := α) ∘ dest (F := F) (α := α)) _root_.id
rw :
  dest (F := F) (α := α)
      (corec (F := F) (α := α)
        (fun (x : F (α ::: Cofix F α)) ↦
          MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: F (α ::: Cofix F α))
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)) x)
        x) =
    x
rw₁ :
  MvFunctor.map (F := F) (α := α ::: F (α ::: Cofix F α)) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
        (corec (F := F) (α := α) fun (x : F (α ::: Cofix F α)) ↦
          MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: F (α ::: Cofix F α))
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)) x))
      (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: F (α ::: Cofix F α))
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)) x) =
    x
rw₂ :
  MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Cofix F α)
      (TypeVec.comp (α := α ::: Cofix F α) (β := α ::: F (α ::: Cofix F α)) (γ := α ::: Cofix F α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
          (corec (F := F) (α := α) fun (x : F (α ::: Cofix F α)) ↦
            MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: F (α ::: Cofix F α))
              (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)) x))
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)))
      x =
    x
rw₃ :
  MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Cofix F α)
      (TypeVec.comp (α := α ::: Cofix F α) (β := α ::: F (α ::: Cofix F α)) (γ := α ::: Cofix F α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (mk (F := F) (α := α)))
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)))
      x =
    x
⊢ (mk (F := F) (α := α) x).dest (F := F) (α := α) = x
have rw₄ : MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Cofix F α)
    (appendFun (α := α) (α' := α) (TypeVec.comp (α := α) (β := α) (γ := α) (TypeVec.id (α := α)) (TypeVec.id (α := α)))
      (mk (F := F) (α := α) ∘ fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)))
    x =
  x
Tactic: rw [Cofix.mk, Cofix.dest_corec, ← comp_map, ← Cofix.mk, ← appendFun_comp, this, id_comp,
    appendFun_id_id, MvFunctor.id_map]
-- 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 : F (α ::: Cofix F α)
this : Eq.{u + 1} (α := Cofix F α → Cofix F α) (mk (F := F) (α := α) ∘ dest (F := F) (α := α)) _root_.id
rw :
  dest (F := F) (α := α)
      (corec (F := F) (α := α)
        (fun (x : F (α ::: Cofix F α)) ↦
          MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: F (α ::: Cofix F α))
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)) x)
        x) =
    x
rw₁ :
  MvFunctor.map (F := F) (α := α ::: F (α ::: Cofix F α)) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
        (corec (F := F) (α := α) fun (x : F (α ::: Cofix F α)) ↦
          MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: F (α ::: Cofix F α))
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)) x))
      (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: F (α ::: Cofix F α))
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)) x) =
    x
rw₂ :
  MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Cofix F α)
      (TypeVec.comp (α := α ::: Cofix F α) (β := α ::: F (α ::: Cofix F α)) (γ := α ::: Cofix F α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
          (corec (F := F) (α := α) fun (x : F (α ::: Cofix F α)) ↦
            MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: F (α ::: Cofix F α))
              (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)) x))
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)))
      x =
    x
rw₃ :
  MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Cofix F α)
      (TypeVec.comp (α := α ::: Cofix F α) (β := α ::: F (α ::: Cofix F α)) (γ := α ::: Cofix F α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (mk (F := F) (α := α)))
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)))
      x =
    x
rw₄ :
  MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α)
        (TypeVec.comp (α := α) (β := α) (γ := α) (TypeVec.id (α := α)) (TypeVec.id (α := α)))
        (mk (F := F) (α := α) ∘ fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)))
      x =
    x
⊢ (mk (F := F) (α := α) x).dest (F := F) (α := α) = x
have rw₅ : MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Cofix F α)
    (appendFun (α := α) (α' := α) (TypeVec.comp (α := α) (β := α) (γ := α) (TypeVec.id (α := α)) (TypeVec.id (α := α)))
      _root_.id)
    x =
  x
Tactic: rw [Cofix.mk, Cofix.dest_corec, ← comp_map, ← Cofix.mk, ← appendFun_comp, this, id_comp,
    appendFun_id_id, MvFunctor.id_map]
-- 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 : F (α ::: Cofix F α)
this : Eq.{u + 1} (α := Cofix F α → Cofix F α) (mk (F := F) (α := α) ∘ dest (F := F) (α := α)) _root_.id
rw :
  dest (F := F) (α := α)
      (corec (F := F) (α := α)
        (fun (x : F (α ::: Cofix F α)) ↦
          MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: F (α ::: Cofix F α))
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)) x)
        x) =
    x
rw₁ :
  MvFunctor.map (F := F) (α := α ::: F (α ::: Cofix F α)) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
        (corec (F := F) (α := α) fun (x : F (α ::: Cofix F α)) ↦
          MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: F (α ::: Cofix F α))
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)) x))
      (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: F (α ::: Cofix F α))
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)) x) =
    x
rw₂ :
  MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Cofix F α)
      (TypeVec.comp (α := α ::: Cofix F α) (β := α ::: F (α ::: Cofix F α)) (γ := α ::: Cofix F α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
          (corec (F := F) (α := α) fun (x : F (α ::: Cofix F α)) ↦
            MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: F (α ::: Cofix F α))
              (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)) x))
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)))
      x =
    x
rw₃ :
  MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Cofix F α)
      (TypeVec.comp (α := α ::: Cofix F α) (β := α ::: F (α ::: Cofix F α)) (γ := α ::: Cofix F α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (mk (F := F) (α := α)))
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)))
      x =
    x
rw₄ :
  MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α)
        (TypeVec.comp (α := α) (β := α) (γ := α) (TypeVec.id (α := α)) (TypeVec.id (α := α)))
        (mk (F := F) (α := α) ∘ fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)))
      x =
    x
rw₅ :
  MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α)
        (TypeVec.comp (α := α) (β := α) (γ := α) (TypeVec.id (α := α)) (TypeVec.id (α := α))) _root_.id)
      x =
    x
⊢ (mk (F := F) (α := α) x).dest (F := F) (α := α) = x
have rw₆ : MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Cofix F α)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) _root_.id) x =
  x
Tactic: rw [Cofix.mk, Cofix.dest_corec, ← comp_map, ← Cofix.mk, ← appendFun_comp, this, id_comp,
    appendFun_id_id, MvFunctor.id_map]
-- 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 y : Cofix F α
h : x.dest (F := F) (α := α) = y.dest (F := F) (α := α)
⊢ x = y
have rw : mk (F := F) (α := α) (x.dest (F := F) (α := α)) = y
Tactic: rw [← Cofix.mk_dest x, h, Cofix.mk_dest]
-- 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 y : Cofix F α
h : x.dest (F := F) (α := α) = y.dest (F := F) (α := α)
rw : mk (F := F) (α := α) (x.dest (F := F) (α := α)) = y
⊢ x = y
have rw₁ : mk (F := F) (α := α) (y.dest (F := F) (α := α)) = y
Tactic: rw [← Cofix.mk_dest x, h, Cofix.mk_dest]
-- 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 y : Cofix F α
h : x.dest (F := F) (α := α) = y.dest (F := F) (α := α)
rw : mk (F := F) (α := α) (x.dest (F := F) (α := α)) = y
rw₁ : mk (F := F) (α := α) (y.dest (F := F) (α := α)) = y
⊢ x = y
have rw₂ : y = y
Tactic: rw [← Cofix.mk_dest x, h, Cofix.mk_dest]
-- 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 y : F (α ::: Cofix F α)
h : mk (F := F) (α := α) x = mk (F := F) (α := α) y
⊢ x = y
have rw : (mk (F := F) (α := α) x).dest (F := F) (α := α) = y
Tactic: rw [← Cofix.dest_mk x, h, Cofix.dest_mk]
-- 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 y : F (α ::: Cofix F α)
h : mk (F := F) (α := α) x = mk (F := F) (α := α) y
rw : (mk (F := F) (α := α) x).dest (F := F) (α := α) = y
⊢ x = y
have rw₁ : (mk (F := F) (α := α) y).dest (F := F) (α := α) = y
Tactic: rw [← Cofix.dest_mk x, h, Cofix.dest_mk]
-- 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 y : F (α ::: Cofix F α)
h : mk (F := F) (α := α) x = mk (F := F) (α := α) y
rw : (mk (F := F) (α := α) x).dest (F := F) (α := α) = y
rw₁ : (mk (F := F) (α := α) y).dest (F := F) (α := α) = y
⊢ x = y
have rw₂ : y = y
Tactic: rw [← Cofix.dest_mk x, h, Cofix.dest_mk]
-- 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 (α := α))
⊢ LiftR' (α := β) (F := F') R (MvFunctor.map (F := F') (α := α) (β := β) f x)
    (MvFunctor.map (F := F') (α := α) (β := β) g x)
have rw : ∃ (u : F' (Subtype_ (α := β ⊗ β) R)),
  MvFunctor.map (F := F') (α := Subtype_ (α := β ⊗ β) R) (β := β)
        (TypeVec.comp (α := Subtype_ (α := β ⊗ β) R) (β := β ⊗ β) (γ := β) (prod.fst (α := β) (β := β))
          (subtypeVal (α := β ⊗ β) R))
        u =
      MvFunctor.map (F := F') (α := α) (β := β) f x ∧
    MvFunctor.map (F := F') (α := Subtype_ (α := β ⊗ β) R) (β := β)
        (TypeVec.comp (α := Subtype_ (α := β ⊗ β) R) (β := β ⊗ β) (γ := β) (prod.snd (α := β) (β := β))
          (subtypeVal (α := β ⊗ β) R))
        u =
      MvFunctor.map (F := F') (α := α) (β := β) g x
Tactic: rw [LiftR_def]
-- 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 (α := α))
⊢ ∃ (u : F' (Subtype_ (α := β ⊗ β) R)),
    MvFunctor.map (F := F') (α := Subtype_ (α := β ⊗ β) R) (β := β)
          (TypeVec.comp (α := Subtype_ (α := β ⊗ β) R) (β := β ⊗ β) (γ := β) (prod.fst (α := β) (β := β))
            (subtypeVal (α := β ⊗ β) R))
          u =
        MvFunctor.map (F := F') (α := α) (β := β) f x ∧
      MvFunctor.map (F := F') (α := Subtype_ (α := β ⊗ β) R) (β := β)
          (TypeVec.comp (α := Subtype_ (α := β ⊗ β) R) (β := β ⊗ β) (γ := β) (prod.snd (α := β) (β := β))
            (subtypeVal (α := β ⊗ β) R))
          u =
        MvFunctor.map (F := F') (α := α) (β := β) g x
have exists : 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
Tactic: exists h <$$> x