Bump mathlib

LeanAPAP.lean

@@ -44,4 +44,3 @@ import LeanAPAP.Prereqs.LpNorm.Weighted
 import LeanAPAP.Prereqs.MarcinkiewiczZygmund
 import LeanAPAP.Prereqs.Multinomial
 import LeanAPAP.Prereqs.Rudin
-import LeanAPAP.Prereqs.WideDiag

LeanAPAP/FiniteField/Basic.lean

@@ -43,7 +43,7 @@ lemma global_dichotomy (hA : A.Nonempty) (hγC : γ ≤ C.card / card G) (hγ :
       abs_mul, abs_of_nonneg, mul_div_cancel_left₀] <;> positivity
   · rw [lpNorm_mu hp''.symm.one_le hC, hp''.symm.coe.inv_sub_one, NNReal.coe_natCast, ← mul_rpow]
     rw [le_div_iff, mul_comm] at hγC
-    refine' rpow_le_rpow_of_nonpos _ hγC (neg_nonpos.2 _)
+    refine rpow_le_rpow_of_nonpos ?_ hγC (neg_nonpos.2 ?_)
     all_goals positivity
   · simp_rw [Nat.cast_mul, Nat.cast_two, p]
     rw [wlpNorm_const_right, mul_assoc, mul_left_comm, NNReal.coe_inv, inv_rpow, rpow_neg]
