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 β
nonem : Nonempty β
S : Finset α
f : OrderEmbedding.{u_1, u_2} (↥S) β
a : α
Slt : Finset β := Finset.image (⇑f : (a : ↥S) → β) ({x ∈ S.attach | (↑x : α) < a})
Sgt : Finset β := Finset.image (⇑f : (a : ↥S) → β) ({x ∈ S.attach | a < (↑x : α)})
b : β
hb : ∀ x ∈ Slt, x < b
hb' : ∀ y ∈ Sgt, b < y
refine_1 :
  StrictMono.{u_1, u_2} (β := β) fun (x : ↥(insert a S)) ↦
    if hx : (↑x : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x : α) hx) else b
⊢ ∃ (g : OrderEmbedding.{u_1, u_2} (↥(insert a S)) β),
    Eq (α := (↑(↑S : Set α) : Type u_1) → β)
      (Function.comp (β := ↥(insert a S)) (⇑g : (a : ↥(insert a S)) → β)
        (Set.inclusion (s := (↑S : Set α)) (t := (↑(insert a S) : Set α)) ⋯))
      (⇑f : (a : ↥S) → β)
have refine_2 : Eq (α := (↑(↑S : Set α) : Type u_1) → β)
  (Function.comp (β := ↥(insert a S))
    (⇑(OrderEmbedding.ofStrictMono
            (fun (x : ↥(insert a S)) ↦
              if hx : (↑x : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x : α) hx) else b)
            sorry :
          OrderEmbedding.{u_1, u_2} (↥(insert a S)) β) :
      (a : ↥(insert a S)) → β)
    (Set.inclusion (s := (↑S : Set α)) (t := (↑(insert a S) : Set α)) sorry))
  (⇑f : (a : ↥S) → β)
Tactic: refine ⟨OrderEmbedding.ofStrictMono
    (fun (x : (insert a S : Finset α)) => if hx : x.1 ∈ S then f ⟨x.1, hx⟩ else b) ?_, ?_⟩
-- 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 β
nonem : Nonempty β
S : Finset α
f : OrderEmbedding.{u_1, u_2} (↥S) β
a : α
Slt : Finset β := Finset.image (⇑f : (a : ↥S) → β) ({x ∈ S.attach | (↑x : α) < a})
Sgt : Finset β := Finset.image (⇑f : (a : ↥S) → β) ({x ∈ S.attach | a < (↑x : α)})
b : β
hb : ∀ x ∈ Slt, x < b
hb' : ∀ y ∈ Sgt, b < y
x : α
hx : x ∈ insert a S
y : α
hy : y ∈ insert a S
hxy : Subtype.mk (p := fun (x : α) ↦ x ∈ insert a S) x hx < Subtype.mk (p := fun (x : α) ↦ x ∈ insert a S) y hy
hxS : x ∈ S
hyS : y ∉ S
⊢ LT.lt.{u_2} (α := β)
    ((fun (x : ↥(insert a S)) ↦
        (if hx : (↑x : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x : α) hx) else b : β))
      (Subtype.mk (p := fun (x : α) ↦ x ∈ insert a S) x hx))
    ((fun (x : ↥(insert a S)) ↦
        (if hx : (↑x : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x : α) hx) else b : β))
      (Subtype.mk (p := fun (x : α) ↦ x ∈ insert a S) y hy))
have obtain : let Slt : Finset β := Finset.image (⇑f : (a : ↥S) → β) ({x ∈ S.attach | (↑x : α) < y});
let Sgt : Finset β := Finset.image (⇑f : (a : ↥S) → β) ({x ∈ S.attach | y < (↑x : α)});
∀ (hb : ∀ x ∈ Slt, x < b) (hb' : ∀ y ∈ Sgt, b < y) (hx : x ∈ insert y S) (hy : y ∈ insert y S)
  (hxy : Subtype.mk (p := fun (x : α) ↦ x ∈ insert y S) x hx < Subtype.mk (p := fun (x : α) ↦ x ∈ insert y S) y hy),
  LT.lt.{u_2} (α := β)
    ((fun (x : ↥(insert y S)) ↦
        (if hx : (↑x : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x : α) hx) else b : β))
      (Subtype.mk (p := fun (x : α) ↦ x ∈ insert y S) x hx))
    ((fun (x : ↥(insert y S)) ↦
        (if hx : (↑x : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x : α) hx) else b : β))
      (Subtype.mk (p := fun (x : α) ↦ x ∈ insert y S) y hy))
