awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.W (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.A
f' : P.drop.B a ⟹ α
f : P.last.B a → P.W α
this_1 :
  MvFunctor.map (F := P.W) (α := α) (β := β) g ∘ f = fun (i : P.last.B a) ↦
    Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ β) ((f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))
      (TypeVec.comp (α := P.wp.B ((f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))) (β := α) (γ := β) g
        ((f i).snd (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α)))
this :
  f = fun (i : P.last.B a) ↦
    Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α) ((f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))
      ((f i).snd (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))
⊢ MvFunctor.map (F := P.W) (α := α) (β := β) g
      (P.wMk (α := α) a f' fun (i : P.last.B a) ↦
        Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α) ((f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))
          ((f i).snd (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))) =
    P.wMk (α := β) a (TypeVec.comp (α := P.drop.B a) (β := α) (γ := β) g f') fun (i : P.last.B a) ↦
      Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ β) ((f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))
        (TypeVec.comp (α := P.wp.B ((f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))) (β := α) (γ := β) g
          ((f i).snd (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α)))
have rw : Eq (α := P.W β)
  (MvFunctor.map (F := P.W) (α := α) (β := β) g
    (Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α)
      (WType.mk (β := P.last.B) a fun (i : P.last.B a) ↦ (f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))
      (P.wPathCasesOn (α := α) f' fun (i : P.last.B a) ↦ (f i).snd (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))))
  (Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ β)
    (WType.mk (β := P.last.B) a fun (i : P.last.B a) ↦ (f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))
    (P.wPathCasesOn (α := β) (TypeVec.comp (α := P.drop.B a) (β := α) (γ := β) g f') fun (i : P.last.B a) ↦
      TypeVec.comp (α := P.wp.B ((f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))) (β := α) (γ := β) g
        ((f i).snd (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))))
Tactic: rw [wMk_eq, wMk_eq]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.W (hypothesis)
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.A
f' : P.drop.B a ⟹ α
f : P.last.B a → P.W α
this_1 :
  MvFunctor.map (F := P.W) (α := α) (β := β) g ∘ f = fun (i : P.last.B a) ↦
    Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ β) ((f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))
      (TypeVec.comp (α := P.wp.B ((f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))) (β := α) (γ := β) g
        ((f i).snd (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α)))
this :
  f = fun (i : P.last.B a) ↦
    Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α) ((f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))
      ((f i).snd (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))
⊢ Eq (α := P.W β)
    (MvFunctor.map (F := P.W) (α := α) (β := β) g
      (Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α)
        (WType.mk (β := P.last.B) a fun (i : P.last.B a) ↦ (f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))
        (P.wPathCasesOn (α := α) f' fun (i : P.last.B a) ↦ (f i).snd (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))))
    (Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ β)
      (WType.mk (β := P.last.B) a fun (i : P.last.B a) ↦ (f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))
      (P.wPathCasesOn (α := β) (TypeVec.comp (α := P.drop.B a) (β := α) (γ := β) g f') fun (i : P.last.B a) ↦
        TypeVec.comp (α := P.wp.B ((f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))) (β := α) (γ := β) g
          ((f i).snd (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))))
have h : ∀ (a : P.wp.A) (f : P.wp.B a ⟹ α),
  Eq (α := (↑P.wp : (α : TypeVec.{u} n) → Type u) β)
    (MvFunctor.map (F := (↑P.wp : (α : TypeVec.{u} n) → Type u)) (α := α) (β := β) g
      (Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α) a f))
    (Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ β) a (TypeVec.comp (α := P.wp.B a) (β := α) (γ := β) g f))
Tactic: have h := MvPFunctor.map_eq P.wp g
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.W (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.A
f' : P.drop.B a ⟹ α
f : P.last.B a → P.W α
this_1 :
  MvFunctor.map (F := P.W) (α := α) (β := β) g ∘ f = fun (i : P.last.B a) ↦
    Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ β) ((f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))
      (TypeVec.comp (α := P.wp.B ((f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))) (β := α) (γ := β) g
        ((f i).snd (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α)))
