fix: precedence of shadow (#5620)

Author: fpvandoorn

Mathlib/Combinatorics/SetFamily/Compression/UV.lean

@@ -323,10 +323,10 @@ that `𝒜` is `(u.erase x, v.erase y)`-compressed. This is the key fact about c
 Kruskal-Katona. -/
 theorem shadow_compression_subset_compression_shadow (u v : Finset α)
     (huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜) :
-    (∂ ) (𝓒 u v 𝒜) ⊆ 𝓒 u v ((∂ ) 𝒜) := by
+    ∂ (𝓒 u v 𝒜) ⊆ 𝓒 u v (∂ 𝒜) := by
   set 𝒜' := 𝓒 u v 𝒜
-  suffices H : ∀ s ∈ (∂ ) 𝒜',
-      s ∉ (∂ ) 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ (∂ ) 𝒜 ∧ (s ∪ v) \ u ∉ (∂ ) 𝒜'
+  suffices H : ∀ s ∈ ∂ 𝒜',
+      s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
   · rintro s hs'
     rw [mem_compression]
     by_cases hs : s ∈ 𝒜.shadow
@@ -431,7 +431,7 @@ such that `𝒜` is `(u.erase x, v.erase y)`-compressed. This is the key UV-comp
 Kruskal-Katona. -/
 theorem card_shadow_compression_le (u v : Finset α)
     (huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜) :
-    ((∂ ) (𝓒 u v 𝒜)).card ≤ ((∂ ) 𝒜).card :=
+    (∂ (𝓒 u v 𝒜)).card ≤ (∂ 𝒜).card :=
   (card_le_of_subset <| shadow_compression_subset_compression_shadow _ _ huv).trans
     (card_compression _ _ _).le
 #align uv.card_shadow_compression_le UV.card_shadow_compression_le

Mathlib/Combinatorics/SetFamily/LYM.lean

@@ -65,7 +65,7 @@ variable [DecidableEq α] [Fintype α]
 /-- The downward **local LYM inequality**, with cancelled denominators. `𝒜` takes up less of `α^(r)`
 (the finsets of card `r`) than `∂𝒜` takes up of `α^(r - 1)`. -/
 theorem card_mul_le_card_shadow_mul (h𝒜 : (𝒜 : Set (Finset α)).Sized r) :
-    𝒜.card * r ≤ ((∂ ) 𝒜).card * (Fintype.card α - r + 1) := by
+    𝒜.card * r ≤ (∂ 𝒜).card * (Fintype.card α - r + 1) := by
   let i : DecidableRel ((. ⊆ .) : Finset α → Finset α → Prop) := fun _ _ => Classical.dec _
   refine' card_mul_le_card_mul' (· ⊆ ·) (fun s hs => _) (fun s hs => _)
   · rw [← h𝒜 hs, ← card_image_of_injOn s.erase_injOn]
@@ -93,7 +93,7 @@ theorem card_mul_le_card_shadow_mul (h𝒜 : (𝒜 : Set (Finset α)).Sized r) :
 than `∂𝒜` takes up of `α^(r - 1)`. -/
 theorem card_div_choose_le_card_shadow_div_choose (hr : r ≠ 0)
     (h𝒜 : (𝒜 : Set (Finset α)).Sized r) : (𝒜.card : 𝕜) / (Fintype.card α).choose r
-    ≤ ((∂ ) 𝒜).card / (Fintype.card α).choose (r - 1) := by
+    ≤ (∂ 𝒜).card / (Fintype.card α).choose (r - 1) := by
   obtain hr' | hr' := lt_or_le (Fintype.card α) r
   · rw [choose_eq_zero_of_lt hr', cast_zero, div_zero]
     exact div_nonneg (cast_nonneg _) (cast_nonneg _)
@@ -149,7 +149,7 @@ theorem falling_zero_subset : falling 0 𝒜 ⊆ {∅} :=
   subset_singleton_iff'.2 fun _ ht => card_eq_zero.1 <| sized_falling _ _ ht
 #align finset.falling_zero_subset Finset.falling_zero_subset
 
-theorem slice_union_shadow_falling_succ : 𝒜 # k ∪ (∂ ) (falling (k + 1) 𝒜) = falling k 𝒜 := by
+theorem slice_union_shadow_falling_succ : 𝒜 # k ∪ ∂ (falling (k + 1) 𝒜) = falling k 𝒜 := by
   ext s
   simp_rw [mem_union, mem_slice, mem_shadow_iff, mem_falling]
   constructor
@@ -171,7 +171,7 @@ variable {𝒜 k}
 /-- The shadow of `falling m 𝒜` is disjoint from the `n`-sized elements of `𝒜`, thanks to the
 antichain property. -/
 theorem IsAntichain.disjoint_slice_shadow_falling {m n : ℕ}
-    (h𝒜 : IsAntichain (· ⊆ ·) (𝒜 : Set (Finset α))) : Disjoint (𝒜 # m) ((∂ ) (falling n 𝒜)) :=
+    (h𝒜 : IsAntichain (· ⊆ ·) (𝒜 : Set (Finset α))) : Disjoint (𝒜 # m) (∂ (falling n 𝒜)) :=
   disjoint_right.2 fun s h₁ h₂ => by
     simp_rw [mem_shadow_iff, mem_falling] at h₁
     obtain ⟨s, ⟨⟨t, ht, hst⟩, _⟩, a, ha, rfl⟩ := h₁

Mathlib/Combinatorics/SetFamily/Shadow.lean

@@ -65,18 +65,18 @@ def shadow (𝒜 : Finset (Finset α)) : Finset (Finset α) :=
 
 -- mathport name: finset.shadow
 -- Porting note: added `inherit_doc` to calm linter
-@[inherit_doc] scoped[FinsetFamily] notation:90 "∂ " => Finset.shadow
+@[inherit_doc] scoped[FinsetFamily] notation:max "∂ " => Finset.shadow
 -- Porting note: had to open FinsetFamily
 open FinsetFamily
 
 /-- The shadow of the empty set is empty. -/
 @[simp]
-theorem shadow_empty : (∂ ) (∅ : Finset (Finset α)) = ∅ :=
+theorem shadow_empty : ∂ (∅ : Finset (Finset α)) = ∅ :=
   rfl
 #align finset.shadow_empty Finset.shadow_empty
 
 @[simp]
-theorem shadow_singleton_empty : (∂ ) ({∅} : Finset (Finset α)) = ∅ :=
+theorem shadow_singleton_empty : ∂ ({∅} : Finset (Finset α)) = ∅ :=
   rfl
 #align finset.shadow_singleton_empty Finset.shadow_singleton_empty
 
@@ -89,17 +89,17 @@ theorem shadow_monotone : Monotone (shadow : Finset (Finset α) → Finset (Fins
 
 /-- `s` is in the shadow of `𝒜` iff there is an `t ∈ 𝒜` from which we can remove one element to
 get `s`. -/
-theorem mem_shadow_iff : s ∈ (∂ ) 𝒜 ↔ ∃ t ∈ 𝒜, ∃ a ∈ t, erase t a = s := by
+theorem mem_shadow_iff : s ∈ ∂ 𝒜 ↔ ∃ t ∈ 𝒜, ∃ a ∈ t, erase t a = s := by
   simp only [shadow, mem_sup, mem_image]
 #align finset.mem_shadow_iff Finset.mem_shadow_iff
 
-theorem erase_mem_shadow (hs : s ∈ 𝒜) (ha : a ∈ s) : erase s a ∈ (∂ ) 𝒜 :=
+theorem erase_mem_shadow (hs : s ∈ 𝒜) (ha : a ∈ s) : erase s a ∈ ∂ 𝒜 :=
   mem_shadow_iff.2 ⟨s, hs, a, ha, rfl⟩
 #align finset.erase_mem_shadow Finset.erase_mem_shadow
 
 /-- `t` is in the shadow of `𝒜` iff we can add an element to it so that the resulting finset is in
 `𝒜`. -/
-theorem mem_shadow_iff_insert_mem : s ∈ (∂ ) 𝒜 ↔ ∃ (a : _) (_ : a ∉ s), insert a s ∈ 𝒜 := by
+theorem mem_shadow_iff_insert_mem : s ∈ ∂ 𝒜 ↔ ∃ (a : _) (_ : a ∉ s), insert a s ∈ 𝒜 := by
   refine' mem_shadow_iff.trans ⟨_, _⟩
   · rintro ⟨s, hs, a, ha, rfl⟩
     refine' ⟨a, not_mem_erase a s, _⟩
@@ -110,22 +110,22 @@ theorem mem_shadow_iff_insert_mem : s ∈ (∂ ) 𝒜 ↔ ∃ (a : _) (_ : a ∉
 
 /-- The shadow of a family of `r`-sets is a family of `r - 1`-sets. -/
 protected theorem Set.Sized.shadow (h𝒜 : (𝒜 : Set (Finset α)).Sized r) :
-    ((∂ ) 𝒜 : Set (Finset α)).Sized (r - 1) := by
+    (∂ 𝒜 : Set (Finset α)).Sized (r - 1) := by
   intro A h
   obtain ⟨A, hA, i, hi, rfl⟩ := mem_shadow_iff.1 h
   rw [card_erase_of_mem hi, h𝒜 hA]
 #align finset.set.sized.shadow Finset.Set.Sized.shadow
 
 theorem sized_shadow_iff (h : ∅ ∉ 𝒜) :
-    ((∂ ) 𝒜 : Set (Finset α)).Sized r ↔ (𝒜 : Set (Finset α)).Sized (r + 1) := by
+    (∂ 𝒜 : Set (Finset α)).Sized r ↔ (𝒜 : Set (Finset α)).Sized (r + 1) := by
   refine' ⟨fun h𝒜 s hs => _, Set.Sized.shadow⟩
   obtain ⟨a, ha⟩ := nonempty_iff_ne_empty.2 (ne_of_mem_of_not_mem hs h)
   rw [← h𝒜 (erase_mem_shadow hs ha), card_erase_add_one ha]
 #align finset.sized_shadow_iff Finset.sized_shadow_iff
 
 /-- `s ∈ ∂ 𝒜` iff `s` is exactly one element less than something from `𝒜` -/
 theorem mem_shadow_iff_exists_mem_card_add_one :
-    s ∈ (∂ ) 𝒜 ↔ ∃ t ∈ 𝒜, s ⊆ t ∧ t.card = s.card + 1 := by
+    s ∈ ∂ 𝒜 ↔ ∃ t ∈ 𝒜, s ⊆ t ∧ t.card = s.card + 1 := by
   refine' mem_shadow_iff_insert_mem.trans ⟨_, _⟩
   · rintro ⟨a, ha, hs⟩
     exact ⟨insert a s, hs, subset_insert _ _, card_insert_of_not_mem ha⟩
@@ -138,7 +138,7 @@ theorem mem_shadow_iff_exists_mem_card_add_one :
 #align finset.mem_shadow_iff_exists_mem_card_add_one Finset.mem_shadow_iff_exists_mem_card_add_one
 
 /-- Being in the shadow of `𝒜` means we have a superset in `𝒜`. -/
-theorem exists_subset_of_mem_shadow (hs : s ∈ (∂ ) 𝒜) : ∃ t ∈ 𝒜, s ⊆ t :=
+theorem exists_subset_of_mem_shadow (hs : s ∈ ∂ 𝒜) : ∃ t ∈ 𝒜, s ⊆ t :=
   let ⟨t, ht, hst⟩ := mem_shadow_iff_exists_mem_card_add_one.1 hs
   ⟨t, ht, hst.1⟩
 #align finset.exists_subset_of_mem_shadow Finset.exists_subset_of_mem_shadow
@@ -189,11 +189,11 @@ def upShadow (𝒜 : Finset (Finset α)) : Finset (Finset α) :=
 
 -- mathport name: finset.up_shadow
 -- Porting note: added `inherit_doc` to calm linter
-@[inherit_doc] scoped[FinsetFamily] notation:90 "∂⁺ " => Finset.upShadow
+@[inherit_doc] scoped[FinsetFamily] notation:max "∂⁺ " => Finset.upShadow
 
 /-- The upper shadow of the empty set is empty. -/
 @[simp]
-theorem upShadow_empty : (∂⁺ ) (∅ : Finset (Finset α)) = ∅ :=
+theorem upShadow_empty : ∂⁺ (∅ : Finset (Finset α)) = ∅ :=
   rfl
 #align finset.up_shadow_empty Finset.upShadow_empty
 
@@ -205,25 +205,25 @@ theorem upShadow_monotone : Monotone (upShadow : Finset (Finset α) → Finset (
 
 /-- `s` is in the upper shadow of `𝒜` iff there is an `t ∈ 𝒜` from which we can remove one element
 to get `s`. -/
-theorem mem_upShadow_iff : s ∈ (∂⁺ ) 𝒜 ↔ ∃ t ∈ 𝒜, ∃ (a : _) (_ : a ∉ t), insert a t = s := by
+theorem mem_upShadow_iff : s ∈ ∂⁺ 𝒜 ↔ ∃ t ∈ 𝒜, ∃ (a : _) (_ : a ∉ t), insert a t = s := by
   simp_rw [upShadow, mem_sup, mem_image, exists_prop, mem_compl]
 #align finset.mem_up_shadow_iff Finset.mem_upShadow_iff
 
-theorem insert_mem_upShadow (hs : s ∈ 𝒜) (ha : a ∉ s) : insert a s ∈ (∂⁺ ) 𝒜 :=
+theorem insert_mem_upShadow (hs : s ∈ 𝒜) (ha : a ∉ s) : insert a s ∈ ∂⁺ 𝒜 :=
   mem_upShadow_iff.2 ⟨s, hs, a, ha, rfl⟩
 #align finset.insert_mem_up_shadow Finset.insert_mem_upShadow
 
 /-- The upper shadow of a family of `r`-sets is a family of `r + 1`-sets. -/
 protected theorem Set.Sized.upShadow (h𝒜 : (𝒜 : Set (Finset α)).Sized r) :
-    ((∂⁺ ) 𝒜 : Set (Finset α)).Sized (r + 1) := by
+    (∂⁺ 𝒜 : Set (Finset α)).Sized (r + 1) := by
   intro A h
   obtain ⟨A, hA, i, hi, rfl⟩ := mem_upShadow_iff.1 h
   rw [card_insert_of_not_mem hi, h𝒜 hA]
 #align finset.set.sized.up_shadow Finset.Set.Sized.upShadow
 
 /-- `t` is in the upper shadow of `𝒜` iff we can remove an element from it so that the resulting
 finset is in `𝒜`. -/
-theorem mem_upShadow_iff_erase_mem : s ∈ (∂⁺ ) 𝒜 ↔ ∃ a ∈ s, s.erase a ∈ 𝒜 := by
+theorem mem_upShadow_iff_erase_mem : s ∈ ∂⁺ 𝒜 ↔ ∃ a ∈ s, s.erase a ∈ 𝒜 := by
   refine' mem_upShadow_iff.trans ⟨_, _⟩
   · rintro ⟨s, hs, a, ha, rfl⟩
     refine' ⟨a, mem_insert_self a s, _⟩
@@ -234,7 +234,7 @@ theorem mem_upShadow_iff_erase_mem : s ∈ (∂⁺ ) 𝒜 ↔ ∃ a ∈ s, s.era
 
 /-- `s ∈ ∂⁺ 𝒜` iff `s` is exactly one element less than something from `𝒜`. -/
 theorem mem_upShadow_iff_exists_mem_card_add_one :
-    s ∈ (∂⁺ ) 𝒜 ↔ ∃ t ∈ 𝒜, t ⊆ s ∧ t.card + 1 = s.card := by
+    s ∈ ∂⁺ 𝒜 ↔ ∃ t ∈ 𝒜, t ⊆ s ∧ t.card + 1 = s.card := by
   refine' mem_upShadow_iff_erase_mem.trans ⟨_, _⟩
   · rintro ⟨a, ha, hs⟩
     exact ⟨s.erase a, hs, erase_subset _ _, card_erase_add_one ha⟩
@@ -246,7 +246,7 @@ theorem mem_upShadow_iff_exists_mem_card_add_one :
 #align finset.mem_up_shadow_iff_exists_mem_card_add_one Finset.mem_upShadow_iff_exists_mem_card_add_one
 
 /-- Being in the upper shadow of `𝒜` means we have a superset in `𝒜`. -/
-theorem exists_subset_of_mem_upShadow (hs : s ∈ (∂⁺ ) 𝒜) : ∃ t ∈ 𝒜, t ⊆ s :=
+theorem exists_subset_of_mem_upShadow (hs : s ∈ ∂⁺ 𝒜) : ∃ t ∈ 𝒜, t ⊆ s :=
   let ⟨t, ht, hts, _⟩ := mem_upShadow_iff_exists_mem_card_add_one.1 hs
   ⟨t, ht, hts⟩
 #align finset.exists_subset_of_mem_up_shadow Finset.exists_subset_of_mem_upShadow
@@ -281,7 +281,7 @@ theorem mem_upShadow_iff_exists_mem_card_add :
 #align finset.mem_up_shadow_iff_exists_mem_card_add Finset.mem_upShadow_iff_exists_mem_card_add
 
 @[simp]
-theorem shadow_image_compl : ((∂ ) 𝒜).image compl = (∂⁺ ) (𝒜.image compl) := by
+theorem shadow_image_compl : (∂ 𝒜).image compl = ∂⁺ (𝒜.image compl) := by
   ext s
   simp only [mem_image, exists_prop, mem_shadow_iff, mem_upShadow_iff]
   constructor
@@ -292,7 +292,7 @@ theorem shadow_image_compl : ((∂ ) 𝒜).image compl = (∂⁺ ) (𝒜.image c
 #align finset.shadow_image_compl Finset.shadow_image_compl
 
 @[simp]
-theorem upShadow_image_compl : ((∂⁺ ) 𝒜).image compl = (∂ ) (𝒜.image compl) := by
+theorem upShadow_image_compl : (∂⁺ 𝒜).image compl = ∂ (𝒜.image compl) := by
   ext s
   simp only [mem_image, exists_prop, mem_shadow_iff, mem_upShadow_iff]
   constructor