awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x_1 : Fix F α
x : F (α ::: Fix F α)
h :
  Eq (α := F (α ::: Fix F α))
    (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
        (mk (F := F) (α := α) ∘
          rec (F := F) (α := α)
            (MvFunctor.map (F := F) (α := α ::: F (α ::: Fix F α)) (β := α ::: Fix F α)
              (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (mk (F := F) (α := α))))))
      x)
    (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (x : Fix F α) ↦ x) x)
⊢ mk (F := F) (α := α)
      (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) _root_.id) x) =
    mk (F := F) (α := α) x
have h₁ : mk (F := F) (α := α)
    (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α) (TypeVec.id (α := α ::: Fix F α)) x) =
  mk (F := F) (α := α) x
Tactic: rw [appendFun_id_id, MvFunctor.id_map]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x_1 : Fix F α
x : F (α ::: Fix F α)
h :
  Eq (α := F (α ::: Fix F α))
    (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
        (mk (F := F) (α := α) ∘
          rec (F := F) (α := α)
            (MvFunctor.map (F := F) (α := α ::: F (α ::: Fix F α)) (β := α ::: Fix F α)
              (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (mk (F := F) (α := α))))))
      x)
    (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (x : Fix F α) ↦ x) x)
h₁ :
  mk (F := F) (α := α)
      (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α) (TypeVec.id (α := α ::: Fix F α)) x) =
    mk (F := F) (α := α) x
⊢ mk (F := F) (α := α)
      (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) _root_.id) x) =
    mk (F := F) (α := α) x
have h₂ : mk (F := F) (α := α) x = mk (F := F) (α := α) x
Tactic: rw [appendFun_id_id, MvFunctor.id_map]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Fix F α)
⊢ rec (F := F) (α := α)
      (MvFunctor.map (F := F) (α := α ::: F (α ::: Fix F α)) (β := α ::: Fix F α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (mk (F := F) (α := α))))
      (mk (F := F) (α := α) x) =
    x
have rw : MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α)
    (comp (α := α ::: Fix F α) (β := α ::: F (α ::: Fix F α)) (γ := α ::: Fix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (mk (F := F) (α := α)))
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (dest (F := F) (α := α))))
    x =
  x
Tactic: rw [Fix.rec_eq, ← Fix.dest, ← comp_map]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Fix F α)
| MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α)
      (comp (α := α ::: Fix F α) (β := α ::: F (α ::: Fix F α)) (γ := α ::: Fix F α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (mk (F := F) (α := α)))
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (dest (F := F) (α := α))))
      x =
    x
have rhs : x
Tactic: rhs
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Fix F α)
| x
have rw : MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α) (TypeVec.id (α := α ::: Fix F α)) x
Tactic: rw [← MvFunctor.id_map x]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Fix F α)
| MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α)
      (comp (α := α ::: Fix F α) (β := α ::: F (α ::: Fix F α)) (γ := α ::: Fix F α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (mk (F := F) (α := α)))
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (dest (F := F) (α := α))))
      x =
    x
have rw : MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α) (TypeVec.id (α := α ::: Fix F α)) x
Tactic: rhs
    rw [← MvFunctor.id_map x]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Fix F α)
⊢ MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α)
      (comp (α := α ::: Fix F α) (β := α ::: F (α ::: Fix F α)) (γ := α ::: Fix F α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (mk (F := F) (α := α)))
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (dest (F := F) (α := α))))
      x =
    x
have conv : MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α)
    (comp (α := α ::: Fix F α) (β := α ::: F (α ::: Fix F α)) (γ := α ::: Fix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (mk (F := F) (α := α)))
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (dest (F := F) (α := α))))
    x =
  MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α) (TypeVec.id (α := α ::: Fix F α)) x
Tactic: conv =>
    rhs
    rw [← MvFunctor.id_map x]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Fix F α)
⊢ MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α)
      (comp (α := α ::: Fix F α) (β := α ::: F (α ::: Fix F α)) (γ := α ::: Fix F α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (mk (F := F) (α := α)))
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (dest (F := F) (α := α))))
      x =
    MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α) (TypeVec.id (α := α ::: Fix F α)) x
have rw : MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (mk (F := F) (α := α) ∘ dest (F := F) (α := α))) x =
  MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α) (TypeVec.id (α := α ::: Fix F α)) x
