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

case mpr
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : LiftPPreservation
⊢ SuppPreservation
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
⊢ SuppPreservation ↔ LiftPPreservation
constructor <;> intro h
case mp.mk
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : SuppPreservation
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
⊢ LiftP p (abs { fst := a, snd := f }) ↔ LiftP p { fst := a, snd := f }
case mp
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : SuppPreservation
⊢ LiftPPreservation
rintro α p ⟨a, f⟩
case mp.mk
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : SuppPreservation
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
h' : SuppPreservation
⊢ LiftP p (abs { fst := a, snd := f }) ↔ LiftP p { fst := a, snd := f }
case mp.mk
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : SuppPreservation
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
⊢ LiftP p (abs { fst := a, snd := f }) ↔ LiftP p { fst := a, snd := f }
have h' := h
case mp.mk
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : SuppPreservation
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
h' : IsUniform
⊢ LiftP p (abs { fst := a, snd := f }) ↔ LiftP p { fst := a, snd := f }
case mp.mk
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : SuppPreservation
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
h' : SuppPreservation
⊢ LiftP p (abs { fst := a, snd := f }) ↔ LiftP p { fst := a, snd := f }
rw [suppPreservation_iff_isUniform] at h'
case mp.mk
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h :
  ∀ ⦃α : TypeVec n⦄ (x : MvPFunctor.Obj (P F) α),
    (fun i => {y | ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P (abs x) → P i y}) = fun i =>
      {y | ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P x → P i y}
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
h' : IsUniform
⊢ LiftP p (abs { fst := a, snd := f }) ↔ LiftP p { fst := a, snd := f }
case mp.mk
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : SuppPreservation
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
h' : IsUniform
⊢ LiftP p (abs { fst := a, snd := f }) ↔ LiftP p { fst := a, snd := f }
dsimp only [SuppPreservation, supp] at h
case mp.mk
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h :
  ∀ ⦃α : TypeVec n⦄ (x : MvPFunctor.Obj (P F) α),
    (fun i => {y | ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P (abs x) → P i y}) = fun i =>
      {y | ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P x → P i y}
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
h' : IsUniform
⊢ (∀ (i : Fin2 n) (u : α i) (x : MvPFunctor.B (P F) a i), f i x = u → p u) ↔
    ∀ (i : Fin2 n) (x : MvPFunctor.B (P F) a i), p (f i x)
case mp.mk
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h :
  ∀ ⦃α : TypeVec n⦄ (x : MvPFunctor.Obj (P F) α),
    (fun i => {y | ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P (abs x) → P i y}) = fun i =>
      {y | ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P x → P i y}
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
h' : IsUniform
⊢ LiftP p (abs { fst := a, snd := f }) ↔ LiftP p { fst := a, snd := f }
simp only [liftP_iff_of_isUniform, supp_eq_of_isUniform, MvPFunctor.liftP_iff', h',
  image_univ, mem_range, exists_imp]
no goals
case mp.mk
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h :
  ∀ ⦃α : TypeVec n⦄ (x : MvPFunctor.Obj (P F) α),
    (fun i => {y | ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P (abs x) → P i y}) = fun i =>
      {y | ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P x → P i y}
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
h' : IsUniform
⊢ (∀ (i : Fin2 n) (u : α i) (x : MvPFunctor.B (P F) a i), f i x = u → p u) ↔
    ∀ (i : Fin2 n) (x : MvPFunctor.B (P F) a i), p (f i x)
constructor <;> intros <;> subst_vars <;> solve_by_elim
case mpr.mk
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : LiftPPreservation
α : 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
h : LiftPPreservation
⊢ SuppPreservation
rintro α ⟨a, f⟩
case mpr.mk
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : ∀ ⦃α : TypeVec n⦄ (p : ⦃i : Fin2 n⦄ → α i → Prop) (x : MvPFunctor.Obj (P F) α), LiftP p (abs x) ↔ LiftP p x
α : 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.mk
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : LiftPPreservation
α : TypeVec n
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
⊢ supp (abs { fst := a, snd := f }) = supp { fst := a, snd := f }
simp only [LiftPPreservation] at h
case mpr.mk.h.h
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : ∀ ⦃α : TypeVec n⦄ (p : ⦃i : Fin2 n⦄ → α i → Prop) (x : MvPFunctor.Obj (P F) α), LiftP p (abs x) ↔ LiftP p x
α : 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 : ∀ ⦃α : TypeVec n⦄ (p : ⦃i : Fin2 n⦄ → α i → Prop) (x : MvPFunctor.Obj (P F) α), LiftP p (abs x) ↔ LiftP p x
α : 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 : ∀ ⦃α : TypeVec n⦄ (p : ⦃i : Fin2 n⦄ → α i → Prop) (x : MvPFunctor.Obj (P F) α), LiftP p (abs x) ↔ LiftP p x
α : 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✝¹
simp only [supp, h, mem_setOf_eq]