[GOAL]
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
⊢ TypeVec.id <$$> x = x
[PROOFSTEP]
rw [← abs_repr x]
[GOAL]
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
⊢ TypeVec.id <$$> abs (repr x) = abs (repr x)
[PROOFSTEP]
cases' repr x with a f
[GOAL]
case mk
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
⊢ TypeVec.id <$$> abs { fst := a, snd := f } = abs { fst := a, snd := f }
[PROOFSTEP]
rw [← abs_map]
[GOAL]
case mk
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
⊢ abs (TypeVec.id <$$> { fst := a, snd := f }) = abs { fst := a, snd := f }
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α β γ : TypeVec n
f : α ⟹ β
g : β ⟹ γ
x : F α
⊢ (g ⊚ f) <$$> x = g <$$> f <$$> x
[PROOFSTEP]
rw [← abs_repr x]
[GOAL]
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α β γ : TypeVec n
f : α ⟹ β
g : β ⟹ γ
x : F α
⊢ (g ⊚ f) <$$> abs (repr x) = g <$$> f <$$> abs (repr x)
[PROOFSTEP]
cases' repr x with a f
[GOAL]
case mk
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α β γ : TypeVec n
f✝ : α ⟹ β
g : β ⟹ γ
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
⊢ (g ⊚ f✝) <$$> abs { fst := a, snd := f } = g <$$> f✝ <$$> abs { fst := a, snd := f }
[PROOFSTEP]
rw [← abs_map, ← abs_map, ← abs_map]
[GOAL]
case mk
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α β γ : TypeVec n
f✝ : α ⟹ β
g : β ⟹ γ
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
⊢ abs ((g ⊚ f✝) <$$> { fst := a, snd := f }) = abs (g <$$> f✝ <$$> { fst := a, snd := f })
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
⊢ LiftP p x ↔ ∃ a f, x = abs { fst := a, snd := f } ∧ ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p (f i j)
[PROOFSTEP]
constructor
[GOAL]
case mp
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
⊢ LiftP p x → ∃ a f, x = abs { fst := a, snd := f } ∧ ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p (f i j)
[PROOFSTEP]
rintro ⟨y, hy⟩
[GOAL]
case mp.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
y : F fun i => Subtype p
hy : (fun i => Subtype.val) <$$> y = x
⊢ ∃ a f, x = abs { fst := a, snd := f } ∧ ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p (f i j)
[PROOFSTEP]
cases' h : repr y with a f
[GOAL]
case mp.intro.mk
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
y : F fun i => Subtype p
hy : (fun i => Subtype.val) <$$> y = x
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ fun i => Subtype p
h : repr y = { fst := a, snd := f }
⊢ ∃ a f, x = abs { fst := a, snd := f } ∧ ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p (f i j)
[PROOFSTEP]
use a, fun i j => (f i j).val
[GOAL]
case h
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
y : F fun i => Subtype p
hy : (fun i => Subtype.val) <$$> y = x
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ fun i => Subtype p
h : repr y = { fst := a, snd := f }
⊢ x = abs { fst := a, snd := fun i j => ↑(f i j) } ∧ ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p ↑(f i j)
[PROOFSTEP]
constructor
[GOAL]
case h.left
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
y : F fun i => Subtype p
hy : (fun i => Subtype.val) <$$> y = x
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ fun i => Subtype p
h : repr y = { fst := a, snd := f }
⊢ x = abs { fst := a, snd := fun i j => ↑(f i j) }
[PROOFSTEP]
rw [← hy, ← abs_repr y, h, ← abs_map]
[GOAL]
case h.left
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
y : F fun i => Subtype p
hy : (fun i => Subtype.val) <$$> y = x
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ fun i => Subtype p
h : repr y = { fst := a, snd := f }
⊢ abs ((fun i => Subtype.val) <$$> { fst := a, snd := f }) = abs { fst := a, snd := fun i j => ↑(f i j) }
[PROOFSTEP]
rfl
[GOAL]
case h.right
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
y : F fun i => Subtype p
hy : (fun i => Subtype.val) <$$> y = x
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ fun i => Subtype p
h : repr y = { fst := a, snd := f }
⊢ ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p ↑(f i j)
[PROOFSTEP]
intro i j
[GOAL]
case h.right
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
y : F fun i => Subtype p
hy : (fun i => Subtype.val) <$$> y = x
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ fun i => Subtype p
h : repr y = { fst := a, snd := f }
i : Fin2 n
j : MvPFunctor.B (P F) a i
⊢ p ↑(f i j)
[PROOFSTEP]
apply (f i j).property
[GOAL]
case mpr
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
⊢ (∃ a f, x = abs { fst := a, snd := f } ∧ ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p (f i j)) → LiftP p x
[PROOFSTEP]
rintro ⟨a, f, h₀, h₁⟩
[GOAL]
case mpr.intro.intro.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
h₀ : x = abs { fst := a, snd := f }
h₁ : ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p (f i j)
⊢ LiftP p x
[PROOFSTEP]
use abs ⟨a, fun i j => ⟨f i j, h₁ i j⟩⟩
[GOAL]
case h
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
h₀ : x = abs { fst := a, snd := f }
h₁ : ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p (f i j)
⊢ (fun i => Subtype.val) <$$> abs { fst := a, snd := fun i j => { val := f i j, property := (_ : p (f i j)) } } = x
[PROOFSTEP]
rw [← abs_map, h₀]
[GOAL]
case h
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
h₀ : x = abs { fst := a, snd := f }
h₁ : ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p (f i j)
⊢ abs ((fun i => Subtype.val) <$$> { fst := a, snd := fun i j => { val := f i j, property := (_ : p (f i j)) } }) =
    abs { fst := a, snd := f }
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
r : {i : Fin2 n} → α i → α i → Prop
x y : F α
⊢ LiftR (fun {i} => r) x y ↔
    ∃ a f₀ f₁,
      x = abs { fst := a, snd := f₀ } ∧
        y = abs { fst := a, snd := f₁ } ∧ ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), r (f₀ i j) (f₁ i j)
