/-
Copyright (c) 2018 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.finset.lattice
! leanprover-community/mathlib commit 2d44d6823a96f9c79b7d1ab185918377be663424
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Finset.Fold
import Mathlib.Data.Finset.Option
import Mathlib.Data.Finset.Pi
import Mathlib.Data.Finset.Prod
import Mathlib.Data.Multiset.Lattice
import Mathlib.Order.CompleteLattice
import Mathlib.Order.Hom.Lattice

/-!
# Lattice operations on finsets
-/


variable {F: Type ?u.364375
F α: Type ?u.138130
α β: Type ?u.8
β γ: Type ?u.364384
γ ι: Type ?u.138139
ι κ: Type ?u.91666
κ : Type _: Type (?u.230778+1)
Type _}

namespace Finset

open Multiset OrderDual

/-! ### sup -/


section Sup

-- TODO: define with just `[Bot α]` where some lemmas hold without requiring `[OrderBot α]`
variable [SemilatticeSup: Type ?u.37973 → Type ?u.37973
SemilatticeSup α: Type ?u.23
α] [OrderBot: (α : Type ?u.36365) → [inst : LE α] → Type ?u.36365
OrderBot α: Type ?u.23
α]

/-- Supremum of a finite set: `sup {a, b, c} f = f a ⊔ f b ⊔ f c` -/
def sup: Finset β → (β → α) → α
sup (s: Finset β
s : Finset: Type ?u.906 → Type ?u.906
Finset β: Type ?u.469
β) (f: β → α
f : β: Type ?u.469
β → α: Type ?u.466
α) : α: Type ?u.466
α :=
  s: Finset β
s.fold: {α : Type ?u.917} →
  {β : Type ?u.916} →
    (op : β → β → β) → [hc : IsCommutative β op] → [ha : IsAssociative β op] → β → (α → β) → Finset α → β
fold (· ⊔ ·): α → α → α
(· ⊔ ·) ⊥: ?m.977
⊥ f: β → α
f
#align finset.sup Finset.sup: {α : Type u_1} → {β : Type u_2} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
Finset.sup

variable {s: Finset β
s s₁: Finset β
s₁ s₂: Finset β
s₂ : Finset: Type ?u.13999 → Type ?u.13999
Finset β: Type ?u.1639
β} {f: β → α
f g: β → α
g : β: Type ?u.46375
β → α: Type ?u.14248
α} {a: α
a : α: Type ?u.1636
α}

theorem sup_def: sup s f = Multiset.sup (Multiset.map f s.val)
sup_def : s: Finset β
s.sup: {α : Type ?u.2559} → {β : Type ?u.2558} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup f: β → α
f = (s: Finset β
s.1: {α : Type ?u.2590} → Finset α → Multiset α
1.map: {α : Type ?u.2593} → {β : Type ?u.2592} → (α → β) → Multiset α → Multiset β
map f: β → α
f).sup: {α : Type ?u.2604} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Multiset α → α
sup :=
  rfl: ∀ {α : Sort ?u.2615} {a : α}, a = a
rfl
#align finset.sup_def Finset.sup_def: ∀ {α : Type u_1} {β : Type u_2} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α},
  sup s f = Multiset.sup (Multiset.map f s.val)
Finset.sup_def

@[simp]
theorem sup_empty: ∀ {α : Type u_1} {β : Type u_2} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {f : β → α}, sup ∅ f = ⊥
sup_empty : (∅: ?m.3095
∅ : Finset: Type ?u.3093 → Type ?u.3093
Finset β: Type ?u.2635
β).sup: {α : Type ?u.3141} → {β : Type ?u.3140} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup f: β → α
f = ⊥: ?m.3172
⊥ :=
  fold_empty: ∀ {α : Type ?u.3674} {β : Type ?u.3673} {op : β → β → β} [hc : IsCommutative β op] [ha : IsAssociative β op] {f : α → β}
  {b : β}, fold op b f ∅ = b
fold_empty
#align finset.sup_empty Finset.sup_empty: ∀ {α : Type u_1} {β : Type u_2} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {f : β → α}, sup ∅ f = ⊥
Finset.sup_empty

@[simp]
theorem sup_cons: ∀ {b : β} (h : ¬b ∈ s), sup (cons b s h) f = f b ⊔ sup s f
sup_cons {b: β
b : β: Type ?u.3836
β} (h: ¬b ∈ s
h : b: β
b ∉ s: Finset β
s) : (cons: {α : Type ?u.4312} → (a : α) → (s : Finset α) → ¬a ∈ s → Finset α
cons b: β
b s: Finset β
s h: ¬b ∈ s
h).sup: {α : Type ?u.4317} → {β : Type ?u.4316} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup f: β → α
f = f: β → α
f b: β
b ⊔ s: Finset β
s.sup: {α : Type ?u.4351} → {β : Type ?u.4350} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup f: β → α
f :=
  fold_cons: ∀ {α : Type ?u.4427} {β : Type ?u.4428} {op : β → β → β} [hc : IsCommutative β op] [ha : IsAssociative β op] {f : α → β}
  {b : β} {s : Finset α} {a : α} (h : ¬a ∈ s), fold op b f (cons a s h) = op (f a) (fold op b f s)
fold_cons h: ¬b ∈ s
h
#align finset.sup_cons Finset.sup_cons: ∀ {α : Type u_2} {β : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α} {b : β}
  (h : ¬b ∈ s), sup (cons b s h) f = f b ⊔ sup s f
Finset.sup_cons

@[simp]
theorem sup_insert: ∀ {α : Type u_2} {β : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α}
  [inst_2 : DecidableEq β] {b : β}, sup (insert b s) f = f b ⊔ sup s f
sup_insert [DecidableEq: Sort ?u.5047 → Sort (max1?u.5047)
DecidableEq β: Type ?u.4591
β] {b: β
b : β: Type ?u.4591
β} : (insert: {α : outParam (Type ?u.5062)} → {γ : Type ?u.5061} → [self : Insert α γ] → α → γ → γ
insert b: β
b s: Finset β
s : Finset: Type ?u.5060 → Type ?u.5060
Finset β: Type ?u.4591
β).sup: {α : Type ?u.5116} → {β : Type ?u.5115} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup f: β → α
f = f: β → α
f b: β
b ⊔ s: Finset β
s.sup: {α : Type ?u.5150} → {β : Type ?u.5149} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup f: β → α
f :=
  fold_insert_idem: ∀ {α : Type ?u.5228} {β : Type ?u.5229} {op : β → β → β} [hc : IsCommutative β op] [ha : IsAssociative β op] {f : α → β}
  {b : β} {s : Finset α} {a : α} [inst : DecidableEq α] [hi : IsIdempotent β op],
  fold op b f (insert a s) = op (f a) (fold op b f s)
fold_insert_idem
#align finset.sup_insert Finset.sup_insert: ∀ {α : Type u_2} {β : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α}
  [inst_2 : DecidableEq β] {b : β}, sup (insert b s) f = f b ⊔ sup s f
Finset.sup_insert

theorem sup_image: ∀ [inst : DecidableEq β] (s : Finset γ) (f : γ → β) (g : β → α), sup (image f s) g = sup s (g ∘ f)
sup_image [DecidableEq: Sort ?u.5971 → Sort (max1?u.5971)
DecidableEq β: Type ?u.5515
β] (s: Finset γ
s : Finset: Type ?u.5980 → Type ?u.5980
Finset γ: Type ?u.5518
γ) (f: γ → β
f : γ: Type ?u.5518
γ → β: Type ?u.5515
β) (g: β → α
g : β: Type ?u.5515
β → α: Type ?u.5512
α) :
    (s: Finset γ
s.image: {α : Type ?u.5993} → {β : Type ?u.5992} → [inst : DecidableEq β] → (α → β) → Finset α → Finset β
image f: γ → β
f).sup: {α : Type ?u.6047} → {β : Type ?u.6046} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup g: β → α
g = s: Finset γ
s.sup: {α : Type ?u.6079} → {β : Type ?u.6078} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup (g: β → α
g ∘ f: γ → β
f) :=
  fold_image_idem: ∀ {α : Type ?u.6115} {β : Type ?u.6117} {γ : Type ?u.6116} {op : β → β → β} [hc : IsCommutative β op]
  [ha : IsAssociative β op] {f : α → β} {b : β} [inst : DecidableEq α] {g : γ → α} {s : Finset γ}
  [hi : IsIdempotent β op], fold op b f (image g s) = fold op b (f ∘ g) s
fold_image_idem
#align finset.sup_image Finset.sup_image: ∀ {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : SemilatticeSup α] [inst_1 : OrderBot α] [inst_2 : DecidableEq β]
  (s : Finset γ) (f : γ → β) (g : β → α), sup (image f s) g = sup s (g ∘ f)
Finset.sup_image

@[simp]
theorem sup_map: ∀ {α : Type u_3} {β : Type u_2} {γ : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderBot α] (s : Finset γ)
  (f : γ ↪ β) (g : β → α), sup (map f s) g = sup s (g ∘ ↑f)
sup_map (s: Finset γ
s : Finset: Type ?u.6829 → Type ?u.6829
Finset γ: Type ?u.6376
γ) (f: γ ↪ β
f : γ: Type ?u.6376
γ ↪ β: Type ?u.6373
β) (g: β → α
g : β: Type ?u.6373
β → α: Type ?u.6370
α) : (s: Finset γ
s.map: {α : Type ?u.6842} → {β : Type ?u.6841} → (α ↪ β) → Finset α → Finset β
map f: γ ↪ β
f).sup: {α : Type ?u.6855} → {β : Type ?u.6854} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup g: β → α
g = s: Finset γ
s.sup: {α : Type ?u.6887} → {β : Type ?u.6886} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup (g: β → α
g ∘ f: γ ↪ β
f) :=
  fold_map: ∀ {α : Type ?u.13401} {β : Type ?u.13402} {γ : Type ?u.13400} {op : β → β → β} [hc : IsCommutative β op]
  [ha : IsAssociative β op] {f : α → β} {b : β} {g : γ ↪ α} {s : Finset γ}, fold op b f (map g s) = fold op b (f ∘ ↑g) s
fold_map
#align finset.sup_map Finset.sup_map: ∀ {α : Type u_3} {β : Type u_2} {γ : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderBot α] (s : Finset γ)
  (f : γ ↪ β) (g : β → α), sup (map f s) g = sup s (g ∘ ↑f)
Finset.sup_map

@[simp]
theorem sup_singleton: ∀ {α : Type u_1} {β : Type u_2} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {f : β → α} {b : β}, sup {b} f = f b
sup_singleton {b: β
b : β: Type ?u.13562
β} : ({b: β
b} : Finset: Type ?u.14022 → Type ?u.14022
Finset β: Type ?u.13562
β).sup: {α : Type ?u.14049} → {β : Type ?u.14048} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup f: β → α
f = f: β → α
f b: β
b :=
  Multiset.sup_singleton: ∀ {α : Type ?u.14082} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {a : α}, Multiset.sup {a} = a
Multiset.sup_singleton
#align finset.sup_singleton Finset.sup_singleton: ∀ {α : Type u_1} {β : Type u_2} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {f : β → α} {b : β}, sup {b} f = f b
Finset.sup_singleton

theorem sup_union: ∀ {α : Type u_2} {β : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s₁ s₂ : Finset β} {f : β → α}
  [inst_2 : DecidableEq β], sup (s₁ ∪ s₂) f = sup s₁ f ⊔ sup s₂ f
sup_union [DecidableEq: Sort ?u.14707 → Sort (max1?u.14707)
DecidableEq β: Type ?u.14251
β] : (s₁: Finset β
s₁ ∪ s₂: Finset β
s₂).sup: {α : Type ?u.14757} → {β : Type ?u.14756} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup f: β → α
f = s₁: Finset β
s₁.sup: {α : Type ?u.14791} → {β : Type ?u.14790} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup f: β → α
f ⊔ s₂: Finset β
s₂.sup: {α : Type ?u.14854} → {β : Type ?u.14853} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup f: β → α
f :=
  Finset.induction_on: ∀ {α : Type ?u.14931} {p : Finset α → Prop} [inst : DecidableEq α] (s : Finset α),
  p ∅ → (∀ ⦃a : α⦄ {s : Finset α}, ¬a ∈ s → p s → p (insert a s)) → p s
