/-
Copyright (c) 2017 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro

! This file was ported from Lean 3 source module data.fintype.lattice
! leanprover-community/mathlib commit 509de852e1de55e1efa8eacfa11df0823f26f226
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Fintype.Card
import Mathlib.Data.Finset.Lattice

/-!
# Lemmas relating fintypes and order/lattice structure.
-/


open Function

open Nat

universe u v

variable {
α: Type ?u.355
α 
β: Type ?u.5
β : 
Type _: Type (?u.20+1)
Type _}

namespace Finset

variable [
Fintype: Type ?u.26 → Type ?u.26
Fintype 
α: Type ?u.20
α] {
s: Finset α
s : 
Finset: Type ?u.29 → Type ?u.29
Finset 
α: Type ?u.355
α}

/-- A special case of `Finset.sup_eq_iSup` that omits the useless `x ∈ univ` binder. -/
theorem 
sup_univ_eq_iSup: ∀ [inst : CompleteLattice β] (f : α → β), sup univ f = iSup f
sup_univ_eq_iSup [
CompleteLattice: Type ?u.32 → Type ?u.32
CompleteLattice 
β: Type ?u.23
β] (
f: α → β
f : 
α: Type ?u.20
α → 
β: Type ?u.23
β) : 
Finset.univ: {α : Type ?u.40} → [inst : Fintype α] → Finset α
Finset.univ.
sup: {α : Type ?u.68} → {β : Type ?u.67} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup 
f: α → β
f = 
iSup: {α : Type ?u.158} → [inst : SupSet α] → {ι : Sort ?u.157} → (ι → α) → α
iSup 
f: α → β
f :=
  (
sup_eq_iSup: ∀ {α : Type ?u.183} {β : Type ?u.182} [inst : CompleteLattice β] (s : Finset α) (f : α → β), sup s f = ⨆ a, ⨆ h, f a
sup_eq_iSup 
_: Finset ?m.184
_ 
f: α → β
f).
trans: ∀ {α : Sort ?u.196} {a b c : α}, a = b → b = c → a = c
trans <| 
congr_arg: ∀ {α : Sort ?u.219} {β : Sort ?u.218} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂
congr_arg 
_: ?m.220 → ?m.221
_ <| 
funext: ∀ {α : Sort ?u.234} {β : α → Sort ?u.233} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g
funext fun 
_: ?m.248
_ => 
iSup_pos: ∀ {α : Type ?u.250} [inst : CompleteLattice α] {p : Prop} {f : p → α} (hp : p), (⨆ h, f h) = f hp
iSup_pos (
mem_univ: ∀ {α : Type ?u.255} [inst : Fintype α] (x : α), x ∈ univ
mem_univ 
_: ?m.256
_)
#align finset.sup_univ_eq_supr 
Finset.sup_univ_eq_iSup: ∀ {α : Type u_2} {β : Type u_1} [inst : Fintype α] [inst_1 : CompleteLattice β] (f : α → β), sup univ f = iSup f
Finset.sup_univ_eq_iSup

/-- A special case of `Finset.inf_eq_iInf` that omits the useless `x ∈ univ` binder. -/
theorem 
inf_univ_eq_iInf: ∀ {α : Type u_2} {β : Type u_1} [inst : Fintype α] [inst_1 : CompleteLattice β] (f : α → β), inf univ f = iInf f
inf_univ_eq_iInf [
CompleteLattice: Type ?u.367 → Type ?u.367
CompleteLattice 
β: Type ?u.358
β] (
f: α → β
f : 
α: Type ?u.355
α → 
β: Type ?u.358
β) : 
Finset.univ: {α : Type ?u.375} → [inst : Fintype α] → Finset α
Finset.univ.
inf: {α : Type ?u.403} → {β : Type ?u.402} → [inst : SemilatticeInf α] → [inst : OrderTop α] → Finset β → (β → α) → α
inf 
f: α → β
f = 
iInf: {α : Type ?u.489} → [inst : InfSet α] → {ι : Sort ?u.488} → (ι → α) → α
iInf 
f: α → β
f :=
  @
