case h.mk
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : α → Type u_2
p : α → Prop
inst✝ : DecidablePred p
s : (i : α) → Set (β i)
f : (i : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
⊢ (f, g) ∈ ↑(piEquivPiSubtypeProd p β).symm ⁻¹' pi univ s ↔ (f, g) ∈ (pi univ fun i => s ↑i) ×ˢ pi univ fun i => s ↑i
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : α → Type u_2
p : α → Prop
inst✝ : DecidablePred p
s : (i : α) → Set (β i)
⊢ ↑(piEquivPiSubtypeProd p β).symm ⁻¹' pi univ s = (pi univ fun i => s ↑i) ×ˢ pi univ fun i => s ↑i
ext ⟨f, g⟩
case h.mk
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : α → Type u_2
p : α → Prop
inst✝ : DecidablePred p
s : (i : α) → Set (β i)
f : (i : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
⊢ (∀ (i : α), ↑(piEquivPiSubtypeProd p β).symm (f, g) i ∈ s i) ↔
    ∀ (x : α), (∀ (b : p x), f { val := x, property := b } ∈ s x) ∧ ∀ (b : ¬p x), g { val := x, property := b } ∈ s x
case h.mk
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : α → Type u_2
p : α → Prop
inst✝ : DecidablePred p
s : (i : α) → Set (β i)
f : (i : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
⊢ (f, g) ∈ ↑(piEquivPiSubtypeProd p β).symm ⁻¹' pi univ s ↔ (f, g) ∈ (pi univ fun i => s ↑i) ×ˢ pi univ fun i => s ↑i
simp only [mem_preimage, mem_univ_pi, prod_mk_mem_set_prod_eq, Subtype.forall, ← forall_and]
case h.mk
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : α → Type u_2
p : α → Prop
inst✝ : DecidablePred p
s : (i : α) → Set (β i)
f : (i : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
i : α
⊢ ↑(piEquivPiSubtypeProd p β).symm (f, g) i ∈ s i ↔
    (∀ (b : p i), f { val := i, property := b } ∈ s i) ∧ ∀ (b : ¬p i), g { val := i, property := b } ∈ s i
case h.mk
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : α → Type u_2
p : α → Prop
inst✝ : DecidablePred p
s : (i : α) → Set (β i)
f : (i : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
⊢ (∀ (i : α), ↑(piEquivPiSubtypeProd p β).symm (f, g) i ∈ s i) ↔
    ∀ (x : α), (∀ (b : p x), f { val := x, property := b } ∈ s x) ∧ ∀ (b : ¬p x), g { val := x, property := b } ∈ s x
refine' forall_congr' fun i => _
case h.mk
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : α → Type u_2
p : α → Prop
inst✝ : DecidablePred p
s : (i : α) → Set (β i)
f : (i : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
i : α
⊢ ↑(piEquivPiSubtypeProd p β).symm (f, g) i ∈ s i ↔
    (∀ (b : p i), f { val := i, property := b } ∈ s i) ∧ ∀ (b : ¬p i), g { val := i, property := b } ∈ s i
case h.mk
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : α → Type u_2
p : α → Prop
inst✝ : DecidablePred p
s : (i : α) → Set (β i)
f : (i : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
i : α
⊢ ↑(piEquivPiSubtypeProd p β).symm (f, g) i ∈ s i ↔
    (∀ (b : p i), f { val := i, property := b } ∈ s i) ∧ ∀ (b : ¬p i), g { val := i, property := b } ∈ s i
dsimp only [Subtype.coe_mk]
case pos
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : α → Type u_2
p : α → Prop
inst✝ : DecidablePred p
s : (i : α) → Set (β i)
f : (i : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
i : α
hi : p i
⊢ ↑(piEquivPiSubtypeProd p β).symm (f, g) i ∈ s i ↔
    (∀ (b : p i), f { val := i, property := b } ∈ s i) ∧ ∀ (b : ¬p i), g { val := i, property := b } ∈ s i

case neg
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : α → Type u_2
p : α → Prop
inst✝ : DecidablePred p
s : (i : α) → Set (β i)
f : (i : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
i : α
hi : ¬p i
⊢ ↑(piEquivPiSubtypeProd p β).symm (f, g) i ∈ s i ↔
    (∀ (b : p i), f { val := i, property := b } ∈ s i) ∧ ∀ (b : ¬p i), g { val := i, property := b } ∈ s i
case h.mk
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : α → Type u_2
p : α → Prop
inst✝ : DecidablePred p
s : (i : α) → Set (β i)
f : (i : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
i : α
⊢ ↑(piEquivPiSubtypeProd p β).symm (f, g) i ∈ s i ↔
    (∀ (b : p i), f { val := i, property := b } ∈ s i) ∧ ∀ (b : ¬p i), g { val := i, property := b } ∈ s i
by_cases hi : p i
case neg
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : α → Type u_2
p : α → Prop
inst✝ : DecidablePred p
s : (i : α) → Set (β i)
f : (i : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
i : α
hi : ¬p i
⊢ ↑(piEquivPiSubtypeProd p β).symm (f, g) i ∈ s i ↔
    (∀ (b : p i), f { val := i, property := b } ∈ s i) ∧ ∀ (b : ¬p i), g { val := i, property := b } ∈ s i
case pos
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : α → Type u_2
p : α → Prop
inst✝ : DecidablePred p
s : (i : α) → Set (β i)
f : (i : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
i : α
hi : p i
⊢ ↑(piEquivPiSubtypeProd p β).symm (f, g) i ∈ s i ↔
    (∀ (b : p i), f { val := i, property := b } ∈ s i) ∧ ∀ (b : ¬p i), g { val := i, property := b } ∈ s i

case neg
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : α → Type u_2
p : α → Prop
inst✝ : DecidablePred p
s : (i : α) → Set (β i)
f : (i : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
i : α
hi : ¬p i
⊢ ↑(piEquivPiSubtypeProd p β).symm (f, g) i ∈ s i ↔
    (∀ (b : p i), f { val := i, property := b } ∈ s i) ∧ ∀ (b : ¬p i), g { val := i, property := b } ∈ s i
. simp [forall_prop_of_true hi, forall_prop_of_false (not_not.2 hi), hi]
no goals
case neg
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : α → Type u_2
p : α → Prop
inst✝ : DecidablePred p
s : (i : α) → Set (β i)
f : (i : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
i : α
hi : ¬p i
⊢ ↑(piEquivPiSubtypeProd p β).symm (f, g) i ∈ s i ↔
    (∀ (b : p i), f { val := i, property := b } ∈ s i) ∧ ∀ (b : ¬p i), g { val := i, property := b } ∈ s i
. simp [forall_prop_of_false hi, hi, forall_prop_of_true hi]
no goals
case pos
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : α → Type u_2
p : α → Prop
inst✝ : DecidablePred p
s : (i : α) → Set (β i)
f : (i : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
i : α
hi : p i
⊢ ↑(piEquivPiSubtypeProd p β).symm (f, g) i ∈ s i ↔
    (∀ (b : p i), f { val := i, property := b } ∈ s i) ∧ ∀ (b : ¬p i), g { val := i, property := b } ∈ s i
simp [forall_prop_of_true hi, forall_prop_of_false (not_not.2 hi), hi]
no goals
case neg
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : α → Type u_2
p : α → Prop
inst✝ : DecidablePred p
s : (i : α) → Set (β i)
f : (i : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
i : α
hi : ¬p i
⊢ ↑(piEquivPiSubtypeProd p β).symm (f, g) i ∈ s i ↔
    (∀ (b : p i), f { val := i, property := b } ∈ s i) ∧ ∀ (b : ¬p i), g { val := i, property := b } ∈ s i
simp [forall_prop_of_false hi, hi, forall_prop_of_true hi]