refactor(data/set/finite): use a custom inductive type (#9164)

Currently Lean treats local assumptions `h : finite s` as local instances, so one needs to do something like
```lean
  unfreezingI { lift s to finset α using hs },
```

I change the definition of `set.finite` to an inductive predicate that replicates the definition of `nonempty` and remove `unfreezingI` here and there. Equivalence to the old definition is given by `set.finite_def`.

src/algebra/big_operators/finprod.lean

@@ -482,7 +482,7 @@ over `i ∈ t`. -/
 @[to_additive] lemma finprod_mem_union_inter (hs : s.finite) (ht : t.finite) :
   (∏ᶠ i ∈ s ∪ t, f i) * ∏ᶠ i ∈ s ∩ t, f i = (∏ᶠ i ∈ s, f i) * ∏ᶠ i ∈ t, f i :=
 begin
-  unfreezingI { lift s to finset α using hs, lift t to finset α using ht },
+  lift s to finset α using hs, lift t to finset α using ht,
   classical,
   rw [← finset.coe_union, ← finset.coe_inter],
   simp only [finprod_mem_coe_finset, finset.prod_union_inter]
@@ -661,7 +661,7 @@ of the products of `f a` over `a ∈ t i`. -/
   (h : pairwise (disjoint on t)) (ht : ∀ i, (t i).finite) :
   ∏ᶠ a ∈ (⋃ i : ι, t i), f a = ∏ᶠ i, (∏ᶠ a ∈ t i, f a) :=
 begin
-  unfreezingI { lift t to ι → finset α using ht },
+  lift t to ι → finset α using ht,
   classical,
   rw [← bUnion_univ, ← finset.coe_univ, ← finset.coe_bUnion,
     finprod_mem_coe_finset, finset.prod_bUnion],
@@ -695,7 +695,7 @@ with the product over `t`. -/
   (f : α → β → M) (hs : s.finite) (ht : t.finite) :
   ∏ᶠ i ∈ s, ∏ᶠ j ∈ t, f i j = ∏ᶠ j ∈ t, ∏ᶠ i ∈ s, f i j :=
 begin
-  unfreezingI { lift s to finset α using hs, lift t to finset β using ht },
+  lift s to finset α using hs, lift t to finset β using ht,
   simp only [finprod_mem_coe_finset],
   exact finset.prod_comm
 end

src/data/mv_polynomial/funext.lean

@@ -27,10 +27,8 @@ variables {R : Type*} [integral_domain R] [infinite R]
 private lemma funext_fin {n : ℕ} {p : mv_polynomial (fin n) R}
   (h : ∀ x : fin n → R, eval x p = 0) : p = 0 :=
 begin
-  unfreezingI { revert R },
-  induction n with n ih,
-  { introsI R _ _ p h,
-    let e := (mv_polynomial.is_empty_ring_equiv R (fin 0)),
+  unfreezingI { induction n with n ih generalizing R },
+  { let e := (mv_polynomial.is_empty_ring_equiv R (fin 0)),
     apply e.injective,
     rw ring_equiv.map_zero,
     convert h fin_zero_elim,
@@ -41,8 +39,7 @@ begin
         ring_equiv.trans_apply, aeval_eq_eval₂_hom],
       congr },
     exact eval₂_hom_congr rfl (subsingleton.elim _ _) rfl },
