Theorem: Set.HSub.hSub.arg_a1.preimage_rule_Ioo (SciLean/Core/FunctionTransformations/Preimage.lean)

State before:
α : Type ?u.44212
β : Type ?u.44215
γ : Type ?u.44218
R : Type u_1
inst✝ : RealScalar R
x' a b : R
⊢ (fun x => x' - x) ⁻¹' Ioo a b = Ioo (x' - b) (x' - a)
Tactic:
ext
State after:
case h
α : Type ?u.44212
β : Type ?u.44215
γ : Type ?u.44218
R : Type u_1
inst✝ : RealScalar R
x' a b x✝ : R
⊢ x✝ ∈ (fun x => x' - x) ⁻¹' Ioo a b ↔ x✝ ∈ Ioo (x' - b) (x' - a)

State before:
case h
α : Type ?u.44212
β : Type ?u.44215
γ : Type ?u.44218
R : Type u_1
inst✝ : RealScalar R
x' a b x✝ : R
⊢ x✝ ∈ (fun x => x' - x) ⁻¹' Ioo a b ↔ x✝ ∈ Ioo (x' - b) (x' - a)
Tactic:
simp
State after:
case h
α : Type ?u.44212
β : Type ?u.44215
γ : Type ?u.44218
R : Type u_1
inst✝ : RealScalar R
x' a b x✝ : R
⊢ a < x' - x✝ ∧ x' - x✝ < b ↔ x' - b < x✝ ∧ x✝ < x' - a

State before:
case h
α : Type ?u.44212
β : Type ?u.44215
γ : Type ?u.44218
R : Type u_1
inst✝ : RealScalar R
x' a b x✝ : R
⊢ a < x' - x✝ ∧ x' - x✝ < b ↔ x' - b < x✝ ∧ x✝ < x' - a
Tactic:
sorry_proof
State after:
no goals