[GOAL]
n m : ℕ
P : MvPFunctor n
A : Type u
α β : TypeVec n
f : α ⟹ β
x : Obj (const n A) α
⊢ get (f <$$> x) = get x
[PROOFSTEP]
cases x
[GOAL]
case mk
n m : ℕ
P : MvPFunctor n
A : Type u
α β : TypeVec n
f : α ⟹ β
fst✝ : (const n A).A
snd✝ : B (const n A) fst✝ ⟹ α
⊢ get (f <$$> { fst := fst✝, snd := snd✝ }) = get { fst := fst✝, snd := snd✝ }
[PROOFSTEP]
rfl
[GOAL]
n m : ℕ
P : MvPFunctor n
A : Type u
α β : TypeVec n
x : A
⊢ get (mk n x) = x
[PROOFSTEP]
rfl
[GOAL]
n m : ℕ
P : MvPFunctor n
A : Type u
α β : TypeVec n
x : Obj (const n A) α
⊢ mk n (get x) = x
[PROOFSTEP]
cases x
[GOAL]
case mk
n m : ℕ
P : MvPFunctor n
A : Type u
α β : TypeVec n
fst✝ : (const n A).A
snd✝ : B (const n A) fst✝ ⟹ α
⊢ mk n (get { fst := fst✝, snd := snd✝ }) = { fst := fst✝, snd := snd✝ }
[PROOFSTEP]
dsimp [const.get, const.mk]
[GOAL]
case mk
n m : ℕ
P : MvPFunctor n
A : Type u
α β : TypeVec n
fst✝ : (const n A).A
snd✝ : B (const n A) fst✝ ⟹ α
⊢ { fst := fst✝, snd := fun x a => PEmpty.elim a } = { fst := fst✝, snd := snd✝ }
[PROOFSTEP]
congr with (_⟨⟩)
[GOAL]
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α β : TypeVec m
f : α ⟹ β
x : Obj (comp P Q) α
⊢ get (f <$$> x) = (fun i x => f <$$> x) <$$> get x
[PROOFSTEP]
rfl
[GOAL]
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α β : TypeVec m
x : Obj P fun i => Obj (Q i) α
⊢ get (mk x) = x
[PROOFSTEP]
rfl
[GOAL]
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α β : TypeVec m
x : Obj (comp P Q) α
⊢ mk (get x) = x
[PROOFSTEP]
rfl
[GOAL]
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : Obj P α
⊢ LiftP p x ↔ ∃ a f, x = { fst := a, snd := f } ∧ ∀ (i : Fin2 n) (j : B P a i), p (f i j)
[PROOFSTEP]
constructor
[GOAL]
case mp
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : Obj P α
⊢ LiftP p x → ∃ a f, x = { fst := a, snd := f } ∧ ∀ (i : Fin2 n) (j : B P a i), p (f i j)
[PROOFSTEP]
rintro ⟨y, hy⟩
[GOAL]
case mp.intro
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : Obj P α
y : Obj P fun i => Subtype p
hy : (fun i => Subtype.val) <$$> y = x
⊢ ∃ a f, x = { fst := a, snd := f } ∧ ∀ (i : Fin2 n) (j : B P a i), p (f i j)
[PROOFSTEP]
cases' h : y with a f
[GOAL]
case mp.intro.mk
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : Obj P α
y : Obj P fun i => Subtype p
hy : (fun i => Subtype.val) <$$> y = x
a : P.A
f : B P a ⟹ fun i => Subtype p
h : y = { fst := a, snd := f }
⊢ ∃ a f, x = { fst := a, snd := f } ∧ ∀ (i : Fin2 n) (j : B P a i), p (f i j)
[PROOFSTEP]
refine' ⟨a, fun i j => (f i j).val, _, fun i j => (f i j).property⟩
[GOAL]
case mp.intro.mk
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : Obj P α
y : Obj P fun i => Subtype p
hy : (fun i => Subtype.val) <$$> y = x
a : P.A
f : B P a ⟹ fun i => Subtype p
h : y = { fst := a, snd := f }
⊢ x = { fst := a, snd := fun i j => ↑(f i j) }
[PROOFSTEP]
rw [← hy, h, map_eq]
[GOAL]
case mp.intro.mk
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : Obj P α
y : Obj P fun i => Subtype p
hy : (fun i => Subtype.val) <$$> y = x
a : P.A
f : B P a ⟹ fun i => Subtype p
h : y = { fst := a, snd := f }
⊢ { fst := a, snd := (fun i => Subtype.val) ⊚ f } = { fst := a, snd := fun i j => ↑(f i j) }
[PROOFSTEP]
rfl
[GOAL]
case mpr
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : Obj P α
⊢ (∃ a f, x = { fst := a, snd := f } ∧ ∀ (i : Fin2 n) (j : B P a i), p (f i j)) → LiftP p x
[PROOFSTEP]
rintro ⟨a, f, xeq, pf⟩
[GOAL]
case mpr.intro.intro.intro
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : Obj P α
a : P.A
f : B P a ⟹ α
xeq : x = { fst := a, snd := f }
pf : ∀ (i : Fin2 n) (j : B P a i), p (f i j)
⊢ LiftP p x
[PROOFSTEP]
use⟨a, fun i j => ⟨f i j, pf i j⟩⟩
[GOAL]
case h
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : Obj P α
a : P.A
f : B P a ⟹ α
xeq : x = { fst := a, snd := f }
pf : ∀ (i : Fin2 n) (j : B P a i), p (f i j)
⊢ (fun i => Subtype.val) <$$> { fst := a, snd := fun i j => { val := f i j, property := (_ : p (f i j)) } } = x
[PROOFSTEP]
rw [xeq]
[GOAL]
case h
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : Obj P α
a : P.A
f : B P a ⟹ α
xeq : x = { fst := a, snd := f }
pf : ∀ (i : Fin2 n) (j : B P a i), p (f i j)
⊢ (fun i => Subtype.val) <$$> { fst := a, snd := fun i j => { val := f i j, property := (_ : p (f i j)) } } =
    { fst := a, snd := f }
