chore(*): switch to lean 3.6.1

.github/workflows/build.yml

@@ -27,6 +27,7 @@ jobs:
         run: leanpkg build | python scripts/detect_errors.py
 
       - name: configure git setup
+        if: always()
         run: |
           git remote add origin-bot "https://leanprover-community-bot:${{ secrets.DEPLOY_NIGHTLY_GITHUB_TOKEN }}@github.com/leanprover-community/mathlib.git"
           git config user.email "leanprover.community@gmail.com"

leanpkg.toml

@@ -1,7 +1,7 @@
 [package]
 name = "mathlib"
 version = "0.1"
-lean_version = "leanprover-community/lean:3.5.1"
+lean_version = "leanprover-community/lean:3.6.1"
 path = "src"
 
 [dependencies]

scripts/nolints.txt

@@ -60,7 +60,7 @@ apply_nolint set.centralizer.add_submonoid doc_blame
 
 -- algebra/direct_limit.lean
 apply_nolint add_comm_group.direct_limit has_inhabited_instance
-apply_nolint field.direct_limit.discrete_field doc_blame
+apply_nolint field.direct_limit.field doc_blame
 apply_nolint field.direct_limit.field doc_blame
 apply_nolint field.direct_limit.inv doc_blame
 apply_nolint module.direct_limit unused_arguments has_inhabited_instance
@@ -1116,7 +1116,7 @@ apply_nolint equiv.comm_monoid doc_blame
 apply_nolint equiv.comm_ring doc_blame
 apply_nolint equiv.comm_semigroup doc_blame
 apply_nolint equiv.comm_semiring doc_blame
-apply_nolint equiv.discrete_field doc_blame
+apply_nolint equiv.field doc_blame
 apply_nolint equiv.division_ring doc_blame
 apply_nolint equiv.domain doc_blame
 apply_nolint equiv.field doc_blame
@@ -1875,7 +1875,7 @@ apply_nolint rat_mul_continuous_lemma ge_or_gt
 
 -- data/real/cau_seq_completion.lean
 apply_nolint cau_seq.completion.Cauchy doc_blame
-apply_nolint cau_seq.completion.discrete_field doc_blame
+apply_nolint cau_seq.completion.field doc_blame
 apply_nolint cau_seq.completion.mk doc_blame
 apply_nolint cau_seq.completion.of_rat doc_blame
 apply_nolint cau_seq.is_complete doc_blame

src/algebra/archimedean.lean

@@ -199,7 +199,7 @@ begin
   cases archimedean_iff_nat_lt.1 (by apply_instance) (1/ε) with n hn,
   existsi n,
   apply div_lt_of_mul_lt_of_pos,
