chore(*): drop some unused args reported by #sanity_check_mathlib (#…

…1490)

* Drop some unused arguments

* Drop more unused arguments

* Move `round` to the bottom of `algebra/archimedean`

Suggested by @rwbarton

src/algebra/archimedean.lean

@@ -174,7 +174,7 @@ begin
   { rw [rat.coe_nat_denom, nat.cast_one], exact one_ne_zero }
 end
 
-theorem exists_nat_one_div_lt {ε : α} (hε : ε > 0) : ∃ n : ℕ, 1 / (n + 1: α) < ε :=
+theorem exists_nat_one_div_lt {ε : α} (hε : 0 < ε) : ∃ n : ℕ, 1 / (n + 1: α) < ε :=
 begin
   cases archimedean_iff_nat_lt.1 (by apply_instance) (1/ε) with n hn,
   existsi n,
@@ -201,19 +201,13 @@ begin
     apply floor_le }
 end
 
-/-- `round` rounds a number to the nearest integer. `round (1 / 2) = 1` -/
-def round [floor_ring α] (x : α) : ℤ := ⌊x + 1 / 2⌋
-
 end linear_ordered_field
 
 section
-variables [discrete_linear_ordered_field α] [archimedean α]
+variables [discrete_linear_ordered_field α]
 
-theorem exists_rat_near (x : α) {ε : α} (ε0 : ε > 0) :
-  ∃ q : ℚ, abs (x - q) < ε :=
-let ⟨q, h₁, h₂⟩ := exists_rat_btwn $
-  lt_trans ((sub_lt_self_iff x).2 ε0) ((lt_add_iff_pos_left x).2 ε0) in
-⟨q, abs_sub_lt_iff.2 ⟨sub_lt.1 h₁, sub_lt_iff_lt_add.2 h₂⟩⟩
+/-- `round` rounds a number to the nearest integer. `round (1 / 2) = 1` -/
+def round [floor_ring α] (x : α) : ℤ := ⌊x + 1 / 2⌋
 
 lemma abs_sub_round [floor_ring α] (x : α) : abs (x - round x) ≤ 1 / 2 :=
 begin
@@ -223,11 +217,18 @@ begin
   split; linarith
 end
 
+variable [archimedean α]
+
+theorem exists_rat_near (x : α) {ε : α} (ε0 : 0 < ε) :
+  ∃ q : ℚ, abs (x - q) < ε :=
+let ⟨q, h₁, h₂⟩ := exists_rat_btwn $
+  lt_trans ((sub_lt_self_iff x).2 ε0) ((lt_add_iff_pos_left x).2 ε0) in
+⟨q, abs_sub_lt_iff.2 ⟨sub_lt.1 h₁, sub_lt_iff_lt_add.2 h₂⟩⟩
+
 instance : archimedean ℚ :=
 archimedean_iff_rat_le.2 $ λ q, ⟨q, by rw rat.cast_id⟩
 
-@[simp] theorem rat.cast_round {α : Type*} [discrete_linear_ordered_field α]
-  [archimedean α] (x : ℚ) : by haveI := archimedean.floor_ring α;
+@[simp] theorem rat.cast_round (x : ℚ) : by haveI := archimedean.floor_ring α;
   exact round (x:α) = round x :=
 have ((x + (1 : ℚ) / (2 : ℚ) : ℚ) : α) = x + 1 / 2, by simp,
 by rw [round, round, ← this, rat.cast_floor]

src/algebra/associated.lean

@@ -407,14 +407,14 @@ instance : preorder (associates α) :=
   le_refl := assume a, ⟨1, by simp⟩,
   le_trans := assume a b c ⟨f₁, h₁⟩ ⟨f₂, h₂⟩, ⟨f₁ * f₂, h₂ ▸ h₁ ▸ (mul_assoc _ _ _).symm⟩}
 