sup_univ_eq_iSup: ∀ {α : Type ?u.514} {β : Type ?u.513} [inst : Fintype α] [inst_1 : CompleteLattice β] (f : α → β), sup univ f = iSup f
sup_univ_eq_iSup 
_: Type ?u.514
_ 
β: Type ?u.358
βᵒᵈ _ _ (
f: α → β
f : 
α: Type ?u.355
α → 
β: Type ?u.358
βᵒᵈ)
#align finset.inf_univ_eq_infi 
Finset.inf_univ_eq_iInf: ∀ {α : Type u_2} {β : Type u_1} [inst : Fintype α] [inst_1 : CompleteLattice β] (f : α → β), inf univ f = iInf f
Finset.inf_univ_eq_iInf

@[simp]
theorem 
fold_inf_univ: ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : SemilatticeInf α] [inst_2 : OrderBot α] (a : α),
  fold (fun x x_1 => x ⊓ x_1) a (fun x => x) univ = ⊥
fold_inf_univ [
SemilatticeInf: Type ?u.588 → Type ?u.588
SemilatticeInf 
α: Type ?u.576
α] [
OrderBot: (α : Type ?u.591) → [inst : LE α] → Type ?u.591
OrderBot 
α: Type ?u.576
α] (
a: α
a : 
α: Type ?u.576
α) :
    -- Porting note: added `haveI`
    haveI : 
IsCommutative: (α : Type ?u.913) → (α → α → α) → Prop
IsCommutative 
α: Type ?u.576
α 
(· ⊓ ·): α → α → α
(· ⊓ ·) := 
inferInstance: ∀ {α : Sort ?u.1136} [i : α], α
inferInstance
    (
Finset.univ: {α : Type ?u.1161} → [inst : Fintype α] → Finset α
Finset.univ.
fold: {α : Type ?u.1189} →
  {β : Type ?u.1188} →
    (op : β → β → β) → [hc : IsCommutative β op] → [ha : IsAssociative β op] → β → (α → β) → Finset α → β
fold 
(· ⊓ ·): α → α → α
(· ⊓ ·) 
a: α
a fun 
x: ?m.1282
x => 
x: ?m.1282
x) = 
⊥: ?m.1701
⊥ :=
  
eq_bot_iff: ∀ {α : Type ?u.2052} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, a = ⊥ ↔ a ≤ ⊥
eq_bot_iff.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 <|
    ((
Finset.fold_op_rel_iff_and: ∀ {α : Type ?u.2451} {β : Type ?u.2452} {op : β → β → β} [hc : IsCommutative β op] [ha : IsAssociative β op] {f : α → β}
  {b : β} {s : Finset α} {r : β → β → Prop},
  (∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z) → ∀ {c : β}, r c (fold op b f s) ↔ r c b ∧ ∀ (x : α), x ∈ s → r c (f x)
Finset.fold_op_rel_iff_and <| @
le_inf_iff: ∀ {α : Type ?u.2462} [inst : SemilatticeInf α] {a b c : α}, a ≤ b ⊓ c ↔ a ≤ b ∧ a ≤ c
le_inf_iff 
α: Type ?u.576
α _).
1: ∀ {a b : Prop}, (a ↔ b) → a → b
1 
le_rfl: ∀ {α : Type ?u.2516} [inst : Preorder α] {a : α}, a ≤ a
le_rfl).
2: ∀ {a b : Prop}, a ∧ b → b
2 
⊥: ?m.2790
⊥ <| 
Finset.mem_univ: ∀ {α : Type ?u.2853} [inst : Fintype α] (x : α), x ∈ univ
Finset.mem_univ 
_: ?m.2854
_
#align finset.fold_inf_univ 
Finset.fold_inf_univ: ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : SemilatticeInf α] [inst_2 : OrderBot α] (a : α),
  fold (fun x x_1 => x ⊓ x_1) a (fun x => x) univ = ⊥