Finset.induction_on s₁: Finset β
s₁
    (by
Goals accomplished! 🐙 F: Type ?u.14245

α: Type u_2

β: Type u_1

γ: Type ?u.14254

ι: Type ?u.14257

κ: Type ?u.14260

inst✝²: SemilatticeSup α

inst✝¹: OrderBot α

s, s₁, s₂: Finset β

f, g: β → α

a: α

inst✝: DecidableEq β

sup (∅ ∪ s₂) f = sup ∅ f ⊔ sup s₂ frw [F: Type ?u.14245

α: Type u_2

β: Type u_1

γ: Type ?u.14254

ι: Type ?u.14257

κ: Type ?u.14260

inst✝²: SemilatticeSup α

inst✝¹: OrderBot α

s, s₁, s₂: Finset β

f, g: β → α

a: α

inst✝: DecidableEq β

sup (∅ ∪ s₂) f = sup ∅ f ⊔ sup s₂ fempty_union: ∀ {α : Type ?u.15013} [inst : DecidableEq α] (s : Finset α), ∅ ∪ s = s
empty_union,F: Type ?u.14245

α: Type u_2

β: Type u_1

γ: Type ?u.14254

ι: Type ?u.14257

κ: Type ?u.14260

inst✝²: SemilatticeSup α

inst✝¹: OrderBot α

s, s₁, s₂: Finset β

f, g: β → α

a: α

inst✝: DecidableEq β

sup s₂ f = sup ∅ f ⊔ sup s₂ f F: Type ?u.14245

α: Type u_2

β: Type u_1

γ: Type ?u.14254

ι: Type ?u.14257

κ: Type ?u.14260

inst✝²: SemilatticeSup α

inst✝¹: OrderBot α

s, s₁, s₂: Finset β

f, g: β → α

a: α

inst✝: DecidableEq β

sup (∅ ∪ s₂) f = sup ∅ f ⊔ sup s₂ fsup_empty: ∀ {α : Type ?u.15148} {β : Type ?u.15149} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {f : β → α}, sup ∅ f = ⊥
sup_empty,F: Type ?u.14245

α: Type u_2

β: Type u_1

γ: Type ?u.14254

ι: Type ?u.14257

κ: Type ?u.14260

inst✝²: SemilatticeSup α

inst✝¹: OrderBot α

s, s₁, s₂: Finset β

f, g: β → α

a: α

inst✝: DecidableEq β

sup s₂ f = ⊥ ⊔ sup s₂ f F: Type ?u.14245

α: Type u_2

β: Type u_1

γ: Type ?u.14254

ι: Type ?u.14257

κ: Type ?u.14260

inst✝²: SemilatticeSup α

inst✝¹: OrderBot α

s, s₁, s₂: Finset β

f, g: β → α

a: α

inst✝: DecidableEq β

sup (∅ ∪ s₂) f = sup ∅ f ⊔ sup s₂ fbot_sup_eq: ∀ {α : Type ?u.15272} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {a : α}, ⊥ ⊔ a = a
bot_sup_eqF: Type ?u.14245

α: Type u_2

β: Type u_1

γ: Type ?u.14254

ι: Type ?u.14257

κ: Type ?u.14260

inst✝²: SemilatticeSup α

inst✝¹: OrderBot α

s, s₁, s₂: Finset β

f, g: β → α

a: α

inst✝: DecidableEq β

sup s₂ f = sup s₂ f]
Goals accomplished! 🐙)
    (fun a: ?m.14996
a s: ?m.14999
s _: ?m.15002
_ ih: ?m.15005
ih => by
Goals accomplished! 🐙 F: Type ?u.14245

α: Type u_2

β: Type u_1

γ: Type ?u.14254

ι: Type ?u.14257

κ: Type ?u.14260

inst✝²: SemilatticeSup α

inst✝¹: OrderBot α

s✝, s₁, s₂: Finset β

f, g: β → α

a✝: α

inst✝: DecidableEq β

a: β

s: Finset β

x✝: ¬a ∈ s

ih: sup (s ∪ s₂) f = sup s f ⊔ sup s₂ f

sup (insert a s ∪ s₂) f = sup (insert a s) f ⊔ sup s₂ frw [F: Type ?u.14245

α: Type u_2

β: Type u_1

γ: Type ?u.14254

ι: Type ?u.14257

κ: Type ?u.14260

inst✝²: SemilatticeSup α

inst✝¹: OrderBot α

s✝, s₁, s₂: Finset β

f, g: β → α

a✝: α

inst✝: DecidableEq β

a: β

s: Finset β

x✝: ¬a ∈ s

ih: sup (s ∪ s₂) f = sup s f ⊔ sup s₂ f

sup (insert a s ∪ s₂) f = sup (insert a s) f ⊔ sup s₂ finsert_union: ∀ {α : Type ?u.15393} [inst : DecidableEq α] (a : α) (s t : Finset α), insert a s ∪ t = insert a (s ∪ t)
insert_union,F: Type ?u.14245

α: Type u_2

β: Type u_1

γ: Type ?u.14254

ι: Type ?u.14257

κ: Type ?u.14260

inst✝²: SemilatticeSup α

inst✝¹: OrderBot α

s✝, s₁, s₂: Finset β

f, g: β → α

a✝: α

inst✝: DecidableEq β

a: β

s: Finset β

x✝: ¬a ∈ s

ih: sup (s ∪ s₂) f = sup s f ⊔ sup s₂ f

sup (insert a (s ∪ s₂)) f = sup (insert a s) f ⊔ sup s₂ f F: Type ?u.14245

α: Type u_2

β: Type u_1

γ: Type ?u.14254

ι: Type ?u.14257

κ: Type ?u.14260

inst✝²: SemilatticeSup α

inst✝¹: OrderBot α

s✝, s₁, s₂: Finset β

f, g: β → α

a✝: α

inst✝: DecidableEq β

a: β

s: Finset β

x✝: ¬a ∈ s

ih: sup (s ∪ s₂) f = sup s f ⊔ sup s₂ f

sup (insert a s ∪ s₂) f = sup (insert a s) f ⊔ sup s₂ fsup_insert: ∀ {α : Type ?u.15530} {β : Type ?u.15529} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α}
  [inst_2 : DecidableEq β] {b : β}, sup (insert b s) f = f b ⊔ sup s f
sup_insert,F: Type ?u.14245

α: Type u_2

β: Type u_1

γ: Type ?u.14254

ι: Type ?u.14257

κ: Type ?u.14260

inst✝²: SemilatticeSup α

inst✝¹: OrderBot α

s✝, s₁, s₂: Finset β

f, g: β → α

a✝: α

inst✝: DecidableEq β

a: β

s: Finset β

x✝: ¬a ∈ s

ih: sup (s ∪ s₂) f = sup s f ⊔ sup s₂ f

f a ⊔ sup (s ∪ s₂) f = sup (insert a s) f ⊔ sup s₂ f F: Type ?u.14245

α: Type u_2

β: Type u_1

γ: Type ?u.14254

ι: Type ?u.14257

κ: Type ?u.14260

inst✝²: SemilatticeSup α

inst✝¹: OrderBot α

s✝, s₁, s₂: Finset β

f, g: β → α

a✝: α

inst✝: DecidableEq β

a: β

s: Finset β

x✝: ¬a ∈ s

ih: sup (s ∪ s₂) f = sup s f ⊔ sup s₂ f

sup (insert a s ∪ s₂) f = sup (insert a s) f ⊔ sup s₂ fsup_insert: ∀ {α : Type ?u.15748} {β : Type ?u.15747} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α}
  [inst_2 : DecidableEq β] {b : β}, sup (insert b s) f = f b ⊔ sup s f
sup_insert,F: Type ?u.14245

α: Type u_2

β: Type u_1

γ: Type ?u.14254

ι: Type ?u.14257

κ: Type ?u.14260

inst✝²: SemilatticeSup α

inst✝¹: OrderBot α

s✝, s₁, s₂: Finset β

f, g: β → α

a✝: α

inst✝: DecidableEq β

a: β

s: Finset β

x✝: ¬a ∈ s

ih: sup (s ∪ s₂) f = sup s f ⊔ sup s₂ f

f a ⊔ sup (s ∪ s₂) f = f a ⊔ sup s f ⊔ sup s₂ f F: Type ?u.14245

α: Type u_2

β: Type u_1

γ: Type ?u.14254

ι: Type ?u.14257

κ: Type ?u.14260

inst✝²: SemilatticeSup α

inst✝¹: OrderBot α

s✝, s₁, s₂: Finset β

f, g: β → α

a✝: α

inst✝: DecidableEq β

a: β

s: Finset β

x✝: ¬a ∈ s

ih: sup (s ∪ s₂) f = sup s f ⊔ sup s₂ f

sup (insert a s ∪ s₂) f = sup (insert a s) f ⊔ sup s₂ fih: sup (s ∪ s₂) f = sup s f ⊔ sup s₂ f
ih,F: Type ?u.14245

α: Type u_2

β: Type u_1

γ: Type ?u.14254

ι: Type ?u.14257

κ: Type ?u.14260

inst✝²: SemilatticeSup α

inst✝¹: OrderBot α

s✝, s₁, s₂: Finset β

f, g: β → α

a✝: α

inst✝: DecidableEq β

a: β

s: Finset β

x✝: ¬a ∈ s

ih: sup (s ∪ s₂) f = sup s f ⊔ sup s₂ f

f a ⊔ (sup s f ⊔ sup s₂ f) = f a ⊔ sup s f ⊔ sup s₂ f F: Type ?u.14245

α: Type u_2

β: Type u_1

γ: Type ?u.14254

ι: Type ?u.14257

κ: Type ?u.14260

inst✝²: SemilatticeSup α

inst✝¹: OrderBot α

s✝, s₁, s₂: Finset β

f, g: β → α

a✝: α

inst✝: DecidableEq β

a: β

s: Finset β

x✝: ¬a ∈ s

ih: sup (s ∪ s₂) f = sup s f ⊔ sup s₂ f

sup (insert a s ∪ s₂) f = sup (insert a s) f ⊔ sup s₂ fsup_assoc: ∀ {α : Type ?u.15979} [inst : SemilatticeSup α] {a b c : α}, a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
sup_assocF: Type ?u.14245

α: Type u_2

β: Type u_1

γ: Type ?u.14254

ι: Type ?u.14257

κ: Type ?u.14260

inst✝²: SemilatticeSup α

inst✝¹: OrderBot α

s✝, s₁, s₂: Finset β

f, g: β → α

a✝: α

inst✝: DecidableEq β

a: β

s: Finset β

x✝: ¬a ∈ s

ih: sup (s ∪ s₂) f = sup s f ⊔ sup s₂ f

f a ⊔ (sup s f ⊔ sup s₂ f) = f a ⊔ (sup s f ⊔ sup s₂ f)]
Goals accomplished! 🐙)
#align finset.sup_union Finset.sup_union: ∀ {α : Type u_2} {β : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s₁ s₂ : Finset β} {f : β → α}
  [inst_2 : DecidableEq β], sup (s₁ ∪ s₂) f = sup s₁ f ⊔ sup s₂ f
Finset.sup_union

theorem sup_sup: ∀ {α : Type u_1} {β : Type u_2} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f g : β → α},
  sup s (f ⊔ g) = sup s f ⊔ sup s g
sup_sup : s: Finset β
s.sup: {α : Type ?u.16613} → {β : Type ?u.16612} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup (f: β → α
f ⊔ g: β → α
g) = s: Finset β
s.sup: {α : Type ?u.16709} → {β : Type ?u.16708} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup f: β → α
f ⊔ s: Finset β
s.sup: {α : Type ?u.16772} → {β : Type ?u.16771} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup g: β → α
g := by
Goals accomplished! 🐙
  F: Type ?u.16149

α: Type u_1

β: Type u_2

γ: Type ?u.16158

ι: Type ?u.16161

κ: Type ?u.16164

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s, s₁, s₂: Finset β

f, g: β → α

a: α

sup s (f ⊔ g) = sup s f ⊔ sup s grefine' Finset.cons_induction_on: ∀ {α : Type ?u.16844} {p : Finset α → Prop} (s : Finset α),
  p ∅ → (∀ ⦃a : α⦄ {s : Finset α} (h : ¬a ∈ s), p s → p (cons a s h)) → p s
Finset.cons_induction_on s: Finset β
s _: sup ∅ (f ⊔ g) = sup ∅ f ⊔ sup ∅ g
_ fun b: ?m.16875
b t: ?m.16878
t _: ?m.16881
_ h: ?m.16884
h => _: sup (cons b t x✝) (f ⊔ g) = sup (cons b t x✝) f ⊔ sup (cons b t x✝) g
_F: Type ?u.16149

α: Type u_1

β: Type u_2

γ: Type ?u.16158

ι: Type ?u.16161

κ: Type ?u.16164

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s, s₁, s₂: Finset β

f, g: β → α

a: α

refine'_1sup ∅ (f ⊔ g) = sup ∅ f ⊔ sup ∅ g
F: Type ?u.16149

α: Type u_1

β: Type u_2

γ: Type ?u.16158

ι: Type ?u.16161

κ: Type ?u.16164

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s, s₁, s₂: Finset β

f, g: β → α

a: α

b: β

t: Finset β

x✝: ¬b ∈ t

h: sup t (f ⊔ g) = sup t f ⊔ sup t g

refine'_2sup (cons b t x✝) (f ⊔ g) = sup (cons b t x✝) f ⊔ sup (cons b t x✝) g
  F: Type ?u.16149

α: Type u_1

β: Type u_2

γ: Type ?u.16158

ι: Type ?u.16161

κ: Type ?u.16164

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s, s₁, s₂: Finset β

f, g: β → α

a: α

sup s (f ⊔ g) = sup s f ⊔ sup s g·F: Type ?u.16149

α: Type u_1

β: Type u_2

