From e4ff00dbc286946143b088218b7f05acae52e5bd Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Tue, 25 Aug 2026 12:55:15 +0200 Subject: [PATCH 1/3] silence sorry warning --- lakefile.toml | 1 + 1 file changed, 1 insertion(+) diff --git a/lakefile.toml b/lakefile.toml index 86a308a..ed3a6d5 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -6,6 +6,7 @@ lintDriver = "batteries/runLinter" pp.unicode.fun = true autoImplicit = false relaxedAutoImplicit = false +warn.sorry = false [[require]] name = "mathlib" From 8574df3efaed09fa3b56684337420707d6800508 Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Tue, 25 Aug 2026 13:32:45 +0200 Subject: [PATCH 2/3] fix some warnings --- FormalBook/Ch28/BrouwerCovering.lean | 4 +-- FormalBook/Ch28/SpernerBrouwer.lean | 51 +++++++++++++--------------- FormalBook/Ch30/EKRAuxiliary.lean | 2 +- FormalBook/Chapter_09.lean | 15 ++++---- FormalBook/Chapter_20.lean | 30 ++++++++-------- FormalBook/Chapter_28.lean | 10 +++--- FormalBook/Chapter_43.lean | 14 ++++---- FormalBook/Chapter_45.lean | 8 ++--- FormalBook/Mathlib/EdgeFinset.lean | 2 +- 9 files changed, 67 insertions(+), 69 deletions(-) diff --git a/FormalBook/Ch28/BrouwerCovering.lean b/FormalBook/Ch28/BrouwerCovering.lean index 4930e1b..cc5e697 100644 --- a/FormalBook/Ch28/BrouwerCovering.lean +++ b/FormalBook/Ch28/BrouwerCovering.lean @@ -21,7 +21,7 @@ private def acLoop : Path acBase acBase where show QuotientAddGroup.mk (1 : ℝ) = QuotientAddGroup.mk 0 rw [QuotientAddGroup.eq]; simp -private def acCov : IsCoveringMap (QuotientAddGroup.mk : ℝ → AddCircle (1 : ℝ)) := +private theorem acCov : IsCoveringMap (QuotientAddGroup.mk : ℝ → AddCircle (1 : ℝ)) := AddCircle.isCoveringMap_coe 1 private theorem acLoop_lift_eq : @@ -245,7 +245,7 @@ private theorem retraction_from_fp_free {f : ℂ → ℂ} private theorem brouwer_complex (f : ℂ → ℂ) (hf : Continuous f) (hB : ∀ x, ‖x‖ ≤ 1 → ‖f x‖ ≤ 1) : ∃ x, ‖x‖ ≤ 1 ∧ f x = x := by - by_contra h; push_neg at h + by_contra h; push Not at h have hfp : ∀ x, ‖x‖ ≤ 1 → f x ≠ x := fun x hx hfx => (h x hx hfx).elim exact no_retraction_complex (retraction_from_fp_free hf hB hfp) diff --git a/FormalBook/Ch28/SpernerBrouwer.lean b/FormalBook/Ch28/SpernerBrouwer.lean index aed6553..9be46bd 100644 --- a/FormalBook/Ch28/SpernerBrouwer.lean +++ b/FormalBook/Ch28/SpernerBrouwer.lean @@ -135,7 +135,7 @@ vertex extraction) below; `sperner_coloring_rainbow_triangles` is proved modulo /-- The standard 2-simplex equals Mathlib's `stdSimplex`. -/ private theorem stdSimplex2_eq : stdSimplex2 = stdSimplex ℝ (Fin 3) := by - ext x; simp only [stdSimplex2, stdSimplex, Set.mem_setOf_eq] + ext x; simp only [stdSimplex2, stdSimplex, Set.mem_ofPred_eq] /-- The standard 2-simplex is compact. -/ private theorem stdSimplex2_isCompact : IsCompact stdSimplex2 := by @@ -146,14 +146,14 @@ private theorem stdSimplex2_isCompact : IsCompact stdSimplex2 := by private theorem spernerColor_exists {f : (Fin 3 → ℝ) → (Fin 3 → ℝ)} {v : Fin 3 → ℝ} (hv : v ∈ stdSimplex2) (hfv : f v ∈ stdSimplex2) (hne : f v ≠ v) : ∃ i : Fin 3, f v i < v i := by - by_contra h; push_neg at h + by_contra h; push Not at h have hsum_v := hv.2; have hsum_fv := hfv.2 have : ∀ i, f v i = v i := by intro i have hle_sum : ∑ j, v j ≤ ∑ j, f v j := Finset.sum_le_sum (fun j _ => h j) rw [hsum_v, hsum_fv] at hle_sum have hge : f v i ≤ v i := by - by_contra hlt; push_neg at hlt + by_contra hlt; push Not at hlt have : ∑ j, v j < ∑ j, f v j := Finset.sum_lt_sum (fun j _ => h j) ⟨i, Finset.mem_univ _, hlt⟩ linarith @@ -167,7 +167,7 @@ private theorem spernerColor_boundary {f : (Fin 3 → ℝ) → (Fin 3 → ℝ)} (hne : f v ≠ v) : spernerColor f v ≠ j := by have hex := spernerColor_exists hv hfv hne intro heq - unfold spernerColor at heq; rw [dif_pos hex] at heq + unfold spernerColor at heq; rw [dite_eq_left hex] at heq have hchoose := hex.choose_spec rw [heq] at hchoose rw [hvj] at hchoose; linarith [hfv.1 j] @@ -201,7 +201,7 @@ private instance subdivVertDecEq (k : ℕ) : DecidableEq (SubdivVert k) := /-- The coordinate map: send a subdivision vertex to its barycentric point in Δ². -/ @[nolint unusedArguments] -private noncomputable def subdivCoord (k : ℕ) (hk : 0 < k) (v : SubdivVert k) : Fin 3 → ℝ := +private noncomputable def subdivCoord (k : ℕ) (_hk : 0 < k) (v : SubdivVert k) : Fin 3 → ℝ := fun i => (v.1 i : ℝ) / (k : ℝ) private theorem subdivCoord_mem (k : ℕ) (hk : 0 < k) (v : SubdivVert k) : @@ -290,7 +290,7 @@ private noncomputable def subdivTriangulation (k : ℕ) (_hk : 0 < k) : have mkVert_coord0 : ∀ a b (h : a + b ≤ k), (mkVert a b h).1 0 = a := by intro a b h; simp [mkVert, Matrix.cons_val_zero] have mkVert_coord1 : ∀ a b (h : a + b ≤ k), (mkVert a b h).1 1 = b := by - intro a b h; simp [mkVert, Matrix.cons_val_one, Matrix.head_cons] + intro a b h; simp [mkVert, Matrix.cons_val_one] have hcard : ∀ t ∈ allTris, t.card = 3 := by intro t ht simp only [allTris, Finset.mem_biUnion, Finset.mem_univ, true_and] at ht @@ -316,7 +316,7 @@ private noncomputable def subdivTriangulation (k : ℕ) (_hk : 0 < k) : rw [Finset.card_insert_of_notMem, Finset.card_insert_of_notMem, Finset.card_singleton] · simp; exact he12 · simp only [Finset.mem_insert, Finset.mem_singleton] - push_neg; exact ⟨he01, he02⟩ + push Not; exact ⟨he01, he02⟩ · -- Down triangle: (i+1,j), (i,j+1), (i+1,j+1) have h01 : mkVert (i+1) j (by omega) ≠ mkVert i (j+1) (by omega) := by intro h; have := congr_arg (fun v => v.1 0) h; simp [mkVert_coord0] at this @@ -333,7 +333,7 @@ private noncomputable def subdivTriangulation (k : ℕ) (_hk : 0 < k) : rw [Finset.card_insert_of_notMem, Finset.card_insert_of_notMem, Finset.card_singleton] · simp; exact he12 · simp only [Finset.mem_insert, Finset.mem_singleton] - push_neg; exact ⟨he01, he02⟩ + push Not; exact ⟨he01, he02⟩ · simp at hcond refine ⟨m, ⟨allTris, hcard⟩, decode, ?_⟩ -- Adjacency: any two vertices in the same triangle differ by ≤ 1 in each coordinate @@ -357,11 +357,11 @@ private noncomputable def subdivTriangulation (k : ℕ) (_hk : 0 < k) : · -- Up triangle: mkVert ii jj, mkVert (ii+1) jj, mkVert ii (jj+1) rcases hda with ha' | ha' | ha' <;> rcases hdb with hb' | hb' | hb' <;> (simp only [Set.mem_Icc]; rw [ha', hb']; fin_cases idx <;> - simp [mkVert, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons] <;> omega) + simp [mkVert, Matrix.cons_val_zero, Matrix.cons_val_one] <;> omega) · -- Down triangle: mkVert (ii+1) jj, mkVert ii (jj+1), mkVert (ii+1) (jj+1) rcases hda with ha' | ha' | ha' <;> rcases hdb with hb' | hb' | hb' <;> (simp only [Set.mem_Icc]; rw [ha', hb']; fin_cases idx <;> - simp [mkVert, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons] <;> omega) + simp [mkVert, Matrix.cons_val_zero, Matrix.cons_val_one] <;> omega) · simp at hcond /-! ### Boundary parity for Sperner coloring @@ -413,7 +413,7 @@ private lemma transitions_parity_nat : ∀ (m : ℕ) (f : Fin (m + 1) → Bool), have hlast_cs : f (Fin.last m).castSucc = f ⟨m, by omega⟩ := congrArg f (by simp [Fin.last, Fin.castSucc]) have hlast_succ : f (Fin.last m).succ = f ⟨m + 1, by omega⟩ := - congrArg f (by simp [Fin.last, Fin.val_succ]) + congrArg f (by simp [Fin.last]) rw [hlast_cs, hlast_succ] rcases Bool.eq_false_or_eq_true (f 0) with h0 | h0 <;> rcases Bool.eq_false_or_eq_true (f (⟨m, by omega⟩ : Fin (m + 2))) with hm | hm <;> @@ -433,14 +433,14 @@ private lemma odd_transitions (n : ℕ) (s : Fin (n + 1) → Bool) @[nolint unusedArguments] private theorem subdivSperner_odd_sum - (f : (Fin 3 → ℝ) → (Fin 3 → ℝ)) (hfS : ∀ x ∈ stdSimplex2, f x ∈ stdSimplex2) - (hne : ∀ x ∈ stdSimplex2, f x ≠ x) - (k : ℕ) (hk : 0 < k) + (f : (Fin 3 → ℝ) → (Fin 3 → ℝ)) (_hfS : ∀ x ∈ stdSimplex2, f x ∈ stdSimplex2) + (_hne : ∀ x ∈ stdSimplex2, f x ≠ x) + (k : ℕ) (_hk : 0 < k) (m : ℕ) (T : Triangulation m) (decode : Fin m → SubdivVert k) - (hadj : ∀ t ∈ T.triangles, ∀ a ∈ t, ∀ b ∈ t, + (_hadj : ∀ t ∈ T.triangles, ∀ a ∈ t, ∀ b ∈ t, ∀ i, ((decode a).1 i : ℤ) - ((decode b).1 i : ℤ) ∈ Set.Icc (-1 : ℤ) 1) (col : Fin m → Fin 3) - (hcol_boundary : ∀ v j, (decode v).1 j = 0 → col v ≠ j) + (_hcol_boundary : ∀ v j, (decode v).1 j = 0 → col v ≠ j) (h_odd_sum_hyp : Odd (∑ t ∈ T.triangles, (t.filter (fun v => col v = 1)).card * (t.filter (fun v => col v = 2)).card)) : ∃ count12 : Finset (Fin m) → ℕ, @@ -528,7 +528,7 @@ private theorem rainbow_triangle_gives_vertices (hne : ∀ x ∈ stdSimplex2, f x ≠ x) (k : ℕ) (hk : 0 < k) (m : ℕ) (T : Triangulation m) (decode : Fin m → SubdivVert k) (col : Fin m → Fin 3) (t : Finset (Fin m)) (ht : t ∈ T.triangles) - (hcard : t.card = 3) (hrainbow : isRainbow col t) + (_hcard : t.card = 3) (hrainbow : isRainbow col t) (hcol_def : ∀ v, col v = spernerColor f (subdivCoord k hk (decode v))) (hadj : ∀ t ∈ T.triangles, ∀ a ∈ t, ∀ b ∈ t, ∀ i, ((decode a).1 i : ℤ) - ((decode b).1 i : ℤ) ∈ Set.Icc (-1 : ℤ) 1) : @@ -555,21 +555,20 @@ private theorem rainbow_triangle_gives_vertices · -- f (v i) i < (v i) i intro i have hcol_i : col (vert i) = i := by - fin_cases i <;> simp only [vert, Matrix.cons_val_zero, Matrix.cons_val_one, - Matrix.head_cons] <;> assumption + fin_cases i <;> simp [vert] <;> assumption rw [hcol_def] at hcol_i unfold spernerColor at hcol_i split_ifs at hcol_i with hex · have := hex.choose_spec; rw [hcol_i] at this; exact this · -- ¬∃ j, f v j < v j means f(v) ≥ v componentwise, and ∑ = 1 forces f(v) = v. -- But hne says f(v) ≠ v, contradiction. - push_neg at hex + push Not at hex have hv_mem := subdivCoord_mem k hk (decode (vert i)) have hfv_mem := hfS _ hv_mem have heq : f (subdivCoord k hk (decode (vert i))) = subdivCoord k hk (decode (vert i)) := by ext j exact le_antisymm (by - by_contra hlt; push_neg at hlt + by_contra hlt; push Not at hlt have : ∑ l, f (subdivCoord k hk (decode (vert i))) l > ∑ l, subdivCoord k hk (decode (vert i)) l := Finset.sum_lt_sum (fun l _ => hex l) @@ -585,11 +584,9 @@ private theorem rainbow_triangle_gives_vertices apply subdivCoord_dist intro idx have hvi : vert i ∈ t := by - fin_cases i <;> simp [vert, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons] <;> - assumption + fin_cases i <;> simp [vert] <;> assumption have hvj : vert j ∈ t := by - fin_cases j <;> simp [vert, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons] <;> - assumption + fin_cases j <;> simp [vert] <;> assumption exact hadj t ht (vert i) hvi (vert j) hvj idx /-- **Geometric Sperner:** For each k ≥ 1, the Sperner coloring of the k-th regular @@ -736,7 +733,7 @@ private theorem brouwer_fixed_point_simplex2_sperner ∃ x ∈ stdSimplex2, f x = x := by -- Use contradiction: assume no fixed point, then spernerColor is always well-defined by_contra hno - push_neg at hno + push Not at hno have hne : ∀ x ∈ stdSimplex2, f x ≠ x := by intro x hx heq; exact hno x hx heq -- For each k ≥ 1, get rainbow triangle vertices @@ -752,7 +749,7 @@ private theorem brouwer_fixed_point_simplex2_sperner suffices hle : ∀ i, f xstar i ≤ xstar i by have heq : f xstar = xstar := by ext i; exact le_antisymm (hle i) (by - by_contra hlt; push_neg at hlt + by_contra hlt; push Not at hlt have : ∑ j, f xstar j < ∑ j, xstar j := Finset.sum_lt_sum (fun j _ => hle j) ⟨i, Finset.mem_univ _, hlt⟩ linarith [hfxstar_mem.2, hxstar_mem.2]) diff --git a/FormalBook/Ch30/EKRAuxiliary.lean b/FormalBook/Ch30/EKRAuxiliary.lean index 708e5de..038c52c 100644 --- a/FormalBook/Ch30/EKRAuxiliary.lean +++ b/FormalBook/Ch30/EKRAuxiliary.lean @@ -98,7 +98,7 @@ lemma arc_lemma {n k : ℕ} (h2k : 2 * k ≤ n) (S : Finset (Fin n)) · obtain ⟨i₀, hi₀⟩ := hne; exact absurd (hS i₀ hi₀ i₀ hi₀) (by simp [circularArc]) have hkn : k ≤ n := by omega obtain ⟨i₀, hi₀⟩ := hne - haveI : NeZero n := ⟨by omega⟩ + have : NeZero n := ⟨by omega⟩ let f : Fin n → ℕ := fun s => let d := (s - i₀).val if d < k then d else d - (n - k) diff --git a/FormalBook/Chapter_09.lean b/FormalBook/Chapter_09.lean index b39771c..bfc9540 100644 --- a/FormalBook/Chapter_09.lean +++ b/FormalBook/Chapter_09.lean @@ -5,10 +5,11 @@ Authors: Moritz Firsching, Julien Michel -/ import FormalBook.Mathlib.Analysis.SpecialFunctions.Integrals.Basic import FormalBook.Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan +import Mathlib.Analysis.Real.Sqrt import Mathlib.Analysis.SpecialFunctions.PolarCoord -import Mathlib.Data.Real.StarOrdered import Mathlib.MeasureTheory.Function.SpecialFunctions.Arctan import Mathlib.RingTheory.Finiteness.Prod +import Mathlib.Tactic.ContinuousFunctionalCalculus import Mathlib.Tactic.NormNum.RealSqrt /-! @@ -83,22 +84,22 @@ theorem euler_series : ∑' n : ℕ, ((n : ℝ) ^ 2)⁻¹ = π ^ 2 / 6 := by · ring_nf convert_to ∑' n : ℕ, ∫⁻ x : ℝ, (Ioo 0 1).indicator 1 x * ofReal x ^ n * ∫⁻ y : ℝ, (Ioo 0 1).indicator 1 y * ofReal y ^ n = _ using 3 with n - . rw [lintegral_mul_const _ (by clear * -; measurability)] + . rw [lintegral_mul_const _ (by measurability)] convert_to ∑' n : ℕ, ∫⁻ x : ℝ, ∫⁻ y : ℝ, (Ioo 0 1).indicator 1 x * (Ioo 0 1).indicator 1 y * (ofReal x * ofReal y) ^ n = _ using 5 with n x - . rw [←lintegral_const_mul _ (by clear * -; measurability)] + . rw [←lintegral_const_mul _ (by measurability)] ring_nf -- Now we exchange the sum and the integrals using Tonelli's theorem twice. -- Using ℝ≥0∞ integrals saves us from checking integrability conditions. convert_to ∫⁻ x : ℝ, ∑' n : ℕ, ∫⁻ y : ℝ, (Ioo 0 1).indicator 1 x * (Ioo 0 1).indicator 1 y * (ofReal x * ofReal y) ^ n = _ using 1 - . rw [lintegral_tsum (by clear * -; measurability)] + . rw [lintegral_tsum (by measurability)] convert_to ∫⁻ x : ℝ, ∫⁻ y : ℝ, ∑' n : ℕ, (Ioo 0 1).indicator 1 x * (Ioo 0 1).indicator 1 y * (ofReal x * ofReal y) ^ n = _ using 3 with x - . rw [lintegral_tsum (by clear * -; measurability)] + . rw [lintegral_tsum (by measurability)] convert_to ∫⁻ x : ℝ, ∫⁻ y : ℝ, (Ioo 0 1).indicator 1 x * (Ioo 0 1).indicator 1 y * ((1 - ofReal x * ofReal y)⁻¹) = _ using 5 with x y · rw [ENNReal.tsum_mul_left, tsum_geometric] @@ -131,7 +132,7 @@ theorem euler_series : ∑' n : ℕ, ((n : ℝ) ^ 2)⁻¹ = π ^ 2 / 6 := by · intro a; ext <;> linarith only have fS_eq_T : f '' S = T := by ext xy - simp only [mem_setOf_eq, mem_image, T, f, S] + simp only [mem_ofPred_eq, mem_image, T, f, S] constructor · intro ⟨uv, h1, h2⟩ set u := uv.1 @@ -309,7 +310,7 @@ theorem euler_series : ∑' n : ℕ, ((n : ℝ) ^ 2)⁻¹ = π ^ 2 / 6 := by · congr! 2 with u rw [←lintegral_const_mul] · ring_nf - · clear *-; measurability + · measurability convert_to (2 * ∫⁻ u : ℝ in Ioo 0 2⁻¹, ∫⁻ v : ℝ in Ioo (-u) u, ofReal ((1 - (u - v) * (u + v))⁻¹)) + diff --git a/FormalBook/Chapter_20.lean b/FormalBook/Chapter_20.lean index f9845a5..ea2a056 100644 --- a/FormalBook/Chapter_20.lean +++ b/FormalBook/Chapter_20.lean @@ -170,11 +170,11 @@ theorem harmonic_geometric_arithmetic₁ (n : ℕ) (hn : 1 ≤ n) rwa [inv_inv, inv_div] at this -- Equality conditions via Mathlib's weighted AM-GM characterization have lhs_a : ∏ i ∈ S, a i ^ w i = geometric := - Real.finset_prod_rpow _ _ (fun i _ => le_of_lt (hpos i)) _ + Real.finsetProd_rpow _ _ (fun i _ => le_of_lt (hpos i)) _ have rhs_a : ∑ i ∈ S, w i * a i = arithmetic := by change ∑ i ∈ S, (1 : ℝ) / ↑n * a i = (∑ i : Finset.Icc 1 n, a i) / ↑n simp_rw [div_mul_eq_mul_div, one_mul]; simp [S, Finset.sum_div] - have eq_a := geom_mean_eq_arith_mean_weighted_iff' S w a hw_pos hw_sum ha_nn + have eq_a := geom_mean_eq_arith_mean_weighted_iff_of_pos' S w a hw_pos hw_sum ha_nn have gm_eq_am : (geometric = arithmetic) ↔ all_equal := by rw [← lhs_a, ← rhs_a, eq_a] constructor @@ -185,14 +185,14 @@ theorem harmonic_geometric_arithmetic₁ (n : ℕ) (hn : 1 ≤ n) simp [Finset.sum_const, nsmul_eq_mul, hS_card, hn_ne] have hb_nn : ∀ i ∈ S, (0 : ℝ) ≤ b i := fun i _ => le_of_lt (hb_pos i) have lhs_b : ∏ i ∈ S, b i ^ w i = geometric⁻¹ := by - rw [Real.finset_prod_rpow _ _ (fun i _ => le_of_lt (hb_pos i)) _] + rw [Real.finsetProd_rpow _ _ (fun i _ => le_of_lt (hb_pos i)) _] have : ∏ i ∈ S, b i = (∏ i ∈ S, a i)⁻¹ := by simp only [b]; exact Finset.prod_inv_distrib a rw [this, Real.inv_rpow (le_of_lt prod_a_pos)] have rhs_b : ∑ i ∈ S, w i * b i = (∑ i : Finset.Icc 1 n, 1 / a i) / ↑n := by change ∑ i ∈ S, (1 : ℝ) / ↑n * (a i)⁻¹ = (∑ i : Finset.Icc 1 n, 1 / a i) / ↑n simp_rw [div_mul_eq_mul_div, one_mul, one_div]; simp [S, Finset.sum_div] - have eq_b := geom_mean_eq_arith_mean_weighted_iff' S w b hw_pos hw_sum hb_nn + have eq_b := geom_mean_eq_arith_mean_weighted_iff_of_pos' S w b hw_pos hw_sum hb_nn have hm_eq_gm : (harmonic = geometric) ↔ all_equal := by constructor · intro heq @@ -252,7 +252,7 @@ theorem harmonic_geometric_arithmetic₂ (n : ℕ) (hn : 1 ≤ n) have prod_a_pos : 0 < ∏ i ∈ S, a i := Finset.prod_pos (fun i _ => hpos i) -- Rewriting lemmas have lhs_a : ∏ i ∈ S, a i ^ w i = geometric := - Real.finset_prod_rpow _ _ (fun i _ => le_of_lt (hpos i)) _ + Real.finsetProd_rpow _ _ (fun i _ => le_of_lt (hpos i)) _ have rhs_a : ∑ i ∈ S, w i * a i = arithmetic := by change ∑ i ∈ S, (1 : ℝ) / ↑n * a i = (∑ i : Finset.Icc 1 n, a i) / ↑n simp_rw [div_mul_eq_mul_div, one_mul]; simp [S, Finset.sum_div] @@ -299,7 +299,7 @@ theorem harmonic_geometric_arithmetic₂ (n : ℕ) (hn : 1 ≤ n) -- Part B: GM = AM ↔ all_equal have gm_eq_am : (geometric = arithmetic) ↔ all_equal := by rw [← lhs_a, ← rhs_a, - geom_mean_eq_arith_mean_weighted_iff' S w a hw_pos hw_sum ha_nn] + geom_mean_eq_arith_mean_weighted_iff_of_pos' S w a hw_pos hw_sum ha_nn] constructor · intro h i; linarith [h i₁ (Finset.mem_univ _), h i (Finset.mem_univ _)] · intro h j _ @@ -312,7 +312,7 @@ theorem harmonic_geometric_arithmetic₂ (n : ℕ) (hn : 1 ≤ n) have hb_pos : ∀ i, 0 < b i := fun i => inv_pos.mpr (hpos i) have hb_nn : ∀ i ∈ S, (0 : ℝ) ≤ b i := fun i _ => le_of_lt (hb_pos i) have lhs_b : ∏ i ∈ S, b i ^ w i = geometric⁻¹ := by - rw [Real.finset_prod_rpow _ _ (fun i _ => le_of_lt (hb_pos i)) _] + rw [Real.finsetProd_rpow _ _ (fun i _ => le_of_lt (hb_pos i)) _] have : ∏ i ∈ S, b i = (∏ i ∈ S, a i)⁻¹ := by simp only [b]; exact Finset.prod_inv_distrib a rw [this, Real.inv_rpow (le_of_lt prod_a_pos)] @@ -380,7 +380,7 @@ theorem harmonic_geometric_arithmetic₂ (n : ℕ) (hn : 1 ≤ n) inv_anti₀ (by positivity) inv_gm_le rwa [inv_inv, inv_div] at this -- Part D: HM = GM ↔ all_equal - have eq_b := geom_mean_eq_arith_mean_weighted_iff' S w b hw_pos hw_sum hb_nn + have eq_b := geom_mean_eq_arith_mean_weighted_iff_of_pos' S w b hw_pos hw_sum hb_nn have hm_eq_gm : (harmonic = geometric) ↔ all_equal := by constructor · intro heq @@ -442,12 +442,12 @@ theorem harmonic_geometric_arithmetic₃ (n : ℕ) (hn : 1 ≤ n) have hb_nn : ∀ i ∈ S, (0 : ℝ) ≤ b i := fun i _ => le_of_lt (hb_pos i) -- Key rewriting lemmas have lhs_a : ∏ i ∈ S, a i ^ w i = geometric := - Real.finset_prod_rpow _ _ (fun i _ => le_of_lt (hpos i)) _ + Real.finsetProd_rpow _ _ (fun i _ => le_of_lt (hpos i)) _ have rhs_a : ∑ i ∈ S, w i * a i = arithmetic := by change ∑ i ∈ S, (1 : ℝ) / ↑n * a i = (∑ i : Finset.Icc 1 n, a i) / ↑n simp_rw [div_mul_eq_mul_div, one_mul]; simp [S, Finset.sum_div] have lhs_b : ∏ i ∈ S, b i ^ w i = geometric⁻¹ := by - rw [Real.finset_prod_rpow _ _ (fun i _ => le_of_lt (hb_pos i)) _] + rw [Real.finsetProd_rpow _ _ (fun i _ => le_of_lt (hb_pos i)) _] have : ∏ i ∈ S, b i = (∏ i ∈ S, a i)⁻¹ := by simp only [b]; exact Finset.prod_inv_distrib a rw [this, Real.inv_rpow (le_of_lt prod_a_pos)] @@ -494,7 +494,7 @@ theorem harmonic_geometric_arithmetic₃ (n : ℕ) (hn : 1 ≤ n) rwa [inv_inv, inv_div] at this case gm_eq => rw [← lhs_a, ← rhs_a, - geom_mean_eq_arith_mean_weighted_iff' S w a hw_pos hw_sum ha_nn] + geom_mean_eq_arith_mean_weighted_iff_of_pos' S w a hw_pos hw_sum ha_nn] constructor · intro h i; linarith [h i₁ (Finset.mem_univ _), h i (Finset.mem_univ _)] · intro h j _ @@ -502,7 +502,7 @@ theorem harmonic_geometric_arithmetic₃ (n : ℕ) (hn : 1 ≤ n) simp_rw [hall]; rw [← Finset.mul_sum] simp [Finset.sum_const, nsmul_eq_mul, hS_card, hn_ne] case hm_eq => - have eq_b := geom_mean_eq_arith_mean_weighted_iff' S w b hw_pos hw_sum hb_nn + have eq_b := geom_mean_eq_arith_mean_weighted_iff_of_pos' S w b hw_pos hw_sum hb_nn have sum_inv_pos : 0 < ∑ i : Finset.Icc 1 n, 1 / a i := Finset.sum_pos (fun i _ => div_pos one_pos (hpos i)) ⟨i₁, Finset.mem_univ _⟩ constructor @@ -630,7 +630,7 @@ theorem mantel_eq_adj_degree (h : G.CliqueFree 3) (heq : #E * 4 = n ^ 2) intro e he induction e with | _ v w => simp at he - by_contra hc; push_neg at hc + by_contra hc; push Not at hc obtain ⟨k, hk⟩ := Finset.inter_nonempty_of_card_lt_card_add_card (by simp) (by simp) hc simp at hk; obtain ⟨hvk, hwk⟩ := hk @@ -668,7 +668,7 @@ theorem mantel_eq_adj_degree (h : G.CliqueFree 3) (heq : #E * 4 = n ^ 2) -- Cauchy–Schwarz, contradicting the edge-count hypothesis. have hforall : ∀ e ∈ E, sum_deg e = n := by by_contra hc - push_neg at hc + push Not at hc obtain ⟨e₀, he₀, hne⟩ := hc have hlt : sum_deg e₀ < n := lt_of_le_of_ne (adj_degree_bnd' e₀ he₀) hne have h1 : ∑ e ∈ E, sum_deg e < ∑ _ ∈ E, n := @@ -805,7 +805,7 @@ private lemma degree_le_indepNum (h : G.CliqueFree 3) (v : α) : G.isIndepSet_neighborSet_of_triangleFree h v have hind' : G.IsIndepSet (G.neighborFinset v : Set α) := by intro x hx y hy hne - simp [SimpleGraph.mem_neighborFinset] at hx hy + simp only [Finset.mem_coe, SimpleGraph.mem_neighborFinset] at hx hy exact hind hx hy hne exact hind'.card_le_indepNum diff --git a/FormalBook/Chapter_28.lean b/FormalBook/Chapter_28.lean index 11a8c7d..e222882 100644 --- a/FormalBook/Chapter_28.lean +++ b/FormalBook/Chapter_28.lean @@ -378,7 +378,7 @@ theorem c4_free_edge_bound -- If 4e ≤ n, done since n * √(4n-3) ≥ 0 by_cases h4e_le : 4 * (e : ℝ) ≤ (n : ℝ) · linarith [mul_nonneg (Nat.cast_nonneg n) (Real.sqrt_nonneg (4 * (n : ℝ) - 3))] - push_neg at h4e_le + push Not at h4e_le -- Otherwise 4e > n, so 4e - n > 0. We square both sides. rw [show 4 * (e : ℝ) ≤ (n : ℝ) + (n : ℝ) * Real.sqrt (4 * (n : ℝ) - 3) ↔ 4 * (e : ℝ) - (n : ℝ) ≤ (n : ℝ) * Real.sqrt (4 * (n : ℝ) - 3) by constructor <;> intro h <;> linarith] @@ -434,7 +434,7 @@ theorem sum_divisor_count (n : ℕ) : exact ⟨Nat.lt_succ_of_le (Nat.le_of_dvd (by omega) hdj), hdj⟩ · rintro ⟨hd_lt, hdj⟩ refine ⟨⟨?_, ?_⟩, hdj⟩ - · by_contra h; push_neg at h; interval_cases d; simp at hdj; exact hj0 hdj + · by_contra h; push Not at h; interval_cases d; simp at hdj; exact hj0 hdj · exact le_trans (Nat.le_of_dvd (by omega) hdj) hj.2 · intro i hi have hioc : Finset.Ioc 0 n = Finset.Icc 1 n := by @@ -721,15 +721,15 @@ lemma orthogonal_set_card [Fintype (PG2 p)] have hφ_apply : ∀ w, φ w = u ⬝ᵥ w := fun _ => rfl have hφ : φ ≠ 0 := by intro h; exact hu ((dotProductEquiv (ZMod p) (Fin 3)).map_eq_zero_iff.mp h) - haveI : FiniteDimensional (ZMod p) (Fin 3 → ZMod p) := inferInstance + have : FiniteDimensional (ZMod p) (Fin 3 → ZMod p) := inferInstance have hfr : Module.finrank (ZMod p) (LinearMap.ker φ) = 2 := by have h1 := Module.Dual.finrank_ker_add_one_of_ne_zero hφ; simp at h1; omega - haveI : Finite (ZMod p) := inferInstance + have : Finite (ZMod p) := inferInstance have hcard : Nat.card (ℙ (ZMod p) (LinearMap.ker φ)) = p + 1 := by rw [Projectivization.card_of_finrank_two _ _ hfr, Nat.card_zmod] have hι_inj : Function.Injective (Projectivization.map (LinearMap.ker φ).subtype (Submodule.injective_subtype _)) := Projectivization.map_injective _ _ - haveI : Fintype (ℙ (ZMod p) (LinearMap.ker φ)) := Fintype.ofFinite _ + have : Fintype (ℙ (ZMod p) (LinearMap.ker φ)) := Fintype.ofFinite _ rw [show p + 1 = Finset.card (Finset.univ : Finset (ℙ (ZMod p) (LinearMap.ker φ))) from by rw [Finset.card_univ, Fintype.card_eq_nat_card]; exact hcard.symm] symm diff --git a/FormalBook/Chapter_43.lean b/FormalBook/Chapter_43.lean index a94289a..b647601 100644 --- a/FormalBook/Chapter_43.lean +++ b/FormalBook/Chapter_43.lean @@ -4,7 +4,7 @@ Authors: Matteo Del Vecchio, Aristotle (Harmonic) import Mathlib.Algebra.Order.Ring.Star import Mathlib.Analysis.InnerProductSpace.PiL2 -import Mathlib.Combinatorics.SimpleGraph.Coloring +import Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex import Mathlib.Data.Int.Star import Mathlib.GroupTheory.GroupAction.SubMulAction.Combination import Mathlib.LinearAlgebra.Vandermonde @@ -129,7 +129,7 @@ lemma lusternik_schnirelmann {d : ℕ} sub_zero, Set.mem_inter_iff, and_true]; · have := closure_inter_sphere_disjoint_neg_of_open_inter_sphere ( U k ) ‹_› (Metric.sphere 0 1 ) ( by aesop ) ; simp_all +decide only [Set.mem_inter_iff, - mem_sphere_iff_norm, sub_zero, norm_neg, Set.disjoint_left, Set.mem_setOf_eq, + mem_sphere_iff_norm, sub_zero, norm_neg, Set.disjoint_left, Set.mem_ofPred_eq, and_true, and_imp, not_and] ; contrapose! this simp_all only [not_false_eq_true, implies_true, true_and] @@ -147,7 +147,7 @@ lemma lusternik_schnirelmann {d : ℕ} } · simp_all only · apply h_neg_x_closure - simp_all only [Set.mem_setOf_eq, Set.inter_subset_left, and_self] + simp_all only [Set.mem_ofPred_eq, Set.inter_subset_left, and_self] /-- A Kneser graph for natural numbers `n`, `k` is a graph with vertices being `k`-subsets of @@ -181,7 +181,7 @@ lemma KneserGraph_chromaticNumber_le (n k d : ℕ) (hk : 1 ≤ k) (h : n = 2 * k by_cases hA : ∃ x ∈ A, (x : ℕ) < d + 1 <;> by_cases hB : ∃ x ∈ B, (x : ℕ) < d + 1 · dsimp [color] - rw [dif_pos hA, dif_pos hB] + rw [dite_eq_left hA, dite_eq_left hB] intro (h_eq : (⟨hA.choose.val, _⟩ : Fin (d + 2)) = ⟨hB.choose.val, _⟩) have h_val : hA.choose.val = hB.choose.val := congr_arg (fun (x : Fin (d + 2)) => x.val) h_eq have h_fin_eq : hA.choose = hB.choose := Fin.ext h_val @@ -189,13 +189,13 @@ lemma KneserGraph_chromaticNumber_le (n k d : ℕ) (hk : 1 ≤ k) (h : n = 2 * k have hB_in : hA.choose ∈ B := by rw [h_fin_eq]; exact hB.choose_spec.1 exact (Finset.disjoint_left.mp hAB) hA_in hB_in · dsimp [color] - rw [dif_pos hA, dif_neg hB] + rw [dite_eq_left hA, dite_eq_right hB] intro (h_eq : (⟨hA.choose.val, _⟩ : Fin (d + 2)) = ⟨d + 1, _⟩) have h_val : hA.choose.val = d + 1 := congr_arg (fun (x : Fin (d + 2)) => x.val) h_eq have h_lt : hA.choose.val < d + 1 := hA.choose_spec.2 omega · dsimp [color] - rw [dif_neg hA, dif_pos hB] + rw [dite_eq_right hA, dite_eq_left hB] intro (h_eq : (⟨d + 1, _⟩ : Fin (d + 2)) = ⟨hB.choose.val, _⟩) have h_val : d + 1 = hB.choose.val := congr_arg (fun (x : Fin (d + 2)) => x.val) h_eq have h_lt : hB.choose.val < d + 1 := hB.choose_spec.2 @@ -298,7 +298,7 @@ lemma is_open_open_set_for_subsets {d : ℕ} (V : Set (Finset (EuclideanSpace exact Finset ( EuclideanSpace ℝ ( Fin d ) ); exact V exact fun A => { x : EuclideanSpace ℝ ( Fin d ) | ∀ y ∈ A, 0 < inner ℝ x y }; - · simp +decide only [Set.setOf_forall]; + · simp +decide only [Set.ofPred_forall]; exact isOpen_biInter_finset fun x hx => isOpen_lt continuous_const <| continuous_id.inner continuous_const; · exact Set.ext fun x => diff --git a/FormalBook/Chapter_45.lean b/FormalBook/Chapter_45.lean index 89a96c1..0ed61ab 100644 --- a/FormalBook/Chapter_45.lean +++ b/FormalBook/Chapter_45.lean @@ -51,7 +51,7 @@ theorem remark_1 {d : ℕ} : ∃ α : Type, ∃ X : Finset α, ∃ 𝓕 : Finset use (Finset.powerset univ).filter (Finset.card · = d) simp only [univ_eq_attach, mem_filter, mem_powerset, and_imp, imp_self, implies_true, true_and] unfold two_colorable - push_neg + push Not intro coloring by_cases h : d ≤ (Finset.univ.filter (coloring · = 1)).card · refine (Finset.exists_subset_card_eq h).imp ?_ @@ -110,7 +110,7 @@ theorem MeasureTheory.measure_biUnion_lt_sum_of_inter {β : Type _} grind only [= Set.subset_def, = mem_erase, cases eager Subtype] · dsimp [t'] simp only [↓reduceIte, coe_sdiff] - rw [← @MeasureTheory.measure_diff_add_inter _ _ P (t j) (t i) + rw [← @MeasureTheory.measure_sdiff_add_inter _ _ P (t j) (t i) (Set.Finite.measurableSet <| finite_toSet (t j))] apply ENNReal.lt_add_right (by apply measure_ne_top) h @@ -184,8 +184,8 @@ theorem theorem_1 {h_d : d ≥ 2} (𝓕 : Finset (Finset X)) simp only [mem_compl, dite_not, Subtype.forall] at H funext x specialize H x.val (by simp only [coe_mem]) - rw [dif_neg (by simp only [Subtype.coe_eta] ; exact (mem_compl.mp x.property)), - dif_neg (by simp only [Subtype.coe_eta] ; exact (mem_compl.mp x.property))] at H + rw [dite_eq_right (by simp only [Subtype.coe_eta] ; exact (mem_compl.mp x.property)), + dite_eq_right (by simp only [Subtype.coe_eta] ; exact (mem_compl.mp x.property))] at H convert H · intro k kdef use (fun x => k x.val) diff --git a/FormalBook/Mathlib/EdgeFinset.lean b/FormalBook/Mathlib/EdgeFinset.lean index c8dd4dd..753203a 100644 --- a/FormalBook/Mathlib/EdgeFinset.lean +++ b/FormalBook/Mathlib/EdgeFinset.lean @@ -24,7 +24,7 @@ theorem isDiag_iff_exists {z : Sym2 α} : z.IsDiag ↔ ∃ x, z = s(x, x) := by theorem not_isDiag_iff_exists {z : Sym2 α} : ¬ z.IsDiag ↔ ∃ x y, x ≠ y ∧ z = s(x, y) := by induction z with | _ x y => rw [mk_isDiag_iff, not_iff_comm] - push_neg + push Not constructor · intro h; simpa using h x y · aesop From 32766ccf85af5dfdcb70c50743b1709769472560 Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Tue, 25 Aug 2026 13:51:45 +0200 Subject: [PATCH 3/3] fix rest of warnings --- FormalBook/Chapter_01.lean | 26 +++++++++++++------------- FormalBook/Chapter_04.lean | 8 ++++---- FormalBook/Chapter_06.lean | 18 ++++++++---------- FormalBook/Chapter_11.lean | 6 +++--- FormalBook/Chapter_21.lean | 2 +- FormalBook/Chapter_35.lean | 12 ++++++------ 6 files changed, 35 insertions(+), 37 deletions(-) diff --git a/FormalBook/Chapter_01.lean b/FormalBook/Chapter_01.lean index 4cd7f19..63baedb 100644 --- a/FormalBook/Chapter_01.lean +++ b/FormalBook/Chapter_01.lean @@ -197,7 +197,7 @@ noncomputable def invRealHom : ℕ →*₀ ℝ := lemma S1_eq_smoothNumbers (x : ℝ) : S₁ x = Nat.smoothNumbers (⌊x⌋₊ + 1) := by ext n - simp only [S₁, Nat.smoothNumbers, Set.mem_setOf_eq] + simp only [S₁, Nat.smoothNumbers, Set.mem_ofPred_eq] constructor · intro hn have hn0 : n ≠ 0 := by @@ -367,7 +367,7 @@ theorem euler_product_rearrangement (x: ℝ) (n: ℕ) (hxge : x ≥ n) (hxlt : x intro he0; subst he0; exact he (Finset.mem_singleton_self 0) have pnin : (p : ℕ)^e ∉ S₁ x := by intro h - simp only [S₁, Set.mem_setOf_eq] at h + simp only [S₁, Set.mem_ofPred_eq] at h have h_dvd : (p : ℕ) ∣ (p : ℕ)^e := dvd_pow_self _ enz have hle : (p : ℝ) ≤ x := h (p : ℕ) pprime h_dvd have : (p : ℕ) ≤ ⌊x⌋ := Int.le_floor.mpr hle @@ -465,7 +465,7 @@ theorem sum_le_infinite_sum (x: ℝ) (n: ℕ) (hxge : x ≥ n) (hxlt : x < n + 1 . have: i ∈ Set.Icc 1 n ∨ i ∉ Set.Icc 1 n := by exact Decidable.em (i ∈ Set.Icc 1 n) rcases this with (case | case) - . simp [case] + . simp have: i ∈ S₁ x := by { unfold S₁ have i_lt_n: i ≤ n := by simp_all only [ge_iff_le, Set.mem_Icc] @@ -478,18 +478,18 @@ theorem sum_le_infinite_sum (x: ℝ) (n: ℕ) (hxge : x ≥ n) (hxlt : x < n + 1 bound } - rewrite [Set.mem_setOf] + rewrite [Set.mem_ofPred] assumption } - simp_all only [ge_iff_le, Set.mem_Icc, Set.indicator_of_mem, le_refl] + simp_all only [ge_iff_le, Set.mem_Icc] sorry - . simp [case] + . simp clear case have: i ∈ (S₁ x) ∨ i ∉ S₁ x := by exact Decidable.em (i ∈ S₁ x) rcases this with (case | case) - . simp_all only [ge_iff_le, Set.indicator_of_mem, inv_nonneg, cast_nonneg] + . simp_all only [ge_iff_le] sorry - . simp_all only [ge_iff_le, not_false_eq_true, Set.indicator_of_notMem, le_refl] + . simp_all only [ge_iff_le] sorry } @@ -534,7 +534,7 @@ theorem geom_series_simp (n : ℕ) (x : ℝ) (hxge : x ≥ n) (hxlt : x < n + 1) clear this apply Finset.prod_image intros i hi j hj hij - have := Nat.nth_injective (Nat.infinite_setOf_prime) hij + have := Nat.nth_injective (Nat.infinite_setOfPred_prime) hij assumption } rewrite [this] @@ -588,7 +588,7 @@ lemma prime_counting_lemma (x : ℝ) : have h_term_le : ∀ k ∈ Finset.Icc 1 (primeCountingReal x), ((Nat.nth Nat.Prime k : ℝ) / ((Nat.nth Nat.Prime k) - 1)) ≤ ((k + 1) : ℝ) / (k : ℝ) := by intro k hk; rw [ div_le_div_iff₀ ] <;> norm_num; · norm_cast; - rw [ Int.subNatNat_eq_coe ] ; push_cast ; nlinarith [ Nat.Prime.one_lt ( Nat.prime_nth_prime k ), show Nat.nth Nat.Prime k ≥ k + 1 from Nat.recOn k ( Nat.Prime.pos ( Nat.prime_nth_prime 0 ) ) fun n ihn => Nat.succ_le_of_lt ( Nat.lt_of_le_of_lt ihn ( Nat.nth_strictMono ( Nat.infinite_setOf_prime ) ( Nat.lt_succ_self _ ) ) ) ]; + rw [ Int.subNatNat_eq_coe ] ; push_cast ; nlinarith [ Nat.Prime.one_lt ( Nat.prime_nth_prime k ), show Nat.nth Nat.Prime k ≥ k + 1 from Nat.recOn k ( Nat.Prime.pos ( Nat.prime_nth_prime 0 ) ) fun n ihn => Nat.succ_le_of_lt ( Nat.lt_of_le_of_lt ihn ( Nat.nth_strictMono ( Nat.infinite_setOfPred_prime ) ( Nat.lt_succ_self _ ) ) ) ]; · exact Nat.Prime.one_lt ( Nat.prime_nth_prime k ); · linarith [ Finset.mem_Icc.mp hk ]; exact Finset.prod_le_prod ( fun _ _ => div_nonneg ( Nat.cast_nonneg _ ) ( sub_nonneg.mpr ( Nat.one_le_cast.mpr ( Nat.Prime.pos ( Nat.prime_nth_prime _ ) ) ) ) ) h_term_le @@ -685,7 +685,7 @@ theorem infinity_of_primes₅ : { p : ℕ | p.Prime }.Infinite := by obtain ⟨b₂, hb₂, hNab₂⟩ := hO₂ a haO₂ refine ⟨b₁*b₂, mul_pos hb₁ hb₂, Set.subset_inter (subset_trans ?_ hNab₁) (subset_trans ?_ hNab₂)⟩ - <;> simp only [N, Set.setOf_subset_setOf, forall_exists_index, forall_apply_eq_imp_iff, + <;> simp only [N, Set.ofPred_subset_ofPred, forall_exists_index, forall_apply_eq_imp_iff, add_right_inj] · refine fun k ↦ ⟨b₂*k, by ring⟩ · refine fun k ↦ ⟨b₁*k, by ring⟩ @@ -706,7 +706,7 @@ theorem infinity_of_primes₅ : { p : ℕ | p.Prime }.Infinite := by have IsClosed_N (a b : ℤ) (hb : 0 < b) : IsClosed (N a b):= by refine isOpen_compl_iff.1 (Or.inr fun n hn ↦ ⟨b, hb, fun k hk ↦ ?_⟩) - simp only [N, Set.mem_compl_iff, Set.mem_setOf_eq, not_exists] at * + simp only [N, Set.mem_compl_iff, Set.mem_ofPred_eq, not_exists] at * intro b₁ hb₁ obtain ⟨m, hm⟩ := hk apply hn (b₁ - m) @@ -726,7 +726,7 @@ theorem infinity_of_primes₅ : { p : ℕ | p.Prime }.Infinite := by rw [Int.ofNat_dvd_left] exact (Nat.minFac_dvd (Int.natAbs n)) ext n - simp only [Set.mem_setOf_eq, N, zero_add, Set.mem_iUnion, exists_prop, Int.reduceNeg, + simp only [Set.mem_ofPred_eq, N, zero_add, Set.mem_iUnion, exists_prop, Int.reduceNeg, Set.mem_compl_iff, Set.mem_insert_iff, Set.mem_singleton_iff, not_or] constructor · intro ⟨p, hp, ⟨k, hk⟩⟩ diff --git a/FormalBook/Chapter_04.lean b/FormalBook/Chapter_04.lean index 0524a58..3b0a678 100644 --- a/FormalBook/Chapter_04.lean +++ b/FormalBook/Chapter_04.lean @@ -136,7 +136,7 @@ variable (k : ℕ) /-- The linear involution `(x, y, z) ↦ (y, x, -z)`. -/ def linearInvo : Function.End (S k) := fun ⟨⟨x, y, z⟩, h⟩ => ⟨⟨y, x, -z⟩, by - simp only [S, Set.mem_setOf_eq] at h ⊢ + simp only [S, Set.mem_ofPred_eq] at h ⊢ exact ⟨by linarith [h], h.2.2, h.2.1⟩ ⟩ theorem linearInvo_sq : linearInvo k ^ 2 = (1 : Function.End (S k)) := by @@ -149,7 +149,7 @@ theorem linearInvo_sq : linearInvo k ^ 2 = (1 : Function.End (S k)) := by ext <;> simp theorem linearInvo_no_fixedPoints : IsEmpty (fixedPoints (linearInvo k)) := by - simp only [isEmpty_subtype, mem_fixedPoints, Subtype.forall, Prod.forall] + simp only [isEmpty_subtype, Subtype.forall, Prod.forall] intro x y z h hfixed have hfixed' : (linearInvo k ⟨⟨x, y, z⟩, h⟩).1.2.2 = z := by rw [hfixed] have : -z = z := hfixed' @@ -188,7 +188,7 @@ def secondInvo : Function.End (U k) := fun ⟨⟨⟨x, y, z⟩, hS⟩, h⟩ => · rw [← hS.1]; ring refine ⟨h, hS.2.2⟩ ⟩, by - simp only [U, gt_iff_lt, secondInvo_fun, Set.mem_setOf_eq] + simp only [U, gt_iff_lt, secondInvo_fun, Set.mem_ofPred_eq] ring_nf exact hS.2.1⟩ @@ -307,6 +307,6 @@ def toTriple := fun (xyz : ℤ × ℤ × ℤ) ↦ -- The second winged derived from the windeg shape of are 73 using `secondInvo`: -#eval secondInvo_fun xyz +-- #eval secondInvo_fun xyz #widget WindmillWidget with ({triple? := (toTriple <| secondInvo_fun xyz)} : WindmillWidgetProps) diff --git a/FormalBook/Chapter_06.lean b/FormalBook/Chapter_06.lean index 0d5c13b..f37ea3e 100644 --- a/FormalBook/Chapter_06.lean +++ b/FormalBook/Chapter_06.lean @@ -119,7 +119,7 @@ lemma div_of_qpoly_div (k n q : ℕ) (hq : 1 < q) (hk : 0 < k) (hn : 0 < n) simp [one_le_pow m q hq', one_le_pow k q hq', one_le_pow (m - k) q hq'] rw [mul_sub, mul_one] ring_nf - simp only [ge_iff_le, add_right_inj] + simp only [add_right_inj] exact (pow_sub_mul_pow (q : ℤ) hkm).symm have h1 : q ^ k - 1 ∣ q ^ (m - k) - 1 := @@ -203,19 +203,19 @@ theorem wedderburn (h: Fintype R): IsField R := by have : ∀ (A : ConjClasses Rˣ), Fintype ↑(Set.centralizer {Quotient.out A}) := fun _ ↦ setFintype (Set.centralizer {Quotient.out _}) - letI fintypea : ∀ (A : ConjClasses Rˣ), Fintype ↑{A | + let fintypea : ∀ (A : ConjClasses Rˣ), Fintype ↑{A | have := finclassa A; Fintype.card ↑(ConjClasses.carrier A) > 1} := fun A ↦ - setFintype {A | let_fun this := finclassa A; Fintype.card ↑(ConjClasses.carrier A) > 1} + setFintype {A | have := finclassa A; Fintype.card ↑(ConjClasses.carrier A) > 1} have : Fintype ↑{A | have := finclassa A; Fintype.card ↑(ConjClasses.carrier A) > 1} := setFintype {A | - let_fun this := finclassa A; + have := finclassa A; Fintype.card ↑(ConjClasses.carrier A) > 1} let S' := ConjClasses.noncenter Rˣ - haveI : Fintype S' := Fintype.ofFinite ↑S' + have : Fintype S' := Fintype.ofFinite ↑S' let S := S'.toFinset --This was wrong: n_k should be the dimension of the centralizer( in `R`), not the cardinality let n_k : S' → ℕ := sorry -- fun A => Fintype.card @@ -224,15 +224,13 @@ theorem wedderburn (h: Fintype R): IsField R := by have h_R: Fintype.card Rˣ = q ^ n - 1 := by have : Fintype.card Rˣ + 1 = Fintype.card R := (Fintype.card_eq_card_units_add_one R).symm rw [← h_card, ← this] - simp only [ge_iff_le, add_le_iff_nonpos_left, nonpos_iff_eq_zero, Fintype.card_ne_zero, - add_tsub_cancel_right] + simp only [add_tsub_cancel_right] have h_Z : Fintype.card Zˣ = q - 1 := by have h : Fintype.card Zˣ + 1 = Fintype.card Z := (Fintype.card_eq_card_units_add_one _).symm have : Fintype.card Z = q := rfl rw [← this, ← h] - simp only [center_toSubsemiring, Subsemiring.center_toSubmonoid, ge_iff_le, - add_le_iff_nonpos_left, nonpos_iff_eq_zero, Fintype.card_ne_zero, add_tsub_cancel_right] + simp only [add_tsub_cancel_right] --class formula (1) @@ -267,7 +265,7 @@ theorem wedderburn (h: Fintype R): IsField R := by have h_k_n_lt_n: n_k A < n := by sorry have h_noneval := phi_div_2 n (n_k A) (h_n_k_A_dvd A) h_k_n_lt_n have := @eval_dvd ℤ _ _ _ q h_noneval - simp only [eval_mul, eval_sub, eval_pow, eval_X, eval_one, IsUnit.mul_iff] at this + simp only [eval_mul, eval_sub, eval_pow, eval_X, eval_one] at this rw [← hq] at * have h_cast_nk : (((q ^ (n_k A) - 1 : ℕ) : ℤ)) = (q : ℤ) ^ (n_k A) - 1 := Nat.cast_sub (hq_pow_pos (n_k A)) diff --git a/FormalBook/Chapter_11.lean b/FormalBook/Chapter_11.lean index ae7d554..9634ce3 100644 --- a/FormalBook/Chapter_11.lean +++ b/FormalBook/Chapter_11.lean @@ -344,7 +344,7 @@ theorem collinear_of_subset_line {S : Set P} {a b : P} theorem exists_ne_of_not_collinear {S : Set P} (hncol : ¬ Collinear ℝ S) : ∃ a ∈ S, ∃ b ∈ S, a ≠ b := by by_contra h - push_neg at h + push Not at h -- if all points coincide, `S` is empty or a singleton: collinear in either case rcases Set.eq_empty_or_nonempty S with rfl | ⟨a, ha⟩ · exact hncol (collinear_empty ℝ P) @@ -364,7 +364,7 @@ theorem exists_third {S : Set P} {a b : P} (ha : a ∈ S) (hb : b ∈ S) (hab : (h : ¬ IsOrdinaryLine (V := V) S a b) : ∃ c ∈ S, c ∈ lineThrough (V := V) a b ∧ c ≠ a ∧ c ≠ b := by by_contra hc - push_neg at hc + push Not at hc refine h ⟨ha, hb, hab, fun c hcS hcL => ?_⟩ by_cases hca : c = a · exact Or.inl hca @@ -384,7 +384,7 @@ that is **strictly closer**. -/ theorem sylvester_gallai (S : Set P) (hfin : S.Finite) (hncol : ¬ Collinear ℝ S) : ∃ a ∈ S, ∃ b ∈ S, IsOrdinaryLine (V := V) S a b := by by_contra hcon - push_neg at hcon + push Not at hcon -- the set of configurations: a point off the line through two other points set T : Set (P × P × P) := {x | x.1 ∈ S ∧ x.2.1 ∈ S ∧ x.2.2 ∈ S ∧ x.2.1 ≠ x.2.2 ∧ diff --git a/FormalBook/Chapter_21.lean b/FormalBook/Chapter_21.lean index db079c8..13f534a 100644 --- a/FormalBook/Chapter_21.lean +++ b/FormalBook/Chapter_21.lean @@ -131,7 +131,7 @@ theorem dalembert_lemma {p : Polynomial ℂ} (hp : p.natDegree > 0) split_ands · calc _ = ‖(∑ k ∈ Icc (m + 1) n, C (c k) * X ^ k).eval z‖ := by congr 2; ext i; simp [r] - _ = ‖∑ k ∈ Icc (m + 1) n, c k * z ^ k‖ := by simp [eval_finset_sum] + _ = ‖∑ k ∈ Icc (m + 1) n, c k * z ^ k‖ := by simp [eval_finsetSum] _ ≤ ∑ k ∈ Icc (m + 1) n, ‖c k * z ^ k‖ := by apply norm_sum_le _ ≤ ∑ k ∈ Icc (m + 1) n, ‖c k‖ * ‖z‖ ^ k := by simp _ ≤ (∑ k ∈ Icc (m + 1) n, ‖c k‖) * ‖z‖ ^ (m + 1) := by diff --git a/FormalBook/Chapter_35.lean b/FormalBook/Chapter_35.lean index b356831..c1862a0 100644 --- a/FormalBook/Chapter_35.lean +++ b/FormalBook/Chapter_35.lean @@ -89,7 +89,7 @@ lemma lemma_35_1_aux {F : Type*} [Field F] [Fintype F] [DecidableEq F] (n : ℕ) apply Or.inl rfl obtain ⟨ q, hq_ne_zero, hq_deg, hq_eval ⟩ := h_poly_b; - simp +decide only [hq_eval, Set.coe_setOf, ha, ↓reduceIte, ge_iff_le] ; + simp +decide only [hq_eval, ha, ↓reduceIte, ge_iff_le] ; rw [ Fintype.card_subtype ] ; exact le_trans ( Finset.card_le_card ( show q.roots.toFinset ⊇ Finset.filter ( fun b => Polynomial.eval b q = 0 ) Finset.univ from fun x hx => by aesop ) ) @@ -107,14 +107,14 @@ lemma lemma_35_1_aux {F : Type*} [Field F] [Fintype F] [DecidableEq F] (n : ℕ) refine' h_count.symm ▸ le_trans ( Finset.sum_le_sum fun a _ => ‹∀ a : Fin n → F, Fintype.card { b : F | ( MvPolynomial.eval ( Fin.cons b a ) ) p = 0 } ≤ if ( MvPolynomial.eval a ) g = 0 then Fintype.card F else d› a ) _; - simp +decide only [Finset.sum_ite, Finset.sum_const, smul_eq_mul, Set.coe_setOf, ne_eq, + simp +decide only [Finset.sum_ite, Finset.sum_const, smul_eq_mul, Set.coe_ofPred, ne_eq, Fintype.card_subtype_compl, Fintype.card_pi, Finset.prod_const, Finset.card_univ, Fintype.card_fin]; simp +decide only [Finset.filter_not, Finset.card_sdiff, Finset.card_univ, Fintype.card_pi, Finset.prod_const, Fintype.card_fin, Finset.inter_univ, Fintype.card_subtype, le_refl]; rcases n with ( _ | n ) <;> simp_all +decide only [ne_eq, zero_tsub, pow_zero, mul_one, Nat.reduceAdd, - Set.coe_setOf, Fintype.card_subtype_compl, Fintype.card_unique, ge_iff_le]; + Set.coe_ofPred, Fintype.card_subtype_compl, Fintype.card_unique, ge_iff_le]; · refine' le_trans h_count _; by_cases h : ( MvPolynomial.eval 0 ) g = 0 <;> simp_all +decide [ Fintype.card_subtype ]; · simp_all +decide only [MvPolynomial.eval_eq', Finset.univ_eq_empty, Finset.prod_empty, @@ -248,7 +248,7 @@ lemma card_exponents_le (n d : ℕ) : intro x; constructor <;> intro hx; · rcases hx with ⟨ a, ⟨ ha₁, ha₂ ⟩, rfl ⟩; convert ha₂ using 1; - simp +decide [ ← Finsupp.sum_finset_sum_index, exponents_le ]; + simp +decide [ ← Finsupp.sum_finsetSum_index, exponents_le ]; · refine' ⟨ fun i => x i, ⟨ _, _ ⟩, _ ⟩; · intro i; have := hx.out; simp_all +decide [ Finsupp.sum_fintype ]; exact le_trans @@ -331,7 +331,7 @@ lemma eval_linePoly {F : Type*} [CommSemiring F] {n : ℕ} (w v : Fin n → F) (linePoly w v p).eval t = MvPolynomial.eval (w + t • v) p := by rw [ linePoly ]; simp +decide [ MvPolynomial.eval₂_eq', MvPolynomial.eval_eq' ]; - simp +decide [ Polynomial.eval_finset_sum, Polynomial.eval_prod ]; + simp +decide [ Polynomial.eval_finsetSum, Polynomial.eval_prod ]; ac_rfl /-- The coefficient of `t^d` in `p(w+tv)` is equal to the evaluation of the homogeneous component @@ -352,7 +352,7 @@ lemma coeff_linePoly_eq_homogeneousComponent_eval {F : Type*} [CommSemiring F] { rw [ Finset.prod_congr rfl fun i _ => by rw [ add_comm, add_pow ] ]; simp +decide [mul_pow ]; rw [ Finset.prod_sum ]; - rw [ Polynomial.finset_sum_coeff, Finset.sum_eq_single ( fun i _ => x i ) ] <;> + rw [ Polynomial.finsetSum_coeff, Finset.sum_eq_single ( fun i _ => x i ) ] <;> simp +decide [Finset.prod_mul_distrib, Finset.prod_pow_eq_pow_sum ] · simp +decide [ Polynomial.coeff_mul, Polynomial.coeff_X_pow ]; rw [ Finset.sum_eq_single ( 0, ∑ i, x i ) ] <;> simp +decide;