awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
α : Type u_1
Q : α → Prop
u v : α → Cofix F
h :
  ∀ (x : α),
    Q x →
      ∃ (a : (P F).A) (f : (P F).B a → Cofix F) (f' : (P F).B a → Cofix F),
        (u x).dest = abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Cofix F) a f) ∧
          (v x).dest = abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Cofix F) a f') ∧
            ∀ (i : (P F).B a), ∃ (x' : α), Q x' ∧ f i = u x' ∧ f' i = v x'
x_1 : α
Qx : Q x_1
R : (w z : Cofix F) → Prop := fun (w z : Cofix F) ↦ ∃ (x' : α), Q x' ∧ w = u x' ∧ z = v x'
x y : Cofix F
h_1 : R x y
x' : α
Qx' : Q x'
xeq : x = u x'
yeq : y = v x'
a : (P F).A
f f' : (P F).B a → Cofix F
ux'eq : (u x').dest = abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Cofix F) a f)
vx'eq : (v x').dest = abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Cofix F) a f')
h' : ∀ (i : (P F).B a), ∃ (x' : α), Q x' ∧ f i = u x' ∧ f' i = v x'
rw :
  ∃ (a : (P F).A) (f₀ : (P F).B a → Cofix F) (f₁ : (P F).B a → Cofix F),
    x.dest = abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Cofix F) a f₀) ∧
      y.dest = abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Cofix F) a f₁) ∧ ∀ (i : (P F).B a), R (f₀ i) (f₁ i)
⊢ Liftr R x.dest y.dest

Tactic:
rw [liftr_iff]

Premises used: QPF.liftr_iff
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
α : Type u_1
Q : α → Prop
u v : α → Cofix F
h :
  ∀ (x : α),
    Q x →
      ∃ (a : (P F).A) (f : (P F).B a → Cofix F) (f' : (P F).B a → Cofix F),
        (u x).dest = abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Cofix F) a f) ∧
          (v x).dest = abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Cofix F) a f') ∧
            ∀ (i : (P F).B a), ∃ (x' : α), Q x' ∧ f i = u x' ∧ f' i = v x'
x_1 : α
Qx : Q x_1
R : (w z : Cofix F) → Prop := fun (w z : Cofix F) ↦ ∃ (x' : α), Q x' ∧ w = u x' ∧ z = v x'
x y : Cofix F
h_1 : R x y
x' : α
Qx' : Q x'
xeq : x = u x'
yeq : y = v x'
a : (P F).A
f f' : (P F).B a → Cofix F
ux'eq : (u x').dest = abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Cofix F) a f)
vx'eq : (v x').dest = abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Cofix F) a f')
h' : ∀ (i : (P F).B a), ∃ (x' : α), Q x' ∧ f i = u x' ∧ f' i = v x'
⊢ ∃ (a : (P F).A) (f₀ : (P F).B a → Cofix F) (f₁ : (P F).B a → Cofix F),
    x.dest = abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Cofix F) a f₀) ∧
      y.dest = abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Cofix F) a f₁) ∧ ∀ (i : (P F).B a), R (f₀ i) (f₁ i)

Tactic:
⟨a, f, f', xeq.symm ▸ ux'eq, yeq.symm ▸ vx'eq, h'⟩

Premises used: Eq.rec, And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
α : Type u_1
Q : α → Prop
u v : α → Cofix F
h :
  ∀ (x : α),
    Q x →
      ∃ (a : (P F).A) (f : (P F).B a → Cofix F) (f' : (P F).B a → Cofix F),
        (u x).dest = abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Cofix F) a f) ∧
          (v x).dest = abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Cofix F) a f') ∧
            ∀ (i : (P F).B a), ∃ (x' : α), Q x' ∧ f i = u x' ∧ f' i = v x'
x_1 : α
Qx : Q x_1
R : (w z : Cofix F) → Prop := fun (w z : Cofix F) ↦ ∃ (x' : α), Q x' ∧ w = u x' ∧ z = v x'
x y : Cofix F
h_1 : R x y
x' : α
Qx' : Q x'
xeq : x = u x'
yeq : y = v x'
a : (P F).A
f f' : (P F).B a → Cofix F
ux'eq : (u x').dest = abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Cofix F) a f)
vx'eq : (v x').dest = abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Cofix F) a f')
h' : ∀ (i : (P F).B a), ∃ (x' : α), Q x' ∧ f i = u x' ∧ f' i = v x'
⊢ ∃ (a : (P F).A) (f₀ : (P F).B a → Cofix F) (f₁ : (P F).B a → Cofix F),
    x.dest = abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Cofix F) a f₀) ∧
      y.dest = abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Cofix F) a f₁) ∧ ∀ (i : (P F).B a), R (f₀ i) (f₁ i)

