-- Mathlib/Order/CountableDenseLinearOrder.lean
theorem exists_across [DenselyOrdered β] [NoMinOrder β] [NoMaxOrder β] [Nonempty β]
    (f : PartialIso α β) (a : α) :
    ∃ b : β, ∀ p ∈ f.val, cmp (Prod.fst p) a = cmp (Prod.snd p) b

Proof state:
case h.mk
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ b, (a, b) ∈ ↑f
this :
  ∀ x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.1 < a) ↑f),
    ∀ y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.1) ↑f), x < y
b : β
hb :
  (∀ x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.1 < a) ↑f), x < b) ∧
    ∀ y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.1) ↑f), b < y
p1 : α
p2 : β
hp : (p1, p2) ∈ ↑f
⊢ cmp (p1, p2).1 a = cmp (p1, p2).2 b

Tactic:
have : p1 ≠ a := fun he ↦ h ⟨p2, he ▸ hp⟩

Result:
case h.mk
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ b, (a, b) ∈ ↑f
this✝ :
  ∀ x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.1 < a) ↑f),
    ∀ y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.1) ↑f), x < y
b : β
hb :
  (∀ x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.1 < a) ↑f), x < b) ∧
    ∀ y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.1) ↑f), b < y
p1 : α
p2 : β
hp : (p1, p2) ∈ ↑f
this : p1 ≠ a
⊢ cmp (p1, p2).1 a = cmp (p1, p2).2 b

Proof state:
case h.mk.inl
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ b, (a, b) ∈ ↑f
this✝¹ :
  ∀ x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.1 < a) ↑f),
    ∀ y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.1) ↑f), x < y
b : β
hb :
  (∀ x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.1 < a) ↑f), x < b) ∧
    ∀ y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.1) ↑f), b < y
p1 : α
p2 : β
hp : (p1, p2) ∈ ↑f
this✝ : p1 ≠ a
hl : p1 < a
this : p1 < a ∧ p2 < b
⊢ cmp (p1, p2).1 a = cmp (p1, p2).2 b

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

Result:
case h.mk.inl
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ b, (a, b) ∈ ↑f
this✝¹ :
  ∀ x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.1 < a) ↑f),
    ∀ y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.1) ↑f), x < y
b : β
hb :
  (∀ x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.1 < a) ↑f), x < b) ∧
    ∀ y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.1) ↑f), b < y
p1 : α
p2 : β
hp : (p1, p2) ∈ ↑f
this✝ : 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

Proof state:
case h.mk
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ b, (a, b) ∈ ↑f
this✝ :
  ∀ x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.1 < a) ↑f),
    ∀ y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.1) ↑f), x < y
b : β
hb :
  (∀ x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.1 < a) ↑f), x < b) ∧
    ∀ y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.1) ↑f), b < y
p1 : α
p2 : β
hp : (p1, p2) ∈ ↑f
this : p1 ≠ a
⊢ cmp (p1, p2).1 a = cmp (p1, p2).2 b

Tactic:
rcases lt_or_gt_of_ne this with hl | hr

Result:
case h.mk.inl
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ b, (a, b) ∈ ↑f
this✝ :
  ∀ x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.1 < a) ↑f),
    ∀ y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.1) ↑f), x < y
b : β
hb :
  (∀ x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.1 < a) ↑f), x < b) ∧
    ∀ y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.1) ↑f), b < y
p1 : α
p2 : β
hp : (p1, p2) ∈ ↑f
this : p1 ≠ a
hl : p1 < a
⊢ cmp (p1, p2).1 a = cmp (p1, p2).2 b

case h.mk.inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ b, (a, b) ∈ ↑f
this✝ :
  ∀ x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.1 < a) ↑f),
    ∀ y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.1) ↑f), x < y
b : β
hb :
  (∀ x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.1 < a) ↑f), x < b) ∧
    ∀ y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.1) ↑f), b < y
p1 : α
p2 : β
hp : (p1, p2) ∈ ↑f
this : p1 ≠ a
hr : p1 > a
⊢ cmp (p1, p2).1 a = cmp (p1, p2).2 b

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
⊢ ∃ b, ∀ p ∈ ↑f, cmp p.1 a = cmp p.2 b

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

Result:
case pos
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
h : ∃ b, (a, b) ∈ ↑f
⊢ ∃ b, ∀ p ∈ ↑f, cmp p.1 a = cmp p.2 b

case neg
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ b, (a, b) ∈ ↑f
⊢ ∃ b, ∀ p ∈ ↑f, cmp p.1 a = cmp p.2 b

Proof state:
case h.mk.inl
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ b, (a, b) ∈ ↑f
this✝¹ :
  ∀ x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.1 < a) ↑f),
    ∀ y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.1) ↑f), x < y
b : β
hb :
  (∀ x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.1 < a) ↑f), x < b) ∧
    ∀ y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.1) ↑f), b < y
p1 : α
p2 : β
hp : (p1, p2) ∈ ↑f
this✝ : 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

Result:
no goals

Proof state:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ b, (a, b) ∈ ↑f
p : α × β
hp1 : p ∈ ↑f ∧ p.1 < a
q : α × β
hq1 : q ∈ ↑f ∧ a < q.1
⊢ p.1 < q.1

Tactic:
exact lt_trans hp1.right hq1.right

Result:
no goals