bump to v4.34.0-rc2

FormalBook/Ch20/CauchyAMGM.lean

@@ -92,7 +92,7 @@ lemma cauchy_amgm_backward_iter (d n : ℕ) (hn : 0 < n) (h : CauchyAMGM (n + d)
   | zero => exact h
   | succ d ihd =>
     apply ihd
-    exact cauchy_amgm_backward (n + d) (by omega) (by convert h using 1)
+    exact cauchy_amgm_backward (n + d) (by omega) (by rw [add_assoc]; exact h)
 
 /-- **Cauchy's AM-GM inequality**: for n ≥ 1 and nonneg reals, ∏aᵢ ≤ (∑aᵢ/n)ⁿ.
     Proved by forward doubling P(2)→P(4)→...→P(2^k), then backward P(2^k)→...→P(n). -/

FormalBook/Ch20/ErdosGallai.lean

@@ -26,9 +26,11 @@ theorem hm_le_gm (a b : ℝ) (ha : 0 < a) (hb : 0 < b) :
   rw [div_le_iff₀ hab]
   have hsqa := Real.mul_self_sqrt ha.le
   have hsqb := Real.mul_self_sqrt hb.le
-  have hsqab : Real.sqrt (a * b) * Real.sqrt (a * b) = a * b := Real.mul_self_sqrt (mul_nonneg ha.le hb.le)
+  have hsqab : Real.sqrt (a * b) * Real.sqrt (a * b) = a * b :=
+    Real.mul_self_sqrt (mul_nonneg ha.le hb.le)
   have hsqab' : Real.sqrt a * Real.sqrt b = Real.sqrt (a * b) := (Real.sqrt_mul ha.le b).symm
-  nlinarith [sq_nonneg (Real.sqrt a - Real.sqrt b), Real.sqrt_nonneg a, Real.sqrt_nonneg b, Real.sqrt_nonneg (a * b)]
+  nlinarith [sq_nonneg (Real.sqrt a - Real.sqrt b), Real.sqrt_nonneg a, Real.sqrt_nonneg b,
+    Real.sqrt_nonneg (a * b)]
 
 /-- Product identity:
     ∏ᵢ (αᵢ - 1) · ∏ᵢ (αᵢ + 1) = ∏ᵢ (αᵢ² - 1). -/
@@ -43,15 +45,18 @@ theorem prod_sub_one_mul_prod_add_one {n : ℕ} (α : Fin n → ℝ) :
 
 /-- f'(1) for our polynomial, up to sign:
     f'(1) = -2 · ∏ᵢ(αᵢ - 1) · ∏ⱼ(βⱼ + 1). -/
+@[nolint defsWithUnderscore]
 noncomputable def erdos_gallai_deriv_at_one {m n : ℕ} (α : Fin m → ℝ) (β : Fin n → ℝ) : ℝ :=
   -2 * (∏ i, (α i - 1)) * (∏ j, (β j + 1))
 
 /-- f'(-1) for our polynomial:
     f'(-1) = 2 · ∏ᵢ(αᵢ + 1) · ∏ⱼ(βⱼ - 1). -/
+@[nolint defsWithUnderscore]
 noncomputable def erdos_gallai_deriv_at_neg_one {m n : ℕ} (α : Fin m → ℝ) (β : Fin n → ℝ) : ℝ :=
   2 * (∏ i, (α i + 1)) * (∏ j, (β j - 1))
 
 /-- C² = ∏ᵢ(αᵢ² - 1) · ∏ⱼ(βⱼ² - 1). -/
+@[nolint defsWithUnderscore]
 noncomputable def erdos_gallai_C_sq {m n : ℕ} (α : Fin m → ℝ) (β : Fin n → ℝ) : ℝ :=
   (∏ i, (α i ^ 2 - 1)) * (∏ j, (β j ^ 2 - 1))
 
@@ -69,6 +74,7 @@ theorem erdos_gallai_deriv_product {m n : ℕ} (α : Fin m → ℝ) (β : Fin n
 
     When f'(1) < 0 and f'(-1) > 0 (normal case), this equals
     2·|f'(1)|·|f'(-1)| / (|f'(1)| + |f'(-1)|), the harmonic mean. -/
+@[nolint defsWithUnderscore]
 noncomputable def erdos_gallai_T {m n : ℕ} (α : Fin m → ℝ) (β : Fin n → ℝ) : ℝ :=
   -2 * (erdos_gallai_deriv_at_one α β) * (erdos_gallai_deriv_at_neg_one α β) /
     (erdos_gallai_deriv_at_one α β - erdos_gallai_deriv_at_neg_one α β)
@@ -78,10 +84,12 @@ noncomputable def erdos_gallai_T {m n : ℕ} (α : Fin m → ℝ) (β : Fin n 
 open MeasureTheory intervalIntegral
 
 /-- f(x) = (1 - x²) · ∏ᵢ (αᵢ - x) · ∏ⱼ (βⱼ + x). -/
+@[nolint defsWithUnderscore]
 noncomputable def erdos_gallai_f {m n : ℕ} (α : Fin m → ℝ) (β : Fin n → ℝ) (x : ℝ) : ℝ :=
   (1 - x ^ 2) * (∏ i, (α i - x)) * (∏ j, (β j + x))
 
 /-- The area A = ∫₋₁¹ f(x) dx. -/
+@[nolint defsWithUnderscore]
 noncomputable def erdos_gallai_area {m n : ℕ} (α : Fin m → ℝ) (β : Fin n → ℝ) : ℝ :=
   ∫ x in (-1 : ℝ)..1, erdos_gallai_f α β x
 
@@ -92,9 +100,9 @@ theorem erdos_gallai_f_continuous {m n : ℕ} (α : Fin m → ℝ) (β : Fin n 
   apply Continuous.mul
   · apply Continuous.mul
     · exact continuous_const.sub (continuous_pow 2)
-    · exact continuous_finset_prod _ fun i _ =>
+    · exact continuous_finsetProd _ fun i _ =>
         continuous_const.sub continuous_id
-  · exact continuous_finset_prod _ fun j _ =>
+  · exact continuous_finsetProd _ fun j _ =>
       continuous_const.add continuous_id
 
 /-- f is interval-integrable on [-1, 1]. -/
@@ -199,10 +207,10 @@ theorem integral_one_sub_sq : ∫ x in (-1:ℝ)..1, (1 - x ^ 2) = 4 / 3 := by
     intro x _
     have h1 := hasDerivAt_id (𝕜 := ℝ) x
     have h3 : HasDerivAt (fun x => x ^ 3 / 3) (x ^ 2) x := by
-      have := (hasDerivAt_pow 3 x).div_const (3 : ℝ)
-      convert this using 1
-      push_cast; ring
-    convert h1.sub h3 using 1
+      have h := (hasDerivAt_pow 3 x).div_const (3 : ℝ)
+      have h_eq : ((3 : ℕ) : ℝ) * x ^ (3 - 1) / 3 = x ^ 2 := by ring
+      rwa [h_eq] at h
+    convert h1.sub h3 using 1 <;> rfl
   have hint : IntervalIntegrable (fun x => (1:ℝ) - x ^ 2) volume (-1) 1 :=
     (continuous_const.sub (continuous_pow 2)).intervalIntegrable _ _
   rw [integral_eq_sub_of_hasDerivAt hderiv hint]

FormalBook/Ch28/BrouwerCovering.lean

@@ -27,7 +27,7 @@ private def acCov : IsCoveringMap (QuotientAddGroup.mk : ℝ → AddCircle (1 :
 private theorem acLoop_lift_eq :
     (⟨fun t => (t : ℝ), continuous_subtype_val⟩ : C(I, ℝ)) =
     acCov.liftPath acLoop.toContinuousMap 0 rfl := by
-  rw [IsCoveringMap.eq_liftPath_iff']
+  rw [acCov.eq_liftPath_iff' rfl]
   exact ⟨by ext; simp [acLoop], by simp⟩
 
 private theorem not_sc_addCircle : ¬ SimplyConnectedSpace (AddCircle (1 : ℝ)) := by
@@ -39,7 +39,7 @@ private theorem not_sc_addCircle : ¬ SimplyConnectedSpace (AddCircle (1 : ℝ))
   have h2 : (acCov.liftPath (Path.refl acBase).toContinuousMap 0 rfl) 1 = (0 : ℝ) := by
     have : (ContinuousMap.const I (0 : ℝ)) =
         acCov.liftPath (Path.refl acBase).toContinuousMap 0 rfl := by
-      rw [IsCoveringMap.eq_liftPath_iff']
+      rw [acCov.eq_liftPath_iff' rfl]
       exact ⟨by ext; simp only [ContinuousMap.const_zero, ContinuousMap.coe_zero,
         Function.comp_apply, Pi.zero_apply, QuotientAddGroup.mk_zero, Path.coe_toContinuousMap,
         Path.refl_apply], by simp only [ContinuousMap.const_zero, ContinuousMap.zero_apply]⟩

FormalBook/Ch28/SpernerBrouwer.lean

@@ -139,7 +139,7 @@ private theorem stdSimplex2_eq : stdSimplex2 = stdSimplex ℝ (Fin 3) := by
 
 /-- The standard 2-simplex is compact. -/
 private theorem stdSimplex2_isCompact : IsCompact stdSimplex2 := by
-  rw [stdSimplex2_eq]; exact isCompact_stdSimplex _
+  rw [stdSimplex2_eq]; exact isCompact_stdSimplex ℝ (Fin 3)
 
 /-- The Sperner coloring is well-defined: if v ∈ Δ² and f(v) ≠ v with f(v) ∈ Δ²,
     then some coordinate strictly decreases. -/
@@ -200,14 +200,15 @@ private instance subdivVertDecEq (k : ℕ) : DecidableEq (SubdivVert k) :=
   inferInstanceAs (DecidableEq { abc : Fin 3 → ℕ // ∑ i, abc i = k })
 
 /-- The coordinate map: send a subdivision vertex to its barycentric point in Δ². -/
+@[nolint unusedArguments]
 private noncomputable def subdivCoord (k : ℕ) (hk : 0 < k) (v : SubdivVert k) : Fin 3 → ℝ :=
   fun i => (v.1 i : ℝ) / (k : ℝ)
 
 private theorem subdivCoord_mem (k : ℕ) (hk : 0 < k) (v : SubdivVert k) :
     subdivCoord k hk v ∈ stdSimplex2 := by
   constructor
   · intro i; apply div_nonneg (Nat.cast_nonneg _) (Nat.cast_nonneg _)
-  · simp only [subdivCoord, div_add_div_same, ← Finset.sum_div]
+  · simp only [subdivCoord, ← Finset.sum_div]
     rw [show (∑ i : Fin 3, (v.1 i : ℝ)) = (∑ i : Fin 3, v.1 i : ℕ) from by push_cast; rfl]
     rw [v.2]; field_simp
 
@@ -430,6 +431,7 @@ private lemma odd_transitions (n : ℕ) (s : Fin (n + 1) → Bool)
   rw [h0, hlast] at h
   simpa using h
 
+@[nolint unusedArguments]
 private theorem subdivSperner_odd_sum
     (f : (Fin 3 → ℝ) → (Fin 3 → ℝ)) (hfS : ∀ x ∈ stdSimplex2, f x ∈ stdSimplex2)
     (hne : ∀ x ∈ stdSimplex2, f x ≠ x)
@@ -520,6 +522,7 @@ private theorem subdivSperner_odd_sum
 
 /-- From a rainbow triangle in the subdivision, extract three vertices with the
     desired geometric properties. -/
+@[nolint unusedArguments]
 private theorem rainbow_triangle_gives_vertices
     (f : (Fin 3 → ℝ) → (Fin 3 → ℝ)) (hfS : ∀ x ∈ stdSimplex2, f x ∈ stdSimplex2)
     (hne : ∀ x ∈ stdSimplex2, f x ≠ x)