[PROOFSTEP]
rfl
[GOAL]
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : B P a ⟹ α
⊢ LiftP p { fst := a, snd := f } ↔ ∀ (i : Fin2 n) (x : B P a i), p (f i x)
[PROOFSTEP]
simp only [liftP_iff, Sigma.mk.inj_iff]
[GOAL]
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : B P a ⟹ α
⊢ (∃ a_1 f_1, { fst := a, snd := f } = { fst := a_1, snd := f_1 } ∧ ∀ (i : Fin2 n) (j : B P a_1 i), p (f_1 i j)) ↔
    ∀ (i : Fin2 n) (x : B P a i), p (f i x)
[PROOFSTEP]
constructor
[GOAL]
case mp
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : B P a ⟹ α
⊢ (∃ a_1 f_1, { fst := a, snd := f } = { fst := a_1, snd := f_1 } ∧ ∀ (i : Fin2 n) (j : B P a_1 i), p (f_1 i j)) →
    ∀ (i : Fin2 n) (x : B P a i), p (f i x)
[PROOFSTEP]
rintro ⟨_, _, ⟨⟩, _⟩
[GOAL]
case mp.intro.intro.intro.refl
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : B P a ⟹ α
right✝ : ∀ (i : Fin2 n) (j : B P a i), p (f i j)
⊢ ∀ (i : Fin2 n) (x : B P a i), p (f i x)
[PROOFSTEP]
assumption
[GOAL]
case mpr
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : B P a ⟹ α
⊢ (∀ (i : Fin2 n) (x : B P a i), p (f i x)) →
    ∃ a_2 f_1, { fst := a, snd := f } = { fst := a_2, snd := f_1 } ∧ ∀ (i : Fin2 n) (j : B P a_2 i), p (f_1 i j)
[PROOFSTEP]
intro
[GOAL]
case mpr
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : B P a ⟹ α
a✝ : ∀ (i : Fin2 n) (x : B P a i), p (f i x)
⊢ ∃ a_1 f_1, { fst := a, snd := f } = { fst := a_1, snd := f_1 } ∧ ∀ (i : Fin2 n) (j : B P a_1 i), p (f_1 i j)
[PROOFSTEP]
repeat'
  first
  | constructor
  | assumption