γ: Type ?u.16158

ι: Type ?u.16161

κ: Type ?u.16164

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s, s₁, s₂: Finset β

f, g: β → α

a: α

refine'_1sup ∅ (f ⊔ g) = sup ∅ f ⊔ sup ∅ g F: Type ?u.16149

α: Type u_1

β: Type u_2

γ: Type ?u.16158

ι: Type ?u.16161

κ: Type ?u.16164

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s, s₁, s₂: Finset β

f, g: β → α

a: α

refine'_1sup ∅ (f ⊔ g) = sup ∅ f ⊔ sup ∅ g
F: Type ?u.16149

α: Type u_1

β: Type u_2

γ: Type ?u.16158

ι: Type ?u.16161

κ: Type ?u.16164

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s, s₁, s₂: Finset β

f, g: β → α

a: α

b: β

t: Finset β

x✝: ¬b ∈ t

h: sup t (f ⊔ g) = sup t f ⊔ sup t g

refine'_2sup (cons b t x✝) (f ⊔ g) = sup (cons b t x✝) f ⊔ sup (cons b t x✝) grw [F: Type ?u.16149

α: Type u_1

β: Type u_2

γ: Type ?u.16158

ι: Type ?u.16161

κ: Type ?u.16164

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s, s₁, s₂: Finset β

f, g: β → α

a: α

refine'_1sup ∅ (f ⊔ g) = sup ∅ f ⊔ sup ∅ gsup_empty: ∀ {α : Type ?u.16892} {β : Type ?u.16893} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {f : β → α}, sup ∅ f = ⊥
sup_empty,F: Type ?u.16149

α: Type u_1

β: Type u_2

γ: Type ?u.16158

ι: Type ?u.16161

κ: Type ?u.16164

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s, s₁, s₂: Finset β

f, g: β → α

a: α

refine'_1⊥ = sup ∅ f ⊔ sup ∅ g F: Type ?u.16149

α: Type u_1

β: Type u_2

γ: Type ?u.16158

ι: Type ?u.16161

κ: Type ?u.16164

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s, s₁, s₂: Finset β

f, g: β → α

a: α

refine'_1sup ∅ (f ⊔ g) = sup ∅ f ⊔ sup ∅ gsup_empty: ∀ {α : Type ?u.17024} {β : Type ?u.17025} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {f : β → α}, sup ∅ f = ⊥
sup_empty,F: Type ?u.16149

α: Type u_1

β: Type u_2

γ: Type ?u.16158

ι: Type ?u.16161

κ: Type ?u.16164

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s, s₁, s₂: Finset β

f, g: β → α

a: α

refine'_1⊥ = ⊥ ⊔ sup ∅ g F: Type ?u.16149

α: Type u_1

β: Type u_2

γ: Type ?u.16158

ι: Type ?u.16161

κ: Type ?u.16164

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s, s₁, s₂: Finset β

f, g: β → α

a: α

refine'_1sup ∅ (f ⊔ g) = sup ∅ f ⊔ sup ∅ gsup_empty: ∀ {α : Type ?u.17128} {β : Type ?u.17129} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {f : β → α}, sup ∅ f = ⊥
sup_empty,F: Type ?u.16149

α: Type u_1

β: Type u_2

γ: Type ?u.16158

ι: Type ?u.16161

κ: Type ?u.16164

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s, s₁, s₂: Finset β

f, g: β → α

a: α

refine'_1⊥ = ⊥ ⊔ ⊥ F: Type ?u.16149

α: Type u_1

β: Type u_2

γ: Type ?u.16158

ι: Type ?u.16161

κ: Type ?u.16164

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s, s₁, s₂: Finset β

f, g: β → α

a: α

refine'_1sup ∅ (f ⊔ g) = sup ∅ f ⊔ sup ∅ gbot_sup_eq: ∀ {α : Type ?u.17232} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {a : α}, ⊥ ⊔ a = a
bot_sup_eqF: Type ?u.16149

α: Type u_1

β: Type u_2

γ: Type ?u.16158

ι: Type ?u.16161

κ: Type ?u.16164

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s, s₁, s₂: Finset β

f, g: β → α

a: α

refine'_1⊥ = ⊥]
Goals accomplished! 🐙
  F: Type ?u.16149

α: Type u_1

β: Type u_2

γ: Type ?u.16158

ι: Type ?u.16161

κ: Type ?u.16164

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s, s₁, s₂: Finset β

f, g: β → α

a: α

sup s (f ⊔ g) = sup s f ⊔ sup s g·F: Type ?u.16149

α: Type u_1

β: Type u_2

γ: Type ?u.16158

ι: Type ?u.16161

κ: Type ?u.16164

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s, s₁, s₂: Finset β

f, g: β → α

a: α

b: β

t: Finset β

x✝: ¬b ∈ t

h: sup t (f ⊔ g) = sup t f ⊔ sup t g

refine'_2sup (cons b t x✝) (f ⊔ g) = sup (cons b t x✝) f ⊔ sup (cons b t x✝) g F: Type ?u.16149

α: Type u_1

β: Type u_2

γ: Type ?u.16158

ι: Type ?u.16161

κ: Type ?u.16164

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s, s₁, s₂: Finset β

f, g: β → α

a: α

b: β

t: Finset β

x✝: ¬b ∈ t

h: sup t (f ⊔ g) = sup t f ⊔ sup t g

refine'_2sup (cons b t x✝) (f ⊔ g) = sup (cons b t x✝) f ⊔ sup (cons b t x✝) grw [F: Type ?u.16149

α: Type u_1

β: Type u_2

γ: Type ?u.16158

ι: Type ?u.16161

κ: Type ?u.16164

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s, s₁, s₂: Finset β

f, g: β → α

a: α

b: β

t: Finset β

x✝: ¬b ∈ t

h: sup t (f ⊔ g) = sup t f ⊔ sup t g

refine'_2sup (cons b t x✝) (f ⊔ g) = sup (cons b t x✝) f ⊔ sup (cons b t x✝) gsup_cons: ∀ {α : Type ?u.17354} {β : Type ?u.17353} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α}
  {b : β} (h : ¬b ∈ s), sup (cons b s h) f = f b ⊔ sup s f
sup_cons,F: Type ?u.16149

α: Type u_1

β: Type u_2

γ: Type ?u.16158

ι: Type ?u.16161

κ: Type ?u.16164

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s, s₁, s₂: Finset β

f, g: β → α

a: α

b: β

t: Finset β

x✝: ¬b ∈ t

h: sup t (f ⊔ g) = sup t f ⊔ sup t g

refine'_2(f ⊔ g) b ⊔ sup t (f ⊔ g) = sup (cons b t x✝) f ⊔ sup (cons b t x✝) g F: Type ?u.16149

α: Type u_1

β: Type u_2

γ: Type ?u.16158

ι: Type ?u.16161

κ: Type ?u.16164

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s, s₁, s₂: Finset β

f, g: β → α

a: α

b: β

t: Finset β

x✝: ¬b ∈ t

h: sup t (f ⊔ g) = sup t f ⊔ sup t g

refine'_2sup (cons b t x✝) (f ⊔ g) = sup (cons b t x✝) f ⊔ sup (cons b t x✝) gsup_cons: ∀ {α : Type ?u.17471} {β : Type ?u.17470} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α}
  {b : β} (h : ¬b ∈ s), sup (cons b s h) f = f b ⊔ sup s f
sup_cons,F: Type ?u.16149

α: Type u_1

β: Type u_2

γ: Type ?u.16158

ι: Type ?u.16161

κ: Type ?u.16164

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s, s₁, s₂: Finset β

f, g: β → α

a: α

b: β

t: Finset β

x✝: ¬b ∈ t

h: sup t (f ⊔ g) = sup t f ⊔ sup t g

refine'_2(f ⊔ g) b ⊔ sup t (f ⊔ g) = f b ⊔ sup t f ⊔ sup (cons b t x✝) g F: Type ?u.16149

α: Type u_1

β: Type u_2

γ: Type ?u.16158

ι: Type ?u.16161

κ: Type ?u.16164

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s, s₁, s₂: Finset β

f, g: β → α

a: α

b: β

t: Finset β

x✝: ¬b ∈ t

h: sup t (f ⊔ g) = sup t f ⊔ sup t g

refine'_2sup (cons b t x✝) (f ⊔ g) = sup (cons b t x✝) f ⊔ sup (cons b t x✝) gsup_cons: ∀ {α : Type ?u.17582} {β : Type ?u.17581} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α}
  {b : β} (h : ¬b ∈ s), sup (cons b s h) f = f b ⊔ sup s f
sup_cons,F: Type ?u.16149

α: Type u_1

β: Type u_2

γ: Type ?u.16158

ι: Type ?u.16161

κ: Type ?u.16164

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s, s₁, s₂: Finset β

f, g: β → α

a: α

b: β

t: Finset β

x✝: ¬b ∈ t

h: sup t (f ⊔ g) = sup t f ⊔ sup t g

refine'_2(f ⊔ g) b ⊔ sup t (f ⊔ g) = f b ⊔ sup t f ⊔ (g b ⊔ sup t g) F: Type ?u.16149

α: Type u_1

β: Type u_2

γ: Type ?u.16158

ι: Type ?u.16161

κ: Type ?u.16164

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s, s₁, s₂: Finset β

f, g: β → α

a: α

b: β

t: Finset β

x✝: ¬b ∈ t

h: sup t (f ⊔ g) = sup t f ⊔ sup t g

refine'_2sup (cons b t x✝) (f ⊔ g) = sup (cons b t x✝) f ⊔ sup (cons b t x✝) gh: ?m.16884
hF: Type ?u.16149

α: Type u_1

β: Type u_2

γ: Type ?u.16158

ι: Type ?u.16161

κ: Type ?u.16164

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s, s₁, s₂: Finset β

f, g: β → α

a: α

b: β

t: Finset β

x✝: ¬b ∈ t

h: sup t (f ⊔ g) = sup t f ⊔ sup t g

refine'_2(f ⊔ g) b ⊔ (sup t f ⊔ sup t g) = f b ⊔ sup t f ⊔ (g b ⊔ sup t g)]F: Type ?u.16149

α: Type u_1

β: Type u_2

γ: Type ?u.16158

ι: Type ?u.16161

κ: Type ?u.16164

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s, s₁, s₂: Finset β

f, g: β → α

a: α

b: β

t: Finset β

x✝: ¬b ∈ t

h: sup t (f ⊔ g) = sup t f ⊔ sup t g

refine'_2(f ⊔ g) b ⊔ (sup t f ⊔ sup t g) = f b ⊔ sup t f ⊔ (g b ⊔ sup t g)
    F: Type ?u.16149

α: Type u_1

β: Type u_2

γ: Type ?u.16158

ι: Type ?u.16161

κ: Type ?u.16164

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s, s₁, s₂: Finset β

f, g: β → α

a: α

b: β

t: Finset β

x✝: ¬b ∈ t

h: sup t (f ⊔ g) = sup t f ⊔ sup t g

refine'_2sup (cons b t x✝) (f ⊔ g) = sup (cons b t x✝) f ⊔ sup (cons b t x✝) gexact sup_sup_sup_comm: ∀ {α : Type ?u.17712} [inst : SemilatticeSup α] (a b c d : α), a ⊔ b ⊔ (c ⊔ d) = a ⊔ c ⊔ (b ⊔ d)
sup_sup_sup_comm _: ?m.17713
_ _: ?m.17713
_ _: ?m.17713
_ _: ?m.17713
_
Goals accomplished! 🐙
#align finset.sup_sup Finset.sup_sup: ∀ {α : Type u_1} {β : Type u_2} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f g : β → α},
  sup s (f ⊔ g) = sup s f ⊔ sup s g
Finset.sup_sup

theorem sup_congr: ∀ {α : Type u_2} {β : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s₁ s₂ : Finset β} {f g : β → α},
  s₁ = s₂ → (∀ (a : β), a ∈ s₂ → f a = g a) → sup s₁ f = sup s₂ g
sup_congr {f: β → α
f g: β → α
g : β: Type ?u.17786
β → α: Type ?u.17783
α} (hs: s₁ = s₂
hs : s₁: Finset β
s₁ = s₂: Finset β
s₂) (hfg: ∀ (a : β), a ∈ s₂ → f a = g a
hfg : ∀ a: ?m.18256
a ∈ s₂: Finset β
s₂, f: β → α
f a: ?m.18256
a = g: β → α
g a: ?m.18256
a) :
    s₁: Finset β
s₁.sup: {α : Type ?u.18295} → {β : Type ?u.18294} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup f: β → α
f = s₂: Finset β
s₂.sup: {α : Type ?u.18326} → {β : Type ?u.18325} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup g: β → α
g := by
Goals accomplished! 🐙
  F: Type ?u.17780

α: Type u_2

β: Type u_1

γ: Type ?u.17789

ι: Type ?u.17792

κ: Type ?u.17795

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s, s₁, s₂: Finset β

f✝, g✝: β → α

a: α

f, g: β → α

hs: s₁ = s₂

hfg: ∀ (a : β), a ∈ s₂ → f a = g a

