awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : Fix F α
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
⊢ (mk (F := F) (α := α) ∘ dest (F := F) (α := α)) x = x

Tactic:
apply Fix.ind_rec

Premises used: MvQPF.Fix.ind_rec
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
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
⊢ 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

Tactic:
rw [Fix.dest, Fix.rec_eq, ← comp_map, ← appendFun_comp, id_comp]

Premises used: MvQPF.comp_map, TypeVec.appendFun_comp, TypeVec.id_comp, MvQPF.Fix.dest, MvQPF.Fix.rec_eq
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
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 α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (x : Fix F α) ↦ x) x) =
    mk (F := F) (α := α) 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 [h]
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
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 α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) _root_.id) x) =
    mk (F := F) (α := α) 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

Tactic:
change Fix.mk (appendFun id id <$$> x) = Fix.mk x

Premises used: MvQPF.Fix.mk, id, TypeVec.appendFun, MvFunctor.map, TypeVec.id
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
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
h₂ h₃ : mk (F := 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

Tactic:
rw [appendFun_id_id, MvFunctor.id_map]

Premises used: MvFunctor.id_map, TypeVec.appendFun_id_id
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Fix F α)
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
⊢ rec (F := F) (α := α)
      (MvFunctor.map (F := F) (α := α ::: F (α ::: Fix F α)) (β := α ::: Fix F α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (mk (F := F) (α := α))))
      (mk (F := F) (α := α) x) =
    x

Tactic:
rw [Fix.rec_eq, ← Fix.dest, ← comp_map]

Premises used: MvQPF.comp_map, MvQPF.Fix.dest, MvQPF.Fix.rec_eq
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Fix F α)
rhs : x
| 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:
rhs
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Fix F α)
rw : MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α) (TypeVec.id (α := α ::: Fix F α)) x
| x

Tactic:
rw [← MvFunctor.id_map x]

Premises used: MvFunctor.id_map
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Fix F α)
rw : MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α) (TypeVec.id (α := α ::: Fix F α)) x
| 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:
rhs
    rw [← MvFunctor.id_map x]

Premises used: MvFunctor.id_map
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Fix F α)
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
⊢ 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:
conv =>
    rhs
    rw [← MvFunctor.id_map x]

Premises used: MvFunctor.id_map
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Fix F α)
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
⊢ 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:
rw [← appendFun_comp, id_comp]

Premises used: TypeVec.appendFun_comp, TypeVec.id_comp
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Fix F α)
h : ∀ (x : Fix F α), (mk (F := F) (α := α) ∘ dest (F := F) (α := α)) x = _root_.id x
⊢ Eq.{u + 1} (α := Fix F α → Fix F α) (mk (F := F) (α := α) ∘ dest (F := F) (α := α)) _root_.id

Tactic:
ext (x : Fix F α)

Premises used: MvQPF.Fix
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x_1 : F (α ::: Fix F α)
x : Fix F α
⊢ (mk (F := F) (α := α) ∘ dest (F := F) (α := α)) x = _root_.id x

Tactic:
apply Fix.mk_dest

Premises used: MvQPF.Fix.mk_dest
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
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

Tactic:
have : Fix.mk ∘ Fix.dest (F := F) (α := α) = _root_.id := by
    ext (x : Fix F α)
    apply Fix.mk_dest
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
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
rw₁ 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
⊢ 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 [this, appendFun_id_id]

Premises used: TypeVec.appendFun_id_id
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
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 (Fix.mk (F := F) (α := α) x)
mk : ∀ (a : (P F).W α), p (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) a)
⊢ ∀ (x : Fix F α), p x

Tactic:
apply Quot.ind

Premises used: Quot.ind
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
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 (Fix.mk (F := F) (α := α) x)
x : (P F).W α
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))
⊢ p (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) x)

Tactic:
induction x using q.P.wInd
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
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))
change : p ⟦(P F).wMk (α := α) a f' f⟧
⊢ p (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) ((P F).wMk (α := α) a f' f))

Tactic:
change p ⟦q.P.wMk a f' f⟧

Premises used: Quotient.mk, MvQPF.P, MvPFunctor.wMk
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
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))
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⟧))))
⊢ p ⟦(P F).wMk (α := α) a f' f⟧

Tactic:
rw [← Fix.ind_aux a f' f]

Premises used: MvQPF.Fix.ind_aux
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
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₁ :
  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⟧)))
⊢ 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:
apply h
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
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₁ :
  ∃ (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)
⊢ 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:
rw [MvQPF.liftP_iff]

Premises used: MvQPF.liftP_iff
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
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)

Tactic:
⟨_, _, rfl, ?_⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
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₁ :
  ∀ (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)
⊢ ∃ (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:
refine ⟨_, _, rfl, ?_⟩
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
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)
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)
⊢ α.PredLast p ((P F).appendContents (α := α) f' (fun (x : (P F).last.B a) ↦ ⟦f x⟧) i j)

Tactic:
cases i
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
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))
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:
apply ih
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
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 : 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:
trivial
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α_1 α : TypeVec.{u} n
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)
⊢ ∀ (x : Fix F α), Quot.mk (WEquiv (F := F) (α := α)) (fixToW (F := F) (α := α) x) = x

Tactic:
apply Quot.ind

Premises used: Quot.ind
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α_1 α : TypeVec.{u} n
a : (P F).W α
mk : WEquiv (F := F) (α := α) (fixToW (F := F) (α := α) (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) a)) a
⊢ 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.sound

Premises used: Quot.sound
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α_1 α : TypeVec.{u} n
a : (P F).W α
⊢ WEquiv (F := F) (α := α) (fixToW (F := F) (α := α) (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) a)) a

Tactic:
apply wrepr_equiv

Premises used: MvQPF.wrepr_equiv
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
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) α
rhs : map (F := Fix F) (α := α) (β := β) g (Quot.mk (WEquiv (F := F) (α := α)) x)
| 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))

Tactic:
rhs
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
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) α
dsimp : Fix.map (F := F) (α := α) (β := β) g (Quot.mk (WEquiv (F := F) (α := α)) x)
| 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))

Tactic:
rhs
      dsimp [MvFunctor.map]

Premises used: MvFunctor.map