Tactic: obtain rfl := Finset.eq_of_mem_insert_of_notMem hy hyS
Cleared hypotheses: a, Slt, Sgt, hb, hb', hx, hy, hxy
-- 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 β
nonem : Nonempty β
S : Finset α
f : OrderEmbedding.{u_1, u_2} (↥S) β
b : β
x y : α
hxS : x ∈ S
hyS : y ∉ S
Slt : Finset β := Finset.image (⇑f : (a : ↥S) → β) ({x ∈ S.attach | (↑x : α) < y})
Sgt : Finset β := Finset.image (⇑f : (a : ↥S) → β) ({x ∈ S.attach | y < (↑x : α)})
hb : ∀ x ∈ Slt, x < b
hb' : ∀ y ∈ Sgt, b < y
hx : x ∈ insert y S
hy : y ∈ insert y S
hxy : Subtype.mk (p := fun (x : α) ↦ x ∈ insert y S) x hx < Subtype.mk (p := fun (x : α) ↦ x ∈ insert y S) y hy
⊢ LT.lt.{u_2} (α := β)
    ((fun (x : ↥(insert y S)) ↦
        (if hx : (↑x : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x : α) hx) else b : β))
      (Subtype.mk (p := fun (x : α) ↦ x ∈ insert y S) x hx))
    ((fun (x : ↥(insert y S)) ↦
        (if hx : (↑x : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x : α) hx) else b : β))
      (Subtype.mk (p := fun (x : α) ↦ x ∈ insert y S) y hy))
have simp : (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) x sorry) < b
Tactic: simp only [hxS, hyS, ↓reduceDIte]
-- 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 β
nonem : Nonempty β
S : Finset α
f : OrderEmbedding.{u_1, u_2} (↥S) β
a : α
Slt : Finset β := Finset.image (⇑f : (a : ↥S) → β) ({x ∈ S.attach | (↑x : α) < a})
Sgt : Finset β := Finset.image (⇑f : (a : ↥S) → β) ({x ∈ S.attach | a < (↑x : α)})
b : β
hb : ∀ x ∈ Slt, x < b
hb' : ∀ y ∈ Sgt, b < y
x : α
hx : x ∈ insert a S
y : α
hy : y ∈ insert a S
hxy : Subtype.mk (p := fun (x : α) ↦ x ∈ insert a S) x hx < Subtype.mk (p := fun (x : α) ↦ x ∈ insert a S) y hy
hxS : x ∈ S
⊢ LT.lt.{u_2} (α := β)
    ((fun (x : ↥(insert a S)) ↦
        (if hx : (↑x : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x : α) hx) else b : β))
      (Subtype.mk (p := fun (x : α) ↦ x ∈ insert a S) x hx))
    ((fun (x : ↥(insert a S)) ↦
        (if hx : (↑x : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x : α) hx) else b : β))
      (Subtype.mk (p := fun (x : α) ↦ x ∈ insert a S) y hy))
have if : ∀ (hyS : y ∈ S),
  LT.lt.{u_2} (α := β)
    ((fun (x : ↥(insert a S)) ↦
        (if hx : (↑x : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x : α) hx) else b : β))
      (Subtype.mk (p := fun (x : α) ↦ x ∈ insert a S) x hx))
    ((fun (x : ↥(insert a S)) ↦
        (if hx : (↑x : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x : α) hx) else b : β))
      (Subtype.mk (p := fun (x : α) ↦ x ∈ insert a S) y hy))
