awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.CountableDenseLinearOrder (goal)
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
⊢ ∃ (b : β), ∀ p ∈ (↑f : Finset (α × β)), cmp p.1 a = cmp p.2 b
have neg : ∀ (h : ¬∃ (b : β), (a, b) ∈ (↑f : Finset (α × β))), ∃ (b : β), ∀ p ∈ (↑f : Finset (α × β)), cmp p.1 a = cmp p.2 b
Tactic: by_cases h : ∃ b, (a, b) ∈ f.val
-- Lean 4 proof step from Mathlib.Order.CountableDenseLinearOrder (goal)
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 (α × β))
⊢ ∃ (b : β), ∀ p ∈ (↑f : Finset (α × β)), cmp p.1 a = cmp p.2 b
have pos : ∀ (b : β) (hb : (a, b) ∈ (↑f : Finset (α × β))), ∃ (b : β), ∀ p ∈ (↑f : Finset (α × β)), cmp p.1 a = cmp p.2 b
Tactic: obtain ⟨b, hb⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.CountableDenseLinearOrder (goal)
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})
⊢ x < y
have 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
Tactic: rw [Finset.mem_image] at hx hy
Cleared hypotheses: hx, y, hy
-- Lean 4 proof step from Mathlib.Order.CountableDenseLinearOrder (goal)
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
⊢ x < y
have rcases : ∀ (p : α × β) (hp1 : p ∈ {p ∈ (↑f : Finset (α × β)) | p.1 < a}), p.2 < y
Tactic: rcases hx with ⟨p, hp1, rfl⟩
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Order.CountableDenseLinearOrder (goal)
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}
⊢ p.2 < y
have rcases : ∀ (q : α × β) (hq1 : q ∈ {p ∈ (↑f : Finset (α × β)) | a < p.1}), p.2 < q.2
Tactic: rcases hy with ⟨q, hq1, rfl⟩
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Order.CountableDenseLinearOrder (goal)
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}
⊢ p.2 < q.2
have rw : ∀ (hp1 : p ∈ (↑f : Finset (α × β)) ∧ p.1 < a) (q : α × β) (hq1 : q ∈ (↑f : Finset (α × β)) ∧ a < q.1), p.2 < q.2
Tactic: rw [Finset.mem_filter] at hp1 hq1
Cleared hypotheses: hp1, q, hq1
-- Lean 4 proof step from Mathlib.Order.CountableDenseLinearOrder (goal)
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.2 < q.2
have rw : p.1 < q.1
Tactic: rw [← lt_iff_lt_of_cmp_eq_cmp (f.prop _ hp1.1 _ hq1.1)]
-- Lean 4 proof step from Mathlib.Order.CountableDenseLinearOrder (hypothesis)
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 (α × β))
⊢ ∃ (b : β), ∀ p ∈ (↑f : Finset (α × β)), cmp p.1 a = cmp p.2 b
have 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
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
-- Lean 4 proof step from Mathlib.Order.CountableDenseLinearOrder (goal)
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 : β), ∀ p ∈ (↑f : Finset (α × β)), cmp p.1 a = cmp p.2 b
have 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
Tactic: obtain ⟨b, hb⟩ := exists_between_finsets _ _ this
-- Lean 4 proof step from Mathlib.Order.CountableDenseLinearOrder (goal)
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
⊢ ∃ (b : β), ∀ p ∈ (↑f : Finset (α × β)), cmp p.1 a = cmp p.2 b
have h₁ : ∀ p ∈ (↑f : Finset (α × β)), cmp p.1 a = cmp p.2 b
Tactic: use b
-- Lean 4 proof step from Mathlib.Order.CountableDenseLinearOrder (hypothesis)
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 (α × β))
⊢ cmp (p1, p2).1 a = cmp (p1, p2).2 b
have this₁ : p1 ≠ a
Tactic: have : p1 ≠ a := fun he ↦ h ⟨p2, he ▸ hp⟩
-- Lean 4 proof step from Mathlib.Order.CountableDenseLinearOrder (goal)
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
⊢ cmp (p1, p2).1 a = cmp (p1, p2).2 b
have h₁ : ∀ (hl : p1 < a), cmp (p1, p2).1 a = cmp (p1, p2).2 b
Tactic: rcases lt_or_gt_of_ne this with hl | hr
-- Lean 4 proof step from Mathlib.Order.CountableDenseLinearOrder (goal)
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
⊢ cmp (p1, p2).1 a = cmp (p1, p2).2 b
have h₂ : ∀ (hr : a < p1), cmp (p1, p2).1 a = cmp (p1, p2).2 b
Tactic: rcases lt_or_gt_of_ne this with hl | hr
-- Lean 4 proof step from Mathlib.Order.CountableDenseLinearOrder (hypothesis)
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
⊢ cmp (p1, p2).1 a = cmp (p1, p2).2 b
have this₁ : 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⟩)⟩
-- Lean 4 proof step from Mathlib.Order.CountableDenseLinearOrder (hypothesis)
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, p2).1 a = cmp (p1, p2).2 b
have this₁ : cmp p1 a = Ordering.lt ∧ cmp p2 b = Ordering.lt
Tactic: rw [← cmp_eq_lt_iff, ← cmp_eq_lt_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Order.CountableDenseLinearOrder (hypothesis)
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
⊢ cmp (p1, p2).1 a = cmp (p1, p2).2 b
have this₁ : 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⟩)⟩
-- Lean 4 proof step from Mathlib.Order.CountableDenseLinearOrder (hypothesis)
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, p2).1 a = cmp (p1, p2).2 b
have this₁ : cmp p1 a = Ordering.gt ∧ cmp p2 b = Ordering.gt
Tactic: rw [← cmp_eq_gt_iff, ← cmp_eq_gt_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Order.CountableDenseLinearOrder (goal)
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 (α := α × β) f (((Equiv.prodComm α β).symm : (a : β × α) → α × β) p : α × β)
have 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 : α × β)
Tactic: rw [← Finset.mem_coe, Finset.coe_image, Equiv.image_eq_preimage_symm] at hp
Cleared hypotheses: hp, q, hq
-- Lean 4 proof step from Mathlib.Order.CountableDenseLinearOrder (goal)
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
⊢ Membership.mem (α := α × β) f (((Equiv.prodComm α β).symm : (a : β × α) → α × β) p : α × β)
have rwa : Membership.mem (α := α × β) (↑f : Set (α × β)) (((Equiv.prodComm α β).symm : (a : β × α) → α × β) p : α × β)
Tactic: rwa [← Finset.mem_coe]
-- Lean 4 proof step from Mathlib.Order.CountableDenseLinearOrder (hypothesis)
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 (α := α × β) f (((Equiv.prodComm α β).symm : (a : β × α) → α × β) q : α × β)
have hq₁ : 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
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.Order.CountableDenseLinearOrder (goal)
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
⊢ Membership.mem (α := α × β) f (((Equiv.prodComm α β).symm : (a : β × α) → α × β) q : α × β)
have rwa : Membership.mem (α := α × β) (↑f : Set (α × β)) (((Equiv.prodComm α β).symm : (a : β × α) → α × β) q : α × β)
Tactic: rwa [← Finset.mem_coe]
-- Lean 4 proof step from Mathlib.Order.CountableDenseLinearOrder (goal)
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 α β
⊢ ∃ (y : PartialIso α β),
    Membership.mem (γ := Set (PartialIso α β)) {f : PartialIso α β | ∃ (b : β), (a, b) ∈ (↑f : Finset (α × β))} y ∧
      f ≤ y
