feat(data/fintype/basic): make subtype_of_fintype computable (#5919)

This smokes out a few places downstream that are missing decidability hypotheses needed for the fintype instance to exist.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/combinatorics/simple_graph/basic.lean

@@ -101,6 +101,9 @@ variables {V : Type u} (G : simple_graph V)
 /-- `G.neighbor_set v` is the set of vertices adjacent to `v` in `G`. -/
 def neighbor_set (v : V) : set V := set_of (G.adj v)
 
+instance neighbor_set.mem_decidable (v : V) [decidable_rel G.adj] :
+  decidable_pred (∈ G.neighbor_set v) := by { unfold neighbor_set, apply_instance }
+
 lemma ne_of_adj {a b : V} (hab : G.adj a b) : a ≠ b :=
 by { rintro rfl, exact G.loopless a hab }
 
@@ -360,6 +363,11 @@ The maximum degree of all vertices
 def max_degree (G : simple_graph V) [nonempty V] [decidable_rel G.adj] : ℕ :=
 finset.max' (univ.image (λ (v : V), G.degree v)) (nonempty.image univ_nonempty _)
 
+/-! The following lemmas about `fintype.card` use noncomputable decidable instances to get fintype
+assumptions. -/
+section
+open_locale classical
+
 lemma degree_lt_card_verts (G : simple_graph V) (v : V) : G.degree v < fintype.card V :=
 begin
   classical,
@@ -408,6 +416,8 @@ begin
       apply common_neighbors_subset_neighbor_set } },
 end
 
+end
+
 end finite
 
 section complement

src/combinatorics/simple_graph/degree_sum.lean

@@ -177,7 +177,7 @@ G.dart_card_eq_sum_degrees.symm.trans G.dart_card_eq_twice_card_edges
 end degree_sum
 
 /-- The handshaking lemma.  See also `simple_graph.sum_degrees_eq_twice_card_edges`. -/
-theorem even_card_odd_degree_vertices [fintype V] :
+theorem even_card_odd_degree_vertices [fintype V] [decidable_rel G.adj] :
   even (univ.filter (λ v, odd (G.degree v))).card :=
 begin
   classical,
@@ -197,7 +197,7 @@ begin
     trivial }
 end
 
-lemma odd_card_odd_degree_vertices_ne [fintype V] [decidable_eq V]
+lemma odd_card_odd_degree_vertices_ne [fintype V] [decidable_eq V] [decidable_rel G.adj]
   (v : V) (h : odd (G.degree v)) :
   odd (univ.filter (λ w, w ≠ v ∧ odd (G.degree w))).card :=
 begin
@@ -220,7 +220,7 @@ begin
   { simpa only [true_and, mem_filter, mem_univ] },
 end
 
-lemma exists_ne_odd_degree_of_exists_odd_degree [fintype V]
+lemma exists_ne_odd_degree_of_exists_odd_degree [fintype V] [decidable_rel G.adj]
   (v : V) (h : odd (G.degree v)) :
   ∃ (w : V), w ≠ v ∧ odd (G.degree w) :=
 begin

src/data/fintype/basic.lean

