Theorem: Set.union_map (GMLInit/Data/Set/Basic.lean)

State before:
α : Sort u_1
β : Sort u_2
γ : ?m.18682
f : α → β
s t : Set α
⊢ Set.map f (s.union t) = (Set.map f s).union (Set.map f t)
Tactic:
apply Set.ext
State after:
case a
α : Sort u_1
β : Sort u_2
γ : ?m.18682
f : α → β
s t : Set α
⊢ ∀ (x : β), x ∈ Set.map f (s.union t) ↔ x ∈ (Set.map f s).union (Set.map f t)

State before:
case a
α : Sort u_1
β : Sort u_2
γ : ?m.18682
f : α → β
s t : Set α
⊢ ∀ (x : β), x ∈ Set.map f (s.union t) ↔ x ∈ (Set.map f s).union (Set.map f t)
Tactic:
intro y
State after:
case a
α : Sort u_1
β : Sort u_2
γ : ?m.18682
f : α → β
s t : Set α
y : β
⊢ y ∈ Set.map f (s.union t) ↔ y ∈ (Set.map f s).union (Set.map f t)

State before:
case a
α : Sort u_1
β : Sort u_2
γ : ?m.18682
f : α → β
s t : Set α
y : β
⊢ y ∈ Set.map f (s.union t) ↔ y ∈ (Set.map f s).union (Set.map f t)
Tactic:
constructor
State after:
case a.mp
α : Sort u_1
β : Sort u_2
γ : ?m.18682
f : α → β
s t : Set α
y : β
⊢ y ∈ Set.map f (s.union t) → y ∈ (Set.map f s).union (Set.map f t)

case a.mpr
α : Sort u_1
β : Sort u_2
γ : ?m.18682
f : α → β
s t : Set α
y : β
⊢ y ∈ (Set.map f s).union (Set.map f t) → y ∈ Set.map f (s.union t)

State before:
case a.mp
α : Sort u_1
β : Sort u_2
γ : ?m.18682
f : α → β
s t : Set α
y : β
⊢ y ∈ Set.map f (s.union t) → y ∈ (Set.map f s).union (Set.map f t)
Tactic:
open Or in intro
| ⟨x, inl hs, h⟩ => left; refine ⟨x, hs, h⟩
| ⟨x, inr ht, h⟩ => right; refine ⟨x, ht, h⟩
State after:
no goals

State before:
case a.mp
α : Sort u_1
β : Sort u_2
γ : ?m.18682
f : α → β
s t : Set α
y : β
⊢ y ∈ Set.map f (s.union t) → y ∈ (Set.map f s).union (Set.map f t)
Tactic:
intro
| ⟨x, inl hs, h⟩ => left; refine ⟨x, hs, h⟩
| ⟨x, inr ht, h⟩ => right; refine ⟨x, ht, h⟩
State after:
no goals

State before:
α : Sort u_1
β : Sort u_2
γ : ?m.18682
f : α → β
s t : Set α
y : β
x✝ : y ∈ Set.map f (s.union t)
x : α
hs : x ∈ s
h : f x = y
⊢ y ∈ (Set.map f s).union (Set.map f t)
Tactic:
left
State after:
case h
α : Sort u_1
β : Sort u_2
γ : ?m.18682
f : α → β
s t : Set α
y : β
x✝ : y ∈ Set.map f (s.union t)
x : α
hs : x ∈ s
h : f x = y
⊢ y ∈ Set.map f s

State before:
case h
α : Sort u_1
β : Sort u_2
γ : ?m.18682
f : α → β
s t : Set α
y : β
x✝ : y ∈ Set.map f (s.union t)
x : α
hs : x ∈ s
h : f x = y
⊢ y ∈ Set.map f s
Tactic:
refine ⟨x, hs, h⟩
State after:
no goals

State before:
α : Sort u_1
β : Sort u_2
γ : ?m.18682
f : α → β
s t : Set α
y : β
x✝ : y ∈ Set.map f (s.union t)
x : α
ht : x ∈ t
h : f x = y
⊢ y ∈ (Set.map f s).union (Set.map f t)
Tactic:
right
State after:
case h
α : Sort u_1
β : Sort u_2
γ : ?m.18682
f : α → β
s t : Set α
y : β
x✝ : y ∈ Set.map f (s.union t)
x : α
ht : x ∈ t
h : f x = y
⊢ y ∈ Set.map f t

State before:
case h
α : Sort u_1
β : Sort u_2
γ : ?m.18682
f : α → β
s t : Set α
y : β
x✝ : y ∈ Set.map f (s.union t)
x : α
ht : x ∈ t
h : f x = y
⊢ y ∈ Set.map f t
Tactic:
refine ⟨x, ht, h⟩
State after:
no goals

State before:
case a.mpr
α : Sort u_1
β : Sort u_2
γ : ?m.18682
f : α → β
s t : Set α
y : β
⊢ y ∈ (Set.map f s).union (Set.map f t) → y ∈ Set.map f (s.union t)
Tactic:
open Or in intro
| inl ⟨x, hs, h⟩ => refine ⟨x, inl hs, h⟩
| inr ⟨x, ht, h⟩ => refine ⟨x, inr ht, h⟩
State after:
no goals

State before:
case a.mpr
α : Sort u_1
β : Sort u_2
γ : ?m.18682
f : α → β
s t : Set α
y : β
⊢ y ∈ (Set.map f s).union (Set.map f t) → y ∈ Set.map f (s.union t)
Tactic:
intro
| inl ⟨x, hs, h⟩ => refine ⟨x, inl hs, h⟩
| inr ⟨x, ht, h⟩ => refine ⟨x, inr ht, h⟩
State after:
no goals

State before:
α : Sort u_1
β : Sort u_2
γ : ?m.18682
f : α → β
s t : Set α
y : β
x✝ : y ∈ (Set.map f s).union (Set.map f t)
x : α
hs : x ∈ s
h : f x = y
⊢ y ∈ Set.map f (s.union t)
Tactic:
refine ⟨x, inl hs, h⟩
State after:
no goals

State before:
α : Sort u_1
β : Sort u_2
γ : ?m.18682
f : α → β
s t : Set α
y : β
x✝ : y ∈ (Set.map f s).union (Set.map f t)
x : α
ht : x ∈ t
h : f x = y
⊢ y ∈ Set.map f (s.union t)
Tactic:
refine ⟨x, inr ht, h⟩
State after:
no goals