this :
  f = fun (i : P.last.B a) ↦
    Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α) ((f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))
      ((f i).snd (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))
h :
  ∀ (a : P.wp.A) (f : P.wp.B a ⟹ α),
    Eq (α := (↑P.wp : (α : TypeVec.{u} n) → Type u) β)
      (MvFunctor.map (F := (↑P.wp : (α : TypeVec.{u} n) → Type u)) (α := α) (β := β) g
        (Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α) a f))
      (Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ β) a (TypeVec.comp (α := P.wp.B a) (β := α) (γ := β) g f))
⊢ Eq (α := P.W β)
    (MvFunctor.map (F := P.W) (α := α) (β := β) g
      (Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α)
        (WType.mk (β := P.last.B) a fun (i : P.last.B a) ↦ (f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))
        (P.wPathCasesOn (α := α) f' fun (i : P.last.B a) ↦ (f i).snd (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))))
    (Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ β)
      (WType.mk (β := P.last.B) a fun (i : P.last.B a) ↦ (f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))
      (P.wPathCasesOn (α := β) (TypeVec.comp (α := P.drop.B a) (β := α) (γ := β) g f') fun (i : P.last.B a) ↦
        TypeVec.comp (α := P.wp.B ((f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))) (β := α) (γ := β) g
          ((f i).snd (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))))
have rw : Eq (α := P.W β)
  (Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ β)
    (WType.mk (β := P.last.B) a fun (i : P.last.B a) ↦ (f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))
    (TypeVec.comp (α :=
      P.wp.B (WType.mk (β := P.last.B) a fun (i : P.last.B a) ↦ (f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))) (β :=
      α) (γ := β) g
      (P.wPathCasesOn (α := α) f' fun (i : P.last.B a) ↦ (f i).snd (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))))
  (Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ β)
    (WType.mk (β := P.last.B) a fun (i : P.last.B a) ↦ (f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))
    (P.wPathCasesOn (α := β) (TypeVec.comp (α := P.drop.B a) (β := α) (γ := β) g f') fun (i : P.last.B a) ↦
      TypeVec.comp (α := P.wp.B ((f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))) (β := α) (γ := β) g
        ((f i).snd (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))))
Tactic: rw [h, comp_wPathCasesOn]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.W (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α γ : TypeVec.{u} n
g : α ⟹ γ
a : P.A
f' : P.drop.B a ⟹ α
f : P.last.B a → P.W α
⊢ MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.W α) (β := γ ::: P.W γ)
      (appendFun (α := α) (α' := γ) g (P.wMap (α := α) (β := γ) g)) (P.objAppend1 (α := α) a f' f) =
    P.objAppend1 (α := γ) a (TypeVec.comp (α := P.drop.B a) (β := α) (γ := γ) g f') fun (x : P.last.B a) ↦
      P.wMap (α := α) (β := γ) g (f x)
have rw : Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (γ ::: P.W γ))
  (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ γ ::: P.W γ) a
    (splitFun (α := P.B a) (α' := γ ::: P.W γ)
      (TypeVec.comp (α := (P.B a).drop) (β := (α ::: P.W α).drop) (γ := (γ ::: P.W γ).drop) g f')
      (P.wMap (α := α) (β := γ) g ∘ f)))
  (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ γ ::: P.W γ) a
    (splitFun (α := P.B a) (α' := γ ::: P.W γ) (TypeVec.comp (α := P.drop.B a) (β := α) (γ := γ) g f')
      fun (x : P.last.B a) ↦ P.wMap (α := α) (β := γ) g (f x)))
Tactic: rw [objAppend1, objAppend1, map_eq, appendFun, ← splitFun_comp]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.W (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
a : P.A
f' : P.drop.B a ⟹ α
f : P.last.B a → P.W α
⊢ P.wDest' (α := α) (P.wMk (α := α) a f' f) =
    Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.W α) a (splitFun (α := P.B a) (α' := α ::: P.W α) f' f)
have rw : Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.W α))
  (P.wRec (α := α)
    (fun (a : P.A) (f' : P.drop.B a ⟹ α) (f : P.last.B a → P.W α)
        (x : P.last.B a → (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.W α)) ↦
      Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.W α) a (splitFun (α := P.B a) (α' := α ::: P.W α) f' f))
    (P.wMk (α := α) a f' f))
  (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.W α) a (splitFun (α := P.B a) (α' := α ::: P.W α) f' f))
Tactic: rw [wDest', wRec_eq]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.W (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
a : P.A
f' : P.drop.B a ⟹ α
f : P.last.B a → P.W α
rw :
  Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.W α))
    (P.wRec (α := α)
      (fun (a : P.A) (f' : P.drop.B a ⟹ α) (f : P.last.B a → P.W α)
          (x : P.last.B a → (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.W α)) ↦
        Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.W α) a (splitFun (α := P.B a) (α' := α ::: P.W α) f' f))
      (P.wMk (α := α) a f' f))
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.W α) a (splitFun (α := P.B a) (α' := α ::: P.W α) f' f))
⊢ P.wDest' (α := α) (P.wMk (α := α) a f' f) =
    Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.W α) a (splitFun (α := P.B a) (α' := α ::: P.W α) f' f)
have rw₁ : Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.W α))
  (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.W α) a (splitFun (α := P.B a) (α' := α ::: P.W α) f' f))
  (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.W α) a (splitFun (α := P.B a) (α' := α ::: P.W α) f' f))
Tactic: rw [wDest', wRec_eq]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.W (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
x : (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.W α)
⊢ P.wDest' (α := α) (P.wMk' (α := α) x) = x
have obtain : ∀ (a : P.A) (f : P.B a ⟹ α ::: P.W α),
  Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.W α))
    (P.wDest' (α := α) (P.wMk' (α := α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.W α) a f)))
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.W α) a f)
Tactic: obtain ⟨a, f⟩ := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.W (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
a : P.A
f : P.B a ⟹ α ::: P.W α
⊢ Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.W α))
    (P.wDest' (α := α) (P.wMk' (α := α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.W α) a f)))
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.W α) a f)
have rw : P.wDest' (α := α)
    (P.wMk (α := α) a (dropFun (α := P.B a) (β := α ::: P.W α) f) (lastFun (α := P.B a) (β := α ::: P.W α) f)) =
  Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.W α) a f