have 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
Tactic: obtain ⟨b, a_b⟩ := exists_across f a
-- Lean 4 proof step from Mathlib.Order.CountableDenseLinearOrder (goal)
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
have 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
Tactic: refine
      ⟨⟨insert (a, b) f.val, fun p hp q hq ↦ ?_⟩, ⟨b, Finset.mem_insert_self _ _⟩,
        Finset.subset_insert _ _⟩
-- Lean 4 proof step from Mathlib.Order.CountableDenseLinearOrder (goal)
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 (α × β))
⊢ cmp p.1 q.1 = cmp p.2 q.2
have 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
Tactic: rw [Finset.mem_insert] at hp hq
Cleared hypotheses: hp, q, hq
-- Lean 4 proof step from Mathlib.Order.CountableDenseLinearOrder (goal)
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 (α × β))
⊢ cmp p.1 q.1 = cmp p.2 q.2
have inl : cmp (a, b).1 q.1 = cmp (a, b).2 q.2
Tactic: rcases hp with (rfl | pf)
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.Order.CountableDenseLinearOrder (goal)
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
⊢ cmp p.1 q.1 = cmp p.2 q.2
have inr : ∀ (pf : p ∈ (↑f : Finset (α × β))), cmp p.1 q.1 = cmp p.2 q.2
Tactic: rcases hp with (rfl | pf)
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Order.CountableDenseLinearOrder (goal)
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 (α × β))
⊢ cmp (a, b).1 q.1 = cmp (a, b).2 q.2
have inl : cmp (a, b).1 (a, b).1 = cmp (a, b).2 (a, b).2
Tactic: rcases hq with (rfl | qf)
Cleared hypotheses: q, hq
-- Lean 4 proof step from Mathlib.Order.CountableDenseLinearOrder (goal)
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
⊢ cmp (a, b).1 q.1 = cmp (a, b).2 q.2
have inl₁ : ∀ (qf : q ∈ (↑f : Finset (α × β))), cmp (a, b).1 q.1 = cmp (a, b).2 q.2
Tactic: rcases hq with (rfl | qf)
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.Order.CountableDenseLinearOrder (goal)
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 (α × β))
⊢ cmp p.1 q.1 = cmp p.2 q.2
have inr : cmp p.1 (a, b).1 = cmp p.2 (a, b).2
Tactic: rcases hq with (rfl | qf)
Cleared hypotheses: q, hq
-- Lean 4 proof step from Mathlib.Order.CountableDenseLinearOrder (goal)
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
⊢ cmp p.1 q.1 = cmp p.2 q.2
have inr₁ : ∀ (qf : q ∈ (↑f : Finset (α × β))), cmp p.1 q.1 = cmp p.2 q.2
Tactic: rcases hq with (rfl | qf)
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.Order.CountableDenseLinearOrder (goal)
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 (a, b).1 q.1 = cmp (a, b).2 q.2
have inl : cmp q.1 (a, b).1 = cmp q.2 (a, b).2
Tactic: rw [cmp_eq_cmp_symm]
-- Lean 4 proof step from Mathlib.Order.CountableDenseLinearOrder (goal)
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 α β
⊢ ∃ (y : PartialIso α β),
    Membership.mem (γ := Set (PartialIso α β)) {f : PartialIso α β | ∃ (a : α), (a, b) ∈ (↑f : Finset (α × β))} y ∧
      f ≤ y
have 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
Tactic: rcases (definedAtLeft α b).isCofinal f.comm with ⟨f', ⟨a, ha⟩, hl⟩
-- Lean 4 proof step from Mathlib.Order.CountableDenseLinearOrder (goal)
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
have refine_1 : (a, b) ∈ (↑f'.comm : Finset (α × β))
Tactic: refine ⟨f'.comm, ⟨a, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Order.CountableDenseLinearOrder (goal)
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 (α × β))
⊢ ∃ (y : PartialIso α β),
    Membership.mem (γ := Set (PartialIso α β)) {f : PartialIso α β | ∃ (a : α), (a, b) ∈ (↑f : Finset (α × β))} y ∧
      f ≤ y
have refine_2 : f ≤ f'.comm
Tactic: refine ⟨f'.comm, ⟨a, ?_⟩, ?_⟩