awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Monotone.Union (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
x : α
hx_1 : x ∈ s ∪ t
hxc : c ≤ x
hx : x ∈ s
inl : ∀ (hx : c ∈ s ∪ t) (hxc : c ≤ c) (hx : c ∈ s), c ∈ t
⊢ x ∈ t
have inr : ∀ (h'x : c < x), x ∈ t
Tactic: rcases eq_or_lt_of_le hxc with (rfl | h'x)
-- Lean 4 proof step from Mathlib.Order.Monotone.Union (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
⊢ StrictMonoOn f (s ∪ t)
have B : ∀ x ∈ s ∪ t, c ≤ x → x ∈ t
Tactic: have B : ∀ x, x ∈ s ∪ t → c ≤ x → x ∈ t := by
    intro x hx hxc
    match hx with
    | Or.inr hx => exact hx
    | Or.inl hx =>
      rcases eq_or_lt_of_le hxc with (rfl | h'x)
      · exact ht.1
      exact (lt_irrefl _ (h'x.trans_le (hs.2 hx))).elim
-- Lean 4 proof step from Mathlib.Order.Monotone.Union (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
B : ∀ x ∈ s ∪ t, c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x < y
⊢ f x < f y
have inl : ∀ (hxc : x < c), f x < f y
Tactic: rcases lt_or_ge x c with (hxc | hcx)
-- Lean 4 proof step from Mathlib.Order.Monotone.Union (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
B : ∀ x ∈ s ∪ t, c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x < y
inl : ∀ (hxc : x < c), f x < f y
⊢ f x < f y
have inr : ∀ (hcx : c ≤ x), f x < f y
Tactic: rcases lt_or_ge x c with (hxc | hcx)
-- Lean 4 proof step from Mathlib.Order.Monotone.Union (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
B : ∀ x ∈ s ∪ t, c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x < y
hxc : x < c
⊢ f x < f y
have xs : x ∈ s
Tactic: have xs : x ∈ s := A _ hx hxc.le
-- Lean 4 proof step from Mathlib.Order.Monotone.Union (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
B : ∀ x ∈ s ∪ t, c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x < y
hxc : x < c
xs : x ∈ s
⊢ f x < f y
have inl : ∀ (hyc : y < c), f x < f y
Tactic: rcases lt_or_ge y c with (hyc | hcy)
-- Lean 4 proof step from Mathlib.Order.Monotone.Union (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
B : ∀ x ∈ s ∪ t, c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x < y
hxc : x < c
xs : x ∈ s
inl : ∀ (hyc : y < c), f x < f y
⊢ f x < f y
have inl₁ : ∀ (hcy : c ≤ y), f x < f y
Tactic: rcases lt_or_ge y c with (hyc | hcy)
-- Lean 4 proof step from Mathlib.Order.Monotone.Union (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
B : ∀ x ∈ s ∪ t, c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x < y
hcx : c ≤ x
⊢ f x < f y
have xt : x ∈ t
Tactic: have xt : x ∈ t := B _ hx hcx
-- Lean 4 proof step from Mathlib.Order.Monotone.Union (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
B : ∀ x ∈ s ∪ t, c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x < y
hcx : c ≤ x
xt : x ∈ t
⊢ f x < f y
have yt : y ∈ t
Tactic: have yt : y ∈ t := B _ hy (hcx.trans hxy.le)
-- Lean 4 proof step from Mathlib.Order.Monotone.Union (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
a : α
f : α → β
h₁ : StrictMonoOn f (Iic a)
h₂ : StrictMonoOn f (Ici a)
⊢ StrictMono f
have rw : StrictMonoOn f (Iic a ∪ Ici a)
Tactic: rw [← strictMonoOn_univ, ← @Iic_union_Ici _ _ a]
-- Lean 4 proof step from Mathlib.Order.Monotone.Union (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
x : α
hx : x ∈ s ∪ t
hxc : x ≤ c
⊢ x ∈ s
have inl : x ∈ s → x ∈ s
Tactic: cases hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Order.Monotone.Union (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
x : α
hx : x ∈ s ∪ t
hxc : x ≤ c
inl : x ∈ s → x ∈ s
⊢ x ∈ s
have inr : x ∈ t → x ∈ s
Tactic: cases hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Order.Monotone.Union (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
x : α
hxc : x ≤ c
h : x ∈ t
⊢ x ∈ s
have inr : ∀ (hs : IsGreatest s x) (ht : IsLeast t x) (hxc : x ≤ x), x ∈ s
Tactic: rcases eq_or_lt_of_le hxc with (rfl | h'x)
Cleared hypotheses: c, hs, ht, hxc
-- Lean 4 proof step from Mathlib.Order.Monotone.Union (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
x : α
hxc : x ≤ c
h : x ∈ t
inr : ∀ (hs : IsGreatest s x) (ht : IsLeast t x) (hxc : x ≤ x), x ∈ s
⊢ x ∈ s
have inr₁ : ∀ (h'x : x < c), x ∈ s
Tactic: rcases eq_or_lt_of_le hxc with (rfl | h'x)
-- Lean 4 proof step from Mathlib.Order.Monotone.Union (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
⊢ MonotoneOn f (s ∪ t)
have A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
Tactic: have A : ∀ x, x ∈ s ∪ t → x ≤ c → x ∈ s := by
    intro x hx hxc
    cases hx
    · assumption
    rcases eq_or_lt_of_le hxc with (rfl | h'x)
    · exact hs.1
    exact (lt_irrefl _ (h'x.trans_le (ht.2 (by assumption)))).elim
-- Lean 4 proof step from Mathlib.Order.Monotone.Union (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
x : α
hx_1 : x ∈ s ∪ t
hxc : c ≤ x
hx : x ∈ s
⊢ x ∈ t
have inl : ∀ (hx : c ∈ s ∪ t) (hxc : c ≤ c) (hx : c ∈ s), c ∈ t
Tactic: rcases eq_or_lt_of_le hxc with (rfl | h'x)
Cleared hypotheses: x, hx_1, hxc, hx
-- Lean 4 proof step from Mathlib.Order.Monotone.Union (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
x : α
hx_1 : x ∈ s ∪ t
hxc : c ≤ x
hx : x ∈ s
inl : ∀ (hx : c ∈ s ∪ t) (hxc : c ≤ c) (hx : c ∈ s), c ∈ t
⊢ x ∈ t
have inr : ∀ (h'x : c < x), x ∈ t
Tactic: rcases eq_or_lt_of_le hxc with (rfl | h'x)
-- Lean 4 proof step from Mathlib.Order.Monotone.Union (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
⊢ MonotoneOn f (s ∪ t)
have B : ∀ x ∈ s ∪ t, c ≤ x → x ∈ t
Tactic: have B : ∀ x, x ∈ s ∪ t → c ≤ x → x ∈ t := by
    intro x hx hxc
    match hx with
    | Or.inr hx => exact hx
    | Or.inl hx =>
      rcases eq_or_lt_of_le hxc with (rfl | h'x)
      · exact ht.1
      exact (lt_irrefl _ (h'x.trans_le (hs.2 hx))).elim
-- Lean 4 proof step from Mathlib.Order.Monotone.Union (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
B : ∀ x ∈ s ∪ t, c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x ≤ y
⊢ f x ≤ f y
have inl : ∀ (hxc : x < c), f x ≤ f y
Tactic: rcases lt_or_ge x c with (hxc | hcx)
-- Lean 4 proof step from Mathlib.Order.Monotone.Union (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
B : ∀ x ∈ s ∪ t, c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x ≤ y
inl : ∀ (hxc : x < c), f x ≤ f y
⊢ f x ≤ f y
have inr : ∀ (hcx : c ≤ x), f x ≤ f y
Tactic: rcases lt_or_ge x c with (hxc | hcx)
-- Lean 4 proof step from Mathlib.Order.Monotone.Union (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
B : ∀ x ∈ s ∪ t, c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x ≤ y
hxc : x < c
⊢ f x ≤ f y
have xs : x ∈ s
Tactic: have xs : x ∈ s := A _ hx hxc.le
-- Lean 4 proof step from Mathlib.Order.Monotone.Union (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
B : ∀ x ∈ s ∪ t, c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x ≤ y
hxc : x < c
xs : x ∈ s
⊢ f x ≤ f y
have inl : ∀ (hyc : y < c), f x ≤ f y
Tactic: rcases lt_or_ge y c with (hyc | hcy)
-- Lean 4 proof step from Mathlib.Order.Monotone.Union (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
B : ∀ x ∈ s ∪ t, c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x ≤ y
hxc : x < c
xs : x ∈ s
inl : ∀ (hyc : y < c), f x ≤ f y
⊢ f x ≤ f y
have inl₁ : ∀ (hcy : c ≤ y), f x ≤ f y
Tactic: rcases lt_or_ge y c with (hyc | hcy)
-- Lean 4 proof step from Mathlib.Order.Monotone.Union (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
B : ∀ x ∈ s ∪ t, c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x ≤ y
hcx : c ≤ x
⊢ f x ≤ f y
have xt : x ∈ t
Tactic: have xt : x ∈ t := B _ hx hcx
-- Lean 4 proof step from Mathlib.Order.Monotone.Union (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
B : ∀ x ∈ s ∪ t, c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x ≤ y
hcx : c ≤ x
xt : x ∈ t
⊢ f x ≤ f y
have yt : y ∈ t
Tactic: have yt : y ∈ t := B _ hy (hcx.trans hxy)
-- Lean 4 proof step from Mathlib.Order.Monotone.Union (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
a : α
f : α → β
h₁ : MonotoneOn f (Iic a)
h₂ : MonotoneOn f (Ici a)
⊢ Monotone f
have rw : MonotoneOn f (Iic a ∪ Ici a)
Tactic: rw [← monotoneOn_univ, ← @Iic_union_Ici _ _ a]
-- Lean 4 proof step from Mathlib.Order.NonemptyFiniteChains (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : PartialOrder X
inst_1 : PartialOrder Y
s : NonemptyFiniteChains X
f : X →o Y
a : Y
ha : Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) a
b : Y
hb : Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) b
⊢ Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x) a ha ≤
      Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x) b hb ∨
    Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x) b hb ≤
      Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x) a ha
have ha₁ : ∃ a_1 ∈ s.finset, (f : (a : X) → Y) a_1 = a
Tactic: simp only [Finset.mem_image] at ha hb
-- Lean 4 proof step from Mathlib.Order.NonemptyFiniteChains (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : PartialOrder X
inst_1 : PartialOrder Y
s : NonemptyFiniteChains X
f : X →o Y
a : Y
ha : Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) a
b : Y
hb : Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) b
ha₁ : ∃ a_1 ∈ s.finset, (f : (a : X) → Y) a_1 = a
⊢ Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x) a ha ≤
      Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x) b hb ∨
    Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x) b hb ≤
      Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x) a ha
have hb₁ : ∃ a ∈ s.finset, (f : (a : X) → Y) a = b
Tactic: simp only [Finset.mem_image] at ha hb
-- Lean 4 proof step from Mathlib.Order.NonemptyFiniteChains (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : PartialOrder X
inst_1 : PartialOrder Y
s : NonemptyFiniteChains X
f : X →o Y
a : Y
ha_1 : Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) a
b : Y
hb_1 : Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) b
ha : ∃ a_1 ∈ s.finset, (f : (a : X) → Y) a_1 = a
hb : ∃ a ∈ s.finset, (f : (a : X) → Y) a = b
⊢ Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x) a ha_1 ≤
      Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x) b
        hb_1 ∨
    Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x) b hb_1 ≤
      Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x) a ha_1
have obtain : ∀ (a : X) (ha' : a ∈ s.finset)
  (ha :
    Membership.mem.{u_2, u_2} (α := Y) (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset)
      ((f : (a : X) → Y) a : Y)),
  Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x)
        ((f : (a : X) → Y) a) ha ≤
      Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x) b
        hb_1 ∨
    Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x) b hb_1 ≤
      Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x)
        ((f : (a : X) → Y) a) ha
Tactic: obtain ⟨a, ha', rfl⟩ := ha
Cleared hypotheses: a, ha_1, ha
-- Lean 4 proof step from Mathlib.Order.NonemptyFiniteChains (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : PartialOrder X
inst_1 : PartialOrder Y
s : NonemptyFiniteChains X
f : X →o Y
b : Y
hb_1 : Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) b
hb : ∃ a ∈ s.finset, (f : (a : X) → Y) a = b
a : X
ha' : a ∈ s.finset
ha :
  Membership.mem.{u_2, u_2} (α := Y) (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset)
    ((f : (a : X) → Y) a : Y)
⊢ Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x)
        ((f : (a : X) → Y) a) ha ≤
      Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x) b
        hb_1 ∨
    Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x) b hb_1 ≤
      Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x)
        ((f : (a : X) → Y) a) ha
have obtain : ∀ (b : X) (hb' : b ∈ s.finset)
  (hb :
    Membership.mem.{u_2, u_2} (α := Y) (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset)
      ((f : (a : X) → Y) b : Y)),
  LE.le.{u_2} (α := ↥(Finset.image (⇑f : (a : X) → Y) s.finset))
      (Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x)
          ((f : (a : X) → Y) a) ha :
        ↥(Finset.image (⇑f : (a : X) → Y) s.finset))
      (Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x)
          ((f : (a : X) → Y) b) hb :
        ↥(Finset.image (⇑f : (a : X) → Y) s.finset)) ∨
    LE.le.{u_2} (α := ↥(Finset.image (⇑f : (a : X) → Y) s.finset))
      (Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x)
          ((f : (a : X) → Y) b) hb :
        ↥(Finset.image (⇑f : (a : X) → Y) s.finset))
      (Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x)
          ((f : (a : X) → Y) a) ha :
        ↥(Finset.image (⇑f : (a : X) → Y) s.finset))
Tactic: obtain ⟨b, hb', rfl⟩ := hb
Cleared hypotheses: b, hb_1, hb
-- Lean 4 proof step from Mathlib.Order.NonemptyFiniteChains (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : PartialOrder X
inst_1 : PartialOrder Y
s : NonemptyFiniteChains X
f : X →o Y
a : X
ha' : a ∈ s.finset
ha :
  Membership.mem.{u_2, u_2} (α := Y) (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset)
    ((f : (a : X) → Y) a : Y)
b : X
hb' : b ∈ s.finset
hb :
  Membership.mem.{u_2, u_2} (α := Y) (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset)
    ((f : (a : X) → Y) b : Y)
⊢ LE.le.{u_2} (α := ↥(Finset.image (⇑f : (a : X) → Y) s.finset))
      (Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x)
          ((f : (a : X) → Y) a) ha :
        ↥(Finset.image (⇑f : (a : X) → Y) s.finset))
      (Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x)
          ((f : (a : X) → Y) b) hb :
        ↥(Finset.image (⇑f : (a : X) → Y) s.finset)) ∨
    LE.le.{u_2} (α := ↥(Finset.image (⇑f : (a : X) → Y) s.finset))
      (Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x)
          ((f : (a : X) → Y) b) hb :
        ↥(Finset.image (⇑f : (a : X) → Y) s.finset))
      (Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x)
          ((f : (a : X) → Y) a) ha :
        ↥(Finset.image (⇑f : (a : X) → Y) s.finset))
have inl : ∀ (h : Subtype.mk (p := fun (x : X) ↦ x ∈ s.finset) a ha' ≤ Subtype.mk (p := fun (x : X) ↦ x ∈ s.finset) b hb'),
  LE.le.{u_2} (α := ↥(Finset.image (⇑f : (a : X) → Y) s.finset))
      (Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x)
          ((f : (a : X) → Y) a) ha :
        ↥(Finset.image (⇑f : (a : X) → Y) s.finset))
      (Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x)
          ((f : (a : X) → Y) b) hb :
        ↥(Finset.image (⇑f : (a : X) → Y) s.finset)) ∨
    LE.le.{u_2} (α := ↥(Finset.image (⇑f : (a : X) → Y) s.finset))
      (Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x)
          ((f : (a : X) → Y) b) hb :
        ↥(Finset.image (⇑f : (a : X) → Y) s.finset))
      (Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x)
          ((f : (a : X) → Y) a) ha :
        ↥(Finset.image (⇑f : (a : X) → Y) s.finset))
Tactic: obtain h | h := s.comparable ⟨_, ha'⟩ ⟨_, hb'⟩
-- Lean 4 proof step from Mathlib.Order.NonemptyFiniteChains (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : PartialOrder X
inst_1 : PartialOrder Y
f : X →o Y
a b : NonemptyFiniteChains X
h : a ≤ b
x : Y
hx : Membership.mem (γ := Finset Y) (finset ((fun (s : NonemptyFiniteChains X) ↦ s.map f) a)) x
⊢ Membership.mem (γ := Finset Y) (finset ((fun (s : NonemptyFiniteChains X) ↦ s.map f) b)) x
have simp : ∀ (hx : ∃ x_1 ∈ a.finset, (f : (a : X) → Y) x_1 = x), ∃ x_1 ∈ b.finset, (f : (a : X) → Y) x_1 = x
Tactic: simp only [mem_map_iff] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Order.NonemptyFiniteChains (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : PartialOrder X
inst_1 : PartialOrder Y
f : X →o Y
a b : NonemptyFiniteChains X
h : a ≤ b
x : Y
hx : ∃ x_1 ∈ a.finset, (f : (a : X) → Y) x_1 = x
⊢ ∃ x_1 ∈ b.finset, (f : (a : X) → Y) x_1 = x
have obtain : ∀ (x : X) (hx : x ∈ a.finset),
  ∃ x_1 ∈ b.finset, Eq.{u_2 + 1} (α := Y) ((f : (a : X) → Y) x_1 : Y) ((f : (a : X) → Y) x : Y)
Tactic: obtain ⟨x, hx, rfl⟩ := hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Order.Northcott (goal)
Goal:
α : Type u_1
β : Type u_2
h : α → β
inst : LinearOrder β
inst_1 : NoMaxOrder β
⊢ Northcott h ↔ Tendsto h cofinite atTop
have simp_rw : (∀ (b : β), Set.Finite.{u_1} (α := α) {a : α | h a ≤ b}) ↔ ∀ (b : β), Set.Finite.{u_1} (α := α) {x : α | h x < b}
Tactic: simp_rw [northcott_iff, tendsto_atTop, eventually_cofinite, not_le]
-- Lean 4 proof step from Mathlib.Order.Northcott (goal)
Goal:
α : Type u_1
β : Type u_2
h : α → β
inst : LinearOrder β
inst_1 : NoMaxOrder β
⊢ (∀ (b : β), Set.Finite.{u_1} (α := α) {a : α | h a ≤ b}) ↔ ∀ (b : β), Set.Finite.{u_1} (α := α) {x : α | h x < b}
have refine : ∀ (H : ∀ (b : β), Set.Finite.{u_1} (α := α) {x : α | h x < b}) (b : β), Set.Finite.{u_1} (α := α) {a : α | h a ≤ b}
Tactic: refine ⟨fun H b ↦ (H b).subset fun x ↦ le_of_lt, fun H b ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Northcott (goal)
Goal:
α : Type u_1
β : Type u_2
h : α → β
inst : LinearOrder β
inst_1 : NoMaxOrder β
H : ∀ (b : β), Set.Finite.{u_1} (α := α) {x : α | h x < b}
b : β
⊢ Set.Finite.{u_1} (α := α) {a : α | h a ≤ b}
have obtain : ∀ (b' : β) (hc : b < b'), Set.Finite.{u_1} (α := α) {a : α | h a ≤ b}
Tactic: obtain ⟨b', hc⟩ := exists_gt b
-- Lean 4 proof step from Mathlib.Order.Northcott (goal)
Goal:
α : Type u_1
β : Type u_2
h : α → β
inst : LinearOrder β
inst_1 : Northcott h
s : Set α
hs : s.Nonempty
⊢ ∃ a ∈ s, ∀ a' ∈ s, h a ≤ h a'
have obtain : ∀ (a₁ : α) (h₁ : a₁ ∈ s), ∃ a ∈ s, ∀ a' ∈ s, h a ≤ h a'
Tactic: obtain ⟨a₁, h₁⟩ := hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Order.Northcott (goal)
Goal:
α : Type u_1
β : Type u_2
h : α → β
inst : LinearOrder β
inst_1 : Northcott h
s : Set α
a₁ : α
h₁ : a₁ ∈ s
⊢ ∃ a ∈ s, ∀ a' ∈ s, h a ≤ h a'
have obtain : ∀ (a₂ : α) (h₂ : a₂ ∈ {a : α | h a ≤ h a₁} ∩ s) (h₃ : ∀ b ∈ {a : α | h a ≤ h a₁} ∩ s, h a₂ ≤ h b),
  ∃ a ∈ s, ∀ a' ∈ s, h a ≤ h a'
Tactic: obtain ⟨a₂, h₂, h₃⟩ := Set.exists_min_image ({a | h a ≤ h a₁} ∩ s) h
    ((finite_le (h a₁)).inter_of_left s) ⟨a₁, le_rfl, h₁⟩
-- Lean 4 proof step from Mathlib.Order.Northcott (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
h : α → β
h' : β → γ
inst : Preorder β
inst_1 : LE γ
inst_2 : Northcott h
H : ∀ (c : γ), BddAbove (h' ⁻¹' {x : γ | x ≤ c})
c : γ
⊢ Set.Finite.{u_1} (α := α) {a : α | (h' ∘ h) a ≤ c}
have obtain : ∀ (b : β) (hb : ∀ y ∈ h' ⁻¹' {x : γ | x ≤ c}, y ≤ b), Set.Finite.{u_1} (α := α) {a : α | (h' ∘ h) a ≤ c}
Tactic: obtain ⟨b, hb⟩ := bddAbove_def.mp (H c)
-- Lean 4 proof step from Mathlib.Order.Northcott (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
h : α → β
h' : β → γ
inst : LE γ
inst_1 : Northcott h'
H : ∀ (b : β), (h ⁻¹' {b}).Finite
c : γ
⊢ Set.Finite.{u_1} (α := α) {a : α | (h' ∘ h) a ≤ c}
have refine : (h '' {a : α | (h' ∘ h) a ≤ c}).Finite
Tactic: refine Set.Finite.of_finite_fibers h ?_ fun x _ ↦ (H x).inter_of_right _