awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
obtain :
  let Slt : Finset β := Finset.image (⇑f : (a : ↥S) → β) ({x_1 ∈ S.attach | (↑x_1 : α) < x});
  let 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),
    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 : ↥(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 hx hxS

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
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
hyS : y ∈ S
simp : b < (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) y ⋯)
⊢ 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:
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
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
hyS : y ∈ S
⊢ b < (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) y ⋯)

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
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
hyS : y ∈ S
⊢ b < (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) y ⋯)

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

Tactic:
simp only [Finset.eq_of_mem_insert_of_notMem hy hyS, lt_self_iff_false] at hxy

Premises used: Finset.eq_of_mem_insert_of_notMem, lt_self_iff_false
-- 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_2 :
  ∀ (x : (↑(↑S : Set α) : Type u_1)),
    Eq.{u_2 + 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 α)) ⋯) x :
        β)
      ((f : (a : ↥S) → β) x : β)
⊢ 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) → β)

Tactic:
ext x
-- 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 : (↑(↑S : Set α) : Type u_1)
⊢ Eq.{u_2 + 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 α)) ⋯) x :
      β)
    ((f : (a : ↥S) → β) x : β)

Tactic:
simp only [OrderEmbedding.coe_ofStrictMono,
      Function.comp_apply, Finset.coe_mem, ↓reduceDIte, Subtype.coe_eta]

Premises used: OrderEmbedding.coe_ofStrictMono, Finset.coe_mem, reduceDIte, Subtype.coe_eta, Function.comp_apply
-- 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 β
inst_5 : Nonempty β
f : PartialIso α β
a : α
pos : ∀ (h : ∃ (b : β), (a, b) ∈ (↑f : Finset (α × β))), ∃ (b : β), ∀ p ∈ (↑f : Finset (α × β)), cmp p.1 a = cmp p.2 b
neg : ∀ (h : ¬∃ (b : β), (a, b) ∈ (↑f : Finset (α × β))), ∃ (b : β), ∀ p ∈ (↑f : Finset (α × β)), cmp p.1 a = cmp p.2 b
⊢ ∃ (b : β), ∀ p ∈ (↑f : Finset (α × β)), cmp p.1 a = cmp p.2 b

Tactic:
by_cases h : ∃ b, (a, b) ∈ f.val

Premises used: Subtype.val
-- 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 β
inst_5 : Nonempty β
f : PartialIso α β
a : α
h : ∃ (b : β), (a, b) ∈ (↑f : Finset (α × β))
pos : ∀ (b : β) (hb : (a, b) ∈ (↑f : Finset (α × β))), ∃ (b : β), ∀ p ∈ (↑f : Finset (α × β)), cmp p.1 a = cmp p.2 b
⊢ ∃ (b : β), ∀ p ∈ (↑f : Finset (α × β)), cmp p.1 a = cmp p.2 b

Tactic:
obtain ⟨b, hb⟩ := h
-- 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 β
inst_5 : Nonempty β
f : PartialIso α β
a : α
b : β
hb : (a, b) ∈ (↑f : Finset (α × β))
⊢ ∃ (b : β), ∀ p ∈ (↑f : Finset (α × β)), cmp p.1 a = cmp p.2 b

Tactic:
⟨b, fun p hp ↦ f.prop _ hp _ hb⟩

Premises used: Prod.mk, Subtype.prop, Exists.intro
-- 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 β
inst_5 : Nonempty β
f : PartialIso α β
a : α
b : β
hb : (a, b) ∈ (↑f : Finset (α × β))
⊢ ∃ (b : β), ∀ p ∈ (↑f : Finset (α × β)), cmp p.1 a = cmp p.2 b

Tactic:
exact ⟨b, fun p hp ↦ f.prop _ hp _ hb⟩
-- 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 β
inst_5 : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ (b : β), (a, b) ∈ (↑f : Finset (α × β))
x : β
hx : x ∈ Finset.image Prod.snd ({p ∈ (↑f : Finset (α × β)) | p.1 < a})
y : β
hy : y ∈ Finset.image Prod.snd ({p ∈ (↑f : Finset (α × β)) | a < p.1})
rw :
  ∀ (hx : ∃ a_1 ∈ {p ∈ (↑f : Finset (α × β)) | p.1 < a}, a_1.2 = x) (y : β)
    (hy : ∃ a_1 ∈ {p ∈ (↑f : Finset (α × β)) | a < p.1}, a_1.2 = y), x < y
⊢ x < y

Tactic:
rw [Finset.mem_image] at hx hy

