n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β : Type u
pp : β → Prop
rr : β → β → Prop
x y : F (α ::: β)
⊢ (∃ u, (fun i t => (↑t).fst) <$$> u = x ∧ (fun i t => (↑t).snd) <$$> u = y) ↔
    ∃ u, (fun i t => (↑t).fst) <$$> u = x ∧ (fun i t => (↑t).snd) <$$> u = y
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β : Type u
pp : β → Prop
rr : β → β → Prop
x y : F (α ::: β)
⊢ LiftR' (RelLast' α rr) x y ↔ LiftR (fun {i} => RelLast α rr) x y
dsimp only [LiftR, LiftR']
case h₀
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β : Type u
pp : β → Prop
rr : β → β → Prop
x y : F (α ::: β)
⊢ MvFunctor.f' rr n α ⊚ MvFunctor.g' rr n α = TypeVec.id

case h₁
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β : Type u
pp : β → Prop
rr : β → β → Prop
x y : F (α ::: β)
⊢ ∀ (u : F fun i => { p_1 // ofRepeat (RelLast' α rr i (prod.mk i p_1.fst p_1.snd)) }),
    (fun i t => (↑t).fst) <$$> u = x ∧ (fun i t => (↑t).snd) <$$> u = y ↔
      (fun i t => (↑t).fst) <$$> MvFunctor.f' rr n α <$$> u = x ∧
        (fun i t => (↑t).snd) <$$> MvFunctor.f' rr n α <$$> u = y
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β : Type u
pp : β → Prop
rr : β → β → Prop
x y : F (α ::: β)
⊢ (∃ u, (fun i t => (↑t).fst) <$$> u = x ∧ (fun i t => (↑t).snd) <$$> u = y) ↔
    ∃ u, (fun i t => (↑t).fst) <$$> u = x ∧ (fun i t => (↑t).snd) <$$> u = y
apply exists_iff_exists_of_mono F (f' rr _ _) (g' rr _ _)
case h₀.a.h.mk
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β : Type u
pp : β → Prop
rr : β → β → Prop
x✝ y : F (α ::: β)
i : Fin2 (n + 1)
x : (α ::: β) i × (α ::: β) i
property✝ : RelLast α rr x.fst x.snd
⊢ (MvFunctor.f' rr n α ⊚ MvFunctor.g' rr n α) i { val := x, property := property✝ } =
    TypeVec.id i { val := x, property := property✝ }
case h₀
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β : Type u
pp : β → Prop
rr : β → β → Prop
x y : F (α ::: β)
⊢ MvFunctor.f' rr n α ⊚ MvFunctor.g' rr n α = TypeVec.id
ext (i⟨x, _⟩) : 2
no goals
case h₀.a.h.mk
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β : Type u
pp : β → Prop
rr : β → β → Prop
x✝ y : F (α ::: β)
i : Fin2 (n + 1)
x : (α ::: β) i × (α ::: β) i
property✝ : RelLast α rr x.fst x.snd
⊢ (MvFunctor.f' rr n α ⊚ MvFunctor.g' rr n α) i { val := x, property := property✝ } =
    TypeVec.id i { val := x, property := property✝ }
cases i <;> rfl
case h₁
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β : Type u
pp : β → Prop
rr : β → β → Prop
x y : F (α ::: β)
u✝ : F fun i => { p_1 // ofRepeat (RelLast' α rr i (prod.mk i p_1.fst p_1.snd)) }
⊢ (fun i t => (↑t).fst) <$$> u✝ = x ∧ (fun i t => (↑t).snd) <$$> u✝ = y ↔
    (fun i t => (↑t).fst) <$$> MvFunctor.f' rr n α <$$> u✝ = x ∧
      (fun i t => (↑t).snd) <$$> MvFunctor.f' rr n α <$$> u✝ = y
case h₁
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β : Type u
pp : β → Prop
rr : β → β → Prop
x y : F (α ::: β)
⊢ ∀ (u : F fun i => { p_1 // ofRepeat (RelLast' α rr i (prod.mk i p_1.fst p_1.snd)) }),
    (fun i t => (↑t).fst) <$$> u = x ∧ (fun i t => (↑t).snd) <$$> u = y ↔
      (fun i t => (↑t).fst) <$$> MvFunctor.f' rr n α <$$> u = x ∧
        (fun i t => (↑t).snd) <$$> MvFunctor.f' rr n α <$$> u = y
intros
case h₁
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β : Type u
pp : β → Prop
rr : β → β → Prop
x y : F (α ::: β)
u✝ : F fun i => { p_1 // ofRepeat (RelLast' α rr i (prod.mk i p_1.fst p_1.snd)) }
⊢ ((fun i t => (↑t).fst) = fun i x => (↑(MvFunctor.f' rr n α i x)).fst) ∧
    (fun i t => (↑t).snd) = fun i x => (↑(MvFunctor.f' rr n α i x)).snd
case h₁
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β : Type u
pp : β → Prop
rr : β → β → Prop
x y : F (α ::: β)
u✝ : F fun i => { p_1 // ofRepeat (RelLast' α rr i (prod.mk i p_1.fst p_1.snd)) }
⊢ (fun i t => (↑t).fst) <$$> u✝ = x ∧ (fun i t => (↑t).snd) <$$> u✝ = y ↔
    (fun i x => (↑(MvFunctor.f' rr n α i x)).fst) <$$> u✝ = x ∧
      (fun i x => (↑(MvFunctor.f' rr n α i x)).snd) <$$> u✝ = y
suffices  (fun i t => t.val.fst) = ((fun i x => (MvFunctor.f' rr n α i x).val.fst))
        ∧ (fun i t => t.val.snd) = ((fun i x => (MvFunctor.f' rr n α i x).val.snd))
by  rcases this with ⟨left, right⟩
    rw[left, right];
no goals
case h₁
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β : Type u
pp : β → Prop
rr : β → β → Prop
x y : F (α ::: β)
u✝ : F fun i => { p_1 // ofRepeat (RelLast' α rr i (prod.mk i p_1.fst p_1.snd)) }
⊢ ((fun i t => (↑t).fst) = fun i x => (↑(MvFunctor.f' rr n α i x)).fst) ∧
    (fun i t => (↑t).snd) = fun i x => (↑(MvFunctor.f' rr n α i x)).snd
constructor <;> ext (i⟨x, _⟩) <;> cases i <;> rfl
case intro
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β : Type u
pp : β → Prop
rr : β → β → Prop
x y : F (α ::: β)
u✝ : F fun i => { p_1 // ofRepeat (RelLast' α rr i (prod.mk i p_1.fst p_1.snd)) }
left : (fun i t => (↑t).fst) = fun i x => (↑(MvFunctor.f' rr n α i x)).fst
right : (fun i t => (↑t).snd) = fun i x => (↑(MvFunctor.f' rr n α i x)).snd
⊢ (fun i t => (↑t).fst) <$$> u✝ = x ∧ (fun i t => (↑t).snd) <$$> u✝ = y ↔
    (fun i x => (↑(MvFunctor.f' rr n α i x)).fst) <$$> u✝ = x ∧
      (fun i x => (↑(MvFunctor.f' rr n α i x)).snd) <$$> u✝ = y
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β : Type u
pp : β → Prop
rr : β → β → Prop
x y : F (α ::: β)
u✝ : F fun i => { p_1 // ofRepeat (RelLast' α rr i (prod.mk i p_1.fst p_1.snd)) }
this :
  ((fun i t => (↑t).fst) = fun i x => (↑(MvFunctor.f' rr n α i x)).fst) ∧
    (fun i t => (↑t).snd) = fun i x => (↑(MvFunctor.f' rr n α i x)).snd
⊢ (fun i t => (↑t).fst) <$$> u✝ = x ∧ (fun i t => (↑t).snd) <$$> u✝ = y ↔
    (fun i x => (↑(MvFunctor.f' rr n α i x)).fst) <$$> u✝ = x ∧
      (fun i x => (↑(MvFunctor.f' rr n α i x)).snd) <$$> u✝ = y
rcases this with ⟨left, right⟩
no goals
case intro
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β : Type u
pp : β → Prop
rr : β → β → Prop
x y : F (α ::: β)
u✝ : F fun i => { p_1 // ofRepeat (RelLast' α rr i (prod.mk i p_1.fst p_1.snd)) }
left : (fun i t => (↑t).fst) = fun i x => (↑(MvFunctor.f' rr n α i x)).fst
right : (fun i t => (↑t).snd) = fun i x => (↑(MvFunctor.f' rr n α i x)).snd
⊢ (fun i t => (↑t).fst) <$$> u✝ = x ∧ (fun i t => (↑t).snd) <$$> u✝ = y ↔
    (fun i x => (↑(MvFunctor.f' rr n α i x)).fst) <$$> u✝ = x ∧
      (fun i x => (↑(MvFunctor.f' rr n α i x)).snd) <$$> u✝ = y
rw[left, right]