-- Mathlib/Data/Finset/Max.lean
theorem card_le_of_interleaved {s t : Finset α}
    (h : ∀ᵉ (x ∈ s) (y ∈ s),
        x < y → (∀ z ∈ s, z ∉ Set.Ioo x y) → ∃ z ∈ t, x < z ∧ z < y) :
    s.card ≤ t.card + 1

Proof state:
α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y
f : α → WithTop α := fun x => (filter (fun y => x < y) t).min
⊢ #s ≤ #t + 1

Tactic:
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)

Result:
α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y
f : α → WithTop α := fun x => (filter (fun y => x < y) t).min
f_mono : StrictMonoOn f ↑s
⊢ #s ≤ #t + 1

Proof state:
case intro.intro.intro
α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → (∀ z ∈ s, z ∉ Set.Ioo x y) → ∃ 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 ∈ s, x < z → a ≤ z
⊢ ∃ z ∈ t, x < z ∧ z < y

Tactic:
rcases h x hx a has hxa fun z hzs hz => hz.2.not_le <| ha _ hzs hz.1 with ⟨b, hbt, hxb, hba⟩

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → (∀ z ∈ s, z ∉ Set.Ioo x y) → ∃ 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 ∈ s, x < z → a ≤ z
b : α
hbt : b ∈ t
hxb : x < b
hba : b < a
⊢ ∃ z ∈ t, x < z ∧ z < y

Proof state:
α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → (∀ z ∈ s, z ∉ Set.Ioo x y) → ∃ z ∈ t, x < z ∧ z < y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x < y
⊢ ∃ z ∈ t, x < z ∧ z < y

Tactic:
rcases exists_next_right ⟨y, hy, hxy⟩ with ⟨a, has, hxa, ha⟩

Result:
case intro.intro.intro
α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → (∀ z ∈ s, z ∉ Set.Ioo x y) → ∃ 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 ∈ s, x < z → a ≤ z
⊢ ∃ z ∈ t, x < z ∧ z < y

Proof state:
α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y
f : α → WithTop α := fun x => (filter (fun y => x < y) t).min
f_mono : StrictMonoOn f ↑s
⊢ #s ≤ #t + 1

Tactic:
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 (Nat.add_le_add_right card_image_le _)

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → (∀ z ∈ s, z ∉ Set.Ioo x y) → ∃ 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 ∈ s, x < z → a ≤ z
b : α
hbt : b ∈ t
hxb : x < b
hba : b < a
⊢ ∃ z ∈ t, x < z ∧ z < y

Tactic:
exact ⟨b, hbt, hxb, hba.trans_le <| ha _ hy hxy⟩

Result:
no goals

Proof state:
α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y
⊢ #s ≤ #t + 1

Tactic:
set f : α → WithTop α := fun x => (t.filter fun y => x < y).min

Result:
α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y
f : α → WithTop α := fun x => (filter (fun y => x < y) t).min
⊢ #s ≤ #t + 1

Proof state:
case intro.intro.intro
α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y
f : α → WithTop α := fun x => (filter (fun y => x < y) t).min
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

Tactic:
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)

Result:
no goals

Proof state:
α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → (∀ z ∈ s, z ∉ Set.Ioo x y) → ∃ z ∈ t, x < z ∧ z < y
⊢ #s ≤ #t + 1

Tactic:
replace h : ∀ᵉ (x ∈ s) (y ∈ s), x < y → ∃ z ∈ t, x < z ∧ z < y := by
  intro x hx y hy hxy
  rcases exists_next_right ⟨y, hy, hxy⟩ with ⟨a, has, hxa, ha⟩
  rcases h x hx a has hxa fun z hzs hz => hz.2.not_le <| ha _ hzs hz.1 with ⟨b, hbt, hxb, hba⟩
  exact ⟨b, hbt, hxb, hba.trans_le <| ha _ hy hxy⟩

Result:
α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y
⊢ #s ≤ #t + 1

Proof state:
α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → (∀ z ∈ s, z ∉ Set.Ioo x y) → ∃ z ∈ t, x < z ∧ z < y
⊢ ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y

Tactic:
intro x hx y hy hxy

Result:
α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → (∀ z ∈ s, z ∉ Set.Ioo x y) → ∃ z ∈ t, x < z ∧ z < y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x < y
⊢ ∃ z ∈ t, x < z ∧ z < y

Proof state:
α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y
f : α → WithTop α := fun x => (filter (fun y => x < y) t).min
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
hxy : x < y
⊢ f x < f y

Tactic:
rcases h x hx y hy hxy with ⟨a, hat, hxa, hay⟩

Result:
case intro.intro.intro
α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y
f : α → WithTop α := fun x => (filter (fun y => x < y) t).min
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

Proof state:
α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y
f : α → WithTop α := fun x => (filter (fun y => x < y) t).min
⊢ StrictMonoOn f ↑s

Tactic:
intro x hx y hy hxy

Result:
α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y
f : α → WithTop α := fun x => (filter (fun y => x < y) t).min
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
hxy : x < y
⊢ f x < f y

Proof state:
α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y
f : α → WithTop α := fun x => (filter (fun y => x < y) t).min
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

Tactic:
simpa using (mem_filter.1 hb).2

Result:
no goals

Proof state:
α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y
f : α → WithTop α := fun x => (filter (fun y => x < y) t).min
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
hxy : x < y
a : α
hat : a ∈ t
hxa : x < a
hay : a < y
⊢ x < a

Tactic:
simpa

Result:
no goals