Tactic: rw [wMk', wDest'_wMk, split_dropFun_lastFun]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.W (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
a : P.A
f : P.B a ⟹ α ::: P.W α
rw :
  P.wDest' (α := α)
      (P.wMk (α := α) a (dropFun (α := P.B a) (β := α ::: P.W α) f) (lastFun (α := P.B a) (β := α ::: P.W α) f)) =
    Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.W α) a f
⊢ Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.W α))
    (P.wDest' (α := α) (P.wMk' (α := α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.W α) a f)))
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.W α) a f)
have rw₁ : Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.W α))
  (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.W α) a
    (splitFun (α := P.B a) (α' := α ::: P.W α) (dropFun (α := P.B a) (β := α ::: P.W α) f)
      (lastFun (α := P.B a) (β := α ::: P.W α) f)))
  (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.W α) a f)
Tactic: rw [wMk', wDest'_wMk, split_dropFun_lastFun]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.W (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
a : P.A
f : P.B a ⟹ α ::: P.W α
rw :
  P.wDest' (α := α)
      (P.wMk (α := α) a (dropFun (α := P.B a) (β := α ::: P.W α) f) (lastFun (α := P.B a) (β := α ::: P.W α) f)) =
    Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.W α) a f
rw₁ :
  Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.W α))
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.W α) a
      (splitFun (α := P.B a) (α' := α ::: P.W α) (dropFun (α := P.B a) (β := α ::: P.W α) f)
        (lastFun (α := P.B a) (β := α ::: P.W α) f)))
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.W α) a f)
⊢ Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.W α))
    (P.wDest' (α := α) (P.wMk' (α := α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.W α) a f)))
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.W α) a f)
have rw₂ : Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.W α))
  (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.W α) a f) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.W α) a f)
