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 β
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
hr : a < p1
this : a < p1 ∧ b < p2
⊢ cmp p1 a = Ordering.gt ∧ cmp p2 b = Ordering.gt

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

Premises used: cmp_eq_gt_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
hr : a < p1
this : cmp p1 a = Ordering.gt ∧ cmp p2 b = Ordering.gt
⊢ 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
hr : a < p1
this : cmp p1 a = Ordering.gt ∧ cmp p2 b = Ordering.gt
⊢ 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 β
f : Finset (α × β)
hf : ∀ p ∈ f, ∀ q ∈ f, cmp p.1 q.1 = cmp p.2 q.2
p : β × α
hp : Membership.mem (γ := Finset (β × α)) (Finset.image (⇑(Equiv.prodComm α β) : (a : α × β) → β × α) f) p
q : β × α
hq : Membership.mem (γ := Finset (β × α)) (Finset.image (⇑(Equiv.prodComm α β) : (a : α × β) → β × α) f) q
rw :
  ∀
    (hp :
      Membership.mem (γ := Set (β × α)) ((⇑(Equiv.prodComm α β).symm : (a : β × α) → α × β) ⁻¹' (↑f : Set (α × β))) p)
    (q : β × α)
    (hq : Membership.mem (γ := Finset (β × α)) (Finset.image (⇑(Equiv.prodComm α β) : (a : α × β) → β × α) f) q),
    Membership.mem (α := α × β) f (((Equiv.prodComm α β).symm : (a : β × α) → α × β) p : α × β)
⊢ Membership.mem (α := α × β) f (((Equiv.prodComm α β).symm : (a : β × α) → α × β) p : α × β)

Tactic:
rw [← Finset.mem_coe, Finset.coe_image, Equiv.image_eq_preimage_symm] at hp

Premises used: Finset.coe_image, Equiv.image_eq_preimage_symm, Finset.mem_coe
-- Module: Mathlib.Order.CountableDenseLinearOrder
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
f : Finset (α × β)
hf : ∀ p ∈ f, ∀ q ∈ f, cmp p.1 q.1 = cmp p.2 q.2
p : β × α
hp : Membership.mem (γ := Set (β × α)) ((⇑(Equiv.prodComm α β).symm : (a : β × α) → α × β) ⁻¹' (↑f : Set (α × β))) p
q : β × α
hq : Membership.mem (γ := Finset (β × α)) (Finset.image (⇑(Equiv.prodComm α β) : (a : α × β) → β × α) f) q
rwa rwa₁ rwa₂ rwa₃ :
  Membership.mem (α := α × β) (↑f : Set (α × β)) (((Equiv.prodComm α β).symm : (a : β × α) → α × β) p : α × β)
⊢ Membership.mem (α := α × β) f (((Equiv.prodComm α β).symm : (a : β × α) → α × β) p : α × β)

Tactic:
rwa [← Finset.mem_coe]

Premises used: Finset.mem_coe
-- Module: Mathlib.Order.CountableDenseLinearOrder
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
f : Finset (α × β)
hf : ∀ p ∈ f, ∀ q ∈ f, cmp p.1 q.1 = cmp p.2 q.2
p : β × α
hp : Membership.mem (γ := Finset (β × α)) (Finset.image (⇑(Equiv.prodComm α β) : (a : α × β) → β × α) f) p
q : β × α
hq : Membership.mem (γ := Finset (β × α)) (Finset.image (⇑(Equiv.prodComm α β) : (a : α × β) → β × α) f) q
⊢ Membership.mem (γ := Set (β × α)) ((⇑(Equiv.prodComm α β).symm : (a : β × α) → α × β) ⁻¹' (↑f : Set (α × β))) q

Tactic:
rw [← Finset.mem_coe, Finset.coe_image, Equiv.image_eq_preimage_symm] at hq

Premises used: Finset.coe_image, Equiv.image_eq_preimage_symm, Finset.mem_coe
-- Module: Mathlib.Order.CountableDenseLinearOrder
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
f : Finset (α × β)
hf : ∀ p ∈ f, ∀ q ∈ f, cmp p.1 q.1 = cmp p.2 q.2
p : β × α
hp : Membership.mem (γ := Finset (β × α)) (Finset.image (⇑(Equiv.prodComm α β) : (a : α × β) → β × α) f) p
q : β × α
hq : Membership.mem (γ := Set (β × α)) ((⇑(Equiv.prodComm α β).symm : (a : β × α) → α × β) ⁻¹' (↑f : Set (α × β))) q
rwa rwa₁ rwa₂ rwa₃ :
  Membership.mem (α := α × β) (↑f : Set (α × β)) (((Equiv.prodComm α β).symm : (a : β × α) → α × β) q : α × β)
⊢ Membership.mem (α := α × β) f (((Equiv.prodComm α β).symm : (a : β × α) → α × β) q : α × β)

Tactic:
rwa [← Finset.mem_coe]

Premises used: Finset.mem_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 β
inst_5 : Nonempty β
a : α
f : PartialIso α β
obtain :
  ∀ (b : β) (a_b : ∀ p ∈ (↑f : Finset (α × β)), cmp p.1 a = cmp p.2 b),
    ∃ (y : PartialIso α β),
      Membership.mem (γ := Set (PartialIso α β)) {f : PartialIso α β | ∃ (b : β), (a, b) ∈ (↑f : Finset (α × β))} y ∧
        f ≤ y
⊢ ∃ (y : PartialIso α β),
    Membership.mem (γ := Set (PartialIso α β)) {f : PartialIso α β | ∃ (b : β), (a, b) ∈ (↑f : Finset (α × β))} y ∧
      f ≤ y

Tactic:
obtain ⟨b, a_b⟩ := exists_across f a

Premises used: Order.PartialIso.exists_across
-- 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 β
a : α
f : PartialIso α β
b : β
a_b : ∀ p ∈ (↑f : Finset (α × β)), cmp p.1 a = cmp p.2 b
⊢ ∃ (y : PartialIso α β),
    Membership.mem (γ := Set (PartialIso α β)) {f : PartialIso α β | ∃ (b : β), (a, b) ∈ (↑f : Finset (α × β))} y ∧
      f ≤ y

Tactic:
⟨⟨insert (a, b) f.val, fun p hp q hq ↦ ?_⟩, ⟨b, Finset.mem_insert_self _ _⟩,
        Finset.subset_insert _ _⟩

Premises used: Finset.mem_insert_self, Insert.insert, Prod.mk, Subtype.mk, And.intro, Exists.intro, Finset.subset_insert, 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 β
a : α
f : PartialIso α β
b : β
a_b : ∀ p ∈ (↑f : Finset (α × β)), cmp p.1 a = cmp p.2 b
fun :
  ∀ (p : α × β) (hp : p ∈ insert (a, b) (↑f : Finset (α × β))) (q : α × β)
    (hq : q ∈ insert (a, b) (↑f : Finset (α × β))), cmp p.1 q.1 = cmp p.2 q.2
⊢ ∃ (y : PartialIso α β),
    Membership.mem (γ := Set (PartialIso α β)) {f : PartialIso α β | ∃ (b : β), (a, b) ∈ (↑f : Finset (α × β))} y ∧
      f ≤ y

Tactic:
refine
      ⟨⟨insert (a, b) f.val, fun p hp q hq ↦ ?_⟩, ⟨b, Finset.mem_insert_self _ _⟩,
        Finset.subset_insert _ _⟩
-- 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 β
a : α
f : PartialIso α β
b : β
a_b : ∀ p ∈ (↑f : Finset (α × β)), cmp p.1 a = cmp p.2 b
p : α × β
hp : p ∈ insert (a, b) (↑f : Finset (α × β))
q : α × β
hq : q ∈ insert (a, b) (↑f : Finset (α × β))
rw :
  ∀ (hp : p = (a, b) ∨ p ∈ (↑f : Finset (α × β))) (q : α × β) (hq : q = (a, b) ∨ q ∈ (↑f : Finset (α × β))),
    cmp p.1 q.1 = cmp p.2 q.2
⊢ cmp p.1 q.1 = cmp p.2 q.2

Tactic:
rw [Finset.mem_insert] at hp hq

Premises used: Finset.mem_insert
-- 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 β
a : α
f : PartialIso α β
b : β
a_b : ∀ p ∈ (↑f : Finset (α × β)), cmp p.1 a = cmp p.2 b
p : α × β
hp : p = (a, b) ∨ p ∈ (↑f : Finset (α × β))
q : α × β
hq : q = (a, b) ∨ q ∈ (↑f : Finset (α × β))
inl : cmp (a, b).1 q.1 = cmp (a, b).2 q.2
inr : ∀ (pf : p ∈ (↑f : Finset (α × β))), cmp p.1 q.1 = cmp p.2 q.2
⊢ cmp p.1 q.1 = cmp p.2 q.2

Tactic:
rcases hp with (rfl | pf)

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 β
a : α
f : PartialIso α β
b : β
a_b : ∀ p ∈ (↑f : Finset (α × β)), cmp p.1 a = cmp p.2 b
q : α × β
hq : q = (a, b) ∨ q ∈ (↑f : Finset (α × β))
inl : cmp (a, b).1 (a, b).1 = cmp (a, b).2 (a, b).2
inl₁ : ∀ (qf : q ∈ (↑f : Finset (α × β))), cmp (a, b).1 q.1 = cmp (a, b).2 q.2
⊢ cmp (a, b).1 q.1 = cmp (a, b).2 q.2

Tactic:
rcases hq with (rfl | qf)

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 β
a : α
f : PartialIso α β
b : β
a_b : ∀ p ∈ (↑f : Finset (α × β)), cmp p.1 a = cmp p.2 b
p q : α × β
hq : q = (a, b) ∨ q ∈ (↑f : Finset (α × β))
pf : p ∈ (↑f : Finset (α × β))
inr : cmp p.1 (a, b).1 = cmp p.2 (a, b).2
inr₁ : ∀ (qf : q ∈ (↑f : Finset (α × β))), cmp p.1 q.1 = cmp p.2 q.2
⊢ cmp p.1 q.1 = cmp p.2 q.2

Tactic:
rcases hq with (rfl | qf)

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 β
a : α
f : PartialIso α β
b : β
a_b : ∀ p ∈ (↑f : Finset (α × β)), cmp p.1 a = cmp p.2 b
⊢ cmp (a, b).1 (a, b).1 = cmp (a, b).2 (a, b).2

Tactic:
simp only [cmp_self_eq_eq]

Premises used: cmp_self_eq_eq
-- 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 β
a : α
f : PartialIso α β
b : β
a_b : ∀ p ∈ (↑f : Finset (α × β)), cmp p.1 a = cmp p.2 b
q : α × β
qf : q ∈ (↑f : Finset (α × β))
inl : cmp q.1 (a, b).1 = cmp q.2 (a, b).2
⊢ cmp (a, b).1 q.1 = cmp (a, b).2 q.2

Tactic:
rw [cmp_eq_cmp_symm]

Premises used: cmp_eq_cmp_symm
-- 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 β
a : α
f : PartialIso α β
b : β
a_b : ∀ p ∈ (↑f : Finset (α × β)), cmp p.1 a = cmp p.2 b
q : α × β
qf : q ∈ (↑f : Finset (α × β))
⊢ cmp q.1 (a, b).1 = cmp q.2 (a, b).2

Tactic:
a_b _ qf
-- 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 β
a : α
f : PartialIso α β
b : β
a_b : ∀ p ∈ (↑f : Finset (α × β)), cmp p.1 a = cmp p.2 b
q : α × β
qf : q ∈ (↑f : Finset (α × β))
⊢ cmp q.1 (a, b).1 = cmp q.2 (a, b).2

Tactic:
exact a_b _ qf
-- 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 β
a : α
f : PartialIso α β
b : β
a_b : ∀ p ∈ (↑f : Finset (α × β)), cmp p.1 a = cmp p.2 b
p : α × β
pf : p ∈ (↑f : Finset (α × β))
⊢ cmp p.1 (a, b).1 = cmp p.2 (a, b).2

Tactic:
a_b _ pf
-- 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 β
a : α
f : PartialIso α β
b : β
a_b : ∀ p ∈ (↑f : Finset (α × β)), cmp p.1 a = cmp p.2 b
p : α × β
pf : p ∈ (↑f : Finset (α × β))
⊢ cmp p.1 (a, b).1 = cmp p.2 (a, b).2

Tactic:
exact a_b _ pf
-- 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 β
a : α
f : PartialIso α β
b : β
a_b : ∀ p ∈ (↑f : Finset (α × β)), cmp p.1 a = cmp p.2 b
p q : α × β
pf : p ∈ (↑f : Finset (α × β))
qf : q ∈ (↑f : Finset (α × β))
⊢ cmp p.1 q.1 = cmp p.2 q.2

Tactic:
f.prop _ pf _ qf

Premises used: 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 β
a : α
f : PartialIso α β
b : β
a_b : ∀ p ∈ (↑f : Finset (α × β)), cmp p.1 a = cmp p.2 b
p q : α × β
pf : p ∈ (↑f : Finset (α × β))
qf : q ∈ (↑f : Finset (α × β))
⊢ cmp p.1 q.1 = cmp p.2 q.2

Tactic:
exact f.prop _ pf _ qf

Premises used: 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 α
b : β
f : PartialIso α β
rcases :
  ∀ (f' : PartialIso β α) (hl : f.comm ≤ f') (a : α) (ha : (b, a) ∈ (↑f' : Finset (β × α))),
    ∃ (y : PartialIso α β),
      Membership.mem (γ := Set (PartialIso α β)) {f : PartialIso α β | ∃ (a : α), (a, b) ∈ (↑f : Finset (α × β))} y ∧
        f ≤ y
⊢ ∃ (y : PartialIso α β),
    Membership.mem (γ := Set (PartialIso α β)) {f : PartialIso α β | ∃ (a : α), (a, b) ∈ (↑f : Finset (α × β))} y ∧
      f ≤ y

Tactic:
rcases (definedAtLeft α b).isCofinal f.comm with ⟨f', ⟨a, ha⟩, hl⟩

Premises used: Order.PartialIso.comm, Order.PartialIso.definedAtLeft, Order.Cofinal.isCofinal
-- 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 α
b : β
f : PartialIso α β
f' : PartialIso β α
hl : f.comm ≤ f'
a : α
ha : (b, a) ∈ (↑f' : Finset (β × α))
⊢ ∃ (y : PartialIso α β),
    Membership.mem (γ := Set (PartialIso α β)) {f : PartialIso α β | ∃ (a : α), (a, b) ∈ (↑f : Finset (α × β))} y ∧
      f ≤ y

Tactic:
⟨f'.comm, ⟨a, ?_⟩, ?_⟩

Premises used: Order.PartialIso.comm, And.intro, 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 α
b : β
f : PartialIso α β
f' : PartialIso β α
hl : f.comm ≤ f'
a : α
ha : (b, a) ∈ (↑f' : Finset (β × α))
refine_1 : (a, b) ∈ (↑f'.comm : Finset (α × β))
refine_2 : f ≤ f'.comm
⊢ ∃ (y : PartialIso α β),
    Membership.mem (γ := Set (PartialIso α β)) {f : PartialIso α β | ∃ (a : α), (a, b) ∈ (↑f : Finset (α × β))} y ∧
      f ≤ y

Tactic:
refine ⟨f'.comm, ⟨a, ?_⟩, ?_⟩
-- 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 α
b : β
f : PartialIso α β
f' : PartialIso β α
hl : f.comm ≤ f'
a : α
ha : (b, a) ∈ (↑f' : Finset (β × α))
refine_1 : (a, b) ∈ (↑(Finset.image (⇑(Equiv.prodComm β α) : (a : β × α) → α × β) (↑f' : Finset (β × α))) : Set (α × β))
refine_1₁ :
  Membership.mem (γ := Set (α × β))
    ((⇑(Equiv.prodComm β α) : (a : β × α) → α × β) '' (↑(↑f' : Finset (β × α)) : Set (β × α))) (a, b)
refine_1₂ refine_1₃ refine_1₄ refine_1₅ :
  Membership.mem (γ := Set (α × β))
    ((⇑(Equiv.prodComm β α).symm : (a : α × β) → β × α) ⁻¹' (↑(↑f' : Finset (β × α)) : Set (β × α))) (a, b)
⊢ Membership.mem (γ := Finset (α × β))
    (Finset.image (⇑(Equiv.prodComm β α) : (a : β × α) → α × β) (↑f' : Finset (β × α))) (a, b)

Tactic:
rwa [← Finset.mem_coe, Finset.coe_image, Equiv.image_eq_preimage_symm]

Premises used: Finset.coe_image, Equiv.image_eq_preimage_symm, Finset.mem_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 α
inst_5 : Nonempty α
b : β
f : PartialIso α β
f' : PartialIso β α
hl : f.comm ≤ f'
a : α
ha : (b, a) ∈ (↑f' : Finset (β × α))
refine_2 :
  (↑(↑f : Finset (α × β)) : Set (α × β)) ⊆
    (↑(Finset.image (⇑(Equiv.prodComm β α) : (a : β × α) → α × β) (↑f' : Finset (β × α))) : Set (α × β))
refine_2₁ :
  (↑(↑f : Finset (α × β)) : Set (α × β)) ⊆
    (⇑(Equiv.prodComm β α) : (a : β × α) → α × β) '' (↑(↑f' : Finset (β × α)) : Set (β × α))
refine_2₂ :
  (⇑(Equiv.prodComm β α).symm : (a : α × β) → β × α) '' (↑(↑f : Finset (α × β)) : Set (α × β)) ⊆
    (↑(↑f' : Finset (β × α)) : Set (β × α))
refine_2₃ :
  (↑(Finset.image (⇑(Equiv.prodComm β α).symm : (a : α × β) → β × α) (↑f : Finset (α × β))) : Set (β × α)) ⊆
    (↑(↑f' : Finset (β × α)) : Set (β × α))
refine_2₄ refine_2₅ refine_2₆ refine_2₇ :
  Finset.image (⇑(Equiv.prodComm β α).symm : (a : α × β) → β × α) (↑f : Finset (α × β)) ⊆ (↑f' : Finset (β × α))
⊢ (↑f : Finset (α × β)) ⊆ Finset.image (⇑(Equiv.prodComm β α) : (a : β × α) → α × β) (↑f' : Finset (β × α))

Tactic:
rwa [← Finset.coe_subset, Finset.coe_image, ← Equiv.symm_image_subset, ← Finset.coe_image,
        Finset.coe_subset]

Premises used: Finset.coe_image, Equiv.symm_image_subset, Finset.coe_subset
-- Module: Mathlib.Order.CountableDenseLinearOrder
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
inst_2 : Countable α
inst_3 : DenselyOrdered β
inst_4 : Nontrivial β
intro : ∀ (val : Encodable α), Nonempty (α ↪o β)
⊢ Nonempty (α ↪o β)

Tactic:
cases nonempty_encodable α

Premises used: nonempty_encodable
-- Module: Mathlib.Order.CountableDenseLinearOrder
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
inst_2 : Countable α
inst_3 : DenselyOrdered β
inst_4 : Nontrivial β
val : Encodable α
intro : ∀ (x y : β) (hxy : x < y), Nonempty (α ↪o β)
⊢ Nonempty (α ↪o β)

Tactic:
rcases exists_pair_lt β with ⟨x, y, hxy⟩

Premises used: exists_pair_lt
-- Module: Mathlib.Order.CountableDenseLinearOrder
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
inst_2 : Countable α
inst_3 : DenselyOrdered β
inst_4 : Nontrivial β
val : Encodable α
x y : β
hxy : x < y
intro : ∀ (a : β) (ha : x < a ∧ a < y), Nonempty (α ↪o β)
⊢ Nonempty (α ↪o β)

Tactic:
obtain ⟨a, ha⟩ := exists_between hxy

Premises used: exists_between
-- Module: Mathlib.Order.CountableDenseLinearOrder
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
inst_2 : Countable α
inst_3 : DenselyOrdered β
inst_4 : Nontrivial β
val : Encodable α
x y : β
hxy : x < y
a : β
ha : x < a ∧ a < y
⊢ Nonempty.{u_2 + 1} (↑(Set.Ioo x y) : Type u_2)

Tactic:
haveI : Nonempty (Set.Ioo x y) := ⟨⟨a, ha⟩⟩
-- Module: Mathlib.Order.CountableDenseLinearOrder
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
inst_2 : Countable α
inst_3 : DenselyOrdered β
inst_4 : Nontrivial β
val : Encodable α
x y : β
hxy : x < y
a : β
ha : x < a ∧ a < y
this : Nonempty.{u_2 + 1} (↑(Set.Ioo x y) : Type u_2)
our_ideal : Ideal (PartialIso.{u_1, u_2} α (↑(Set.Ioo x y) : Type u_2)) :=
  idealOfCofinals default (definedAtLeft (↑(Set.Ioo x y) : Type u_2))
F : (a : α) →
  { b : (↑(Set.Ioo x y) : Type u_2) // ∃ f ∈ our_ideal, (a, b) ∈ (↑f : Finset (α × (↑(Set.Ioo x y) : Type u_2))) } :=
  fun (a : α) ↦ funOfIdeal a our_ideal ⋯
⊢ Nonempty (α ↪o β)

Tactic:
⟨RelEmbedding.trans (OrderEmbedding.ofStrictMono (fun a ↦ (F a).val) fun a₁ a₂ ↦ ?_)
        (OrderEmbedding.subtype _)⟩

Premises used: Nonempty.intro, OrderEmbedding.ofStrictMono, OrderEmbedding.subtype, RelEmbedding.trans, Subtype.val
-- Module: Mathlib.Order.CountableDenseLinearOrder
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
inst_2 : Countable α
inst_3 : DenselyOrdered β
inst_4 : Nontrivial β
val : Encodable α
x y : β
hxy : x < y
a : β
ha : x < a ∧ a < y
this : Nonempty.{u_2 + 1} (↑(Set.Ioo x y) : Type u_2)
our_ideal : Ideal (PartialIso.{u_1, u_2} α (↑(Set.Ioo x y) : Type u_2)) :=
  idealOfCofinals default (definedAtLeft (↑(Set.Ioo x y) : Type u_2))
F : (a : α) →
  { b : (↑(Set.Ioo x y) : Type u_2) // ∃ f ∈ our_ideal, (a, b) ∈ (↑f : Finset (α × (↑(Set.Ioo x y) : Type u_2))) } :=
  fun (a : α) ↦ funOfIdeal a our_ideal ⋯
intro :
  ∀ (a₁ a₂ : α),
    a₁ < a₂ →
      LT.lt.{u_2} (α := (↑(Set.Ioo x y) : Type u_2)) ((fun (a : α) ↦ (↑(F a) : (↑(Set.Ioo x y) : Type u_2))) a₁)
        ((fun (a : α) ↦ (↑(F a) : (↑(Set.Ioo x y) : Type u_2))) a₂)
⊢ Nonempty (α ↪o β)

Tactic:
refine
    ⟨RelEmbedding.trans (OrderEmbedding.ofStrictMono (fun a ↦ (F a).val) fun a₁ a₂ ↦ ?_)
        (OrderEmbedding.subtype _)⟩
-- Module: Mathlib.Order.CountableDenseLinearOrder
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
inst_2 : Countable α
inst_3 : DenselyOrdered β
inst_4 : Nontrivial β
val : Encodable α
x y : β
hxy : x < y
a : β
ha : x < a ∧ a < y
this : Nonempty.{u_2 + 1} (↑(Set.Ioo x y) : Type u_2)
our_ideal : Ideal (PartialIso.{u_1, u_2} α (↑(Set.Ioo x y) : Type u_2)) :=
  idealOfCofinals default (definedAtLeft (↑(Set.Ioo x y) : Type u_2))
F : (a : α) →
  { b : (↑(Set.Ioo x y) : Type u_2) // ∃ f ∈ our_ideal, (a, b) ∈ (↑f : Finset (α × (↑(Set.Ioo x y) : Type u_2))) } :=
  fun (a : α) ↦ funOfIdeal a our_ideal ⋯
a₁ a₂ : α
intro :
  ∀ (f : PartialIso.{u_1, u_2} α (↑(Set.Ioo x y) : Type u_2)) (hf : f ∈ our_ideal)
    (ha₁ : (a₁, (↑(F a₁) : (↑(Set.Ioo x y) : Type u_2))) ∈ (↑f : Finset (α × (↑(Set.Ioo x y) : Type u_2)))),
    a₁ < a₂ →
      LT.lt.{u_2} (α := (↑(Set.Ioo x y) : Type u_2)) ((fun (a : α) ↦ (↑(F a) : (↑(Set.Ioo x y) : Type u_2))) a₁)
        ((fun (a : α) ↦ (↑(F a) : (↑(Set.Ioo x y) : Type u_2))) a₂)
⊢ a₁ < a₂ →
    LT.lt.{u_2} (α := (↑(Set.Ioo x y) : Type u_2)) ((fun (a : α) ↦ (↑(F a) : (↑(Set.Ioo x y) : Type u_2))) a₁)
      ((fun (a : α) ↦ (↑(F a) : (↑(Set.Ioo x y) : Type u_2))) a₂)

Tactic:
rcases (F a₁).prop with ⟨f, hf, ha₁⟩

Premises used: Subtype.prop