-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
lemma preimage_const_mul_Ioi_or_Iio (hb : a ≠ 0) {U V : Set α}
    (hU : U ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a}) (hV : V = HMul.hMul a ⁻¹' U) :
    V ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a}

Proof state:
case h.inl.h
α : Type u_1
inst✝ : LinearOrderedField α
a : α
hb✝ : a ≠ 0
U V : Set α
hV : V = HMul.hMul a ⁻¹' U
aU : α
haU : U = Ioi aU
hb : a < 0
⊢ HMul.hMul a ⁻¹' Ioi aU = Iio (a⁻¹ * aU)

Tactic:
rw [Set.preimage_const_mul_Ioi_of_neg _ hb, div_eq_inv_mul]

Result:
no goals

Proof state:
case h.inl
α : Type u_1
inst✝ : LinearOrderedField α
a : α
hb✝ : a ≠ 0
U V : Set α
hV : V = HMul.hMul a ⁻¹' U
aU : α
haU : U = Ioi aU
hb : a < 0
⊢ HMul.hMul a ⁻¹' Ioi aU = Ioi (a⁻¹ * aU) ∨ HMul.hMul a ⁻¹' Ioi aU = Iio (a⁻¹ * aU)

Tactic:
right

Result:
case h.inl.h
α : Type u_1
inst✝ : LinearOrderedField α
a : α
hb✝ : a ≠ 0
U V : Set α
hV : V = HMul.hMul a ⁻¹' U
aU : α
haU : U = Ioi aU
hb : a < 0
⊢ HMul.hMul a ⁻¹' Ioi aU = Iio (a⁻¹ * aU)

Proof state:
case h.inr
α : Type u_1
inst✝ : LinearOrderedField α
a : α
hb✝ : a ≠ 0
U V : Set α
hV : V = HMul.hMul a ⁻¹' U
aU : α
haU : U = Iio aU
hb : a > 0
⊢ HMul.hMul a ⁻¹' Iio aU = Ioi (a⁻¹ * aU) ∨ HMul.hMul a ⁻¹' Iio aU = Iio (a⁻¹ * aU)

Tactic:
right

Result:
case h.inr.h
α : Type u_1
inst✝ : LinearOrderedField α
a : α
hb✝ : a ≠ 0
U V : Set α
hV : V = HMul.hMul a ⁻¹' U
aU : α
haU : U = Iio aU
hb : a > 0
⊢ HMul.hMul a ⁻¹' Iio aU = Iio (a⁻¹ * aU)

Proof state:
case h.inr
α : Type u_1
inst✝ : LinearOrderedField α
a : α
hb✝ : a ≠ 0
U V : Set α
hV : V = HMul.hMul a ⁻¹' U
aU : α
haU : U = Ioi aU
hb : a > 0
⊢ HMul.hMul a ⁻¹' Ioi aU = Ioi (a⁻¹ * aU) ∨ HMul.hMul a ⁻¹' Ioi aU = Iio (a⁻¹ * aU)

Tactic:
left

Result:
case h.inr.h
α : Type u_1
inst✝ : LinearOrderedField α
a : α
hb✝ : a ≠ 0
U V : Set α
hV : V = HMul.hMul a ⁻¹' U
aU : α
haU : U = Ioi aU
hb : a > 0
⊢ HMul.hMul a ⁻¹' Ioi aU = Ioi (a⁻¹ * aU)

Proof state:
case h.inr.h
α : Type u_1
inst✝ : LinearOrderedField α
a : α
hb✝ : a ≠ 0
U V : Set α
hV : V = HMul.hMul a ⁻¹' U
aU : α
haU : U = Ioi aU
hb : a > 0
⊢ HMul.hMul a ⁻¹' Ioi aU = Ioi (a⁻¹ * aU)

Tactic:
rw [Set.preimage_const_mul_Ioi _ hb, div_eq_inv_mul]

Result:
no goals