[PROOFSTEP]
constructor
[GOAL]
case mp
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
r : {i : Fin2 n} → α i → α i → Prop
x y : F α
⊢ LiftR (fun {i} => r) x y →
    ∃ a f₀ f₁,
      x = abs { fst := a, snd := f₀ } ∧
        y = abs { fst := a, snd := f₁ } ∧ ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), r (f₀ i j) (f₁ i j)
[PROOFSTEP]
rintro ⟨u, xeq, yeq⟩
[GOAL]
case mp.intro.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
r : {i : Fin2 n} → α i → α i → Prop
x y : F α
u : F fun i => { p // (fun {i} => r) p.fst p.snd }
xeq : (fun i t => (↑t).fst) <$$> u = x
yeq : (fun i t => (↑t).snd) <$$> u = y
⊢ ∃ a f₀ f₁,
    x = abs { fst := a, snd := f₀ } ∧
      y = abs { fst := a, snd := f₁ } ∧ ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), r (f₀ i j) (f₁ i j)
[PROOFSTEP]
cases' h : repr u with a f
[GOAL]
case mp.intro.intro.mk
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
r : {i : Fin2 n} → α i → α i → Prop
x y : F α
u : F fun i => { p // (fun {i} => r) p.fst p.snd }
xeq : (fun i t => (↑t).fst) <$$> u = x
yeq : (fun i t => (↑t).snd) <$$> u = y
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ fun i => { p // (fun {i} => r) p.fst p.snd }
h : repr u = { fst := a, snd := f }
⊢ ∃ a f₀ f₁,
    x = abs { fst := a, snd := f₀ } ∧
      y = abs { fst := a, snd := f₁ } ∧ ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), r (f₀ i j) (f₁ i j)
[PROOFSTEP]
use a, fun i j => (f i j).val.fst, fun i j => (f i j).val.snd
[GOAL]
case h
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
r : {i : Fin2 n} → α i → α i → Prop
x y : F α
u : F fun i => { p // (fun {i} => r) p.fst p.snd }
xeq : (fun i t => (↑t).fst) <$$> u = x
yeq : (fun i t => (↑t).snd) <$$> u = y
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ fun i => { p // (fun {i} => r) p.fst p.snd }
h : repr u = { fst := a, snd := f }
⊢ x = abs { fst := a, snd := fun i j => (↑(f i j)).fst } ∧
    y = abs { fst := a, snd := fun i j => (↑(f i j)).snd } ∧
      ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), r (↑(f i j)).fst (↑(f i j)).snd
[PROOFSTEP]
constructor
[GOAL]
case h.left
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
r : {i : Fin2 n} → α i → α i → Prop
x y : F α
u : F fun i => { p // (fun {i} => r) p.fst p.snd }
xeq : (fun i t => (↑t).fst) <$$> u = x
yeq : (fun i t => (↑t).snd) <$$> u = y
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ fun i => { p // (fun {i} => r) p.fst p.snd }
h : repr u = { fst := a, snd := f }
⊢ x = abs { fst := a, snd := fun i j => (↑(f i j)).fst }
[PROOFSTEP]
rw [← xeq, ← abs_repr u, h, ← abs_map]
[GOAL]
case h.left
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
r : {i : Fin2 n} → α i → α i → Prop
x y : F α
u : F fun i => { p // (fun {i} => r) p.fst p.snd }
xeq : (fun i t => (↑t).fst) <$$> u = x
yeq : (fun i t => (↑t).snd) <$$> u = y
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ fun i => { p // (fun {i} => r) p.fst p.snd }
h : repr u = { fst := a, snd := f }
⊢ abs ((fun i t => (↑t).fst) <$$> { fst := a, snd := f }) = abs { fst := a, snd := fun i j => (↑(f i j)).fst }
[PROOFSTEP]
rfl
[GOAL]
case h.right
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
r : {i : Fin2 n} → α i → α i → Prop
x y : F α
u : F fun i => { p // (fun {i} => r) p.fst p.snd }
xeq : (fun i t => (↑t).fst) <$$> u = x
yeq : (fun i t => (↑t).snd) <$$> u = y
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ fun i => { p // (fun {i} => r) p.fst p.snd }
h : repr u = { fst := a, snd := f }
⊢ y = abs { fst := a, snd := fun i j => (↑(f i j)).snd } ∧
    ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), r (↑(f i j)).fst (↑(f i j)).snd
[PROOFSTEP]
constructor
[GOAL]
case h.right.left
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
r : {i : Fin2 n} → α i → α i → Prop
x y : F α
u : F fun i => { p // (fun {i} => r) p.fst p.snd }
xeq : (fun i t => (↑t).fst) <$$> u = x
yeq : (fun i t => (↑t).snd) <$$> u = y
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ fun i => { p // (fun {i} => r) p.fst p.snd }
h : repr u = { fst := a, snd := f }
⊢ y = abs { fst := a, snd := fun i j => (↑(f i j)).snd }
[PROOFSTEP]
rw [← yeq, ← abs_repr u, h, ← abs_map]
[GOAL]
case h.right.left
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
r : {i : Fin2 n} → α i → α i → Prop
x y : F α
u : F fun i => { p // (fun {i} => r) p.fst p.snd }
xeq : (fun i t => (↑t).fst) <$$> u = x
yeq : (fun i t => (↑t).snd) <$$> u = y
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ fun i => { p // (fun {i} => r) p.fst p.snd }
h : repr u = { fst := a, snd := f }
⊢ abs ((fun i t => (↑t).snd) <$$> { fst := a, snd := f }) = abs { fst := a, snd := fun i j => (↑(f i j)).snd }
[PROOFSTEP]
rfl
[GOAL]
case h.right.right
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
r : {i : Fin2 n} → α i → α i → Prop
x y : F α
u : F fun i => { p // (fun {i} => r) p.fst p.snd }
xeq : (fun i t => (↑t).fst) <$$> u = x
yeq : (fun i t => (↑t).snd) <$$> u = y
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ fun i => { p // (fun {i} => r) p.fst p.snd }
h : repr u = { fst := a, snd := f }
⊢ ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), r (↑(f i j)).fst (↑(f i j)).snd
[PROOFSTEP]
intro i j
[GOAL]
case h.right.right
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
r : {i : Fin2 n} → α i → α i → Prop
x y : F α
u : F fun i => { p // (fun {i} => r) p.fst p.snd }
xeq : (fun i t => (↑t).fst) <$$> u = x
yeq : (fun i t => (↑t).snd) <$$> u = y
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ fun i => { p // (fun {i} => r) p.fst p.snd }
h : repr u = { fst := a, snd := f }
i : Fin2 n
j : MvPFunctor.B (P F) a i
⊢ r (↑(f i j)).fst (↑(f i j)).snd
[PROOFSTEP]
exact (f i j).property
[GOAL]
case mpr
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
r : {i : Fin2 n} → α i → α i → Prop
x y : F α
⊢ (∃ a f₀ f₁,
      x = abs { fst := a, snd := f₀ } ∧
        y = abs { fst := a, snd := f₁ } ∧ ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), r (f₀ i j) (f₁ i j)) →
    LiftR (fun {i} => r) x y
[PROOFSTEP]
rintro ⟨a, f₀, f₁, xeq, yeq, h⟩
[GOAL]
case mpr.intro.intro.intro.intro.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
r : {i : Fin2 n} → α i → α i → Prop
x y : F α
a : (P F).A
f₀ f₁ : MvPFunctor.B (P F) a ⟹ α
xeq : x = abs { fst := a, snd := f₀ }
yeq : y = abs { fst := a, snd := f₁ }
h : ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), r (f₀ i j) (f₁ i j)
⊢ LiftR (fun {i} => r) x y
[PROOFSTEP]
use abs ⟨a, fun i j => ⟨(f₀ i j, f₁ i j), h i j⟩⟩
[GOAL]
case h
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
r : {i : Fin2 n} → α i → α i → Prop
x y : F α
a : (P F).A
f₀ f₁ : MvPFunctor.B (P F) a ⟹ α
xeq : x = abs { fst := a, snd := f₀ }
yeq : y = abs { fst := a, snd := f₁ }
h : ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), r (f₀ i j) (f₁ i j)
⊢ (fun i t => (↑t).fst) <$$>
        abs { fst := a, snd := fun i j => { val := (f₀ i j, f₁ i j), property := (_ : r (f₀ i j) (f₁ i j)) } } =
      x ∧
    (fun i t => (↑t).snd) <$$>
        abs { fst := a, snd := fun i j => { val := (f₀ i j, f₁ i j), property := (_ : r (f₀ i j) (f₁ i j)) } } =
      y
[PROOFSTEP]
dsimp
[GOAL]
case h
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
r : {i : Fin2 n} → α i → α i → Prop
x y : F α
a : (P F).A
f₀ f₁ : MvPFunctor.B (P F) a ⟹ α
xeq : x = abs { fst := a, snd := f₀ }
yeq : y = abs { fst := a, snd := f₁ }
h : ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), r (f₀ i j) (f₁ i j)
⊢ (fun i t => (↑t).fst) <$$>
        abs { fst := a, snd := fun i j => { val := (f₀ i j, f₁ i j), property := (_ : r (f₀ i j) (f₁ i j)) } } =
      x ∧
    (fun i t => (↑t).snd) <$$>
        abs { fst := a, snd := fun i j => { val := (f₀ i j, f₁ i j), property := (_ : r (f₀ i j) (f₁ i j)) } } =
      y
[PROOFSTEP]
constructor
[GOAL]
case h.left
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
r : {i : Fin2 n} → α i → α i → Prop
x y : F α
a : (P F).A
f₀ f₁ : MvPFunctor.B (P F) a ⟹ α
xeq : x = abs { fst := a, snd := f₀ }
yeq : y = abs { fst := a, snd := f₁ }
h : ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), r (f₀ i j) (f₁ i j)
⊢ (fun i t => (↑t).fst) <$$>
      abs { fst := a, snd := fun i j => { val := (f₀ i j, f₁ i j), property := (_ : r (f₀ i j) (f₁ i j)) } } =
    x
[PROOFSTEP]
rw [xeq, ← abs_map]
[GOAL]
case h.left
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
r : {i : Fin2 n} → α i → α i → Prop
x y : F α
a : (P F).A
f₀ f₁ : MvPFunctor.B (P F) a ⟹ α
xeq : x = abs { fst := a, snd := f₀ }
yeq : y = abs { fst := a, snd := f₁ }
h : ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), r (f₀ i j) (f₁ i j)
⊢ abs
      ((fun i t => (↑t).fst) <$$>
        { fst := a, snd := fun i j => { val := (f₀ i j, f₁ i j), property := (_ : r (f₀ i j) (f₁ i j)) } }) =
    abs { fst := a, snd := f₀ }
[PROOFSTEP]
rfl
[GOAL]
case h.right
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
r : {i : Fin2 n} → α i → α i → Prop
x y : F α
a : (P F).A
f₀ f₁ : MvPFunctor.B (P F) a ⟹ α
xeq : x = abs { fst := a, snd := f₀ }
yeq : y = abs { fst := a, snd := f₁ }
h : ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), r (f₀ i j) (f₁ i j)
⊢ (fun i t => (↑t).snd) <$$>
      abs { fst := a, snd := fun i j => { val := (f₀ i j, f₁ i j), property := (_ : r (f₀ i j) (f₁ i j)) } } =
    y
[PROOFSTEP]
rw [yeq, ← abs_map]
[GOAL]
case h.right
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
r : {i : Fin2 n} → α i → α i → Prop
x y : F α
a : (P F).A
f₀ f₁ : MvPFunctor.B (P F) a ⟹ α
xeq : x = abs { fst := a, snd := f₀ }
yeq : y = abs { fst := a, snd := f₁ }
h : ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), r (f₀ i j) (f₁ i j)
⊢ abs
      ((fun i t => (↑t).snd) <$$>
        { fst := a, snd := fun i j => { val := (f₀ i j, f₁ i j), property := (_ : r (f₀ i j) (f₁ i j)) } }) =
    abs { fst := a, snd := f₁ }
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
i : Fin2 n
u : α i
⊢ u ∈ supp x i ↔ ∀ (a : (P F).A) (f : MvPFunctor.B (P F) a ⟹ α), abs { fst := a, snd := f } = x → u ∈ f i '' univ
[PROOFSTEP]
rw [supp]
[GOAL]
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
i : Fin2 n
u : α i
⊢ u ∈ {y | ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P x → P i y} ↔
    ∀ (a : (P F).A) (f : MvPFunctor.B (P F) a ⟹ α), abs { fst := a, snd := f } = x → u ∈ f i '' univ
[PROOFSTEP]
dsimp
[GOAL]
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
i : Fin2 n
u : α i
⊢ (∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P x → P i u) ↔
    ∀ (a : (P F).A) (f : MvPFunctor.B (P F) a ⟹ α), abs { fst := a, snd := f } = x → u ∈ f i '' univ
[PROOFSTEP]
constructor
[GOAL]
case mp
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
i : Fin2 n
u : α i
⊢ (∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P x → P i u) →
    ∀ (a : (P F).A) (f : MvPFunctor.B (P F) a ⟹ α), abs { fst := a, snd := f } = x → u ∈ f i '' univ
[PROOFSTEP]
intro h a f haf
[GOAL]
case mp
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
i : Fin2 n
u : α i
h : ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P x → P i u
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
haf : abs { fst := a, snd := f } = x
⊢ u ∈ f i '' univ
[PROOFSTEP]
have : LiftP (fun i u => u ∈ f i '' univ) x := by
  rw [liftP_iff]
  refine' ⟨a, f, haf.symm, _⟩
  intro i u
  exact mem_image_of_mem _ (mem_univ _)
[GOAL]
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
i : Fin2 n
u : α i
h : ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P x → P i u
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
haf : abs { fst := a, snd := f } = x
⊢ LiftP (fun i u => u ∈ f i '' univ) x
[PROOFSTEP]
rw [liftP_iff]
[GOAL]
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
i : Fin2 n
u : α i
h : ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P x → P i u
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
haf : abs { fst := a, snd := f } = x
⊢ ∃ a_1 f_1, x = abs { fst := a_1, snd := f_1 } ∧ ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a_1 i), f_1 i j ∈ f i '' univ
[PROOFSTEP]
refine' ⟨a, f, haf.symm, _⟩
[GOAL]
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
i : Fin2 n
u : α i
h : ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P x → P i u
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
haf : abs { fst := a, snd := f } = x
⊢ ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), f i j ∈ f i '' univ
[PROOFSTEP]
intro i u
[GOAL]
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
i✝ : Fin2 n
u✝ : α i✝
h : ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P x → P i✝ u✝
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
haf : abs { fst := a, snd := f } = x
i : Fin2 n
u : MvPFunctor.B (P F) a i
⊢ f i u ∈ f i '' univ
[PROOFSTEP]
exact mem_image_of_mem _ (mem_univ _)
[GOAL]
case mp
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
i : Fin2 n
u : α i
h : ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P x → P i u
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
haf : abs { fst := a, snd := f } = x
this : LiftP (fun i u => u ∈ f i '' univ) x
⊢ u ∈ f i '' univ
[PROOFSTEP]
exact h this
[GOAL]
case mpr
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
i : Fin2 n
u : α i
⊢ (∀ (a : (P F).A) (f : MvPFunctor.B (P F) a ⟹ α), abs { fst := a, snd := f } = x → u ∈ f i '' univ) →
    ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P x → P i u
[PROOFSTEP]
intro h p
[GOAL]
case mpr
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
i : Fin2 n
u : α i
h : ∀ (a : (P F).A) (f : MvPFunctor.B (P F) a ⟹ α), abs { fst := a, snd := f } = x → u ∈ f i '' univ
p : (i : Fin2 n) → α i → Prop
⊢ LiftP p x → p i u
[PROOFSTEP]
rw [liftP_iff]
[GOAL]
case mpr
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
i : Fin2 n
u : α i
h : ∀ (a : (P F).A) (f : MvPFunctor.B (P F) a ⟹ α), abs { fst := a, snd := f } = x → u ∈ f i '' univ
p : (i : Fin2 n) → α i → Prop
⊢ (∃ a f, x = abs { fst := a, snd := f } ∧ ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p i (f i j)) → p i u
[PROOFSTEP]
rintro ⟨a, f, xeq, h'⟩
[GOAL]
case mpr.intro.intro.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
i : Fin2 n
u : α i
h : ∀ (a : (P F).A) (f : MvPFunctor.B (P F) a ⟹ α), abs { fst := a, snd := f } = x → u ∈ f i '' univ
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ fun i => α i
xeq : x = abs { fst := a, snd := f }
h' : ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p i (f i j)
⊢ p i u
[PROOFSTEP]
rcases h a f xeq.symm with ⟨i, _, hi⟩
[GOAL]
case mpr.intro.intro.intro.intro.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
i✝ : Fin2 n
u : α i✝
h : ∀ (a : (P F).A) (f : MvPFunctor.B (P F) a ⟹ α), abs { fst := a, snd := f } = x → u ∈ f i✝ '' univ
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ fun i => α i
xeq : x = abs { fst := a, snd := f }
h' : ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p i (f i j)
i : MvPFunctor.B (P F) a i✝
left✝ : i ∈ univ
hi : f i✝ i = u
⊢ p i✝ u
[PROOFSTEP]
rw [← hi]
[GOAL]
case mpr.intro.intro.intro.intro.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
i✝ : Fin2 n
u : α i✝
h : ∀ (a : (P F).A) (f : MvPFunctor.B (P F) a ⟹ α), abs { fst := a, snd := f } = x → u ∈ f i✝ '' univ
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ fun i => α i
xeq : x = abs { fst := a, snd := f }
h' : ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p i (f i j)
i : MvPFunctor.B (P F) a i✝
left✝ : i ∈ univ
hi : f i✝ i = u
⊢ p i✝ (f i✝ i)
[PROOFSTEP]
apply h'
[GOAL]
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
i : Fin2 n
x : F α
⊢ supp x i = {u | ∀ (a : (P F).A) (f : MvPFunctor.B (P F) a ⟹ α), abs { fst := a, snd := f } = x → u ∈ f i '' univ}
[PROOFSTEP]
ext
[GOAL]
case h
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
i : Fin2 n
x : F α
x✝ : α i
⊢ x✝ ∈ supp x i ↔
    x✝ ∈ {u | ∀ (a : (P F).A) (f : MvPFunctor.B (P F) a ⟹ α), abs { fst := a, snd := f } = x → u ∈ f i '' univ}
[PROOFSTEP]
apply mem_supp
[GOAL]
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
⊢ (∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u) ↔
    ∃ a f,
      abs { fst := a, snd := f } = x ∧
        ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
          abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ
[PROOFSTEP]
constructor
[GOAL]
case mp
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
⊢ (∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u) →
    ∃ a f,
      abs { fst := a, snd := f } = x ∧
        ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
          abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ
[PROOFSTEP]
intro h
[GOAL]
case mp
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
h : ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
⊢ ∃ a f,
    abs { fst := a, snd := f } = x ∧
      ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
        abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ
[PROOFSTEP]
have : LiftP (supp x) x := by rw [h]; introv ; exact id
[GOAL]
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
h : ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
⊢ LiftP (supp x) x
[PROOFSTEP]
rw [h]
[GOAL]
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
h : ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
⊢ ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → supp x i u
[PROOFSTEP]
introv
[GOAL]
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
h : ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
i : Fin2 n
u : α i
⊢ u ∈ supp x i → supp x i u
[PROOFSTEP]
exact id
[GOAL]
case mp
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
h : ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
this : LiftP (supp x) x
⊢ ∃ a f,
    abs { fst := a, snd := f } = x ∧
      ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
        abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ
[PROOFSTEP]
rw [liftP_iff] at this
[GOAL]
case mp
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
h : ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
this✝ : LiftP (supp x) x
this : ∃ a f, x = abs { fst := a, snd := f } ∧ ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), supp x i (f i j)
⊢ ∃ a f,
    abs { fst := a, snd := f } = x ∧
      ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
        abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ
[PROOFSTEP]
rcases this with ⟨a, f, xeq, h'⟩
[GOAL]
case mp.intro.intro.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
h : ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
this : LiftP (supp x) x
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ fun i => α i
xeq : x = abs { fst := a, snd := f }
h' : ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), supp x i (f i j)
⊢ ∃ a f,
    abs { fst := a, snd := f } = x ∧
      ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
        abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ
[PROOFSTEP]
refine' ⟨a, f, xeq.symm, _⟩
[GOAL]
case mp.intro.intro.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
h : ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
this : LiftP (supp x) x
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ fun i => α i
xeq : x = abs { fst := a, snd := f }
h' : ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), supp x i (f i j)
⊢ ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
    abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ
[PROOFSTEP]
intro a' f' h''
[GOAL]
case mp.intro.intro.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
h : ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
this : LiftP (supp x) x
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ fun i => α i
xeq : x = abs { fst := a, snd := f }
h' : ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), supp x i (f i j)
a' : Fin2 n
f' : (P F).A
h'' : MvPFunctor.B (P F) f' ⟹ α
⊢ abs { fst := f', snd := h'' } = x → f a' '' univ ⊆ h'' a' '' univ
[PROOFSTEP]
rintro hu u ⟨j, _h₂, hfi⟩
[GOAL]
case mp.intro.intro.intro.intro.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
h : ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
this : LiftP (supp x) x
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ fun i => α i
xeq : x = abs { fst := a, snd := f }
h' : ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), supp x i (f i j)
a' : Fin2 n
f' : (P F).A
h'' : MvPFunctor.B (P F) f' ⟹ α
hu : abs { fst := f', snd := h'' } = x
u : α a'
j : MvPFunctor.B (P F) a a'
_h₂ : j ∈ univ
hfi : f a' j = u
⊢ u ∈ h'' a' '' univ
[PROOFSTEP]
have hh : u ∈ supp x a' := by rw [← hfi]; apply h'
[GOAL]
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
h : ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
this : LiftP (supp x) x
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ fun i => α i
xeq : x = abs { fst := a, snd := f }
h' : ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), supp x i (f i j)
a' : Fin2 n
f' : (P F).A
h'' : MvPFunctor.B (P F) f' ⟹ α
hu : abs { fst := f', snd := h'' } = x
u : α a'
j : MvPFunctor.B (P F) a a'
_h₂ : j ∈ univ
hfi : f a' j = u
⊢ u ∈ supp x a'
[PROOFSTEP]
rw [← hfi]
[GOAL]
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
h : ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
this : LiftP (supp x) x
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ fun i => α i
xeq : x = abs { fst := a, snd := f }
h' : ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), supp x i (f i j)
a' : Fin2 n
f' : (P F).A
h'' : MvPFunctor.B (P F) f' ⟹ α
hu : abs { fst := f', snd := h'' } = x
u : α a'
j : MvPFunctor.B (P F) a a'
_h₂ : j ∈ univ
hfi : f a' j = u
⊢ f a' j ∈ supp x a'
[PROOFSTEP]
apply h'
[GOAL]
case mp.intro.intro.intro.intro.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
h : ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
this : LiftP (supp x) x
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ fun i => α i
xeq : x = abs { fst := a, snd := f }
h' : ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), supp x i (f i j)
a' : Fin2 n
f' : (P F).A
h'' : MvPFunctor.B (P F) f' ⟹ α
hu : abs { fst := f', snd := h'' } = x
u : α a'
j : MvPFunctor.B (P F) a a'
_h₂ : j ∈ univ
hfi : f a' j = u
hh : u ∈ supp x a'
⊢ u ∈ h'' a' '' univ
[PROOFSTEP]
refine' (mem_supp x _ u).mp hh _ _ hu
[GOAL]
case mpr
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
⊢ (∃ a f,
      abs { fst := a, snd := f } = x ∧
        ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
          abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ) →
    ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
[PROOFSTEP]
rintro ⟨a, f, xeq, h⟩ p
[GOAL]
case mpr.intro.intro.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
xeq : abs { fst := a, snd := f } = x
h :
  ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
    abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ
p : (i : Fin2 n) → α i → Prop
⊢ LiftP p x ↔ ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
[PROOFSTEP]
rw [liftP_iff]
[GOAL]
case mpr.intro.intro.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
xeq : abs { fst := a, snd := f } = x
h :
  ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
    abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ
p : (i : Fin2 n) → α i → Prop
⊢ (∃ a f, x = abs { fst := a, snd := f } ∧ ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p i (f i j)) ↔
    ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
[PROOFSTEP]
constructor
[GOAL]
case mpr.intro.intro.intro.mp
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
xeq : abs { fst := a, snd := f } = x
h :
  ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
    abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ
p : (i : Fin2 n) → α i → Prop
⊢ (∃ a f, x = abs { fst := a, snd := f } ∧ ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p i (f i j)) →
    ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
[PROOFSTEP]
rintro ⟨a', f', xeq', h'⟩ i u usuppx
[GOAL]
case mpr.intro.intro.intro.mp.intro.intro.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
xeq : abs { fst := a, snd := f } = x
h :
  ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
    abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ
p : (i : Fin2 n) → α i → Prop
a' : (P F).A
f' : MvPFunctor.B (P F) a' ⟹ fun i => α i
xeq' : x = abs { fst := a', snd := f' }
h' : ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a' i), p i (f' i j)
i : Fin2 n
u : α i
usuppx : u ∈ supp x i
⊢ p i u
[PROOFSTEP]
rcases(mem_supp x _ u).mp (@usuppx) a' f' xeq'.symm with ⟨i, _, f'ieq⟩
[GOAL]
case mpr.intro.intro.intro.mp.intro.intro.intro.intro.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
xeq : abs { fst := a, snd := f } = x
h :
  ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
    abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ
p : (i : Fin2 n) → α i → Prop
a' : (P F).A
f' : MvPFunctor.B (P F) a' ⟹ fun i => α i
xeq' : x = abs { fst := a', snd := f' }
h' : ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a' i), p i (f' i j)
i✝ : Fin2 n
u : α i✝
usuppx : u ∈ supp x i✝
i : MvPFunctor.B (P F) a' i✝
left✝ : i ∈ univ
f'ieq : f' i✝ i = u
⊢ p i✝ u
[PROOFSTEP]
rw [← f'ieq]
[GOAL]
case mpr.intro.intro.intro.mp.intro.intro.intro.intro.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
xeq : abs { fst := a, snd := f } = x
h :
  ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
    abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ
p : (i : Fin2 n) → α i → Prop
a' : (P F).A
f' : MvPFunctor.B (P F) a' ⟹ fun i => α i
xeq' : x = abs { fst := a', snd := f' }
h' : ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a' i), p i (f' i j)
i✝ : Fin2 n
u : α i✝
usuppx : u ∈ supp x i✝
i : MvPFunctor.B (P F) a' i✝
left✝ : i ∈ univ
f'ieq : f' i✝ i = u
⊢ p i✝ (f' i✝ i)
[PROOFSTEP]
apply h'
[GOAL]
case mpr.intro.intro.intro.mpr
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
xeq : abs { fst := a, snd := f } = x
h :
  ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
    abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ
p : (i : Fin2 n) → α i → Prop
⊢ (∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u) →
    ∃ a f, x = abs { fst := a, snd := f } ∧ ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p i (f i j)
[PROOFSTEP]
intro h'
[GOAL]
case mpr.intro.intro.intro.mpr
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
xeq : abs { fst := a, snd := f } = x
h :
  ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
    abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ
p : (i : Fin2 n) → α i → Prop
h' : ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
⊢ ∃ a f, x = abs { fst := a, snd := f } ∧ ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p i (f i j)
[PROOFSTEP]
refine' ⟨a, f, xeq.symm, _⟩
[GOAL]
case mpr.intro.intro.intro.mpr
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
xeq : abs { fst := a, snd := f } = x
h :
  ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
    abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ
p : (i : Fin2 n) → α i → Prop
h' : ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
⊢ ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p i (f i j)
[PROOFSTEP]
intro j y
[GOAL]
case mpr.intro.intro.intro.mpr
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
xeq : abs { fst := a, snd := f } = x
h :
  ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
    abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ
p : (i : Fin2 n) → α i → Prop
h' : ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
j : Fin2 n
y : MvPFunctor.B (P F) a j
⊢ p j (f j y)
[PROOFSTEP]
apply h'
[GOAL]
case mpr.intro.intro.intro.mpr.a
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
xeq : abs { fst := a, snd := f } = x
h :
  ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
    abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ
p : (i : Fin2 n) → α i → Prop
h' : ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
j : Fin2 n
y : MvPFunctor.B (P F) a j
⊢ f j y ∈ supp x j
[PROOFSTEP]
rw [mem_supp]
[GOAL]
case mpr.intro.intro.intro.mpr.a
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
xeq : abs { fst := a, snd := f } = x
h :
  ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
    abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ
p : (i : Fin2 n) → α i → Prop
h' : ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
j : Fin2 n
y : MvPFunctor.B (P F) a j
⊢ ∀ (a : (P F).A) (f_1 : MvPFunctor.B (P F) a ⟹ α), abs { fst := a, snd := f_1 } = x → f j y ∈ f_1 j '' univ
[PROOFSTEP]
intro a' f' xeq'
[GOAL]
case mpr.intro.intro.intro.mpr.a
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
xeq : abs { fst := a, snd := f } = x
h :
  ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
    abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ
p : (i : Fin2 n) → α i → Prop
h' : ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
j : Fin2 n
y : MvPFunctor.B (P F) a j
a' : (P F).A
f' : MvPFunctor.B (P F) a' ⟹ α
xeq' : abs { fst := a', snd := f' } = x
⊢ f j y ∈ f' j '' univ
[PROOFSTEP]
apply h _ a' f' xeq'
[GOAL]
case mpr.intro.intro.intro.mpr.a.a
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
xeq : abs { fst := a, snd := f } = x
h :
  ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
    abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ
p : (i : Fin2 n) → α i → Prop
h' : ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
j : Fin2 n
y : MvPFunctor.B (P F) a j
a' : (P F).A
f' : MvPFunctor.B (P F) a' ⟹ α
xeq' : abs { fst := a', snd := f' } = x
⊢ f j y ∈ f j '' univ
[PROOFSTEP]
apply mem_image_of_mem _ (mem_univ _)
[GOAL]
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
[PROOFSTEP]
intro
[GOAL]
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
[PROOFSTEP]
ext u
[GOAL]
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
[PROOFSTEP]
rw [mem_supp]
[GOAL]
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
[PROOFSTEP]
constructor
[GOAL]
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
[PROOFSTEP]
intro h'
[GOAL]
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
[PROOFSTEP]
apply h' _ _ rfl
[GOAL]
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
[PROOFSTEP]
intro h' a' f' e
[GOAL]
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
[PROOFSTEP]
rw [← h _ _ _ _ e.symm]
[GOAL]
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
[PROOFSTEP]
apply h'
[GOAL]
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : IsUniform
α : TypeVec n
x : F α
p : (i : Fin2 n) → α i → Prop
⊢ LiftP p x ↔ ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
[PROOFSTEP]
rw [liftP_iff, ← abs_repr x]
[GOAL]
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : IsUniform
α : TypeVec n
x : F α
p : (i : Fin2 n) → α i → Prop
⊢ (∃ a f, abs (repr x) = abs { fst := a, snd := f } ∧ ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p i (f i j)) ↔
    ∀ (i : Fin2 n) (u : α i), u ∈ supp (abs (repr x)) i → p i u
[PROOFSTEP]
cases' repr x with a f
[GOAL]
case mk
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : IsUniform
α : TypeVec n
x : F α
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
⊢ (∃ a_1 f_1,
      abs { fst := a, snd := f } = abs { fst := a_1, snd := f_1 } ∧
        ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a_1 i), p i (f_1 i j)) ↔
    ∀ (i : Fin2 n) (u : α i), u ∈ supp (abs { fst := a, snd := f }) i → p i u
[PROOFSTEP]
constructor
[GOAL]
case mk.mp
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : IsUniform
α : TypeVec n
x : F α
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
⊢ (∃ a_1 f_1,
      abs { fst := a, snd := f } = abs { fst := a_1, snd := f_1 } ∧
        ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a_1 i), p i (f_1 i j)) →
    ∀ (i : Fin2 n) (u : α i), u ∈ supp (abs { fst := a, snd := f }) i → p i u
[PROOFSTEP]
rintro ⟨a', f', abseq, hf⟩ u
[GOAL]
case mk.mp.intro.intro.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : IsUniform
α : TypeVec n
x : F α
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
a' : (P F).A
f' : MvPFunctor.B (P F) a' ⟹ fun i => α i
abseq : abs { fst := a, snd := f } = abs { fst := a', snd := f' }
hf : ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a' i), p i (f' i j)
u : Fin2 n
⊢ ∀ (u_1 : α u), u_1 ∈ supp (abs { fst := a, snd := f }) u → p u u_1
[PROOFSTEP]
rw [supp_eq_of_isUniform h, h _ _ _ _ abseq]
[GOAL]
case mk.mp.intro.intro.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : IsUniform
α : TypeVec n
x : F α
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
a' : (P F).A
f' : MvPFunctor.B (P F) a' ⟹ fun i => α i
abseq : abs { fst := a, snd := f } = abs { fst := a', snd := f' }
hf : ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a' i), p i (f' i j)
u : Fin2 n
⊢ ∀ (u_1 : α u), u_1 ∈ f' u '' univ → p u u_1
[PROOFSTEP]
rintro b ⟨i, _, hi⟩
[GOAL]
case mk.mp.intro.intro.intro.intro.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : IsUniform
α : TypeVec n
x : F α
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
a' : (P F).A
f' : MvPFunctor.B (P F) a' ⟹ fun i => α i
abseq : abs { fst := a, snd := f } = abs { fst := a', snd := f' }
hf : ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a' i), p i (f' i j)
u : Fin2 n
b : α u
i : MvPFunctor.B (P F) a' u
left✝ : i ∈ univ
hi : f' u i = b
⊢ p u b
[PROOFSTEP]
rw [← hi]
[GOAL]
case mk.mp.intro.intro.intro.intro.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : IsUniform
α : TypeVec n
x : F α
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
a' : (P F).A
f' : MvPFunctor.B (P F) a' ⟹ fun i => α i
abseq : abs { fst := a, snd := f } = abs { fst := a', snd := f' }
hf : ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a' i), p i (f' i j)
u : Fin2 n
b : α u
i : MvPFunctor.B (P F) a' u
left✝ : i ∈ univ
hi : f' u i = b
⊢ p u (f' u i)
[PROOFSTEP]
apply hf
[GOAL]
case mk.mpr
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : IsUniform
α : TypeVec n
x : F α
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
⊢ (∀ (i : Fin2 n) (u : α i), u ∈ supp (abs { fst := a, snd := f }) i → p i u) →
    ∃ a_2 f_1,
      abs { fst := a, snd := f } = abs { fst := a_2, snd := f_1 } ∧
        ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a_2 i), p i (f_1 i j)
[PROOFSTEP]
intro h'
[GOAL]
case mk.mpr
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : IsUniform
α : TypeVec n
x : F α
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
h' : ∀ (i : Fin2 n) (u : α i), u ∈ supp (abs { fst := a, snd := f }) i → p i u
⊢ ∃ a_1 f_1,
    abs { fst := a, snd := f } = abs { fst := a_1, snd := f_1 } ∧
      ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a_1 i), p i (f_1 i j)
[PROOFSTEP]
refine' ⟨a, f, rfl, fun _ i => h' _ _ _⟩
[GOAL]
case mk.mpr
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : IsUniform
α : TypeVec n
x : F α
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
h' : ∀ (i : Fin2 n) (u : α i), u ∈ supp (abs { fst := a, snd := f }) i → p i u
x✝ : Fin2 n
i : MvPFunctor.B (P F) a x✝
⊢ f x✝ i ∈ supp (abs { fst := a, snd := f }) x✝
[PROOFSTEP]
rw [supp_eq_of_isUniform h]
[GOAL]
case mk.mpr
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : IsUniform
α : TypeVec n
x : F α
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
h' : ∀ (i : Fin2 n) (u : α i), u ∈ supp (abs { fst := a, snd := f }) i → p i u
x✝ : Fin2 n
i : MvPFunctor.B (P F) a x✝
⊢ f x✝ i ∈ f x✝ '' univ
[PROOFSTEP]
exact ⟨i, mem_univ i, rfl⟩
[GOAL]
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : IsUniform
α β : TypeVec n
g : α ⟹ β
x : F α
i : Fin2 n
⊢ supp (g <$$> x) i = g i '' supp x i
[PROOFSTEP]
rw [← abs_repr x]
[GOAL]
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : IsUniform
α β : TypeVec n
g : α ⟹ β
x : F α
i : Fin2 n
⊢ supp (g <$$> abs (repr x)) i = g i '' supp (abs (repr x)) i
[PROOFSTEP]
cases' repr x with a f
[GOAL]
case mk
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : IsUniform
α β : TypeVec n
g : α ⟹ β
x : F α
i : Fin2 n
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
⊢ supp (g <$$> abs { fst := a, snd := f }) i = g i '' supp (abs { fst := a, snd := f }) i
[PROOFSTEP]
rw [← abs_map, MvPFunctor.map_eq]
[GOAL]
case mk
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : IsUniform
α β : TypeVec n
g : α ⟹ β
x : F α
i : Fin2 n
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
⊢ supp (abs { fst := a, snd := g ⊚ f }) i = g i '' supp (abs { fst := a, snd := f }) i
[PROOFSTEP]
rw [supp_eq_of_isUniform h, supp_eq_of_isUniform h, ← image_comp]
[GOAL]
case mk
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : IsUniform
α β : TypeVec n
g : α ⟹ β
x : F α
i : Fin2 n
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
⊢ (g ⊚ f) i '' univ = g i ∘ f i '' univ
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
⊢ SuppPreservation ↔ IsUniform
[PROOFSTEP]
constructor
[GOAL]
case mp
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
⊢ SuppPreservation → IsUniform
[PROOFSTEP]
intro h α a a' f f' h' i
[GOAL]
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
[PROOFSTEP]
rw [← MvPFunctor.supp_eq, ← MvPFunctor.supp_eq, ← h, h', h]
[GOAL]
case mpr
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
⊢ IsUniform → SuppPreservation
[PROOFSTEP]
rintro h α ⟨a, f⟩
[GOAL]
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 }
[PROOFSTEP]
ext
[GOAL]
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✝¹
[PROOFSTEP]
rwa [supp_eq_of_isUniform, MvPFunctor.supp_eq]
[GOAL]
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
⊢ SuppPreservation ↔ LiftPPreservation
[PROOFSTEP]
constructor
[GOAL]
case mp
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
⊢ SuppPreservation → LiftPPreservation
[PROOFSTEP]
intro h
[GOAL]
case mpr
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
⊢ LiftPPreservation → SuppPreservation
[PROOFSTEP]
intro h
[GOAL]
case mp
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : SuppPreservation
⊢ LiftPPreservation
[PROOFSTEP]
rintro α p ⟨a, f⟩
[GOAL]
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 }
[PROOFSTEP]
have h' := h
[GOAL]
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 }
[PROOFSTEP]
rw [suppPreservation_iff_isUniform] at h'
[GOAL]
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 }
[PROOFSTEP]
dsimp only [SuppPreservation, supp] at h
[GOAL]
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 }
[PROOFSTEP]
simp only [liftP_iff_of_isUniform, supp_eq_of_isUniform, MvPFunctor.liftP_iff', h', image_univ, mem_range, exists_imp]
[GOAL]
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)
[PROOFSTEP]
constructor
[GOAL]
case mp.mk.mp
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)
[PROOFSTEP]
intros
[GOAL]
case mp.mk.mpr
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) (x : MvPFunctor.B (P F) a i), p (f i x)) →
    ∀ (i : Fin2 n) (u : α i) (x : MvPFunctor.B (P F) a i), f i x = u → p u