Tactic: if hyS : y ∈ S
      then simpa only [hxS, hyS, ↓reduceDIte, OrderEmbedding.lt_iff_lt, Subtype.mk_lt_mk]
      else
        obtain rfl := Finset.eq_of_mem_insert_of_notMem hy hyS
        simp only [hxS, hyS, ↓reduceDIte]
        exact hb _ (Finset.mem_image_of_mem _ (Finset.mem_filter.2 ⟨Finset.mem_attach _ _, hxy⟩))
-- 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 β
nonem : Nonempty β
S : Finset α
f : OrderEmbedding.{u_1, u_2} (↥S) β
a : α
Slt : Finset β := Finset.image (⇑f : (a : ↥S) → β) ({x ∈ S.attach | (↑x : α) < a})
Sgt : Finset β := Finset.image (⇑f : (a : ↥S) → β) ({x ∈ S.attach | a < (↑x : α)})
b : β
hb : ∀ x ∈ Slt, x < b
hb' : ∀ y ∈ Sgt, b < y
x : α
hx : x ∈ insert a S
y : α
hy : y ∈ insert a S
hxy : Subtype.mk (p := fun (x : α) ↦ x ∈ insert a S) x hx < Subtype.mk (p := fun (x : α) ↦ x ∈ insert a S) y hy
hxS : x ∈ S
if :
  ∀ (hyS : y ∈ S),
    LT.lt.{u_2} (α := β)
      ((fun (x : ↥(insert a S)) ↦
          (if hx : (↑x : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x : α) hx) else b : β))
        (Subtype.mk (p := fun (x : α) ↦ x ∈ insert a S) x hx))
      ((fun (x : ↥(insert a S)) ↦
          (if hx : (↑x : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x : α) hx) else b : β))
        (Subtype.mk (p := fun (x : α) ↦ x ∈ insert a S) y hy))
⊢ LT.lt.{u_2} (α := β)
    ((fun (x : ↥(insert a S)) ↦
        (if hx : (↑x : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x : α) hx) else b : β))
      (Subtype.mk (p := fun (x : α) ↦ x ∈ insert a S) x hx))
    ((fun (x : ↥(insert a S)) ↦
        (if hx : (↑x : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x : α) hx) else b : β))
      (Subtype.mk (p := fun (x : α) ↦ x ∈ insert a S) y hy))
have if₁ : ∀ (hyS : y ∉ S),
  LT.lt.{u_2} (α := β)
    ((fun (x : ↥(insert a S)) ↦
        (if hx : (↑x : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x : α) hx) else b : β))
      (Subtype.mk (p := fun (x : α) ↦ x ∈ insert a S) x hx))
    ((fun (x : ↥(insert a S)) ↦
        (if hx : (↑x : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x : α) hx) else b : β))
      (Subtype.mk (p := fun (x : α) ↦ x ∈ insert a S) y hy))
Tactic: if hyS : y ∈ S
      then simpa only [hxS, hyS, ↓reduceDIte, OrderEmbedding.lt_iff_lt, Subtype.mk_lt_mk]
      else
        obtain rfl := Finset.eq_of_mem_insert_of_notMem hy hyS
        simp only [hxS, hyS, ↓reduceDIte]
        exact hb _ (Finset.mem_image_of_mem _ (Finset.mem_filter.2 ⟨Finset.mem_attach _ _, hxy⟩))
