ext
α : Type ?u.15024
β : Type ?u.15027
γ : Type ?u.15030
R : Type u_1
inst✝ : RealScalar R
x' a b : R
⊢ (fun x => x' + x) ⁻¹' Ioo a b = Ioo (a - x') (b - x')
case h
α : Type ?u.15024
β : Type ?u.15027
γ : Type ?u.15030
R : Type u_1
inst✝ : RealScalar R
x' a b x✝ : R
⊢ x✝ ∈ (fun x => x' + x) ⁻¹' Ioo a b ↔ x✝ ∈ Ioo (a - x') (b - x')