-- 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:
α : 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 : β
hx : x ∈ Slt
y : β
hy : y ∈ Sgt
⊢ x < y

Tactic:
simp only [Finset.mem_image, Finset.mem_filter, Finset.mem_attach, true_and, Subtype.exists,
  exists_and_left, Slt, Sgt] at hx hy

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 β
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

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⟩
hyS : y ∉ S
⊢ (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:
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_2
α : 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
⊢ ⇑(OrderEmbedding.ofStrictMono (fun x => if hx : ↑x ∈ S then f ⟨↑x, hx⟩ else b) ⋯) ∘ Set.inclusion ⋯ = ⇑f

Tactic:
ext x

Result:
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

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)
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⟩
hxS : x ∈ S
hyS : y ∈ S
⊢ (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:
simpa only [hxS, hyS, ↓reduceDIte, OrderEmbedding.lt_iff_lt, Subtype.mk_lt_mk]

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)
⊢ ∃ g, ⇑g ∘ Set.inclusion ⋯ = ⇑f

Tactic:
obtain ⟨b, hb, hb'⟩ := Order.exists_between_finsets Slt Sgt (fun x hx y hy => by
  simp only [Finset.mem_image, Finset.mem_filter, Finset.mem_attach, true_and, Subtype.exists,
    exists_and_left, Slt, Sgt] at hx hy
  obtain ⟨_, hx, _, rfl⟩ := hx
  obtain ⟨_, hy, _, rfl⟩ := hy
  exact f.strictMono (hx.trans hy))

Result:
case 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)
b : β
hb : ∀ x ∈ Slt, x < b
hb' : ∀ y ∈ Sgt, b < y
⊢ ∃ g, ⇑g ∘ Set.inclusion ⋯ = ⇑f

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 : α
⊢ ∃ g, ⇑g ∘ Set.inclusion ⋯ = ⇑f

Tactic:
let Slt := (S.attach.filter (fun (x : S) => x < a)).image f

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 β
a : α
Slt : Finset β := Finset.image (⇑f) (Finset.filter (fun x => ↑x < a) S.attach)
⊢ ∃ g, ⇑g ∘ Set.inclusion ⋯ = ⇑f

Proof state:
case 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)
b : β
hb : ∀ x ∈ Slt, x < b
hb' : ∀ y ∈ Sgt, b < y
⊢ ∃ g, ⇑g ∘ Set.inclusion ⋯ = ⇑f

Tactic:
refine ⟨OrderEmbedding.ofStrictMono
  (fun (x : (insert a S : Finset α)) => if hx : x.1 ∈ S then f ⟨x.1, hx⟩ else b) ?_, ?_⟩

Result:
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

case intro.intro.refine_2
α : 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
⊢ ⇑(OrderEmbedding.ofStrictMono (fun x => if hx : ↑x ∈ S then f ⟨↑x, hx⟩ else b) ?intro.intro.refine_1) ∘
      Set.inclusion ⋯ =
    ⇑f