sup s₁ f = sup s₂ gsubst hs: s₁ = s₂
hsF: Type ?u.17780

α: Type u_2

β: Type u_1

γ: Type ?u.17789

ι: Type ?u.17792

κ: Type ?u.17795

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s, s₁: Finset β

f✝, g✝: β → α

a: α

f, g: β → α

hfg: ∀ (a : β), a ∈ s₁ → f a = g a

sup s₁ f = sup s₁ g
  F: Type ?u.17780

α: Type u_2

β: Type u_1

γ: Type ?u.17789

ι: Type ?u.17792

κ: Type ?u.17795

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s, s₁, s₂: Finset β

f✝, g✝: β → α

a: α

f, g: β → α

hs: s₁ = s₂

hfg: ∀ (a : β), a ∈ s₂ → f a = g a

sup s₁ f = sup s₂ gexact Finset.fold_congr: ∀ {α : Type ?u.18364} {β : Type ?u.18365} {op : β → β → β} [hc : IsCommutative β op] [ha : IsAssociative β op]
  {f : α → β} {b : β} {s : Finset α} {g : α → β}, (∀ (x : α), x ∈ s → f x = g x) → fold op b f s = fold op b g s
Finset.fold_congr hfg: ∀ (a : β), a ∈ s₁ → f a = g a
hfg
Goals accomplished! 🐙
#align finset.sup_congr Finset.sup_congr: ∀ {α : Type u_2} {β : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s₁ s₂ : Finset β} {f g : β → α},
  s₁ = s₂ → (∀ (a : β), a ∈ s₂ → f a = g a) → sup s₁ f = sup s₂ g
Finset.sup_congr

@[simp]
theorem _root_.map_finset_sup: ∀ {F : Type u_2} {α : Type u_3} {β : Type u_1} {ι : Type u_4} [inst : SemilatticeSup α] [inst_1 : OrderBot α]
  [inst_2 : SemilatticeSup β] [inst_3 : OrderBot β] [inst_4 : SupBotHomClass F α β] (f : F) (s : Finset ι) (g : ι → α),
  ↑f (sup s g) = sup s (↑f ∘ g)
_root_.map_finset_sup [SemilatticeSup: Type ?u.18963 → Type ?u.18963
SemilatticeSup β: Type ?u.18507
β] [OrderBot: (α : Type ?u.18966) → [inst : LE α] → Type ?u.18966
OrderBot β: Type ?u.18507
β] [SupBotHomClass: Type ?u.19390 →
  (α : outParam (Type ?u.19389)) →
    (β : outParam (Type ?u.19388)) →
      [inst : Sup α] → [inst : Sup β] → [inst : Bot α] → [inst : Bot β] → Type (max(max?u.19390?u.19389)?u.19388)
SupBotHomClass F: Type ?u.18501
F α: Type ?u.18504
α β: Type ?u.18507
β] (f: F
f : F: Type ?u.18501
F)
    (s: Finset ι
s : Finset: Type ?u.20234 → Type ?u.20234
Finset ι: Type ?u.18513
ι) (g: ι → α
g : ι: Type ?u.18513
ι → α: Type ?u.18504
α) : f: F
f (s: Finset ι
s.sup: {α : Type ?u.23665} → {β : Type ?u.23664} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup g: ι → α
g) = s: Finset ι
s.sup: {α : Type ?u.23739} → {β : Type ?u.23738} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup (f: F
f ∘ g: ι → α
g) :=
  Finset.cons_induction_on: ∀ {α : Type ?u.27117} {p : Finset α → Prop} (s : Finset α),
  p ∅ → (∀ ⦃a : α⦄ {s : Finset α} (h : ¬a ∈ s), p s → p (cons a s h)) → p s
Finset.cons_induction_on s: Finset ι
s (map_bot: ∀ {F : Type ?u.27150} {α : outParam (Type ?u.27149)} {β : outParam (Type ?u.27148)} [inst : Bot α] [inst_1 : Bot β]
  [self : BotHomClass F α β] (f : F), ↑f ⊥ = ⊥
map_bot f: F
f) fun i: ?m.28234
i s: ?m.28237
s _: ?m.28240
_ h: ?m.28243
h => by
Goals accomplished! 🐙
    F: Type u_2

α: Type u_3

β: Type u_1

γ: Type ?u.18510

ι: Type u_4

κ: Type ?u.18516

inst✝⁴: SemilatticeSup α

inst✝³: OrderBot α

s✝¹, s₁, s₂: Finset β

f✝, g✝: β → α

a: α

inst✝²: SemilatticeSup β

inst✝¹: OrderBot β

inst✝: SupBotHomClass F α β

f: F

s✝: Finset ι

g: ι → α

i: ι

s: Finset ι

x✝: ¬i ∈ s

h: ↑f (sup s g) = sup s (↑f ∘ g)

↑f (sup (cons i s x✝) g) = sup (cons i s x✝) (↑f ∘ g)rw [F: Type u_2

α: Type u_3

β: Type u_1

γ: Type ?u.18510

ι: Type u_4

κ: Type ?u.18516

inst✝⁴: SemilatticeSup α

inst✝³: OrderBot α

s✝¹, s₁, s₂: Finset β

f✝, g✝: β → α

a: α

inst✝²: SemilatticeSup β

inst✝¹: OrderBot β

inst✝: SupBotHomClass F α β

f: F

s✝: Finset ι

g: ι → α

i: ι

s: Finset ι

x✝: ¬i ∈ s

h: ↑f (sup s g) = sup s (↑f ∘ g)

↑f (sup (cons i s x✝) g) = sup (cons i s x✝) (↑f ∘ g)sup_cons: ∀ {α : Type ?u.28252} {β : Type ?u.28251} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α}
  {b : β} (h : ¬b ∈ s), sup (cons b s h) f = f b ⊔ sup s f
sup_cons,F: Type u_2

α: Type u_3

β: Type u_1

γ: Type ?u.18510

ι: Type u_4

κ: Type ?u.18516

inst✝⁴: SemilatticeSup α

inst✝³: OrderBot α

s✝¹, s₁, s₂: Finset β

f✝, g✝: β → α

a: α

inst✝²: SemilatticeSup β

inst✝¹: OrderBot β

inst✝: SupBotHomClass F α β

f: F

s✝: Finset ι

g: ι → α

i: ι

s: Finset ι

x✝: ¬i ∈ s

h: ↑f (sup s g) = sup s (↑f ∘ g)

↑f (g i ⊔ sup s g) = sup (cons i s x✝) (↑f ∘ g) F: Type u_2

α: Type u_3

β: Type u_1

γ: Type ?u.18510

ι: Type u_4

κ: Type ?u.18516

inst✝⁴: SemilatticeSup α

inst✝³: OrderBot α

s✝¹, s₁, s₂: Finset β

f✝, g✝: β → α

a: α

inst✝²: SemilatticeSup β

inst✝¹: OrderBot β

inst✝: SupBotHomClass F α β

f: F

s✝: Finset ι

g: ι → α

i: ι

s: Finset ι

x✝: ¬i ∈ s

h: ↑f (sup s g) = sup s (↑f ∘ g)

↑f (sup (cons i s x✝) g) = sup (cons i s x✝) (↑f ∘ g)sup_cons: ∀ {α : Type ?u.28401} {β : Type ?u.28400} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α}
  {b : β} (h : ¬b ∈ s), sup (cons b s h) f = f b ⊔ sup s f
sup_cons,F: Type u_2

α: Type u_3

β: Type u_1

γ: Type ?u.18510

ι: Type u_4

κ: Type ?u.18516

inst✝⁴: SemilatticeSup α

inst✝³: OrderBot α

s✝¹, s₁, s₂: Finset β

f✝, g✝: β → α

a: α

inst✝²: SemilatticeSup β

inst✝¹: OrderBot β

inst✝: SupBotHomClass F α β

f: F

s✝: Finset ι

g: ι → α

i: ι

s: Finset ι

x✝: ¬i ∈ s

h: ↑f (sup s g) = sup s (↑f ∘ g)

↑f (g i ⊔ sup s g) = (↑f ∘ g) i ⊔ sup s (↑f ∘ g) F: Type u_2

α: Type u_3

β: Type u_1

γ: Type ?u.18510

ι: Type u_4

κ: Type ?u.18516

inst✝⁴: SemilatticeSup α

inst✝³: OrderBot α

s✝¹, s₁, s₂: Finset β

f✝, g✝: β → α

a: α

inst✝²: SemilatticeSup β

inst✝¹: OrderBot β

inst✝: SupBotHomClass F α β

f: F

s✝: Finset ι

g: ι → α

i: ι

s: Finset ι

x✝: ¬i ∈ s

h: ↑f (sup s g) = sup s (↑f ∘ g)

↑f (sup (cons i s x✝) g) = sup (cons i s x✝) (↑f ∘ g)map_sup: ∀ {F : Type ?u.28524} {α : outParam (Type ?u.28523)} {β : outParam (Type ?u.28522)} [inst : Sup α] [inst_1 : Sup β]
  [self : SupHomClass F α β] (f : F) (a b : α), ↑f (a ⊔ b) = ↑f a ⊔ ↑f b
map_sup,F: Type u_2

α: Type u_3

β: Type u_1

γ: Type ?u.18510

ι: Type u_4

κ: Type ?u.18516

inst✝⁴: SemilatticeSup α

inst✝³: OrderBot α

s✝¹, s₁, s₂: Finset β

f✝, g✝: β → α

a: α

inst✝²: SemilatticeSup β

inst✝¹: OrderBot β

inst✝: SupBotHomClass F α β

f: F

s✝: Finset ι

g: ι → α

i: ι

s: Finset ι

x✝: ¬i ∈ s

h: ↑f (sup s g) = sup s (↑f ∘ g)

↑f (g i) ⊔ ↑f (sup s g) = (↑f ∘ g) i ⊔ sup s (↑f ∘ g) F: Type u_2

α: Type u_3

β: Type u_1

γ: Type ?u.18510

ι: Type u_4

κ: Type ?u.18516

inst✝⁴: SemilatticeSup α

inst✝³: OrderBot α

s✝¹, s₁, s₂: Finset β

f✝, g✝: β → α

a: α

inst✝²: SemilatticeSup β

inst✝¹: OrderBot β

inst✝: SupBotHomClass F α β

f: F

s✝: Finset ι

g: ι → α

i: ι

s: Finset ι

x✝: ¬i ∈ s

h: ↑f (sup s g) = sup s (↑f ∘ g)

↑f (sup (cons i s x✝) g) = sup (cons i s x✝) (↑f ∘ g)h: ↑f (sup s g) = sup s (↑f ∘ g)
h,F: Type u_2

α: Type u_3

β: Type u_1

γ: Type ?u.18510

ι: Type u_4

κ: Type ?u.18516

inst✝⁴: SemilatticeSup α

inst✝³: OrderBot α

s✝¹, s₁, s₂: Finset β

f✝, g✝: β → α

a: α

inst✝²: SemilatticeSup β

inst✝¹: OrderBot β

inst✝: SupBotHomClass F α β

f: F

s✝: Finset ι

g: ι → α

i: ι

s: Finset ι

x✝: ¬i ∈ s

h: ↑f (sup s g) = sup s (↑f ∘ g)

↑f (g i) ⊔ sup s (↑f ∘ g) = (↑f ∘ g) i ⊔ sup s (↑f ∘ g) F: Type u_2

α: Type u_3

β: Type u_1

γ: Type ?u.18510

ι: Type u_4

κ: Type ?u.18516

inst✝⁴: SemilatticeSup α

inst✝³: OrderBot α

s✝¹, s₁, s₂: Finset β

f✝, g✝: β → α

a: α

inst✝²: SemilatticeSup β

inst✝¹: OrderBot β

inst✝: SupBotHomClass F α β

f: F

s✝: Finset ι

g: ι → α

i: ι

s: Finset ι

x✝: ¬i ∈ s

h: ↑f (sup s g) = sup s (↑f ∘ g)

↑f (sup (cons i s x✝) g) = sup (cons i s x✝) (↑f ∘ g)Function.comp_apply: ∀ {β : Sort ?u.33049} {δ : Sort ?u.33050} {α : Sort ?u.33051} {f : β → δ} {g : α → β} {x : α}, (f ∘ g) x = f (g x)
Function.comp_applyF: Type u_2

α: Type u_3

β: Type u_1

γ: Type ?u.18510

ι: Type u_4

κ: Type ?u.18516

inst✝⁴: SemilatticeSup α

inst✝³: OrderBot α

s✝¹, s₁, s₂: Finset β

f✝, g✝: β → α

a: α

inst✝²: SemilatticeSup β

inst✝¹: OrderBot β

inst✝: SupBotHomClass F α β

f: F

s✝: Finset ι

g: ι → α

i: ι

s: Finset ι

x✝: ¬i ∈ s

h: ↑f (sup s g) = sup s (↑f ∘ g)

