chore(algebra/char_zero): split (#17760)

hrmacbeth · hrmacbeth · commit 70d50ecfd490 · 2022-12-02T02:44:24.000Z
Split `algebra/char_zero` into `algebra/char_zero/lemmas` and `algebra/char_zero/infinite` (there was already a `algebra/char_zero/defs`), with the former not importing finset.

As intended, this caused a few files which had been getting their finset import by this path to require that import explicitly.  I've added the finset imports explicitly on all such files, except for `tactic/positivity`, the point being that I actually want to remove the finset import from positivity.  I moved the `fin{set,type}.card` positivity extensions from `tactic/positivity` to `data/fintype/card`.
diff --git a/archive/oxford_invariants/2021summer/week3_p1.lean b/archive/oxford_invariants/2021summer/week3_p1.lean
@@ -5,7 +5,7 @@ Authors: Yaël Dillies, Bhavik Mehta
 -/
 import algebra.big_operators.order
 import algebra.big_operators.ring
-import algebra.char_zero
+import algebra.char_zero.lemmas
 import data.rat.cast
 
 /-!
diff --git a/src/algebra/algebra/basic.lean b/src/algebra/algebra/basic.lean
@@ -8,7 +8,7 @@ import algebra.module.ulift
 import algebra.ne_zero
 import algebra.ring.aut
 import algebra.ring.ulift
-import algebra.char_zero
+import algebra.char_zero.lemmas
 import linear_algebra.span
 import tactic.abel
 
diff --git a/src/algebra/char_zero/infinite.lean b/src/algebra/char_zero/infinite.lean
@@ -0,0 +1,16 @@
+/-
+Copyright (c) 2020 Johan Commelin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johan Commelin
+-/
+import algebra.char_zero.defs
+import data.fintype.lattice
+
+/-! # A characteristic-zero semiring is infinite -/
+
+open set
+variables (M : Type*) [add_monoid_with_one M] [char_zero M]
+
+@[priority 100] -- see Note [lower instance priority]
+instance char_zero.infinite : infinite M :=
+infinite.of_injective coe nat.cast_injective
diff --git a/src/algebra/char_zero/lemmas.lean b/src/algebra/char_zero/lemmas.lean
@@ -5,7 +5,6 @@ Authors: Mario Carneiro
 -/
 
 import data.nat.cast.field
-import data.fintype.lattice
 import algebra.group_power.lemmas
 
 /-!
@@ -47,10 +46,6 @@ section
 
 variables (M : Type*) [add_monoid_with_one M] [char_zero M]
 
-@[priority 100] -- see Note [lower instance priority]
-instance char_zero.infinite : infinite M :=
-infinite.of_injective coe nat.cast_injective
-
 instance char_zero.ne_zero.two : ne_zero (2 : M) :=
 ⟨have ((2:ℕ):M) ≠ 0, from nat.cast_ne_zero.2 dec_trivial, by rwa [nat.cast_two] at this⟩
 
diff --git a/src/algebra/order/field/power.lean b/src/algebra/order/field/power.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Lewis, Leonardo de Moura, Mario Carneiro, Floris van Doorn
 -/
 import algebra.parity
-import algebra.char_zero
+import algebra.char_zero.lemmas
 import algebra.group_with_zero.power
 import algebra.order.field.basic
 
diff --git a/src/algebra/order/floor.lean b/src/algebra/order/floor.lean
@@ -5,6 +5,7 @@ Authors: Mario Carneiro, Kevin Kappelmann
 -/
 import data.int.lemmas
 import data.set.intervals.group
+import data.set.lattice
 import tactic.abel
 import tactic.linarith
 import tactic.positivity
diff --git a/src/algebra/order/hom/ring.lean b/src/algebra/order/hom/ring.lean
@@ -7,6 +7,7 @@ import algebra.order.archimedean
 import algebra.order.hom.monoid
 import algebra.order.ring.defs
 import algebra.ring.equiv
+import tactic.wlog
 
 /-!
 # Ordered ring homomorphisms
diff --git a/src/combinatorics/catalan.lean b/src/combinatorics/catalan.lean
@@ -5,7 +5,7 @@ Authors: Julian Kuelshammer
 -/
 import data.nat.choose.central
 import algebra.big_operators.fin
-import algebra.char_zero
+import algebra.char_zero.lemmas
 import tactic.field_simp
 import tactic.linear_combination
 
diff --git a/src/data/enat/basic.lean b/src/data/enat/basic.lean
@@ -5,7 +5,7 @@ Authors: Yury Kudryashov
 -/
 import data.nat.lattice
 import data.nat.succ_pred
-import algebra.char_zero
+import algebra.char_zero.lemmas
 import algebra.order.sub.with_top
 import algebra.order.ring.with_top
 
diff --git a/src/data/fintype/card.lean b/src/data/fintype/card.lean
@@ -6,6 +6,7 @@ Authors: Mario Carneiro
 import data.fintype.basic
 import data.finset.card
 import data.list.nodup_equiv_fin
+import tactic.positivity
 import tactic.wlog
 
 /-!
@@ -967,3 +968,22 @@ begin
     rw hn at hlt,
     exact (ih (fintype.card β) hlt _ rfl), }
 end