Tactic:
exact ⟨a, f, f', xeq.symm ▸ ux'eq, yeq.symm ▸ vx'eq, h'⟩
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
G : Type u → Type u
inst : Functor G
FG_abs : {α : Type u} → F α → G α
FG_repr : {α : Type u} → G α → F α
FG_abs_repr : ∀ {α : Type u} (x : G α), FG_abs (FG_repr x) = x
FG_abs_map : ∀ {α β : Type u} (f : α → β) (x : F α), FG_abs (f <$> x) = f <$> FG_abs x
α : Type u
x : G α
rw : FG_abs (FG_repr x) = x
rw₁ rw₂ : x = x
⊢ FG_abs (abs.{u, u_1, u} (repr (FG_repr x))) = x

Tactic:
rw [abs_repr, FG_abs_repr]

Premises used: QPF.abs_repr
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
G : Type u → Type u
inst : Functor G
FG_abs : {α : Type u} → F α → G α
FG_repr : {α : Type u} → G α → F α
FG_abs_repr : ∀ {α : Type u} (x : G α), FG_abs (FG_repr x) = x
FG_abs_map : ∀ {α β : Type u} (f : α → β) (x : F α), FG_abs (f <$> x) = f <$> FG_abs x
α β : Type u
f : α → β
x : (↑(P F) : (α : Type u) → Type (max u u_1)) α
rw : FG_abs (f <$> abs x) = f <$> FG_abs (abs x)
rw₁ rw₂ : f <$> FG_abs (abs x) = f <$> FG_abs (abs x)
⊢ FG_abs (abs ((P F).map f x)) = f <$> FG_abs (abs x)

Tactic:
rw [abs_map, FG_abs_map]

Premises used: QPF.abs_map
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
α : Type u
x : F α
u : α
mp :
  (∀ ⦃p : α → Prop⦄, Liftp p x → p u) →
    ∀ (a : PFunctor.A.{u, u_1} (P F)) (f : (P F).B a → α),
      abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) = x → u ∈ f '' univ
mpr :
  (∀ (a : PFunctor.A.{u, u_1} (P F)) (f : (P F).B a → α),
      abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) = x → u ∈ f '' univ) →
    ∀ ⦃p : α → Prop⦄, Liftp p x → p u
⊢ (∀ ⦃p : α → Prop⦄, Liftp p x → p u) ↔
    ∀ (a : PFunctor.A.{u, u_1} (P F)) (f : (P F).B a → α),
      abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) = x → u ∈ f '' univ

Tactic:
constructor
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
α : Type u
x : F α
u : α
h : ∀ ⦃p : α → Prop⦄, Liftp p x → p u
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
haf : abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) = x
rw :
  ∃ (a_1 : PFunctor.A.{u, u_1} (P F)) (f_1 : (P F).B a_1 → α),
    x = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a_1 f_1) ∧
      ∀ (i : (P F).B a_1), f_1 i ∈ f '' univ
⊢ Liftp (fun (u : α) ↦ u ∈ f '' univ) x

Tactic:
rw [liftp_iff]

Premises used: QPF.liftp_iff
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
α : Type u
x : F α
u : α
h : ∀ ⦃p : α → Prop⦄, Liftp p x → p u
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
haf : abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) = x
⊢ ∃ (a_1 : PFunctor.A.{u, u_1} (P F)) (f_1 : (P F).B a_1 → α),
    x = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a_1 f_1) ∧
      ∀ (i : (P F).B a_1), f_1 i ∈ f '' univ

Tactic:
⟨a, f, haf.symm, fun i => mem_image_of_mem _ (mem_univ _)⟩

Premises used: Set.mem_image_of_mem, And.intro, Exists.intro, Set.mem_univ, Eq.symm
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
α : Type u
x : F α
u : α
h : ∀ ⦃p : α → Prop⦄, Liftp p x → p u
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
haf : abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) = x
⊢ ∃ (a_1 : PFunctor.A.{u, u_1} (P F)) (f_1 : (P F).B a_1 → α),
    x = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a_1 f_1) ∧
      ∀ (i : (P F).B a_1), f_1 i ∈ f '' univ

Tactic:
exact ⟨a, f, haf.symm, fun i => mem_image_of_mem _ (mem_univ _)⟩
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
α : Type u
x : F α
u : α
h : ∀ ⦃p : α → Prop⦄, Liftp p x → p u
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
haf : abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) = x
⊢ Liftp (fun (u : α) ↦ u ∈ f '' univ) x

