awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
i : (P F).B a'
left : Membership.mem (γ := Set ((P F).B a')) univ i
f'ieq : f' i = u
mpr : p (f' i)
⊢ p u

Tactic:
rw [← f'ieq]
-- 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
i : (P F).B a'
left : Membership.mem (γ := Set ((P F).B a')) univ i
f'ieq : 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 α
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
h' : ∀ 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)

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 α
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
h' : ∀ u ∈ supp x, p u
mpr : ∀ (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)

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 α
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
h' : ∀ u ∈ supp x, p u
i : (P F).B a
mpr : f i ∈ supp x
⊢ 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 α
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
h' : ∀ u ∈ supp x, p u
i : (P F).B a
mpr :
  ∀ (a : PFunctor.A.{u, u_1} (P F)) (f_1 : (P F).B a → α),
    abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f_1) = x → f i ∈ f_1 '' univ
⊢ f i ∈ supp x

Tactic:
rw [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 α
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
h' : ∀ u ∈ supp x, p u
i : (P F).B a
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
mpr : f i ∈ f '' univ
⊢ f i ∈ f' '' univ

Tactic:
apply h a' f' xeq'
-- 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
h' : ∀ u ∈ supp x, p u
i : (P F).B a
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
⊢ f i ∈ f '' univ

Tactic:
apply mem_image_of_mem _ (mem_univ _)

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

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

Tactic:
rw [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
h : IsUniform.{u, u_1} (F := F)
α : Type u
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
u : α
h₁ :
  (∀ (a_1 : PFunctor.A.{u, u_1} (P F)) (f_1 : (P F).B a_1 → α),
      Eq (α := F α) (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a_1 f_1))
          (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f)) →
        u ∈ f_1 '' univ) →
    u ∈ f '' univ
h₂ :
  u ∈ f '' univ →
    ∀ (a_2 : PFunctor.A.{u, u_1} (P F)) (f_1 : (P F).B a_2 → α),
      Eq (α := F α) (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a_2 f_1))
          (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f)) →
        u ∈ f_1 '' univ
⊢ (∀ (a_1 : PFunctor.A.{u, u_1} (P F)) (f_1 : (P F).B a_1 → α),
      Eq (α := F α) (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a_1 f_1))
          (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f)) →
        u ∈ f_1 '' univ) ↔
    u ∈ f '' univ

Tactic:
constructor
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
h : IsUniform.{u, u_1} (F := F)
α : Type u
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
u : α
h' :
  ∀ (a_1 : PFunctor.A.{u, u_1} (P F)) (f_1 : (P F).B a_1 → α),
    Eq (α := F α) (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a_1 f_1))
        (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f)) →
      u ∈ f_1 '' univ
⊢ u ∈ f '' univ

Tactic:
apply h' _ _ rfl

Premises used: rfl
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
h : IsUniform.{u, u_1} (F := F)
α : Type u
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
u : α
h' : u ∈ f '' univ
a' : PFunctor.A.{u, u_1} (P F)
f' : (P F).B a' → α
e :
  Eq (α := F α) (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a' f'))
    (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))
h₁ : u ∈ f '' univ
⊢ u ∈ f' '' univ

Tactic:
rw [← h _ _ _ _ e.symm]

Premises used: Eq.symm
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
h : IsUniform.{u, u_1} (F := F)
α : Type u
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
u : α
h' : u ∈ f '' univ
a' : PFunctor.A.{u, u_1} (P F)
f' : (P F).B a' → α
e :
  Eq (α := F α) (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a' f'))
    (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))
⊢ u ∈ f '' univ

Tactic:
apply h'
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
h : IsUniform.{u, u_1} (F := F)
α : Type u
x : F α
p : α → Prop
rw :
  (∃ (a : PFunctor.A.{u, u_1} (P F)) (f : (P F).B a → α),
      abs.{u, u_1, u} (repr 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 (abs.{u, u_1, u} (repr x)), p u
⊢ Liftp p x ↔ ∀ u ∈ supp x, p u

Tactic:
rw [liftp_iff, ← abs_repr x]

Premises used: QPF.abs_repr, QPF.liftp_iff
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
h : IsUniform.{u, u_1} (F := F)
α : Type u
x : F α
p : α → Prop
obtain :
  ∀ (a : PFunctor.A.{u, u_1} (P F)) (f : (P F).B a → α),
    (∃ (a_1 : PFunctor.A.{u, u_1} (P F)) (f_1 : (P F).B a_1 → α),
        Eq (α := F α) (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))
            (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), p (f_1 i)) ↔
      ∀ (u : α),
        Membership.mem (γ := Set α)
            (supp (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))) u →
          p u
