implicit

Author: vihdzp

Mathlib/Order/Cofinal.lean

@@ -34,11 +34,11 @@ variable {α β : Type*}
 section LE
 variable [LE α]
 
-theorem IsCofinal.of_isEmpty [IsEmpty α] (s : Set α) : IsCofinal s :=
+theorem IsCofinal.of_isEmpty [IsEmpty α] {s : Set α} : IsCofinal s :=
   fun a ↦ isEmptyElim a
 
 theorem isCofinal_empty_iff : IsCofinal (∅ : Set α) ↔ IsEmpty α := by
-  refine ⟨fun h ↦ ⟨fun a ↦ ?_⟩, fun h ↦ .of_isEmpty _⟩
+  refine ⟨fun h ↦ ⟨fun a ↦ ?_⟩, fun h ↦ .of_isEmpty⟩
   simpa using h a
 
 @[simp]

Mathlib/Order/DirSupClosed.lean

@@ -63,14 +63,14 @@ def DirSupInacc (s : Set α) : Prop :=
 @[simp] lemma DirSupClosed.dirSupClosedOn : DirSupClosed s → DirSupClosedOn D s := @fun h _ _ ↦ @h _
 @[simp] lemma DirSupInacc.dirSupInaccOn : DirSupInacc s → DirSupInaccOn D s := @fun h _ _ ↦ @h _
 
-@[simp] theorem DirSupClosed.of_isEmpty [IsEmpty α] (s : Set α) : DirSupClosed s :=
+@[simp] theorem DirSupClosed.of_isEmpty [IsEmpty α] {s : Set α} : DirSupClosed s :=
   fun _ _ ⟨a, _⟩ ↦ isEmptyElim a
 
-@[simp] theorem DirSupInacc.of_isEmpty [IsEmpty α] (s : Set α) : DirSupInacc s :=
+@[simp] theorem DirSupInacc.of_isEmpty [IsEmpty α] {s : Set α} : DirSupInacc s :=
   fun _ ⟨a, _⟩ ↦ isEmptyElim a
 
-theorem DirSupClosedOn.of_isEmpty [IsEmpty α] (s : Set α) : DirSupClosedOn D s := by simp
-theorem DirSupInaccOn.of_isEmpty [IsEmpty α] (s : Set α) : DirSupInaccOn D s := by simp
+theorem DirSupClosedOn.of_isEmpty [IsEmpty α] {s : Set α} : DirSupClosedOn D s := by simp
+theorem DirSupInaccOn.of_isEmpty [IsEmpty α] {s : Set α} : DirSupInaccOn D s := by simp
 
 @[gcongr]
 lemma DirSupClosedOn.mono (hD : D₁ ⊆ D₂) (hf : DirSupClosedOn D₂ s) : DirSupClosedOn D₁ s :=

Mathlib/SetTheory/Cardinal/Cofinality/Club.lean

@@ -23,7 +23,7 @@ For any type equipped with the Scott-Hausdorff topology (which includes well-ord
 topology), `DirSupClosed s` and `IsClosed s` are equivalent predicates.
 -/
 
-@[expose] public section
+public section
 
 universe u v
 
@@ -41,8 +41,8 @@ structure IsClub {α : Type*} [LinearOrder α] (s : Set α) where
 variable {α : Type v} {s t : Set α} {x : α} [LinearOrder α]
 
 @[simp]
-theorem IsClub.of_isEmpty [IsEmpty α] (s : Set α) : IsClub s :=
-  ⟨.of_isEmpty s, .of_isEmpty s⟩
+theorem IsClub.of_isEmpty [IsEmpty α] {s : Set α} : IsClub s :=
+  ⟨.of_isEmpty, .of_isEmpty⟩
 
 @[simp]
 theorem IsClub.univ : IsClub (α := α) .univ :=