Tactic:
have : Liftp (fun u => u ∈ f '' univ) x := by
      rw [liftp_iff]
      exact ⟨a, f, haf.symm, fun i => mem_image_of_mem _ (mem_univ _)⟩
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
α : Type u
x : F α
u : α
h : ∀ ⦃p : α → Prop⦄, Liftp p x → p u
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
haf : abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) = x
this : Liftp (fun (u : α) ↦ u ∈ f '' univ) x
⊢ u ∈ f '' univ

Tactic:
h this
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
α : Type u
x : F α
u : α
h : ∀ ⦃p : α → Prop⦄, Liftp p x → p u
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
haf : abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) = x
this : Liftp (fun (u : α) ↦ u ∈ f '' univ) x
⊢ u ∈ f '' univ

Tactic:
exact h this
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
α : Type u
x : F α
u : α
h :
  ∀ (a : PFunctor.A.{u, u_1} (P F)) (f : (P F).B a → α),
    abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) = x → u ∈ f '' univ
p : α → Prop
mpr :
  (∃ (a : PFunctor.A.{u, u_1} (P F)) (f : (P F).B a → α),
      x = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) ∧ ∀ (i : (P F).B a), p (f i)) →
    p u
⊢ Liftp p x → p u

Tactic:
rw [liftp_iff]

Premises used: QPF.liftp_iff
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
α : Type u
x : F α
u : α
h :
  ∀ (a : PFunctor.A.{u, u_1} (P F)) (f : (P F).B a → α),
    abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) = x → u ∈ f '' univ
p : α → Prop
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
xeq : x = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f)
h' : ∀ (i : (P F).B a), p (f i)
mpr : ∀ (i : (P F).B a), Membership.mem (γ := Set ((P F).B a)) univ i → ∀ (hi : f i = u), p u
⊢ p u

Tactic:
rcases h a f xeq.symm with ⟨i, _, hi⟩

Premises used: Eq.symm
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
α : Type u
x : F α
u : α
h :
  ∀ (a : PFunctor.A.{u, u_1} (P F)) (f : (P F).B a → α),
    abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) = x → u ∈ f '' univ
p : α → Prop
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
xeq : x = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f)
h' : ∀ (i : (P F).B a), p (f i)
i : (P F).B a
left : Membership.mem (γ := Set ((P F).B a)) univ i
hi : f i = u
mpr : p (f i)
⊢ p u

Tactic:
rw [← hi]
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
α : Type u
x : F α
u : α
h :
  ∀ (a : PFunctor.A.{u, u_1} (P F)) (f : (P F).B a → α),
    abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) = x → u ∈ f '' univ
p : α → Prop
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
xeq : x = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f)
h' : ∀ (i : (P F).B a), p (f i)
i : (P F).B a
left : Membership.mem (γ := Set ((P F).B a)) univ i
hi : f i = u
⊢ p (f i)

Tactic:
apply h'
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
α : Type u
x : F α
h :
  ∀ (x_1 : α),
    x_1 ∈ supp x ↔
      Membership.mem (γ := Set α)
        {u : α |
          ∀ (a : PFunctor.A.{u, u_1} (P F)) (f : (P F).B a → α),
            abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) = x → u ∈ f '' univ}
        x_1
⊢ supp x =
    {u : α |
      ∀ (a : PFunctor.A.{u, u_1} (P F)) (f : (P F).B a → α),
        abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) = x → u ∈ f '' univ}

Tactic:
ext
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
α : Type u
x : F α
x_1 : α
⊢ x_1 ∈ supp x ↔
    Membership.mem (γ := Set α)
      {u : α |
        ∀ (a : PFunctor.A.{u, u_1} (P F)) (f : (P F).B a → α),
          abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) = x → u ∈ f '' univ}
      x_1

Tactic:
apply mem_supp

Premises used: QPF.mem_supp
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
α : Type u
x : F α
mp :
  (∀ (p : α → Prop), Liftp p x ↔ ∀ u ∈ supp x, p u) →
    ∃ (a : PFunctor.A.{u, u_1} (P F)) (f : (P F).B a → α),
      abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) = x ∧
        ∀ (a' : PFunctor.A.{u, u_1} (P F)) (f' : (P F).B a' → α),
          abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a' f') = x → f '' univ ⊆ f' '' univ
mpr :
  (∃ (a : PFunctor.A.{u, u_1} (P F)) (f : (P F).B a → α),
      abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) = x ∧
        ∀ (a' : PFunctor.A.{u, u_1} (P F)) (f' : (P F).B a' → α),
          abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a' f') = x →
            f '' univ ⊆ f' '' univ) →
    ∀ (p : α → Prop), Liftp p x ↔ ∀ u ∈ supp x, p u
