n : ℕ
α β γ : TypeVec n
F : TypeVec n → Type v
inst✝¹ : MvFunctor F
P : α ⟹ TypeVec.repeat n Prop
R : α ⊗ α ⟹ TypeVec.repeat n Prop
inst✝ : LawfulMvFunctor F
x y : F α
⊢ ∀ (u : F fun i => { p // (fun i x y => ofRepeat (R i (prod.mk i x y))) i p.fst p.snd }),
    (fun i t => (↑t).fst) <$$> u = x ∧ (fun i t => (↑t).snd) <$$> u = y ↔
      (prod.fst ⊚ fun i x => prod.mk i (↑x).fst (↑x).snd) <$$> u = x ∧
        (prod.snd ⊚ fun i x => prod.mk i (↑x).fst (↑x).snd) <$$> u = y
n : ℕ
α β γ : TypeVec n
F : TypeVec n → Type v
inst✝¹ : MvFunctor F
P : α ⟹ TypeVec.repeat n Prop
R : α ⊗ α ⟹ TypeVec.repeat n Prop
inst✝ : LawfulMvFunctor F
x y : F α
⊢ ∀ (u : F fun i => { p // (fun i x y => ofRepeat (R i (prod.mk i x y))) i p.fst p.snd }),
    (fun i t => (↑t).fst) <$$> u = x ∧ (fun i t => (↑t).snd) <$$> u = y ↔
      (prod.fst ⊚ subtypeVal R) <$$> toSubtype' R <$$> u = x ∧ (prod.snd ⊚ subtypeVal R) <$$> toSubtype' R <$$> u = y
simp only [map_map, comp_assoc, subtypeVal_toSubtype']
no goals
n : ℕ
α β γ : TypeVec n
F : TypeVec n → Type v
inst✝¹ : MvFunctor F
P : α ⟹ TypeVec.repeat n Prop
R : α ⊗ α ⟹ TypeVec.repeat n Prop
inst✝ : LawfulMvFunctor F
x y : F α
⊢ ∀ (u : F fun i => { p // (fun i x y => ofRepeat (R i (prod.mk i x y))) i p.fst p.snd }),
    (fun i t => (↑t).fst) <$$> u = x ∧ (fun i t => (↑t).snd) <$$> u = y ↔
      (prod.fst ⊚ fun i x => prod.mk i (↑x).fst (↑x).snd) <$$> u = x ∧
        (prod.snd ⊚ fun i x => prod.mk i (↑x).fst (↑x).snd) <$$> u = y
simp [comp]