⊢ (∃ (a : PFunctor.A.{u, u_1} (P F)) (f : (P F).B a → α),
      abs.{u, u_1, u} (repr 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 (abs.{u, u_1, u} (repr x)), p u

Tactic:
obtain ⟨a, f⟩ := repr x

Premises used: QPF.repr
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
h : IsUniform.{u, u_1} (F := F)
α : Type u
x : F α
p : α → Prop
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
mp :
  (∃ (a_1 : PFunctor.A.{u, u_1} (P F)) (f_1 : (P F).B a_1 → α),
      Eq (α := F α) (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))
          (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), p (f_1 i)) →
    ∀ (u : α),
      Membership.mem (γ := Set α) (supp (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f)))
          u →
        p u
mpr :
  (∀ (u : α),
      Membership.mem (γ := Set α) (supp (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f)))
          u →
        p u) →
    ∃ (a_2 : PFunctor.A.{u, u_1} (P F)) (f_1 : (P F).B a_2 → α),
      Eq (α := F α) (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))
          (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a_2 f_1)) ∧
        ∀ (i : (P F).B a_2), p (f_1 i)
⊢ (∃ (a_1 : PFunctor.A.{u, u_1} (P F)) (f_1 : (P F).B a_1 → α),
      Eq (α := F α) (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))
          (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), p (f_1 i)) ↔
    ∀ (u : α),
      Membership.mem (γ := Set α) (supp (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f)))
          u →
        p u

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

Tactic:
rw [supp_eq_of_isUniform h, h _ _ _ _ abseq]

Premises used: QPF.supp_eq_of_isUniform
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
h : IsUniform.{u, u_1} (F := F)
α : Type u
x : F α
p : α → Prop
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
a' : PFunctor.A.{u, u_1} (P F)
f' : (P F).B a' → α
abseq :
  Eq (α := F α) (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))
    (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a' f'))
hf : ∀ (i : (P F).B a'), p (f' i)
u : α
i : (P F).B a'
left : Membership.mem (γ := Set ((P F).B a')) univ i
hi : f' i = u
mp : 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
h : IsUniform.{u, u_1} (F := F)
α : Type u
x : F α
p : α → Prop
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
a' : PFunctor.A.{u, u_1} (P F)
f' : (P F).B a' → α
abseq :
  Eq (α := F α) (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))
    (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a' f'))
hf : ∀ (i : (P F).B a'), p (f' i)
u : α
i : (P F).B a'
left : Membership.mem (γ := Set ((P F).B a')) univ i
hi : f' i = u
⊢ p (f' i)

Tactic:
apply hf
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
h : IsUniform.{u, u_1} (F := F)
α : Type u
x : F α
p : α → Prop
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
h' :
  ∀ (u : α),
    Membership.mem (γ := Set α) (supp (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f)))
        u →
      p u
⊢ ∃ (a_1 : PFunctor.A.{u, u_1} (P F)) (f_1 : (P F).B a_1 → α),
    Eq (α := F α) (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))
        (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), p (f_1 i)

Tactic:
⟨a, f, rfl, fun i => h' _ ?_⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
h : IsUniform.{u, u_1} (F := F)
α : Type u
x : F α
p : α → Prop
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
h' :
  ∀ (u : α),
    Membership.mem (γ := Set α) (supp (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f)))
        u →
      p u
mpr :
  ∀ (i : (P F).B a),
    Membership.mem (γ := Set α) (supp (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f)))
      (f i)
⊢ ∃ (a_1 : PFunctor.A.{u, u_1} (P F)) (f_1 : (P F).B a_1 → α),
    Eq (α := F α) (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))
        (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), p (f_1 i)

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

Tactic:
rw [supp_eq_of_isUniform h]

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

Tactic:
⟨i, mem_univ i, rfl⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.mem_univ, Set.image, rfl
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
h : IsUniform.{u, u_1} (F := F)
α : Type u
x : F α
p : α → Prop
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
h' :
  ∀ (u : α),
    Membership.mem (γ := Set α) (supp (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f)))
        u →
      p u
i : (P F).B a
⊢ f i ∈ f '' univ

Tactic:
exact ⟨i, mem_univ i, rfl⟩
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
h : IsUniform.{u, u_1} (F := F)
α β : Type u
g : α → β
x : F α
rw : supp (g <$> abs.{u, u_1, u} (repr x)) = g '' supp (abs.{u, u_1, u} (repr x))
⊢ supp (g <$> x) = g '' supp x

Tactic:
rw [← abs_repr x]

Premises used: QPF.abs_repr
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
h : IsUniform.{u, u_1} (F := F)
α β : Type u
g : α → β
x : F α
obtain :
  ∀ (a : PFunctor.A.{u, u_1} (P F)) (f : (P F).B a → α),
    supp (g <$> abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f)) =
      g '' supp (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))