Premises used: Finset.mem_image
-- 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 β
inst_5 : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ (b : β), (a, b) ∈ (↑f : Finset (α × β))
x : β
hx : ∃ a_1 ∈ {p ∈ (↑f : Finset (α × β)) | p.1 < a}, a_1.2 = x
y : β
hy : ∃ a_1 ∈ {p ∈ (↑f : Finset (α × β)) | a < p.1}, a_1.2 = y
rcases : ∀ (p : α × β) (hp1 : p ∈ {p ∈ (↑f : Finset (α × β)) | p.1 < a}), p.2 < y
⊢ x < y

Tactic:
rcases hx with ⟨p, hp1, rfl⟩

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 β
inst_5 : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ (b : β), (a, b) ∈ (↑f : Finset (α × β))
y : β
hy : ∃ a_1 ∈ {p ∈ (↑f : Finset (α × β)) | a < p.1}, a_1.2 = y
p : α × β
hp1 : p ∈ {p ∈ (↑f : Finset (α × β)) | p.1 < a}
rcases : ∀ (q : α × β) (hq1 : q ∈ {p ∈ (↑f : Finset (α × β)) | a < p.1}), p.2 < q.2
⊢ p.2 < y

Tactic:
rcases hy with ⟨q, hq1, rfl⟩

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 β
inst_5 : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ (b : β), (a, b) ∈ (↑f : Finset (α × β))
p : α × β
hp1 : p ∈ {p ∈ (↑f : Finset (α × β)) | p.1 < a}
q : α × β
hq1 : q ∈ {p ∈ (↑f : Finset (α × β)) | a < p.1}
rw : ∀ (hp1 : p ∈ (↑f : Finset (α × β)) ∧ p.1 < a) (q : α × β) (hq1 : q ∈ (↑f : Finset (α × β)) ∧ a < q.1), p.2 < q.2
⊢ p.2 < q.2

Tactic:
rw [Finset.mem_filter] at hp1 hq1

Premises used: Finset.mem_filter
-- 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 β
inst_5 : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ (b : β), (a, b) ∈ (↑f : Finset (α × β))
p : α × β
hp1 : p ∈ (↑f : Finset (α × β)) ∧ p.1 < a
q : α × β
hq1 : q ∈ (↑f : Finset (α × β)) ∧ a < q.1
rw : p.1 < q.1
⊢ p.2 < q.2

Tactic:
rw [← lt_iff_lt_of_cmp_eq_cmp (f.prop _ hp1.1 _ hq1.1)]

Premises used: lt_iff_lt_of_cmp_eq_cmp, And.left, Subtype.prop
-- 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 β
inst_5 : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ (b : β), (a, b) ∈ (↑f : Finset (α × β))
p : α × β
hp1 : p ∈ (↑f : Finset (α × β)) ∧ p.1 < a
q : α × β
hq1 : q ∈ (↑f : Finset (α × β)) ∧ a < q.1
⊢ p.1 < q.1

Tactic:
lt_trans hp1.right hq1.right

Premises used: lt_trans, And.right
-- 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 β
inst_5 : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ (b : β), (a, b) ∈ (↑f : Finset (α × β))
p : α × β
hp1 : p ∈ (↑f : Finset (α × β)) ∧ p.1 < a
q : α × β
hq1 : q ∈ (↑f : Finset (α × β)) ∧ a < q.1
⊢ p.1 < q.1

Tactic:
exact lt_trans hp1.right hq1.right

Premises used: lt_trans, And.right
-- 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 β
inst_5 : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ (b : β), (a, b) ∈ (↑f : Finset (α × β))
⊢ ∀ x ∈ Finset.image Prod.snd ({p ∈ (↑f : Finset (α × β)) | p.1 < a}),
    ∀ y ∈ Finset.image Prod.snd ({p ∈ (↑f : Finset (α × β)) | a < p.1}), x < y

Tactic:
have :
    ∀ x ∈ {p ∈ f.val | p.fst < a}.image Prod.snd,
      ∀ y ∈ {p ∈ f.val | a < p.fst}.image Prod.snd, x < y := by
    intro x hx y hy
    rw [Finset.mem_image] at hx hy
    rcases hx with ⟨p, hp1, rfl⟩
    rcases hy with ⟨q, hq1, rfl⟩
    rw [Finset.mem_filter] at hp1 hq1
    rw [← lt_iff_lt_of_cmp_eq_cmp (f.prop _ hp1.1 _ hq1.1)]
    exact lt_trans hp1.right hq1.right
-- 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 β
inst_5 : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ (b : β), (a, b) ∈ (↑f : Finset (α × β))
this :
  ∀ x ∈ Finset.image Prod.snd ({p ∈ (↑f : Finset (α × β)) | p.1 < a}),
    ∀ y ∈ Finset.image Prod.snd ({p ∈ (↑f : Finset (α × β)) | a < p.1}), x < y
