[GOAL]
P : PFunctor
α β : Type u
p : Obj P (W P)
⊢ dest (mk p) = p
[PROOFSTEP]
cases p
[GOAL]
case mk
P : PFunctor
α β : Type u
fst✝ : P.A
snd✝ : B P fst✝ → W P
⊢ dest (mk { fst := fst✝, snd := snd✝ }) = { fst := fst✝, snd := snd✝ }
[PROOFSTEP]
rfl
[GOAL]
P : PFunctor
α β : Type u
p : W P
⊢ mk (dest p) = p
[PROOFSTEP]
cases p
[GOAL]
case mk
P : PFunctor
α β : Type u
a✝ : P.A
f✝ : B P a✝ → WType P.B
⊢ mk (dest (WType.mk a✝ f✝)) = WType.mk a✝ f✝
[PROOFSTEP]
rfl
[GOAL]
P : PFunctor
α✝ β✝ α β : Type u
x : Obj P α
f : α → β
⊢ (f <$> x).fst = x.fst
[PROOFSTEP]
cases x
[GOAL]
case mk
P : PFunctor
α✝ β✝ α β : Type u
f : α → β
fst✝ : P.A
snd✝ : B P fst✝ → α
⊢ (f <$> { fst := fst✝, snd := snd✝ }).fst = { fst := fst✝, snd := snd✝ }.fst
[PROOFSTEP]
rfl
[GOAL]
P : PFunctor
α✝ β✝ : Type u
inst✝² : DecidableEq P.A
α β : Type u
inst✝¹ : Inhabited α
inst✝ : Inhabited β
x : Obj P α
f : α → β
i : IdxCat P
h : i.fst = x.fst
⊢ Obj.iget (f <$> x) i = f (Obj.iget x i)
[PROOFSTEP]
simp only [Obj.iget, fst_map, *, dif_pos, eq_self_iff_true]
[GOAL]
P : PFunctor
α✝ β✝ : Type u
inst✝² : DecidableEq P.A
α β : Type u
inst✝¹ : Inhabited α
inst✝ : Inhabited β
x : Obj P α
f : α → β
i : IdxCat P
h : i.fst = x.fst
⊢ Sigma.snd (f <$> x) (cast (_ : B P i.fst = B P (f <$> x).fst) i.snd) =
    f (Sigma.snd x (cast (_ : B P i.fst = B P x.fst) i.snd))
[PROOFSTEP]
cases x
[GOAL]
case mk
P : PFunctor
α✝ β✝ : Type u
inst✝² : DecidableEq P.A
α β : Type u
inst✝¹ : Inhabited α
inst✝ : Inhabited β
f : α → β
i : IdxCat P
fst✝ : P.A
snd✝ : B P fst✝ → α
h : i.fst = { fst := fst✝, snd := snd✝ }.fst
⊢ Sigma.snd (f <$> { fst := fst✝, snd := snd✝ })
      (cast (_ : B P i.fst = B P (f <$> { fst := fst✝, snd := snd✝ }).fst) i.snd) =
    f (Sigma.snd { fst := fst✝, snd := snd✝ } (cast (_ : B P i.fst = B P { fst := fst✝, snd := snd✝ }.fst) i.snd))
[PROOFSTEP]
rfl
[GOAL]
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)
[PROOFSTEP]
constructor
[GOAL]
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)
[PROOFSTEP]
rintro ⟨y, hy⟩
[GOAL]
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)
[PROOFSTEP]
cases' h : y with a f
[GOAL]
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)
[PROOFSTEP]
refine' ⟨a, fun i => (f i).val, _, fun i => (f i).property⟩
[GOAL]
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) }
[PROOFSTEP]
rw [← hy, h, PFunctor.map_eq]
[GOAL]
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) }
[PROOFSTEP]
congr
[GOAL]
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
[PROOFSTEP]
rintro ⟨a, f, xeq, pf⟩
[GOAL]
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
[PROOFSTEP]
use⟨a, fun i => ⟨f i, pf i⟩⟩
[GOAL]
case h
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
[PROOFSTEP]
rw [xeq]
[GOAL]
case h
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 }
[PROOFSTEP]
rfl
[GOAL]
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)
[PROOFSTEP]
simp only [liftp_iff, Sigma.mk.inj_iff]
[GOAL]
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)
[PROOFSTEP]
constructor
[GOAL]
case mp
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)
[PROOFSTEP]
intro h
[GOAL]
case mpr
P : PFunctor
α : Type u
p : α → Prop
a : P.A
f : B P a → α
⊢ (∀ (i : B P a), p (f i)) → ∃ a_2 f_1, { fst := a, snd := f } = { fst := a_2, snd := f_1 } ∧ ∀ (i : B P a_2), p (f_1 i)
[PROOFSTEP]
intro h
[GOAL]
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)
[PROOFSTEP]
rcases h with ⟨a', f', heq, h'⟩
[GOAL]
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)
[PROOFSTEP]
cases heq
[GOAL]
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)
[PROOFSTEP]
assumption
[GOAL]
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)
[PROOFSTEP]
repeat'
  first
  | constructor
  | assumption
