awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : CompleteDistribLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sdiff : α → α → α
eq_sdiff : sdiff = SDiff.sdiff
hnot : α → α
⊢ HNot α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : CompleteDistribLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sdiff : α → α → α
eq_sdiff : sdiff = SDiff.sdiff
hnot : α → α
eq_hnot : hnot = HNot.hnot
himp : α → α → α
⊢ HImp α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : CompleteDistribLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sdiff : α → α → α
eq_sdiff : sdiff = SDiff.sdiff
hnot : α → α
eq_hnot : hnot = HNot.hnot
himp : α → α → α
eq_himp : himp = HImp.himp
compl : α → α
⊢ Compl α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : CompleteDistribLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sdiff : α → α → α
eq_sdiff : sdiff = SDiff.sdiff
hnot : α → α
eq_hnot : hnot = HNot.hnot
himp : α → α → α
eq_himp : himp = HImp.himp
compl : α → α
eq_compl : compl = Compl.compl
sSup : Set α → α
⊢ SupSet α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : CompleteDistribLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sdiff : α → α → α
eq_sdiff : sdiff = SDiff.sdiff
hnot : α → α
eq_hnot : hnot = HNot.hnot
himp : α → α → α
eq_himp : himp = HImp.himp
compl : α → α
eq_compl : compl = Compl.compl
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
⊢ InfSet α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
⊢ LE α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
⊢ Max α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
⊢ Min α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sSup : Set α → α
⊢ SupSet α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
⊢ InfSet α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
subst_vars : ∀ (s : Set α), s.Nonempty → BddAbove s → IsLUB s (SupSet.sSup s)
⊢ ∀ (s : Set α), s.Nonempty → BddAbove s → IsLUB s (sSup s)

Tactic:
subst_vars
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : ConditionallyCompleteLattice α
__Lattice : Lattice α := Lattice.copy toLattice LE.le ⋯ max ⋯ min ⋯
⊢ ∀ (s : Set α), s.Nonempty → BddAbove s → IsLUB s (sSup s)

Tactic:
c.isLUB_csSup

Premises used: ConditionallyCompleteLattice.isLUB_csSup
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : ConditionallyCompleteLattice α
__Lattice : Lattice α := Lattice.copy toLattice LE.le ⋯ max ⋯ min ⋯
⊢ ∀ (s : Set α), s.Nonempty → BddAbove s → IsLUB s (sSup s)

Tactic:
exact c.isLUB_csSup

Premises used: ConditionallyCompleteLattice.isLUB_csSup
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
subst_vars : ∀ (s : Set α), s.Nonempty → BddBelow s → IsGLB s (InfSet.sInf s)
⊢ ∀ (s : Set α), s.Nonempty → BddBelow s → IsGLB s (sInf s)

Tactic:
subst_vars
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : ConditionallyCompleteLattice α
__Lattice : Lattice α := Lattice.copy toLattice LE.le ⋯ max ⋯ min ⋯
⊢ ∀ (s : Set α), s.Nonempty → BddBelow s → IsGLB s (sInf s)

Tactic:
c.isGLB_csInf

Premises used: ConditionallyCompleteLattice.isGLB_csInf
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : ConditionallyCompleteLattice α
__Lattice : Lattice α := Lattice.copy toLattice LE.le ⋯ max ⋯ min ⋯
⊢ ∀ (s : Set α), s.Nonempty → BddBelow s → IsGLB s (sInf s)

Tactic:
exact c.isGLB_csInf

Premises used: ConditionallyCompleteLattice.isGLB_csInf
-- Module: Mathlib.Order.CountableDenseLinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : NoMinOrder α
inst_3 : NoMaxOrder α
nonem : Nonempty α
lo hi : Finset α
lo_lt_hi : ∀ x ∈ lo, ∀ y ∈ hi, x < y
⊢ ∃ (m : α), (∀ x ∈ lo, x < m) ∧ ∀ y ∈ hi, m < y

