[GOAL]
n : ℕ
α β γ : TypeVec n
F : TypeVec n → Type v
inst✝¹ : MvFunctor F
P✝ : α ⟹ TypeVec.repeat n Prop
R : α ⊗ α ⟹ TypeVec.repeat n Prop
inst✝ : LawfulMvFunctor F
P : F α → Prop
q : F β → Prop
f : α ⟹ β
g : β ⟹ α
h₀ : f ⊚ g = TypeVec.id
h₁ : ∀ (u : F α), P u ↔ q (f <$$> u)
⊢ (∃ u, P u) ↔ ∃ u, q u
[PROOFSTEP]
constructor
[GOAL]
case mp
n : ℕ
α β γ : TypeVec n
F : TypeVec n → Type v
inst✝¹ : MvFunctor F
P✝ : α ⟹ TypeVec.repeat n Prop
R : α ⊗ α ⟹ TypeVec.repeat n Prop
inst✝ : LawfulMvFunctor F
P : F α → Prop
q : F β → Prop
f : α ⟹ β
g : β ⟹ α
h₀ : f ⊚ g = TypeVec.id
h₁ : ∀ (u : F α), P u ↔ q (f <$$> u)
⊢ (∃ u, P u) → ∃ u, q u
[PROOFSTEP]
rintro ⟨u, h₂⟩
[GOAL]
case mpr
n : ℕ
α β γ : TypeVec n
F : TypeVec n → Type v
inst✝¹ : MvFunctor F
P✝ : α ⟹ TypeVec.repeat n Prop
R : α ⊗ α ⟹ TypeVec.repeat n Prop
inst✝ : LawfulMvFunctor F
P : F α → Prop
q : F β → Prop
f : α ⟹ β
g : β ⟹ α
h₀ : f ⊚ g = TypeVec.id
h₁ : ∀ (u : F α), P u ↔ q (f <$$> u)
⊢ (∃ u, q u) → ∃ u, P u
[PROOFSTEP]
rintro ⟨u, h₂⟩
[GOAL]
case mp.intro
n : ℕ
α β γ : TypeVec n
F : TypeVec n → Type v
inst✝¹ : MvFunctor F
P✝ : α ⟹ TypeVec.repeat n Prop
R : α ⊗ α ⟹ TypeVec.repeat n Prop
inst✝ : LawfulMvFunctor F
P : F α → Prop
q : F β → Prop
f : α ⟹ β
g : β ⟹ α
h₀ : f ⊚ g = TypeVec.id
h₁ : ∀ (u : F α), P u ↔ q (f <$$> u)
u : F α
h₂ : P u
⊢ ∃ u, q u
[PROOFSTEP]
refine ⟨f <$$> u, ?_⟩
[GOAL]
case mp.intro
n : ℕ
α β γ : TypeVec n
F : TypeVec n → Type v
inst✝¹ : MvFunctor F
P✝ : α ⟹ TypeVec.repeat n Prop
R : α ⊗ α ⟹ TypeVec.repeat n Prop
inst✝ : LawfulMvFunctor F
P : F α → Prop
q : F β → Prop
f : α ⟹ β
g : β ⟹ α
h₀ : f ⊚ g = TypeVec.id
h₁ : ∀ (u : F α), P u ↔ q (f <$$> u)
u : F α
h₂ : P u
⊢ q (f <$$> u)
[PROOFSTEP]
apply (h₁ u).mp h₂
[GOAL]
case mpr.intro
n : ℕ
α β γ : TypeVec n
F : TypeVec n → Type v
inst✝¹ : MvFunctor F
P✝ : α ⟹ TypeVec.repeat n Prop
R : α ⊗ α ⟹ TypeVec.repeat n Prop
inst✝ : LawfulMvFunctor F
P : F α → Prop
q : F β → Prop
f : α ⟹ β
g : β ⟹ α
h₀ : f ⊚ g = TypeVec.id
h₁ : ∀ (u : F α), P u ↔ q (f <$$> u)
u : F β
h₂ : q u
⊢ ∃ u, P u
[PROOFSTEP]
refine ⟨g <$$> u, ?_⟩
[GOAL]
case mpr.intro
n : ℕ
α β γ : TypeVec n
F : TypeVec n → Type v
inst✝¹ : MvFunctor F
P✝ : α ⟹ TypeVec.repeat n Prop
R : α ⊗ α ⟹ TypeVec.repeat n Prop
inst✝ : LawfulMvFunctor F
P : F α → Prop
q : F β → Prop
f : α ⟹ β
g : β ⟹ α
h₀ : f ⊚ g = TypeVec.id
h₁ : ∀ (u : F α), P u ↔ q (f <$$> u)
u : F β
h₂ : q u
⊢ P (g <$$> u)
[PROOFSTEP]
apply (h₁ _).mpr _
[GOAL]
n : ℕ
α β γ : TypeVec n
F : TypeVec n → Type v
inst✝¹ : MvFunctor F
P✝ : α ⟹ TypeVec.repeat n Prop
R : α ⊗ α ⟹ TypeVec.repeat n Prop
inst✝ : LawfulMvFunctor F
P : F α → Prop
q : F β → Prop
f : α ⟹ β
g : β ⟹ α
h₀ : f ⊚ g = TypeVec.id
h₁ : ∀ (u : F α), P u ↔ q (f <$$> u)
u : F β
h₂ : q u
⊢ q (f <$$> g <$$> u)
[PROOFSTEP]
simp only [MvFunctor.map_map, h₀, LawfulMvFunctor.id_map, h₂]
[GOAL]
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 : F α
⊢ ∀ (u : F fun i => Subtype ((fun i x => ofRepeat (P i x)) i)),
    (fun i => Subtype.val) <$$> u = x ↔ subtypeVal P <$$> toSubtype P <$$> u = x
