-- Mathlib/Data/Set/Image.lean
theorem powerset_insert (s : Set α) (a : α) : 𝒫 insert a s = 𝒫 s ∪ insert a '' 𝒫 s

Proof state:
case pos.h.refine_1
α : Type u_1
s : Set α
a : α
t : Set α
h : t ⊆ insert a s
hs : a ∈ t
⊢ t ⊆ insert a s

Tactic:
assumption

Result:
no goals

Proof state:
case h.mpr.inr.intro.intro
α : Type u_1
s : Set α
a : α
s' : Set α
h₁ : s' ⊆ s
⊢ insert a s' ⊆ insert a s

Tactic:
exact insert_subset_insert h₁

Result:
no goals

Proof state:
α : Type u_1
s : Set α
a : α
⊢ 𝒫 insert a s = 𝒫 s ∪ insert a '' 𝒫 s

Tactic:
ext t

Result:
case h
α : Type u_1
s : Set α
a : α
t : Set α
⊢ t ∈ 𝒫 insert a s ↔ t ∈ 𝒫 s ∪ insert a '' 𝒫 s

Proof state:
case h.mp
α : Type u_1
s : Set α
a : α
t : Set α
h : t ⊆ insert a s
⊢ t ⊆ s ∨ ∃ x ⊆ s, insert a x = t

Tactic:
by_cases hs : a ∈ t

Result:
case pos
α : Type u_1
s : Set α
a : α
t : Set α
h : t ⊆ insert a s
hs : a ∈ t
⊢ t ⊆ s ∨ ∃ x ⊆ s, insert a x = t

case neg
α : Type u_1
s : Set α
a : α
t : Set α
h : t ⊆ insert a s
hs : a ∉ t
⊢ t ⊆ s ∨ ∃ x ⊆ s, insert a x = t

Proof state:
case h
α : Type u_1
s : Set α
a : α
t : Set α
⊢ t ⊆ insert a s ↔ t ⊆ s ∨ ∃ x ⊆ s, insert a x = t

Tactic:
constructor

Result:
case h.mp
α : Type u_1
s : Set α
a : α
t : Set α
⊢ t ⊆ insert a s → t ⊆ s ∨ ∃ x ⊆ s, insert a x = t

case h.mpr
α : Type u_1
s : Set α
a : α
t : Set α
⊢ (t ⊆ s ∨ ∃ x ⊆ s, insert a x = t) → t ⊆ insert a s

Proof state:
case pos.h.refine_1
α : Type u_1
s : Set α
a : α
t : Set α
h : t ⊆ insert a s
hs : a ∈ t
⊢ t \ {a} ⊆ s

Tactic:
rw [diff_singleton_subset_iff]

Result:
case pos.h.refine_1
α : Type u_1
s : Set α
a : α
t : Set α
h : t ⊆ insert a s
hs : a ∈ t
⊢ t ⊆ insert a s

Proof state:
case h
α : Type u_1
s : Set α
a : α
t : Set α
⊢ t ∈ 𝒫 insert a s ↔ t ∈ 𝒫 s ∪ insert a '' 𝒫 s

Tactic:
simp_rw [mem_union, mem_image, mem_powerset_iff]

Result:
case h
α : Type u_1
s : Set α
a : α
t : Set α
⊢ t ⊆ insert a s ↔ t ⊆ s ∨ ∃ x ⊆ s, insert a x = t

Proof state:
case pos.h
α : Type u_1
s : Set α
a : α
t : Set α
h : t ⊆ insert a s
hs : a ∈ t
⊢ ∃ x ⊆ s, insert a x = t

Tactic:
refine ⟨t \ {a}, ?_, ?_⟩

Result:
case pos.h.refine_1
α : Type u_1
s : Set α
a : α
t : Set α
h : t ⊆ insert a s
hs : a ∈ t
⊢ t \ {a} ⊆ s

case pos.h.refine_2
α : Type u_1
s : Set α
a : α
t : Set α
h : t ⊆ insert a s
hs : a ∈ t
⊢ insert a (t \ {a}) = t

Proof state:
case pos
α : Type u_1
s : Set α
a : α
t : Set α
h : t ⊆ insert a s
hs : a ∈ t
⊢ t ⊆ s ∨ ∃ x ⊆ s, insert a x = t

Tactic:
right

Result:
case pos.h
α : Type u_1
s : Set α
a : α
t : Set α
h : t ⊆ insert a s
hs : a ∈ t
⊢ ∃ x ⊆ s, insert a x = t

Proof state:
case pos.h.refine_2
α : Type u_1
s : Set α
a : α
t : Set α
h : t ⊆ insert a s
hs : a ∈ t
⊢ insert a (t \ {a}) = t

Tactic:
rw [insert_diff_singleton, insert_eq_of_mem hs]

Result:
no goals

Proof state:
case h.mp
α : Type u_1
s : Set α
a : α
t : Set α
⊢ t ⊆ insert a s → t ⊆ s ∨ ∃ x ⊆ s, insert a x = t

Tactic:
intro h

Result:
case h.mp
α : Type u_1
s : Set α
a : α
t : Set α
h : t ⊆ insert a s
⊢ t ⊆ s ∨ ∃ x ⊆ s, insert a x = t

Proof state:
case neg
α : Type u_1
s : Set α
a : α
t : Set α
h : t ⊆ insert a s
hs : a ∉ t
⊢ t ⊆ s ∨ ∃ x ⊆ s, insert a x = t

Tactic:
left

Result:
case neg.h
α : Type u_1
s : Set α
a : α
t : Set α
h : t ⊆ insert a s
hs : a ∉ t
⊢ t ⊆ s

Proof state:
case h.mpr
α : Type u_1
s : Set α
a : α
t : Set α
⊢ (t ⊆ s ∨ ∃ x ⊆ s, insert a x = t) → t ⊆ insert a s

Tactic:
rintro (h | ⟨s', h₁, rfl⟩)

Result:
case h.mpr.inl
α : Type u_1
s : Set α
a : α
t : Set α
h : t ⊆ s
⊢ t ⊆ insert a s

case h.mpr.inr.intro.intro
α : Type u_1
s : Set α
a : α
s' : Set α
h₁ : s' ⊆ s
⊢ insert a s' ⊆ insert a s

Proof state:
case neg.h
α : Type u_1
s : Set α
a : α
t : Set α
h : t ⊆ insert a s
hs : a ∉ t
⊢ t ⊆ s

Tactic:
exact (subset_insert_iff_of_not_mem hs).mp h

Result:
no goals

Proof state:
case h.mpr.inl
α : Type u_1
s : Set α
a : α
t : Set α
h : t ⊆ s
⊢ t ⊆ insert a s

Tactic:
exact subset_trans h (subset_insert a s)

Result:
no goals