From 635d083b2ba3efd679778c265548039ece704dc0 Mon Sep 17 00:00:00 2001
From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date: Wed, 24 May 2023 15:38:45 +0000
Subject: [PATCH] chore: restore simp tag for
 BoxIntegral.BoxAdditiveMap.map_split_add (#4294)

---
 Mathlib/Analysis/BoxIntegral/Partition/Additive.lean | 2 +-
 Mathlib/Data/Option/Defs.lean                        | 6 +++++-
 2 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Analysis/BoxIntegral/Partition/Additive.lean b/Mathlib/Analysis/BoxIntegral/Partition/Additive.lean
index 0baff9b6de200a..095035e9cc9714 100644
--- a/Mathlib/Analysis/BoxIntegral/Partition/Additive.lean
+++ b/Mathlib/Analysis/BoxIntegral/Partition/Additive.lean
@@ -109,7 +109,7 @@ instance {R} [Monoid R] [DistribMulAction R M] : SMul R (ι →ᵇᵃ[I₀] M) :
 instance : AddCommMonoid (ι →ᵇᵃ[I₀] M) :=
   Function.Injective.addCommMonoid _ coe_injective rfl (fun _ _ => rfl) fun _ _ => rfl
 
--- Porting note: LHS not in simp normal form due to Option.elim' @[simp]
+@[simp]
 theorem map_split_add (f : ι →ᵇᵃ[I₀] M) (hI : ↑I ≤ I₀) (i : ι) (x : ℝ) :
     (I.splitLower i x).elim' 0 f + (I.splitUpper i x).elim' 0 f = f I := by
   rw [← f.sum_partition_boxes hI (isPartitionSplit I i x), sum_split_boxes]
diff --git a/Mathlib/Data/Option/Defs.lean b/Mathlib/Data/Option/Defs.lean
index 8c3b816bd95937..6173e13a60cdd8 100644
--- a/Mathlib/Data/Option/Defs.lean
+++ b/Mathlib/Data/Option/Defs.lean
@@ -60,12 +60,16 @@ variable {α : Type _} {β : Type _}
 -- attribute [inline] Option.isSome Option.isNone
 
 /-- An elimination principle for `Option`. It is a nondependent version of `Option.rec`. -/
-@[simp]
 protected def elim' (b : β) (f : α → β) : Option α → β
   | some a => f a
   | none => b
 #align option.elim Option.elim'
 
+@[simp]
+theorem elim'_none (b : β) (f : α → β) : Option.elim' b f none = b := rfl
+@[simp]
+theorem elim'_some (b : β) (f : α → β) : Option.elim' b f (some a) = f a := rfl
+
 theorem mem_some_iff {α : Type _} {a b : α} : a ∈ some b ↔ b = a := by simp
 #align option.mem_some_iff Option.mem_some_iff