feat(Algebra/GroupPower): Miscellaneous lemmas (#9388)

Generalise `pow_ite`/`ite_pow` and give a version of `pow_add_pow_le` that doesn't require the exponent to be nonzero.

From LeanAPAP

Mathlib/Algebra/Group/Basic.lean

@@ -4,8 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Simon Hudon, Mario Carneiro
 -/
 import Mathlib.Algebra.Group.Defs
-import Mathlib.Tactic.SimpRw
 import Mathlib.Tactic.Cases
+import Mathlib.Tactic.SimpRw
+import Mathlib.Tactic.SplitIfs
 
 #align_import algebra.group.basic from "leanprover-community/mathlib"@"a07d750983b94c530ab69a726862c2ab6802b38c"
 
@@ -1055,3 +1056,27 @@ theorem multiplicative_of_isTotal (p : α → Prop) (hswap : ∀ {a b}, p a →
   exacts [⟨pa, pb⟩, ⟨pb, pc⟩, ⟨pa, pc⟩]
 #align multiplicative_of_is_total multiplicative_of_isTotal
 #align additive_of_is_total additive_of_isTotal
+
+section ite
+variable {α β : Type*} [Pow α β]
+
+@[to_additive (attr := simp) dite_smul]
+lemma pow_dite (p : Prop) [Decidable p] (a : α) (b : p → β) (c : ¬ p → β) :
+    a ^ (if h : p then b h else c h) = if h : p then a ^ b h else a ^ c h := by split_ifs <;> rfl
+
+@[to_additive (attr := simp) smul_dite]
+lemma dite_pow (p : Prop) [Decidable p] (a : p → α) (b : ¬ p → α) (c : β) :
+    (if h : p then a h else b h) ^ c = if h : p then a h ^ c else b h ^ c := by split_ifs <;> rfl
+
+@[to_additive (attr := simp) ite_smul]
+lemma pow_ite (p : Prop) [Decidable p] (a : α) (b c : β) :
+    a ^ (if p then b else c) = if p then a ^ b else a ^ c := pow_dite _ _ _ _
+
+@[to_additive (attr := simp) smul_ite]
+lemma ite_pow (p : Prop) [Decidable p] (a b : α) (c : β) :
+    (if p then a else b) ^ c = if p then a ^ c else b ^ c := dite_pow _ _ _ _
+
+set_option linter.existingAttributeWarning false in
+attribute [to_additive (attr := simp)] dite_smul smul_dite ite_smul smul_ite
+
+end ite

Mathlib/Algebra/GroupPower/Basic.lean

@@ -43,24 +43,6 @@ First we prove some facts about `SemiconjBy` and `Commute`. They do not require
 `pow` and/or `nsmul` and will be useful later in this file.
 -/
 
-
-section Pow
-
-variable [Pow M ℕ]
-
-@[to_additive (attr := simp) ite_nsmul]
-theorem pow_ite (P : Prop) [Decidable P] (a : M) (b c : ℕ) :
-    (a ^ if P then b else c) = if P then a ^ b else a ^ c := by split_ifs <;> rfl
-#align pow_ite pow_ite
-
-@[to_additive (attr := simp) nsmul_ite]
-theorem ite_pow (P : Prop) [Decidable P] (a b : M) (c : ℕ) :
-    (if P then a else b) ^ c = if P then a ^ c else b ^ c := by split_ifs <;> rfl
-#align ite_pow ite_pow
-
-end Pow
-
-
 /-!
 ### Monoids
 -/

Mathlib/Algebra/GroupPower/Order.lean

@@ -35,7 +35,7 @@ end CanonicallyOrderedCommSemiring
 
 section OrderedSemiring
 
-variable [OrderedSemiring R] {a x y : R} {n m : ℕ}
+variable [OrderedSemiring R] {a b x y : R} {n m : ℕ}
 
 theorem zero_pow_le_one : ∀ n : ℕ, (0 : R) ^ n ≤ 1
   | 0 => (pow_zero _).le
@@ -113,6 +113,11 @@ theorem one_lt_pow (ha : 1 < a) : ∀ {n : ℕ} (_ : n ≠ 0), 1 < a ^ n
     exact one_lt_mul_of_lt_of_le ha (one_le_pow_of_one_le ha.le _)
 #align one_lt_pow one_lt_pow
 
+lemma pow_add_pow_le' (ha : 0 ≤ a) (hb : 0 ≤ b) : a ^ n + b ^ n ≤ 2 * (a + b) ^ n := by
+  rw [two_mul]
+  exact add_le_add (pow_le_pow_left ha (le_add_of_nonneg_right hb) _)
+    (pow_le_pow_left hb (le_add_of_nonneg_left ha) _)
+
 end OrderedSemiring
 
 section StrictOrderedSemiring

Mathlib/Algebra/SMulWithZero.lean

@@ -178,7 +178,6 @@ protected lemma MulActionWithZero.nontrivial
 variable {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]
 

Mathlib/Analysis/Convex/Combination.lean

@@ -513,15 +513,13 @@ to prove that this map is linear. -/
 theorem Set.Finite.convexHull_eq_image {s : Set E} (hs : s.Finite) : convexHull R s =
     haveI := hs.fintype
     (⇑(∑ x : s, (@LinearMap.proj R s _ (fun _ => R) _ _ x).smulRight x.1)) '' stdSimplex R s := by
-  -- Porting note: Original proof didn't need to specify `hs.fintype`
-  rw [← @convexHull_basis_eq_stdSimplex _ _ _ hs.fintype, ← LinearMap.convexHull_image,
-    ← Set.range_comp]
-  simp_rw [Function.comp]
+  letI := hs.fintype
+  rw [← convexHull_basis_eq_stdSimplex, ← LinearMap.convexHull_image, ← Set.range_comp]
   apply congr_arg
+  simp_rw [Function.comp]
   convert Subtype.range_coe.symm
-  -- Porting note: Original proof didn't need to specify `hs.fintype` and `(1 : R)`
-  simp [LinearMap.sum_apply, ite_smul _ (1 : R), Finset.filter_eq,
-    @Finset.mem_univ _ hs.fintype _]
+  -- Porting note: Original proof didn't need to specify `(1 : R)`
+  simp [LinearMap.sum_apply, ite_smul _ _ (1 : R), Finset.filter_eq, Finset.mem_univ]
 #align set.finite.convex_hull_eq_image Set.Finite.convexHull_eq_image
 
 /-- All values of a function `f ∈ stdSimplex 𝕜 ι` belong to `[0, 1]`. -/

Mathlib/GroupTheory/GroupAction/Defs.lean

@@ -458,24 +458,6 @@ theorem Commute.smul_left [Mul α] [SMulCommClass M α α] [IsScalarTower M α 
 
 end
 
-section ite
-
-variable [SMul M α] (p : Prop) [Decidable p]
-
-@[to_additive]
-theorem ite_smul (a₁ a₂ : M) (b : α) : ite p a₁ a₂ • b = ite p (a₁ • b) (a₂ • b) := by
-  split_ifs <;> rfl
-#align ite_smul ite_smul
-#align ite_vadd ite_vadd
-
-@[to_additive]
-theorem smul_ite (a : M) (b₁ b₂ : α) : a • ite p b₁ b₂ = ite p (a • b₁) (a • b₂) := by
-  split_ifs <;> rfl
-#align smul_ite smul_ite
-#align vadd_ite vadd_ite
-
-end ite
-
 section
 
 variable [Monoid M] [MulAction M α]
@@ -742,9 +724,8 @@ 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]
+    (a • if p then b else 0) = if p then a • b else 0 := by split_ifs <;> simp
 
 /-- Pullback a zero-preserving scalar multiplication along an injective zero-preserving map.
 See note [reducible non-instances]. -/