Finset.fold_inf_univ

@[simp]
theorem 
fold_sup_univ: ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : SemilatticeSup α] [inst_2 : OrderTop α] (a : α),
  fold (fun x x_1 => x ⊔ x_1) a (fun x => x) univ = ⊤
fold_sup_univ [
SemilatticeSup: Type ?u.3263 → Type ?u.3263
SemilatticeSup 
α: Type ?u.3251
α] [
OrderTop: (α : Type ?u.3266) → [inst : LE α] → Type ?u.3266
OrderTop 
α: Type ?u.3251
α] (
a: α
a : 
α: Type ?u.3251
α) :
    -- Porting note: added `haveI`
    haveI : 
IsCommutative: (α : Type ?u.3704) → (α → α → α) → Prop
IsCommutative 
α: Type ?u.3251
α 
(· ⊔ ·): α → α → α
(· ⊔ ·) := 
inferInstance: ∀ {α : Sort ?u.3746} [i : α], α
inferInstance
    (
Finset.univ: {α : Type ?u.3773} → [inst : Fintype α] → Finset α
Finset.univ.
fold: {α : Type ?u.3801} →
  {β : Type ?u.3800} →
    (op : β → β → β) → [hc : IsCommutative β op] → [ha : IsAssociative β op] → β → (α → β) → Finset α → β
fold 
(· ⊔ ·): α → α → α
(· ⊔ ·) 
a: α
a fun 
x: ?m.3891
x => 
x: ?m.3891
x) = 
⊤: ?m.3980
⊤ :=
  @
fold_inf_univ: ∀ {α : Type ?u.4386} [inst : Fintype α] [inst_1 : SemilatticeInf α] [inst_2 : OrderBot α] (a : α),
  fold (fun x x_1 => x ⊓ x_1) a (fun x => x) univ = ⊥
fold_inf_univ 
α: Type ?u.3251
αᵒᵈ _ _ _ 
_: αᵒᵈ
_
#align finset.fold_sup_univ 
Finset.fold_sup_univ: ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : SemilatticeSup α] [inst_2 : OrderTop α] (a : α),
  fold (fun x x_1 => x ⊔ x_1) a (fun x => x) univ = ⊤
Finset.fold_sup_univ

end Finset

open Finset Function

theorem 
Finite.exists_max: ∀ [inst : Finite α] [inst : Nonempty α] [inst : LinearOrder β] (f : α → β), ∃ x₀, ∀ (x : α), f x ≤ f x₀
Finite.exists_max [
Finite: Sort ?u.4502 → Prop
Finite 
α: Type ?u.4496
α] [
Nonempty: Sort ?u.4505 → Prop
Nonempty 
α: Type ?u.4496
α] [
LinearOrder: Type ?u.4508 → Type ?u.4508
LinearOrder 
β: Type ?u.4499
β] (
f: α → β
f : 
α: Type ?u.4496
α → 
β: Type ?u.4499
β) :
    ∃ 
x₀: α
x₀ : 
α: Type ?u.4496
α, ∀ 
x: ?m.4520
x, 
f: α → β
f 
x: ?m.4520
x ≤ 
f: α → β
f 
x₀: α
x₀ := by
Goals accomplished! 🐙
  
α: Type u_1

β: Type u_2

inst✝²: Finite α

inst✝¹: Nonempty α

inst✝: LinearOrder β

f: α → β

∃ x₀, ∀ (x : α), f x ≤ f x₀cases 
nonempty_fintype: ∀ (α : Type ?u.4943) [inst : Finite α], Nonempty (Fintype α)
nonempty_fintype 
α: Type u_1
α
α: Type u_1

β: Type u_2

inst✝²: Finite α

inst✝¹: Nonempty α

inst✝: LinearOrder β

f: α → β

val✝: Fintype α

intro
∃ x₀, ∀ (x : α), f x ≤ f x₀
  
α: Type u_1