Proof state:
case h.inr.h
α : Type u_1
inst✝ : LinearOrderedField α
a : α
hb✝ : a ≠ 0
U V : Set α
hV : V = HMul.hMul a ⁻¹' U
aU : α
haU : U = Iio aU
hb : a > 0
⊢ HMul.hMul a ⁻¹' Iio aU = Iio (a⁻¹ * aU)

Tactic:
rw [Set.preimage_const_mul_Iio _ hb, div_eq_inv_mul]

Result:
no goals

Proof state:
case h.inl
α : Type u_1
inst✝ : LinearOrderedField α
a : α
hb✝ : a ≠ 0
U V : Set α
hV : V = HMul.hMul a ⁻¹' U
aU : α
haU : U = Iio aU
hb : a < 0
⊢ HMul.hMul a ⁻¹' Iio aU = Ioi (a⁻¹ * aU) ∨ HMul.hMul a ⁻¹' Iio aU = Iio (a⁻¹ * aU)

Tactic:
left

Result:
case h.inl.h
α : Type u_1
inst✝ : LinearOrderedField α
a : α
hb✝ : a ≠ 0
U V : Set α
hV : V = HMul.hMul a ⁻¹' U
aU : α
haU : U = Iio aU
hb : a < 0
⊢ HMul.hMul a ⁻¹' Iio aU = Ioi (a⁻¹ * aU)

Proof state:
case h.inl.h
α : Type u_1
inst✝ : LinearOrderedField α
a : α
hb✝ : a ≠ 0
U V : Set α
hV : V = HMul.hMul a ⁻¹' U
aU : α
haU : U = Iio aU
hb : a < 0
⊢ HMul.hMul a ⁻¹' Iio aU = Ioi (a⁻¹ * aU)

Tactic:
rw [Set.preimage_const_mul_Iio_of_neg _ hb, div_eq_inv_mul]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a : α
hb : a ≠ 0
U V : Set α
hU : U ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a}
hV : V = HMul.hMul a ⁻¹' U
⊢ V ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a}

Tactic:
obtain ⟨aU, (haU | haU)⟩ := hU <;>
simp only [hV, haU, mem_setOf_eq] <;>
use a⁻¹ * aU <;>
rcases lt_or_gt_of_ne hb with (hb | hb)

Result:
case h.inl
α : Type u_1
inst✝ : LinearOrderedField α
a : α
hb✝ : a ≠ 0
U V : Set α
hV : V = HMul.hMul a ⁻¹' U
aU : α
haU : U = Ioi aU
hb : a < 0
⊢ HMul.hMul a ⁻¹' Ioi aU = Ioi (a⁻¹ * aU) ∨ HMul.hMul a ⁻¹' Ioi aU = Iio (a⁻¹ * aU)

case h.inr
α : Type u_1
inst✝ : LinearOrderedField α
a : α
hb✝ : a ≠ 0
U V : Set α
hV : V = HMul.hMul a ⁻¹' U
aU : α
haU : U = Ioi aU
hb : a > 0
⊢ HMul.hMul a ⁻¹' Ioi aU = Ioi (a⁻¹ * aU) ∨ HMul.hMul a ⁻¹' Ioi aU = Iio (a⁻¹ * aU)

case h.inl
α : Type u_1
inst✝ : LinearOrderedField α
a : α
hb✝ : a ≠ 0
U V : Set α
hV : V = HMul.hMul a ⁻¹' U
aU : α
haU : U = Iio aU
hb : a < 0
⊢ HMul.hMul a ⁻¹' Iio aU = Ioi (a⁻¹ * aU) ∨ HMul.hMul a ⁻¹' Iio aU = Iio (a⁻¹ * aU)

case h.inr
α : Type u_1
inst✝ : LinearOrderedField α
a : α
hb✝ : a ≠ 0
U V : Set α
hV : V = HMul.hMul a ⁻¹' U
aU : α
haU : U = Iio aU
hb : a > 0
⊢ HMul.hMul a ⁻¹' Iio aU = Ioi (a⁻¹ * aU) ∨ HMul.hMul a ⁻¹' Iio aU = Iio (a⁻¹ * aU)