[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
⊢ ∃ b, ∀ (p : α × β), p ∈ ↑f → cmp p.fst a = cmp p.snd b
[PROOFSTEP]
by_cases h : ∃ b, (a, b) ∈ f.val
[GOAL]
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 : α × β), p ∈ ↑f → cmp p.fst a = cmp p.snd b
[PROOFSTEP]
cases' h with b hb
[GOAL]
case pos.intro
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
b : β
hb : (a, b) ∈ ↑f
⊢ ∃ b, ∀ (p : α × β), p ∈ ↑f → cmp p.fst a = cmp p.snd b
[PROOFSTEP]
exact ⟨b, fun p hp ↦ f.prop _ hp _ hb⟩
[GOAL]
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 : α × β), p ∈ ↑f → cmp p.fst a = cmp p.snd b
[PROOFSTEP]
have :
  ∀ x ∈ (f.val.filter fun p : α × β ↦ p.fst < a).image Prod.snd,
    ∀ y ∈ (f.val.filter fun p : α × β ↦ 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
[GOAL]
α : 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
⊢ ∀ (x : β),
    x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.fst < a) ↑f) →
      ∀ (y : β), y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.fst) ↑f) → x < y
[PROOFSTEP]
intro x hx y hy
[GOAL]
α : 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
x : β
hx : x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.fst < a) ↑f)
y : β
hy : y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.fst) ↑f)
⊢ x < y
[PROOFSTEP]
rw [Finset.mem_image] at hx hy 
[GOAL]
α : 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
x : β
hx : ∃ a_1, a_1 ∈ Finset.filter (fun p => p.fst < a) ↑f ∧ a_1.snd = x
y : β
hy : ∃ a_1, a_1 ∈ Finset.filter (fun p => a < p.fst) ↑f ∧ a_1.snd = y
⊢ x < y
[PROOFSTEP]
rcases hx with ⟨p, hp1, rfl⟩
[GOAL]
case 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
y : β
hy : ∃ a_1, a_1 ∈ Finset.filter (fun p => a < p.fst) ↑f ∧ a_1.snd = y
p : α × β
hp1 : p ∈ Finset.filter (fun p => p.fst < a) ↑f
⊢ p.snd < y
[PROOFSTEP]
rcases hy with ⟨q, hq1, rfl⟩
[GOAL]
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 ∈ Finset.filter (fun p => p.fst < a) ↑f
q : α × β
hq1 : q ∈ Finset.filter (fun p => a < p.fst) ↑f
⊢ p.snd < q.snd
[PROOFSTEP]
rw [Finset.mem_filter] at hp1 hq1 
[GOAL]
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.fst < a
q : α × β
hq1 : q ∈ ↑f ∧ a < q.fst
⊢ p.snd < q.snd
[PROOFSTEP]
rw [← lt_iff_lt_of_cmp_eq_cmp (f.prop _ hp1.1 _ hq1.1)]
[GOAL]
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.fst < a
q : α × β
hq1 : q ∈ ↑f ∧ a < q.fst
⊢ p.fst < q.fst
[PROOFSTEP]
exact lt_trans hp1.right hq1.right
[GOAL]
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
this :
  ∀ (x : β),
    x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.fst < a) ↑f) →
      ∀ (y : β), y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.fst) ↑f) → x < y
⊢ ∃ b, ∀ (p : α × β), p ∈ ↑f → cmp p.fst a = cmp p.snd b
[PROOFSTEP]
cases' exists_between_finsets _ _ this with b hb
[GOAL]
case neg.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
this :
  ∀ (x : β),
    x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.fst < a) ↑f) →
      ∀ (y : β), y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.fst) ↑f) → x < y
b : β
hb :
  (∀ (x : β), x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.fst < a) ↑f) → x < b) ∧
    ∀ (y : β), y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.fst) ↑f) → b < y
⊢ ∃ b, ∀ (p : α × β), p ∈ ↑f → cmp p.fst a = cmp p.snd b
[PROOFSTEP]
use b
[GOAL]
case h
α : 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 : β),
    x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.fst < a) ↑f) →
      ∀ (y : β), y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.fst) ↑f) → x < y
b : β
hb :
  (∀ (x : β), x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.fst < a) ↑f) → x < b) ∧
    ∀ (y : β), y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.fst) ↑f) → b < y