-- 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 β
nonem : Nonempty β
S : Finset α
f : OrderEmbedding.{u_1, u_2} (↥S) β
a : α
Slt : Finset β := Finset.image (⇑f : (a : ↥S) → β) ({x ∈ S.attach | (↑x : α) < a})
Sgt : Finset β := Finset.image (⇑f : (a : ↥S) → β) ({x ∈ S.attach | a < (↑x : α)})
b : β
hb : ∀ x ∈ Slt, x < b
hb' : ∀ y ∈ Sgt, b < y
x : α
hx : x ∈ insert a S
y : α
hy : y ∈ insert a S
hxy : Subtype.mk (p := fun (x : α) ↦ x ∈ insert a S) x hx < Subtype.mk (p := fun (x : α) ↦ x ∈ insert a S) y hy
hxS : x ∉ S
⊢ LT.lt.{u_2} (α := β)
    ((fun (x : ↥(insert a S)) ↦
        (if hx : (↑x : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x : α) hx) else b : β))
      (Subtype.mk (p := fun (x : α) ↦ x ∈ insert a S) x hx))
    ((fun (x : ↥(insert a S)) ↦
        (if hx : (↑x : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x : α) hx) else b : β))
      (Subtype.mk (p := fun (x : α) ↦ x ∈ insert a S) y hy))
have obtain : let Slt : Finset β := Finset.image (⇑f : (a : ↥S) → β) ({x_1 ∈ S.attach | (↑x_1 : α) < x});
let Sgt : Finset β := Finset.image (⇑f : (a : ↥S) → β) ({x_1 ∈ S.attach | x < (↑x_1 : α)});
∀ (hb : ∀ x ∈ Slt, x < b) (hb' : ∀ y ∈ Sgt, b < y) (hx : x ∈ insert x S) (hy : y ∈ insert x S)
  (hxy :
    Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ insert x S) x hx < Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ insert x S) y hy),
  LT.lt.{u_2} (α := β)
    ((fun (x_1 : ↥(insert x S)) ↦
        (if hx : (↑x_1 : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x_1 : α) hx) else b :
          β))
      (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ insert x S) x hx))
    ((fun (x_1 : ↥(insert x S)) ↦
        (if hx : (↑x_1 : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x_1 : α) hx) else b :
          β))
      (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ insert x S) y hy))
Tactic: obtain rfl := Finset.eq_of_mem_insert_of_notMem hx hxS
Cleared hypotheses: a, Slt, Sgt, hb, hb', hx, hy, hxy
-- 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 β
nonem : Nonempty β
S : Finset α
f : OrderEmbedding.{u_1, u_2} (↥S) β
b : β
x y : α
hxS : x ∉ S
Slt : Finset β := Finset.image (⇑f : (a : ↥S) → β) ({x_1 ∈ S.attach | (↑x_1 : α) < x})
Sgt : Finset β := Finset.image (⇑f : (a : ↥S) → β) ({x_1 ∈ S.attach | x < (↑x_1 : α)})
hb : ∀ x ∈ Slt, x < b
hb' : ∀ y ∈ Sgt, b < y
hx : x ∈ insert x S
hy : y ∈ insert x S
hxy : Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ insert x S) x hx < Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ insert x S) y hy
hyS : y ∈ S
⊢ LT.lt.{u_2} (α := β)
    ((fun (x_1 : ↥(insert x S)) ↦
        (if hx : (↑x_1 : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x_1 : α) hx) else b :
          β))
      (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ insert x S) x hx))
    ((fun (x_1 : ↥(insert x S)) ↦
        (if hx : (↑x_1 : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x_1 : α) hx) else b :
          β))
      (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ insert x S) y hy))
have simp : b < (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) y sorry)
Tactic: simp only [hxS, hyS, ↓reduceDIte]
-- 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 β
nonem : Nonempty β
S : Finset α
f : OrderEmbedding.{u_1, u_2} (↥S) β
b : β
x y : α
hxS : x ∉ S
Slt : Finset β := Finset.image (⇑f : (a : ↥S) → β) ({x_1 ∈ S.attach | (↑x_1 : α) < x})
Sgt : Finset β := Finset.image (⇑f : (a : ↥S) → β) ({x_1 ∈ S.attach | x < (↑x_1 : α)})
hb : ∀ x ∈ Slt, x < b
hb' : ∀ y ∈ Sgt, b < y
hx : x ∈ insert x S
hy : y ∈ insert x S
hxy : Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ insert x S) x hx < Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ insert x S) y hy
⊢ LT.lt.{u_2} (α := β)
    ((fun (x_1 : ↥(insert x S)) ↦
        (if hx : (↑x_1 : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x_1 : α) hx) else b :
          β))
      (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ insert x S) x hx))
    ((fun (x_1 : ↥(insert x S)) ↦
        (if hx : (↑x_1 : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x_1 : α) hx) else b :
          β))
      (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ insert x S) y hy))
