case mp
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : Obj P α
⊢ LiftR r x y →
    ∃ a f₀ f₁,
      x = { fst := a, snd := f₀ } ∧ y = { fst := a, snd := f₁ } ∧ ∀ (i : Fin2 n) (j : B P a i), r (f₀ i j) (f₁ i j)

case mpr
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : Obj P α
⊢ (∃ a f₀ f₁,
      x = { fst := a, snd := f₀ } ∧ y = { fst := a, snd := f₁ } ∧ ∀ (i : Fin2 n) (j : B P a i), r (f₀ i j) (f₁ i j)) →
    LiftR r x y
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : Obj P α
⊢ LiftR r x y ↔
    ∃ a f₀ f₁,
      x = { fst := a, snd := f₀ } ∧ y = { fst := a, snd := f₁ } ∧ ∀ (i : Fin2 n) (j : B P a i), r (f₀ i j) (f₁ i j)
constructor
case mpr.intro.intro.intro.intro.intro
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → 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 : Fin2 n) (j : B P a i), r (f₀ i j) (f₁ i j)
⊢ LiftR r x y
case mpr
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : Obj P α
⊢ (∃ a f₀ f₁,
      x = { fst := a, snd := f₀ } ∧ y = { fst := a, snd := f₁ } ∧ ∀ (i : Fin2 n) (j : B P a i), r (f₀ i j) (f₁ i j)) →
    LiftR r x y
rintro ⟨a, f₀, f₁, xeq, yeq, h⟩
case mpr.intro.intro.intro.intro.intro
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → 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 : Fin2 n) (j : B P a i), r (f₀ i j) (f₁ i j)
⊢ (fun i t => (↑t).fst) <$$>
        { fst := a, snd := fun i j => { val := (f₀ i j, f₁ i j), property := (_ : r (f₀ i j) (f₁ i j)) } } =
      x ∧
    (fun i t => (↑t).snd) <$$>
        { fst := a, snd := fun i j => { val := (f₀ i j, f₁ i j), property := (_ : r (f₀ i j) (f₁ i j)) } } =
      y
case mpr.intro.intro.intro.intro.intro
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → 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 : Fin2 n) (j : B P a i), r (f₀ i j) (f₁ i j)
⊢ LiftR r x y
use ⟨a, fun i j => ⟨(f₀ i j, f₁ i j), h i j⟩⟩
case mpr.intro.intro.intro.intro.intro
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → 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 : Fin2 n) (j : B P a i), r (f₀ i j) (f₁ i j)
⊢ (fun i t => (↑t).fst) <$$>
        { fst := a, snd := fun i j => { val := (f₀ i j, f₁ i j), property := (_ : r (f₀ i j) (f₁ i j)) } } =
      x ∧
    (fun i t => (↑t).snd) <$$>
        { fst := a, snd := fun i j => { val := (f₀ i j, f₁ i j), property := (_ : r (f₀ i j) (f₁ i j)) } } =
      y
case mpr.intro.intro.intro.intro.intro
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → 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 : Fin2 n) (j : B P a i), r (f₀ i j) (f₁ i j)
⊢ (fun i t => (↑t).fst) <$$>
        { fst := a, snd := fun i j => { val := (f₀ i j, f₁ i j), property := (_ : r (f₀ i j) (f₁ i j)) } } =
      x ∧
    (fun i t => (↑t).snd) <$$>
        { fst := a, snd := fun i j => { val := (f₀ i j, f₁ i j), property := (_ : r (f₀ i j) (f₁ i j)) } } =
      y
dsimp
case mpr.intro.intro.intro.intro.intro.left
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → 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 : Fin2 n) (j : B P a i), r (f₀ i j) (f₁ i j)
⊢ (fun i t => (↑t).fst) <$$>
      { fst := a, snd := fun i j => { val := (f₀ i j, f₁ i j), property := (_ : r (f₀ i j) (f₁ i j)) } } =
    x

case mpr.intro.intro.intro.intro.intro.right
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → 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 : Fin2 n) (j : B P a i), r (f₀ i j) (f₁ i j)
⊢ (fun i t => (↑t).snd) <$$>
      { fst := a, snd := fun i j => { val := (f₀ i j, f₁ i j), property := (_ : r (f₀ i j) (f₁ i j)) } } =
    y
case mpr.intro.intro.intro.intro.intro
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → 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 : Fin2 n) (j : B P a i), r (f₀ i j) (f₁ i j)
⊢ (fun i t => (↑t).fst) <$$>
        { fst := a, snd := fun i j => { val := (f₀ i j, f₁ i j), property := (_ : r (f₀ i j) (f₁ i j)) } } =
      x ∧
    (fun i t => (↑t).snd) <$$>
        { fst := a, snd := fun i j => { val := (f₀ i j, f₁ i j), property := (_ : r (f₀ i j) (f₁ i j)) } } =
      y
