chore(data/fintype): rework fintype.equiv_fin and dependencies (#7136)

These changes should make the declarations `fintype.equiv_fin`, `fintype.card_eq`
and `fintype.equiv_of_card_eq` more convenient to use.

Renamed:
 * `fintype.equiv_fin` -> `fintype.trunc_equiv_fin`

Deleted:
 * `fintype.nonempty_equiv_of_card_eq` (use `fintype.equiv_of_card_eq` instead)
 * `fintype.exists_equiv_fin` (use `fintype.card` and `fintype.(trunc_)equiv_fin` instead)

Added:
 * `fintype.equiv_fin`: noncomputable, non-`trunc` version of `fintype.equiv_fin`
 * `fintype.equiv_of_card_eq`: noncomputable, non-`trunc` version of `fintype.trunc_equiv_of_card_eq`
 * `fintype.(trunc_)equiv_fin_of_card_eq` (intermediate result/specialization of `fintype.(trunc_)equiv_of_card_eq`

[Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/.60fintype.2Eequiv_fin.60.20.2B.20.60fin.2Ecast.60)



Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

src/category_theory/Fintype.lean

@@ -82,7 +82,7 @@ instance : full incl := { preimage := λ _ _ f, f }
 instance : faithful incl := {}
 instance : ess_surj incl :=
 { mem_ess_image := λ X,
-  let F := trunc.out (fintype.equiv_fin X) in
+  let F := fintype.equiv_fin X in
   ⟨fintype.card X, ⟨⟨F.symm, F, F.self_comp_symm, F.symm_comp_self⟩⟩⟩ }
 
 noncomputable instance : is_equivalence incl :=

src/category_theory/limits/constructions/finite_products_of_binary_products.lean

@@ -136,7 +136,7 @@ end }
 lemma has_finite_products_of_has_binary_and_terminal : has_finite_products C :=
 ⟨λ J 𝒥₁ 𝒥₂, begin
   resetI,
-  rcases fintype.equiv_fin J with ⟨e⟩,
+  let e := fintype.equiv_fin J,
   apply has_limits_of_shape_of_equivalence (discrete.equivalence (e.trans equiv.ulift.symm)).symm,
   refine has_limits_of_shape_ulift_fin (fintype.card J),
 end⟩
@@ -205,8 +205,7 @@ def preserves_finite_products_of_preserves_binary_and_terminal
   preserves_limits_of_shape.{v} (discrete J) F :=
 begin
   classical,
-  refine trunc.rec_on_subsingleton (fintype.equiv_fin J) _,
-  intro e,
+  let e := fintype.equiv_fin J,
   haveI := preserves_ulift_fin_of_preserves_binary_and_terminal F (fintype.card J),
   apply preserves_limits_of_shape_of_equiv (discrete.equivalence (e.trans equiv.ulift.symm)).symm,
 end
@@ -316,7 +315,7 @@ end }
 lemma has_finite_coproducts_of_has_binary_and_terminal : has_finite_coproducts C :=
 ⟨λ J 𝒥₁ 𝒥₂, begin
   resetI,
-  rcases fintype.equiv_fin J with ⟨e⟩,
+  let e := fintype.equiv_fin J,
   apply has_colimits_of_shape_of_equivalence (discrete.equivalence (e.trans equiv.ulift.symm)).symm,
   refine has_colimits_of_shape_ulift_fin (fintype.card J),
 end⟩
@@ -384,8 +383,7 @@ def preserves_finite_coproducts_of_preserves_binary_and_initial
   preserves_colimits_of_shape.{v} (discrete J) F :=
 begin
   classical,
-  refine trunc.rec_on_subsingleton (fintype.equiv_fin J) _,
-  intro e,
+  let e := fintype.equiv_fin J,
   haveI := preserves_ulift_fin_of_preserves_binary_and_initial F (fintype.card J),
   apply preserves_colimits_of_shape_of_equiv (discrete.equivalence (e.trans equiv.ulift.symm)).symm,
 end

