bump to nightly-2024-02-17-08

mathlib commit leanprover-community/mathlib@65a1391

Archive/Wiedijk100Theorems/BallotProblem.lean

@@ -172,7 +172,7 @@ theorem countedSequence_finite : ∀ p q : ℕ, (countedSequence p q).Finite
     rw [counted_succ_succ, Set.finite_union, Set.finite_image_iff (list.cons_injective.inj_on _),
       Set.finite_image_iff (list.cons_injective.inj_on _)]
     exact ⟨counted_sequence_finite _ _, counted_sequence_finite _ _⟩
-#align ballot.counted_sequence_finite Ballot.countedSequence_finite
+#align ballot.counted_sequence_finite Ballot.countedSequence_finiteₓ
 
 theorem countedSequence_nonempty : ∀ p q : ℕ, (countedSequence p q).Nonempty
   | 0, q => by simp

Mathbin/Algebra/Group/Basic.lean

@@ -1154,16 +1154,16 @@ theorem leftInverse_inv_mul_mul_right (c : G) :
 #align left_inverse_neg_add_add_right leftInverse_neg_add_add_right
 -/
 
-#print exists_npow_eq_one_of_zpow_eq_one /-
+#print exists_pow_eq_one_of_zpow_eq_one /-
 @[to_additive]
-theorem exists_npow_eq_one_of_zpow_eq_one {n : ℤ} (hn : n ≠ 0) {x : G} (h : x ^ n = 1) :
+theorem exists_pow_eq_one_of_zpow_eq_one {n : ℤ} (hn : n ≠ 0) {x : G} (h : x ^ n = 1) :
     ∃ n : ℕ, 0 < n ∧ x ^ n = 1 := by
   cases' n with n n
   · rw [zpow_ofNat] at h 
     refine' ⟨n, Nat.pos_of_ne_zero fun n0 => hn _, h⟩; rw [n0]; rfl
   · rw [zpow_negSucc, inv_eq_one] at h 
     refine' ⟨n + 1, n.succ_pos, h⟩
-#align exists_npow_eq_one_of_zpow_eq_one exists_npow_eq_one_of_zpow_eq_one
+#align exists_npow_eq_one_of_zpow_eq_one exists_pow_eq_one_of_zpow_eq_one
 #align exists_nsmul_eq_zero_of_zsmul_eq_zero exists_nsmul_eq_zero_of_zsmul_eq_zero
 -/
 

Mathbin/Algebra/Hom/Equiv/Units/Basic.lean

@@ -32,12 +32,12 @@ def toUnits [Group G] : G ≃* Gˣ
 #align to_add_units toAddUnits
 -/
 
-#print coe_toUnits /-
+#print val_toUnits_apply /-
 @[simp, to_additive]
-theorem coe_toUnits [Group G] (g : G) : (toUnits g : G) = g :=
+theorem val_toUnits_apply [Group G] (g : G) : (toUnits g : G) = g :=
   rfl
-#align coe_to_units coe_toUnits
-#align coe_to_add_units coe_toAddUnits
+#align coe_to_units val_toUnits_apply
+#align coe_to_add_units val_toAddUnits_apply
 -/
 
 namespace Units

Mathbin/Algebra/Order/Floor.lean

@@ -1948,28 +1948,28 @@ theorem Nat.ceil_int : (Nat.ceil : ℤ → ℕ) = Int.toNat :=
 
 variable {a : α}
 
-#print Nat.cast_floor_eq_int_floor /-
-theorem Nat.cast_floor_eq_int_floor (ha : 0 ≤ a) : (⌊a⌋₊ : ℤ) = ⌊a⌋ := by
+#print Int.ofNat_floor_eq_floor /-
+theorem Int.ofNat_floor_eq_floor (ha : 0 ≤ a) : (⌊a⌋₊ : ℤ) = ⌊a⌋ := by
   rw [← Int.floor_toNat, Int.toNat_of_nonneg (Int.floor_nonneg.2 ha)]
-#align nat.cast_floor_eq_int_floor Nat.cast_floor_eq_int_floor
+#align nat.cast_floor_eq_int_floor Int.ofNat_floor_eq_floor
 -/
 
