feat: (if P then 1 else 0) • a (#8347)

Two simple lemmas, `smul_ite_zero`, and `ite_smul_zero`.
Also delete `Finset.sum_univ_ite` since it is now provable by `simp` thanks to these.

Rename and turn around the following to match the direction that `simp` goes in:
* `ite_mul_zero_left` → `ite_zero_mul`
* `ite_mul_zero_right` → `mul_ite_zero`
* `ite_and_mul_zero` → `ite_zero_mul_ite_zero`

Mathlib/Algebra/Ring/Defs.lean

@@ -213,6 +213,21 @@ theorem ite_mul {α} [Mul α] (P : Prop) [Decidable P] (a b c : α) :
 -- `mul_ite` and `ite_mul`.
 attribute [simp] mul_ite ite_mul
 
+section MulZeroClass
+variable [MulZeroClass α] (P Q : Prop) [Decidable P] [Decidable Q] (a b : α)
+
+lemma ite_zero_mul : ite P a 0 * b = ite P (a * b) 0 := by simp
+#align ite_mul_zero_left ite_zero_mul
+
+lemma mul_ite_zero : a * ite P b 0 = ite P (a * b) 0 := by simp
+#align ite_mul_zero_right mul_ite_zero
+
+lemma ite_zero_mul_ite_zero : ite P a 0 * ite Q b 0 = ite (P ∧ Q) (a * b) 0 := by
+  simp only [← ite_and, ite_mul, mul_ite, mul_zero, zero_mul, and_comm]
+#align ite_and_mul_zero ite_zero_mul_ite_zero
+
+end MulZeroClass
+
 -- Porting note: no @[simp] because simp proves it
 theorem mul_boole {α} [MulZeroOneClass α] (P : Prop) [Decidable P] (a : α) :
     (a * if P then 1 else 0) = if P then a else 0 := by simp
@@ -223,19 +238,6 @@ theorem boole_mul {α} [MulZeroOneClass α] (P : Prop) [Decidable P] (a : α) :
     (if P then 1 else 0) * a = if P then a else 0 := by simp
 #align boole_mul boole_mul
 
-theorem ite_mul_zero_left {α : Type*} [MulZeroClass α] (P : Prop) [Decidable P] (a b : α) :
-    ite P (a * b) 0 = ite P a 0 * b := by by_cases h : P <;> simp [h]
-#align ite_mul_zero_left ite_mul_zero_left
-
-theorem ite_mul_zero_right {α : Type*} [MulZeroClass α] (P : Prop) [Decidable P] (a b : α) :
-    ite P (a * b) 0 = a * ite P b 0 := by by_cases h : P <;> simp [h]
-#align ite_mul_zero_right ite_mul_zero_right
-
-theorem ite_and_mul_zero {α : Type*} [MulZeroClass α] (P Q : Prop) [Decidable P] [Decidable Q]
-    (a b : α) : ite (P ∧ Q) (a * b) 0 = ite P a 0 * ite Q b 0 := by
-  simp only [← ite_and, ite_mul, mul_ite, mul_zero, zero_mul, and_comm]
-#align ite_and_mul_zero ite_and_mul_zero
-
 /-- A not-necessarily-unital, not-necessarily-associative, but commutative semiring. -/
 class NonUnitalNonAssocCommSemiring (α : Type u) extends NonUnitalNonAssocSemiring α, CommMagma α
 

Mathlib/Algebra/SMulWithZero.lean

@@ -176,7 +176,13 @@ protected lemma MulActionWithZero.nontrivial
 #align mul_action_with_zero.nontrivial MulActionWithZero.nontrivial
 
 variable {R M}
-variable [MulActionWithZero R M] [Zero M'] [SMul R M']
+variable [MulActionWithZero R M] [Zero M'] [SMul R M'] (p : Prop) [Decidable p]
+
+@[simp]
+lemma ite_zero_smul (a : R) (b : M) : (if p then a else 0 : R) • b = if p then a • b else 0 := by
+  rw [ite_smul, zero_smul]
+
+lemma boole_smul (a : M) : (if p then 1 else 0 : R) • a = if p then a else 0 := by simp
 
 /-- Pullback a `MulActionWithZero` structure along an injective zero-preserving homomorphism.
 See note [reducible non-instances]. -/

Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean

@@ -77,7 +77,7 @@ variable [MulZeroOneClass R] {a b : α} {e : Sym2 α}
 
 theorem incMatrix_apply_mul_incMatrix_apply : G.incMatrix R a e * G.incMatrix R b e =
     (G.incidenceSet a ∩ G.incidenceSet b).indicator 1 e := by
-  classical simp only [incMatrix, Set.indicator_apply, ← ite_and_mul_zero, Pi.one_apply, mul_one,
+  classical simp only [incMatrix, Set.indicator_apply, ite_zero_mul_ite_zero, Pi.one_apply, mul_one,
     Set.mem_inter_iff]
 #align simple_graph.inc_matrix_apply_mul_inc_matrix_apply SimpleGraph.incMatrix_apply_mul_incMatrix_apply
 
@@ -150,7 +150,7 @@ theorem sum_incMatrix_apply_of_not_mem_edgeSet (h : e ∉ G.edgeSet) :
 theorem incMatrix_transpose_mul_diag [DecidableRel G.Adj] :
     ((G.incMatrix R)ᵀ * G.incMatrix R) e e = if e ∈ G.edgeSet then 2 else 0 := by
   classical
-    simp only [Matrix.mul_apply, incMatrix_apply', transpose_apply, ← ite_and_mul_zero, one_mul,
+    simp only [Matrix.mul_apply, incMatrix_apply', transpose_apply, ite_zero_mul_ite_zero, one_mul,
       sum_boole, and_self_iff]
     split_ifs with h
     · revert h

Mathlib/GroupTheory/GroupAction/Defs.lean

@@ -733,6 +733,10 @@ theorem smul_zero (a : M) : a • (0 : A) = 0 :=
   SMulZeroClass.smul_zero _
 #align smul_zero smul_zero
 
+@[simp]
+lemma smul_ite_zero (p : Prop) [Decidable p] (a : M) (b : A) :
+    (a • if p then b else 0) = if p then a • b else 0 := by rw [smul_ite, smul_zero]
+
 /-- Pullback a zero-preserving scalar multiplication along an injective zero-preserving map.
 See note [reducible non-instances]. -/
 @[reducible]

Mathlib/LinearAlgebra/FinsuppVectorSpace.lean

@@ -180,12 +180,6 @@ theorem _root_.Finset.sum_single_ite (a : R) (i : n) :
   simp [hx']
 #align finset.sum_single_ite Finset.sum_single_ite
 
--- Porting note: LHS of equivFun_symm_stdBasis simplifies to this
-@[simp]
-theorem _root_.Finset.sum_univ_ite (b : n → M) (i : n) :
-    (Finset.sum Finset.univ fun (x : n) => (if i = x then (1:R) else 0) • b x) = b i := by
-  simp only [ite_smul, zero_smul, one_smul, Finset.sum_ite_eq, Finset.mem_univ, ite_true]
-
 theorem equivFun_symm_stdBasis (b : Basis n R M) (i : n) :
     b.equivFun.symm (LinearMap.stdBasis R (fun _ => R) i 1) = b i := by
   simp

Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean

@@ -84,9 +84,8 @@ theorem Basis.parallelepiped_eq_map  {ι E : Type*} [Fintype ι] [NormedAddCommG
       b.equivFunL.symm.continuous b.equivFunL.symm.isOpenMap := by
   classical
   rw [← Basis.parallelepiped_basisFun, ← Basis.parallelepiped_map]
-  congr
-  ext; simp only [map_apply, Pi.basisFun_apply, equivFun_symm_apply, LinearMap.stdBasis_apply',
-    Finset.sum_univ_ite]
+  congr with x
+  simp
 
 open MeasureTheory MeasureTheory.Measure
 

Mathlib/NumberTheory/ArithmeticFunction.lean

@@ -1042,15 +1042,9 @@ theorem moebius_apply_isPrimePow_not_prime {n : ℕ} (hn : IsPrimePow n) (hn' :
 theorem isMultiplicative_moebius : IsMultiplicative μ := by
   rw [IsMultiplicative.iff_ne_zero]
   refine' ⟨by simp, fun {n m} hn hm hnm => _⟩
-  -- porting note: the rest of this proof was a single `simp only` with all the lemmas thrown in
-  -- followed by the last `rw`.
-  simp only [moebius, ZeroHom.coe_mk]
-  dsimp only [coe_mk, ZeroHom.toFun_eq_coe, Eq.ndrec, ZeroHom.coe_mk]
-  simp only [IsUnit.mul_iff, Nat.isUnit_iff, squarefree_mul hnm, ite_and, mul_ite, ite_mul,
-    zero_mul, mul_zero]
-  rw [cardFactors_mul hn hm, pow_add, ite_mul_zero_left, ite_mul_zero_right]
-  split_ifs <;>  -- porting note: added
-  simp           -- porting note: added
+  simp only [moebius, ZeroHom.coe_mk, coe_mk, ZeroHom.toFun_eq_coe, Eq.ndrec, ZeroHom.coe_mk,
+    IsUnit.mul_iff, Nat.isUnit_iff, squarefree_mul hnm, ite_zero_mul_ite_zero,
+    cardFactors_mul hn hm, pow_add]
 #align nat.arithmetic_function.is_multiplicative_moebius Nat.ArithmeticFunction.isMultiplicative_moebius
 
 open UniqueFactorizationMonoid

Mathlib/NumberTheory/RamificationInertia.lean

@@ -333,8 +333,8 @@ theorem FinrankQuotientMap.span_eq_top [IsDomain R] [IsDomain S] [Algebra K L] [
   let B := A.adjugate
   have A_smul : ∀ i, ∑ j, A i j • a j = 0 := by
     intros
-    simp only [Matrix.sub_apply, Matrix.of_apply, ne_eq, Matrix.one_apply, sub_smul,
-      Finset.sum_sub_distrib, hA', Finset.sum_univ_ite, sub_self]
+    simp [Matrix.sub_apply, Matrix.of_apply, ne_eq, Matrix.one_apply, sub_smul,
+      Finset.sum_sub_distrib, hA', sub_self]
   -- since `span S {det A} / M = 0`.
   have d_smul : ∀ i, A.det • a i = 0 := by
     intro i

Mathlib/RingTheory/PolynomialAlgebra.lean

@@ -103,8 +103,8 @@ theorem toFunLinear_mul_tmul_mul (a₁ a₂ : A) (p₁ p₂ : R[X]) :
     conv_rhs => rw [coeff_mul]
     simp_rw [finset_sum_coeff, coeff_monomial, Finset.sum_ite_eq', mem_support_iff, Ne.def, mul_ite,
       mul_zero, ite_mul, zero_mul]
-    simp_rw [ite_mul_zero_left (¬coeff p₁ _ = 0) (a₁ * (algebraMap R A) (coeff p₁ _))]
-    simp_rw [ite_mul_zero_right (¬coeff p₂ _ = 0) _ (_ * _)]
+    simp_rw [←ite_zero_mul (¬coeff p₁ _ = 0) (a₁ * (algebraMap R A) (coeff p₁ _))]
+    simp_rw [←mul_ite_zero (¬coeff p₂ _ = 0) _ (_ * _)]
     simp_rw [toFunLinear_mul_tmul_mul_aux_1, toFunLinear_mul_tmul_mul_aux_2]
 #align poly_equiv_tensor.to_fun_linear_mul_tmul_mul PolyEquivTensor.toFunLinear_mul_tmul_mul