⊢ ∀ (p : α × β), p ∈ ↑f → cmp p.fst a = cmp p.snd b
[PROOFSTEP]
rintro ⟨p1, p2⟩ hp
[GOAL]
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 : β),
    x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.fst < a) ↑f) →
      ∀ (y : β), y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.fst) ↑f) → x < y
b : β
hb :
  (∀ (x : β), x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.fst < a) ↑f) → x < b) ∧
    ∀ (y : β), y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.fst) ↑f) → b < y
p1 : α
p2 : β
hp : (p1, p2) ∈ ↑f
⊢ cmp (p1, p2).fst a = cmp (p1, p2).snd b
[PROOFSTEP]
have : p1 ≠ a := fun he ↦ h ⟨p2, he ▸ hp⟩
[GOAL]
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 : β),
    x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.fst < a) ↑f) →
      ∀ (y : β), y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.fst) ↑f) → x < y
b : β
hb :
  (∀ (x : β), x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.fst < a) ↑f) → x < b) ∧
    ∀ (y : β), y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.fst) ↑f) → b < y
p1 : α
p2 : β
hp : (p1, p2) ∈ ↑f
this : p1 ≠ a
⊢ cmp (p1, p2).fst a = cmp (p1, p2).snd b
[PROOFSTEP]
cases' lt_or_gt_of_ne this with hl hr
[GOAL]
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 : β),
    x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.fst < a) ↑f) →
      ∀ (y : β), y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.fst) ↑f) → x < y
b : β
hb :
  (∀ (x : β), x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.fst < a) ↑f) → x < b) ∧
    ∀ (y : β), y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.fst) ↑f) → b < y
p1 : α
p2 : β
hp : (p1, p2) ∈ ↑f
this : p1 ≠ a
hl : p1 < a
⊢ cmp (p1, p2).fst a = cmp (p1, p2).snd b
[PROOFSTEP]
have : p1 < a ∧ p2 < b := ⟨hl, hb.1 _ (Finset.mem_image.mpr ⟨(p1, p2), Finset.mem_filter.mpr ⟨hp, hl⟩, rfl⟩)⟩
[GOAL]
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 : β),
    x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.fst < a) ↑f) →
      ∀ (y : β), y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.fst) ↑f) → x < y
b : β
hb :
  (∀ (x : β), x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.fst < a) ↑f) → x < b) ∧
    ∀ (y : β), y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.fst) ↑f) → b < y
p1 : α
p2 : β
hp : (p1, p2) ∈ ↑f
this✝ : p1 ≠ a
hl : p1 < a
this : p1 < a ∧ p2 < b
⊢ cmp (p1, p2).fst a = cmp (p1, p2).snd b
[PROOFSTEP]
rw [← cmp_eq_lt_iff, ← cmp_eq_lt_iff] at this 
[GOAL]
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 : β),
    x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.fst < a) ↑f) →
      ∀ (y : β), y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.fst) ↑f) → x < y
b : β
hb :
  (∀ (x : β), x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.fst < a) ↑f) → x < b) ∧
    ∀ (y : β), y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.fst) ↑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).fst a = cmp (p1, p2).snd b
[PROOFSTEP]
exact this.1.trans this.2.symm
[GOAL]
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 : β),
    x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.fst < a) ↑f) →
      ∀ (y : β), y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.fst) ↑f) → x < y
b : β
hb :
  (∀ (x : β), x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.fst < a) ↑f) → x < b) ∧
    ∀ (y : β), y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.fst) ↑f) → b < y
p1 : α
p2 : β
hp : (p1, p2) ∈ ↑f
this : p1 ≠ a
hr : p1 > a
⊢ cmp (p1, p2).fst a = cmp (p1, p2).snd b
[PROOFSTEP]
have : a < p1 ∧ b < p2 := ⟨hr, hb.2 _ (Finset.mem_image.mpr ⟨(p1, p2), Finset.mem_filter.mpr ⟨hp, hr⟩, rfl⟩)⟩
[GOAL]
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 : β),
    x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.fst < a) ↑f) →
      ∀ (y : β), y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.fst) ↑f) → x < y
b : β
hb :
  (∀ (x : β), x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.fst < a) ↑f) → x < b) ∧
    ∀ (y : β), y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.fst) ↑f) → b < y
