refactor(data/real/basic): make real irreducible (#454)

Author: ChrisHughes24

analysis/complex.lean

@@ -93,8 +93,8 @@ tendsto_of_uniform_continuous_subtype
     (λ x, id))
   (mem_nhds_sets
     (is_open_prod
-      (continuous_abs _ $ is_open_gt' _)
-      (continuous_abs _ $ is_open_gt' _))
+      (continuous_abs _ $ is_open_gt' (abs a₁ + 1))
+      (continuous_abs _ $ is_open_gt' (abs a₂ + 1)))
     ⟨lt_add_one (abs a₁), lt_add_one (abs a₂)⟩)
 
 local attribute [semireducible] real.le

analysis/limits.lean

@@ -139,9 +139,9 @@ lemma tendsto_coe_iff {f : ℕ → ℕ} : tendsto (λ n, (f n : ℝ)) at_top at_
     (have _, from tendsto_infi.1 h i, by simpa using tendsto_principal.1 this),
   λ h, tendsto.comp h tendsto_of_nat_at_top_at_top ⟩
 
-lemma tendsto_pow_at_top_at_top_of_gt_1_nat {k : ℕ} (h : k > 1) : tendsto (λn:ℕ, k ^ n) at_top at_top :=
+lemma tendsto_pow_at_top_at_top_of_gt_1_nat {k : ℕ} (h : 1 < k) : tendsto (λn:ℕ, k ^ n) at_top at_top :=
 tendsto_coe_iff.1 $
-  have hr : (k : ℝ) > 1, from show (k : ℝ) > (1 : ℕ), from nat.cast_lt.2 h,
+  have hr : 1 < (k : ℝ), by rw [← nat.cast_one, nat.cast_lt]; exact h,
   by simpa using tendsto_pow_at_top_at_top_of_gt_1 hr
 
 lemma tendsto_inverse_at_top_nhds_0_nat : tendsto (λ n : ℕ, (n : ℝ)⁻¹) at_top (nhds 0) :=

analysis/real.lean

@@ -182,8 +182,8 @@ tendsto_of_uniform_continuous_subtype
     (λ x, id))
   (mem_nhds_sets
     (is_open_prod
-      (real.continuous_abs _ $ is_open_gt' _)
-      (real.continuous_abs _ $ is_open_gt' _))
+      (real.continuous_abs _ $ is_open_gt' (abs a₁ + 1))
+      (real.continuous_abs _ $ is_open_gt' (abs a₂ + 1)))
     ⟨lt_add_one (abs a₁), lt_add_one (abs a₂)⟩)
 
 instance : topological_ring ℝ :=

data/complex/basic.lean

@@ -58,24 +58,24 @@ instance : has_add ℂ := ⟨λ z w, ⟨z.re + w.re, z.im + w.im⟩⟩
 
 @[simp] lemma add_re (z w : ℂ) : (z + w).re = z.re + w.re := rfl
 @[simp] lemma add_im (z w : ℂ) : (z + w).im = z.im + w.im := rfl
-@[simp] lemma of_real_add (r s : ℝ) : ((r + s : ℝ) : ℂ) = r + s := rfl
+@[simp] lemma of_real_add (r s : ℝ) : ((r + s : ℝ) : ℂ) = r + s := ext_iff.2 $ by simp
 
-@[simp] lemma of_real_bit0 (r : ℝ) : ((bit0 r : ℝ) : ℂ) = bit0 r := rfl
-@[simp] lemma of_real_bit1 (r : ℝ) : ((bit1 r : ℝ) : ℂ) = bit1 r := rfl
+@[simp] lemma of_real_bit0 (r : ℝ) : ((bit0 r : ℝ) : ℂ) = bit0 r := ext_iff.2 $ by simp [bit0]
+@[simp] lemma of_real_bit1 (r : ℝ) : ((bit1 r : ℝ) : ℂ) = bit1 r := ext_iff.2 $ by simp [bit1]
 
 instance : has_neg ℂ := ⟨λ z, ⟨-z.re, -z.im⟩⟩
 
 @[simp] lemma neg_re (z : ℂ) : (-z).re = -z.re := rfl
 @[simp] lemma neg_im (z : ℂ) : (-z).im = -z.im := rfl
-@[simp] lemma of_real_neg (r : ℝ) : ((-r : ℝ) : ℂ) = -r := rfl
+@[simp] lemma of_real_neg (r : ℝ) : ((-r : ℝ) : ℂ) = -r := ext_iff.2 $ by simp
 
 instance : has_mul ℂ := ⟨λ z w, ⟨z.re * w.re - z.im * w.im, z.re * w.im + z.im * w.re⟩⟩
 
 @[simp] lemma mul_re (z w : ℂ) : (z * w).re = z.re * w.re - z.im * w.im := rfl
 @[simp] lemma mul_im (z w : ℂ) : (z * w).im = z.re * w.im + z.im * w.re := rfl
 @[simp] lemma of_real_mul (r s : ℝ) : ((r * s : ℝ) : ℂ) = r * s := ext_iff.2 $ by simp
 
-@[simp] lemma I_mul_I : I * I = -1 := rfl
+@[simp] lemma I_mul_I : I * I = -1 := ext_iff.2 $ by simp
 
 lemma I_ne_zero : (I : ℂ) ≠ 0 := mt (congr_arg im) zero_ne_one.symm
 
@@ -90,12 +90,12 @@ def conj (z : ℂ) : ℂ := ⟨z.re, -z.im⟩
 @[simp] lemma conj_re (z : ℂ) : (conj z).re = z.re := rfl
 @[simp] lemma conj_im (z : ℂ) : (conj z).im = -z.im := rfl
 
-@[simp] lemma conj_of_real (r : ℝ) : conj r = r := rfl
+@[simp] lemma conj_of_real (r : ℝ) : conj r = r := ext_iff.2 $ by simp [conj]
 
-@[simp] lemma conj_zero : conj 0 = 0 := rfl
-@[simp] lemma conj_one : conj 1 = 1 := rfl
-@[simp] lemma conj_I : conj I = -I := rfl
-@[simp] lemma conj_neg_I : conj (-I) = I := rfl
+@[simp] lemma conj_zero : conj 0 = 0 := ext_iff.2 $ by simp [conj]
+@[simp] lemma conj_one : conj 1 = 1 := ext_iff.2 $ by simp
+@[simp] lemma conj_I : conj I = -I := ext_iff.2 $ by simp
+@[simp] lemma conj_neg_I : conj (-I) = I := ext_iff.2 $ by simp
 
 @[simp] lemma conj_add (z w : ℂ) : conj (z + w) = conj z + conj w :=
 ext_iff.2 $ by simp
@@ -127,9 +127,9 @@ def norm_sq (z : ℂ) : ℝ := z.re * z.re + z.im * z.im
 @[simp] lemma norm_sq_of_real (r : ℝ) : norm_sq r = r * r :=
 by simp [norm_sq]
 
-@[simp] lemma norm_sq_zero : norm_sq 0 = 0 := rfl
-@[simp] lemma norm_sq_one : norm_sq 1 = 1 := rfl
-@[simp] lemma norm_sq_I : norm_sq I = 1 := rfl
+@[simp] lemma norm_sq_zero : norm_sq 0 = 0 := by simp [norm_sq]
+@[simp] lemma norm_sq_one : norm_sq 1 = 1 := by simp [norm_sq]
+@[simp] lemma norm_sq_I : norm_sq I = 1 := by simp [norm_sq]
 
 lemma norm_sq_nonneg (z : ℂ) : 0 ≤ norm_sq z :=
 add_nonneg (mul_self_nonneg _) (mul_self_nonneg _)
@@ -179,7 +179,7 @@ by refine { zero := 0, add := (+), neg := has_neg.neg, one := 1, mul := (*), ..}
 
 @[simp] lemma sub_re (z w : ℂ) : (z - w).re = z.re - w.re := rfl
 @[simp] lemma sub_im (z w : ℂ) : (z - w).im = z.im - w.im := rfl
-@[simp] lemma of_real_sub (r s : ℝ) : ((r - s : ℝ) : ℂ) = r - s := rfl
+@[simp] lemma of_real_sub (r s : ℝ) : ((r - s : ℝ) : ℂ) = r - s := ext_iff.2 $ by simp
 @[simp] lemma of_real_pow (r : ℝ) (n : ℕ) : ((r ^ n : ℝ) : ℂ) = r ^ n :=
 by induction n; simp [*, of_real_mul, pow_succ]
 
@@ -228,7 +228,9 @@ noncomputable instance : discrete_field ℂ :=
 by rw [division_def, of_real_mul, division_def, of_real_inv]
 
 @[simp] theorem of_real_int_cast : ∀ n : ℤ, ((n : ℝ) : ℂ) = n :=
-int.eq_cast (λ n, ((n : ℝ) : ℂ)) rfl (by simp)
+int.eq_cast (λ n, ((n : ℝ) : ℂ))
+  (by rw [int.cast_one, of_real_one])
+  (λ _ _, by rw [int.cast_add, of_real_add])
 
 @[simp] theorem of_real_nat_cast (n : ℕ) : ((n : ℝ) : ℂ) = n :=
 by rw [← int.cast_coe_nat, of_real_int_cast]; refl

data/complex/exponential.lean

@@ -907,7 +907,7 @@ lemma abs_exp_sub_one_le {x : ℂ} (hx : abs x ≤ 1) :
   abs (exp x - 1) ≤ 2 * abs x :=
 calc abs (exp x - 1) = abs (exp x - (range 1).sum (λ m, x ^ m / m.fact)) :
   by simp [sum_range_succ]
-... ≤ abs x ^ 1 * ((nat.succ 1) * (nat.fact 1 * 1)⁻¹) :
+... ≤ abs x ^ 1 * ((nat.succ 1) * (nat.fact 1 * (1 : ℕ))⁻¹) :
   exp_bound hx dec_trivial
 ... = 2 * abs x : by simp [two_mul, mul_two, mul_add, mul_comm]
 

data/padics/hensel.lean

@@ -78,7 +78,7 @@ lt_of_le_of_lt (norm_nonneg _) hnorm
 private lemma deriv_sq_norm_ne_zero : ∥F.derivative.eval a∥^2 ≠ 0 := ne_of_gt deriv_sq_norm_pos
 
 private lemma deriv_norm_ne_zero : ∥F.derivative.eval a∥ ≠ 0 :=
-λ h, deriv_sq_norm_ne_zero (by simp *; refl)
+λ h, deriv_sq_norm_ne_zero (by simp [*, _root_.pow_two])
 
 private lemma deriv_norm_pos : 0 < ∥F.derivative.eval a∥ :=
 lt_of_le_of_ne (norm_nonneg _) (ne.symm deriv_norm_ne_zero)

data/real/basic.lean

@@ -11,14 +11,17 @@ import order.conditionally_complete_lattice data.real.cau_seq_completion
 
 def real := @cau_seq.completion.Cauchy ℚ _ _ _ abs _
 notation `ℝ` := real
-local attribute [reducible] real
 
 namespace real
 open cau_seq cau_seq.completion
 
 def of_rat (x : ℚ) : ℝ := of_rat x
 
-instance : comm_ring ℝ := cau_seq.completion.comm_ring
+def mk (x : cau_seq ℚ abs) : ℝ := cau_seq.completion.mk x
+
+def comm_ring_aux : comm_ring ℝ := cau_seq.completion.comm_ring
+
+instance : comm_ring ℝ := { ..comm_ring_aux }
 
 /- Extra instances to short-circuit type class resolution -/
 instance : ring ℝ               := by apply_instance
@@ -49,6 +52,12 @@ instance : has_lt ℝ :=
 
 @[simp] theorem mk_lt {f g : cau_seq ℚ abs} : mk f < mk g ↔ f < g := iff.rfl
 
+theorem mk_eq {f g : cau_seq ℚ abs} : mk f = mk g ↔ f ≈ g := mk_eq
+
+theorem quotient_mk_eq_mk (f : cau_seq ℚ abs) : ⟦f⟧ = mk f := rfl
+
+theorem mk_eq_mk {f : cau_seq ℚ abs} : cau_seq.completion.mk f = mk f := rfl
+
 @[simp] theorem mk_pos {f : cau_seq ℚ abs} : 0 < mk f ↔ pos f :=
 iff_of_eq (congr_arg pos (sub_zero f))
 
@@ -66,13 +75,13 @@ instance : linear_order ℝ :=
 { le := (≤), lt := (<),
   le_refl := λ a, or.inr rfl,
   le_trans := λ a b c, quotient.induction_on₃ a b c $
-    λ f g h, by simpa using le_trans,
+    λ f g h, by simpa [quotient_mk_eq_mk] using le_trans,
   lt_iff_le_not_le := λ a b, quotient.induction_on₂ a b $
-    λ f g, by simpa using lt_iff_le_not_le,
+    λ f g, by simpa [quotient_mk_eq_mk] using lt_iff_le_not_le,
   le_antisymm := λ a b, quotient.induction_on₂ a b $
-    λ f g, by simpa [mk_eq] using @cau_seq.le_antisymm _ _ f g,
+    λ f g, by simpa [mk_eq, quotient_mk_eq_mk] using @cau_seq.le_antisymm _ _ f g,
   le_total := λ a b, quotient.induction_on₂ a b $
-    λ f g, by simpa using le_total f g }
+    λ f g, by simpa [quotient_mk_eq_mk] using le_total f g }
 
 instance : partial_order ℝ := by apply_instance
 instance : preorder ℝ      := by apply_instance
@@ -82,7 +91,9 @@ theorem of_rat_lt {x y : ℚ} : of_rat x < of_rat y ↔ x < y := const_lt
 protected theorem zero_lt_one : (0 : ℝ) < 1 := of_rat_lt.2 zero_lt_one
 
 protected theorem mul_pos {a b : ℝ} : 0 < a → 0 < b → 0 < a * b :=
-quotient.induction_on₂ a b $ λ f g, by simpa using cau_seq.mul_pos
+quotient.induction_on₂ a b $ λ f g,
+  show pos (f - 0) → pos (g - 0) → pos (f * g - 0),
+  by simpa using cau_seq.mul_pos
 
 instance : linear_ordered_comm_ring ℝ :=
 { add_le_add_left := λ a b h c,
@@ -112,19 +123,18 @@ instance : domain ℝ                     := by apply_instance
 local attribute [instance] classical.prop_decidable
 
 noncomputable instance : discrete_linear_ordered_field ℝ :=
-{ inv            := has_inv.inv,
-  inv_mul_cancel := @cau_seq.completion.inv_mul_cancel _ _ _ _ _ _,
-  mul_inv_cancel := λ x x0, by rw [mul_comm, cau_seq.completion.inv_mul_cancel x0],
-  inv_zero       := inv_zero,
-  decidable_le   := by apply_instance,
-  ..real.linear_ordered_comm_ring }
+{ decidable_le := by apply_instance,
+  ..real.linear_ordered_comm_ring,
+  ..real.domain,
+  ..cau_seq.completion.discrete_field }
 
 /- Extra instances to short-circuit type class resolution -/
+
 noncomputable instance : linear_ordered_field ℝ    := by apply_instance
 noncomputable instance : decidable_linear_ordered_comm_ring ℝ := by apply_instance
 noncomputable instance : decidable_linear_ordered_semiring ℝ := by apply_instance
 noncomputable instance : decidable_linear_ordered_comm_group ℝ := by apply_instance
-noncomputable instance real.discrete_field : discrete_field ℝ          := by apply_instance
+noncomputable instance discrete_field : discrete_field ℝ := by apply_instance
 noncomputable instance : field ℝ                   := by apply_instance
 noncomputable instance : division_ring ℝ           := by apply_instance
 noncomputable instance : integral_domain ℝ         := by apply_instance
@@ -159,7 +169,7 @@ end
 
 theorem mk_le_of_forall_le {f : cau_seq ℚ abs} {x : ℝ} :
   (∃ i, ∀ j ≥ i, (f j : ℝ) ≤ x) → mk f ≤ x
-| ⟨i, H⟩ := by rw [← neg_le_neg_iff, mk_neg]; exact
+| ⟨i, H⟩ := by rw [← neg_le_neg_iff, ← mk_eq_mk, mk_neg]; exact
   le_mk_of_forall_le ⟨i, λ j ij, by simp [H _ ij]⟩
 
 theorem mk_near_of_forall_near {f : cau_seq ℚ abs} {x : ℝ} {ε : ℝ}
@@ -176,6 +186,12 @@ let ⟨M, M0, H⟩ := f.bounded' 0 in
 ⟨M, mk_le_of_forall_le ⟨0, λ i _,
   rat.cast_le.2 $ le_of_lt (abs_lt.1 (H i)).2⟩⟩
 
+/- mark `real` irreducible in order to prevent `auto_cases` unfolding reals,
+since users rarely want to consider real numbers as Cauchy sequences.
+Marking `comm_ring_aux` `irreducible` is done to ensure that there are no problems
+with non definitionally equal instances, caused by making `real` irreducible-/
+attribute [irreducible] real comm_ring_aux
+
 noncomputable instance : floor_ring ℝ := archimedean.floor_ring _
 
 theorem is_cau_seq_iff_lift {f : ℕ → ℚ} : is_cau_seq abs f ↔ is_cau_seq abs (λ i, (f i : ℝ)) :=
@@ -188,7 +204,7 @@ theorem is_cau_seq_iff_lift {f : ℕ → ℚ} : is_cau_seq abs f ↔ is_cau_seq
 
 theorem of_near (f : ℕ → ℚ) (x : ℝ)
   (h : ∀ ε > 0, ∃ i, ∀ j ≥ i, abs ((f j : ℝ) - x) < ε) :
-  ∃ h', cau_seq.completion.mk ⟨f, h'⟩ = x :=
+  ∃ h', real.mk ⟨f, h'⟩ = x :=
 ⟨is_cau_seq_iff_lift.2 (of_near _ (const abs x) h),
  sub_eq_zero.1 $ abs_eq_zero.1 $
   eq_of_le_of_forall_le_of_dense (abs_nonneg _) $ λ ε ε0,