refactor(Measure): improve defeq for ⊤ (#12706)

Now `(⊤ : Measure α).toOuterMeasure = ⊤` is defeq.

Author: urkud

Mathlib/MeasureTheory/Measure/MeasureSpace.lean

@@ -1057,35 +1057,36 @@ instance instCompleteSemilatticeInf [MeasurableSpace α] : CompleteSemilatticeIn
 #align measure_theory.measure.complete_semilattice_Inf MeasureTheory.Measure.instCompleteSemilatticeInf
 
 instance instCompleteLattice [MeasurableSpace α] : CompleteLattice (Measure α) :=
-  { /- Porting note:
-    Adding an explicit `top` made `leanchecker` fail in Lean3 because of lean#364,
-    but in Lean4 it's all right.
-    top := (⊤ : OuterMeasure α).toMeasure
-      (by rw [OuterMeasure.top_caratheodory]; exact le_top)
-    le_top := fun a s hs => by
-      rcases s.eq_empty_or_nonempty with rfl | h <;>
-      dsimp only [] <;>
-        [simp, (rw [fun h' => toMeasure_apply ⊤ h' hs, OuterMeasure.top_apply h]; exact le_top) ]
-    -/
-    completeLatticeOfCompleteSemilatticeInf (Measure α) with
+  { completeLatticeOfCompleteSemilatticeInf (Measure α) with
+    top :=
+      { toOuterMeasure := ⊤,
+        m_iUnion := by
+          intro f _ _
+          refine (OuterMeasure.iUnion _ _).antisymm ?_
+          if hne : (⋃ i, f i).Nonempty then
+            rw [OuterMeasure.top_apply hne]
+            exact le_top
+          else
+            simp_all [Set.not_nonempty_iff_eq_empty]
+        trimmed := le_antisymm le_top (OuterMeasure.le_trim _) },
+    le_top := fun μ => toOuterMeasure_le.mp le_top
     bot := 0
     bot_le := fun _a _s => bot_le }
 #align measure_theory.measure.complete_lattice MeasureTheory.Measure.instCompleteLattice
 
 end sInf
 
 @[simp]
-theorem _root_.MeasureTheory.OuterMeasure.toMeasure_top [MeasurableSpace α] :
+theorem _root_.MeasureTheory.OuterMeasure.toMeasure_top :
     (⊤ : OuterMeasure α).toMeasure (by rw [OuterMeasure.top_caratheodory]; exact le_top) =
       (⊤ : Measure α) :=
-  top_unique <| le_intro fun s hs hne => by
-    simp [hne, toMeasure_apply ⊤ _ hs, OuterMeasure.top_apply]
+  toOuterMeasure_toMeasure (μ := ⊤)
 #align measure_theory.outer_measure.to_measure_top MeasureTheory.OuterMeasure.toMeasure_top
 
 @[simp]
 theorem toOuterMeasure_top [MeasurableSpace α] :
-    (⊤ : Measure α).toOuterMeasure = (⊤ : OuterMeasure α) := by
-  rw [← OuterMeasure.toMeasure_top, toMeasure_toOuterMeasure, OuterMeasure.trim_top]
+    (⊤ : Measure α).toOuterMeasure = (⊤ : OuterMeasure α) :=
+  rfl
 #align measure_theory.measure.to_outer_measure_top MeasureTheory.Measure.toOuterMeasure_top
 
 @[simp]