case mp
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
p : α → Prop
x : F α
⊢ Liftp p x → ∃ u, abs u = x ∧ ∀ (i : PFunctor.B (P F) u.fst), p (Sigma.snd u i)

case mpr
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
p : α → Prop
x : F α
⊢ (∃ u, abs u = x ∧ ∀ (i : PFunctor.B (P F) u.fst), p (Sigma.snd u i)) → Liftp p x
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
p : α → Prop
x : F α
⊢ Liftp p x ↔ ∃ u, abs u = x ∧ ∀ (i : PFunctor.B (P F) u.fst), p (Sigma.snd u i)
constructor
case mpr.intro.mk.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
p : α → Prop
x : F α
a : (P F).A
f : PFunctor.B (P F) a → α
h₀ : abs { fst := a, snd := f } = x
h₁ : ∀ (i : PFunctor.B (P F) { fst := a, snd := f }.fst), p (Sigma.snd { fst := a, snd := f } i)
⊢ Liftp p x
case mpr
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
p : α → Prop
x : F α
⊢ (∃ u, abs u = x ∧ ∀ (i : PFunctor.B (P F) u.fst), p (Sigma.snd u i)) → Liftp p x
rintro ⟨⟨a, f⟩, h₀, h₁⟩
case mpr.intro.mk.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
p : α → Prop
x : F α
a : (P F).A
f : PFunctor.B (P F) a → α
h₀ : abs { fst := a, snd := f } = x
h₁ : ∀ (i : PFunctor.B (P F) a), p (f i)
⊢ Liftp p x
case mpr.intro.mk.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
p : α → Prop
x : F α
a : (P F).A
f : PFunctor.B (P F) a → α
h₀ : abs { fst := a, snd := f } = x
h₁ : ∀ (i : PFunctor.B (P F) { fst := a, snd := f }.fst), p (Sigma.snd { fst := a, snd := f } i)
⊢ Liftp p x
dsimp at *
case mpr.intro.mk.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
p : α → Prop
x : F α
a : (P F).A
f : PFunctor.B (P F) a → α
h₀ : abs { fst := a, snd := f } = x
h₁ : ∀ (i : PFunctor.B (P F) a), p (f i)
⊢ Subtype.val <$> abs { fst := a, snd := fun i => { val := f i, property := (_ : p (f i)) } } = x
case mpr.intro.mk.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
p : α → Prop
x : F α
a : (P F).A
f : PFunctor.B (P F) a → α
h₀ : abs { fst := a, snd := f } = x
h₁ : ∀ (i : PFunctor.B (P F) a), p (f i)
⊢ Liftp p x
use abs ⟨a, fun i => ⟨f i, h₁ i⟩⟩
case mpr.intro.mk.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
p : α → Prop
x : F α
a : (P F).A
f : PFunctor.B (P F) a → α
h₀ : abs { fst := a, snd := f } = x
h₁ : ∀ (i : PFunctor.B (P F) a), p (f i)
⊢ abs (Subtype.val <$> { fst := a, snd := fun i => { val := f i, property := (_ : p (f i)) } }) =
    abs { fst := a, snd := f }
case mpr.intro.mk.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
p : α → Prop
x : F α
a : (P F).A
f : PFunctor.B (P F) a → α
h₀ : abs { fst := a, snd := f } = x
h₁ : ∀ (i : PFunctor.B (P F) a), p (f i)
⊢ Subtype.val <$> abs { fst := a, snd := fun i => { val := f i, property := (_ : p (f i)) } } = x
rw [← abs_map, ← h₀]
no goals
case mpr.intro.mk.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
p : α → Prop
x : F α
a : (P F).A
f : PFunctor.B (P F) a → α
h₀ : abs { fst := a, snd := f } = x
h₁ : ∀ (i : PFunctor.B (P F) a), p (f i)
⊢ abs (Subtype.val <$> { fst := a, snd := fun i => { val := f i, property := (_ : p (f i)) } }) =
    abs { fst := a, snd := f }
