case h
F : Type ?u.388258
α : Type u_1
β : Type ?u.388264
γ : Type ?u.388267
ι : Type ?u.388270
κ : Type ?u.388273
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s t : Finset α
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x < y → (∀ (z : α), z ∈ s → ¬z ∈ Set.Ioo x y) → ∃ z, z ∈ t ∧ x < z ∧ z < y
⊢ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x < y → ∃ z, z ∈ t ∧ x < z ∧ z < y

F : Type ?u.388258
α : Type u_1
β : Type ?u.388264
γ : Type ?u.388267
ι : Type ?u.388270
κ : Type ?u.388273
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s t : Finset α
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x < y → ∃ z, z ∈ t ∧ x < z ∧ z < y
⊢ card s ≤ card t + 1
F : Type ?u.388258
α : Type u_1
β : Type ?u.388264
γ : Type ?u.388267
ι : Type ?u.388270
κ : Type ?u.388273
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s t : Finset α
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x < y → (∀ (z : α), z ∈ s → ¬z ∈ Set.Ioo x y) → ∃ z, z ∈ t ∧ x < z ∧ z < y
⊢ card s ≤ card t + 1
replace h : ∀ (x) (_ : x ∈ s) (y) (_ : y ∈ s), x < y → ∃ z ∈ t, x < z ∧ z < y
F : Type ?u.388258
α : Type u_1
β : Type ?u.388264
γ : Type ?u.388267
ι : Type ?u.388270
κ : Type ?u.388273
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s t : Finset α
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x < y → ∃ z, z ∈ t ∧ x < z ∧ z < y
f : α → WithTop α := fun x => Finset.min (filter (fun y => x < y) t)
⊢ card s ≤ card t + 1
F : Type ?u.388258
α : Type u_1
β : Type ?u.388264
γ : Type ?u.388267
ι : Type ?u.388270
κ : Type ?u.388273
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s t : Finset α
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x < y → ∃ z, z ∈ t ∧ x < z ∧ z < y
⊢ card s ≤ card t + 1
set f : α → WithTop α := fun x => (t.filter fun y => x < y).min
F : Type ?u.388258
α : Type u_1
β : Type ?u.388264
γ : Type ?u.388267
ι : Type ?u.388270
κ : Type ?u.388273
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s t : Finset α
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x < y → ∃ z, z ∈ t ∧ x < z ∧ z < y
f : α → WithTop α := fun x => Finset.min (filter (fun y => x < y) t)
f_mono : StrictMonoOn f ↑s
⊢ card s ≤ card t + 1
F : Type ?u.388258
α : Type u_1
β : Type ?u.388264
γ : Type ?u.388267
ι : Type ?u.388270
κ : Type ?u.388273
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s t : Finset α
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x < y → ∃ z, z ∈ t ∧ x < z ∧ z < y
f : α → WithTop α := fun x => Finset.min (filter (fun y => x < y) t)
⊢ card s ≤ card t + 1
have f_mono : StrictMonoOn f s := by
  intro x hx y hy hxy
  rcases h x hx y hy hxy with ⟨a, hat, hxa, hay⟩
  calc
    f x ≤ a := min_le (mem_filter.2 ⟨hat, by simpa⟩)
    _ < f y :=
      (Finset.lt_inf_iff <| WithTop.coe_lt_top a).2 fun b hb =>
        WithTop.coe_lt_coe.2 <| hay.trans (by simpa using (mem_filter.1 hb).2)
no goals
F : Type ?u.388258
α : Type u_1
β : Type ?u.388264
γ : Type ?u.388267
ι : Type ?u.388270
κ : Type ?u.388273
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s t : Finset α
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x < y → ∃ z, z ∈ t ∧ x < z ∧ z < y
f : α → WithTop α := fun x => Finset.min (filter (fun y => x < y) t)
f_mono : StrictMonoOn f ↑s
⊢ card s ≤ card t + 1
calc
  s.card = (s.image f).card := (card_image_of_injOn f_mono.injOn).symm
  _ ≤ (insert ⊤ (t.image (↑)) : Finset (WithTop α)).card :=
    card_mono <| image_subset_iff.2 fun x _ =>
        insert_subset_insert _ (image_subset_image <| filter_subset _ _)
          (min_mem_insert_top_image_coe _)
  _ ≤ t.card + 1 := (card_insert_le _ _).trans (add_le_add_right card_image_le _)