Tactic: rw [← appendFun_comp, id_comp]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Fix F α)
⊢ Eq.{u + 1} (α := Fix F α → Fix F α) (mk (F := F) (α := α) ∘ dest (F := F) (α := α)) _root_.id
have h : ∀ (x : Fix F α), (mk (F := F) (α := α) ∘ dest (F := F) (α := α)) x = _root_.id x
Tactic: ext (x : Fix F α)
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (hypothesis)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Fix F α)
⊢ MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (mk (F := F) (α := α) ∘ dest (F := F) (α := α))) x =
    MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α) (TypeVec.id (α := α ::: Fix F α)) x
have this : Eq.{u + 1} (α := Fix F α → Fix F α) (mk (F := F) (α := α) ∘ dest (F := F) (α := α)) _root_.id
Tactic: have : Fix.mk ∘ Fix.dest (F := F) (α := α) = _root_.id := by
    ext (x : Fix F α)
    apply Fix.mk_dest
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Fix F α)
this : Eq.{u + 1} (α := Fix F α → Fix F α) (mk (F := F) (α := α) ∘ dest (F := F) (α := α)) _root_.id
⊢ MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (mk (F := F) (α := α) ∘ dest (F := F) (α := α))) x =
    MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α) (TypeVec.id (α := α ::: Fix F α)) x
have rw : MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) _root_.id) x =
  MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α) (TypeVec.id (α := α ::: Fix F α)) x
Tactic: rw [this, appendFun_id_id]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Fix F α)
this : Eq.{u + 1} (α := Fix F α → Fix F α) (mk (F := F) (α := α) ∘ dest (F := F) (α := α)) _root_.id
rw :
  MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) _root_.id) x =
    MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α) (TypeVec.id (α := α ::: Fix F α)) x
⊢ MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (mk (F := F) (α := α) ∘ dest (F := F) (α := α))) x =
    MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α) (TypeVec.id (α := α ::: Fix F α)) x
have rw₁ : MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α) (TypeVec.id (α := α ::: Fix F α)) x =
  MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α) (TypeVec.id (α := α ::: Fix F α)) x