β: Type u_2

inst✝²: Finite α

inst✝¹: Nonempty α

inst✝: LinearOrder β

f: α → β

∃ x₀, ∀ (x : α), f x ≤ f x₀simpa using 
exists_max_image: ∀ {α : Type ?u.6081} {β : Type ?u.6080} [inst : LinearOrder α] (s : Finset β) (f : β → α),
  Finset.Nonempty s → ∃ x, x ∈ s ∧ ∀ (x' : β), x' ∈ s → f x' ≤ f x
exists_max_image 
univ: {α : Type ?u.6085} → [inst : Fintype α] → Finset α
univ 
f: α → β
f 
univ_nonempty: ∀ {α : Type ?u.6140} [inst : Fintype α] [inst_1 : Nonempty α], Finset.Nonempty univ
univ_nonempty
Goals accomplished! 🐙
#align finite.exists_max 
Finite.exists_max: ∀ {α : Type u_1} {β : Type u_2} [inst : Finite α] [inst : Nonempty α] [inst : LinearOrder β] (f : α → β),
  ∃ x₀, ∀ (x : α), f x ≤ f x₀
Finite.exists_max

theorem 
Finite.exists_min: ∀ [inst : Finite α] [inst : Nonempty α] [inst : LinearOrder β] (f : α → β), ∃ x₀, ∀ (x : α), f x₀ ≤ f x
Finite.exists_min [
Finite: Sort ?u.8579 → Prop
Finite 
α: Type ?u.8573
α] [
Nonempty: Sort ?u.8582 → Prop
Nonempty 
α: Type ?u.8573
α] [
LinearOrder: Type ?u.8585 → Type ?u.8585
LinearOrder 
β: Type ?u.8576
β] (
f: α → β
f : 
α: Type ?u.8573
α → 
β: Type ?u.8576
β) :
    ∃ 
x₀: α
x₀ : 
α: Type ?u.8573
α, ∀ 
x: ?m.8597
x, 
f: α → β
f 
x₀: α
x₀ ≤ 
f: α → β
f 
x: ?m.8597
x := by
Goals accomplished! 🐙
  
α: Type u_1

β: Type u_2

inst✝²: Finite α

inst✝¹: Nonempty α

inst✝: LinearOrder β

f: α → β

∃ x₀, ∀ (x : α), f x₀ ≤ f xcases 
nonempty_fintype: ∀ (α : Type ?u.9020) [inst : Finite α], Nonempty (Fintype α)
nonempty_fintype 
α: Type u_1
α
α: Type u_1

β: Type u_2

inst✝²: Finite α

inst✝¹: Nonempty α

inst✝: LinearOrder β

f: α → β

val✝: Fintype α

intro
∃ x₀, ∀ (x : α), f x₀ ≤ f x
  
α: Type u_1

β: Type u_2

inst✝²: Finite α

inst✝¹: Nonempty α

inst✝: LinearOrder β

f: α → β

∃ x₀, ∀ (x : α), f x₀ ≤ f xsimpa using 
exists_min_image: ∀ {α : Type ?u.10158} {β : Type ?u.10157} [inst : LinearOrder α] (s : Finset β) (f : β → α),
  Finset.Nonempty s → ∃ x, x ∈ s ∧ ∀ (x' : β), x' ∈ s → f x ≤ f x'
exists_min_image 
univ: {α : Type ?u.10162} → [inst : Fintype α] → Finset α
univ 
f: α → β
f 
univ_nonempty: ∀ {α : Type ?u.10217} [inst : Fintype α] [inst_1 : Nonempty α], Finset.Nonempty univ
univ_nonempty
Goals accomplished! 🐙
#align finite.exists_min 
Finite.exists_min: ∀ {α : Type u_1} {β : Type u_2} [inst : Finite α] [inst : Nonempty α] [inst : LinearOrder β] (f : α → β),
  ∃ x₀, ∀ (x : α), f x₀ ≤ f x
Finite.exists_min