[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Lattice α
inst✝ : Lattice β
a a₁ a₂ b b₁ b₂ c x : α
h : a ≤ b
⊢ [[a, b]] = Icc a b
[PROOFSTEP]
rw [uIcc, inf_eq_left.2 h, sup_eq_right.2 h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Lattice α
inst✝ : Lattice β
a a₁ a₂ b b₁ b₂ c x : α
h : b ≤ a
⊢ [[a, b]] = Icc b a
[PROOFSTEP]
rw [uIcc, inf_eq_right.2 h, sup_eq_left.2 h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Lattice α
inst✝ : Lattice β
a✝ a₁ a₂ b✝ b₁ b₂ c x a b : α
⊢ [[a, b]] = [[b, a]]
[PROOFSTEP]
simp_rw [uIcc, inf_comm, sup_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Lattice α
inst✝ : Lattice β
a a₁ a₂ b b₁ b₂ c x : α
⊢ [[a, a]] = {a}
[PROOFSTEP]
simp [uIcc]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Lattice α
inst✝ : Lattice β
a✝ a₁ a₂ b✝ b₁ b₂ c x : α
a b : α × β
⊢ [[a, b]] = [[a.fst, b.fst]] ×ˢ [[a.snd, b.snd]]
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DistribLattice α
a a₁ a₂ b b₁ b₂ c x : α
⊢ b ∈ [[a, c]] → c ∈ [[a, b]] → b = c
[PROOFSTEP]
simpa only [uIcc_comm a] using eq_of_mem_uIcc_of_mem_uIcc
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DistribLattice α
a✝ a₁ a₂ b✝ b₁ b₂ c✝ x a b c : α
h : (fun b => [[b, a]]) b = (fun b => [[b, a]]) c
⊢ b = c
[PROOFSTEP]
rw [ext_iff] at h 
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DistribLattice α
a✝ a₁ a₂ b✝ b₁ b₂ c✝ x a b c : α
h : ∀ (x : α), x ∈ (fun b => [[b, a]]) b ↔ x ∈ (fun b => [[b, a]]) c
⊢ b = c
[PROOFSTEP]
exact eq_of_mem_uIcc_of_mem_uIcc ((h _).1 left_mem_uIcc) ((h _).2 left_mem_uIcc)
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DistribLattice α
a✝ a₁ a₂ b b₁ b₂ c x a : α
⊢ Injective (uIcc a)
[PROOFSTEP]
simpa only [uIcc_comm] using uIcc_injective_right a
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
⊢ [[a, b]] = Icc a b ∪ Icc b a
[PROOFSTEP]
rw [Icc_union_Icc', max_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
⊢ [[a, b]] = Icc (min a b) (max a b)
[PROOFSTEP]
rfl
[GOAL]
case h₁
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
⊢ b ≤ b
[PROOFSTEP]
rfl
[GOAL]
case h₂
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
⊢ a ≤ a
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
⊢ a ∈ [[b, c]] ↔ b ≤ a ∧ a ≤ c ∨ c ≤ a ∧ a ≤ b
[PROOFSTEP]
simp [uIcc_eq_union]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x✝ x : α
⊢ x ∈ [[a, c]] → x ∈ [[a, b]] ∪ [[b, c]]
[PROOFSTEP]
simp only [mem_uIcc, mem_union]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x✝ x : α
⊢ a ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
[PROOFSTEP]
cases' le_total a c with h1 h1
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x✝ x : α
h1 : a ≤ c
⊢ a ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
[PROOFSTEP]
cases' le_total x b with h2 h2
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x✝ x : α
h1 : c ≤ a
⊢ a ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
[PROOFSTEP]
cases' le_total x b with h2 h2
[GOAL]
case inl.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x✝ x : α
h1 : a ≤ c
h2 : x ≤ b
⊢ a ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
[PROOFSTEP]
tauto
[GOAL]
case inl.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x✝ x : α
h1 : a ≤ c
h2 : b ≤ x
⊢ a ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
[PROOFSTEP]
tauto
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x✝ x : α
h1 : c ≤ a
h2 : x ≤ b
⊢ a ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
[PROOFSTEP]
tauto
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x✝ x : α
h1 : c ≤ a
h2 : b ≤ x
⊢ a ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
⊢ Monotone f ∨ Antitone f ↔ ∀ (a b c : α), c ∈ [[a, b]] → f c ∈ [[f a, f b]]
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
⊢ Monotone f ∨ Antitone f → ∀ (a b c : α), c ∈ [[a, b]] → f c ∈ [[f a, f b]]
[PROOFSTEP]
rintro (hf | hf) a b c
[GOAL]
case mp.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ a₁ a₂ b✝ b₁ b₂ c✝ x : α
hf : Monotone f
a b c : α
⊢ c ∈ [[a, b]] → f c ∈ [[f a, f b]]
[PROOFSTEP]
simp_rw [← Icc_min_max, ← hf.map_min, ← hf.map_max]
[GOAL]
case mp.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ a₁ a₂ b✝ b₁ b₂ c✝ x : α
hf : Antitone f
a b c : α
⊢ c ∈ [[a, b]] → f c ∈ [[f a, f b]]
[PROOFSTEP]
simp_rw [← Icc_min_max, ← hf.map_min, ← hf.map_max]
[GOAL]
case mp.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ a₁ a₂ b✝ b₁ b₂ c✝ x : α
hf : Monotone f
a b c : α
⊢ c ∈ Icc (min a b) (max a b) → f c ∈ Icc (f (min a b)) (f (max a b))
case mp.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ a₁ a₂ b✝ b₁ b₂ c✝ x : α
hf : Antitone f
a b c : α
⊢ c ∈ Icc (min a b) (max a b) → f c ∈ Icc (f (max a b)) (f (min a b))
[PROOFSTEP]
exacts [fun hc => ⟨hf hc.1, hf hc.2⟩, fun hc => ⟨hf hc.2, hf hc.1⟩]
[GOAL]
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
⊢ (∀ (a b c : α), c ∈ [[a, b]] → f c ∈ [[f a, f b]]) → Monotone f ∨ Antitone f
[PROOFSTEP]
contrapose!
[GOAL]
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
⊢ ¬Monotone f ∧ ¬Antitone f → ∃ a b c, c ∈ [[a, b]] ∧ ¬f c ∈ [[f a, f b]]
[PROOFSTEP]
rw [not_monotone_not_antitone_iff_exists_le_le]
[GOAL]
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
⊢ (∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)) →
    ∃ a b c, c ∈ [[a, b]] ∧ ¬f c ∈ [[f a, f b]]
[PROOFSTEP]
rintro ⟨a, b, c, hab, hbc, ⟨hfab, hfcb⟩ | ⟨hfba, hfbc⟩⟩
[GOAL]
case mpr.intro.intro.intro.intro.intro.inl.intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ a₁ a₂ b✝ b₁ b₂ c✝ x a b c : α
hab : a ≤ b
hbc : b ≤ c
hfab : f a < f b
hfcb : f c < f b
⊢ ∃ a b c, c ∈ [[a, b]] ∧ ¬f c ∈ [[f a, f b]]
[PROOFSTEP]
exact ⟨a, c, b, Icc_subset_uIcc ⟨hab, hbc⟩, fun h => h.2.not_lt <| max_lt hfab hfcb⟩
[GOAL]
case mpr.intro.intro.intro.intro.intro.inr.intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ a₁ a₂ b✝ b₁ b₂ c✝ x a b c : α
hab : a ≤ b
hbc : b ≤ c
hfba : f b < f a
hfbc : f b < f c
⊢ ∃ a b c, c ∈ [[a, b]] ∧ ¬f c ∈ [[f a, f b]]
[PROOFSTEP]
exact ⟨a, c, b, Icc_subset_uIcc ⟨hab, hbc⟩, fun h => h.1.not_lt <| lt_min hfba hfbc⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
⊢ MonotoneOn f s ∨ AntitoneOn f s ↔
    ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → ∀ (c : α), c ∈ s → c ∈ [[a, b]] → f c ∈ [[f a, f b]]
[PROOFSTEP]
simp [monotoneOn_iff_monotone, antitoneOn_iff_antitone, monotone_or_antitone_iff_uIcc, mem_uIcc]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
h : a ≤ b
⊢ Ι a b = Ioc a b
[PROOFSTEP]
simp [uIoc, h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
h : b < a
⊢ Ι a b = Ioc b a
[PROOFSTEP]
simp [uIoc, le_of_lt h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
⊢ Ι a b = Ioc a b ∪ Ioc b a
[PROOFSTEP]
cases le_total a b
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
h✝ : a ≤ b
⊢ Ι a b = Ioc a b ∪ Ioc b a
[PROOFSTEP]
simp [uIoc, *]
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
h✝ : b ≤ a
⊢ Ι a b = Ioc a b ∪ Ioc b a
[PROOFSTEP]
simp [uIoc, *]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
⊢ a ∈ Ι b c ↔ b < a ∧ a ≤ c ∨ c < a ∧ a ≤ b
[PROOFSTEP]
rw [uIoc_eq_union, mem_union, mem_Ioc, mem_Ioc]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
⊢ ¬a ∈ Ι b c ↔ a ≤ b ∧ a ≤ c ∨ c < a ∧ b < a
[PROOFSTEP]
simp only [uIoc_eq_union, mem_union, mem_Ioc, not_lt, ← not_le]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
⊢ ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) ↔ a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
⊢ a ∈ Ι a b ↔ b < a
[PROOFSTEP]
simp [mem_uIoc]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
⊢ b ∈ Ι a b ↔ a < b
[PROOFSTEP]
simp [mem_uIoc]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
P : α → Prop
⊢ (∀ (x : α), x ∈ Ι a b → P x) ↔ (∀ (x : α), x ∈ Ioc a b → P x) ∧ ∀ (x : α), x ∈ Ioc b a → P x
[PROOFSTEP]
simp only [uIoc_eq_union, mem_union, or_imp, forall_and]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ a₁ a₂ b✝ b₁ b₂ c x a b : α
⊢ Ι a b = Ι b a
[PROOFSTEP]
simp only [uIoc, min_comm a b, max_comm a b]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
⊢ a ∈ Ι b c → b ∈ Ι a c → a = b
[PROOFSTEP]
simp_rw [mem_uIoc]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
⊢ b < a ∧ a ≤ c ∨ c < a ∧ a ≤ b → a < b ∧ b ≤ c ∨ c < b ∧ b ≤ a → a = b
[PROOFSTEP]
rintro (⟨_, _⟩ | ⟨_, _⟩) (⟨_, _⟩ | ⟨_, _⟩)
[GOAL]
case inl.intro.inl.intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : a < b
right✝ : b ≤ c
⊢ a = b
[PROOFSTEP]
apply le_antisymm
[GOAL]
case inl.intro.inr.intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : c < b
right✝ : b ≤ a
⊢ a = b
[PROOFSTEP]
apply le_antisymm
[GOAL]
case inr.intro.inl.intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
left✝¹ : c < a
right✝¹ : a ≤ b
left✝ : a < b
right✝ : b ≤ c
⊢ a = b
[PROOFSTEP]
apply le_antisymm
[GOAL]
case inr.intro.inr.intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
left✝¹ : c < a
right✝¹ : a ≤ b
left✝ : c < b
right✝ : b ≤ a
⊢ a = b
[PROOFSTEP]
apply le_antisymm
[GOAL]
case inl.intro.inl.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : a < b
right✝ : b ≤ c
⊢ a ≤ b
[PROOFSTEP]
first
| assumption
| exact le_of_lt ‹_›
| exact le_trans ‹_› (le_of_lt ‹_›)
[GOAL]
case inl.intro.inl.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : a < b
right✝ : b ≤ c
⊢ a ≤ b
[PROOFSTEP]
assumption
[GOAL]
case inl.intro.inl.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : a < b
right✝ : b ≤ c
⊢ a ≤ b
[PROOFSTEP]
exact le_of_lt ‹_›
[GOAL]
case inl.intro.inl.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : a < b
right✝ : b ≤ c
⊢ b ≤ a
[PROOFSTEP]
first
| assumption
| exact le_of_lt ‹_›
| exact le_trans ‹_› (le_of_lt ‹_›)
[GOAL]
case inl.intro.inl.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : a < b
right✝ : b ≤ c
⊢ b ≤ a
[PROOFSTEP]
assumption
[GOAL]
case inl.intro.inl.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : a < b
right✝ : b ≤ c
⊢ b ≤ a
[PROOFSTEP]
exact le_of_lt ‹_›
[GOAL]
case inl.intro.inr.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : c < b
right✝ : b ≤ a
⊢ a ≤ b
[PROOFSTEP]
first
| assumption
| exact le_of_lt ‹_›
| exact le_trans ‹_› (le_of_lt ‹_›)
[GOAL]
case inl.intro.inr.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : c < b
right✝ : b ≤ a
⊢ a ≤ b
[PROOFSTEP]
assumption
[GOAL]
case inl.intro.inr.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : c < b
right✝ : b ≤ a
⊢ a ≤ b
[PROOFSTEP]
exact le_of_lt ‹_›
[GOAL]
case inl.intro.inr.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : c < b
right✝ : b ≤ a
⊢ a ≤ b
[PROOFSTEP]
exact le_trans ‹_› (le_of_lt ‹_›)
[GOAL]
case inl.intro.inr.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : c < b
right✝ : b ≤ a
⊢ b ≤ a
[PROOFSTEP]
first
| assumption
| exact le_of_lt ‹_›
| exact le_trans ‹_› (le_of_lt ‹_›)
[GOAL]
case inl.intro.inr.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : c < b
right✝ : b ≤ a
⊢ b ≤ a
[PROOFSTEP]
assumption
[GOAL]
case inr.intro.inl.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
left✝¹ : c < a
right✝¹ : a ≤ b
left✝ : a < b
right✝ : b ≤ c
⊢ a ≤ b
[PROOFSTEP]
first
| assumption
| exact le_of_lt ‹_›
| exact le_trans ‹_› (le_of_lt ‹_›)
[GOAL]
case inr.intro.inl.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
left✝¹ : c < a
right✝¹ : a ≤ b
left✝ : a < b
right✝ : b ≤ c
⊢ a ≤ b
[PROOFSTEP]
assumption
[GOAL]
case inr.intro.inl.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
left✝¹ : c < a
right✝¹ : a ≤ b
left✝ : a < b
right✝ : b ≤ c
⊢ b ≤ a
[PROOFSTEP]
first
| assumption
| exact le_of_lt ‹_›
| exact le_trans ‹_› (le_of_lt ‹_›)
[GOAL]
case inr.intro.inl.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
left✝¹ : c < a
right✝¹ : a ≤ b
left✝ : a < b
right✝ : b ≤ c
⊢ b ≤ a
[PROOFSTEP]
assumption
[GOAL]
case inr.intro.inl.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
left✝¹ : c < a
right✝¹ : a ≤ b
left✝ : a < b
right✝ : b ≤ c
⊢ b ≤ a
[PROOFSTEP]
exact le_of_lt ‹_›
[GOAL]
case inr.intro.inl.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
left✝¹ : c < a
right✝¹ : a ≤ b
left✝ : a < b
right✝ : b ≤ c
⊢ b ≤ a
[PROOFSTEP]
exact le_trans ‹_› (le_of_lt ‹_›)
[GOAL]
case inr.intro.inr.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
left✝¹ : c < a
right✝¹ : a ≤ b
left✝ : c < b
right✝ : b ≤ a
⊢ a ≤ b
[PROOFSTEP]
first
| assumption
| exact le_of_lt ‹_›
| exact le_trans ‹_› (le_of_lt ‹_›)
[GOAL]
case inr.intro.inr.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
left✝¹ : c < a
right✝¹ : a ≤ b
left✝ : c < b
right✝ : b ≤ a
⊢ a ≤ b
[PROOFSTEP]
assumption
[GOAL]
case inr.intro.inr.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
left✝¹ : c < a
right✝¹ : a ≤ b
left✝ : c < b
right✝ : b ≤ a
⊢ b ≤ a
[PROOFSTEP]
first
| assumption
| exact le_of_lt ‹_›
| exact le_trans ‹_› (le_of_lt ‹_›)
[GOAL]
case inr.intro.inr.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
left✝¹ : c < a
right✝¹ : a ≤ b
left✝ : c < b
right✝ : b ≤ a
⊢ b ≤ a
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
⊢ b ∈ Ι a c → c ∈ Ι a b → b = c
[PROOFSTEP]
simpa only [uIoc_comm a] using eq_of_mem_uIoc_of_mem_uIoc
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
⊢ ¬a ∈ Ι b c → ¬b ∈ Ι a c → a = b
[PROOFSTEP]
simp_rw [not_mem_uIoc]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
⊢ a ≤ b ∧ a ≤ c ∨ c < a ∧ b < a → b ≤ a ∧ b ≤ c ∨ c < b ∧ a < b → a = b
[PROOFSTEP]
rintro (⟨_, _⟩ | ⟨_, _⟩) (⟨_, _⟩ | ⟨_, _⟩)
[GOAL]
case inl.intro.inl.intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : a ≤ b
right✝¹ : a ≤ c
left✝ : b ≤ a
right✝ : b ≤ c
⊢ a = b
[PROOFSTEP]
apply le_antisymm
[GOAL]
case inl.intro.inr.intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : a ≤ b
right✝¹ : a ≤ c
left✝ : c < b
right✝ : a < b
⊢ a = b
[PROOFSTEP]
apply le_antisymm
[GOAL]
case inr.intro.inl.intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : c < a
right✝¹ : b < a
left✝ : b ≤ a
right✝ : b ≤ c
⊢ a = b
[PROOFSTEP]
apply le_antisymm
[GOAL]
case inr.intro.inr.intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : c < a
right✝¹ : b < a
left✝ : c < b
right✝ : a < b
⊢ a = b
[PROOFSTEP]
apply le_antisymm
[GOAL]
case inl.intro.inl.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : a ≤ b
right✝¹ : a ≤ c
left✝ : b ≤ a
right✝ : b ≤ c
⊢ a ≤ b
[PROOFSTEP]
first
| assumption
| exact le_of_lt ‹_›
| exact absurd hb (not_le_of_lt ‹c < b›)
| exact absurd ha (not_le_of_lt ‹c < a›)
[GOAL]
case inl.intro.inl.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : a ≤ b
right✝¹ : a ≤ c
left✝ : b ≤ a
right✝ : b ≤ c
⊢ a ≤ b
[PROOFSTEP]
assumption
[GOAL]
case inl.intro.inl.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : a ≤ b
right✝¹ : a ≤ c
left✝ : b ≤ a
right✝ : b ≤ c
⊢ b ≤ a
[PROOFSTEP]
first
| assumption
| exact le_of_lt ‹_›
| exact absurd hb (not_le_of_lt ‹c < b›)
| exact absurd ha (not_le_of_lt ‹c < a›)
[GOAL]
case inl.intro.inl.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : a ≤ b
right✝¹ : a ≤ c
left✝ : b ≤ a
right✝ : b ≤ c
⊢ b ≤ a
[PROOFSTEP]
assumption
[GOAL]
case inl.intro.inr.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : a ≤ b
right✝¹ : a ≤ c
left✝ : c < b
right✝ : a < b
⊢ a ≤ b
[PROOFSTEP]
first
| assumption
| exact le_of_lt ‹_›
| exact absurd hb (not_le_of_lt ‹c < b›)
| exact absurd ha (not_le_of_lt ‹c < a›)
[GOAL]
case inl.intro.inr.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : a ≤ b
right✝¹ : a ≤ c
left✝ : c < b
right✝ : a < b
⊢ a ≤ b
[PROOFSTEP]
assumption
[GOAL]
case inl.intro.inr.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : a ≤ b
right✝¹ : a ≤ c
left✝ : c < b
right✝ : a < b
⊢ b ≤ a
[PROOFSTEP]
first
| assumption
| exact le_of_lt ‹_›
| exact absurd hb (not_le_of_lt ‹c < b›)
| exact absurd ha (not_le_of_lt ‹c < a›)
[GOAL]
case inl.intro.inr.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : a ≤ b
right✝¹ : a ≤ c
left✝ : c < b
right✝ : a < b
⊢ b ≤ a
[PROOFSTEP]
assumption
[GOAL]
case inl.intro.inr.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : a ≤ b
right✝¹ : a ≤ c
left✝ : c < b
right✝ : a < b
⊢ b ≤ a
[PROOFSTEP]
exact le_of_lt ‹_›
[GOAL]
case inl.intro.inr.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : a ≤ b
right✝¹ : a ≤ c
left✝ : c < b
right✝ : a < b
⊢ b ≤ a
[PROOFSTEP]
exact absurd hb (not_le_of_lt ‹c < b›)
[GOAL]
case inr.intro.inl.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : c < a
right✝¹ : b < a
left✝ : b ≤ a
right✝ : b ≤ c
⊢ a ≤ b
[PROOFSTEP]
first
| assumption
| exact le_of_lt ‹_›
| exact absurd hb (not_le_of_lt ‹c < b›)
| exact absurd ha (not_le_of_lt ‹c < a›)
[GOAL]
case inr.intro.inl.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : c < a
right✝¹ : b < a
left✝ : b ≤ a
right✝ : b ≤ c
⊢ a ≤ b
[PROOFSTEP]
assumption
[GOAL]
case inr.intro.inl.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : c < a
right✝¹ : b < a
left✝ : b ≤ a
right✝ : b ≤ c
⊢ a ≤ b
[PROOFSTEP]
exact le_of_lt ‹_›
[GOAL]
case inr.intro.inl.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : c < a
right✝¹ : b < a
left✝ : b ≤ a
right✝ : b ≤ c
⊢ a ≤ b
[PROOFSTEP]
exact absurd hb (not_le_of_lt ‹c < b›)
[GOAL]
case inr.intro.inl.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : c < a
right✝¹ : b < a
left✝ : b ≤ a
right✝ : b ≤ c
⊢ a ≤ b
[PROOFSTEP]
exact absurd ha (not_le_of_lt ‹c < a›)
[GOAL]
case inr.intro.inl.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : c < a
right✝¹ : b < a
left✝ : b ≤ a
right✝ : b ≤ c
⊢ b ≤ a
[PROOFSTEP]
first
| assumption
| exact le_of_lt ‹_›
| exact absurd hb (not_le_of_lt ‹c < b›)
| exact absurd ha (not_le_of_lt ‹c < a›)
[GOAL]
case inr.intro.inl.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : c < a
right✝¹ : b < a
left✝ : b ≤ a
right✝ : b ≤ c
⊢ b ≤ a
[PROOFSTEP]
assumption
[GOAL]
case inr.intro.inr.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : c < a
right✝¹ : b < a
left✝ : c < b
right✝ : a < b
⊢ a ≤ b
[PROOFSTEP]
first
| assumption
| exact le_of_lt ‹_›
| exact absurd hb (not_le_of_lt ‹c < b›)
| exact absurd ha (not_le_of_lt ‹c < a›)
[GOAL]
case inr.intro.inr.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : c < a
right✝¹ : b < a
left✝ : c < b
right✝ : a < b
⊢ a ≤ b
[PROOFSTEP]
assumption
[GOAL]
case inr.intro.inr.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : c < a
right✝¹ : b < a
left✝ : c < b
right✝ : a < b
⊢ a ≤ b
[PROOFSTEP]
exact le_of_lt ‹_›
[GOAL]
case inr.intro.inr.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : c < a
right✝¹ : b < a
left✝ : c < b
right✝ : a < b
⊢ b ≤ a
[PROOFSTEP]
first
| assumption
| exact le_of_lt ‹_›
| exact absurd hb (not_le_of_lt ‹c < b›)
| exact absurd ha (not_le_of_lt ‹c < a›)
[GOAL]
case inr.intro.inr.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : c < a
right✝¹ : b < a
left✝ : c < b
right✝ : a < b
⊢ b ≤ a
[PROOFSTEP]
assumption
[GOAL]
case inr.intro.inr.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : c < a
right✝¹ : b < a
left✝ : c < b
right✝ : a < b
⊢ b ≤ a
[PROOFSTEP]
exact le_of_lt ‹_›
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ a₁ a₂ b b₁ b₂ c x a : α
⊢ Injective fun b => Ι b a
[PROOFSTEP]
rintro b c h
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ a₁ a₂ b✝ b₁ b₂ c✝ x a b c : α
h : (fun b => Ι b a) b = (fun b => Ι b a) c
⊢ b = c
[PROOFSTEP]
rw [ext_iff] at h 
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ a₁ a₂ b✝ b₁ b₂ c✝ x a b c : α
h : ∀ (x : α), x ∈ (fun b => Ι b a) b ↔ x ∈ (fun b => Ι b a) c
⊢ b = c
[PROOFSTEP]
obtain ha | ha := le_or_lt b a
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ a₁ a₂ b✝ b₁ b₂ c✝ x a b c : α
h : ∀ (x : α), x ∈ (fun b => Ι b a) b ↔ x ∈ (fun b => Ι b a) c
ha : b ≤ a
⊢ b = c
[PROOFSTEP]
have hb := (h b).not
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ a₁ a₂ b✝ b₁ b₂ c✝ x 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
[PROOFSTEP]
simp only [ha, left_mem_uIoc, not_lt, true_iff_iff, not_mem_uIoc, ← not_le, and_true_iff, not_true, false_and_iff,
  not_false_iff, true_iff_iff, or_false_iff] at hb 
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ a₁ a₂ b✝ b₁ b₂ c✝ x 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
[PROOFSTEP]
refine' hb.eq_of_not_lt fun hc => _
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ a₁ a₂ b✝ b₁ b₂ c✝ x 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
[PROOFSTEP]
simpa [ha, and_iff_right hc, ← @not_le _ _ _ a, iff_not_self, -not_le] using h c
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ a₁ a₂ b✝ b₁ b₂ c✝ x a b c : α
h : ∀ (x : α), x ∈ (fun b => Ι b a) b ↔ x ∈ (fun b => Ι b a) c
ha : a < b
⊢ b = c
[PROOFSTEP]
refine' eq_of_mem_uIoc_of_mem_uIoc ((h _).1 <| left_mem_uIoc.2 ha) ((h _).2 <| left_mem_uIoc.2 <| ha.trans_le _)
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ a₁ a₂ b✝ b₁ b₂ c✝ x a b c : α
h : ∀ (x : α), x ∈ (fun b => Ι b a) b ↔ x ∈ (fun b => Ι b a) c
ha : a < b
⊢ b ≤ c
[PROOFSTEP]
simpa [ha, ha.not_le, mem_uIoc] using h b
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ a₁ a₂ b b₁ b₂ c x a : α
⊢ Injective (Ι a)
[PROOFSTEP]
simpa only [uIoc_comm] using uIoc_injective_right a
