-- Mathlib/Data/PFunctor/Univariate/Basic.lean
theorem liftp_iff {α : Type u} (p : α → Prop) (x : P α) :
    Liftp p x ↔ ∃ a f, x = ⟨a, f⟩ ∧ ∀ i, p (f i)

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

Tactic:
rintro ⟨y, hy⟩

Result:
case mp.intro
P : PFunctor.{u}
α : Type u
p : α → Prop
x : ↑P α
y : ↑P (Subtype p)
hy : Subtype.val <$> y = x
⊢ ∃ a f, x = ⟨a, f⟩ ∧ ∀ (i : P.B a), p (f i)

Proof state:
P : PFunctor.{u}
α : Type u
p : α → Prop
x : ↑P α
⊢ Liftp p x ↔ ∃ a f, x = ⟨a, f⟩ ∧ ∀ (i : P.B a), p (f i)

Tactic:
constructor

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

case mpr
P : PFunctor.{u}
α : Type u
p : α → Prop
x : ↑P α
⊢ (∃ a f, x = ⟨a, f⟩ ∧ ∀ (i : P.B a), p (f i)) → Liftp p x

Proof state:
case h
P : PFunctor.{u}
α : Type u
p : α → Prop
x : ↑P α
a : P.A
f : P.B a → α
xeq : x = ⟨a, f⟩
pf : ∀ (i : P.B a), p (f i)
⊢ Subtype.val <$> ⟨a, fun i => ⟨f i, ⋯⟩⟩ = x

Tactic:
rw [xeq]

Result:
case h
P : PFunctor.{u}
α : Type u
p : α → Prop
x : ↑P α
a : P.A
f : P.B a → α
xeq : x = ⟨a, f⟩
pf : ∀ (i : P.B a), p (f i)
⊢ Subtype.val <$> ⟨a, fun i => ⟨f i, ⋯⟩⟩ = ⟨a, f⟩

Proof state:
case mp.intro.mk
P : PFunctor.{u}
α : Type u
p : α → Prop
x : ↑P α
y : ↑P (Subtype p)
hy : Subtype.val <$> y = x
a : P.A
f : P.B a → Subtype p
h : y = ⟨a, f⟩
⊢ ∃ a f, x = ⟨a, f⟩ ∧ ∀ (i : P.B a), p (f i)

Tactic:
refine ⟨a, fun i => (f i).val, ?_, fun i => (f i).property⟩

Result:
case mp.intro.mk
P : PFunctor.{u}
α : Type u
p : α → Prop
x : ↑P α
y : ↑P (Subtype p)
hy : Subtype.val <$> y = x
a : P.A
f : P.B a → Subtype p
h : y = ⟨a, f⟩
⊢ x = ⟨a, fun i => ↑(f i)⟩

Proof state:
case mp.intro.mk
P : PFunctor.{u}
α : Type u
p : α → Prop
x : ↑P α
y : ↑P (Subtype p)
hy : Subtype.val <$> y = x
a : P.A
f : P.B a → Subtype p
h : y = ⟨a, f⟩
⊢ ⟨a, Subtype.val ∘ f⟩ = ⟨a, fun i => ↑(f i)⟩

Tactic:
congr

Result:
no goals

Proof state:
case h
P : PFunctor.{u}
α : Type u
p : α → Prop
x : ↑P α
a : P.A
f : P.B a → α
xeq : x = ⟨a, f⟩
pf : ∀ (i : P.B a), p (f i)
⊢ Subtype.val <$> ⟨a, fun i => ⟨f i, ⋯⟩⟩ = ⟨a, f⟩

Tactic:
rfl

Result:
no goals

Proof state:
case mpr.intro.intro.intro
P : PFunctor.{u}
α : Type u
p : α → Prop
x : ↑P α
a : P.A
f : P.B a → α
xeq : x = ⟨a, f⟩
pf : ∀ (i : P.B a), p (f i)
⊢ Liftp p x

Tactic:
use ⟨a, fun i => ⟨f i, pf i⟩⟩

Result:
case h
P : PFunctor.{u}
α : Type u
p : α → Prop
x : ↑P α
a : P.A
f : P.B a → α
xeq : x = ⟨a, f⟩
pf : ∀ (i : P.B a), p (f i)
⊢ Subtype.val <$> ⟨a, fun i => ⟨f i, ⋯⟩⟩ = x

Proof state:
case mp.intro
P : PFunctor.{u}
α : Type u
p : α → Prop
x : ↑P α
y : ↑P (Subtype p)
hy : Subtype.val <$> y = x
⊢ ∃ a f, x = ⟨a, f⟩ ∧ ∀ (i : P.B a), p (f i)

Tactic:
rcases h : y with ⟨a, f⟩

Result:
case mp.intro.mk
P : PFunctor.{u}
α : Type u
p : α → Prop
x : ↑P α
y : ↑P (Subtype p)
hy : Subtype.val <$> y = x
a : P.A
f : P.B a → Subtype p
h : y = ⟨a, f⟩
⊢ ∃ a f, x = ⟨a, f⟩ ∧ ∀ (i : P.B a), p (f i)

Proof state:
case mpr
P : PFunctor.{u}
α : Type u
p : α → Prop
x : ↑P α
⊢ (∃ a f, x = ⟨a, f⟩ ∧ ∀ (i : P.B a), p (f i)) → Liftp p x

Tactic:
rintro ⟨a, f, xeq, pf⟩

Result:
case mpr.intro.intro.intro
P : PFunctor.{u}
α : Type u
p : α → Prop
x : ↑P α
a : P.A
f : P.B a → α
xeq : x = ⟨a, f⟩
pf : ∀ (i : P.B a), p (f i)
⊢ Liftp p x

Proof state:
case mp.intro.mk
P : PFunctor.{u}
α : Type u
p : α → Prop
x : ↑P α
y : ↑P (Subtype p)
hy : Subtype.val <$> y = x
a : P.A
f : P.B a → Subtype p
h : y = ⟨a, f⟩
⊢ x = ⟨a, fun i => ↑(f i)⟩

Tactic:
rw [← hy, h, map_eq_map, PFunctor.map_eq]

Result:
case mp.intro.mk
P : PFunctor.{u}
α : Type u
p : α → Prop
x : ↑P α
y : ↑P (Subtype p)
hy : Subtype.val <$> y = x
a : P.A
f : P.B a → Subtype p
h : y = ⟨a, f⟩
⊢ ⟨a, Subtype.val ∘ f⟩ = ⟨a, fun i => ↑(f i)⟩