Bump mathlib

.gitignore

@@ -5,6 +5,7 @@
 /build
 /leanpkg.path
 /lake-packages
+/.lake
 
 decls.pickle
 decls.yaml

LeanAPAP.lean

@@ -11,10 +11,10 @@ import LeanAPAP.Mathlib.Algebra.Group.Basic
 import LeanAPAP.Mathlib.Algebra.Group.Equiv.Basic
 import LeanAPAP.Mathlib.Algebra.Group.Hom.Defs
 import LeanAPAP.Mathlib.Algebra.Group.Hom.Instances
-import LeanAPAP.Mathlib.Algebra.Group.TypeTags
 import LeanAPAP.Mathlib.Algebra.GroupPower.Basic
 import LeanAPAP.Mathlib.Algebra.GroupPower.Hom
 import LeanAPAP.Mathlib.Algebra.GroupPower.Order
+import LeanAPAP.Mathlib.Algebra.Group.TypeTags
 import LeanAPAP.Mathlib.Algebra.Module.Basic
 import LeanAPAP.Mathlib.Algebra.Order.LatticeGroup
 import LeanAPAP.Mathlib.Algebra.Order.Ring.Canonical
@@ -58,7 +58,7 @@ import LeanAPAP.Mathlib.Data.Nat.Order.Basic
 import LeanAPAP.Mathlib.Data.Nat.Parity
 import LeanAPAP.Mathlib.Data.Pi.Algebra
 import LeanAPAP.Mathlib.Data.Rat.Order
-import LeanAPAP.Mathlib.Data.Real.Basic
+import LeanAPAP.Mathlib.Data.Real.Archimedean
 import LeanAPAP.Mathlib.Data.Real.ENNReal
 import LeanAPAP.Mathlib.Data.Real.NNReal
 import LeanAPAP.Mathlib.Data.Real.Sqrt
@@ -70,14 +70,12 @@ import LeanAPAP.Mathlib.GroupTheory.Submonoid.Basic
 import LeanAPAP.Mathlib.GroupTheory.Submonoid.Operations
 import LeanAPAP.Mathlib.LinearAlgebra.FiniteDimensional
 import LeanAPAP.Mathlib.LinearAlgebra.Ray
-import LeanAPAP.Mathlib.Logic.Basic
 import LeanAPAP.Mathlib.NumberTheory.LegendreSymbol.AddChar.Basic
 import LeanAPAP.Mathlib.NumberTheory.LegendreSymbol.AddChar.Duality
 import LeanAPAP.Mathlib.Order.ConditionallyCompleteLattice.Finset
 import LeanAPAP.Mathlib.Order.Disjoint
 import LeanAPAP.Mathlib.Order.Heyting.Basic
 import LeanAPAP.Mathlib.Order.Partition.Finpartition
-import LeanAPAP.Mathlib.Tactic.Binop
 import LeanAPAP.Mathlib.Tactic.Positivity
 import LeanAPAP.Physics.AlmostPeriodicity
 import LeanAPAP.Physics.DRC

LeanAPAP/Mathlib/Algebra/GroupPower/Order.lean

@@ -26,7 +26,8 @@ end StrictOrderedSemiring
 section LinearOrderedSemiring
 variable [LinearOrderedSemiring α] {a b : α} {n : ℕ}
 
-lemma pow_eq_one_iff_of_nonneg (ha : 0 ≤ a) (hn : n ≠ 0) : a ^ n = 1 ↔ a = 1 := by
+-- TODO: Golf `pow_eq_one_iff_of_nonneg`
+example (ha : 0 ≤ a) (hn : n ≠ 0) : a ^ n = 1 ↔ a = 1 := by
   simp only [le_antisymm_iff, pow_le_one_iff_of_nonneg ha hn, one_le_pow_iff_of_nonneg ha hn]
 
 lemma pow_le_pow_iff_left (ha : 0 ≤ a) (hb : 0 ≤ b) (hn : n ≠ 0) : a ^ n ≤ b ^ n ↔ a ≤ b :=

LeanAPAP/Mathlib/Analysis/Complex/Circle.lean

