-- Mathlib/Data/QPF/Univariate/Basic.lean
theorem liftp_iff_of_isUniform (h : q.IsUniform) {α : Type u} (x : F α) (p : α → Prop) :
    Liftp p x ↔ ∀ u ∈ supp x, p u

Proof state:
case mk.mp.intro.intro.intro.intro.intro
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : (P F).B a → α
a' : (P F).A
f' : (P F).B a' → α
abseq : abs ⟨a, f⟩ = abs ⟨a', f'⟩
hf : ∀ (i : (P F).B a'), p (f' i)
u : α
i : (P F).B a'
left✝ : i ∈ univ
hi : f' i = u
⊢ p (f' i)

Tactic:
apply hf

Result:
no goals

Proof state:
case mk.mpr
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : (P F).B a → α
h' : ∀ u ∈ supp (abs ⟨a, f⟩), p u
i : (P F).B a
⊢ f i ∈ f '' univ

Tactic:
exact ⟨i, mem_univ i, rfl⟩

Result:
no goals

Proof state:
case mk.mp.intro.intro.intro
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : (P F).B a → α
a' : (P F).A
f' : (P F).B a' → α
abseq : abs ⟨a, f⟩ = abs ⟨a', f'⟩
hf : ∀ (i : (P F).B a'), p (f' i)
u : α
⊢ u ∈ supp (abs ⟨a, f⟩) → p u

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

Result:
case mk.mp.intro.intro.intro
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : (P F).B a → α
a' : (P F).A
f' : (P F).B a' → α
abseq : abs ⟨a, f⟩ = abs ⟨a', f'⟩
hf : ∀ (i : (P F).B a'), p (f' i)
u : α
⊢ u ∈ f' '' univ → p u

Proof state:
case mk.mp.intro.intro.intro.intro.intro
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : (P F).B a → α
a' : (P F).A
f' : (P F).B a' → α
abseq : abs ⟨a, f⟩ = abs ⟨a', f'⟩
hf : ∀ (i : (P F).B a'), p (f' i)
u : α
i : (P F).B a'
left✝ : i ∈ univ
hi : f' i = u
⊢ p u

Tactic:
rw [← hi]

Result:
case mk.mp.intro.intro.intro.intro.intro
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : (P F).B a → α
a' : (P F).A
f' : (P F).B a' → α
abseq : abs ⟨a, f⟩ = abs ⟨a', f'⟩
hf : ∀ (i : (P F).B a'), p (f' i)
u : α
i : (P F).B a'
left✝ : i ∈ univ
hi : f' i = u
⊢ p (f' i)

Proof state:
case mk.mpr
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : (P F).B a → α
h' : ∀ u ∈ supp (abs ⟨a, f⟩), p u
⊢ ∃ a_1 f_1, abs ⟨a, f⟩ = abs ⟨a_1, f_1⟩ ∧ ∀ (i : (P F).B a_1), p (f_1 i)

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

Result:
case mk.mpr
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : (P F).B a → α
h' : ∀ u ∈ supp (abs ⟨a, f⟩), p u
i : (P F).B a
⊢ f i ∈ supp (abs ⟨a, f⟩)

Proof state:
case mk.mp.intro.intro.intro
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : (P F).B a → α
a' : (P F).A
f' : (P F).B a' → α
abseq : abs ⟨a, f⟩ = abs ⟨a', f'⟩
hf : ∀ (i : (P F).B a'), p (f' i)
u : α
⊢ u ∈ f' '' univ → p u

Tactic:
rintro ⟨i, _, hi⟩

Result:
case mk.mp.intro.intro.intro.intro.intro
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : (P F).B a → α
a' : (P F).A
f' : (P F).B a' → α
abseq : abs ⟨a, f⟩ = abs ⟨a', f'⟩
hf : ∀ (i : (P F).B a'), p (f' i)
u : α
i : (P F).B a'
left✝ : i ∈ univ
hi : f' i = u
⊢ p u

Proof state:
case mk.mpr
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : (P F).B a → α
⊢ (∀ u ∈ supp (abs ⟨a, f⟩), p u) → ∃ a_2 f_1, abs ⟨a, f⟩ = abs ⟨a_2, f_1⟩ ∧ ∀ (i : (P F).B a_2), p (f_1 i)

Tactic:
intro h'

Result:
case mk.mpr
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : (P F).B a → α
h' : ∀ u ∈ supp (abs ⟨a, f⟩), p u
⊢ ∃ a_1 f_1, abs ⟨a, f⟩ = abs ⟨a_1, f_1⟩ ∧ ∀ (i : (P F).B a_1), p (f_1 i)

Proof state:
case mk.mpr
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : (P F).B a → α
h' : ∀ u ∈ supp (abs ⟨a, f⟩), p u
i : (P F).B a
⊢ f i ∈ supp (abs ⟨a, f⟩)

Tactic:
rw [supp_eq_of_isUniform h]

Result:
case mk.mpr
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : (P F).B a → α
h' : ∀ u ∈ supp (abs ⟨a, f⟩), p u
i : (P F).B a
⊢ f i ∈ f '' univ

Proof state:
case mk
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : (P F).B a → α
⊢ (∃ a_1 f_1, abs ⟨a, f⟩ = abs ⟨a_1, f_1⟩ ∧ ∀ (i : (P F).B a_1), p (f_1 i)) ↔ ∀ u ∈ supp (abs ⟨a, f⟩), p u

Tactic:
constructor

Result:
case mk.mp
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : (P F).B a → α
⊢ (∃ a_1 f_1, abs ⟨a, f⟩ = abs ⟨a_1, f_1⟩ ∧ ∀ (i : (P F).B a_1), p (f_1 i)) → ∀ u ∈ supp (abs ⟨a, f⟩), p u

case mk.mpr
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : (P F).B a → α
⊢ (∀ u ∈ supp (abs ⟨a, f⟩), p u) → ∃ a_2 f_1, abs ⟨a, f⟩ = abs ⟨a_2, f_1⟩ ∧ ∀ (i : (P F).B a_2), p (f_1 i)

Proof state:
case mk.mp
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : (P F).B a → α
⊢ (∃ a_1 f_1, abs ⟨a, f⟩ = abs ⟨a_1, f_1⟩ ∧ ∀ (i : (P F).B a_1), p (f_1 i)) → ∀ u ∈ supp (abs ⟨a, f⟩), p u

Tactic:
rintro ⟨a', f', abseq, hf⟩ u

Result:
case mk.mp.intro.intro.intro
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : (P F).B a → α
a' : (P F).A
f' : (P F).B a' → α
abseq : abs ⟨a, f⟩ = abs ⟨a', f'⟩
hf : ∀ (i : (P F).B a'), p (f' i)
u : α
⊢ u ∈ supp (abs ⟨a, f⟩) → p u

Proof state:
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
x : F α
p : α → Prop
⊢ Liftp p x ↔ ∀ u ∈ supp x, p u

Tactic:
rw [liftp_iff, ← abs_repr x]

Result:
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
x : F α
p : α → Prop
⊢ (∃ a f, abs (repr x) = abs ⟨a, f⟩ ∧ ∀ (i : (P F).B a), p (f i)) ↔ ∀ u ∈ supp (abs (repr x)), p u

Proof state:
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
x : F α
p : α → Prop
⊢ (∃ a f, abs (repr x) = abs ⟨a, f⟩ ∧ ∀ (i : (P F).B a), p (f i)) ↔ ∀ u ∈ supp (abs (repr x)), p u

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

Result:
case mk
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : (P F).B a → α
⊢ (∃ a_1 f_1, abs ⟨a, f⟩ = abs ⟨a_1, f_1⟩ ∧ ∀ (i : (P F).B a_1), p (f_1 i)) ↔ ∀ u ∈ supp (abs ⟨a, f⟩), p u