src/computability/turing_machine.lean

@@ -1366,7 +1366,9 @@ theorem exists_enc_dec [fintype Γ] :
   ∃ n (enc : Γ → vector bool n) (dec : vector bool n → Γ),
     enc (default _) = vector.repeat ff n ∧ ∀ a, dec (enc a) = a :=
 begin
-  rcases fintype.exists_equiv_fin Γ with ⟨n, ⟨F⟩⟩,
+  letI := classical.dec_eq Γ,
+  let n := fintype.card Γ,
+  obtain ⟨F⟩ := fintype.trunc_equiv_fin Γ,
   let G : fin n ↪ fin n → bool := ⟨λ a b, a = b,
     λ a b h, of_to_bool_true $ (congr_fun h b).trans $ to_bool_tt rfl⟩,
   let H := (F.to_embedding.trans G).trans

src/data/equiv/list.lean

@@ -114,7 +114,7 @@ by haveI := decidable_eq_of_encodable α; exact
 
 def fintype_arrow (α : Type*) (β : Type*) [decidable_eq α] [fintype α] [encodable β] :
   trunc (encodable (α → β)) :=
-(fintype.equiv_fin α).map $
+(fintype.trunc_equiv_fin α).map $
   λf, encodable.of_equiv (fin (fintype.card α) → β) $
   equiv.arrow_congr f (equiv.refl _)
 

src/data/fintype/basic.lean

@@ -241,18 +241,30 @@ def equiv_fin_of_forall_mem_list {α} [decidable_eq α]
  λ ⟨i, h⟩, fin.eq_of_veq $ list.nodup_iff_nth_le_inj.1 nd _ _
    (list.index_of_lt_length.2 (list.nth_le_mem _ _ _)) h $ by simp⟩
 
-/-- There is (computably) a bijection between `α` and `fin n` where
-  `n = card α`. Since it is not unique, and depends on which permutation
-  of the universe list is used, the bijection is wrapped in `trunc` to
-  preserve computability.  -/
-def equiv_fin (α) [decidable_eq α] [fintype α] : trunc (α ≃ fin (card α)) :=
+/-- There is (computably) a bijection between `α` and `fin (card α)`.
+
+Since it is not unique, and depends on which permutation
+of the universe list is used, the bijection is wrapped in `trunc` to
+preserve computability.
+
+See `fintype.equiv_fin` for the noncomputable version,
+and `fintype.trunc_equiv_fin_of_card_eq` and `fintype.equiv_fin_of_card_eq`
+for an equiv `α ≃ fin n` given `fintype.card α = n`.
+-/
+def trunc_equiv_fin (α) [decidable_eq α] [fintype α] : trunc (α ≃ fin (card α)) :=
 by unfold card finset.card; exact
 quot.rec_on_subsingleton (@univ α _).1
   (λ l (h : ∀ x:α, x ∈ l) (nd : l.nodup), trunc.mk (equiv_fin_of_forall_mem_list h nd))
   mem_univ_val univ.2
 
-theorem exists_equiv_fin (α) [fintype α] : ∃ n, nonempty (α ≃ fin n) :=
-by haveI := classical.dec_eq α; exact ⟨card α, (equiv_fin α).nonempty⟩
+/-- There is a (noncomputable) bijection between `α` and `fin (card α)`.
+
+See `fintype.trunc_equiv_fin` for the computable version,
+and `fintype.trunc_equiv_fin_of_card_eq` and `fintype.equiv_fin_of_card_eq`
+for an equiv `α ≃ fin n` given `fintype.card α = n`.
+-/
+noncomputable def equiv_fin (α) [fintype α] : α ≃ fin (card α) :=
+by { letI := classical.dec_eq α, exact (trunc_equiv_fin α).out }
 
 instance (α : Type*) : subsingleton (fintype α) :=
 ⟨λ ⟨s₁, h₁⟩ ⟨s₂, h₂⟩, by congr; simp [finset.ext_iff, h₁, h₂]⟩