@@ -243,6 +243,12 @@ def of_surjective [decidable_eq β] [fintype α] (f : α → β) (H : function.s
   fintype β :=
 ⟨univ.image f, λ b, let ⟨a, e⟩ := H b in e ▸ mem_image_of_mem _ (mem_univ _)⟩
 
+instance subtype_of_fintype {α : Sort*} [fintype α] (p : α → Prop) [decidable_pred p] :
+  fintype (subtype p) :=
+{ elems := ⟨((finset.univ : finset α).filter p).1.pmap subtype.mk (by simp),
+  multiset.nodup_pmap (λ _ _ _ _, subtype.mk.inj) (multiset.nodup_filter p finset.univ.nodup)⟩,
+  complete := λ ⟨x, h⟩, by simp [h] }
+
 /-- Given an injective function to a fintype, the domain is also a
 fintype. This is noncomputable because injectivity alone cannot be
 used to construct preimages. -/
@@ -252,9 +258,6 @@ if hα : nonempty α then by letI := classical.inhabited_of_nonempty hα;
   exact of_surjective (inv_fun f) (inv_fun_surjective H)
 else ⟨∅, λ x, (hα ⟨x⟩).elim⟩
 
-noncomputable instance subtype_of_fintype [fintype α] (p : α → Prop) : fintype (subtype p) :=
-fintype.of_injective coe subtype.coe_injective
-
 /-- If `f : α ≃ β` and `α` is a fintype, then `β` is also a fintype. -/
 def of_equiv (α : Type*) [fintype α] (f : α ≃ β) : fintype β := of_bijective _ f.bijective
 

src/data/fintype/card.lean

@@ -285,7 +285,8 @@ end
 
 @[to_additive]
 lemma finset.prod_to_finset_eq_subtype {M : Type*} [comm_monoid M] [fintype α]
-  (p : α → Prop) (f : α → M) : ∏ a in {x | p x}.to_finset, f a = ∏ a : subtype p, f a :=
+  (p : α → Prop) [decidable_pred p] (f : α → M) :
+    ∏ a in {x | p x}.to_finset, f a = ∏ a : subtype p, f a :=
 by { rw ← finset.prod_subtype, simp }
 
 @[to_additive] lemma finset.prod_fiberwise [decidable_eq β] [fintype β] [comm_monoid γ]

src/field_theory/galois.lean

@@ -321,8 +321,9 @@ begin
   have p : 0 < findim (intermediate_field.fixed_field (⊤ : subgroup (E ≃ₐ[F] E))) E := findim_pos,
   rw [←intermediate_field.findim_eq_one_iff, ←mul_left_inj' (ne_of_lt p).symm, findim_mul_findim,
       ←h, one_mul, intermediate_field.findim_fixed_field_eq_card],
-  exact fintype.card_congr { to_fun := λ g, ⟨g, subgroup.mem_top g⟩, inv_fun := coe,
-    left_inv := λ g, rfl, right_inv := λ _, by { ext, refl } },
+  apply fintype.card_congr,
+  exact { to_fun := λ g, ⟨g, subgroup.mem_top g⟩, inv_fun := coe,
+          left_inv := λ g, rfl, right_inv := λ _, by { ext, refl } },
 end
 
 variables {F} {E} {p : polynomial F}

src/group_theory/order_of_element.lean

@@ -301,6 +301,7 @@ lemma is_cyclic_of_prime_card [group α] [fintype α] {p : ℕ} [hp : fact p.pri
 ⟨begin
   obtain ⟨g, hg⟩ : ∃ g : α, g ≠ 1,
   from fintype.exists_ne_of_one_lt_card (by { rw h, exact nat.prime.one_lt hp }) 1,
+  classical, -- for fintype (subgroup.gpowers g)
   have : fintype.card (subgroup.gpowers g) ∣ p,
   { rw ←h,
     apply card_subgroup_dvd_card },

src/group_theory/perm/subgroup.lean

@@ -21,13 +21,13 @@ universes u
 
 @[simp]
 lemma sum_congr_hom.card_range {α β : Type*}
-  [decidable_eq α] [decidable_eq β] [fintype α] [fintype β] :
+  [fintype (sum_congr_hom α β).range] [fintype (perm α × perm β)] :
   fintype.card (sum_congr_hom α β).range = fintype.card (perm α × perm β) :=
 fintype.card_eq.mpr ⟨(set.range (sum_congr_hom α β) sum_congr_hom_injective).symm⟩
 
 @[simp]
 lemma sigma_congr_right_hom.card_range {α : Type*} {β : α → Type*}
-  [decidable_eq α] [∀ a, decidable_eq (β a)] [fintype α] [∀ a, fintype (β a)] :
+  [fintype (sigma_congr_right_hom β).range] [fintype (Π a, perm (β a))] :
   fintype.card (sigma_congr_right_hom β).range = fintype.card (Π a, perm (β a)) :=
 fintype.card_eq.mpr ⟨(set.range (sigma_congr_right_hom β) sigma_congr_right_hom_injective).symm⟩
 

src/group_theory/subgroup.lean

@@ -160,6 +160,10 @@ lemma coe_coe (K : subgroup G) : ↥(K : set G) = K := rfl
 attribute [norm_cast] add_subgroup.mem_coe
 attribute [norm_cast] add_subgroup.coe_coe
 
+@[to_additive]
+instance (K : subgroup G) [d : decidable_pred K.carrier] [fintype G] : fintype K :=
+show fintype {g : G // g ∈ K.carrier}, from infer_instance
+
 end subgroup
 
 @[to_additive]
@@ -362,10 +366,13 @@ begin
     exact ⟨h x, by { rintros rfl, exact H.one_mem }⟩ },
 end
 
-@[to_additive] lemma eq_top_of_card_eq [fintype G] (h : fintype.card H = fintype.card G) : H = ⊤ :=
+@[to_additive] lemma eq_top_of_card_eq [fintype H] [fintype G]
+  (h : fintype.card H = fintype.card G) : H = ⊤ :=
 begin
+  classical,
+  rw fintype.card_congr (equiv.refl _) at h, -- this swaps the fintype instance to classical
   change fintype.card H.carrier = _ at h,
-  cases H with S hS1 hS2 hS3,
+  unfreezingI { cases H with S hS1 hS2 hS3, },
   have : S = set.univ,
   { suffices : S.to_finset = finset.univ,
     { rwa [←set.to_finset_univ, set.to_finset_inj] at this, },