case h
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
a : P.A
f : B P a ⟹ α
i : Fin2 n
x : α i
⊢ x ∈ supp { fst := a, snd := f } i ↔ x ∈ f i '' univ
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
a : P.A
f : B P a ⟹ α
i : Fin2 n
⊢ supp { fst := a, snd := f } i = f i '' univ
ext x
case h
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
a : P.A
f : B P a ⟹ α
i : Fin2 n
x : α i
⊢ (∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, LiftP P_1 { fst := a, snd := f } → P_1 i x) ↔ ∃ y, f i y = x
case h
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
a : P.A
f : B P a ⟹ α
i : Fin2 n
x : α i
⊢ x ∈ supp { fst := a, snd := f } i ↔ x ∈ f i '' univ
simp only [supp, image_univ, mem_range, mem_setOf_eq]
case h.mp
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
a : P.A
f : B P a ⟹ α
i : Fin2 n
x : α i
h : ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, LiftP P_1 { fst := a, snd := f } → P_1 i x
⊢ ∃ y, f i y = x

case h.mpr
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
a : P.A
f : B P a ⟹ α
i : Fin2 n
x : α i
h : ∃ y, f i y = x
⊢ ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, LiftP P_1 { fst := a, snd := f } → P_1 i x
case h
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
a : P.A
f : B P a ⟹ α
i : Fin2 n
x : α i
⊢ (∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, LiftP P_1 { fst := a, snd := f } → P_1 i x) ↔ ∃ y, f i y = x
constructor <;> intro h
case h.mp
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
a : P.A
f : B P a ⟹ α
i : Fin2 n
x : α i
h : ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, LiftP P_1 { fst := a, snd := f } → P_1 i x
⊢ LiftP (fun i x => ∃ y, f i y = x) { fst := a, snd := f }
case h.mp
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
a : P.A
f : B P a ⟹ α
i : Fin2 n
x : α i
h : ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, LiftP P_1 { fst := a, snd := f } → P_1 i x
⊢ ∃ y, f i y = x
apply @h fun i x => ∃ y : P.B a i, f i y = x
case h.mp
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
a : P.A
f : B P a ⟹ α
i : Fin2 n
x : α i
h : ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, LiftP P_1 { fst := a, snd := f } → P_1 i x
⊢ ∀ (i : Fin2 n) (x : B P a i), ∃ y, f i y = f i x
case h.mp
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
a : P.A
f : B P a ⟹ α
i : Fin2 n
x : α i
h : ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, LiftP P_1 { fst := a, snd := f } → P_1 i x
⊢ LiftP (fun i x => ∃ y, f i y = x) { fst := a, snd := f }
rw [liftP_iff']
case h.mp
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
a : P.A
f : B P a ⟹ α
i : Fin2 n
x : α i
h : ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, LiftP P_1 { fst := a, snd := f } → P_1 i x
i✝ : Fin2 n
x✝ : B P a i✝
⊢ ∃ y, f i✝ y = f i✝ x✝
case h.mp
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
a : P.A
f : B P a ⟹ α
i : Fin2 n
x : α i
h : ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, LiftP P_1 { fst := a, snd := f } → P_1 i x
⊢ ∀ (i : Fin2 n) (x : B P a i), ∃ y, f i y = f i x
intros
no goals
case h.mp
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
a : P.A
f : B P a ⟹ α
i : Fin2 n
x : α i
h : ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, LiftP P_1 { fst := a, snd := f } → P_1 i x
i✝ : Fin2 n
x✝ : B P a i✝
⊢ ∃ y, f i✝ y = f i✝ x✝
refine' ⟨_, rfl⟩
case h.mpr
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
a : P.A
f : B P a ⟹ α
i : Fin2 n
x : α i
h : ∃ y, f i y = x
⊢ ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, (∀ (i : Fin2 n) (x : B P a i), P_1 i (f i x)) → P_1 i x
case h.mpr
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
a : P.A
f : B P a ⟹ α
i : Fin2 n
x : α i
h : ∃ y, f i y = x
⊢ ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, LiftP P_1 { fst := a, snd := f } → P_1 i x
simp only [liftP_iff']
case h.mpr.intro
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
a : P.A
f : B P a ⟹ α
i : Fin2 n
x : α i
w✝ : B P a i
h✝ : f i w✝ = x
⊢ ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, (∀ (i : Fin2 n) (x : B P a i), P_1 i (f i x)) → P_1 i x
case h.mpr
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
a : P.A
f : B P a ⟹ α
i : Fin2 n
x : α i
h : ∃ y, f i y = x
⊢ ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, (∀ (i : Fin2 n) (x : B P a i), P_1 i (f i x)) → P_1 i x
cases h
case h.mpr.intro
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
a : P.A
f : B P a ⟹ α
i : Fin2 n
w✝ : B P a i
⊢ ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, (∀ (i : Fin2 n) (x : B P a i), P_1 i (f i x)) → P_1 i (f i w✝)
case h.mpr.intro
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
a : P.A
f : B P a ⟹ α
i : Fin2 n
x : α i
w✝ : B P a i
h✝ : f i w✝ = x
⊢ ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, (∀ (i : Fin2 n) (x : B P a i), P_1 i (f i x)) → P_1 i x
subst x
no goals
case h.mpr.intro
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
a : P.A
f : B P a ⟹ α
i : Fin2 n
w✝ : B P a i
⊢ ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, (∀ (i : Fin2 n) (x : B P a i), P_1 i (f i x)) → P_1 i (f i w✝)
tauto