diff --git a/Mathlib/Algebra/Order/Floor.lean b/Mathlib/Algebra/Order/Floor.lean index 6bd51a8b46a96..478a21d5d6e8c 100644 --- a/Mathlib/Algebra/Order/Floor.lean +++ b/Mathlib/Algebra/Order/Floor.lean @@ -222,21 +222,13 @@ theorem floor_eq_zero : ⌊a⌋₊ = 0 ↔ a < 1 := by rw [← lt_one_iff, ← @cast_one α] exact floor_lt' Nat.one_ne_zero -#adaptation_note -/-- -After nightly-2024-09-06 we can remove the `_root_` prefix below. --/ theorem floor_eq_iff (ha : 0 ≤ a) : ⌊a⌋₊ = n ↔ ↑n ≤ a ∧ a < ↑n + 1 := by rw [← le_floor_iff ha, ← Nat.cast_one, ← Nat.cast_add, ← floor_lt ha, Nat.lt_add_one_iff, - le_antisymm_iff, _root_.and_comm] + le_antisymm_iff, and_comm] -#adaptation_note -/-- -After nightly-2024-09-06 we can remove the `_root_` prefix below. --/ theorem floor_eq_iff' (hn : n ≠ 0) : ⌊a⌋₊ = n ↔ ↑n ≤ a ∧ a < ↑n + 1 := by rw [← le_floor_iff' hn, ← Nat.cast_one, ← Nat.cast_add, ← floor_lt' (Nat.add_one_ne_zero n), - Nat.lt_add_one_iff, le_antisymm_iff, _root_.and_comm] + Nat.lt_add_one_iff, le_antisymm_iff, and_comm] theorem floor_eq_on_Ico (n : ℕ) : ∀ a ∈ (Set.Ico n (n + 1) : Set α), ⌊a⌋₊ = n := fun _ ⟨h₀, h₁⟩ => (floor_eq_iff <| n.cast_nonneg.trans h₀).mpr ⟨h₀, h₁⟩ @@ -328,14 +320,10 @@ theorem floor_lt_ceil_of_lt_of_pos {a b : α} (h : a < b) (h' : 0 < b) : ⌊a⌋ exact h.trans_le (le_ceil _) · rwa [floor_of_nonpos ha.le, lt_ceil, Nat.cast_zero] -#adaptation_note -/-- -After nightly-2024-09-06 we can remove the `_root_` prefix below. --/ theorem ceil_eq_iff (hn : n ≠ 0) : ⌈a⌉₊ = n ↔ ↑(n - 1) < a ∧ a ≤ n := by rw [← ceil_le, ← not_le, ← ceil_le, not_le, tsub_lt_iff_right (Nat.add_one_le_iff.2 (pos_iff_ne_zero.2 hn)), Nat.lt_add_one_iff, - le_antisymm_iff, _root_.and_comm] + le_antisymm_iff, and_comm] @[simp] theorem preimage_ceil_zero : (Nat.ceil : α → ℕ) ⁻¹' {0} = Iic 0 := diff --git a/Mathlib/Algebra/Ring/Parity.lean b/Mathlib/Algebra/Ring/Parity.lean index d257486efbda8..9205b9aeff65a 100644 --- a/Mathlib/Algebra/Ring/Parity.lean +++ b/Mathlib/Algebra/Ring/Parity.lean @@ -233,14 +233,10 @@ lemma even_or_odd (n : ℕ) : Even n ∨ Odd n := (even_xor_odd n).or lemma even_or_odd' (n : ℕ) : ∃ k, n = 2 * k ∨ n = 2 * k + 1 := by simpa only [← two_mul, exists_or, Odd, Even] using even_or_odd n -#adaptation_note -/-- -After nightly-2024-09-06 we can remove the `_root_` prefix below. --/ lemma even_xor_odd' (n : ℕ) : ∃ k, Xor' (n = 2 * k) (n = 2 * k + 1) := by obtain ⟨k, rfl⟩ | ⟨k, rfl⟩ := even_or_odd n <;> use k · simpa only [← two_mul, eq_self_iff_true, xor_true] using (succ_ne_self (2 * k)).symm - · simpa only [xor_true, _root_.xor_comm] using (succ_ne_self _) + · simpa only [xor_true, xor_comm] using (succ_ne_self _) lemma mod_two_add_add_odd_mod_two (m : ℕ) {n : ℕ} (hn : Odd n) : m % 2 + (m + n) % 2 = 1 := ((even_or_odd m).elim fun hm ↦ by rw [even_iff.1 hm, odd_iff.1 (hm.add_odd hn)]) fun hm ↦ by diff --git a/Mathlib/Combinatorics/SetFamily/KruskalKatona.lean b/Mathlib/Combinatorics/SetFamily/KruskalKatona.lean index 29713f6399feb..8b5ce0135fec7 100644 --- a/Mathlib/Combinatorics/SetFamily/KruskalKatona.lean +++ b/Mathlib/Combinatorics/SetFamily/KruskalKatona.lean @@ -52,10 +52,6 @@ namespace Finset namespace Colex variable {α : Type*} [LinearOrder α] {𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)} {s t : Finset α} {r : ℕ} -#adaptation_note -/-- -After nightly-2024-09-06 we can remove the `_root_` prefix below. --/ /-- This is important for iterating Kruskal-Katona: the shadow of an initial segment is also an initial segment. -/ lemma shadow_initSeg [Fintype α] (hs : s.Nonempty) : @@ -71,7 +67,7 @@ lemma shadow_initSeg [Fintype α] (hs : s.Nonempty) : · simpa [ha] using erase_le_erase_min' hts hst.ge (mem_insert_self _ _) -- Now show that if t ≤ s - min s, there is j such that t ∪ j ≤ s -- We choose j as the smallest thing not in t - simp_rw [le_iff_eq_or_lt, lt_iff_exists_filter_lt, mem_sdiff, filter_inj, _root_.and_assoc] + simp_rw [le_iff_eq_or_lt, lt_iff_exists_filter_lt, mem_sdiff, filter_inj, and_assoc] simp only [toColex_inj, ofColex_toColex, ne_eq, and_imp] rintro cards' (rfl | ⟨k, hks, hkt, z⟩) -- If t = s - min s, then use j = min s so t ∪ j = s @@ -129,17 +125,13 @@ variable {α : Type*} [LinearOrder α] {s U V : Finset α} {n : ℕ} namespace UV -#adaptation_note -/-- -After nightly-2024-09-06 we can remove the `_root_` prefix below. --/ /-- Applying the compression makes the set smaller in colex. This is intuitive since a portion of the set is being "shifted down" as `max U < max V`. -/ lemma toColex_compress_lt_toColex {hU : U.Nonempty} {hV : V.Nonempty} (h : max' U hU < max' V hV) (hA : compress U V s ≠ s) : toColex (compress U V s) < toColex s := by rw [compress, ite_ne_right_iff] at hA rw [compress, if_pos hA.1, lt_iff_exists_filter_lt] - simp_rw [mem_sdiff (s := s), filter_inj, _root_.and_assoc] + simp_rw [mem_sdiff (s := s), filter_inj, and_assoc] refine ⟨_, hA.1.2 <| max'_mem _ hV, not_mem_sdiff_of_mem_right <| max'_mem _ _, fun a ha ↦ ?_⟩ have : a ∉ V := fun H ↦ ha.not_le (le_max' _ _ H) have : a ∉ U := fun H ↦ ha.not_lt ((le_max' _ _ H).trans_lt h) diff --git a/Mathlib/Combinatorics/SimpleGraph/Regularity/Equitabilise.lean b/Mathlib/Combinatorics/SimpleGraph/Regularity/Equitabilise.lean index e74fad0ddff83..96d140587f9cc 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Regularity/Equitabilise.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Regularity/Equitabilise.lean @@ -32,10 +32,6 @@ namespace Finpartition variable {α : Type*} [DecidableEq α] {s t : Finset α} {m n a b : ℕ} {P : Finpartition s} -#adaptation_note -/-- -After nightly-2024-09-06 we can remove the `_root_` prefix below. --/ /-- Given a partition `P` of `s`, as well as a proof that `a * m + b * (m + 1) = s.card`, we can find a new partition `Q` of `s` where each part has size `m` or `m + 1`, every part of `P` is the union of parts of `Q` plus at most `m` extra elements, there are `b` parts of size `m + 1` and @@ -50,7 +46,7 @@ theorem equitabilise_aux (hs : a * m + b * (m + 1) = s.card) : obtain rfl | m_pos := m.eq_zero_or_pos · refine ⟨⊥, by simp, ?_, by simpa [Finset.filter_true_of_mem] using hs.symm⟩ simp only [le_zero_iff, card_eq_zero, mem_biUnion, exists_prop, mem_filter, id, - _root_.and_assoc, sdiff_eq_empty_iff_subset, subset_iff] + and_assoc, sdiff_eq_empty_iff_subset, subset_iff] exact fun x hx a ha => ⟨{a}, mem_map_of_mem _ (P.le hx ha), singleton_subset_iff.2 ha, mem_singleton_self _⟩ -- Prove the case `m > 0` by strong induction on `s` diff --git a/Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean b/Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean index a96ef7c723fb8..c3c8b49e6cd43 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean @@ -83,10 +83,6 @@ lemma LocallyLinear.map (f : α ↪ β) (hG : G.LocallyLinear) : (G.map f).Local · rw [← Equiv.coe_toEmbedding, ← map_symm] exact LocallyLinear.map _ -#adaptation_note -/-- -After nightly-2024-09-06 we can remove the `_root_` prefix below. --/ lemma edgeDisjointTriangles_iff_mem_sym2_subsingleton : G.EdgeDisjointTriangles ↔ ∀ ⦃e : Sym2 α⦄, ¬ e.IsDiag → {s ∈ G.cliqueSet 3 | e ∈ (s : Finset α).sym2}.Subsingleton := by @@ -96,7 +92,7 @@ lemma edgeDisjointTriangles_iff_mem_sym2_subsingleton : ext s simp only [mem_sym2_iff, Sym2.mem_iff, forall_eq_or_imp, forall_eq, Set.sep_and, Set.mem_inter_iff, Set.mem_sep_iff, mem_cliqueSet_iff, Set.mem_setOf_eq, - and_and_and_comm (b := _ ∈ _), _root_.and_self, is3Clique_iff] + and_and_and_comm (b := _ ∈ _), and_self, is3Clique_iff] constructor · rintro ⟨⟨c, d, e, hcd, hce, hde, rfl⟩, hab⟩ simp only [mem_insert, mem_singleton] at hab diff --git a/Mathlib/Data/Finset/NatDivisors.lean b/Mathlib/Data/Finset/NatDivisors.lean index 03edf844dbd26..cbc7aa896c2f5 100644 --- a/Mathlib/Data/Finset/NatDivisors.lean +++ b/Mathlib/Data/Finset/NatDivisors.lean @@ -16,16 +16,12 @@ exhibiting `Nat.divisors` as a multiplicative homomorphism from `ℕ` to `Finset open Nat Finset open scoped Pointwise -#adaptation_note -/-- -After nightly-2024-09-06 we can remove the `_root_` prefix below. --/ /-- The divisors of a product of natural numbers are the pointwise product of the divisors of the factors. -/ lemma Nat.divisors_mul (m n : ℕ) : divisors (m * n) = divisors m * divisors n := by ext k simp_rw [mem_mul, mem_divisors, dvd_mul, mul_ne_zero_iff, ← exists_and_left, ← exists_and_right] - simp only [_root_.and_assoc, _root_.and_comm, and_left_comm] + simp only [and_assoc, and_comm, and_left_comm] /-- `Nat.divisors` as a `MonoidHom`. -/ @[simps] diff --git a/Mathlib/Data/Int/Defs.lean b/Mathlib/Data/Int/Defs.lean index 5312b39a07639..6bf06c9ff023a 100644 --- a/Mathlib/Data/Int/Defs.lean +++ b/Mathlib/Data/Int/Defs.lean @@ -43,12 +43,7 @@ protected lemma le_antisymm_iff : a = b ↔ a ≤ b ∧ b ≤ a := protected lemma le_iff_eq_or_lt : a ≤ b ↔ a = b ∨ a < b := by rw [Int.le_antisymm_iff, Int.lt_iff_le_not_le, ← and_or_left]; simp [em] -#adaptation_note -/-- -After nightly-2024-09-06 we can remove the `_root_` prefix below. --/ -protected lemma le_iff_lt_or_eq : a ≤ b ↔ a < b ∨ a = b := by rw [Int.le_iff_eq_or_lt, - _root_.or_comm] +protected lemma le_iff_lt_or_eq : a ≤ b ↔ a < b ∨ a = b := by rw [Int.le_iff_eq_or_lt, or_comm] end Order diff --git a/Mathlib/Data/List/Basic.lean b/Mathlib/Data/List/Basic.lean index 43008b218c99b..d3d29ac80d33d 100644 --- a/Mathlib/Data/List/Basic.lean +++ b/Mathlib/Data/List/Basic.lean @@ -2177,18 +2177,13 @@ end Forall theorem get_attach (L : List α) (i) : (L.attach.get i).1 = L.get ⟨i, length_attach (L := L) ▸ i.2⟩ := by simp -#adaptation_note -/-- -After nightly-2024-09-06 we can remove the `_root_` prefix below. --/ @[simp 1100] theorem mem_map_swap (x : α) (y : β) (xs : List (α × β)) : (y, x) ∈ map Prod.swap xs ↔ (x, y) ∈ xs := by induction' xs with x xs xs_ih · simp only [not_mem_nil, map_nil] · cases' x with a b - simp only [mem_cons, Prod.mk.inj_iff, map, Prod.swap_prod_mk, Prod.exists, xs_ih, - _root_.and_comm] + simp only [mem_cons, Prod.mk.inj_iff, map, Prod.swap_prod_mk, Prod.exists, xs_ih, and_comm] theorem dropSlice_eq (xs : List α) (n m : ℕ) : dropSlice n m xs = xs.take n ++ xs.drop (n + m) := by induction n generalizing xs diff --git a/Mathlib/Data/List/Chain.lean b/Mathlib/Data/List/Chain.lean index a627cab57f2a6..965aee596b838 100644 --- a/Mathlib/Data/List/Chain.lean +++ b/Mathlib/Data/List/Chain.lean @@ -47,10 +47,6 @@ theorem Chain.iff_mem {a : α} {l : List α} : theorem chain_singleton {a b : α} : Chain R a [b] ↔ R a b := by simp only [chain_cons, Chain.nil, and_true] -#adaptation_note -/-- -After nightly-2024-09-06 we can remove the `_root_` prefix below. --/ theorem chain_split {a b : α} {l₁ l₂ : List α} : Chain R a (l₁ ++ b :: l₂) ↔ Chain R a (l₁ ++ [b]) ∧ Chain R b l₂ := by induction' l₁ with x l₁ IH generalizing a <;> @@ -243,18 +239,13 @@ theorem Chain'.cons' {x} : ∀ {l : List α}, Chain' R l → (∀ y ∈ l.head?, theorem chain'_cons' {x l} : Chain' R (x :: l) ↔ (∀ y ∈ head? l, R x y) ∧ Chain' R l := ⟨fun h => ⟨h.rel_head?, h.tail⟩, fun ⟨h₁, h₂⟩ => h₂.cons' h₁⟩ -#adaptation_note -/-- -After nightly-2024-09-06 we can remove the `_root_` prefixes below. --/ theorem chain'_append : ∀ {l₁ l₂ : List α}, Chain' R (l₁ ++ l₂) ↔ Chain' R l₁ ∧ Chain' R l₂ ∧ ∀ x ∈ l₁.getLast?, ∀ y ∈ l₂.head?, R x y | [], l => by simp - | [a], l => by simp [chain'_cons', _root_.and_comm] + | [a], l => by simp [chain'_cons', and_comm] | a :: b :: l₁, l₂ => by - rw [cons_append, cons_append, chain'_cons, chain'_cons, ← cons_append, chain'_append, - _root_.and_assoc] + rw [cons_append, cons_append, chain'_cons, chain'_cons, ← cons_append, chain'_append, and_assoc] simp theorem Chain'.append (h₁ : Chain' R l₁) (h₂ : Chain' R l₂) @@ -293,16 +284,12 @@ theorem Chain'.imp_head {x y} (h : ∀ {z}, R x z → R y z) {l} (hl : Chain' R Chain' R (y :: l) := hl.tail.cons' fun _ hz => h <| hl.rel_head? hz -#adaptation_note -/-- -After nightly-2024-09-06 we can remove the `_root_` prefix below. --/ theorem chain'_reverse : ∀ {l}, Chain' R (reverse l) ↔ Chain' (flip R) l | [] => Iff.rfl | [a] => by simp only [chain'_singleton, reverse_singleton] | a :: b :: l => by rw [chain'_cons, reverse_cons, reverse_cons, append_assoc, cons_append, nil_append, - chain'_split, ← reverse_cons, @chain'_reverse (b :: l), _root_.and_comm, chain'_pair, flip] + chain'_split, ← reverse_cons, @chain'_reverse (b :: l), and_comm, chain'_pair, flip] theorem chain'_iff_get {R} : ∀ {l : List α}, Chain' R l ↔ ∀ (i : ℕ) (h : i < length l - 1), @@ -320,10 +307,6 @@ theorem Chain'.append_overlap {l₁ l₂ l₃ : List α} (h₁ : Chain' R (l₁ h₁.append h₂.right_of_append <| by simpa only [getLast?_append_of_ne_nil _ hn] using (chain'_append.1 h₂).2.2 -#adaptation_note -/-- -After nightly-2024-09-06 we can remove the `_root_` prefix below. --/ lemma chain'_join : ∀ {L : List (List α)}, [] ∉ L → (Chain' R L.join ↔ (∀ l ∈ L, Chain' R l) ∧ L.Chain' (fun l₁ l₂ => ∀ᵉ (x ∈ l₁.getLast?) (y ∈ l₂.head?), R x y)) @@ -333,7 +316,7 @@ lemma chain'_join : ∀ {L : List (List α)}, [] ∉ L → rw [mem_cons, not_or, ← Ne] at hL rw [join, chain'_append, chain'_join hL.2, forall_mem_cons, chain'_cons] rw [mem_cons, not_or, ← Ne] at hL - simp only [forall_mem_cons, _root_.and_assoc, join, head?_append_of_ne_nil _ hL.2.1.symm] + simp only [forall_mem_cons, and_assoc, join, head?_append_of_ne_nil _ hL.2.1.symm] exact Iff.rfl.and (Iff.rfl.and <| Iff.rfl.and and_comm) /-- If `a` and `b` are related by the reflexive transitive closure of `r`, then there is an diff --git a/Mathlib/Data/List/Nodup.lean b/Mathlib/Data/List/Nodup.lean index e8c9adf26282f..f1a4e94793afc 100644 --- a/Mathlib/Data/List/Nodup.lean +++ b/Mathlib/Data/List/Nodup.lean @@ -102,17 +102,13 @@ theorem nodup_iff_get?_ne_get? {l : List α} : l.Nodup ↔ ∀ i j : ℕ, i < j → j < l.length → l.get? i ≠ l.get? j := by simp [nodup_iff_getElem?_ne_getElem?] -#adaptation_note -/-- -After nightly-2024-09-06 we can remove the `_root_` prefix below. --/ theorem Nodup.ne_singleton_iff {l : List α} (h : Nodup l) (x : α) : l ≠ [x] ↔ l = [] ∨ ∃ y ∈ l, y ≠ x := by induction' l with hd tl hl · simp · specialize hl h.of_cons by_cases hx : tl = [x] - · simpa [hx, _root_.and_comm, and_or_left] using h + · simpa [hx, and_comm, and_or_left] using h · rw [← Ne, hl] at hx rcases hx with (rfl | ⟨y, hy, hx⟩) · simp @@ -178,13 +174,9 @@ theorem Nodup.append (d₁ : Nodup l₁) (d₂ : Nodup l₂) (dj : Disjoint l₁ theorem nodup_append_comm {l₁ l₂ : List α} : Nodup (l₁ ++ l₂) ↔ Nodup (l₂ ++ l₁) := by simp only [nodup_append, and_left_comm, disjoint_comm] -#adaptation_note -/-- -After nightly-2024-09-06 we can remove the `_root_` prefix below. --/ theorem nodup_middle {a : α} {l₁ l₂ : List α} : Nodup (l₁ ++ a :: l₂) ↔ Nodup (a :: (l₁ ++ l₂)) := by - simp only [nodup_append, not_or, and_left_comm, _root_.and_assoc, nodup_cons, mem_append, + simp only [nodup_append, not_or, and_left_comm, and_assoc, nodup_cons, mem_append, disjoint_cons_right] theorem Nodup.of_map (f : α → β) {l : List α} : Nodup (map f l) → Nodup l := @@ -267,14 +259,10 @@ theorem nodup_join {L : List (List α)} : Nodup (join L) ↔ (∀ l ∈ L, Nodup l) ∧ Pairwise Disjoint L := by simp only [Nodup, pairwise_join, disjoint_left.symm, forall_mem_ne] -#adaptation_note -/-- -After nightly-2024-09-06 we can remove the `_root_` prefix below. --/ theorem nodup_bind {l₁ : List α} {f : α → List β} : Nodup (l₁.bind f) ↔ (∀ x ∈ l₁, Nodup (f x)) ∧ Pairwise (fun a b : α => Disjoint (f a) (f b)) l₁ := by - simp only [List.bind, nodup_join, pairwise_map, _root_.and_comm, and_left_comm, mem_map, + simp only [List.bind, nodup_join, pairwise_map, and_comm, and_left_comm, mem_map, exists_imp, and_imp] rw [show (∀ (l : List β) (x : α), f x = l → x ∈ l₁ → Nodup l) ↔ ∀ x : α, x ∈ l₁ → Nodup (f x) from forall_swap.trans <| forall_congr' fun _ => forall_eq'] diff --git a/Mathlib/Data/List/Perm.lean b/Mathlib/Data/List/Perm.lean index f0e74dcc0d2b3..14611136f55f6 100644 --- a/Mathlib/Data/List/Perm.lean +++ b/Mathlib/Data/List/Perm.lean @@ -246,17 +246,13 @@ theorem Perm.bagInter {l₁ l₂ t₁ t₂ : List α} (hl : l₁ ~ l₂) (ht : t l₁.bagInter t₁ ~ l₂.bagInter t₂ := ht.bagInter_left l₂ ▸ hl.bagInter_right _ -#adaptation_note -/-- -After nightly-2024-09-06 we can remove the `_root_` prefix below. --/ theorem perm_replicate_append_replicate {l : List α} {a b : α} {m n : ℕ} (h : a ≠ b) : l ~ replicate m a ++ replicate n b ↔ count a l = m ∧ count b l = n ∧ l ⊆ [a, b] := by rw [perm_iff_count, ← Decidable.and_forall_ne a, ← Decidable.and_forall_ne b] suffices l ⊆ [a, b] ↔ ∀ c, c ≠ b → c ≠ a → c ∉ l by simp (config := { contextual := true }) [count_replicate, h, this, count_eq_zero, Ne.symm] trans ∀ c, c ∈ l → c = b ∨ c = a - · simp [subset_def, _root_.or_comm] + · simp [subset_def, or_comm] · exact forall_congr' fun _ => by rw [← and_imp, ← not_or, not_imp_not] theorem Perm.dedup {l₁ l₂ : List α} (p : l₁ ~ l₂) : dedup l₁ ~ dedup l₂ := diff --git a/Mathlib/Data/List/Permutation.lean b/Mathlib/Data/List/Permutation.lean index 37fb13a041412..dfa4674956933 100644 --- a/Mathlib/Data/List/Permutation.lean +++ b/Mathlib/Data/List/Permutation.lean @@ -166,10 +166,6 @@ theorem foldr_permutationsAux2 (t : α) (ts : List α) (r L : List (List α)) : · rfl · simp_rw [foldr_cons, ih, bind_cons, append_assoc, permutationsAux2_append] -#adaptation_note -/-- -After nightly-2024-09-06 we can remove the `_root_` prefix below. --/ theorem mem_foldr_permutationsAux2 {t : α} {ts : List α} {r L : List (List α)} {l' : List α} : l' ∈ foldr (fun y r => (permutationsAux2 t ts r y id).2) r L ↔ l' ∈ r ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ L ∧ l₂ ≠ [] ∧ l' = l₁ ++ t :: l₂ ++ ts := by @@ -180,7 +176,7 @@ theorem mem_foldr_permutationsAux2 {t : α} {ts : List α} {r L : List (List α) ⟨fun ⟨_, aL, l₁, l₂, l0, e, h⟩ => ⟨l₁, l₂, l0, e ▸ aL, h⟩, fun ⟨l₁, l₂, l0, aL, h⟩ => ⟨_, aL, l₁, l₂, l0, rfl, h⟩⟩ rw [foldr_permutationsAux2] - simp only [mem_permutationsAux2', ← this, _root_.or_comm, and_left_comm, mem_append, mem_bind, + simp only [mem_permutationsAux2', ← this, or_comm, and_left_comm, mem_append, mem_bind, append_assoc, cons_append, exists_prop] theorem length_foldr_permutationsAux2 (t : α) (ts : List α) (r L : List (List α)) : diff --git a/Mathlib/Data/List/Rotate.lean b/Mathlib/Data/List/Rotate.lean index 923a8ba69b0ed..04072b6a698df 100644 --- a/Mathlib/Data/List/Rotate.lean +++ b/Mathlib/Data/List/Rotate.lean @@ -104,15 +104,11 @@ theorem rotate_cons_succ (l : List α) (a : α) (n : ℕ) : (a :: l : List α).rotate (n + 1) = (l ++ [a]).rotate n := by rw [rotate_eq_rotate', rotate_eq_rotate', rotate'_cons_succ] -#adaptation_note -/-- -After nightly-2024-09-06 we can remove the `_root_` prefix below. --/ @[simp] theorem mem_rotate : ∀ {l : List α} {a : α} {n : ℕ}, a ∈ l.rotate n ↔ a ∈ l | [], _, n => by simp | a :: l, _, 0 => by simp - | a :: l, _, n + 1 => by simp [rotate_cons_succ, mem_rotate, _root_.or_comm] + | a :: l, _, n + 1 => by simp [rotate_cons_succ, mem_rotate, or_comm] @[simp] theorem length_rotate (l : List α) (n : ℕ) : (l.rotate n).length = l.length := by diff --git a/Mathlib/Data/Multiset/Basic.lean b/Mathlib/Data/Multiset/Basic.lean index 0ecc3f20a0bed..0c4fb024e449e 100644 --- a/Mathlib/Data/Multiset/Basic.lean +++ b/Mathlib/Data/Multiset/Basic.lean @@ -1832,25 +1832,17 @@ theorem filter_filter (q) [DecidablePred q] (s : Multiset α) : filter p (filter q s) = filter (fun a => p a ∧ q a) s := Quot.inductionOn s fun l => by simp -#adaptation_note -/-- -After nightly-2024-09-06 we can remove the `_root_` prefix below. --/ lemma filter_comm (q) [DecidablePred q] (s : Multiset α) : - filter p (filter q s) = filter q (filter p s) := by simp [_root_.and_comm] + filter p (filter q s) = filter q (filter p s) := by simp [and_comm] theorem filter_add_filter (q) [DecidablePred q] (s : Multiset α) : filter p s + filter q s = filter (fun a => p a ∨ q a) s + filter (fun a => p a ∧ q a) s := Multiset.induction_on s rfl fun a s IH => by by_cases p a <;> by_cases q a <;> simp [*] -#adaptation_note -/-- -After nightly-2024-09-06 we can remove the `_root_` prefix below. --/ theorem filter_add_not (s : Multiset α) : filter p s + filter (fun a => ¬p a) s = s := by rw [filter_add_filter, filter_eq_self.2, filter_eq_nil.2] · simp only [add_zero] - · simp [Decidable.em, -Bool.not_eq_true, -not_and, not_and_or, _root_.or_comm] + · simp [Decidable.em, -Bool.not_eq_true, -not_and, not_and_or, or_comm] · simp only [Bool.not_eq_true, decide_eq_true_eq, Bool.eq_false_or_eq_true, decide_True, implies_true, Decidable.em] @@ -2690,13 +2682,9 @@ lemma add_eq_union_left_of_le [DecidableEq α] {s t u : Multiset α} (h : t ≤ · rintro ⟨h0, rfl⟩ exact h0 -#adaptation_note -/-- -After nightly-2024-09-06 we can remove the `_root_` prefix below. --/ lemma add_eq_union_right_of_le [DecidableEq α] {x y z : Multiset α} (h : z ≤ y) : x + y = x ∪ z ↔ y = z ∧ x.Disjoint y := by - simpa only [_root_.and_comm] using add_eq_union_left_of_le h + simpa only [and_comm] using add_eq_union_left_of_le h theorem disjoint_map_map {f : α → γ} {g : β → γ} {s : Multiset α} {t : Multiset β} : Disjoint (s.map f) (t.map g) ↔ ∀ a ∈ s, ∀ b ∈ t, f a ≠ g b := by diff --git a/Mathlib/Data/Nat/Factorization/Basic.lean b/Mathlib/Data/Nat/Factorization/Basic.lean index 1285453521a3b..27ddcf0d3a424 100644 --- a/Mathlib/Data/Nat/Factorization/Basic.lean +++ b/Mathlib/Data/Nat/Factorization/Basic.lean @@ -455,10 +455,6 @@ theorem setOf_pow_dvd_eq_Icc_factorization {n p : ℕ} (pp : p.Prime) (hn : n ext simp [Nat.lt_succ_iff, one_le_iff_ne_zero, pp.pow_dvd_iff_le_factorization hn] -#adaptation_note -/-- -After nightly-2024-09-06 we can remove the `_root_` prefix below. --/ /-- The set of positive powers of prime `p` that divide `n` is exactly the set of positive natural numbers up to `n.factorization p`. -/ theorem Icc_factorization_eq_pow_dvd (n : ℕ) {p : ℕ} (pp : Prime p) : @@ -466,7 +462,7 @@ theorem Icc_factorization_eq_pow_dvd (n : ℕ) {p : ℕ} (pp : Prime p) : rcases eq_or_ne n 0 with (rfl | hn) · simp ext x - simp only [mem_Icc, Finset.mem_filter, mem_Ico, _root_.and_assoc, and_congr_right_iff, + simp only [mem_Icc, Finset.mem_filter, mem_Ico, and_assoc, and_congr_right_iff, pp.pow_dvd_iff_le_factorization hn, iff_and_self] exact fun _ H => lt_of_le_of_lt H (factorization_lt p hn) diff --git a/Mathlib/Data/Nat/Log.lean b/Mathlib/Data/Nat/Log.lean index 744b67ca07c10..f2cf3df6eca07 100644 --- a/Mathlib/Data/Nat/Log.lean +++ b/Mathlib/Data/Nat/Log.lean @@ -121,15 +121,11 @@ lemma log_le_self (b x : ℕ) : log b x ≤ x := theorem lt_pow_succ_log_self {b : ℕ} (hb : 1 < b) (x : ℕ) : x < b ^ (log b x).succ := lt_pow_of_log_lt hb (lt_succ_self _) -#adaptation_note -/-- -After nightly-2024-09-06 we can remove the `_root_` prefix below. --/ theorem log_eq_iff {b m n : ℕ} (h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0) : log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1) := by rcases em (1 < b ∧ n ≠ 0) with (⟨hb, hn⟩ | hbn) · rw [le_antisymm_iff, ← Nat.lt_succ_iff, ← pow_le_iff_le_log, ← lt_pow_iff_log_lt, - _root_.and_comm] <;> assumption + and_comm] <;> assumption have hm : m ≠ 0 := h.resolve_right hbn rw [not_and_or, not_lt, Ne, not_not] at hbn rcases hbn with (hb | rfl) diff --git a/Mathlib/Data/Nat/WithBot.lean b/Mathlib/Data/Nat/WithBot.lean index 418d1347bbc66..125eeae18ef2b 100644 --- a/Mathlib/Data/Nat/WithBot.lean +++ b/Mathlib/Data/Nat/WithBot.lean @@ -30,13 +30,9 @@ theorem add_eq_zero_iff {n m : WithBot ℕ} : n + m = 0 ↔ n = 0 ∧ m = 0 := b · simp [WithBot.add_bot] simp [← WithBot.coe_add, add_eq_zero_iff_of_nonneg] -#adaptation_note -/-- -After nightly-2024-09-06 we can remove the `_root_` prefix below. --/ theorem add_eq_one_iff {n m : WithBot ℕ} : n + m = 1 ↔ n = 0 ∧ m = 1 ∨ n = 1 ∧ m = 0 := by cases n - · simp only [WithBot.bot_add, WithBot.bot_ne_one, WithBot.bot_ne_zero, false_and, _root_.or_self] + · simp only [WithBot.bot_add, WithBot.bot_ne_one, WithBot.bot_ne_zero, false_and, or_self] cases m · simp [WithBot.add_bot] simp [← WithBot.coe_add, Nat.add_eq_one_iff] diff --git a/Mathlib/Data/PFunctor/Univariate/M.lean b/Mathlib/Data/PFunctor/Univariate/M.lean index 699b8b76a816f..73fe251a4dda5 100644 --- a/Mathlib/Data/PFunctor/Univariate/M.lean +++ b/Mathlib/Data/PFunctor/Univariate/M.lean @@ -470,10 +470,6 @@ theorem corec_def {X} (f : X → F X) (x₀ : X) : M.corec f x₀ = M.mk (F.map dsimp only [PFunctor.map] congr -#adaptation_note -/-- -After nightly-2024-09-06 we can remove the `_root_` prefix below. --/ theorem ext_aux [Inhabited (M F)] [DecidableEq F.A] {n : ℕ} (x y z : M F) (hx : Agree' n z x) (hy : Agree' n z y) (hrec : ∀ ps : Path F, n = ps.length → iselect ps x = iselect ps y) : x.approx (n + 1) = y.approx (n + 1) := by diff --git a/Mathlib/Logic/Encodable/Basic.lean b/Mathlib/Logic/Encodable/Basic.lean index c111c09a26737..60412ec201292 100644 --- a/Mathlib/Logic/Encodable/Basic.lean +++ b/Mathlib/Logic/Encodable/Basic.lean @@ -555,13 +555,9 @@ theorem sequence_mono_nat {r : β → β → Prop} {f : α → β} (hf : Directe · exact (Classical.choose_spec (hf p p)).1 · exact (Classical.choose_spec (hf p a)).1 -#adaptation_note -/-- -After nightly-2024-09-06 we can remove the `_root_` prefix below. --/ theorem rel_sequence {r : β → β → Prop} {f : α → β} (hf : Directed r f) (a : α) : r (f a) (f (hf.sequence f (encode a + 1))) := by - simp only [Directed.sequence, add_eq, add_zero, encodek, _root_.and_self] + simp only [Directed.sequence, add_eq, add_zero, encodek, and_self] exact (Classical.choose_spec (hf _ a)).2 variable [Preorder β] {f : α → β} diff --git a/Mathlib/NumberTheory/Bertrand.lean b/Mathlib/NumberTheory/Bertrand.lean index 7f3a1d190e6f7..772c5d12f2dff 100644 --- a/Mathlib/NumberTheory/Bertrand.lean +++ b/Mathlib/NumberTheory/Bertrand.lean @@ -121,10 +121,6 @@ theorem bertrand_main_inequality {n : ℕ} (n_large : 512 ≤ n) : · norm_num1 · exact cast_div_le.trans (by norm_cast) -#adaptation_note -/-- -After nightly-2024-09-06 we can remove the `_root_` prefix below. --/ /-- A lemma that tells us that, in the case where Bertrand's postulate does not hold, the prime factorization of the central binomial coefficient only has factors at most `2 * n / 3 + 1`. -/ @@ -138,7 +134,7 @@ theorem centralBinom_factorization_small (n : ℕ) (n_large : 2 < n) rw [Finset.mem_range, Nat.lt_succ_iff] at hx h2x rw [not_le, div_lt_iff_lt_mul' three_pos, mul_comm x] at h2x replace no_prime := not_exists.mp no_prime x - rw [← _root_.and_assoc, not_and', not_and_or, not_lt] at no_prime + rw [← and_assoc, not_and', not_and_or, not_lt] at no_prime cases' no_prime hx with h h · rw [factorization_eq_zero_of_non_prime n.centralBinom h, Nat.pow_zero] · rw [factorization_centralBinom_of_two_mul_self_lt_three_mul n_large h h2x, Nat.pow_zero] diff --git a/Mathlib/NumberTheory/Divisors.lean b/Mathlib/NumberTheory/Divisors.lean index 43de39c1d54b0..0c98cefad6ecd 100644 --- a/Mathlib/NumberTheory/Divisors.lean +++ b/Mathlib/NumberTheory/Divisors.lean @@ -66,14 +66,10 @@ theorem filter_dvd_eq_properDivisors (h : n ≠ 0) : theorem properDivisors.not_self_mem : ¬n ∈ properDivisors n := by simp [properDivisors] -#adaptation_note -/-- -After nightly-2024-09-06 we can remove the `_root_` prefix below. --/ @[simp] theorem mem_properDivisors {m : ℕ} : n ∈ properDivisors m ↔ n ∣ m ∧ n < m := by rcases eq_or_ne m 0 with (rfl | hm); · simp [properDivisors] - simp only [_root_.and_comm, ← filter_dvd_eq_properDivisors hm, mem_filter, mem_range] + simp only [and_comm, ← filter_dvd_eq_properDivisors hm, mem_filter, mem_range] theorem insert_self_properDivisors (h : n ≠ 0) : insert n (properDivisors n) = divisors n := by rw [divisors, properDivisors, Ico_succ_right_eq_insert_Ico (one_le_iff_ne_zero.2 h), @@ -100,15 +96,11 @@ theorem dvd_of_mem_divisors {m : ℕ} (h : n ∈ divisors m) : n ∣ m := by · apply dvd_zero · simp [mem_divisors.1 h] -#adaptation_note -/-- -After nightly-2024-09-06 we can remove the `_root_` prefix below. --/ @[simp] theorem mem_divisorsAntidiagonal {x : ℕ × ℕ} : x ∈ divisorsAntidiagonal n ↔ x.fst * x.snd = n ∧ n ≠ 0 := by simp only [divisorsAntidiagonal, Finset.mem_Ico, Ne, Finset.mem_filter, Finset.mem_product] - rw [_root_.and_comm] + rw [and_comm] apply and_congr_right rintro rfl constructor <;> intro h @@ -429,14 +421,10 @@ theorem sum_properDivisors_eq_one_iff_prime : ∑ x ∈ n.properDivisors, x = 1 (one_mem_properDivisors_iff_one_lt.2 (succ_lt_succ (Nat.succ_pos _)))) ((sum_singleton _ _).trans h.symm) -#adaptation_note -/-- -After nightly-2024-09-06 we can remove the `_root_` prefix below. --/ theorem mem_properDivisors_prime_pow {p : ℕ} (pp : p.Prime) (k : ℕ) {x : ℕ} : x ∈ properDivisors (p ^ k) ↔ ∃ (j : ℕ) (_ : j < k), x = p ^ j := by rw [mem_properDivisors, Nat.dvd_prime_pow pp, ← exists_and_right] - simp only [exists_prop, _root_.and_assoc] + simp only [exists_prop, and_assoc] apply exists_congr intro a constructor <;> intro h @@ -481,17 +469,13 @@ theorem prod_divisorsAntidiagonal' {M : Type*} [CommMonoid M] (f : ℕ → ℕ rw [← map_swap_divisorsAntidiagonal, Finset.prod_map] exact prod_divisorsAntidiagonal fun i j => f j i -#adaptation_note -/-- -After nightly-2024-09-06 we can remove the `_root_` prefix below. --/ /-- The factors of `n` are the prime divisors -/ theorem primeFactors_eq_to_filter_divisors_prime (n : ℕ) : n.primeFactors = (divisors n).filter Prime := by rcases n.eq_zero_or_pos with (rfl | hn) · simp · ext q - simpa [hn, hn.ne', mem_primeFactorsList] using _root_.and_comm + simpa [hn, hn.ne', mem_primeFactorsList] using and_comm @[deprecated (since := "2024-07-17")] alias prime_divisors_eq_to_filter_divisors_prime := primeFactors_eq_to_filter_divisors_prime diff --git a/Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean b/Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean index b2cb30daa0d3e..392736e26084d 100644 --- a/Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean +++ b/Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean @@ -180,10 +180,6 @@ private theorem sum_Ico_eq_card_lt {p q : ℕ} : (by simp (config := { contextual := true }) only [mem_filter, mem_sigma, and_self_iff, forall_true_iff, mem_product]) (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) -#adaptation_note -/-- -After nightly-2024-09-06 we can remove the `_root_` prefix below. --/ /-- Each of the sums in this lemma is the cardinality of the set of integer points in each of the two triangles formed by the diagonal of the rectangle `(0, p/2) × (0, q/2)`. Adding them gives the number of points in the rectangle. -/ @@ -197,7 +193,7 @@ theorem sum_mul_div_add_sum_mul_div_eq_mul (p q : ℕ) [hp : Fact p.Prime] (hq0 card_equiv (Equiv.prodComm _ _) (fun ⟨_, _⟩ => by simp (config := { contextual := true }) only [mem_filter, and_self_iff, Prod.swap_prod_mk, - forall_true_iff, mem_product, Equiv.prodComm_apply, _root_.and_assoc, and_left_comm]) + forall_true_iff, mem_product, Equiv.prodComm_apply, and_assoc, and_left_comm]) have hdisj : Disjoint ((Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ).filter fun x : ℕ × ℕ => x.2 * p ≤ x.1 * q) ((Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ).filter fun x : ℕ × ℕ => x.1 * q ≤ x.2 * p) := by diff --git a/Mathlib/NumberTheory/SumFourSquares.lean b/Mathlib/NumberTheory/SumFourSquares.lean index a08b8c479c8ee..5d7a765adee86 100644 --- a/Mathlib/NumberTheory/SumFourSquares.lean +++ b/Mathlib/NumberTheory/SumFourSquares.lean @@ -121,10 +121,6 @@ private theorem sum_four_squares_of_two_mul_sum_four_squares {m a b c d : ℤ} have : (∑ x, f (σ x) ^ 2) = ∑ x, f x ^ 2 := Equiv.sum_comp σ (f · ^ 2) simpa only [← hx, ← hy, Fin.sum_univ_four, add_assoc] using this -#adaptation_note -/-- -After nightly-2024-09-06 we can remove the `_root_` prefix below. --/ /-- Lagrange's **four squares theorem** for a prime number. Use `Nat.sum_four_squares` instead. -/ protected theorem Prime.sum_four_squares {p : ℕ} (hp : p.Prime) : ∃ a b c d : ℕ, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = p := by @@ -174,10 +170,9 @@ protected theorem Prime.sum_four_squares {p : ℕ} (hp : p.Prime) : -- The quotient `r` is not zero, because otherwise `f a = f b = f c = f d = 0`, hence -- `m` divides each `a`, `b`, `c`, `d`, thus `m ∣ p` which is impossible. rcases (zero_le r).eq_or_gt with rfl | hr₀ - · replace hr : f a = 0 ∧ f b = 0 ∧ f c = 0 ∧ f d = 0 := by simpa [_root_.and_assoc] using hr + · replace hr : f a = 0 ∧ f b = 0 ∧ f c = 0 ∧ f d = 0 := by simpa [and_assoc] using hr obtain ⟨⟨a, rfl⟩, ⟨b, rfl⟩, ⟨c, rfl⟩, ⟨d, rfl⟩⟩ : m ∣ a ∧ m ∣ b ∧ m ∣ c ∧ m ∣ d := by - simp only [← ZMod.natCast_zmod_eq_zero_iff_dvd, ← hf_mod, hr, Int.cast_zero, - _root_.and_self] + simp only [← ZMod.natCast_zmod_eq_zero_iff_dvd, ← hf_mod, hr, Int.cast_zero, and_self] have : m * m ∣ m * p := habcd ▸ ⟨a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2, by ring⟩ rw [mul_dvd_mul_iff_left hm₀.ne'] at this exact (hp.eq_one_or_self_of_dvd _ this).elim hm₁.ne' hmp.ne diff --git a/Mathlib/Order/Interval/Finset/Nat.lean b/Mathlib/Order/Interval/Finset/Nat.lean index d59c44eaa2139..8be56194d6481 100644 --- a/Mathlib/Order/Interval/Finset/Nat.lean +++ b/Mathlib/Order/Interval/Finset/Nat.lean @@ -185,14 +185,10 @@ theorem Ico_image_const_sub_eq_Ico (hac : a ≤ c) : rintro ⟨x, hx, rfl⟩ omega -#adaptation_note -/-- -After nightly-2024-09-06 we can remove the `_root_` prefix below. --/ theorem Ico_succ_left_eq_erase_Ico : Ico a.succ b = erase (Ico a b) a := by ext x - rw [Ico_succ_left, mem_erase, mem_Ico, mem_Ioo, ← _root_.and_assoc, ne_comm, - _root_.and_comm (a := a ≠ x), lt_iff_le_and_ne] + rw [Ico_succ_left, mem_erase, mem_Ico, mem_Ioo, ← and_assoc, ne_comm, + and_comm (a := a ≠ x), lt_iff_le_and_ne] theorem mod_injOn_Ico (n a : ℕ) : Set.InjOn (· % a) (Finset.Ico n (n + a)) := by induction' n with n ih diff --git a/Mathlib/RingTheory/MvPolynomial/Symmetric/NewtonIdentities.lean b/Mathlib/RingTheory/MvPolynomial/Symmetric/NewtonIdentities.lean index ddadb79adcf83..3aa09ead7b4ab 100644 --- a/Mathlib/RingTheory/MvPolynomial/Symmetric/NewtonIdentities.lean +++ b/Mathlib/RingTheory/MvPolynomial/Symmetric/NewtonIdentities.lean @@ -250,17 +250,13 @@ theorem sum_antidiagonal_card_esymm_psum_eq_zero : simp [← sum_filter_add_sum_filter_not (antidiagonal k) (fun a ↦ a.fst < k), ← mul_esymm_eq_sum, mul_add, ← mul_assoc, ← pow_add, mul_comm ↑k (esymm σ R k)] -#adaptation_note -/-- -After nightly-2024-09-06 we can remove the `_root_` prefix below. --/ /-- A version of Newton's identities which may be more useful in the case that we know the values of the elementary symmetric polynomials and would like to calculate the values of the power sums. -/ theorem psum_eq_mul_esymm_sub_sum (k : ℕ) (h : 0 < k) : psum σ R k = (-1) ^ (k + 1) * k * esymm σ R k - ∑ a ∈ (antidiagonal k).filter (fun a ↦ a.fst ∈ Set.Ioo 0 k), (-1) ^ a.fst * esymm σ R a.fst * psum σ R a.snd := by - simp only [Set.Ioo, Set.mem_setOf_eq, _root_.and_comm] + simp only [Set.Ioo, Set.mem_setOf_eq, and_comm] have hesymm := mul_esymm_eq_sum σ R k rw [← (sum_filter_add_sum_filter_not ((antidiagonal k).filter (fun a ↦ a.fst < k)) (fun a ↦ 0 < a.fst) (fun a ↦ (-1) ^ a.fst * esymm σ R a.fst * psum σ R a.snd))] at hesymm diff --git a/Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean b/Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean index 43e050ec7489d..4a1ad15664ee8 100644 --- a/Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean +++ b/Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean @@ -104,17 +104,12 @@ theorem cyclotomic_pos {n : ℕ} (hn : 2 < n) {R} [LinearOrderedCommRing R] (x : exact hn'.ne' hi.2.2.1 · simpa only [eval_X, eval_one, cyclotomic_two, eval_add] using h.right.le -#adaptation_note -/-- -After nightly-2024-09-06 we can remove the `_root_` prefix below. --/ theorem cyclotomic_pos_and_nonneg (n : ℕ) {R} [LinearOrderedCommRing R] (x : R) : (1 < x → 0 < eval x (cyclotomic n R)) ∧ (1 ≤ x → 0 ≤ eval x (cyclotomic n R)) := by rcases n with (_ | _ | _ | n) - · simp only [cyclotomic_zero, eval_one, zero_lt_one, implies_true, zero_le_one, - _root_.and_self] + · simp only [cyclotomic_zero, eval_one, zero_lt_one, implies_true, zero_le_one, and_self] · simp only [zero_add, cyclotomic_one, eval_sub, eval_X, eval_one, sub_pos, imp_self, sub_nonneg, - _root_.and_self] + and_self] · simp only [zero_add, reduceAdd, cyclotomic_two, eval_add, eval_X, eval_one] constructor <;> intro <;> linarith · constructor <;> intro <;> [skip; apply le_of_lt] <;> apply cyclotomic_pos (by omega)