pointwise birkhoff theorem

Author: lua-vr

Archive/Examples/Eisenstein.lean

@@ -59,7 +59,7 @@ example : Irreducible (X ^ 4 - 10 * X ^ 2 + 1 : ℤ[X]) := by
       CharP.ker_intAlgebraMap_eq_span 3, span_singleton_pow, mem_span_singleton]
       norm_num
     rw [hfq, ← modByMonicHom_apply, map_add]
-    convert zero_add _
+    convert! zero_add _
     · rw [← LinearMap.mem_ker, mem_ker_modByMonic hq_monic]
       rw [pow_two, ← sub_mul]
       apply dvd_mul_left

Archive/Imo/Imo1959Q2.lean

@@ -60,7 +60,7 @@ theorem sqrt_two_mul_sub_one_le_one : sqrt (2 * x - 1) ≤ 1 ↔ x ≤ 1 := by
 theorem isGood_iff_eq_sqrt_two (hx : x ∈ Icc (1 / 2) 1) : IsGood x A ↔ A = sqrt 2 := by
   have : sqrt (2 * x - 1) ≤ 1 := sqrt_two_mul_sub_one_le_one.2 hx.2
   simp only [isGood_iff, hx.1, abs_sub_comm _ (1 : ℝ), abs_of_nonneg (sub_nonneg.2 this), and_true]
-  suffices 2 = A * sqrt 2 ↔ A = sqrt 2 by convert this using 2; ring
+  suffices 2 = A * sqrt 2 ↔ A = sqrt 2 by convert! this using 2; ring
   rw [← div_eq_iff, div_sqrt, eq_comm]
   positivity
 

Archive/Imo/Imo1982Q3.lean

@@ -74,7 +74,7 @@ end Imo1982Q3
 theorem imo1982_q3a (hx : Antitone x) (h0 : x 0 = 1) (hp : ∀ k, 0 < x k) :
     ∃ n : ℕ, 3.999 ≤ ∑ k ∈ range n, (x k) ^ 2 / x (k + 1) := by
   use 4000
-  convert Imo1982Q3.ineq (Nat.succ_ne_zero 3998) hx h0 hp
+  convert! Imo1982Q3.ineq (Nat.succ_ne_zero 3998) hx h0 hp
   norm_num
 
 /-- Part b of the problem is solved by `x k = (1 / 2) ^ k`. -/
@@ -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/Imo1994Q1.lean

