From 59f72a90276da41af9f9e7bd18f96530d0f0d01c Mon Sep 17 00:00:00 2001 From: grunweg Date: Wed, 13 Mar 2024 20:53:14 +0000 Subject: [PATCH] chore: remove more autoImplicit (#11336) ... or reduce its scope (the full removal is not as obvious). --- Archive/Imo/Imo1987Q1.lean | 5 +---- Mathlib/Algebra/AddTorsor.lean | 5 +---- Mathlib/Algebra/Algebra/Equiv.lean | 3 --- Mathlib/Algebra/Algebra/Hom.lean | 5 +---- Mathlib/Algebra/Algebra/NonUnitalHom.lean | 5 +---- Mathlib/Algebra/Category/GroupCat/Basic.lean | 5 +---- Mathlib/Algebra/Category/GroupWithZeroCat.lean | 7 +++---- Mathlib/Algebra/Category/ModuleCat/Free.lean | 6 ++---- .../Algebra/Category/ModuleCat/Presheaf.lean | 3 +-- .../Algebra/Category/ModuleCat/Projective.lean | 4 +--- Mathlib/Algebra/Category/MonCat/Basic.lean | 6 ++---- Mathlib/Algebra/Category/Ring/Basic.lean | 16 +++++++++------- Mathlib/Algebra/CharZero/Defs.lean | 4 ++-- Mathlib/Algebra/Field/MinimalAxioms.lean | 2 +- Mathlib/Algebra/Field/Opposite.lean | 4 ++-- .../Algebra/Homology/DifferentialObject.lean | 5 +---- Mathlib/Algebra/Homology/ImageToKernel.lean | 5 +---- .../Homology/ShortComplex/LeftHomology.lean | 11 +++++------ .../Homology/ShortComplex/RightHomology.lean | 10 ++++------ Mathlib/Algebra/Invertible/Basic.lean | 3 --- Mathlib/Algebra/Module/Torsion.lean | 6 +++--- Mathlib/Algebra/Order/Archimedean.lean | 4 ++-- Mathlib/Algebra/Order/CauSeq/Basic.lean | 6 +++--- Mathlib/Algebra/Order/Group/Bounds.lean | 4 +--- Mathlib/Algebra/Order/Invertible.lean | 4 +--- .../Algebra/Order/Monoid/Canonical/Defs.lean | 5 +---- Mathlib/Algebra/Order/Monoid/TypeTags.lean | 2 +- Mathlib/Algebra/Order/Monoid/Units.lean | 4 ++-- Mathlib/Algebra/Order/Sub/Prod.lean | 2 +- Mathlib/Algebra/PUnitInstances.lean | 14 +++++++------- Mathlib/Algebra/Ring/Basic.lean | 15 ++++++++------- Mathlib/Algebra/Ring/MinimalAxioms.lean | 2 +- Mathlib/Algebra/RingQuot.lean | 5 +---- Mathlib/AlgebraicTopology/SimplicialObject.lean | 7 ++----- Mathlib/AlgebraicTopology/SimplicialSet.lean | 10 ++++------ Mathlib/CategoryTheory/ConnectedComponents.lean | 6 +++--- .../SimpleGraph/Connectivity/Subgraph.lean | 8 ++++---- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean | 3 +-- Mathlib/Computability/NFA.lean | 6 ++---- Mathlib/Data/Finset/Lattice.lean | 6 ++---- Mathlib/Data/Int/Basic.lean | 12 ++++++------ Mathlib/Order/CompleteLattice.lean | 4 ++-- Mathlib/Order/Estimator.lean | 1 - Mathlib/Order/Iterate.lean | 17 +++++++---------- Mathlib/Order/Minimal.lean | 7 ++++--- Mathlib/Order/PropInstances.lean | 5 ++--- 46 files changed, 110 insertions(+), 169 deletions(-) diff --git a/Archive/Imo/Imo1987Q1.lean b/Archive/Imo/Imo1987Q1.lean index adc0a98a1697c..0dc0be5e39ed1 100644 --- a/Archive/Imo/Imo1987Q1.lean +++ b/Archive/Imo/Imo1987Q1.lean @@ -24,9 +24,6 @@ The original problem assumes `n ≥ 1`. It turns out that a version with `n * (n holds true for `n = 0` as well, so we first prove it, then deduce the original version in the case `n ≥ 1`. -/ - -set_option autoImplicit true - variable (α : Type*) [Fintype α] [DecidableEq α] open scoped BigOperators Nat @@ -62,7 +59,7 @@ def fiber (k : ℕ) : Set (Perm α) := {σ : Perm α | card (fixedPoints σ) = k} #align imo1987_q1.fiber Imo1987Q1.fiber -instance : Fintype (fiber α k) := by unfold fiber; infer_instance +instance {k : ℕ} : Fintype (fiber α k) := by unfold fiber; infer_instance @[simp] theorem mem_fiber {σ : Perm α} {k : ℕ} : σ ∈ fiber α k ↔ card (fixedPoints σ) = k := diff --git a/Mathlib/Algebra/AddTorsor.lean b/Mathlib/Algebra/AddTorsor.lean index 6c2ae3172a455..d9507a7ec5117 100644 --- a/Mathlib/Algebra/AddTorsor.lean +++ b/Mathlib/Algebra/AddTorsor.lean @@ -39,9 +39,6 @@ multiplicative group actions). -/ -set_option autoImplicit true - - /-- An `AddTorsor G P` gives a structure to the nonempty type `P`, acted on by an `AddGroup G` with a transitive and free action given by the `+ᵥ` operation and a corresponding subtraction given by the @@ -277,7 +274,7 @@ end comm namespace Prod -variable {G : Type*} [AddGroup G] [AddGroup G'] [AddTorsor G P] [AddTorsor G' P'] +variable {G G' P P' : Type*} [AddGroup G] [AddGroup G'] [AddTorsor G P] [AddTorsor G' P'] instance instAddTorsor : AddTorsor (G × G') (P × P') where vadd v p := (v.1 +ᵥ p.1, v.2 +ᵥ p.2) diff --git a/Mathlib/Algebra/Algebra/Equiv.lean b/Mathlib/Algebra/Algebra/Equiv.lean index 3850598f18e1e..ec20fcd745c3b 100644 --- a/Mathlib/Algebra/Algebra/Equiv.lean +++ b/Mathlib/Algebra/Algebra/Equiv.lean @@ -21,9 +21,6 @@ This file defines bundled isomorphisms of `R`-algebras. * `A ≃ₐ[R] B` : `R`-algebra equivalence from `A` to `B`. -/ -set_option autoImplicit true - - open BigOperators universe u v w u₁ v₁ diff --git a/Mathlib/Algebra/Algebra/Hom.lean b/Mathlib/Algebra/Algebra/Hom.lean index 3f126da76f3a9..9c6c1ea2d54e6 100644 --- a/Mathlib/Algebra/Algebra/Hom.lean +++ b/Mathlib/Algebra/Algebra/Hom.lean @@ -23,9 +23,6 @@ This file defines bundled homomorphisms of `R`-algebras. * `A →ₐ[R] B` : `R`-algebra homomorphism from `A` to `B`. -/ -set_option autoImplicit true - - open BigOperators universe u v w u₁ v₁ @@ -62,7 +59,7 @@ class AlgHomClass (F : Type*) (R A B : outParam Type*) namespace AlgHomClass -variable {R : Type*} {A : Type*} {B : Type*} [CommSemiring R] [Semiring A] [Semiring B] +variable {R A B F : Type*} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [FunLike F A B] -- see Note [lower instance priority] diff --git a/Mathlib/Algebra/Algebra/NonUnitalHom.lean b/Mathlib/Algebra/Algebra/NonUnitalHom.lean index fca4694bc14fe..42221362eb7e1 100644 --- a/Mathlib/Algebra/Algebra/NonUnitalHom.lean +++ b/Mathlib/Algebra/Algebra/NonUnitalHom.lean @@ -43,9 +43,6 @@ TODO: add `NonUnitalAlgEquiv` when needed. non-unital, algebra, morphism -/ -set_option autoImplicit true - - universe u v w w₁ w₂ w₃ variable (R : Type u) (A : Type v) (B : Type w) (C : Type w₁) @@ -442,7 +439,7 @@ variable {R A B} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] -- see Note [lower instance priority] -instance (priority := 100) [FunLike F A B] [AlgHomClass F R A B] : +instance (priority := 100) {F : Type*} [FunLike F A B] [AlgHomClass F R A B] : NonUnitalAlgHomClass F R A B := { ‹AlgHomClass F R A B› with map_smul := map_smul } diff --git a/Mathlib/Algebra/Category/GroupCat/Basic.lean b/Mathlib/Algebra/Category/GroupCat/Basic.lean index fa38ddc536cd4..96c5070fa933f 100644 --- a/Mathlib/Algebra/Category/GroupCat/Basic.lean +++ b/Mathlib/Algebra/Category/GroupCat/Basic.lean @@ -19,9 +19,6 @@ We introduce the bundled categories: along with the relevant forgetful functors between them, and to the bundled monoid categories. -/ -set_option autoImplicit true - - universe u v open CategoryTheory @@ -80,7 +77,7 @@ lemma coe_comp {X Y Z : GroupCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → lemma comp_def {X Y Z : GroupCat} {f : X ⟶ Y} {g : Y ⟶ Z} : f ≫ g = g.comp f := rfl -- porting note (#10756): added lemma -@[simp] lemma forget_map (f : X ⟶ Y) : (forget GroupCat).map f = (f : X → Y) := rfl +@[simp] lemma forget_map {X Y : GroupCat} (f : X ⟶ Y) : (forget GroupCat).map f = (f : X → Y) := rfl @[to_additive (attr := ext)] lemma ext {X Y : GroupCat} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g := diff --git a/Mathlib/Algebra/Category/GroupWithZeroCat.lean b/Mathlib/Algebra/Category/GroupWithZeroCat.lean index 58d13d3af3dde..449223a76de25 100644 --- a/Mathlib/Algebra/Category/GroupWithZeroCat.lean +++ b/Mathlib/Algebra/Category/GroupWithZeroCat.lean @@ -14,9 +14,6 @@ import Mathlib.Algebra.Category.MonCat.Basic This file defines `GroupWithZeroCat`, the category of groups with zero. -/ -set_option autoImplicit true - - universe u open CategoryTheory Order @@ -73,7 +70,9 @@ instance groupWithZeroConcreteCategory : ConcreteCategory GroupWithZeroCat where forget_faithful := ⟨fun h => DFunLike.coe_injective h⟩ -- porting note (#10756): added lemma -@[simp] lemma forget_map (f : X ⟶ Y) : (forget GroupWithZeroCat).map f = f := rfl +@[simp] lemma forget_map {X Y : GroupWithZeroCat} (f : X ⟶ Y) : + (forget GroupWithZeroCat).map f = f := rfl + instance hasForgetToBipointed : HasForget₂ GroupWithZeroCat Bipointed where forget₂ := { obj := fun X => ⟨X, 0, 1⟩ diff --git a/Mathlib/Algebra/Category/ModuleCat/Free.lean b/Mathlib/Algebra/Category/ModuleCat/Free.lean index 50d332538e370..9f90f1cd4caaf 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Free.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Free.lean @@ -26,8 +26,6 @@ linear algebra, module, free -/ -set_option autoImplicit true - open CategoryTheory namespace ModuleCat @@ -83,7 +81,7 @@ end LinearIndependent section Span - +set_option autoImplicit true in /-- In the commutative diagram ``` f g @@ -166,7 +164,7 @@ theorem free_shortExact_rank_add [Module.Free R S.X₁] [Module.Free R S.X₃] exact ⟨Basis.indexEquiv (Module.Free.chooseBasis R S.X₂) (Basis.ofShortExact hS' (Module.Free.chooseBasis R S.X₁) (Module.Free.chooseBasis R S.X₃))⟩ -theorem free_shortExact_finrank_add [Module.Free R S.X₁] [Module.Free R S.X₃] +theorem free_shortExact_finrank_add {n p : ℕ} [Module.Free R S.X₁] [Module.Free R S.X₃] [Module.Finite R S.X₁] [Module.Finite R S.X₃] (hN : FiniteDimensional.finrank R S.X₁ = n) (hP : FiniteDimensional.finrank R S.X₃ = p) diff --git a/Mathlib/Algebra/Category/ModuleCat/Presheaf.lean b/Mathlib/Algebra/Category/ModuleCat/Presheaf.lean index 54f8b072e2bb7..ff455552bb71e 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Presheaf.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Presheaf.lean @@ -22,13 +22,12 @@ as a presheaf of abelian groups with additional data. * Pushforward and pullback. -/ -universe v₁ u₁ u +universe v₁ u₁ u v open CategoryTheory LinearMap Opposite variable {C : Type u₁} [Category.{v₁} C] -set_option autoImplicit true in /-- A presheaf of modules over a given presheaf of rings, described as a presheaf of abelian groups, and the extra data of the action at each object, and a condition relating functoriality and scalar multiplication. -/ diff --git a/Mathlib/Algebra/Category/ModuleCat/Projective.lean b/Mathlib/Algebra/Category/ModuleCat/Projective.lean index b47176b046c7b..5b3f8cda91f82 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Projective.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Projective.lean @@ -15,9 +15,7 @@ import Mathlib.Data.Finsupp.Basic # The category of `R`-modules has enough projectives. -/ -set_option autoImplicit true - -universe v u +universe v u u' open CategoryTheory diff --git a/Mathlib/Algebra/Category/MonCat/Basic.lean b/Mathlib/Algebra/Category/MonCat/Basic.lean index 8f5b97ad1e1ff..c2dbca73f1374 100644 --- a/Mathlib/Algebra/Category/MonCat/Basic.lean +++ b/Mathlib/Algebra/Category/MonCat/Basic.lean @@ -20,9 +20,6 @@ We introduce the bundled categories: along with the relevant forgetful functors between them. -/ -set_option autoImplicit true - - universe u v open CategoryTheory @@ -102,7 +99,8 @@ lemma coe_id {X : MonCat} : (𝟙 X : X → X) = id := rfl lemma coe_comp {X Y Z : MonCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl -- porting note (#10756): added lemma -@[to_additive (attr := simp)] lemma forget_map (f : X ⟶ Y) : (forget MonCat).map f = f := rfl +@[to_additive (attr := simp)] lemma forget_map {X Y : MonCat} (f : X ⟶ Y) : + (forget MonCat).map f = f := rfl @[to_additive (attr := ext)] lemma ext {X Y : MonCat} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g := diff --git a/Mathlib/Algebra/Category/Ring/Basic.lean b/Mathlib/Algebra/Category/Ring/Basic.lean index 6f2e184e02622..e455f632a7b02 100644 --- a/Mathlib/Algebra/Category/Ring/Basic.lean +++ b/Mathlib/Algebra/Category/Ring/Basic.lean @@ -20,9 +20,6 @@ We introduce the bundled categories: along with the relevant forgetful functors between them. -/ -set_option autoImplicit true - - universe u v open CategoryTheory @@ -92,7 +89,8 @@ lemma coe_id {X : SemiRingCat} : (𝟙 X : X → X) = id := rfl lemma coe_comp {X Y Z : SemiRingCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl -- porting note (#10756): added lemma -@[simp] lemma forget_map (f : X ⟶ Y) : (forget SemiRingCat).map f = (f : X → Y) := rfl +@[simp] lemma forget_map {X Y : SemiRingCat} (f : X ⟶ Y) : + (forget SemiRingCat).map f = (f : X → Y) := rfl lemma ext {X Y : SemiRingCat} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g := RingHom.ext w @@ -150,6 +148,7 @@ theorem ofHom_apply {R S : Type u} [Semiring R] [Semiring S] (f : R →+* S) (x set_option linter.uppercaseLean3 false in #align SemiRing.of_hom_apply SemiRingCat.ofHom_apply +set_option autoImplicit true in /-- Ring equivalence are isomorphisms in category of semirings -/ @@ -216,7 +215,7 @@ lemma coe_id {X : RingCat} : (𝟙 X : X → X) = id := rfl lemma coe_comp {X Y Z : RingCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl -- porting note (#10756): added lemma -@[simp] lemma forget_map (f : X ⟶ Y) : (forget RingCat).map f = (f : X → Y) := rfl +@[simp] lemma forget_map {X Y : RingCat} (f : X ⟶ Y) : (forget RingCat).map f = (f : X → Y) := rfl lemma ext {X Y : RingCat} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g := RingHom.ext w @@ -322,7 +321,8 @@ lemma coe_id {X : CommSemiRingCat} : (𝟙 X : X → X) = id := rfl lemma coe_comp {X Y Z : CommSemiRingCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl -- porting note (#10756): added lemma -@[simp] lemma forget_map (f : X ⟶ Y) : (forget CommSemiRingCat).map f = (f : X → Y) := rfl +@[simp] lemma forget_map {X Y : CommSemiRingCat} (f : X ⟶ Y) : + (forget CommSemiRingCat).map f = (f : X → Y) := rfl lemma ext {X Y : CommSemiRingCat} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g := RingHom.ext w @@ -379,6 +379,7 @@ instance hasForgetToCommMonCat : HasForget₂ CommSemiRingCat CommMonCat := set_option linter.uppercaseLean3 false in #align CommSemiRing.has_forget_to_CommMon CommSemiRingCat.hasForgetToCommMonCat +set_option autoImplicit true in /-- Ring equivalence are isomorphisms in category of commutative semirings -/ @@ -442,7 +443,8 @@ lemma coe_id {X : CommRingCat} : (𝟙 X : X → X) = id := rfl lemma coe_comp {X Y Z : CommRingCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl -- porting note (#10756): added lemma -@[simp] lemma forget_map (f : X ⟶ Y) : (forget CommRingCat).map f = (f : X → Y) := rfl +@[simp] lemma forget_map {X Y : CommRingCat} (f : X ⟶ Y) : + (forget CommRingCat).map f = (f : X → Y) := rfl lemma ext {X Y : CommRingCat} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g := RingHom.ext w diff --git a/Mathlib/Algebra/CharZero/Defs.lean b/Mathlib/Algebra/CharZero/Defs.lean index d1b33a2a259cc..332b04025ca6d 100644 --- a/Mathlib/Algebra/CharZero/Defs.lean +++ b/Mathlib/Algebra/CharZero/Defs.lean @@ -29,8 +29,6 @@ from the natural numbers into it is injective. * Unify with `CharP` (possibly using an out-parameter) -/ -set_option autoImplicit true - /-- Typeclass for monoids with characteristic zero. (This is usually stated on fields but it makes sense for any additive monoid with 1.) @@ -47,6 +45,8 @@ class CharZero (R) [AddMonoidWithOne R] : Prop where cast_injective : Function.Injective (Nat.cast : ℕ → R) #align char_zero CharZero +variable {R : Type*} + theorem charZero_of_inj_zero [AddGroupWithOne R] (H : ∀ n : ℕ, (n : R) = 0 → n = 0) : CharZero R := ⟨@fun m n h => by diff --git a/Mathlib/Algebra/Field/MinimalAxioms.lean b/Mathlib/Algebra/Field/MinimalAxioms.lean index 360b33f28883e..6357510456749 100644 --- a/Mathlib/Algebra/Field/MinimalAxioms.lean +++ b/Mathlib/Algebra/Field/MinimalAxioms.lean @@ -19,7 +19,7 @@ a minimum number of equalities. -/ -set_option autoImplicit true +universe u /-- Define a `Field` structure on a Type by proving a minimized set of axioms. Note that this uses the default definitions for `npow`, `nsmul`, `zsmul`, `div` and `sub` diff --git a/Mathlib/Algebra/Field/Opposite.lean b/Mathlib/Algebra/Field/Opposite.lean index 8d5da6e4cfa5b..429d495194d8c 100644 --- a/Mathlib/Algebra/Field/Opposite.lean +++ b/Mathlib/Algebra/Field/Opposite.lean @@ -13,8 +13,6 @@ import Mathlib.Data.Int.Cast.Lemmas # Field structure on the multiplicative/additive opposite -/ -set_option autoImplicit true - namespace MulOpposite variable (α : Type*) @@ -59,6 +57,8 @@ end MulOpposite namespace AddOpposite +variable {α : Type*} + instance divisionSemiring [DivisionSemiring α] : DivisionSemiring αᵃᵒᵖ := { AddOpposite.groupWithZero α, AddOpposite.semiring α with } diff --git a/Mathlib/Algebra/Homology/DifferentialObject.lean b/Mathlib/Algebra/Homology/DifferentialObject.lean index e533e7959022c..eb913fad16024 100644 --- a/Mathlib/Algebra/Homology/DifferentialObject.lean +++ b/Mathlib/Algebra/Homology/DifferentialObject.lean @@ -18,9 +18,6 @@ This equivalence is probably not particularly useful in practice; it's here to check that definitions match up as expected. -/ -set_option autoImplicit true - - open CategoryTheory CategoryTheory.Limits open scoped Classical @@ -58,7 +55,7 @@ theorem objEqToHom_d {x y : β} (h : x = y) : #align homological_complex.eq_to_hom_d CategoryTheory.DifferentialObject.objEqToHom_d @[reassoc (attr := simp)] -theorem d_squared_apply : X.d x ≫ X.d _ = 0 := congr_fun X.d_squared _ +theorem d_squared_apply {x : β} : X.d x ≫ X.d _ = 0 := congr_fun X.d_squared _ @[reassoc (attr := simp)] theorem eqToHom_f' {X Y : DifferentialObject ℤ (GradedObjectWithShift b V)} (f : X ⟶ Y) {x y : β} diff --git a/Mathlib/Algebra/Homology/ImageToKernel.lean b/Mathlib/Algebra/Homology/ImageToKernel.lean index bd1d5565ee414..37403b7321229 100644 --- a/Mathlib/Algebra/Homology/ImageToKernel.lean +++ b/Mathlib/Algebra/Homology/ImageToKernel.lean @@ -24,10 +24,7 @@ renamed `homology'`. It is planned that this definition shall be removed and rep -/ -set_option autoImplicit true - - -universe v u +universe v u w open CategoryTheory CategoryTheory.Limits diff --git a/Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean b/Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean index 9ff3baac49e6f..9c8dcdc751f5b 100644 --- a/Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean +++ b/Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean @@ -29,8 +29,6 @@ and `S.homology`. -/ -set_option autoImplicit true - namespace CategoryTheory open Category Limits @@ -421,21 +419,22 @@ instance : Epi S.leftHomologyπ := by dsimp only [leftHomologyπ] infer_instance -lemma leftHomology_ext_iff (f₁ f₂ : S.leftHomology ⟶ A) : +lemma leftHomology_ext_iff {A : C} (f₁ f₂ : S.leftHomology ⟶ A) : f₁ = f₂ ↔ S.leftHomologyπ ≫ f₁ = S.leftHomologyπ ≫ f₂ := by rw [cancel_epi] @[ext] -lemma leftHomology_ext (f₁ f₂ : S.leftHomology ⟶ A) +lemma leftHomology_ext {A : C} (f₁ f₂ : S.leftHomology ⟶ A) (h : S.leftHomologyπ ≫ f₁ = S.leftHomologyπ ≫ f₂) : f₁ = f₂ := by simpa only [leftHomology_ext_iff] using h -lemma cycles_ext_iff (f₁ f₂ : A ⟶ S.cycles) : +lemma cycles_ext_iff {A : C} (f₁ f₂ : A ⟶ S.cycles) : f₁ = f₂ ↔ f₁ ≫ S.iCycles = f₂ ≫ S.iCycles := by rw [cancel_mono] @[ext] -lemma cycles_ext (f₁ f₂ : A ⟶ S.cycles) (h : f₁ ≫ S.iCycles = f₂ ≫ S.iCycles) : f₁ = f₂ := by +lemma cycles_ext {A : C} (f₁ f₂ : A ⟶ S.cycles) (h : f₁ ≫ S.iCycles = f₂ ≫ S.iCycles) : + f₁ = f₂ := by simpa only [cycles_ext_iff] using h lemma isIso_iCycles (hg : S.g = 0) : IsIso S.iCycles := diff --git a/Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean b/Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean index 8082e6ce957e1..0b11d58481f18 100644 --- a/Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean +++ b/Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean @@ -27,8 +27,6 @@ In `Homology.lean`, when `S` has two compatible left and right homology data -/ -set_option autoImplicit true - namespace CategoryTheory open Category Limits @@ -513,21 +511,21 @@ instance : Mono S.rightHomologyι := by dsimp only [rightHomologyι] infer_instance -lemma rightHomology_ext_iff (f₁ f₂ : A ⟶ S.rightHomology) : +lemma rightHomology_ext_iff {A : C} (f₁ f₂ : A ⟶ S.rightHomology) : f₁ = f₂ ↔ f₁ ≫ S.rightHomologyι = f₂ ≫ S.rightHomologyι := by rw [cancel_mono] @[ext] -lemma rightHomology_ext (f₁ f₂ : A ⟶ S.rightHomology) +lemma rightHomology_ext {A : C} (f₁ f₂ : A ⟶ S.rightHomology) (h : f₁ ≫ S.rightHomologyι = f₂ ≫ S.rightHomologyι) : f₁ = f₂ := by simpa only [rightHomology_ext_iff] -lemma opcycles_ext_iff (f₁ f₂ : S.opcycles ⟶ A) : +lemma opcycles_ext_iff {A : C} (f₁ f₂ : S.opcycles ⟶ A) : f₁ = f₂ ↔ S.pOpcycles ≫ f₁ = S.pOpcycles ≫ f₂ := by rw [cancel_epi] @[ext] -lemma opcycles_ext (f₁ f₂ : S.opcycles ⟶ A) +lemma opcycles_ext {A : C} (f₁ f₂ : S.opcycles ⟶ A) (h : S.pOpcycles ≫ f₁ = S.pOpcycles ≫ f₂) : f₁ = f₂ := by simpa only [opcycles_ext_iff] diff --git a/Mathlib/Algebra/Invertible/Basic.lean b/Mathlib/Algebra/Invertible/Basic.lean index aac695f7798fa..a10baa50cb5ed 100644 --- a/Mathlib/Algebra/Invertible/Basic.lean +++ b/Mathlib/Algebra/Invertible/Basic.lean @@ -15,9 +15,6 @@ import Mathlib.Algebra.Ring.Defs -/ -set_option autoImplicit true - - universe u variable {α : Type u} diff --git a/Mathlib/Algebra/Module/Torsion.lean b/Mathlib/Algebra/Module/Torsion.lean index 487c559e72152..b766a86f0b0f4 100644 --- a/Mathlib/Algebra/Module/Torsion.lean +++ b/Mathlib/Algebra/Module/Torsion.lean @@ -62,9 +62,6 @@ import Mathlib.Data.Set.Lattice Torsion, submodule, module, quotient -/ -set_option autoImplicit true - - namespace Ideal section TorsionOf @@ -173,6 +170,7 @@ def torsionBySet (s : Set R) : Submodule R M := sInf (torsionBy R M '' s) #align submodule.torsion_by_set Submodule.torsionBySet +set_option autoImplicit true in -- Porting note: torsion' had metavariables and factoring out this fixed it -- perhaps there is a better fix /-- The additive submonoid of all elements `x` of `M` such that `a • x = 0` @@ -187,6 +185,7 @@ def torsion'AddSubMonoid (S : Type w) [CommMonoid S] [DistribMulAction S M] : rw [smul_add, mul_smul, mul_comm, mul_smul, hx, hy, smul_zero, smul_zero, add_zero] zero_mem' := ⟨1, smul_zero 1⟩ +set_option autoImplicit true in /-- The `S`-torsion submodule, containing all elements `x` of `M` such that `a • x = 0` for some `a` in `S`. -/ @[simps!] @@ -833,6 +832,7 @@ namespace Ideal.Quotient open Submodule +universe w theorem torsionBy_eq_span_singleton {R : Type w} [CommRing R] (a b : R) (ha : a ∈ R⁰) : torsionBy R (R ⧸ R ∙ a * b) a = R ∙ mk (R ∙ a * b) b := by ext x; rw [mem_torsionBy_iff, Submodule.mem_span_singleton] diff --git a/Mathlib/Algebra/Order/Archimedean.lean b/Mathlib/Algebra/Order/Archimedean.lean index c3b853a17eb84..bd2834c5d8bdc 100644 --- a/Mathlib/Algebra/Order/Archimedean.lean +++ b/Mathlib/Algebra/Order/Archimedean.lean @@ -30,8 +30,6 @@ number `n` such that `x ≤ n • y`. * `ℕ`, `ℤ`, and `ℚ` are archimedean. -/ -set_option autoImplicit true - open Int Set variable {α : Type*} @@ -50,6 +48,8 @@ instance OrderDual.archimedean [OrderedAddCommGroup α] [Archimedean α] : Archi ⟨n, by rwa [neg_nsmul, neg_le_neg_iff] at hn⟩⟩ #align order_dual.archimedean OrderDual.archimedean +variable {M : Type*} + theorem exists_lt_nsmul [OrderedAddCommMonoid M] [Archimedean M] [CovariantClass M M (· + ·) (· < ·)] {a : M} (ha : 0 < a) (b : M) : ∃ n : ℕ, b < n • a := diff --git a/Mathlib/Algebra/Order/CauSeq/Basic.lean b/Mathlib/Algebra/Order/CauSeq/Basic.lean index 438b7edc26a59..2241b6aa6f12d 100644 --- a/Mathlib/Algebra/Order/CauSeq/Basic.lean +++ b/Mathlib/Algebra/Order/CauSeq/Basic.lean @@ -39,7 +39,7 @@ assert_not_exists Module assert_not_exists Submonoid assert_not_exists FloorRing -set_option autoImplicit true +variable {α β : Type*} open IsAbsoluteValue @@ -349,7 +349,7 @@ theorem const_sub (x y : β) : const (x - y) = const x - const y := section SMul -variable [SMul G β] [IsScalarTower G β β] +variable {G : Type*} [SMul G β] [IsScalarTower G β β] instance : SMul G (CauSeq β abv) := ⟨fun a f => (ofEq (const (a • (1 : β)) * f) (a • (f : ℕ → β))) fun _ => smul_one_mul _ _⟩ @@ -580,7 +580,7 @@ theorem mul_equiv_mul {f1 f2 g1 g2 : CauSeq β abv} (hf : f1 ≈ f2) (hg : g1 -/ #align cau_seq.mul_equiv_mul CauSeq.mul_equiv_mul -theorem smul_equiv_smul [SMul G β] [IsScalarTower G β β] {f1 f2 : CauSeq β abv} (c : G) +theorem smul_equiv_smul {G : Type*} [SMul G β] [IsScalarTower G β β] {f1 f2 : CauSeq β abv} (c : G) (hf : f1 ≈ f2) : c • f1 ≈ c • f2 := by simpa [const_smul, smul_one_mul _ _] using mul_equiv_mul (const_equiv.mpr <| Eq.refl <| c • (1 : β)) hf diff --git a/Mathlib/Algebra/Order/Group/Bounds.lean b/Mathlib/Algebra/Order/Group/Bounds.lean index 3a25a03dfa15d..126a80695d374 100644 --- a/Mathlib/Algebra/Order/Group/Bounds.lean +++ b/Mathlib/Algebra/Order/Group/Bounds.lean @@ -12,11 +12,9 @@ import Mathlib.Algebra.Order.Group.Defs # Least upper bound and the greatest lower bound in linear ordered additive commutative groups -/ -set_option autoImplicit true - section LinearOrderedAddCommGroup -variable [LinearOrderedAddCommGroup α] {s : Set α} {a ε : α} +variable {α : Type*} [LinearOrderedAddCommGroup α] {s : Set α} {a ε : α} theorem IsGLB.exists_between_self_add (h : IsGLB s a) (hε : 0 < ε) : ∃ b ∈ s, a ≤ b ∧ b < a + ε := h.exists_between <| lt_add_of_pos_right _ hε diff --git a/Mathlib/Algebra/Order/Invertible.lean b/Mathlib/Algebra/Order/Invertible.lean index ee044b4d7045a..600cae7ae7fe1 100644 --- a/Mathlib/Algebra/Order/Invertible.lean +++ b/Mathlib/Algebra/Order/Invertible.lean @@ -13,9 +13,7 @@ import Mathlib.Data.Nat.Cast.Order # Lemmas about `invOf` in ordered (semi)rings. -/ -set_option autoImplicit true - -variable [LinearOrderedSemiring α] {a : α} +variable {α : Type*} [LinearOrderedSemiring α] {a : α} @[simp] theorem invOf_pos [Invertible a] : 0 < ⅟ a ↔ 0 < a := diff --git a/Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean b/Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean index 39b8460570d0d..d641f378b1575 100644 --- a/Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean +++ b/Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean @@ -14,9 +14,6 @@ import Mathlib.Algebra.Order.Monoid.Defs # Canonically ordered monoids -/ -set_option autoImplicit true - - universe u variable {α : Type u} @@ -308,7 +305,7 @@ theorem of_gt {M} [CanonicallyOrderedAddCommMonoid M] {x y : M} (h : x < y) : Ne -- 1 < p is still an often-used `Fact`, due to `Nat.Prime` implying it, and it implying `Nontrivial` -- on `ZMod`'s ring structure. We cannot just set this to be any `x < y`, else that becomes a -- metavariable and it will hugely slow down typeclass inference. -instance (priority := 10) of_gt' [CanonicallyOrderedAddCommMonoid M] [One M] {y : M} +instance (priority := 10) of_gt' {M : Type*} [CanonicallyOrderedAddCommMonoid M] [One M] {y : M} -- Porting note: Fact.out has different type signature from mathlib3 [Fact (1 < y)] : NeZero y := of_gt <| @Fact.out (1 < y) _ #align ne_zero.of_gt' NeZero.of_gt' diff --git a/Mathlib/Algebra/Order/Monoid/TypeTags.lean b/Mathlib/Algebra/Order/Monoid/TypeTags.lean index 818c12d5a03d2..b891ba7d927fd 100644 --- a/Mathlib/Algebra/Order/Monoid/TypeTags.lean +++ b/Mathlib/Algebra/Order/Monoid/TypeTags.lean @@ -11,7 +11,7 @@ import Mathlib.Algebra.Order.Monoid.Canonical.Defs /-! # Ordered monoid structures on `Multiplicative α` and `Additive α`. -/ -set_option autoImplicit true +variable {α : Type*} instance : ∀ [LE α], LE (Multiplicative α) := fun {inst} => inst diff --git a/Mathlib/Algebra/Order/Monoid/Units.lean b/Mathlib/Algebra/Order/Monoid/Units.lean index 3d448403476f4..887e65e1f382e 100644 --- a/Mathlib/Algebra/Order/Monoid/Units.lean +++ b/Mathlib/Algebra/Order/Monoid/Units.lean @@ -13,10 +13,10 @@ import Mathlib.Algebra.Group.Units # Units in ordered monoids -/ -set_option autoImplicit true - namespace Units +variable {α : Type*} + @[to_additive] instance [Monoid α] [Preorder α] : Preorder αˣ := Preorder.lift val diff --git a/Mathlib/Algebra/Order/Sub/Prod.lean b/Mathlib/Algebra/Order/Sub/Prod.lean index 6b07253dbd573..627fd0984511c 100644 --- a/Mathlib/Algebra/Order/Sub/Prod.lean +++ b/Mathlib/Algebra/Order/Sub/Prod.lean @@ -10,7 +10,7 @@ import Mathlib.Algebra.Order.Sub.Defs # Products of `OrderedSub` types. -/ -set_option autoImplicit true +variable {α β : Type*} instance Prod.orderedSub [Preorder α] [Add α] [Sub α] [OrderedSub α] [Sub β] [Preorder β] [Add β] [OrderedSub β] : diff --git a/Mathlib/Algebra/PUnitInstances.lean b/Mathlib/Algebra/PUnitInstances.lean index cc8b7faae487d..562e117130b38 100644 --- a/Mathlib/Algebra/PUnitInstances.lean +++ b/Mathlib/Algebra/PUnitInstances.lean @@ -18,8 +18,6 @@ This file collects facts about algebraic structures on the one-element type, e.g commutative ring. -/ -set_option autoImplicit true - namespace PUnit @[to_additive] @@ -50,21 +48,21 @@ theorem one_eq : (1 : PUnit) = unit := -- note simp can prove this when the Boolean ring structure is introduced @[to_additive] -theorem mul_eq : x * y = unit := +theorem mul_eq {x y : PUnit} : x * y = unit := rfl #align punit.mul_eq PUnit.mul_eq #align punit.add_eq PUnit.add_eq -- `sub_eq` simplifies `PUnit.sub_eq`, but the latter is eligible for `dsimp` @[to_additive (attr := simp, nolint simpNF)] -theorem div_eq : x / y = unit := +theorem div_eq {x y : PUnit} : x / y = unit := rfl #align punit.div_eq PUnit.div_eq #align punit.sub_eq PUnit.sub_eq -- `neg_eq` simplifies `PUnit.neg_eq`, but the latter is eligible for `dsimp` @[to_additive (attr := simp, nolint simpNF)] -theorem inv_eq : x⁻¹ = unit := +theorem inv_eq {x : PUnit} : x⁻¹ = unit := rfl #align punit.inv_eq PUnit.inv_eq #align punit.neg_eq PUnit.neg_eq @@ -98,12 +96,12 @@ instance normalizedGCDMonoid : NormalizedGCDMonoid PUnit where normalize_lcm := by intros; rfl -- Porting note (#10618): simpNF lint: simp can prove this @[simp] -theorem gcd_eq : gcd x y = unit := +theorem gcd_eq {x y : PUnit} : gcd x y = unit := rfl #align punit.gcd_eq PUnit.gcd_eq -- Porting note (#10618): simpNF lint: simp can prove this @[simp] -theorem lcm_eq : lcm x y = unit := +theorem lcm_eq {x y : PUnit} : lcm x y = unit := rfl #align punit.lcm_eq PUnit.lcm_eq @@ -129,6 +127,8 @@ instance : LinearOrderedAddCommMonoidWithTop PUnit := { PUnit.instCompleteBooleanAlgebra, PUnit.linearOrderedCancelAddCommMonoid with top_add' := fun _ => rfl } +variable {R S : Type*} + @[to_additive] instance smul : SMul R PUnit := ⟨fun _ _ => unit⟩ diff --git a/Mathlib/Algebra/Ring/Basic.lean b/Mathlib/Algebra/Ring/Basic.lean index 48f186058533f..acbec8167aa5a 100644 --- a/Mathlib/Algebra/Ring/Basic.lean +++ b/Mathlib/Algebra/Ring/Basic.lean @@ -22,7 +22,7 @@ the present file is about their interaction. For the definitions of semirings and rings see `Algebra.Ring.Defs`. -/ -set_option autoImplicit true +variable {R : Type*} open Function @@ -48,7 +48,8 @@ end AddHom section AddHomClass -variable {F : Type*} [NonAssocSemiring α] [NonAssocSemiring β] [FunLike F α β] [AddHomClass F α β] +variable {α β F : Type*} [NonAssocSemiring α] [NonAssocSemiring β] + [FunLike F α β] [AddHomClass F α β] set_option linter.deprecated false in /-- Additive homomorphisms preserve `bit0`. -/ @@ -98,7 +99,7 @@ section HasDistribNeg section Mul -variable [Mul α] [HasDistribNeg α] +variable {α : Type*} [Mul α] [HasDistribNeg α] open MulOpposite @@ -111,7 +112,7 @@ end Mul section Group -variable [Group α] [HasDistribNeg α] +variable {α : Type*} [Group α] [HasDistribNeg α] @[simp] theorem inv_neg' (a : α) : (-a)⁻¹ = -a⁻¹ := by @@ -124,7 +125,7 @@ end HasDistribNeg section NonUnitalCommRing -variable [NonUnitalCommRing α] {a b c : α} +variable {α : Type*} [NonUnitalCommRing α] {a b c : α} attribute [local simp] add_assoc add_comm add_left_comm mul_comm @@ -142,11 +143,11 @@ set_option linter.uppercaseLean3 false in end NonUnitalCommRing -theorem succ_ne_self [NonAssocRing α] [Nontrivial α] (a : α) : a + 1 ≠ a := fun h => +theorem succ_ne_self {α : Type*} [NonAssocRing α] [Nontrivial α] (a : α) : a + 1 ≠ a := fun h => one_ne_zero ((add_right_inj a).mp (by simp [h])) #align succ_ne_self succ_ne_self -theorem pred_ne_self [NonAssocRing α] [Nontrivial α] (a : α) : a - 1 ≠ a := fun h ↦ +theorem pred_ne_self {α : Type*} [NonAssocRing α] [Nontrivial α] (a : α) : a - 1 ≠ a := fun h ↦ one_ne_zero (neg_injective ((add_right_inj a).mp (by simp [← sub_eq_add_neg, h]))) #align pred_ne_self pred_ne_self diff --git a/Mathlib/Algebra/Ring/MinimalAxioms.lean b/Mathlib/Algebra/Ring/MinimalAxioms.lean index 26b043b3a5595..a5f345358b389 100644 --- a/Mathlib/Algebra/Ring/MinimalAxioms.lean +++ b/Mathlib/Algebra/Ring/MinimalAxioms.lean @@ -22,7 +22,7 @@ a minimum number of equalities. -/ -set_option autoImplicit true +universe u /-- Define a `Ring` structure on a Type by proving a minimized set of axioms. Note that this uses the default definitions for `npow`, `nsmul`, `zsmul` and `sub` diff --git a/Mathlib/Algebra/RingQuot.lean b/Mathlib/Algebra/RingQuot.lean index 7fd1f7c0ab415..1cf7aa6ba1055 100644 --- a/Mathlib/Algebra/RingQuot.lean +++ b/Mathlib/Algebra/RingQuot.lean @@ -23,10 +23,7 @@ definition, which is made irreducible for this purpose. Since everything runs in parallel for quotients of `R`-algebras, we do that case at the same time. -/ -set_option autoImplicit true - - -universe uR uS uT uA +universe uR uS uT uA u₄ variable {R : Type uR} [Semiring R] diff --git a/Mathlib/AlgebraicTopology/SimplicialObject.lean b/Mathlib/AlgebraicTopology/SimplicialObject.lean index f40b72872e2fd..a8871aa1b57e4 100644 --- a/Mathlib/AlgebraicTopology/SimplicialObject.lean +++ b/Mathlib/AlgebraicTopology/SimplicialObject.lean @@ -21,9 +21,6 @@ Use the notation `X _[n]` in the `Simplicial` locale to obtain the `n`-th term o -/ -set_option autoImplicit true - - open Opposite open CategoryTheory @@ -233,7 +230,7 @@ def Truncated (n : ℕ) := (SimplexCategory.Truncated n)ᵒᵖ ⥤ C #align category_theory.simplicial_object.truncated CategoryTheory.SimplicialObject.Truncated -instance : Category (Truncated C n) := by +instance {n : ℕ} : Category (Truncated C n) := by dsimp [Truncated] infer_instance @@ -605,7 +602,7 @@ def Truncated (n : ℕ) := SimplexCategory.Truncated n ⥤ C #align category_theory.cosimplicial_object.truncated CategoryTheory.CosimplicialObject.Truncated -instance : Category (Truncated C n) := by +instance {n : ℕ} : Category (Truncated C n) := by dsimp [Truncated] infer_instance diff --git a/Mathlib/AlgebraicTopology/SimplicialSet.lean b/Mathlib/AlgebraicTopology/SimplicialSet.lean index 20e62a14e4310..fc86f81f34ff5 100644 --- a/Mathlib/AlgebraicTopology/SimplicialSet.lean +++ b/Mathlib/AlgebraicTopology/SimplicialSet.lean @@ -33,9 +33,6 @@ from a non-surjective order preserving function `Fin n → Fin n` a morphism `Δ[n] ⟶ ∂Δ[n]`. -/ -set_option autoImplicit true - - universe v u open CategoryTheory CategoryTheory.Limits @@ -352,18 +349,19 @@ instance Truncated.largeCategory (n : ℕ) : LargeCategory (Truncated n) := by dsimp only [Truncated] infer_instance -instance Truncated.hasLimits : HasLimits (Truncated n) := by +instance Truncated.hasLimits {n : ℕ} : HasLimits (Truncated n) := by dsimp only [Truncated] infer_instance -instance Truncated.hasColimits : HasColimits (Truncated n) := by +instance Truncated.hasColimits {n : ℕ} : HasColimits (Truncated n) := by dsimp only [Truncated] infer_instance -- Porting note (#10756): added an `ext` lemma. -- See https://github.com/leanprover-community/mathlib4/issues/5229 @[ext] -lemma Truncated.hom_ext {X Y : Truncated n} {f g : X ⟶ Y} (w : ∀ n, f.app n = g.app n) : f = g := +lemma Truncated.hom_ext {n : ℕ} {X Y : Truncated n} {f g : X ⟶ Y} (w : ∀ n, f.app n = g.app n) : + f = g := NatTrans.ext _ _ (funext w) /-- The skeleton functor on simplicial sets. -/ diff --git a/Mathlib/CategoryTheory/ConnectedComponents.lean b/Mathlib/CategoryTheory/ConnectedComponents.lean index d172cef4a5da0..eee2578219132 100644 --- a/Mathlib/CategoryTheory/ConnectedComponents.lean +++ b/Mathlib/CategoryTheory/ConnectedComponents.lean @@ -22,9 +22,6 @@ particular `Decomposed J` is the category (definitionally) given by the sigma-ty components of `J`, and it is shown that this is equivalent to `J`. -/ -set_option autoImplicit true - - universe v₁ v₂ v₃ u₁ u₂ noncomputable section @@ -52,6 +49,7 @@ def Component (j : ConnectedComponents J) : Type u₁ := FullSubcategory fun k => Quotient.mk'' k = j #align category_theory.component CategoryTheory.Component +set_option autoImplicit true in instance : Category (Component (j : ConnectedComponents J)) := FullSubcategory.category _ @@ -62,9 +60,11 @@ def Component.ι (j : ConnectedComponents J) : Component j ⥤ J := fullSubcategoryInclusion _ #align category_theory.component.ι CategoryTheory.Component.ι +set_option autoImplicit true in instance : Full (Component.ι (j : ConnectedComponents J)) := FullSubcategory.full _ +set_option autoImplicit true in instance : Faithful (Component.ι (j : ConnectedComponents J)) := FullSubcategory.faithful _ diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean index 4f5dc5f2ad7f6..d92119017771c 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean @@ -15,10 +15,9 @@ import Mathlib.Combinatorics.SimpleGraph.Connectivity -/ -set_option autoImplicit true - namespace SimpleGraph +universe u v variable {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} namespace Subgraph @@ -156,7 +155,8 @@ end Subgraph section induced_subgraphs -lemma connected_induce_iff : (G.induce s).Connected ↔ ((⊤ : G.Subgraph).induce s).Connected := by +lemma connected_induce_iff {s : Set V} : + (G.induce s).Connected ↔ ((⊤ : G.Subgraph).induce s).Connected := by rw [induce_eq_coe_induce_top, ← Subgraph.connected_iff'] lemma induce_union_connected {s t : Set V} @@ -181,7 +181,7 @@ lemma Walk.connected_induce_support {u v : V} (p : G.Walk u v) : rw [← p.verts_toSubgraph] exact p.toSubgraph_connected.induce_verts -lemma induce_connected_adj_union {s t : Set V} +lemma induce_connected_adj_union {v w : V} {s t : Set V} (sconn : (G.induce s).Connected) (tconn : (G.induce t).Connected) (hv : v ∈ s) (hw : w ∈ t) (ha : G.Adj v w) : (G.induce (s ∪ t)).Connected := by diff --git a/Mathlib/Combinatorics/SimpleGraph/Subgraph.lean b/Mathlib/Combinatorics/SimpleGraph/Subgraph.lean index 1fed4e2289507..a6a04e55a241b 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Subgraph.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Subgraph.lean @@ -901,8 +901,7 @@ theorem edgeSet_subgraphOfAdj {v w : V} (hvw : G.Adj v w) : forall₂_true_iff] #align simple_graph.edge_set_subgraph_of_adj SimpleGraph.edgeSet_subgraphOfAdj -set_option autoImplicit true in -lemma subgraphOfAdj_le_of_adj (H : G.Subgraph) (h : H.Adj v w) : +lemma subgraphOfAdj_le_of_adj {v w : V} (H : G.Subgraph) (h : H.Adj v w) : G.subgraphOfAdj (H.adj_sub h) ≤ H := by constructor · intro x diff --git a/Mathlib/Computability/NFA.lean b/Mathlib/Computability/NFA.lean index 476abfdf187e3..7bed580983b5b 100644 --- a/Mathlib/Computability/NFA.lean +++ b/Mathlib/Computability/NFA.lean @@ -19,9 +19,6 @@ Note that this definition allows for Automaton with infinite states; a `Fintype` supplied for true NFA's. -/ -set_option autoImplicit true - - open Set open Computability @@ -108,7 +105,8 @@ theorem eval_append_singleton (x : List α) (a : α) : M.eval (x ++ [a]) = M.ste def accepts : Language α := {x | ∃ S ∈ M.accept, S ∈ M.eval x} #align NFA.accepts NFA.accepts -theorem mem_accepts : x ∈ M.accepts ↔ ∃ S ∈ M.accept, S ∈ M.evalFrom M.start x := by rfl +theorem mem_accepts {x : List α} : x ∈ M.accepts ↔ ∃ S ∈ M.accept, S ∈ M.evalFrom M.start x := by + rfl /-- `M.toDFA` is a `DFA` constructed from an `NFA` `M` using the subset construction. The states is the type of `Set`s of `M.state` and the step function is `M.stepSet`. -/ diff --git a/Mathlib/Data/Finset/Lattice.lean b/Mathlib/Data/Finset/Lattice.lean index 0c8f1f29c7ce0..0b416027e0ecf 100644 --- a/Mathlib/Data/Finset/Lattice.lean +++ b/Mathlib/Data/Finset/Lattice.lean @@ -17,9 +17,6 @@ import Mathlib.Order.Hom.Lattice # Lattice operations on finsets -/ -set_option autoImplicit true - - variable {F α β γ ι κ : Type*} namespace Finset @@ -1029,7 +1026,8 @@ theorem inf'_le {b : β} (h : b ∈ s) : s.inf' ⟨b, h⟩ f ≤ f b := le_sup' (α := αᵒᵈ) f h #align finset.inf'_le Finset.inf'_le -theorem inf'_le_of_le (hb : b ∈ s) (h : f b ≤ a) : s.inf' ⟨b, hb⟩ f ≤ a := (inf'_le _ hb).trans h +theorem inf'_le_of_le {a : α} {b : β} (hb : b ∈ s) (h : f b ≤ a) : + s.inf' ⟨b, hb⟩ f ≤ a := (inf'_le _ hb).trans h #align finset.inf'_le_of_le Finset.inf'_le_of_le @[simp] diff --git a/Mathlib/Data/Int/Basic.lean b/Mathlib/Data/Int/Basic.lean index f6ab4b5aff4e3..73e7d6cb2e086 100644 --- a/Mathlib/Data/Int/Basic.lean +++ b/Mathlib/Data/Int/Basic.lean @@ -16,8 +16,6 @@ import Mathlib.Order.Monotone.Basic This file contains instances on `ℤ`. The stronger one is `Int.linearOrderedCommRing`. -/ -set_option autoImplicit true - open Nat namespace Int @@ -57,10 +55,10 @@ instance instCommRingInt : CommRing ℤ where intCast_ofNat _ := rfl intCast_negSucc _ := rfl -@[simp, norm_cast] lemma cast_id : Int.cast n = n := rfl +@[simp, norm_cast] lemma cast_id {n : ℤ} : Int.cast n = n := rfl @[simp, norm_cast] -theorem cast_mul [NonAssocRing α] : ∀ m n, ((m * n : ℤ) : α) = m * n := fun m => by +theorem cast_mul {α : Type*} [NonAssocRing α] : ∀ m n, ((m * n : ℤ) : α) = m * n := fun m => by obtain ⟨m, rfl | rfl⟩ := Int.eq_nat_or_neg m · induction m with | zero => simp @@ -70,10 +68,12 @@ theorem cast_mul [NonAssocRing α] : ∀ m n, ((m * n : ℤ) : α) = m * n := fu | succ m ih => simp_all [add_mul] #align int.cast_mul Int.cast_mulₓ -- dubious translation, type involves HasLiftT -lemma cast_Nat_cast [AddGroupWithOne R] : (Int.cast (Nat.cast n) : R) = Nat.cast n := +lemma cast_Nat_cast {n : ℕ} {R : Type*} [AddGroupWithOne R] : + (Int.cast (Nat.cast n) : R) = Nat.cast n := Int.cast_ofNat _ -@[simp, norm_cast] lemma cast_pow [Ring R] (n : ℤ) (m : ℕ) : ↑(n ^ m) = (n ^ m : R) := by +@[simp, norm_cast] lemma cast_pow {R : Type*} [Ring R] (n : ℤ) (m : ℕ) : + ↑(n ^ m) = (n ^ m : R) := by induction' m with m ih <;> simp [_root_.pow_succ, *] #align int.cast_pow Int.cast_pow diff --git a/Mathlib/Order/CompleteLattice.lean b/Mathlib/Order/CompleteLattice.lean index 00051c55e56df..2e6faee193584 100644 --- a/Mathlib/Order/CompleteLattice.lean +++ b/Mathlib/Order/CompleteLattice.lean @@ -45,8 +45,6 @@ In lemma names, * `⨅ i, f i` : `iInf f`, the infimum of the range of `f`. -/ -set_option autoImplicit true - open Function OrderDual Set variable {α β β₂ γ : Type*} {ι ι' : Sort*} {κ : ι → Sort*} {κ' : ι' → Sort*} @@ -1972,6 +1970,8 @@ protected def Function.Injective.completeLattice [Sup α] [Inf α] [SupSet α] [ namespace ULift +universe v + instance supSet [SupSet α] : SupSet (ULift.{v} α) where sSup s := ULift.up (sSup <| ULift.up ⁻¹' s) theorem down_sSup [SupSet α] (s : Set (ULift.{v} α)) : (sSup s).down = sSup (ULift.up ⁻¹' s) := rfl diff --git a/Mathlib/Order/Estimator.lean b/Mathlib/Order/Estimator.lean index 083fc375065ec..c170b3cfb27a5 100644 --- a/Mathlib/Order/Estimator.lean +++ b/Mathlib/Order/Estimator.lean @@ -33,7 +33,6 @@ the exact value. -/ set_option autoImplicit true -set_option relaxedAutoImplicit true /-- Given `[EstimatorData a ε]` diff --git a/Mathlib/Order/Iterate.lean b/Mathlib/Order/Iterate.lean index 634d240497896..a59942b391de3 100644 --- a/Mathlib/Order/Iterate.lean +++ b/Mathlib/Order/Iterate.lean @@ -18,16 +18,13 @@ Current selection of inequalities is motivated by formalization of the rotation a circle homeomorphism. -/ -set_option autoImplicit true - - open Function open Function (Commute) namespace Monotone -variable [Preorder α] {f : α → α} {x y : ℕ → α} +variable {α : Type*} [Preorder α] {f : α → α} {x y : ℕ → α} /-! ### Comparison of two sequences @@ -90,7 +87,7 @@ Then we specialize these two lemmas to the case `β = α`, `h = id`. -/ -variable {g : β → β} {h : β → α} +variable {β : Type*} {g : β → β} {h : β → α} open Function @@ -130,7 +127,7 @@ namespace Function section Preorder -variable [Preorder α] {f : α → α} +variable {α : Type*} [Preorder α] {f : α → α} /-- If $x ≤ f x$ for all $x$ (we write this as `id ≤ f`), then the same is true for any iterate `f^[n]` of `f`. -/ @@ -167,7 +164,7 @@ namespace Commute section Preorder -variable [Preorder α] {f g : α → α} +variable {α : Type*} [Preorder α] {f g : α → α} theorem iterate_le_of_map_le (h : Commute f g) (hf : Monotone f) (hg : Monotone g) {x} (hx : f x ≤ g x) (n : ℕ) : f^[n] x ≤ g^[n] x := by @@ -192,7 +189,7 @@ theorem iterate_pos_lt_of_map_lt' (h : Commute f g) (hf : StrictMono f) (hg : Mo end Preorder -variable [LinearOrder α] {f g : α → α} +variable {α : Type*} [LinearOrder α] {f g : α → α} theorem iterate_pos_lt_iff_map_lt (h : Commute f g) (hf : Monotone f) (hg : StrictMono g) {x n} (hn : 0 < n) : f^[n] x < g^[n] x ↔ f x < g x := by @@ -229,7 +226,7 @@ end Function namespace Monotone -variable [Preorder α] {f : α → α} {x : α} +variable {α : Type*} [Preorder α] {f : α → α} {x : α} /-- If `f` is a monotone map and `x ≤ f x` at some point `x`, then the iterates `f^[n] x` form a monotone sequence. -/ @@ -249,7 +246,7 @@ end Monotone namespace StrictMono -variable [Preorder α] {f : α → α} {x : α} +variable {α : Type*} [Preorder α] {f : α → α} {x : α} /-- If `f` is a strictly monotone map and `x < f x` at some point `x`, then the iterates `f^[n] x` form a strictly monotone sequence. -/ diff --git a/Mathlib/Order/Minimal.lean b/Mathlib/Order/Minimal.lean index f29090420b791..6f00f392ccee4 100644 --- a/Mathlib/Order/Minimal.lean +++ b/Mathlib/Order/Minimal.lean @@ -24,9 +24,6 @@ This file defines minimal and maximal of a set with respect to an arbitrary rela Do we need a `Finset` version? -/ -set_option autoImplicit true - - open Function Set variable {α : Type*} (r r₁ r₂ : α → α → Prop) (s t : Set α) (a b : α) @@ -93,6 +90,8 @@ theorem eq_of_mem_minimals (ha : a ∈ minimals r s) (hb : b ∈ s) (h : r b a) antisymm (ha.2 hb h) h #align eq_of_mem_minimals eq_of_mem_minimals +set_option autoImplicit true + theorem mem_maximals_iff : x ∈ maximals r s ↔ x ∈ s ∧ ∀ ⦃y⦄, y ∈ s → r x y → x = y := by simp only [maximals, Set.mem_sep_iff, and_congr_right_iff] refine' fun _ ↦ ⟨fun h y hys hxy ↦ antisymm hxy (h hys hxy), fun h y hys hxy ↦ _⟩ @@ -144,6 +143,8 @@ theorem minimals_antichain : IsAntichain r (minimals r s) := end IsAntisymm +set_option autoImplicit true + theorem mem_minimals_iff_forall_ssubset_not_mem (s : Set (Set α)) : x ∈ minimals (· ⊆ ·) s ↔ x ∈ s ∧ ∀ ⦃y⦄, y ⊂ x → y ∉ s := mem_minimals_iff_forall_lt_not_mem' (· ⊂ ·) diff --git a/Mathlib/Order/PropInstances.lean b/Mathlib/Order/PropInstances.lean index 8f0b421c9ec3c..e19cada10aac8 100644 --- a/Mathlib/Order/PropInstances.lean +++ b/Mathlib/Order/PropInstances.lean @@ -15,9 +15,6 @@ Instances on `Prop` such as `DistribLattice`, `BoundedOrder`, `LinearOrder`. -/ -set_option autoImplicit true - - /-- Propositions form a distributive lattice. -/ instance Prop.instDistribLattice : DistribLattice Prop where sup := Or @@ -113,6 +110,8 @@ theorem Prop.isCompl_iff {P Q : Prop} : IsCompl P Q ↔ ¬(P ↔ Q) := by -- Porting note: Lean 3 would unfold these for us, but we need to do it manually now section decidable_instances + +universe u variable {α : Type u} instance Prop.decidablePredBot : DecidablePred (⊥ : α → Prop) := fun _ => instDecidableFalse