Skip to content

Commit

Permalink
chore: fix some Lean-3-isms in comments (#10240)
Browse files Browse the repository at this point in the history
  • Loading branch information
TwoFX authored and atarnoam committed Feb 9, 2024
1 parent 555effe commit daf9969
Show file tree
Hide file tree
Showing 8 changed files with 8 additions and 8 deletions.
2 changes: 1 addition & 1 deletion Mathlib/Algebra/Invertible/Defs.lean
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,7 @@ variables {α : Type*} [Monoid α]
def something_that_needs_inverses (x : α) [Invertible x] := sorry
section
local attribute [instance] invertibleOne
attribute [local instance] invertibleOne
def something_one := something_that_needs_inverses 1
end
```
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Analysis/NormedSpace/MatrixExponential.lean
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@ Lemmas like `exp_add_of_commute` require a canonical norm on the type; while the
sensible choices for the norm of a `Matrix` (`Matrix.normedAddCommGroup`,
`Matrix.frobeniusNormedAddCommGroup`, `Matrix.linftyOpNormedAddCommGroup`), none of them
are canonical. In an application where a particular norm is chosen using
`local attribute [instance]`, then the usual lemmas about `exp` are fine. When choosing a norm is
`attribute [local instance]`, then the usual lemmas about `exp` are fine. When choosing a norm is
undesirable, the results in this file can be used.
In this file, we copy across the lemmas about `exp`, but hide the requirement for a norm inside the
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/CategoryTheory/EqToHom.lean
Original file line number Diff line number Diff line change
Expand Up @@ -300,7 +300,7 @@ end Functor
as we lose the ability to use results that interact with `F`,
e.g. the naturality of a natural transformation.
In some files it may be appropriate to use `local attribute [simp] eqToHom_map`, however.
In some files it may be appropriate to use `attribute [local simp] eqToHom_map`, however.
-/
theorem eqToHom_map (F : C ⥤ D) {X Y : C} (p : X = Y) :
F.map (eqToHom p) = eqToHom (congr_arg F.obj p) := by cases p; simp
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/CategoryTheory/Limits/Pi.lean
Original file line number Diff line number Diff line change
Expand Up @@ -144,7 +144,7 @@ With the addition of
`import CategoryTheory.Limits.Shapes.Types`
we can use:
```
local attribute [instance] hasLimit_of_hasLimit_comp_eval
attribute [local instance] hasLimit_of_hasLimit_comp_eval
example : hasBinaryProducts (I → Type v₁) := ⟨by infer_instance⟩
```
-/
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/CategoryTheory/Types.lean
Original file line number Diff line number Diff line change
Expand Up @@ -396,7 +396,7 @@ instance : SplitEpiCategory (Type u) where
end CategoryTheory

-- We prove `equivIsoIso` and then use that to sneakily construct `equivEquivIso`.
-- (In this order the proofs are handled by `obviously`.)
-- (In this order the proofs are handled by `aesop_cat`.)
/-- Equivalences (between types in the same universe) are the same as (isomorphic to) isomorphisms
of types. -/
@[simps]
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Data/Prod/TProd.lean
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ construction/theorem that is easier to define/prove on binary products than on f
* Then we can use the equivalence `List.TProd.piEquivTProd` below (or enhanced versions of it,
like a `MeasurableEquiv` for product measures) to get the construction on `∀ i : ι, α i`, at
least when assuming `[Fintype ι] [Encodable ι]` (using `Encodable.sortedUniv`).
Using `local attribute [instance] Fintype.toEncodable` we can get rid of the argument
Using `attribute [local instance] Fintype.toEncodable` we can get rid of the argument
`[Encodable ι]`.
## Main definitions
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Logic/Equiv/List.lean
Original file line number Diff line number Diff line change
Expand Up @@ -139,7 +139,7 @@ def _root_.Fintype.truncEncodable (α : Type*) [DecidableEq α] [Fintype α] : T

/-- A noncomputable way to arbitrarily choose an ordering on a finite type.
It is not made into a global instance, since it involves an arbitrary choice.
This can be locally made into an instance with `local attribute [instance] Fintype.toEncodable`. -/
This can be locally made into an instance with `attribute [local instance] Fintype.toEncodable`. -/
noncomputable def _root_.Fintype.toEncodable (α : Type*) [Fintype α] : Encodable α := by
classical exact (Fintype.truncEncodable α).out
#align fintype.to_encodable Fintype.toEncodable
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/RingTheory/Bezout.lean
Original file line number Diff line number Diff line change
Expand Up @@ -95,7 +95,7 @@ end Gcd

attribute [local instance] toGCDDomain

-- Note that the proof depends on the `local attribute [instance]` above, and is thus necessary to
-- Note that the proof depends on the `attribute [local instance]` above, and is thus necessary to
-- be stated.
instance (priority := 100) [IsDomain R] [IsBezout R] : IsIntegrallyClosed R := by
classical exact GCDMonoid.toIsIntegrallyClosed
Expand Down

0 comments on commit daf9969

Please sign in to comment.