have if : ∀ (hyS : y ∈ S),
  LT.lt.{u_2} (α := β)
    ((fun (x_1 : ↥(insert x S)) ↦
        (if hx : (↑x_1 : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x_1 : α) hx) else b :
          β))
      (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ insert x S) x hx))
    ((fun (x_1 : ↥(insert x S)) ↦
        (if hx : (↑x_1 : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x_1 : α) hx) else b :
          β))
      (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ insert x S) y hy))
Tactic: if hyS : y ∈ S
      then
        simp only [hxS, hyS, ↓reduceDIte]
        exact hb' _ (Finset.mem_image_of_mem _ (Finset.mem_filter.2 ⟨Finset.mem_attach _ _, hxy⟩))
      else simp only [Finset.eq_of_mem_insert_of_notMem hy hyS, lt_self_iff_false] at hxy
-- 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 β
nonem : Nonempty β
S : Finset α
f : OrderEmbedding.{u_1, u_2} (↥S) β
b : β
x y : α
hxS : x ∉ S
Slt : Finset β := Finset.image (⇑f : (a : ↥S) → β) ({x_1 ∈ S.attach | (↑x_1 : α) < x})
Sgt : Finset β := Finset.image (⇑f : (a : ↥S) → β) ({x_1 ∈ S.attach | x < (↑x_1 : α)})
hb : ∀ x ∈ Slt, x < b
hb' : ∀ y ∈ Sgt, b < y
hx : x ∈ insert x S
hy : y ∈ insert x S
hxy : Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ insert x S) x hx < Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ insert x S) y hy
if :
  ∀ (hyS : y ∈ S),
    LT.lt.{u_2} (α := β)
      ((fun (x_1 : ↥(insert x S)) ↦
          (if hx : (↑x_1 : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x_1 : α) hx) else b :
            β))
        (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ insert x S) x hx))
      ((fun (x_1 : ↥(insert x S)) ↦
          (if hx : (↑x_1 : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x_1 : α) hx) else b :
            β))
        (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ insert x S) y hy))
⊢ LT.lt.{u_2} (α := β)
    ((fun (x_1 : ↥(insert x S)) ↦
        (if hx : (↑x_1 : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x_1 : α) hx) else b :
          β))
      (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ insert x S) x hx))
    ((fun (x_1 : ↥(insert x S)) ↦
        (if hx : (↑x_1 : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x_1 : α) hx) else b :
          β))
      (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ insert x S) y hy))
have if₁ : ∀ (hyS : y ∉ S),
  LT.lt.{u_2} (α := β)
    ((fun (x_1 : ↥(insert x S)) ↦
        (if hx : (↑x_1 : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x_1 : α) hx) else b :
          β))
      (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ insert x S) x hx))
    ((fun (x_1 : ↥(insert x S)) ↦
        (if hx : (↑x_1 : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x_1 : α) hx) else b :
          β))
      (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ insert x S) y hy))
Tactic: if hyS : y ∈ S
      then
        simp only [hxS, hyS, ↓reduceDIte]
        exact hb' _ (Finset.mem_image_of_mem _ (Finset.mem_filter.2 ⟨Finset.mem_attach _ _, hxy⟩))
      else simp only [Finset.eq_of_mem_insert_of_notMem hy hyS, lt_self_iff_false] at hxy