⊢ supp (g <$> abs.{u, u_1, u} (repr x)) = g '' supp (abs.{u, u_1, u} (repr x))

Tactic:
obtain ⟨a, f⟩ := repr x

Premises used: QPF.repr
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
h : IsUniform.{u, u_1} (F := F)
α β : Type u
g : α → β
x : F α
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
rw :
  supp (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → β) a (g ∘ f))) =
    g '' supp (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))
⊢ supp (g <$> abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f)) =
    g '' supp (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))

Tactic:
rw [← abs_map, PFunctor.map_eq]

Premises used: QPF.abs_map, PFunctor.map_eq
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
h : IsUniform.{u, u_1} (F := F)
α β : Type u
g : α → β
x : F α
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
rw : g ∘ f '' univ = g '' supp (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))
rw₁ : g ∘ f '' univ = g '' f '' univ
rw₂ rw₃ : g '' f '' univ = g '' f '' univ
⊢ supp (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → β) a (g ∘ f))) =
    g '' supp (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))

Tactic:
rw [supp_eq_of_isUniform h, supp_eq_of_isUniform h, image_comp]

Premises used: Set.image_comp, QPF.supp_eq_of_isUniform
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
mp : SuppPreservation.{u, u_1} (F := F) → IsUniform.{u, u_1} (F := F)
mpr : IsUniform.{u, u_1} (F := F) → SuppPreservation.{u, u_1} (F := F)
⊢ SuppPreservation.{u, u_1} (F := F) ↔ IsUniform.{u, u_1} (F := F)

Tactic:
constructor
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
h : SuppPreservation.{u, u_1} (F := F)
α : Type u
a a' : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
f' : (P F).B a' → α
h' :
  Eq (α := F α) (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))
    (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a' f'))
mp :
  supp (F := (↑(P F) : (α : Type u) → Type (max u u_1)))
      (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) =
    f' '' univ
mp₁ :
  Eq.{u + 1} (α := Set α)
    (supp (F := (↑(P F) : (α : Type u) → Type (max u u_1)))
      (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))
    (supp (F := (↑(P F) : (α : Type u) → Type (max u u_1)))
      (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a' f'))
mp₂ :
  Eq (α := Set α) (supp (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f)))
    (supp (F := (↑(P F) : (α : Type u) → Type (max u u_1)))
      (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a' f'))
mp₃ :
  Eq (α := Set α) (supp (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a' f')))
    (supp (F := (↑(P F) : (α : Type u) → Type (max u u_1)))
      (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a' f'))
mp₄ mp₅ :
  Eq.{u + 1} (α := Set α)
    (supp (F := (↑(P F) : (α : Type u) → Type (max u u_1)))
      (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a' f'))
    (supp (F := (↑(P F) : (α : Type u) → Type (max u u_1)))
      (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a' f'))
⊢ f '' univ = f' '' univ

Tactic:
rw [← PFunctor.supp_eq, ← PFunctor.supp_eq, ← h, h', h]

Premises used: PFunctor.supp_eq
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
h : IsUniform.{u, u_1} (F := F)
α : Type u
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
mpr :
  f '' univ =
    supp (F := (↑(P F) : (α : Type u) → Type (max u u_1)))
      (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f)
mpr₁ : IsUniform.{u, u_1} (F := F)
mpr₂ : f '' univ = f '' univ
mpr₃ : IsUniform.{u, u_1} (F := F)
mpr₄ : f '' univ = f '' univ
mpr₅ mpr₆ mpr₇ : IsUniform.{u, u_1} (F := F)
⊢ Eq (α := Set α) (supp (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f)))
    (supp (F := (↑(P F) : (α : Type u) → Type (max u u_1)))
      (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))

Tactic:
rwa [supp_eq_of_isUniform, PFunctor.supp_eq]

Premises used: PFunctor.supp_eq, QPF.supp_eq_of_isUniform
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
mp : SuppPreservation.{u, u_1} (F := F) → LiftpPreservation.{u, u_1} (F := F)
mpr : LiftpPreservation.{u, u_1} (F := F) → SuppPreservation.{u, u_1} (F := F)
⊢ SuppPreservation.{u, u_1} (F := F) ↔ LiftpPreservation.{u, u_1} (F := F)

Tactic:
constructor
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
h : SuppPreservation.{u, u_1} (F := F)
α : Type u
p : α → Prop
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
⊢ SuppPreservation.{u, u_1} (F := F)

Tactic:
have h' := h
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
h : SuppPreservation.{u, u_1} (F := F)
α : Type u
p : α → Prop
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
h' : SuppPreservation.{u, u_1} (F := F)
⊢ IsUniform.{u, u_1} (F := F)

Tactic:
rw [suppPreservation_iff_uniform] at h'

Premises used: QPF.suppPreservation_iff_uniform