feat(Finset/{NAry,Pointwise}): add lemmas about Finset.sup etc (#8950)

Author: urkud

Mathlib/Data/Finset/Image.lean

@@ -818,6 +818,8 @@ theorem fin_map {n} {s : Finset ℕ} : (s.fin n).map Fin.valEmbedding = s.filter
   simp [Finset.fin, Finset.map_map]
 #align finset.fin_map Finset.fin_map
 
+/-- If a `Finset` is a subset of the image of a `Set` under `f`,
+then it is equal to the `Finset.image` of a `Finset` subset of that `Set`. -/
 theorem subset_image_iff [DecidableEq β] {s : Set α} {t : Finset β} {f : α → β} :
     ↑t ⊆ f '' s ↔ ∃ s' : Finset α, ↑s' ⊆ s ∧ s'.image f = t := by
   constructor; swap

Mathlib/Data/Finset/Lattice.lean

@@ -856,13 +856,13 @@ protected theorem sup'_comm {t : Finset γ} (hs : s.Nonempty) (ht : t.Nonempty)
   eq_of_forall_ge_iff fun a => by simpa using forall₂_swap
 #align finset.sup'_comm Finset.sup'_comm
 
-theorem sup'_product_left {t : Finset γ} (hs : s.Nonempty) (ht : t.Nonempty) (f : β × γ → α) :
-    (s ×ˢ t).sup' (hs.product ht) f = s.sup' hs fun i => t.sup' ht fun i' => f ⟨i, i'⟩ :=
+theorem sup'_product_left {t : Finset γ} (h : (s ×ˢ t).Nonempty) (f : β × γ → α) :
+    (s ×ˢ t).sup' h f = s.sup' h.fst fun i => t.sup' h.snd fun i' => f ⟨i, i'⟩ :=
   eq_of_forall_ge_iff fun a => by simp [@forall_swap _ γ]
 #align finset.sup'_product_left Finset.sup'_product_left
 
-theorem sup'_product_right {t : Finset γ} (hs : s.Nonempty) (ht : t.Nonempty) (f : β × γ → α) :
-    (s ×ˢ t).sup' (hs.product ht) f = t.sup' ht fun i' => s.sup' hs fun i => f ⟨i, i'⟩ := by
+theorem sup'_product_right {t : Finset γ} (h : (s ×ˢ t).Nonempty) (f : β × γ → α) :
+    (s ×ˢ t).sup' h f = t.sup' h.snd fun i' => s.sup' h.fst fun i => f ⟨i, i'⟩ := by
   rw [sup'_product_left, Finset.sup'_comm]
 #align finset.sup'_product_right Finset.sup'_product_right
 
@@ -1035,14 +1035,14 @@ protected theorem inf'_comm {t : Finset γ} (hs : s.Nonempty) (ht : t.Nonempty)
   @Finset.sup'_comm αᵒᵈ _ _ _ _ _ hs ht _
 #align finset.inf'_comm Finset.inf'_comm
 
-theorem inf'_product_left {t : Finset γ} (hs : s.Nonempty) (ht : t.Nonempty) (f : β × γ → α) :
-    (s ×ˢ t).inf' (hs.product ht) f = s.inf' hs fun i => t.inf' ht fun i' => f ⟨i, i'⟩ :=
-  @sup'_product_left αᵒᵈ _ _ _ _ _ hs ht _
+theorem inf'_product_left {t : Finset γ} (h : (s ×ˢ t).Nonempty) (f : β × γ → α) :
+    (s ×ˢ t).inf' h f = s.inf' h.fst fun i => t.inf' h.snd fun i' => f ⟨i, i'⟩ :=
+  sup'_product_left (α := αᵒᵈ) h f
 #align finset.inf'_product_left Finset.inf'_product_left
 
-theorem inf'_product_right {t : Finset γ} (hs : s.Nonempty) (ht : t.Nonempty) (f : β × γ → α) :
-    (s ×ˢ t).inf' (hs.product ht) f = t.inf' ht fun i' => s.inf' hs fun i => f ⟨i, i'⟩ :=
-  @sup'_product_right αᵒᵈ _ _ _ _ _ hs ht _
+theorem inf'_product_right {t : Finset γ} (h : (s ×ˢ t).Nonempty) (f : β × γ → α) :
+    (s ×ˢ t).inf' h f = t.inf' h.snd fun i' => s.inf' h.fst fun i => f ⟨i, i'⟩ :=
+  sup'_product_right (α := αᵒᵈ) h f
 #align finset.inf'_product_right Finset.inf'_product_right
 
 section Prod
@@ -1219,7 +1219,7 @@ theorem sup'_inf_distrib_right (f : ι → α) (a : α) : s.sup' hs f ⊓ a = s.
 
 theorem sup'_inf_sup' (f : ι → α) (g : κ → α) :
     s.sup' hs f ⊓ t.sup' ht g = (s ×ˢ t).sup' (hs.product ht) fun i => f i.1 ⊓ g i.2 := by
-  simp_rw [Finset.sup'_inf_distrib_right, Finset.sup'_inf_distrib_left, sup'_product_left hs ht]
+  simp_rw [Finset.sup'_inf_distrib_right, Finset.sup'_inf_distrib_left, sup'_product_left]
 #align finset.sup'_inf_sup' Finset.sup'_inf_sup'
 
 theorem inf'_sup_distrib_left (f : ι → α) (a : α) : a ⊔ s.inf' hs f = s.inf' hs fun i => a ⊔ f i :=

Mathlib/Data/Finset/NAry.lean

@@ -317,15 +317,12 @@ theorem image₂_mk_eq_product [DecidableEq α] [DecidableEq β] (s : Finset α)
 
 @[simp]
 theorem image₂_curry (f : α × β → γ) (s : Finset α) (t : Finset β) :
-    image₂ (curry f) s t = (s ×ˢ t).image f := by
-  classical
-  rw [← image₂_mk_eq_product, image_image₂]
-  dsimp (config := { unfoldPartialApp := true }) [curry]
+    image₂ (curry f) s t = (s ×ˢ t).image f := rfl
 #align finset.image₂_curry Finset.image₂_curry
 
 @[simp]
 theorem image_uncurry_product (f : α → β → γ) (s : Finset α) (t : Finset β) :
-    (s ×ˢ t).image (uncurry f) = image₂ f s t := by rw [← image₂_curry, curry_uncurry]
+    (s ×ˢ t).image (uncurry f) = image₂ f s t := rfl
 #align finset.image_uncurry_product Finset.image_uncurry_product
 
 theorem image₂_swap (f : α → β → γ) (s : Finset α) (t : Finset β) :
@@ -529,6 +526,8 @@ theorem card_dvd_card_image₂_left (hf : ∀ b ∈ t, Injective fun a => f a b)
     s.card ∣ (image₂ f s t).card := by rw [← image₂_swap]; exact card_dvd_card_image₂_right hf ht
 #align finset.card_dvd_card_image₂_left Finset.card_dvd_card_image₂_left
 
+/-- If a `Finset` is a subset of the image of two `Set`s under a binary operation,
+then it is a subset of the `Finset.image₂` of two `Finset` subsets of these `Set`s. -/
 theorem subset_image₂ {s : Set α} {t : Set β} (hu : ↑u ⊆ image2 f s t) :
     ∃ (s' : Finset α) (t' : Finset β), ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ image₂ f s' t' := by
   rw [← Set.image_prod, subset_image_iff] at hu
@@ -540,6 +539,8 @@ theorem subset_image₂ {s : Set α} {t : Set β} (hu : ↑u ⊆ image2 f s t) :
   exact ⟨fun _ h ↦ (hu h).1, fun _ h ↦ (hu h).2, fun x hx ↦ mem_image₂_of_mem hx hx⟩
 #align finset.subset_image₂ Finset.subset_image₂
 
+section UnionInter
+
 variable [DecidableEq α] [DecidableEq β]
 
 theorem image₂_inter_union_subset_union :
@@ -570,6 +571,80 @@ theorem image₂_union_inter_subset {f : α → α → β} {s t : Finset α} (hf
     exact image2_union_inter_subset hf
 #align finset.image₂_union_inter_subset Finset.image₂_union_inter_subset
 
+end UnionInter
+
+section SemilatticeSup
+
+variable [SemilatticeSup δ]
+
+@[simp (default + 1)] -- otherwise `simp` doesn't use `forall_image₂_iff`
+lemma sup'_image₂_le {g : γ → δ} {a : δ} (h : (image₂ f s t).Nonempty) :
+    sup' (image₂ f s t) h g ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, g (f x y) ≤ a := by
+  rw [sup'_le_iff, forall_image₂_iff]
+
+lemma sup'_image₂_left (g : γ → δ) (h : (image₂ f s t).Nonempty) :
+    sup' (image₂ f s t) h g =
+      sup' s h.of_image₂_left fun x ↦ sup' t h.of_image₂_right (g <| f x ·) := by
+  simp only [image₂, sup'_image, sup'_product_left]; rfl
+
+lemma sup'_image₂_right (g : γ → δ) (h : (image₂ f s t).Nonempty) :
+    sup' (image₂ f s t) h g =
+      sup' t h.of_image₂_right fun y ↦ sup' s h.of_image₂_left (g <| f · y) := by
+  simp only [image₂, sup'_image, sup'_product_right]; rfl
+
+variable [OrderBot δ]
+
+@[simp (default + 1)] -- otherwise `simp` doesn't use `forall_image₂_iff`
+lemma sup_image₂_le {g : γ → δ} {a : δ} :
+    sup (image₂ f s t) g ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, g (f x y) ≤ a := by
+  rw [Finset.sup_le_iff, forall_image₂_iff]
+
+variable (s t)
+
+lemma sup_image₂_left (g : γ → δ) : sup (image₂ f s t) g = sup s fun x ↦ sup t (g <| f x ·) := by
+  simp only [image₂, sup_image, sup_product_left]; rfl
+
+lemma sup_image₂_right (g : γ → δ) : sup (image₂ f s t) g = sup t fun y ↦ sup s (g <| f · y) := by
+  simp only [image₂, sup_image, sup_product_right]; rfl
+
+end SemilatticeSup
+
+section SemilatticeInf
+
+variable [SemilatticeInf δ]
+
+@[simp (default + 1)] -- otherwise `simp` doesn't use `forall_image₂_iff`
+lemma le_inf'_image₂ {g : γ → δ} {a : δ} (h : (image₂ f s t).Nonempty) :
+    a ≤ inf' (image₂ f s t) h g ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ g (f x y) := by
+  rw [le_inf'_iff, forall_image₂_iff]
+
+lemma inf'_image₂_left (g : γ → δ) (h : (image₂ f s t).Nonempty) :
+    inf' (image₂ f s t) h g =
+      inf' s h.of_image₂_left fun x ↦ inf' t h.of_image₂_right (g <| f x ·) :=
+  sup'_image₂_left (δ := δᵒᵈ) g h
+
+lemma inf'_image₂_right (g : γ → δ) (h : (image₂ f s t).Nonempty) :
+    inf' (image₂ f s t) h g =
+      inf' t h.of_image₂_right fun y ↦ inf' s h.of_image₂_left (g <| f · y) :=
+  sup'_image₂_right (δ := δᵒᵈ) g h
+
+variable [OrderTop δ]
+
+@[simp (default + 1)] -- otherwise `simp` doesn't use `forall_image₂_iff`
+lemma le_inf_image₂ {g : γ → δ} {a : δ} :
+    a ≤ inf (image₂ f s t) g ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ g (f x y) :=
+  sup_image₂_le (δ := δᵒᵈ)
+
+variable (s t)
+
+lemma inf_image₂_left (g : γ → δ) : inf (image₂ f s t) g = inf s fun x ↦ inf t (g ∘ f x) :=
+  sup_image₂_left (δ := δᵒᵈ) ..
+
+lemma inf_image₂_right (g : γ → δ) : inf (image₂ f s t) g = inf t fun y ↦ inf s (g <| f · y) :=
+  sup_image₂_right (δ := δᵒᵈ) ..
+
+end SemilatticeInf
+
 end Finset
 
 open Finset

Mathlib/Data/Finset/Pointwise.lean

@@ -65,7 +65,6 @@ namespace Finset
 
 /-! ### `0`/`1` as finsets -/
 
-
 section One
 
 variable [One α] {s : Finset α} {a : α}
@@ -169,18 +168,41 @@ theorem singletonOneHom_apply (a : α) : singletonOneHom a = {a} :=
 
 /-- Lift a `OneHom` to `Finset` via `image`. -/
 @[to_additive (attr := simps) "Lift a `ZeroHom` to `Finset` via `image`"]
-def imageOneHom [DecidableEq β] [One β] [OneHomClass F α β] (f : F) : OneHom (Finset α) (Finset β)
-    where
+def imageOneHom [DecidableEq β] [One β] [OneHomClass F α β] (f : F) :
+    OneHom (Finset α) (Finset β) where
   toFun := Finset.image f
   map_one' := by rw [image_one, map_one, singleton_one]
 #align finset.image_one_hom Finset.imageOneHom
 #align finset.image_zero_hom Finset.imageZeroHom
 
+@[to_additive (attr := simp)]
+lemma sup_one [SemilatticeSup β] [OrderBot β] (f : α → β) : sup 1 f = f 1 := sup_singleton
+
+@[to_additive (attr := simp)]
+lemma sup'_one [SemilatticeSup β] (f : α → β) : sup' 1 one_nonempty f = f 1 := rfl
+
+@[to_additive (attr := simp)]
+lemma inf_one [SemilatticeInf β] [OrderTop β] (f : α → β) : inf 1 f = f 1 := inf_singleton
+
+@[to_additive (attr := simp)]
+lemma inf'_one [SemilatticeInf β] (f : α → β) : inf' 1 one_nonempty f = f 1 := rfl
+
+@[to_additive (attr := simp)]
+lemma max_one [LinearOrder α] : (1 : Finset α).max = 1 := rfl
+
+@[to_additive (attr := simp)]
+lemma min_one [LinearOrder α] : (1 : Finset α).min = 1 := rfl
+
+@[to_additive (attr := simp)]
+lemma max'_one [LinearOrder α] : (1 : Finset α).max' one_nonempty = 1 := rfl
+
+@[to_additive (attr := simp)]
+lemma min'_one [LinearOrder α] : (1 : Finset α).min' one_nonempty = 1 := rfl
+
 end One
 
 /-! ### Finset negation/inversion -/
 
-
 section Inv
 
 variable [DecidableEq α] [Inv α] {s s₁ s₂ t t₁ t₂ u : Finset α} {a b : α}
@@ -260,6 +282,26 @@ theorem inv_insert (a : α) (s : Finset α) : (insert a s)⁻¹ = insert a⁻¹
 #align finset.inv_insert Finset.inv_insert
 #align finset.neg_insert Finset.neg_insert
 
+@[to_additive (attr := simp)]
+lemma sup_inv [SemilatticeSup β] [OrderBot β] (s : Finset α) (f : α → β) :
+    sup s⁻¹ f = sup s (f ·⁻¹) :=
+  sup_image ..
+
+@[to_additive (attr := simp)]
+lemma sup'_inv [SemilatticeSup β] {s : Finset α} (hs : s⁻¹.Nonempty) (f : α → β) :
+    sup' s⁻¹ hs f = sup' s hs.of_inv (f ·⁻¹) :=
+  sup'_image ..
+
+@[to_additive (attr := simp)]
+lemma inf_inv [SemilatticeInf β] [OrderTop β] (s : Finset α) (f : α → β) :
+    inf s⁻¹ f = inf s (f ·⁻¹) :=
+  inf_image ..
+
+@[to_additive (attr := simp)]
+lemma inf'_inv [SemilatticeInf β] {s : Finset α} (hs : s⁻¹.Nonempty) (f : α → β) :
+    inf' s⁻¹ hs f = inf' s hs.of_inv (f ·⁻¹) :=
+  inf'_image ..
+
 @[to_additive] lemma image_op_inv (s : Finset α) : s⁻¹.image op = (s.image op)⁻¹ :=
   image_comm op_inv
 
@@ -520,11 +562,40 @@ def imageMulHom : Finset α →ₙ* Finset β where
 #align finset.image_mul_hom Finset.imageMulHom
 #align finset.image_add_hom Finset.imageAddHom
 
+@[to_additive (attr := simp (default + 1))]
+lemma sup_mul_le [SemilatticeSup β] [OrderBot β] {s t : Finset α} {f : α → β} {a : β} :
+    sup (s * t) f ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, f (x * y) ≤ a :=
+  sup_image₂_le
+
+@[to_additive]
+lemma sup_mul_left [SemilatticeSup β] [OrderBot β] (s t : Finset α) (f : α → β) :
+    sup (s * t) f = sup s fun x ↦ sup t (f <| x * ·) :=
+  sup_image₂_left ..
+
+@[to_additive]
+lemma sup_mul_right [SemilatticeSup β] [OrderBot β] (s t : Finset α) (f : α → β) :
+    sup (s * t) f = sup t fun y ↦ sup s (f <| · * y) :=
+  sup_image₂_right ..
+
+@[to_additive (attr := simp (default + 1))]
+lemma le_inf_mul [SemilatticeInf β] [OrderTop β] {s t : Finset α} {f : α → β} {a : β} :
+    a ≤ inf (s * t) f ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ f (x * y) :=
+  le_inf_image₂
+
+@[to_additive]
+lemma inf_mul_left [SemilatticeInf β] [OrderTop β] (s t : Finset α) (f : α → β) :
+    inf (s * t) f = inf s fun x ↦ inf t (f <| x * ·) :=
+  inf_image₂_left ..
+
+@[to_additive]
+lemma inf_mul_right [SemilatticeInf β] [OrderTop β] (s t : Finset α) (f : α → β) :
+    inf (s * t) f = inf t fun y ↦ inf s (f <| · * y) :=
+  inf_image₂_right ..
+
 end Mul
 
 /-! ### Finset subtraction/division -/
 
-
 section Div
 
 variable [DecidableEq α] [Div α] {s s₁ s₂ t t₁ t₂ u : Finset α} {a b : α}
@@ -709,6 +780,36 @@ theorem subset_div {s t : Set α} :
 #align finset.subset_div Finset.subset_div
 #align finset.subset_sub Finset.subset_sub
 
+@[to_additive (attr := simp (default + 1))]
+lemma sup_div_le [SemilatticeSup β] [OrderBot β] {s t : Finset α} {f : α → β} {a : β} :
+    sup (s / t) f ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, f (x /  y) ≤ a :=
+  sup_image₂_le
+
+@[to_additive]
+lemma sup_div_left [SemilatticeSup β] [OrderBot β] (s t : Finset α) (f : α → β) :
+    sup (s / t) f = sup s fun x ↦ sup t (f <| x / ·) :=
+  sup_image₂_left ..
+
+@[to_additive]
+lemma sup_div_right [SemilatticeSup β] [OrderBot β] (s t : Finset α) (f : α → β) :
+    sup (s / t) f = sup t fun y ↦ sup s (f <| · / y) :=
+  sup_image₂_right ..
+
+@[to_additive (attr := simp (default + 1))]
+lemma le_inf_div [SemilatticeInf β] [OrderTop β] {s t : Finset α} {f : α → β} {a : β} :
+    a ≤ inf (s / t) f ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ f (x / y) :=
+  le_inf_image₂
+
+@[to_additive]
+lemma inf_div_left [SemilatticeInf β] [OrderTop β] (s t : Finset α) (f : α → β) :
+    inf (s / t) f = inf s fun x ↦ inf t (f <| x / ·) :=
+  inf_image₂_left ..
+
+@[to_additive]
+lemma inf_div_right [SemilatticeInf β] [OrderTop β] (s t : Finset α) (f : α → β) :
+    inf (s / t) f = inf t fun y ↦ inf s (f <| · / y) :=
+  inf_image₂_right ..
+
 end Div
 
 /-! ### Instances -/