feat(data/pi): Composition of addition/subtraction/... of functions (#10305)

Author: YaelDillies

src/algebra/group/pi.lean

@@ -124,19 +124,6 @@ instance comm_monoid_with_zero [∀ i, comm_monoid_with_zero $ f i] :
 by refine_struct { zero := (0 : Π i, f i), one := (1 : Π i, f i), mul := (*),
   npow := monoid.npow }; tactic.pi_instance_derive_field
 
-section instance_lemmas
-open function
-
-variables {α β γ : Type*}
-
-@[simp, to_additive] lemma const_one [has_one β] : const α (1 : β) = 1 := rfl
-
-@[simp, to_additive] lemma comp_one [has_one β] {f : β → γ} : f ∘ 1 = const α (f 1) := rfl
-
-@[simp, to_additive] lemma one_comp [has_one γ] {f : α → β} : (1 : β → γ) ∘ f = 1 := rfl
-
-end instance_lemmas
-
 end pi
 
 section monoid_hom

src/data/pi.lean

@@ -15,8 +15,11 @@ This file provides basic definitions and notation instances for Pi types.
 Instances of more sophisticated classes are defined in `pi.lean` files elsewhere.
 -/
 
+open function
+
 universes u v₁ v₂ v₃
 variable {I : Type u}     -- The indexing type
+variables {α β γ : Type*}
 -- The families of types already equipped with instances
 variables {f : I → Type v₁} {g : I → Type v₂} {h : I → Type v₃}
 variables (x y : Π i, f i) (i : I)
@@ -32,6 +35,12 @@ namespace pi
 
 @[to_additive] lemma one_def [Π i, has_one $ f i] : (1 : Π i, f i) = λ i, 1 := rfl
 
+@[simp, to_additive] lemma const_one [has_one β] : const α (1 : β) = 1 := rfl
+
+@[simp, to_additive] lemma one_comp [has_one γ] (x : α → β) : (1 : β → γ) ∘ x = 1 := rfl
+
+@[simp, to_additive] lemma comp_one [has_one β] (x : β → γ) : x ∘ 1 = const α (x 1) := rfl
+
 @[to_additive]
 instance has_mul [∀ i, has_mul $ f i] :
   has_mul (Π i : I, f i) :=
@@ -40,18 +49,34 @@ instance has_mul [∀ i, has_mul $ f i] :
 
 @[to_additive] lemma mul_def [Π i, has_mul $ f i] : x * y = λ i, x i * y i := rfl
 
+@[simp, to_additive] lemma const_mul [has_mul β] (a b : β) :
+  const α a * const α b = const α (a * b) := rfl
+
+@[to_additive] lemma mul_comp [has_mul γ] (x y : β → γ) (z : α → β) :
+  (x * y) ∘ z = x ∘ z * y ∘ z := rfl
+
 @[to_additive] instance has_inv [∀ i, has_inv $ f i] :
   has_inv (Π i : I, f i) :=
   ⟨λ f i, (f i)⁻¹⟩
 @[simp, to_additive] lemma inv_apply [∀ i, has_inv $ f i] : x⁻¹ i = (x i)⁻¹ := rfl
 @[to_additive] lemma inv_def [Π i, has_inv $ f i] : x⁻¹ = λ i, (x i)⁻¹ := rfl
 
+@[to_additive] lemma const_inv [has_inv β] (a : β) : (const α a)⁻¹ = const α a⁻¹ := rfl
+
+@[to_additive] lemma inv_comp [has_inv γ] (x : β → γ) (y : α → β) : x⁻¹ ∘ y = (x ∘ y)⁻¹ := rfl
+
 @[to_additive] instance has_div [Π i, has_div $ f i] :
   has_div (Π i : I, f i) :=
 ⟨λ f g i, f i / g i⟩
 @[simp, to_additive] lemma div_apply [Π i, has_div $ f i] : (x / y) i = x i / y i := rfl
 @[to_additive] lemma div_def [Π i, has_div $ f i] : x / y = λ i, x i / y i := rfl
 
+@[to_additive] lemma div_comp [has_div γ] (x y : β → γ) (z : α → β) :
+  (x / y) ∘ z = x ∘ z / y ∘ z := rfl
+
+@[simp, to_additive] lemma const_div [has_div β] (a b : β) :
+  const α a / const α b = const α (a / b) := rfl
+
 section
 
 variables [decidable_eq I]
@@ -116,11 +141,8 @@ end
 end pi
 
 section extend
-
 namespace function
 
-variables {α β γ : Type*}
-
 @[to_additive]
 lemma extend_one [has_one γ] (f : α → β) :
   function.extend f (1 : α → γ) (1 : β → γ) = 1 :=