-- 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 β
nonem : Nonempty β
S : Finset α
f : OrderEmbedding.{u_1, u_2} (↥S) β
a : α
Slt : Finset β := Finset.image (⇑f : (a : ↥S) → β) ({x ∈ S.attach | (↑x : α) < a})
Sgt : Finset β := Finset.image (⇑f : (a : ↥S) → β) ({x ∈ S.attach | a < (↑x : α)})
b : β
hb : ∀ x ∈ Slt, x < b
hb' : ∀ y ∈ Sgt, b < y
x : α
hx : x ∈ insert a S
y : α
hy : y ∈ insert a S
hxy : Subtype.mk (p := fun (x : α) ↦ x ∈ insert a S) x hx < Subtype.mk (p := fun (x : α) ↦ x ∈ insert a S) y hy
⊢ LT.lt.{u_2} (α := β)
    ((fun (x : ↥(insert a S)) ↦
        (if hx : (↑x : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x : α) hx) else b : β))
      (Subtype.mk (p := fun (x : α) ↦ x ∈ insert a S) x hx))
    ((fun (x : ↥(insert a S)) ↦
        (if hx : (↑x : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x : α) hx) else b : β))
      (Subtype.mk (p := fun (x : α) ↦ x ∈ insert a S) y hy))
have if : ∀ (hxS : x ∈ S),
  LT.lt.{u_2} (α := β)
    ((fun (x : ↥(insert a S)) ↦
        (if hx : (↑x : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x : α) hx) else b : β))
      (Subtype.mk (p := fun (x : α) ↦ x ∈ insert a S) x hx))
    ((fun (x : ↥(insert a S)) ↦
        (if hx : (↑x : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x : α) hx) else b : β))
      (Subtype.mk (p := fun (x : α) ↦ x ∈ insert a S) y hy))
Tactic: if hxS : x ∈ S
    then if hyS : y ∈ S
      then simpa only [hxS, hyS, ↓reduceDIte, OrderEmbedding.lt_iff_lt, Subtype.mk_lt_mk]
      else
        obtain rfl := Finset.eq_of_mem_insert_of_notMem hy hyS
        simp only [hxS, hyS, ↓reduceDIte]
        exact hb _ (Finset.mem_image_of_mem _ (Finset.mem_filter.2 ⟨Finset.mem_attach _ _, hxy⟩))
    else
      obtain rfl := Finset.eq_of_mem_insert_of_notMem hx hxS
      if hyS : y ∈ S
      then
        simp only [hxS, hyS, ↓reduceDIte]
        exact hb' _ (Finset.mem_image_of_mem _ (Finset.mem_filter.2 ⟨Finset.mem_attach _ _, hxy⟩))
      else simp only [Finset.eq_of_mem_insert_of_notMem hy hyS, lt_self_iff_false] at hxy
-- 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 β
nonem : Nonempty β
S : Finset α
f : OrderEmbedding.{u_1, u_2} (↥S) β
a : α
Slt : Finset β := Finset.image (⇑f : (a : ↥S) → β) ({x ∈ S.attach | (↑x : α) < a})
Sgt : Finset β := Finset.image (⇑f : (a : ↥S) → β) ({x ∈ S.attach | a < (↑x : α)})
b : β
hb : ∀ x ∈ Slt, x < b
hb' : ∀ y ∈ Sgt, b < y
x : α
hx : x ∈ insert a S
y : α
hy : y ∈ insert a S
hxy : Subtype.mk (p := fun (x : α) ↦ x ∈ insert a S) x hx < Subtype.mk (p := fun (x : α) ↦ x ∈ insert a S) y hy
if :
  ∀ (hxS : x ∈ S),
    LT.lt.{u_2} (α := β)
      ((fun (x : ↥(insert a S)) ↦
          (if hx : (↑x : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x : α) hx) else b : β))
        (Subtype.mk (p := fun (x : α) ↦ x ∈ insert a S) x hx))
      ((fun (x : ↥(insert a S)) ↦
          (if hx : (↑x : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x : α) hx) else b : β))
        (Subtype.mk (p := fun (x : α) ↦ x ∈ insert a S) y hy))
