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
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr (F := F) (α := α) r
ra₁a₂_1 : r aa₁ aa₂
r' : (b₁ b₂ : (P F).M β) → Prop :=
  fun (b₁ b₂ : (P F).M β) ↦
    ∃ (a₁ : (P F).M α) (a₂ : (P F).M α),
      r a₁ a₂ ∧
        b₁ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₁ ∧
          b₂ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₂
b₁ b₂ : (P F).M β
a₁ a₂ : (P F).M α
ra₁a₂ : r a₁ a₂
b₁eq : b₁ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₁
b₂eq : b₂ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₂
u : Quot r → Quot r' :=
  Quot.lift (r := r) (fun (x : (P F).M α) ↦ Quot.mk r' (MvFunctor.map (F := (P F).M) (α := α) (β := β) g x)) ⋯
hu : (Quot.mk r' ∘ fun (x : (P F).M α) ↦ MvFunctor.map (F := (P F).M) (α := α) (β := β) g x) = u ∘ Quot.mk r
⊢ abs (F := F) (α := β ::: Quot r')
      (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).M α) (β := β ::: Quot r')
        (TypeVec.comp (α := α ::: (P F).M α) (β := β ::: (P F).M β) (γ := β ::: Quot r')
          (appendFun (α := β) (α' := β) (TypeVec.id (α := β)) (Quot.mk r'))
          (appendFun (α := α) (α' := β) g fun (x : (P F).M α) ↦ MvFunctor.map (F := (P F).M) (α := α) (β := β) g x))
        (M.dest (P F) (α := α) a₁)) =
    abs (F := F) (α := β ::: Quot r')
      (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).M α) (β := β ::: Quot r')
        (TypeVec.comp (α := α ::: (P F).M α) (β := β ::: (P F).M β) (γ := β ::: Quot r')
          (appendFun (α := β) (α' := β) (TypeVec.id (α := β)) (Quot.mk r'))
          (appendFun (α := α) (α' := β) g fun (x : (P F).M α) ↦ MvFunctor.map (F := (P F).M) (α := α) (β := β) g x))
        (M.dest (P F) (α := α) a₂))
have h : abs (F := F) (α := β ::: Quot r')
    (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).M α) (β := β ::: Quot r')
      (TypeVec.comp (α := α ::: (P F).M α) (β := α ::: Quot r) (γ := β ::: Quot r') (appendFun (α := α) (α' := β) g u)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)))
      (M.dest (P F) (α := α) a₁)) =
  abs (F := F) (α := β ::: Quot r')
    (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).M α) (β := β ::: Quot r')
      (TypeVec.comp (α := α ::: (P F).M α) (β := α ::: Quot r) (γ := β ::: Quot r') (appendFun (α := α) (α' := β) g u)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)))
      (M.dest (P F) (α := α) a₂))
Tactic: rw [← appendFun_comp, id_comp, hu, ← comp_id g, appendFun_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
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr (F := F) (α := α) r
ra₁a₂_1 : r aa₁ aa₂
r' : (b₁ b₂ : (P F).M β) → Prop :=
  fun (b₁ b₂ : (P F).M β) ↦
    ∃ (a₁ : (P F).M α) (a₂ : (P F).M α),
      r a₁ a₂ ∧
        b₁ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₁ ∧
          b₂ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₂
b₁ b₂ : (P F).M β
a₁ a₂ : (P F).M α
ra₁a₂ : r a₁ a₂
b₁eq : b₁ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₁
b₂eq : b₂ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₂
u : Quot r → Quot r' :=
  Quot.lift (r := r) (fun (x : (P F).M α) ↦ Quot.mk r' (MvFunctor.map (F := (P F).M) (α := α) (β := β) g x)) ⋯
hu : (Quot.mk r' ∘ fun (x : (P F).M α) ↦ MvFunctor.map (F := (P F).M) (α := α) (β := β) g x) = u ∘ Quot.mk r
⊢ abs (F := F) (α := β ::: Quot r')
      (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).M α) (β := β ::: Quot r')
        (TypeVec.comp (α := α ::: (P F).M α) (β := α ::: Quot r) (γ := β ::: Quot r') (appendFun (α := α) (α' := β) g u)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)))
        (M.dest (P F) (α := α) a₁)) =
    abs (F := F) (α := β ::: Quot r')
      (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).M α) (β := β ::: Quot r')
        (TypeVec.comp (α := α ::: (P F).M α) (β := α ::: Quot r) (γ := β ::: Quot r') (appendFun (α := α) (α' := β) g u)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)))
        (M.dest (P F) (α := α) a₂))
have h : abs (F := F) (α := β ::: Quot r')
    (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: Quot r) (β := β ::: Quot r')
      (appendFun (α := α) (α' := β) g u)
      (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).M α) (β := α ::: Quot r)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (M.dest (P F) (α := α) a₁))) =
  abs (F := F) (α := β ::: Quot r')
    (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).M α) (β := β ::: Quot r')
      (TypeVec.comp (α := α ::: (P F).M α) (β := α ::: Quot r) (γ := β ::: Quot r') (appendFun (α := α) (α' := β) g u)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)))
      (M.dest (P F) (α := α) a₂))
