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 α
b : β
f : PartialIso α β
f' : PartialIso β α
hl : f.comm ≤ f'
a : α
ha : (b, a) ∈ (↑f' : Finset (β × α))
⊢ Membership.mem (γ := Finset (α × β))
    (Finset.image (⇑(Equiv.prodComm β α) : (a : β × α) → α × β) (↑f' : Finset (β × α))) (a, b)
have refine_1 : (a, b) ∈ (↑(Finset.image (⇑(Equiv.prodComm β α) : (a : β × α) → α × β) (↑f' : Finset (β × α))) : Set (α × β))
Tactic: rwa [← Finset.mem_coe, Finset.coe_image, Equiv.image_eq_preimage_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 α β
f' : PartialIso β α
hl : f.comm ≤ f'
a : α
ha : (b, a) ∈ (↑f' : Finset (β × α))
refine_1 : (a, b) ∈ (↑(Finset.image (⇑(Equiv.prodComm β α) : (a : β × α) → α × β) (↑f' : Finset (β × α))) : Set (α × β))
⊢ Membership.mem (γ := Finset (α × β))
    (Finset.image (⇑(Equiv.prodComm β α) : (a : β × α) → α × β) (↑f' : Finset (β × α))) (a, b)
have refine_1₁ : Membership.mem (γ := Set (α × β))
  ((⇑(Equiv.prodComm β α) : (a : β × α) → α × β) '' (↑(↑f' : Finset (β × α)) : Set (β × α))) (a, b)
Tactic: rwa [← Finset.mem_coe, Finset.coe_image, Equiv.image_eq_preimage_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 α β
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)
⊢ Membership.mem (γ := Finset (α × β))
    (Finset.image (⇑(Equiv.prodComm β α) : (a : β × α) → α × β) (↑f' : Finset (β × α))) (a, b)
have refine_1₂ : Membership.mem (γ := Set (α × β))
  ((⇑(Equiv.prodComm β α).symm : (a : α × β) → β × α) ⁻¹' (↑(↑f' : Finset (β × α)) : Set (β × α))) (a, b)
Tactic: rwa [← Finset.mem_coe, Finset.coe_image, Equiv.image_eq_preimage_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 α β
f' : PartialIso β α
hl : f.comm ≤ f'
a : α
ha : (b, a) ∈ (↑f' : Finset (β × α))
⊢ (↑f : Finset (α × β)) ⊆ Finset.image (⇑(Equiv.prodComm β α) : (a : β × α) → α × β) (↑f' : Finset (β × α))
have refine_2 : (↑(↑f : Finset (α × β)) : Set (α × β)) ⊆
  (↑(Finset.image (⇑(Equiv.prodComm β α) : (a : β × α) → α × β) (↑f' : Finset (β × α))) : Set (α × β))
Tactic: rwa [← Finset.coe_subset, Finset.coe_image, ← Equiv.symm_image_subset, ← Finset.coe_image,
        Finset.coe_subset]
-- 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_2 :
  (↑(↑f : Finset (α × β)) : Set (α × β)) ⊆
    (↑(Finset.image (⇑(Equiv.prodComm β α) : (a : β × α) → α × β) (↑f' : Finset (β × α))) : Set (α × β))
⊢ (↑f : Finset (α × β)) ⊆ Finset.image (⇑(Equiv.prodComm β α) : (a : β × α) → α × β) (↑f' : Finset (β × α))
have refine_2₁ : (↑(↑f : Finset (α × β)) : Set (α × β)) ⊆
  (⇑(Equiv.prodComm β α) : (a : β × α) → α × β) '' (↑(↑f' : Finset (β × α)) : Set (β × α))
Tactic: rwa [← Finset.coe_subset, Finset.coe_image, ← Equiv.symm_image_subset, ← Finset.coe_image,
        Finset.coe_subset]
-- 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_2 :
  (↑(↑f : Finset (α × β)) : Set (α × β)) ⊆
    (↑(Finset.image (⇑(Equiv.prodComm β α) : (a : β × α) → α × β) (↑f' : Finset (β × α))) : Set (α × β))
refine_2₁ :
  (↑(↑f : Finset (α × β)) : Set (α × β)) ⊆
    (⇑(Equiv.prodComm β α) : (a : β × α) → α × β) '' (↑(↑f' : Finset (β × α)) : Set (β × α))
⊢ (↑f : Finset (α × β)) ⊆ Finset.image (⇑(Equiv.prodComm β α) : (a : β × α) → α × β) (↑f' : Finset (β × α))
have refine_2₂ : (⇑(Equiv.prodComm β α).symm : (a : α × β) → β × α) '' (↑(↑f : Finset (α × β)) : Set (α × β)) ⊆
  (↑(↑f' : Finset (β × α)) : Set (β × α))
Tactic: rwa [← Finset.coe_subset, Finset.coe_image, ← Equiv.symm_image_subset, ← Finset.coe_image,
        Finset.coe_subset]
-- 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_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 (β × α))
⊢ (↑f : Finset (α × β)) ⊆ Finset.image (⇑(Equiv.prodComm β α) : (a : β × α) → α × β) (↑f' : Finset (β × α))
have refine_2₃ : (↑(Finset.image (⇑(Equiv.prodComm β α).symm : (a : α × β) → β × α) (↑f : Finset (α × β))) : Set (β × α)) ⊆
  (↑(↑f' : Finset (β × α)) : Set (β × α))
Tactic: rwa [← Finset.coe_subset, Finset.coe_image, ← Equiv.symm_image_subset, ← Finset.coe_image,
        Finset.coe_subset]
-- 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_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 (β × α))
⊢ (↑f : Finset (α × β)) ⊆ Finset.image (⇑(Equiv.prodComm β α) : (a : β × α) → α × β) (↑f' : Finset (β × α))
have refine_2₄ : Finset.image (⇑(Equiv.prodComm β α).symm : (a : α × β) → β × α) (↑f : Finset (α × β)) ⊆ (↑f' : Finset (β × α))
Tactic: rwa [← Finset.coe_subset, Finset.coe_image, ← Equiv.symm_image_subset, ← Finset.coe_image,
        Finset.coe_subset]
-- Lean 4 proof step from Mathlib.Order.CountableDenseLinearOrder (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
inst_2 : Countable α
inst_3 : DenselyOrdered β
inst_4 : Nontrivial β
⊢ Nonempty (α ↪o β)
have intro : ∀ (val : Encodable α), Nonempty (α ↪o β)
Tactic: cases nonempty_encodable α
-- Lean 4 proof step from Mathlib.Order.CountableDenseLinearOrder (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
inst_2 : Countable α
inst_3 : DenselyOrdered β
inst_4 : Nontrivial β
val : Encodable α
⊢ Nonempty (α ↪o β)
have intro : ∀ (x y : β) (hxy : x < y), Nonempty (α ↪o β)
Tactic: rcases exists_pair_lt β with ⟨x, y, hxy⟩
-- Lean 4 proof step from Mathlib.Order.CountableDenseLinearOrder (goal)
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
⊢ Nonempty (α ↪o β)
have intro : ∀ (a : β) (ha : x < a ∧ a < y), Nonempty (α ↪o β)
Tactic: obtain ⟨a, ha⟩ := exists_between hxy
-- Lean 4 proof step from Mathlib.Order.CountableDenseLinearOrder (hypothesis)
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 (α ↪o β)
have this : Nonempty.{u_2 + 1} (↑(Set.Ioo x y) : Type u_2)
Tactic: haveI : Nonempty (Set.Ioo x y) := ⟨⟨a, ha⟩⟩
-- Lean 4 proof step from Mathlib.Order.CountableDenseLinearOrder (goal)
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 β)
have 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₂)
Tactic: refine
    ⟨RelEmbedding.trans (OrderEmbedding.ofStrictMono (fun a ↦ (F a).val) fun a₁ a₂ ↦ ?_)
        (OrderEmbedding.subtype _)⟩
-- Lean 4 proof step from Mathlib.Order.CountableDenseLinearOrder (goal)
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₂ : α
⊢ 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₂)
have 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₂)
Tactic: rcases (F a₁).prop with ⟨f, hf, ha₁⟩
-- Lean 4 proof step from Mathlib.Order.CountableDenseLinearOrder (goal)
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₂ : α
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₂)
have intro : ∀ (g : PartialIso.{u_1, u_2} α (↑(Set.Ioo x y) : Type u_2)) (hg : g ∈ our_ideal)
  (ha₂ : (a₂, (↑(F a₂) : (↑(Set.Ioo x y) : Type u_2))) ∈ (↑g : 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₂)
Tactic: rcases (F a₂).prop with ⟨g, hg, ha₂⟩
-- Lean 4 proof step from Mathlib.Order.CountableDenseLinearOrder (goal)
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₂ : α
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)))
g : PartialIso.{u_1, u_2} α (↑(Set.Ioo x y) : Type u_2)
hg : g ∈ our_ideal
ha₂ : (a₂, (↑(F a₂) : (↑(Set.Ioo x y) : Type u_2))) ∈ (↑g : 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₂)
have intro : ∀ (m : PartialIso.{u_1, u_2} α (↑(Set.Ioo x y) : Type u_2))
  (_hm : m ∈ (↑our_ideal : Set (PartialIso α (↑(Set.Ioo x y) : Type u_2)))) (fm : f ≤ m) (gm : g ≤ m),
  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 our_ideal.directed _ hf _ hg with ⟨m, _hm, fm, gm⟩
-- Lean 4 proof step from Mathlib.Order.CountableDenseLinearOrder (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
inst_2 : Countable α
inst_3 : DenselyOrdered α
inst_4 : NoMinOrder α
inst_5 : NoMaxOrder α
inst_6 : Nonempty α
inst_7 : Countable β
inst_8 : DenselyOrdered β
inst_9 : NoMinOrder β
inst_10 : NoMaxOrder β
inst_11 : Nonempty β
⊢ Nonempty (α ≃o β)
have intro : ∀ (val : Encodable α), Nonempty (α ≃o β)
Tactic: cases nonempty_encodable α
-- Lean 4 proof step from Mathlib.Order.CountableDenseLinearOrder (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
inst_2 : Countable α
inst_3 : DenselyOrdered α
inst_4 : NoMinOrder α
inst_5 : NoMaxOrder α
inst_6 : Nonempty α
inst_7 : Countable β
inst_8 : DenselyOrdered β
inst_9 : NoMinOrder β
inst_10 : NoMaxOrder β
inst_11 : Nonempty β
val : Encodable α
⊢ Nonempty (α ≃o β)
have intro : ∀ (val : Encodable β), Nonempty (α ≃o β)
Tactic: cases nonempty_encodable β
-- Lean 4 proof step from Mathlib.Order.CountableDenseLinearOrder (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
inst_2 : Countable α
inst_3 : DenselyOrdered α
inst_4 : NoMinOrder α
inst_5 : NoMaxOrder α
inst_6 : Nonempty α
inst_7 : Countable β
inst_8 : DenselyOrdered β
inst_9 : NoMinOrder β
inst_10 : NoMaxOrder β
inst_11 : Nonempty β
val : Encodable α
val_1 : Encodable β
to_cofinal : α ⊕ β → Cofinal (PartialIso α β) :=
  fun (p : α ⊕ β) ↦
    Sum.recOn (motive := fun (x : α ⊕ β) ↦ Cofinal (PartialIso α β)) p (definedAtLeft β) (definedAtRight α)
our_ideal : Ideal (PartialIso α β) := idealOfCofinals default to_cofinal
F : (a : α) → { b : β // ∃ f ∈ our_ideal, (a, b) ∈ (↑f : Finset (α × β)) } := fun (a : α) ↦ funOfIdeal a our_ideal ⋯
G : (b : β) → { a : α // ∃ f ∈ our_ideal, (a, b) ∈ (↑f : Finset (α × β)) } := fun (b : β) ↦ invOfIdeal b our_ideal ⋯
a : α
b : β
⊢ cmp a ((fun (b : β) ↦ (↑(G b) : α)) b) = cmp ((fun (a : α) ↦ (↑(F a) : β)) a) b
have rcases : ∀ (f : PartialIso α β) (hf : f ∈ our_ideal) (ha : (a, (↑(F a) : β)) ∈ (↑f : Finset (α × β))),
  cmp a ((fun (b : β) ↦ (↑(G b) : α)) b) = cmp ((fun (a : α) ↦ (↑(F a) : β)) a) b
Tactic: rcases (F a).prop with ⟨f, hf, ha⟩
-- Lean 4 proof step from Mathlib.Order.CountableDenseLinearOrder (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
inst_2 : Countable α
inst_3 : DenselyOrdered α
inst_4 : NoMinOrder α
inst_5 : NoMaxOrder α
inst_6 : Nonempty α
inst_7 : Countable β
inst_8 : DenselyOrdered β
inst_9 : NoMinOrder β
inst_10 : NoMaxOrder β
inst_11 : Nonempty β
val : Encodable α
val_1 : Encodable β
to_cofinal : α ⊕ β → Cofinal (PartialIso α β) :=
  fun (p : α ⊕ β) ↦
    Sum.recOn (motive := fun (x : α ⊕ β) ↦ Cofinal (PartialIso α β)) p (definedAtLeft β) (definedAtRight α)
our_ideal : Ideal (PartialIso α β) := idealOfCofinals default to_cofinal
F : (a : α) → { b : β // ∃ f ∈ our_ideal, (a, b) ∈ (↑f : Finset (α × β)) } := fun (a : α) ↦ funOfIdeal a our_ideal ⋯
G : (b : β) → { a : α // ∃ f ∈ our_ideal, (a, b) ∈ (↑f : Finset (α × β)) } := fun (b : β) ↦ invOfIdeal b our_ideal ⋯
a : α
b : β
f : PartialIso α β
hf : f ∈ our_ideal
ha : (a, (↑(F a) : β)) ∈ (↑f : Finset (α × β))
⊢ cmp a ((fun (b : β) ↦ (↑(G b) : α)) b) = cmp ((fun (a : α) ↦ (↑(F a) : β)) a) b
have rcases : ∀ (g : PartialIso α β) (hg : g ∈ our_ideal) (hb : ((↑(G b) : α), b) ∈ (↑g : Finset (α × β))),
  cmp a ((fun (b : β) ↦ (↑(G b) : α)) b) = cmp ((fun (a : α) ↦ (↑(F a) : β)) a) b
Tactic: rcases (G b).prop with ⟨g, hg, hb⟩
-- Lean 4 proof step from Mathlib.Order.CountableDenseLinearOrder (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
inst_2 : Countable α
inst_3 : DenselyOrdered α
inst_4 : NoMinOrder α
inst_5 : NoMaxOrder α
inst_6 : Nonempty α
inst_7 : Countable β
inst_8 : DenselyOrdered β
inst_9 : NoMinOrder β
inst_10 : NoMaxOrder β
inst_11 : Nonempty β
val : Encodable α
val_1 : Encodable β
to_cofinal : α ⊕ β → Cofinal (PartialIso α β) :=
  fun (p : α ⊕ β) ↦
    Sum.recOn (motive := fun (x : α ⊕ β) ↦ Cofinal (PartialIso α β)) p (definedAtLeft β) (definedAtRight α)
our_ideal : Ideal (PartialIso α β) := idealOfCofinals default to_cofinal
F : (a : α) → { b : β // ∃ f ∈ our_ideal, (a, b) ∈ (↑f : Finset (α × β)) } := fun (a : α) ↦ funOfIdeal a our_ideal ⋯
G : (b : β) → { a : α // ∃ f ∈ our_ideal, (a, b) ∈ (↑f : Finset (α × β)) } := fun (b : β) ↦ invOfIdeal b our_ideal ⋯
a : α
b : β
f : PartialIso α β
hf : f ∈ our_ideal
ha : (a, (↑(F a) : β)) ∈ (↑f : Finset (α × β))
g : PartialIso α β
hg : g ∈ our_ideal
hb : ((↑(G b) : α), b) ∈ (↑g : Finset (α × β))
⊢ cmp a ((fun (b : β) ↦ (↑(G b) : α)) b) = cmp ((fun (a : α) ↦ (↑(F a) : β)) a) b
have rcases : ∀ m ∈ (↑our_ideal : Set (PartialIso α β)),
  ∀ (fm : f ≤ m) (gm : g ≤ m), cmp a ((fun (b : β) ↦ (↑(G b) : α)) b) = cmp ((fun (a : α) ↦ (↑(F a) : β)) a) b
Tactic: rcases our_ideal.directed _ hf _ hg with ⟨m, _, fm, gm⟩
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : a ≤ b
⊢ ¬a ⩿ b ↔ ∃ (c : α), a < c ∧ c < b
have simp_rw : ¬(a ≤ b ∧ ∀ ⦃c : α⦄, a < c → ¬c < b) ↔ ∃ (c : α), a < c ∧ c < b
Tactic: simp_rw [WCovBy, h, true_and, not_forall, exists_prop, not_not]
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : a ≤ b
simp_rw : ¬(a ≤ b ∧ ∀ ⦃c : α⦄, a < c → ¬c < b) ↔ ∃ (c : α), a < c ∧ c < b
⊢ ¬a ⩿ b ↔ ∃ (c : α), a < c ∧ c < b
have simp_rw₁ : ¬(True ∧ ∀ ⦃c : α⦄, a < c → ¬c < b) ↔ ∃ (c : α), a < c ∧ c < b
Tactic: simp_rw [WCovBy, h, true_and, not_forall, exists_prop, not_not]
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : a ≤ b
simp_rw : ¬(a ≤ b ∧ ∀ ⦃c : α⦄, a < c → ¬c < b) ↔ ∃ (c : α), a < c ∧ c < b
simp_rw₁ : ¬(True ∧ ∀ ⦃c : α⦄, a < c → ¬c < b) ↔ ∃ (c : α), a < c ∧ c < b
⊢ ¬a ⩿ b ↔ ∃ (c : α), a < c ∧ c < b
have simp_rw₂ : (¬∀ ⦃c : α⦄, a < c → ¬c < b) ↔ ∃ (c : α), a < c ∧ c < b
Tactic: simp_rw [WCovBy, h, true_and, not_forall, exists_prop, not_not]
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : a ≤ b
simp_rw : ¬(a ≤ b ∧ ∀ ⦃c : α⦄, a < c → ¬c < b) ↔ ∃ (c : α), a < c ∧ c < b
simp_rw₁ : ¬(True ∧ ∀ ⦃c : α⦄, a < c → ¬c < b) ↔ ∃ (c : α), a < c ∧ c < b
simp_rw₂ : (¬∀ ⦃c : α⦄, a < c → ¬c < b) ↔ ∃ (c : α), a < c ∧ c < b
⊢ ¬a ⩿ b ↔ ∃ (c : α), a < c ∧ c < b
have simp_rw₃ : (∃ (x : α) (_ : a < x), ¬¬x < b) ↔ ∃ (c : α), a < c ∧ c < b
Tactic: simp_rw [WCovBy, h, true_and, not_forall, exists_prop, not_not]
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : a ≤ b
simp_rw : ¬(a ≤ b ∧ ∀ ⦃c : α⦄, a < c → ¬c < b) ↔ ∃ (c : α), a < c ∧ c < b
simp_rw₁ : ¬(True ∧ ∀ ⦃c : α⦄, a < c → ¬c < b) ↔ ∃ (c : α), a < c ∧ c < b
simp_rw₂ : (¬∀ ⦃c : α⦄, a < c → ¬c < b) ↔ ∃ (c : α), a < c ∧ c < b
simp_rw₃ : (∃ (x : α) (_ : a < x), ¬¬x < b) ↔ ∃ (c : α), a < c ∧ c < b
⊢ ¬a ⩿ b ↔ ∃ (c : α), a < c ∧ c < b
have simp_rw₄ : (∃ (x : α), a < x ∧ ¬¬x < b) ↔ ∃ (c : α), a < c ∧ c < b
Tactic: simp_rw [WCovBy, h, true_and, not_forall, exists_prop, not_not]
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
a b : α
f : α ↪o β
hab : a ⩿ b
h : OrdConnected.{u_2} (α := β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
⊢ WCovBy.{u_2} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β)
have refine : ∀ (c : β) (ha : (f : (a : α) → β) a < c) (hb : c < (f : (a : α) → β) b), False
Tactic: refine ⟨f.monotone hab.le, fun c ha hb => ?_⟩
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
a b : α
f : α ↪o β
hab : a ⩿ b
h : OrdConnected.{u_2} (α := β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
c : β
ha : (f : (a : α) → β) a < c
hb : c < (f : (a : α) → β) b
⊢ False
have obtain : ∀ (c : α) (ha : LT.lt.{u_2} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) c : β))
  (hb : LT.lt.{u_2} (α := β) ((f : (a : α) → β) c : β) ((f : (a : α) → β) b : β)), False
Tactic: obtain ⟨c, rfl⟩ := h.out (mem_range_self _) (mem_range_self _) ⟨ha.le, hb.le⟩
Cleared hypotheses: c, ha, hb
-- Lean 4 proof step from Mathlib.Order.Cover (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
a b : α
f : α ↪o β
hab : a ⩿ b
h : OrdConnected.{u_2} (α := β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
c : α
ha : LT.lt.{u_2} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) c : β)
hb : LT.lt.{u_2} (α := β) ((f : (a : α) → β) c : β) ((f : (a : α) → β) b : β)
⊢ False
have ha₁ : a < c
Tactic: rw [f.lt_iff_lt] at ha hb
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.Order.Cover (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
a b : α
f : α ↪o β
hab : a ⩿ b
h : OrdConnected.{u_2} (α := β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
c : α
ha : LT.lt.{u_2} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) c : β)
hb : LT.lt.{u_2} (α := β) ((f : (a : α) → β) c : β) ((f : (a : α) → β) b : β)
ha₁ : a < c
⊢ False
have hb₁ : c < b
Tactic: rw [f.lt_iff_lt] at ha hb
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b c : α
h : a ⩿ b
h2 : a ≤ c
h3 : c ≤ b
⊢ c = a ∨ c = b
have inl : ∀ (h2 : a = c), c = a ∨ c = b
Tactic: rcases h2.eq_or_lt with (h2 | h2)
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b c : α
h : a ⩿ b
h2 : a ≤ c
h3 : c ≤ b
inl : ∀ (h2 : a = c), c = a ∨ c = b
⊢ c = a ∨ c = b
have inr : ∀ (h2 : a < c), c = a ∨ c = b
Tactic: rcases h2.eq_or_lt with (h2 | h2)