[Merged by Bors] - chore(*): remove instance arguments that are inferrable from earlier

src/analysis/convex/basic.lean

@@ -279,6 +279,22 @@ begin
   rw midpoint_add_sub
 end
 
+@[simp] lemma left_mem_open_segment_iff [densely_ordered 𝕜] [no_zero_smul_divisors 𝕜 E] {x y : E} :
+  x ∈ open_segment 𝕜 x y ↔ x = y :=
+begin
+  split,
+  { rintro ⟨a, b, ha, hb, hab, hx⟩,
+    refine smul_right_injective _ hb.ne' ((add_right_inj (a • x)).1 _),
+    rw [hx, ←add_smul, hab, one_smul] },
+  { rintro rfl,
+    rw open_segment_same,
+    exact mem_singleton _ }
+end
+
+@[simp] lemma right_mem_open_segment_iff [densely_ordered 𝕜] [no_zero_smul_divisors 𝕜 E] {x y : E} :
+  y ∈ open_segment 𝕜 x y ↔ x = y :=
+by rw [open_segment_symm, left_mem_open_segment_iff, eq_comm]
+
 end add_comm_group
 end linear_ordered_ring
 
@@ -324,22 +340,6 @@ begin
     rw [← add_div, div_self hab.ne'] }
 end
 
-@[simp] lemma left_mem_open_segment_iff [no_zero_smul_divisors 𝕜 E] {x y : E} :
-  x ∈ open_segment 𝕜 x y ↔ x = y :=
-begin
-  split,
-  { rintro ⟨a, b, ha, hb, hab, hx⟩,
-    refine smul_right_injective _ hb.ne' ((add_right_inj (a • x)).1 _),
-    rw [hx, ←add_smul, hab, one_smul] },
-  { rintro rfl,
-    rw open_segment_same,
-    exact mem_singleton _ }
-end
-
-@[simp] lemma right_mem_open_segment_iff {x y : E} :
-  y ∈ open_segment 𝕜 x y ↔ x = y :=
-by rw [open_segment_symm, left_mem_open_segment_iff, eq_comm]
-
 end add_comm_group
 end linear_ordered_field
 

src/analysis/convex/extreme.lean

@@ -185,12 +185,13 @@ convex_iff_open_segment_subset.2 (λ x₁ x₂ ⟨hx₁A, hx₁B⟩ ⟨hx₂A, h
 
 end ordered_semiring
 
-section linear_ordered_field
-variables {𝕜} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] {A B : set E} {x : E}
+section linear_ordered_ring
+variables {𝕜} [linear_ordered_ring 𝕜] [add_comm_group E] [module 𝕜 E]
+variables [densely_ordered 𝕜] [no_zero_smul_divisors 𝕜 E] {A B : set E} {x : E}
 
 /-- A useful restatement using `segment`: `x` is an extreme point iff the only (closed) segments
 that contain it are those with `x` as one of their endpoints. -/
-lemma mem_extreme_points_iff_forall_segment [no_zero_smul_divisors 𝕜 E] :
+lemma mem_extreme_points_iff_forall_segment :
   x ∈ A.extreme_points 𝕜 ↔ x ∈ A ∧ ∀ (x₁ x₂ ∈ A), x ∈ segment 𝕜 x₁ x₂ → x₁ = x ∨ x₂ = x :=
 begin
   split,
@@ -232,6 +233,7 @@ begin
   by_contra,
   exact (convex_hull_min (subset_diff.2 ⟨subset_convex_hull 𝕜 _, disjoint_singleton_right.2 h⟩) hx.2
     hx.1).2 rfl,
+  apply_instance
 end
 
-end linear_ordered_field
+end linear_ordered_ring

src/analysis/inner_product_space/projection.lean

@@ -1175,7 +1175,7 @@ lemma std_orthonormal_basis_orthonormal :
 (exists_subset_is_orthonormal_basis (orthonormal_empty 𝕜 E)).some_spec.some_spec.some_spec.2
 
 instance : fintype (orthonormal_basis_index 𝕜 E) :=
-@is_noetherian.fintype_basis_index _ _ _ _ _ _ _
+@is_noetherian.fintype_basis_index _ _ _ _ _ _
   (is_noetherian.iff_fg.2 infer_instance) (std_orthonormal_basis 𝕜 E)
 
 variables {𝕜 E}

src/category_theory/simple.lean

@@ -117,7 +117,7 @@ begin
 end
 
 lemma cokernel_zero_of_nonzero_to_simple
-  {X Y : C} [simple Y] {f : X ⟶ Y} [has_cokernel f] (w : f ≠ 0) :
+  {X Y : C} [simple Y] {f : X ⟶ Y} (w : f ≠ 0) :
   cokernel.π f = 0 :=
 begin
   classical,

src/field_theory/finiteness.lean

@@ -20,10 +20,6 @@ namespace is_noetherian
 
 variables {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module K V]
 
--- PROJECT: Show all division rings are noetherian.
--- This is currently annoying because we only have ideal of commutative rings.
-variables [is_noetherian_ring K]
-
 /--
 A module over a division ring is noetherian if and only if
 its dimension (as a cardinal) is strictly less than the first infinite cardinal `ω`.

src/linear_algebra/finite_dimensional.lean

@@ -98,7 +98,7 @@ iff_fg.1 is_noetherian_pi
 
 /-- A finite dimensional vector space over a finite field is finite -/
 noncomputable def fintype_of_fintype [fintype K] [finite_dimensional K V] : fintype V :=
-module.fintype_of_fintype (@finset_basis K V _ _ _ _ (iff_fg.2 infer_instance))
+module.fintype_of_fintype (@finset_basis K V _ _ _ (iff_fg.2 infer_instance))
 
 variables {K V}
 
@@ -229,9 +229,9 @@ variables (K V)
 
 /-- A finite dimensional vector space has a basis indexed by `fin (finrank K V)`. -/
 noncomputable def fin_basis [finite_dimensional K V] : basis (fin (finrank K V)) K V :=
-have h : fintype.card (@finset_basis_index K V _ _ _ _ (iff_fg.2 infer_instance)) = finrank K V,
-from (finrank_eq_card_basis (@finset_basis K V _ _ _ _ (iff_fg.2 infer_instance))).symm,
-(@finset_basis K V _ _ _ _ (iff_fg.2 infer_instance)).reindex (fintype.equiv_fin_of_card_eq h)
+have h : fintype.card (@finset_basis_index K V _ _ _ (iff_fg.2 infer_instance)) = finrank K V,
+from (finrank_eq_card_basis (@finset_basis K V _ _ _ (iff_fg.2 infer_instance))).symm,
+(@finset_basis K V _ _ _ (iff_fg.2 infer_instance)).reindex (fintype.equiv_fin_of_card_eq h)
 
 /-- An `n`-dimensional vector space has a basis indexed by `fin n`. -/
 noncomputable def fin_basis_of_finrank_eq [finite_dimensional K V] {n : ℕ} (hn : finrank K V = n) :