↑f (g i) ⊔ sup s (↑f ∘ g) = ↑f (g i) ⊔ sup s (↑f ∘ g)]
Goals accomplished! 🐙
#align map_finset_sup map_finset_sup: ∀ {F : Type u_2} {α : Type u_3} {β : Type u_1} {ι : Type u_4} [inst : SemilatticeSup α] [inst_1 : OrderBot α]
  [inst_2 : SemilatticeSup β] [inst_3 : OrderBot β] [inst_4 : SupBotHomClass F α β] (f : F) (s : Finset ι) (g : ι → α),
  ↑f (sup s g) = sup s (↑f ∘ g)
map_finset_sup

@[simp]
protected theorem sup_le_iff: ∀ {α : Type u_1} {β : Type u_2} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α} {a : α},
  sup s f ≤ a ↔ ∀ (b : β), b ∈ s → f b ≤ a
sup_le_iff {a: α
a : α: Type ?u.33151
α} : s: Finset β
s.sup: {α : Type ?u.33614} → {β : Type ?u.33613} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup f: β → α
f ≤ a: α
a ↔ ∀ b: ?m.34064
b ∈ s: Finset β
s, f: β → α
f b: ?m.34064
b ≤ a: α
a := by
Goals accomplished! 🐙
  F: Type ?u.33148

α: Type u_1

β: Type u_2

γ: Type ?u.33157

ι: Type ?u.33160

κ: Type ?u.33163

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s, s₁, s₂: Finset β

f, g: β → α

a✝, a: α

sup s f ≤ a ↔ ∀ (b : β), b ∈ s → f b ≤ aapply Iff.trans: ∀ {a b c : Prop}, (a ↔ b) → (b ↔ c) → (a ↔ c)
Iff.trans Multiset.sup_le: ∀ {α : Type ?u.34109} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Multiset α} {a : α},
  Multiset.sup s ≤ a ↔ ∀ (b : α), b ∈ s → b ≤ a
Multiset.sup_leF: Type ?u.33148

α: Type u_1

β: Type u_2

γ: Type ?u.33157

ι: Type ?u.33160

κ: Type ?u.33163

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s, s₁, s₂: Finset β

f, g: β → α

a✝, a: α

(∀ (b : α), b ∈ Multiset.map f s.val → b ≤ a) ↔ ∀ (b : β), b ∈ s → f b ≤ a
  F: Type ?u.33148

α: Type u_1

β: Type u_2

γ: Type ?u.33157

ι: Type ?u.33160

κ: Type ?u.33163

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s, s₁, s₂: Finset β

f, g: β → α

a✝, a: α

sup s f ≤ a ↔ ∀ (b : β), b ∈ s → f b ≤ asimp only [Multiset.mem_map: ∀ {α : Type ?u.34310} {β : Type ?u.34311} {f : α → β} {b : β} {s : Multiset α},
  b ∈ Multiset.map f s ↔ ∃ a, a ∈ s ∧ f a = b
Multiset.mem_map, and_imp: ∀ {a b c : Prop}, a ∧ b → c ↔ a → b → c
and_imp, exists_imp: ∀ {α : Sort ?u.34360} {p : α → Prop} {b : Prop}, (∃ x, p x) → b ↔ ∀ (x : α), p x → b
exists_imp]F: Type ?u.33148

α: Type u_1

β: Type u_2

γ: Type ?u.33157

ι: Type ?u.33160

κ: Type ?u.33163

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s, s₁, s₂: Finset β

f, g: β → α

a✝, a: α

(∀ (b : α) (x : β), x ∈ s.val → f x = b → b ≤ a) ↔ ∀ (b : β), b ∈ s → f b ≤ a
  F: Type ?u.33148

α: Type u_1

β: Type u_2

γ: Type ?u.33157

ι: Type ?u.33160

κ: Type ?u.33163

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s, s₁, s₂: Finset β

f, g: β → α

a✝, a: α

sup s f ≤ a ↔ ∀ (b : β), b ∈ s → f b ≤ aexact ⟨fun k: ?m.34687
k b: ?m.34694
b hb: ?m.34697
hb => k: ?m.34687
k _: α
_ _: β
_ hb: ?m.34697
hb rfl: ∀ {α : Sort ?u.34713} {a : α}, a = a
rfl, fun k: ?m.34729
k a': ?m.34734
a' b: ?m.34737
b hb: ?m.34740
hb h: ?m.34743
h => h: ?m.34743
h ▸ k: ?m.34729
k _: β
_ hb: ?m.34740
hb⟩
Goals accomplished! 🐙
#align finset.sup_le_iff Finset.sup_le_iff: ∀ {α : Type u_1} {β : Type u_2} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α} {a : α},
  sup s f ≤ a ↔ ∀ (b : β), b ∈ s → f b ≤ a
Finset.sup_le_iff

alias Finset.sup_le_iff: ∀ {α : Type u_1} {β : Type u_2} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α} {a : α},
  sup s f ≤ a ↔ ∀ (b : β), b ∈ s → f b ≤ a
Finset.sup_le_iff ↔ _ sup_le: ∀ {α : Type u_1} {β : Type u_2} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α} {a : α},
  (∀ (b : β), b ∈ s → f b ≤ a) → sup s f ≤ a
sup_le
#align finset.sup_le Finset.sup_le: ∀ {α : Type u_1} {β : Type u_2} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α} {a : α},
  (∀ (b : β), b ∈ s → f b ≤ a) → sup s f ≤ a
Finset.sup_le

-- Porting note: removed `attribute [protected] sup_le`

theorem sup_const_le: (sup s fun x => a) ≤ a
sup_const_le : (s: Finset β
s.sup: {α : Type ?u.35342} → {β : Type ?u.35341} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup fun _: ?m.35355
_ => a: α
a) ≤ a: α
a :=
  Finset.sup_le: ∀ {α : Type ?u.35794} {β : Type ?u.35795} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α}
  {a : α}, (∀ (b : β), b ∈ s → f b ≤ a) → sup s f ≤ a
Finset.sup_le fun _: ?m.35874
_ _: ?m.35877
_ => le_rfl: ∀ {α : Type ?u.35879} [inst : Preorder α] {a : α}, a ≤ a
le_rfl
#align finset.sup_const_le Finset.sup_const_le: ∀ {α : Type u_1} {β : Type u_2} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {a : α},
  (sup s fun x => a) ≤ a
Finset.sup_const_le

theorem le_sup: ∀ {α : Type u_2} {β : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α} {b : β},
  b ∈ s → f b ≤ sup s f
le_sup {b: β
b : β: Type ?u.36350
β} (hb: b ∈ s
hb : b: β
b ∈ s: Finset β
s) : f: β → α
f b: β
b ≤ s: Finset β
s.sup: {α : Type ?u.36839} → {β : Type ?u.36838} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup f: β → α
f :=
  Finset.sup_le_iff: ∀ {α : Type ?u.37292} {β : Type ?u.37293} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α}
  {a : α}, sup s f ≤ a ↔ ∀ (b : β), b ∈ s → f b ≤ a
Finset.sup_le_iff.1: ∀ {a b : Prop}, (a ↔ b) → a → b
1 le_rfl: ∀ {α : Type ?u.37355} [inst : Preorder α] {a : α}, a ≤ a
le_rfl _: ?m.37295
_ hb: b ∈ s
hb
#align finset.le_sup Finset.le_sup: ∀ {α : Type u_2} {β : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α} {b : β},
  b ∈ s → f b ≤ sup s f
Finset.le_sup

theorem le_sup_of_le: ∀ {α : Type u_2} {β : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α} {a : α}
  {b : β}, b ∈ s → a ≤ f b → a ≤ sup s f
le_sup_of_le {b: β
b : β: Type ?u.37961
β} (hb: b ∈ s
hb : b: β
b ∈ s: Finset β
s) (h: a ≤ f b
h : a: α
a ≤ f: β → α
f b: β
b) : a: α
a ≤ s: Finset β
s.sup: {α : Type ?u.38873} → {β : Type ?u.38872} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup f: β → α
f := h: a ≤ f b
h.trans: ∀ {α : Type ?u.38910} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ c
trans <| le_sup: ∀ {α : Type ?u.39340} {β : Type ?u.39339} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α}
  {b : β}, b ∈ s → f b ≤ sup s f
le_sup hb: b ∈ s
hb
#align finset.le_sup_of_le Finset.le_sup_of_le: ∀ {α : Type u_2} {β : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α} {a : α}
  {b : β}, b ∈ s → a ≤ f b → a ≤ sup s f
Finset.le_sup_of_le

@[simp]
theorem sup_biUnion: ∀ [inst : DecidableEq β] (s : Finset γ) (t : γ → Finset β), sup (Finset.biUnion s t) f = sup s fun x => sup (t x) f
sup_biUnion [DecidableEq: Sort ?u.39899 → Sort (max1?u.39899)
DecidableEq β: Type ?u.39443
β] (s: Finset γ
s : Finset: Type ?u.39908 → Type ?u.39908
Finset γ: Type ?u.39446
γ) (t: γ → Finset β
t : γ: Type ?u.39446
γ → Finset: Type ?u.39913 → Type ?u.39913
Finset β: Type ?u.39443
β) :
    (s: Finset γ
s.biUnion: {α : Type ?u.39918} → {β : Type ?u.39917} → [inst : DecidableEq β] → Finset α → (α → Finset β) → Finset β
biUnion t: γ → Finset β
t).sup: {α : Type ?u.39974} → {β : Type ?u.39973} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup f: β → α
f = s: Finset γ
s.sup: {α : Type ?u.40005} → {β : Type ?u.40004} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup fun x: ?m.40017
x => (t: γ → Finset β
t x: ?m.40017
x).sup: {α : Type ?u.40020} → {β : Type ?u.40019} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup f: β → α
f :=
  eq_of_forall_ge_iff: ∀ {α : Type ?u.40092} [inst : PartialOrder α] {a b : α}, (∀ (c : α), a ≤ c ↔ b ≤ c) → a = b
eq_of_forall_ge_iff fun c: ?m.40141
c => by
Goals accomplished! 🐙 F: Type ?u.39437

α: Type u_3

β: Type u_1

γ: Type u_2

ι: Type ?u.39449

κ: Type ?u.39452

inst✝²: SemilatticeSup α

inst✝¹: OrderBot α

s✝, s₁, s₂: Finset β

f, g: β → α

a: α

inst✝: DecidableEq β

s: Finset γ

t: γ → Finset β

c: α

sup (Finset.biUnion s t) f ≤ c ↔ (sup s fun x => sup (t x) f) ≤ csimp [@forall_swap: ∀ {α : Sort ?u.40559} {β : Sort ?u.40560} {p : α → β → Prop}, (∀ (x : α) (y : β), p x y) ↔ ∀ (y : β) (x : α), p x y
forall_swap _: Sort ?u.40559
_ β: Type u_1
β]
Goals accomplished! 🐙
#align finset.sup_bUnion Finset.sup_biUnion: ∀ {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {f : β → α}
  [inst_2 : DecidableEq β] (s : Finset γ) (t : γ → Finset β), sup (Finset.biUnion s t) f = sup s fun x => sup (t x) f
Finset.sup_biUnion

theorem sup_const: ∀ {α : Type u_2} {β : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β},
  Finset.Nonempty s → ∀ (c : α), (sup s fun x => c) = c
sup_const {s: Finset β
s : Finset: Type ?u.46831 → Type ?u.46831
Finset β: Type ?u.46375
β} (h: Finset.Nonempty s
h : s: Finset β
s.Nonempty: {α : Type ?u.46834} → Finset α → Prop
Nonempty) (c: α
c : α: Type ?u.46372
α) : (s: Finset β
s.sup: {α : Type ?u.46845} → {β : Type ?u.46844} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup fun _: ?m.46857
_ => c: α
c) = c: α
c :=
  eq_of_forall_ge_iff: ∀ {α : Type ?u.46882} [inst : PartialOrder α] {a b : α}, (∀ (c : α), a ≤ c ↔ b ≤ c) → a = b
eq_of_forall_ge_iff (fun _: ?m.46931
_ => Finset.sup_le_iff: ∀ {α : Type ?u.46933} {β : Type ?u.46934} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α}
  {a : α}, sup s f ≤ a ↔ ∀ (b : β), b ∈ s → f b ≤ a
Finset.sup_le_iff.trans: ∀ {a b c : Prop}, (a ↔ b) → (b ↔ c) → (a ↔ c)
trans h: Finset.Nonempty s
h.forall_const: ∀ {α : Type ?u.47431} {s : Finset α}, Finset.Nonempty s → ∀ {p : Prop}, (∀ (x : α), x ∈ s → p) ↔ p
forall_const)
#align finset.sup_const Finset.sup_const: ∀ {α : Type u_2} {β : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β},
  Finset.Nonempty s → ∀ (c : α), (sup s fun x => c) = c
Finset.sup_const

@[simp]
theorem sup_bot: ∀ {α : Type u_2} {β : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderBot α] (s : Finset β), (sup s fun x => ⊥) = ⊥
sup_bot (s: Finset β
s : Finset: Type ?u.47931 → Type ?u.47931
Finset β: Type ?u.47475
β) : (s: Finset β
s.sup: {α : Type ?u.47936} → {β : Type ?u.47935} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup fun _: ?m.47949
_ => ⊥: ?m.47952
⊥) = (⊥: ?m.48123
⊥ : α: Type ?u.47472
α) := by
Goals accomplished! 🐙
  F: Type ?u.47469

