awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.PFunctor.Multivariate.W
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 ⟹ α))
dsimp :
  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 ⟹ α)))
⊢ 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 ⟹ β)
        (Sigma.fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α)
          ((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 ⟹ α)) :
                (a : P.wp.A) × P.wp.B a ⟹ α))
            i))
        (TypeVec.comp (α :=
          P.wp.B
            (Sigma.fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α)
              ((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 ⟹ α)) :
                    (a : P.wp.A) × P.wp.B a ⟹ α))
                i)))
          (β := α) (γ := β) g
          (Sigma.snd (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α)
            ((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 ⟹ α)) :
                  (a : P.wp.A) × P.wp.B a ⟹ α))
              i)))

Tactic:
dsimp
-- Module: Mathlib.Data.PFunctor.Multivariate.W
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 ⟹ α))
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 ⟹ α))))
⊢ 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 ⟹ α)))

Tactic:
rw [wMk_eq, wMk_eq]

Premises used: MvPFunctor.wMk_eq
-- Module: Mathlib.Data.PFunctor.Multivariate.W
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 ⟹ α))
⊢ ∀ (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
-- Module: Mathlib.Data.PFunctor.Multivariate.W
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 α
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)))
⊢ 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)

Tactic:
rw [objAppend1, objAppend1, map_eq, appendFun, ← splitFun_comp]

Premises used: MvPFunctor.map_eq, TypeVec.splitFun_comp, MvPFunctor.objAppend1, TypeVec.appendFun
-- Module: Mathlib.Data.PFunctor.Multivariate.W
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 α
⊢ 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:
rfl
-- Module: Mathlib.Data.PFunctor.Multivariate.W
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))
rw₁ 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))
⊢ 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)

Tactic:
rw [wDest', wRec_eq]

Premises used: MvPFunctor.wRec_eq, MvPFunctor.wDest'
-- Module: Mathlib.Data.PFunctor.Multivariate.W
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
x : (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.W α)
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)
⊢ P.wDest' (α := α) (P.wMk' (α := α) x) = x

Tactic:
obtain ⟨a, f⟩ := x
-- Module: Mathlib.Data.PFunctor.Multivariate.W
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)
rw₂ 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)
⊢ 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:
rw [wMk', wDest'_wMk, split_dropFun_lastFun]

Premises used: MvPFunctor.wDest'_wMk, MvPFunctor.wMk', TypeVec.split_dropFun_lastFun
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
Goal:
P : PFunctor.{uA, uB}
α β : Type v
f : α → β
x : (↑P : (α : Type v) → Type (max v uA uB)) α
⊢ f <$> x = P.map f x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
Goal:
P : PFunctor.{uA, uB}
α : Type v₁
β : Type v₂
f : α → β
a : P.A
g : P.B a → α
⊢ P.map f (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a g) = Sigma.mk (β := fun (x : P.A) ↦ P.B x → β) a (f ∘ g)

Tactic:
rfl

Premises used: PFunctor.map, rfl
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
Goal:
P : PFunctor.{uA, uB}
α : Type v₁
⊢ ∀ (x : (↑P : (α : Type v₁) → Type (max v₁ uA uB)) α), P.map id x = x

Tactic:
fun ⟨_, _⟩ => rfl

Premises used: id, PFunctor.map, _private.0.PFunctor.id_map.match_1, Eq, rfl
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
Goal:
P : PFunctor.{uA, uB}
α : Type v₁
β : Type v₂
γ : Type v₃
f : α → β
g : β → γ
⊢ ∀ (x : (↑P : (α : Type v₁) → Type (max v₁ uA uB)) α), P.map g (P.map f x) = P.map (g ∘ f) x

Tactic:
fun ⟨_, _⟩ => rfl

Premises used: Function.comp, PFunctor.map, _private.0.PFunctor.id_map.match_1, Eq, rfl
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
Goal:
P : PFunctor.{uA, uB}
p : (↑P : (α : Type (max uB uA)) → Type (max (max uB uA) uA uB)) P.W
mk :
  ∀ (fst : P.A) (snd : P.B fst → P.W),
    (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
⊢ (W.mk p).dest = p

Tactic:
cases p
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
Goal:
P : PFunctor.{uA, uB}
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:
rfl
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
Goal:
P : PFunctor.{uA, uB}
p : P.W
mk : ∀ (a : P.A) (f : P.B a → WType P.B), W.mk (dest (WType.mk (β := P.B) a f)) = WType.mk (β := P.B) a f
⊢ W.mk p.dest = p

Tactic:
cases p
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
Goal:
P : PFunctor.{uA, uB}
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:
rfl
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
Goal:
P : PFunctor.{uA, uB}
α : Type v₁
β : Type v₂
x : (↑P : (α : Type v₁) → Type (max v₁ uA uB)) α
f : α → β
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)
⊢ (P.map f x).fst (β := fun (x : P.A) ↦ P.B x → β) = x.fst (β := fun (x : P.A) ↦ P.B x → α)

Tactic:
cases x
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
Goal:
P : PFunctor.{uA, uB}
α : Type v₁
β : Type v₂
f : α → β
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:
rfl
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
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 → α)
simp :
  (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))))
⊢ (P.map f x).iget i = f (x.iget i)

Tactic:
simp only [Obj.iget, fst_map, *, dif_pos]

Premises used: PFunctor.fst_map, dif_pos, PFunctor.Obj.iget
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
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 → α)
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 ⋯ (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 ⋯ (i.snd (β := 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))))

Tactic:
cases x
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
Goal:
P : PFunctor.{uA, uB}
α : Type v₁
β : Type v₂
inst : DecidableEq P.A
inst_1 : Inhabited α
inst_2 : Inhabited β
f : α → β
i : P.Idx
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 ⋯ (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 ⋯ (i.snd (β := fun (x : P.A) ↦ P.B x))))

Tactic:
rfl
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
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)
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
⊢ 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
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
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
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)
⊢ ∃ (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⟩
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
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)

Tactic:
⟨a, fun i => (f i).val, ?_, fun i => (f i).property⟩

Premises used: And.intro, Exists.intro, Subtype.val, Subtype.property
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
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
mp : x = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a fun (i : P.B a) ↦ (↑(f i) : α)
⊢ ∃ (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:
refine ⟨a, fun i => (f i).val, ?_, fun i => (f i).property⟩
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
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
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) : α))
⊢ x = 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]

Premises used: PFunctor.map_eq_map, PFunctor.map_eq
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
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
⊢ 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:
congr
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
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)
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) ⋯) =
    x
⊢ Liftp p x

Tactic:
use ⟨a, fun i => ⟨f i, pf i⟩⟩
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
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)
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) ⋯))
    (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f)
⊢ 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

Tactic:
rw [xeq]
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
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)
⊢ 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) ⋯))
    (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f)

Tactic:
rfl
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
Goal:
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
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)
⊢ 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)

Tactic:
simp only [liftp_iff]

Premises used: PFunctor.liftp_iff
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
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)
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)
⊢ (∃ (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
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
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)
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)
⊢ ∀ (i : P.B a), p (f i)

Tactic:
rcases h with ⟨a', f', heq, h'⟩