[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
e : α ≃ β
s : Set α
t : Set β
⊢ ↑e.symm '' t ⊆ s ↔ t ⊆ ↑e '' s
[PROOFSTEP]
rw [image_subset_iff, e.image_eq_preimage]
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
e : α ≃ β
s : Set α
t : Set β
⊢ s ⊆ ↑e.symm '' t ↔ ↑e.symm.symm '' s ⊆ t
[PROOFSTEP]
rw [e.symm.subset_image]
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
e : α ≃ β
s : Set α
t : Set β
⊢ ↑e.symm.symm '' s ⊆ t ↔ ↑e '' s ⊆ t
[PROOFSTEP]
rw [e.symm_symm]
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
u : Set γ
⊢ ↑(prodAssoc α β γ) ⁻¹' s ×ˢ t ×ˢ u = (s ×ˢ t) ×ˢ u
[PROOFSTEP]
ext
[GOAL]
case h
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
u : Set γ
x✝ : (α × β) × γ
⊢ x✝ ∈ ↑(prodAssoc α β γ) ⁻¹' s ×ˢ t ×ˢ u ↔ x✝ ∈ (s ×ˢ t) ×ˢ u
[PROOFSTEP]
simp [and_assoc]
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
u : Set γ
⊢ ↑(prodAssoc α β γ).symm ⁻¹' (s ×ˢ t) ×ˢ u = s ×ˢ t ×ˢ u
[PROOFSTEP]
ext
[GOAL]
case h
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
u : Set γ
x✝ : α × β × γ
⊢ x✝ ∈ ↑(prodAssoc α β γ).symm ⁻¹' (s ×ˢ t) ×ˢ u ↔ x✝ ∈ s ×ˢ t ×ˢ u
[PROOFSTEP]
simp [and_assoc]
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
u : Set γ
⊢ ↑(prodAssoc α β γ) '' (s ×ˢ t) ×ˢ u = s ×ˢ t ×ˢ u
[PROOFSTEP]
simpa only [Equiv.image_eq_preimage] using prod_assoc_symm_preimage
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
u : Set γ
⊢ ↑(prodAssoc α β γ).symm '' s ×ˢ t ×ˢ u = (s ×ˢ t) ×ˢ u
[PROOFSTEP]
simpa only [Equiv.image_eq_preimage] using prod_assoc_preimage
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
s : Set (α × β)
x : ↑s
⊢ (↑x).snd ∈ {y | ((↑x).fst, y) ∈ s}
[PROOFSTEP]
simp
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
e : α ≃ β
s : Set α
x : ↑s
⊢ ↑e ↑x ∈ ↑e '' s
[PROOFSTEP]
simp
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
e : α ≃ β
s : Set α
y : ↑(↑e '' s)
⊢ ↑e.symm ↑y ∈ s
[PROOFSTEP]
rcases y with ⟨-, ⟨a, ⟨m, rfl⟩⟩⟩
[GOAL]
case mk.intro.intro
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
e : α ≃ β
s : Set α
a : α
m : a ∈ s
⊢ ↑e.symm ↑{ val := ↑e a, property := (_ : ∃ a_1, a_1 ∈ s ∧ ↑e a_1 = ↑e a) } ∈ s
[PROOFSTEP]
simpa using m
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
e : α ≃ β
s : Set α
x : ↑s
⊢ (fun y => { val := ↑e.symm ↑y, property := (_ : ↑e.symm ↑y ∈ s) })
      ((fun x => { val := ↑e ↑x, property := (_ : ↑e ↑x ∈ ↑e '' s) }) x) =
    x
[PROOFSTEP]
simp
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
e : α ≃ β
s : Set α
y : ↑(↑e '' s)
⊢ (fun x => { val := ↑e ↑x, property := (_ : ↑e ↑x ∈ ↑e '' s) })
      ((fun y => { val := ↑e.symm ↑y, property := (_ : ↑e.symm ↑y ∈ s) }) y) =
    y
[PROOFSTEP]
simp
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type ?u.13643
s t : Set α
p : α → Prop
inst✝ : DecidablePred p
hs : ∀ (x : α), x ∈ s → p x
ht : ∀ (x : α), x ∈ t → ¬p x
x✝ : ↑(s ∪ t)
x : α
h' : x ∈ s ∪ t
⊢ (fun o =>
        match o with
        | Sum.inl x => { val := ↑x, property := (_ : ↑x ∈ s ∨ ↑x ∈ t) }
        | Sum.inr x => { val := ↑x, property := (_ : ↑x ∈ s ∨ ↑x ∈ t) })
      ((fun x =>
          if hp : p ↑x then Sum.inl { val := ↑x, property := (_ : ↑x ∈ s) }
          else Sum.inr { val := ↑x, property := (_ : ↑x ∈ t) })
        { val := x, property := h' }) =
    { val := x, property := h' }
[PROOFSTEP]
by_cases h : p x
[GOAL]
case pos
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type ?u.13643
s t : Set α
p : α → Prop
inst✝ : DecidablePred p
hs : ∀ (x : α), x ∈ s → p x
ht : ∀ (x : α), x ∈ t → ¬p x
x✝ : ↑(s ∪ t)
x : α
h' : x ∈ s ∪ t
h : p x
⊢ (fun o =>
        match o with
        | Sum.inl x => { val := ↑x, property := (_ : ↑x ∈ s ∨ ↑x ∈ t) }
        | Sum.inr x => { val := ↑x, property := (_ : ↑x ∈ s ∨ ↑x ∈ t) })
      ((fun x =>
          if hp : p ↑x then Sum.inl { val := ↑x, property := (_ : ↑x ∈ s) }
          else Sum.inr { val := ↑x, property := (_ : ↑x ∈ t) })
        { val := x, property := h' }) =
    { val := x, property := h' }
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type ?u.13643
s t : Set α
p : α → Prop
inst✝ : DecidablePred p
hs : ∀ (x : α), x ∈ s → p x
ht : ∀ (x : α), x ∈ t → ¬p x
x✝ : ↑(s ∪ t)
x : α
h' : x ∈ s ∪ t
h : ¬p x
⊢ (fun o =>
        match o with
        | Sum.inl x => { val := ↑x, property := (_ : ↑x ∈ s ∨ ↑x ∈ t) }
        | Sum.inr x => { val := ↑x, property := (_ : ↑x ∈ s ∨ ↑x ∈ t) })
      ((fun x =>
          if hp : p ↑x then Sum.inl { val := ↑x, property := (_ : ↑x ∈ s) }
          else Sum.inr { val := ↑x, property := (_ : ↑x ∈ t) })
        { val := x, property := h' }) =
    { val := x, property := h' }
[PROOFSTEP]
simp [h]
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type ?u.13643
s t : Set α
p : α → Prop
inst✝ : DecidablePred p
hs : ∀ (x : α), x ∈ s → p x
ht : ∀ (x : α), x ∈ t → ¬p x
o : ↑s ⊕ ↑t
⊢ (fun x =>
        if hp : p ↑x then Sum.inl { val := ↑x, property := (_ : ↑x ∈ s) }
        else Sum.inr { val := ↑x, property := (_ : ↑x ∈ t) })
      ((fun o =>
          match o with
          | Sum.inl x => { val := ↑x, property := (_ : ↑x ∈ s ∨ ↑x ∈ t) }
          | Sum.inr x => { val := ↑x, property := (_ : ↑x ∈ s ∨ ↑x ∈ t) })
        o) =
    o
[PROOFSTEP]
rcases o with (⟨x, h⟩ | ⟨x, h⟩) <;> [simp [hs _ h]; simp [ht _ h]]
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type ?u.13643
s t : Set α
p : α → Prop
inst✝ : DecidablePred p
hs : ∀ (x : α), x ∈ s → p x
ht : ∀ (x : α), x ∈ t → ¬p x
o : ↑s ⊕ ↑t
⊢ (fun x =>
        if hp : p ↑x then Sum.inl { val := ↑x, property := (_ : ↑x ∈ s) }
        else Sum.inr { val := ↑x, property := (_ : ↑x ∈ t) })
      ((fun o =>
          match o with
          | Sum.inl x => { val := ↑x, property := (_ : ↑x ∈ s ∨ ↑x ∈ t) }
          | Sum.inr x => { val := ↑x, property := (_ : ↑x ∈ s ∨ ↑x ∈ t) })
        o) =
    o
[PROOFSTEP]
rcases o with (⟨x, h⟩ | ⟨x, h⟩)
[GOAL]
case inl.mk
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type ?u.13643
s t : Set α
p : α → Prop
inst✝ : DecidablePred p
hs : ∀ (x : α), x ∈ s → p x
ht : ∀ (x : α), x ∈ t → ¬p x
x : α
h : x ∈ s
⊢ (fun x =>
        if hp : p ↑x then Sum.inl { val := ↑x, property := (_ : ↑x ∈ s) }
        else Sum.inr { val := ↑x, property := (_ : ↑x ∈ t) })
      ((fun o =>
          match o with
          | Sum.inl x => { val := ↑x, property := (_ : ↑x ∈ s ∨ ↑x ∈ t) }
          | Sum.inr x => { val := ↑x, property := (_ : ↑x ∈ s ∨ ↑x ∈ t) })
        (Sum.inl { val := x, property := h })) =
    Sum.inl { val := x, property := h }
[PROOFSTEP]
simp [hs _ h]
[GOAL]
case inr.mk
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type ?u.13643
s t : Set α
p : α → Prop
inst✝ : DecidablePred p
hs : ∀ (x : α), x ∈ s → p x
ht : ∀ (x : α), x ∈ t → ¬p x
x : α
h : x ∈ t
⊢ (fun x =>
        if hp : p ↑x then Sum.inl { val := ↑x, property := (_ : ↑x ∈ s) }
        else Sum.inr { val := ↑x, property := (_ : ↑x ∈ t) })
      ((fun o =>
          match o with
          | Sum.inl x => { val := ↑x, property := (_ : ↑x ∈ s ∨ ↑x ∈ t) }
          | Sum.inr x => { val := ↑x, property := (_ : ↑x ∈ s ∨ ↑x ∈ t) })
        (Sum.inr { val := x, property := h })) =
    Sum.inr { val := x, property := h }
[PROOFSTEP]
simp [ht _ h]
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type ?u.20174
a : α
x✝ : ↑{a}
x : α
h : x ∈ {a}
⊢ (fun x => { val := a, property := (_ : a ∈ {a}) }) ((fun x => PUnit.unit) { val := x, property := h }) =
    { val := x, property := h }
[PROOFSTEP]
simp at h 
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type ?u.20174
a : α
x✝ : ↑{a}
x : α
h✝ : x ∈ {a}
h : x = a
⊢ (fun x => { val := a, property := (_ : a ∈ {a}) }) ((fun x => PUnit.unit) { val := x, property := h✝ }) =
    { val := x, property := h✝ }
[PROOFSTEP]
subst x
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type ?u.20174
a : α
x✝ : ↑{a}
h : a = a
⊢ (fun x => { val := a, property := (_ : a ∈ {a}) }) ((fun x => PUnit.unit) { val := a, property := (_ : a = a) }) =
    { val := a, property := (_ : a = a) }
[PROOFSTEP]
rfl
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a : α
H : ¬a ∈ s
⊢ insert a s = s ∪ {a}
[PROOFSTEP]
simp
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a : α
H : ¬a ∈ s
x : α
x✝ : x ∈ s ∩ {a}
hx : x ∈ s
right✝ : x ∈ {a}
⊢ x ∈ ∅
[PROOFSTEP]
simp_all
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type ?u.24478
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
⊢ s ∩ sᶜ ⊆ ∅
[PROOFSTEP]
simp [Set.ext_iff]
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type ?u.24478
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
⊢ s ∪ sᶜ = univ
[PROOFSTEP]
simp
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
x : α
hx : x ∈ s
⊢ ↑(Set.sumCompl s).symm x = Sum.inl { val := x, property := hx }
[PROOFSTEP]
have : ((⟨x, Or.inl hx⟩ : (s ∪ sᶜ : Set α)) : α) ∈ s := hx
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
x : α
hx : x ∈ s
this : ↑{ val := x, property := (_ : x ∈ s ∨ x ∈ sᶜ) } ∈ s
⊢ ↑(Set.sumCompl s).symm x = Sum.inl { val := x, property := hx }
[PROOFSTEP]
rw [Equiv.Set.sumCompl]
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
x : α
hx : x ∈ s
this : ↑{ val := x, property := (_ : x ∈ s ∨ x ∈ sᶜ) } ∈ s
⊢ ↑(Trans.trans (Trans.trans (Set.union (_ : s ∩ sᶜ ⊆ ∅)).symm (Set.ofEq (_ : s ∪ sᶜ = univ))) (Set.univ α)).symm x =
    Sum.inl { val := x, property := hx }
[PROOFSTEP]
simpa using Set.union_apply_left (by simp) this
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
x : α
hx : x ∈ s
this : ↑{ val := x, property := (_ : x ∈ s ∨ x ∈ sᶜ) } ∈ s
⊢ s ∩ sᶜ ⊆ ∅
[PROOFSTEP]
simp
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
x : α
hx : ¬x ∈ s
⊢ ↑(Set.sumCompl s).symm x = Sum.inr { val := x, property := hx }
[PROOFSTEP]
have : ((⟨x, Or.inr hx⟩ : (s ∪ sᶜ : Set α)) : α) ∈ sᶜ := hx
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
x : α
hx : ¬x ∈ s
this : ↑{ val := x, property := (_ : x ∈ s ∨ x ∈ sᶜ) } ∈ sᶜ
⊢ ↑(Set.sumCompl s).symm x = Sum.inr { val := x, property := hx }
[PROOFSTEP]
rw [Equiv.Set.sumCompl]
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
x : α
hx : ¬x ∈ s
this : ↑{ val := x, property := (_ : x ∈ s ∨ x ∈ sᶜ) } ∈ sᶜ
⊢ ↑(Trans.trans (Trans.trans (Set.union (_ : s ∩ sᶜ ⊆ ∅)).symm (Set.ofEq (_ : s ∪ sᶜ = univ))) (Set.univ α)).symm x =
    Sum.inr { val := x, property := hx }
[PROOFSTEP]
simpa using Set.union_apply_right (by simp) this
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
x : α
hx : ¬x ∈ s
this : ↑{ val := x, property := (_ : x ∈ s ∨ x ∈ sᶜ) } ∈ sᶜ
⊢ s ∩ sᶜ ⊆ ∅
[PROOFSTEP]
simp
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u_1
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
x : ↑s
⊢ ↑(Set.sumCompl s).symm ↑x = Sum.inl x
[PROOFSTEP]
cases' x with x hx
[GOAL]
case mk
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u_1
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
x : α
hx : x ∈ s
⊢ ↑(Set.sumCompl s).symm ↑{ val := x, property := hx } = Sum.inl { val := x, property := hx }
[PROOFSTEP]
exact Set.sumCompl_symm_apply_of_mem hx
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u_1
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
x : ↑sᶜ
⊢ ↑(Set.sumCompl s).symm ↑x = Sum.inr x
[PROOFSTEP]
cases' x with x hx
[GOAL]
case mk
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u_1
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
x : α
hx : x ∈ sᶜ
⊢ ↑(Set.sumCompl s).symm ↑{ val := x, property := hx } = Sum.inr { val := x, property := hx }
[PROOFSTEP]
exact Set.sumCompl_symm_apply_of_not_mem hx
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type ?u.32810
s t : Set α
h : s ⊆ t
inst✝ : DecidablePred fun x => x ∈ s
⊢ s ∩ (t \ s) ⊆ ∅
[PROOFSTEP]
simp [inter_diff_self]
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type ?u.32810
s t : Set α
h : s ⊆ t
inst✝ : DecidablePred fun x => x ∈ s
⊢ s ∪ t \ s = t
[PROOFSTEP]
simp [union_diff_self, union_eq_self_of_subset_left h]
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u_1
s t : Set α
h : s ⊆ t
inst✝ : DecidablePred fun x => x ∈ s
x : ↑t
hx : ↑x ∈ s
⊢ ↑(Set.sumDiffSubset h).symm x = Sum.inl { val := ↑x, property := hx }
[PROOFSTEP]
apply (Equiv.Set.sumDiffSubset h).injective
[GOAL]
case a
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u_1
s t : Set α
h : s ⊆ t
inst✝ : DecidablePred fun x => x ∈ s
x : ↑t
hx : ↑x ∈ s
⊢ ↑(Set.sumDiffSubset h) (↑(Set.sumDiffSubset h).symm x) =
    ↑(Set.sumDiffSubset h) (Sum.inl { val := ↑x, property := hx })
[PROOFSTEP]
simp only [apply_symm_apply, sumDiffSubset_apply_inl]
[GOAL]
case a
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u_1
s t : Set α
h : s ⊆ t
inst✝ : DecidablePred fun x => x ∈ s
x : ↑t
hx : ↑x ∈ s
⊢ x = inclusion h { val := ↑x, property := hx }
[PROOFSTEP]
exact Subtype.eq rfl
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u_1
s t : Set α
h : s ⊆ t
inst✝ : DecidablePred fun x => x ∈ s
x : ↑t
hx : ¬↑x ∈ s
⊢ ↑(Set.sumDiffSubset h).symm x = Sum.inr { val := ↑x, property := (_ : ↑x ∈ t ∧ ¬↑x ∈ s) }
[PROOFSTEP]
apply (Equiv.Set.sumDiffSubset h).injective
[GOAL]
case a
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u_1
s t : Set α
h : s ⊆ t
inst✝ : DecidablePred fun x => x ∈ s
x : ↑t
hx : ¬↑x ∈ s
⊢ ↑(Set.sumDiffSubset h) (↑(Set.sumDiffSubset h).symm x) =
    ↑(Set.sumDiffSubset h) (Sum.inr { val := ↑x, property := (_ : ↑x ∈ t ∧ ¬↑x ∈ s) })
[PROOFSTEP]
simp only [apply_symm_apply, sumDiffSubset_apply_inr]
[GOAL]
case a
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u_1
s t : Set α
h : s ⊆ t
inst✝ : DecidablePred fun x => x ∈ s
x : ↑t
hx : ¬↑x ∈ s
⊢ x = inclusion (_ : t \ s ⊆ t) { val := ↑x, property := (_ : ↑x ∈ t ∧ ¬↑x ∈ s) }
[PROOFSTEP]
exact Subtype.eq rfl
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u
s t : Set α
inst✝ : DecidablePred fun x => x ∈ s
⊢ ↑(s ∪ t) ⊕ ↑(s ∩ t) ≃ ↑(s ∪ t \ s) ⊕ ↑(s ∩ t)
[PROOFSTEP]
rw [union_diff_self]
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u
s t : Set α
inst✝ : DecidablePred fun x => x ∈ s
⊢ ↑(t \ s) ⊕ ↑(s ∩ t) ≃ ↑(t \ s ∪ s ∩ t)
[PROOFSTEP]
refine' (Set.union' (· ∉ s) _ _).symm
[GOAL]
case refine'_1
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u
s t : Set α
inst✝ : DecidablePred fun x => x ∈ s
⊢ ∀ (x : α), x ∈ t \ s → (fun x => ¬x ∈ s) x
case refine'_2
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u
s t : Set α
inst✝ : DecidablePred fun x => x ∈ s
⊢ ∀ (x : α), x ∈ s ∩ t → ¬(fun x => ¬x ∈ s) x
[PROOFSTEP]
exacts [fun x hx => hx.2, fun x hx => not_not_intro hx.1]
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u
s t : Set α
inst✝ : DecidablePred fun x => x ∈ s
⊢ ↑s ⊕ ↑(t \ s ∪ s ∩ t) ≃ ↑s ⊕ ↑t
[PROOFSTEP]
{ rw [(_ : t \ s ∪ s ∩ t = t)]
  rw [union_comm, inter_comm, inter_union_diff]
}
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u
s t : Set α
inst✝ : DecidablePred fun x => x ∈ s
⊢ ↑s ⊕ ↑(t \ s ∪ s ∩ t) ≃ ↑s ⊕ ↑t
[PROOFSTEP]
rw [(_ : t \ s ∪ s ∩ t = t)]
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u
s t : Set α
inst✝ : DecidablePred fun x => x ∈ s
⊢ t \ s ∪ s ∩ t = t
[PROOFSTEP]
rw [union_comm, inter_comm, inter_union_diff]
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u
β : Type v
s : Set α
t : Set β
inst✝¹ : DecidablePred fun x => x ∈ s
inst✝ : DecidablePred fun x => x ∈ t
e₀ : ↑s ≃ ↑t
e₁ : ↑sᶜ ≃ ↑tᶜ
x : ↑s
⊢ ↑(Trans.trans (Trans.trans (Set.sumCompl s).symm (sumCongr e₀ e₁)) (Set.sumCompl t)) ↑x = ↑(↑e₀ x)
[PROOFSTEP]
simp only [Sum.map_inl, trans_apply, sumCongr_apply, Set.sumCompl_apply_inl, Set.sumCompl_symm_apply, Trans.trans]
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u
β : Type v
s : Set α
t : Set β
inst✝¹ : DecidablePred fun x => x ∈ s
inst✝ : DecidablePred fun x => x ∈ t
e₀ : ↑s ≃ ↑t
e : { e // ∀ (x : ↑s), ↑e ↑x = ↑(↑e₀ x) }
⊢ (fun e₁ =>
        { val := Trans.trans (Trans.trans (Set.sumCompl s).symm (sumCongr e₀ e₁)) (Set.sumCompl t),
          property := (_ : ∀ (x : ↑s), ↑(Set.sumCompl t) (↑(sumCongr e₀ e₁) (↑(Set.sumCompl s).symm ↑x)) = ↑(↑e₀ x)) })
      ((fun e => subtypeEquiv ↑e (_ : ∀ (a : α), ¬a ∈ s ↔ ¬↑↑e a ∈ t)) e) =
    e
[PROOFSTEP]
ext x
[GOAL]
case a.H
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u
β : Type v
s : Set α
t : Set β
inst✝¹ : DecidablePred fun x => x ∈ s
inst✝ : DecidablePred fun x => x ∈ t
e₀ : ↑s ≃ ↑t
e : { e // ∀ (x : ↑s), ↑e ↑x = ↑(↑e₀ x) }
x : α
⊢ ↑↑((fun e₁ =>
              { val := Trans.trans (Trans.trans (Set.sumCompl s).symm (sumCongr e₀ e₁)) (Set.sumCompl t),
                property :=
                  (_ : ∀ (x : ↑s), ↑(Set.sumCompl t) (↑(sumCongr e₀ e₁) (↑(Set.sumCompl s).symm ↑x)) = ↑(↑e₀ x)) })
            ((fun e => subtypeEquiv ↑e (_ : ∀ (a : α), ¬a ∈ s ↔ ¬↑↑e a ∈ t)) e))
      x =
    ↑↑e x
[PROOFSTEP]
by_cases hx : x ∈ s
[GOAL]
case pos
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u
β : Type v
s : Set α
t : Set β
inst✝¹ : DecidablePred fun x => x ∈ s
inst✝ : DecidablePred fun x => x ∈ t
e₀ : ↑s ≃ ↑t
e : { e // ∀ (x : ↑s), ↑e ↑x = ↑(↑e₀ x) }
x : α
hx : x ∈ s
⊢ ↑↑((fun e₁ =>
              { val := Trans.trans (Trans.trans (Set.sumCompl s).symm (sumCongr e₀ e₁)) (Set.sumCompl t),
                property :=
                  (_ : ∀ (x : ↑s), ↑(Set.sumCompl t) (↑(sumCongr e₀ e₁) (↑(Set.sumCompl s).symm ↑x)) = ↑(↑e₀ x)) })
            ((fun e => subtypeEquiv ↑e (_ : ∀ (a : α), ¬a ∈ s ↔ ¬↑↑e a ∈ t)) e))
      x =
    ↑↑e x
[PROOFSTEP]
simp only [Set.sumCompl_symm_apply_of_mem hx, ← e.prop ⟨x, hx⟩, Sum.map_inl, sumCongr_apply, trans_apply,
  Subtype.coe_mk, Set.sumCompl_apply_inl, Trans.trans]
[GOAL]
case neg
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u
β : Type v
s : Set α
t : Set β
inst✝¹ : DecidablePred fun x => x ∈ s
inst✝ : DecidablePred fun x => x ∈ t
e₀ : ↑s ≃ ↑t
e : { e // ∀ (x : ↑s), ↑e ↑x = ↑(↑e₀ x) }
x : α
hx : ¬x ∈ s
⊢ ↑↑((fun e₁ =>
              { val := Trans.trans (Trans.trans (Set.sumCompl s).symm (sumCongr e₀ e₁)) (Set.sumCompl t),
                property :=
                  (_ : ∀ (x : ↑s), ↑(Set.sumCompl t) (↑(sumCongr e₀ e₁) (↑(Set.sumCompl s).symm ↑x)) = ↑(↑e₀ x)) })
            ((fun e => subtypeEquiv ↑e (_ : ∀ (a : α), ¬a ∈ s ↔ ¬↑↑e a ∈ t)) e))
      x =
    ↑↑e x
[PROOFSTEP]
simp only [Set.sumCompl_symm_apply_of_not_mem hx, Sum.map_inr, subtypeEquiv_apply, Set.sumCompl_apply_inr, trans_apply,
  sumCongr_apply, Subtype.coe_mk, Trans.trans]
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u
β : Type v
s : Set α
t : Set β
inst✝¹ : DecidablePred fun x => x ∈ s
inst✝ : DecidablePred fun x => x ∈ t
e₀ : ↑s ≃ ↑t
e : ↑sᶜ ≃ ↑tᶜ
x : { a // a ∈ sᶜ }
⊢ ↑((fun e => subtypeEquiv ↑e (_ : ∀ (a : α), ¬a ∈ s ↔ ¬↑↑e a ∈ t))
          ((fun e₁ =>
              { val := Trans.trans (Trans.trans (Set.sumCompl s).symm (sumCongr e₀ e₁)) (Set.sumCompl t),
                property :=
                  (_ : ∀ (x : ↑s), ↑(Set.sumCompl t) (↑(sumCongr e₀ e₁) (↑(Set.sumCompl s).symm ↑x)) = ↑(↑e₀ x)) })
            e))
      x =
    ↑e x
[PROOFSTEP]
simp only [Sum.map_inr, subtypeEquiv_apply, Set.sumCompl_apply_inr, Function.comp_apply, sumCongr_apply,
  Equiv.coe_trans, Subtype.coe_eta, Subtype.coe_mk, Trans.trans, Set.sumCompl_symm_apply_compl]
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : α → Type u_2
s : (a : α) → Set (β a)
x✝ : ↑(pi univ s)
f : (i : α) → β i
hf : f ∈ pi univ s
⊢ (fun f => { val := fun a => ↑(f a), property := (_ : ∀ (a : α), a ∈ univ → ↑(f a) ∈ s a) })
      ((fun f a => { val := ↑f a, property := (_ : ↑f a ∈ s a) }) { val := f, property := hf }) =
    { val := f, property := hf }
[PROOFSTEP]
ext a
[GOAL]
case a.h
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : α → Type u_2
s : (a : α) → Set (β a)
x✝ : ↑(pi univ s)
f : (i : α) → β i
hf : f ∈ pi univ s
a : α
⊢ ↑((fun f => { val := fun a => ↑(f a), property := (_ : ∀ (a : α), a ∈ univ → ↑(f a) ∈ s a) })
          ((fun f a => { val := ↑f a, property := (_ : ↑f a ∈ s a) }) { val := f, property := hf }))
      a =
    ↑{ val := f, property := hf } a
[PROOFSTEP]
rfl
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : α → Type u_2
s : (a : α) → Set (β a)
f : (a : α) → ↑(s a)
⊢ (fun f a => { val := ↑f a, property := (_ : ↑f a ∈ s a) })
      ((fun f => { val := fun a => ↑(f a), property := (_ : ∀ (a : α), a ∈ univ → ↑(f a) ∈ s a) }) f) =
    f
[PROOFSTEP]
ext a
[GOAL]
case h.a
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : α → Type u_2
s : (a : α) → Set (β a)
f : (a : α) → ↑(s a)
a : α
⊢ ↑((fun f a => { val := ↑f a, property := (_ : ↑f a ∈ s a) })
        ((fun f => { val := fun a => ↑(f a), property := (_ : ∀ (a : α), a ∈ univ → ↑(f a) ∈ s a) }) f) a) =
    ↑(f a)
[PROOFSTEP]
rfl
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
f : α → β
s : Set α
H : Injective f
x : α
h : x ∈ s
⊢ ↑(Set.image f s H).symm { val := f x, property := (_ : ∃ a, a ∈ s ∧ f a = f x) } = { val := x, property := h }
[PROOFSTEP]
apply (Set.image f s H).injective
[GOAL]
case a
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
f : α → β
s : Set α
H : Injective f
x : α
h : x ∈ s
⊢ ↑(Set.image f s H) (↑(Set.image f s H).symm { val := f x, property := (_ : ∃ a, a ∈ s ∧ f a = f x) }) =
    ↑(Set.image f s H) { val := x, property := h }
[PROOFSTEP]
simp [(Set.image f s H).apply_symm_apply]
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
u s : Set α
⊢ (fun x => ↑(↑(Set.image f s hf).symm x)) ⁻¹' u = Subtype.val ⁻¹' (f '' u)
[PROOFSTEP]
ext ⟨b, a, has, rfl⟩
[GOAL]
case h.mk.intro.intro
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
u s : Set α
a : α
has : a ∈ s
⊢ { val := f a, property := (_ : ∃ a_1, a_1 ∈ s ∧ f a_1 = f a) } ∈ (fun x => ↑(↑(Set.image f s hf).symm x)) ⁻¹' u ↔
    { val := f a, property := (_ : ∃ a_1, a_1 ∈ s ∧ f a_1 = f a) } ∈ Subtype.val ⁻¹' (f '' u)
[PROOFSTEP]
have : ∀ h : ∃ a', a' ∈ s ∧ a' = a, Classical.choose h = a := fun h => (Classical.choose_spec h).2
[GOAL]
case h.mk.intro.intro
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
u s : Set α
a : α
has : a ∈ s
this : ∀ (h : ∃ a', a' ∈ s ∧ a' = a), Classical.choose h = a
⊢ { val := f a, property := (_ : ∃ a_1, a_1 ∈ s ∧ f a_1 = f a) } ∈ (fun x => ↑(↑(Set.image f s hf).symm x)) ⁻¹' u ↔
    { val := f a, property := (_ : ∃ a_1, a_1 ∈ s ∧ f a_1 = f a) } ∈ Subtype.val ⁻¹' (f '' u)
[PROOFSTEP]
simp [Equiv.Set.image, Equiv.Set.imageOfInjOn, hf.eq_iff, this]
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type ?u.53602
S : Set α
x : Set ↑S
⊢ Subtype.val '' x ∈ 𝒫 S
[PROOFSTEP]
rintro _ ⟨a : S, _, rfl⟩
[GOAL]
case intro.intro
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type ?u.53602
S : Set α
x : Set ↑S
a : ↑S
left✝ : a ∈ x
⊢ ↑a ∈ S
[PROOFSTEP]
exact a.2
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type ?u.53602
S : Set α
x : ↑(𝒫 S)
⊢ (fun x => { val := Subtype.val '' x, property := (_ : ∀ ⦃a : α⦄, a ∈ Subtype.val '' x → a ∈ S) })
      ((fun x => Subtype.val ⁻¹' ↑x) x) =
    x
[PROOFSTEP]
ext y
[GOAL]
case a.h
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type ?u.53602
S : Set α
x : ↑(𝒫 S)
y : α
⊢ y ∈
      ↑((fun x => { val := Subtype.val '' x, property := (_ : ∀ ⦃a : α⦄, a ∈ Subtype.val '' x → a ∈ S) })
          ((fun x => Subtype.val ⁻¹' ↑x) x)) ↔
    y ∈ ↑x
[PROOFSTEP]
exact ⟨fun ⟨⟨_, _⟩, h, rfl⟩ => h, fun h => ⟨⟨_, x.2 h⟩, h, rfl⟩⟩
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type ?u.53602
S : Set α
x : Set ↑S
⊢ (fun x => Subtype.val ⁻¹' ↑x)
      ((fun x => { val := Subtype.val '' x, property := (_ : ∀ ⦃a : α⦄, a ∈ Subtype.val '' x → a ∈ S) }) x) =
    x
[PROOFSTEP]
ext
[GOAL]
case h
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type ?u.53602
S : Set α
x : Set ↑S
x✝ : ↑S
⊢ x✝ ∈
      (fun x => Subtype.val ⁻¹' ↑x)
        ((fun x => { val := Subtype.val '' x, property := (_ : ∀ ⦃a : α⦄, a ∈ Subtype.val '' x → a ∈ S) }) x) ↔
    x✝ ∈ x
[PROOFSTEP]
simp
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
f : α → β
s : Set ↑(range f)
x : ↑(rangeSplitting f '' s)
⊢ f ↑x ∈ range f
[PROOFSTEP]
simp
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
f : α → β
s : Set ↑(range f)
x : ↑(rangeSplitting f '' s)
⊢ { val := f ↑x, property := (_ : f ↑x ∈ range f) } ∈ s
[PROOFSTEP]
rcases x with ⟨x, ⟨y, ⟨m, rfl⟩⟩⟩
[GOAL]
case mk.intro.intro
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
f : α → β
s : Set ↑(range f)
y : ↑(range f)
m : y ∈ s
⊢ { val := f ↑{ val := rangeSplitting f y, property := (_ : ∃ a, a ∈ s ∧ rangeSplitting f a = rangeSplitting f y) },
      property :=
        (_ :
          f ↑{ val := rangeSplitting f y, property := (_ : ∃ a, a ∈ s ∧ rangeSplitting f a = rangeSplitting f y) } ∈
            range f) } ∈
    s
[PROOFSTEP]
simpa [apply_rangeSplitting f] using m
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
f : α → β
s : Set ↑(range f)
x : ↑(rangeSplitting f '' s)
⊢ (fun x => { val := rangeSplitting f ↑x, property := (_ : ∃ a, a ∈ s ∧ rangeSplitting f a = rangeSplitting f ↑x) })
      ((fun x =>
          { val := { val := f ↑x, property := (_ : f ↑x ∈ range f) },
            property := (_ : { val := f ↑x, property := (_ : f ↑x ∈ range f) } ∈ s) })
        x) =
    x
[PROOFSTEP]
rcases x with ⟨x, ⟨y, ⟨m, rfl⟩⟩⟩
[GOAL]
case mk.intro.intro
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
f : α → β
s : Set ↑(range f)
y : ↑(range f)
m : y ∈ s
⊢ (fun x => { val := rangeSplitting f ↑x, property := (_ : ∃ a, a ∈ s ∧ rangeSplitting f a = rangeSplitting f ↑x) })
      ((fun x =>
          { val := { val := f ↑x, property := (_ : f ↑x ∈ range f) },
            property := (_ : { val := f ↑x, property := (_ : f ↑x ∈ range f) } ∈ s) })
        { val := rangeSplitting f y, property := (_ : ∃ a, a ∈ s ∧ rangeSplitting f a = rangeSplitting f y) }) =
    { val := rangeSplitting f y, property := (_ : ∃ a, a ∈ s ∧ rangeSplitting f a = rangeSplitting f y) }
[PROOFSTEP]
simp [apply_rangeSplitting f]
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
f : α → β
s : Set ↑(range f)
x : ↑s
⊢ (fun x =>
        { val := { val := f ↑x, property := (_ : f ↑x ∈ range f) },
          property := (_ : { val := f ↑x, property := (_ : f ↑x ∈ range f) } ∈ s) })
      ((fun x =>
          { val := rangeSplitting f ↑x, property := (_ : ∃ a, a ∈ s ∧ rangeSplitting f a = rangeSplitting f ↑x) })
        x) =
    x
[PROOFSTEP]
simp [apply_rangeSplitting f]
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
val✝ : β
h : Sum.inr val✝ ∈ range Sum.inl
⊢ False
[PROOFSTEP]
rcases h with ⟨x, h'⟩
[GOAL]
case intro
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
val✝ : β
x : α
h' : Sum.inl x = Sum.inr val✝
⊢ False
[PROOFSTEP]
cases h'
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
val✝ : α
h : Sum.inl val✝ ∈ range Sum.inr
⊢ False
[PROOFSTEP]
rcases h with ⟨x, h'⟩
[GOAL]
case intro
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
val✝ : α
x : β
h' : Sum.inr x = Sum.inl val✝
⊢ False
[PROOFSTEP]
cases h'
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Sort u_1
β : Type u_2
f : α → β
hf : Injective f
a : α
⊢ ↑(ofInjective f hf).symm { val := f a, property := (_ : ∃ y, f y = f a) } = a
[PROOFSTEP]
apply (ofInjective f hf).injective
[GOAL]
case a
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Sort u_1
β : Type u_2
f : α → β
hf : Injective f
a : α
⊢ ↑(ofInjective f hf) (↑(ofInjective f hf).symm { val := f a, property := (_ : ∃ y, f y = f a) }) =
    ↑(ofInjective f hf) a
[PROOFSTEP]
simp [apply_ofInjective_symm hf]
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
⊢ ↑(ofInjective f hf).symm = rangeSplitting f
[PROOFSTEP]
ext ⟨y, x, rfl⟩
[GOAL]
case h.mk.intro
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
x : α
⊢ ↑(ofInjective f hf).symm { val := f x, property := (_ : ∃ y, f y = f x) } =
    rangeSplitting f { val := f x, property := (_ : ∃ y, f y = f x) }
[PROOFSTEP]
apply hf
[GOAL]
case h.mk.intro.a
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
x : α
⊢ f (↑(ofInjective f hf).symm { val := f x, property := (_ : ∃ y, f y = f x) }) =
    f (rangeSplitting f { val := f x, property := (_ : ∃ y, f y = f x) })
[PROOFSTEP]
simp [apply_rangeSplitting f]
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
f : α → β
f_inv : Nonempty α → β → α
hf : ∀ (h : Nonempty α), LeftInverse (f_inv h) f
⊢ ofLeftInverse f f_inv hf = ofInjective f (_ : Injective f)
[PROOFSTEP]
ext
[GOAL]
case H.a
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
f : α → β
f_inv : Nonempty α → β → α
hf : ∀ (h : Nonempty α), LeftInverse (f_inv h) f
x✝ : α
⊢ ↑(↑(ofLeftInverse f f_inv hf) x✝) = ↑(↑(ofInjective f (_ : Injective f)) x✝)
[PROOFSTEP]
simp
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
f : α → β
f_inv : β → α
hf : LeftInverse f_inv f
⊢ ofLeftInverse' f f_inv hf = ofInjective f (_ : Injective f)
[PROOFSTEP]
ext
[GOAL]
case H.a
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
f : α → β
f_inv : β → α
hf : LeftInverse f_inv f
x✝ : α
⊢ ↑(↑(ofLeftInverse' f f_inv hf) x✝) = ↑(↑(ofInjective f (_ : Injective f)) x✝)
[PROOFSTEP]
simp
[GOAL]
α✝ : 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
[PROOFSTEP]
ext ⟨f, g⟩
[GOAL]
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
[PROOFSTEP]
simp only [mem_preimage, mem_univ_pi, prod_mk_mem_set_prod_eq, Subtype.forall, ← forall_and]
[GOAL]
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
[PROOFSTEP]
refine' forall_congr' fun i => _
[GOAL]
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
[PROOFSTEP]
dsimp only [Subtype.coe_mk]
  -- Porting note: Two lines below were `by_cases hi <;> simp [hi]`
    -- This regression is https://github.com/leanprover/lean4/issues/1926
[GOAL]
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
[PROOFSTEP]
by_cases hi : p i
[GOAL]
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
[PROOFSTEP]
simp [forall_prop_of_true hi, forall_prop_of_false (not_not.2 hi), hi]
[GOAL]
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
[PROOFSTEP]
simp [forall_prop_of_false hi, hi, forall_prop_of_true hi]
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : Type u_1
β : Sort u_2
γ : Sort u_3
p : α → Prop
e : β ≃ Subtype p
v : β → γ
w : α → γ
j : β
x : γ
inst✝² : DecidableEq β
inst✝¹ : DecidableEq α
inst✝ : (j : α) → Decidable (p j)
⊢ (fun i => if h : p i then update v j x (↑e.symm { val := i, property := h }) else w i) =
    update (fun i => if h : p i then v (↑e.symm { val := i, property := h }) else w i) (↑(↑e j)) x
[PROOFSTEP]
ext i
[GOAL]
case h
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : Type u_1
β : Sort u_2
γ : Sort u_3
p : α → Prop
e : β ≃ Subtype p
v : β → γ
w : α → γ
j : β
x : γ
inst✝² : DecidableEq β
inst✝¹ : DecidableEq α
inst✝ : (j : α) → Decidable (p j)
i : α
⊢ (if h : p i then update v j x (↑e.symm { val := i, property := h }) else w i) =
    update (fun i => if h : p i then v (↑e.symm { val := i, property := h }) else w i) (↑(↑e j)) x i
[PROOFSTEP]
by_cases h : p i
[GOAL]
case pos
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : Type u_1
β : Sort u_2
γ : Sort u_3
p : α → Prop
e : β ≃ Subtype p
v : β → γ
w : α → γ
j : β
x : γ
inst✝² : DecidableEq β
inst✝¹ : DecidableEq α
inst✝ : (j : α) → Decidable (p j)
i : α
h : p i
⊢ (if h : p i then update v j x (↑e.symm { val := i, property := h }) else w i) =
    update (fun i => if h : p i then v (↑e.symm { val := i, property := h }) else w i) (↑(↑e j)) x i
[PROOFSTEP]
rw [dif_pos h, Function.update_apply_equiv_apply, Equiv.symm_symm, Function.update_apply, Function.update_apply,
  dif_pos h]
[GOAL]
case pos
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : Type u_1
β : Sort u_2
γ : Sort u_3
p : α → Prop
e : β ≃ Subtype p
v : β → γ
w : α → γ
j : β
x : γ
inst✝² : DecidableEq β
inst✝¹ : DecidableEq α
inst✝ : (j : α) → Decidable (p j)
i : α
h : p i
⊢ (if { val := i, property := h } = ↑e j then x else (v ∘ ↑e.symm) { val := i, property := h }) =
    if i = ↑(↑e j) then x else v (↑e.symm { val := i, property := h })
[PROOFSTEP]
have h_coe : (⟨i, h⟩ : Subtype p) = e j ↔ i = e j := Subtype.ext_iff.trans (by rw [Subtype.coe_mk])
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : Type u_1
β : Sort u_2
γ : Sort u_3
p : α → Prop
e : β ≃ Subtype p
v : β → γ
w : α → γ
j : β
x : γ
inst✝² : DecidableEq β
inst✝¹ : DecidableEq α
inst✝ : (j : α) → Decidable (p j)
i : α
h : p i
⊢ ↑{ val := i, property := h } = ↑(↑e j) ↔ i = ↑(↑e j)
[PROOFSTEP]
rw [Subtype.coe_mk]
[GOAL]
case pos
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : Type u_1
β : Sort u_2
γ : Sort u_3
p : α → Prop
e : β ≃ Subtype p
v : β → γ
w : α → γ
j : β
x : γ
inst✝² : DecidableEq β
inst✝¹ : DecidableEq α
inst✝ : (j : α) → Decidable (p j)
i : α
h : p i
h_coe : { val := i, property := h } = ↑e j ↔ i = ↑(↑e j)
⊢ (if { val := i, property := h } = ↑e j then x else (v ∘ ↑e.symm) { val := i, property := h }) =
    if i = ↑(↑e j) then x else v (↑e.symm { val := i, property := h })
[PROOFSTEP]
simp [h_coe]
[GOAL]
case neg
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : Type u_1
β : Sort u_2
γ : Sort u_3
p : α → Prop
e : β ≃ Subtype p
v : β → γ
w : α → γ
j : β
x : γ
inst✝² : DecidableEq β
inst✝¹ : DecidableEq α
inst✝ : (j : α) → Decidable (p j)
i : α
h : ¬p i
⊢ (if h : p i then update v j x (↑e.symm { val := i, property := h }) else w i) =
    update (fun i => if h : p i then v (↑e.symm { val := i, property := h }) else w i) (↑(↑e j)) x i
[PROOFSTEP]
have : i ≠ e j := by
  contrapose! h
  have : p (e j : α) := (e j).2
  rwa [← h] at this 
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : Type u_1
β : Sort u_2
γ : Sort u_3
p : α → Prop
e : β ≃ Subtype p
v : β → γ
w : α → γ
j : β
x : γ
inst✝² : DecidableEq β
inst✝¹ : DecidableEq α
inst✝ : (j : α) → Decidable (p j)
i : α
h : ¬p i
⊢ i ≠ ↑(↑e j)
[PROOFSTEP]
contrapose! h
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : Type u_1
β : Sort u_2
γ : Sort u_3
p : α → Prop
e : β ≃ Subtype p
v : β → γ
w : α → γ
j : β
x : γ
inst✝² : DecidableEq β
inst✝¹ : DecidableEq α
inst✝ : (j : α) → Decidable (p j)
i : α
h : i = ↑(↑e j)
⊢ p i
[PROOFSTEP]
have : p (e j : α) := (e j).2
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : Type u_1
β : Sort u_2
γ : Sort u_3
p : α → Prop
e : β ≃ Subtype p
v : β → γ
w : α → γ
j : β
x : γ
inst✝² : DecidableEq β
inst✝¹ : DecidableEq α
inst✝ : (j : α) → Decidable (p j)
i : α
h : i = ↑(↑e j)
this : p ↑(↑e j)
⊢ p i
[PROOFSTEP]
rwa [← h] at this 
[GOAL]
case neg
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : Type u_1
β : Sort u_2
γ : Sort u_3
p : α → Prop
e : β ≃ Subtype p
v : β → γ
w : α → γ
j : β
x : γ
inst✝² : DecidableEq β
inst✝¹ : DecidableEq α
inst✝ : (j : α) → Decidable (p j)
i : α
h : ¬p i
this : i ≠ ↑(↑e j)
⊢ (if h : p i then update v j x (↑e.symm { val := i, property := h }) else w i) =
    update (fun i => if h : p i then v (↑e.symm { val := i, property := h }) else w i) (↑(↑e j)) x i
[PROOFSTEP]
simp [h, this]
