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

State before:
α : Type ?u.28921
β : Type ?u.28924
γ : Type ?u.28927
R : Type u_1
inst✝ : RealScalar R
x' a b : R
⊢ (fun x => x - x') ⁻¹' Ioo a b = Ioo (a + x') (b + x')
Tactic:
ext
State after:
case h
α : Type ?u.28921
β : Type ?u.28924
γ : Type ?u.28927
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')

State before:
case h
α : Type ?u.28921
β : Type ?u.28924
γ : Type ?u.28927
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')
Tactic:
simp
State after:
case h
α : Type ?u.28921
β : Type ?u.28924
γ : Type ?u.28927
R : Type u_1
inst✝ : RealScalar R
x' a b x✝ : R
⊢ a < x✝ - x' ∧ x✝ - x' < b ↔ a + x' < x✝ ∧ x✝ < b + x'

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