awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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
⊢ Liftp p x → p u
have 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
Tactic: rw [liftp_iff]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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)
⊢ p u
have mpr : ∀ (i : (P F).B a), Membership.mem (γ := Set ((P F).B a)) univ i → ∀ (hi : f i = u), p u
Tactic: rcases h a f xeq.symm with ⟨i, _, hi⟩
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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 u
have mpr : p (f i)
Tactic: rw [← hi]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
α : Type u
x : F α
⊢ 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}
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
α : Type u
x : F α
⊢ (∀ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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
⊢ (∀ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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
have rw : ∀ u ∈ supp x, u ∈ supp x
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (hypothesis)
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 → α),
    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
have this : Liftp (fun (x_1 : α) ↦ x_1 ∈ supp x) x
Tactic: have : Liftp (· ∈ supp x) x := by rw [h]; intro u; exact id
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (hypothesis)
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 → α),
    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
have 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
Tactic: rw [liftp_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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
⊢ ∃ (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
have 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
Tactic: rcases this with ⟨a, f, xeq, h'⟩
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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
have 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
Tactic: refine ⟨a, f, xeq.symm, ?_⟩
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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
have rw : f i ∈ supp x
Tactic: rw [← hfi]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (hypothesis)
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 ∈ f' '' univ
have this : u ∈ supp x
Tactic: have : u ∈ supp x := by rw [← hfi]; apply h'
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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
⊢ Liftp p x ↔ ∀ u ∈ supp x, p u
have 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
Tactic: rw [liftp_iff]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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 → α),
      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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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
⊢ (∃ (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
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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
⊢ p u
have mpr : ∀ (i : (P F).B a'), Membership.mem (γ := Set ((P F).B a')) univ i → ∀ (f'ieq : f' i = u), p u
Tactic: rcases (mem_supp x u).mp usuppx a' f' xeq'.symm with ⟨i, _, f'ieq⟩
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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 u
have mpr : p (f' i)
Tactic: rw [← f'ieq]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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)
have mpr : ∀ (i : (P F).B a), p (f i)
Tactic: refine ⟨a, f, xeq.symm, ?_⟩
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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
⊢ p (f i)
have mpr : f i ∈ supp x
Tactic: apply h'
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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
⊢ f i ∈ supp x
have 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
Tactic: rw [mem_supp]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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
have mpr : f i ∈ f '' univ
Tactic: apply h a' f' xeq'
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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 → α
⊢ supp (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f)) = f '' univ
have 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
Tactic: ext u
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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 : α
⊢ 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
have 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: rw [mem_supp]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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 : α
⊢ (∀ (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
have 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: constructor
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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
⊢ (∀ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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
⊢ Liftp p x ↔ ∀ u ∈ supp x, p u
have 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
Tactic: rw [liftp_iff, ← abs_repr x]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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 → α),
      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
have 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
Tactic: obtain ⟨a, f⟩ := repr x
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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_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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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
⊢ (∃ (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
have 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)
Tactic: constructor