@@ -55,7 +55,7 @@ lemma global_dichotomy (hA : A.Nonempty) (hγC : γ ≤ C.card / card G) (hγ :
     push_cast
     norm_num
     rw [← neg_mul, rpow_mul, one_div, rpow_inv_le_iff_of_pos]
-    refine' (rpow_le_rpow_of_exponent_ge hγ hγ₁ $ neg_le_neg $
+    exact (rpow_le_rpow_of_exponent_ge hγ hγ₁ $ neg_le_neg $
       inv_le_inv_of_le (curlog_pos hγ hγ₁) $ Nat.le_ceil _).trans $
         (rpow_neg_inv_curlog_le hγ.le hγ₁).trans $ exp_one_lt_d9.le.trans $ by norm_num
     all_goals positivity
@@ -79,7 +79,7 @@ lemma di_in_ff (hε₀ : 0 < ε) (hε₁ : ε < 1) (hαA : α ≤ A.card / card
           (1 + ε / 32) * α ≤ ‖𝟭_[ℝ] A * μ V'‖_[⊤] := by
   obtain rfl | hA := A.eq_empty_or_nonempty
   · stop
-    refine' ⟨⊤, univ, _⟩
+    refine ⟨⊤, univ, _⟩
     rw [AffineSubspace.direction_top]
     simp only [AffineSubspace.top_coe, coe_univ, eq_self_iff_true, finrank_top, tsub_self,
       Nat.cast_zero, indicate_empty, zero_mul, lpNorm_zero, true_and_iff,

LeanAPAP/Mathlib/Algebra/BigOperators/Pi.lean

@@ -16,8 +16,7 @@ lemma filter_piFinset_card_of_mem [∀ a, DecidableEq (δ a)] (t : ∀ a, Finset
   have : (t' a).card = 1 := by simp [t']
   have h₁ : ∏ b in univ.erase a, (t b).card = ∏ b, (t' b).card := by
     rw [← prod_erase (f := fun b ↦ (t' b).card) univ this]
-    refine' Finset.prod_congr rfl _
-    intro b hb
+    refine Finset.prod_congr rfl fun b hb ↦ ?_
     simp only [mem_erase, Ne, mem_univ, and_true_iff] at hb
     simp only [dif_neg (Ne.symm hb), t']
   have h₂ : ∏ b, (t' b).card = ∏ b, ∑ i in t' b, 1 := by simp
@@ -26,14 +25,14 @@ lemma filter_piFinset_card_of_mem [∀ a, DecidableEq (δ a)] (t : ∀ a, Finset
   congr 1
   ext f
   simp only [mem_filter, mem_piFinset, t']
-  refine' ⟨_, fun h ↦ _⟩
+  refine ⟨?_, fun h ↦ ?_⟩
   · rintro ⟨hf, rfl⟩ b
     split_ifs with h₁
     · cases h₁
       simp
     · exact hf _
   have : f a = x := by simpa using h a
-  refine' ⟨fun b ↦ _, this⟩
+  refine ⟨fun b ↦ ?_, this⟩
   obtain rfl | hab := eq_or_ne a b
   · rwa [this]
   · simpa [dif_neg hab] using h b

LeanAPAP/Mathlib/Algebra/Group/AddChar.lean

@@ -71,7 +71,7 @@ lemma sum_eq_ite (ψ : AddChar G R) : ∑ a, ψ a = if ψ = 0 then ↑(card G) e
   split_ifs with h
   · simp [h, card_univ]
   obtain ⟨x, hx⟩ := ne_one_iff.1 h
-  refine' eq_zero_of_mul_eq_self_left hx _
+  refine eq_zero_of_mul_eq_self_left hx ?_
   rw [Finset.mul_sum]
   exact Fintype.sum_equiv (Equiv.addLeft x) _ _ fun y ↦ (map_add_eq_mul ..).symm
 

LeanAPAP/Physics/DRC.lean

@@ -23,7 +23,7 @@ private lemma lemma_0 (p : ℕ) (B₁ B₂ A : Finset G) (f : G → ℝ) :
     @sum_comm _ _ (Fin p → G), sum_dconv_mul, dconv_apply_sub, Fintype.sum_pow, map_indicate]
   congr with b₁
   congr with b₂
-  refine' Fintype.sum_equiv (Equiv.neg $ Fin p → G) _ _ fun s ↦ _
+  refine Fintype.sum_equiv (Equiv.neg $ Fin p → G) _ _ fun s ↦ ?_
   rw [←smul_mul_assoc, ←smul_mul_smul, card_smul_mu_apply, card_smul_mu_apply, indicate_inter_apply,
     indicate_inter_apply, mul_mul_mul_comm, prod_mul_distrib]
   simp [c, indicate_inf_apply, ←translate_indicate, sub_eq_add_neg, mul_assoc, add_comm]

LeanAPAP/Physics/Unbalancing.lean

@@ -30,7 +30,7 @@ lemma pow_inner_nonneg' {f : G → ℂ} (hf : f = g ○ g) (hν : (↑) ∘ ν =
     simp only [mem_filter, mem_univ, true_and_iff]
     rintro _ _ rfl
     rfl
-  refine' (sum_congr rfl fun _ _ ↦ sum_congr rfl $ this _).trans _
+  refine (sum_congr rfl fun _ _ ↦ sum_congr rfl $ this _).trans ?_
   simp_rw [dconv_apply_sub, sum_fiberwise, ←univ_product_univ, sum_product]
   simp only [sum_pow', sum_mul_sum, map_mul, starRingEnd_self_apply, Fintype.piFinset_univ,
     ←Complex.conj_mul', sum_product, map_sum, map_prod,
@@ -84,7 +84,7 @@ private lemma unbalancing' (p : ℕ) (hp : 5 ≤ p) (hp₁ : Odd p) (hε₀ : 0
       _ = _ := ?_
     rw [wlpNorm_pow_eq_sum hp₁.pos.ne']
     dsimp
-    refine' sum_congr rfl fun i _ ↦ _
+    refine sum_congr rfl fun i _ ↦ ?_
     rw [←abs_of_nonneg ((Nat.Odd.sub_odd hp₁ odd_one).pow_nonneg $ f _), abs_pow,
       pow_sub_one_mul hp₁.pos.ne']
     simp [l2Inner_eq_sum, ←sum_add_distrib, ←mul_add, ←pow_sub_one_mul hp₁.pos.ne' (f _),

LeanAPAP/Prereqs/AddChar/Basic.lean

@@ -28,7 +28,7 @@ lemma expect_eq_ite (ψ : AddChar G R) : 𝔼 a, ψ a = if ψ = 0 then 1 else 0
   split_ifs with h
   · simp [h, card_univ, univ_nonempty]
   obtain ⟨x, hx⟩ := ne_one_iff.1 h
-  refine' eq_zero_of_mul_eq_self_left hx _
+  refine eq_zero_of_mul_eq_self_left hx ?_
   rw [Finset.mul_expect]
   exact Fintype.expect_equiv (Equiv.addLeft x) _ _ fun y ↦ (map_add_eq_mul _ _ _).symm
 

LeanAPAP/Prereqs/AddChar/Defs.lean

@@ -20,7 +20,7 @@ variable [Finite G] [NormedField R]
   (ψ.toMonoidHom.isOfFinOrder $ isOfFinOrder_of_finite _).norm_eq_one
 
 @[simp] lemma coe_ne_zero (ψ : AddChar G R) : (ψ : G → R) ≠ 0 :=
-  Function.ne_iff.2 ⟨0, fun h ↦ by simpa only [h, Pi.zero_apply, zero_ne_one] using map_zero_eq_one ψ⟩
+  ne_iff.2 ⟨0, fun h ↦ by simpa only [h, Pi.zero_apply, zero_ne_one] using map_zero_eq_one ψ⟩
 
 end NormedField
 
@@ -56,7 +56,7 @@ protected def directSum (ψ : ∀ i, AddChar (π i) R) : AddChar (⨁ i, π i) R
 
 lemma directSum_injective :
     Injective (AddChar.directSum : (∀ i, AddChar (π i) R) → AddChar (⨁ i, π i) R) := by
-  refine' AddChar.toAddMonoidHomEquiv.symm.injective.comp $ DirectSum.toAddMonoid_injective.comp _
+  refine AddChar.toAddMonoidHomEquiv.symm.injective.comp $ DirectSum.toAddMonoid_injective.comp ?_
   rintro ψ χ h
   simpa [Function.funext_iff] using h
 

LeanAPAP/Prereqs/AddChar/PontryaginDuality.lean

@@ -128,8 +128,8 @@ def circleEquivComplex [Finite α] : AddChar α circle ≃+ AddChar α ℂ where
 /-- `ZMod n` is (noncanonically) isomorphic to its group of characters. -/
 def zmodAddEquiv (hn : n ≠ 0) : ZMod n ≃+ AddChar (ZMod n) ℂ := by
   haveI : NeZero n := ⟨hn⟩
-  refine' AddEquiv.ofBijective
-    (circleEquivComplex.toAddMonoidHom.comp $ AddChar.toAddMonoidHom $ zmodHom n) _
+  refine AddEquiv.ofBijective
+    (circleEquivComplex.toAddMonoidHom.comp $ AddChar.toAddMonoidHom $ zmodHom n) ?_
   rw [Fintype.bijective_iff_injective_and_card, card_eq]
   exact ⟨circleEquivComplex.injective.comp $ zmod_injective hn, rfl⟩
 
@@ -154,7 +154,7 @@ variable {α}
 lemma complexBasis_apply (ψ : AddChar α ℂ) : complexBasis α ψ = ψ := by rw [coe_complexBasis]
 
 lemma exists_apply_ne_zero : (∃ ψ : AddChar α ℂ, ψ a ≠ 1) ↔ a ≠ 0 := by
-  refine' ⟨_, fun ha ↦ _⟩
+  refine ⟨?_, fun ha ↦ ?_⟩
   · rintro ⟨ψ, hψ⟩ rfl
     exact hψ ψ.map_zero_eq_one
   classical

LeanAPAP/Prereqs/Chang.lean

@@ -21,7 +21,7 @@ lemma α_nonneg (f : G → ℂ) : 0 ≤ α f := by unfold α; positivity
 lemma α_pos (hf : f ≠ 0) : 0 < α f := by unfold α; positivity
 
 lemma α_le_one (f : G → ℂ) : α f ≤ 1 := by
-  refine' div_le_one_of_le (div_le_of_nonneg_of_le_mul _ _ _) _
+  refine div_le_one_of_le (div_le_of_nonneg_of_le_mul ?_ ?_ ?_) ?_
   any_goals positivity
   rw [l1Norm_eq_sum, l2Norm_sq_eq_sum]
   exact sq_sum_le_card_mul_sum_sq
@@ -149,20 +149,20 @@ lemma chang (hf : f ≠ 0) (hη : 0 < η) :
   have : 0 < α f := α_pos hf
   set β := ⌈curlog (α f)⌉₊
   have hβ : 0 < β := Nat.ceil_pos.2 (curlog_pos (α_pos hf) $ α_le_one _)
-  refine' le_of_pow_le_pow_left hβ.ne' zero_le' $ Nat.cast_le.1 $ le_of_mul_le_mul_right _
+  refine le_of_pow_le_pow_left hβ.ne' zero_le' $ Nat.cast_le.1 $ le_of_mul_le_mul_right ?_
     (by positivity : 0 < ↑Δ.card ^ β * (η ^ (2 * β) * α f))
   push_cast
   rw [←mul_assoc, ←pow_add, ←two_mul]
-  refine' ((spec_hoelder hη.le hΔη hβ.ne').trans $ hΔ.boringEnergy_le _).trans _
-  refine' le_trans _ $ mul_le_mul_of_nonneg_right (pow_le_pow_left _ (Nat.le_ceil _) _) _
+  refine ((spec_hoelder hη.le hΔη hβ.ne').trans $ hΔ.boringEnergy_le _).trans ?_
+  refine le_trans ?_ $ mul_le_mul_of_nonneg_right (pow_le_pow_left ?_ (Nat.le_ceil _) _) ?_
   rw [mul_right_comm, div_pow, mul_pow, mul_pow, exp_one_pow, ←pow_mul, mul_div_assoc]
   calc
     _ = (changConst * Δ.card * β) ^ β := by ring
     _ ≤ (changConst * Δ.card * β) ^ β * (α f * exp β) := ?_
     _ ≤ (changConst * Δ.card * β) ^ β * ((η / η) ^ (2 * β) * α f * exp β) := by
         rw [div_self hη.ne', one_pow, one_mul]
     _ = _ := by ring
-  refine' le_mul_of_one_le_right (by positivity) _
+  refine le_mul_of_one_le_right (by positivity) ?_
   rw [←inv_pos_le_iff_one_le_mul']
   exact inv_le_exp_curlog.trans $ exp_monotone $ Nat.le_ceil _
   all_goals positivity

LeanAPAP/Prereqs/Convolution/Compact.lean

@@ -502,9 +502,9 @@ lemma support_iterNConv_subset (f : α → β) : ∀ n, support (f ∗^ₙ n) 
 --   · simp [apply_ite card, eq_comm]
 --   simp_rw [iterNConv_succ, nconv_eq_expect_sub', ih, indicate_apply, boole_mul, expect_ite, filter_univ_mem,
 --     expect_const_zero, add_zero, ←Nat.cast_expect, ←Finset.card_sigma, Nat.cast_inj]
---   refine' Finset.card_bij (fun f _ ↦ Fin.cons f.1 f.2) _ _ _
+--   refine Finset.card_bij (fun f _ ↦ Fin.cons f.1 f.2) _ _ _
 --   · simp only [Fin.expect_cons, eq_sub_iff_add_eq', mem_sigma, mem_filter, mem_piFinset, and_imp]
---     refine' fun bf hb hf ha ↦ ⟨Fin.cases _ _, ha⟩
+--     refine fun bf hb hf ha ↦ ⟨Fin.cases _ _, ha⟩
 --     · exact hb
 --     · simpa only [Fin.cons_succ]
 --   · simp only [Sigma.ext_iff, Fin.cons_eq_cons, heq_iff_eq, imp_self, imp_true_iff, forall_const,

LeanAPAP/Prereqs/Convolution/Discrete/Defs.lean

@@ -164,9 +164,8 @@ lemma mul_smul_conv_comm [Monoid γ] [DistribMulAction γ β] [IsScalarTower γ
 lemma conv_assoc (f g h : α → β) : f ∗ g ∗ h = f ∗ (g ∗ h) := by
   ext a
   simp only [sum_mul, mul_sum, conv_apply, sum_sigma']
-  refine' sum_nbij' (fun ⟨(_b, c), (d, e)⟩ ↦ ⟨(d, e + c), (e, c)⟩)
-    (fun ⟨(b, _c), (d, e)⟩ ↦ ⟨(b + d, e), (b, d)⟩) _ _ _ _ _ <;>
-    aesop (add simp [add_assoc, mul_assoc])
+  apply sum_nbij' (fun ⟨(_b, c), (d, e)⟩ ↦ ⟨(d, e + c), (e, c)⟩)
+    (fun ⟨(b, _c), (d, e)⟩ ↦ ⟨(b + d, e), (b, d)⟩) <;> aesop (add simp [add_assoc, mul_assoc])
 
 lemma conv_right_comm (f g h : α → β) : f ∗ g ∗ h = f ∗ h ∗ g := by
   rw [conv_assoc, conv_assoc, conv_comm g]
@@ -200,7 +199,7 @@ lemma map_dconv (f g : α → ℝ≥0) (a : α) : (↑((f ○ g) a) : ℝ) = ((
     Function.comp_apply]
 
 lemma conv_eq_sum_sub (f g : α → β) (a : α) : (f ∗ g) a = ∑ t, f (a - t) * g t := by
-  rw [conv_apply]; refine' sum_nbij' Prod.snd (fun b ↦ (a - b, b)) _ _ _ _ _ <;> aesop
+  rw [conv_apply]; apply sum_nbij' Prod.snd (fun b ↦ (a - b, b)) <;> aesop
 
 lemma dconv_eq_sum_sub (f g : α → β) (a : α) : (f ○ g) a = ∑ t, f (a - t) * conj (g (-t)) := by
   simp [←conv_conjneg, conv_eq_sum_sub]

LeanAPAP/Prereqs/Convolution/Order.lean

@@ -22,7 +22,7 @@ variable [StrictOrderedCommSemiring β] [StarRing β] [StarOrderedRing β] {f g
 
 --TODO: Those can probably be generalised to `OrderedCommSemiring` but we don't really care
 @[simp] lemma support_conv (hf : 0 ≤ f) (hg : 0 ≤ g) : support (f ∗ g) = support f + support g := by
-  refine' (support_conv_subset _ _).antisymm _
+  refine (support_conv_subset _ _).antisymm ?_
   rintro _ ⟨a, ha, b, hb, rfl⟩
   rw [mem_support, conv_apply_add]
   exact ne_of_gt $ sum_pos' (fun c _ ↦ mul_nonneg (hf _) $ hg _) ⟨0, mem_univ _,
@@ -36,7 +36,7 @@ lemma conv_pos (hf : 0 < f) (hg : 0 < g) : 0 < f ∗ g := by
   rw [Pi.lt_def] at hf hg ⊢
   obtain ⟨hf, a, ha⟩ := hf
   obtain ⟨hg, b, hb⟩ := hg
-  refine' ⟨conv_nonneg hf hg, a + b, _⟩
+  refine ⟨conv_nonneg hf hg, a + b, ?_⟩
   rw [conv_apply_add]
   exact sum_pos' (fun c _ ↦ mul_nonneg (hf _) $ hg _) ⟨0, by simpa using mul_pos ha hb⟩
 

LeanAPAP/Prereqs/Convolution/ThreeAP.lean

@@ -21,7 +21,7 @@ lemma ThreeAPFree.l2Inner_mu_conv_mu_mu_two_smul_mu (hG : Odd (card G))
     Finset.sum_eq_zero, Finset.sum_eq_zero, add_zero, add_zero, pow_succ', mul_inv,
     mul_inv_cancel_left₀]
   · exact Nat.cast_ne_zero.2 hs'.card_pos.ne'
-  · refine' fun i hi ↦ not_ne_iff.1 fun h ↦ (mem_offDiag.1 hi).2.2 _
+  · refine fun i hi ↦ not_ne_iff.1 fun h ↦ (mem_offDiag.1 hi).2.2 ?_
     simp_rw [mul_ne_zero_iff, ←mem_support, support_mu, mem_coe, mem_image, two_smul] at h
     obtain ⟨b, hb, hab⟩ := h.2
     obtain rfl := hs h.1.1 hb h.1.2 hab.symm

LeanAPAP/Prereqs/Curlog.lean

@@ -51,11 +51,11 @@ lemma rpow_neg_inv_curlog_le (hx : 0 ≤ x) (hx' : x ≤ 1) : x ^ (-(curlog x)
   · simp
   have : -1 / log (1 / x) ≤ -1 / curlog x := by
     rw [neg_div, neg_div, neg_le_neg_iff]
-    refine' one_div_le_one_div_of_le _ (log_one_div_le_curlog hx.le)
-    refine' log_pos _
+    refine one_div_le_one_div_of_le ?_ (log_one_div_le_curlog hx.le)
+    refine log_pos ?_
     rwa [lt_div_iff hx, one_mul]
   rw [←one_div, ←neg_div]
-  refine' (rpow_le_rpow_of_exponent_ge hx hx'.le this).trans _
+  refine (rpow_le_rpow_of_exponent_ge hx hx'.le this).trans ?_
   rw [one_div, log_inv, rpow_def_of_pos hx, neg_div_neg_eq, mul_one_div, div_self]
   exact log_ne_zero_of_pos_of_ne_one hx hx'.ne
 

LeanAPAP/Prereqs/Energy.lean

@@ -34,7 +34,7 @@ lemma boringEnergy_eq (n : ℕ) (s : Finset G) : boringEnergy n s = ∑ x, (𝟭
   rw [←Finset.sum_fiberwise _ fun f : Fin n → G ↦ ∑ i, f i]
   congr with x
   rw [indicate_iterConv_apply, sq, ←nsmul_eq_mul, ←sum_const]
-  refine' sum_congr rfl fun f hf ↦ _
+  refine sum_congr rfl fun f hf ↦ ?_
   simp_rw [(mem_filter.1 hf).2, eq_comm]
 
 @[simp] lemma boringEnergy_zero (s : Finset G) : boringEnergy 0 s = 1 := by simp [boringEnergy]

LeanAPAP/Prereqs/FourierTransform/Compact.lean

@@ -174,7 +174,7 @@ lemma nlpNorm_nconv_le_nlpNorm_ndconv (hn₀ : n ≠ 0) (hn : Even n) (f : α 
     map_mul, Fintype.sum_pow, Fintype.sum_mul_sum]
   sorry
   -- simp only [@expect_comm _ _ α, ←mul_expect, prod_mul_prod_comm]
-  -- refine' (norm_expect_le _ _).trans_eq (Complex.ofReal_injective _)
+  -- refine (norm_expect_le _ _).trans_eq (Complex.ofReal_injective _)
   -- simp only [norm_mul, norm_prod, RCLike.norm_conj, ←pow_mul]
   -- push_cast
   -- have : ∀ f g : Fin n → AddChar α ℂ, 0 ≤ ∑ a, ∏ i, conj (f i a) * g i a := by
@@ -191,7 +191,7 @@ lemma nlpNorm_nconv_le_nlpNorm_ndconv (hn₀ : n ≠ 0) (hn : Even n) (f : α 
   --   ext
   --   rw [←Complex.eq_coe_norm_of_nonneg (this _ _)]
   -- simp only [@expect_comm _ _ α, mul_expect, map_prod, map_mul, RCLike.conj_conj, ←prod_mul_distrib]
-  -- refine' expect_congr rfl fun x _ ↦ expect_congr rfl fun a _ ↦ prod_congr rfl fun i _ ↦ _
+  -- refine expect_congr rfl fun x _ ↦ expect_congr rfl fun a _ ↦ prod_congr rfl fun i _ ↦ _
   -- ring
 
 --TODO: Can we unify with `nlpNorm_nconv_le_nlpNorm_ndconv`?

LeanAPAP/Prereqs/FourierTransform/Discrete.lean

@@ -88,7 +88,7 @@ lemma dft_conj (f : α → ℂ) (ψ : AddChar α ℂ) : dft (conj f) ψ = conj (
 
 lemma dft_conjneg_apply (f : α → ℂ) (ψ : AddChar α ℂ) : dft (conjneg f) ψ = conj (dft f ψ) := by
   simp only [dft_apply, l2Inner_eq_sum, conjneg_apply, map_sum, map_mul, RCLike.conj_conj]
-  refine' Fintype.sum_equiv (Equiv.neg α) _ _ fun i ↦ _
+  refine Fintype.sum_equiv (Equiv.neg α) _ _ fun i ↦ ?_
   simp only [Equiv.neg_apply, ←inv_apply_eq_conj, ←inv_apply', inv_apply]
 
 @[simp]
@@ -166,7 +166,7 @@ lemma lpNorm_conv_le_lpNorm_dconv (hn₀ : n ≠ 0) (hn : Even n) (f : α → 
 --   simp_rw [pow_mul', ←norm_pow _ n, Complex.ofReal_pow, ←Complex.conj_mul', map_pow, map_sum,
 --     map_mul, Fintype.sum_pow, Fintype.sum_mul_sum]
 --   simp only [@sum_comm _ _ α, ←mul_sum, prod_mul_prod_comm]
---   refine' (norm_sum_le _ _).trans_eq (Complex.ofReal_injective _)
+--   refine (norm_sum_le _ _).trans_eq (Complex.ofReal_injective _)
 --   simp only [norm_mul, norm_prod, RCLike.norm_conj, ←pow_mul]
 --   push_cast
 --   have : ∀ f g : Fin n → AddChar α ℂ, 0 ≤ ∑ a, ∏ i, conj (f i a) * g i a := by
@@ -183,12 +183,11 @@ lemma lpNorm_conv_le_lpNorm_dconv (hn₀ : n ≠ 0) (hn : Even n) (f : α → 
 --     ext
 --     rw [←Complex.eq_coe_norm_of_nonneg (this _ _)]
 --   simp only [@sum_comm _ _ α, mul_sum, map_prod, map_mul, RCLike.conj_conj, ←prod_mul_distrib]
---   refine' sum_congr rfl fun x _ ↦ sum_congr rfl fun a _ ↦ prod_congr rfl fun i _ ↦ _
+--   refine sum_congr rfl fun x _ ↦ sum_congr rfl fun a _ ↦ prod_congr rfl fun i _ ↦ _
 --   ring
 
 --TODO: Can we unify with `lpNorm_conv_le_lpNorm_dconv`?
 lemma lpNorm_conv_le_lpNorm_dconv' (hn₀ : n ≠ 0) (hn : Even n) (f : α → ℝ) :
     ‖f ∗ f‖_[n] ≤ ‖f ○ f‖_[n] := by
   simpa only [←Complex.coe_comp_conv, ←Complex.coe_comp_dconv, Complex.lpNorm_coe_comp] using
     lpNorm_conv_le_lpNorm_dconv hn₀ hn ((↑) ∘ f)
-

LeanAPAP/Prereqs/Function/Indicator/Defs.lean

@@ -177,7 +177,7 @@ variable [Nontrivial β] [CharZero β] {a : α}
 
 @[simp] lemma mu_apply_eq_zero : μ_[β] s a = 0 ↔ a ∉ s := by
   simp only [mu_apply, mul_boole, ite_eq_right_iff, inv_eq_zero, Nat.cast_eq_zero, card_eq_zero]
-  refine' imp_congr_right fun ha ↦ _
+  refine imp_congr_right fun ha ↦ ?_
   simp only [ne_empty_of_mem ha]
 
 lemma mu_apply_ne_zero : μ_[β] s a ≠ 0 ↔ a ∈ s := mu_apply_eq_zero.not_left

LeanAPAP/Prereqs/LpNorm/Compact.lean

@@ -495,7 +495,7 @@ lemma nlpNorm_rpow_indicate (hp : p ≠ 0) (s : Finset α) : ‖𝟭_[β] s‖
   all_goals positivity
 
 lemma nlpNorm_indicate (hp : p ≠ 0) (s : Finset α) : ‖𝟭_[β] s‖ₙ_[p] = s.dens ^ (p⁻¹ : ℝ) := by
-  refine' (eq_rpow_inv _ _ _).2 (nlpNorm_rpow_indicate _ _) <;> positivity
+  refine (eq_rpow_inv ?_ ?_ ?_).2 (nlpNorm_rpow_indicate ?_ _) <;> positivity
 
 lemma nlpNorm_pow_indicate {p : ℕ} (hp : p ≠ 0) (s : Finset α) :
     ‖𝟭_[β] s‖ₙ_[p] ^ (p : ℝ) = s.dens := by

LeanAPAP/Prereqs/LpNorm/Discrete/Basic.lean

@@ -88,7 +88,7 @@ lemma lpNorm_rpow_indicate (hp : p ≠ 0) (s : Finset α) : ‖𝟭_[β] s‖_[p
     sum_boole, this, zero_rpow, filter_mem_eq_inter]
 
 lemma lpNorm_indicate (hp : p ≠ 0) (s : Finset α) : ‖𝟭_[β] s‖_[p] = s.card ^ (p⁻¹ : ℝ) := by
-  refine' (eq_rpow_inv _ _ _).2 (lpNorm_rpow_indicate _ _) <;> positivity
+  refine (eq_rpow_inv ?_ ?_ ?_).2 (lpNorm_rpow_indicate ?_ _) <;> positivity
 
 lemma lpNorm_pow_indicate {p : ℕ} (hp : p ≠ 0) (s : Finset α) :
     ‖𝟭_[β] s‖_[p] ^ (p : ℝ) = s.card := by

LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean

@@ -536,8 +536,8 @@ lemma lpNorm_prod_le {s : Finset ι} (hs : s.Nonempty) {p : ι → ℝ≥0} (hp
     simp [←hpq]
   simp_rw [prod_cons]
   rw [sum_cons, ←inv_inv (∑ _ ∈ _, _ : ℝ≥0)] at hpq
-  refine'
-    (lpNorm_mul_le (hp _) (inv_ne_zero (sum_pos (fun _ _ ↦ _) hs).ne') _ hpq _ _).trans
+  refine
+    (lpNorm_mul_le (hp _) (inv_ne_zero (sum_pos (fun _ _ ↦ ?_) hs).ne') _ hpq _ _).trans
       (mul_le_mul_of_nonneg_left (ih hs _ (inv_inv _).symm) lpNorm_nonneg)
   exact pos_iff_ne_zero.2 (inv_ne_zero $ hp _)
 

LeanAPAP/Prereqs/LpNorm/Weighted.lean

@@ -80,8 +80,8 @@ section one_le
 lemma wlpNorm_add_le (hp : 1 ≤ p) (w : ι → ℝ≥0) (f g : ∀ i, α i) :
     ‖f + g‖_[p, w] ≤ ‖f‖_[p, w] + ‖g‖_[p, w] := by
   unfold wlpNorm
-  refine' (lpNorm_add_le (by exact_mod_cast hp) _ _).trans'
-    (lpNorm_mono (fun i ↦ by dsimp; positivity) fun i ↦ _)
+  refine (lpNorm_add_le (by exact_mod_cast hp) _ _).trans'
+    (lpNorm_mono (fun i ↦ by dsimp; positivity) fun i ↦ ?_)
   dsimp
   rw [←smul_add]
   exact smul_le_smul_of_nonneg_left (norm_add_le _ _) (zero_le _)