awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Monotone.Union
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
⊢ x ∈ s

Tactic:
have xs : x ∈ s := A _ hx hxc.le
-- Module: Mathlib.Order.Monotone.Union
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
inl₁ : ∀ (hcy : c ≤ y), f x < f y
⊢ f x < f y

Tactic:
rcases lt_or_ge y c with (hyc | hcy)

Premises used: lt_or_ge
-- Module: Mathlib.Order.Monotone.Union
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
hyc : y < c
⊢ f x < f y

Tactic:
h₁ xs (A _ hy hyc.le) hxy

Premises used: LT.lt.le
-- Module: Mathlib.Order.Monotone.Union
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
hyc : y < c
⊢ f x < f y

Tactic:
exact h₁ xs (A _ hy hyc.le) hxy

Premises used: LT.lt.le
-- Module: Mathlib.Order.Monotone.Union
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
hcy : c ≤ y
⊢ f x < f y

Tactic:
(h₁ xs hs.1 hxc).trans_le (h₂.monotoneOn ht.1 (B _ hy hcy) hcy)

Premises used: And.left, LT.lt.trans_le, StrictMonoOn.monotoneOn
-- Module: Mathlib.Order.Monotone.Union
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
hcy : c ≤ y
⊢ f x < f y

Tactic:
exact (h₁ xs hs.1 hxc).trans_le (h₂.monotoneOn ht.1 (B _ hy hcy) hcy)

Premises used: And.left, LT.lt.trans_le, StrictMonoOn.monotoneOn
-- Module: Mathlib.Order.Monotone.Union
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
⊢ x ∈ t

Tactic:
have xt : x ∈ t := B _ hx hcx
-- Module: Mathlib.Order.Monotone.Union
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
⊢ y ∈ t

Tactic:
have yt : y ∈ t := B _ hy (hcx.trans hxy.le)
-- Module: Mathlib.Order.Monotone.Union
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
yt : y ∈ t
⊢ f x < f y

Tactic:
h₂ xt yt hxy
-- Module: Mathlib.Order.Monotone.Union
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
yt : y ∈ t
⊢ f x < f y

Tactic:
exact h₂ xt yt hxy
-- Module: Mathlib.Order.Monotone.Union
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
a : α
f : α → β
h₁ : StrictMonoOn f (Iic a)
h₂ : StrictMonoOn f (Ici a)
rw : StrictMonoOn f (Iic a ∪ Ici a)
⊢ StrictMono f

Tactic:
rw [← strictMonoOn_univ, ← @Iic_union_Ici _ _ a]

Premises used: strictMonoOn_univ, Set.Iic_union_Ici
-- Module: Mathlib.Order.Monotone.Union
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
a : α
f : α → β
h₁ : StrictMonoOn f (Iic a)
h₂ : StrictMonoOn f (Ici a)
⊢ StrictMonoOn f (Iic a ∪ Ici a)

Tactic:
StrictMonoOn.union h₁ h₂ isGreatest_Iic isLeast_Ici

Premises used: StrictMonoOn.union, isLeast_Ici, isGreatest_Iic
-- Module: Mathlib.Order.Monotone.Union
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
a : α
f : α → β
h₁ : StrictMonoOn f (Iic a)
h₂ : StrictMonoOn f (Ici a)
⊢ StrictMonoOn f (Iic a ∪ Ici a)

Tactic:
exact StrictMonoOn.union h₁ h₂ isGreatest_Iic isLeast_Ici

Premises used: StrictMonoOn.union, isLeast_Ici, isGreatest_Iic
-- Module: Mathlib.Order.Monotone.Union
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s t : Set α
c : α
h₁ : StrictAntiOn f s
h₂ : StrictAntiOn f t
hs : IsGreatest s c
ht : IsLeast t c
⊢ StrictAntiOn f (s ∪ t)

Tactic:
(h₁.dual_right.union h₂.dual_right hs ht).dual_right

Premises used: StrictMonoOn.union, OrderDual, StrictMonoOn.dual_right, StrictAntiOn.dual_right
-- Module: Mathlib.Order.Monotone.Union
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
a : α
f : α → β
h₁ : StrictAntiOn f (Iic a)
h₂ : StrictAntiOn f (Ici a)
⊢ StrictAnti f

Tactic:
(h₁.dual_right.Iic_union_Ici h₂.dual_right).dual_right

Premises used: StrictMono.dual_right, StrictMonoOn.Iic_union_Ici, OrderDual, StrictAntiOn.dual_right
-- Module: Mathlib.Order.Monotone.Union
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
inr : x ∈ t → x ∈ s
⊢ x ∈ s

Tactic:
cases hx
-- Module: Mathlib.Order.Monotone.Union
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 ∈ s
⊢ x ∈ s

