-- Mathlib/Order/Interval/Set/UnorderedInterval.lean
lemma uIoc_injective_right (a : α) : Injective fun b => Ι b a

Proof state:
case inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : ∀ (x : α), x ∈ (fun b => Ι b a) b ↔ x ∈ (fun b => Ι b a) c
ha : b ≤ a
hb : b ≤ c
⊢ b = c

Tactic:
refine hb.eq_of_not_lt fun hc => ?_

Result:
case inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : ∀ (x : α), x ∈ (fun b => Ι b a) b ↔ x ∈ (fun b => Ι b a) c
ha : b ≤ a
hb : b ≤ c
hc : b < c
⊢ False

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : ∀ (x : α), x ∈ (fun b => Ι b a) b ↔ x ∈ (fun b => Ι b a) c
⊢ b = c

Tactic:
obtain ha | ha := le_or_lt b a

Result:
case inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : ∀ (x : α), x ∈ (fun b => Ι b a) b ↔ x ∈ (fun b => Ι b a) c
ha : b ≤ a
⊢ b = c

case inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : ∀ (x : α), x ∈ (fun b => Ι b a) b ↔ x ∈ (fun b => Ι b a) c
ha : a < b
⊢ b = c

Proof state:
case inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : ∀ (x : α), x ∈ (fun b => Ι b a) b ↔ x ∈ (fun b => Ι b a) c
ha : a < b
⊢ b ≤ c

Tactic:
simpa [ha, ha.not_le, mem_uIoc] using h b

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : ∀ (x : α), x ∈ (fun b => Ι b a) b ↔ x ∈ (fun b => Ι b a) c
ha : b ≤ a
hb : b ≤ c
hc : b < c
⊢ False

Tactic:
simpa [ha, and_iff_right hc, ← @not_le _ _ _ a, iff_not_self, -not_le] using h c

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a : α
⊢ Injective fun b => Ι b a

Tactic:
rintro b c h

Result:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : (fun b => Ι b a) b = (fun b => Ι b a) c
⊢ b = c

Proof state:
case inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : ∀ (x : α), x ∈ (fun b => Ι b a) b ↔ x ∈ (fun b => Ι b a) c
ha : a < b
⊢ b = c

Tactic:
refine
  eq_of_mem_uIoc_of_mem_uIoc ((h _).1 <| left_mem_uIoc.2 ha)
    ((h _).2 <| left_mem_uIoc.2 <| ha.trans_le ?_)

Result:
case inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : ∀ (x : α), x ∈ (fun b => Ι b a) b ↔ x ∈ (fun b => Ι b a) c
ha : a < b
⊢ b ≤ c

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : (fun b => Ι b a) b = (fun b => Ι b a) c
⊢ b = c

Tactic:
rw [Set.ext_iff] at h

Result:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : ∀ (x : α), x ∈ (fun b => Ι b a) b ↔ x ∈ (fun b => Ι b a) c
⊢ b = c

Proof state:
case inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : ∀ (x : α), x ∈ (fun b => Ι b a) b ↔ x ∈ (fun b => Ι b a) c
ha : b ≤ a
hb : b ∉ (fun b => Ι b a) b ↔ b ∉ (fun b => Ι b a) c
⊢ b = c

Tactic:
simp only [ha, left_mem_uIoc, not_lt, true_iff, not_mem_uIoc, ← not_le,
  and_true, not_true, false_and, not_false_iff, or_false] at hb

Result:
case inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : ∀ (x : α), x ∈ (fun b => Ι b a) b ↔ x ∈ (fun b => Ι b a) c
ha : b ≤ a
hb : b ≤ c
⊢ b = c

Proof state:
case inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : ∀ (x : α), x ∈ (fun b => Ι b a) b ↔ x ∈ (fun b => Ι b a) c
ha : b ≤ a
⊢ b = c

Tactic:
have hb := (h b).not

Result:
case inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : ∀ (x : α), x ∈ (fun b => Ι b a) b ↔ x ∈ (fun b => Ι b a) c
ha : b ≤ a
hb : b ∉ (fun b => Ι b a) b ↔ b ∉ (fun b => Ι b a) c
⊢ b = c