Tactic: rw [wMk', wDest'_wMk, split_dropFun_lastFun]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.Basic (goal)
Goal:
P : PFunctor.{uA, uB}
p : (↑P : (α : Type (max uB uA)) → Type (max (max uB uA) uA uB)) P.W
⊢ (mk p).dest = p
have mk : ∀ (fst : P.A) (snd : P.B fst → P.W),
  (mk (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.W) fst snd)).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.W) fst snd
Tactic: cases p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.Basic (goal)
Goal:
P : PFunctor.{uA, uB}
p : P.W
⊢ mk p.dest = p
have mk : ∀ (a : P.A) (f : P.B a → WType P.B), mk (dest (WType.mk (β := P.B) a f)) = WType.mk (β := P.B) a f
Tactic: cases p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.Basic (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type v₁
β : Type v₂
x : (↑P : (α : Type v₁) → Type (max v₁ uA uB)) α
f : α → β
⊢ (P.map f x).fst (β := fun (x : P.A) ↦ P.B x → β) = x.fst (β := fun (x : P.A) ↦ P.B x → α)
have mk : ∀ (fst : P.A) (snd : P.B fst → α),
  (P.map f (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) fst snd)).fst (β := fun (x : P.A) ↦ P.B x → β) =
    Sigma.fst (β := fun (x : P.A) ↦ P.B x → α) (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) fst snd)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.Basic (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type v₁
β : Type v₂
inst : DecidableEq P.A
inst_1 : Inhabited α
inst_2 : Inhabited β
x : (↑P : (α : Type v₁) → Type (max v₁ uA uB)) α
f : α → β
i : P.Idx
h : i.fst (β := fun (x : P.A) ↦ P.B x) = x.fst (β := fun (x : P.A) ↦ P.B x → α)
⊢ (P.map f x).iget i = f (x.iget i)
have simp : (P.map f x).snd (β := fun (x : P.A) ↦ P.B x → β) (cast sorry (i.snd (β := fun (x : P.A) ↦ P.B x))) =
  f (x.snd (β := fun (x : P.A) ↦ P.B x → α) (cast sorry (i.snd (β := fun (x : P.A) ↦ P.B x))))
Tactic: simp only [Obj.iget, fst_map, *, dif_pos]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.Basic (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type v₁
β : Type v₂
inst : DecidableEq P.A
inst_1 : Inhabited α
inst_2 : Inhabited β
x : (↑P : (α : Type v₁) → Type (max v₁ uA uB)) α
f : α → β
i : P.Idx
h : i.fst (β := fun (x : P.A) ↦ P.B x) = x.fst (β := fun (x : P.A) ↦ P.B x → α)
⊢ (P.map f x).snd (β := fun (x : P.A) ↦ P.B x → β) (cast ⋯ (i.snd (β := fun (x : P.A) ↦ P.B x))) =
    f (x.snd (β := fun (x : P.A) ↦ P.B x → α) (cast ⋯ (i.snd (β := fun (x : P.A) ↦ P.B x))))
have mk : ∀ (fst : P.A) (snd : P.B fst → α)
  (h :
    i.fst (β := fun (x : P.A) ↦ P.B x) =
      Sigma.fst (β := fun (x : P.A) ↦ P.B x → α) (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) fst snd)),
  (P.map f (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) fst snd)).snd (β := fun (x : P.A) ↦ P.B x → β)
      (cast sorry (i.snd (β := fun (x : P.A) ↦ P.B x))) =
    f
      (Sigma.snd (β := fun (x : P.A) ↦ P.B x → α) (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) fst snd)
        (cast sorry (i.snd (β := fun (x : P.A) ↦ P.B x))))
