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
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)
⊢ 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₁)))))
have 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₁))))
Tactic: rw [appendFun_comp_splitFun, appendFun_comp_splitFun]
-- 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 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)
⊢ 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₁))))
have 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₁))))
Tactic: rw [id_comp, id_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 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)
⊢ 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₁))))
have 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
Tactic: congr 2 with (i j)
-- 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 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
⊢ 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
have 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
Tactic: rcases i with - | i
Cleared hypotheses: i, j
-- 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 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
⊢ 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
have 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
Tactic: rcases i with - | i
Cleared hypotheses: i, j
-- 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 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
⊢ 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
have 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)
Tactic: apply Quot.sound
-- 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 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
⊢ 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
have h₁ : f₀ i.fs j = f₁ i.fs j
Tactic: change f₀ _ j = f₁ _ j
-- 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 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
⊢ LiftR (F := F) (α := α ::: Cofix F α) (α.RelLast r) (x.dest (F := F) (α := α)) (y.dest (F := F) (α := α))
have rw : LiftR' (α := α ::: Cofix F α) (F := F) (α.RelLast' r) (x.dest (F := F) (α := α)) (y.dest (F := F) (α := α))
Tactic: rw [← LiftR_RelLast_iff]
-- 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_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'
⊢ LiftR (F := F) (α := α ::: Cofix F α) (α.RelLast R) (x.dest (F := F) (α := α)) (y.dest (F := F) (α := α))
have 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) (α := α))
Tactic: rcases h x' Qx' with ⟨a, f', f₀, f₁, ux'eq, vx'eq, 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
β : 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'
⊢ LiftR (F := F) (α := α ::: Cofix F α) (α.RelLast R) (x.dest (F := F) (α := α)) (y.dest (F := F) (α := α))
have 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)
Tactic: rw [liftR_iff]
-- 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_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)
have f'₁ : ∀ (i : Fin2 (n + 1)) (j : (P F).B a i),
  α.RelLast R ((P F).appendContents (α := α) f' f₀ i j) ((P F).appendContents (α := α) f' f₁ i j)
Tactic: refine
        ⟨a, q.P.appendContents f' f₀, q.P.appendContents f' f₁, xeq.symm ▸ ux'eq,
          yeq.symm ▸ vx'eq, ?_⟩