@@ -405,12 +417,54 @@ multiset.card_map _ _
 theorem card_congr {α β} [fintype α] [fintype β] (f : α ≃ β) : card α = card β :=
 by rw ← of_equiv_card f; congr
 
+section
+
+variables [fintype α] [fintype β]
+
+/-- If the cardinality of `α` is `n`, there is computably a bijection between `α` and `fin n`.
+
+See `fintype.equiv_fin_of_card_eq` for the noncomputable definition,
+and `fintype.trunc_equiv_fin` and `fintype.equiv_fin` for the bijection `α ≃ fin (card α)`.
+-/
+def trunc_equiv_fin_of_card_eq [decidable_eq α] {n : ℕ} (h : fintype.card α = n) :
+  trunc (α ≃ fin n) :=
+(trunc_equiv_fin α).map (λ e, e.trans (fin.cast h).to_equiv)
+
+
+/-- If the cardinality of `α` is `n`, there is noncomputably a bijection between `α` and `fin n`.
+
+See `fintype.trunc_equiv_fin_of_card_eq` for the computable definition,
+and `fintype.trunc_equiv_fin` and `fintype.equiv_fin` for the bijection `α ≃ fin (card α)`.
+-/
+noncomputable def equiv_fin_of_card_eq {n : ℕ} (h : fintype.card α = n) :
+  α ≃ fin n :=
+by { letI := classical.dec_eq α, exact (trunc_equiv_fin_of_card_eq h).out }
+
+/-- Two `fintype`s with the same cardinality are (computably) in bijection.
+
+See `fintype.equiv_of_card_eq` for the noncomputable version,
+and `fintype.trunc_equiv_fin_of_card_eq` and `fintype.equiv_fin_of_card_eq` for
+the specialization to `fin`.
+-/
+def trunc_equiv_of_card_eq [decidable_eq α] [decidable_eq β] (h : card α = card β) :
+  trunc (α ≃ β) :=
+(trunc_equiv_fin_of_card_eq h).bind (λ e, (trunc_equiv_fin β).map (λ e', e.trans e'.symm))
+
+/-- Two `fintype`s with the same cardinality are (noncomputably) in bijection.
+
+See `fintype.trunc_equiv_of_card_eq` for the computable version,
+and `fintype.trunc_equiv_fin_of_card_eq` and `fintype.equiv_fin_of_card_eq` for
+the specialization to `fin`.
+-/
+noncomputable def equiv_of_card_eq (h : card α = card β) : α ≃ β :=
+by { letI := classical.dec_eq α, letI := classical.dec_eq β,
+     exact (trunc_equiv_of_card_eq h).out }
+
+end
+
 theorem card_eq {α β} [F : fintype α] [G : fintype β] : card α = card β ↔ nonempty (α ≃ β) :=
-⟨λ h, ⟨by classical;
-  calc α ≃ fin (card α) : trunc.out (equiv_fin α)
-     ... ≃ fin (card β) : by rw h
-     ... ≃ β : (trunc.out (equiv_fin β)).symm⟩,
-λ ⟨f⟩, card_congr f⟩
+⟨λ h, by { haveI := classical.prop_decidable, exact (trunc_equiv_of_card_eq h).nonempty },
+ λ ⟨f⟩, card_congr f⟩
 
 /-- Any subsingleton type with a witness is a fintype (with one term). -/
 def of_subsingleton (a : α) [subsingleton α] : fintype α :=
@@ -829,29 +883,14 @@ have injective (e.symm ∘ f) ↔ surjective (e.symm ∘ f), from injective_iff_
 λ hsurj, by simpa [function.comp] using
   e.injective.comp (this.2 (e.symm.surjective.comp hsurj))⟩
 
