[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
⊢ StrictMonoOn f (s ∪ t)
[PROOFSTEP]
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
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
⊢ ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
[PROOFSTEP]
intro x hx hxc
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
x : α
hx : x ∈ s ∪ t
hxc : x ≤ c
⊢ x ∈ s
[PROOFSTEP]
cases hx
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
x : α
hxc : x ≤ c
h✝ : x ∈ s
⊢ x ∈ s
[PROOFSTEP]
assumption
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
x : α
hxc : x ≤ c
h✝ : x ∈ t
⊢ x ∈ s
[PROOFSTEP]
rcases eq_or_lt_of_le hxc with (rfl | h'x)
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
x : α
h✝ : x ∈ t
hs : IsGreatest s x
ht : IsLeast t x
hxc : x ≤ x
⊢ x ∈ s
[PROOFSTEP]
exact hs.1
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
x : α
hxc : x ≤ c
h✝ : x ∈ t
h'x : x < c
⊢ x ∈ s
[PROOFSTEP]
exact (lt_irrefl _ (h'x.trans_le (ht.2 (by assumption)))).elim
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
x : α
hxc : x ≤ c
h✝ : x ∈ t
h'x : x < c
⊢ x ∈ t
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
⊢ StrictMonoOn f (s ∪ t)
[PROOFSTEP]
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
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
⊢ ∀ (x : α), x ∈ s ∪ t → c ≤ x → x ∈ t
[PROOFSTEP]
intro x hx hxc
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
x : α
hx : x ∈ s ∪ t
hxc : c ≤ x
⊢ x ∈ t
[PROOFSTEP]
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
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
x : α
hx✝ : x ∈ s ∪ t
hxc : c ≤ x
hx : x ∈ t
⊢ x ∈ t
[PROOFSTEP]
exact hx
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
x : α
hx✝ : x ∈ s ∪ t
hxc : c ≤ x
hx : x ∈ s
⊢ x ∈ t
[PROOFSTEP]
rcases eq_or_lt_of_le hxc with (rfl | h'x)
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
hx✝ : c ∈ s ∪ t
hxc : c ≤ c
hx : c ∈ s
⊢ c ∈ t
[PROOFSTEP]
exact ht.1
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
x : α
hx✝ : x ∈ s ∪ t
hxc : c ≤ x
hx : x ∈ s
h'x : c < x
⊢ x ∈ t
[PROOFSTEP]
exact (lt_irrefl _ (h'x.trans_le (hs.2 hx))).elim
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
B : ∀ (x : α), x ∈ s ∪ t → c ≤ x → x ∈ t
⊢ StrictMonoOn f (s ∪ t)
[PROOFSTEP]
intro x hx y hy hxy
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
B : ∀ (x : α), x ∈ s ∪ t → c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x < y
⊢ f x < f y
[PROOFSTEP]
rcases lt_or_le x c with (hxc | hcx)
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
B : ∀ (x : α), 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
[PROOFSTEP]
have xs : x ∈ s := A _ hx hxc.le
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
B : ∀ (x : α), 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
[PROOFSTEP]
rcases lt_or_le y c with (hyc | hcy)
[GOAL]
case inl.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
B : ∀ (x : α), 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
[PROOFSTEP]
exact h₁ xs (A _ hy hyc.le) hxy
[GOAL]
case inl.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
B : ∀ (x : α), 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
[PROOFSTEP]
exact (h₁ xs hs.1 hxc).trans_le (h₂.monotoneOn ht.1 (B _ hy hcy) hcy)
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
B : ∀ (x : α), 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
[PROOFSTEP]
have xt : x ∈ t := B _ hx hcx
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
B : ∀ (x : α), 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
[PROOFSTEP]
have yt : y ∈ t := B _ hy (hcx.trans hxy.le)
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
B : ∀ (x : α), 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
[PROOFSTEP]
exact h₂ xt yt hxy
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
h₁ : StrictMonoOn f (Iic a)
h₂ : StrictMonoOn f (Ici a)
⊢ StrictMono f
[PROOFSTEP]
rw [← strictMonoOn_univ, ← @Iic_union_Ici _ _ a]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
h₁ : StrictMonoOn f (Iic a)
h₂ : StrictMonoOn f (Ici a)
⊢ StrictMonoOn f (Iic a ∪ Ici a)
[PROOFSTEP]
exact StrictMonoOn.union h₁ h₂ isGreatest_Iic isLeast_Ici
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
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)
[PROOFSTEP]
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
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
⊢ ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
[PROOFSTEP]
intro x hx hxc
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
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
[PROOFSTEP]
cases hx
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
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
[PROOFSTEP]
assumption
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
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
[PROOFSTEP]
rcases eq_or_lt_of_le hxc with (rfl | h'x)
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
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
[PROOFSTEP]
exact hs.1
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
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
[PROOFSTEP]
exact (lt_irrefl _ (h'x.trans_le (ht.2 (by assumption)))).elim
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
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
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
⊢ MonotoneOn f (s ∪ t)
[PROOFSTEP]
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
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
⊢ ∀ (x : α), x ∈ s ∪ t → c ≤ x → x ∈ t
[PROOFSTEP]
intro x hx hxc
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
x : α
hx : x ∈ s ∪ t
hxc : c ≤ x
⊢ x ∈ t
[PROOFSTEP]
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
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
x : α
hx✝ : x ∈ s ∪ t
hxc : c ≤ x
hx : x ∈ t
⊢ x ∈ t
[PROOFSTEP]
exact hx
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
x : α
hx✝ : x ∈ s ∪ t
hxc : c ≤ x
hx : x ∈ s
⊢ x ∈ t
[PROOFSTEP]
rcases eq_or_lt_of_le hxc with (rfl | h'x)
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
hx✝ : c ∈ s ∪ t
hxc : c ≤ c
hx : c ∈ s
⊢ c ∈ t
[PROOFSTEP]
exact ht.1
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
x : α
hx✝ : x ∈ s ∪ t
hxc : c ≤ x
hx : x ∈ s
h'x : c < x
⊢ x ∈ t
[PROOFSTEP]
exact (lt_irrefl _ (h'x.trans_le (hs.2 hx))).elim
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
B : ∀ (x : α), x ∈ s ∪ t → c ≤ x → x ∈ t
⊢ MonotoneOn f (s ∪ t)
[PROOFSTEP]
intro x hx y hy hxy
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
B : ∀ (x : α), x ∈ s ∪ t → c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x ≤ y
⊢ f x ≤ f y
[PROOFSTEP]
rcases lt_or_le x c with (hxc | hcx)
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
B : ∀ (x : α), 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
[PROOFSTEP]
have xs : x ∈ s := A _ hx hxc.le
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
B : ∀ (x : α), 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
[PROOFSTEP]
rcases lt_or_le y c with (hyc | hcy)
[GOAL]
case inl.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
B : ∀ (x : α), 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
[PROOFSTEP]
exact h₁ xs (A _ hy hyc.le) hxy
[GOAL]
case inl.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
B : ∀ (x : α), 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
[PROOFSTEP]
exact (h₁ xs hs.1 hxc.le).trans (h₂ ht.1 (B _ hy hcy) hcy)
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
B : ∀ (x : α), 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
[PROOFSTEP]
have xt : x ∈ t := B _ hx hcx
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
B : ∀ (x : α), 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
[PROOFSTEP]
have yt : y ∈ t := B _ hy (hcx.trans hxy)
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
B : ∀ (x : α), 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
[PROOFSTEP]
exact h₂ xt yt hxy
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
h₁ : MonotoneOn f (Iic a)
h₂ : MonotoneOn f (Ici a)
⊢ Monotone f
[PROOFSTEP]
rw [← monotoneOn_univ, ← @Iic_union_Ici _ _ a]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
h₁ : MonotoneOn f (Iic a)
h₂ : MonotoneOn f (Ici a)
⊢ MonotoneOn f (Iic a ∪ Ici a)
[PROOFSTEP]
exact MonotoneOn.union_right h₁ h₂ isGreatest_Iic isLeast_Ici