⊢ LT.lt.{u_2} (α := β)
    ((fun (x : ↥(insert a S)) ↦
        (if hx : (↑x : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x : α) hx) else b : β))
      (Subtype.mk (p := fun (x : α) ↦ x ∈ insert a S) x hx))
    ((fun (x : ↥(insert a S)) ↦
        (if hx : (↑x : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x : α) hx) else b : β))
      (Subtype.mk (p := fun (x : α) ↦ x ∈ insert a S) y hy))
have if₁ : ∀ (hxS : x ∉ S),
  LT.lt.{u_2} (α := β)
    ((fun (x : ↥(insert a S)) ↦
        (if hx : (↑x : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x : α) hx) else b : β))
      (Subtype.mk (p := fun (x : α) ↦ x ∈ insert a S) x hx))
    ((fun (x : ↥(insert a S)) ↦
        (if hx : (↑x : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x : α) hx) else b : β))
      (Subtype.mk (p := fun (x : α) ↦ x ∈ insert a S) y hy))
Tactic: if hxS : x ∈ S
    then if hyS : y ∈ S
      then simpa only [hxS, hyS, ↓reduceDIte, OrderEmbedding.lt_iff_lt, Subtype.mk_lt_mk]
      else
        obtain rfl := Finset.eq_of_mem_insert_of_notMem hy hyS
        simp only [hxS, hyS, ↓reduceDIte]
        exact hb _ (Finset.mem_image_of_mem _ (Finset.mem_filter.2 ⟨Finset.mem_attach _ _, hxy⟩))
    else
      obtain rfl := Finset.eq_of_mem_insert_of_notMem hx hxS
      if hyS : y ∈ S
      then
        simp only [hxS, hyS, ↓reduceDIte]
        exact hb' _ (Finset.mem_image_of_mem _ (Finset.mem_filter.2 ⟨Finset.mem_attach _ _, hxy⟩))
      else simp only [Finset.eq_of_mem_insert_of_notMem hy hyS, lt_self_iff_false] at hxy
-- 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 β
nonem : Nonempty β
S : Finset α
f : OrderEmbedding.{u_1, u_2} (↥S) β
a : α
Slt : Finset β := Finset.image (⇑f : (a : ↥S) → β) ({x ∈ S.attach | (↑x : α) < a})
Sgt : Finset β := Finset.image (⇑f : (a : ↥S) → β) ({x ∈ S.attach | a < (↑x : α)})
b : β
hb : ∀ x ∈ Slt, x < b
hb' : ∀ y ∈ Sgt, b < y
⊢ Eq (α := (↑(↑S : Set α) : Type u_1) → β)
    (Function.comp (β := ↥(insert a S))
      (⇑(OrderEmbedding.ofStrictMono
              (fun (x : ↥(insert a S)) ↦
                if hx : (↑x : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x : α) hx) else b)
              ⋯ :
            OrderEmbedding.{u_1, u_2} (↥(insert a S)) β) :
        (a : ↥(insert a S)) → β)
      (Set.inclusion (s := (↑S : Set α)) (t := (↑(insert a S) : Set α)) ⋯))
    (⇑f : (a : ↥S) → β)
have refine_2 : ∀ (x : (↑(↑S : Set α) : Type u_1)),
  Eq.{u_2 + 1} (α := β)
    (Function.comp (β := ↥(insert a S))
        (⇑(OrderEmbedding.ofStrictMono
                (fun (x : ↥(insert a S)) ↦
                  if hx : (↑x : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x : α) hx)
                  else b)
                sorry :
              OrderEmbedding.{u_1, u_2} (↥(insert a S)) β) :
          (a : ↥(insert a S)) → β)
        (Set.inclusion (s := (↑S : Set α)) (t := (↑(insert a S) : Set α)) sorry) x :
      β)
    ((f : (a : ↥S) → β) x : β)
Tactic: ext x
-- 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 : α
⊢ ∃ (b : β), ∀ p ∈ (↑f : Finset (α × β)), cmp p.1 a = cmp p.2 b
have pos : ∀ (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