n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : IsUniform
α : TypeVec n
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
i✝ : Fin2 n
⊢ supp (abs { fst := a, snd := f }) i✝ = f i✝ '' univ
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : IsUniform
α : TypeVec n
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
⊢ ∀ (i : Fin2 n), supp (abs { fst := a, snd := f }) i = f i '' univ
intro
case h
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : IsUniform
α : TypeVec n
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
i✝ : Fin2 n
u : α i✝
⊢ u ∈ supp (abs { fst := a, snd := f }) i✝ ↔ u ∈ f i✝ '' univ
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : IsUniform
α : TypeVec n
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
i✝ : Fin2 n
⊢ supp (abs { fst := a, snd := f }) i✝ = f i✝ '' univ
ext u
case h
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : IsUniform
α : TypeVec n
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
i✝ : Fin2 n
u : α i✝
⊢ (∀ (a_1 : (P F).A) (f_1 : MvPFunctor.B (P F) a_1 ⟹ α),
      abs { fst := a_1, snd := f_1 } = abs { fst := a, snd := f } → u ∈ f_1 i✝ '' univ) ↔
    u ∈ f i✝ '' univ
case h
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : IsUniform
α : TypeVec n
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
i✝ : Fin2 n
u : α i✝
⊢ u ∈ supp (abs { fst := a, snd := f }) i✝ ↔ u ∈ f i✝ '' univ
rw [mem_supp]
case h.mp
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : IsUniform
α : TypeVec n
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
i✝ : Fin2 n
u : α i✝
⊢ (∀ (a_1 : (P F).A) (f_1 : MvPFunctor.B (P F) a_1 ⟹ α),
      abs { fst := a_1, snd := f_1 } = abs { fst := a, snd := f } → u ∈ f_1 i✝ '' univ) →
    u ∈ f i✝ '' univ

case h.mpr
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : IsUniform
α : TypeVec n
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
i✝ : Fin2 n
u : α i✝
⊢ u ∈ f i✝ '' univ →
    ∀ (a_2 : (P F).A) (f_1 : MvPFunctor.B (P F) a_2 ⟹ α),
      abs { fst := a_2, snd := f_1 } = abs { fst := a, snd := f } → u ∈ f_1 i✝ '' univ
case h
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : IsUniform
α : TypeVec n
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
i✝ : Fin2 n
u : α i✝
⊢ (∀ (a_1 : (P F).A) (f_1 : MvPFunctor.B (P F) a_1 ⟹ α),
      abs { fst := a_1, snd := f_1 } = abs { fst := a, snd := f } → u ∈ f_1 i✝ '' univ) ↔
    u ∈ f i✝ '' univ
constructor
case h.mpr
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : IsUniform
α : TypeVec n
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
i✝ : Fin2 n
u : α i✝
h' : u ∈ f i✝ '' univ
a' : (P F).A
f' : MvPFunctor.B (P F) a' ⟹ α
e : abs { fst := a', snd := f' } = abs { fst := a, snd := f }
⊢ u ∈ f' i✝ '' univ
case h.mpr
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : IsUniform
α : TypeVec n
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
i✝ : Fin2 n
u : α i✝
⊢ u ∈ f i✝ '' univ →
    ∀ (a_2 : (P F).A) (f_1 : MvPFunctor.B (P F) a_2 ⟹ α),
      abs { fst := a_2, snd := f_1 } = abs { fst := a, snd := f } → u ∈ f_1 i✝ '' univ
intro h' a' f' e
case h.mpr
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : IsUniform
α : TypeVec n
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
i✝ : Fin2 n
u : α i✝
h' : u ∈ f i✝ '' univ
a' : (P F).A
f' : MvPFunctor.B (P F) a' ⟹ α
e : abs { fst := a', snd := f' } = abs { fst := a, snd := f }
⊢ u ∈ f i✝ '' univ
case h.mpr
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : IsUniform
α : TypeVec n
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
i✝ : Fin2 n
u : α i✝
h' : u ∈ f i✝ '' univ
a' : (P F).A
f' : MvPFunctor.B (P F) a' ⟹ α
e : abs { fst := a', snd := f' } = abs { fst := a, snd := f }
⊢ u ∈ f' i✝ '' univ
rw [← h _ _ _ _ e.symm]
no goals
case h.mpr
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : IsUniform
α : TypeVec n
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
i✝ : Fin2 n
u : α i✝
h' : u ∈ f i✝ '' univ
a' : (P F).A
f' : MvPFunctor.B (P F) a' ⟹ α
e : abs { fst := a', snd := f' } = abs { fst := a, snd := f }
⊢ u ∈ f i✝ '' univ
apply h'
case h.mp
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : IsUniform
α : TypeVec n
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
i✝ : Fin2 n
u : α i✝
h' :
  ∀ (a_1 : (P F).A) (f_1 : MvPFunctor.B (P F) a_1 ⟹ α),
    abs { fst := a_1, snd := f_1 } = abs { fst := a, snd := f } → u ∈ f_1 i✝ '' univ
⊢ u ∈ f i✝ '' univ
case h.mp
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : IsUniform
α : TypeVec n
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
i✝ : Fin2 n
u : α i✝
⊢ (∀ (a_1 : (P F).A) (f_1 : MvPFunctor.B (P F) a_1 ⟹ α),
      abs { fst := a_1, snd := f_1 } = abs { fst := a, snd := f } → u ∈ f_1 i✝ '' univ) →
    u ∈ f i✝ '' univ
intro h'
no goals
case h.mp
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : IsUniform
α : TypeVec n
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
i✝ : Fin2 n
u : α i✝
h' :
  ∀ (a_1 : (P F).A) (f_1 : MvPFunctor.B (P F) a_1 ⟹ α),
    abs { fst := a_1, snd := f_1 } = abs { fst := a, snd := f } → u ∈ f_1 i✝ '' univ
⊢ u ∈ f i✝ '' univ
apply h' _ _ rfl