case h
α : Type u_1
β : Type ?u.61243
γ : Type ?u.61246
ι : Sort ?u.61249
ι' : Sort ?u.61252
s : Set α
a : α
t : Set α
⊢ t ∈ 𝒫 insert a s ↔ t ∈ 𝒫 s ∪ insert a '' 𝒫 s
α : Type u_1
β : Type ?u.61243
γ : Type ?u.61246
ι : Sort ?u.61249
ι' : Sort ?u.61252
s : Set α
a : α
⊢ 𝒫 insert a s = 𝒫 s ∪ insert a '' 𝒫 s
ext t
case h
α : Type u_1
β : Type ?u.61243
γ : Type ?u.61246
ι : Sort ?u.61249
ι' : Sort ?u.61252
s : Set α
a : α
t : Set α
⊢ t ⊆ insert a s ↔ t ⊆ s ∨ ∃ x, x ⊆ s ∧ insert a x = t
case h
α : Type u_1
β : Type ?u.61243
γ : Type ?u.61246
ι : Sort ?u.61249
ι' : Sort ?u.61252
s : Set α
a : α
t : Set α
⊢ t ∈ 𝒫 insert a s ↔ t ∈ 𝒫 s ∪ insert a '' 𝒫 s
simp_rw [mem_union, mem_image, mem_powerset_iff]
case h.mp
α : Type u_1
β : Type ?u.61243
γ : Type ?u.61246
ι : Sort ?u.61249
ι' : Sort ?u.61252
s : Set α
a : α
t : Set α
⊢ t ⊆ insert a s → t ⊆ s ∨ ∃ x, x ⊆ s ∧ insert a x = t

case h.mpr
α : Type u_1
β : Type ?u.61243
γ : Type ?u.61246
ι : Sort ?u.61249
ι' : Sort ?u.61252
s : Set α
a : α
t : Set α
⊢ (t ⊆ s ∨ ∃ x, x ⊆ s ∧ insert a x = t) → t ⊆ insert a s
case h
α : Type u_1
β : Type ?u.61243
γ : Type ?u.61246
ι : Sort ?u.61249
ι' : Sort ?u.61252
s : Set α
a : α
t : Set α
⊢ t ⊆ insert a s ↔ t ⊆ s ∨ ∃ x, x ⊆ s ∧ insert a x = t
constructor
case h.mp
α : Type u_1
β : Type ?u.61243
γ : Type ?u.61246
ι : Sort ?u.61249
ι' : Sort ?u.61252
s : Set α
a : α
t : Set α
h : t ⊆ insert a s
⊢ t ⊆ s ∨ ∃ x, x ⊆ s ∧ insert a x = t
case h.mp
α : Type u_1
β : Type ?u.61243
γ : Type ?u.61246
ι : Sort ?u.61249
ι' : Sort ?u.61252
s : Set α
a : α
t : Set α
⊢ t ⊆ insert a s → t ⊆ s ∨ ∃ x, x ⊆ s ∧ insert a x = t
intro h
case pos
α : Type u_1
β : Type ?u.61243
γ : Type ?u.61246
ι : Sort ?u.61249
ι' : Sort ?u.61252
s : Set α
a : α
t : Set α
h : t ⊆ insert a s
hs : a ∈ t
⊢ t ⊆ s ∨ ∃ x, x ⊆ s ∧ insert a x = t

case neg
α : Type u_1
β : Type ?u.61243
γ : Type ?u.61246
ι : Sort ?u.61249
ι' : Sort ?u.61252
s : Set α
a : α
t : Set α
h : t ⊆ insert a s
hs : ¬a ∈ t
⊢ t ⊆ s ∨ ∃ x, x ⊆ s ∧ insert a x = t
case h.mp
α : Type u_1
β : Type ?u.61243
γ : Type ?u.61246
ι : Sort ?u.61249
ι' : Sort ?u.61252
s : Set α
a : α
t : Set α
h : t ⊆ insert a s
⊢ t ⊆ s ∨ ∃ x, x ⊆ s ∧ insert a x = t
by_cases hs : a ∈ t
case pos.h
α : Type u_1
β : Type ?u.61243
γ : Type ?u.61246
ι : Sort ?u.61249
ι' : Sort ?u.61252
s : Set α
a : α
t : Set α
h : t ⊆ insert a s
hs : a ∈ t
⊢ ∃ x, x ⊆ s ∧ insert a x = t
case pos
α : Type u_1
β : Type ?u.61243
γ : Type ?u.61246
ι : Sort ?u.61249
ι' : Sort ?u.61252
s : Set α
a : α
t : Set α
h : t ⊆ insert a s
hs : a ∈ t
⊢ t ⊆ s ∨ ∃ x, x ⊆ s ∧ insert a x = t
right
case pos.h.refine'_1
α : Type u_1
β : Type ?u.61243
γ : Type ?u.61246
ι : Sort ?u.61249
ι' : Sort ?u.61252
s : Set α
a : α
t : Set α
h : t ⊆ insert a s
hs : a ∈ t
⊢ t \ {a} ⊆ s

