-- 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)
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:
obtain rfl := Finset.eq_of_mem_insert_of_not_mem hy hyS

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

Tactic:
let Sgt := (S.attach.filter (fun (x : S) => a < x)).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)
Sgt : Finset β := Finset.image (⇑f) (Finset.filter (fun x => a < ↑x) S.attach)
⊢ ∃ 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 : α
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
⊢ (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:
obtain rfl := Finset.eq_of_mem_insert_of_not_mem hx hxS

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

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
⊢ (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 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⟩))

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⟩
hyS : y ∈ S
⊢ b < f ⟨y, ⋯⟩

Tactic:
exact hb' _ (Finset.mem_image_of_mem _ (Finset.mem_filter.2 ⟨Finset.mem_attach _ _, hxy⟩))

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⟩
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 [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
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
⊢ b < f ⟨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
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

Tactic:
exact hb _ (Finset.mem_image_of_mem _ (Finset.mem_filter.2 ⟨Finset.mem_attach _ _, hxy⟩))

Result:
no goals