+
+namespace tactic
+open positivity
+
+private lemma card_univ_pos (α : Type*) [fintype α] [nonempty α] :
+  0 < (finset.univ : finset α).card :=
+finset.univ_nonempty.card_pos
+
+/-- Extension for the `positivity` tactic: `finset.card s` is positive if `s` is nonempty. -/
+@[positivity]
+meta def positivity_finset_card : expr → tactic strictness
+| `(finset.card %%s) := do -- TODO: Partial decision procedure for `finset.nonempty`
+                          p ← to_expr ``(finset.nonempty %%s) >>= find_assumption,
+                          positive <$> mk_app ``finset.nonempty.card_pos [p]
+| `(@fintype.card %%α %%i) := positive <$> mk_mapp ``fintype.card_pos [α, i, none]
+| e := pp e >>= fail ∘ format.bracket "The expression `"
+    "` isn't of the form `finset.card s` or `fintype.card α`"
+
+end tactic
diff --git a/src/data/int/interval.lean b/src/data/int/interval.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
-import algebra.char_zero
+import algebra.char_zero.lemmas
 import order.locally_finite
 import data.finset.locally_finite
 
diff --git a/src/data/polynomial/ring_division.lean b/src/data/polynomial/ring_division.lean
@@ -3,6 +3,7 @@ Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Johannes Hölzl, Scott Morrison, Jens Wagemaker, Johan Commelin
 -/
+import algebra.char_zero.infinite
 import data.polynomial.algebra_map
 import data.polynomial.degree.lemmas
 import data.polynomial.div
diff --git a/src/tactic/positivity.lean b/src/tactic/positivity.lean
@@ -6,6 +6,7 @@ Authors: Mario Carneiro, Heather Macbeth, Yaël Dillies
 import tactic.norm_num
 import algebra.order.field.power
 import algebra.order.hom.basic
+import data.nat.factorial.basic
 
 /-! # `positivity` tactic
 
@@ -719,20 +720,6 @@ meta def positivity_asc_factorial : expr → tactic strictness
 | e := pp e >>= fail ∘ format.bracket "The expression `"
          "` isn't of the form `nat.asc_factorial n k`"
 
-private lemma card_univ_pos (α : Type*) [fintype α] [nonempty α] :
-  0 < (finset.univ : finset α).card :=
-finset.univ_nonempty.card_pos
-
-/-- Extension for the `positivity` tactic: `finset.card s` is positive if `s` is nonempty. -/
-@[positivity]
-meta def positivity_finset_card : expr → tactic strictness
-| `(finset.card %%s) := do -- TODO: Partial decision procedure for `finset.nonempty`
-                          p ← to_expr ``(finset.nonempty %%s) >>= find_assumption,
-                          positive <$> mk_app ``finset.nonempty.card_pos [p]
-| `(@fintype.card %%α %%i) := positive <$> mk_mapp ``fintype.card_pos [α, i, none]
-| e := pp e >>= fail ∘ format.bracket "The expression `"
-    "` isn't of the form `finset.card s` or `fintype.card α`"
-
 /-- Extension for the `positivity` tactic: nonnegative maps take nonnegative values. -/
 @[positivity]
 meta def positivity_map : expr → tactic strictness
diff --git a/test/library_search/filter.lean b/test/library_search/filter.lean
@@ -6,8 +6,19 @@ open filter
 set_option trace.silence_library_search true
 
 example {α β γ : Type*} {A : filter α} {B : filter β} {C : filter γ} {f : α → β} {g : β → γ}
-  (hf : tendsto f A B) (hg : tendsto g B C) : tendsto (g ∘ f) A C :=
+  (hf : tendsto f A B) (hg : tendsto g B C) : map (g ∘ f) A = map g (map f A) :=
+by library_search
+
+example {α β γ : Type*} {A : filter α} {B : filter β} {C : filter γ} {f : α → β} {g : β → γ}
+  (hf : tendsto f A B) (hg : tendsto g B C) : map g (map f A) ≤ C :=
 calc
-map (g ∘ f) A = map g (map f A) : by library_search
-          ... ≤ map g B         : by library_search!
+map g (map f A) ≤ map g B       : by library_search!
           ... ≤ C               : by library_search!
+
+-- this was the original version of the test, as of Dec 2022 it times out
+-- example {α β γ : Type*} {A : filter α} {B : filter β} {C : filter γ} {f : α → β} {g : β → γ}
+--   (hf : tendsto f A B) (hg : tendsto g B C) : tendsto (g ∘ f) A C :=
+-- calc
+-- map (g ∘ f) A = map g (map f A) : by library_search
+--           ... ≤ map g B         : by library_search!
+--           ... ≤ C               : by library_search!