[PROOFSTEP]
simp [MvFunctor.map_map]
[GOAL]
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
[PROOFSTEP]
simp only [map_map, comp_assoc, subtypeVal_toSubtype']
[GOAL]
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
[PROOFSTEP]
simp [comp]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α✝ : TypeVec n
β : Type u
pp : β → Prop
x✝ : ℕ
α : TypeVec x✝
i : Fin2 x✝
x : (fun i => { p_1 // ofRepeat (PredLast' α pp i p_1) }) (Fin2.fs i)
⊢ ofRepeat (PredLast' α pp (Fin2.fs i) ↑x) = PredLast α pp ↑x
[PROOFSTEP]
simp only [PredLast]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α✝ : TypeVec n
β : Type u
pp : β → Prop
x✝ : ℕ
α : TypeVec x✝
i : Fin2 x✝
x : (fun i => { p_1 // ofRepeat (PredLast' α pp i p_1) }) (Fin2.fs i)
⊢ ofRepeat (PredLast' α pp (Fin2.fs i) ↑x) = True
[PROOFSTEP]
erw [const_iff_true]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α✝ : TypeVec n
β : Type u
pp : β → Prop
x✝ : ℕ
α : TypeVec x✝
i : Fin2 x✝
x : (fun i => { p_1 // PredLast α pp p_1 }) (Fin2.fs i)
⊢ PredLast α pp ↑x = ofRepeat (PredLast' α pp (Fin2.fs i) ↑x)
[PROOFSTEP]
simp only [PredLast]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α✝ : TypeVec n
β : Type u
pp : β → Prop
x✝ : ℕ
α : TypeVec x✝
i : Fin2 x✝
x : (fun i => { p_1 // PredLast α pp p_1 }) (Fin2.fs i)
⊢ True = ofRepeat (PredLast' α pp (Fin2.fs i) ↑x)
[PROOFSTEP]
erw [const_iff_true]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β✝ : Type u
pp : β✝ → Prop
β : Type u
P : β → Prop
x : F (α ::: β)
⊢ LiftP' (PredLast' α P) x ↔ LiftP (PredLast α P) x
[PROOFSTEP]
dsimp only [LiftP, LiftP']
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β✝ : Type u
pp : β✝ → Prop
β : Type u
P : β → Prop
x : F (α ::: β)
⊢ (∃ u, (fun i => Subtype.val) <$$> u = x) ↔ ∃ u, (fun i => Subtype.val) <$$> u = x
[PROOFSTEP]
apply exists_iff_exists_of_mono F (f _ n α) (g _ n α)
[GOAL]
case h₀
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β✝ : Type u
pp : β✝ → Prop
β : Type u
P : β → Prop
x : F (α ::: β)
⊢ MvFunctor.f P n α ⊚ MvFunctor.g P n α = TypeVec.id
[PROOFSTEP]
ext i ⟨x, _⟩
[GOAL]
case h₀.a.h.mk.a
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β✝ : Type u
pp : β✝ → Prop
β : Type u
P : β → Prop
x✝ : F (α ::: β)
i : Fin2 (n + 1)
x : (α ::: β) i
property✝ : PredLast α P x
⊢ ↑((MvFunctor.f P n α ⊚ MvFunctor.g P n α) i { val := x, property := property✝ }) =
    ↑(TypeVec.id i { val := x, property := property✝ })
[PROOFSTEP]
cases i
[GOAL]
case h₀.a.h.mk.a.fz
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β✝ : Type u
pp : β✝ → Prop
β : Type u
P : β → Prop
x✝ : F (α ::: β)
x : (α ::: β) Fin2.fz
property✝ : PredLast α P x
⊢ ↑((MvFunctor.f P n α ⊚ MvFunctor.g P n α) Fin2.fz { val := x, property := property✝ }) =
    ↑(TypeVec.id Fin2.fz { val := x, property := property✝ })
[PROOFSTEP]
rfl
[GOAL]
case h₀.a.h.mk.a.fs
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β✝ : Type u
pp : β✝ → Prop
β : Type u
P : β → Prop
x✝ : F (α ::: β)
a✝ : Fin2 (Nat.add n 0)
x : (α ::: β) (Fin2.fs a✝)
property✝ : PredLast α P x
⊢ ↑((MvFunctor.f P n α ⊚ MvFunctor.g P n α) (Fin2.fs a✝) { val := x, property := property✝ }) =
    ↑(TypeVec.id (Fin2.fs a✝) { val := x, property := property✝ })
[PROOFSTEP]
rfl
[GOAL]
case h₁
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β✝ : Type u
pp : β✝ → Prop
β : Type u
P : β → Prop
x : F (α ::: β)
⊢ ∀ (u : F fun i => { p_1 // ofRepeat (PredLast' α P i p_1) }),
    (fun i => Subtype.val) <$$> u = x ↔ (fun i => Subtype.val) <$$> MvFunctor.f P n α <$$> u = x
[PROOFSTEP]
intros
[GOAL]
case h₁
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β✝ : Type u
pp : β✝ → Prop
β : Type u
P : β → Prop
x : F (α ::: β)
u✝ : F fun i => { p_1 // ofRepeat (PredLast' α P i p_1) }
⊢ (fun i => Subtype.val) <$$> u✝ = x ↔ (fun i => Subtype.val) <$$> MvFunctor.f P n α <$$> u✝ = x
[PROOFSTEP]
rw [MvFunctor.map_map]
[GOAL]
case h₁
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β✝ : Type u
pp : β✝ → Prop
β : Type u
P : β → Prop
x : F (α ::: β)
u✝ : F fun i => { p_1 // ofRepeat (PredLast' α P i p_1) }
⊢ (fun i => Subtype.val) <$$> u✝ = x ↔ ((fun i => Subtype.val) ⊚ MvFunctor.f P n α) <$$> u✝ = x
[PROOFSTEP]
dsimp [(· ⊚ ·)]
[GOAL]
case h₁
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β✝ : Type u
pp : β✝ → Prop
β : Type u
P : β → Prop
x : F (α ::: β)
u✝ : F fun i => { p_1 // ofRepeat (PredLast' α P i p_1) }
⊢ (fun i => Subtype.val) <$$> u✝ = x ↔ (fun i x => ↑(MvFunctor.f P n α i x)) <$$> u✝ = x
[PROOFSTEP]
suffices (fun i => Subtype.val) = (fun i x => (MvFunctor.f P n α i x).val) by rw [this];
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β✝ : Type u
pp : β✝ → Prop
β : Type u
P : β → Prop
x : F (α ::: β)
u✝ : F fun i => { p_1 // ofRepeat (PredLast' α P i p_1) }
this : (fun i => Subtype.val) = fun i x => ↑(MvFunctor.f P n α i x)
⊢ (fun i => Subtype.val) <$$> u✝ = x ↔ (fun i x => ↑(MvFunctor.f P n α i x)) <$$> u✝ = x
[PROOFSTEP]
rw [this]
[GOAL]
case h₁
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β✝ : Type u
pp : β✝ → Prop
β : Type u
P : β → Prop
x : F (α ::: β)
u✝ : F fun i => { p_1 // ofRepeat (PredLast' α P i p_1) }
⊢ (fun i => Subtype.val) = fun i x => ↑(MvFunctor.f P n α i x)
[PROOFSTEP]
ext i ⟨x, _⟩
[GOAL]
case h₁.h.h.mk
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β✝ : Type u
pp : β✝ → Prop
β : Type u
P : β → Prop
x✝ : F (α ::: β)
u✝ : F fun i => { p_1 // ofRepeat (PredLast' α P i p_1) }
i : Fin2 (n + 1)
x : (α ::: β) i
property✝ : ofRepeat (PredLast' α P i x)
⊢ ↑{ val := x, property := property✝ } = ↑(MvFunctor.f P n α i { val := x, property := property✝ })
[PROOFSTEP]
cases i
[GOAL]
case h₁.h.h.mk.fz
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β✝ : Type u
pp : β✝ → Prop
β : Type u
P : β → Prop
x✝ : F (α ::: β)
u✝ : F fun i => { p_1 // ofRepeat (PredLast' α P i p_1) }
x : (α ::: β) Fin2.fz
property✝ : ofRepeat (PredLast' α P Fin2.fz x)
⊢ ↑{ val := x, property := property✝ } = ↑(MvFunctor.f P n α Fin2.fz { val := x, property := property✝ })
[PROOFSTEP]
rfl
[GOAL]
case h₁.h.h.mk.fs
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β✝ : Type u
pp : β✝ → Prop
β : Type u
P : β → Prop
x✝ : F (α ::: β)
u✝ : F fun i => { p_1 // ofRepeat (PredLast' α P i p_1) }
a✝ : Fin2 (Nat.add n 0)
x : (α ::: β) (Fin2.fs a✝)
property✝ : ofRepeat (PredLast' α P (Fin2.fs a✝) x)
⊢ ↑{ val := x, property := property✝ } = ↑(MvFunctor.f P n α (Fin2.fs a✝) { val := x, property := property✝ })
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α✝ : TypeVec n
β : Type u
pp : β → Prop
rr : β → β → Prop
x✝ : ℕ
α : TypeVec x✝
i : Fin2 x✝
x : (fun i => { p_1 // ofRepeat (RelLast' α rr i (prod.mk i p_1.fst p_1.snd)) }) (Fin2.fs i)
⊢ ofRepeat (RelLast' α rr (Fin2.fs i) (prod.mk (Fin2.fs i) (↑x).fst (↑x).snd)) = RelLast α rr (↑x).fst (↑x).snd
[PROOFSTEP]
simp only [RelLast]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α✝ : TypeVec n
β : Type u
pp : β → Prop
rr : β → β → Prop
x✝ : ℕ
α : TypeVec x✝
i : Fin2 x✝
x : (fun i => { p_1 // ofRepeat (RelLast' α rr i (prod.mk i p_1.fst p_1.snd)) }) (Fin2.fs i)
⊢ ofRepeat (RelLast' α rr (Fin2.fs i) (prod.mk (Fin2.fs i) (↑x).fst (↑x).snd)) = ((↑x).fst = (↑x).snd)
[PROOFSTEP]
erw [repeatEq_iff_eq]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α✝ : TypeVec n
β : Type u
pp : β → Prop
rr : β → β → Prop
x✝ : ℕ
α : TypeVec x✝
i : Fin2 x✝
x : (fun i => { p_1 // RelLast α rr p_1.fst p_1.snd }) (Fin2.fs i)
⊢ RelLast α rr (↑x).fst (↑x).snd = ofRepeat (RelLast' α rr (Fin2.fs i) (prod.mk (Fin2.fs i) (↑x).fst (↑x).snd))
[PROOFSTEP]
simp only [RelLast]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α✝ : TypeVec n
β : Type u
pp : β → Prop
rr : β → β → Prop
x✝ : ℕ
α : TypeVec x✝
i : Fin2 x✝
x : (fun i => { p_1 // RelLast α rr p_1.fst p_1.snd }) (Fin2.fs i)
⊢ ((↑x).fst = (↑x).snd) = ofRepeat (RelLast' α rr (Fin2.fs i) (prod.mk (Fin2.fs i) (↑x).fst (↑x).snd))
[PROOFSTEP]
erw [repeatEq_iff_eq]
[GOAL]
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
[PROOFSTEP]
dsimp only [LiftR, LiftR']
[GOAL]
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
[PROOFSTEP]
apply exists_iff_exists_of_mono F (f' rr _ _) (g' rr _ _)
[GOAL]
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
[PROOFSTEP]
ext i ⟨x, _⟩ : 2
[GOAL]
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✝ }
[PROOFSTEP]
cases i
[GOAL]
case h₀.a.h.mk.fz
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 (α ::: β)
x : (α ::: β) Fin2.fz × (α ::: β) Fin2.fz
property✝ : RelLast α rr x.fst x.snd
⊢ (MvFunctor.f' rr n α ⊚ MvFunctor.g' rr n α) Fin2.fz { val := x, property := property✝ } =
    TypeVec.id Fin2.fz { val := x, property := property✝ }
[PROOFSTEP]
rfl
[GOAL]
case h₀.a.h.mk.fs
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 (α ::: β)
a✝ : Fin2 (Nat.add n 0)
x : (α ::: β) (Fin2.fs a✝) × (α ::: β) (Fin2.fs a✝)
property✝ : RelLast α rr x.fst x.snd
⊢ (MvFunctor.f' rr n α ⊚ MvFunctor.g' rr n α) (Fin2.fs a✝) { val := x, property := property✝ } =
    TypeVec.id (Fin2.fs a✝) { val := x, property := property✝ }
[PROOFSTEP]
rfl
[GOAL]
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
[PROOFSTEP]
intros
[GOAL]
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
[PROOFSTEP]
simp [MvFunctor.map_map, (· ⊚ ·)]
  -- porting note: proof was
      -- rw [MvFunctor.map_map, MvFunctor.map_map, (· ⊚ ·), (· ⊚ ·)]
      -- congr <;> ext i ⟨x, _⟩ <;> cases i <;> rfl
[GOAL]
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
[PROOFSTEP]
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];
[GOAL]
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
[PROOFSTEP]
rcases this with ⟨left, right⟩
[GOAL]
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
[PROOFSTEP]
rw [left, right]
[GOAL]
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
[PROOFSTEP]
constructor
[GOAL]
case h₁.left
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
[PROOFSTEP]
ext i ⟨x, _⟩
[GOAL]
case h₁.right
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).snd) = fun i x => (↑(MvFunctor.f' rr n α i x)).snd
[PROOFSTEP]
ext i ⟨x, _⟩
[GOAL]
case h₁.left.h.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 (α ::: β)
u✝ : F fun i => { p_1 // ofRepeat (RelLast' α rr i (prod.mk i p_1.fst p_1.snd)) }
i : Fin2 (n + 1)
x : (α ::: β) i × (α ::: β) i
property✝ : ofRepeat (RelLast' α rr i (prod.mk i x.fst x.snd))
⊢ (↑{ val := x, property := property✝ }).fst = (↑(MvFunctor.f' rr n α i { val := x, property := property✝ })).fst
[PROOFSTEP]
cases i
[GOAL]
case h₁.right.h.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 (α ::: β)
u✝ : F fun i => { p_1 // ofRepeat (RelLast' α rr i (prod.mk i p_1.fst p_1.snd)) }
i : Fin2 (n + 1)
x : (α ::: β) i × (α ::: β) i
property✝ : ofRepeat (RelLast' α rr i (prod.mk i x.fst x.snd))
⊢ (↑{ val := x, property := property✝ }).snd = (↑(MvFunctor.f' rr n α i { val := x, property := property✝ })).snd
[PROOFSTEP]
cases i
[GOAL]
case h₁.left.h.h.mk.fz
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)) }
x : (α ::: β) Fin2.fz × (α ::: β) Fin2.fz
property✝ : ofRepeat (RelLast' α rr Fin2.fz (prod.mk Fin2.fz x.fst x.snd))
⊢ (↑{ val := x, property := property✝ }).fst = (↑(MvFunctor.f' rr n α Fin2.fz { val := x, property := property✝ })).fst
[PROOFSTEP]
rfl
[GOAL]
case h₁.left.h.h.mk.fs
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)) }
a✝ : Fin2 (Nat.add n 0)
x : (α ::: β) (Fin2.fs a✝) × (α ::: β) (Fin2.fs a✝)
property✝ : ofRepeat (RelLast' α rr (Fin2.fs a✝) (prod.mk (Fin2.fs a✝) x.fst x.snd))
⊢ (↑{ val := x, property := property✝ }).fst =
    (↑(MvFunctor.f' rr n α (Fin2.fs a✝) { val := x, property := property✝ })).fst
[PROOFSTEP]
rfl
[GOAL]
case h₁.right.h.h.mk.fz
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)) }
x : (α ::: β) Fin2.fz × (α ::: β) Fin2.fz
property✝ : ofRepeat (RelLast' α rr Fin2.fz (prod.mk Fin2.fz x.fst x.snd))
⊢ (↑{ val := x, property := property✝ }).snd = (↑(MvFunctor.f' rr n α Fin2.fz { val := x, property := property✝ })).snd
[PROOFSTEP]
rfl
[GOAL]
case h₁.right.h.h.mk.fs
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)) }
a✝ : Fin2 (Nat.add n 0)
x : (α ::: β) (Fin2.fs a✝) × (α ::: β) (Fin2.fs a✝)
property✝ : ofRepeat (RelLast' α rr (Fin2.fs a✝) (prod.mk (Fin2.fs a✝) x.fst x.snd))
⊢ (↑{ val := x, property := property✝ }).snd =
    (↑(MvFunctor.f' rr n α (Fin2.fs a✝) { val := x, property := property✝ })).snd
[PROOFSTEP]
rfl