-instance [comm_monoid α] : has_dvd (associates α) := ⟨(≤)⟩
+instance : has_dvd (associates α) := ⟨(≤)⟩
 
 @[simp] lemma mk_one : associates.mk (1 : α) = 1 := rfl
 
 lemma mk_pow (a : α) (n : ℕ) : associates.mk (a ^ n) = (associates.mk a) ^ n :=
 by induction n; simp [*, pow_succ, associates.mk_mul_mk.symm]
 
-lemma dvd_eq_le [comm_monoid α] : ((∣) : associates α → associates α → Prop) = (≤) := rfl
+lemma dvd_eq_le : ((∣) : associates α → associates α → Prop) = (≤) := rfl
 
 theorem prod_mk {p : multiset α} : (p.map associates.mk).prod = associates.mk p.prod :=
 multiset.induction_on p (by simp; refl) $ assume a s ih, by simp [ih]; refl
@@ -611,7 +611,7 @@ begin
     simpa [is_unit_mk] using h _ _ this }
 end
 
-lemma eq_of_mul_eq_mul_left [integral_domain α] :
+lemma eq_of_mul_eq_mul_left :
   ∀(a b c : associates α), a ≠ 0 → a * b = a * c → b = c :=
 begin
   rintros ⟨a⟩ ⟨b⟩ ⟨c⟩ ha h,
@@ -620,11 +620,11 @@ begin
   exact quotient.sound' ⟨u, eq_of_mul_eq_mul_left (mt (mk_zero_eq a).2 ha) hu⟩
 end
 
-lemma le_of_mul_le_mul_left [integral_domain α] (a b c : associates α) (ha : a ≠ 0) :
+lemma le_of_mul_le_mul_left (a b c : associates α) (ha : a ≠ 0) :
   a * b ≤ a * c → b ≤ c
 | ⟨d, hd⟩ := ⟨d, eq_of_mul_eq_mul_left a _ _ ha $ by rwa ← mul_assoc⟩
 
-lemma one_or_eq_of_le_of_prime [integral_domain α] :
+lemma one_or_eq_of_le_of_prime :
   ∀(p m : associates α), prime p → m ≤ p → (m = 1 ∨ m = p)
 | _ m ⟨hp0, hp1, h⟩ ⟨d, rfl⟩ :=
 match h m d (le_refl _) with

src/algebra/floor.lean

@@ -104,7 +104,7 @@ lemma floor_eq_iff {r : α} {z : ℤ} :
 by rw [←le_floor, ←int.cast_one, ←int.cast_add, ←floor_lt,
 int.lt_add_one_iff, le_antisymm_iff, and.comm]
 
-lemma floor_ring_unique [linear_ordered_ring α] (inst1 inst2 : floor_ring α) :
+lemma floor_ring_unique {α} [linear_ordered_ring α] (inst1 inst2 : floor_ring α) :
   @floor _ _ inst1 = @floor _ _ inst2 :=
 begin
   ext v,

src/algebra/group/units.lean

@@ -111,7 +111,7 @@ section monoid
   theorem divp_assoc (a b : α) (u : units α) : a * b /ₚ u = a * (b /ₚ u) :=
   mul_assoc _ _ _
 
-  @[simp] theorem divp_inv (x : α) (u : units α) : a /ₚ u⁻¹ = a * u := rfl
+  @[simp] theorem divp_inv (u : units α) : a /ₚ u⁻¹ = a * u := rfl
 
   @[simp] theorem divp_mul_cancel (a : α) (u : units α) : a /ₚ u * u = a :=
   (mul_assoc _ _ _).trans $ by rw [units.inv_mul, mul_one]

src/algebra/group/with_one.lean

@@ -74,14 +74,21 @@ section lift
 @[to_additive]
 def lift {β : Type v} [has_one β] (f : α → β) : (with_one α) → β := λ x, option.cases_on x 1 f
 
-variables [semigroup α] {β : Type v} [monoid β] (f : α → β)
+variables [ha : semigroup α] {β : Type v} [monoid β] (f : α → β)
 
 @[simp, to_additive]
 lemma lift_coe (x : α) : lift f x = f x := rfl
 
 @[simp, to_additive]
 lemma lift_one : lift f 1 = 1 := rfl
 
