Fix Archive and Counterexamples.

Author: Vierkantor

Archive/Imo/Imo1982Q3.lean

@@ -88,6 +88,6 @@ theorem imo1982_q3b : ∃ x : ℕ → ℝ, Antitone x ∧ x 0 = 1 ∧ (∀ k, 0
     simp_rw [← pow_mul, pow_succ, ← div_eq_mul_inv, div_div_eq_mul_div, mul_comm, mul_div_assoc,
       ← mul_sum, div_eq_mul_inv, this, ← two_add_two_eq_four, ← mul_two,
       mul_lt_mul_iff_of_pos_left two_pos]
-    convert NNReal.coe_lt_coe.2 <| geom_sum_lt (inv_ne_zero two_ne_zero) two_inv_lt_one n
+    convert! NNReal.coe_lt_coe.2 <| geom_sum_lt (inv_ne_zero two_ne_zero) two_inv_lt_one n
     · simp
     · norm_num

Archive/Imo/Imo2006Q5.lean

@@ -72,7 +72,7 @@ theorem Polynomial.isPeriodicPt_eval_two {P : Polynomial ℤ} {t : ℤ}
   have Hdvd : C.Chain (· ∣ ·) := by
     rw [Cycle.chain_map, periodicOrbit_chain' _ ht]
     intro n
-    convert sub_dvd_eval_sub ((fun x => P.eval x)^[n + 1] t) ((fun x => P.eval x)^[n] t) P <;>
+    convert! sub_dvd_eval_sub ((fun x => P.eval x)^[n + 1] t) ((fun x => P.eval x)^[n] t) P <;>
       rw [Function.iterate_succ_apply']
   -- Any two entries in C have the same absolute value.
   have Habs :

Archive/Imo/Imo2008Q2.lean

@@ -51,7 +51,7 @@ theorem imo2008_q2a (x y z : ℝ) (h : x * y * z = 1) (hx : x ≠ 1) (hy : y ≠
   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)))
+  convert! sq_nonneg ((c * (m ^ 2 + n ^ 2 + m * n) - m * (m + n) ^ 2) / (m * n * (m + n)))
   simp [field, hc_sub_sub]; ring
 
 def rationalSolutions :=

Archive/Imo/Imo2015Q6.lean

@@ -161,7 +161,7 @@ lemma sum_telescope {m n : ℕ} (hm : N ≤ m) (hn : m < n) :
 
 include ht in
 lemma le_sum_pool : ∑ i ∈ range b, (i : ℤ) ≤ ∑ x ∈ pool a t, x := by
-  convert sum_range_le_sum fun x mx ↦ (mem_Icc.mp ((pool_subset_Icc ha) mx)).1
+  convert! sum_range_le_sum fun x mx ↦ (mem_Icc.mp ((pool_subset_Icc ha) mx)).1
   · rw [hbN _ ht]
   · rw [zero_add]
 

Archive/Imo/Imo2024Q1.lean

@@ -52,7 +52,7 @@ lemma condition_sub_two_mul_int_iff {α : ℝ} (m : ℤ) : Condition (α - 2 * m
   simp_rw [← Finset.sum_sub_distrib, mul_sub]
   norm_cast
   simp_rw [Int.floor_sub_intCast, sub_sub_cancel_left]
-  convert condition_two_mul_int (-m) n hn
+  convert! condition_two_mul_int (-m) n hn
   norm_cast
   rw [Int.floor_intCast]
   simp
@@ -76,7 +76,7 @@ lemma mem_Ico_one_of_mem_Ioo (h : α ∈ Set.Ioo 0 2) : α ∈ Set.Ico 1 2 := by
   apply hr.ne'
   suffices ⌈α⁻¹⌉₊ = (1 : ℤ) from mod_cast this
   apply Int.eq_one_of_dvd_one (Int.zero_le_ofNat _)
-  convert hc ⌈α⁻¹⌉₊ (zero_lt_one.trans hr)
+  convert! hc ⌈α⁻¹⌉₊ (zero_lt_one.trans hr)
   rw [← Finset.add_sum_Ico_eq_sum_Icc hr.le]
   convert (add_zero _).symm
   · rw [Int.floor_eq_iff]
@@ -153,7 +153,7 @@ lemma not_condition_of_mem_Ioo {α : ℝ} (h : α ∈ Set.Ioo 0 2) : ¬Condition
   have hna := (hc.mem_Ico_n_of_mem_Ioo h hn).1
   rcases h with ⟨-, h2⟩
   have hna' : 2 - (n : ℝ)⁻¹ ≤ α := by
-    convert hna using 1
+    convert! hna using 1
     field
   rw [sub_eq_add_neg, ← le_sub_iff_add_le', neg_le, neg_sub] at hna'
   rw [le_inv_comm₀ (by linarith) (mod_cast hn), ← not_lt] at hna'

Archive/Imo/Imo2024Q2.lean

@@ -37,7 +37,7 @@ lemma dvd_pow_iff_of_dvd_sub {a b d n : ℕ} {z : ℤ} (ha : a.Coprime d)
   congr
   suffices (((ZMod.unitOfCoprime _ ha) ^ z : (ZMod d)ˣ) : ZMod d) =
       (((ZMod.unitOfCoprime _ ha) ^ (n : ℤ) : (ZMod d)ˣ) : ZMod d) by
-    convert this
+    convert! this
   rw [sub_eq_iff_eq_add] at hk
   rw [hk, zpow_add, zpow_mul]
   norm_cast

Archive/Imo/Imo2024Q3.lean

@@ -113,7 +113,7 @@ lemma apply_add_one_eq_card {n : ℕ} (h : N ≤ n) :
   simp
 
 @[simp] lemma nth_apply_eq_zero (n : ℕ) : Nat.nth (a · = 0) n = 0 := by
-  convert Nat.nth_false _ with i
+  convert! Nat.nth_false _ with i
   simp only [(hc.pos i).ne']
 
 lemma nth_apply_add_one_eq {n : ℕ} (h : N ≤ n) : Nat.nth (a · = a n) (a (n + 1) - 1) = n := by
@@ -244,7 +244,7 @@ lemma card_lt_M_of_M_le {n : ℕ} (h : M a N ≤ n) :
   have ha : M a N ≤ a (Nat.nth (a · = n) (M a N - 1)) := (Nat.nth_mem _ hin').symm ▸ h
   refine ⟨ha, ?_⟩
   suffices H : a (Nat.nth (fun x ↦ a x = n) (M a N - 1) + 1) = M a N from Nat.le_of_eq H.symm
-  convert hc.apply_nth_add_one_eq hin' (N_lt_of_M_le_apply ha).le using 1
+  convert! hc.apply_nth_add_one_eq hin' (N_lt_of_M_le_apply ha).le using 1
 
 lemma bddAbove_setOf_infinite_setOf_apply_eq : BddAbove {m | {i | a i = m}.Infinite} := by
   refine ⟨M a N, fun x hi ↦ ?_⟩
@@ -542,7 +542,7 @@ lemma apply_sub_one_big_of_apply_small_of_N'_lt {i : ℕ} (h : Small a (a i)) (h
 
 lemma apply_sub_two_small_of_apply_small_of_N'_lt {i : ℕ} (h : Small a (a i)) (hN' : N' a N < i) :
     Small a (a (i - 2)) := by
-  convert hc.apply_sub_one_small_of_apply_big_of_N'_le
+  convert! hc.apply_sub_one_small_of_apply_big_of_N'_le
     (hc.apply_sub_one_big_of_apply_small_of_N'_lt h hN') (by lia) using 1
 
 lemma N_add_one_lt_apply_of_apply_big_of_N'_le {i : ℕ} (h : Big a (a i)) (hN' : N' a N ≤ i) :
@@ -751,8 +751,8 @@ lemma exists_apply_sub_two_eq_of_apply_eq {i j : ℕ} (hi : N' a N + 2 < i) (hij
           congr 1
           ext t
           simp only [Finset.mem_filter, Finset.mem_range]
-          refine ⟨fun ⟨htj, htj'⟩ ↦ ⟨?_, by convert htj' using 1⟩,
-            fun ⟨htj, htj'⟩ ↦ ⟨by lia, by convert htj' using 1⟩⟩
+          refine ⟨fun ⟨htj, htj'⟩ ↦ ⟨?_, by convert! htj' using 1⟩,
+            fun ⟨htj, htj'⟩ ↦ ⟨by lia, by convert! htj' using 1⟩⟩
           by_contra htj''
           have ht1 : t = j - 1 := by lia
           subst ht1
@@ -923,7 +923,7 @@ lemma exists_p_eq : ∃ b c, ∀ n, b < n → p a (N' a N + 2 * n) = c := by
       · have hs : Small a (a (N' a N + 2 * (2 + t + u))) := by
           rw [hc.small_apply_N'_add_iff_even]
           simp
-        convert hc.p_apply_le_p_apply_add_two (by lia) hs using 1
+        convert! hc.p_apply_le_p_apply_add_two (by lia) hs using 1
   refine ⟨1 + t, c, fun n hn ↦ ?_⟩
   rw [show n = 2 + t + (n - (2 + t)) by lia]
   exact heqc _

Archive/Imo/Imo2024Q5.lean

@@ -249,12 +249,12 @@ lemma Path.findFstEq_eq_find?_le (p : Path N) (r : Fin (N + 2)) : p.findFstEq r
 
 lemma Path.firstMonster_isSome {p : Path N} {m : MonsterData N} :
     (p.firstMonster m).isSome = true ↔ ∃ x, x ∈ p.cells ∧ x ∈ m.monsterCells := by
-  convert List.find?_isSome
+  convert! List.find?_isSome
   simp
 
 lemma Path.firstMonster_eq_none {p : Path N} {m : MonsterData N} :
     (p.firstMonster m) = none ↔ ∀ x, x ∈ p.cells → x ∉ m.monsterCells := by
-  convert List.find?_eq_none
+  convert! List.find?_eq_none
   simp
 
 lemma Path.one_lt_length_cells (p : Path N) : 1 < p.cells.length := by
@@ -339,7 +339,7 @@ lemma Path.firstMonster_eq_of_findFstEq_mem {p : Path N} {m : MonsterData N}
       List.isChain_iff_getElem.1 p.valid_move_seq 0 (by lia)
     simp_rw [Adjacent, Nat.dist] at adj
     have hc0 : (p.cells[0].1 : ℕ) = 0 := by
-      convert Fin.ext_iff.1 p.head_first_row
+      convert! Fin.ext_iff.1 p.head_first_row
       exact List.getElem_zero _
     have hc1 : (p.cells[1].1 : ℕ) ≠ 0 := Fin.val_ne_iff.2 h0
     have h1 : (p.cells[1].1 : ℕ) = 1 := by lia
@@ -452,7 +452,7 @@ def Path.reflect (p : Path N) : Path N where
 lemma Path.firstMonster_reflect (p : Path N) (m : MonsterData N) :
     p.reflect.firstMonster m.reflect = (p.firstMonster m).map Cell.reflect := by
   simp_rw [firstMonster, reflect, List.find?_map]
-  convert rfl
+  convert! rfl
   simp only [Function.comp_apply, decide_eq_decide, MonsterData.monsterCells]
   refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
   · rcases h with ⟨i, hi⟩
@@ -509,7 +509,7 @@ lemma Strategy.play_two (s : Strategy N) (m : MonsterData N) {k : ℕ} (hk : 2 <
   · have h : (1 : Fin 2) = Fin.last 1 := rfl
     simp only [Fin.snoc_zero, Nat.reduceAdd, Fin.mk_one, Fin.isValue, Matrix.cons_val]
     simp only [h, Fin.snoc_last]
-    convert rfl
+    convert! rfl
     simp_rw [Fin.fin_one_eq_zero, Matrix.cons_val]
 
 lemma Strategy.WinsIn.mono (s : Strategy N) (m : MonsterData N) {k₁ k₂ : ℕ} (h : s.WinsIn m k₁)
@@ -555,7 +555,7 @@ lemma row1_mem_monsterCells_monsterData12 (hN : 2 ≤ N) (c₁ c₂ : Fin (N + 1
 
 lemma row2_mem_monsterCells_monsterData12 (hN : 2 ≤ N) {c₁ c₂ : Fin (N + 1)} (h : c₁ ≠ c₂) :
     (⟨2, by lia⟩, c₂) ∈ (monsterData12 hN c₁ c₂).monsterCells := by
-  convert Set.mem_range_self (row2 hN)
+  convert! Set.mem_range_self (row2 hN)
   exact (monsterData12_apply_row2 hN h).symm
 
 lemma Strategy.not_forcesWinIn_two (s : Strategy N) (hN : 2 ≤ N) : ¬ s.ForcesWinIn 2 := by

Archive/Kuratowski.lean

@@ -102,7 +102,7 @@ theorem mem_theFourteen_iff_isObtainable {s t : Set X} :
 complement operations from a single set `s` is at most 14. -/
 theorem ncard_isObtainable_le_fourteen (s : Set X) : {t | IsObtainable s t}.ncard ≤ 14 := by
   classical
-  convert Set.ncard_coe_finset _ ▸ (theFourteen s).toFinset_card_le
+  convert! Set.ncard_coe_finset _ ▸ (theFourteen s).toFinset_card_le
   simp [Set.ext_iff, mem_theFourteen_iff_isObtainable]
 
 end Topology.ClosureCompl

Archive/Sensitivity.lean

@@ -90,7 +90,7 @@ theorem succ_n_eq (p q : Q n.succ) : p = q ↔ p 0 = q 0 ∧ π p = π q := by
     by_cases hx : x = 0
     · rwa [hx]
     · rw [← Fin.succ_pred x hx]
-      convert congr_fun h (Fin.pred x hx)
+      convert! congr_fun h (Fin.pred x hx)
 
 /-- The adjacency relation defining the graph structure on `Q n`:
 `p.adjacent q` if there is an edge from `p` to `q` in `Q n`. -/
@@ -392,7 +392,7 @@ theorem exists_eigenvalue (H : Set (Q m.succ)) (hH : Card H ≥ 2 ^ m + 1) :
     apply dim_V
   have dimW : dim W = card H := by
     have li : LinearIndependent ℝ (H.restrict e) := by
-      convert (dualBases_e_ε m.succ).basis.linearIndependent.comp _ Subtype.val_injective
+      convert! (dualBases_e_ε m.succ).basis.linearIndependent.comp _ Subtype.val_injective
       rw [(dualBases_e_ε _).coe_basis]
       rfl
     have hdW := rank_span li