Tactic: rw [this, appendFun_id_id]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (F := F) (α := α ::: Fix F α) (α.PredLast p) x → p (mk (F := F) (α := α) x)
⊢ ∀ (x : Fix F α), p x
have mk : ∀ (a : (P F).W α), p (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) a)
Tactic: apply Quot.ind
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (F := F) (α := α ::: Fix F α) (α.PredLast p) x → p (mk (F := F) (α := α) x)
x : (P F).W α
⊢ p (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) x)
have mk : ∀ (a : (P F).A) (f' : (P F).drop.B a ⟹ α) (f : (P F).last.B a → (P F).W α),
  (∀ (i : (P F).last.B a), p (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) (f i))) →
    p (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) ((P F).wMk (α := α) a f' f))
Tactic: induction x using q.P.wInd
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (F := F) (α := α ::: Fix F α) (α.PredLast p) x → p (mk (F := F) (α := α) x)
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
ih : ∀ (i : (P F).last.B a), p (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) (f i))
⊢ p (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) ((P F).wMk (α := α) a f' f))
have change : p ⟦(P F).wMk (α := α) a f' f⟧
Tactic: change p ⟦q.P.wMk a f' f⟧
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (F := F) (α := α ::: Fix F α) (α.PredLast p) x → p (mk (F := F) (α := α) x)
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
ih : ∀ (i : (P F).last.B a), p (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) (f i))
⊢ p ⟦(P F).wMk (α := α) a f' f⟧
have rw : p
  (mk (F := F) (α := α)
    (abs (F := F) (α := α ::: Fix F α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Fix F α) a
        ((P F).appendContents (α := α) f' fun (x : (P F).last.B a) ↦ ⟦f x⟧))))
Tactic: rw [← Fix.ind_aux a f' f]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (F := F) (α := α ::: Fix F α) (α.PredLast p) x → p (mk (F := F) (α := α) x)
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
ih : ∀ (i : (P F).last.B a), p (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) (f i))
⊢ p
    (mk (F := F) (α := α)
      (abs (F := F) (α := α ::: Fix F α)
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Fix F α) a
          ((P F).appendContents (α := α) f' fun (x : (P F).last.B a) ↦ ⟦f x⟧))))
have a₁ : LiftP (F := F) (α := α ::: Fix F α) (α.PredLast p)
  (abs (F := F) (α := α ::: Fix F α)
    (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Fix F α) a
      ((P F).appendContents (α := α) f' fun (x : (P F).last.B a) ↦ ⟦f x⟧)))
Tactic: apply h
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (F := F) (α := α ::: Fix F α) (α.PredLast p) x → p (mk (F := F) (α := α) x)
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
ih : ∀ (i : (P F).last.B a), p (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) (f i))
⊢ LiftP (F := F) (α := α ::: Fix F α) (α.PredLast p)
    (abs (F := F) (α := α ::: Fix F α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Fix F α) a
        ((P F).appendContents (α := α) f' fun (x : (P F).last.B a) ↦ ⟦f x⟧)))
have a₁ : ∃ (a_1 : (P F).A) (f_1 : (P F).B a_1 ⟹ α ::: Fix F α),
  Eq (α := F (α ::: Fix F α))
      (abs (F := F) (α := α ::: Fix F α)
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Fix F α) a
          ((P F).appendContents (α := α) f' fun (x : (P F).last.B a) ↦ ⟦f x⟧)))
      (abs (F := F) (α := α ::: Fix F α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Fix F α) a_1 f_1)) ∧
    ∀ (i : Fin2 (n + 1)) (j : (P F).B a_1 i), α.PredLast p (f_1 i j)
Tactic: rw [MvQPF.liftP_iff]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (F := F) (α := α ::: Fix F α) (α.PredLast p) x → p (mk (F := F) (α := α) x)
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
ih : ∀ (i : (P F).last.B a), p (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) (f i))
⊢ ∃ (a_1 : (P F).A) (f_1 : (P F).B a_1 ⟹ α ::: Fix F α),
    Eq (α := F (α ::: Fix F α))
        (abs (F := F) (α := α ::: Fix F α)
          (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Fix F α) a
            ((P F).appendContents (α := α) f' fun (x : (P F).last.B a) ↦ ⟦f x⟧)))
        (abs (F := F) (α := α ::: Fix F α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Fix F α) a_1 f_1)) ∧
      ∀ (i : Fin2 (n + 1)) (j : (P F).B a_1 i), α.PredLast p (f_1 i j)
have a₁ : ∀ (i : Fin2 (n + 1)) (j : (P F).B a i),
  α.PredLast p ((P F).appendContents (α := α) f' (fun (x : (P F).last.B a) ↦ ⟦f x⟧) i j)
Tactic: refine ⟨_, _, rfl, ?_⟩
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (F := F) (α := α ::: Fix F α) (α.PredLast p) x → p (mk (F := F) (α := α) x)
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
ih : ∀ (i : (P F).last.B a), p (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) (f i))
i : Fin2 (n + 1)
j : (P F).B a i
⊢ α.PredLast p ((P F).appendContents (α := α) f' (fun (x : (P F).last.B a) ↦ ⟦f x⟧) i j)
have a₁ : ∀ (j : (P F).B a Fin2.fz), α.PredLast p ((P F).appendContents (α := α) f' (fun (x : (P F).last.B a) ↦ ⟦f x⟧) Fin2.fz j)
Tactic: cases i
Cleared hypotheses: i, j
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (F := F) (α := α ::: Fix F α) (α.PredLast p) x → p (mk (F := F) (α := α) x)
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
ih : ∀ (i : (P F).last.B a), p (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) (f i))
i : Fin2 (n + 1)
j : (P F).B a i
a₁ :
  ∀ (j : (P F).B a Fin2.fz),
    α.PredLast p ((P F).appendContents (α := α) f' (fun (x : (P F).last.B a) ↦ ⟦f x⟧) Fin2.fz j)
⊢ α.PredLast p ((P F).appendContents (α := α) f' (fun (x : (P F).last.B a) ↦ ⟦f x⟧) i j)
have a₂ : ∀ (a_1 : Fin2 n) (j : (P F).B a a_1.fs),
  α.PredLast p ((P F).appendContents (α := α) f' (fun (x : (P F).last.B a) ↦ ⟦f x⟧) a_1.fs j)
Tactic: cases i
Cleared hypotheses: i, j
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α_1 α : TypeVec.{u} n
⊢ ∀ (x : Fix F α), Quot.mk (WEquiv (F := F) (α := α)) (fixToW (F := F) (α := α) x) = x
have mk : ∀ (a : (P F).W α),
  Eq (α := Fix F α)
    (Quot.mk (WEquiv (F := F) (α := α))
      (fixToW (F := F) (α := α) (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) a)))
    (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) a)
Tactic: apply Quot.ind
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α_1 α : TypeVec.{u} n
a : (P F).W α
⊢ Eq (α := Fix F α)
    (Quot.mk (WEquiv (F := F) (α := α))
      (fixToW (F := F) (α := α) (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) a)))
    (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) a)
have mk : WEquiv (F := F) (α := α) (fixToW (F := F) (α := α) (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) a)) a
Tactic: apply Quot.sound
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α_1 α β : TypeVec.{u} n
g : α ⟹ β
x : (↑(P F).wp : (α : TypeVec.{u} n) → Type u) α
| Eq (α := Fix F β)
    (Quot.mk (WEquiv (F := F) (α := β)) (map (F := (↑(P F).wp : (α : TypeVec.{u} n) → Type u)) (α := α) (β := β) g x))
    (map (F := Fix F) (α := α) (β := β) g (Quot.mk (WEquiv (F := F) (α := α)) x))
have rhs : map (F := Fix F) (α := α) (β := β) g (Quot.mk (WEquiv (F := F) (α := α)) x)
Tactic: rhs
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α_1 α β : TypeVec.{u} n
g : α ⟹ β
x : (↑(P F).wp : (α : TypeVec.{u} n) → Type u) α
| Eq (α := Fix F β)
    (Quot.mk (WEquiv (F := F) (α := β)) (map (F := (↑(P F).wp : (α : TypeVec.{u} n) → Type u)) (α := α) (β := β) g x))
    (map (F := Fix F) (α := α) (β := β) g (Quot.mk (WEquiv (F := F) (α := α)) x))
have dsimp : Fix.map (F := F) (α := α) (β := β) g (Quot.mk (WEquiv (F := F) (α := α)) x)
Tactic: rhs
      dsimp [MvFunctor.map]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Fix F α → Type u
g :
  (x : F (α ::: Sigma β)) →
    β
      (mk (F := F) (α := α)
        (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) x))
x : Fix F α
y : Sigma β :=
  rec (F := F) (α := α)
    (fun (i : F (α ::: Sigma β)) ↦
      Sigma.mk (β := β)
        (mk (F := F) (α := α)
          (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) i))
        (g i))
    x
⊢ x = y.fst (β := β)
have symm : y.fst (β := β) = x
Tactic: symm
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Fix F α → Type u
g :
  (x : F (α ::: Sigma β)) →
    β
      (mk (F := F) (α := α)
        (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) x))
x : Fix F α
y : Sigma β :=
  rec (F := F) (α := α)
    (fun (i : F (α ::: Sigma β)) ↦
      Sigma.mk (β := β)
        (mk (F := F) (α := α)
          (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) i))
        (g i))
    x
⊢ Sigma.fst (β := β)
      (rec (F := F) (α := α)
        (fun (i : F (α ::: Sigma β)) ↦
          Sigma.mk (β := β)
            (mk (F := F) (α := α)
              (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
                (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) i))
            (g i))
        x) =
    x
have apply : ∀ (x : F (α ::: Fix F α)),
  MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (x : Fix F α) ↦
          Sigma.fst (β := β)
            (rec (F := F) (α := α)
              (fun (i : F (α ::: Sigma β)) ↦
                Sigma.mk (β := β)
                  (mk (F := F) (α := α)
                    (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
                      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) i))
                  (g i))
              x))
        x =
      MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) _root_.id) x →
    Sigma.fst (β := β)
        (rec (F := F) (α := α)
          (fun (i : F (α ::: Sigma β)) ↦
            Sigma.mk (β := β)
              (mk (F := F) (α := α)
                (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
                  (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) i))
              (g i))
          (mk (F := F) (α := α) x)) =
      _root_.id (mk (F := F) (α := α) x)
Tactic: apply Fix.ind_rec _ id _ x