-lemma nonempty_equiv_of_card_eq (h : card α = card β) :
-  nonempty (α ≃ β) :=
-begin
-  obtain ⟨m, ⟨f⟩⟩ := exists_equiv_fin α,
-  obtain ⟨n, ⟨g⟩⟩ := exists_equiv_fin β,
-  suffices : m = n,
-  { subst this, exact ⟨f.trans g.symm⟩ },
-  calc m = card (fin m) : (card_fin m).symm
-     ... = card α       : card_congr f.symm
-     ... = card β       : h
-     ... = card (fin n) : card_congr g
-     ... = n            : card_fin n
-end
-
 lemma bijective_iff_injective_and_card (f : α → β) :
   bijective f ↔ injective f ∧ card α = card β :=
 begin
   split,
   { intro h, exact ⟨h.1, card_congr (equiv.of_bijective f h)⟩ },
   { rintro ⟨hf, h⟩,
     refine ⟨hf, _⟩,
-    obtain ⟨e⟩ : nonempty (α ≃ β) := nonempty_equiv_of_card_eq h,
-    rwa ← injective_iff_surjective_of_equiv e }
+    rwa ← injective_iff_surjective_of_equiv (equiv_of_card_eq h) }
 end
 
 lemma bijective_iff_surjective_and_card (f : α → β) :
@@ -861,8 +900,7 @@ begin
   { intro h, exact ⟨h.2, card_congr (equiv.of_bijective f h)⟩, },
   { rintro ⟨hf, h⟩,
     refine ⟨_, hf⟩,
-    obtain ⟨e⟩ : nonempty (α ≃ β) := nonempty_equiv_of_card_eq h,
-    rwa injective_iff_surjective_of_equiv e }
+    rwa injective_iff_surjective_of_equiv (equiv_of_card_eq h) }
 end
 
 end fintype
@@ -1258,8 +1296,8 @@ def fintype_perm [fintype α] : fintype (perm α) :=
 
 instance [fintype α] [fintype β] : fintype (α ≃ β) :=
 if h : fintype.card β = fintype.card α