p1 : α
p2 : β
hp : (p1, p2) ∈ ↑f
this✝ : p1 ≠ a
hr : p1 > a
this : a < p1 ∧ b < p2
⊢ cmp (p1, p2).fst a = cmp (p1, p2).snd b
[PROOFSTEP]
rw [← cmp_eq_gt_iff, ← cmp_eq_gt_iff] at this 
[GOAL]
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 : β),
    x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.fst < a) ↑f) →
      ∀ (y : β), y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.fst) ↑f) → x < y
b : β
hb :
  (∀ (x : β), x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.fst < a) ↑f) → x < b) ∧
    ∀ (y : β), y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.fst) ↑f) → b < y
p1 : α
p2 : β
hp : (p1, p2) ∈ ↑f
this✝ : p1 ≠ a
hr : p1 > a
this : cmp p1 a = Ordering.gt ∧ cmp p2 b = Ordering.gt
⊢ cmp (p1, p2).fst a = cmp (p1, p2).snd b
[PROOFSTEP]
exact this.1.trans this.2.symm
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : Finset (α × β)
hf : ∀ (p : α × β), p ∈ f → ∀ (q : α × β), q ∈ f → cmp p.fst q.fst = cmp p.snd q.snd
p : β × α
hp : p ∈ Finset.image (↑(Equiv.prodComm α β)) f
q : β × α
hq : q ∈ Finset.image (↑(Equiv.prodComm α β)) f
⊢ ↑(Equiv.prodComm α β).symm p ∈ f
[PROOFSTEP]
rw [← Finset.mem_coe, Finset.coe_image, Equiv.image_eq_preimage] at hp 
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : Finset (α × β)
hf : ∀ (p : α × β), p ∈ f → ∀ (q : α × β), q ∈ f → cmp p.fst q.fst = cmp p.snd q.snd
p : β × α
hp : p ∈ ↑(Equiv.prodComm α β).symm ⁻¹' ↑f
q : β × α
hq : q ∈ Finset.image (↑(Equiv.prodComm α β)) f
⊢ ↑(Equiv.prodComm α β).symm p ∈ f
[PROOFSTEP]
rwa [← Finset.mem_coe]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : Finset (α × β)
hf : ∀ (p : α × β), p ∈ f → ∀ (q : α × β), q ∈ f → cmp p.fst q.fst = cmp p.snd q.snd
p : β × α
hp : p ∈ Finset.image (↑(Equiv.prodComm α β)) f
q : β × α
hq : q ∈ Finset.image (↑(Equiv.prodComm α β)) f
⊢ ↑(Equiv.prodComm α β).symm q ∈ f
[PROOFSTEP]
rw [← Finset.mem_coe, Finset.coe_image, Equiv.image_eq_preimage] at hq 
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : Finset (α × β)
hf : ∀ (p : α × β), p ∈ f → ∀ (q : α × β), q ∈ f → cmp p.fst q.fst = cmp p.snd q.snd
p : β × α
hp : p ∈ Finset.image (↑(Equiv.prodComm α β)) f
q : β × α
hq : q ∈ ↑(Equiv.prodComm α β).symm ⁻¹' ↑f
⊢ ↑(Equiv.prodComm α β).symm q ∈ f
[PROOFSTEP]
rwa [← Finset.mem_coe]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
a : α
f : PartialIso α β
⊢ ∃ y, y ∈ {f | ∃ b, (a, b) ∈ ↑f} ∧ f ≤ y
[PROOFSTEP]
cases' exists_across f a with b a_b
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
a : α
f : PartialIso α β
b : β
a_b : ∀ (p : α × β), p ∈ ↑f → cmp p.fst a = cmp p.snd b
⊢ ∃ y, y ∈ {f | ∃ b, (a, b) ∈ ↑f} ∧ f ≤ y
[PROOFSTEP]
refine ⟨⟨insert (a, b) f.val, fun p hp q hq ↦ ?_⟩, ⟨b, Finset.mem_insert_self _ _⟩, Finset.subset_insert _ _⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
a : α
f : PartialIso α β
b : β
a_b : ∀ (p : α × β), p ∈ ↑f → cmp p.fst a = cmp p.snd b
p : α × β
hp : p ∈ insert (a, b) ↑f
q : α × β
hq : q ∈ insert (a, b) ↑f
⊢ cmp p.fst q.fst = cmp p.snd q.snd
[PROOFSTEP]
rw [Finset.mem_insert] at hp hq 
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
a : α
f : PartialIso α β
b : β
a_b : ∀ (p : α × β), p ∈ ↑f → cmp p.fst a = cmp p.snd b
p : α × β
hp : p = (a, b) ∨ p ∈ ↑f
q : α × β
hq : q = (a, b) ∨ q ∈ ↑f
⊢ cmp p.fst q.fst = cmp p.snd q.snd
[PROOFSTEP]
rcases hp with (rfl | pf)
[GOAL]
case intro.inl
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
a : α
f : PartialIso α β
b : β
a_b : ∀ (p : α × β), p ∈ ↑f → cmp p.fst a = cmp p.snd b
q : α × β
hq : q = (a, b) ∨ q ∈ ↑f
⊢ cmp (a, b).fst q.fst = cmp (a, b).snd q.snd
[PROOFSTEP]
rcases hq with (rfl | qf)
[GOAL]
case intro.inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
a : α
f : PartialIso α β
b : β
a_b : ∀ (p : α × β), p ∈ ↑f → cmp p.fst a = cmp p.snd b
p q : α × β
hq : q = (a, b) ∨ q ∈ ↑f
pf : p ∈ ↑f
⊢ cmp p.fst q.fst = cmp p.snd q.snd
[PROOFSTEP]
rcases hq with (rfl | qf)
[GOAL]
case intro.inl.inl
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
a : α
f : PartialIso α β
b : β
a_b : ∀ (p : α × β), p ∈ ↑f → cmp p.fst a = cmp p.snd b
⊢ cmp (a, b).fst (a, b).fst = cmp (a, b).snd (a, b).snd
[PROOFSTEP]
simp only [cmp_self_eq_eq]
[GOAL]
case intro.inl.inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
a : α
f : PartialIso α β
b : β
a_b : ∀ (p : α × β), p ∈ ↑f → cmp p.fst a = cmp p.snd b
q : α × β
qf : q ∈ ↑f
⊢ cmp (a, b).fst q.fst = cmp (a, b).snd q.snd
[PROOFSTEP]
rw [cmp_eq_cmp_symm]
[GOAL]
case intro.inl.inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
a : α
f : PartialIso α β
b : β
a_b : ∀ (p : α × β), p ∈ ↑f → cmp p.fst a = cmp p.snd b
q : α × β
qf : q ∈ ↑f
⊢ cmp q.fst (a, b).fst = cmp q.snd (a, b).snd
[PROOFSTEP]
exact a_b _ qf
[GOAL]
case intro.inr.inl
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
a : α
f : PartialIso α β
b : β
a_b : ∀ (p : α × β), p ∈ ↑f → cmp p.fst a = cmp p.snd b
p : α × β
pf : p ∈ ↑f
⊢ cmp p.fst (a, b).fst = cmp p.snd (a, b).snd
[PROOFSTEP]
exact a_b _ pf
[GOAL]
case intro.inr.inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
a : α
f : PartialIso α β
b : β
a_b : ∀ (p : α × β), p ∈ ↑f → cmp p.fst a = cmp p.snd b
p q : α × β
pf : p ∈ ↑f
qf : q ∈ ↑f
⊢ cmp p.fst q.fst = cmp p.snd q.snd
[PROOFSTEP]
exact f.prop _ pf _ qf
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered α
inst✝² : NoMinOrder α
inst✝¹ : NoMaxOrder α
inst✝ : Nonempty α
b : β
f : PartialIso α β
⊢ ∃ y, y ∈ {f | ∃ a, (a, b) ∈ ↑f} ∧ f ≤ y
[PROOFSTEP]
rcases(definedAtLeft α b).mem_gt f.comm with ⟨f', ⟨a, ha⟩, hl⟩
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered α
inst✝² : NoMinOrder α
inst✝¹ : NoMaxOrder α
inst✝ : Nonempty α
b : β
f : PartialIso α β
f' : PartialIso β α
hl : PartialIso.comm f ≤ f'
a : α
ha : (b, a) ∈ ↑f'
⊢ ∃ y, y ∈ {f | ∃ a, (a, b) ∈ ↑f} ∧ f ≤ y
[PROOFSTEP]
refine' ⟨f'.comm, ⟨a, _⟩, _⟩
[GOAL]
case intro.intro.intro.refine'_1
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered α
inst✝² : NoMinOrder α
inst✝¹ : NoMaxOrder α
inst✝ : Nonempty α
b : β
f : PartialIso α β
f' : PartialIso β α
hl : PartialIso.comm f ≤ f'
a : α
ha : (b, a) ∈ ↑f'
⊢ (a, b) ∈ ↑(PartialIso.comm f')
[PROOFSTEP]
change (a, b) ∈ f'.val.image _
[GOAL]
case intro.intro.intro.refine'_1
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered α
inst✝² : NoMinOrder α
inst✝¹ : NoMaxOrder α
inst✝ : Nonempty α
b : β
f : PartialIso α β
f' : PartialIso β α
hl : PartialIso.comm f ≤ f'
a : α
ha : (b, a) ∈ ↑f'
⊢ (a, b) ∈ Finset.image ↑(Equiv.prodComm β α) ↑f'
[PROOFSTEP]
rwa [← Finset.mem_coe, Finset.coe_image, Equiv.image_eq_preimage]
[GOAL]
case intro.intro.intro.refine'_2
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered α
inst✝² : NoMinOrder α
inst✝¹ : NoMaxOrder α
inst✝ : Nonempty α
b : β
f : PartialIso α β
f' : PartialIso β α
hl : PartialIso.comm f ≤ f'
a : α
ha : (b, a) ∈ ↑f'
⊢ f ≤ PartialIso.comm f'
[PROOFSTEP]
change _ ⊆ f'.val.image _
[GOAL]
case intro.intro.intro.refine'_2
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered α
inst✝² : NoMinOrder α
inst✝¹ : NoMaxOrder α
inst✝ : Nonempty α
b : β
f : PartialIso α β
f' : PartialIso β α
hl : PartialIso.comm f ≤ f'
a : α
ha : (b, a) ∈ ↑f'
⊢ (fun a => ↑a) f ⊆ Finset.image ↑(Equiv.prodComm β α) ↑f'
[PROOFSTEP]
rwa [← Finset.coe_subset, Finset.coe_image, ← Equiv.subset_image, ← Finset.coe_image, Finset.coe_subset]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : Encodable α
inst✝¹ : DenselyOrdered β
inst✝ : Nontrivial β
⊢ Nonempty (α ↪o β)
[PROOFSTEP]
rcases exists_pair_lt β with ⟨x, y, hxy⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : Encodable α
inst✝¹ : DenselyOrdered β
inst✝ : Nontrivial β
x y : β
hxy : x < y
⊢ Nonempty (α ↪o β)
[PROOFSTEP]
cases' exists_between hxy with a ha
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : Encodable α
inst✝¹ : DenselyOrdered β
inst✝ : Nontrivial β
x y : β
hxy : x < y
a : β
ha : x < a ∧ a < y
⊢ Nonempty (α ↪o β)
[PROOFSTEP]
haveI : Nonempty (Set.Ioo x y) := ⟨⟨a, ha⟩⟩
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : Encodable α
inst✝¹ : DenselyOrdered β
inst✝ : Nontrivial β
x y : β
hxy : x < y
a : β
ha : x < a ∧ a < y
this : Nonempty ↑(Set.Ioo x y)
⊢ Nonempty (α ↪o β)
[PROOFSTEP]
let our_ideal : Ideal (PartialIso α _) := idealOfCofinals default (definedAtLeft (Set.Ioo x y))
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : Encodable α
inst✝¹ : DenselyOrdered β
inst✝ : Nontrivial β
x y : β
hxy : x < y
a : β
ha : x < a ∧ a < y
this : Nonempty ↑(Set.Ioo x y)
our_ideal : Ideal (PartialIso α ↑(Set.Ioo x y)) := idealOfCofinals default (definedAtLeft ↑(Set.Ioo x y))
⊢ Nonempty (α ↪o β)
[PROOFSTEP]
let F a := funOfIdeal a our_ideal (cofinal_meets_idealOfCofinals _ _ a)
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : Encodable α
inst✝¹ : DenselyOrdered β
inst✝ : Nontrivial β
x y : β
hxy : x < y
a : β
ha : x < a ∧ a < y
this : Nonempty ↑(Set.Ioo x y)
our_ideal : Ideal (PartialIso α ↑(Set.Ioo x y)) := idealOfCofinals default (definedAtLeft ↑(Set.Ioo x y))
F : (a : α) → { b // ∃ f, f ∈ our_ideal ∧ (a, b) ∈ ↑f } :=
  fun a =>
    funOfIdeal a our_ideal
      (_ : ∃ x_1, x_1 ∈ definedAtLeft (↑(Set.Ioo x y)) a ∧ x_1 ∈ idealOfCofinals default (definedAtLeft ↑(Set.Ioo x y)))
⊢ Nonempty (α ↪o β)
[PROOFSTEP]
refine ⟨RelEmbedding.trans (OrderEmbedding.ofStrictMono (fun a ↦ (F a).val) fun a₁ a₂ ↦ ?_) (OrderEmbedding.subtype _)⟩
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : Encodable α
inst✝¹ : DenselyOrdered β
inst✝ : Nontrivial β
x y : β
hxy : x < y
a : β
ha : x < a ∧ a < y
this : Nonempty ↑(Set.Ioo x y)
our_ideal : Ideal (PartialIso α ↑(Set.Ioo x y)) := idealOfCofinals default (definedAtLeft ↑(Set.Ioo x y))
F : (a : α) → { b // ∃ f, f ∈ our_ideal ∧ (a, b) ∈ ↑f } :=
  fun a =>
    funOfIdeal a our_ideal
      (_ : ∃ x_1, x_1 ∈ definedAtLeft (↑(Set.Ioo x y)) a ∧ x_1 ∈ idealOfCofinals default (definedAtLeft ↑(Set.Ioo x y)))
a₁ a₂ : α
⊢ a₁ < a₂ → (fun a => ↑(F a)) a₁ < (fun a => ↑(F a)) a₂
[PROOFSTEP]
rcases(F a₁).prop with ⟨f, hf, ha₁⟩
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : Encodable α
inst✝¹ : DenselyOrdered β
inst✝ : Nontrivial β
x y : β
hxy : x < y
a : β
ha : x < a ∧ a < y
this : Nonempty ↑(Set.Ioo x y)
our_ideal : Ideal (PartialIso α ↑(Set.Ioo x y)) := idealOfCofinals default (definedAtLeft ↑(Set.Ioo x y))
F : (a : α) → { b // ∃ f, f ∈ our_ideal ∧ (a, b) ∈ ↑f } :=
  fun a =>
    funOfIdeal a our_ideal
      (_ : ∃ x_1, x_1 ∈ definedAtLeft (↑(Set.Ioo x y)) a ∧ x_1 ∈ idealOfCofinals default (definedAtLeft ↑(Set.Ioo x y)))
a₁ a₂ : α
f : PartialIso α ↑(Set.Ioo x y)
hf : f ∈ our_ideal
ha₁ : (a₁, ↑(F a₁)) ∈ ↑f
⊢ a₁ < a₂ → (fun a => ↑(F a)) a₁ < (fun a => ↑(F a)) a₂
[PROOFSTEP]
rcases(F a₂).prop with ⟨g, hg, ha₂⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : Encodable α
inst✝¹ : DenselyOrdered β
inst✝ : Nontrivial β
x y : β
hxy : x < y
a : β
ha : x < a ∧ a < y
this : Nonempty ↑(Set.Ioo x y)
our_ideal : Ideal (PartialIso α ↑(Set.Ioo x y)) := idealOfCofinals default (definedAtLeft ↑(Set.Ioo x y))
F : (a : α) → { b // ∃ f, f ∈ our_ideal ∧ (a, b) ∈ ↑f } :=
  fun a =>
    funOfIdeal a our_ideal
      (_ : ∃ x_1, x_1 ∈ definedAtLeft (↑(Set.Ioo x y)) a ∧ x_1 ∈ idealOfCofinals default (definedAtLeft ↑(Set.Ioo x y)))
a₁ a₂ : α
f : PartialIso α ↑(Set.Ioo x y)
hf : f ∈ our_ideal
ha₁ : (a₁, ↑(F a₁)) ∈ ↑f
g : PartialIso α ↑(Set.Ioo x y)
hg : g ∈ our_ideal
ha₂ : (a₂, ↑(F a₂)) ∈ ↑g
⊢ a₁ < a₂ → (fun a => ↑(F a)) a₁ < (fun a => ↑(F a)) a₂
[PROOFSTEP]
rcases our_ideal.directed _ hf _ hg with ⟨m, _hm, fm, gm⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : Encodable α
inst✝¹ : DenselyOrdered β
inst✝ : Nontrivial β
x y : β
hxy : x < y
a : β
ha : x < a ∧ a < y
this : Nonempty ↑(Set.Ioo x y)
our_ideal : Ideal (PartialIso α ↑(Set.Ioo x y)) := idealOfCofinals default (definedAtLeft ↑(Set.Ioo x y))
F : (a : α) → { b // ∃ f, f ∈ our_ideal ∧ (a, b) ∈ ↑f } :=
  fun a =>
    funOfIdeal a our_ideal
      (_ : ∃ x_1, x_1 ∈ definedAtLeft (↑(Set.Ioo x y)) a ∧ x_1 ∈ idealOfCofinals default (definedAtLeft ↑(Set.Ioo x y)))
a₁ a₂ : α
f : PartialIso α ↑(Set.Ioo x y)
hf : f ∈ our_ideal
ha₁ : (a₁, ↑(F a₁)) ∈ ↑f
g : PartialIso α ↑(Set.Ioo x y)
hg : g ∈ our_ideal
ha₂ : (a₂, ↑(F a₂)) ∈ ↑g
m : PartialIso α ↑(Set.Ioo x y)
_hm : m ∈ ↑our_ideal
fm : f ≤ m
gm : g ≤ m
⊢ a₁ < a₂ → (fun a => ↑(F a)) a₁ < (fun a => ↑(F a)) a₂
[PROOFSTEP]
exact (lt_iff_lt_of_cmp_eq_cmp <| m.prop (a₁, _) (fm ha₁) (a₂, _) (gm ha₂)).mp
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹¹ : LinearOrder α
inst✝¹⁰ : LinearOrder β
inst✝⁹ : Encodable α
inst✝⁸ : DenselyOrdered α
inst✝⁷ : NoMinOrder α
inst✝⁶ : NoMaxOrder α
inst✝⁵ : Nonempty α
inst✝⁴ : Encodable β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
to_cofinal : α ⊕ β → Cofinal (PartialIso α β) := fun p => Sum.recOn p (definedAtLeft β) (definedAtRight α)
our_ideal : Ideal (PartialIso α β) := idealOfCofinals default to_cofinal
F : (a : α) → { b // ∃ f, f ∈ our_ideal ∧ (a, b) ∈ ↑f } :=
  fun a => funOfIdeal a our_ideal (_ : ∃ x, x ∈ to_cofinal (Sum.inl a) ∧ x ∈ idealOfCofinals default to_cofinal)
G : (b : β) → { a // ∃ f, f ∈ our_ideal ∧ (a, b) ∈ ↑f } :=
  fun b => invOfIdeal b our_ideal (_ : ∃ x, x ∈ to_cofinal (Sum.inr b) ∧ x ∈ idealOfCofinals default to_cofinal)
a : α
b : β
⊢ cmp a ((fun b => ↑(G b)) b) = cmp ((fun a => ↑(F a)) a) b
[PROOFSTEP]
rcases(F a).prop with ⟨f, hf, ha⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹¹ : LinearOrder α
inst✝¹⁰ : LinearOrder β
inst✝⁹ : Encodable α
inst✝⁸ : DenselyOrdered α
inst✝⁷ : NoMinOrder α
inst✝⁶ : NoMaxOrder α
inst✝⁵ : Nonempty α
inst✝⁴ : Encodable β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
to_cofinal : α ⊕ β → Cofinal (PartialIso α β) := fun p => Sum.recOn p (definedAtLeft β) (definedAtRight α)
our_ideal : Ideal (PartialIso α β) := idealOfCofinals default to_cofinal
F : (a : α) → { b // ∃ f, f ∈ our_ideal ∧ (a, b) ∈ ↑f } :=
  fun a => funOfIdeal a our_ideal (_ : ∃ x, x ∈ to_cofinal (Sum.inl a) ∧ x ∈ idealOfCofinals default to_cofinal)
G : (b : β) → { a // ∃ f, f ∈ our_ideal ∧ (a, b) ∈ ↑f } :=
  fun b => invOfIdeal b our_ideal (_ : ∃ x, x ∈ to_cofinal (Sum.inr b) ∧ x ∈ idealOfCofinals default to_cofinal)
a : α
b : β
f : PartialIso α β
hf : f ∈ our_ideal
ha : (a, ↑(F a)) ∈ ↑f
⊢ cmp a ((fun b => ↑(G b)) b) = cmp ((fun a => ↑(F a)) a) b
[PROOFSTEP]
rcases(G b).prop with ⟨g, hg, hb⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹¹ : LinearOrder α
inst✝¹⁰ : LinearOrder β
inst✝⁹ : Encodable α
inst✝⁸ : DenselyOrdered α
inst✝⁷ : NoMinOrder α
inst✝⁶ : NoMaxOrder α
inst✝⁵ : Nonempty α
inst✝⁴ : Encodable β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
to_cofinal : α ⊕ β → Cofinal (PartialIso α β) := fun p => Sum.recOn p (definedAtLeft β) (definedAtRight α)
our_ideal : Ideal (PartialIso α β) := idealOfCofinals default to_cofinal
F : (a : α) → { b // ∃ f, f ∈ our_ideal ∧ (a, b) ∈ ↑f } :=
  fun a => funOfIdeal a our_ideal (_ : ∃ x, x ∈ to_cofinal (Sum.inl a) ∧ x ∈ idealOfCofinals default to_cofinal)
G : (b : β) → { a // ∃ f, f ∈ our_ideal ∧ (a, b) ∈ ↑f } :=
  fun b => invOfIdeal b our_ideal (_ : ∃ x, x ∈ to_cofinal (Sum.inr b) ∧ x ∈ idealOfCofinals default to_cofinal)
a : α
b : β
f : PartialIso α β
hf : f ∈ our_ideal
ha : (a, ↑(F a)) ∈ ↑f
g : PartialIso α β
hg : g ∈ our_ideal
hb : (↑(G b), b) ∈ ↑g
⊢ cmp a ((fun b => ↑(G b)) b) = cmp ((fun a => ↑(F a)) a) b
[PROOFSTEP]
rcases our_ideal.directed _ hf _ hg with ⟨m, _, fm, gm⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹¹ : LinearOrder α
inst✝¹⁰ : LinearOrder β
inst✝⁹ : Encodable α
inst✝⁸ : DenselyOrdered α
inst✝⁷ : NoMinOrder α
inst✝⁶ : NoMaxOrder α
inst✝⁵ : Nonempty α
inst✝⁴ : Encodable β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
to_cofinal : α ⊕ β → Cofinal (PartialIso α β) := fun p => Sum.recOn p (definedAtLeft β) (definedAtRight α)
our_ideal : Ideal (PartialIso α β) := idealOfCofinals default to_cofinal
F : (a : α) → { b // ∃ f, f ∈ our_ideal ∧ (a, b) ∈ ↑f } :=
  fun a => funOfIdeal a our_ideal (_ : ∃ x, x ∈ to_cofinal (Sum.inl a) ∧ x ∈ idealOfCofinals default to_cofinal)
G : (b : β) → { a // ∃ f, f ∈ our_ideal ∧ (a, b) ∈ ↑f } :=
  fun b => invOfIdeal b our_ideal (_ : ∃ x, x ∈ to_cofinal (Sum.inr b) ∧ x ∈ idealOfCofinals default to_cofinal)
a : α
b : β
f : PartialIso α β
hf : f ∈ our_ideal
ha : (a, ↑(F a)) ∈ ↑f
g : PartialIso α β
hg : g ∈ our_ideal
hb : (↑(G b), b) ∈ ↑g
m : PartialIso α β
left✝ : m ∈ ↑our_ideal
fm : f ≤ m
gm : g ≤ m
⊢ cmp a ((fun b => ↑(G b)) b) = cmp ((fun a => ↑(F a)) a) b
[PROOFSTEP]
exact m.prop (a, _) (fm ha) (_, b) (gm hb)