Tactic:
if nlo : lo.Nonempty then
    if nhi : hi.Nonempty then
      -- both sets are nonempty, use `DenselyOrdered`
        Exists.elim
        (exists_between (lo_lt_hi _ (Finset.max'_mem _ nlo) _ (Finset.min'_mem _ nhi))) fun m hm ↦
        ⟨m, fun x hx ↦ lt_of_le_of_lt (Finset.le_max' lo x hx) hm.1, fun y hy ↦
          lt_of_lt_of_le hm.2 (Finset.min'_le hi y hy)⟩
    else -- upper set is empty, use `NoMaxOrder`
        Exists.elim
        (exists_gt (Finset.max' lo nlo)) fun m hm ↦
        ⟨m, fun x hx ↦ lt_of_le_of_lt (Finset.le_max' lo x hx) hm, fun y hy ↦ (nhi ⟨y, hy⟩).elim⟩
  else
    if nhi : hi.Nonempty then
      -- lower set is empty, use `NoMinOrder`
        Exists.elim
        (exists_lt (Finset.min' hi nhi)) fun m hm ↦
        ⟨m, fun x hx ↦ (nlo ⟨x, hx⟩).elim, fun y hy ↦ lt_of_lt_of_le hm (Finset.min'_le hi y hy)⟩
    else -- both sets are empty, use `Nonempty`
          nonem.elim
        fun m ↦ ⟨m, fun x hx ↦ (nlo ⟨x, hx⟩).elim, fun y hy ↦ (nhi ⟨y, hy⟩).elim⟩

Premises used: Finset.min', lt_of_le_of_lt, Finset.min'_le, Nonempty.elim, Finset.max'_mem, False.elim, Finset.min'_mem, Finset.max', NoMaxOrder.exists_gt, exists_between, dite, And.right, And.left, Finset.le_max', And.intro, Exists.intro, Finset.Nonempty, NoMinOrder.exists_lt, lt_of_lt_of_le, Exists.elim
-- 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 : α)})
x : β
hx : x ∈ Slt
y : β
hy : y ∈ Sgt
⊢ ∃ a_1 < a, ∃ (x_1 : a_1 ∈ S), (f : (a : ↥S) → β) (Subtype.mk (p := fun (a : α) ↦ a ∈ S) a_1 ⋯) = x

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

Premises used: Finset.mem_image, Finset.mem_attach, Subtype.exists, exists_and_left, Finset.mem_filter, true_and
-- 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 : α)})
x : β
hx : x ∈ Slt
y : β
hy : y ∈ Sgt
hx₁ : ∃ a_1 < a, ∃ (x_1 : a_1 ∈ S), (f : (a : ↥S) → β) (Subtype.mk (p := fun (a : α) ↦ a ∈ S) a_1 ⋯) = x
⊢ ∃ (a_1 : α), a < a_1 ∧ ∃ (x : a_1 ∈ S), (f : (a : ↥S) → β) (Subtype.mk (p := fun (a : α) ↦ a ∈ S) a_1 ⋯) = 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

Premises used: Finset.mem_image, Finset.mem_attach, Subtype.exists, exists_and_left, Finset.mem_filter, true_and
-- 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 : α)})
x y : β
hx : ∃ a_1 < a, ∃ (x_1 : a_1 ∈ S), (f : (a : ↥S) → β) (Subtype.mk (p := fun (a : α) ↦ a ∈ S) a_1 ⋯) = x
hy : ∃ (a_1 : α), a < a_1 ∧ ∃ (x : a_1 ∈ S), (f : (a : ↥S) → β) (Subtype.mk (p := fun (a : α) ↦ a ∈ S) a_1 ⋯) = y
obtain : ∀ (w : α) (hx : w < a) (w_1 : w ∈ S), (f : (a : ↥S) → β) (Subtype.mk (p := fun (a : α) ↦ a ∈ S) w ⋯) < y
⊢ x < y

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

Premises used: rfl
-- 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 : α)})
y : β
hy : ∃ (a_1 : α), a < a_1 ∧ ∃ (x : a_1 ∈ S), (f : (a : ↥S) → β) (Subtype.mk (p := fun (a : α) ↦ a ∈ S) a_1 ⋯) = y
w : α
hx : w < a
w_1 : w ∈ S
obtain :
  ∀ (w_2 : α) (hy : a < w_2) (w_3 : w_2 ∈ S),
    LT.lt.{u_2} (α := β) ((f : (a : ↥S) → β) (Subtype.mk (p := fun (a : α) ↦ a ∈ S) w ⋯) : β)
      ((f : (a : ↥S) → β) (Subtype.mk (p := fun (a : α) ↦ a ∈ S) w_2 ⋯) : β)
