chore(linear_algebra): continue removing decidable_eq assumptions (#1404

)

* chore(linear_algebra): continue remocing decidable_eq assumptions

* chore(data/mv_polynomial): get rid of unnecessary changes to instance depth

* fix build

* change class instance depth

* class_instance depth
t Please enter the commit message for your changes. Lines starting

* delete some more decidable_eq

* Update finite_dimensional.lean

* Update finite_dimensional.lean

* Update finite_dimensional.lean

src/field_theory/finite_card.lean

@@ -14,7 +14,7 @@ namespace finite_field
 theorem card (p : ℕ) [char_p α p] : ∃ (n : ℕ+), nat.prime p ∧ fintype.card α = p^(n : ℕ) :=
 have hp : nat.prime p, from char_p.char_is_prime α p,
 have V : vector_space (zmodp p hp) α, from {..zmod.to_module'},
-let ⟨n, h⟩ := @vector_space.card_fintype _ _ _ _ _ _ V _ _ in
+let ⟨n, h⟩ := @vector_space.card_fintype _ _ _ _ V _ _ in
 have hn : n > 0, from or.resolve_left (nat.eq_zero_or_pos n)
   (assume h0 : n = 0,
   have fintype.card α = 1, by rw[←nat.pow_zero (fintype.card _), ←h0]; exact h,

src/linear_algebra/basic.lean

@@ -1549,7 +1549,7 @@ begin
   { exact hI i hiI }
 end
 
-lemma std_basis_eq_single [decidable_eq α] {a : α} :
+lemma std_basis_eq_single {a : α} :
   (λ (i : ι), (std_basis α (λ _ : ι, α) i) a) = λ (i : ι), (finsupp.single i a) :=
 begin
   ext i j,

src/linear_algebra/basis.lean

@@ -27,10 +27,9 @@ import linear_algebra.basic linear_algebra.finsupp order.zorn
 noncomputable theory
 
 open function lattice set submodule
+open_locale classical
 
 variables {ι : Type*} {ι' : Type*} {α : Type*} {β : Type*} {γ : Type*} {δ : Type*} {v : ι → β}
-variables [decidable_eq ι] [decidable_eq ι']
-          [decidable_eq α] [decidable_eq β] [decidable_eq γ] [decidable_eq δ]
 
 section module
 variables [ring α] [add_comm_group β] [add_comm_group γ] [add_comm_group δ]
@@ -104,7 +103,7 @@ end
 
 lemma linear_independent_span (hs : linear_independent α v) :
   @linear_independent ι α (span α (range v))
-      (λ i : ι, ⟨v i, subset_span (mem_range_self i)⟩) _ _ _ _ _ _ :=
+      (λ i : ι, ⟨v i, subset_span (mem_range_self i)⟩) _ _ _ :=
 begin
   rw linear_independent_iff at *,
   intros l hl,
@@ -328,7 +327,6 @@ lemma linear_independent_Union_finite_subtype {ι : Type*} {f : ι → set β}
   (hd : ∀i, ∀t:set ι, finite t → i ∉ t → disjoint (span α (f i)) (⨆i∈t, span α (f i))) :
   linear_independent α (λ x, x : (⋃i, f i) → β) :=
 begin
-  classical,
   rw [Union_eq_Union_finset f],
   apply linear_independent_Union_of_directed,
   apply directed_of_sup,
@@ -354,7 +352,6 @@ begin
 end
 
 lemma linear_independent_Union_finite {η : Type*} {ιs : η → Type*}
-  [decidable_eq η] [∀ j, decidable_eq (ιs j)]
   {f : Π j : η, ιs j → β}
   (hindep : ∀j, linear_independent α (f j))
   (hd : ∀i, ∀t:set η, finite t → i ∉ t →
@@ -677,7 +674,7 @@ lemma constr_sub {g f : ι → γ} (hs : is_basis α v) :
 by simp [constr_add, constr_neg]
 
 -- this only works on functions if `α` is a commutative ring
-lemma constr_smul {ι α β γ} [decidable_eq ι] [decidable_eq α] [decidable_eq β] [decidable_eq γ] [comm_ring α]
+lemma constr_smul {ι α β γ} [comm_ring α]
   [add_comm_group β] [add_comm_group γ] [module α β] [module α γ]
   {v : ι → α} {f : ι → γ} {a : α} (hv : is_basis α v) {b : β} :
   hv.constr (λb, a • f b) = a • hv.constr f :=
@@ -719,7 +716,7 @@ end
 
 end is_basis
 
-lemma is_basis_singleton_one (α : Type*) [unique ι] [decidable_eq α] [ring α] :
+lemma is_basis_singleton_one (α : Type*) [unique ι] [ring α] :
   is_basis α (λ (_ : ι), (1 : α)) :=
 begin
   split,
@@ -735,7 +732,7 @@ lemma linear_equiv.is_basis (hs : is_basis α v)
   (f : β ≃ₗ[α] γ) : is_basis α (f ∘ v) :=
 begin
   split,
-  { apply @linear_independent.image _ _ _ _ _ _ _ _ _ _ _ _ _ _ hs.1 (f : β →ₗ[α] γ),
+  { apply @linear_independent.image _ _ _ _ _ _ _ _ _ _ hs.1 (f : β →ₗ[α] γ),
     simp [linear_equiv.ker f] },
   { rw set.range_comp,
     have : span α ((f : β →ₗ[α] γ) '' range v) = ⊤,
@@ -745,7 +742,7 @@ begin
 end
 
 lemma is_basis_span (hs : linear_independent α v) :
-  @is_basis ι α (span α (range v)) (λ i : ι, ⟨v i, subset_span (mem_range_self _)⟩) _ _ _ _ _ _ :=
+  @is_basis ι α (span α (range v)) (λ i : ι, ⟨v i, subset_span (mem_range_self _)⟩) _ _ _ :=
 begin
 split,
 { apply linear_independent_span hs },
@@ -844,7 +841,7 @@ end
 
 lemma linear_independent_singleton {x : β} (hx : x ≠ 0) : linear_independent α (λ x, x : ({x} : set β) → β) :=
 begin
-  apply @linear_independent_unique _ _ _ _ _ _ _ _ _ _ _ _,
+  apply @linear_independent_unique _ _ _ _ _ _ _ _ _,
   apply set.unique_singleton,
   apply hx,
 end
@@ -865,8 +862,7 @@ begin
   rw ← union_singleton,
   have x0 : x ≠ 0 := mt (by rintro rfl; apply zero_mem _) hx,
   apply linear_independent_union hs (linear_independent_singleton x0),
-  rwa [disjoint_span_singleton x0],
-  exact classical.dec_eq α
+  rwa [disjoint_span_singleton x0]
 end
 
 lemma exists_linear_independent (hs : linear_independent α (λ x, x : s → β)) (hst : s ⊆ t) :
@@ -890,7 +886,7 @@ lemma exists_subset_is_basis (hs : linear_independent α (λ x, x : s → β)) :
   ∃b, s ⊆ b ∧ is_basis α (λ i : b, i.val) :=
 let ⟨b, hb₀, hx, hb₂, hb₃⟩ := exists_linear_independent hs (@subset_univ _ _) in
 ⟨ b, hx,
-  @linear_independent.restrict_of_comp_subtype _ _ _ id _ _ _ _ _ _ _ hb₃,
+  @linear_independent.restrict_of_comp_subtype _ _ _ id _ _ _ _ hb₃,
   by simp; exact eq_top_iff.2 hb₂⟩
 
 variables (α β)
@@ -976,7 +972,7 @@ begin
   rcases exists_subset_is_basis this with ⟨C, BC, hC⟩,
   haveI : inhabited β := ⟨0⟩,
   use hC.constr (function.restrict (inv_fun f) C : C → β),
-  apply @is_basis.ext _ _ _ _ _ _ _ _ (show decidable_eq β, by assumption) _ _ _ _ _ _ _ hB,
+  apply @is_basis.ext _ _ _ _ _ _ _ _ _ _ _ _ hB,
   intros b,
   rw image_subset_iff at BC,
   simp,
@@ -995,7 +991,7 @@ begin
   rcases exists_is_basis α γ with ⟨C, hC⟩,
   haveI : inhabited β := ⟨0⟩,
   use hC.constr (function.restrict (inv_fun f) C : C → β),
-  apply @is_basis.ext _ _ _ _ _ _ _ _ (show decidable_eq γ, by assumption) _ _ _ _ _ _ _ hC,
+  apply @is_basis.ext _ _ _ _ _ _ _ _ _ _ _ _ hC,
   intros c,
   simp [constr_basis hC],
   exact right_inverse_inv_fun (linear_map.range_eq_top.1 hf_surj) _
@@ -1040,9 +1036,9 @@ open set linear_map
 
 section module
 variables {η : Type*} {ιs : η → Type*} {φ : η → Type*}
-variables [ring α] [∀i, add_comm_group (φ i)] [∀i, module α (φ i)] [fintype η] [decidable_eq η]
+variables [ring α] [∀i, add_comm_group (φ i)] [∀i, module α (φ i)] [fintype η]
 
-lemma linear_independent_std_basis [∀ j, decidable_eq (ιs j)]  [∀ i, decidable_eq (φ i)]
+lemma linear_independent_std_basis
   (v : Πj, ιs j → (φ j)) (hs : ∀i, linear_independent α (v i)) :
   linear_independent α (λ (ji : Σ j, ιs j), std_basis α φ ji.1 (v ji.1 ji.2)) :=
 begin
@@ -1073,8 +1069,7 @@ begin
       (disjoint_std_basis_std_basis _ _ _ _ h₃), }
 end
 
-lemma is_basis_std_basis [∀ j, decidable_eq (ιs j)] [∀ j, decidable_eq (φ j)]
-  (s : Πj, ιs j → (φ j)) (hs : ∀j, is_basis α (s j)) :
+lemma is_basis_std_basis (s : Πj, ιs j → (φ j)) (hs : ∀j, is_basis α (s j)) :
   is_basis α (λ (ji : Σ j, ιs j), std_basis α φ ji.1 (s ji.1 ji.2)) :=
 begin
   split,
@@ -1102,18 +1097,19 @@ lemma is_basis_fun₀ : is_basis α
        (std_basis α (λ (i : η), α) (ji.fst)) 1) :=
 begin
   haveI := classical.dec_eq,
-  apply @is_basis_std_basis α _ η (λi:η, unit) (λi:η, α) _ _ _ _ _ _ _ (λ _ _, (1 : α))
-      (assume i, @is_basis_singleton_one _ _ _ _ _ _),
+  apply @is_basis_std_basis α η (λi:η, unit) (λi:η, α) _ _ _ _ (λ _ _, (1 : α))
+      (assume i, @is_basis_singleton_one _ _ _ _),
 end
 
 lemma is_basis_fun : is_basis α (λ i, std_basis α (λi:η, α) i 1) :=
 begin
-  apply is_basis.comp (is_basis_fun₀ α) (λ i, ⟨i, punit.star⟩),
+  apply is_basis.comp (is_basis_fun₀ α) (λ i, ⟨i, punit.star⟩) ,
   { apply bijective_iff_has_inverse.2,
     use (λ x, x.1),
     simp [function.left_inverse, function.right_inverse],
     intros _ b,
     rw [unique.eq_default b, unique.eq_default punit.star] },
+  apply_instance
 end
 
 end

src/linear_algebra/dimension.lean

@@ -15,23 +15,25 @@ variables {α : Type u} {β γ δ ε : Type v}
 variables {ι : Type w} {ι' : Type w'} {η : Type u''} {φ : η → Type u'}
 -- TODO: relax these universe constraints
 
+open_locale classical
+
 section vector_space
-variables [decidable_eq ι] [decidable_eq ι'] [discrete_field α] [add_comm_group β] [vector_space α β]
+variables [discrete_field α] [add_comm_group β] [vector_space α β]
 include α
 open submodule lattice function set
 
 variables (α β)
 def vector_space.dim : cardinal :=
 cardinal.min
-  (nonempty_subtype.2 (@exists_is_basis α β _ (classical.dec_eq _) _ _ _))
+  (nonempty_subtype.2 (@exists_is_basis α β _ _ _))
   (λ b, cardinal.mk b.1)
 variables {α β}
 
 open vector_space
 
 section
 set_option class.instance_max_depth 50
-theorem is_basis.le_span (zero_ne_one : (0 : α) ≠ 1) [decidable_eq β] {v : ι → β} {J : set β} (hv : is_basis α v)
+theorem is_basis.le_span (zero_ne_one : (0 : α) ≠ 1) {v : ι → β} {J : set β} (hv : is_basis α v)
    (hJ : span α J = ⊤) : cardinal.mk (range v) ≤ cardinal.mk J :=
 begin
   cases le_or_lt cardinal.omega (cardinal.mk J) with oJ oJ,
@@ -69,7 +71,7 @@ end
 end
 
 /-- dimension theorem -/
-theorem mk_eq_mk_of_basis [decidable_eq β] {v : ι → β} {v' : ι' → β}
+theorem mk_eq_mk_of_basis {v : ι → β} {v' : ι' → β}
   (hv : is_basis α v) (hv' : is_basis α v') :
   cardinal.lift.{w w'} (cardinal.mk ι) = cardinal.lift.{w' w} (cardinal.mk ι') :=
 begin
@@ -88,19 +90,18 @@ begin
       apply (cardinal.mk_range_eq_of_inj (hv.injective zero_ne_one)).symm, }, }
 end
 
-theorem is_basis.mk_range_eq_dim [decidable_eq β] {v : ι → β} (h : is_basis α v) :
+theorem is_basis.mk_range_eq_dim {v : ι → β} (h : is_basis α v) :
   cardinal.mk (range v) = dim α β :=
 begin
   have := show ∃ v', dim α β = _, from cardinal.min_eq _ _,
   rcases this with ⟨v', e⟩,
   rw e,
   apply cardinal.lift_inj.1,
   rw cardinal.mk_range_eq_of_inj (h.injective zero_ne_one),
-  convert @mk_eq_mk_of_basis _ _ _ _ _ (id _) _ _ _ (id _) _ _ h v'.property,
-  apply_instance,
+  convert @mk_eq_mk_of_basis _ _ _ _ _ _ _ _ _ h v'.property
 end
 
-theorem is_basis.mk_eq_dim [decidable_eq β] {v : ι → β} (h : is_basis α v) :
+theorem is_basis.mk_eq_dim {v : ι → β} (h : is_basis α v) :
   cardinal.lift.{w v} (cardinal.mk ι) = cardinal.lift.{v w} (dim α β) :=
 by rw [←h.mk_range_eq_dim, cardinal.mk_range_eq_of_inj (h.injective zero_ne_one)]
 
@@ -115,21 +116,21 @@ cardinal.lift_inj.1 $ hb.mk_eq_dim.symm.trans (f.is_basis hb).mk_eq_dim
 
 @[simp] lemma dim_bot : dim α (⊥ : submodule α β) = 0 :=
 by letI := classical.dec_eq β;
-  rw [← cardinal.lift_inj, ← (@is_basis_empty_bot pempty α β _ _ _ _ _ _ not_nonempty_pempty).mk_eq_dim,
+  rw [← cardinal.lift_inj, ← (@is_basis_empty_bot pempty α β _ _ _ not_nonempty_pempty).mk_eq_dim,
     cardinal.mk_pempty]
 
 @[simp] lemma dim_top : dim α (⊤ : submodule α β) = dim α β :=
 linear_equiv.dim_eq (linear_equiv.of_top _ rfl)
 
 lemma dim_of_field (α : Type*) [discrete_field α] : dim α α = 1 :=
-by rw [←cardinal.lift_inj, ← (@is_basis_singleton_one punit _ α _ _ _).mk_eq_dim, cardinal.mk_punit]
+by rw [←cardinal.lift_inj, ← (@is_basis_singleton_one punit α _ _).mk_eq_dim, cardinal.mk_punit]
 
-lemma dim_span [decidable_eq β] {v : ι → β} (hv : linear_independent α v) :
+lemma dim_span {v : ι → β} (hv : linear_independent α v) :
   dim α ↥(span α (range v)) = cardinal.mk (range v) :=
 by rw [←cardinal.lift_inj, ← (is_basis_span hv).mk_eq_dim,
-    cardinal.mk_range_eq_of_inj (@linear_independent.injective ι α β v _ _ _ _ _ _ zero_ne_one hv)]
+    cardinal.mk_range_eq_of_inj (@linear_independent.injective ι α β v _ _ _ zero_ne_one hv)]
 
-lemma dim_span_set [decidable_eq β] {s : set β} (hs : linear_independent α (λ x, x : s → β)) :
+lemma dim_span_set {s : set β} (hs : linear_independent α (λ x, x : s → β)) :
   dim α ↥(span α s) = cardinal.mk s :=
 by rw [← @set_of_mem_eq _ s, ← subtype.val_range]; exact dim_span hs
 
@@ -158,7 +159,7 @@ begin
   rcases exists_is_basis α β with ⟨b, hb⟩,
   rcases exists_is_basis α γ with ⟨c, hc⟩,
   rw [← cardinal.lift_inj,
-      ← @is_basis.mk_eq_dim α (β × γ) _ _ _ _ _ _ _ (is_basis_inl_union_inr hb hc),
+      ← @is_basis.mk_eq_dim α (β × γ) _ _ _ _ _ (is_basis_inl_union_inr hb hc),
       cardinal.lift_add, cardinal.lift_mk,
       ← hb.mk_eq_dim, ← hc.mk_eq_dim,
       cardinal.lift_mk, cardinal.lift_mk,
@@ -167,7 +168,7 @@ begin
       ⟨equiv.ulift.trans (equiv.sum_congr (@equiv.ulift b) (@equiv.ulift c)).symm ⟩),
 end
 
-theorem dim_quotient (p : submodule α β) [decidable_eq p.quotient]:
+theorem dim_quotient (p : submodule α β) :
   dim α p.quotient + dim α p = dim α β :=
 by classical; exact let ⟨f⟩ := quotient_prod_linear_equiv p in dim_prod.symm.trans f.dim_eq
 
@@ -305,9 +306,7 @@ open linear_map
 
 lemma dim_pi : vector_space.dim α (Πi, φ i) = cardinal.sum (λi, vector_space.dim α (φ i)) :=
 begin
-  letI := λ i, classical.dec_eq (φ i),
   choose b hb using assume i, exists_is_basis α (φ i),
-  haveI := classical.dec_eq η,
   have : is_basis α (λ (ji : Σ j, b j), std_basis α (λ j, φ j) ji.fst ji.snd.val),
     by apply pi.is_basis_std_basis _ hb,
   rw [←cardinal.lift_inj, ← this.mk_eq_dim],
@@ -343,7 +342,7 @@ lemma exists_mem_ne_zero_of_dim_pos {s : submodule α β} (h : vector_space.dim
   ∃ b : β, b ∈ s ∧ b ≠ 0 :=
 exists_mem_ne_zero_of_ne_bot $ assume eq, by rw [(>), eq, dim_bot] at h; exact lt_irrefl _ h
 
-lemma exists_is_basis_fintype [decidable_eq β] (h : dim α β < cardinal.omega) :
+lemma exists_is_basis_fintype (h : dim α β < cardinal.omega) :
   ∃ s : (set β), (is_basis α (subtype.val : s → β)) ∧ nonempty (fintype s) :=
 begin
   cases exists_is_basis α β with s hs,
@@ -404,7 +403,7 @@ variables [discrete_field α] [add_comm_group β] [vector_space α β]
 open vector_space
 
 /-- Version of linear_equiv.dim_eq without universe constraints. -/
-theorem linear_equiv.dim_eq_lift [decidable_eq β] [decidable_eq γ'] (f : β ≃ₗ[α] γ') :
+theorem linear_equiv.dim_eq_lift (f : β ≃ₗ[α] γ') :
   cardinal.lift.{v v'} (dim α β) = cardinal.lift.{v' v} (dim α γ') :=
 begin
   cases exists_is_basis α β with b hb,

src/linear_algebra/dual.lean

@@ -45,7 +45,7 @@ open vector_space module module.dual submodule linear_map cardinal function
 
 instance dual.vector_space : vector_space K (dual K V) := {..dual.module K V}
 
-variables [decidable_eq V] [decidable_eq (module.dual K V)] [decidable_eq ι]
+variables [decidable_eq ι]
 variables {B : ι → V} (h : is_basis K B)
 
 include h
@@ -85,8 +85,7 @@ begin
     rw [to_dual_swap_eq_to_dual, to_dual_apply],
     { split_ifs with hx,
       { rwa [hx, coord_fun_eq_repr, repr_eq_single, finsupp.single_apply, if_pos rfl] },
-      { rw [coord_fun_eq_repr, repr_eq_single, finsupp.single_apply], symmetry, convert if_neg hx } } },
-  { exact classical.dec_eq K }
+      { rw [coord_fun_eq_repr, repr_eq_single, finsupp.single_apply], symmetry, convert if_neg hx } } }
 end
 
 lemma to_dual_inj (v : V) (a : h.to_dual v = 0) : v = 0 :=
@@ -114,8 +113,7 @@ begin
       rw [h.to_dual_eq_repr _ i, repr_total h],
       { simpa },
       { rw [finsupp.mem_supported],
-        exact λ _ _, set.mem_univ _ } },
-    { exact classical.dec_eq K } },
+        exact λ _ _, set.mem_univ _ } } },
   { intros a _,
     apply fin.complete }
 end
@@ -138,9 +136,9 @@ h.to_dual_equiv.is_basis h
 @[simp] lemma to_dual_to_dual [decidable_eq (dual K (dual K V))] [fintype ι] :
   (h.dual_basis_is_basis.to_dual).comp h.to_dual = eval K V :=
 begin
-  apply @is_basis.ext _ _ _ _ _ _ _ _ (classical.dec_eq (dual K (dual K V))) _ _ _ _ _ _ _ h,
+  apply @is_basis.ext _ _ _ _ _ _ _ _ _ _ _ _ h,
   intros i,
-  apply @is_basis.ext _ _ _ _ _ _ _ _ (classical.dec_eq _) _ _ _ _ _ _ _ h.dual_basis_is_basis,
+  apply @is_basis.ext _ _ _ _ _ _ _ _ _ _ _ _ h.dual_basis_is_basis,
   intros j,
   dunfold eval,
   rw [linear_map.flip_apply, linear_map.id_apply, linear_map.comp_apply],