+@[to_additive]
+theorem lift_unique (f : with_one α → β) (hf : f 1 = 1) :
+  f = lift (f ∘ coe) :=
+funext $ λ x, with_one.cases_on x hf $ λ x, rfl
+
+include ha
+
 @[to_additive lift_is_add_monoid_hom]
 instance lift_is_monoid_hom [hf : is_mul_hom f] : is_monoid_hom (lift f) :=
 { map_one := lift_one f,
@@ -90,28 +97,22 @@ instance lift_is_monoid_hom [hf : is_mul_hom f] : is_monoid_hom (lift f) :=
     with_one.cases_on y (by rw [mul_one, lift_one, mul_one]) $ λ y,
     @is_mul_hom.map_mul α β _ _ f hf x y }
 
-@[to_additive]
-theorem lift_unique (f : with_one α → β) (hf : f 1 = 1) :
-  f = lift (f ∘ coe) :=
-funext $ λ x, with_one.cases_on x hf $ λ x, rfl
-
 end lift
 
 section map
 
 @[to_additive]
 def map {β : Type v} (f : α → β) : with_one α → with_one β := option.map f
 
-variables [semigroup α] {β : Type v} [semigroup β] (f : α → β)
-
 @[to_additive]
-lemma map_eq [semigroup α] {β : Type v} [semigroup β] (f : α → β) :
-  map f = lift (coe ∘ f) :=
+lemma map_eq {β : Type v} (f : α → β) : map f = lift (coe ∘ f) :=
 funext $ assume x,
 @with_one.cases_on α (λ x, map f x = lift (coe ∘ f) x) x rfl (λ a, rfl)
 
+variables [semigroup α] {β : Type v} [semigroup β] (f : α → β) [is_mul_hom f]
+
 @[to_additive map_is_add_monoid_hom]
-instance map_is_monoid_hom [is_mul_hom f] : is_monoid_hom (map f) :=
+instance map_is_monoid_hom : is_monoid_hom (map f) :=
 by rw map_eq; apply with_one.lift_is_monoid_hom
 
 end map

src/category/basic.lean

@@ -54,8 +54,6 @@ attribute [functor_norm] seq_assoc pure_seq_eq_map
 @[simp] theorem pure_id'_seq (x : F α) : pure (λx, x) <*> x = x :=
 pure_id_seq x
 
-variables  [is_lawful_applicative F]
-
 attribute [functor_norm] seq_assoc pure_seq_eq_map
 
 @[functor_norm] theorem seq_map_assoc (x : F (α → β)) (f : γ → α) (y : F γ) :

src/category/bitraversable/instances.lean

@@ -76,9 +76,9 @@ def flip.bitraverse {α α' β β'} (f : α → F α') (f' : β → F β') : fli
 instance bitraversable.flip : bitraversable (flip t) :=
 { bitraverse := @flip.bitraverse t _ }
 
-variables [is_lawful_bitraversable t]
 open is_lawful_bitraversable
-instance is_lawful_bitraversable.flip  : is_lawful_bitraversable (flip t)  :=
+instance is_lawful_bitraversable.flip [is_lawful_bitraversable t]
+  : is_lawful_bitraversable (flip t)  :=
 by constructor; introsI; casesm is_lawful_bitraversable t; apply_assumption
 
 open bitraversable functor

src/category/monad/writer.lean

@@ -67,7 +67,7 @@ section
   instance (m m') [monad m] [monad m'] : monad_functor m m' (writer_t ω m) (writer_t ω m') :=
   ⟨@writer_t.monad_map ω m m' _ _⟩
 
