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
β : Type u
g₁ g₂ : Fix F α → β
h :
  ∀ (x : F (α ::: Fix F α)),
    MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₁)
          x =
        MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₂) x →
      g₁ (mk (F := F) (α := α) x) = g₂ (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),
    g₁ (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) (f i)) =
      g₂ (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) (f i))
⊢ g₁ ⟦(P F).wMk (α := α) a f' f⟧ = g₂ ⟦(P F).wMk (α := α) a f' f⟧
have rw : g₁
    (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⟧)))) =
  g₂
    (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
β : Type u
g₁ g₂ : Fix F α → β
h :
  ∀ (x : F (α ::: Fix F α)),
    MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₁)
          x =
        MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₂) x →
      g₁ (mk (F := F) (α := α) x) = g₂ (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),
    g₁ (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) (f i)) =
      g₂ (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) (f i))
⊢ g₁
      (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⟧)))) =
    g₂
      (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₁ : Eq (α := F (α ::: β))
  (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₁)
    (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⟧))))
  (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₂)
    (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
β : Type u
g₁ g₂ : Fix F α → β
h :
  ∀ (x : F (α ::: Fix F α)),
    MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₁)
          x =
        MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₂) x →
      g₁ (mk (F := F) (α := α) x) = g₂ (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),
    g₁ (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) (f i)) =
      g₂ (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) (f i))
⊢ Eq (α := F (α ::: β))
    (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₁)
      (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⟧))))
    (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₂)
      (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₁ : Eq (α := F (α ::: β))
  (abs (F := F) (α := α ::: β)
    (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: β) a
      (comp (α := (P F).B a) (β := α ::: Fix F α) (γ := α ::: β) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₁)
        ((P F).appendContents (α := α) f' fun (x : (P F).last.B a) ↦ ⟦f x⟧))))
  (abs (F := F) (α := α ::: β)
    (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: β) a
      (comp (α := (P F).B a) (β := α ::: Fix F α) (γ := α ::: β) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₂)
        ((P F).appendContents (α := α) f' fun (x : (P F).last.B a) ↦ ⟦f x⟧))))
Tactic: rw [← abs_map, ← abs_map, MvPFunctor.map_eq, MvPFunctor.map_eq]
-- 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
β : Type u
g₁ g₂ : Fix F α → β
h :
  ∀ (x : F (α ::: Fix F α)),
    MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₁)
          x =
        MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₂) x →
      g₁ (mk (F := F) (α := α) x) = g₂ (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),
    g₁ (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) (f i)) =
      g₂ (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) (f i))
⊢ Eq (α := F (α ::: β))
    (abs (F := F) (α := α ::: β)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: β) a
        (comp (α := (P F).B a) (β := α ::: Fix F α) (γ := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₁)
          ((P F).appendContents (α := α) f' fun (x : (P F).last.B a) ↦ ⟦f x⟧))))
    (abs (F := F) (α := α ::: β)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: β) a
        (comp (α := (P F).B a) (β := α ::: Fix F α) (γ := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₂)
          ((P F).appendContents (α := α) f' fun (x : (P F).last.B a) ↦ ⟦f x⟧))))
have a₁ : comp (α := (P F).B a) (β := α ::: Fix F α) (γ := α ::: β) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₁)
    ((P F).appendContents (α := α) f' fun (x : (P F).last.B a) ↦ ⟦f x⟧) =
  comp (α := (P F).B a) (β := α ::: Fix F α) (γ := α ::: β) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₂)
    ((P F).appendContents (α := α) f' fun (x : (P F).last.B a) ↦ ⟦f x⟧)
Tactic: congr 2
-- 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
β : Type u
g₁ g₂ : Fix F α → β
h :
  ∀ (x : F (α ::: Fix F α)),
    MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₁)
          x =
        MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₂) x →
      g₁ (mk (F := F) (α := α) x) = g₂ (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),
    g₁ (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) (f i)) =
      g₂ (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) (f i))
⊢ comp (α := (P F).B a) (β := α ::: Fix F α) (γ := α ::: β) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₁)
      ((P F).appendContents (α := α) f' fun (x : (P F).last.B a) ↦ ⟦f x⟧) =
    comp (α := (P F).B a) (β := α ::: Fix F α) (γ := α ::: β) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₂)
      ((P F).appendContents (α := α) f' fun (x : (P F).last.B a) ↦ ⟦f x⟧)
have a₁ : splitFun (α := (P F).B a) (α' := α ::: β)
    (comp (α := ((P F).B a).drop) (β := (α ::: Fix F α).drop) (γ := (α ::: β).drop) (TypeVec.id (α := α)) f')
    (g₁ ∘ fun (x : (P F).last.B a) ↦ ⟦f x⟧) =
  splitFun (α := (P F).B a) (α' := α ::: β)
    (comp (α := ((P F).B a).drop) (β := (α ::: Fix F α).drop) (γ := (α ::: β).drop) (TypeVec.id (α := α)) f')
    (g₂ ∘ fun (x : (P F).last.B a) ↦ ⟦f x⟧)
Tactic: rw [MvPFunctor.appendContents, appendFun, appendFun, ← splitFun_comp, ← splitFun_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
β : Type u
g₁ g₂ : Fix F α → β
h :
  ∀ (x : F (α ::: Fix F α)),
    MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₁)
          x =
        MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₂) x →
      g₁ (mk (F := F) (α := α) x) = g₂ (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),
    g₁ (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) (f i)) =
      g₂ (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) (f i))
⊢ Eq (α := (P F).last.B a → β) (g₁ ∘ fun (x : (P F).last.B a) ↦ ⟦f x⟧) (g₂ ∘ fun (x : (P F).last.B a) ↦ ⟦f x⟧)
have h₁ : ∀ (x : (P F).last.B a), (g₁ ∘ fun (x : (P F).last.B a) ↦ ⟦f x⟧) x = (g₂ ∘ fun (x : (P F).last.B a) ↦ ⟦f x⟧) x
Tactic: ext x
-- 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
β : Type u
g₁ g₂ : Fix F α → β
h :
  ∀ (x : F (α ::: Fix F α)),
    MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₁)
          x =
        MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₂) x →
      g₁ (mk (F := F) (α := α) x) = g₂ (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),
    g₁ (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) (f i)) =
      g₂ (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) (f i))
