bump to nightly-2023-10-25-06

mathlib commit leanprover-community/mathlib@3365b20

Mathbin/Combinatorics/SetFamily/Shadow.lean

@@ -318,9 +318,9 @@ theorem mem_upShadow_iff_exists_mem_card_add :
 #align finset.mem_up_shadow_iff_exists_mem_card_add Finset.mem_upShadow_iff_exists_mem_card_add
 -/
 
-#print Finset.shadow_image_compl /-
+#print Finset.upShadow_compls /-
 @[simp]
-theorem shadow_image_compl : ((∂ ) 𝒜).image compl = (∂⁺ ) (𝒜.image compl) :=
+theorem upShadow_compls : ((∂ ) 𝒜).image compl = (∂⁺ ) (𝒜.image compl) :=
   by
   ext s
   simp only [mem_image, exists_prop, mem_shadow_iff, mem_up_shadow_iff]
@@ -329,12 +329,12 @@ theorem shadow_image_compl : ((∂ ) 𝒜).image compl = (∂⁺ ) (𝒜.image c
     exact ⟨sᶜ, ⟨s, hs, rfl⟩, a, not_mem_compl.2 ha, compl_erase.symm⟩
   · rintro ⟨_, ⟨s, hs, rfl⟩, a, ha, rfl⟩
     exact ⟨s.erase a, ⟨s, hs, a, not_mem_compl.1 ha, rfl⟩, compl_erase⟩
-#align finset.shadow_image_compl Finset.shadow_image_compl
+#align finset.shadow_image_compl Finset.upShadow_compls
 -/
 
-#print Finset.upShadow_image_compl /-
+#print Finset.shadow_compls /-
 @[simp]
-theorem upShadow_image_compl : ((∂⁺ ) 𝒜).image compl = (∂ ) (𝒜.image compl) :=
+theorem shadow_compls : ((∂⁺ ) 𝒜).image compl = (∂ ) (𝒜.image compl) :=
   by
   ext s
   simp only [mem_image, exists_prop, mem_shadow_iff, mem_up_shadow_iff]
@@ -343,7 +343,7 @@ theorem upShadow_image_compl : ((∂⁺ ) 𝒜).image compl = (∂ ) (𝒜.image
     exact ⟨sᶜ, ⟨s, hs, rfl⟩, a, mem_compl.2 ha, compl_insert.symm⟩
   · rintro ⟨_, ⟨s, hs, rfl⟩, a, ha, rfl⟩
     exact ⟨insert a s, ⟨s, hs, a, mem_compl.1 ha, rfl⟩, compl_insert⟩
-#align finset.up_shadow_image_compl Finset.upShadow_image_compl
+#align finset.up_shadow_image_compl Finset.shadow_compls
 -/
 
 end UpShadow

Mathbin/Computability/RegularExpressions.lean

@@ -279,7 +279,7 @@ theorem add_rmatch_iff (P Q : RegularExpression α) (x : List α) :
     (P + Q).rmatch x ↔ P.rmatch x ∨ Q.rmatch x :=
   by
   induction' x with _ _ ih generalizing P Q
-  · simp only [rmatch, match_epsilon, Bool.or_coe_iff]
+  · simp only [rmatch, match_epsilon, Bool.coe_or_iff]
   · repeat' rw [rmatch]
     rw [deriv]
     exact ih _ _
@@ -296,7 +296,7 @@ theorem mul_rmatch_iff (P Q : RegularExpression α) (x : List α) :
     · intro h
       refine' ⟨[], [], rfl, _⟩
       rw [rmatch, rmatch]
-      rwa [Bool.and_coe_iff] at h 
+      rwa [Bool.coe_and_iff] at h 
     · rintro ⟨t, u, h₁, h₂⟩
       cases' List.append_eq_nil.1 h₁.symm with ht hu
       subst ht

Mathbin/Data/Bool/AllAny.lean

@@ -39,7 +39,7 @@ theorem all_iff_forall {p : α → Bool} : all l p ↔ ∀ a ∈ l, p a :=
   by
   induction' l with a l ih
   · exact iff_of_true rfl (forall_mem_nil _)
-  simp only [all_cons, Bool.and_coe_iff, ih, forall_mem_cons]
+  simp only [all_cons, Bool.coe_and_iff, ih, forall_mem_cons]
 #align list.all_iff_forall List.all_iff_forall
 -/
 
@@ -66,7 +66,7 @@ theorem any_iff_exists {p : α → Bool} : any l p ↔ ∃ a ∈ l, p a :=
   by
   induction' l with a l ih
   · exact iff_of_false Bool.not_false' (not_exists_mem_nil _)
-  simp only [any_cons, Bool.or_coe_iff, ih, exists_mem_cons_iff]
+  simp only [any_cons, Bool.coe_or_iff, ih, exists_mem_cons_iff]
 #align list.any_iff_exists List.any_iff_exists
 -/
 

Mathbin/Data/Bool/Basic.lean

@@ -198,9 +198,9 @@ theorem not_ne_id : not ≠ id := fun h => false_ne_true <| congr_fun h true
 #align bool.bnot_ne_id Bool.not_ne_id
 -/
 
-#print Bool.coe_bool_iff /-
-theorem coe_bool_iff : ∀ {a b : Bool}, (a ↔ b) ↔ a = b := by decide
-#align bool.coe_bool_iff Bool.coe_bool_iff
+#print Bool.coe_iff_coe /-
+theorem coe_iff_coe : ∀ {a b : Bool}, (a ↔ b) ↔ a = b := by decide
+#align bool.coe_bool_iff Bool.coe_iff_coe
 -/
 
 #print Bool.eq_true_of_ne_false /-

Mathbin/RepresentationTheory/GroupCohomology/Basic.lean

@@ -80,20 +80,20 @@ namespace groupCohomology
 
 variable [Monoid G]
 
-#print GroupCohomology.linearYonedaObjResolution /-
+#print groupCohomology.linearYonedaObjResolution /-
 /-- The complex `Hom(P, A)`, where `P` is the standard resolution of `k` as a trivial `k`-linear
 `G`-representation. -/
 abbrev linearYonedaObjResolution (A : Rep k G) : CochainComplex (ModuleCat.{u} k) ℕ :=
   HomologicalComplex.unop
     ((((linearYoneda k (Rep k G)).obj A).rightOp.mapHomologicalComplex _).obj (resolution k G))
-#align group_cohomology.linear_yoneda_obj_resolution GroupCohomology.linearYonedaObjResolution
+#align group_cohomology.linear_yoneda_obj_resolution groupCohomology.linearYonedaObjResolution
 -/
 
-#print GroupCohomology.linearYonedaObjResolution_d_apply /-
+#print groupCohomology.linearYonedaObjResolution_d_apply /-
 theorem linearYonedaObjResolution_d_apply {A : Rep k G} (i j : ℕ) (x : (resolution k G).pt i ⟶ A) :
     (linearYonedaObjResolution A).d i j x = (resolution k G).d j i ≫ x :=
   rfl
-#align group_cohomology.linear_yoneda_obj_resolution_d_apply GroupCohomology.linearYonedaObjResolution_d_apply
+#align group_cohomology.linear_yoneda_obj_resolution_d_apply groupCohomology.linearYonedaObjResolution_d_apply
 -/
 
 end groupCohomology
@@ -102,7 +102,7 @@ namespace InhomogeneousCochains
 
 open Rep groupCohomology
 
-#print InhomogeneousCochains.d /-
+#print inhomogeneousCochains.d /-
 /-- The differential in the complex of inhomogeneous cochains used to
 calculate group cohomology. -/
 @[simps]
@@ -119,12 +119,12 @@ def d [Monoid G] (n : ℕ) (A : Rep k G) : ((Fin n → G) → A) →ₗ[k] (Fin
     ext x
     simp only [Pi.smul_apply, RingHom.id_apply, map_smul, smul_add, Finset.smul_sum, ← smul_assoc,
       smul_eq_mul, mul_comm r]
-#align inhomogeneous_cochains.d InhomogeneousCochains.d
+#align inhomogeneous_cochains.d inhomogeneousCochains.d
 -/
 
 variable [Group G] (n) (A : Rep k G)
 
-#print InhomogeneousCochains.d_eq /-
+#print inhomogeneousCochains.d_eq /-
 /-- The theorem that our isomorphism `Fun(Gⁿ, A) ≅ Hom(k[Gⁿ⁺¹], A)` (where the righthand side is
 morphisms in `Rep k G`) commutes with the differentials in the complex of inhomogeneous cochains
 and the homogeneous `linear_yoneda_obj_resolution`. -/
@@ -152,7 +152,7 @@ theorem d_eq :
     exact
       Finset.sum_congr rfl fun j hj => by
         rw [diagonal_hom_equiv_symm_partial_prod_succ, Fin.val_succ]
-#align inhomogeneous_cochains.d_eq InhomogeneousCochains.d_eq
+#align inhomogeneous_cochains.d_eq inhomogeneousCochains.d_eq
 -/
 
 end InhomogeneousCochains
@@ -163,24 +163,24 @@ variable [Group G] (n) (A : Rep k G)
 
 open InhomogeneousCochains
 
-#print GroupCohomology.inhomogeneousCochains /-
+#print groupCohomology.inhomogeneousCochains /-
 /-- Given a `k`-linear `G`-representation `A`, this is the complex of inhomogeneous cochains
 $$0 \to \mathrm{Fun}(G^0, A) \to \mathrm{Fun}(G^1, A) \to \mathrm{Fun}(G^2, A) \to \dots$$
 which calculates the group cohomology of `A`. -/
 noncomputable abbrev inhomogeneousCochains : CochainComplex (ModuleCat k) ℕ :=
   CochainComplex.of (fun n => ModuleCat.of k ((Fin n → G) → A))
-    (fun n => InhomogeneousCochains.d n A) fun n =>
+    (fun n => inhomogeneousCochains.d n A) fun n =>
     by
     ext x y
     have := LinearMap.ext_iff.1 ((linear_yoneda_obj_resolution A).d_comp_d n (n + 1) (n + 2))
     simp only [ModuleCat.coe_comp, Function.comp_apply] at this 
     simp only [ModuleCat.coe_comp, Function.comp_apply, d_eq, LinearEquiv.toModuleIso_hom,
       LinearEquiv.toModuleIso_inv, LinearEquiv.coe_coe, LinearEquiv.symm_apply_apply, this,
       LinearMap.zero_apply, map_zero, Pi.zero_apply]
-#align group_cohomology.inhomogeneous_cochains GroupCohomology.inhomogeneousCochains
+#align group_cohomology.inhomogeneous_cochains groupCohomology.inhomogeneousCochains
 -/
 
-#print GroupCohomology.inhomogeneousCochainsIso /-
+#print groupCohomology.inhomogeneousCochainsIso /-
 /-- Given a `k`-linear `G`-representation `A`, the complex of inhomogeneous cochains is isomorphic
 to `Hom(P, A)`, where `P` is the standard resolution of `k` as a trivial `G`-representation. -/
 def inhomogeneousCochainsIso : inhomogeneousCochains A ≅ linearYonedaObjResolution A :=
@@ -190,7 +190,7 @@ def inhomogeneousCochainsIso : inhomogeneousCochains A ≅ linearYonedaObjResolu
     subst h
     simp only [CochainComplex.of_d, d_eq, category.assoc, iso.symm_hom, iso.hom_inv_id,
       category.comp_id]
-#align group_cohomology.inhomogeneous_cochains_iso GroupCohomology.inhomogeneousCochainsIso
+#align group_cohomology.inhomogeneous_cochains_iso groupCohomology.inhomogeneousCochainsIso
 -/
 
 end groupCohomology