case mp
P : PFunctor
α : Type u
p : α → Prop
x : Obj P α
⊢ Liftp p x → ∃ a f, x = { fst := a, snd := f } ∧ ∀ (i : B P a), p (f i)

case mpr
P : PFunctor
α : Type u
p : α → Prop
x : Obj P α
⊢ (∃ a f, x = { fst := a, snd := f } ∧ ∀ (i : B P a), p (f i)) → Liftp p x
P : PFunctor
α : Type u
p : α → Prop
x : Obj P α
⊢ Liftp p x ↔ ∃ a f, x = { fst := a, snd := f } ∧ ∀ (i : B P a), p (f i)
constructor
case mpr.intro.intro.intro
P : PFunctor
α : Type u
p : α → Prop
x : Obj P α
a : P.A
f : B P a → α
xeq : x = { fst := a, snd := f }
pf : ∀ (i : B P a), p (f i)
⊢ Liftp p x
case mpr
P : PFunctor
α : Type u
p : α → Prop
x : Obj P α
⊢ (∃ a f, x = { fst := a, snd := f } ∧ ∀ (i : B P a), p (f i)) → Liftp p x
rintro ⟨a, f, xeq, pf⟩
case mpr.intro.intro.intro
P : PFunctor
α : Type u
p : α → Prop
x : Obj P α
a : P.A
f : B P a → α
xeq : x = { fst := a, snd := f }
pf : ∀ (i : B P a), p (f i)
⊢ Subtype.val <$> { fst := a, snd := fun i => { val := f i, property := (_ : p (f i)) } } = x
case mpr.intro.intro.intro
P : PFunctor
α : Type u
p : α → Prop
x : Obj P α
a : P.A
f : B P a → α
xeq : x = { fst := a, snd := f }
pf : ∀ (i : B P a), p (f i)
⊢ Liftp p x
use ⟨a, fun i => ⟨f i, pf i⟩⟩
case mpr.intro.intro.intro
P : PFunctor
α : Type u
p : α → Prop
x : Obj P α
a : P.A
f : B P a → α
xeq : x = { fst := a, snd := f }
pf : ∀ (i : B P a), p (f i)
⊢ Subtype.val <$> { fst := a, snd := fun i => { val := f i, property := (_ : p (f i)) } } = { fst := a, snd := f }
case mpr.intro.intro.intro
P : PFunctor
α : Type u
p : α → Prop
x : Obj P α
a : P.A
f : B P a → α
xeq : x = { fst := a, snd := f }
pf : ∀ (i : B P a), p (f i)
⊢ Subtype.val <$> { fst := a, snd := fun i => { val := f i, property := (_ : p (f i)) } } = x
rw [xeq]
no goals
case mpr.intro.intro.intro
P : PFunctor
α : Type u
p : α → Prop
x : Obj P α
a : P.A
f : B P a → α
xeq : x = { fst := a, snd := f }
pf : ∀ (i : B P a), p (f i)
⊢ Subtype.val <$> { fst := a, snd := fun i => { val := f i, property := (_ : p (f i)) } } = { fst := a, snd := f }
rfl
case mp.intro
P : PFunctor
α : Type u
p : α → Prop
x : Obj P α
y : Obj P (Subtype p)
hy : Subtype.val <$> y = x
⊢ ∃ a f, x = { fst := a, snd := f } ∧ ∀ (i : B P a), p (f i)
case mp
P : PFunctor
α : Type u
p : α → Prop
x : Obj P α
⊢ Liftp p x → ∃ a f, x = { fst := a, snd := f } ∧ ∀ (i : B P a), p (f i)
rintro ⟨y, hy⟩
case mp.intro.mk
P : PFunctor
α : Type u
p : α → Prop
x : Obj P α
y : Obj P (Subtype p)
hy : Subtype.val <$> y = x
a : P.A
f : B P a → Subtype p
h : y = { fst := a, snd := f }
⊢ ∃ a f, x = { fst := a, snd := f } ∧ ∀ (i : B P a), p (f i)
case mp.intro
P : PFunctor
α : Type u
p : α → Prop
x : Obj P α
y : Obj P (Subtype p)
hy : Subtype.val <$> y = x
⊢ ∃ a f, x = { fst := a, snd := f } ∧ ∀ (i : B P a), p (f i)
cases' h : y with a f
case mp.intro.mk
P : PFunctor
α : Type u
p : α → Prop
x : Obj P α
y : Obj P (Subtype p)
hy : Subtype.val <$> y = x
a : P.A
f : B P a → Subtype p
h : y = { fst := a, snd := f }
⊢ x = { fst := a, snd := fun i => ↑(f i) }
case mp.intro.mk
P : PFunctor
α : Type u
p : α → Prop
x : Obj P α
y : Obj P (Subtype p)
hy : Subtype.val <$> y = x
a : P.A
f : B P a → Subtype p
h : y = { fst := a, snd := f }
⊢ ∃ a f, x = { fst := a, snd := f } ∧ ∀ (i : B P a), p (f i)
refine' ⟨a, fun i => (f i).val, _, fun i => (f i).property⟩
case mp.intro.mk
P : PFunctor
α : Type u
p : α → Prop
x : Obj P α
y : Obj P (Subtype p)
hy : Subtype.val <$> y = x
a : P.A
f : B P a → Subtype p
h : y = { fst := a, snd := f }
⊢ { fst := a, snd := Subtype.val ∘ f } = { fst := a, snd := fun i => ↑(f i) }
case mp.intro.mk
P : PFunctor
α : Type u
p : α → Prop
x : Obj P α
y : Obj P (Subtype p)
hy : Subtype.val <$> y = x
a : P.A
f : B P a → Subtype p
h : y = { fst := a, snd := f }
⊢ x = { fst := a, snd := fun i => ↑(f i) }
rw [← hy, h, PFunctor.map_eq]
no goals
case mp.intro.mk
P : PFunctor
α : Type u
p : α → Prop
x : Obj P α
y : Obj P (Subtype p)
hy : Subtype.val <$> y = x
a : P.A
f : B P a → Subtype p
h : y = { fst := a, snd := f }
⊢ { fst := a, snd := Subtype.val ∘ f } = { fst := a, snd := fun i => ↑(f i) }
congr