Tactic: rw [q.P.comp_map, q.P.comp_map, abs_map, pr ra₁a₂, ← abs_map]
-- 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 y : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr (F := F) (α := α) r
rxy : r x y
⊢ Eq (α := F (α ::: Cofix F α))
    (MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
      (abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) x)))
    (MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
      (abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) y)))
have this : ∀ (x y : (P F).M α), r x y → Mcongr (F := F) (α := α) x y
Tactic: have : ∀ x y, r x y → Mcongr x y := by
        intro x y h
        exact ⟨r, pr, 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
x y : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr (F := F) (α := α) r
rxy : r x y
this : ∀ (x y : (P F).M α), r x y → Mcongr (F := F) (α := α) x y
⊢ Eq (α := F (α ::: Cofix F α))
    (MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
      (abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) x)))
    (MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
      (abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) y)))
have rw : MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r (Mcongr (F := F) (α := α)) this ∘ Quot.mk r))
    (abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) x)) =
  MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r (Mcongr (F := F) (α := α)) this ∘ Quot.mk r))
    (abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) y))
Tactic: rw [← Quot.factor_mk_eq _ _ 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 y : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr (F := F) (α := α) r
rxy : r x y
this : ∀ (x y : (P F).M α), r x y → Mcongr (F := F) (α := α) x y
| MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r (Mcongr (F := F) (α := α)) this ∘ Quot.mk r))
      (abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) x)) =
    MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r (Mcongr (F := F) (α := α)) this ∘ Quot.mk r))
      (abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) y))
have lhs : MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
  (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r (Mcongr (F := F) (α := α)) this ∘ Quot.mk r))
  (abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) x))
Tactic: lhs
-- 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 : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr (F := F) (α := α) r
rxy : r x y
this : ∀ (x y : (P F).M α), r x y → Mcongr (F := F) (α := α) x y
| MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r (Mcongr (F := F) (α := α)) this ∘ Quot.mk r))
    (abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) x))
have rw : MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
  (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r (Mcongr (F := F) (α := α)) this ∘ Quot.mk r))
  (abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) y))
Tactic: rw [appendFun_comp_id, comp_map, ← abs_map, pr rxy, abs_map, ← comp_map,
          ← appendFun_comp_id]
-- 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 : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr (F := F) (α := α) r
rxy : r x y
this : ∀ (x y : (P F).M α), r x y → Mcongr (F := F) (α := α) x y
| MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r (Mcongr (F := F) (α := α)) this ∘ Quot.mk r))
      (abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) x)) =
    MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r (Mcongr (F := F) (α := α)) this ∘ Quot.mk r))
      (abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) y))
have rw : MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
  (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r (Mcongr (F := F) (α := α)) this ∘ Quot.mk r))
  (abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) y))
Tactic: lhs
        rw [appendFun_comp_id, comp_map, ← abs_map, pr rxy, abs_map, ← comp_map,
          ← appendFun_comp_id]
-- 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 : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr (F := F) (α := α) r
rxy : r x y
this : ∀ (x y : (P F).M α), r x y → Mcongr (F := F) (α := α) x y
⊢ MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r (Mcongr (F := F) (α := α)) this ∘ Quot.mk r))
      (abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) x)) =
    MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r (Mcongr (F := F) (α := α)) this ∘ Quot.mk r))
      (abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) y))
have conv : MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r (Mcongr (F := F) (α := α)) this ∘ Quot.mk r))
    (abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) x)) =
  MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r (Mcongr (F := F) (α := α)) this ∘ Quot.mk r))
    (abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) y))
Tactic: conv =>
        lhs
        rw [appendFun_comp_id, comp_map, ← abs_map, pr rxy, abs_map, ← comp_map,
          ← appendFun_comp_id]
-- 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 : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr (F := F) (α := α) r
rxy : r x y
this : ∀ (x y : (P F).M α), r x y → Mcongr (F := F) (α := α) x y
conv :
  MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r (Mcongr (F := F) (α := α)) this ∘ Quot.mk r))
      (abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) x)) =
    MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r (Mcongr (F := F) (α := α)) this ∘ Quot.mk r))
      (abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) y))
⊢ MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r (Mcongr (F := F) (α := α)) this ∘ Quot.mk r))
      (abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) x)) =
    MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r (Mcongr (F := F) (α := α)) this ∘ Quot.mk r))
      (abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) y))
have conv₁ : MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r (Mcongr (F := F) (α := α)) this ∘ Quot.mk r))
    (abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) y)) =
  MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r (Mcongr (F := F) (α := α)) this ∘ Quot.mk r))
    (abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) y))
Tactic: conv =>
        lhs
        rw [appendFun_comp_id, comp_map, ← abs_map, pr rxy, abs_map, ← comp_map,
          ← appendFun_comp_id]
-- 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
β : Type u
g : β → F (α ::: β)
x : β
| Eq (α := F (α ::: Cofix F α)) (dest (F := F) (α := α) (corec (F := F) (α := α) g x))
    (MvFunctor.map (F := F) (α := α ::: β) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (corec (F := F) (α := α) g)) (g x))