-  @[inline] protected def adapt {ω' : Type u} [monad m] {α : Type u} (f : ω → ω') : writer_t ω m α → writer_t ω' m α :=
+  @[inline] protected def adapt {ω' : Type u} {α : Type u} (f : ω → ω') : writer_t ω m α → writer_t ω' m α :=
   λ x, ⟨prod.map id f <$> x.run⟩
 
   instance (ε) [has_one ω] [monad m] [monad_except ε m] : monad_except ε (writer_t ω m) :=

src/category_theory/limits/shapes/equalizers.lean

@@ -108,15 +108,15 @@ def cofork.of_π {P : C} (π : Y ⟶ P) (w : f ≫ π = g ≫ π) : cofork f g :
 
 def fork.ι (t : fork f g) := t.π.app zero
 def cofork.π (t : cofork f g) := t.ι.app one
-def fork.condition (t : fork f g) : (fork.ι t) ≫ f = (fork.ι t) ≫ g :=
+lemma fork.condition (t : fork f g) : (fork.ι t) ≫ f = (fork.ι t) ≫ g :=
 begin
   erw [t.w left, ← t.w right], refl
 end
-def cofork.condition (t : cofork f g) : f ≫ (cofork.π t) = g ≫ (cofork.π t) :=
+lemma cofork.condition (t : cofork f g) : f ≫ (cofork.π t) = g ≫ (cofork.π t) :=
 begin
   erw [t.w left, ← t.w right], refl
 end