[GOAL]
case mpr
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : B P a ⟹ α
a✝ : ∀ (i : Fin2 n) (x : B P a i), p (f i x)
⊢ ∃ a_1 f_1, { fst := a, snd := f } = { fst := a_1, snd := f_1 } ∧ ∀ (i : Fin2 n) (j : B P a_1 i), p (f_1 i j)
[PROOFSTEP]
first
| constructor
| assumption
[GOAL]
case mpr
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : B P a ⟹ α
a✝ : ∀ (i : Fin2 n) (x : B P a i), p (f i x)
⊢ ∃ a_1 f_1, { fst := a, snd := f } = { fst := a_1, snd := f_1 } ∧ ∀ (i : Fin2 n) (j : B P a_1 i), p (f_1 i j)
[PROOFSTEP]
constructor
[GOAL]
case mpr.h
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : B P a ⟹ α
a✝ : ∀ (i : Fin2 n) (x : B P a i), p (f i x)
⊢ ∃ f_1, { fst := a, snd := f } = { fst := ?mpr.w, snd := f_1 } ∧ ∀ (i : Fin2 n) (j : B P ?mpr.w i), p (f_1 i j)
[PROOFSTEP]
first
| constructor
| assumption
[GOAL]
case mpr.h
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : B P a ⟹ α
a✝ : ∀ (i : Fin2 n) (x : B P a i), p (f i x)
⊢ ∃ f_1, { fst := a, snd := f } = { fst := ?mpr.w, snd := f_1 } ∧ ∀ (i : Fin2 n) (j : B P ?mpr.w i), p (f_1 i j)
[PROOFSTEP]
constructor
[GOAL]
case mpr.h.h
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : B P a ⟹ α
a✝ : ∀ (i : Fin2 n) (x : B P a i), p (f i x)
⊢ { fst := a, snd := f } = { fst := ?mpr.w, snd := ?mpr.h.w } ∧ ∀ (i : Fin2 n) (j : B P ?mpr.w i), p (?mpr.h.w i j)
[PROOFSTEP]
first
| constructor
| assumption
[GOAL]
case mpr.h.h
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : B P a ⟹ α
a✝ : ∀ (i : Fin2 n) (x : B P a i), p (f i x)
⊢ { fst := a, snd := f } = { fst := ?mpr.w, snd := ?mpr.h.w } ∧ ∀ (i : Fin2 n) (j : B P ?mpr.w i), p (?mpr.h.w i j)
[PROOFSTEP]
constructor
[GOAL]
case mpr.h.h.left
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : B P a ⟹ α
a✝ : ∀ (i : Fin2 n) (x : B P a i), p (f i x)
⊢ { fst := a, snd := f } = { fst := ?mpr.w, snd := ?mpr.h.w }
[PROOFSTEP]
first
| constructor
| assumption
[GOAL]
case mpr.h.h.left
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : B P a ⟹ α
a✝ : ∀ (i : Fin2 n) (x : B P a i), p (f i x)
⊢ { fst := a, snd := f } = { fst := ?mpr.w, snd := ?mpr.h.w }
[PROOFSTEP]
constructor
[GOAL]
case mpr.h.h.right
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : B P a ⟹ α
a✝ : ∀ (i : Fin2 n) (x : B P a i), p (f i x)
⊢ ∀ (i : Fin2 n) (j : B P a i), p (f i j)
[PROOFSTEP]
first
| constructor
| assumption
[GOAL]
case mpr.h.h.right
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : B P a ⟹ α
a✝ : ∀ (i : Fin2 n) (x : B P a i), p (f i x)
⊢ ∀ (i : Fin2 n) (j : B P a i), p (f i j)
[PROOFSTEP]
constructor
[GOAL]
case mpr.h.h.right
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : B P a ⟹ α
a✝ : ∀ (i : Fin2 n) (x : B P a i), p (f i x)
⊢ ∀ (i : Fin2 n) (j : B P a i), p (f i j)
[PROOFSTEP]
assumption
[GOAL]
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : Obj P α
⊢ LiftR r x y ↔
    ∃ a f₀ f₁,
      x = { fst := a, snd := f₀ } ∧ y = { fst := a, snd := f₁ } ∧ ∀ (i : Fin2 n) (j : B P a i), r (f₀ i j) (f₁ i j)
[PROOFSTEP]
constructor
[GOAL]
case mp
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : Obj P α
⊢ LiftR r x y →
    ∃ a f₀ f₁,
      x = { fst := a, snd := f₀ } ∧ y = { fst := a, snd := f₁ } ∧ ∀ (i : Fin2 n) (j : B P a i), r (f₀ i j) (f₁ i j)
