Minigolf

grunweg · grunweg · commit be007b67699d · 2025-07-03T23:50:58.000+02:00
diff --git a/Mathlib/Analysis/Calculus/ContDiff/Basic.lean b/Mathlib/Analysis/Calculus/ContDiff/Basic.lean
@@ -572,8 +572,7 @@ section contDiffOn_union
 lemma ContDiffOn.union_of_isOpen (hf : ContDiffOn 𝕜 n f s) (hf' : ContDiffOn 𝕜 n f t)
     (hs : IsOpen s) (ht : IsOpen t) :
     ContDiffOn 𝕜 n f (s ∪ t) := by
-  intro x hx
-  obtain (hx | hx) := hx
+  rintro x (hx | hx)
   · exact (hf x hx).contDiffAt (hs.mem_nhds hx) |>.contDiffWithinAt
   · exact (hf' x hx).contDiffAt (ht.mem_nhds hx) |>.contDiffWithinAt
 
