-- Mathlib/Data/PFunctor/Univariate/Basic.lean
theorem supp_eq {α : Type u} (a : P.A) (f : P.B a → α) :
    @supp.{u} P.Obj _ α (⟨a, f⟩ : P α) = f '' univ

Proof state:
case h.mpr.intro
P : PFunctor.{u}
α : Type u
a : P.A
f : P.B a → α
x : α
w✝ : P.B a
h✝ : f w✝ = x
⊢ ∀ ⦃p : α → Prop⦄, (∀ (i : P.B a), p (f i)) → p x

Tactic:
subst x

Result:
case h.mpr.intro
P : PFunctor.{u}
α : Type u
a : P.A
f : P.B a → α
w✝ : P.B a
⊢ ∀ ⦃p : α → Prop⦄, (∀ (i : P.B a), p (f i)) → p (f w✝)

Proof state:
P : PFunctor.{u}
α : Type u
a : P.A
f : P.B a → α
⊢ supp ⟨a, f⟩ = f '' univ

Tactic:
ext x

Result:
case h
P : PFunctor.{u}
α : Type u
a : P.A
f : P.B a → α
x : α
⊢ x ∈ supp ⟨a, f⟩ ↔ x ∈ f '' univ

Proof state:
case h
P : PFunctor.{u}
α : Type u
a : P.A
f : P.B a → α
x : α
⊢ (∀ ⦃p : α → Prop⦄, Liftp p ⟨a, f⟩ → p x) ↔ ∃ y, f y = x

Tactic:
constructor <;> intro h

Result:
case h.mp
P : PFunctor.{u}
α : Type u
a : P.A
f : P.B a → α
x : α
h : ∀ ⦃p : α → Prop⦄, Liftp p ⟨a, f⟩ → p x
⊢ ∃ y, f y = x

case h.mpr
P : PFunctor.{u}
α : Type u
a : P.A
f : P.B a → α
x : α
h : ∃ y, f y = x
⊢ ∀ ⦃p : α → Prop⦄, Liftp p ⟨a, f⟩ → p x

Proof state:
case h.mpr
P : PFunctor.{u}
α : Type u
a : P.A
f : P.B a → α
x : α
h : ∃ y, f y = x
⊢ ∀ ⦃p : α → Prop⦄, Liftp p ⟨a, f⟩ → p x

Tactic:
simp only [liftp_iff']

Result:
case h.mpr
P : PFunctor.{u}
α : Type u
a : P.A
f : P.B a → α
x : α
h : ∃ y, f y = x
⊢ ∀ ⦃p : α → Prop⦄, (∀ (i : P.B a), p (f i)) → p x

Proof state:
case h.mp
P : PFunctor.{u}
α : Type u
a : P.A
f : P.B a → α
x : α
h : ∀ ⦃p : α → Prop⦄, Liftp p ⟨a, f⟩ → p x
⊢ ∀ (i : P.B a), ∃ y, f y = f i

Tactic:
intro

Result:
case h.mp
P : PFunctor.{u}
α : Type u
a : P.A
f : P.B a → α
x : α
h : ∀ ⦃p : α → Prop⦄, Liftp p ⟨a, f⟩ → p x
i✝ : P.B a
⊢ ∃ y, f y = f i✝

Proof state:
case h.mpr
P : PFunctor.{u}
α : Type u
a : P.A
f : P.B a → α
x : α
h : ∃ y, f y = x
⊢ ∀ ⦃p : α → Prop⦄, (∀ (i : P.B a), p (f i)) → p x

Tactic:
cases h

Result:
case h.mpr.intro
P : PFunctor.{u}
α : Type u
a : P.A
f : P.B a → α
x : α
w✝ : P.B a
h✝ : f w✝ = x
⊢ ∀ ⦃p : α → Prop⦄, (∀ (i : P.B a), p (f i)) → p x

Proof state:
case h
P : PFunctor.{u}
α : Type u
a : P.A
f : P.B a → α
x : α
⊢ x ∈ supp ⟨a, f⟩ ↔ x ∈ f '' univ

Tactic:
simp only [supp, image_univ, mem_range, mem_setOf_eq]

Result:
case h
P : PFunctor.{u}
α : Type u
a : P.A
f : P.B a → α
x : α
⊢ (∀ ⦃p : α → Prop⦄, Liftp p ⟨a, f⟩ → p x) ↔ ∃ y, f y = x

Proof state:
case h.mp
P : PFunctor.{u}
α : Type u
a : P.A
f : P.B a → α
x : α
h : ∀ ⦃p : α → Prop⦄, Liftp p ⟨a, f⟩ → p x
⊢ ∃ y, f y = x

Tactic:
apply @h fun x => ∃ y : P.B a, f y = x

Result:
case h.mp
P : PFunctor.{u}
α : Type u
a : P.A
f : P.B a → α
x : α
h : ∀ ⦃p : α → Prop⦄, Liftp p ⟨a, f⟩ → p x
⊢ Liftp (fun x => ∃ y, f y = x) ⟨a, f⟩

Proof state:
case h.mp
P : PFunctor.{u}
α : Type u
a : P.A
f : P.B a → α
x : α
h : ∀ ⦃p : α → Prop⦄, Liftp p ⟨a, f⟩ → p x
⊢ Liftp (fun x => ∃ y, f y = x) ⟨a, f⟩

Tactic:
rw [liftp_iff']

Result:
case h.mp
P : PFunctor.{u}
α : Type u
a : P.A
f : P.B a → α
x : α
h : ∀ ⦃p : α → Prop⦄, Liftp p ⟨a, f⟩ → p x
⊢ ∀ (i : P.B a), ∃ y, f y = f i

Proof state:
case h.mpr.intro
P : PFunctor.{u}
α : Type u
a : P.A
f : P.B a → α
w✝ : P.B a
⊢ ∀ ⦃p : α → Prop⦄, (∀ (i : P.B a), p (f i)) → p (f w✝)

Tactic:
tauto

Result:
no goals

Proof state:
case h.mp
P : PFunctor.{u}
α : Type u
a : P.A
f : P.B a → α
x : α
h : ∀ ⦃p : α → Prop⦄, Liftp p ⟨a, f⟩ → p x
i✝ : P.B a
⊢ ∃ y, f y = f i✝

Tactic:
exact ⟨_, rfl⟩

Result:
no goals