chore(data/real/cau_seq{_completion}): add lemmas about pow and smul (#…

…17796)

This also takes the opportunity to golf the algebraic instances, which should make porting easier.

src/data/real/cau_seq.lean

@@ -7,6 +7,8 @@ import algebra.group_power.lemmas
 import algebra.order.absolute_value
 import algebra.order.group.min_max
 import algebra.order.field.basic
+import algebra.ring.pi
+import group_theory.group_action.pi
 
 /-!
 # Cauchy sequences
@@ -249,17 +251,14 @@ instance : has_smul G (cau_seq β abv) :=
 @[simp, norm_cast] lemma smul_apply (a : G) (f : cau_seq β abv) (i : ℕ) : (a • f) i = a • f i := rfl
 lemma const_smul (a : G) (x : β) : const (a • x) = a • const x := rfl
 
+instance : is_scalar_tower G (cau_seq β abv) (cau_seq β abv) :=
+⟨λ a f g, subtype.ext $ smul_assoc a ⇑f ⇑g⟩
+
 end has_smul
 
 instance : add_group (cau_seq β abv) :=
-by refine_struct
-     { add := (+),
-       neg := has_neg.neg,
-       zero := (0 : cau_seq β abv),
-       sub := has_sub.sub,
-       zsmul := (•),
-       nsmul := (•) };
-intros; try { refl }; apply ext; simp [add_comm, add_left_comm, sub_eq_add_neg, add_mul]
+function.injective.add_group _ subtype.coe_injective
+  rfl coe_add coe_neg coe_sub (λ _ _, coe_smul _ _) (λ _ _, coe_smul _ _)
 
 instance : add_group_with_one (cau_seq β abv) :=
 { one := 1,
@@ -279,15 +278,9 @@ instance : has_pow (cau_seq β abv) ℕ :=
 lemma const_pow (x : β) (n : ℕ) : const (x ^ n) = const x ^ n := rfl
 
 instance : ring (cau_seq β abv) :=
-by refine_struct
-     { add := (+),
-       zero := (0 : cau_seq β abv),
-       mul := (*),
-       one := 1,
-       npow := λ n f, f ^ n,
-       .. cau_seq.add_group_with_one };
-intros; try { refl }; apply ext;
-simp [mul_add, mul_assoc, add_mul, add_comm, add_left_comm, sub_eq_add_neg, pow_succ]
+function.injective.ring _ subtype.coe_injective
+  rfl rfl coe_add coe_mul coe_neg coe_sub (λ _ _, coe_smul _ _) (λ _ _, coe_smul _ _) coe_pow
+  (λ _, rfl) (λ _, rfl)
 
 instance {β : Type*} [comm_ring β] {abv : β → α} [is_absolute_value abv] :
   comm_ring (cau_seq β abv) :=
@@ -437,6 +430,20 @@ lemma mul_equiv_mul {f1 f2 g1 g2 : cau_seq β abv} (hf : f1 ≈ f2) (hg : g1 ≈
 by simpa only [mul_sub, sub_mul, sub_add_sub_cancel]
   using add_lim_zero (mul_lim_zero_left g1 hf) (mul_lim_zero_right f2 hg)
 
+lemma smul_equiv_smul [has_smul G β] [is_scalar_tower G β β] {f1 f2 : cau_seq β abv}
+  (c : G) (hf : f1 ≈ f2) :
+  c • f1 ≈ c • f2 :=
+by simpa [const_smul, smul_one_mul _ _]
+  using mul_equiv_mul (const_equiv.mpr $ eq.refl $ c • 1) hf
+
+lemma pow_equiv_pow {f1 f2 : cau_seq β abv} (hf : f1 ≈ f2) (n : ℕ) :
+  f1 ^ n ≈ f2 ^ n :=
+begin
+  induction n with n ih,
+  { simp only [pow_zero, setoid.refl] },
+  { simpa only [pow_succ] using mul_equiv_mul hf ih, },
+end
+
 end ring
 
 section is_domain

src/data/real/cau_seq_completion.lean

@@ -63,6 +63,24 @@ instance : has_sub Cauchy :=
 
 @[simp] theorem mk_sub (f g : cau_seq β abv) : mk f - mk g = mk (f - g) := rfl
 
+instance {γ : Type*} [has_smul γ β] [is_scalar_tower γ β β] : has_smul γ Cauchy :=
+⟨λ c, quotient.map ((•) c) $ λ f₁ g₁ hf, smul_equiv_smul _ hf⟩
+
+@[simp] theorem mk_smul  {γ : Type*} [has_smul γ β] [is_scalar_tower γ β β] (c : γ)
+  (f : cau_seq β abv) :
+  c • mk f = mk (c • f) := rfl
+
+instance : has_pow Cauchy ℕ :=
+⟨λ x n, quotient.map (^ n) (λ f₁ g₁ hf, pow_equiv_pow hf _) x⟩
+
+@[simp] theorem mk_pow (n : ℕ) (f : cau_seq β abv) : mk f ^ n = mk (f ^ n) := rfl
+
+instance : has_nat_cast Cauchy := ⟨λ n, mk n⟩
+instance : has_int_cast Cauchy := ⟨λ n, mk n⟩
+
+@[simp] theorem of_rat_nat_cast (n : ℕ) : of_rat n = n := rfl
+@[simp] theorem of_rat_int_cast (z : ℤ) : of_rat z = z := rfl
+
 theorem of_rat_add (x y : β) : of_rat (x + y) = of_rat x + of_rat y :=
 congr_arg mk (const_add _ _)
 
@@ -76,30 +94,12 @@ private lemma zero_def : 0 = mk 0 := rfl
 
 private lemma one_def : 1 = mk 1 := rfl
 
-instance : add_group Cauchy :=
-by refine { add := (+), zero := (0 : Cauchy), sub := has_sub.sub, neg := has_neg.neg,
-  sub_eq_add_neg := _, nsmul := nsmul_rec, zsmul := zsmul_rec, .. }; try { intros; refl };
-{ repeat {refine λ a, quotient.induction_on a (λ _, _)},
-  simp [zero_def, add_comm, add_left_comm, sub_eq_neg_add] }
-
-instance : add_group_with_one Cauchy :=
-{ nat_cast := λ n, mk n,
-  nat_cast_zero := congr_arg mk nat.cast_zero,
-  nat_cast_succ := λ n, congr_arg mk (nat.cast_succ n),
-  int_cast := λ n, mk n,
-  int_cast_of_nat := λ n, congr_arg mk (int.cast_of_nat n),
-  int_cast_neg_succ_of_nat := λ n, congr_arg mk (int.cast_neg_succ_of_nat n),
-  one := 1,
-  .. Cauchy.add_group }
-
-@[simp] theorem of_rat_nat_cast (n : ℕ) : of_rat n = n := rfl
-@[simp] theorem of_rat_int_cast (z : ℤ) : of_rat z = z := rfl
-
 instance : ring Cauchy :=
-by refine { add := (+), zero := (0 : Cauchy), mul := (*), one := 1, npow := npow_rec,
-    .. Cauchy.add_group_with_one, .. }; try { intros; refl };
-{ repeat {refine λ a, quotient.induction_on a (λ _, _)},
-  simp [zero_def, one_def, mul_add, add_mul, add_comm, add_left_comm, sub_eq_add_neg, ←mul_assoc] }
+function.surjective.ring mk (surjective_quotient_mk _)
+  zero_def.symm one_def.symm (λ _ _, (mk_add _ _).symm) (λ _ _, (mk_mul _ _).symm)
+  (λ _, (mk_neg _).symm) (λ _ _, (mk_sub _ _).symm)
+  (λ _ _, (mk_smul _ _).symm) (λ _ _, (mk_smul _ _).symm)
+  (λ _ _, (mk_pow _ _).symm) (λ _, rfl) (λ _, rfl)
 
 /-- `cau_seq.completion.of_rat` as a `ring_hom`  -/
 @[simps]
@@ -121,8 +121,11 @@ parameters {β : Type*} [comm_ring β] {abv : β → α} [is_absolute_value abv]
 local notation `Cauchy` := @Cauchy _ _ _ _ abv _
 
 instance : comm_ring Cauchy :=
-{ mul_comm := quotient.ind₂ $ by exact λ a b, congr_arg quotient.mk $ mul_comm a b,
-  ..Cauchy.ring }
+function.surjective.comm_ring mk (surjective_quotient_mk _)
+  zero_def.symm one_def.symm (λ _ _, (mk_add _ _).symm) (λ _ _, (mk_mul _ _).symm)
+  (λ _, (mk_neg _).symm) (λ _ _, (mk_sub _ _).symm)
+  (λ _ _, (mk_smul _ _).symm) (λ _ _, (mk_smul _ _).symm)
+  (λ _ _, (mk_pow _ _).symm) (λ _, rfl) (λ _, rfl)
 
 end