-then trunc.rec_on_subsingleton (fintype.equiv_fin α)
-  (λ eα, trunc.rec_on_subsingleton (fintype.equiv_fin β)
+then trunc.rec_on_subsingleton (fintype.trunc_equiv_fin α)
+  (λ eα, trunc.rec_on_subsingleton (fintype.trunc_equiv_fin β)
     (λ eβ, @fintype.of_equiv _ (perm α) fintype_perm
       (equiv_congr (equiv.refl α) (eα.trans (eq.rec_on h eβ.symm)) : (α ≃ α) ≃ (α ≃ β))))
 else ⟨∅, λ x, false.elim (h (fintype.card_eq.2 ⟨x.symm⟩))⟩

src/data/mv_polynomial/rename.lean

@@ -188,7 +188,8 @@ theorem exists_fin_rename (p : mv_polynomial σ R) :
   ∃ (n : ℕ) (f : fin n → σ) (hf : injective f) (q : mv_polynomial (fin n) R), p = rename f q :=
 begin
   obtain ⟨s, q, rfl⟩ := exists_finset_rename p,
-  obtain ⟨n, ⟨e⟩⟩ := fintype.exists_equiv_fin {x // x ∈ s},
+  let n := fintype.card {x // x ∈ s},
+  let e := fintype.equiv_fin {x // x ∈ s},
   refine ⟨n, coe ∘ e.symm, subtype.val_injective.comp e.symm.injective, rename e q, _⟩,
   rw [← rename_rename, rename_rename e],
   simp only [function.comp, equiv.symm_apply_apply, rename_rename]

src/data/set/finite.lean

@@ -84,11 +84,7 @@ theorem exists_finite_iff_finset {p : set α → Prop} :
   λ ⟨s, hs⟩, ⟨↑s, finite_mem_finset s, hs⟩⟩
 
 lemma finite.fin_embedding {s : set α} (h : finite s) : ∃ (n : ℕ) (f : fin n ↪ α), range f = s :=
-begin
-  classical,
-  obtain ⟨f⟩ := (fintype.equiv_fin (h.to_finset : set α)).nonempty,
-  exact ⟨_, f.symm.as_embedding, by simp⟩
-end
+⟨_, (fintype.equiv_fin (h.to_finset : set α)).symm.as_embedding, by simp⟩
 
 lemma finite.fin_param {s : set α} (h : finite s) :
   ∃ (n : ℕ) (f : fin n → α), injective f ∧ range f = s :=

src/field_theory/finite/polynomial.lean

@@ -172,10 +172,7 @@ calc module.rank K (R σ K) =
   ... = cardinal.mk (σ → fin (fintype.card K)) :
     quotient.sound ⟨equiv.arrow_congr (equiv.refl σ) (equiv.fin_equiv_subtype _).symm⟩
   ... = cardinal.mk (σ → K) :
-  begin
-    refine (trunc.induction_on (fintype.equiv_fin K) $ assume (e : K ≃ fin (fintype.card K)), _),
-    refine quotient.sound ⟨equiv.arrow_congr (equiv.refl σ) e.symm⟩
-  end
+    quotient.sound ⟨equiv.arrow_congr (equiv.refl σ) (fintype.equiv_fin K).symm⟩
   ... = fintype.card (σ → K) : cardinal.fintype_card _
 
 instance : finite_dimensional K (R σ K) :=

src/group_theory/perm/sign.lean

@@ -652,7 +652,7 @@ end
   `sign_aux2 f _` recursively calculates the sign of `f`. -/
 def sign_aux3 [fintype α] (f : perm α) {s : multiset α} : (∀ x, x ∈ s) → units ℤ :=
 quotient.hrec_on s (λ l h, sign_aux2 l f)
-  (trunc.induction_on (equiv_fin α)
+  (trunc.induction_on (fintype.trunc_equiv_fin α)
     (λ e l₁ l₂ h, function.hfunext
       (show (∀ x, x ∈ l₁) = ∀ x, x ∈ l₂, by simp only [h.mem_iff])
       (λ h₁ h₂ _, by rw [← sign_aux_eq_sign_aux2 _ _ e (λ _ _, h₁ _),
@@ -662,9 +662,9 @@ lemma sign_aux3_mul_and_swap [fintype α] (f g : perm α) (s : multiset α) (hs
   sign_aux3 (f * g) hs = sign_aux3 f hs * sign_aux3 g hs ∧ ∀ x y, x ≠ y →
   sign_aux3 (swap x y) hs = -1 :=
 let ⟨l, hl⟩ := quotient.exists_rep s in
-let ⟨e, _⟩ := (equiv_fin α).exists_rep in
+let e := equiv_fin α in
 begin
-  clear _let_match _let_match,
+  clear _let_match,
   subst hl,
   show sign_aux2 l (f * g) = sign_aux2 l f * sign_aux2 l g ∧
     ∀ x y, x ≠ y → sign_aux2 l (swap x y) = -1,
@@ -722,7 +722,7 @@ lemma sign_aux3_symm_trans_trans [decidable_eq β] [fintype β] (f : perm α)
   sign_aux3 ((e.symm.trans f).trans e) ht = sign_aux3 f hs :=
 quotient.induction_on₂ t s
   (λ l₁ l₂ h₁ h₂, show sign_aux2 _ _ = sign_aux2 _ _,
-    from let n := (equiv_fin β).out in
+    from let n := equiv_fin β in
     by { rw [← sign_aux_eq_sign_aux2 _ _ n (λ _ _, h₁ _),
         ← sign_aux_eq_sign_aux2 _ _ (e.trans n) (λ _ _, h₂ _)],
       exact congr_arg sign_aux

src/linear_algebra/free_module.lean

@@ -221,8 +221,8 @@ lemma is_basis.card_le_card_of_linear_independent
 begin
   haveI := classical.dec_eq ι,
   haveI := classical.dec_eq ι',
-  obtain ⟨e⟩ := fintype.equiv_fin ι,
-  obtain ⟨e'⟩ := fintype.equiv_fin ι',
+  let e := fintype.equiv_fin ι,
+  let e' := fintype.equiv_fin ι',
   have hb := hb.comp _ e.symm.bijective,
   have hv := (linear_independent_equiv e'.symm).mpr hv,
   have hv := hv.map' _ hb.equiv_fun.ker,

src/logic/small.lean

@@ -80,8 +80,7 @@ end
 @[priority 100]
 instance small_of_fintype (α : Type v) [fintype α] : small.{w} α :=
 begin
-  obtain ⟨n, ⟨e⟩⟩ := fintype.exists_equiv_fin α,
-  rw small_congr e,
+  rw small_congr (fintype.equiv_fin α),
   apply_instance,
 end
 

src/ring_theory/finiteness.lean

@@ -196,9 +196,10 @@ begin
   split,
   { rw iff_quotient_mv_polynomial',
     rintro ⟨ι, hfintype, ⟨f, hsur⟩⟩,
-    obtain ⟨n, equiv⟩ := @fintype.exists_equiv_fin ι hfintype,
-    replace equiv := mv_polynomial.rename_equiv R (nonempty.some equiv),
-    exact ⟨n, alg_hom.comp f equiv.symm, function.surjective.comp hsur
+    letI := hfintype,
+    obtain ⟨equiv⟩ := @fintype.trunc_equiv_fin ι (classical.dec_eq ι) hfintype,
+    replace equiv := mv_polynomial.rename_equiv R equiv,
+    exact ⟨fintype.card ι, alg_hom.comp f equiv.symm, function.surjective.comp hsur
       (alg_equiv.symm equiv).surjective⟩ },
   { rintro ⟨n, ⟨f, hsur⟩⟩,
     exact finite_type.of_surjective (finite_type.mv_polynomial R (fin n)) f hsur }
@@ -252,9 +253,9 @@ variable (R)
 /-- The ring of polynomials in finitely many variables is finitely presented. -/
 lemma mv_polynomial (ι : Type u_2) [fintype ι] : finite_presentation R (mv_polynomial ι R) :=
 begin
-  obtain ⟨n, equiv⟩ := @fintype.exists_equiv_fin ι _,
-  replace equiv := mv_polynomial.rename_equiv R (nonempty.some equiv),
-  use [n, alg_equiv.to_alg_hom equiv.symm],
+  obtain ⟨equiv⟩ := @fintype.trunc_equiv_fin ι (classical.dec_eq ι) _,
+  replace equiv := mv_polynomial.rename_equiv R equiv,
+  refine ⟨_, alg_equiv.to_alg_hom equiv.symm, _⟩,
   split,
   { exact (alg_equiv.symm equiv).surjective },
   suffices hinj : function.injective equiv.symm.to_alg_hom.to_ring_hom,
@@ -312,9 +313,9 @@ begin
     exact ring_hom.ker_coe_equiv ulift_var.to_ring_equiv, },
   { rintro ⟨ι, hfintype, f, hf⟩,
     haveI : fintype ι := hfintype,
-    obtain ⟨n, equiv⟩ := fintype.exists_equiv_fin ι,
-    replace equiv := mv_polynomial.rename_equiv R (nonempty.some equiv),
-    refine ⟨n, f.comp equiv.symm,
+    obtain ⟨equiv⟩ := @fintype.trunc_equiv_fin ι (classical.dec_eq ι) _,
+    replace equiv := mv_polynomial.rename_equiv R equiv,
+    refine ⟨fintype.card ι, f.comp equiv.symm,
       hf.1.comp (alg_equiv.symm equiv).surjective,
       submodule.fg_ker_ring_hom_comp _ f _ hf.2 equiv.symm.surjective⟩,
     convert submodule.fg_bot,
@@ -326,8 +327,10 @@ as `R`-algebra. -/
 lemma mv_polynomial_of_finite_presentation (hfp : finite_presentation R A) (ι : Type*)
   [fintype ι] : finite_presentation R (_root_.mv_polynomial ι A) :=
 begin
-  obtain ⟨n, e⟩ := fintype.exists_equiv_fin ι,
-  replace e := (mv_polynomial.rename_equiv A (nonempty.some e)).restrict_scalars R,
+  classical,
+  let n := fintype.card ι,
+  obtain ⟨e⟩ := fintype.trunc_equiv_fin ι,
+  replace e := (mv_polynomial.rename_equiv A e).restrict_scalars R,
   refine equiv _ e.symm,
   obtain ⟨m, I, e, hfg⟩ := iff.1 hfp,
   refine equiv _ (mv_polynomial.map_alg_equiv (fin n) e),

src/ring_theory/jacobson.lean

@@ -552,7 +552,7 @@ instance {R : Type*} [comm_ring R] {ι : Type*} [fintype ι] [is_jacobson R] :
   is_jacobson (mv_polynomial ι R) :=
 begin
   haveI := classical.dec_eq ι,
-  obtain ⟨e⟩ := fintype.equiv_fin ι,
+  let e := fintype.equiv_fin ι,
   rw is_jacobson_iso (rename_equiv R e).to_ring_equiv,
   exact is_jacobson_mv_polynomial_fin _
 end
@@ -595,7 +595,7 @@ lemma comp_C_integral_of_surjective_of_jacobson {R : Type*} [integral_domain R]
   (hf : function.surjective f) : (f.comp C).is_integral :=
 begin
   haveI := classical.dec_eq σ,
-  obtain ⟨e⟩ := fintype.equiv_fin σ,
+  obtain ⟨e⟩ := fintype.trunc_equiv_fin σ,
   let f' : mv_polynomial (fin _) R →+* S :=
     f.comp (rename_equiv R e.symm).to_ring_equiv.to_ring_hom,
   have hf' : function.surjective f' :=

src/ring_theory/polynomial/basic.lean

@@ -682,9 +682,8 @@ theorem is_noetherian_ring_fin [is_noetherian_ring R] :
 is itself a noetherian ring. -/
 instance is_noetherian_ring [fintype σ] [is_noetherian_ring R] :
   is_noetherian_ring (mv_polynomial σ R) :=
-trunc.induction_on (fintype.equiv_fin σ) $ λ e,
 @is_noetherian_ring_of_ring_equiv (mv_polynomial (fin (fintype.card σ)) R) _ _ _
-  (rename_equiv R e.symm).to_ring_equiv is_noetherian_ring_fin
+  (rename_equiv R (fintype.equiv_fin σ).symm).to_ring_equiv is_noetherian_ring_fin
 
 lemma is_integral_domain_fin_zero (R : Type u) [comm_ring R] (hR : is_integral_domain R) :
   is_integral_domain (mv_polynomial (fin 0) R) :=
@@ -708,10 +707,9 @@ lemma is_integral_domain_fin (R : Type u) [comm_ring R] (hR : is_integral_domain
 
 lemma is_integral_domain_fintype (R : Type u) (σ : Type v) [comm_ring R] [fintype σ]
   (hR : is_integral_domain R) : is_integral_domain (mv_polynomial σ R) :=
-trunc.induction_on (fintype.equiv_fin σ) $ λ e,
 @ring_equiv.is_integral_domain _ (mv_polynomial (fin $ fintype.card σ) R) _ _
   (mv_polynomial.is_integral_domain_fin _ hR _)
-  (rename_equiv R e).to_ring_equiv
+  (rename_equiv R (fintype.equiv_fin σ)).to_ring_equiv
 
 /-- Auxilliary definition:
 Multivariate polynomials in finitely many variables over an integral domain form an integral domain.