α: Type u_2

β: Type u_1

γ: Type ?u.47478

ι: Type ?u.47481

κ: Type ?u.47484

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s✝, s₁, s₂: Finset β

f, g: β → α

a: α

s: Finset β

(sup s fun x => ⊥) = ⊥obtain rfl: s = ∅
rflrfl | hs: s = ∅ ∨ Finset.Nonempty s
 | hs: Finset.Nonempty s
hs := s: Finset β
s.eq_empty_or_nonempty: ∀ {α : Type ?u.48690} (s : Finset α), s = ∅ ∨ Finset.Nonempty s
eq_empty_or_nonemptyF: Type ?u.47469

α: Type u_2

β: Type u_1

γ: Type ?u.47478

ι: Type ?u.47481

κ: Type ?u.47484

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s, s₁, s₂: Finset β

f, g: β → α

a: α

inl(sup ∅ fun x => ⊥) = ⊥
F: Type ?u.47469

α: Type u_2

β: Type u_1

γ: Type ?u.47478

ι: Type ?u.47481

κ: Type ?u.47484

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s✝, s₁, s₂: Finset β

f, g: β → α

a: α

s: Finset β

hs: Finset.Nonempty s

inr(sup s fun x => ⊥) = ⊥
  F: Type ?u.47469

α: Type u_2

β: Type u_1

γ: Type ?u.47478

ι: Type ?u.47481

κ: Type ?u.47484

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s✝, s₁, s₂: Finset β

f, g: β → α

a: α

s: Finset β

(sup s fun x => ⊥) = ⊥·F: Type ?u.47469

α: Type u_2

β: Type u_1

γ: Type ?u.47478

ι: Type ?u.47481

κ: Type ?u.47484

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s, s₁, s₂: Finset β

f, g: β → α

a: α

inl(sup ∅ fun x => ⊥) = ⊥ F: Type ?u.47469

α: Type u_2

β: Type u_1

γ: Type ?u.47478

ι: Type ?u.47481

κ: Type ?u.47484

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s, s₁, s₂: Finset β

f, g: β → α

a: α

inl(sup ∅ fun x => ⊥) = ⊥
F: Type ?u.47469

α: Type u_2

β: Type u_1

γ: Type ?u.47478

ι: Type ?u.47481

κ: Type ?u.47484

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s✝, s₁, s₂: Finset β

f, g: β → α

a: α

s: Finset β

hs: Finset.Nonempty s

inr(sup s fun x => ⊥) = ⊥exact sup_empty: ∀ {α : Type ?u.48740} {β : Type ?u.48741} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {f : β → α}, sup ∅ f = ⊥
sup_empty
Goals accomplished! 🐙
  F: Type ?u.47469

α: Type u_2

β: Type u_1

γ: Type ?u.47478

ι: Type ?u.47481

κ: Type ?u.47484

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s✝, s₁, s₂: Finset β

f, g: β → α

a: α

s: Finset β

(sup s fun x => ⊥) = ⊥·F: Type ?u.47469

α: Type u_2

β: Type u_1

γ: Type ?u.47478

ι: Type ?u.47481

κ: Type ?u.47484

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s✝, s₁, s₂: Finset β

f, g: β → α

a: α

s: Finset β

hs: Finset.Nonempty s

inr(sup s fun x => ⊥) = ⊥ F: Type ?u.47469

α: Type u_2

β: Type u_1

γ: Type ?u.47478

ι: Type ?u.47481

κ: Type ?u.47484

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s✝, s₁, s₂: Finset β

f, g: β → α

a: α

s: Finset β

hs: Finset.Nonempty s

inr(sup s fun x => ⊥) = ⊥exact sup_const: ∀ {α : Type ?u.48820} {β : Type ?u.48819} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β},
  Finset.Nonempty s → ∀ (c : α), (sup s fun x => c) = c
sup_const hs: Finset.Nonempty s
hs _: ?m.48821
_
Goals accomplished! 🐙
#align finset.sup_bot Finset.sup_bot: ∀ {α : Type u_2} {β : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderBot α] (s : Finset β), (sup s fun x => ⊥) = ⊥
Finset.sup_bot

theorem sup_ite: ∀ {α : Type u_2} {β : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f g : β → α}
  (p : β → Prop) [inst_2 : DecidablePred p],
  (sup s fun i => if p i then f i else g i) = sup (filter p s) f ⊔ sup (filter (fun i => ¬p i) s) g
sup_ite (p: β → Prop
p : β: Type ?u.48915
β → Prop: Type
Prop) [DecidablePred: {α : Sort ?u.49375} → (α → Prop) → Sort (max1?u.49375)
DecidablePred p: β → Prop
p] :
    (s: Finset β
s.sup: {α : Type ?u.49387} → {β : Type ?u.49386} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup fun i: ?m.49400
i => ite: {α : Sort ?u.49402} → (c : Prop) → [h : Decidable c] → α → α → α
ite (p: β → Prop
p i: ?m.49400
i) (f: β → α
f i: ?m.49400
i) (g: β → α
g i: ?m.49400
i)) = (s: Finset β
s.filter: {α : Type ?u.49432} → (p : α → Prop) → [inst : DecidablePred p] → Finset α → Finset α
filter p: β → Prop
p).sup: {α : Type ?u.49454} → {β : Type ?u.49453} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup f: β → α
f ⊔ (s: Finset β
s.filter: {α : Type ?u.49516} → (p : α → Prop) → [inst : DecidablePred p] → Finset α → Finset α
filter fun i: ?m.49524
i => ¬p: β → Prop
p i: ?m.49524
i).sup: {α : Type ?u.49559} → {β : Type ?u.49558} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup g: β → α
g :=
  fold_ite: ∀ {α : Type ?u.49637} {β : Type ?u.49636} {op : β → β → β} [hc : IsCommutative β op] [ha : IsAssociative β op]
  {f : α → β} {b : β} {s : Finset α} [inst : IsIdempotent β op] {g : α → β} (p : α → Prop) [inst : DecidablePred p],
  fold op b (fun i => if p i then f i else g i) s =     op (fold op b f (filter p s)) (fold op b g (filter (fun i => ¬p i) s))
fold_ite _: ?m.49638 → Prop
_
#align finset.sup_ite Finset.sup_ite: ∀ {α : Type u_2} {β : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f g : β → α}
  (p : β → Prop) [inst_2 : DecidablePred p],
  (sup s fun i => if p i then f i else g i) = sup (filter p s) f ⊔ sup (filter (fun i => ¬p i) s) g
Finset.sup_ite

theorem sup_mono_fun: ∀ {α : Type u_2} {β : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f g : β → α},
  (∀ (b : β), b ∈ s → f b ≤ g b) → sup s f ≤ sup s g
sup_mono_fun {g: β → α
g : β: Type ?u.50010
β → α: Type ?u.50007
α} (h: ∀ (b : β), b ∈ s → f b ≤ g b
h : ∀ b: ?m.50471
b ∈ s: Finset β
s, f: β → α
f b: ?m.50471
b ≤ g: β → α
g b: ?m.50471
b) : s: Finset β
s.sup: {α : Type ?u.50932} → {β : Type ?u.50931} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup f: β → α
f ≤ s: Finset β
s.sup: {α : Type ?u.50961} → {β : Type ?u.50960} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup g: β → α
g :=
  Finset.sup_le: ∀ {α : Type ?u.50984} {β : Type ?u.50985} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α}
  {a : α}, (∀ (b : β), b ∈ s → f b ≤ a) → sup s f ≤ a
Finset.sup_le fun b: ?m.51064
b hb: ?m.51067
hb => le_trans: ∀ {α : Type ?u.51069} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ c
le_trans (h: ∀ (b : β), b ∈ s → f b ≤ g b
h b: ?m.51064
b hb: ?m.51067
hb) (le_sup: ∀ {α : Type ?u.51511} {β : Type ?u.51510} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α}
  {b : β}, b ∈ s → f b ≤ sup s f
le_sup hb: ?m.51067
hb)
#align finset.sup_mono_fun Finset.sup_mono_fun: ∀ {α : Type u_2} {β : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f g : β → α},
  (∀ (b : β), b ∈ s → f b ≤ g b) → sup s f ≤ sup s g
Finset.sup_mono_fun

theorem sup_mono: ∀ {α : Type u_2} {β : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s₁ s₂ : Finset β} {f : β → α},
  s₁ ⊆ s₂ → sup s₁ f ≤ sup s₂ f
sup_mono (h: s₁ ⊆ s₂
h : s₁: Finset β
s₁ ⊆ s₂: Finset β
s₂) : s₁: Finset β
s₁.sup: {α : Type ?u.52090} → {β : Type ?u.52089} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup f: β → α
f ≤ s₂: Finset β
s₂.sup: {α : Type ?u.52121} → {β : Type ?u.52120} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup f: β → α
f :=
  Finset.sup_le: ∀ {α : Type ?u.52556} {β : Type ?u.52557} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α}
  {a : α}, (∀ (b : β), b ∈ s → f b ≤ a) → sup s f ≤ a
Finset.sup_le (fun _: ?m.52636
_ hb: ?m.52639
hb => le_sup: ∀ {α : Type ?u.52642} {β : Type ?u.52641} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α}
  {b : β}, b ∈ s → f b ≤ sup s f
le_sup (h: s₁ ⊆ s₂
h hb: ?m.52639
hb))
#align finset.sup_mono Finset.sup_mono: ∀ {α : Type u_2} {β : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s₁ s₂ : Finset β} {f : β → α},
  s₁ ⊆ s₂ → sup s₁ f ≤ sup s₂ f
Finset.sup_mono

protected theorem sup_comm: ∀ {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : SemilatticeSup α] [inst_1 : OrderBot α] (s : Finset β)
  (t : Finset γ) (f : β → γ → α), (sup s fun b => sup t (f b)) = sup t fun c => sup s fun b => f b c
sup_comm (s: Finset β
s : Finset: Type ?u.53202 → Type ?u.53202
Finset β: Type ?u.52746
β) (t: Finset γ
t : Finset: Type ?u.53205 → Type ?u.53205
Finset γ: Type ?u.52749
γ) (f: β → γ → α
f : β: Type ?u.52746
β → γ: Type ?u.52749
γ → α: Type ?u.52743
α) :
    (s: Finset β
s.sup: {α : Type ?u.53216} → {β : Type ?u.53215} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup fun b: ?m.53229
b => t: Finset γ
t.sup: {α : Type ?u.53232} → {β : Type ?u.53231} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup (f: β → γ → α
f b: ?m.53229
b)) = t: Finset γ
t.sup: {α : Type ?u.53317} → {β : Type ?u.53316} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup fun c: ?m.53329
c => s: Finset β
s.sup: {α : Type ?u.53332} → {β : Type ?u.53331} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup fun b: ?m.53393
b => f: β → γ → α
f b: ?m.53393
b c: ?m.53329
c := by
Goals accomplished! 🐙
  F: Type ?u.52740

α: Type u_3

β: Type u_1

γ: Type u_2

ι: Type ?u.52752

κ: Type ?u.52755

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s✝, s₁, s₂: Finset β

f✝, g: β → α

a: α

s: Finset β

t: Finset γ

f: β → γ → α

(sup s fun b => sup t (f b)) = sup t fun c => sup s fun b => f b crefine' eq_of_forall_ge_iff: ∀ {α : Type ?u.53406} [inst : PartialOrder α] {a b : α}, (∀ (c : α), a ≤ c ↔ b ≤ c) → a = b
eq_of_forall_ge_iff fun a: ?m.53455
a => _: ?m.53409 ≤ a ↔ ?m.53410 ≤ a
_F: Type ?u.52740

α: Type u_3

β: Type u_1

γ: Type u_2

ι: Type ?u.52752

κ: Type ?u.52755

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s✝, s₁, s₂: Finset β

f✝, g: β → α

a✝: α

s: Finset β

t: Finset γ

f: β → γ → α

a: α

(sup s fun b => sup t (f b)) ≤ a ↔ (sup t fun c => sup s fun b => f b c) ≤ a
  F: Type ?u.52740

α: Type u_3

β: Type u_1

γ: Type u_2

ι: Type ?u.52752

κ: Type ?u.52755

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s✝, s₁, s₂: Finset β

f✝, g: β → α

a: α

s: Finset β

t: Finset γ

f: β → γ → α

