chore: restore simp tag for BoxIntegral.BoxAdditiveMap.map_split_add (#…

…4294)
leanprover-community · May 24, 2023 · 635d083 · 635d083
1 parent a45230d
commit 635d083
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 2 deletions.
diff --git 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
@@ -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