lolwut

leanprover-community · Mar 11, 2024 · d93ec60 · d93ec60
1 parent b4aa595
commit d93ec60
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/Mathlib/MeasureTheory/MeasurableSpace/Basic.lean b/Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
@@ -186,9 +186,9 @@ theorem le_map_comap : m ≤ (m.comap g).map g :=
 
 end Functors
 
-@[simp] theorem map_const {m} (b : β) : MeasurableSpace.map (fun _a : α ↦ b) m = ⊤ := by
-  refine eq_top_iff.2 <| fun s ?_
-  by_cases b ∈ s <;> simp [*, map_def] <;> rw [Set.preimage_id'] <;> simp
+@[simp] theorem map_const {m} (b : β) : MeasurableSpace.map (fun _a : α ↦ b) m = ⊤ :=
+  eq_top_iff.2 <| fun s
+    by_cases b ∈ s <;> simp [*, map_def] <;> rw [Set.preimage_id'] <;> simp
 #align measurable_space.map_const MeasurableSpace.map_const
 
 set_option tactic.skipAssignedInstances false in