constructor
case mpr.intro.intro.intro.intro.intro.right
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → 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 : Fin2 n) (j : B P a i), r (f₀ i j) (f₁ i j)
⊢ (fun i t => (↑t).snd) <$$>
      { fst := a, snd := fun i j => { val := (f₀ i j, f₁ i j), property := (_ : r (f₀ i j) (f₁ i j)) } } =
    { fst := a, snd := f₁ }
case mpr.intro.intro.intro.intro.intro.right
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → 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 : Fin2 n) (j : B P a i), r (f₀ i j) (f₁ i j)
⊢ (fun i t => (↑t).snd) <$$>
      { fst := a, snd := fun i j => { val := (f₀ i j, f₁ i j), property := (_ : r (f₀ i j) (f₁ i j)) } } =
    y
rw [yeq]
no goals
case mpr.intro.intro.intro.intro.intro.right
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → 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 : Fin2 n) (j : B P a i), r (f₀ i j) (f₁ i j)
⊢ (fun i t => (↑t).snd) <$$>
      { fst := a, snd := fun i j => { val := (f₀ i j, f₁ i j), property := (_ : r (f₀ i j) (f₁ i j)) } } =
    { fst := a, snd := f₁ }
rfl
case mp.intro.intro
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : Obj P α
u : Obj P fun i => { p // r p.fst p.snd }
xeq : (fun i t => (↑t).fst) <$$> u = x
yeq : (fun i t => (↑t).snd) <$$> u = y
⊢ ∃ a f₀ f₁,
    x = { fst := a, snd := f₀ } ∧ y = { fst := a, snd := f₁ } ∧ ∀ (i : Fin2 n) (j : B P a i), r (f₀ i j) (f₁ i j)
case mp
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : Obj P α
⊢ LiftR r x y →
    ∃ a f₀ f₁,
      x = { fst := a, snd := f₀ } ∧ y = { fst := a, snd := f₁ } ∧ ∀ (i : Fin2 n) (j : B P a i), r (f₀ i j) (f₁ i j)
rintro ⟨u, xeq, yeq⟩
case mp.intro.intro.mk
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : Obj P α
u : Obj P fun i => { p // r p.fst p.snd }
xeq : (fun i t => (↑t).fst) <$$> u = x
yeq : (fun i t => (↑t).snd) <$$> u = y
a : P.A
f : B P a ⟹ fun i => { 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 : Fin2 n) (j : B P a i), r (f₀ i j) (f₁ i j)
case mp.intro.intro
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : Obj P α
u : Obj P fun i => { p // r p.fst p.snd }
xeq : (fun i t => (↑t).fst) <$$> u = x
yeq : (fun i t => (↑t).snd) <$$> u = y
⊢ ∃ a f₀ f₁,
    x = { fst := a, snd := f₀ } ∧ y = { fst := a, snd := f₁ } ∧ ∀ (i : Fin2 n) (j : B P a i), r (f₀ i j) (f₁ i j)
cases' h : u with a f
case mp.intro.intro.mk
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : Obj P α
u : Obj P fun i => { p // r p.fst p.snd }
xeq : (fun i t => (↑t).fst) <$$> u = x
yeq : (fun i t => (↑t).snd) <$$> u = y
a : P.A
f : B P a ⟹ fun i => { p // r p.fst p.snd }
h : u = { fst := a, snd := f }
⊢ x = { fst := a, snd := fun i j => (↑(f i j)).fst } ∧
    y = { fst := a, snd := fun i j => (↑(f i j)).snd } ∧
      ∀ (i : Fin2 n) (j : B P a i), r ((fun i j => (↑(f i j)).fst) i j) ((fun i j => (↑(f i j)).snd) i j)
case mp.intro.intro.mk
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : Obj P α
u : Obj P fun i => { p // r p.fst p.snd }
xeq : (fun i t => (↑t).fst) <$$> u = x
yeq : (fun i t => (↑t).snd) <$$> u = y
a : P.A
f : B P a ⟹ fun i => { 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 : Fin2 n) (j : B P a i), r (f₀ i j) (f₁ i j)
use a, fun i j => (f i j).val.fst, fun i j => (f i j).val.snd
case mp.intro.intro.mk.left
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : Obj P α
u : Obj P fun i => { p // r p.fst p.snd }
xeq : (fun i t => (↑t).fst) <$$> u = x
yeq : (fun i t => (↑t).snd) <$$> u = y
a : P.A
f : B P a ⟹ fun i => { p // r p.fst p.snd }
h : u = { fst := a, snd := f }
⊢ x = { fst := a, snd := fun i j => (↑(f i j)).fst }

case mp.intro.intro.mk.right
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : Obj P α
u : Obj P fun i => { p // r p.fst p.snd }
xeq : (fun i t => (↑t).fst) <$$> u = x
yeq : (fun i t => (↑t).snd) <$$> u = y
a : P.A
f : B P a ⟹ fun i => { p // r p.fst p.snd }
h : u = { fst := a, snd := f }
⊢ y = { fst := a, snd := fun i j => (↑(f i j)).snd } ∧
    ∀ (i : Fin2 n) (j : B P a i), r ((fun i j => (↑(f i j)).fst) i j) ((fun i j => (↑(f i j)).snd) i j)
case mp.intro.intro.mk
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : Obj P α
u : Obj P fun i => { p // r p.fst p.snd }
xeq : (fun i t => (↑t).fst) <$$> u = x
yeq : (fun i t => (↑t).snd) <$$> u = y
a : P.A
f : B P a ⟹ fun i => { p // r p.fst p.snd }
h : u = { fst := a, snd := f }
⊢ x = { fst := a, snd := fun i j => (↑(f i j)).fst } ∧
    y = { fst := a, snd := fun i j => (↑(f i j)).snd } ∧
      ∀ (i : Fin2 n) (j : B P a i), r ((fun i j => (↑(f i j)).fst) i j) ((fun i j => (↑(f i j)).snd) i j)
constructor
case mp.intro.intro.mk.right.left
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : Obj P α
u : Obj P fun i => { p // r p.fst p.snd }
xeq : (fun i t => (↑t).fst) <$$> u = x
yeq : (fun i t => (↑t).snd) <$$> u = y
a : P.A
f : B P a ⟹ fun i => { p // r p.fst p.snd }
h : u = { fst := a, snd := f }
⊢ y = { fst := a, snd := fun i j => (↑(f i j)).snd }

case mp.intro.intro.mk.right.right
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : Obj P α
u : Obj P fun i => { p // r p.fst p.snd }
xeq : (fun i t => (↑t).fst) <$$> u = x
yeq : (fun i t => (↑t).snd) <$$> u = y
a : P.A
f : B P a ⟹ fun i => { p // r p.fst p.snd }
h : u = { fst := a, snd := f }
⊢ ∀ (i : Fin2 n) (j : B P a i), r ((fun i j => (↑(f i j)).fst) i j) ((fun i j => (↑(f i j)).snd) i j)
case mp.intro.intro.mk.right
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : Obj P α
u : Obj P fun i => { p // r p.fst p.snd }
xeq : (fun i t => (↑t).fst) <$$> u = x
yeq : (fun i t => (↑t).snd) <$$> u = y
a : P.A
f : B P a ⟹ fun i => { p // r p.fst p.snd }
h : u = { fst := a, snd := f }
⊢ y = { fst := a, snd := fun i j => (↑(f i j)).snd } ∧
    ∀ (i : Fin2 n) (j : B P a i), r ((fun i j => (↑(f i j)).fst) i j) ((fun i j => (↑(f i j)).snd) i j)
constructor
case mp.intro.intro.mk.right.right
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : Obj P α
u : Obj P fun i => { p // r p.fst p.snd }
xeq : (fun i t => (↑t).fst) <$$> u = x
yeq : (fun i t => (↑t).snd) <$$> u = y
a : P.A
f : B P a ⟹ fun i => { p // r p.fst p.snd }
h : u = { fst := a, snd := f }
i : Fin2 n
j : B P a i
⊢ r ((fun i j => (↑(f i j)).fst) i j) ((fun i j => (↑(f i j)).snd) i j)
case mp.intro.intro.mk.right.right
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : Obj P α
u : Obj P fun i => { p // r p.fst p.snd }
xeq : (fun i t => (↑t).fst) <$$> u = x
yeq : (fun i t => (↑t).snd) <$$> u = y
a : P.A
f : B P a ⟹ fun i => { p // r p.fst p.snd }
h : u = { fst := a, snd := f }
⊢ ∀ (i : Fin2 n) (j : B P a i), r ((fun i j => (↑(f i j)).fst) i j) ((fun i j => (↑(f i j)).snd) i j)
intro i j
no goals
case mp.intro.intro.mk.right.right
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : Obj P α
u : Obj P fun i => { p // r p.fst p.snd }
xeq : (fun i t => (↑t).fst) <$$> u = x
yeq : (fun i t => (↑t).snd) <$$> u = y
a : P.A
f : B P a ⟹ fun i => { p // r p.fst p.snd }
h : u = { fst := a, snd := f }
i : Fin2 n
j : B P a i
⊢ r ((fun i j => (↑(f i j)).fst) i j) ((fun i j => (↑(f i j)).snd) i j)
exact (f i j).property
case mp.intro.intro.mk.left
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : Obj P α
u : Obj P fun i => { p // r p.fst p.snd }
xeq : (fun i t => (↑t).fst) <$$> u = x
yeq : (fun i t => (↑t).snd) <$$> u = y
a : P.A
f : B P a ⟹ fun i => { p // r p.fst p.snd }
h : u = { fst := a, snd := f }
⊢ (fun i t => (↑t).fst) <$$> { fst := a, snd := f } = { fst := a, snd := fun i j => (↑(f i j)).fst }
case mp.intro.intro.mk.left
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : Obj P α
u : Obj P fun i => { p // r p.fst p.snd }
xeq : (fun i t => (↑t).fst) <$$> u = x
yeq : (fun i t => (↑t).snd) <$$> u = y
a : P.A
f : B P a ⟹ fun i => { p // r p.fst p.snd }
h : u = { fst := a, snd := f }
⊢ x = { fst := a, snd := fun i j => (↑(f i j)).fst }
rw [← xeq, h]
no goals
case mp.intro.intro.mk.left
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : Obj P α
u : Obj P fun i => { p // r p.fst p.snd }
xeq : (fun i t => (↑t).fst) <$$> u = x
yeq : (fun i t => (↑t).snd) <$$> u = y
a : P.A
f : B P a ⟹ fun i => { p // r p.fst p.snd }
h : u = { fst := a, snd := f }
⊢ (fun i t => (↑t).fst) <$$> { fst := a, snd := f } = { fst := a, snd := fun i j => (↑(f i j)).fst }
rfl
case mp.intro.intro.mk.right.left
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : Obj P α
u : Obj P fun i => { p // r p.fst p.snd }
xeq : (fun i t => (↑t).fst) <$$> u = x
yeq : (fun i t => (↑t).snd) <$$> u = y
a : P.A
f : B P a ⟹ fun i => { p // r p.fst p.snd }
h : u = { fst := a, snd := f }
⊢ (fun i t => (↑t).snd) <$$> { fst := a, snd := f } = { fst := a, snd := fun i j => (↑(f i j)).snd }
case mp.intro.intro.mk.right.left
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : Obj P α
u : Obj P fun i => { p // r p.fst p.snd }
xeq : (fun i t => (↑t).fst) <$$> u = x
yeq : (fun i t => (↑t).snd) <$$> u = y
a : P.A
f : B P a ⟹ fun i => { p // r p.fst p.snd }
h : u = { fst := a, snd := f }
⊢ y = { fst := a, snd := fun i j => (↑(f i j)).snd }
rw [← yeq, h]
no goals
case mp.intro.intro.mk.right.left
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : Obj P α
u : Obj P fun i => { p // r p.fst p.snd }
xeq : (fun i t => (↑t).fst) <$$> u = x
yeq : (fun i t => (↑t).snd) <$$> u = y
a : P.A
f : B P a ⟹ fun i => { p // r p.fst p.snd }
h : u = { fst := a, snd := f }
⊢ (fun i t => (↑t).snd) <$$> { fst := a, snd := f } = { fst := a, snd := fun i j => (↑(f i j)).snd }
rfl
case mpr.intro.intro.intro.intro.intro.left
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → 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 : Fin2 n) (j : B P a i), r (f₀ i j) (f₁ i j)
⊢ (fun i t => (↑t).fst) <$$>
      { fst := a, snd := fun i j => { val := (f₀ i j, f₁ i j), property := (_ : r (f₀ i j) (f₁ i j)) } } =
    { fst := a, snd := f₀ }
case mpr.intro.intro.intro.intro.intro.left
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → 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 : Fin2 n) (j : B P a i), r (f₀ i j) (f₁ i j)
⊢ (fun i t => (↑t).fst) <$$>
      { fst := a, snd := fun i j => { val := (f₀ i j, f₁ i j), property := (_ : r (f₀ i j) (f₁ i j)) } } =
    x
rw [xeq]
no goals
case mpr.intro.intro.intro.intro.intro.left
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → 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 : Fin2 n) (j : B P a i), r (f₀ i j) (f₁ i j)
⊢ (fun i t => (↑t).fst) <$$>
      { fst := a, snd := fun i j => { val := (f₀ i j, f₁ i j), property := (_ : r (f₀ i j) (f₁ i j)) } } =
    { fst := a, snd := f₀ }
rfl