⊢ splitFun (α := (P F).B a) (α' := α ::: β)
      (comp (α := ((P F).B a).drop) (β := (α ::: Fix F α).drop) (γ := (α ::: β).drop) (TypeVec.id (α := α)) f')
      (g₁ ∘ fun (x : (P F).last.B a) ↦ ⟦f x⟧) =
    splitFun (α := (P F).B a) (α' := α ::: β)
      (comp (α := ((P F).B a).drop) (β := (α ::: Fix F α).drop) (γ := (α ::: β).drop) (TypeVec.id (α := α)) f')
      (g₂ ∘ fun (x : (P F).last.B a) ↦ ⟦f x⟧)
have this : Eq (α := (P F).last.B a → β) (g₁ ∘ fun (x : (P F).last.B a) ↦ ⟦f x⟧) (g₂ ∘ fun (x : (P F).last.B a) ↦ ⟦f x⟧)
Tactic: have : (g₁ ∘ fun x => ⟦f x⟧) = g₂ ∘ fun x => ⟦f x⟧ := by
      ext x
      exact ih 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
β : Type u
g₁ g₂ : Fix F α → β
h :
  ∀ (x : F (α ::: Fix F α)),
    MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₁)
          x =
        MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₂) x →
      g₁ (mk (F := F) (α := α) x) = g₂ (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),
    g₁ (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) (f i)) =
      g₂ (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) (f i))
this : Eq (α := (P F).last.B a → β) (g₁ ∘ fun (x : (P F).last.B a) ↦ ⟦f x⟧) (g₂ ∘ fun (x : (P F).last.B a) ↦ ⟦f x⟧)
⊢ splitFun (α := (P F).B a) (α' := α ::: β)
      (comp (α := ((P F).B a).drop) (β := (α ::: Fix F α).drop) (γ := (α ::: β).drop) (TypeVec.id (α := α)) f')
      (g₁ ∘ fun (x : (P F).last.B a) ↦ ⟦f x⟧) =
    splitFun (α := (P F).B a) (α' := α ::: β)
      (comp (α := ((P F).B a).drop) (β := (α ::: Fix F α).drop) (γ := (α ::: β).drop) (TypeVec.id (α := α)) f')
      (g₂ ∘ fun (x : (P F).last.B a) ↦ ⟦f x⟧)
have a₁ : splitFun (α := (P F).B a) (α' := α ::: β)
    (comp (α := ((P F).B a).drop) (β := (α ::: Fix F α).drop) (γ := (α ::: β).drop) (TypeVec.id (α := α)) f')
    (g₂ ∘ fun (x : (P F).last.B a) ↦ ⟦f x⟧) =
  splitFun (α := (P F).B a) (α' := α ::: β)
    (comp (α := ((P F).B a).drop) (β := (α ::: Fix F α).drop) (γ := (α ::: β).drop) (TypeVec.id (α := α)) f')
    (g₂ ∘ fun (x : (P F).last.B a) ↦ ⟦f x⟧)
Tactic: rw [this]
-- 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
β : Type u
g : F (α ::: β) → β
h : Fix F α → β
hyp :
  ∀ (x : F (α ::: Fix F α)),
    h (mk (F := F) (α := α) x) =
      g
        (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) h) x)
⊢ rec (F := F) (α := α) g = h
have h₁ : ∀ (x : Fix F α), rec (F := F) (α := α) g x = h x
Tactic: ext 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
β : Type u
g : F (α ::: β) → β
h : Fix F α → β
hyp :
  ∀ (x : F (α ::: Fix F α)),
    h (mk (F := F) (α := α) x) =
      g
        (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) h) x)
x : Fix F α
⊢ rec (F := F) (α := α) g x = h x
have h₁ : ∀ (x : F (α ::: Fix F α)),
  MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (rec (F := F) (α := α) g)) x =
      MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) h)
        x →
    rec (F := F) (α := α) g (mk (F := F) (α := α) x) = h (mk (F := F) (α := α) x)
Tactic: apply Fix.ind_rec
-- 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
β : Type u
g : F (α ::: β) → β
h : Fix F α → β
hyp :
  ∀ (x : F (α ::: Fix F α)),
    h (mk (F := F) (α := α) x) =
      g
        (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) h) x)
