feat(algebra/char_zero): char_zero.infinite (#4593)

src/algebra/char_zero.lean

@@ -6,6 +6,7 @@ Authors: Mario Carneiro
 Natural homomorphism from the natural numbers into a monoid with one.
 -/
 import data.nat.cast
+import data.fintype.basic
 import tactic.wlog
 
 /-- Typeclass for monoids with characteristic zero.
@@ -60,8 +61,12 @@ end
 
 end nat
 
-@[field_simps] lemma two_ne_zero' {R : Type*} [add_monoid R] [has_one R] [char_zero R] : (2:R) ≠ 0 :=
-have ((2:ℕ):R) ≠ 0, from nat.cast_ne_zero.2 dec_trivial,
+@[priority 100] -- see Note [lower instance priority]
+instance char_zero.infinite (α : Type*) [add_monoid α] [has_one α] [char_zero α] : infinite α :=
+infinite.of_injective coe nat.cast_injective
+
+@[field_simps] lemma two_ne_zero' {α : Type*} [add_monoid α] [has_one α] [char_zero α] : (2:α) ≠ 0 :=
+have ((2:ℕ):α) ≠ 0, from nat.cast_ne_zero.2 dec_trivial,
 by rwa [nat.cast_succ, nat.cast_one] at this
 
 section

src/data/fintype/basic.lean

@@ -1131,8 +1131,13 @@ lemma exists_not_mem_finset [infinite α] (s : finset α) : ∃ x, x ∉ s :=
 not_forall.1 $ λ h, not_fintype ⟨s, h⟩
 
 @[priority 100] -- see Note [lower instance priority]
-instance nonempty (α : Type*) [infinite α] : nonempty α :=
-nonempty_of_exists (exists_not_mem_finset (∅ : finset α))
+instance (α : Type*) [H : infinite α] : nontrivial α :=
+⟨let ⟨x, hx⟩ := exists_not_mem_finset (∅ : finset α) in
+let ⟨y, hy⟩ := exists_not_mem_finset ({x} : finset α) in
+⟨y, x, by simpa only [mem_singleton] using hy⟩⟩
+
+lemma nonempty (α : Type*) [infinite α] : nonempty α :=
+by apply_instance
 
 lemma of_injective [infinite β] (f : β → α) (hf : injective f) : infinite α :=
 ⟨λ I, by exactI not_fintype (fintype.of_injective f hf)⟩