Merge branch 'master' into port/CategoryTheory.Pi.Basic

Mathlib.lean

@@ -136,6 +136,7 @@ import Mathlib.Algebra.Order.Group.WithTop
 import Mathlib.Algebra.Order.Hom.Basic
 import Mathlib.Algebra.Order.Hom.Monoid
 import Mathlib.Algebra.Order.Invertible
+import Mathlib.Algebra.Order.Kleene
 import Mathlib.Algebra.Order.LatticeGroup
 import Mathlib.Algebra.Order.Module
 import Mathlib.Algebra.Order.Monoid.Basic
@@ -232,6 +233,7 @@ import Mathlib.CategoryTheory.Functor.Const
 import Mathlib.CategoryTheory.Functor.Default
 import Mathlib.CategoryTheory.Functor.FullyFaithful
 import Mathlib.CategoryTheory.Functor.Functorial
+import Mathlib.CategoryTheory.Functor.InvIsos
 import Mathlib.CategoryTheory.Iso
 import Mathlib.CategoryTheory.NatIso
 import Mathlib.CategoryTheory.NatTrans
@@ -301,6 +303,7 @@ import Mathlib.Data.DList.Basic
 import Mathlib.Data.DList.Instances
 import Mathlib.Data.Dfinsupp.Basic
 import Mathlib.Data.Dfinsupp.Interval
+import Mathlib.Data.Dfinsupp.Lex
 import Mathlib.Data.Dfinsupp.NeLocus
 import Mathlib.Data.Dfinsupp.Order
 import Mathlib.Data.ENat.Basic
@@ -766,6 +769,7 @@ import Mathlib.Lean.Message
 import Mathlib.Lean.Meta
 import Mathlib.Lean.Meta.Simp
 import Mathlib.LinearAlgebra.AffineSpace.Basic
+import Mathlib.LinearAlgebra.Basic
 import Mathlib.LinearAlgebra.GeneralLinearGroup
 import Mathlib.Logic.Basic
 import Mathlib.Logic.Denumerable
@@ -928,6 +932,7 @@ import Mathlib.SetTheory.Cardinal.Basic
 import Mathlib.SetTheory.Cardinal.Finite
 import Mathlib.SetTheory.Cardinal.SchroederBernstein
 import Mathlib.SetTheory.Lists
+import Mathlib.SetTheory.Ordinal.Basic
 import Mathlib.Tactic.Abel
 import Mathlib.Tactic.Alias
 import Mathlib.Tactic.ApplyFun
@@ -944,6 +949,7 @@ import Mathlib.Tactic.ClearExcept
 import Mathlib.Tactic.Clear_
 import Mathlib.Tactic.Coe
 import Mathlib.Tactic.Constructor
+import Mathlib.Tactic.Continuity
 import Mathlib.Tactic.Contrapose
 import Mathlib.Tactic.Conv
 import Mathlib.Tactic.Convert
@@ -1035,8 +1041,10 @@ import Mathlib.Tactic.Zify.Attr
 import Mathlib.Testing.SlimCheck.Gen
 import Mathlib.Testing.SlimCheck.Sampleable
 import Mathlib.Testing.SlimCheck.Testable
+import Mathlib.Topology.Alexandroff
 import Mathlib.Topology.Algebra.ConstMulAction
 import Mathlib.Topology.Algebra.Constructions
+import Mathlib.Topology.Algebra.MulAction
 import Mathlib.Topology.Algebra.Order.Archimedean
 import Mathlib.Topology.Algebra.Order.Compact
 import Mathlib.Topology.Algebra.Order.ExtendFrom
@@ -1061,6 +1069,7 @@ import Mathlib.Topology.Connected
 import Mathlib.Topology.Constructions
 import Mathlib.Topology.ContinuousFunction.Basic
 import Mathlib.Topology.ContinuousFunction.CocompactMap
+import Mathlib.Topology.ContinuousFunction.T0Sierpinski
 import Mathlib.Topology.ContinuousOn
 import Mathlib.Topology.DenseEmbedding
 import Mathlib.Topology.DiscreteQuotient
@@ -1077,6 +1086,7 @@ import Mathlib.Topology.LocallyConstant.Basic
 import Mathlib.Topology.LocallyFinite
 import Mathlib.Topology.Maps
 import Mathlib.Topology.NhdsSet