-  { introsI R _ _ p h,
-    let e := (fin_succ_equiv R n).to_ring_equiv,
+  { let e := (fin_succ_equiv R n).to_ring_equiv,
     apply e.injective,
     simp only [ring_equiv.map_zero],
     apply polynomial.funext,

src/data/set/finite.lean

@@ -21,7 +21,10 @@ namespace set
 
 /-- A set is finite if the subtype is a fintype, i.e. there is a
   list that enumerates its members. -/
-def finite (s : set α) : Prop := nonempty (fintype s)
+inductive finite (s : set α) : Prop
+| intro : fintype s → finite
+
+lemma finite_def {s : set α} : finite s ↔ nonempty (fintype s) := ⟨λ ⟨h⟩, ⟨h⟩, λ ⟨h⟩, ⟨h⟩⟩
 
 /-- A set is infinite if it is not finite. -/
 def infinite (s : set α) : Prop := ¬ finite s
@@ -30,7 +33,7 @@ def infinite (s : set α) : Prop := ¬ finite s
 that because `finite` isn't a typeclass, this will not fire if it
 is made into an instance -/
 noncomputable def finite.fintype {s : set α} (h : finite s) : fintype s :=
-classical.choice h
+classical.choice $ finite_def.1 h
 
 /-- Get a finset from a finite set -/
 noncomputable def finite.to_finset {s : set α} (h : finite s) : finset α :=
@@ -243,7 +246,7 @@ theorem infinite_univ [h : _root_.infinite α] : infinite (@univ α) :=
 infinite_univ_iff.2 h
 
 theorem infinite_coe_iff {s : set α} : _root_.infinite s ↔ infinite s :=
-⟨λ ⟨h₁⟩ h₂, h₁ h₂.some, λ h₁, ⟨λ h₂, h₁ ⟨h₂⟩⟩⟩
+⟨λ ⟨h₁⟩ h₂, h₁ h₂.fintype, λ h₁, ⟨λ h₂, h₁ ⟨h₂⟩⟩⟩
 
 theorem infinite.to_subtype {s : set α} (h : infinite s) : _root_.infinite s :=
 infinite_coe_iff.2 h
@@ -387,7 +390,7 @@ theorem infinite.exists_ne_map_eq_of_maps_to {s : set α} {t : set β} {f : α 
   (hs : infinite s) (hf : maps_to f s t) (ht : finite t) :
   ∃ (x ∈ s) (y ∈ s), x ≠ y ∧ f x = f y :=
 begin
-  unfreezingI { contrapose! ht },
+  contrapose! ht,
   exact infinite_of_inj_on_maps_to (λ x hx y hy, not_imp_not.1 (ht x hx y hy)) hf hs
 end
 

src/field_theory/finiteness.lean

@@ -31,19 +31,15 @@ its dimension (as a cardinal) is strictly less than the first infinite cardinal
 lemma iff_dim_lt_omega : is_noetherian K V ↔ module.rank K V < omega.{v} :=
 begin
   let b := basis.of_vector_space K V,
-  have := b.mk_eq_dim,
-  simp only [lift_id] at this,
-  rw [← this, lt_omega_iff_fintype, ← @set.set_of_mem_eq _ (basis.of_vector_space_index K V),
-      ← subtype.range_coe_subtype],
+  rw [← b.mk_eq_dim'', lt_omega_iff_finite],
   split,
-  { intro,
-    resetI,
-    simpa using finite_of_linear_independent (basis.of_vector_space_index.linear_independent K V) },
+  { introI,
+    exact finite_of_linear_independent (basis.of_vector_space_index.linear_independent K V) },
   { assume hbfinite,
     refine @is_noetherian_of_linear_equiv K (⊤ : submodule K V) V _
       _ _ _ _ (linear_equiv.of_top _ rfl) (id _),
     refine is_noetherian_of_fg_of_noetherian _ ⟨set.finite.to_finset hbfinite, _⟩,
-    rw [set.finite.coe_to_finset, ← b.span_eq, basis.coe_of_vector_space] }
+    rw [set.finite.coe_to_finset, ← b.span_eq, basis.coe_of_vector_space, subtype.range_coe] }
 end
 
 variables (K V)

src/field_theory/separable.lean

@@ -383,8 +383,8 @@ else or.inl $ (separable_iff_derivative_ne_zero hf).2 H
 theorem exists_separable_of_irreducible {f : polynomial F} (hf : irreducible f) (hf0 : f ≠ 0) :
   ∃ (n : ℕ) (g : polynomial F), g.separable ∧ expand F (p ^ n) g = f :=
 begin
-  generalize hn : f.nat_degree = N, unfreezingI { revert f },
-  apply nat.strong_induction_on N, intros N ih f hf hf0 hn,
+  unfreezingI {
+    induction hn : f.nat_degree using nat.strong_induction_on with N ih generalizing f },
   rcases separable_or p hf with h | ⟨h1, g, hg, hgf⟩,
   { refine ⟨0, f, h, _⟩, rw [pow_zero, expand_one] },
   { cases N with N,

src/geometry/euclidean/circumcenter.lean

@@ -196,8 +196,7 @@ lemma _root_.affine_independent.exists_unique_dist_eq {ι : Type*} [hne : nonemp
   ∃! cccr : (P × ℝ), cccr.fst ∈ affine_span ℝ (set.range p) ∧
     ∀ i, dist (p i) cccr.fst = cccr.snd :=
 begin
-  generalize' hn : fintype.card ι = n,
-  unfreezingI { induction n with m hm generalizing ι },
+  unfreezingI { induction hn : fintype.card ι with m hm generalizing ι },
   { exfalso,
     have h := fintype.card_pos_iff.2 hne,
     rw hn at h,

src/linear_algebra/dimension.lean

@@ -755,7 +755,7 @@ classical.choice (b.nonempty_fintype_index_of_dim_lt_omega h)
 lemma basis.finite_index_of_dim_lt_omega {ι : Type*} {s : set ι}
   (b : basis s R M) (h : module.rank R M < cardinal.omega) :
   s.finite :=
-b.nonempty_fintype_index_of_dim_lt_omega h
+finite_def.2 (b.nonempty_fintype_index_of_dim_lt_omega h)
 
 lemma dim_span {v : ι → M} (hv : linear_independent R v) :
   module.rank R ↥(span R (range v)) = cardinal.mk (range v) :=
@@ -780,7 +780,7 @@ variables {K V}
 /-- If a vector space has a finite dimension, the index set of `basis.of_vector_space` is finite. -/
 lemma basis.finite_of_vector_space_index_of_dim_lt_omega (h : module.rank K V < cardinal.omega) :
   (basis.of_vector_space_index K V).finite :=
-(basis.of_vector_space K V).nonempty_fintype_index_of_dim_lt_omega h
+finite_def.2 $ (basis.of_vector_space K V).nonempty_fintype_index_of_dim_lt_omega h
 
 variables [add_comm_group V'] [module K V']
 

src/linear_algebra/finite_dimensional.lean

@@ -330,11 +330,11 @@ begin
       (submodule.subtype S) (by simpa using bS.linear_independent) (by simp),
   set b := basis.extend this with b_eq,
   letI : fintype (this.extend _) :=
-    classical.choice (finite_of_linear_independent (by simpa using b.linear_independent)),
+    (finite_of_linear_independent (by simpa using b.linear_independent)).fintype,
   letI : fintype (subtype.val '' basis.of_vector_space_index K S) :=
-    classical.choice (finite_of_linear_independent this),
+    (finite_of_linear_independent this).fintype,
   letI : fintype (basis.of_vector_space_index K S) :=
-    classical.choice (finite_of_linear_independent (by simpa using bS.linear_independent)),
+    (finite_of_linear_independent (by simpa using bS.linear_independent)).fintype,
   have : subtype.val '' (basis.of_vector_space_index K S) = this.extend (set.subset_univ _),
   from set.eq_of_subset_of_card_le (this.subset_extend _)
     (by rw [set.card_image_of_injective _ subtype.val_injective, ← finrank_eq_card_basis bS,

src/order/conditionally_complete_lattice.lean

@@ -513,7 +513,7 @@ lemma finset.nonempty.cInf_mem {s : finset α} (h : s.nonempty) : Inf (s : set 
 @finset.nonempty.cSup_mem (order_dual α) _ _ h
 
 lemma set.nonempty.cSup_mem (h : s.nonempty) (hs : finite s) : Sup s ∈ s :=
-by { unfreezingI { lift s to finset α using hs }, exact finset.nonempty.cSup_mem h }
+by { lift s to finset α using hs, exact finset.nonempty.cSup_mem h }
 
 lemma set.nonempty.cInf_mem (h : s.nonempty) (hs : finite s) : Inf s ∈ s :=
 @set.nonempty.cSup_mem (order_dual α) _ _ h hs

src/order/filter/basic.lean

@@ -870,7 +870,7 @@ by simpa using infi_principal_finset finset.univ f
 lemma infi_principal_finite {ι : Type w} {s : set ι} (hs : finite s) (f : ι → set α) :
   (⨅ i ∈ s, 𝓟 (f i)) = 𝓟 (⋂ i ∈ s, f i) :=
 begin
-  unfreezingI { lift s to finset ι using hs }, -- TODO: why `unfreezingI` is needed?
+  lift s to finset ι using hs,
   exact_mod_cast infi_principal_finset s f
 end
 

src/set_theory/cardinal.lean

@@ -812,7 +812,7 @@ lt_omega.trans ⟨λ ⟨n, e⟩, begin
 end, λ ⟨_⟩, by exactI ⟨_, fintype_card _⟩⟩
 
 theorem lt_omega_iff_finite {α} {S : set α} : mk S < omega ↔ finite S :=
-lt_omega_iff_fintype
+lt_omega_iff_fintype.trans finite_def.symm
 
 instance can_lift_cardinal_nat : can_lift cardinal ℕ :=
 ⟨ coe, λ x, x < omega, λ x hx, let ⟨n, hn⟩ := lt_omega.mp hx in ⟨n, hn.symm⟩⟩