⊢ (∀ (p : α → Prop), Liftp p x ↔ ∀ u ∈ supp x, p u) ↔
    ∃ (a : PFunctor.A.{u, u_1} (P F)) (f : (P F).B a → α),
      abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) = x ∧
        ∀ (a' : PFunctor.A.{u, u_1} (P F)) (f' : (P F).B a' → α),
          abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a' f') = x → f '' univ ⊆ f' '' univ

Tactic:
constructor
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ u ∈ supp x, p u
rw : ∀ u ∈ supp x, u ∈ supp x
⊢ Liftp (fun (x_1 : α) ↦ x_1 ∈ supp x) x

Tactic:
rw [h]
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ u ∈ supp x, p u
u : α
⊢ u ∈ supp x → u ∈ supp x

Tactic:
id

Premises used: id
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ u ∈ supp x, p u
u : α
⊢ u ∈ supp x → u ∈ supp x

Tactic:
exact id

Premises used: id
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ u ∈ supp x, p u
⊢ Liftp (fun (x_1 : α) ↦ x_1 ∈ supp x) x

Tactic:
have : Liftp (· ∈ supp x) x := by rw [h]; intro u; exact id
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ u ∈ supp x, p u
this : Liftp (fun (x_1 : α) ↦ x_1 ∈ supp x) x
⊢ ∃ (a : PFunctor.A.{u, u_1} (P F)) (f : (P F).B a → α),
    x = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) ∧ ∀ (i : (P F).B a), f i ∈ supp x

Tactic:
rw [liftp_iff] at this

Premises used: QPF.liftp_iff
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ u ∈ supp x, p u
this :
  ∃ (a : PFunctor.A.{u, u_1} (P F)) (f : (P F).B a → α),
    x = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) ∧ ∀ (i : (P F).B a), f i ∈ supp x
mp :
  ∀ (a : PFunctor.A.{u, u_1} (P F)) (f : (P F).B a → α)
    (xeq : x = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))
    (h' : ∀ (i : (P F).B a), f i ∈ supp x),
    ∃ (a : PFunctor.A.{u, u_1} (P F)) (f : (P F).B a → α),
      abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) = x ∧
        ∀ (a' : PFunctor.A.{u, u_1} (P F)) (f' : (P F).B a' → α),
          abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a' f') = x → f '' univ ⊆ f' '' univ
⊢ ∃ (a : PFunctor.A.{u, u_1} (P F)) (f : (P F).B a → α),
    abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) = x ∧
      ∀ (a' : PFunctor.A.{u, u_1} (P F)) (f' : (P F).B a' → α),
        abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a' f') = x → f '' univ ⊆ f' '' univ

Tactic:
rcases this with ⟨a, f, xeq, h'⟩
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ u ∈ supp x, p u
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
xeq : x = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f)
h' : ∀ (i : (P F).B a), f i ∈ supp x
⊢ ∃ (a : PFunctor.A.{u, u_1} (P F)) (f : (P F).B a → α),
    abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) = x ∧
      ∀ (a' : PFunctor.A.{u, u_1} (P F)) (f' : (P F).B a' → α),
        abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a' f') = x → f '' univ ⊆ f' '' univ

Tactic:
⟨a, f, xeq.symm, ?_⟩

Premises used: And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ u ∈ supp x, p u
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
xeq : x = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f)
h' : ∀ (i : (P F).B a), f i ∈ supp x
mp :
  ∀ (a' : PFunctor.A.{u, u_1} (P F)) (f' : (P F).B a' → α),
    abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a' f') = x → f '' univ ⊆ f' '' univ
⊢ ∃ (a : PFunctor.A.{u, u_1} (P F)) (f : (P F).B a → α),
    abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) = x ∧
      ∀ (a' : PFunctor.A.{u, u_1} (P F)) (f' : (P F).B a' → α),
        abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a' f') = x → f '' univ ⊆ f' '' univ

Tactic:
refine ⟨a, f, xeq.symm, ?_⟩
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ u ∈ supp x, p u
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
xeq : x = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f)
h' : ∀ (i : (P F).B a), f i ∈ supp x
a' : PFunctor.A.{u, u_1} (P F)
f' : (P F).B a' → α
h'' : abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a' f') = x
u : α
i : (P F).B a
left : Membership.mem (γ := Set ((P F).B a)) univ i
hfi : f i = u
rw : f i ∈ supp x
⊢ u ∈ supp x