@@ -59,6 +59,7 @@ lemma e_eq_one : e r = 1 ↔ ∃ n : ℤ, r = n := by
   simp [e_apply, exp_eq_one, mul_comm (2 * π), pi_ne_zero]
 
 lemma e_inj : e r = e s ↔ r ≡ s [PMOD 1] := by
-  simp [AddCommGroup.ModEq, ←e_eq_one, div_eq_one, map_sub_eq_div, eq_comm]
+  simp [AddCommGroup.ModEq, ←e_eq_one, div_eq_one, map_sub_eq_div, eq_comm (b := 1),
+    eq_comm (a := e r)]
 
 end Circle

LeanAPAP/Mathlib/Data/Fintype/Basic.lean

@@ -8,7 +8,8 @@ namespace Finset
 lemma filter_mem_univ (s : Finset α) : univ.filter (· ∈ s) = s := by simp [filter_mem_eq_inter]
 
 -- @[simp] --TODO: Unsimp `finset.univ_unique`
-lemma singleton_eq_univ [Subsingleton α] (a : α) : ({a} : Finset α) = univ := by ext; simp
+lemma singleton_eq_univ [Subsingleton α] (a : α) : ({a} : Finset α) = univ := by
+  ext b; simp [Subsingleton.elim a b]
 
 end Finset
 

LeanAPAP/Mathlib/Data/Real/Archimedean.lean

@@ -0,0 +1,3 @@
+import Mathlib.Data.Real.Archimedean
+
+attribute [simp] Real.ciSup_empty

LeanAPAP/Mathlib/NumberTheory/LegendreSymbol/AddChar/Basic.lean

@@ -14,14 +14,8 @@ Rename
 * `map_zero_one` → `map_zero_eq_one`
 * `map_nsmul_pow` → `map_nsmul_eq_pow`
 * `coe_toFun_apply` → whatever is better, maybe change to `ψ.toMonoidNom a = ψ (of_mul a)`.
-
-Kill the evil instance `AddChar.MonoidHomClass`. It creates a diamond for
-`FunLike (AddChar G R) _ _`.
 -/
 
---TODO: This instance is evil
-attribute [-instance] AddChar.monoidHomClass
-
 open Finset hiding card
 open Fintype (card)
 open Function
@@ -35,26 +29,37 @@ variable [AddMonoid G] [AddMonoid H] [CommMonoid R] {ψ : AddChar G R}
 
 instance : AddCommMonoid (AddChar G R) := Additive.addCommMonoid
 
-instance instFunLike : FunLike (AddChar G R) G fun _ ↦ R where
+-- Replace ad-hoc `FunLike` instance
+example : FunLike (AddChar G R) G fun _ ↦ R where
   coe := (⇑)
   coe_injective' ψ χ h := by obtain ⟨⟨_, _⟩, _⟩ := ψ; congr
 
+attribute [simp, norm_cast] mul_apply one_apply
+
 -- TODO: Replace `AddChar.toMonoidHom`
 /-- Interpret an additive character as a monoid homomorphism. -/
 def toMonoidHom' : AddChar G R ≃ (Multiplicative G →* R) := Equiv.refl _
 
 @[simp, norm_cast]
-lemma coe_toMonoid_hom (ψ : AddChar G R) : ⇑(toMonoidHom' ψ) = ψ ∘ Multiplicative.toAdd := rfl
+lemma coe_toMonoidHom' (ψ : AddChar G R) : ⇑(toMonoidHom' ψ) = ψ ∘ Multiplicative.toAdd := rfl
 
