α : Type u_1
β : Type u_2
γ : Type ?u.45305
ι : Sort ?u.45308
ι' : Sort ?u.45311
f✝ : α → β
s✝ t : Set α
f : α → β
g : β → α
b : β
s : Set α
h₁ : LeftInverse g f
h₂ : Function.RightInverse g f
⊢ b ∈ g ⁻¹' s ↔ g b ∈ s
α : Type u_1
β : Type u_2
γ : Type ?u.45305
ι : Sort ?u.45308
ι' : Sort ?u.45311
f✝ : α → β
s✝ t : Set α
f : α → β
g : β → α
b : β
s : Set α
h₁ : LeftInverse g f
h₂ : Function.RightInverse g f
⊢ b ∈ f '' s ↔ g b ∈ s
rw [image_eq_preimage_of_inverse h₁ h₂]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.45305
ι : Sort ?u.45308
ι' : Sort ?u.45311
f✝ : α → β
s✝ t : Set α
f : α → β
g : β → α
b : β
s : Set α
h₁ : LeftInverse g f
h₂ : Function.RightInverse g f
⊢ b ∈ g ⁻¹' s ↔ g b ∈ s
rfl