case mp
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
r : α → α → Prop
x y : F α
⊢ Liftr r x y →
    ∃ a f₀ f₁,
      x = abs { fst := a, snd := f₀ } ∧ y = abs { fst := a, snd := f₁ } ∧ ∀ (i : PFunctor.B (P F) a), r (f₀ i) (f₁ i)

case mpr
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
r : α → α → Prop
x y : F α
⊢ (∃ a f₀ f₁,
      x = abs { fst := a, snd := f₀ } ∧ y = abs { fst := a, snd := f₁ } ∧ ∀ (i : PFunctor.B (P F) a), r (f₀ i) (f₁ i)) →
    Liftr r x y
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
r : α → α → Prop
x y : F α
⊢ Liftr r x y ↔
    ∃ a f₀ f₁,
      x = abs { fst := a, snd := f₀ } ∧ y = abs { fst := a, snd := f₁ } ∧ ∀ (i : PFunctor.B (P F) a), r (f₀ i) (f₁ i)
constructor
case mpr.intro.intro.intro.intro.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
r : α → α → Prop
x y : F α
a : (P F).A
f₀ f₁ : PFunctor.B (P F) a → α
xeq : x = abs { fst := a, snd := f₀ }
yeq : y = abs { fst := a, snd := f₁ }
h : ∀ (i : PFunctor.B (P F) a), r (f₀ i) (f₁ i)
⊢ Liftr r x y
case mpr
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
r : α → α → Prop
x y : F α
⊢ (∃ a f₀ f₁,
      x = abs { fst := a, snd := f₀ } ∧ y = abs { fst := a, snd := f₁ } ∧ ∀ (i : PFunctor.B (P F) a), r (f₀ i) (f₁ i)) →
    Liftr r x y
rintro ⟨a, f₀, f₁, xeq, yeq, h⟩
case mpr.intro.intro.intro.intro.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
r : α → α → Prop
x y : F α
a : (P F).A
f₀ f₁ : PFunctor.B (P F) a → α
xeq : x = abs { fst := a, snd := f₀ }
yeq : y = abs { fst := a, snd := f₁ }
h : ∀ (i : PFunctor.B (P F) a), r (f₀ i) (f₁ i)
⊢ (fun t => (↑t).fst) <$> abs { fst := a, snd := fun i => { val := (f₀ i, f₁ i), property := (_ : r (f₀ i) (f₁ i)) } } =
      x ∧
    (fun t => (↑t).snd) <$>
        abs { fst := a, snd := fun i => { val := (f₀ i, f₁ i), property := (_ : r (f₀ i) (f₁ i)) } } =
      y
case mpr.intro.intro.intro.intro.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
r : α → α → Prop
x y : F α
a : (P F).A
f₀ f₁ : PFunctor.B (P F) a → α
xeq : x = abs { fst := a, snd := f₀ }
yeq : y = abs { fst := a, snd := f₁ }
h : ∀ (i : PFunctor.B (P F) a), r (f₀ i) (f₁ i)
⊢ Liftr r x y
use abs ⟨a, fun i => ⟨(f₀ i, f₁ i), h i⟩⟩
case mpr.intro.intro.intro.intro.intro.left
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
r : α → α → Prop
x y : F α
a : (P F).A
f₀ f₁ : PFunctor.B (P F) a → α
xeq : x = abs { fst := a, snd := f₀ }
yeq : y = abs { fst := a, snd := f₁ }
h : ∀ (i : PFunctor.B (P F) a), r (f₀ i) (f₁ i)
⊢ (fun t => (↑t).fst) <$> abs { fst := a, snd := fun i => { val := (f₀ i, f₁ i), property := (_ : r (f₀ i) (f₁ i)) } } =
    x

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

case mp.intro.intro.mk.right
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
r : α → α → Prop
x y : F α
u : F { p // r p.fst p.snd }
xeq : (fun t => (↑t).fst) <$> u = x
yeq : (fun t => (↑t).snd) <$> u = y
a : (P F).A
f : PFunctor.B (P F) a → { p // r p.fst p.snd }
h : repr u = { fst := a, snd := f }
⊢ y = abs { fst := a, snd := fun i => (↑(f i)).snd } ∧
    ∀ (i : PFunctor.B (P F) a), r ((fun i => (↑(f i)).fst) i) ((fun i => (↑(f i)).snd) i)
case mp.intro.intro.mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
r : α → α → Prop
x y : F α
u : F { p // r p.fst p.snd }
xeq : (fun t => (↑t).fst) <$> u = x
yeq : (fun t => (↑t).snd) <$> u = y
a : (P F).A
f : PFunctor.B (P F) a → { p // r p.fst p.snd }
h : repr u = { fst := a, snd := f }
⊢ x = abs { fst := a, snd := fun i => (↑(f i)).fst } ∧
    y = abs { fst := a, snd := fun i => (↑(f i)).snd } ∧
      ∀ (i : PFunctor.B (P F) a), r ((fun i => (↑(f i)).fst) i) ((fun i => (↑(f i)).snd) i)
constructor
case mp.intro.intro.mk.right.left
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
r : α → α → Prop
x y : F α
u : F { p // r p.fst p.snd }
xeq : (fun t => (↑t).fst) <$> u = x
yeq : (fun t => (↑t).snd) <$> u = y
a : (P F).A
f : PFunctor.B (P F) a → { p // r p.fst p.snd }
h : repr u = { fst := a, snd := f }
⊢ y = abs { fst := a, snd := fun i => (↑(f i)).snd }

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