[PROOFSTEP]
rintro ⟨u, xeq, yeq⟩
[GOAL]
case mp.intro.intro
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : Obj P α
u : Obj P fun i => { p // 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 = { fst := a, snd := f₀ } ∧ y = { fst := a, snd := f₁ } ∧ ∀ (i : Fin2 n) (j : B P a i), r (f₀ i j) (f₁ i j)
[PROOFSTEP]
cases' h : u with a f
[GOAL]
case mp.intro.intro.mk
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : Obj P α
u : Obj P fun i => { p // r p.fst p.snd }
xeq : (fun i t => (↑t).fst) <$$> u = x
yeq : (fun i t => (↑t).snd) <$$> u = y
a : P.A
f : B P a ⟹ fun i => { p // r p.fst p.snd }
h : u = { fst := a, snd := f }
⊢ ∃ a f₀ f₁,
    x = { fst := a, snd := f₀ } ∧ y = { fst := a, snd := f₁ } ∧ ∀ (i : Fin2 n) (j : B P 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 m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : Obj P α
u : Obj P fun i => { p // r p.fst p.snd }
xeq : (fun i t => (↑t).fst) <$$> u = x
yeq : (fun i t => (↑t).snd) <$$> u = y
a : P.A
f : B P a ⟹ fun i => { p // r p.fst p.snd }
h : u = { fst := a, snd := f }
⊢ x = { fst := a, snd := fun i j => (↑(f i j)).fst } ∧
    y = { fst := a, snd := fun i j => (↑(f i j)).snd } ∧ ∀ (i : Fin2 n) (j : B P a i), r (↑(f i j)).fst (↑(f i j)).snd
[PROOFSTEP]
constructor
[GOAL]
case h.left
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : Obj P α
u : Obj P fun i => { p // r p.fst p.snd }
xeq : (fun i t => (↑t).fst) <$$> u = x
yeq : (fun i t => (↑t).snd) <$$> u = y
a : P.A
f : B P a ⟹ fun i => { p // r p.fst p.snd }
h : u = { fst := a, snd := f }
⊢ x = { fst := a, snd := fun i j => (↑(f i j)).fst }
[PROOFSTEP]
rw [← xeq, h]
[GOAL]
case h.left
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : Obj P α
u : Obj P fun i => { p // r p.fst p.snd }
xeq : (fun i t => (↑t).fst) <$$> u = x
yeq : (fun i t => (↑t).snd) <$$> u = y
a : P.A
f : B P a ⟹ fun i => { p // r p.fst p.snd }
h : u = { fst := a, snd := f }
⊢ (fun i t => (↑t).fst) <$$> { fst := a, snd := f } = { fst := a, snd := fun i j => (↑(f i j)).fst }
[PROOFSTEP]
rfl
[GOAL]
case h.right
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : Obj P α
u : Obj P fun i => { p // r p.fst p.snd }
xeq : (fun i t => (↑t).fst) <$$> u = x
yeq : (fun i t => (↑t).snd) <$$> u = y
a : P.A
f : B P a ⟹ fun i => { p // r p.fst p.snd }
h : u = { fst := a, snd := f }
⊢ y = { fst := a, snd := fun i j => (↑(f i j)).snd } ∧ ∀ (i : Fin2 n) (j : B P a i), r (↑(f i j)).fst (↑(f i j)).snd
[PROOFSTEP]
constructor
[GOAL]
case h.right.left
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : Obj P α
u : Obj P fun i => { p // r p.fst p.snd }
xeq : (fun i t => (↑t).fst) <$$> u = x
yeq : (fun i t => (↑t).snd) <$$> u = y
a : P.A
f : B P a ⟹ fun i => { p // r p.fst p.snd }
h : u = { fst := a, snd := f }
⊢ y = { fst := a, snd := fun i j => (↑(f i j)).snd }
[PROOFSTEP]
rw [← yeq, h]
[GOAL]
case h.right.left
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : Obj P α
u : Obj P fun i => { p // r p.fst p.snd }
xeq : (fun i t => (↑t).fst) <$$> u = x
yeq : (fun i t => (↑t).snd) <$$> u = y
a : P.A
f : B P a ⟹ fun i => { p // r p.fst p.snd }
h : u = { fst := a, snd := f }
⊢ (fun i t => (↑t).snd) <$$> { fst := a, snd := f } = { fst := a, snd := fun i j => (↑(f i j)).snd }
[PROOFSTEP]
rfl
[GOAL]
case h.right.right
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : Obj P α
u : Obj P fun i => { p // r p.fst p.snd }
xeq : (fun i t => (↑t).fst) <$$> u = x
yeq : (fun i t => (↑t).snd) <$$> u = y
a : P.A
f : B P a ⟹ fun i => { p // r p.fst p.snd }
h : u = { fst := a, snd := f }
⊢ ∀ (i : Fin2 n) (j : B P a i), r (↑(f i j)).fst (↑(f i j)).snd
[PROOFSTEP]
intro i j
[GOAL]
case h.right.right
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : Obj P α
u : Obj P fun i => { p // r p.fst p.snd }
xeq : (fun i t => (↑t).fst) <$$> u = x
yeq : (fun i t => (↑t).snd) <$$> u = y
a : P.A
f : B P a ⟹ fun i => { p // r p.fst p.snd }
h : u = { fst := a, snd := f }
i : Fin2 n
j : B P a i
⊢ r (↑(f i j)).fst (↑(f i j)).snd
[PROOFSTEP]
exact (f i j).property
[GOAL]
case mpr
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : Obj P α
⊢ (∃ a f₀ f₁,
      x = { fst := a, snd := f₀ } ∧ y = { fst := a, snd := f₁ } ∧ ∀ (i : Fin2 n) (j : B P a i), r (f₀ i j) (f₁ i j)) →
    LiftR r x y
[PROOFSTEP]
rintro ⟨a, f₀, f₁, xeq, yeq, h⟩
[GOAL]
case mpr.intro.intro.intro.intro.intro
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : Obj P α
a : P.A
f₀ f₁ : B P a ⟹ α
xeq : x = { fst := a, snd := f₀ }
yeq : y = { fst := a, snd := f₁ }
h : ∀ (i : Fin2 n) (j : B P a i), r (f₀ i j) (f₁ i j)
⊢ LiftR r x y
[PROOFSTEP]
use⟨a, fun i j => ⟨(f₀ i j, f₁ i j), h i j⟩⟩
[GOAL]
case h
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : Obj P α
a : P.A
f₀ f₁ : B P a ⟹ α
xeq : x = { fst := a, snd := f₀ }
yeq : y = { fst := a, snd := f₁ }
h : ∀ (i : Fin2 n) (j : B P a i), r (f₀ i j) (f₁ i j)
⊢ (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)) } } =
      x ∧
    (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)) } } =
      y
[PROOFSTEP]
dsimp
[GOAL]
case h
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : Obj P α
a : P.A
f₀ f₁ : B P a ⟹ α
xeq : x = { fst := a, snd := f₀ }
yeq : y = { fst := a, snd := f₁ }
h : ∀ (i : Fin2 n) (j : B P a i), r (f₀ i j) (f₁ i j)
⊢ (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)) } } =
      x ∧
    (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)) } } =
      y
[PROOFSTEP]
constructor
[GOAL]
case h.left
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : Obj P α
a : P.A
f₀ f₁ : B P a ⟹ α
xeq : x = { fst := a, snd := f₀ }
yeq : y = { fst := a, snd := f₁ }
h : ∀ (i : Fin2 n) (j : B P a i), r (f₀ i j) (f₁ i j)
⊢ (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)) } } =
    x
[PROOFSTEP]
rw [xeq]
[GOAL]
case h.left
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : Obj P α
a : P.A
f₀ f₁ : B P a ⟹ α
xeq : x = { fst := a, snd := f₀ }
yeq : y = { fst := a, snd := f₁ }
h : ∀ (i : Fin2 n) (j : B P a i), r (f₀ i j) (f₁ i j)
⊢ (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)) } } =
    { fst := a, snd := f₀ }
[PROOFSTEP]
rfl
[GOAL]
case h.right
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : Obj P α
a : P.A
f₀ f₁ : B P a ⟹ α
xeq : x = { fst := a, snd := f₀ }
yeq : y = { fst := a, snd := f₁ }
h : ∀ (i : Fin2 n) (j : B P a i), r (f₀ i j) (f₁ i j)
⊢ (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)) } } =
    y
