α : Type u_2
β : Type u_1
γ : Type ?u.65002
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : LinearOrder β
c : β
⊢ c ≥ fold min b f s ↔ b ≤ c ∨ ∃ x, x ∈ s ∧ f x ≤ c
α : Type u_2
β : Type u_1
γ : Type ?u.65002
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : LinearOrder β
c : β
⊢ fold min b f s ≤ c ↔ b ≤ c ∨ ∃ x, x ∈ s ∧ f x ≤ c
show _ ≥ _ ↔ _
case hr
α : Type u_2
β : Type u_1
γ : Type ?u.65002
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : LinearOrder β
c : β
⊢ ∀ {x y z : β}, x ≥ min y z ↔ x ≥ y ∨ x ≥ z
α : Type u_2
β : Type u_1
γ : Type ?u.65002
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : LinearOrder β
c : β
⊢ c ≥ fold min b f s ↔ b ≤ c ∨ ∃ x, x ∈ s ∧ f x ≤ c
apply fold_op_rel_iff_or
case hr
α : Type u_2
β : Type u_1
γ : Type ?u.65002
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : LinearOrder β
c x y z : β
⊢ x ≥ min y z ↔ x ≥ y ∨ x ≥ z
case hr
α : Type u_2
β : Type u_1
γ : Type ?u.65002
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : LinearOrder β
c : β
⊢ ∀ {x y z : β}, x ≥ min y z ↔ x ≥ y ∨ x ≥ z
intro x y z
case hr
α : Type u_2
β : Type u_1
γ : Type ?u.65002
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : LinearOrder β
c x y z : β
⊢ min y z ≤ x ↔ x ≥ y ∨ x ≥ z
case hr
α : Type u_2
β : Type u_1
γ : Type ?u.65002
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : LinearOrder β
c x y z : β
⊢ x ≥ min y z ↔ x ≥ y ∨ x ≥ z
show _ ≤ _ ↔ _
no goals
case hr
α : Type u_2
β : Type u_1
γ : Type ?u.65002
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : LinearOrder β
c x y z : β
⊢ min y z ≤ x ↔ x ≥ y ∨ x ≥ z
exact min_le_iff