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

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

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

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

case a.mpr
α : Sort u_2
β : Sort u_1
γ : ?m.5720
f : α → β
a : α
y : β
⊢ y ∈ Set.pure (f a) → y ∈ Set.map f (Set.pure a)

State before:
case a.mp
α : Sort u_2
β : Sort u_1
γ : ?m.5720
f : α → β
a : α
y : β
⊢ y ∈ Set.map f (Set.pure a) → y ∈ Set.pure (f a)
Tactic:
intro ⟨_, rfl, h⟩
State after:
case a.mp
α : Sort u_2
β : Sort u_1
γ : ?m.5720
f : α → β
a : α
y : β
h : f a = y
⊢ y ∈ Set.pure (f a)

State before:
case a.mp
α : Sort u_2
β : Sort u_1
γ : ?m.5720
f : α → β
a : α
y : β
h : f a = y
⊢ y ∈ Set.pure (f a)
Tactic:
rw [←h]
State after:
case a.mp
α : Sort u_2
β : Sort u_1
γ : ?m.5720
f : α → β
a : α
y : β
h : f a = y
⊢ f a ∈ Set.pure (f a)

State before:
case a.mp
α : Sort u_2
β : Sort u_1
γ : ?m.5720
f : α → β
a : α
y : β
h : f a = y
⊢ f a ∈ Set.pure (f a)
Tactic:
rfl
State after:
no goals

State before:
case a.mpr
α : Sort u_2
β : Sort u_1
γ : ?m.5720
f : α → β
a : α
y : β
⊢ y ∈ Set.pure (f a) → y ∈ Set.map f (Set.pure a)
Tactic:
intro (h : y = f a)
State after:
case a.mpr
α : Sort u_2
β : Sort u_1
γ : ?m.5720
f : α → β
a : α
y : β
h : y = f a
⊢ y ∈ Set.map f (Set.pure a)

State before:
case a.mpr
α : Sort u_2
β : Sort u_1
γ : ?m.5720
f : α → β
a : α
y : β
h : y = f a
⊢ y ∈ Set.map f (Set.pure a)
Tactic:
refine ⟨a, rfl, h.symm⟩
State after:
no goals