⊢ (f : (a : ↥S) → β) (Subtype.mk (p := fun (a : α) ↦ a ∈ S) w ⋯) < y

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

Premises used: rfl
-- 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 : α)})
w : α
hx : w < a
w_1 : w ∈ S
w_2 : α
hy : a < w_2
w_3 : w_2 ∈ S
⊢ LT.lt.{u_2} (α := β) ((f : (a : ↥S) → β) (Subtype.mk (p := fun (a : α) ↦ a ∈ S) w ⋯) : β)
    ((f : (a : ↥S) → β) (Subtype.mk (p := fun (a : α) ↦ a ∈ S) w_2 ⋯) : β)

Tactic:
f.strictMono (hx.trans hy)

Premises used: OrderEmbedding.strictMono, LT.lt.trans
-- 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 : α)})
w : α
hx : w < a
w_1 : w ∈ S
w_2 : α
hy : a < w_2
w_3 : w_2 ∈ S
⊢ LT.lt.{u_2} (α := β) ((f : (a : ↥S) → β) (Subtype.mk (p := fun (a : α) ↦ a ∈ S) w ⋯) : β)
    ((f : (a : ↥S) → β) (Subtype.mk (p := fun (a : α) ↦ a ∈ S) w_2 ⋯) : β)

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

Premises used: OrderEmbedding.strictMono
-- 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 : α)})
obtain :
  ∀ (b : β) (hb : ∀ x ∈ Slt, x < b) (hb' : ∀ y ∈ Sgt, b < y),
    ∃ (g : OrderEmbedding.{u_1, u_2} (↥(insert a S)) β),
      Eq (α := (↑(↑S : Set α) : Type u_1) → β)
        (Function.comp (β := ↥(insert a S)) (⇑g : (a : ↥(insert a S)) → β)
          (Set.inclusion (s := (↑S : Set α)) (t := (↑(insert a S) : Set α)) ⋯))
        (⇑f : (a : ↥S) → β)
⊢ ∃ (g : OrderEmbedding.{u_1, u_2} (↥(insert a S)) β),
    Eq (α := (↑(↑S : Set α) : Type u_1) → β)
      (Function.comp (β := ↥(insert a S)) (⇑g : (a : ↥(insert a S)) → β)
        (Set.inclusion (s := (↑S : Set α)) (t := (↑(insert a S) : Set α)) ⋯))
      (⇑f : (a : ↥S) → β)

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

Premises used: Order.exists_between_finsets
-- 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
⊢ ∃ (g : OrderEmbedding.{u_1, u_2} (↥(insert a S)) β),
    Eq (α := (↑(↑S : Set α) : Type u_1) → β)
      (Function.comp (β := ↥(insert a S)) (⇑g : (a : ↥(insert a S)) → β)
        (Set.inclusion (s := (↑S : Set α)) (t := (↑(insert a S) : Set α)) ⋯))
      (⇑f : (a : ↥S) → β)

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

Premises used: Membership.mem, dite, Subtype.mk, OrderEmbedding.ofStrictMono, Exists.intro, Subtype.val, DFunLike.coe
-- 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
refine_1 :
  StrictMono.{u_1, 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
refine_2 :
  Eq (α := (↑(↑S : Set α) : Type u_1) → β)
    (Function.comp (β := ↥(insert a S))
      (⇑(OrderEmbedding.ofStrictMono
              (fun (x : ↥(insert a S)) ↦
                if hx : (↑x : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x : α) hx) else b)
              ⋯ :
            OrderEmbedding.{u_1, u_2} (↥(insert a S)) β) :
        (a : ↥(insert a S)) → β)
      (Set.inclusion (s := (↑S : Set α)) (t := (↑(insert a S) : Set α)) ⋯))
    (⇑f : (a : ↥S) → β)
⊢ ∃ (g : OrderEmbedding.{u_1, u_2} (↥(insert a S)) β),
    Eq (α := (↑(↑S : Set α) : Type u_1) → β)
      (Function.comp (β := ↥(insert a S)) (⇑g : (a : ↥(insert a S)) → β)
        (Set.inclusion (s := (↑S : Set α)) (t := (↑(insert a S) : Set α)) ⋯))
      (⇑f : (a : ↥S) → β)

Tactic:
refine ⟨OrderEmbedding.ofStrictMono
    (fun (x : (insert a S : Finset α)) => if hx : x.1 ∈ S then f ⟨x.1, hx⟩ else b) ?_, ?_⟩
-- 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
hxS : x ∈ S
hyS : y ∈ 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))

