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
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
dsimp only [LiftP, LiftP']
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

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
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
apply exists_iff_exists_of_mono F (f _ n α) (g _ n α)
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✝ })
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
ext (i⟨x, _⟩)
no goals
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✝ })
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
β : 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
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
intros
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
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
rw [MvFunctor.map_map]
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)
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
suffices (fun i => Subtype.val) = (fun i x => (MvFunctor.f P n α i x).val)
  by rw[this];
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✝ })
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)
ext (i⟨x, _⟩)
no goals
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✝ })
cases i <;> rfl
no goals
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
rw[this]