-- 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) β
b : β
x y : α
hxS : x ∉ S
Slt : Finset β := Finset.image (⇑f : (a : ↥S) → β) ({x_1 ∈ S.attach | (↑x_1 : α) < x})
Sgt : Finset β := Finset.image (⇑f : (a : ↥S) → β) ({x_1 ∈ S.attach | x < (↑x_1 : α)})
hb : ∀ x ∈ Slt, x < b
hb' : ∀ y ∈ Sgt, b < y
hx : x ∈ insert x S
hy : y ∈ insert x S
hxy : Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ insert x S) x hx < Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ insert x S) y hy
if :
  ∀ (hyS : y ∈ S),
    LT.lt.{u_2} (α := β)
      ((fun (x_1 : ↥(insert x S)) ↦
          (if hx : (↑x_1 : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x_1 : α) hx) else b :
            β))
        (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ insert x S) x hx))
      ((fun (x_1 : ↥(insert x S)) ↦
          (if hx : (↑x_1 : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x_1 : α) hx) else b :
            β))
        (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ insert x S) y hy))
if₁ :
  ∀ (hyS : y ∉ S),
    LT.lt.{u_2} (α := β)
      ((fun (x_1 : ↥(insert x S)) ↦
          (if hx : (↑x_1 : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x_1 : α) hx) else b :
            β))
        (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ insert x S) x hx))
      ((fun (x_1 : ↥(insert x S)) ↦
          (if hx : (↑x_1 : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x_1 : α) hx) else b :
            β))
        (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ insert x S) y hy))
if₂ :
  ∀ (hyS : y ∈ S),
    LT.lt.{u_2} (α := β)
      ((fun (x_1 : ↥(insert x S)) ↦
          (if hx : (↑x_1 : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x_1 : α) hx) else b :
            β))
        (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ insert x S) x hx))
      ((fun (x_1 : ↥(insert x S)) ↦
          (if hx : (↑x_1 : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x_1 : α) hx) else b :
            β))
        (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ insert x S) y hy))
if₃ if₄ :
  ∀ (hyS : y ∉ S),
    LT.lt.{u_2} (α := β)
      ((fun (x_1 : ↥(insert x S)) ↦
          (if hx : (↑x_1 : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x_1 : α) hx) else b :
            β))
        (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ insert x S) x hx))
      ((fun (x_1 : ↥(insert x S)) ↦
          (if hx : (↑x_1 : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x_1 : α) hx) else b :
            β))
        (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ insert x S) y hy))
⊢ LT.lt.{u_2} (α := β)
    ((fun (x_1 : ↥(insert x S)) ↦
        (if hx : (↑x_1 : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x_1 : α) hx) else b :
          β))
      (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ insert x S) x hx))
    ((fun (x_1 : ↥(insert x S)) ↦
        (if hx : (↑x_1 : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x_1 : α) hx) else b :
          β))
      (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ insert x S) 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_notMem hy hyS, lt_self_iff_false] at hxy

Premises used: Iff.mpr, Finset.mem_attach, reduceDIte, lt_self_iff_false, And.intro, Finset.mem_filter, Finset.mem_image_of_mem