(sup s fun b => sup t (f b)) = sup t fun c => sup s fun b => f b csimp_rw [F: Type ?u.52740

α: Type u_3

β: Type u_1

γ: Type u_2

ι: Type ?u.52752

κ: Type ?u.52755

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s✝, s₁, s₂: Finset β

f✝, g: β → α

a✝: α

s: Finset β

t: Finset γ

f: β → γ → α

a: α

(sup s fun b => sup t (f b)) ≤ a ↔ (sup t fun c => sup s fun b => f b c) ≤ aFinset.sup_le_iffF: Type ?u.52740

α: Type u_3

β: Type u_1

γ: Type u_2

ι: Type ?u.52752

κ: Type ?u.52755

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s✝, s₁, s₂: Finset β

f✝, g: β → α

a✝: α

s: Finset β

t: Finset γ

f: β → γ → α

a: α

(∀ (b : β), b ∈ s → ∀ (b_1 : γ), b_1 ∈ t → f b b_1 ≤ a) ↔ ∀ (b : γ), b ∈ t → ∀ (b_1 : β), b_1 ∈ s → f b_1 b ≤ a]F: Type ?u.52740

α: Type u_3

β: Type u_1

γ: Type u_2

ι: Type ?u.52752

κ: Type ?u.52755

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s✝, s₁, s₂: Finset β

f✝, g: β → α

a✝: α

s: Finset β

t: Finset γ

f: β → γ → α

a: α

(∀ (b : β), b ∈ s → ∀ (b_1 : γ), b_1 ∈ t → f b b_1 ≤ a) ↔ ∀ (b : γ), b ∈ t → ∀ (b_1 : β), b_1 ∈ s → f b_1 b ≤ a
  F: Type ?u.52740

α: Type u_3

β: Type u_1

γ: Type u_2

ι: Type ?u.52752

κ: Type ?u.52755

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s✝, s₁, s₂: Finset β

f✝, g: β → α

a: α

s: Finset β

t: Finset γ

f: β → γ → α

(sup s fun b => sup t (f b)) = sup t fun c => sup s fun b => f b cexact ⟨fun h: ?m.54276
h c: ?m.54283
c hc: ?m.54286
hc b: ?m.54289
b hb: ?m.54292
hb => h: ?m.54276
h b: ?m.54289
b hb: ?m.54292
hb c: ?m.54283
c hc: ?m.54286
hc, fun h: ?m.54309
h b: ?m.54316
b hb: ?m.54319
hb c: ?m.54322
c hc: ?m.54325
hc => h: ?m.54309
h c: ?m.54322
c hc: ?m.54325
hc b: ?m.54316
b hb: ?m.54319
hb⟩
Goals accomplished! 🐙
#align finset.sup_comm Finset.sup_comm: ∀ {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : SemilatticeSup α] [inst_1 : OrderBot α] (s : Finset β)
  (t : Finset γ) (f : β → γ → α), (sup s fun b => sup t (f b)) = sup t fun c => sup s fun b => f b c
Finset.sup_comm

@[simp, nolint simpNF: Std.Tactic.Lint.Linter
simpNF] -- Porting note: linter claims that LHS does not simplify
theorem sup_attach: ∀ {α : Type u_2} {β : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderBot α] (s : Finset β) (f : β → α),
  (sup (attach s) fun x => f ↑x) = sup s f
sup_attach (s: Finset β
s : Finset: Type ?u.54878 → Type ?u.54878
Finset β: Type ?u.54422
β) (f: β → α
f : β: Type ?u.54422
β → α: Type ?u.54419
α) : (s: Finset β
s.attach: {α : Type ?u.54886} → (s : Finset α) → Finset { x // x ∈ s }
attach.sup: {α : Type ?u.54890} → {β : Type ?u.54889} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup fun x: ?m.54902
x => f: β → α
f x: ?m.54902
x) = s: Finset β
s.sup: {α : Type ?u.55053} → {β : Type ?u.55052} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup f: β → α
f :=
  (s: Finset β
s.attach: {α : Type ?u.55071} → (s : Finset α) → Finset { x // x ∈ s }
attach.sup_map: ∀ {α : Type ?u.55076} {β : Type ?u.55075} {γ : Type ?u.55074} [inst : SemilatticeSup α] [inst_1 : OrderBot α]
  (s : Finset γ) (f : γ ↪ β) (g : β → α), sup (map f s) g = sup s (g ∘ ↑f)
sup_map (Function.Embedding.subtype: {α : Sort ?u.55090} → (p : α → Prop) → Subtype p ↪ α
Function.Embedding.subtype _: ?m.55091 → Prop
_) f: β → α
f).symm: ∀ {α : Sort ?u.55121} {a b : α}, a = b → b = a
symm.trans: ∀ {α : Sort ?u.55128} {a b c : α}, a = b → b = c → a = c
trans <| congr_arg: ∀ {α : Sort ?u.55149} {β : Sort ?u.55148} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂
congr_arg _: ?m.55150 → ?m.55151
_ attach_map_val: ∀ {α : Type ?u.55254} {s : Finset α}, map (Function.Embedding.subtype fun x => x ∈ s) (attach s) = s
attach_map_val
#align finset.sup_attach Finset.sup_attach: ∀ {α : Type u_2} {β : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderBot α] (s : Finset β) (f : β → α),
  (sup (attach s) fun x => f ↑x) = sup s f
Finset.sup_attach

/-- See also `Finset.product_biUnion`. -/
theorem sup_product_left: ∀ {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : SemilatticeSup α] [inst_1 : OrderBot α] (s : Finset β)
  (t : Finset γ) (f : β × γ → α), sup (s ×ˢ t) f = sup s fun i => sup t fun i' => f (i, i')
sup_product_left (s: Finset β
s : Finset: Type ?u.55781 → Type ?u.55781
Finset β: Type ?u.55325
β) (t: Finset γ
t : Finset: Type ?u.55784 → Type ?u.55784
Finset γ: Type ?u.55328
γ) (f: β × γ → α
f : β: Type ?u.55325
β × γ: Type ?u.55328
γ → α: Type ?u.55322
α) :
    (s: Finset β
s ×ˢ t: Finset γ
t).sup: {α : Type ?u.55827} → {β : Type ?u.55826} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup f: β × γ → α
f = s: Finset β
s.sup: {α : Type ?u.55861} → {β : Type ?u.55860} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup fun i: ?m.55873
i => t: Finset γ
t.sup: {α : Type ?u.55876} → {β : Type ?u.55875} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup fun i': ?m.55937
i' => f: β × γ → α
f ⟨i: ?m.55873
i, i': ?m.55937
i'⟩ := by
Goals accomplished! 🐙
  F: Type ?u.55319

α: Type u_3

β: Type u_1

γ: Type u_2

ι: Type ?u.55331

κ: Type ?u.55334

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s✝, s₁, s₂: Finset β

f✝, g: β → α

a: α

s: Finset β

t: Finset γ

f: β × γ → α

sup (s ×ˢ t) f = sup s fun i => sup t fun i' => f (i, i')simp only [le_antisymm_iff: ∀ {α : Type ?u.55969} [inst : PartialOrder α] {a b : α}, a = b ↔ a ≤ b ∧ b ≤ a
le_antisymm_iff, Finset.sup_le_iff: ∀ {α : Type ?u.55988} {β : Type ?u.55989} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α}
  {a : α}, sup s f ≤ a ↔ ∀ (b : β), b ∈ s → f b ≤ a
Finset.sup_le_iff, mem_product: ∀ {α : Type ?u.56029} {β : Type ?u.56030} {s : Finset α} {t : Finset β} {p : α × β}, p ∈ s ×ˢ t ↔ p.fst ∈ s ∧ p.snd ∈ t
mem_product, and_imp: ∀ {a b c : Prop}, a ∧ b → c ↔ a → b → c
and_imp, Prod.forall: ∀ {α : Type ?u.56084} {β : Type ?u.56085} {p : α × β → Prop}, (∀ (x : α × β), p x) ↔ ∀ (a : α) (b : β), p (a, b)
Prod.forall]F: Type ?u.55319

α: Type u_3

β: Type u_1

γ: Type u_2

ι: Type ?u.55331

κ: Type ?u.55334

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s✝, s₁, s₂: Finset β

f✝, g: β → α

a: α

s: Finset β

t: Finset γ

f: β × γ → α

(∀ (a : β) (b : γ), a ∈ s → b ∈ t → f (a, b) ≤ sup s fun i => sup t fun i' => f (i, i')) ∧   ∀ (b : β), b ∈ s → ∀ (b_1 : γ), b_1 ∈ t → f (b, b_1) ≤ sup (s ×ˢ t) f
  -- Porting note: was one expression.
  F: Type ?u.55319

α: Type u_3

β: Type u_1

γ: Type u_2

ι: Type ?u.55331

κ: Type ?u.55334

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s✝, s₁, s₂: Finset β

f✝, g: β → α

a: α

s: Finset β

t: Finset γ

f: β × γ → α

sup (s ×ˢ t) f = sup s fun i => sup t fun i' => f (i, i')refine ⟨fun b: ?m.57202
b c: ?m.57205
c hb: ?m.57208
hb hc: ?m.57211
hc => ?_: f (b, c) ≤ sup s fun i => sup t fun i' => f (i, i')
?_, fun b: ?m.57220
b hb: ?m.57223
hb c: ?m.57226
c hc: ?m.57229
hc => ?_: f (b, c) ≤ sup (s ×ˢ t) f
?_⟩F: Type ?u.55319

α: Type u_3

β: Type u_1

γ: Type u_2

ι: Type ?u.55331

κ: Type ?u.55334

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s✝, s₁, s₂: Finset β

f✝, g: β → α

a: α

s: Finset β

t: Finset γ

f: β × γ → α

b: β

c: γ

hb: b ∈ s

hc: c ∈ t

refine_1f (b, c) ≤ sup s fun i => sup t fun i' => f (i, i')
F: Type ?u.55319

α: Type u_3

β: Type u_1

γ: Type u_2

ι: Type ?u.55331

κ: Type ?u.55334

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s✝, s₁, s₂: Finset β

f✝, g: β → α

a: α

s: Finset β

t: Finset γ

f: β × γ → α

b: β

hb: b ∈ s

c: γ

hc: c ∈ t

refine_2f (b, c) ≤ sup (s ×ˢ t) f
  F: Type ?u.55319

α: Type u_3

β: Type u_1

γ: Type u_2

ι: Type ?u.55331

κ: Type ?u.55334

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s✝, s₁, s₂: Finset β

f✝, g: β → α

a: α

s: Finset β

t: Finset γ

f: β × γ → α

sup (s ×ˢ t) f = sup s fun i => sup t fun i' => f (i, i')·F: Type ?u.55319

α: Type u_3

β: Type u_1

γ: Type u_2

ι: Type ?u.55331

κ: Type ?u.55334

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s✝, s₁, s₂: Finset β

f✝, g: β → α

a: α

s: Finset β

t: Finset γ

f: β × γ → α

b: β

c: γ

hb: b ∈ s

hc: c ∈ t

refine_1f (b, c) ≤ sup s fun i => sup t fun i' => f (i, i') F: Type ?u.55319

α: Type u_3

β: Type u_1

γ: Type u_2

ι: Type ?u.55331

κ: Type ?u.55334

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s✝, s₁, s₂: Finset β

f✝, g: β → α

a: α

s: Finset β

t: Finset γ

f: β × γ → α

b: β

c: γ

hb: b ∈ s

hc: c ∈ t

refine_1f (b, c) ≤ sup s fun i => sup t fun i' => f (i, i')
F: Type ?u.55319

α: Type u_3

β: Type u_1

γ: Type u_2

ι: Type ?u.55331

κ: Type ?u.55334

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s✝, s₁, s₂: Finset β

f✝, g: β → α

a: α

s: Finset β

t: Finset γ

f: β × γ → α

b: β

hb: b ∈ s

c: γ

hc: c ∈ t

refine_2f (b, c) ≤ sup (s ×ˢ t) frefine (le_sup: ∀ {α : Type ?u.57238} {β : Type ?u.57237} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α}
  {b : β}, b ∈ s → f b ≤ sup s f
le_sup hb: ?m.57208
hb).trans': ∀ {α : Type ?u.57300} [inst : Preorder α] {a b c : α}, b ≤ c → a ≤ b → a ≤ c
trans' ?_: ?m.57310 ≤ ?m.57311
?_F: Type ?u.55319

α: Type u_3

β: Type u_1

γ: Type u_2

ι: Type ?u.55331

κ: Type ?u.55334

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s✝, s₁, s₂: Finset β

f✝, g: β → α

a: α

s: Finset β

t: Finset γ

f: β × γ → α

b: β

c: γ

hb: b ∈ s

hc: c ∈ t

refine_1f (b, c) ≤ sup t fun i' => f (b, i')
    F: Type ?u.55319

α: Type u_3

β: Type u_1

γ: Type u_2

ι: Type ?u.55331

κ: Type ?u.55334

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s✝, s₁, s₂: Finset β

f✝, g: β → α

a: α

s: Finset β

t: Finset γ

f: β × γ → α

b: β

c: γ

hb: b ∈ s

hc: c ∈ t

refine_1f (b, c) ≤ sup s fun i => sup t fun i' => f (i, i')exact @le_sup: ∀ {α : Type ?u.57727} {β : Type ?u.57726} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α}
  {b : β}, b ∈ s → f b ≤ sup s f
le_sup _: Type ?u.57727
_ _: Type ?u.57726
_ _ _ _: Finset ?m.57729
_ (fun c: ?m.57734
c => f: β × γ → α
f (b: ?m.57202
b, c: ?m.57734
c)) c: ?m.57205
c hc: ?m.57211
hc
Goals accomplished! 🐙
  F: Type ?u.55319