@@ -54,7 +54,7 @@ theorem imo1994_q1 (n : ℕ) (m : ℕ) (A : Finset ℕ) (hm : #A = m + 1)
   -- `i ↦ m-i`
   -- We reindex the sum by fin (m+1)
   have : ∑ x ∈ A, x = ∑ i : Fin (m + 1), a i := by
-    convert sum_image fun x _ y _ => a.eq_iff_eq.1
+    convert! sum_image fun x _ y _ => a.eq_iff_eq.1
     rw [← coe_inj]; simp [a]
   rw [this]; clear this
   -- The main proof is a simple calculation by rearranging one of the two sums

Archive/Imo/Imo1998Q2.lean

@@ -210,7 +210,7 @@ end
 theorem clear_denominators {a b k : ℕ} (ha : 0 < a) (hb : 0 < b) :
     (b - 1 : ℚ) / (2 * b) ≤ k / a ↔ ((b : ℕ) - 1) * a ≤ k * (2 * b) := by
   rw [div_le_div_iff₀]
-  on_goal 1 => convert Nat.cast_le (α := ℚ)
+  on_goal 1 => convert! Nat.cast_le (α := ℚ)
   all_goals simp [ha, hb]
 
 end

Archive/Imo/Imo2001Q5.lean

@@ -104,7 +104,7 @@ lemma x_pos : 0 < s.x := by
   have col := s.ABC_eq; rw [h, mul_zero] at col
   replace col : Collinear ℝ {s.A, s.B, s.C} := by
     apply collinear_of_sin_eq_zero; rw [col, Real.sin_zero]
-  apply s.not_collinear_BAC; convert col using 1; grind
+  apply s.not_collinear_BAC; convert! col using 1; grind
 
 lemma Q_ne_A : s.Q ≠ s.A := by
   by_contra h; have := s.ABQ_eq
@@ -127,7 +127,7 @@ lemma x_lt_pi_div_three : s.x < π / 3 := by
   have col : ∠ s.A s.C s.B = 0 := by linarith [s.ACB_eq, angle_nonneg s.A s.C s.B]
   replace col : Collinear ℝ {s.A, s.C, s.B} := by
     apply collinear_of_sin_eq_zero; rw [col, Real.sin_zero]
-  apply s.not_collinear_BAC; convert col using 1; grind
+  apply s.not_collinear_BAC; convert! col using 1; grind
 
 lemma APB_eq : ∠ s.A s.P s.B = 5 * π / 6 - 2 * s.x := by
   have := angle_add_angle_add_angle_eq_pi s.P s.A_ne_B

Archive/Imo/Imo2006Q3.lean

@@ -79,8 +79,8 @@ theorem subst_proof₁ (x y z s : ℝ) (hxyz : x + y + z = 0) :
   · rw [div_mul_eq_mul_div, le_div_iff₀' zero_lt_32]
     exact subst_wlog h' hxyz
   rcases (mul_nonneg_of_three x y z).resolve_left h' with h | h
-  · convert this y z x _ h using 2 <;> linarith
-  · convert this z x y _ h using 2 <;> linarith
+  · convert! this y z x _ h using 2 <;> linarith
+  · convert! this z x y _ h using 2 <;> linarith
 
 theorem proof₁ {a b c : ℝ} :
     |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤

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 :
@@ -112,7 +112,7 @@ theorem Polynomial.isPeriodicPt_eval_two {P : Polynomial ℤ} {t : ℤ}
     -- They must have opposite sign, so that P^{k + 1}(t) - P^k(t) = P^{k + 2}(t) - P^{k + 1}(t).
     rcases Int.natAbs_eq_natAbs_iff.1 (Habs n n.succ) with hn' | hn'
     · apply (hn _).elim
-      convert hn' <;> simp only [Function.iterate_succ_apply']
+      convert! hn' <;> simp only [Function.iterate_succ_apply']
     -- We deduce P^{k + 2}(t) = P^k(t) and hence P(P(t)) = t.
     · rw [neg_sub, sub_right_inj] at hn'
       simp only [Function.iterate_succ_apply'] at hn'

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/Imo2010Q5.lean

@@ -79,7 +79,7 @@ lemma push {B : Fin 6 → ℕ} {i : Fin 6} (rB : Reachable B) (hi : i < 5) :
     Reachable (B - single i (B i) + single (i + 1) (2 * B i)) := by
   obtain hc | hc := (B i).eq_zero_or_pos
   · rwa [hc, mul_zero, single_zero, single_zero, add_zero, tsub_zero]
-  · convert (rB.move1 hi hc).push hi using 1
+  · convert! (rB.move1 hi hc).push hi using 1
     ext k; simp only [add_apply, sub_apply]
     rcases eq_or_ne k i with rfl | hk
     · simp_rw [single_eq_same, tsub_self, single_succ]
@@ -92,29 +92,29 @@ termination_by B i
 /-- `(0, 0, 5, 11, 0, 0)` is reachable. -/
 lemma five_eleven : Reachable (single 2 5 + single 3 11) := by
   have R : Reachable (single 1 3 + single 2 1 + single 3 1 + single 4 1 + single 5 1) := by
-    convert base.push (show 0 < 5 by decide) using 1; decide
+    convert! base.push (show 0 < 5 by decide) using 1; decide
   replace R : Reachable (single 2 7 + single 3 1 + single 4 1 + single 5 1) := by
-    convert R.push (show 1 < 5 by decide) using 1; decide
+    convert! R.push (show 1 < 5 by decide) using 1; decide
   replace R : Reachable (single 2 7 + single 4 3 + single 5 1) := by
-    convert R.push (show 3 < 5 by decide) using 1; decide
+    convert! R.push (show 3 < 5 by decide) using 1; decide
   replace R : Reachable (single 2 7 + single 5 7) := by
-    convert R.push (show 4 < 5 by decide) using 1; decide
+    convert! R.push (show 4 < 5 by decide) using 1; decide
   replace R : Reachable (single 2 6 + single 3 2 + single 5 7) := by
-    convert R.move1 (show 2 < 5 by decide) (by decide) using 1; decide
+    convert! R.move1 (show 2 < 5 by decide) (by decide) using 1; decide
   replace R : Reachable (single 2 6 + single 3 1 + single 4 2 + single 5 7) := by
-    convert R.move1 (show 3 < 5 by decide) (by decide) using 1; decide
+    convert! R.move1 (show 3 < 5 by decide) (by decide) using 1; decide
   replace R : Reachable (single 2 6 + single 3 1 + single 5 11) := by
-    convert R.push (show 4 < 5 by decide) using 1; decide
+    convert! R.push (show 4 < 5 by decide) using 1; decide
   replace R : Reachable (single 2 6 + single 4 11) := by
-    convert R.move2 (show 3 < 4 by decide) (by decide) using 1; decide
-  convert R.move2 (show 2 < 4 by decide) (by decide) using 1; decide
+    convert! R.move2 (show 3 < 4 by decide) (by decide) using 1; decide
+  convert! R.move2 (show 2 < 4 by decide) (by decide) using 1; decide
 
 /-- Decrement $B_i$ and double $B_{i+1}$, assuming $B_{i+2} = 0$, by doing `push, move2`. -/
 lemma double {B : Fin 6 → ℕ} {i : Fin 6}
     (rB : Reachable B) (hi : i < 4) (pB : 0 < B i) (zB : B (i + 2) = 0) :
     Reachable (B + single (i + 1) (B (i + 1)) - single i 1) := by
-  convert (rB.push (show i + 1 < 5 by grind)).move2 hi (by
-    rw [add_apply, sub_apply, single_succ]; grind)
+  convert!
+    (rB.push (show i + 1 < 5 by grind)).move2 hi (by rw [add_apply, sub_apply, single_succ]; grind)
   ext k; simp only [comp_apply, add_apply, sub_apply]
   have (j : Fin 6) : j + 1 + 1 = j + 2 := by grind
   rcases eq_or_ne k i with rfl | hk
@@ -132,7 +132,7 @@ lemma doubles {B : Fin 6 → ℕ} {i : Fin 6} (rB : Reachable B) (hi : i < 4) (z
     Reachable (update (B - single i (B i)) (i + 1) (B (i + 1) * 2 ^ B i)) := by
   obtain hc | hc := (B i).eq_zero_or_pos
   · rwa [hc, single_zero, tsub_zero, pow_zero, mul_one, update_eq_self]
-  · convert (rB.double hi hc zB).doubles hi (by
+  · convert! (rB.double hi hc zB).doubles hi (by
       rw [sub_apply, add_apply, single_eq_of_ne (by simp), zB, zero_add, zero_tsub]) using 1
     ext k
     simp_rw [sub_apply, add_apply, single_eq_same, single_succ, single_succ', add_zero, tsub_zero,
@@ -149,9 +149,9 @@ termination_by B i
 lemma exp {B : Fin 6 → ℕ} {i : Fin 6}
     (rB : Reachable B) (hi : i < 4) (pB : 0 < B i) (zB : B (i + 1) = 0) (zB' : B (i + 2) = 0) :
     Reachable (B - single i (B i) + single (i + 1) (2 ^ B i)) := by
-  convert (rB.move1 (show i < 5 by grind) pB).doubles hi (by
+  convert! (rB.move1 (show i < 5 by grind) pB).doubles hi (by
     rw [add_apply, sub_apply, zB', single_eq_of_ne (by simp), tsub_zero,
-      single_eq_of_ne (by simp), zero_add]) using 1
+        single_eq_of_ne (by simp), zero_add]) using 1
   simp_rw [add_apply, sub_apply, single_eq_same, single_succ, single_succ', zB, zero_tsub, zero_add,
     add_zero, ← pow_succ', Nat.sub_add_cancel pB]
   ext k; simp only [add_apply, sub_apply]
@@ -167,7 +167,7 @@ lemma exp_mid {k n : ℕ} (h : Reachable (single 2 (k + 1) + single 3 n)) (hn :
     Reachable (single 2 k + single 3 (2 ^ n)) := by
   have md := h.exp (show 3 < 4 by decide) (by simp [hn])
     (by simp [add_apply, single_eq_of_ne]) (by simp [add_apply, single_eq_of_ne])
-  convert md.move2 (show 2 < 4 by decide) (by
+  convert! md.move2 (show 2 < 4 by decide) (by
     simp only [add_apply, sub_apply, single_eq_same]
     iterate 3 rw [single_eq_of_ne (by decide)]
     simp) using 1
@@ -192,7 +192,7 @@ lemma reduce {m n : ℕ} (h : Reachable (single 3 n)) (hmn : m ≤ n) : Reachabl
   | base => exact h
   | succ k _ ih =>
     apply ih
-    convert h.move2 (show 3 < 4 by decide) k.succ_pos
+    convert! h.move2 (show 3 < 4 by decide) k.succ_pos
     ext i; simp only [sub_apply, comp_apply]
     rcases eq_or_ne i 3 with rfl | i3
     · rw [swap_apply_of_ne_of_ne (by decide) (by decide)]
@@ -231,7 +231,7 @@ theorem result : Reachable (single 5 (2010 ^ 2010 ^ 2010)) := by
   -- See https://github.com/leanprover/lean4/issues/11713
   set m : ℕ := 2010
   have hm : m = 2010 := by rfl
-  convert ((quarter_target hm).push (show 3 < 5 by decide)).push (show 4 < 5 by decide)
+  convert! ((quarter_target hm).push (show 3 < 5 by decide)).push (show 4 < 5 by decide)
   simp only [single_eq_same, tsub_self, Fin.reduceAdd, zero_add, single_inj]
   rw [← mul_assoc, show 2 * 2 = 4 by rfl, mul_comm, Nat.div_mul_cancel]
   trans 2010 ^ 2