case h.mk
α✝ : Type ?u.12591
β : Type ?u.12594
γ : Type ?u.12597
ι : Sort ?u.12600
ι' : Sort ?u.12603
f : α✝ → β
g : β → γ
α : Type u_1
s u v : Set α
hsuv : s ⊆ u ∪ v
H : s ∩ (u ∩ v) = ∅
x : α
x_in_s : x ∈ s
⊢ { val := x, property := x_in_s } ∈ Subtype.val ⁻¹' u ↔ { val := x, property := x_in_s } ∈ (Subtype.val ⁻¹' v)ᶜ
α✝ : Type ?u.12591
β : Type ?u.12594
γ : Type ?u.12597
ι : Sort ?u.12600
ι' : Sort ?u.12603
f : α✝ → β
g : β → γ
α : Type u_1
s u v : Set α
hsuv : s ⊆ u ∪ v
H : s ∩ (u ∩ v) = ∅
⊢ Subtype.val ⁻¹' u = (Subtype.val ⁻¹' v)ᶜ
ext ⟨x, x_in_s⟩
case h.mk.mp
α✝ : Type ?u.12591
β : Type ?u.12594
γ : Type ?u.12597
ι : Sort ?u.12600
ι' : Sort ?u.12603
f : α✝ → β
g : β → γ
α : Type u_1
s u v : Set α
hsuv : s ⊆ u ∪ v
H : s ∩ (u ∩ v) = ∅
x : α
x_in_s : x ∈ s
⊢ { val := x, property := x_in_s } ∈ Subtype.val ⁻¹' u → { val := x, property := x_in_s } ∈ (Subtype.val ⁻¹' v)ᶜ

case h.mk.mpr
α✝ : Type ?u.12591
β : Type ?u.12594
γ : Type ?u.12597
ι : Sort ?u.12600
ι' : Sort ?u.12603
f : α✝ → β
g : β → γ
α : Type u_1
s u v : Set α
hsuv : s ⊆ u ∪ v
H : s ∩ (u ∩ v) = ∅
x : α
x_in_s : x ∈ s
⊢ { val := x, property := x_in_s } ∈ (Subtype.val ⁻¹' v)ᶜ → { val := x, property := x_in_s } ∈ Subtype.val ⁻¹' u
case h.mk
α✝ : Type ?u.12591
β : Type ?u.12594
γ : Type ?u.12597
ι : Sort ?u.12600
ι' : Sort ?u.12603
f : α✝ → β
g : β → γ
α : Type u_1
s u v : Set α
hsuv : s ⊆ u ∪ v
H : s ∩ (u ∩ v) = ∅
x : α
x_in_s : x ∈ s
⊢ { val := x, property := x_in_s } ∈ Subtype.val ⁻¹' u ↔ { val := x, property := x_in_s } ∈ (Subtype.val ⁻¹' v)ᶜ
constructor
case h.mk.mp
α✝ : Type ?u.12591
β : Type ?u.12594
γ : Type ?u.12597
ι : Sort ?u.12600
ι' : Sort ?u.12603
f : α✝ → β
g : β → γ
α : Type u_1
s u v : Set α
hsuv : s ⊆ u ∪ v
H : s ∩ (u ∩ v) = ∅
x : α
x_in_s : x ∈ s
x_in_u : { val := x, property := x_in_s } ∈ Subtype.val ⁻¹' u
x_in_v : { val := x, property := x_in_s } ∈ Subtype.val ⁻¹' v
⊢ False
case h.mk.mp
α✝ : Type ?u.12591
β : Type ?u.12594
γ : Type ?u.12597
ι : Sort ?u.12600
ι' : Sort ?u.12603
f : α✝ → β
g : β → γ
α : Type u_1
s u v : Set α
hsuv : s ⊆ u ∪ v
H : s ∩ (u ∩ v) = ∅
x : α
x_in_s : x ∈ s
⊢ { val := x, property := x_in_s } ∈ Subtype.val ⁻¹' u → { val := x, property := x_in_s } ∈ (Subtype.val ⁻¹' v)ᶜ
intro x_in_u x_in_v
no goals
case h.mk.mp
α✝ : Type ?u.12591
β : Type ?u.12594
γ : Type ?u.12597
ι : Sort ?u.12600
ι' : Sort ?u.12603
f : α✝ → β
g : β → γ
α : Type u_1
s u v : Set α
hsuv : s ⊆ u ∪ v
H : s ∩ (u ∩ v) = ∅
x : α
x_in_s : x ∈ s
x_in_u : { val := x, property := x_in_s } ∈ Subtype.val ⁻¹' u
x_in_v : { val := x, property := x_in_s } ∈ Subtype.val ⁻¹' v
⊢ False
exact eq_empty_iff_forall_not_mem.mp H x ⟨x_in_s, ⟨x_in_u, x_in_v⟩⟩
case h.mk.mpr
α✝ : Type ?u.12591
β : Type ?u.12594
γ : Type ?u.12597
ι : Sort ?u.12600
ι' : Sort ?u.12603
f : α✝ → β
g : β → γ
α : Type u_1
s u v : Set α
hsuv : s ⊆ u ∪ v
H : s ∩ (u ∩ v) = ∅
x : α
x_in_s : x ∈ s
hx : { val := x, property := x_in_s } ∈ (Subtype.val ⁻¹' v)ᶜ
⊢ { val := x, property := x_in_s } ∈ Subtype.val ⁻¹' u
case h.mk.mpr
α✝ : Type ?u.12591
β : Type ?u.12594
γ : Type ?u.12597
ι : Sort ?u.12600
ι' : Sort ?u.12603
f : α✝ → β
g : β → γ
α : Type u_1
s u v : Set α
hsuv : s ⊆ u ∪ v
H : s ∩ (u ∩ v) = ∅
x : α
x_in_s : x ∈ s
⊢ { val := x, property := x_in_s } ∈ (Subtype.val ⁻¹' v)ᶜ → { val := x, property := x_in_s } ∈ Subtype.val ⁻¹' u
intro hx
no goals
case h.mk.mpr
α✝ : Type ?u.12591
β : Type ?u.12594
γ : Type ?u.12597
ι : Sort ?u.12600
ι' : Sort ?u.12603
f : α✝ → β
g : β → γ
α : Type u_1
s u v : Set α
hsuv : s ⊆ u ∪ v
H : s ∩ (u ∩ v) = ∅
x : α
x_in_s : x ∈ s
hx : { val := x, property := x_in_s } ∈ (Subtype.val ⁻¹' v)ᶜ
⊢ { val := x, property := x_in_s } ∈ Subtype.val ⁻¹' u
exact Or.elim (hsuv x_in_s) id fun hx' => hx.elim hx'