α: Type u_3

β: Type u_1

γ: Type u_2

ι: Type ?u.55331

κ: Type ?u.55334

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s✝, s₁, s₂: Finset β

f✝, g: β → α

a: α

s: Finset β

t: Finset γ

f: β × γ → α

sup (s ×ˢ t) f = sup s fun i => sup t fun i' => f (i, i')·F: Type ?u.55319

α: Type u_3

β: Type u_1

γ: Type u_2

ι: Type ?u.55331

κ: Type ?u.55334

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s✝, s₁, s₂: Finset β

f✝, g: β → α

a: α

s: Finset β

t: Finset γ

f: β × γ → α

b: β

hb: b ∈ s

c: γ

hc: c ∈ t

refine_2f (b, c) ≤ sup (s ×ˢ t) f F: Type ?u.55319

α: Type u_3

β: Type u_1

γ: Type u_2

ι: Type ?u.55331

κ: Type ?u.55334

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s✝, s₁, s₂: Finset β

f✝, g: β → α

a: α

s: Finset β

t: Finset γ

f: β × γ → α

b: β

hb: b ∈ s

c: γ

hc: c ∈ t

refine_2f (b, c) ≤ sup (s ×ˢ t) fexact le_sup: ∀ {α : Type ?u.57750} {β : Type ?u.57749} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α}
  {b : β}, b ∈ s → f b ≤ sup s f
le_sup <| mem_product: ∀ {α : Type ?u.57820} {β : Type ?u.57821} {s : Finset α} {t : Finset β} {p : α × β}, p ∈ s ×ˢ t ↔ p.fst ∈ s ∧ p.snd ∈ t
mem_product.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 ⟨hb: ?m.57223
hb, hc: ?m.57229
hc⟩
Goals accomplished! 🐙
#align finset.sup_product_left Finset.sup_product_left: ∀ {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : SemilatticeSup α] [inst_1 : OrderBot α] (s : Finset β)
  (t : Finset γ) (f : β × γ → α), sup (s ×ˢ t) f = sup s fun i => sup t fun i' => f (i, i')
Finset.sup_product_left

theorem sup_product_right: ∀ (s : Finset β) (t : Finset γ) (f : β × γ → α), sup (s ×ˢ t) f = sup t fun i' => sup s fun i => f (i, i')
sup_product_right (s: Finset β
s : Finset: Type ?u.58389 → Type ?u.58389
Finset β: Type ?u.57933
β) (t: Finset γ
t : Finset: Type ?u.58392 → Type ?u.58392
Finset γ: Type ?u.57936
γ) (f: β × γ → α
f : β: Type ?u.57933
β × γ: Type ?u.57936
γ → α: Type ?u.57930
α) :
    (s: Finset β
s ×ˢ t: Finset γ
t).sup: {α : Type ?u.58435} → {β : Type ?u.58434} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup f: β × γ → α
f = t: Finset γ
t.sup: {α : Type ?u.58469} → {β : Type ?u.58468} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup fun i': ?m.58481
i' => s: Finset β
s.sup: {α : Type ?u.58484} → {β : Type ?u.58483} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup fun i: ?m.58545
i => f: β × γ → α
f ⟨i: ?m.58545
i, i': ?m.58481
i'⟩ := by
Goals accomplished! 🐙
  F: Type ?u.57927

α: Type u_3

β: Type u_1

γ: Type u_2

ι: Type ?u.57939

κ: Type ?u.57942

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s✝, s₁, s₂: Finset β

f✝, g: β → α

a: α

s: Finset β

t: Finset γ

f: β × γ → α

sup (s ×ˢ t) f = sup t fun i' => sup s fun i => f (i, i')rw [F: Type ?u.57927

α: Type u_3

β: Type u_1

γ: Type u_2

ι: Type ?u.57939

κ: Type ?u.57942

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s✝, s₁, s₂: Finset β

f✝, g: β → α

a: α

s: Finset β

t: Finset γ

f: β × γ → α

sup (s ×ˢ t) f = sup t fun i' => sup s fun i => f (i, i')sup_product_left: ∀ {α : Type ?u.58568} {β : Type ?u.58566} {γ : Type ?u.58567} [inst : SemilatticeSup α] [inst_1 : OrderBot α]
  (s : Finset β) (t : Finset γ) (f : β × γ → α), sup (s ×ˢ t) f = sup s fun i => sup t fun i' => f (i, i')
sup_product_left,F: Type ?u.57927

α: Type u_3

β: Type u_1

γ: Type u_2

ι: Type ?u.57939

κ: Type ?u.57942

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s✝, s₁, s₂: Finset β

f✝, g: β → α

a: α

s: Finset β

t: Finset γ

f: β × γ → α

(sup s fun i => sup t fun i' => f (i, i')) = sup t fun i' => sup s fun i => f (i, i') F: Type ?u.57927

α: Type u_3

β: Type u_1

γ: Type u_2

ι: Type ?u.57939

κ: Type ?u.57942

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s✝, s₁, s₂: Finset β

f✝, g: β → α

a: α

s: Finset β

t: Finset γ

f: β × γ → α

sup (s ×ˢ t) f = sup t fun i' => sup s fun i => f (i, i')Finset.sup_comm: ∀ {α : Type ?u.58729} {β : Type ?u.58727} {γ : Type ?u.58728} [inst : SemilatticeSup α] [inst_1 : OrderBot α]
  (s : Finset β) (t : Finset γ) (f : β → γ → α), (sup s fun b => sup t (f b)) = sup t fun c => sup s fun b => f b c
Finset.sup_commF: Type ?u.57927

α: Type u_3

β: Type u_1

γ: Type u_2

ι: Type ?u.57939

κ: Type ?u.57942

inst✝¹: SemilatticeSup α

inst✝: OrderBot α

s✝, s₁, s₂: Finset β

f✝, g: β → α

a: α

s: Finset β

t: Finset γ

f: β × γ → α

(sup t fun c => sup s fun b => f (b, c)) = sup t fun i' => sup s fun i => f (i, i')]
Goals accomplished! 🐙
#align finset.sup_product_right Finset.sup_product_right: ∀ {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : SemilatticeSup α] [inst_1 : OrderBot α] (s : Finset β)
  (t : Finset γ) (f : β × γ → α), sup (s ×ˢ t) f = sup t fun i' => sup s fun i => f (i, i')
Finset.sup_product_right

@[simp]
theorem sup_erase_bot: ∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderBot α] [inst_2 : DecidableEq α] (s : Finset α),
  sup (erase s ⊥) id = sup s id
sup_erase_bot [DecidableEq: Sort ?u.59344 → Sort (max1?u.59344)
DecidableEq α: Type ?u.58885
α] (s: Finset α
s : Finset: Type ?u.59353 → Type ?u.59353
Finset α: Type ?u.58885
α) : (s: Finset α
s.erase: {α : Type ?u.59357} → [inst : DecidableEq α] → Finset α → α → Finset α
erase ⊥: ?m.59368
⊥).sup: {α : Type ?u.59889} → {β : Type ?u.59888} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup id: {α : Sort ?u.59900} → α → α
id = s: Finset α
s.sup: {α : Type ?u.59916} → {β : Type ?u.59915} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup id: {α : Sort ?u.59927} → α → α
id := by
Goals accomplished! 🐙
  F: Type ?u.58882

α: Type u_1

β: Type ?u.58888

γ: Type ?u.58891

ι: Type ?u.58894

κ: Type ?u.58897

inst✝²: SemilatticeSup α

inst✝¹: OrderBot α

s✝, s₁, s₂: Finset β

f, g: β → α

a: α

inst✝: DecidableEq α

s: Finset α

sup (erase s ⊥) id = sup s idrefine' (sup_mono: ∀ {α : Type ?u.59941} {β : Type ?u.59940} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s₁ s₂ : Finset β}
  {f : β → α}, s₁ ⊆ s₂ → sup s₁ f ≤ sup s₂ f
sup_mono (s: Finset α
s.erase_subset: ∀ {α : Type ?u.59949} [inst : DecidableEq α] (a : α) (s : Finset α), erase s a ⊆ s
erase_subset _: ?m.59958
_)).antisymm: ∀ {α : Type ?u.60042} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≤ a → a = b
antisymm (Finset.sup_le_iff: ∀ {α : Type ?u.60242} {β : Type ?u.60243} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α}
  {a : α}, sup s f ≤ a ↔ ∀ (b : β), b ∈ s → f b ≤ a
Finset.sup_le_iff.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 fun a: ?m.60317
a ha: ?m.60320
ha => _: ?m.60297 a ≤ ?m.60298
_)F: Type ?u.58882

α: Type u_1

β: Type ?u.58888

γ: Type ?u.58891

ι: Type ?u.58894

κ: Type ?u.58897

inst✝²: SemilatticeSup α

inst✝¹: OrderBot α

s✝, s₁, s₂: Finset β

f, g: β → α

a✝: α

inst✝: DecidableEq α

s: Finset α

a: α

ha: a ∈ s

id a ≤ sup (erase s ⊥) id
  F: Type ?u.58882

α: Type u_1

β: Type ?u.58888

γ: Type ?u.58891

ι: Type ?u.58894

κ: Type ?u.58897

inst✝²: SemilatticeSup α

inst✝¹: OrderBot α

s✝, s₁, s₂: Finset β

f, g: β → α

a: α

inst✝: DecidableEq α

s: Finset α

sup (erase s ⊥) id = sup s idobtain rfl: a = ⊥
rflrfl | ha': a = ⊥ ∨ a ≠ ⊥
 | ha': a ≠ ⊥
ha' := eq_or_ne: ∀ {α : Sort ?u.60743} (x y : α), x = y ∨ x ≠ y
eq_or_ne a: ?m.60317
a ⊥: ?m.60746
⊥F: Type ?u.58882

α: Type u_1

β: Type ?u.58888

γ: Type ?u.58891

ι: Type ?u.58894

κ: Type ?u.58897

inst✝²: SemilatticeSup α

inst✝¹: OrderBot α

s✝, s₁, s₂: Finset β

f, g: β → α

a: α

inst✝: DecidableEq α

s: Finset α

ha: ⊥ ∈ s

inlid ⊥ ≤ sup (erase s ⊥) id
F: Type ?u.58882

α: Type u_1

β: Type ?u.58888

γ: Type ?u.58891

ι: Type ?u.58894

κ: Type ?u.58897

inst✝²: SemilatticeSup α

inst✝¹: OrderBot α

s✝, s₁, s₂: Finset β

f, g: β → α

a✝: α

inst✝: DecidableEq α

s: Finset α

a: α

ha: a ∈ s

ha': a ≠ ⊥

inrid a ≤ sup (erase s ⊥) id
  F: Type ?u.58882

α: Type u_1

β: Type ?u.58888

γ: Type ?u.58891

ι: Type ?u.58894

κ: Type ?u.58897

inst✝²: SemilatticeSup α

inst✝¹: OrderBot α

s✝, s₁, s₂: Finset β

f, g: β → α

a: α

inst✝: DecidableEq α

s: Finset α

sup (erase s ⊥) id = sup s id·F: Type ?u.58882

α: Type u_1

β: Type ?u.58888

γ: Type ?u.58891

ι: Type ?u.58894

κ: Type ?u.58897

inst✝²: SemilatticeSup α

inst✝¹: OrderBot α

s✝, s₁, s₂: Finset β

f, g: β → α

a: α

inst✝: DecidableEq α

s: Finset α

ha: ⊥ ∈ s

inlid ⊥ ≤ sup (erase s ⊥) id F: Type ?u.58882

α: Type u_1

β: Type ?u.58888

γ: Type ?u.58891

ι: Type ?u.58894

κ: Type ?u.58897

inst✝²: SemilatticeSup α

inst✝¹: OrderBot α

s✝, s₁, s₂: Finset β

f, g: β → α

a: α

inst✝: DecidableEq α

s: Finset α

ha: ⊥ ∈ s

inlid ⊥ ≤ sup (erase s ⊥) id
F: Type ?u.58882

α: Type u_1

β: Type ?u.58888

γ: Type ?u.58891

ι: Type ?u.58894

κ: Type ?u.58897

inst✝²: SemilatticeSup α

inst✝¹: OrderBot α

s✝, s₁, s₂: Finset β

f, g: β → α

a✝: α

inst✝: DecidableEq α

s: Finset α

a: α

ha: a ∈ s

ha': a ≠ ⊥

inrid a ≤ sup (erase s ⊥) idexact bot_le: ∀ {α : Type ?u.61183} [inst : LE α] [inst_1 : OrderBot α] {a : α}, ⊥ ≤ a
bot_le
Goals accomplished! 🐙
  F: Type ?u.58882

α: Type u_1

β: Type ?u.58888

γ: Type ?u.58891

ι: Type ?u.58894

κ: Type ?u.58897

inst✝²: SemilatticeSup α

inst✝¹: OrderBot α

s✝, s₁, s₂: Finset β

f, g