chore(*): switch to lean 3.6.1 (leanprover-community#2064)

* chore(*): switch to lean 3.6.0

* Port `src/linear_algebra` to Lean 3.6c

* Port `src/ring_theory` to Lean 3.6c

* Port `src/algebra` and its dependencies to Lean 3.6c

* Port `src/group_theory` to Lean 3.6c

* WIP: Ports part of `src/data` to Lean 3.6c

* Port `src/data` (and dependencies) to Lean 3.6

* fix set_theory.lists

* fix ring2

* fix pell.lean

these aren't the cleanest proofs, but pell.lean is kind of a standalone thing.

* fix dioph.lean

* Port `src/number_theory/sum_four_squares.lean` to Lean 3.6c

* Port `src/field_theory` to Lean 3.6

* Port `src/computability` to Lean 3.6c

* Port `src/measure_theory` (and dependencies) to Lean 3.6c

* fix manifold/real_instances

* fix analysis/complex/polynomial

* Fix some compile errors in `real_inner_product`

* Upgrade to Lean 3.6.1

* perf: speed up calls to linarith

* Reduce instance priorities for potentially noncomputable instances.

* Remove cyclic instance.

* Make arguments {implicit} in instances where they can be filled in via unification.

* Make inner_product_space compile.

* Style.

* Port data.nat.modeq

* Port data.int.parity

* Port data.int.modeq

* Port data.real.hyperreal

* fix(ci): always run git setup step

closes leanprover-community#2079

(cherry picked from commit 8a0157d)

* Remove pre-3.6 legacy code.

* Fix test/monotonicity.lean

* Fix test/ring_exp.lean

* Fix test/conv.lean

* Fix archive/imo1988_q6.lean

* Fix docs/tutorial/Zmod37.lean

* Fix archive/sensitivity.lean

* refactor(algebra/lie_algebra): lie_algebra should not extend lie_ring

* remove unused argument

* add doc-string to instance that became a def

* add docstring

* Fix linting error ☺

* Fix data.real.irrational

* fixing a proof

* cleaning up proof

* fix broken proof

* fix proof

* fix some more proofs

* fix

* fix proofs

Co-authored-by: Vierkantor <Vierkantor@users.noreply.github.com>
Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: Scott Morrison <scott@tqft.net>

archive/imo1988_q6.lean

@@ -255,7 +255,7 @@ begin
     apply eq_iff_eq_cancel_right.2,
     simp, ring, },
   { -- Show that the solution set is symmetric in a and b.
-    intros x y, simp [mul_comm], },
+    cc },
   { -- Show that the claim is true if b = 0.
     simp },
   { -- Show that the claim is true if a = b.

archive/sensitivity.lean

@@ -282,7 +282,7 @@ lemma f_squared : ∀ v : V n, (f n) (f n v) = (n : ℝ) • v :=
 begin
   induction n with n IH; intro,
   { simpa only [nat.cast_zero, zero_smul] },
-  { cases v, simp [f_succ_apply, IH, add_smul] }
+  { cases v, simp [f_succ_apply, IH, add_smul], abel }
 end
 
 -- We now compute the matrix of f in the e basis (p is the line index,
@@ -332,7 +332,8 @@ begin
   rcases hv with ⟨v, rfl⟩,
   have : √(m+1) * √(m+1) = m+1 :=
     real.mul_self_sqrt (by exact_mod_cast zero_le _),
-  simp [-add_comm, this, f_succ_apply, g_apply, f_squared, smul_add, add_smul, smul_smul],
+  simp [this, f_succ_apply, g_apply, f_squared, smul_add, add_smul, smul_smul],
+  abel
 end
 
 /- -------------------------------------------------------------------------\

docs/tutorial/Zmod37.lean

@@ -42,7 +42,7 @@ begin
   -- Hl : l * 37 = b - a, and Hm : m * 37 = c - b
   -- Goal : ∃ k, k * 37 = c - a
   use (l + m),
-  simp [add_mul, Hl, Hm],
+  rw [add_mul, Hl, Hm], ring
 end
 
 -- so we've now seen a general technique for proving a ≈ b -- use (the k that works)
@@ -95,7 +95,7 @@ begin
   apply quotient.sound,
   -- goal now a₁ + a₂ ≈ b₁ + b₂, and we know how to do these.
   use (m + n),
-  simp [add_mul, Hm, Hn]
+  rw [add_mul, Hm, Hn], ring
 end
 
 -- That lemma above is *exactly* what we need to make sure addition is

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 :=