From 65a2d2cee3d0f227772a961e149e659457c8c8e9 Mon Sep 17 00:00:00 2001 From: David Renshaw Date: Wed, 18 Dec 2024 21:27:05 -0500 Subject: [PATCH] more multiGoal linting --- Compfiles/Imo1970P4.lean | 36 ++++++++++++++++++------------------ Compfiles/Imo1984P1.lean | 24 ++++++++++++++---------- Compfiles/Imo2012P4.lean | 2 +- Compfiles/Usa1992P2.lean | 14 +++++++------- lakefile.lean | 5 ++--- 5 files changed, 42 insertions(+), 39 deletions(-) diff --git a/Compfiles/Imo1970P4.lean b/Compfiles/Imo1970P4.lean index 9d97d47f..5c2d52e3 100644 --- a/Compfiles/Imo1970P4.lean +++ b/Compfiles/Imo1970P4.lean @@ -209,24 +209,24 @@ lemma odd_props (n : ℕ) (odd_s : Finset ℕ) (s_odd_eq : odd_s = (Finset.Icc n ext x simp_all only [Finset.mem_insert, Finset.mem_singleton, Finset.mem_filter, Finset.mem_Icc] apply Iff.intro - intro H - constructor - · omega - · cases H - case inl h3 => - simp_all only [Even.add_one] - case inr h4 => - cases h4 - case inl h5 => - have : Odd 3 := by decide - have := Even.add_odd h this - rw[h5] - exact this - case inr h6 => - have : Odd 5 := by decide - have := Even.add_odd h this - rw[h6] - exact this + · intro H + constructor + · omega + · cases H + case inl h3 => + simp_all only [Even.add_one] + case inr h4 => + cases h4 + case inl h5 => + have : Odd 3 := by decide + have := Even.add_odd h this + rw[h5] + exact this + case inr h6 => + have : Odd 5 := by decide + have := Even.add_odd h this + rw[h6] + exact this intro H obtain ⟨a, Hh⟩ := H have h3 := Odd.not_two_dvd_nat Hh diff --git a/Compfiles/Imo1984P1.lean b/Compfiles/Imo1984P1.lean index b69b2405..7301e4d4 100644 --- a/Compfiles/Imo1984P1.lean +++ b/Compfiles/Imo1984P1.lean @@ -32,7 +32,8 @@ lemma geom_mean_le_arith_mean_3 {a b c : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hc · apply Real.rpow_nonneg abc_pos · let w := (1 : ℝ) / 3 change (a * b * c) ^ w ≤ (a + b + c) / 3 - trans w * a + w * b + w * c; rotate_left; unfold w; field_simp + trans w * a + w * b + w * c; rotate_left + · unfold w; field_simp rw [Real.mul_rpow (by positivity) hc] rw [Real.mul_rpow ha hb] apply Real.geom_mean_le_arith_mean3_weighted; all_goals try norm_num; try positivity @@ -69,20 +70,23 @@ problem imo1984_p1 (x y z : ℝ) by linarith] exact this x z y ⟨hx0, hz0, hy0⟩ (by rw [←h₁]; linarith) hx0 hz0 hy0 hxz hxy (by linarith) · constructor - · suffices habs : abs ((1 - 2 * x) * (1 - 2 * y) * (1 - 2 * z)) ≤ 1 - have ⟨i, _⟩ := abs_le.mp habs; linarith only [i] + · suffices habs : abs ((1 - 2 * x) * (1 - 2 * y) * (1 - 2 * z)) ≤ 1 by + have ⟨i, _⟩ := abs_le.mp habs; linarith only [i] rw [abs_mul, abs_mul] - apply mul_le_one₀ - apply mul_le_one₀ - all_goals try positivity - all_goals rw [abs_le]; constructor <;> linarith - · suffices habs : ((1 - 2 * x) * (1 - 2 * y) * (1 - 2 * z)) ≤ (1 : ℝ) / 27; linarith [habs] + refine mul_le_one₀ (mul_le_one₀ ?_ (by positivity) ?_) (by positivity) ?_ <;> + (rw [abs_le]; constructor) <;> linarith + · suffices habs : ((1 - 2 * x) * (1 - 2 * y) * (1 - 2 * z)) ≤ (1 : ℝ) / 27 by linarith [habs] conv => lhs; rw [← h₁] have h1 : 0 ≤ (x + y + z - 2 * x) := by linarith have h2 : 0 ≤ (x + y + z - 2 * y) := by linarith by_cases h3 : 0 ≤ (x + y + z - 2 * z); rotate_left - · trans 0; rotate_left; norm_num; apply nonpos_of_neg_nonneg - rw [←mul_neg]; apply mul_nonneg; positivity; linarith + · trans 0; rotate_left + · norm_num + apply nonpos_of_neg_nonneg + rw [←mul_neg] + apply mul_nonneg + · positivity + · linarith · apply le_trans (geom_mean_le_arith_mean_3 h1 h2 h3) rw [show (x + y + z - 2 * x + (x + y + z - 2 * y) + (x + y + z - 2 * z)) = 1 by rw [←h₁]; ring_nf] diff --git a/Compfiles/Imo2012P4.lean b/Compfiles/Imo2012P4.lean index eca78516..d5f57755 100644 --- a/Compfiles/Imo2012P4.lean +++ b/Compfiles/Imo2012P4.lean @@ -288,7 +288,7 @@ problem imo2012_p4 (f : ℤ → ℤ) : rcases sol with ⟨d, h⟩ · rcases Int.even_or_odd a with evena | odda - simp [(h a).right evena]; rotate_left; simp [(h a).left odda] + simp only [(h a).right evena]; rotate_left; simp only [(h a).left odda] all_goals rcases Int.even_or_odd b with evenb | oddb simp [(h b).right evenb]; rotate_left; simp [(h b).left oddb] diff --git a/Compfiles/Usa1992P2.lean b/Compfiles/Usa1992P2.lean index dae6b0ed..b1021b3b 100644 --- a/Compfiles/Usa1992P2.lean +++ b/Compfiles/Usa1992P2.lean @@ -51,13 +51,13 @@ problem usa1992_p2 : ∑ i ∈ Finset.range 89, (π / 180).sin / ((↑i * π / 180).cos * (↑(i + 1) * π / 180).cos) = ∑ i ∈ Finset.range 89, (((↑(i + 1)) * π / 180).sin / ((↑(i + 1)) * π / 180).cos - (↑i * π / 180).sin / (↑i * π / 180).cos) - rw [new_goal] - rw [Finset.sum_range_sub (fun i ↦ (↑i * π / 180).sin / (↑i * π / 180).cos) 89] - simp only [Nat.cast_ofNat, CharP.cast_eq_zero, zero_mul, zero_div, - sin_zero, cos_zero, div_one, sub_zero] - rw [← Real.cos_pi_div_two_sub, ← Real.cos_pi_div_two_sub] - rw [show (π / 2 - 89 * π / 180) = π / 180 by ring] - rw [show (π / 2 - π / 180) = 89 * π / 180 by ring] + · rw [new_goal] + rw [Finset.sum_range_sub (fun i ↦ (↑i * π / 180).sin / (↑i * π / 180).cos) 89] + simp only [Nat.cast_ofNat, CharP.cast_eq_zero, zero_mul, zero_div, + sin_zero, cos_zero, div_one, sub_zero] + rw [← Real.cos_pi_div_two_sub, ← Real.cos_pi_div_two_sub] + rw [show (π / 2 - 89 * π / 180) = π / 180 by ring] + rw [show (π / 2 - π / 180) = 89 * π / 180 by ring] apply Finset.sum_congr rfl simp only [Finset.mem_range] diff --git a/lakefile.lean b/lakefile.lean index e6d5f8f3..65fb533c 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -6,12 +6,11 @@ abbrev leanOptions : Array LeanOption := #[ ⟨`pp.unicode.fun, true⟩, -- pretty-prints `fun a ↦ b` ⟨`autoImplicit, false⟩, ⟨`relaxedAutoImplicit, false⟩ --- ⟨`weak.linter.style.multiGoal, true⟩ ] package compfiles where - leanOptions := leanOptions - moreServerOptions := leanOptions + leanOptions := leanOptions -- ++ #[⟨`weak.linter.style.multiGoal, true⟩] + moreServerOptions := leanOptions -- ++ #[⟨`linter.style.multiGoal, true⟩] @[default_target] lean_lib ProblemExtraction