Tactic:
rw [← hfi]
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ u ∈ supp x, p u
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
xeq : x = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f)
h' : ∀ (i : (P F).B a), f i ∈ supp x
a' : PFunctor.A.{u, u_1} (P F)
f' : (P F).B a' → α
h'' : abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a' f') = x
u : α
i : (P F).B a
left : Membership.mem (γ := Set ((P F).B a)) univ i
hfi : f i = u
⊢ f i ∈ supp x

Tactic:
apply h'
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ u ∈ supp x, p u
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
xeq : x = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f)
h' : ∀ (i : (P F).B a), f i ∈ supp x
a' : PFunctor.A.{u, u_1} (P F)
f' : (P F).B a' → α
h'' : abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a' f') = x
u : α
i : (P F).B a
left : Membership.mem (γ := Set ((P F).B a)) univ i
hfi : f i = u
⊢ u ∈ supp x

Tactic:
have : u ∈ supp x := by rw [← hfi]; apply h'
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ u ∈ supp x, p u
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
xeq : x = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f)
h' : ∀ (i : (P F).B a), f i ∈ supp x
a' : PFunctor.A.{u, u_1} (P F)
f' : (P F).B a' → α
h'' : abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a' f') = x
u : α
i : (P F).B a
left : Membership.mem (γ := Set ((P F).B a)) univ i
hfi : f i = u
this : u ∈ supp x
⊢ u ∈ f' '' univ

Tactic:
(mem_supp x u).mp this _ _ h''

Premises used: QPF.mem_supp, Iff.mp
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ u ∈ supp x, p u
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
xeq : x = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f)
h' : ∀ (i : (P F).B a), f i ∈ supp x
a' : PFunctor.A.{u, u_1} (P F)
f' : (P F).B a' → α
h'' : abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a' f') = x
u : α
i : (P F).B a
left : Membership.mem (γ := Set ((P F).B a)) univ i
hfi : f i = u
this : u ∈ supp x
⊢ u ∈ f' '' univ

Tactic:
exact (mem_supp x u).mp this _ _ h''

Premises used: QPF.mem_supp, Iff.mp
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
α : Type u
x : F α
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
xeq : abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) = x
h :
  ∀ (a' : PFunctor.A.{u, u_1} (P F)) (f' : (P F).B a' → α),
    abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a' f') = x → f '' univ ⊆ f' '' univ
p : α → Prop
mpr :
  (∃ (a : PFunctor.A.{u, u_1} (P F)) (f : (P F).B a → α),
      x = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) ∧ ∀ (i : (P F).B a), p (f i)) ↔
    ∀ u ∈ supp x, p u
⊢ Liftp p x ↔ ∀ u ∈ supp x, p u

Tactic:
rw [liftp_iff]

Premises used: QPF.liftp_iff
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
α : Type u
x : F α
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
xeq : abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) = x
h :
  ∀ (a' : PFunctor.A.{u, u_1} (P F)) (f' : (P F).B a' → α),
    abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a' f') = x → f '' univ ⊆ f' '' univ
p : α → Prop
mpr :
  (∃ (a : PFunctor.A.{u, u_1} (P F)) (f : (P F).B a → α),
      x = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) ∧ ∀ (i : (P F).B a), p (f i)) →
    ∀ u ∈ supp x, p u
mpr₁ :
  (∀ u ∈ supp x, p u) →
    ∃ (a : PFunctor.A.{u, u_1} (P F)) (f : (P F).B a → α),
      x = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) ∧ ∀ (i : (P F).B a), p (f i)
⊢ (∃ (a : PFunctor.A.{u, u_1} (P F)) (f : (P F).B a → α),
      x = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) ∧ ∀ (i : (P F).B a), p (f i)) ↔
    ∀ u ∈ supp x, p u

Tactic:
constructor
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
α : Type u
x : F α
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
xeq : abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) = x
h :
  ∀ (a' : PFunctor.A.{u, u_1} (P F)) (f' : (P F).B a' → α),
    abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a' f') = x → f '' univ ⊆ f' '' univ
p : α → Prop
a' : PFunctor.A.{u, u_1} (P F)
f' : (P F).B a' → α
xeq' : x = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a' f')
h' : ∀ (i : (P F).B a'), p (f' i)
u : α
usuppx : u ∈ supp x
mpr : ∀ (i : (P F).B a'), Membership.mem (γ := Set ((P F).B a')) univ i → ∀ (f'ieq : f' i = u), p u
⊢ p u

Tactic:
rcases (mem_supp x u).mp usuppx a' f' xeq'.symm with ⟨i, _, f'ieq⟩

Premises used: QPF.mem_supp, Iff.mp, Eq.symm