case mp
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
⊢ SuppPreservation → IsUniform

case mpr
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
⊢ IsUniform → SuppPreservation
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
⊢ SuppPreservation ↔ IsUniform
constructor
case mp
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : SuppPreservation
α : TypeVec n
a a' : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
f' : MvPFunctor.B (P F) a' ⟹ α
h' : abs { fst := a, snd := f } = abs { fst := a', snd := f' }
i : Fin2 n
⊢ f i '' univ = f' i '' univ
case mp
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
⊢ SuppPreservation → IsUniform
intro h α a a' f f' h' i
no goals
case mp
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : SuppPreservation
α : TypeVec n
a a' : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
f' : MvPFunctor.B (P F) a' ⟹ α
h' : abs { fst := a, snd := f } = abs { fst := a', snd := f' }
i : Fin2 n
⊢ f i '' univ = f' i '' univ
rw [← MvPFunctor.supp_eq, ← MvPFunctor.supp_eq, ← h, h', h]
case mpr.mk
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 ⟹ α
⊢ supp (abs { fst := a, snd := f }) = supp { fst := a, snd := f }
case mpr
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
⊢ IsUniform → SuppPreservation
rintro h α ⟨a, f⟩
case mpr.mk.h.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 ⟹ α
x✝¹ : Fin2 n
x✝ : α x✝¹
⊢ x✝ ∈ supp (abs { fst := a, snd := f }) x✝¹ ↔ x✝ ∈ supp { fst := a, snd := f } x✝¹
case mpr.mk
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 ⟹ α
⊢ supp (abs { fst := a, snd := f }) = supp { fst := a, snd := f }
ext
no goals
case mpr.mk.h.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 ⟹ α
x✝¹ : Fin2 n
x✝ : α x✝¹
⊢ x✝ ∈ supp (abs { fst := a, snd := f }) x✝¹ ↔ x✝ ∈ supp { fst := a, snd := f } x✝¹
rwa [supp_eq_of_isUniform, MvPFunctor.supp_eq]