[GOAL]
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)
[PROOFSTEP]
first
| constructor
| assumption
[GOAL]
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)
[PROOFSTEP]
constructor
[GOAL]
case mpr.h
P : PFunctor
α : Type u
p : α → Prop
a : P.A
f : B P a → α
h : ∀ (i : B P a), p (f i)
⊢ ∃ f_1, { fst := a, snd := f } = { fst := ?mpr.w, snd := f_1 } ∧ ∀ (i : B P ?mpr.w), p (f_1 i)
[PROOFSTEP]
first
| constructor
| assumption
[GOAL]
case mpr.h
P : PFunctor
α : Type u
p : α → Prop
a : P.A
f : B P a → α
h : ∀ (i : B P a), p (f i)
⊢ ∃ f_1, { fst := a, snd := f } = { fst := ?mpr.w, snd := f_1 } ∧ ∀ (i : B P ?mpr.w), p (f_1 i)
[PROOFSTEP]
constructor
[GOAL]
case mpr.h.h
P : PFunctor
α : Type u
p : α → Prop
a : P.A
f : B P a → α
h : ∀ (i : B P a), p (f i)
⊢ { fst := a, snd := f } = { fst := ?mpr.w, snd := ?mpr.h.w } ∧ ∀ (i : B P ?mpr.w), p (?mpr.h.w i)
[PROOFSTEP]
first
| constructor
| assumption
[GOAL]
case mpr.h.h
P : PFunctor
α : Type u
p : α → Prop
a : P.A
f : B P a → α
h : ∀ (i : B P a), p (f i)
⊢ { fst := a, snd := f } = { fst := ?mpr.w, snd := ?mpr.h.w } ∧ ∀ (i : B P ?mpr.w), p (?mpr.h.w i)
[PROOFSTEP]
constructor
[GOAL]
case mpr.h.h.left
P : PFunctor
α : Type u
p : α → Prop
a : P.A
f : B P a → α
h : ∀ (i : B P a), p (f i)
⊢ { fst := a, snd := f } = { fst := ?mpr.w, snd := ?mpr.h.w }
[PROOFSTEP]
first
| constructor
| assumption
[GOAL]
case mpr.h.h.left
P : PFunctor
α : Type u
p : α → Prop
a : P.A
f : B P a → α
h : ∀ (i : B P a), p (f i)
⊢ { fst := a, snd := f } = { fst := ?mpr.w, snd := ?mpr.h.w }
[PROOFSTEP]
constructor
[GOAL]
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)
[PROOFSTEP]
first
| constructor
| assumption
[GOAL]
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)
[PROOFSTEP]
constructor
[GOAL]
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)
[PROOFSTEP]
assumption
[GOAL]
P : PFunctor
α : Type u
r : α → α → Prop
x y : Obj P α
⊢ Liftr r x y ↔ ∃ a f₀ f₁, x = { fst := a, snd := f₀ } ∧ y = { fst := a, snd := f₁ } ∧ ∀ (i : B P a), r (f₀ i) (f₁ i)
[PROOFSTEP]
constructor
[GOAL]
case mp
P : PFunctor
α : Type u
r : α → α → Prop
x y : Obj P α
⊢ Liftr r x y → ∃ a f₀ f₁, x = { fst := a, snd := f₀ } ∧ y = { fst := a, snd := f₁ } ∧ ∀ (i : B P a), r (f₀ i) (f₁ i)
[PROOFSTEP]
rintro ⟨u, xeq, yeq⟩
[GOAL]
case mp.intro.intro
P : PFunctor
α : Type u
r : α → α → Prop
x y : Obj P α
u : Obj P { p // r p.fst p.snd }
xeq : (fun t => (↑t).fst) <$> u = x
yeq : (fun t => (↑t).snd) <$> u = y
⊢ ∃ a f₀ f₁, x = { fst := a, snd := f₀ } ∧ y = { fst := a, snd := f₁ } ∧ ∀ (i : B P a), r (f₀ i) (f₁ i)
[PROOFSTEP]
cases' h : u with a f
[GOAL]
case mp.intro.intro.mk
P : PFunctor
α : Type u
r : α → α → Prop
x y : Obj P α
u : Obj P { p // r p.fst p.snd }
xeq : (fun t => (↑t).fst) <$> u = x
yeq : (fun t => (↑t).snd) <$> u = y
a : P.A
f : B P a → { p // r p.fst p.snd }
h : u = { fst := a, snd := f }
⊢ ∃ a f₀ f₁, x = { fst := a, snd := f₀ } ∧ y = { fst := a, snd := f₁ } ∧ ∀ (i : B P a), r (f₀ i) (f₁ i)
[PROOFSTEP]
use a, fun i => (f i).val.fst, fun i => (f i).val.snd
[GOAL]
case h
P : PFunctor
α : Type u
r : α → α → Prop
x y : Obj P α
u : Obj P { p // r p.fst p.snd }
xeq : (fun t => (↑t).fst) <$> u = x
yeq : (fun t => (↑t).snd) <$> u = y
a : P.A
f : B P a → { p // r p.fst p.snd }
h : u = { fst := a, snd := f }
⊢ x = { fst := a, snd := fun i => (↑(f i)).fst } ∧
    y = { fst := a, snd := fun i => (↑(f i)).snd } ∧ ∀ (i : B P a), r (↑(f i)).fst (↑(f i)).snd
[PROOFSTEP]
constructor
[GOAL]
case h.left
P : PFunctor
α : Type u
r : α → α → Prop
x y : Obj P α
u : Obj P { p // r p.fst p.snd }
xeq : (fun t => (↑t).fst) <$> u = x
yeq : (fun t => (↑t).snd) <$> u = y
a : P.A
f : B P a → { p // r p.fst p.snd }
h : u = { fst := a, snd := f }
⊢ x = { fst := a, snd := fun i => (↑(f i)).fst }
[PROOFSTEP]
rw [← xeq, h]
[GOAL]
case h.left
P : PFunctor
α : Type u
r : α → α → Prop
x y : Obj P α
u : Obj P { p // r p.fst p.snd }
xeq : (fun t => (↑t).fst) <$> u = x
yeq : (fun t => (↑t).snd) <$> u = y
a : P.A
f : B P a → { p // r p.fst p.snd }
h : u = { fst := a, snd := f }
⊢ (fun t => (↑t).fst) <$> { fst := a, snd := f } = { fst := a, snd := fun i => (↑(f i)).fst }
[PROOFSTEP]
rfl
[GOAL]
case h.right
P : PFunctor
α : Type u
r : α → α → Prop
x y : Obj P α
u : Obj P { p // r p.fst p.snd }
xeq : (fun t => (↑t).fst) <$> u = x
yeq : (fun t => (↑t).snd) <$> u = y
a : P.A
f : B P a → { p // r p.fst p.snd }
h : u = { fst := a, snd := f }
⊢ y = { fst := a, snd := fun i => (↑(f i)).snd } ∧ ∀ (i : B P a), r (↑(f i)).fst (↑(f i)).snd
[PROOFSTEP]
constructor
[GOAL]
case h.right.left
P : PFunctor
α : Type u
r : α → α → Prop
x y : Obj P α
u : Obj P { p // r p.fst p.snd }
xeq : (fun t => (↑t).fst) <$> u = x
yeq : (fun t => (↑t).snd) <$> u = y
a : P.A
f : B P a → { p // r p.fst p.snd }
h : u = { fst := a, snd := f }
⊢ y = { fst := a, snd := fun i => (↑(f i)).snd }
[PROOFSTEP]
rw [← yeq, h]
[GOAL]
case h.right.left
P : PFunctor
α : Type u
r : α → α → Prop
x y : Obj P α
u : Obj P { p // r p.fst p.snd }
xeq : (fun t => (↑t).fst) <$> u = x
yeq : (fun t => (↑t).snd) <$> u = y
a : P.A
f : B P a → { p // r p.fst p.snd }
h : u = { fst := a, snd := f }
⊢ (fun t => (↑t).snd) <$> { fst := a, snd := f } = { fst := a, snd := fun i => (↑(f i)).snd }
[PROOFSTEP]
rfl
[GOAL]
case h.right.right
P : PFunctor
α : Type u
r : α → α → Prop
x y : Obj P α
u : Obj P { p // r p.fst p.snd }
xeq : (fun t => (↑t).fst) <$> u = x
yeq : (fun t => (↑t).snd) <$> u = y
a : P.A
f : B P a → { p // r p.fst p.snd }
h : u = { fst := a, snd := f }
⊢ ∀ (i : B P a), r (↑(f i)).fst (↑(f i)).snd
[PROOFSTEP]
intro i
[GOAL]
case h.right.right
P : PFunctor
α : Type u
r : α → α → Prop
x y : Obj P α
u : Obj P { p // r p.fst p.snd }
xeq : (fun t => (↑t).fst) <$> u = x
yeq : (fun t => (↑t).snd) <$> u = y
a : P.A
f : B P a → { p // r p.fst p.snd }
h : u = { fst := a, snd := f }
i : B P a
⊢ r (↑(f i)).fst (↑(f i)).snd
[PROOFSTEP]
exact (f i).property
[GOAL]
case mpr
P : PFunctor
α : Type u
r : α → α → Prop
x y : Obj P α
⊢ (∃ a f₀ f₁, x = { fst := a, snd := f₀ } ∧ y = { fst := a, snd := f₁ } ∧ ∀ (i : B P a), r (f₀ i) (f₁ i)) → Liftr r x y
[PROOFSTEP]
rintro ⟨a, f₀, f₁, xeq, yeq, h⟩
[GOAL]
case mpr.intro.intro.intro.intro.intro
P : PFunctor
α : Type u
r : α → α → Prop
x y : Obj P α
a : P.A
f₀ f₁ : B P a → α
xeq : x = { fst := a, snd := f₀ }
yeq : y = { fst := a, snd := f₁ }
h : ∀ (i : B P a), r (f₀ i) (f₁ i)
⊢ Liftr r x y
[PROOFSTEP]
use⟨a, fun i => ⟨(f₀ i, f₁ i), h i⟩⟩
[GOAL]
case h
P : PFunctor
α : Type u
r : α → α → Prop
x y : Obj P α
a : P.A
f₀ f₁ : B P a → α
xeq : x = { fst := a, snd := f₀ }
yeq : y = { fst := a, snd := f₁ }
h : ∀ (i : B P a), r (f₀ i) (f₁ i)
⊢ (fun t => (↑t).fst) <$> { fst := a, snd := fun i => { val := (f₀ i, f₁ i), property := (_ : r (f₀ i) (f₁ i)) } } = x ∧
    (fun t => (↑t).snd) <$> { fst := a, snd := fun i => { val := (f₀ i, f₁ i), property := (_ : r (f₀ i) (f₁ i)) } } = y
[PROOFSTEP]
constructor
[GOAL]
case h.left
P : PFunctor
α : Type u
r : α → α → Prop
x y : Obj P α
a : P.A
f₀ f₁ : B P a → α
xeq : x = { fst := a, snd := f₀ }
yeq : y = { fst := a, snd := f₁ }
h : ∀ (i : B P a), r (f₀ i) (f₁ i)
⊢ (fun t => (↑t).fst) <$> { fst := a, snd := fun i => { val := (f₀ i, f₁ i), property := (_ : r (f₀ i) (f₁ i)) } } = x
[PROOFSTEP]
rw [xeq]
[GOAL]
case h.left
P : PFunctor
α : Type u
r : α → α → Prop
x y : Obj P α
a : P.A
f₀ f₁ : B P a → α
xeq : x = { fst := a, snd := f₀ }
yeq : y = { fst := a, snd := f₁ }
h : ∀ (i : B P a), r (f₀ i) (f₁ i)
⊢ (fun t => (↑t).fst) <$> { fst := a, snd := fun i => { val := (f₀ i, f₁ i), property := (_ : r (f₀ i) (f₁ i)) } } =
    { fst := a, snd := f₀ }
[PROOFSTEP]
rfl
[GOAL]
case h.right
P : PFunctor
α : Type u
r : α → α → Prop
x y : Obj P α
a : P.A
f₀ f₁ : B P a → α
xeq : x = { fst := a, snd := f₀ }
yeq : y = { fst := a, snd := f₁ }
h : ∀ (i : B P a), r (f₀ i) (f₁ i)
⊢ (fun t => (↑t).snd) <$> { fst := a, snd := fun i => { val := (f₀ i, f₁ i), property := (_ : r (f₀ i) (f₁ i)) } } = y
[PROOFSTEP]
rw [yeq]
[GOAL]
case h.right
P : PFunctor
α : Type u
r : α → α → Prop
x y : Obj P α
a : P.A
f₀ f₁ : B P a → α
xeq : x = { fst := a, snd := f₀ }
yeq : y = { fst := a, snd := f₁ }
h : ∀ (i : B P a), r (f₀ i) (f₁ i)
⊢ (fun t => (↑t).snd) <$> { fst := a, snd := fun i => { val := (f₀ i, f₁ i), property := (_ : r (f₀ i) (f₁ i)) } } =
    { fst := a, snd := f₁ }
[PROOFSTEP]
rfl
[GOAL]
P : PFunctor
α : Type u
a : P.A
f : B P a → α
⊢ supp { fst := a, snd := f } = f '' univ
[PROOFSTEP]
ext x
[GOAL]
case h
P : PFunctor
α : Type u
a : P.A
f : B P a → α
x : α
⊢ x ∈ supp { fst := a, snd := f } ↔ x ∈ f '' univ
[PROOFSTEP]
simp only [supp, image_univ, mem_range, mem_setOf_eq]
[GOAL]
case h
P : PFunctor
α : Type u
a : P.A
f : B P a → α
x : α
⊢ (∀ ⦃p : α → Prop⦄, Liftp p { fst := a, snd := f } → p x) ↔ ∃ y, f y = x
[PROOFSTEP]
constructor
[GOAL]
case h.mp
P : PFunctor
α : Type u
a : P.A
f : B P a → α
x : α
⊢ (∀ ⦃p : α → Prop⦄, Liftp p { fst := a, snd := f } → p x) → ∃ y, f y = x
[PROOFSTEP]
intro h
[GOAL]
case h.mpr
P : PFunctor
α : Type u
a : P.A
f : B P a → α
x : α
⊢ (∃ y, f y = x) → ∀ ⦃p : α → Prop⦄, Liftp p { fst := a, snd := f } → p x
[PROOFSTEP]
intro h
[GOAL]
case h.mp
P : PFunctor
α : Type u
a : P.A
f : B P a → α
x : α
h : ∀ ⦃p : α → Prop⦄, Liftp p { fst := a, snd := f } → p x
⊢ ∃ y, f y = x
[PROOFSTEP]
apply @h fun x => ∃ y : P.B a, f y = x
[GOAL]
case h.mp
P : PFunctor
α : Type u
a : P.A
f : B P a → α
x : α
h : ∀ ⦃p : α → Prop⦄, Liftp p { fst := a, snd := f } → p x
⊢ Liftp (fun x => ∃ y, f y = x) { fst := a, snd := f }
[PROOFSTEP]
rw [liftp_iff']
[GOAL]
case h.mp
P : PFunctor
α : Type u
a : P.A
f : B P a → α
x : α
h : ∀ ⦃p : α → Prop⦄, Liftp p { fst := a, snd := f } → p x
⊢ ∀ (i : B P a), ∃ y, f y = f i
[PROOFSTEP]
intro
[GOAL]
case h.mp
P : PFunctor
α : Type u
a : P.A
f : B P a → α
x : α
h : ∀ ⦃p : α → Prop⦄, Liftp p { fst := a, snd := f } → p x
i✝ : B P a
⊢ ∃ y, f y = f i✝
[PROOFSTEP]
refine' ⟨_, rfl⟩
[GOAL]
case h.mpr
P : PFunctor
α : Type u
a : P.A
f : B P a → α
x : α
h : ∃ y, f y = x
⊢ ∀ ⦃p : α → Prop⦄, Liftp p { fst := a, snd := f } → p x
[PROOFSTEP]
simp only [liftp_iff']
[GOAL]
case h.mpr
P : PFunctor
α : Type u
a : P.A
f : B P a → α
x : α
h : ∃ y, f y = x
⊢ ∀ ⦃p : α → Prop⦄, (∀ (i : B P a), p (f i)) → p x
[PROOFSTEP]
cases h
[GOAL]
case h.mpr.intro
P : PFunctor
α : Type u
a : P.A
f : B P a → α
x : α
w✝ : B P a
h✝ : f w✝ = x
⊢ ∀ ⦃p : α → Prop⦄, (∀ (i : B P a), p (f i)) → p x
[PROOFSTEP]
subst x
[GOAL]
case h.mpr.intro
P : PFunctor
α : Type u
a : P.A
f : B P a → α
w✝ : B P a
⊢ ∀ ⦃p : α → Prop⦄, (∀ (i : B P a), p (f i)) → p (f w✝)
[PROOFSTEP]
tauto