[PROOFSTEP]
rw [yeq]
[GOAL]
case h.right
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : Obj P α
a : P.A
f₀ f₁ : B P a ⟹ α
xeq : x = { fst := a, snd := f₀ }
yeq : y = { fst := a, snd := f₁ }
h : ∀ (i : Fin2 n) (j : B P a i), r (f₀ i j) (f₁ i j)
⊢ (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)) } } =
    { fst := a, snd := f₁ }
[PROOFSTEP]
rfl
[GOAL]
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
[PROOFSTEP]
ext x
[GOAL]
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
[PROOFSTEP]
simp only [supp, image_univ, mem_range, mem_setOf_eq]
[GOAL]
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
[PROOFSTEP]
constructor
[GOAL]
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
⊢ (∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, LiftP P_1 { fst := a, snd := f } → P_1 i x) → ∃ y, f i y = x
[PROOFSTEP]
intro h
[GOAL]
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
⊢ (∃ y, f i y = x) → ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, LiftP P_1 { fst := a, snd := f } → P_1 i x
[PROOFSTEP]
intro h
[GOAL]
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
[PROOFSTEP]
apply @h fun i x => ∃ y : P.B a i, f i y = x
[GOAL]
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 }
[PROOFSTEP]
rw [liftP_iff']
[GOAL]
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
[PROOFSTEP]
intros
[GOAL]
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✝
[PROOFSTEP]
refine' ⟨_, rfl⟩
[GOAL]
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
[PROOFSTEP]
simp only [liftP_iff']
[GOAL]
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
[PROOFSTEP]
cases h
[GOAL]
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
[PROOFSTEP]
subst x
[GOAL]
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✝)
[PROOFSTEP]
tauto


[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι → Type u_4
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x : (i : ι) × α i
i✝ j : ι
a : α i✝
i : ι
⊢ range (Sigma.mk i) = Sigma.fst ⁻¹' {i}
[PROOFSTEP]
apply Subset.antisymm
[GOAL]
case h₁
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι → Type u_4
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x : (i : ι) × α i
i✝ j : ι
a : α i✝
i : ι
⊢ range (Sigma.mk i) ⊆ Sigma.fst ⁻¹' {i}
[PROOFSTEP]
rintro _ ⟨b, rfl⟩
[GOAL]
case h₁.intro
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι → Type u_4
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x : (i : ι) × α i
i✝ j : ι
a : α i✝
i : ι
b : α i
⊢ { fst := i, snd := b } ∈ Sigma.fst ⁻¹' {i}
[PROOFSTEP]
simp
[GOAL]
case h₂
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι → Type u_4
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x : (i : ι) × α i
i✝ j : ι
a : α i✝
i : ι
⊢ Sigma.fst ⁻¹' {i} ⊆ range (Sigma.mk i)
[PROOFSTEP]
rintro ⟨x, y⟩ (rfl | _)
[GOAL]
case h₂.mk.refl
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι → Type u_4
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x✝ : (i : ι) × α i
i j : ι
a : α i
x : ι
y : α x
⊢ { fst := x, snd := y } ∈ range (Sigma.mk { fst := x, snd := y }.fst)
[PROOFSTEP]
exact mem_range_self y
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι → Type u_4
s✝ s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x : (i : ι) × α i
i j : ι
a : α i
h : i ≠ j
s : Set (α j)
⊢ Sigma.mk i ⁻¹' (Sigma.mk j '' s) = ∅
[PROOFSTEP]
ext x
[GOAL]
case h
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι → Type u_4
s✝ s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x✝ : (i : ι) × α i
i j : ι
a : α i
h : i ≠ j
s : Set (α j)
x : α i
⊢ x ∈ Sigma.mk i ⁻¹' (Sigma.mk j '' s) ↔ x ∈ ∅
[PROOFSTEP]
simp [h.symm]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β✝ : ι → Type u_4
s✝ s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x : (i : ι) × α i
i✝ j : ι
a : α i✝
β : ι' → Type u_5
f : ι → ι'
hf : Function.Injective f
g : (i : ι) → α i → β (f i)
i : ι
s : Set (β (f i))
⊢ Sigma.mk i '' (g i ⁻¹' s) = Sigma.map f g ⁻¹' (Sigma.mk (f i) '' s)
[PROOFSTEP]
refine' (image_sigmaMk_preimage_sigmaMap_subset f g i s).antisymm _
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β✝ : ι → Type u_4
s✝ s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x : (i : ι) × α i
i✝ j : ι
a : α i✝
β : ι' → Type u_5
f : ι → ι'
hf : Function.Injective f
g : (i : ι) → α i → β (f i)
i : ι
s : Set (β (f i))
⊢ Sigma.map f g ⁻¹' (Sigma.mk (f i) '' s) ⊆ Sigma.mk i '' (g i ⁻¹' s)
[PROOFSTEP]
rintro ⟨j, x⟩ ⟨y, hys, hxy⟩
[GOAL]
case mk.intro.intro
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β✝ : ι → Type u_4
s✝ s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x✝ : (i : ι) × α i
i✝ j✝ : ι
a : α i✝
β : ι' → Type u_5
f : ι → ι'
hf : Function.Injective f
g : (i : ι) → α i → β (f i)
i : ι
s : Set (β (f i))
j : ι
x : α j
y : β (f i)
hys : y ∈ s
hxy : { fst := f i, snd := y } = Sigma.map f g { fst := j, snd := x }
⊢ { fst := j, snd := x } ∈ Sigma.mk i '' (g i ⁻¹' s)
[PROOFSTEP]
simp only [hf.eq_iff, Sigma.map, Sigma.ext_iff] at hxy
[GOAL]
case mk.intro.intro
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β✝ : ι → Type u_4
s✝ s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x✝ : (i : ι) × α i
i✝ j✝ : ι
a : α i✝
β : ι' → Type u_5
f : ι → ι'
hf : Function.Injective f
g : (i : ι) → α i → β (f i)
i : ι
s : Set (β (f i))
j : ι
x : α j
y : β (f i)
hys : y ∈ s
hxy : i = j ∧ HEq y (g j x)
⊢ { fst := j, snd := x } ∈ Sigma.mk i '' (g i ⁻¹' s)
[PROOFSTEP]
rcases hxy with ⟨rfl, hxy⟩
[GOAL]
case mk.intro.intro.intro
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β✝ : ι → Type u_4
s✝ s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x✝ : (i : ι) × α i
i✝ j : ι
a : α i✝
β : ι' → Type u_5
f : ι → ι'
hf : Function.Injective f
g : (i : ι) → α i → β (f i)
i : ι
s : Set (β (f i))
y : β (f i)
hys : y ∈ s
x : α i
hxy : HEq y (g i x)
⊢ { fst := i, snd := x } ∈ Sigma.mk i '' (g i ⁻¹' s)
[PROOFSTEP]
rw [heq_iff_eq] at hxy
[GOAL]
case mk.intro.intro.intro
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β✝ : ι → Type u_4
s✝ s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x✝ : (i : ι) × α i
i✝ j : ι
a : α i✝
β : ι' → Type u_5
f : ι → ι'
hf : Function.Injective f
g : (i : ι) → α i → β (f i)
i : ι
s : Set (β (f i))
y : β (f i)
hys : y ∈ s
x : α i
hxy : y = g i x
⊢ { fst := i, snd := x } ∈ Sigma.mk i '' (g i ⁻¹' s)
[PROOFSTEP]
subst y
[GOAL]
case mk.intro.intro.intro
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β✝ : ι → Type u_4
s✝ s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x✝ : (i : ι) × α i
i✝ j : ι
a : α i✝
β : ι' → Type u_5
f : ι → ι'
hf : Function.Injective f
g : (i : ι) → α i → β (f i)
i : ι
s : Set (β (f i))
x : α i
hys : g i x ∈ s
⊢ { fst := i, snd := x } ∈ Sigma.mk i '' (g i ⁻¹' s)
[PROOFSTEP]
exact ⟨x, hys, rfl⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι → Type u_4
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x✝ : (i : ι) × α i
i j : ι
a : α i
x : (i : ι) × α i
⊢ x ∈ Set.Sigma {i} t ↔ x ∈ Sigma.mk i '' t i
[PROOFSTEP]
constructor
[GOAL]
case mp
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι → Type u_4
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x✝ : (i : ι) × α i
i j : ι
a : α i
x : (i : ι) × α i
⊢ x ∈ Set.Sigma {i} t → x ∈ Sigma.mk i '' t i
[PROOFSTEP]
obtain ⟨j, a⟩ := x
[GOAL]
case mp.mk
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι → Type u_4
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x : (i : ι) × α i
i j✝ : ι
a✝ : α i
j : ι
a : α j
⊢ { fst := j, snd := a } ∈ Set.Sigma {i} t → { fst := j, snd := a } ∈ Sigma.mk i '' t i
[PROOFSTEP]
rintro ⟨rfl : j = i, ha⟩
[GOAL]
case mp.mk.intro
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι → Type u_4
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x : (i : ι) × α i
j✝ j : ι
a✝ : α j
ha : { fst := j, snd := a✝ }.snd ∈ t { fst := j, snd := a✝ }.fst
a : α j
⊢ { fst := j, snd := a✝ } ∈ Sigma.mk j '' t j
[PROOFSTEP]
exact mem_image_of_mem _ ha
[GOAL]
case mpr
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι → Type u_4
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x✝ : (i : ι) × α i
i j : ι
a : α i
x : (i : ι) × α i
⊢ x ∈ Sigma.mk i '' t i → x ∈ Set.Sigma {i} t
[PROOFSTEP]
rintro ⟨b, hb, rfl⟩
[GOAL]
case mpr.intro.intro
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι → Type u_4
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x : (i : ι) × α i
i j : ι
a b : α i
hb : b ∈ t i
⊢ { fst := i, snd := b } ∈ Set.Sigma {i} t
[PROOFSTEP]
exact ⟨rfl, hb⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι → Type u_4
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x : (i : ι) × α i
i j : ι
a✝ : α i
a : (i : ι) → α i
⊢ (Set.Sigma s fun i => {a i}) = (fun i => { fst := i, snd := a i }) '' s
[PROOFSTEP]
ext ⟨x, y⟩
[GOAL]
case h.mk
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι → Type u_4
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x✝ : (i : ι) × α i
i j : ι
a✝ : α i
a : (i : ι) → α i
x : ι
y : α x
⊢ ({ fst := x, snd := y } ∈ Set.Sigma s fun i => {a i}) ↔
    { fst := x, snd := y } ∈ (fun i => { fst := i, snd := a i }) '' s
[PROOFSTEP]
simp [and_left_comm, eq_comm]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι → Type u_4
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x : (i : ι) × α i
i j : ι
a✝ : α i
a : (i : ι) → α i
⊢ (Set.Sigma {i} fun i => {a i}) = {{ fst := i, snd := a i }}
[PROOFSTEP]
rw [sigma_singleton, image_singleton]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι → Type u_4
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x : (i : ι) × α i
i j : ι
a : α i
⊢ Set.Sigma s₁ t₁ ∩ Set.Sigma s₂ t₂ = Set.Sigma (s₁ ∩ s₂) fun i => t₁ i ∩ t₂ i
[PROOFSTEP]
ext ⟨x, y⟩
[GOAL]
case h.mk
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι → Type u_4
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x✝ : (i : ι) × α i
i j : ι
a : α i
x : ι
y : α x
⊢ { fst := x, snd := y } ∈ Set.Sigma s₁ t₁ ∩ Set.Sigma s₂ t₂ ↔
    { fst := x, snd := y } ∈ Set.Sigma (s₁ ∩ s₂) fun i => t₁ i ∩ t₂ i
[PROOFSTEP]
simp [and_assoc, and_left_comm]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι → Type u_4
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x : (i : ι) × α i
i j : ι
a : α i
⊢ Set.Sigma (insert i s) t = Sigma.mk i '' t i ∪ Set.Sigma s t
[PROOFSTEP]
rw [insert_eq, union_sigma, singleton_sigma]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι → Type u_4
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x : (i : ι) × α i
i j : ι
a : α i
⊢ α i
[PROOFSTEP]
exact a
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι → Type u_4
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x : (i : ι) × α i
i j : ι
a✝ : α i
a : (i : ι) → α i
⊢ (Set.Sigma s fun i => insert (a i) (t i)) = (fun i => { fst := i, snd := a i }) '' s ∪ Set.Sigma s t
[PROOFSTEP]
simp_rw [insert_eq, sigma_union, sigma_singleton]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι → Type u_4
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x : (i : ι) × α i
i j : ι
a : α i
inst✝ : DecidablePred fun x => x ∈ s
⊢ Sigma.mk i ⁻¹' Set.Sigma s t = if i ∈ s then t i else ∅
[PROOFSTEP]
split_ifs
[GOAL]
case pos
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι → Type u_4
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x : (i : ι) × α i
i j : ι
a : α i
inst✝ : DecidablePred fun x => x ∈ s
h✝ : i ∈ s
⊢ Sigma.mk i ⁻¹' Set.Sigma s t = t i
[PROOFSTEP]
simp [*]
[GOAL]
case neg
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι → Type u_4
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x : (i : ι) × α i
i j : ι
a : α i
inst✝ : DecidablePred fun x => x ∈ s
h✝ : ¬i ∈ s
⊢ Sigma.mk i ⁻¹' Set.Sigma s t = ∅
[PROOFSTEP]
simp [*]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β✝ : ι → Type u_4
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x : (i : ι) × α i
i j : ι
a : α i
β : Type u_5
inst✝ : DecidablePred fun x => x ∈ s
g : β → α i
x✝ : β
⊢ x✝ ∈ (fun b => { fst := i, snd := g b }) ⁻¹' Set.Sigma s t ↔ x✝ ∈ if i ∈ s then g ⁻¹' t i else ∅
[PROOFSTEP]
split_ifs
[GOAL]
case pos
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β✝ : ι → Type u_4
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x : (i : ι) × α i
i j : ι
a : α i
β : Type u_5
inst✝ : DecidablePred fun x => x ∈ s
g : β → α i
x✝ : β
h✝ : i ∈ s
⊢ x✝ ∈ (fun b => { fst := i, snd := g b }) ⁻¹' Set.Sigma s t ↔ x✝ ∈ g ⁻¹' t i
[PROOFSTEP]
simp [*]
[GOAL]
case neg
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β✝ : ι → Type u_4
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x : (i : ι) × α i
i j : ι
a : α i
β : Type u_5
inst✝ : DecidablePred fun x => x ∈ s
g : β → α i
x✝ : β
h✝ : ¬i ∈ s
⊢ x✝ ∈ (fun b => { fst := i, snd := g b }) ⁻¹' Set.Sigma s t ↔ x✝ ∈ ∅
[PROOFSTEP]
simp [*]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι → Type u_4
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x : (i : ι) × α i
i j : ι
a : α i
f : (i : ι) → α i → β i
⊢ ∀ (x : (i : ι) × β i),
    (x ∈ Set.Sigma univ fun i => range (f i)) ↔ x ∈ range fun x => { fst := x.fst, snd := f x.fst x.snd }
[PROOFSTEP]
simp [range]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι → Type u_4
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x : (i : ι) × α i
i j : ι
a : α i
⊢ (¬∃ i, i ∈ s ∧ Set.Nonempty (t i)) ↔ ∀ (i : ι), i ∈ s → t i = ∅
[PROOFSTEP]
simp only [not_nonempty_iff_eq_empty, not_and, not_exists]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι → Type u_4
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x✝ : (i : ι) × α i
i j : ι
a : α i
x : (i : ι) × α i
⊢ x ∈ Set.Sigma s₁ t₁ \ Set.Sigma s₂ t₂ ↔ x ∈ Set.Sigma s₁ (t₁ \ t₂) ∪ Set.Sigma (s₁ \ s₂) t₁
[PROOFSTEP]
by_cases h₁ : x.1 ∈ s₁
[GOAL]
case pos
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι → Type u_4
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x✝ : (i : ι) × α i
i j : ι
a : α i
x : (i : ι) × α i
h₁ : x.fst ∈ s₁
⊢ x ∈ Set.Sigma s₁ t₁ \ Set.Sigma s₂ t₂ ↔ x ∈ Set.Sigma s₁ (t₁ \ t₂) ∪ Set.Sigma (s₁ \ s₂) t₁
[PROOFSTEP]
by_cases h₂ : x.2 ∈ t₁ x.1
[GOAL]
case neg
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι → Type u_4
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x✝ : (i : ι) × α i
i j : ι
a : α i
x : (i : ι) × α i
h₁ : ¬x.fst ∈ s₁
⊢ x ∈ Set.Sigma s₁ t₁ \ Set.Sigma s₂ t₂ ↔ x ∈ Set.Sigma s₁ (t₁ \ t₂) ∪ Set.Sigma (s₁ \ s₂) t₁
[PROOFSTEP]
by_cases h₂ : x.2 ∈ t₁ x.1
[GOAL]
case pos
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι → Type u_4
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x✝ : (i : ι) × α i
i j : ι
a : α i
x : (i : ι) × α i
h₁ : x.fst ∈ s₁
h₂ : x.snd ∈ t₁ x.fst
⊢ x ∈ Set.Sigma s₁ t₁ \ Set.Sigma s₂ t₂ ↔ x ∈ Set.Sigma s₁ (t₁ \ t₂) ∪ Set.Sigma (s₁ \ s₂) t₁
[PROOFSTEP]
simp [*, ← imp_iff_or_not]
[GOAL]
case neg
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι → Type u_4
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x✝ : (i : ι) × α i
i j : ι
a : α i
x : (i : ι) × α i
h₁ : x.fst ∈ s₁
h₂ : ¬x.snd ∈ t₁ x.fst
⊢ x ∈ Set.Sigma s₁ t₁ \ Set.Sigma s₂ t₂ ↔ x ∈ Set.Sigma s₁ (t₁ \ t₂) ∪ Set.Sigma (s₁ \ s₂) t₁
[PROOFSTEP]
simp [*, ← imp_iff_or_not]
[GOAL]
case pos
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι → Type u_4
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x✝ : (i : ι) × α i
i j : ι
a : α i
x : (i : ι) × α i
h₁ : ¬x.fst ∈ s₁
h₂ : x.snd ∈ t₁ x.fst
⊢ x ∈ Set.Sigma s₁ t₁ \ Set.Sigma s₂ t₂ ↔ x ∈ Set.Sigma s₁ (t₁ \ t₂) ∪ Set.Sigma (s₁ \ s₂) t₁
[PROOFSTEP]
simp [*, ← imp_iff_or_not]
[GOAL]
case neg
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι → Type u_4
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x✝ : (i : ι) × α i
i j : ι
a : α i
x : (i : ι) × α i
h₁ : ¬x.fst ∈ s₁
h₂ : ¬x.snd ∈ t₁ x.fst
⊢ x ∈ Set.Sigma s₁ t₁ \ Set.Sigma s₂ t₂ ↔ x ∈ Set.Sigma s₁ (t₁ \ t₂) ∪ Set.Sigma (s₁ \ s₂) t₁
[PROOFSTEP]
simp [*, ← imp_iff_or_not]