chore(data/real/cau_seq_completion): remove use of parameters (#18122)

This helps with porting

src/data/real/basic.lean

@@ -25,7 +25,7 @@ open_locale pointwise
 /-- The type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
 numbers. -/
 structure real := of_cauchy ::
-(cauchy : @cau_seq.completion.Cauchy ℚ _ _ _ abs _)
+(cauchy : cau_seq.completion.Cauchy (abs : ℚ → ℚ))
 notation `ℝ` := real
 
 attribute [pp_using_anonymous_constructor] real
@@ -50,7 +50,7 @@ lemma ext_cauchy {x y : real} : x.cauchy = y.cauchy → x = y :=
 ext_cauchy_iff.2
 
 /-- The real numbers are isomorphic to the quotient of Cauchy sequences on the rationals. -/
-def equiv_Cauchy : ℝ ≃ cau_seq.completion.Cauchy :=
+def equiv_Cauchy : ℝ ≃ cau_seq.completion.Cauchy abs :=
 ⟨real.cauchy, real.of_cauchy, λ ⟨_⟩, rfl, λ _, rfl⟩
 
 -- irreducible doesn't work for instances: https://github.com/leanprover-community/lean/issues/511
@@ -88,7 +88,7 @@ lemma cauchy_inv : ∀ f, (f⁻¹ : ℝ).cauchy = f.cauchy⁻¹
 
 /-- `real.equiv_Cauchy` as a ring equivalence. -/
 @[simps]
-def ring_equiv_Cauchy : ℝ ≃+* cau_seq.completion.Cauchy :=
+def ring_equiv_Cauchy : ℝ ≃+* cau_seq.completion.Cauchy abs :=
 { to_fun := cauchy,
   inv_fun := of_cauchy,
   map_add' := cauchy_add,

src/data/real/cau_seq_completion.lean

@@ -16,85 +16,87 @@ namespace cau_seq.completion
 open cau_seq
 
 section
-parameters {α : Type*} [linear_ordered_field α]
-parameters {β : Type*} [ring β] {abv : β → α} [is_absolute_value abv]
+variables {α : Type*} [linear_ordered_field α]
+variables {β : Type*} [ring β] (abv : β → α) [is_absolute_value abv]
 
 /-- The Cauchy completion of a ring with absolute value. -/
 def Cauchy := @quotient (cau_seq _ abv) cau_seq.equiv
 
+variables {abv}
+
 /-- The map from Cauchy sequences into the Cauchy completion. -/
-def mk : cau_seq _ abv → Cauchy := quotient.mk
+def mk : cau_seq _ abv → Cauchy abv := quotient.mk
 
-@[simp] theorem mk_eq_mk (f) : @eq Cauchy ⟦f⟧ (mk f) := rfl
+@[simp] theorem mk_eq_mk (f) : @eq (Cauchy abv) ⟦f⟧ (mk f) := rfl
 
-theorem mk_eq {f g} : mk f = mk g ↔ f ≈ g := quotient.eq
+theorem mk_eq {f g : cau_seq _ abv} : mk f = mk g ↔ f ≈ g := quotient.eq
 
 /-- The map from the original ring into the Cauchy completion. -/
-def of_rat (x : β) : Cauchy := mk (const abv x)
+def of_rat (x : β) : Cauchy abv := mk (const abv x)
 
-instance : has_zero Cauchy := ⟨of_rat 0⟩
-instance : has_one Cauchy := ⟨of_rat 1⟩
-instance : inhabited Cauchy := ⟨0⟩
+instance : has_zero (Cauchy abv) := ⟨of_rat 0⟩
+instance : has_one (Cauchy abv) := ⟨of_rat 1⟩
+instance : inhabited (Cauchy abv) := ⟨0⟩
 
-theorem of_rat_zero : of_rat 0 = 0 := rfl
-theorem of_rat_one : of_rat 1 = 1 := rfl
+theorem of_rat_zero : (of_rat 0 : Cauchy abv) = 0 := rfl
+theorem of_rat_one : (of_rat 1 : Cauchy abv) = 1 := rfl
 
-@[simp] theorem mk_eq_zero {f} : mk f = 0 ↔ lim_zero f :=
+@[simp] theorem mk_eq_zero {f : cau_seq _ abv} : mk f = 0 ↔ lim_zero f :=
 by have : mk f = 0 ↔ lim_zero (f - 0) := quotient.eq;
    rwa sub_zero at this
 
-instance : has_add Cauchy :=
+instance : has_add (Cauchy abv) :=
 ⟨quotient.map₂ (+) $ λ f₁ g₁ hf f₂ g₂ hg, add_equiv_add hf hg⟩
 
 @[simp] theorem mk_add (f g : cau_seq β abv) : mk f + mk g = mk (f + g) := rfl
 
-instance : has_neg Cauchy :=
+instance : has_neg (Cauchy abv) :=
 ⟨quotient.map has_neg.neg $ λ f₁ f₂ hf, neg_equiv_neg hf⟩
 
 @[simp] theorem mk_neg (f : cau_seq β abv) : -mk f = mk (-f) := rfl
 
-instance : has_mul Cauchy :=
+instance : has_mul (Cauchy abv) :=
 ⟨quotient.map₂ (*) $ λ f₁ g₁ hf f₂ g₂ hg, mul_equiv_mul hf hg⟩
 
 @[simp] theorem mk_mul (f g : cau_seq β abv) : mk f * mk g = mk (f * g) := rfl
 
-instance : has_sub Cauchy :=
+instance : has_sub (Cauchy abv) :=
 ⟨quotient.map₂ has_sub.sub $ λ f₁ g₁ hf f₂ g₂ hg, sub_equiv_sub hf hg⟩
 
 @[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 :=
+instance {γ : Type*} [has_smul γ β] [is_scalar_tower γ β β] : has_smul γ (Cauchy abv) :=
 ⟨λ 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 ℕ :=
+instance : has_pow (Cauchy abv) ℕ :=
 ⟨λ 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⟩
+instance : has_nat_cast (Cauchy abv) := ⟨λ n, mk n⟩
+instance : has_int_cast (Cauchy abv) := ⟨λ 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
+@[simp] theorem of_rat_nat_cast (n : ℕ) : (of_rat n : Cauchy abv) = n := rfl
+@[simp] theorem of_rat_int_cast (z : ℤ) : (of_rat z : Cauchy abv) = z := rfl
 
-theorem of_rat_add (x y : β) : of_rat (x + y) = of_rat x + of_rat y :=
+theorem of_rat_add (x y : β) : of_rat (x + y) = (of_rat x + of_rat y : Cauchy abv) :=
 congr_arg mk (const_add _ _)
 
-theorem of_rat_neg (x : β) : of_rat (-x) = -of_rat x :=
+theorem of_rat_neg (x : β) : of_rat (-x) = (-of_rat x : Cauchy abv) :=
 congr_arg mk (const_neg _)
 
-theorem of_rat_mul (x y : β) : of_rat (x * y) = of_rat x * of_rat y :=
+theorem of_rat_mul (x y : β) : of_rat (x * y) = (of_rat x * of_rat y : Cauchy abv) :=
 congr_arg mk (const_mul _ _)
 
-private lemma zero_def : 0 = mk 0 := rfl
+private lemma zero_def : 0 = (mk 0 : Cauchy abv) := rfl
 
-private lemma one_def : 1 = mk 1 := rfl
+private lemma one_def : 1 = (mk 1 : Cauchy abv) := rfl
 
-instance : ring Cauchy :=
+instance : ring (Cauchy abv) :=
 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)
@@ -103,24 +105,23 @@ function.surjective.ring mk (surjective_quotient_mk _)
 
 /-- `cau_seq.completion.of_rat` as a `ring_hom`  -/
 @[simps]
-def of_rat_ring_hom : β →+* Cauchy :=
+def of_rat_ring_hom : β →+* Cauchy abv :=
 { to_fun := of_rat,
   map_zero' := of_rat_zero,
   map_one' := of_rat_one,
   map_add' := of_rat_add,
   map_mul' := of_rat_mul, }
 
-theorem of_rat_sub (x y : β) : of_rat (x - y) = of_rat x - of_rat y :=
+theorem of_rat_sub (x y : β) : of_rat (x - y) = (of_rat x - of_rat y : Cauchy abv) :=
 congr_arg mk (const_sub _ _)
 
 end
 
 section
-parameters {α : Type*} [linear_ordered_field α]
-parameters {β : Type*} [comm_ring β] {abv : β → α} [is_absolute_value abv]
-local notation `Cauchy` := @Cauchy _ _ _ _ abv _
+variables {α : Type*} [linear_ordered_field α]
+variables {β : Type*} [comm_ring β] {abv : β → α} [is_absolute_value abv]
 
-instance : comm_ring Cauchy :=
+instance : comm_ring (Cauchy abv) :=
 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)
@@ -132,15 +133,14 @@ end
 open_locale classical
 section
 
-parameters {α : Type*} [linear_ordered_field α]
-parameters {β : Type*} [division_ring β] {abv : β → α} [is_absolute_value abv]
-local notation `Cauchy` := @Cauchy _ _ _ _ abv _
+variables {α : Type*} [linear_ordered_field α]
+variables {β : Type*} [division_ring β] {abv : β → α} [is_absolute_value abv]
 
-instance : has_rat_cast Cauchy := ⟨λ q, of_rat q⟩
+instance : has_rat_cast (Cauchy abv) := ⟨λ q, of_rat q⟩
 
-@[simp] theorem of_rat_rat_cast (q : ℚ) : of_rat (↑q : β) = (q : Cauchy) := rfl
+@[simp] theorem of_rat_rat_cast (q : ℚ) : of_rat (↑q : β) = (q : Cauchy abv) := rfl
 
-noncomputable instance : has_inv Cauchy :=
+noncomputable instance : has_inv (Cauchy abv) :=
 ⟨λ x, quotient.lift_on x
   (λ f, mk $ if h : lim_zero f then 0 else inv f h) $
 λ f g fg, begin
@@ -156,7 +156,7 @@ noncomputable instance : has_inv Cauchy :=
         mul_assoc, Ig', mul_one] }
 end⟩
 
-@[simp] theorem inv_zero : (0 : Cauchy)⁻¹ = 0 :=
+@[simp] theorem inv_zero : (0 : Cauchy abv)⁻¹ = 0 :=
 congr_arg mk $ by rw dif_pos; [refl, exact zero_lim_zero]
 
 @[simp] theorem inv_mk {f} (hf) : (@mk α _ β _ abv _ f)⁻¹ = mk (inv f hf) :=
@@ -167,26 +167,26 @@ have lim_zero (1 - 0), from setoid.symm h,
 have lim_zero 1, by simpa,
 one_ne_zero $ const_lim_zero.1 this
 
-lemma zero_ne_one : (0 : Cauchy) ≠ 1 :=
+lemma zero_ne_one : (0 : Cauchy abv) ≠ 1 :=
 λ h, cau_seq_zero_ne_one $ mk_eq.1 h
 
-protected theorem inv_mul_cancel {x : Cauchy} : x ≠ 0 → x⁻¹ * x = 1 :=
+protected theorem inv_mul_cancel {x : Cauchy abv} : x ≠ 0 → x⁻¹ * x = 1 :=
 quotient.induction_on x $ λ f hf, begin
   simp at hf, simp [hf],
   exact quotient.sound (cau_seq.inv_mul_cancel hf)
 end
 
-protected theorem mul_inv_cancel {x : Cauchy} : x ≠ 0 → x * x⁻¹ = 1 :=
+protected theorem mul_inv_cancel {x : Cauchy abv} : x ≠ 0 → x * x⁻¹ = 1 :=
 quotient.induction_on x $ λ f hf, begin
   simp at hf, simp [hf],
   exact quotient.sound (cau_seq.mul_inv_cancel hf)
 end
 
-theorem of_rat_inv (x : β) : of_rat (x⁻¹) = ((of_rat x)⁻¹ : Cauchy) :=
+theorem of_rat_inv (x : β) : of_rat (x⁻¹) = ((of_rat x)⁻¹ : Cauchy abv) :=
 congr_arg mk $ by split_ifs with h; [simp [const_lim_zero.1 h], refl]
 
 /-- The Cauchy completion forms a division ring. -/
-noncomputable instance : division_ring Cauchy :=
+noncomputable instance : division_ring (Cauchy abv) :=
 { inv              := has_inv.inv,
   mul_inv_cancel   := λ x, cau_seq.completion.mul_inv_cancel,
   exists_pair_ne   := ⟨0, 1, zero_ne_one⟩,
@@ -196,28 +196,27 @@ noncomputable instance : division_ring Cauchy :=
     by rw [rat.cast_mk', of_rat_mul, of_rat_int_cast, of_rat_inv, of_rat_nat_cast],
   .. Cauchy.ring }
 
-theorem of_rat_div (x y : β) : of_rat (x / y) = (of_rat x / of_rat y : Cauchy) :=
+theorem of_rat_div (x y : β) : of_rat (x / y) = (of_rat x / of_rat y : Cauchy abv) :=
 by simp only [div_eq_mul_inv, of_rat_inv, of_rat_mul]
 
 /-- Show the first 10 items of a representative of this equivalence class of cauchy sequences.
 
 The representative chosen is the one passed in the VM to `quot.mk`, so two cauchy sequences
 converging to the same number may be printed differently.
 -/
-meta instance [has_repr β] : has_repr Cauchy :=
+meta instance [has_repr β] : has_repr (Cauchy abv) :=
 { repr := λ r,
   let N := 10, seq := r.unquot in
     "(sorry /- " ++ (", ".intercalate $ (list.range N).map $ repr ∘ seq) ++ ", ... -/)" }
 
 end
 
 section
-parameters {α : Type*} [linear_ordered_field α]
-parameters {β : Type*} [field β] {abv : β → α} [is_absolute_value abv]
-local notation `Cauchy` := @Cauchy _ _ _ _ abv _
+variables {α : Type*} [linear_ordered_field α]
+variables {β : Type*} [field β] {abv : β → α} [is_absolute_value abv]
 
 /-- The Cauchy completion forms a field. -/
-noncomputable instance : field Cauchy :=
+noncomputable instance : field (Cauchy abv) :=
 { .. Cauchy.division_ring,
   .. Cauchy.comm_ring }