P : PFunctor
α : Type u
p : α → Prop
a : P.A
f : B P a → α
⊢ (∃ a_1 f_1, { fst := a, snd := f } = { fst := a_1, snd := f_1 } ∧ ∀ (i : B P a_1), p (f_1 i)) ↔ ∀ (i : B P a), p (f i)
P : PFunctor
α : Type u
p : α → Prop
a : P.A
f : B P a → α
⊢ Liftp p { fst := a, snd := f } ↔ ∀ (i : B P a), p (f i)
simp only [liftp_iff, Sigma.mk.inj_iff]
case mp
P : PFunctor
α : Type u
p : α → Prop
a : P.A
f : B P a → α
h : ∃ a_1 f_1, { fst := a, snd := f } = { fst := a_1, snd := f_1 } ∧ ∀ (i : B P a_1), p (f_1 i)
⊢ ∀ (i : B P a), p (f i)

case mpr
P : PFunctor
α : Type u
p : α → Prop
a : P.A
f : B P a → α
h : ∀ (i : B P a), p (f i)
⊢ ∃ a_1 f_1, { fst := a, snd := f } = { fst := a_1, snd := f_1 } ∧ ∀ (i : B P a_1), p (f_1 i)
P : PFunctor
α : Type u
p : α → Prop
a : P.A
f : B P a → α
⊢ (∃ a_1 f_1, { fst := a, snd := f } = { fst := a_1, snd := f_1 } ∧ ∀ (i : B P a_1), p (f_1 i)) ↔ ∀ (i : B P a), p (f i)
constructor <;> intro h
no goals
case mpr
P : PFunctor
α : Type u
p : α → Prop
a : P.A
f : B P a → α
h : ∀ (i : B P a), p (f i)
⊢ ∃ a_1 f_1, { fst := a, snd := f } = { fst := a_1, snd := f_1 } ∧ ∀ (i : B P a_1), p (f_1 i)
repeat' first |constructor|assumption
case mp.intro.intro.intro
P : PFunctor
α : Type u
p : α → Prop
a : P.A
f : B P a → α
a' : P.A
f' : B P a' → α
heq : { fst := a, snd := f } = { fst := a', snd := f' }
h' : ∀ (i : B P a'), p (f' i)
⊢ ∀ (i : B P a), p (f i)
case mp
P : PFunctor
α : Type u
p : α → Prop
a : P.A
f : B P a → α
h : ∃ a_1 f_1, { fst := a, snd := f } = { fst := a_1, snd := f_1 } ∧ ∀ (i : B P a_1), p (f_1 i)
⊢ ∀ (i : B P a), p (f i)
rcases h with ⟨a', f', heq, h'⟩
case mp.intro.intro.intro.refl
P : PFunctor
α : Type u
p : α → Prop
a : P.A
f : B P a → α
h' : ∀ (i : B P a), p (f i)
⊢ ∀ (i : B P a), p (f i)
case mp.intro.intro.intro
P : PFunctor
α : Type u
p : α → Prop
a : P.A
f : B P a → α
a' : P.A
f' : B P a' → α
heq : { fst := a, snd := f } = { fst := a', snd := f' }
h' : ∀ (i : B P a'), p (f' i)
⊢ ∀ (i : B P a), p (f i)
cases heq
no goals
case mp.intro.intro.intro.refl
P : PFunctor
α : Type u
p : α → Prop
a : P.A
f : B P a → α
h' : ∀ (i : B P a), p (f i)
⊢ ∀ (i : B P a), p (f i)
assumption
no goals
case mpr.h.h.right
P : PFunctor
α : Type u
p : α → Prop
a : P.A
f : B P a → α
h : ∀ (i : B P a), p (f i)
⊢ ∀ (i : B P a), p (f i)
first |constructor|assumption
case mpr.h.h.right
P : PFunctor
α : Type u
p : α → Prop
a : P.A
f : B P a → α
h : ∀ (i : B P a), p (f i)
⊢ ∀ (i : B P a), p (f i)
case mpr.h.h.right
P : PFunctor
α : Type u
p : α → Prop
a : P.A
f : B P a → α
h : ∀ (i : B P a), p (f i)
⊢ ∀ (i : B P a), p (f i)
constructor
no goals
case mpr.h.h.right
P : PFunctor
α : Type u
p : α → Prop
a : P.A
f : B P a → α
h : ∀ (i : B P a), p (f i)
⊢ ∀ (i : B P a), p (f i)
assumption