chore(tactic/localized): lower priority of bad decidability instances…

… in classical locale (#2932)

Also add a decidability instance for complex numbers.

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/monoid_algebra.2Emul_apply/near/199595932
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/slow.20elaboration/near/199543997

Co-authored-by: Gabriel Ebner <gebner@gebner.org>

src/data/complex/basic.lean

@@ -15,6 +15,8 @@ notation `ℂ` := complex
 
 namespace complex
 
+noncomputable instance : decidable_eq ℂ := classical.dec_eq _
+
 @[simp] theorem eta : ∀ z : ℂ, complex.mk z.re z.im = z
 | ⟨a, b⟩ := rfl
 

src/data/real/basic.lean

@@ -149,6 +149,9 @@ noncomputable instance : semilattice_inf ℝ := by apply_instance
 noncomputable instance : semilattice_sup ℝ := by apply_instance
 noncomputable instance : has_inf ℝ         := by apply_instance
 noncomputable instance : has_sup ℝ         := by apply_instance
+noncomputable instance decidable_lt (a b : ℝ) : decidable (a < b) := by apply_instance
+noncomputable instance decidable_le (a b : ℝ) : decidable (a ≤ b) := by apply_instance
+noncomputable instance decidable_eq (a b : ℝ) : decidable (a = b) := by apply_instance
 
 lemma le_of_forall_epsilon_le {a b : real} (h : ∀ε, ε > 0 → a ≤ b + ε) : a ≤ b :=
 le_of_forall_le_of_dense $ assume x hxb,

src/measure_theory/indicator_function.lean

@@ -107,15 +107,14 @@ end
 
 end order
 
-section tendsto
-variables {ι : Type*} [semilattice_sup ι] [has_zero β]
-
-lemma tendsto_indicator_of_monotone [nonempty ι] (s : ι → set α) (hs : monotone s) (f : α → β)
-  (a : α) : tendsto (λi, indicator (s i) f a) at_top (pure $ indicator (Union s) f a) :=
+lemma tendsto_indicator_of_monotone {ι} [semilattice_sup ι] [has_zero β]
+  (s : ι → set α) (hs : monotone s) (f : α → β) (a : α) :
+  tendsto (λi, indicator (s i) f a) at_top (pure $ indicator (Union s) f a) :=
 begin
   by_cases h : ∃i, a ∈ s i,
-  { simp only [tendsto_pure, mem_at_top_sets, mem_set_of_eq],
-    rcases h with ⟨i, hi⟩,
+  { rcases h with ⟨i, hi⟩,
+    haveI : inhabited ι := ⟨i⟩,
+    simp only [tendsto_pure, mem_at_top_sets, mem_set_of_eq],
     use i, assume n hn,
     rw [indicator_of_mem (hs hn hi) _, indicator_of_mem ((subset_Union _ _) hi) _] },
   { rw [not_exists] at h,
@@ -127,12 +126,14 @@ begin
     exact tendsto_const_pure }
 end
 
-lemma tendsto_indicator_of_antimono [nonempty ι] (s : ι → set α) (hs : ∀i j, i ≤ j → s j ⊆ s i) (f : α → β)
-  (a : α) : tendsto (λi, indicator (s i) f a) at_top (pure $ indicator (Inter s) f a) :=
+lemma tendsto_indicator_of_antimono {ι} [semilattice_sup ι] [has_zero β]
+  (s : ι → set α) (hs : ∀i j, i ≤ j → s j ⊆ s i) (f : α → β) (a : α) :
+  tendsto (λi, indicator (s i) f a) at_top (pure $ indicator (Inter s) f a) :=
 begin
   by_cases h : ∃i, a ∉ s i,
-  { simp only [tendsto_pure, mem_at_top_sets, mem_set_of_eq],
-    rcases h with ⟨i, hi⟩,
+  { rcases h with ⟨i, hi⟩,
+    haveI : inhabited ι := ⟨i⟩,
+    simp only [tendsto_pure, mem_at_top_sets, mem_set_of_eq],
     use i, assume n hn,
     rw [indicator_of_not_mem _ _, indicator_of_not_mem _ _],
     { simp only [mem_Inter, not_forall], exact ⟨i, hi⟩ },
@@ -146,7 +147,7 @@ begin
     exact tendsto_const_pure }
 end
 
-lemma tendsto_indicator_bUnion_finset (s : ι → set α) (f : α → β) (a : α) :
+lemma tendsto_indicator_bUnion_finset {ι} [has_zero β] (s : ι → set α) (f : α → β) (a : α) :
   tendsto (λ (n : finset ι), indicator (⋃i∈n, s i) f a) at_top (pure $ indicator (Union s) f a) :=
 begin
   by_cases h : ∃i, a ∈ s i,
@@ -169,5 +170,3 @@ begin
     rw this,
     exact tendsto_const_pure }
 end
-
-end tendsto

src/tactic/localized.lean

@@ -133,8 +133,12 @@ add_tactic_doc
 meta def print_localized_commands (ns : list name) : tactic unit :=
 do cmds ← get_localized ns, cmds.mmap' trace
 
--- you can run `open_locale classical` to get the decidability of all propositions.
+-- you can run `open_locale classical` to get the decidability of all propositions, and downgrade
+-- the priority of decidability instances that make Lean run through all the algebraic hierarchy
+-- whenever it wants to solve a decidability question
 localized "attribute [instance, priority 9] classical.prop_decidable" in classical
+localized "attribute [instance, priority 8] eq.decidable decidable_eq_of_decidable_le" in classical
+
 
 localized "postfix `?`:9001 := optional" in parser
 localized "postfix *:9001 := lean.parser.many" in parser