more multiGoal linting

dwrensha · Dec 19, 2024 · 65a2d2c · 65a2d2c
1 parent 03722eb
commit 65a2d2c
Show file tree

Hide file tree

Showing 5 changed files with 42 additions and 39 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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