Tactic:
simpa only [hxS, hyS, ↓reduceDIte, OrderEmbedding.lt_iff_lt, Subtype.mk_lt_mk]

Premises used: Subtype.mk_lt_mk, reduceDIte, OrderEmbedding.lt_iff_lt
-- 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
hxS : x ∈ S
hyS : y ∉ S
obtain :
  let Slt : Finset β := Finset.image (⇑f : (a : ↥S) → β) ({x ∈ S.attach | (↑x : α) < y});
  let Sgt : Finset β := Finset.image (⇑f : (a : ↥S) → β) ({x ∈ S.attach | y < (↑x : α)});
  ∀ (hb : ∀ x ∈ Slt, x < b) (hb' : ∀ y ∈ Sgt, b < y) (hx : x ∈ insert y S) (hy : y ∈ insert y S)
    (hxy : Subtype.mk (p := fun (x : α) ↦ x ∈ insert y S) x hx < Subtype.mk (p := fun (x : α) ↦ x ∈ insert y S) y hy),
    LT.lt.{u_2} (α := β)
      ((fun (x : ↥(insert y 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 y S) x hx))
      ((fun (x : ↥(insert y 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 y 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:
obtain rfl := Finset.eq_of_mem_insert_of_notMem hy hyS

Premises used: Finset.eq_of_mem_insert_of_notMem, rfl
-- 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
hyS : y ∉ S
Slt : Finset β := Finset.image (⇑f : (a : ↥S) → β) ({x ∈ S.attach | (↑x : α) < y})
Sgt : Finset β := Finset.image (⇑f : (a : ↥S) → β) ({x ∈ S.attach | y < (↑x : α)})
hb : ∀ x ∈ Slt, x < b
hb' : ∀ y ∈ Sgt, b < y
hx : x ∈ insert y S
hy : y ∈ insert y S
hxy : Subtype.mk (p := fun (x : α) ↦ x ∈ insert y S) x hx < Subtype.mk (p := fun (x : α) ↦ x ∈ insert y S) y hy
simp : (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) x ⋯) < b
⊢ LT.lt.{u_2} (α := β)
    ((fun (x : ↥(insert y 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 y S) x hx))
    ((fun (x : ↥(insert y 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 y S) y hy))

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

Premises used: reduceDIte
-- 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
hyS : y ∉ S
Slt : Finset β := Finset.image (⇑f : (a : ↥S) → β) ({x ∈ S.attach | (↑x : α) < y})
Sgt : Finset β := Finset.image (⇑f : (a : ↥S) → β) ({x ∈ S.attach | y < (↑x : α)})
hb : ∀ x ∈ Slt, x < b
hb' : ∀ y ∈ Sgt, b < y
hx : x ∈ insert y S
hy : y ∈ insert y S
hxy : Subtype.mk (p := fun (x : α) ↦ x ∈ insert y S) x hx < Subtype.mk (p := fun (x : α) ↦ x ∈ insert y S) y hy
⊢ (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) x ⋯) < b

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

Premises used: Iff.mpr, Finset.mem_attach, And.intro, Finset.mem_filter, Finset.mem_image_of_mem
-- 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
hyS : y ∉ S
Slt : Finset β := Finset.image (⇑f : (a : ↥S) → β) ({x ∈ S.attach | (↑x : α) < y})
Sgt : Finset β := Finset.image (⇑f : (a : ↥S) → β) ({x ∈ S.attach | y < (↑x : α)})
hb : ∀ x ∈ Slt, x < b
hb' : ∀ y ∈ Sgt, b < y
hx : x ∈ insert y S
hy : y ∈ insert y S
hxy : Subtype.mk (p := fun (x : α) ↦ x ∈ insert y S) x hx < Subtype.mk (p := fun (x : α) ↦ x ∈ insert y S) y hy
⊢ (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) x ⋯) < b

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

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