x_1 : Fix F α
x : F (α ::: Fix F α)
hyp' :
  MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (rec (F := F) (α := α) g)) x =
    MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) h) x
⊢ rec (F := F) (α := α) g (mk (F := F) (α := α) x) = h (mk (F := F) (α := α) x)
have h₁ : rec (F := F) (α := α) g (mk (F := F) (α := α) x) =
  g
    (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) h)
      x)
Tactic: rw [hyp, ← hyp', Fix.rec_eq]
-- 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
β : Type u
g : F (α ::: β) → β
h : Fix F α → β
hyp :
  ∀ (x : F (α ::: Fix F α)),
    h (mk (F := F) (α := α) x) =
      g
        (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) h) x)
x_1 : Fix F α
x : F (α ::: Fix F α)
hyp' :
  MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (rec (F := F) (α := α) g)) x =
    MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) h) x
h₁ :
  rec (F := F) (α := α) g (mk (F := F) (α := α) x) =
    g
      (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) h)
        x)
⊢ rec (F := F) (α := α) g (mk (F := F) (α := α) x) = h (mk (F := F) (α := α) x)
have h₂ : rec (F := F) (α := α) g (mk (F := F) (α := α) x) =
  g
    (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (rec (F := F) (α := α) g)) x)
Tactic: rw [hyp, ← hyp', Fix.rec_eq]
-- 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
β : Type u
g : F (α ::: β) → β
h : Fix F α → β
hyp :
  ∀ (x : F (α ::: Fix F α)),
    h (mk (F := F) (α := α) x) =
      g
        (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) h) x)
x_1 : Fix F α
x : F (α ::: Fix F α)
hyp' :
  MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (rec (F := F) (α := α) g)) x =
    MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) h) x
h₁ :
  rec (F := F) (α := α) g (mk (F := F) (α := α) x) =
    g
      (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) h)
        x)
h₂ :
  rec (F := F) (α := α) g (mk (F := F) (α := α) x) =
    g
      (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (rec (F := F) (α := α) g)) x)
⊢ rec (F := F) (α := α) g (mk (F := F) (α := α) x) = h (mk (F := F) (α := α) x)
have h₃ : g
    (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (rec (F := F) (α := α) g)) x) =
  g
    (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (rec (F := F) (α := α) g)) x)
Tactic: rw [hyp, ← hyp', Fix.rec_eq]
-- 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 : Fix F α
⊢ (mk (F := F) (α := α) ∘ dest (F := F) (α := α)) x = x
have h : ∀ (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 α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (x : Fix F α) ↦ x) x →
    (mk (F := F) (α := α) ∘ dest (F := F) (α := α)) (mk (F := F) (α := α) x) = mk (F := F) (α := α) x
Tactic: apply Fix.ind_rec
-- 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 α)
⊢ 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 α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (x : Fix F α) ↦ x) x →
    mk (F := F) (α := α) ((mk (F := F) (α := α) x).dest (F := F) (α := α)) = mk (F := F) (α := α) x
have 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 (α := α))
          (mk (F := F) (α := α) ∘
            rec (F := F) (α := α)
              (MvFunctor.map (F := F) (α := α ::: F (α ::: Fix F α)) (β := α ::: Fix F α)
                (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (mk (F := F) (α := α))))))
        x) =
    mk (F := F) (α := α) x
Tactic: rw [Fix.dest, Fix.rec_eq, ← comp_map, ← 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_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 (α := α))
          (mk (F := F) (α := α) ∘
            rec (F := F) (α := α)
              (MvFunctor.map (F := F) (α := α ::: F (α ::: Fix F α)) (β := α ::: Fix F α)
                (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (mk (F := F) (α := α))))))
        x) =
    mk (F := F) (α := α) x
have h₁ : mk (F := F) (α := α)
    (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (x : Fix F α) ↦ x) x) =
  mk (F := F) (α := α) x
Tactic: rw [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
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 (α := α)) fun (x : Fix F α) ↦ x) x) =
    mk (F := F) (α := α) x
have h₁ : mk (F := F) (α := α)
    (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) _root_.id) x) =
  mk (F := F) (α := α) x
Tactic: change Fix.mk (appendFun id id <$$> x) = Fix.mk x