case pos.h.refine'_2
α : Type u_1
β : Type ?u.61243
γ : Type ?u.61246
ι : Sort ?u.61249
ι' : Sort ?u.61252
s : Set α
a : α
t : Set α
h : t ⊆ insert a s
hs : a ∈ t
⊢ insert a (t \ {a}) = t
case pos.h
α : Type u_1
β : Type ?u.61243
γ : Type ?u.61246
ι : Sort ?u.61249
ι' : Sort ?u.61252
s : Set α
a : α
t : Set α
h : t ⊆ insert a s
hs : a ∈ t
⊢ ∃ x, x ⊆ s ∧ insert a x = t
refine' ⟨t \ {a}, _, _⟩
case pos.h.refine'_1
α : Type u_1
β : Type ?u.61243
γ : Type ?u.61246
ι : Sort ?u.61249
ι' : Sort ?u.61252
s : Set α
a : α
t : Set α
h : t ⊆ insert a s
hs : a ∈ t
⊢ t ⊆ insert a s
case pos.h.refine'_1
α : Type u_1
β : Type ?u.61243
γ : Type ?u.61246
ι : Sort ?u.61249
ι' : Sort ?u.61252
s : Set α
a : α
t : Set α
h : t ⊆ insert a s
hs : a ∈ t
⊢ t \ {a} ⊆ s
rw [diff_singleton_subset_iff]
no goals
case pos.h.refine'_1
α : Type u_1
β : Type ?u.61243
γ : Type ?u.61246
ι : Sort ?u.61249
ι' : Sort ?u.61252
s : Set α
a : α
t : Set α
h : t ⊆ insert a s
hs : a ∈ t
⊢ t ⊆ insert a s
assumption
no goals
case pos.h.refine'_2
α : Type u_1
β : Type ?u.61243
γ : Type ?u.61246
ι : Sort ?u.61249
ι' : Sort ?u.61252
s : Set α
a : α
t : Set α
h : t ⊆ insert a s
hs : a ∈ t
⊢ insert a (t \ {a}) = t
rw [insert_diff_singleton, insert_eq_of_mem hs]
case neg.h
α : Type u_1
β : Type ?u.61243
γ : Type ?u.61246
ι : Sort ?u.61249
ι' : Sort ?u.61252
s : Set α
a : α
t : Set α
h : t ⊆ insert a s
hs : ¬a ∈ t
⊢ t ⊆ s
case neg
α : Type u_1
β : Type ?u.61243
γ : Type ?u.61246
ι : Sort ?u.61249
ι' : Sort ?u.61252
s : Set α
a : α
t : Set α
h : t ⊆ insert a s
hs : ¬a ∈ t
⊢ t ⊆ s ∨ ∃ x, x ⊆ s ∧ insert a x = t
left
no goals
case neg.h
α : Type u_1
β : Type ?u.61243
γ : Type ?u.61246
ι : Sort ?u.61249
ι' : Sort ?u.61252
s : Set α
a : α
t : Set α
h : t ⊆ insert a s
hs : ¬a ∈ t
⊢ t ⊆ s
exact (subset_insert_iff_of_not_mem hs).mp h
case h.mpr.inl
α : Type u_1
β : Type ?u.61243
γ : Type ?u.61246
ι : Sort ?u.61249
ι' : Sort ?u.61252
s : Set α
a : α
t : Set α
h : t ⊆ s
⊢ t ⊆ insert a s

case h.mpr.inr.intro.intro
α : Type u_1
β : Type ?u.61243
γ : Type ?u.61246
ι : Sort ?u.61249
ι' : Sort ?u.61252
s : Set α
a : α
s' : Set α
h₁ : s' ⊆ s
⊢ insert a s' ⊆ insert a s
case h.mpr
α : Type u_1
β : Type ?u.61243
γ : Type ?u.61246
ι : Sort ?u.61249
ι' : Sort ?u.61252
s : Set α
a : α
t : Set α
⊢ (t ⊆ s ∨ ∃ x, x ⊆ s ∧ insert a x = t) → t ⊆ insert a s
rintro (h | ⟨s', h₁, rfl⟩)
no goals
case h.mpr.inl
α : Type u_1
β : Type ?u.61243
γ : Type ?u.61246
ι : Sort ?u.61249
ι' : Sort ?u.61252
s : Set α
a : α
t : Set α
h : t ⊆ s
⊢ t ⊆ insert a s
exact subset_trans h (subset_insert a s)
no goals
case h.mpr.inr.intro.intro
α : Type u_1
β : Type ?u.61243
γ : Type ?u.61246
ι : Sort ?u.61249
ι' : Sort ?u.61252
s : Set α
a : α
s' : Set α
h₁ : s' ⊆ s
⊢ insert a s' ⊆ insert a s
exact insert_subset_insert h₁