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

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

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

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

case a.mpr
α : Sort u_2
β : Sort u_1
γ : ?m.6074
f : α → β
a : α
p : Prop
y : β
⊢ y ∈ Set.pureIf (f a) p → y ∈ Set.map f (Set.pureIf a p)

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

State before:
case a.mp
α : Sort u_2
β : Sort u_1
γ : ?m.6074
f : α → β
a : α
p : Prop
y : β
hp : p
h : f a = y
⊢ y ∈ Set.pureIf (f a) p
Tactic:
refine ⟨h.symm, hp⟩
State after:
no goals

State before:
case a.mpr
α : Sort u_2
β : Sort u_1
γ : ?m.6074
f : α → β
a : α
p : Prop
y : β
⊢ y ∈ Set.pureIf (f a) p → y ∈ Set.map f (Set.pureIf a p)
Tactic:
intro ⟨h, hp⟩
State after:
case a.mpr
α : Sort u_2
β : Sort u_1
γ : ?m.6074
f : α → β
a : α
p : Prop
y : β
h : y = f a
hp : p
⊢ y ∈ Set.map f (Set.pureIf a p)

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