Tactic:
assumption
-- Module: Mathlib.Order.Monotone.Union
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
inr₁ : ∀ (h'x : x < c), x ∈ s
⊢ x ∈ s

Tactic:
rcases eq_or_lt_of_le hxc with (rfl | h'x)

Premises used: eq_or_lt_of_le, rfl
-- Module: Mathlib.Order.Monotone.Union
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s t : Set α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
x : α
h : x ∈ t
hs : IsGreatest s x
ht : IsLeast t x
hxc : x ≤ x
⊢ x ∈ s

Tactic:
hs.1

Premises used: And.left
-- Module: Mathlib.Order.Monotone.Union
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s t : Set α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
x : α
h : x ∈ t
hs : IsGreatest s x
ht : IsLeast t x
hxc : x ≤ x
⊢ x ∈ s

Tactic:
exact hs.1

Premises used: And.left
-- Module: Mathlib.Order.Monotone.Union
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
h'x : x < c
⊢ x ∈ t

Tactic:
assumption
-- Module: Mathlib.Order.Monotone.Union
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
h'x : x < c
⊢ x ∈ s

Tactic:
exact (lt_irrefl _ (h'x.trans_le (ht.2 (by assumption)))).elim

Premises used: lt_irrefl, False.elim, And.right, LT.lt.trans_le
-- Module: Mathlib.Order.Monotone.Union
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 ∈ 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
-- Module: Mathlib.Order.Monotone.Union
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 ∈ t
⊢ x ∈ t

Tactic:
hx
-- Module: Mathlib.Order.Monotone.Union
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 ∈ t
⊢ x ∈ t

Tactic:
exact hx
-- Module: Mathlib.Order.Monotone.Union
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
inr : ∀ (h'x : c < x), x ∈ t
⊢ x ∈ t

Tactic:
rcases eq_or_lt_of_le hxc with (rfl | h'x)

Premises used: eq_or_lt_of_le, rfl
-- Module: Mathlib.Order.Monotone.Union
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
hx_1 : c ∈ s ∪ t
hxc : c ≤ c
hx : c ∈ s
⊢ c ∈ t

Tactic:
ht.1

Premises used: And.left
-- Module: Mathlib.Order.Monotone.Union
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
hx_1 : c ∈ s ∪ t
hxc : c ≤ c
hx : c ∈ s
⊢ c ∈ t

Tactic:
exact ht.1

Premises used: And.left
-- Module: Mathlib.Order.Monotone.Union
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
h'x : c < x
⊢ x ∈ t

Tactic:
(lt_irrefl _ (h'x.trans_le (hs.2 hx))).elim

Premises used: lt_irrefl, False.elim, And.right, LT.lt.trans_le
-- Module: Mathlib.Order.Monotone.Union
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
h'x : c < x
⊢ x ∈ t

Tactic:
exact (lt_irrefl _ (h'x.trans_le (hs.2 hx))).elim

Premises used: lt_irrefl, False.elim, And.right, LT.lt.trans_le
-- Module: Mathlib.Order.Monotone.Union
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 : x ∈ s ∪ t
hxc : c ≤ x
⊢ x ∈ t

Tactic:
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
-- Module: Mathlib.Order.Monotone.Union
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 ∈ 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
-- Module: Mathlib.Order.Monotone.Union
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
inr : ∀ (hcx : c ≤ x), f x ≤ f y
⊢ f x ≤ f y

Tactic:
rcases lt_or_ge x c with (hxc | hcx)

Premises used: lt_or_ge
-- Module: Mathlib.Order.Monotone.Union
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
⊢ x ∈ s

Tactic:
have xs : x ∈ s := A _ hx hxc.le
-- Module: Mathlib.Order.Monotone.Union
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
inl₁ : ∀ (hcy : c ≤ y), f x ≤ f y
⊢ f x ≤ f y

Tactic:
rcases lt_or_ge y c with (hyc | hcy)

Premises used: lt_or_ge
-- Module: Mathlib.Order.Monotone.Union
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
hyc : y < c
⊢ f x ≤ f y

Tactic:
h₁ xs (A _ hy hyc.le) hxy

Premises used: LT.lt.le
-- Module: Mathlib.Order.Monotone.Union
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
hyc : y < c
⊢ f x ≤ f y

Tactic:
exact h₁ xs (A _ hy hyc.le) hxy

Premises used: LT.lt.le
-- Module: Mathlib.Order.Monotone.Union
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
hcy : c ≤ y
⊢ f x ≤ f y

Tactic:
(h₁ xs hs.1 hxc.le).trans (h₂ ht.1 (B _ hy hcy) hcy)

Premises used: LT.lt.le, And.left, LE.le.trans
-- Module: Mathlib.Order.Monotone.Union
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
hcy : c ≤ y
⊢ f x ≤ f y

Tactic:
exact (h₁ xs hs.1 hxc.le).trans (h₂ ht.1 (B _ hy hcy) hcy)

Premises used: LT.lt.le, And.left, LE.le.trans
-- Module: Mathlib.Order.Monotone.Union
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
⊢ x ∈ t

Tactic:
have xt : x ∈ t := B _ hx hcx
-- Module: Mathlib.Order.Monotone.Union
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
⊢ y ∈ t

Tactic:
have yt : y ∈ t := B _ hy (hcx.trans hxy)
-- Module: Mathlib.Order.Monotone.Union
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
yt : y ∈ t
⊢ f x ≤ f y

Tactic:
h₂ xt yt hxy
-- Module: Mathlib.Order.Monotone.Union
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
yt : y ∈ t
⊢ f x ≤ f y

Tactic:
exact h₂ xt yt hxy
-- Module: Mathlib.Order.Monotone.Union
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
a : α
f : α → β
h₁ : MonotoneOn f (Iic a)
h₂ : MonotoneOn f (Ici a)
rw : MonotoneOn f (Iic a ∪ Ici a)
⊢ Monotone f

Tactic:
rw [← monotoneOn_univ, ← @Iic_union_Ici _ _ a]

Premises used: Set.Iic_union_Ici, monotoneOn_univ
-- Module: Mathlib.Order.Monotone.Union
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
a : α
f : α → β
h₁ : MonotoneOn f (Iic a)
h₂ : MonotoneOn f (Ici a)
⊢ MonotoneOn f (Iic a ∪ Ici a)

Tactic:
MonotoneOn.union_right h₁ h₂ isGreatest_Iic isLeast_Ici

Premises used: isLeast_Ici, isGreatest_Iic, MonotoneOn.union_right
-- Module: Mathlib.Order.Monotone.Union
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
a : α
f : α → β
h₁ : MonotoneOn f (Iic a)
h₂ : MonotoneOn f (Ici a)
⊢ MonotoneOn f (Iic a ∪ Ici a)

Tactic:
exact MonotoneOn.union_right h₁ h₂ isGreatest_Iic isLeast_Ici

Premises used: isLeast_Ici, isGreatest_Iic, MonotoneOn.union_right
-- Module: Mathlib.Order.Monotone.Union
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s t : Set α
c : α
h₁ : AntitoneOn f s
h₂ : AntitoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
⊢ AntitoneOn f (s ∪ t)

Tactic:
(h₁.dual_right.union_right h₂.dual_right hs ht).dual_right

Premises used: AntitoneOn.dual_right, MonotoneOn.dual_right, OrderDual, MonotoneOn.union_right
-- Module: Mathlib.Order.Monotone.Union
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
a : α
f : α → β
h₁ : AntitoneOn f (Iic a)
h₂ : AntitoneOn f (Ici a)
⊢ Antitone f

Tactic:
(h₁.dual_right.Iic_union_Ici h₂.dual_right).dual_right

Premises used: MonotoneOn.Iic_union_Ici, AntitoneOn.dual_right, Monotone.dual_right, OrderDual
-- Module: Mathlib.Order.Nat
Goal:
⊢ Eq (α := ℕ) ⊥ 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Nat
Goal:
p : ℕ → Prop
inst : DecidablePred p
hp : ∃ (n : ℕ), p n
⊢ IsLeast {n : ℕ | p n} (Nat.find (p := p) hp)

Tactic:
⟨Nat.find_spec hp, fun _ ↦ Nat.find_min' hp⟩

Premises used: IsLeast, Nat.find_min', And.intro, Nat.find_spec
-- Module: Mathlib.Order.Nat
Goal:
s : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ s
hs : s.Nonempty
⊢ IsLeast s (Nat.find (p := Membership.mem s) hs)

Tactic:
Nat.isLeast_find hs

Premises used: Set.Mem, setOf, Nat.isLeast_find
-- Module: Mathlib.Order.NonemptyFiniteChains
Goal:
X : Type u
inst_1 : PartialOrder X
x x_1 : NonemptyFiniteChains X
h : x.finset = x_1.finset
⊢ x = x_1

Tactic:
aesop
-- Module: Mathlib.Order.NonemptyFiniteChains
Goal:
X : Type u_1
inst : PartialOrder X
A B : NonemptyFiniteChains X
⊢ A ≤ B ↔ A.finset ≤ B.finset

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.NonemptyFiniteChains
Goal:
X : Type u_1
inst : PartialOrder X
A B : NonemptyFiniteChains X
⊢ A < B ↔ A.finset < B.finset

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.NonemptyFiniteChains
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
⊢ ∃ a_1 ∈ s.finset, (f : (a : X) → Y) a_1 = a

Tactic:
simp only [Finset.mem_image] at ha hb

Premises used: Finset.mem_image
-- Module: Mathlib.Order.NonemptyFiniteChains
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
⊢ ∃ a ∈ s.finset, (f : (a : X) → Y) a = b

Tactic:
simp only [Finset.mem_image] at ha hb

Premises used: Finset.mem_image
-- Module: Mathlib.Order.NonemptyFiniteChains
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
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
⊢ 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

Tactic:
obtain ⟨a, ha', rfl⟩ := ha

Premises used: rfl