feat(data/pi): bit[01]_apply simp lemmas (#11086)

leanprover-community · Dec 28, 2021 · f452b38 · f452b38
1 parent 94bb466
commit f452b38
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/src/data/pi.lean b/src/data/pi.lean
@@ -55,6 +55,10 @@ instance has_mul [∀ i, has_mul $ f i] :
 @[to_additive] lemma mul_comp [has_mul γ] (x y : β → γ) (z : α → β) :
   (x * y) ∘ z = x ∘ z * y ∘ z := rfl
 
+@[simp] lemma bit0_apply [Π i, has_add $ f i] : (bit0 x) i = bit0 (x i) := rfl
+
+@[simp] lemma bit1_apply [Π i, has_add $ f i] [Π i, has_one $ f i] : (bit1 x) i = bit1 (x i) := rfl
+
 @[to_additive] instance has_inv [∀ i, has_inv $ f i] :
   has_inv (Π i : I, f i) :=
   ⟨λ f i, (f i)⁻¹⟩