Merge remote-tracking branch 'upstream/master' into silence-docstring-urls

Author: Vierkantor

.github/workflows/build_template.yml

@@ -743,6 +743,12 @@ jobs:
       - name: clean up the import graph file
         run: rm import_graph.dot
 
+      - name: check all scripts build successfully
+        run: |
+          lake env lean scripts/create_deprecated_modules.lean
+          lake env lean scripts/autolabel.lean
+          lake exe check_title_labels --labels "t-algebra" "feat: dummy PR for testing"
+
       - name: build everything
         # make sure everything is available for test/import_all.lean
         # and that miscellaneous executables still work

Archive/Imo/Imo1962Q1.lean

@@ -105,9 +105,7 @@ lemma case_more_digits {c n : ℕ} (hc : (digits 10 c).length ≥ 6) (hpp : Prob
 Now we combine these cases to show that 153846 is the smallest solution.
 -/
 
-lemma satisfied_by_153846 : ProblemPredicate 153846 := by
-  norm_num [ProblemPredicate]
-  decide
+lemma satisfied_by_153846 : ProblemPredicate 153846 := by simp +decide [ProblemPredicate]
 
 lemma no_smaller_solutions (n : ℕ) (hn : ProblemPredicate n) : n ≥ 153846 := by
   have ⟨c, hcn⟩ := without_digits hn

Archive/Imo/Imo1962Q4.lean

@@ -59,8 +59,7 @@ Now we can solve for `x` using basic-ish trigonometry.
 -/
 theorem solve_cos2_half {x : ℝ} : cos x ^ 2 = 1 / 2 ↔ ∃ k : ℤ, x = (2 * ↑k + 1) * π / 4 := by
   rw [cos_sq]
-  simp only [add_eq_left, div_eq_zero_iff]
-  norm_num
+  simp only [add_eq_left, div_eq_zero_iff, OfNat.ofNat_ne_zero, or_false]
   rw [cos_eq_zero_iff]
   constructor <;>
     · rintro ⟨k, h⟩

Archive/Imo/Imo1988Q6.lean

@@ -179,7 +179,7 @@ theorem constant_descent_vieta_jumping (x y : ℕ) {claim : Prop} {H : ℕ → 
     suffices hc : c ≠ mx from lt_of_le_of_ne (mod_cast c_lt) hc
     -- However, recall that B(m_x) ≠ m_x + m_y.
     -- If c = m_x, we can prove B(m_x) = m_x + m_y.
-    contrapose! hm_B₂
+    contrapose hm_B₂
     subst c
     simp [hV₁]
     -- Hence p' = (c, m_x) lies on the upper branch, and we are done.
@@ -281,7 +281,7 @@ example {a b : ℕ} (h : a * b ∣ a ^ 2 + b ^ 2 + 1) : 3 * a * b = a ^ 2 + b ^
       apply ne_of_gt
       push Not at h_base
       calc
-        z * y > x * y := by apply mul_lt_mul_of_pos_right <;> lia
+        z * y > x * y := by gcongr; lia
         _ ≥ x * (x + 1) := by apply mul_le_mul <;> lia
         _ > x * x + 1 := by
           rw [mul_add]

Archive/Imo/Imo2008Q2.lean

@@ -46,9 +46,9 @@ theorem imo2008_q2a (x y z : ℝ) (h : x * y * z = 1) (hx : x ≠ 1) (hy : y ≠
     x ^ 2 / (x - 1) ^ 2 + y ^ 2 / (y - 1) ^ 2 + z ^ 2 / (z - 1) ^ 2 ≥ 1 := by
   obtain ⟨a, b, c, ha, hb, hc, rfl, rfl, rfl⟩ := subst_abc h
   obtain ⟨m, n, rfl, rfl⟩ : ∃ m n, b = c - m ∧ a = c - m - n := by use c - b, b - a; simp
-  have hm_ne_zero : m ≠ 0 := by contrapose! hy; simpa [field]
-  have hn_ne_zero : n ≠ 0 := by contrapose! hx; simpa [field]
-  have hmn_ne_zero : m + n ≠ 0 := by contrapose! hz; field_simp; linarith
+  have hm_ne_zero : m ≠ 0 := by contrapose hy; simpa [field]
+  have hn_ne_zero : n ≠ 0 := by contrapose hx; simpa [field]
+  have hmn_ne_zero : m + n ≠ 0 := by contrapose hz; field_simp; linarith
   have hc_sub_sub : c - (c - m - n) = m + n := by abel
   rw [ge_iff_le, ← sub_nonneg]
   convert sq_nonneg ((c * (m ^ 2 + n ^ 2 + m * n) - m * (m + n) ^ 2) / (m * n * (m + n)))

Archive/Imo/Imo2019Q4.lean

@@ -75,6 +75,7 @@ theorem upper_bound {k n : ℕ} (hk : k > 0)
 
 end Imo2019Q4
 
+set_option linter.flexible false in -- TODO: fix non-terminal simp
 theorem imo2019_q4 {k n : ℕ} (hk : 0 < k) (hn : 0 < n) :
     (k ! : ℤ) = ∏ i ∈ range n, ((2 : ℤ) ^ n - (2 : ℤ) ^ i) ↔ (k, n) = (1, 1) ∨ (k, n) = (3, 2) := by
   -- The implication `←` holds.
@@ -90,7 +91,7 @@ theorem imo2019_q4 {k n : ℕ} (hk : 0 < k) (hn : 0 < n) :
   -- n = 2
   · right; congr; norm_num [prod_range_succ] at h; norm_cast at h; rwa [← factorial_inj']
     norm_num
-  all_goals exfalso; norm_num [prod_range_succ] at h; norm_cast at h
+  all_goals exfalso; simp [prod_range_succ] at h; norm_cast at h
   -- n = 3
   · refine monotone_factorial.ne_of_lt_of_lt_nat 5 ?_ ?_ _ h <;> decide
   -- n = 4

Archive/MiuLanguage/DecisionNec.lean

@@ -133,7 +133,7 @@ theorem goodm_of_rule2 (xs : Miustr) (_ : Derivable (M :: xs)) (h₂ : Goodm (M
   constructor
   · rfl
   · obtain ⟨mhead, mtail⟩ := h₂
-    contrapose! mtail
+    contrapose mtail
     rw [cons_append] at mtail
     exact or_self_iff.mp (mem_append.mp mtail)
 
@@ -145,7 +145,7 @@ theorem goodm_of_rule3 (as bs : Miustr) (h₁ : Derivable (as ++ [I, I, I] ++ bs
   · cases as
     · contradiction
     exact mhead
-  · contrapose! nmtail
+  · contrapose nmtail
     rcases exists_cons_of_ne_nil k with ⟨x, xs, rfl⟩
     simp_rw [cons_append] at nmtail ⊢
     simpa using nmtail
@@ -163,7 +163,7 @@ theorem goodm_of_rule4 (as bs : Miustr) (h₁ : Derivable (as ++ [U, U] ++ bs))
   · cases as
     · contradiction
     exact mhead
-  · contrapose! nmtail
+  · contrapose nmtail
     rcases exists_cons_of_ne_nil k with ⟨x, xs, rfl⟩
     simp_rw [cons_append] at nmtail ⊢
     simpa using nmtail

Archive/OxfordInvariants/Summer2021/Week3P1.lean

@@ -95,9 +95,7 @@ theorem OxfordInvariants.Week3P1 (n : ℕ) (a : ℕ → ℕ) (a_pos : ∀ i ≤
     Claim that the sum equals `1` -/
     refine ⟨1, ?_, ?_⟩
     -- Check that this indeed equals the sum
-    · rw [Nat.cast_one, Finset.sum_range_one]
-      norm_num
-      rw [div_self]
+    · rw [Nat.cast_one, Finset.sum_range_one, zero_add, div_self]
       exact (mul_pos (a_pos 0 (Nat.zero_le _)) (a_pos 1 (Nat.zero_lt_succ _))).ne'
     -- Check the divisibility condition
     · rw [mul_one, tsub_self]

Archive/Sensitivity.lean

@@ -131,7 +131,7 @@ theorem adj_iff_proj_adj {p q : Q n.succ} (h₀ : p 0 = q 0) :
     rw [← Fin.pred_inj (ha := (?ha : y ≠ 0)) (hb := (?hb : i.succ ≠ 0)),
       Fin.pred_succ]
     case ha =>
-      contrapose! hy
+      contrapose hy
       rw [hy, h₀]
     case hb =>
       apply Fin.succ_ne_zero

Archive/Wiedijk100Theorems/PerfectNumbers.lean

@@ -62,7 +62,7 @@ theorem eq_two_pow_mul_odd {n : ℕ} (hpos : 0 < n) : ∃ k m : ℕ, n = 2 ^ k *
   refine ⟨hm, ?_⟩
   rw [even_iff_two_dvd]
   have hg := h.not_pow_dvd_of_multiplicity_lt (Nat.lt_succ_self _)
-  contrapose! hg
+  contrapose hg
   rcases hg with ⟨k, rfl⟩
   apply Dvd.intro k
   rw [pow_succ, mul_assoc, ← hm]
@@ -105,7 +105,7 @@ theorem eq_two_pow_mul_prime_mersenne_of_even_perfect {n : ℕ} (ev : Even n) (p
         apply ne_of_lt _ jcon2
         rw [mersenne, ← Nat.pred_eq_sub_one, Nat.lt_pred_iff, ← pow_one (Nat.succ 1)]
         apply pow_lt_pow_right₀ (Nat.lt_succ_self 1) (Nat.succ_lt_succ k.succ_pos)
-    contrapose! hm
+    contrapose hm
     simp [hm]
 
 /-- The Euclid-Euler theorem characterizing even perfect numbers -/