+import Mathlib.Topology.NoetherianSpace
 import Mathlib.Topology.OmegaCompletePartialOrder
 import Mathlib.Topology.Order
 import Mathlib.Topology.Order.Basic
@@ -1090,13 +1100,15 @@ import Mathlib.Topology.Perfect
 import Mathlib.Topology.Separation
 import Mathlib.Topology.Sets.Closeds
 import Mathlib.Topology.Sets.Opens
+import Mathlib.Topology.Sets.Order
 import Mathlib.Topology.ShrinkingLemma
 import Mathlib.Topology.Sober
 import Mathlib.Topology.Spectral.Hom
 import Mathlib.Topology.StoneCech
 import Mathlib.Topology.SubsetProperties
 import Mathlib.Topology.Support
 import Mathlib.Topology.UniformSpace.AbsoluteValue
+import Mathlib.Topology.UniformSpace.AbstractCompletion
 import Mathlib.Topology.UniformSpace.Basic
 import Mathlib.Topology.UniformSpace.Cauchy
 import Mathlib.Topology.UniformSpace.CompleteSeparated

Mathlib/Algebra/FreeMonoid/Basic.lean

@@ -226,8 +226,7 @@ lemma prodAux_eq : ∀ l : List M, FreeMonoid.prodAux l = l.prod
 /-- Equivalence between maps `α → M` and monoid homomorphisms `FreeMonoid α →* M`. -/
 @[to_additive "Equivalence between maps `α → A` and additive monoid homomorphisms
 `FreeAddMonoid α →+ A`."]
-def lift : (α → M) ≃ (FreeMonoid α →* M)
-    where
+def lift : (α → M) ≃ (FreeMonoid α →* M) where
   toFun f :=
   { toFun := fun l ↦ prodAux ((toList l).map f)
     map_one' := rfl
@@ -238,6 +237,11 @@ def lift : (α → M) ≃ (FreeMonoid α →* M)
 #align free_monoid.lift FreeMonoid.lift
 #align free_add_monoid.lift FreeAddMonoid.lift
 
+-- porting note: new
+@[to_additive (attr := simp)]
+theorem lift_ofList (f : α → M) (l : List α) : lift f (ofList l) = (l.map f).prod :=
+prodAux_eq _
+
 @[to_additive (attr := simp)]
 theorem lift_symm_apply (f : FreeMonoid α →* M) : lift.symm f = f ∘ of := rfl
 #align free_monoid.lift_symm_apply FreeMonoid.lift_symm_apply

Mathlib/Algebra/Hom/Freiman.lean

@@ -127,10 +127,9 @@ see also Algebra.Hom.Group for similar -/
 @[to_additive (attr := coe)
     " Turn an element of a type `F` satisfying `AddFreimanHomClass F A β n` into an actual
     `AddFreimanHom`. This is declared as the default coercion from `F` to `AddFreimanHom A β n`."]
-def _root_.FreimanHomClass.toFreimanHom [FreimanHomClass F A β n] (f : F) :
-    A →*[n] β where
-   toFun := FunLike.coe f
-   map_prod_eq_map_prod' := FreimanHomClass.map_prod_eq_map_prod' f
+def _root_.FreimanHomClass.toFreimanHom [FreimanHomClass F A β n] (f : F) : A →*[n] β where
+  toFun := FunLike.coe f
+  map_prod_eq_map_prod' := FreimanHomClass.map_prod_eq_map_prod' f
 
 /-- Any type satisfying `SMulHomClass` can be cast into `MulActionHom` via
   `SMulHomClass.toMulActionHom`. -/
@@ -149,8 +148,7 @@ theorem map_prod_eq_map_prod [FreimanHomClass F A β n] (f : F) {s t : Multiset
 
 @[to_additive]
 theorem map_mul_map_eq_map_mul_map [FreimanHomClass F A β 2] (f : F) (ha : a ∈ A) (hb : b ∈ A)
-    (hc : c ∈ A) (hd : d ∈ A) (h : a * b = c * d) : f a * f b = f c * f d :=
-  by
+    (hc : c ∈ A) (hd : d ∈ A) (h : a * b = c * d) : f a * f b = f c * f d := by
   simp_rw [← prod_pair] at h⊢
   refine' map_prod_eq_map_prod f _ _ (card_pair _ _) (card_pair _ _) h <;> simp [ha, hb, hc, hd]
 #align map_mul_map_eq_map_mul_map map_mul_map_eq_map_mul_map
@@ -159,18 +157,17 @@ theorem map_mul_map_eq_map_mul_map [FreimanHomClass F A β 2] (f : F) (ha : a 
 namespace FreimanHom
 
 @[to_additive]
-instance funLike : FunLike (A →*[n] β) α fun _ => β
-    where
+instance funLike : FunLike (A →*[n] β) α fun _ => β where
   coe := toFun
   coe_injective' f g h := by cases f; cases g; congr
 #align freiman_hom.fun_like FreimanHom.funLike
 #align add_freiman_hom.fun_like AddFreimanHom.funLike
 
-@[to_additive]
-instance freiman_hom_class : FreimanHomClass (A →*[n] β) A β n
-    where map_prod_eq_map_prod' := map_prod_eq_map_prod'
-#align freiman_hom.freiman_hom_class FreimanHom.freiman_hom_class
-#align add_freiman_hom.freiman_hom_class AddFreimanHom.freiman_hom_class
+@[to_additive addFreimanHomClass]
+instance freimanHomClass : FreimanHomClass (A →*[n] β) A β n where
+  map_prod_eq_map_prod' := map_prod_eq_map_prod'
+#align freiman_hom.freiman_hom_class FreimanHom.freimanHomClass
+#align add_freiman_hom.freiman_hom_class AddFreimanHom.addFreimanHomClass
 
 -- porting note: not helpful in lean4
 -- /-- Helper instance for when there's too many metavariables to apply `fun_like.has_coe_to_fun`
@@ -185,10 +182,10 @@ initialize_simps_projections FreimanHom (toFun → apply)
 initialize_simps_projections AddFreimanHom (toFun → apply)
 
 @[to_additive (attr := simp)]
-theorem to_fun_eq_coe (f : A →*[n] β) : f.toFun = f :=
+theorem toFun_eq_coe (f : A →*[n] β) : f.toFun = f :=
   rfl
-#align freiman_hom.to_fun_eq_coe FreimanHom.to_fun_eq_coe
-#align add_freiman_hom.to_fun_eq_coe AddFreimanHom.to_fun_eq_coe
+#align freiman_hom.to_fun_eq_coe FreimanHom.toFun_eq_coe
+#align add_freiman_hom.to_fun_eq_coe AddFreimanHom.toFun_eq_coe
 
 @[to_additive (attr := ext)]
 theorem ext ⦃f g : A →*[n] β⦄ (h : ∀ x, f x = g x) : f = g :=
@@ -497,8 +494,7 @@ variable [CommMonoid α] [CancelCommMonoid β] {A : Set α} {m n : ℕ}
 theorem map_prod_eq_map_prod_of_le [FreimanHomClass F A β n] (f : F) {s t : Multiset α}
     (hsA : ∀ x ∈ s, x ∈ A) (htA : ∀ x ∈ t, x ∈ A)
     (hs : Multiset.card s = m) (ht : Multiset.card t = m)
-    (hst : s.prod = t.prod) (h : m ≤ n) : (s.map f).prod = (t.map f).prod :=
-  by
+    (hst : s.prod = t.prod) (h : m ≤ n) : (s.map f).prod = (t.map f).prod := by
   obtain rfl | hm := m.eq_zero_or_pos
   · rw [card_eq_zero] at hs ht
     rw [hs, ht]
@@ -544,10 +540,9 @@ def FreimanHom.toFreimanHom (h : m ≤ n) (f : A →*[n] β) : A →*[m] β wher
       "An additive `n`-Freiman homomorphism is
       also an additive `m`-Freiman homomorphism for any `m ≤ n`."]
 theorem FreimanHom.FreimanHomClass_of_le [FreimanHomClass F A β n] (h : m ≤ n) :
-    FreimanHomClass F A β m :=
-  {
-    map_prod_eq_map_prod' := fun f _ _ hsA htA hs ht hst =>
-      map_prod_eq_map_prod_of_le f hsA htA hs ht hst h }
+    FreimanHomClass F A β m where
+  map_prod_eq_map_prod' f _ _ hsA htA hs ht hst :=
+    map_prod_eq_map_prod_of_le f hsA htA hs ht hst h
 #align freiman_hom.freiman_hom_class_of_le FreimanHom.FreimanHomClass_of_le
 #align add_freiman_hom.add_freiman_hom_class_of_le AddFreimanHom.addFreimanHomClass_of_le
 

Mathlib/Algebra/Module/Submodule/Lattice.lean

@@ -118,14 +118,13 @@ theorem exists_mem_ne_zero_of_ne_bot {p : Submodule R M} (h : p ≠ ⊥) : ∃ b
 
 /-- The bottom submodule is linearly equivalent to punit as an `R`-module. -/
 @[simps]
-def botEquivPUnit : (⊥ : Submodule R M) ≃ₗ[R] PUnit
-    where
+def botEquivPUnit : (⊥ : Submodule R M) ≃ₗ[R] PUnit where
   toFun _ := PUnit.unit
   invFun _ := 0
-  map_add' := fun _ _ ↦ rfl
-  map_smul' := fun _ _ ↦ rfl
-  left_inv := by intro ; simp only [eq_iff_true_of_subsingleton]
-  right_inv := fun _ ↦ rfl
+  map_add' _ _ := rfl
+  map_smul' _ _ := rfl
+  left_inv _ := Subsingleton.elim _ _
+  right_inv _ := rfl
 #align submodule.bot_equiv_punit Submodule.botEquivPUnit
 
 theorem eq_bot_of_subsingleton (p : Submodule R M) [Subsingleton p] : p = ⊥ := by
@@ -183,14 +182,13 @@ theorem eq_top_iff' {p : Submodule R M} : p = ⊤ ↔ ∀ x, x ∈ p :=
 
 This is the module version of `AddSubmonoid.topEquiv`. -/
 @[simps]
-def topEquiv : (⊤ : Submodule R M) ≃ₗ[R] M
-    where
+def topEquiv : (⊤ : Submodule R M) ≃ₗ[R] M where
   toFun x := x
   invFun x := ⟨x, mem_top⟩
-  map_add' := fun _ _ ↦ rfl
-  map_smul' := fun _ _ ↦ rfl
-  left_inv := fun _ ↦ rfl
-  right_inv := fun _ ↦ rfl
+  map_add' _ _ := rfl
+  map_smul' _ _ := rfl
+  left_inv _ := rfl
+  right_inv _ := rfl
 #align submodule.top_equiv Submodule.topEquiv
 
 instance : InfSet (Submodule R M) :=
@@ -200,10 +198,10 @@ instance : InfSet (Submodule R M) :=
       add_mem' := by simp (config := { contextual := true }) [add_mem]
       smul_mem' := by simp (config := { contextual := true }) [smul_mem] }⟩
 
-private theorem Inf_le' {S : Set (Submodule R M)} {p} : p ∈ S → infₛ S ≤ p :=
+private theorem infₛ_le' {S : Set (Submodule R M)} {p} : p ∈ S → infₛ S ≤ p :=
   Set.binterᵢ_subset_of_mem
 
-private theorem le_Inf' {S : Set (Submodule R M)} {p} : (∀ q ∈ S, p ≤ q) → p ≤ infₛ S :=
+private theorem le_infₛ' {S : Set (Submodule R M)} {p} : (∀ q ∈ S, p ≤ q) → p ≤ infₛ S :=
   Set.subset_interᵢ₂
 
 instance : HasInf (Submodule R M) :=
@@ -217,17 +215,17 @@ instance : CompleteLattice (Submodule R M) :=
   { (inferInstance : OrderTop (Submodule R M)),
     (inferInstance : OrderBot (Submodule R M)) with
     sup := fun a b ↦ infₛ { x | a ≤ x ∧ b ≤ x }
-    le_sup_left := fun _ _ ↦ le_Inf' fun _ ⟨h, _⟩ ↦ h
-    le_sup_right := fun _ _ ↦ le_Inf' fun _ ⟨_, h⟩ ↦ h
-    sup_le := fun _ _ _ h₁ h₂ ↦ Inf_le' ⟨h₁, h₂⟩
+    le_sup_left := fun _ _ ↦ le_infₛ' fun _ ⟨h, _⟩ ↦ h
+    le_sup_right := fun _ _ ↦ le_infₛ' fun _ ⟨_, h⟩ ↦ h
+    sup_le := fun _ _ _ h₁ h₂ ↦ infₛ_le' ⟨h₁, h₂⟩
     inf := (· ⊓ ·)
     le_inf := fun _ _ _ ↦ Set.subset_inter
     inf_le_left := fun _ _ ↦ Set.inter_subset_left _ _
     inf_le_right := fun _ _ ↦ Set.inter_subset_right _ _
-    le_supₛ := fun _ _ hs ↦ le_Inf' fun _ hq ↦ by exact hq _ hs
-    supₛ_le := fun _ _ hs ↦ Inf_le' hs
-    le_infₛ := fun _ _ ↦ le_Inf'
-    infₛ_le := fun _ _ ↦ Inf_le' }
+    le_supₛ := fun _ _ hs ↦ le_infₛ' fun _ hq ↦ by exact hq _ hs
+    supₛ_le := fun _ _ hs ↦ infₛ_le' hs
+    le_infₛ := fun _ _ ↦ le_infₛ'
+    infₛ_le := fun _ _ ↦ infₛ_le' }
 
 @[simp]
 theorem inf_coe : ↑(p ⊓ q) = (p ∩ q : Set M) :=
@@ -309,12 +307,12 @@ theorem sum_mem_supᵢ {ι : Type _} [Fintype ι] {f : ι → M} {p : ι → Sub
   sum_mem fun i _ ↦ mem_supᵢ_of_mem i (h i)
 #align submodule.sum_mem_supr Submodule.sum_mem_supᵢ
 
-theorem sum_mem_bsupr {ι : Type _} {s : Finset ι} {f : ι → M} {p : ι → Submodule R M}
+theorem sum_mem_bsupᵢ {ι : Type _} {s : Finset ι} {f : ι → M} {p : ι → Submodule R M}
     (h : ∀ i ∈ s, f i ∈ p i) : (∑ i in s, f i) ∈ ⨆ i ∈ s, p i :=
   sum_mem fun i hi ↦ mem_supᵢ_of_mem i <| mem_supᵢ_of_mem hi (h i hi)
-#align submodule.sum_mem_bsupr Submodule.sum_mem_bsupr
+#align submodule.sum_mem_bsupr Submodule.sum_mem_bsupᵢ
 
-/-! Note that `Submodule.mem_supr` is provided in `LinearAlgebra/Span.lean`. -/
+/-! Note that `Submodule.mem_supᵢ` is provided in `LinearAlgebra/Span.lean`. -/
 
 
 theorem mem_supₛ_of_mem {S : Set (Submodule R M)} {s : Submodule R M} (hs : s ∈ S) :
@@ -344,12 +342,11 @@ section NatSubmodule
 
 -- Porting note: `S.toNatSubmodule` doesn't work. I used `AddSubmonoid.toNatSubmodule S` instead.
 /-- An additive submonoid is equivalent to a ℕ-submodule. -/
-def AddSubmonoid.toNatSubmodule : AddSubmonoid M ≃o Submodule ℕ M
-    where
+def AddSubmonoid.toNatSubmodule : AddSubmonoid M ≃o Submodule ℕ M where
   toFun S := { S with smul_mem' := fun r s hs ↦ show r • s ∈ S from nsmul_mem hs _ }
   invFun := Submodule.toAddSubmonoid
-  left_inv := fun _ ↦ rfl
-  right_inv := fun _ ↦ rfl
+  left_inv _ := rfl
+  right_inv _ := rfl
   map_rel_iff' := Iff.rfl
 #align add_submonoid.to_nat_submodule AddSubmonoid.toNatSubmodule
 
@@ -387,12 +384,11 @@ variable [AddCommGroup M]
 
 -- Porting note: `S.toIntSubmodule` doesn't work. I used `AddSubgroup.toIntSubmodule S` instead.
 /-- An additive subgroup is equivalent to a ℤ-submodule. -/
-def AddSubgroup.toIntSubmodule : AddSubgroup M ≃o Submodule ℤ M
-    where
+def AddSubgroup.toIntSubmodule : AddSubgroup M ≃o Submodule ℤ M where
   toFun S := { S with smul_mem' := fun _ _ hs ↦ S.zsmul_mem hs _ }
   invFun := Submodule.toAddSubgroup
-  left_inv := fun _ ↦ rfl
-  right_inv := fun _ ↦ rfl
+  left_inv _ := rfl
+  right_inv _ := rfl
   map_rel_iff' := Iff.rfl
 #align add_subgroup.to_int_submodule AddSubgroup.toIntSubmodule