-#print Nat.cast_floor_eq_cast_int_floor /-
-theorem Nat.cast_floor_eq_cast_int_floor (ha : 0 ≤ a) : (⌊a⌋₊ : α) = ⌊a⌋ := by
-  rw [← Nat.cast_floor_eq_int_floor ha, Int.cast_ofNat]
-#align nat.cast_floor_eq_cast_int_floor Nat.cast_floor_eq_cast_int_floor
+#print natCast_floor_eq_intCast_floor /-
+theorem natCast_floor_eq_intCast_floor (ha : 0 ≤ a) : (⌊a⌋₊ : α) = ⌊a⌋ := by
+  rw [← Int.ofNat_floor_eq_floor ha, Int.cast_ofNat]
+#align nat.cast_floor_eq_cast_int_floor natCast_floor_eq_intCast_floor
 -/
 
-#print Nat.cast_ceil_eq_int_ceil /-
-theorem Nat.cast_ceil_eq_int_ceil (ha : 0 ≤ a) : (⌈a⌉₊ : ℤ) = ⌈a⌉ := by
+#print Int.ofNat_ceil_eq_ceil /-
+theorem Int.ofNat_ceil_eq_ceil (ha : 0 ≤ a) : (⌈a⌉₊ : ℤ) = ⌈a⌉ := by
   rw [← Int.ceil_toNat, Int.toNat_of_nonneg (Int.ceil_nonneg ha)]
-#align nat.cast_ceil_eq_int_ceil Nat.cast_ceil_eq_int_ceil
+#align nat.cast_ceil_eq_int_ceil Int.ofNat_ceil_eq_ceil
 -/
 
-#print Nat.cast_ceil_eq_cast_int_ceil /-
-theorem Nat.cast_ceil_eq_cast_int_ceil (ha : 0 ≤ a) : (⌈a⌉₊ : α) = ⌈a⌉ := by
-  rw [← Nat.cast_ceil_eq_int_ceil ha, Int.cast_ofNat]
-#align nat.cast_ceil_eq_cast_int_ceil Nat.cast_ceil_eq_cast_int_ceil
+#print natCast_ceil_eq_intCast_ceil /-
+theorem natCast_ceil_eq_intCast_ceil (ha : 0 ≤ a) : (⌈a⌉₊ : α) = ⌈a⌉ := by
+  rw [← Int.ofNat_ceil_eq_ceil ha, Int.cast_ofNat]
+#align nat.cast_ceil_eq_cast_int_ceil natCast_ceil_eq_intCast_ceil
 -/
 
 end FloorRingToSemiring

Mathbin/Algebra/Order/Hom/Monoid.lean

@@ -83,15 +83,13 @@ infixr:25 " →+o " => OrderAddMonoidHom
 
 section
 
-#print OrderAddMonoidHomClass /-
 /-- `order_add_monoid_hom_class F α β` states that `F` is a type of ordered monoid homomorphisms.
 
 You should also extend this typeclass when you extend `order_add_monoid_hom`. -/
 class OrderAddMonoidHomClass (F : Type _) (α β : outParam <| Type _) [Preorder α] [Preorder β]
     [AddZeroClass α] [AddZeroClass β] extends AddMonoidHomClass F α β where
   Monotone (f : F) : Monotone f
 #align order_add_monoid_hom_class OrderAddMonoidHomClass
--/
 
 end
 
@@ -123,7 +121,6 @@ infixr:25 " →*o " => OrderMonoidHom
 
 section
 
-#print OrderMonoidHomClass /-
 /-- `order_monoid_hom_class F α β` states that `F` is a type of ordered monoid homomorphisms.
 
 You should also extend this typeclass when you extend `order_monoid_hom`. -/
