chore(algebra/*/pi): add missing lemmas about function.update and set…

….piecewise (#9935)

This adds `function.update_{zero,one,add,mul,sub,div,neg,inv,smul,vadd}`, and moves `pi.piecewise_{sub,div,neg,inv}` into the `set` namespace to match `set.piecewise_{add,mul}`.

This also adds `finset.piecewise_erase_univ`, as this is tangentially related.

src/algebra/group/pi.lean

@@ -245,6 +245,33 @@ end
 
 end single
 
+namespace function
+
+@[simp, to_additive]
+lemma update_one [Π i, has_one (f i)] [decidable_eq I] (i : I) :
+  update (1 : Π i, f i) i 1 = 1 :=
+update_eq_self i 1
+
+@[to_additive]
+lemma update_mul [Π i, has_mul (f i)] [decidable_eq I]
+  (f₁ f₂ : Π i, f i) (i : I) (x₁ : f i) (x₂ : f i) :
+  update (f₁ * f₂) i (x₁ * x₂) = update f₁ i x₁ * update f₂ i x₂ :=
+funext $ λ j, (apply_update₂ (λ i, (*)) f₁ f₂ i x₁ x₂ j).symm
+
+@[to_additive]
+lemma update_inv [Π i, has_inv (f i)] [decidable_eq I]
+  (f₁ : Π i, f i) (i : I) (x₁ : f i) :
+  update (f₁⁻¹) i (x₁⁻¹) = (update f₁ i x₁)⁻¹ :=
+funext $ λ j, (apply_update (λ i, has_inv.inv) f₁ i x₁ j).symm
+
+@[to_additive]
+lemma update_div [Π i, has_div (f i)] [decidable_eq I]
+  (f₁ f₂ : Π i, f i) (i : I) (x₁ : f i) (x₂ : f i) :
+  update (f₁ / f₂) i (x₁ / x₂) = update f₁ i x₁ / update f₂ i x₂ :=
+funext $ λ j, (apply_update₂ (λ i, (/)) f₁ f₂ i x₁ x₂ j).symm
+
+end function
+
 section piecewise
 
 @[to_additive]
@@ -254,13 +281,13 @@ lemma set.piecewise_mul [Π i, has_mul (f i)] (s : set I) [Π i, decidable (i 
 s.piecewise_op₂ _ _ _ _ (λ _, (*))
 
 @[to_additive]
-lemma pi.piecewise_inv [Π i, has_inv (f i)] (s : set I) [Π i, decidable (i ∈ s)]
+lemma set.piecewise_inv [Π i, has_inv (f i)] (s : set I) [Π i, decidable (i ∈ s)]
   (f₁ g₁ : Π i, f i) :
   s.piecewise (f₁⁻¹) (g₁⁻¹) = (s.piecewise f₁ g₁)⁻¹ :=
 s.piecewise_op f₁ g₁ (λ _ x, x⁻¹)
 
 @[to_additive]
-lemma pi.piecewise_div [Π i, has_div (f i)] (s : set I) [Π i, decidable (i ∈ s)]
+lemma set.piecewise_div [Π i, has_div (f i)] (s : set I) [Π i, decidable (i ∈ s)]
   (f₁ f₂ g₁ g₂ : Π i, f i) :
   s.piecewise (f₁ / f₂) (g₁ / g₂) = s.piecewise f₁ g₁ / s.piecewise f₂ g₂ :=
 s.piecewise_op₂ _ _ _ _ (λ _, (/))

src/algebra/module/pi.lean

@@ -13,12 +13,13 @@ import algebra.ring.pi
 This file defines instances for module, mul_action and related structures on Pi Types
 -/
 
-namespace pi
 universes u v w
 variable {I : Type u}     -- The indexing type
 variable {f : I → Type v} -- The family of types already equipped with instances
 variables (x y : Π i, f i) (i : I)
 
+namespace pi
+
 @[to_additive pi.has_vadd]
 instance has_scalar {α : Type*} [Π i, has_scalar α $ f i] :
   has_scalar α (Π i : I, f i) :=
@@ -202,6 +203,26 @@ instance (α) {r : semiring α} {m : Π i, add_comm_monoid $ f i}
 
 end pi
 
+namespace function
+
+@[to_additive]
+lemma update_smul {α : Type*} [Π i, has_scalar α (f i)] [decidable_eq I]
+  (c : α) (f₁ : Π i, f i) (i : I) (x₁ : f i) :
+  update (c • f₁) i (c • x₁) = c • update f₁ i x₁ :=
+funext $ λ j, (apply_update (λ i, (•) c) f₁ i x₁ j).symm
+
+end function
+
+namespace set
+
+@[to_additive]
+lemma piecewise_smul {α : Type*} [Π i, has_scalar α (f i)] (s : set I) [Π i, decidable (i ∈ s)]
+  (c : α) (f₁ g₁ : Π i, f i) :
+  s.piecewise (c • f₁) (c • g₁) = c • s.piecewise f₁ g₁ :=
+s.piecewise_op _ _ (λ _, (•) c)
+
+end set
+
 section extend
 
 @[to_additive]

src/data/fintype/basic.lean

@@ -145,6 +145,9 @@ by simp [ext_iff]
 lemma compl_ne_univ_iff_nonempty [decidable_eq α] (s : finset α) : sᶜ ≠ univ ↔ s.nonempty :=
 by simp [eq_univ_iff_forall, finset.nonempty]
 
+lemma compl_singleton [decidable_eq α] (a : α) : ({a} : finset α)ᶜ = univ.erase a :=
+by rw [compl_eq_univ_sdiff, sdiff_singleton_eq_erase]
+
 @[simp] lemma univ_inter [decidable_eq α] (s : finset α) :
   univ ∩ s = s := ext $ λ a, by simp
 
@@ -161,6 +164,10 @@ lemma piecewise_compl [decidable_eq α] (s : finset α) [Π i : α, decidable (i
   sᶜ.piecewise f g = s.piecewise g f :=
 by { ext i, simp [piecewise] }
 
+@[simp] lemma piecewise_erase_univ {δ : α → Sort*} [decidable_eq α] (a : α) (f g : Π a, δ a) :
+  (finset.univ.erase a).piecewise f g = function.update f a (g a) :=
+by rw [←compl_singleton, piecewise_compl, piecewise_singleton]
+
 lemma univ_map_equiv_to_embedding {α β : Type*} [fintype α] [fintype β] (e : α ≃ β) :
   univ.map e.to_embedding = univ :=
 eq_univ_iff_forall.mpr (λ b, mem_map.mpr ⟨e.symm b, mem_univ _, by simp⟩)

src/logic/function/basic.lean

@@ -443,6 +443,15 @@ begin
   { simp [h] }
 end
 
+lemma apply_update₂ {ι : Sort*} [decidable_eq ι] {α β γ : ι → Sort*}
+  (f : Π i, α i → β i → γ i) (g : Π i, α i) (h : Π i, β i) (i : ι) (v : α i) (w : β i) (j : ι) :
+  f j (update g i v j) (update h i w j) = update (λ k, f k (g k) (h k)) i (f i v w) j :=
+begin
+  by_cases h : j = i,
+  { subst j, simp },
+  { simp [h] }
+end
+
 lemma comp_update {α' : Sort*} {β : Sort*} (f : α' → β) (g : α → α') (i : α) (v : α') :
   f ∘ (update g i v) = update (f ∘ g) i (f v) :=
 funext $ apply_update _ _ _ _