-  { simp, apply add_pos_of_pos_of_nonneg zero_lt_one, apply nat.cast_nonneg },
+  { simp, apply add_pos_of_nonneg_of_pos, apply nat.cast_nonneg, apply zero_lt_one },
   { apply (div_lt_iff' hε).1,
     transitivity,
     { exact hn },

src/algebra/direct_limit.lean

@@ -516,13 +516,8 @@ by rw [_root_.mul_comm, direct_limit.mul_inv_cancel G f hp]
 protected noncomputable def field : field (ring.direct_limit G f) :=
 { inv := inv G f,
   mul_inv_cancel := λ p, direct_limit.mul_inv_cancel G f,
-  inv_mul_cancel := λ p, direct_limit.inv_mul_cancel G f,
-  .. direct_limit.nonzero_comm_ring G f }
-
-protected noncomputable def discrete_field : discrete_field (ring.direct_limit G f) :=
-{ has_decidable_eq := classical.dec_eq _,
   inv_zero := dif_pos rfl,
-  ..direct_limit.field G f }
+  .. direct_limit.nonzero_comm_ring G f }
 
 end
 

src/algebra/euclidean_domain.lean

@@ -11,7 +11,9 @@ import data.int.basic
 universe u
 
 section prio
-set_option default_priority 100 -- see Note [default priority]
+-- Extra low priority since this instance could accidentally pull in an
+-- unwanted classical decidability assumption.
+set_option default_priority 70 -- see Note [default priority]
 class euclidean_domain (α : Type u) extends nonzero_comm_ring α :=
 (quotient : α → α → α)
 (quotient_zero : ∀ a, quotient a 0 = 0)
@@ -38,10 +40,10 @@ variables [euclidean_domain α]
 
 local infix ` ≺ `:50 := euclidean_domain.r
 
-@[priority 100] -- see Note [lower instance priority]
+@[priority 70] -- see Note [lower instance priority]
 instance : has_div α := ⟨quotient⟩
 
-@[priority 100] -- see Note [lower instance priority]
+@[priority 70] -- see Note [lower instance priority]
 instance : has_mod α := ⟨remainder⟩
 
 theorem div_add_mod (a b : α) : b * (a / b) + a % b = a :=
@@ -240,7 +242,7 @@ by have := @xgcd_aux_P _ _ _ a b a b 1 0 0 1
   (by rw [P, mul_one, mul_zero, add_zero]) (by rw [P, mul_one, mul_zero, zero_add]);
 rwa [xgcd_aux_val, xgcd_val] at this
 
-@[priority 100] -- see Note [lower instance priority]
+@[priority 70] -- see Note [lower instance priority]
 instance (α : Type*) [e : euclidean_domain α] : integral_domain α :=
 by haveI := classical.dec_eq α; exact
 { eq_zero_or_eq_zero_of_mul_eq_zero :=
@@ -338,7 +340,7 @@ instance int.euclidean_domain : euclidean_domain ℤ :=
     exact mul_le_mul_of_nonneg_left (int.nat_abs_pos_of_ne_zero b0) (nat.zero_le _) }
 
 @[priority 100] -- see Note [lower instance priority]
-instance discrete_field.to_euclidean_domain {K : Type u} [discrete_field K] : euclidean_domain K :=
+instance field.to_euclidean_domain {K : Type u} [field K] [decidable_eq K] : euclidean_domain K :=
 { quotient := (/),
   remainder := λ a b, if b = 0 then a else 0,
   quotient_zero := div_zero,

src/algebra/field.lean

@@ -9,11 +9,6 @@ open set
 universe u
 variables {α : Type u}
 
-/-- Core version `division_ring_has_div` erratically requires two instances of `division_ring` -/
--- priority 900 sufficient as core version has custom-set lower priority (100)
-@[priority 900] -- see Note [lower instance priority]
-instance division_ring_has_div' [division_ring α] : has_div α := ⟨algebra.div⟩
-
 @[priority 100] -- see Note [lower instance priority]
 instance division_ring.to_domain [s : division_ring α] : domain α :=
 { eq_zero_or_eq_zero_of_mul_eq_zero := λ a b h,
@@ -23,14 +18,14 @@ instance division_ring.to_domain [s : division_ring α] : domain α :=
 
 @[simp] theorem inv_one [division_ring α] : (1⁻¹ : α) = 1 := by rw [inv_eq_one_div, one_div_one]
 
-@[simp] theorem inv_inv' [discrete_field α] (x : α) : x⁻¹⁻¹ = x :=
-if h : x = 0
-then by rw [h, inv_zero, inv_zero]
-else division_ring.inv_inv h
+attribute [simp] inv_inv'
 
-lemma inv_involutive' [discrete_field α] : function.involutive (has_inv.inv : α → α) :=
+lemma inv_inv'' [division_ring α] (x : α) : x⁻¹⁻¹ = x :=
 inv_inv'
 
+lemma inv_involutive' [division_ring α] : function.involutive (has_inv.inv : α → α) :=
+@inv_inv' _ _
+
 namespace units
 variables [division_ring α] {a b : α}
 
@@ -70,14 +65,14 @@ congr_arg _ $ units.inv_eq_inv _
   a /ₚ units.mk0 b hb = a / b :=
 divp_eq_div _ _
 
-lemma inv_div (ha : a ≠ 0) (hb : b ≠ 0) : (a / b)⁻¹ = b / a :=
-(mul_inv_eq (inv_ne_zero hb) ha).trans $ by rw division_ring.inv_inv hb; refl
+lemma inv_div : (a / b)⁻¹ = b / a :=
+(mul_inv' _ _).trans (by rw inv_inv'; refl)
 
-lemma inv_div_left (ha : a ≠ 0) (hb : b ≠ 0) : a⁻¹ / b = (b * a)⁻¹ :=
-(mul_inv_eq ha hb).symm
+lemma inv_div_left : a⁻¹ / b = (b * a)⁻¹ :=
+(mul_inv' _ _).symm
 
-lemma neg_inv (h : a ≠ 0) : - a⁻¹ = (- a)⁻¹ :=
-by rw [inv_eq_one_div, inv_eq_one_div, div_neg_eq_neg_div _ h]
+lemma neg_inv : - a⁻¹ = (- a)⁻¹ :=
+by rw [inv_eq_one_div, inv_eq_one_div, div_neg_eq_neg_div]
 
 lemma division_ring.inv_comm_of_comm (h : a ≠ 0) (H : a * b = b * a) : a⁻¹ * b = b * a⁻¹ :=
 begin
@@ -106,15 +101,14 @@ by rw [← divp_mk0 _ hc, ← divp_mk0 _ hc, divp_right_inj]
 lemma sub_div (a b c : α) : (a - b) / c = a / c - b / c :=
 (div_sub_div_same _ _ _).symm
 
-lemma division_ring.inv_inj (ha : a ≠ 0) (hb : b ≠ 0) : a⁻¹ = b⁻¹ ↔ a = b :=
-⟨λ h, by rw [← division_ring.inv_inv ha, ← division_ring.inv_inv hb, h], congr_arg (λx,x⁻¹)⟩
+lemma division_ring.inv_inj : a⁻¹ = b⁻¹ ↔ a = b :=
+⟨λ h, by rw [← inv_inv'' a, h, inv_inv''], congr_arg (λx,x⁻¹)⟩
 
-lemma division_ring.inv_eq_iff (ha : a ≠ 0) (hb : b ≠ 0) : a⁻¹ = b ↔ b⁻¹ = a :=
-by rw [← division_ring.inv_inj (inv_ne_zero ha) hb,
-       eq_comm, division_ring.inv_inv ha]
+lemma division_ring.inv_eq_iff  : a⁻¹ = b ↔ b⁻¹ = a :=
+by rw [← division_ring.inv_inj, eq_comm, inv_inv'']
 
-lemma div_neg (a : α) (hb : b ≠ 0) : a / -b = -(a / b) :=
-by rw [← division_ring.neg_div_neg_eq _ (neg_ne_zero.2 hb), neg_neg, neg_div]
+lemma div_neg (a : α) : a / -b = -(a / b) :=
+by rw [← div_neg_eq_neg_div]
 
 lemma div_eq_iff_mul_eq (hb : b ≠ 0) : a / b = c ↔ c * b = a :=
 ⟨λ h, by rw [← h, div_mul_cancel _ hb],
@@ -149,11 +143,11 @@ by rw [div_mul_eq_mul_div, mul_comm, mul_div_right_comm]
 lemma mul_div_comm (a b c : α) : a * (b / c) = b * (a / c) :=
 by rw [← mul_div_assoc, mul_comm, mul_div_assoc]
 
-lemma field.div_right_comm (a : α) (hb : b ≠ 0) (hc : c ≠ 0) : (a / b) / c = (a / c) / b :=
-by rw [field.div_div_eq_div_mul _ hb hc, field.div_div_eq_div_mul _ hc hb, mul_comm]
+lemma field.div_right_comm (a : α) : (a / b) / c = (a / c) / b :=
+by rw [div_div_eq_div_mul, div_div_eq_div_mul, mul_comm]
 
-lemma field.div_div_div_cancel_right (a : α) (hb : b ≠ 0) (hc : c ≠ 0) : (a / c) / (b / c) = a / b :=
-by rw [field.div_div_eq_mul_div _ hb hc, div_mul_cancel _ hc]
+lemma field.div_div_div_cancel_right (a : α) (hc : c ≠ 0) : (a / c) / (b / c) = a / b :=
+by rw [div_div_eq_mul_div, div_mul_cancel _ hc]
 
 lemma div_mul_div_cancel (a : α) (hc : c ≠ 0) : (a / c) * (c / b) = a / b :=
 by rw [← mul_div_assoc, div_mul_cancel _ hc]
@@ -169,46 +163,29 @@ by simpa using @div_eq_div_iff _ _ a b c 1 hb one_ne_zero
 lemma eq_div_iff (hb : b ≠ 0) : c = a / b ↔ c * b = a :=
 by simpa using @div_eq_div_iff _ _ c 1 a b one_ne_zero hb
 
-lemma field.div_div_cancel (ha : a ≠ 0) (hb : b ≠ 0) : a / (a / b) = b :=
-by rw [div_eq_mul_inv, inv_div ha hb, mul_div_cancel' _ ha]
+lemma field.div_div_cancel (ha : a ≠ 0) : a / (a / b) = b :=
+by rw [div_eq_mul_inv, inv_div, mul_div_cancel' _ ha]
 
 lemma add_div' (a b c : α) (hc : c ≠ 0) :
   b + a / c = (b * c + a) / c :=
 by simpa using div_add_div b a one_ne_zero hc
 
 lemma div_add' (a b c : α) (hc : c ≠ 0) :
   a / c + b = (a + b * c) / c :=
-by simpa using div_add_div b a one_ne_zero hc
+by rwa [add_comm, add_div', add_comm]
 
 end
 
 section
-variables [discrete_field α] {a b c : α}
+variables [field α] {a b c : α}
 
 attribute [simp] inv_zero div_zero
 
-lemma div_right_comm (a b c : α) : (a / b) / c = (a / c) / b :=
-if b0 : b = 0 then by simp only [b0, div_zero, zero_div] else
-if c0 : c = 0 then by simp only [c0, div_zero, zero_div] else
-field.div_right_comm _ b0 c0
-
-lemma div_div_div_cancel_right (a b : α) (hc : c ≠ 0) : (a / c) / (b / c) = a / b :=
-if b0 : b = 0 then by simp only [b0, div_zero, zero_div] else
-field.div_div_div_cancel_right _ b0 hc
-
-lemma div_div_cancel (ha : a ≠ 0) : a / (a / b) = b :=
-if b0 : b = 0 then by simp only [b0, div_zero] else
-field.div_div_cancel ha b0
-
 @[simp] lemma inv_eq_zero {a : α} : a⁻¹ = 0 ↔ a = 0 :=
 classical.by_cases (assume : a = 0, by simp [*])(assume : a ≠ 0, by simp [*, inv_ne_zero])
 
 lemma neg_inv' (a : α) : (-a)⁻¹ = - a⁻¹ :=
-begin
-  by_cases a = 0,
-  { rw [h, neg_zero, inv_zero, neg_zero] },
-  { rw [neg_inv h] }
-end
+neg_inv.symm
 
 end
 
@@ -242,7 +219,7 @@ end
 
 section
 
-variables {β : Type*} [discrete_field α] [discrete_field β] (f : α →+* β) {x y : α}
+variables {β : Type*} [field α] [field β] (f : α →+* β) {x y : α}
 
 lemma map_inv : f x⁻¹ = (f x)⁻¹ :=
 classical.by_cases (by rintro rfl; simp only [map_zero f, inv_zero]) (map_inv' f)
@@ -273,7 +250,7 @@ lemma injective : function.injective f := (of f).injective
 end
 
 section
-variables {β : Type*} [discrete_field α] [discrete_field β]
+variables {β : Type*} [field α] [field β]
 variables (f : α → β) [is_ring_hom f] {x y : α}
 
 lemma map_inv : f x⁻¹ = (f x)⁻¹ := (of f).map_inv

src/algebra/field_power.lean

@@ -60,7 +60,7 @@ pow_one a
 
 end field_power
 
-@[simp] lemma ring_hom.map_fpow {α β : Type*} [discrete_field α] [discrete_field β] (f : α →+* β)
+@[simp] lemma ring_hom.map_fpow {α β : Type*} [field α] [field β] (f : α →+* β)
   (a : α) : ∀ (n : ℤ), f (a ^ n) = f a ^ n
 | (n : ℕ) := f.map_pow a n
 | -[1+n] := by simp [fpow_neg_succ_of_nat, f.map_pow, f.map_inv]
@@ -76,7 +76,7 @@ end
 
 namespace is_ring_hom
 
-lemma map_fpow {α β : Type*} [discrete_field α] [discrete_field β] (f : α → β) [is_ring_hom f]
+lemma map_fpow {α β : Type*} [field α] [field β] (f : α → β) [is_ring_hom f]
   (a : α) : ∀ (n : ℤ), f (a ^ n) = f a ^ n :=
 (ring_hom.of f).map_fpow a
 
@@ -86,13 +86,13 @@ lemma map_fpow' {K L : Type*} [division_ring K] [division_ring L] (f : K → L)
 
 end is_ring_hom
 
-section discrete_field_power
+section field_power
 open int
-variables {K : Type u} [discrete_field K]
+variables {K : Type u} [field K]
 
 lemma zero_fpow : ∀ z : ℤ, z ≠ 0 → (0 : K) ^ z = 0
 | (of_nat n) h := zero_gpow _ $ by rintro rfl; exact h rfl
-| -[1+n] h := show 1/(0*0^n)=(0:K), by rw [zero_mul, one_div_zero]
+| -[1+n] h := show 1/(0*0^n)=(0:K), by simp
 
 lemma fpow_neg (a : K) : ∀ n : ℤ, a ^ (-n) = 1 / a ^ n
 | (0) := by simp
@@ -104,6 +104,7 @@ by rw [sub_eq_add_neg, fpow_add ha, fpow_neg, ←div_eq_mul_one_div]
 
 lemma fpow_mul (a : K) (i j : ℤ) : a ^ (i * j) = (a ^ i) ^ j :=
 begin
+  classical,
   by_cases a = 0,
   { subst h,
     have : ¬ i = 0 → ¬ j = 0 → ¬ i * j = 0, begin rw [mul_eq_zero, not_or_distrib], exact and.intro end,
@@ -120,7 +121,7 @@ lemma mul_fpow (a b : K) : ∀(i : ℤ), (a * b) ^ i = (a ^ i) * (b ^ i)
   by rw [fpow_neg_succ_of_nat, fpow_neg_succ_of_nat, fpow_neg_succ_of_nat,
       mul_pow, div_mul_div, one_mul]
 
-end discrete_field_power
+end field_power
 
 section ordered_field_power
 open int
@@ -212,6 +213,7 @@ begin
   have hxm₀ : x^m ≠ 0 := ne_of_gt hxm,
   suffices : 1 < x^(n-m),
   { replace := mul_lt_mul_of_pos_right this hxm,
+    simp [sub_eq_add_neg] at this,
     simpa [*, fpow_add, mul_assoc, fpow_neg, inv_mul_cancel], },
   apply one_lt_fpow hx, linarith,
 end
@@ -243,7 +245,7 @@ end
 end ordered
 
 section
-variables {K : Type*} [discrete_field K]
+variables {K : Type*} [field K]
 
 @[simp] theorem fpow_neg_mul_fpow_self (n : ℕ) {x : K} (h : x ≠ 0) :
   x^-(n:ℤ) * x^n = 1 :=

src/algebra/floor.lean

@@ -146,7 +146,7 @@ theorem fract_eq_iff {r s : α} : fract r = s ↔ 0 ≤ s ∧ s < 1 ∧ ∃ z :
     rw [eq_sub_iff_add_eq, add_comm, ←eq_sub_iff_add_eq],
     rcases h with ⟨hge, hlt, ⟨z, hz⟩⟩,
     rw [hz, int.cast_inj, floor_eq_iff, ←hz],
-    clear hz, split; linarith {discharger := `[simp]}
+    clear hz, split; simpa [sub_eq_add_neg]
   end⟩
 
 theorem fract_eq_fract {r s : α} : fract r = fract s ↔ ∃ z : ℤ, r - s = z :=
@@ -160,14 +160,14 @@ theorem fract_eq_fract {r s : α} : fract r = fract s ↔ ∃ z : ℤ, r - s = z
   split, exact fract_lt_one _,
   use z + ⌊s⌋,
   rw [eq_add_of_sub_eq hz, int.cast_add],
-  unfold fract, simp
+  unfold fract, simp [sub_eq_add_neg]
 end⟩
 
 @[simp] lemma fract_fract (r : α) : fract (fract r) = fract r :=
-by rw fract_eq_fract; exact ⟨-⌊r⌋, by unfold fract;simp⟩
+by rw fract_eq_fract; exact ⟨-⌊r⌋, by simp [sub_eq_add_neg, fract]⟩
 
 theorem fract_add (r s : α) : ∃ z : ℤ, fract (r + s) - fract r - fract s = z :=
-⟨⌊r⌋ + ⌊s⌋ - ⌊r + s⌋, by unfold fract; simp⟩
+⟨⌊r⌋ + ⌊s⌋ - ⌊r + s⌋, by unfold fract; simp [sub_eq_add_neg]; abel⟩
 
 theorem fract_mul_nat (r : α) (b : ℕ) : ∃ z : ℤ, fract r * b - fract (r * b) = z :=
 begin

src/algebra/geom_sum.lean

@@ -148,4 +148,4 @@ have h₄ : x * x⁻¹ ^ n = x⁻¹ ^ n * x,
     rw [pow_succ, ← mul_assoc, mul_inv_cancel hx0, one_mul]),
 by rw [geom_sum h₁, div_eq_iff_mul_eq h₂, ← domain.mul_left_inj h₃,
     ← mul_assoc, ← mul_assoc, mul_inv_cancel h₃];
-  simp [mul_add, add_mul, mul_inv_cancel hx0, mul_assoc, h₄]
+  simp [mul_add, add_mul, mul_inv_cancel hx0, mul_assoc, h₄, sub_eq_add_neg, add_comm, add_left_comm]