have lhs : dest (F := F) (α := α) (corec (F := F) (α := α) g x)
Tactic: lhs
-- 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
β : Type u
g : β → F (α ::: β)
x : β
| dest (F := F) (α := α) (corec (F := F) (α := α) g x)
have rw : Quot.lift (r := Mcongr (F := F) (α := α))
  (fun (x : (P F).M α) ↦
    MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
      (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) x)))
  sorry (Quot.mk (Mcongr (F := F) (α := α)) (corecF (F := F) (α := α) g x))
Tactic: rw [Cofix.dest, Cofix.corec]
-- 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
β : Type u
g : β → F (α ::: β)
x : β
| Eq (α := F (α ::: Cofix F α)) (dest (F := F) (α := α) (corec (F := F) (α := α) g x))
    (MvFunctor.map (F := F) (α := α ::: β) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (corec (F := F) (α := α) g)) (g x))
have rw : Quot.lift (r := Mcongr (F := F) (α := α))
  (fun (x : (P F).M α) ↦
    MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
      (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) x)))
  sorry (Quot.mk (Mcongr (F := F) (α := α)) (corecF (F := F) (α := α) g x))
Tactic: lhs
    rw [Cofix.dest, Cofix.corec]
-- 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
β : Type u
g : β → F (α ::: β)
x : β
⊢ Eq (α := F (α ::: Cofix F α)) (dest (F := F) (α := α) (corec (F := F) (α := α) g x))
    (MvFunctor.map (F := F) (α := α ::: β) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (corec (F := F) (α := α) g)) (g x))
have conv : Eq (α := F (α ::: Cofix F α))
  (Quot.lift (r := Mcongr (F := F) (α := α))
    (fun (x : (P F).M α) ↦
      MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
        (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) x)))
    sorry (Quot.mk (Mcongr (F := F) (α := α)) (corecF (F := F) (α := α) g x)))
  (MvFunctor.map (F := F) (α := α ::: β) (β := α ::: Cofix F α)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (corec (F := F) (α := α) g)) (g x))
Tactic: conv =>
    lhs
    rw [Cofix.dest, Cofix.corec]
-- 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
β : Type u
g : β → F (α ::: β)
x : β
⊢ MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
      (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) (corecF (F := F) (α := α) g x))) =
    MvFunctor.map (F := F) (α := α ::: β) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (corec (F := F) (α := α) g)) (g x)
have rw : Eq (α := F (α ::: Cofix F α))
  (MvFunctor.map (F := F) (α := α ::: β) (β := α ::: Cofix F α)
    (appendFun (α := α) (α' := α) (TypeVec.comp (α := α) (β := α) (γ := α) (TypeVec.id (α := α)) (TypeVec.id (α := α)))
      (Quot.mk (Mcongr (F := F) (α := α)) ∘ corecF (F := F) (α := α) g))
    (g x))
  (MvFunctor.map (F := F) (α := α ::: β) (β := α ::: Cofix F α)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (corec (F := F) (α := α) g)) (g x))
Tactic: rw [corecF_eq, abs_map, abs_repr, ← comp_map, ← appendFun_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 : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h :
  ∀ (x y : Cofix F α),
    r x y →
      MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (x.dest (F := F) (α := α)) =
        MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (y.dest (F := F) (α := α))
x : Cofix F α
⊢ ∀ (y : Cofix F α), r x y → x = y
have mk : ∀ (a : (P F).M α) (y : Cofix F α), r (Quot.mk (Mcongr (F := F) (α := α)) a) y → Quot.mk (Mcongr (F := F) (α := α)) a = y
Tactic: rcases 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
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h :
  ∀ (x y : Cofix F α),
    r x y →
      MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (x.dest (F := F) (α := α)) =
        MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (y.dest (F := F) (α := α))
x : (P F).M α
y : Cofix F α
⊢ r (Quot.mk (Mcongr (F := F) (α := α)) x) y → Quot.mk (Mcongr (F := F) (α := α)) x = y
have mk : ∀ (a : (P F).M α),
  r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) a) →
    Eq (α := Cofix F α) (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) a)
Tactic: rcases 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 : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h :
  ∀ (x y : Cofix F α),
    r x y →
      MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (x.dest (F := F) (α := α)) =
        MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (y.dest (F := F) (α := α))
x y : (P F).M α
rxy : r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
⊢ Eq (α := Cofix F α) (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
have mk : Mcongr (F := F) (α := α) x y
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
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h :
  ∀ (x y : Cofix F α),
    r x y →
      MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (x.dest (F := F) (α := α)) =
        MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (y.dest (F := F) (α := α))
x y : (P F).M α
rxy : r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
r' : (x y : (P F).M α) → Prop :=
  fun (x y : (P F).M α) ↦ r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
⊢ Mcongr (F := F) (α := α) x y
have hr' : r' = fun (x y : (P F).M α) ↦ r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
Tactic: have hr' : r' = fun x y => r (Quot.mk _ x) (Quot.mk _ y) := rfl