rfl
case mp.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
⊢ ∃ u, abs u = x ∧ ∀ (i : PFunctor.B (P F) u.fst), p (Sigma.snd u i)
case mp
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
p : α → Prop
x : F α
⊢ Liftp p x → ∃ u, abs u = x ∧ ∀ (i : PFunctor.B (P F) u.fst), p (Sigma.snd u i)
rintro ⟨y, hy⟩
case mp.intro.mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
a : (P F).A
f : PFunctor.B (P F) a → Subtype p
h : repr y = { fst := a, snd := f }
⊢ ∃ u, abs u = x ∧ ∀ (i : PFunctor.B (P F) u.fst), p (Sigma.snd u i)
case mp.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
⊢ ∃ u, abs u = x ∧ ∀ (i : PFunctor.B (P F) u.fst), p (Sigma.snd u i)
cases' h : repr y with a f
case mp.intro.mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
a : (P F).A
f : PFunctor.B (P F) a → Subtype p
h : repr y = { fst := a, snd := f }
⊢ abs { fst := a, snd := fun i => ↑(f i) } = x ∧
    ∀ (i : PFunctor.B (P F) { fst := a, snd := fun i => ↑(f i) }.fst),
      p (Sigma.snd { fst := a, snd := fun i => ↑(f i) } i)
case mp.intro.mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
a : (P F).A
f : PFunctor.B (P F) a → Subtype p
h : repr y = { fst := a, snd := f }
⊢ ∃ u, abs u = x ∧ ∀ (i : PFunctor.B (P F) u.fst), p (Sigma.snd u i)
use ⟨a, fun i => (f i).val⟩
case mp.intro.mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
a : (P F).A
f : PFunctor.B (P F) a → Subtype p
h : repr y = { fst := a, snd := f }
⊢ abs { fst := a, snd := fun i => ↑(f i) } = x ∧ ∀ (i : PFunctor.B (P F) a), p ↑(f i)
case mp.intro.mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
a : (P F).A
f : PFunctor.B (P F) a → Subtype p
h : repr y = { fst := a, snd := f }
⊢ abs { fst := a, snd := fun i => ↑(f i) } = x ∧
    ∀ (i : PFunctor.B (P F) { fst := a, snd := fun i => ↑(f i) }.fst),
      p (Sigma.snd { fst := a, snd := fun i => ↑(f i) } i)
dsimp
case mp.intro.mk.left
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
a : (P F).A
f : PFunctor.B (P F) a → Subtype p
h : repr y = { fst := a, snd := f }
⊢ abs { fst := a, snd := fun i => ↑(f i) } = x

case mp.intro.mk.right
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
a : (P F).A
f : PFunctor.B (P F) a → Subtype p
h : repr y = { fst := a, snd := f }
⊢ ∀ (i : PFunctor.B (P F) a), p ↑(f i)
case mp.intro.mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
a : (P F).A
f : PFunctor.B (P F) a → Subtype p
h : repr y = { fst := a, snd := f }
⊢ abs { fst := a, snd := fun i => ↑(f i) } = x ∧ ∀ (i : PFunctor.B (P F) a), p ↑(f i)
constructor
case mp.intro.mk.right
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
a : (P F).A
f : PFunctor.B (P F) a → Subtype p
h : repr y = { fst := a, snd := f }
i : PFunctor.B (P F) a
⊢ p ↑(f i)
case mp.intro.mk.right
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
a : (P F).A
f : PFunctor.B (P F) a → Subtype p
h : repr y = { fst := a, snd := f }
⊢ ∀ (i : PFunctor.B (P F) a), p ↑(f i)
intro i
no goals
case mp.intro.mk.right
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
a : (P F).A
f : PFunctor.B (P F) a → Subtype p
h : repr y = { fst := a, snd := f }
i : PFunctor.B (P F) a
⊢ p ↑(f i)
apply (f i).property
case mp.intro.mk.left
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
a : (P F).A
f : PFunctor.B (P F) a → Subtype p
h : repr y = { fst := a, snd := f }
⊢ abs { fst := a, snd := fun i => ↑(f i) } = abs (Subtype.val <$> { fst := a, snd := f })
case mp.intro.mk.left
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
a : (P F).A
f : PFunctor.B (P F) a → Subtype p
h : repr y = { fst := a, snd := f }
⊢ abs { fst := a, snd := fun i => ↑(f i) } = x
rw [← hy, ← abs_repr y, h, ← abs_map]
no goals
case mp.intro.mk.left
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
a : (P F).A
f : PFunctor.B (P F) a → Subtype p
h : repr y = { fst := a, snd := f }
⊢ abs { fst := a, snd := fun i => ↑(f i) } = abs (Subtype.val <$> { fst := a, snd := f })
rfl