neg :
  ∀ (b : β)
    (hb :
      (∀ x ∈ Finset.image Prod.snd ({p ∈ (↑f : Finset (α × β)) | p.1 < a}), x < b) ∧
        ∀ y ∈ Finset.image Prod.snd ({p ∈ (↑f : Finset (α × β)) | a < p.1}), b < y),
    ∃ (b : β), ∀ p ∈ (↑f : Finset (α × β)), cmp p.1 a = cmp p.2 b
⊢ ∃ (b : β), ∀ p ∈ (↑f : Finset (α × β)), cmp p.1 a = cmp p.2 b

Tactic:
obtain ⟨b, hb⟩ := exists_between_finsets _ _ this

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 β
inst_5 : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ (b : β), (a, b) ∈ (↑f : Finset (α × β))
this :
  ∀ x ∈ Finset.image Prod.snd ({p ∈ (↑f : Finset (α × β)) | p.1 < a}),
    ∀ y ∈ Finset.image Prod.snd ({p ∈ (↑f : Finset (α × β)) | a < p.1}), x < y
b : β
hb :
  (∀ x ∈ Finset.image Prod.snd ({p ∈ (↑f : Finset (α × β)) | p.1 < a}), x < b) ∧
    ∀ y ∈ Finset.image Prod.snd ({p ∈ (↑f : Finset (α × β)) | a < p.1}), b < y
h₁ : ∀ p ∈ (↑f : Finset (α × β)), cmp p.1 a = cmp p.2 b
⊢ ∃ (b : β), ∀ p ∈ (↑f : Finset (α × β)), cmp p.1 a = cmp p.2 b

Tactic:
use 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 β
inst_5 : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ (b : β), (a, b) ∈ (↑f : Finset (α × β))
this :
  ∀ x ∈ Finset.image Prod.snd ({p ∈ (↑f : Finset (α × β)) | p.1 < a}),
    ∀ y ∈ Finset.image Prod.snd ({p ∈ (↑f : Finset (α × β)) | a < p.1}), x < y
b : β
hb :
  (∀ x ∈ Finset.image Prod.snd ({p ∈ (↑f : Finset (α × β)) | p.1 < a}), x < b) ∧
    ∀ y ∈ Finset.image Prod.snd ({p ∈ (↑f : Finset (α × β)) | a < p.1}), b < y
p1 : α
p2 : β
hp : (p1, p2) ∈ (↑f : Finset (α × β))
⊢ p1 ≠ a

Tactic:
have : p1 ≠ a := fun he ↦ h ⟨p2, he ▸ hp⟩
-- 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 β
inst_5 : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ (b : β), (a, b) ∈ (↑f : Finset (α × β))
this_1 :
  ∀ x ∈ Finset.image Prod.snd ({p ∈ (↑f : Finset (α × β)) | p.1 < a}),
    ∀ y ∈ Finset.image Prod.snd ({p ∈ (↑f : Finset (α × β)) | a < p.1}), x < y
b : β
hb :
  (∀ x ∈ Finset.image Prod.snd ({p ∈ (↑f : Finset (α × β)) | p.1 < a}), x < b) ∧
    ∀ y ∈ Finset.image Prod.snd ({p ∈ (↑f : Finset (α × β)) | a < p.1}), b < y
p1 : α
p2 : β
hp : (p1, p2) ∈ (↑f : Finset (α × β))
this : p1 ≠ a
h₁ : ∀ (hl : p1 < a), cmp (p1, p2).1 a = cmp (p1, p2).2 b
h₂ : ∀ (hr : a < p1), cmp (p1, p2).1 a = cmp (p1, p2).2 b
⊢ cmp (p1, p2).1 a = cmp (p1, p2).2 b

Tactic:
rcases lt_or_gt_of_ne this with hl | hr

Premises used: lt_or_gt_of_ne
-- 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 β
inst_5 : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ (b : β), (a, b) ∈ (↑f : Finset (α × β))
this_1 :
  ∀ x ∈ Finset.image Prod.snd ({p ∈ (↑f : Finset (α × β)) | p.1 < a}),
    ∀ y ∈ Finset.image Prod.snd ({p ∈ (↑f : Finset (α × β)) | a < p.1}), x < y
b : β
hb :
  (∀ x ∈ Finset.image Prod.snd ({p ∈ (↑f : Finset (α × β)) | p.1 < a}), x < b) ∧
    ∀ y ∈ Finset.image Prod.snd ({p ∈ (↑f : Finset (α × β)) | a < p.1}), b < y
p1 : α
p2 : β
hp : (p1, p2) ∈ (↑f : Finset (α × β))
this : p1 ≠ a
hl : p1 < a
⊢ p1 < a ∧ p2 < b

