Theorem: Set.Neg.neg.arg_a1.preimage_rule_Ioo (SciLean/Core/FunctionTransformations/Preimage.lean)

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

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

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