-- Module: Mathlib.Order.CountableDenseLinearOrder
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
inst_2 : DenselyOrdered β
inst_3 : NoMinOrder β
inst_4 : NoMaxOrder β
nonem : Nonempty β
S : Finset α
f : OrderEmbedding.{u_1, u_2} (↥S) β
a : α
Slt : Finset β := Finset.image (⇑f : (a : ↥S) → β) ({x ∈ S.attach | (↑x : α) < a})
Sgt : Finset β := Finset.image (⇑f : (a : ↥S) → β) ({x ∈ S.attach | a < (↑x : α)})
b : β
hb : ∀ x ∈ Slt, x < b
hb' : ∀ y ∈ Sgt, b < y
x : α
hx : x ∈ insert a S
y : α
hy : y ∈ insert a S
hxy : Subtype.mk (p := fun (x : α) ↦ x ∈ insert a S) x hx < Subtype.mk (p := fun (x : α) ↦ x ∈ insert a S) y hy
if :
  ∀ (hxS : x ∈ S),
    LT.lt.{u_2} (α := β)
      ((fun (x : ↥(insert a S)) ↦
          (if hx : (↑x : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x : α) hx) else b : β))
        (Subtype.mk (p := fun (x : α) ↦ x ∈ insert a S) x hx))
      ((fun (x : ↥(insert a S)) ↦
          (if hx : (↑x : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x : α) hx) else b : β))
        (Subtype.mk (p := fun (x : α) ↦ x ∈ insert a S) y hy))
if₁ :
  ∀ (hxS : x ∉ S),
    LT.lt.{u_2} (α := β)
      ((fun (x : ↥(insert a S)) ↦
          (if hx : (↑x : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x : α) hx) else b : β))
        (Subtype.mk (p := fun (x : α) ↦ x ∈ insert a S) x hx))
      ((fun (x : ↥(insert a S)) ↦
          (if hx : (↑x : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x : α) hx) else b : β))
        (Subtype.mk (p := fun (x : α) ↦ x ∈ insert a S) y hy))
if₂ :
  ∀ (hxS : x ∈ S),
    LT.lt.{u_2} (α := β)
      ((fun (x : ↥(insert a S)) ↦
          (if hx : (↑x : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x : α) hx) else b : β))
        (Subtype.mk (p := fun (x : α) ↦ x ∈ insert a S) x hx))
      ((fun (x : ↥(insert a S)) ↦
          (if hx : (↑x : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x : α) hx) else b : β))
        (Subtype.mk (p := fun (x : α) ↦ x ∈ insert a S) y hy))
if₃ if₄ :
  ∀ (hxS : x ∉ S),
    LT.lt.{u_2} (α := β)
      ((fun (x : ↥(insert a S)) ↦
          (if hx : (↑x : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x : α) hx) else b : β))
        (Subtype.mk (p := fun (x : α) ↦ x ∈ insert a S) x hx))
      ((fun (x : ↥(insert a S)) ↦
          (if hx : (↑x : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x : α) hx) else b : β))
        (Subtype.mk (p := fun (x : α) ↦ x ∈ insert a S) y hy))
⊢ LT.lt.{u_2} (α := β)
    ((fun (x : ↥(insert a S)) ↦
        (if hx : (↑x : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x : α) hx) else b : β))
      (Subtype.mk (p := fun (x : α) ↦ x ∈ insert a S) x hx))
    ((fun (x : ↥(insert a S)) ↦
        (if hx : (↑x : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x : α) hx) else b : β))
      (Subtype.mk (p := fun (x : α) ↦ x ∈ insert a S) 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_notMem 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_notMem 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_notMem hy hyS, lt_self_iff_false] at hxy

Premises used: Iff.mpr, Subtype.mk_lt_mk, Finset.mem_attach, reduceDIte, lt_self_iff_false, And.intro, Finset.mem_filter, OrderEmbedding.lt_iff_lt, Finset.mem_image_of_mem, rfl