case h
α : Type u_1
β : Type u_2
γ : Type ?u.39407
f g : α → β
s : Sym2 α
h : ∀ (x : α), x ∈ s → f x = g x
y : β
⊢ y ∈ map f s ↔ y ∈ map g s
α : Type u_1
β : Type u_2
γ : Type ?u.39407
f g : α → β
s : Sym2 α
h : ∀ (x : α), x ∈ s → f x = g x
⊢ map f s = map g s
ext y
case h
α : Type u_1
β : Type u_2
γ : Type ?u.39407
f g : α → β
s : Sym2 α
h : ∀ (x : α), x ∈ s → f x = g x
y : β
⊢ (∃ a, a ∈ s ∧ f a = y) ↔ ∃ a, a ∈ s ∧ g a = y
case h
α : Type u_1
β : Type u_2
γ : Type ?u.39407
f g : α → β
s : Sym2 α
h : ∀ (x : α), x ∈ s → f x = g x
y : β
⊢ y ∈ map f s ↔ y ∈ map g s
simp only [mem_map]
case h.mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.39407
f g : α → β
s : Sym2 α
h : ∀ (x : α), x ∈ s → f x = g x
w : α
hw : w ∈ s
⊢ ∃ a, a ∈ s ∧ f a = g w
case h.mpr
α : Type u_1
β : Type u_2
γ : Type ?u.39407
f g : α → β
s : Sym2 α
h : ∀ (x : α), x ∈ s → f x = g x
y : β
⊢ (∃ a, a ∈ s ∧ g a = y) → ∃ a, a ∈ s ∧ f a = y
rintro ⟨w, hw, rfl⟩
no goals
case h.mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.39407
f g : α → β
s : Sym2 α
h : ∀ (x : α), x ∈ s → f x = g x
w : α
hw : w ∈ s
⊢ ∃ a, a ∈ s ∧ f a = g w
exact ⟨w, hw, by simp [hw, h]⟩
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.39407
f g : α → β
s : Sym2 α
h : ∀ (x : α), x ∈ s → f x = g x
w : α
hw : w ∈ s
⊢ f w = g w
simp [hw, h]