-- Mathlib/Order/CountableDenseLinearOrder.lean
lemma exists_orderEmbedding_insert [DenselyOrdered β] [NoMinOrder β] [NoMaxOrder β]
    [nonem : Nonempty β]  (S : Finset α) (f : S ↪o β) (a : α) :
    ∃ (g : (insert a S : Finset α) ↪o β),
      g ∘ (Set.inclusion ((S.subset_insert a) : ↑S ⊆ ↑(insert a S))) = f

Proof state:
case intro.intro.refine_1.mk.mk
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : DenselyOrdered β
inst✝¹ : NoMinOrder β
inst✝ : NoMaxOrder β
nonem : Nonempty β
S : Finset α
f : { x // x ∈ S } ↪o β
a : α
Slt : Finset β := Finset.image (⇑f) (Finset.filter (fun x => ↑x < a) S.attach)
Sgt : Finset β := Finset.image (⇑f) (Finset.filter (fun x => a < ↑x) S.attach)
b : β
hb : ∀ x ∈ Slt, x < b
hb' : ∀ y ∈ Sgt, b < y
x : α
hx : x ∈ insert a S
y : α
hy : y ∈ insert a S
hxy : ⟨x, hx⟩ < ⟨y, hy⟩
⊢ (fun x => if hx : ↑x ∈ S then f ⟨↑x, hx⟩ else b) ⟨x, hx⟩ < (fun x => if hx : ↑x ∈ S then f ⟨↑x, hx⟩ else b) ⟨y, hy⟩

Tactic:
if hxS : x ∈ S
then if hyS : y ∈ S
  then simpa only [hxS, hyS, ↓reduceDIte, OrderEmbedding.lt_iff_lt, Subtype.mk_lt_mk]
  else
    obtain rfl := Finset.eq_of_mem_insert_of_not_mem hy hyS
    simp only [hxS, hyS, ↓reduceDIte]
    exact hb _ (Finset.mem_image_of_mem _ (Finset.mem_filter.2 ⟨Finset.mem_attach _ _, hxy⟩))
else
  obtain rfl := Finset.eq_of_mem_insert_of_not_mem hx hxS
  if hyS : y ∈ S
  then
    simp only [hxS, hyS, ↓reduceDIte]
    exact hb' _ (Finset.mem_image_of_mem _ (Finset.mem_filter.2 ⟨Finset.mem_attach _ _, hxy⟩))
  else simp only [Finset.eq_of_mem_insert_of_not_mem hy hyS, lt_self_iff_false] at hxy

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : DenselyOrdered β
inst✝¹ : NoMinOrder β
inst✝ : NoMaxOrder β
nonem : Nonempty β
S : Finset α
f : { x // x ∈ S } ↪o β
a : α
Slt : Finset β := Finset.image (⇑f) (Finset.filter (fun x => ↑x < a) S.attach)
Sgt : Finset β := Finset.image (⇑f) (Finset.filter (fun x => a < ↑x) S.attach)
w✝³ : α
hx : w✝³ < a
w✝² : w✝³ ∈ S
w✝¹ : α
hy : a < w✝¹
w✝ : w✝¹ ∈ S
⊢ f ⟨w✝³, ⋯⟩ < f ⟨w✝¹, ⋯⟩

Tactic:
exact f.strictMono (hx.trans hy)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : DenselyOrdered β
inst✝¹ : NoMinOrder β
inst✝ : NoMaxOrder β
nonem : Nonempty β
S : Finset α
f : { x // x ∈ S } ↪o β
a : α
Slt : Finset β := Finset.image (⇑f) (Finset.filter (fun x => ↑x < a) S.attach)
Sgt : Finset β := Finset.image (⇑f) (Finset.filter (fun x => a < ↑x) S.attach)
x y : β
hx : ∃ a_1 < a, ∃ (x_1 : a_1 ∈ S), f ⟨a_1, ⋯⟩ = x
hy : ∃ a_1, a < a_1 ∧ ∃ (x : a_1 ∈ S), f ⟨a_1, ⋯⟩ = y
⊢ x < y

Tactic:
obtain ⟨_, hx, _, rfl⟩ := hx

Result:
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : DenselyOrdered β
inst✝¹ : NoMinOrder β
inst✝ : NoMaxOrder β
nonem : Nonempty β
S : Finset α
f : { x // x ∈ S } ↪o β
a : α
Slt : Finset β := Finset.image (⇑f) (Finset.filter (fun x => ↑x < a) S.attach)
Sgt : Finset β := Finset.image (⇑f) (Finset.filter (fun x => a < ↑x) S.attach)
y : β
hy : ∃ a_1, a < a_1 ∧ ∃ (x : a_1 ∈ S), f ⟨a_1, ⋯⟩ = y
w✝¹ : α
hx : w✝¹ < a
w✝ : w✝¹ ∈ S
⊢ f ⟨w✝¹, ⋯⟩ < y

Proof state:
case intro.intro.refine_2.h
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : DenselyOrdered β
inst✝¹ : NoMinOrder β
inst✝ : NoMaxOrder β
nonem : Nonempty β
S : Finset α
f : { x // x ∈ S } ↪o β
a : α
Slt : Finset β := Finset.image (⇑f) (Finset.filter (fun x => ↑x < a) S.attach)
Sgt : Finset β := Finset.image (⇑f) (Finset.filter (fun x => a < ↑x) S.attach)
b : β
hb : ∀ x ∈ Slt, x < b
hb' : ∀ y ∈ Sgt, b < y
x : ↑(Membership.mem S.val)
⊢ (⇑(OrderEmbedding.ofStrictMono (fun x => if hx : ↑x ∈ S then f ⟨↑x, hx⟩ else b) ⋯) ∘ Set.inclusion ⋯) x = f x

Tactic:
simp only [Finset.coe_sort_coe, OrderEmbedding.coe_ofStrictMono, Finset.insert_val,
  Function.comp_apply, Finset.coe_mem, ↓reduceDIte, Subtype.coe_eta]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : DenselyOrdered β
inst✝¹ : NoMinOrder β
inst✝ : NoMaxOrder β
nonem : Nonempty β
S : Finset α
f : { x // x ∈ S } ↪o β
b : β
x y : α
hxS : x ∉ S
Slt : Finset β := Finset.image (⇑f) (Finset.filter (fun x_1 => ↑x_1 < x) S.attach)
Sgt : Finset β := Finset.image (⇑f) (Finset.filter (fun x_1 => x < ↑x_1) S.attach)
hb : ∀ x ∈ Slt, x < b
hb' : ∀ y ∈ Sgt, b < y
hx : x ∈ insert x S
hy : y ∈ insert x S
hxy : ⟨x, hx⟩ < ⟨y, hy⟩
⊢ (fun x_1 => if hx : ↑x_1 ∈ S then f ⟨↑x_1, hx⟩ else b) ⟨x, hx⟩ <
    (fun x_1 => if hx : ↑x_1 ∈ S then f ⟨↑x_1, hx⟩ else b) ⟨y, hy⟩

Tactic:
if hyS : y ∈ S
then
  simp only [hxS, hyS, ↓reduceDIte]
  exact hb' _ (Finset.mem_image_of_mem _ (Finset.mem_filter.2 ⟨Finset.mem_attach _ _, hxy⟩))
else simp only [Finset.eq_of_mem_insert_of_not_mem hy hyS, lt_self_iff_false] at hxy

Result:
no goals

Proof state:
case intro.intro.refine_1
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : DenselyOrdered β
inst✝¹ : NoMinOrder β
inst✝ : NoMaxOrder β
nonem : Nonempty β
S : Finset α
f : { x // x ∈ S } ↪o β
a : α
Slt : Finset β := Finset.image (⇑f) (Finset.filter (fun x => ↑x < a) S.attach)
Sgt : Finset β := Finset.image (⇑f) (Finset.filter (fun x => a < ↑x) S.attach)
b : β
hb : ∀ x ∈ Slt, x < b
hb' : ∀ y ∈ Sgt, b < y
⊢ StrictMono fun x => if hx : ↑x ∈ S then f ⟨↑x, hx⟩ else b

Tactic:
rintro ⟨x, hx⟩ ⟨y, hy⟩ hxy

Result:
case intro.intro.refine_1.mk.mk
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : DenselyOrdered β
inst✝¹ : NoMinOrder β
inst✝ : NoMaxOrder β
nonem : Nonempty β
S : Finset α
f : { x // x ∈ S } ↪o β
a : α
Slt : Finset β := Finset.image (⇑f) (Finset.filter (fun x => ↑x < a) S.attach)
Sgt : Finset β := Finset.image (⇑f) (Finset.filter (fun x => a < ↑x) S.attach)
b : β
hb : ∀ x ∈ Slt, x < b
hb' : ∀ y ∈ Sgt, b < y
x : α
hx : x ∈ insert a S
y : α
hy : y ∈ insert a S
hxy : ⟨x, hx⟩ < ⟨y, hy⟩
⊢ (fun x => if hx : ↑x ∈ S then f ⟨↑x, hx⟩ else b) ⟨x, hx⟩ < (fun x => if hx : ↑x ∈ S then f ⟨↑x, hx⟩ else b) ⟨y, hy⟩

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : DenselyOrdered β
inst✝¹ : NoMinOrder β
inst✝ : NoMaxOrder β
nonem : Nonempty β
S : Finset α
f : { x // x ∈ S } ↪o β
b : β
x y : α
hxS : x ∈ S
hyS : y ∉ S
Slt : Finset β := Finset.image (⇑f) (Finset.filter (fun x => ↑x < y) S.attach)
Sgt : Finset β := Finset.image (⇑f) (Finset.filter (fun x => y < ↑x) S.attach)
hb : ∀ x ∈ Slt, x < b
hb' : ∀ y ∈ Sgt, b < y
hx : x ∈ insert y S
hy : y ∈ insert y S
hxy : ⟨x, hx⟩ < ⟨y, hy⟩
⊢ (fun x => if hx : ↑x ∈ S then f ⟨↑x, hx⟩ else b) ⟨x, hx⟩ < (fun x => if hx : ↑x ∈ S then f ⟨↑x, hx⟩ else b) ⟨y, hy⟩

Tactic:
simp only [hxS, hyS, ↓reduceDIte]

Result:
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : DenselyOrdered β
inst✝¹ : NoMinOrder β
inst✝ : NoMaxOrder β
nonem : Nonempty β
S : Finset α
f : { x // x ∈ S } ↪o β
b : β
x y : α
hxS : x ∈ S
hyS : y ∉ S
Slt : Finset β := Finset.image (⇑f) (Finset.filter (fun x => ↑x < y) S.attach)
Sgt : Finset β := Finset.image (⇑f) (Finset.filter (fun x => y < ↑x) S.attach)
hb : ∀ x ∈ Slt, x < b
hb' : ∀ y ∈ Sgt, b < y
hx : x ∈ insert y S
hy : y ∈ insert y S
hxy : ⟨x, hx⟩ < ⟨y, hy⟩
⊢ f ⟨x, ⋯⟩ < b