[PROOFSTEP]
intros
[GOAL]
case mp.mk.mp
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
a✝ : ∀ (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✝)
[PROOFSTEP]
subst_vars
[GOAL]
case mp.mk.mpr
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
a✝¹ : ∀ (i : Fin2 n) (x : MvPFunctor.B (P F) a i), p (f i x)
i✝ : Fin2 n
u✝ : α i✝
x✝ : MvPFunctor.B (P F) a i✝
a✝ : f i✝ x✝ = u✝
⊢ p u✝
[PROOFSTEP]
subst_vars
[GOAL]
case mp.mk.mp
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
a✝ : ∀ (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✝)
[PROOFSTEP]
solve_by_elim
[GOAL]
case mp.mk.mpr
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
a✝ : ∀ (i : Fin2 n) (x : MvPFunctor.B (P F) a i), p (f i x)
i✝ : Fin2 n
x✝ : MvPFunctor.B (P F) a i✝
⊢ p (f i✝ x✝)
[PROOFSTEP]
solve_by_elim
[GOAL]
case mpr
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : LiftPPreservation
⊢ SuppPreservation
[PROOFSTEP]
rintro α ⟨a, f⟩
[GOAL]
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 }
[PROOFSTEP]
simp only [LiftPPreservation] at h
[GOAL]
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 }
[PROOFSTEP]
ext
[GOAL]
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✝¹
[PROOFSTEP]
simp only [supp, h, mem_setOf_eq]
[GOAL]
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
⊢ LiftPPreservation ↔ IsUniform
[PROOFSTEP]
rw [← suppPreservation_iff_liftpPreservation, suppPreservation_iff_isUniform]