@@ -133,19 +130,16 @@ class OrderMonoidHomClass (F : Type _) (α β : outParam <| Type _) [Preorder α
   Monotone (f : F) : Monotone f
 #align order_monoid_hom_class OrderMonoidHomClass
 #align order_add_monoid_hom_class OrderAddMonoidHomClass
--/
 
 end
 
-#print OrderMonoidHomClass.toOrderHomClass /-
 -- See note [lower instance priority]
 @[to_additive]
 instance (priority := 100) OrderMonoidHomClass.toOrderHomClass [OrderMonoidHomClass F α β] :
     OrderHomClass F α β :=
   { ‹OrderMonoidHomClass F α β› with mapRel := OrderMonoidHomClass.monotone }
 #align order_monoid_hom_class.to_order_hom_class OrderMonoidHomClass.toOrderHomClass
-#align order_add_monoid_hom_class.to_order_hom_class OrderAddMonoidHomClass.toOrderHomClass
--/
+#align order_add_monoid_hom_class.to_order_hom_class OrderAddMonoidHomClass.to_order_hom_class
 
 @[to_additive]
 instance [OrderMonoidHomClass F α β] : CoeTC F (α →*o β) :=
@@ -181,7 +175,6 @@ infixr:25 " →*₀o " => OrderMonoidWithZeroHom
 
 section
 
-#print OrderMonoidWithZeroHomClass /-
 /-- `order_monoid_with_zero_hom_class F α β` states that `F` is a type of
 ordered monoid with zero homomorphisms.
 
@@ -190,17 +183,14 @@ class OrderMonoidWithZeroHomClass (F : Type _) (α β : outParam <| Type _) [Pre
     [MulZeroOneClass α] [MulZeroOneClass β] extends MonoidWithZeroHomClass F α β where
   Monotone (f : F) : Monotone f
 #align order_monoid_with_zero_hom_class OrderMonoidWithZeroHomClass
--/
 
 end
 
-#print OrderMonoidWithZeroHomClass.toOrderMonoidHomClass /-
 -- See note [lower instance priority]
 instance (priority := 100) OrderMonoidWithZeroHomClass.toOrderMonoidHomClass
     [OrderMonoidWithZeroHomClass F α β] : OrderMonoidHomClass F α β :=
   { ‹OrderMonoidWithZeroHomClass F α β› with }
 #align order_monoid_with_zero_hom_class.to_order_monoid_hom_class OrderMonoidWithZeroHomClass.toOrderMonoidHomClass
--/
 
 instance [OrderMonoidWithZeroHomClass F α β] : CoeTC F (α →*₀o β) :=
   ⟨fun f =>

Mathbin/Algebra/Order/Hom/Ring.lean

@@ -73,57 +73,45 @@ structure OrderRingIso (α β : Type _) [Mul α] [Add α] [LE α] [Mul β] [Add
 
 infixl:25 " ≃+*o " => OrderRingIso
 
-#print OrderRingHomClass /-
 /-- `order_ring_hom_class F α β` states that `F` is a type of ordered semiring homomorphisms.
 You should extend this typeclass when you extend `order_ring_hom`. -/
 class OrderRingHomClass (F : Type _) (α β : outParam <| Type _) [NonAssocSemiring α] [Preorder α]
     [NonAssocSemiring β] [Preorder β] extends RingHomClass F α β where
   Monotone (f : F) : Monotone f
 #align order_ring_hom_class OrderRingHomClass
--/
 
-#print OrderRingIsoClass /-
 /-- `order_ring_iso_class F α β` states that `F` is a type of ordered semiring isomorphisms.
 You should extend this class when you extend `order_ring_iso`. -/
 class OrderRingIsoClass (F : Type _) (α β : outParam (Type _)) [Mul α] [Add α] [LE α] [Mul β]
     [Add β] [LE β] extends RingEquivClass F α β where
   map_le_map_iff (f : F) {a b : α} : f a ≤ f b ↔ a ≤ b
 #align order_ring_iso_class OrderRingIsoClass
--/
 
-#print OrderRingHomClass.toOrderAddMonoidHomClass /-
 -- See note [lower priority instance]
 instance (priority := 100) OrderRingHomClass.toOrderAddMonoidHomClass [NonAssocSemiring α]
     [Preorder α] [NonAssocSemiring β] [Preorder β] [OrderRingHomClass F α β] :
     OrderAddMonoidHomClass F α β :=
   { ‹OrderRingHomClass F α β› with }
 #align order_ring_hom_class.to_order_add_monoid_hom_class OrderRingHomClass.toOrderAddMonoidHomClass
--/
 
-#print OrderRingHomClass.toOrderMonoidWithZeroHomClass /-
 -- See note [lower priority instance]
 instance (priority := 100) OrderRingHomClass.toOrderMonoidWithZeroHomClass [NonAssocSemiring α]
     [Preorder α] [NonAssocSemiring β] [Preorder β] [OrderRingHomClass F α β] :
     OrderMonoidWithZeroHomClass F α β :=
   { ‹OrderRingHomClass F α β› with }
 #align order_ring_hom_class.to_order_monoid_with_zero_hom_class OrderRingHomClass.toOrderMonoidWithZeroHomClass
--/
 
-#print OrderRingIsoClass.toOrderIsoClass /-
 -- See note [lower instance priority]
 instance (priority := 100) OrderRingIsoClass.toOrderIsoClass [Mul α] [Add α] [LE α] [Mul β] [Add β]
     [LE β] [OrderRingIsoClass F α β] : OrderIsoClass F α β :=
   { ‹OrderRingIsoClass F α β› with }
 #align order_ring_iso_class.to_order_iso_class OrderRingIsoClass.toOrderIsoClass
--/
 
-#print OrderRingIsoClass.toOrderRingHomClass /-
 -- See note [lower instance priority]
 instance (priority := 100) OrderRingIsoClass.toOrderRingHomClass [NonAssocSemiring α] [Preorder α]
     [NonAssocSemiring β] [Preorder β] [OrderRingIsoClass F α β] : OrderRingHomClass F α β :=
   { ‹OrderRingIsoClass F α β› with Monotone := fun f => OrderHomClass.mono f }
 #align order_ring_iso_class.to_order_ring_hom_class OrderRingIsoClass.toOrderRingHomClass
--/
 
 instance [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β]
     [OrderRingHomClass F α β] : CoeTC F (α →+*o β) :=

Mathbin/Algebra/Quaternion.lean

@@ -638,7 +638,7 @@ theorem rank_eq_four [StrongRankCondition R] : Module.rank R ℍ[R,c₁,c₂] =
 theorem finrank_eq_four [StrongRankCondition R] : FiniteDimensional.finrank R ℍ[R,c₁,c₂] = 4 :=
   by
   have : Cardinal.toNat 4 = 4 := by
-    rw [← Cardinal.toNat_cast 4, Nat.cast_bit0, Nat.cast_bit0, Nat.cast_one]
+    rw [← Cardinal.toNat_natCast 4, Nat.cast_bit0, Nat.cast_bit0, Nat.cast_one]
   rw [FiniteDimensional.finrank, rank_eq_four, this]
 #align quaternion_algebra.finrank_eq_four QuaternionAlgebra.finrank_eq_four
 -/

Mathbin/Analysis/Complex/UpperHalfPlane/Basic.lean

@@ -323,63 +323,63 @@ instance SLAction {R : Type _} [CommRing R] [Algebra R ℝ] : MulAction SL(2, R)
 instance : Coe SL(2, ℤ) GL(2, ℝ)⁺ :=
   ⟨fun g => ((g : SL(2, ℝ)) : GL(2, ℝ)⁺)⟩
 
-#print UpperHalfPlane.SLOnGLPos /-
-instance SLOnGLPos : SMul SL(2, ℤ) GL(2, ℝ)⁺ :=
+#print UpperHalfPlane.ModularGroup.SLOnGLPos /-
+instance UpperHalfPlane.ModularGroup.SLOnGLPos : SMul SL(2, ℤ) GL(2, ℝ)⁺ :=
   ⟨fun s g => s * g⟩
-#align upper_half_plane.SL_on_GL_pos UpperHalfPlane.SLOnGLPos
+#align upper_half_plane.SL_on_GL_pos UpperHalfPlane.ModularGroup.SLOnGLPos
 -/
 
-#print UpperHalfPlane.SLOnGLPos_smul_apply /-
-theorem SLOnGLPos_smul_apply (s : SL(2, ℤ)) (g : GL(2, ℝ)⁺) (z : ℍ) :
+#print UpperHalfPlane.ModularGroup.SLOnGLPos_smul_apply /-
+theorem UpperHalfPlane.ModularGroup.SLOnGLPos_smul_apply (s : SL(2, ℤ)) (g : GL(2, ℝ)⁺) (z : ℍ) :
     (s • g) • z = ((s : GL(2, ℝ)⁺) * g) • z :=
   rfl
-#align upper_half_plane.SL_on_GL_pos_smul_apply UpperHalfPlane.SLOnGLPos_smul_apply
+#align upper_half_plane.SL_on_GL_pos_smul_apply UpperHalfPlane.ModularGroup.SLOnGLPos_smul_apply
 -/
 
-#print UpperHalfPlane.SL_to_GL_tower /-
-instance SL_to_GL_tower : IsScalarTower SL(2, ℤ) GL(2, ℝ)⁺ ℍ
+#print UpperHalfPlane.ModularGroup.SL_to_GL_tower /-
+instance UpperHalfPlane.ModularGroup.SL_to_GL_tower : IsScalarTower SL(2, ℤ) GL(2, ℝ)⁺ ℍ
     where smul_assoc := by intro s g z; simp only [SL_on_GL_pos_smul_apply, coe_coe];
     apply mul_smul'
-#align upper_half_plane.SL_to_GL_tower UpperHalfPlane.SL_to_GL_tower
+#align upper_half_plane.SL_to_GL_tower UpperHalfPlane.ModularGroup.SL_to_GL_tower
 -/
 
-#print UpperHalfPlane.subgroupGLPos /-
-instance subgroupGLPos : SMul Γ GL(2, ℝ)⁺ :=
+#print UpperHalfPlane.ModularGroup.subgroupGLPos /-
+instance UpperHalfPlane.ModularGroup.subgroupGLPos : SMul Γ GL(2, ℝ)⁺ :=
   ⟨fun s g => s * g⟩
-#align upper_half_plane.subgroup_GL_pos UpperHalfPlane.subgroupGLPos
+#align upper_half_plane.subgroup_GL_pos UpperHalfPlane.ModularGroup.subgroupGLPos
 -/
 
-#print UpperHalfPlane.subgroup_on_glpos_smul_apply /-
-theorem subgroup_on_glpos_smul_apply (s : Γ) (g : GL(2, ℝ)⁺) (z : ℍ) :
+#print UpperHalfPlane.ModularGroup.subgroup_on_glpos_smul_apply /-
+theorem UpperHalfPlane.ModularGroup.subgroup_on_glpos_smul_apply (s : Γ) (g : GL(2, ℝ)⁺) (z : ℍ) :
     (s • g) • z = ((s : GL(2, ℝ)⁺) * g) • z :=
   rfl
-#align upper_half_plane.subgroup_on_GL_pos_smul_apply UpperHalfPlane.subgroup_on_glpos_smul_apply
+#align upper_half_plane.subgroup_on_GL_pos_smul_apply UpperHalfPlane.ModularGroup.subgroup_on_glpos_smul_apply
 -/
 
-#print UpperHalfPlane.subgroup_on_glpos /-
-instance subgroup_on_glpos : IsScalarTower Γ GL(2, ℝ)⁺ ℍ
+#print UpperHalfPlane.ModularGroup.subgroup_on_glpos /-
+instance UpperHalfPlane.ModularGroup.subgroup_on_glpos : IsScalarTower Γ GL(2, ℝ)⁺ ℍ
     where smul_assoc := by intro s g z; simp only [subgroup_on_GL_pos_smul_apply, coe_coe];
     apply mul_smul'
-#align upper_half_plane.subgroup_on_GL_pos UpperHalfPlane.subgroup_on_glpos
+#align upper_half_plane.subgroup_on_GL_pos UpperHalfPlane.ModularGroup.subgroup_on_glpos
 -/
 
-#print UpperHalfPlane.subgroupSL /-
-instance subgroupSL : SMul Γ SL(2, ℤ) :=
+#print UpperHalfPlane.ModularGroup.subgroupSL /-
+instance UpperHalfPlane.ModularGroup.subgroupSL : SMul Γ SL(2, ℤ) :=
   ⟨fun s g => s * g⟩
-#align upper_half_plane.subgroup_SL UpperHalfPlane.subgroupSL
+#align upper_half_plane.subgroup_SL UpperHalfPlane.ModularGroup.subgroupSL
 -/
 
-#print UpperHalfPlane.subgroup_on_SL_apply /-
-theorem subgroup_on_SL_apply (s : Γ) (g : SL(2, ℤ)) (z : ℍ) :
+#print UpperHalfPlane.ModularGroup.subgroup_on_SL_apply /-
+theorem UpperHalfPlane.ModularGroup.subgroup_on_SL_apply (s : Γ) (g : SL(2, ℤ)) (z : ℍ) :
     (s • g) • z = ((s : SL(2, ℤ)) * g) • z :=
   rfl
-#align upper_half_plane.subgroup_on_SL_apply UpperHalfPlane.subgroup_on_SL_apply
+#align upper_half_plane.subgroup_on_SL_apply UpperHalfPlane.ModularGroup.subgroup_on_SL_apply
 -/
 
-#print UpperHalfPlane.subgroup_to_SL_tower /-
-instance subgroup_to_SL_tower : IsScalarTower Γ SL(2, ℤ) ℍ
+#print UpperHalfPlane.ModularGroup.subgroup_to_SL_tower /-
+instance UpperHalfPlane.ModularGroup.subgroup_to_SL_tower : IsScalarTower Γ SL(2, ℤ) ℍ
     where smul_assoc s g z := by rw [subgroup_on_SL_apply]; apply MulAction.hMul_smul
-#align upper_half_plane.subgroup_to_SL_tower UpperHalfPlane.subgroup_to_SL_tower
+#align upper_half_plane.subgroup_to_SL_tower UpperHalfPlane.ModularGroup.subgroup_to_SL_tower
 -/
 
 end ModularScalarTowers
@@ -439,31 +439,32 @@ section SLModularAction
 
 variable (g : SL(2, ℤ)) (z : ℍ) (Γ : Subgroup SL(2, ℤ))
 
-#print UpperHalfPlane.sl_moeb /-
+#print UpperHalfPlane.ModularGroup.sl_moeb /-
 @[simp]
-theorem sl_moeb (A : SL(2, ℤ)) (z : ℍ) : A • z = (A : GL(2, ℝ)⁺) • z :=
+theorem UpperHalfPlane.ModularGroup.sl_moeb (A : SL(2, ℤ)) (z : ℍ) : A • z = (A : GL(2, ℝ)⁺) • z :=
   rfl
-#align upper_half_plane.sl_moeb UpperHalfPlane.sl_moeb
+#align upper_half_plane.sl_moeb UpperHalfPlane.ModularGroup.sl_moeb
 -/
 
-#print UpperHalfPlane.subgroup_moeb /-
-theorem subgroup_moeb (A : Γ) (z : ℍ) : A • z = (A : GL(2, ℝ)⁺) • z :=
+#print UpperHalfPlane.ModularGroup.subgroup_moeb /-
+theorem UpperHalfPlane.ModularGroup.subgroup_moeb (A : Γ) (z : ℍ) : A • z = (A : GL(2, ℝ)⁺) • z :=
   rfl
-#align upper_half_plane.subgroup_moeb UpperHalfPlane.subgroup_moeb
+#align upper_half_plane.subgroup_moeb UpperHalfPlane.ModularGroup.subgroup_moeb
 -/
 
-#print UpperHalfPlane.subgroup_to_sl_moeb /-
+#print UpperHalfPlane.ModularGroup.subgroup_to_sl_moeb /-
 @[simp]
-theorem subgroup_to_sl_moeb (A : Γ) (z : ℍ) : A • z = (A : SL(2, ℤ)) • z :=
+theorem UpperHalfPlane.ModularGroup.subgroup_to_sl_moeb (A : Γ) (z : ℍ) :
+    A • z = (A : SL(2, ℤ)) • z :=
   rfl
-#align upper_half_plane.subgroup_to_sl_moeb UpperHalfPlane.subgroup_to_sl_moeb
+#align upper_half_plane.subgroup_to_sl_moeb UpperHalfPlane.ModularGroup.subgroup_to_sl_moeb
 -/
 
-#print UpperHalfPlane.SL_neg_smul /-
+#print UpperHalfPlane.ModularGroup.SL_neg_smul /-
 @[simp]
-theorem SL_neg_smul (g : SL(2, ℤ)) (z : ℍ) : -g • z = g • z := by
+theorem UpperHalfPlane.ModularGroup.SL_neg_smul (g : SL(2, ℤ)) (z : ℍ) : -g • z = g • z := by
   simp only [coe_GL_pos_neg, sl_moeb, coe_coe, coe_int_neg, neg_smul]
-#align upper_half_plane.SL_neg_smul UpperHalfPlane.SL_neg_smul
+#align upper_half_plane.SL_neg_smul UpperHalfPlane.ModularGroup.SL_neg_smul
 -/
 
 #print UpperHalfPlane.c_mul_im_sq_le_normSq_denom /-
@@ -478,20 +479,20 @@ theorem c_mul_im_sq_le_normSq_denom (z : ℍ) (g : SL(2, ℝ)) :
 #align upper_half_plane.c_mul_im_sq_le_norm_sq_denom UpperHalfPlane.c_mul_im_sq_le_normSq_denom
 -/
 
-#print UpperHalfPlane.SpecialLinearGroup.im_smul_eq_div_normSq /-
-theorem SpecialLinearGroup.im_smul_eq_div_normSq : (g • z).im = z.im / Complex.normSq (denom g z) :=
+#print UpperHalfPlane.ModularGroup.im_smul_eq_div_normSq /-
+theorem ModularGroup.im_smul_eq_div_normSq : (g • z).im = z.im / Complex.normSq (denom g z) :=
   by
   convert im_smul_eq_div_norm_sq g z
   simp only [coe_coe, general_linear_group.coe_det_apply, coe_GL_pos_coe_GL_coe_matrix,
     Int.coe_castRingHom, (g : SL(2, ℝ)).Prop, one_mul]
-#align upper_half_plane.special_linear_group.im_smul_eq_div_norm_sq UpperHalfPlane.SpecialLinearGroup.im_smul_eq_div_normSq
+#align upper_half_plane.special_linear_group.im_smul_eq_div_norm_sq UpperHalfPlane.ModularGroup.im_smul_eq_div_normSq
 -/
 
-#print UpperHalfPlane.denom_apply /-
-theorem denom_apply (g : SL(2, ℤ)) (z : ℍ) :
+#print UpperHalfPlane.ModularGroup.denom_apply /-
+theorem UpperHalfPlane.ModularGroup.denom_apply (g : SL(2, ℤ)) (z : ℍ) :
     denom g z = (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 * z + (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 := by
   simp
-#align upper_half_plane.denom_apply UpperHalfPlane.denom_apply
+#align upper_half_plane.denom_apply UpperHalfPlane.ModularGroup.denom_apply
 -/
 
 end SLModularAction

Mathbin/Analysis/Convolution.lean

@@ -400,7 +400,7 @@ theorem HasCompactSupport.convolutionExistsAt {x₀ : G}
           v.to_measurable_equiv.measurable_embedding).1
       A
   ext x
-  simp only [Homeomorph.neg, sub_eq_add_neg, coe_toAddUnits, Homeomorph.trans_apply,
+  simp only [Homeomorph.neg, sub_eq_add_neg, val_toAddUnits_apply, Homeomorph.trans_apply,
     Equiv.neg_apply, Equiv.toFun_as_coe, Homeomorph.homeomorph_mk_coe, Equiv.coe_fn_mk,
     Homeomorph.coe_addLeft]
 #align has_compact_support.convolution_exists_at HasCompactSupport.convolutionExistsAt