case h
F : Type ?u.388258
α : Type u_1
β : Type ?u.388264
γ : Type ?u.388267
ι : Type ?u.388270
κ : Type ?u.388273
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x✝ : α
s t : Finset α
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x < y → (∀ (z : α), z ∈ s → ¬z ∈ Set.Ioo x y) → ∃ z, z ∈ t ∧ x < z ∧ z < y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x < y
⊢ ∃ z, z ∈ t ∧ x < z ∧ z < y
case h
F : Type ?u.388258
α : Type u_1
β : Type ?u.388264
γ : Type ?u.388267
ι : Type ?u.388270
κ : Type ?u.388273
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s t : Finset α
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x < y → (∀ (z : α), z ∈ s → ¬z ∈ Set.Ioo x y) → ∃ z, z ∈ t ∧ x < z ∧ z < y
⊢ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x < y → ∃ z, z ∈ t ∧ x < z ∧ z < y
intro x hx y hy hxy
case h.intro.intro.intro
F : Type ?u.388258
α : Type u_1
β : Type ?u.388264
γ : Type ?u.388267
ι : Type ?u.388270
κ : Type ?u.388273
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x✝ : α
s t : Finset α
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x < y → (∀ (z : α), z ∈ s → ¬z ∈ Set.Ioo x y) → ∃ z, z ∈ t ∧ x < z ∧ z < y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x < y
a : α
has : a ∈ s
hxa : x < a
ha : ∀ (z : α), z ∈ s → x < z → a ≤ z
⊢ ∃ z, z ∈ t ∧ x < z ∧ z < y
case h
F : Type ?u.388258
α : Type u_1
β : Type ?u.388264
γ : Type ?u.388267
ι : Type ?u.388270
κ : Type ?u.388273
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x✝ : α
s t : Finset α
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x < y → (∀ (z : α), z ∈ s → ¬z ∈ Set.Ioo x y) → ∃ z, z ∈ t ∧ x < z ∧ z < y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x < y
⊢ ∃ z, z ∈ t ∧ x < z ∧ z < y
rcases exists_next_right ⟨y, hy, hxy⟩ with ⟨a, has, hxa, ha⟩
case h.intro.intro.intro.intro.intro.intro
F : Type ?u.388258
α : Type u_1
β : Type ?u.388264
γ : Type ?u.388267
ι : Type ?u.388270
κ : Type ?u.388273
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x✝ : α
s t : Finset α
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x < y → (∀ (z : α), z ∈ s → ¬z ∈ Set.Ioo x y) → ∃ z, z ∈ t ∧ x < z ∧ z < y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x < y
a : α
has : a ∈ s
hxa : x < a
ha : ∀ (z : α), z ∈ s → x < z → a ≤ z
b : α
hbt : b ∈ t
hxb : x < b
hba : b < a
⊢ ∃ z, z ∈ t ∧ x < z ∧ z < y
case h.intro.intro.intro
F : Type ?u.388258
α : Type u_1
β : Type ?u.388264
γ : Type ?u.388267
ι : Type ?u.388270
κ : Type ?u.388273
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x✝ : α
s t : Finset α
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x < y → (∀ (z : α), z ∈ s → ¬z ∈ Set.Ioo x y) → ∃ z, z ∈ t ∧ x < z ∧ z < y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x < y
a : α
has : a ∈ s
hxa : x < a
ha : ∀ (z : α), z ∈ s → x < z → a ≤ z
⊢ ∃ z, z ∈ t ∧ x < z ∧ z < y
rcases h x hx a has hxa fun z hzs hz => hz.2.not_le <| ha _ hzs hz.1 with ⟨b, hbt, hxb, hba⟩
no goals
case h.intro.intro.intro.intro.intro.intro
F : Type ?u.388258
α : Type u_1
β : Type ?u.388264
γ : Type ?u.388267
ι : Type ?u.388270
κ : Type ?u.388273
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x✝ : α
s t : Finset α
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x < y → (∀ (z : α), z ∈ s → ¬z ∈ Set.Ioo x y) → ∃ z, z ∈ t ∧ x < z ∧ z < y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x < y
a : α
has : a ∈ s
hxa : x < a
ha : ∀ (z : α), z ∈ s → x < z → a ≤ z
b : α
hbt : b ∈ t
hxb : x < b
hba : b < a
⊢ ∃ z, z ∈ t ∧ x < z ∧ z < y
exact ⟨b, hbt, hxb, hba.trans_le <| ha _ hy hxy⟩
F : Type ?u.388258
α : Type u_1
β : Type ?u.388264
γ : Type ?u.388267
ι : Type ?u.388270
κ : Type ?u.388273
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x✝ : α
s t : Finset α
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x < y → ∃ z, z ∈ t ∧ x < z ∧ z < y
f : α → WithTop α := fun x => Finset.min (filter (fun y => x < y) t)
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
hxy : x < y
⊢ f x < f y
F : Type ?u.388258
α : Type u_1
β : Type ?u.388264
γ : Type ?u.388267
ι : Type ?u.388270
κ : Type ?u.388273
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s t : Finset α
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x < y → ∃ z, z ∈ t ∧ x < z ∧ z < y
f : α → WithTop α := fun x => Finset.min (filter (fun y => x < y) t)
⊢ StrictMonoOn f ↑s
intro x hx y hy hxy
case intro.intro.intro
F : Type ?u.388258
α : Type u_1
β : Type ?u.388264
γ : Type ?u.388267
ι : Type ?u.388270
κ : Type ?u.388273
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x✝ : α
s t : Finset α
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x < y → ∃ z, z ∈ t ∧ x < z ∧ z < y
f : α → WithTop α := fun x => Finset.min (filter (fun y => x < y) t)
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
hxy : x < y
a : α
hat : a ∈ t
hxa : x < a
hay : a < y
⊢ f x < f y
F : Type ?u.388258
α : Type u_1
β : Type ?u.388264
γ : Type ?u.388267
ι : Type ?u.388270
κ : Type ?u.388273
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x✝ : α
s t : Finset α
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x < y → ∃ z, z ∈ t ∧ x < z ∧ z < y
f : α → WithTop α := fun x => Finset.min (filter (fun y => x < y) t)
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
hxy : x < y
⊢ f x < f y
rcases h x hx y hy hxy with ⟨a, hat, hxa, hay⟩
no goals
case intro.intro.intro
F : Type ?u.388258
α : Type u_1
β : Type ?u.388264
γ : Type ?u.388267
ι : Type ?u.388270
κ : Type ?u.388273
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x✝ : α
s t : Finset α
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x < y → ∃ z, z ∈ t ∧ x < z ∧ z < y
f : α → WithTop α := fun x => Finset.min (filter (fun y => x < y) t)
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
hxy : x < y
a : α
hat : a ∈ t
hxa : x < a
hay : a < y
⊢ f x < f y
calc
  f x ≤ a := min_le (mem_filter.2 ⟨hat, by simpa⟩)
  _ < f y :=
    (Finset.lt_inf_iff <| WithTop.coe_lt_top a).2 fun b hb =>
      WithTop.coe_lt_coe.2 <| hay.trans (by simpa using (mem_filter.1 hb).2)
no goals
F : Type ?u.388258
α : Type u_1
β : Type ?u.388264
γ : Type ?u.388267
ι : Type ?u.388270
κ : Type ?u.388273
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x✝ : α
s t : Finset α
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x < y → ∃ z, z ∈ t ∧ x < z ∧ z < y
f : α → WithTop α := fun x => Finset.min (filter (fun y => x < y) t)
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
hxy : x < y
a : α
hat : a ∈ t
hxa : x < a
hay : a < y
⊢ x < a
simpa
no goals
F : Type ?u.388258
α : Type u_1
β : Type ?u.388264
γ : Type ?u.388267
ι : Type ?u.388270
κ : Type ?u.388273
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x✝ : α
s t : Finset α
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x < y → ∃ z, z ∈ t ∧ x < z ∧ z < y
f : α → WithTop α := fun x => Finset.min (filter (fun y => x < y) t)
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
hxy : x < y
a : α
hat : a ∈ t
hxa : x < a
hay : a < y
b : α
hb : b ∈ filter (fun y_1 => y < y_1) t
⊢ y < b
simpa using (mem_filter.1 hb).2