-
+ 
 def cone.of_fork
   {F : walking_parallel_pair.{v} ⥤ C} (t : fork (F.map left) (F.map right)) : cone F :=
 { X := t.X,

src/category_theory/limits/shapes/pullbacks.lean

@@ -287,12 +287,12 @@ abbreviation pushout.desc {W X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} [has_colimit
   (h : Y ⟶ W) (k : Z ⟶ W) (w : f ≫ h = g ≫ k) : pushout f g ⟶ W :=
 colimit.desc _ (pushout_cocone.mk h k w)
 
-lemma pullback.condition {W X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [has_limit (cospan f g)] :
+lemma pullback.condition {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [has_limit (cospan f g)] :
   (pullback.fst : pullback f g ⟶ X) ≫ f = pullback.snd ≫ g :=
 (limit.w (cospan f g) walking_cospan.hom.inl).trans
 (limit.w (cospan f g) walking_cospan.hom.inr).symm
 
-lemma pushout.condition {W X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} [has_colimit (span f g)] :
+lemma pushout.condition {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} [has_colimit (span f g)] :
   f ≫ (pushout.inl : Y ⟶ pushout f g) = g ≫ pushout.inr :=
 (colimit.w (span f g) walking_span.hom.fst).trans
 (colimit.w (span f g) walking_span.hom.snd).symm

src/data/equiv/algebra.lean

@@ -64,13 +64,21 @@ protected def inv (α) [group α] : α ≃ α :=
   left_inv  := assume a, inv_inv a,
   right_inv := assume a, inv_inv a }
 
-def units_equiv_ne_zero (α : Type*) [field α] : units α ≃ {a : α | a ≠ 0} :=
+end group
+
+section field
+
+variables (α) [field α]
+
+def units_equiv_ne_zero : units α ≃ {a : α | a ≠ 0} :=
 ⟨λ a, ⟨a.1, units.ne_zero _⟩, λ a, units.mk0 _ a.2, λ ⟨_, _, _, _⟩, units.ext rfl, λ ⟨_, _⟩, rfl⟩
 
-@[simp] lemma coe_units_equiv_ne_zero [field α] (a : units α) :
+variable {α}
+
+@[simp] lemma coe_units_equiv_ne_zero (a : units α) :
   ((units_equiv_ne_zero α a) : α) = a := rfl
 
-end group
+end field
 
 section instances
 

src/data/equiv/basic.lean

@@ -885,7 +885,7 @@ by { cases π, refl }
 @[simp] lemma swap_inv {α : Type*} [decidable_eq α] (x y : α) :
   (swap x y)⁻¹ = swap x y := rfl
 
-@[simp] lemma symm_trans_swap_trans [decidable_eq α] [decidable_eq β] (a b : α)
+@[simp] lemma symm_trans_swap_trans [decidable_eq β] (a b : α)
   (e : α ≃ β) : (e.symm.trans (swap a b)).trans e = swap (e a) (e b) :=
 equiv.ext _ _ (λ x, begin
   have : ∀ a, e.symm x = a ↔ x = e a :=

src/measure_theory/ae_eq_fun.lean

@@ -87,7 +87,6 @@ lemma lift_rel_mk_mk {γ : Type*} [measurable_space γ] (r : β → γ → Prop)
 iff.rfl
 
 section order
-variables [measurable_space β]
 
 instance [preorder β] : preorder (α →ₘ β) :=
 { le          := lift_rel (≤),
@@ -156,16 +155,15 @@ end add_comm_monoid
 
 section add_group
 
-variables {γ : Type*}
-  [topological_space γ] [second_countable_topology γ] [add_group γ] [topological_add_group γ]
+variables {γ : Type*} [topological_space γ] [add_group γ] [topological_add_group γ]
 
 protected def neg : (α →ₘ γ) → (α →ₘ γ) := comp has_neg.neg (measurable_neg measurable_id)
 
 instance : has_neg (α →ₘ γ) := ⟨ae_eq_fun.neg⟩
 
 @[simp] lemma neg_mk (f : α → γ) (hf) : -(mk f hf) = mk (-f) (measurable_neg hf) := rfl
 
-instance : add_group (α →ₘ γ) :=
+instance [second_countable_topology γ] : add_group (α →ₘ γ) :=
 { neg          := ae_eq_fun.neg,
   add_left_neg := by rintros ⟨a⟩; exact quotient.sound (univ_mem_sets' $ assume a, add_left_neg _),
   .. ae_eq_fun.add_monoid
@@ -187,8 +185,8 @@ end add_comm_group
 
 section semimodule
 
-variables {K : Type*} [semiring K] [topological_space K] [second_countable_topology K]
-variables {γ : Type*} [topological_space γ] [second_countable_topology γ]
+variables {K : Type*} [semiring K] [topological_space K]
+variables {γ : Type*} [topological_space γ]
           [add_comm_monoid γ] [semimodule K γ] [topological_semimodule K γ]
 
 protected def smul : K → (α →ₘ γ) → (α →ₘ γ) :=
@@ -199,7 +197,7 @@ instance : has_scalar K (α →ₘ γ) := ⟨ae_eq_fun.smul⟩
 @[simp] lemma smul_mk (c : K) (f : α → γ) (hf) : c • (mk f hf) = mk (c • f) (measurable_smul hf) :=
 rfl
 
-variables [topological_add_monoid γ]
+variables [second_countable_topology γ] [topological_add_monoid γ]
 
 instance : semimodule K (α →ₘ γ) :=
 { one_smul  := by { rintros ⟨f, hf⟩, simp only [quot_mk_eq_mk, smul_mk, one_smul] },
@@ -223,7 +221,7 @@ end semimodule
 
 section vector_space
 
-variables {K : Type*} [discrete_field K] [topological_space K] [second_countable_topology K]
+variables {K : Type*} [discrete_field K] [topological_space K]
 variables {γ : Type*} [topological_space γ] [second_countable_topology γ] [add_comm_group γ]
           [topological_add_group γ] [vector_space K γ] [topological_semimodule K γ]
 
@@ -302,7 +300,7 @@ end metric
 
 section normed_group
 
-variables {γ : Type*} [normed_group γ] [second_countable_topology γ] [topological_add_group γ]
+variables {γ : Type*} [normed_group γ] [second_countable_topology γ]
 
 lemma edist_eq_add_add : ∀ {f g h : α →ₘ γ}, edist f g = edist (f + h) (g + h) :=
 begin
@@ -318,7 +316,7 @@ section normed_space
 
 set_option class.instance_max_depth 100
 
-variables {K : Type*} [normed_field K] [second_countable_topology K]
+variables {K : Type*} [normed_field K]
 variables {γ : Type*} [normed_group γ] [second_countable_topology γ] [normed_space K γ]
 
 lemma edist_smul (x : K) : ∀ f : α →ₘ γ, edist (x • f) 0 = (ennreal.of_real ∥x∥) * edist f 0 :=

src/measure_theory/borel_space.lean

@@ -157,11 +157,11 @@ sup_le
   (comap_le_iff_le_map.mpr $ measurable_of_continuous continuous_fst)
   (comap_le_iff_le_map.mpr $ measurable_of_continuous continuous_snd)
 
-lemma borel_induced [t : topological_space β] (f : α → β) :
+lemma borel_induced {α β} [t : topological_space β] (f : α → β) :
   @borel α (t.induced f) = (borel β).comap f :=
 comap_generate_from.symm
 
-lemma borel_eq_subtype [topological_space α] (s : set α) : borel s = subtype.measurable_space :=
+lemma borel_eq_subtype (s : set α) : borel s = subtype.measurable_space :=
 borel_induced coe
 
 lemma borel_prod [second_countable_topology α] [topological_space β] [second_countable_topology β] :
@@ -178,7 +178,7 @@ le_antisymm borel_prod_le begin
       eq.symm ▸ is_measurable_set_prod (is_measurable_of_is_open hu) (is_measurable_of_is_open hv))
 end
 
-lemma measurable_of_continuous2
+lemma measurable_of_continuous2 {α β γ}
   [topological_space α] [second_countable_topology α]
   [topological_space β] [second_countable_topology β]
   [topological_space γ] [measurable_space δ] {f : δ → α} {g : δ → β} {c : α → β → γ}
@@ -236,7 +236,7 @@ lemma measurable_coe_int_real : measurable (λa, a : ℤ → ℝ) :=
 assume s (hs : is_measurable s), by trivial
 
 section ordered_topology
-variables [linear_order α] [topological_space α] [ordered_topology α] {a b c : α}
+variables [linear_order α] [ordered_topology α] {a b c : α}
 
 lemma is_measurable_Ioo : is_measurable (Ioo a b) := is_measurable_of_is_open is_open_Ioo
 
@@ -299,15 +299,13 @@ lemma measurable.infi {α} [topological_space α] [complete_linear_order α]
 measurable.is_glb hf $ λ b, is_glb_infi
 
 lemma measurable.supr_Prop {α} [topological_space α] [complete_linear_order α]
-  [orderable_topology α] [second_countable_topology α]
   {β} [measurable_space β] {p : Prop} {f : β → α} (hf : measurable f) :
   measurable (λ b, ⨆ h : p, f b) :=
 classical.by_cases
   (assume h : p, begin convert hf, funext, exact supr_pos h end)
   (assume h : ¬p, begin convert measurable_const, funext, exact supr_neg h end)
 
 lemma measurable.infi_Prop {α} [topological_space α] [complete_linear_order α]
-  [orderable_topology α] [second_countable_topology α]
   {β} [measurable_space β] {p : Prop} {f : β → α} (hf : measurable f) :
   measurable (λ b, ⨅ h : p, f b) :=
 classical.by_cases
@@ -505,8 +503,8 @@ lemma measurable_smul' {α : Type*} {β : Type*} {γ : Type*}
 measurable_of_continuous2 (continuous_smul continuous_fst continuous_snd) hf hg
 
 lemma measurable_smul {α : Type*} {β : Type*} {γ : Type*}
-  [semiring α] [topological_space α] [second_countable_topology α]
-  [topological_space β] [add_comm_monoid β] [second_countable_topology β]
+  [semiring α] [topological_space α]
+  [topological_space β] [add_comm_monoid β]
   [semimodule α β] [topological_semimodule α β] [measurable_space γ]
   {c : α} {g : γ → β} (hg : measurable g) : measurable (λ x, c • g x) :=
 measurable.comp (measurable_of_continuous (continuous_smul continuous_const continuous_id)) hg