Merge branch 'master' into diffgeo-docstrings-preelaborators

Author: grunweg

.github/actions/get-mathlib-ci/action.yml

@@ -10,7 +10,7 @@ inputs:
     # Default pinned commit used by workflows unless they explicitly override.
     # Update this ref as needed to pick up changes to mathlib-ci scripts
     # This is also updated automatically by .github/workflows/update_dependencies.yml
-    default: aafe3df227b81f681afa3978f9eab0e2bbcd0582
+    default: 194b03113712fdf55c2c29651f161893f0305fe8
   path:
     description: Checkout destination path.
     required: false

.github/workflows/build_template.yml

@@ -222,7 +222,7 @@ jobs:
 
       - name: validate lake-manifest.json inputRevs
         # Only enforce this on the main mathlib4 repository, not on nightly-testing
-        if: github.repository == 'leanprover-community/mathlib4'
+        if: github.repository == 'leanprover-community/mathlib4' && github.ref_name != 'nightly-testing'
         shell: bash
         run: |
           cd pr-branch

.github/workflows/lake_cache_shadow.yml

@@ -24,6 +24,7 @@ We add some local simp lemmas so we can unfold the definitions of the normalizat
 attribute [local simp] normalized hasNestedIf hasConstantIf hasRedundantIf disjoint vars
   List.disjoint
 
+set_option warning.simp.varHead false in
 attribute [local simp] apply_ite ite_eq_iff'
 
 variable {b : Bool} {f : ℕ → Bool} {i : ℕ} {t e : IfExpr}

Archive/Examples/IfNormalization/Result.lean

@@ -65,27 +65,27 @@ def normalize' (l : AList (fun _ : ℕ => Bool)) :
             · congr
               ext w
               by_cases h : w = v
-              · substs h
+              · subst h
                 simp_all
               · simp_all
             · congr
               ext w
               by_cases h : w = v
-              · substs h
+              · subst h
                 simp_all
               · simp_all
           · simp only [cond_true, h, ht₁]
             refine ⟨fun _ => ?_, fun _ => ?_⟩
             · congr
               ext w
               by_cases h : w = v
-              · substs h
+              · subst h
                 simp_all
               · simp_all
             · congr
               ext w
               by_cases h : w = v
-              · substs h
+              · subst h
                 simp_all
               · simp_all
         · have := ht₃ v

Archive/Examples/IfNormalization/WithoutAesop.lean

@@ -3,7 +3,7 @@ Copyright (c) 2024 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
-import Mathlib.Data.Real.Sqrt
+import Mathlib.Analysis.Real.Sqrt
 
 /-!
 # IMO 1959 Q2

Archive/Imo/Imo1959Q2.lean

@@ -3,7 +3,7 @@ Copyright (c) 2024 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
-import Mathlib.Data.Real.Sqrt
+import Mathlib.Analysis.Real.Sqrt
 
 /-!
 # IMO 1960 Q2

Archive/Imo/Imo1960Q2.lean

@@ -42,5 +42,5 @@ theorem imo1977_q6 (f : ℕ+ → ℕ+) (h : ∀ n, f (f n) < f (n + 1)) : ∀ n,
     refine imo1977_q6_nat (fun m => if 0 < m then f m.toPNat' else 0) ?_ n
     intro x; cases x
     · simp
-    · simpa using h _
+    · simpa using! h _
   simpa

Archive/Imo/Imo1977Q6.lean

@@ -85,7 +85,7 @@ def fixedPointsEquiv' :
 theorem main_fintype : ∑ k ∈ range (card α + 1), k * p α k = card α * (card α - 1)! := by
   have A : ∀ (k) (σ : fiber α k), card (fixedPoints (↑σ : Perm α)) = k := fun k σ => σ.2
   simpa [A, ← Fin.sum_univ_eq_sum_range, -card_ofFinset, Finset.card_univ, card_fixed_points,
-    mul_comm] using card_congr (fixedPointsEquiv' α)
+    mul_comm] using! card_congr (fixedPointsEquiv' α)
 
 /-- Main statement for permutations of `Fin n`, a version that works for `n = 0`. -/
 theorem main₀ (n : ℕ) : ∑ k ∈ range (n + 1), k * p (Fin n) k = n * (n - 1)! := by

Archive/Imo/Imo1987Q1.lean

@@ -171,7 +171,7 @@ theorem constant_descent_vieta_jumping (x y : ℕ) {claim : Prop} {H : ℕ → 
   rw [exceptional_empty, Set.diff_empty]
   -- Now we are ready to prove that p' = (c, m_x) lies on the upper branch.
   -- We need to check two conditions: H(c, m_x) and c < m_x.
-  constructor <;> dsimp only
+  constructor
   · -- The first condition is not so hard. After all, c is the other root of the quadratic equation.
     rw [H_symm, H_quad]
     simpa using h_root