-@[simp, norm_cast] lemma coe_toMonoid_hom_symm (ψ : Multiplicative G →* R) :
+@[simp, norm_cast] lemma coe_toMonoidHom'_symm (ψ : Multiplicative G →* R) :
     ⇑(toMonoidHom'.symm ψ) = ψ ∘ Multiplicative.ofAdd := rfl
 
-@[simp] lemma toMonoid_hom_apply (ψ : AddChar G R) (a : Multiplicative G) :
+@[simp] lemma toMonoidHom'_apply (ψ : AddChar G R) (a : Multiplicative G) :
     toMonoidHom' ψ a = ψ (Multiplicative.toAdd a) := rfl
 
-@[simp] lemma toMonoid_hom_symm_apply (ψ : Multiplicative G →* R) (a : G) :
+@[simp] lemma toMonoidHom'_symm_apply (ψ : Multiplicative G →* R) (a : G) :
     toMonoidHom'.symm ψ a = ψ (Multiplicative.ofAdd a) := rfl
 
+@[simp] lemma toMonoidHom'_zero : toMonoidHom' (0 : AddChar G R) = 1 := rfl
+@[simp] lemma toMonoidHom'_symm_one : toMonoidHom'.symm (1 : Multiplicative G →* R) = 0 := rfl
+
+@[simp] lemma toMonoidHom'_add (ψ φ : AddChar G R) :
+    toMonoidHom' (ψ + φ) = toMonoidHom' ψ * toMonoidHom' φ := rfl
+@[simp] lemma toMonoidHom'_symm_mul (ψ φ : Multiplicative G →* R) :
+  toMonoidHom'.symm (ψ * φ) = toMonoidHom'.symm ψ + toMonoidHom'.symm φ := rfl
+
 /-- Interpret an additive character as a monoid homomorphism. -/
 def toAddMonoidHom : AddChar G R ≃ (G →+ Additive R) := MonoidHom.toAdditive
 
@@ -115,10 +120,11 @@ def compAddMonoidHom (ψ : AddChar H R) (f : G →+ H) : AddChar G R :=
   toMonoidHom'.symm $ ψ.toMonoidHom'.comp $ AddMonoidHom.toMultiplicative f
 
 @[simp] lemma compAddMonoidHom_apply (ψ : AddChar H R) (f : G →+ H) (a : G) :
-    ψ.compAddMonoidHom f a = ψ (f a) := rfl
+    (ψ.compAddMonoidHom f) a = ψ (f a) := rfl
 
 @[simp, norm_cast]
-lemma coe_compAddMonoidHom (ψ : AddChar H R) (f : G →+ H) : ⇑(ψ.compAddMonoidHom f) = ψ ∘ f := rfl
+lemma coe_compAddMonoidHom (ψ : AddChar H R) (f : G →+ H) :
+    (ψ.compAddMonoidHom f) = ψ ∘ f := rfl
 
 lemma compAddMonoidHom_injective_left (f : G →+ H) (hf : Surjective f) :
     Injective fun ψ : AddChar H R ↦ ψ.compAddMonoidHom f := by
@@ -157,7 +163,7 @@ section NormedField
 variable [Finite G] [NormedField R]
 
 @[simp] lemma norm_apply (ψ : AddChar G R) (x : G) : ‖ψ x‖ = 1 :=
-  (ψ.isOfFinOrder $ exists_pow_eq_one _).norm_eq_one
+  (ψ.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_one ψ⟩

LeanAPAP/Mathlib/NumberTheory/LegendreSymbol/AddChar/Duality.lean

@@ -32,9 +32,6 @@ variable [DivisionRing α] {a b c p : α}
 
 end AddCommGroup
 
---TODO: This instance is evil
-attribute [-instance] AddChar.monoidHomClass
-
 noncomputable section
 
 open circle Circle Finset Function Multiplicative
@@ -67,6 +64,7 @@ private def zmodAux (n : ℕ) : AddChar (ZMod n) circle :=
 -- probably an evil lemma
 -- @[simp] lemma zmodAux_apply (n : ℕ) (x : ZMod n) : zmodAux n x = e (x / n) :=
 -- by simp [zmodAux]
+
 lemma zmodAux_injective (hn : n ≠ 0) : Injective (zmodAux n) := by
   replace hn : (n : ℝ) ≠ 0 := Nat.cast_ne_zero.2 hn
   simp [zmodAux, ZMod.lift_injective, CharP.int_cast_eq_zero_iff _ n, e_eq_one, div_eq_iff hn,
@@ -79,12 +77,25 @@ to `e ^ (2 * π * i * x * y / n)`. -/
 def zmod (n : ℕ) (x : ZMod n) : AddChar (ZMod n) circle :=
   (zmodAux n).compAddMonoidHom $ AddMonoidHom.mulLeft x
 
-@[simp] lemma zmod_apply (n : ℕ) (x y : ℤ) : zmod n x y = e (x * y / n) := by
+@[simp] lemma zmod_apply (n : ℕ) (x y : ℤ) :
+    (zmod n x) (y : ZMod n) = e (x * y / n) := by
   simp [zmod, ←Int.cast_mul x y, -Int.cast_mul]
 
+@[simp] lemma zmod_zero (n : ℕ) : zmod n 0 = 1 := by
+  refine FunLike.ext _ _ ?_
+  rw [ZMod.int_cast_surjective.forall]
+  rintro y
+  simpa using zmod_apply n 0 y
+
+@[simp] lemma zmod_add (n : ℕ) : ∀ x y : ZMod n, zmod n (x + y) = zmod n x * zmod n y := by
+  simp only [FunLike.ext_iff, ZMod.int_cast_surjective.forall, ←Int.cast_add, AddChar.mul_apply,
+    zmod_apply]
+  simp [add_mul, add_div]
+
 -- probably an evil lemma
 -- @[simp] lemma zmod_apply (n : ℕ) (x y : ZMod n) : zmod n x y = e (x * y / n) :=
 -- by simp [addChar.zmod, ZMod.coe_mul]
+
 lemma zmod_injective (hn : n ≠ 0) : Injective (zmod n) := by
   simp_rw [Injective, ZMod.int_cast_surjective.forall]
   rintro x y h
@@ -94,22 +105,14 @@ lemma zmod_injective (hn : n ≠ 0) : Injective (zmod n) := by
     CharP.intCast_eq_intCast (ZMod n) n] using (zmod_apply _ _ _).symm.trans $
     (FunLike.congr_fun h ((1 : ℤ) : ZMod n)).trans $ zmod_apply _ _ _
 
-
 @[simp] lemma zmod_inj (hn : n ≠ 0) {x y : ZMod n} : zmod n x = zmod n y ↔ x = y :=
   (zmod_injective hn).eq_iff
 
 def zmodHom (n : ℕ) : AddChar (ZMod n) (AddChar (ZMod n) circle) :=
-  AddChar.toMonoidHom'.symm
-    { toFun := fun x ↦ AddChar.toMonoidHom' (zmod n $ toAdd x)
-      map_one' := FunLike.ext _ _ $ by
-        rw [Multiplicative.forall, ZMod.int_cast_surjective.forall]
-        rintro m
-        simp [zmod]
-      map_mul' := by
-        simp only [Multiplicative.forall, ZMod.int_cast_surjective.forall, FunLike.ext_iff]
-        rintro x y z
-        simp only [toAdd_mul, toAdd_ofAdd, toMonoid_hom_apply, MonoidHom.mul_apply, zmod_apply,
-          ←map_add_mul, ←add_div, ←add_mul, ←Int.cast_add, e_inj] }
+  toMonoidHom'.symm
+    { toFun := fun x ↦ toMonoidHom'.symm (zmod n $ toAdd x)
+      map_one' := by simp; rfl
+      map_mul' := by simp; rintro x y; rfl }
 
 def mkZModAux {ι : Type} [DecidableEq ι] (n : ι → ℕ) (u : ∀ i, ZMod (n i)) :
     AddChar (⨁ i, ZMod (n i)) circle :=
@@ -178,7 +181,7 @@ lemma exists_apply_ne_zero : (∃ ψ : AddChar α ℂ, ψ a ≠ 1) ↔ a ≠ 0 :
   · rintro ⟨ψ, hψ⟩ rfl
     exact hψ ψ.map_zero_one
   classical
-  by_contra' h
+  by_contra! h
   let f : α → ℂ := fun b ↦ if a = b then 1 else 0
   have h₀ := congr_fun ((complexBasis α).sum_repr f) 0
   have h₁ := congr_fun ((complexBasis α).sum_repr f) a