[GOAL]
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ b✝ c d a b : α
⊢ min a b = a ∧ a ≤ b ∨ min a b = b ∧ b < a
[PROOFSTEP]
by_cases h : a ≤ b
[GOAL]
case pos
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ b✝ c d a b : α
h : a ≤ b
⊢ min a b = a ∧ a ≤ b ∨ min a b = b ∧ b < a
[PROOFSTEP]
left
[GOAL]
case pos.h
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ b✝ c d a b : α
h : a ≤ b
⊢ min a b = a ∧ a ≤ b
[PROOFSTEP]
exact ⟨min_eq_left h, h⟩
[GOAL]
case neg
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ b✝ c d a b : α
h : ¬a ≤ b
⊢ min a b = a ∧ a ≤ b ∨ min a b = b ∧ b < a
[PROOFSTEP]
right
[GOAL]
case neg.h
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ b✝ c d a b : α
h : ¬a ≤ b
⊢ min a b = b ∧ b < a
[PROOFSTEP]
exact ⟨min_eq_right (le_of_lt (not_le.mp h)), not_le.mp h⟩
[GOAL]
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b c d : α
⊢ min a b = c ↔ a = c ∧ a ≤ b ∨ b = c ∧ b ≤ a
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b c d : α
⊢ min a b = c → a = c ∧ a ≤ b ∨ b = c ∧ b ≤ a
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b c d : α
h : min a b = c
⊢ a = c ∧ a ≤ b ∨ b = c ∧ b ≤ a
[PROOFSTEP]
refine' Or.imp (fun h' => _) (fun h' => _) (le_total a b)
[GOAL]
case mp.refine'_1
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b c d : α
h : min a b = c
h' : a ≤ b
⊢ a = c ∧ a ≤ b
[PROOFSTEP]
exact ⟨by simpa [h'] using h, h'⟩
[GOAL]
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b c d : α
h : min a b = c
h' : a ≤ b
⊢ a = c
[PROOFSTEP]
simpa [h'] using h
[GOAL]
case mp.refine'_2
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b c d : α
h : min a b = c
h' : b ≤ a
⊢ b = c ∧ b ≤ a
[PROOFSTEP]
exact ⟨by simpa [h'] using h, h'⟩
[GOAL]
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b c d : α
h : min a b = c
h' : b ≤ a
⊢ b = c
[PROOFSTEP]
simpa [h'] using h
[GOAL]
case mpr
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b c d : α
⊢ a = c ∧ a ≤ b ∨ b = c ∧ b ≤ a → min a b = c
[PROOFSTEP]
rintro (⟨rfl, h⟩ | ⟨rfl, h⟩)
[GOAL]
case mpr.inl.intro
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b d : α
h : a ≤ b
⊢ min a b = a
[PROOFSTEP]
simp [h]
[GOAL]
case mpr.inr.intro
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b d : α
h : b ≤ a
⊢ min a b = b
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b c d : α
⊢ min a c < min b c ↔ a < b ∧ a < c
[PROOFSTEP]
simp_rw [lt_min_iff, min_lt_iff, or_iff_left (lt_irrefl _)]
[GOAL]
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b c d : α
⊢ (a < b ∨ c < b) ∧ a < c ↔ a < b ∧ a < c
[PROOFSTEP]
exact and_congr_left fun h => or_iff_left_of_imp h.trans
[GOAL]
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b c d : α
⊢ min a b < min a c ↔ b < c ∧ b < a
[PROOFSTEP]
simp_rw [min_comm a, min_lt_min_left_iff]
[GOAL]
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b c d : α
⊢ ∀ (a : α), max a a = a
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b c d : α
⊢ ∀ (a : α), min a a = a
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b c d : α
hf : MonotoneOn f s
ha : a ∈ s
hb : b ∈ s
⊢ f (max a b) = max (f a) (f b)
[PROOFSTEP]
cases' le_total a b with h h
[GOAL]
case inl
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b c d : α
hf : MonotoneOn f s
ha : a ∈ s
hb : b ∈ s
h : a ≤ b
⊢ f (max a b) = max (f a) (f b)
[PROOFSTEP]
simp only [max_eq_right, max_eq_left, hf ha hb, hf hb ha, h]
[GOAL]
case inr
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b c d : α
hf : MonotoneOn f s
ha : a ∈ s
hb : b ∈ s
h : b ≤ a
⊢ f (max a b) = max (f a) (f b)
[PROOFSTEP]
simp only [max_eq_right, max_eq_left, hf ha hb, hf hb ha, h]
[GOAL]
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b c d : α
hf : Monotone f
⊢ f (max a b) = max (f a) (f b)
[PROOFSTEP]
cases' le_total a b with h h
[GOAL]
case inl
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b c d : α
hf : Monotone f
h : a ≤ b
⊢ f (max a b) = max (f a) (f b)
[PROOFSTEP]
simp [h, hf h]
[GOAL]
case inr
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b c d : α
hf : Monotone f
h : b ≤ a
⊢ f (max a b) = max (f a) (f b)
[PROOFSTEP]
simp [h, hf h]
[GOAL]
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b c d : α
hf : Antitone f
⊢ f (max a b) = min (f a) (f b)
[PROOFSTEP]
cases' le_total a b with h h
[GOAL]
case inl
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b c d : α
hf : Antitone f
h : a ≤ b
⊢ f (max a b) = min (f a) (f b)
[PROOFSTEP]
simp [h, hf h]
[GOAL]
case inr
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b c d : α
hf : Antitone f
h : b ≤ a
⊢ f (max a b) = min (f a) (f b)
[PROOFSTEP]
simp [h, hf h]
[GOAL]
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ b✝ c d a b : α
⊢ min a b = a ∨ min a b = b
[PROOFSTEP]
cases le_total a b
[GOAL]
case inl
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ b✝ c d a b : α
h✝ : a ≤ b
⊢ min a b = a ∨ min a b = b
[PROOFSTEP]
simp [*]
[GOAL]
case inr
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ b✝ c d a b : α
h✝ : b ≤ a
⊢ min a b = a ∨ min a b = b
[PROOFSTEP]
simp [*]
