case h
α : Type u_1
β : Type u_2
γ : Type ?u.27036
ι : Sort ?u.27039
ι' : Sort ?u.27042
f✝ : α → β
s✝ t : Set α
f g : α → β
s : Set α
h : ∀ (a : α), a ∈ s → f a = g a
x : β
⊢ x ∈ f '' s ↔ x ∈ g '' s
α : Type u_1
β : Type u_2
γ : Type ?u.27036
ι : Sort ?u.27039
ι' : Sort ?u.27042
f✝ : α → β
s✝ t : Set α
f g : α → β
s : Set α
h : ∀ (a : α), a ∈ s → f a = g a
⊢ f '' s = g '' s
ext x
case h
α : Type u_1
β : Type u_2
γ : Type ?u.27036
ι : Sort ?u.27039
ι' : Sort ?u.27042
f✝ : α → β
s✝ t : Set α
f g : α → β
s : Set α
h : ∀ (a : α), a ∈ s → f a = g a
x : β
⊢ (∃ x_1, x_1 ∈ s ∧ f x_1 = x) ↔ ∃ x_1, x_1 ∈ s ∧ g x_1 = x
case h
α : Type u_1
β : Type u_2
γ : Type ?u.27036
ι : Sort ?u.27039
ι' : Sort ?u.27042
f✝ : α → β
s✝ t : Set α
f g : α → β
s : Set α
h : ∀ (a : α), a ∈ s → f a = g a
x : β
⊢ x ∈ f '' s ↔ x ∈ g '' s
rw [mem_image, mem_image]
no goals
case h
α : Type u_1
β : Type u_2
γ : Type ?u.27036
ι : Sort ?u.27039
ι' : Sort ?u.27042
f✝ : α → β
s✝ t : Set α
f g : α → β
s : Set α
h : ∀ (a : α), a ∈ s → f a = g a
x : β
⊢ (∃ x_1, x_1 ∈ s ∧ f x_1 = x) ↔ ∃ x_1, x_1 ∈ s ∧ g x_1 = x
exact {
  mp := by
    rintro ⟨a, ha1, ha2⟩
    exact ⟨a, ⟨ha1, (h a ha1) ▸ ha2⟩⟩,
  mpr := by
    rintro ⟨a, ha1, ha2⟩
    exact ⟨a, ⟨ha1, (h a ha1) ▸ ha2⟩⟩
}
case intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.27036
ι : Sort ?u.27039
ι' : Sort ?u.27042
f✝ : α → β
s✝ t : Set α
f g : α → β
s : Set α
h : ∀ (a : α), a ∈ s → f a = g a
x : β
a : α
ha1 : a ∈ s
ha2 : f a = x
⊢ ∃ x_1, x_1 ∈ s ∧ g x_1 = x
α : Type u_1
β : Type u_2
γ : Type ?u.27036
ι : Sort ?u.27039
ι' : Sort ?u.27042
f✝ : α → β
s✝ t : Set α
f g : α → β
s : Set α
h : ∀ (a : α), a ∈ s → f a = g a
x : β
⊢ (∃ x_1, x_1 ∈ s ∧ f x_1 = x) → ∃ x_1, x_1 ∈ s ∧ g x_1 = x
rintro ⟨a, ha1, ha2⟩
no goals
case intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.27036
ι : Sort ?u.27039
ι' : Sort ?u.27042
f✝ : α → β
s✝ t : Set α
f g : α → β
s : Set α
h : ∀ (a : α), a ∈ s → f a = g a
x : β
a : α
ha1 : a ∈ s
ha2 : f a = x
⊢ ∃ x_1, x_1 ∈ s ∧ g x_1 = x
exact ⟨a, ⟨ha1, (h a ha1) ▸ ha2⟩⟩
case intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.27036
ι : Sort ?u.27039
ι' : Sort ?u.27042
f✝ : α → β
s✝ t : Set α
f g : α → β
s : Set α
h : ∀ (a : α), a ∈ s → f a = g a
x : β
a : α
ha1 : a ∈ s
ha2 : g a = x
⊢ ∃ x_1, x_1 ∈ s ∧ f x_1 = x
α : Type u_1
β : Type u_2
γ : Type ?u.27036
ι : Sort ?u.27039
ι' : Sort ?u.27042
f✝ : α → β
s✝ t : Set α
f g : α → β
s : Set α
h : ∀ (a : α), a ∈ s → f a = g a
x : β
⊢ (∃ x_1, x_1 ∈ s ∧ g x_1 = x) → ∃ x_1, x_1 ∈ s ∧ f x_1 = x
rintro ⟨a, ha1, ha2⟩
no goals
case intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.27036
ι : Sort ?u.27039
ι' : Sort ?u.27042
f✝ : α → β
s✝ t : Set α
f g : α → β
s : Set α
h : ∀ (a : α), a ∈ s → f a = g a
x : β
a : α
ha1 : a ∈ s
ha2 : g a = x
⊢ ∃ x_1, x_1 ∈ s ∧ f x_1 = x
exact ⟨a, ⟨ha1, (h a ha1) ▸ ha2⟩⟩