[GOAL]
n : ℕ
i : Fin2 n
⊢ ∀ {α : TypeVec n} (x : Prj i α), abs i (repr i x) = x
[PROOFSTEP]
intros
[GOAL]
n : ℕ
i : Fin2 n
α✝ : TypeVec n
x✝ : Prj i α✝
⊢ abs i (repr i x✝) = x✝
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
i : Fin2 n
⊢ ∀ {α β : TypeVec n} (f : α ⟹ β) (p : MvPFunctor.Obj (P i) α), abs i (f <$$> p) = f <$$> abs i p
[PROOFSTEP]
intros α β f P
[GOAL]
n : ℕ
i : Fin2 n
α β : TypeVec n
f : α ⟹ β
P : MvPFunctor.Obj (MvQPF.Prj.P i) α
⊢ abs i (f <$$> P) = f <$$> abs i P
[PROOFSTEP]
cases P
[GOAL]
case mk
n : ℕ
i : Fin2 n
α β : TypeVec n
f : α ⟹ β
fst✝ : (P i).A
snd✝ : MvPFunctor.B (P i) fst✝ ⟹ α
⊢ abs i (f <$$> { fst := fst✝, snd := snd✝ }) = f <$$> abs i { fst := fst✝, snd := snd✝ }
[PROOFSTEP]
rfl