Tactic:
have : p1 < a ∧ p2 < b :=
      ⟨hl, hb.1 _ (Finset.mem_image.mpr ⟨(p1, p2), Finset.mem_filter.mpr ⟨hp, hl⟩, 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 β
inst_5 : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ (b : β), (a, b) ∈ (↑f : Finset (α × β))
this_1 :
  ∀ x ∈ Finset.image Prod.snd ({p ∈ (↑f : Finset (α × β)) | p.1 < a}),
    ∀ y ∈ Finset.image Prod.snd ({p ∈ (↑f : Finset (α × β)) | a < p.1}), x < y
b : β
hb :
  (∀ x ∈ Finset.image Prod.snd ({p ∈ (↑f : Finset (α × β)) | p.1 < a}), x < b) ∧
    ∀ y ∈ Finset.image Prod.snd ({p ∈ (↑f : Finset (α × β)) | a < p.1}), b < y
p1 : α
p2 : β
hp : (p1, p2) ∈ (↑f : Finset (α × β))
this_2 : p1 ≠ a
hl : p1 < a
this : p1 < a ∧ p2 < b
⊢ cmp p1 a = Ordering.lt ∧ cmp p2 b = Ordering.lt

Tactic:
rw [← cmp_eq_lt_iff, ← cmp_eq_lt_iff] at this

Premises used: cmp_eq_lt_iff
-- 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 β
inst_5 : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ (b : β), (a, b) ∈ (↑f : Finset (α × β))
this_1 :
  ∀ x ∈ Finset.image Prod.snd ({p ∈ (↑f : Finset (α × β)) | p.1 < a}),
    ∀ y ∈ Finset.image Prod.snd ({p ∈ (↑f : Finset (α × β)) | a < p.1}), x < y
b : β
hb :
  (∀ x ∈ Finset.image Prod.snd ({p ∈ (↑f : Finset (α × β)) | p.1 < a}), x < b) ∧
    ∀ y ∈ Finset.image Prod.snd ({p ∈ (↑f : Finset (α × β)) | a < p.1}), b < y
p1 : α
p2 : β
hp : (p1, p2) ∈ (↑f : Finset (α × β))
this_2 : p1 ≠ a
hl : p1 < a
this : cmp p1 a = Ordering.lt ∧ cmp p2 b = Ordering.lt
⊢ cmp (p1, p2).1 a = cmp (p1, p2).2 b

Tactic:
this.1.trans this.2.symm

Premises used: And.right, And.left, Eq.symm, Eq.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 β
inst_5 : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ (b : β), (a, b) ∈ (↑f : Finset (α × β))
this_1 :
  ∀ x ∈ Finset.image Prod.snd ({p ∈ (↑f : Finset (α × β)) | p.1 < a}),
    ∀ y ∈ Finset.image Prod.snd ({p ∈ (↑f : Finset (α × β)) | a < p.1}), x < y
b : β
hb :
  (∀ x ∈ Finset.image Prod.snd ({p ∈ (↑f : Finset (α × β)) | p.1 < a}), x < b) ∧
    ∀ y ∈ Finset.image Prod.snd ({p ∈ (↑f : Finset (α × β)) | a < p.1}), b < y
p1 : α
p2 : β
hp : (p1, p2) ∈ (↑f : Finset (α × β))
this_2 : p1 ≠ a
hl : p1 < a
this : cmp p1 a = Ordering.lt ∧ cmp p2 b = Ordering.lt
⊢ cmp (p1, p2).1 a = cmp (p1, p2).2 b

Tactic:
exact this.1.trans this.2.symm

Premises used: And.right, And.left, Eq.symm, Eq.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 β
inst_5 : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ (b : β), (a, b) ∈ (↑f : Finset (α × β))
this_1 :
  ∀ x ∈ Finset.image Prod.snd ({p ∈ (↑f : Finset (α × β)) | p.1 < a}),
    ∀ y ∈ Finset.image Prod.snd ({p ∈ (↑f : Finset (α × β)) | a < p.1}), x < y
b : β
hb :
  (∀ x ∈ Finset.image Prod.snd ({p ∈ (↑f : Finset (α × β)) | p.1 < a}), x < b) ∧
    ∀ y ∈ Finset.image Prod.snd ({p ∈ (↑f : Finset (α × β)) | a < p.1}), b < y
p1 : α
p2 : β
hp : (p1, p2) ∈ (↑f : Finset (α × β))
this : p1 ≠ a
hr : a < p1
⊢ a < p1 ∧ b < p2

Tactic:
have : a < p1 ∧ b < p2 :=
      ⟨hr, hb.2 _ (Finset.mem_image.mpr ⟨(p1, p2), Finset.mem_filter.mpr ⟨hp, hr⟩, rfl⟩)⟩