Tactic: cases x
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.Basic (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
x : (↑P : (α : Type u) → Type (max u uA uB)) α
⊢ Liftp p x ↔ ∃ (a : P.A) (f : P.B a → α), x = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f ∧ ∀ (i : P.B a), p (f i)
have mp : Liftp p x → ∃ (a : P.A) (f : P.B a → α), x = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f ∧ ∀ (i : P.B a), p (f i)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.Basic (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
x : (↑P : (α : Type u) → Type (max u uA uB)) α
mp : Liftp p x → ∃ (a : P.A) (f : P.B a → α), x = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f ∧ ∀ (i : P.B a), p (f i)
⊢ Liftp p x ↔ ∃ (a : P.A) (f : P.B a → α), x = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f ∧ ∀ (i : P.B a), p (f i)
have mpr : (∃ (a : P.A) (f : P.B a → α), x = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f ∧ ∀ (i : P.B a), p (f i)) → Liftp p x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.Basic (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
x : (↑P : (α : Type u) → Type (max u uA uB)) α
y : (↑P : (α : Type u) → Type (max u uA uB)) (Subtype p)
hy : Subtype.val (p := p) <$> y = x
⊢ ∃ (a : P.A) (f : P.B a → α), x = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f ∧ ∀ (i : P.B a), p (f i)
have mp : ∀ (a : P.A) (f : P.B a → Subtype p) (h : y = Sigma.mk (β := fun (x : P.A) ↦ P.B x → Subtype p) a f),
  ∃ (a : P.A) (f : P.B a → α), x = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f ∧ ∀ (i : P.B a), p (f i)
Tactic: rcases h : y with ⟨a, f⟩
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.Basic (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
x : (↑P : (α : Type u) → Type (max u uA uB)) α
y : (↑P : (α : Type u) → Type (max u uA uB)) (Subtype p)
hy : Subtype.val (p := p) <$> y = x
a : P.A
f : P.B a → Subtype p
h : y = Sigma.mk (β := fun (x : P.A) ↦ P.B x → Subtype p) a f
⊢ ∃ (a : P.A) (f : P.B a → α), x = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f ∧ ∀ (i : P.B a), p (f i)
have mp : x = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a fun (i : P.B a) ↦ (↑(f i) : α)
Tactic: refine ⟨a, fun i => (f i).val, ?_, fun i => (f i).property⟩
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.Basic (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
x : (↑P : (α : Type u) → Type (max u uA uB)) α
y : (↑P : (α : Type u) → Type (max u uA uB)) (Subtype p)
hy : Subtype.val (p := p) <$> y = x
a : P.A
f : P.B a → Subtype p
h : y = Sigma.mk (β := fun (x : P.A) ↦ P.B x → Subtype p) a f
⊢ x = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a fun (i : P.B a) ↦ (↑(f i) : α)
have mp : Eq (α := (↑P : (α : Type u) → Type (max u uA uB)) α)
  (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a (Subtype.val (p := p) ∘ f))
  (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a fun (i : P.B a) ↦ (↑(f i) : α))
Tactic: rw [← hy, h, map_eq_map, PFunctor.map_eq]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.Basic (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
x : (↑P : (α : Type u) → Type (max u uA uB)) α
a : P.A
f : P.B a → α
xeq : x = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f
pf : ∀ (i : P.B a), p (f i)
⊢ Liftp p x
have h : Functor.map (α := Subtype p) (Subtype.val (p := p))
    (Sigma.mk (β := fun (x : P.A) ↦ P.B x → Subtype p) a fun (i : P.B a) ↦ Subtype.mk (p := p) (f i) sorry) =
  x
Tactic: use ⟨a, fun i => ⟨f i, pf i⟩⟩
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.Basic (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
x : (↑P : (α : Type u) → Type (max u uA uB)) α
a : P.A
f : P.B a → α
xeq : x = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f
pf : ∀ (i : P.B a), p (f i)
⊢ Functor.map (α := Subtype p) (Subtype.val (p := p))
      (Sigma.mk (β := fun (x : P.A) ↦ P.B x → Subtype p) a fun (i : P.B a) ↦ Subtype.mk (p := p) (f i) ⋯) =
    x
have h : Eq (α := (↑P : (α : Type u) → Type (max u uA uB)) α)
  (Functor.map (α := Subtype p) (Subtype.val (p := p))
    (Sigma.mk (β := fun (x : P.A) ↦ P.B x → Subtype p) a fun (i : P.B a) ↦ Subtype.mk (p := p) (f i) sorry))
  (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f)
Tactic: rw [xeq]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.Basic (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
⊢ Liftp (F := (↑P : (α : Type u) → Type (max u uA uB))) p (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f) ↔
    ∀ (i : P.B a), p (f i)
have simp : (∃ (a_1 : P.A) (f_1 : P.B a_1 → α),
    Eq (α := (↑P : (α : Type u) → Type (max u uA uB)) α) (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f)
        (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a_1 f_1) ∧
      ∀ (i : P.B a_1), p (f_1 i)) ↔
  ∀ (i : P.B a), p (f i)
Tactic: simp only [liftp_iff]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.Basic (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
⊢ (∃ (a_1 : P.A) (f_1 : P.B a_1 → α),
      Eq (α := (↑P : (α : Type u) → Type (max u uA uB)) α) (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f)
          (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a_1 f_1) ∧
        ∀ (i : P.B a_1), p (f_1 i)) ↔
    ∀ (i : P.B a), p (f i)
have mp : (∃ (a_1 : P.A) (f_1 : P.B a_1 → α),
    Eq (α := (↑P : (α : Type u) → Type (max u uA uB)) α) (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f)
        (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a_1 f_1) ∧
      ∀ (i : P.B a_1), p (f_1 i)) →
  ∀ (i : P.B a), p (f i)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.Basic (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
mp :
  (∃ (a_1 : P.A) (f_1 : P.B a_1 → α),
      Eq (α := (↑P : (α : Type u) → Type (max u uA uB)) α) (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f)
          (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a_1 f_1) ∧
        ∀ (i : P.B a_1), p (f_1 i)) →
    ∀ (i : P.B a), p (f i)
⊢ (∃ (a_1 : P.A) (f_1 : P.B a_1 → α),
      Eq (α := (↑P : (α : Type u) → Type (max u uA uB)) α) (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f)
          (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a_1 f_1) ∧
        ∀ (i : P.B a_1), p (f_1 i)) ↔
    ∀ (i : P.B a), p (f i)
have mpr : (∀ (i : P.B a), p (f i)) →
  ∃ (a_2 : P.A) (f_1 : P.B a_2 → α),
    Eq (α := (↑P : (α : Type u) → Type (max u uA uB)) α) (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f)
        (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a_2 f_1) ∧
      ∀ (i : P.B a_2), p (f_1 i)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.Basic (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
h :
  ∃ (a_1 : P.A) (f_1 : P.B a_1 → α),
    Eq (α := (↑P : (α : Type u) → Type (max u uA uB)) α) (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f)
        (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a_1 f_1) ∧
      ∀ (i : P.B a_1), p (f_1 i)
⊢ ∀ (i : P.B a), p (f i)
have mp : ∀ (a' : P.A) (f' : P.B a' → α)
  (heq :
    Eq (α := (↑P : (α : Type u) → Type (max u uA uB)) α) (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f)
      (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a' f'))
  (h' : ∀ (i : P.B a'), p (f' i)) (i : P.B a), p (f i)
Tactic: rcases h with ⟨a', f', heq, h'⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.Basic (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
h : ∀ (i : P.B a), p (f i)
⊢ ∃ (a_1 : P.A) (f_1 : P.B a_1 → α),
    Eq (α := (↑P : (α : Type u) → Type (max u uA uB)) α) (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f)
        (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a_1 f_1) ∧
      ∀ (i : P.B a_1), p (f_1 i)
have mpr : ∃ (f_1 : P.B a → α),
  Eq (α := (↑P : (α : Type u) → Type (max u uA uB)) α) (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f)
      (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f_1) ∧
    ∀ (i : P.B a), p (f_1 i)
Tactic: constructor