* script setup and documentation
* fetch mathlib nightly when relevant
* use credentials to access `github.com`
* locate correct git directory, and add prompt
* add confirmation message to setup-dev-scripts
* adding --build-all option

…#850)

* refactor(*): unify group/monoid_action, use standard names, make semimodule extend action

* Rename action to mul_action

* Generalize lemmas. Also, add class for multiplicative action on additive structure

* Add pi-instances

* Dirty hacky fix

* Remove #print and set_option pp.all

* clean up proof, avoid diamonds

* Fix some build issues

* Fix build

* Rename mul_action_add to distrib_mul_action

* Bump up the type class search depth in some places

…hentication

…metimes blocked (#859)

…860)

)

…lly changed branches (#857)

I always found these tactics confusing, but I finally figured out what they do and so I rewrote the docs so that I understand them better.

Reference to a mathlib file which no longer exists has been fixed, and a more user-friendly example of an equivalence relation has been added in a tutorial.

* fix(data/complex/exponential): make complex.exp irreducible

See discussion at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/-T50000.20challenge

Using `ring` (and other tactics) on terms involving `exp` can lead to some unpleasant and unnecessary unfolding.

* refactor(data/complex/exponential): improve trig proofs

* fix build

* fix(algebra/group): prove lemma for comm_semigroup instead of comm_monoid

* feat(topology/order): make nhds irreducible

* move nhds irreducible to topology.basic

…ducible (#1052)

* refactor(topology/metric/gromov_hausdorff): remove linarith calls

* refactor(topology/metric/hausdorff_dist): make hausdorff_dist irreducible

* feat(tactic/ring, tactic/linarith): add reducibility parameter

* fix(tactic/ring): interactive parsing for argument to ring1

* feat(tactic/linarith): better input syntax linarith only [...]

* fix(docs/tactics): fix linarith doc

* feat(topology/opens): continuous.comap : opens Y → opens X

From the perfectoid project.

* Update opens.lean

* feat(tactic/basic): adds `contrapose` tactic

* fix(tactic/push_neg): fix is_prop testing

* Setup error message testing following Rob, add tests for `contrapose`

* refactor(tactic/interactive): move noninteractive success_if_fail_with_msg to tactic/core

)

* chore(ring_theory/algebra): simp-lemmas for alg_hom.to_linear_map

From the perfectoid project.

* Stupid error

* Update src/ring_theory/algebra.lean

Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

* feat(category_theory): limits in CommRing

* by

* rename

* sections

* Update src/category_theory/types.lean

Co-Authored-By: Johannes Hölzl <johannes.hoelzl@gmx.de>

From the perfectoid project.

…pace` (#1072)

I've been using this file and `range_const` doesn't seem to require the spurious `measure_space` instance. `measurable_space` seems to suffice.

Prove that the image of the closure is the closure of the image,
for submonoids/groups/rings.

From the perfectoid project.

* feat(data/nat): various lemmas

* protect a definition

* fixes

* Rob's suggestions

* Mario’s proof

(Working offline, let’s see what Travis says)

* minigolf

* feat(linear_algebra/basic): general_linear_group basics

This patch proves that the general_linear_group (defined as units in the
endomorphism ring) are equivalent to the group of linear equivalences.

* shorten proof of ext

* Add mul_equiv

* Use coe

* Fix stupid error

* doc

* update emb_domain doc string

* typo

* splitting adjunction.lean

* chore(CommRing/adjunctions): refactor proofs

* remove unnecessary assumptions

* add helpful doc-string

* cleanup

* breaking things, haven't finished yet

* deterministic timeout

* unfold_coes to the rescue

* one more int.cast

* yet another int.cast

* Update src/data/mv_polynomial.lean

Co-Authored-By: Johan Commelin <johan@commelin.net>

* Update src/data/mv_polynomial.lean

Co-Authored-By: Johan Commelin <johan@commelin.net>

* WIP

* Fix build

* Fix build

* refactor(set_theory/ordinal): shorten proof of well_ordering_thm§

* Update ordinal.lean

* Update ordinal.lean

* Update ordinal.lean

* Improve readability

* shorten proof

* Shorten proof

* feat(algebra/order_functions): generalize strict_mono.monotone (#1022)

* moving stuff to where it belongs

* removed unecessary import

* Changed to union

* Update src/group_theory/subgroup.lean

Co-Authored-By: Johan Commelin <johan@commelin.net>

* Stylistic changes

* Added authorship

* Moved mem_conjugates_of_set

* Authorship

* Trying fixes

* Putting everything in the right order

* removed import

…ith extra structure on stalks (#1018)

* feat(category_theory/colimits): missing simp lemmas

* feat(category_theory): functor.map_nat_iso

* define `functor.map_nat_iso`, and relate to whiskering
* rename `functor.on_iso` to `functor.map_iso`
* add some missing lemmas about whiskering

* fix(category_theory): presheaves, unbundled and bundled, and pushforwards

* restoring `(opens X)ᵒᵖ`

* various changes from working on stalks

* rename `nbhds` to `open_nhds`

* fix introduced typo

* typo

* compactify a proof

* rename `presheaf` to `presheaf_on_space`

* fix(category_theory): turn `has_limits` classes into structures

* naming instances to avoid collisions

* breaking up instances.topological_spaces

* fixing all the other pi-type typclasses

* fix import

* oops

* fix import

* feat(category_theory): stalks of sheaves

* renaming

* fixes after rebase

* nothing

* yay, got rid of the @s

* attempting a very general version of structured stalks

* missed one

* typo

* WIP

* oops

* the presheaf of continuous functions to ℂ

* restoring eq_to_hom simp lemmas

* removing unnecessary simp lemma

* remove another superfluous lemma

* removing the nat_trans and vcomp notations; use \hom and \gg

* a simpler proposal

* getting rid of vcomp

* fix

* splitting files

* renaming

* probably working again?

* update notation

* remove old lemma

* fix

* comment out unfinished stuff

* cleanup

* use iso_whisker_right instead of map_nat_iso

* proofs magically got easier?

* improve some proofs

* moving instances

* remove crap

* tidy

* minimise imports

* chore(travis): disable the check for minimal imports

* Update src/algebraic_geometry/presheafed_space.lean

Co-Authored-By: semorrison <scott@tqft.net>

* writing `op_induction` tactic, and improving proofs

* squeeze_simping

* cleanup

* rearranging

* cleanup

* cleaning up

* cleaning up

* move

* cleaning up

* structured stalks

* comment

* structured stalks

* more simp lemmas

* formatting

* Update src/category_theory/instances/Top/presheaf_of_functions.lean

Co-Authored-By: Floris van Doorn <fpvdoorn@gmail.com>

* fixes in response to review

* tidy regressions... :-(

* oops

* Update src/algebraic_geometry/presheafed_space.lean

Co-Authored-By: Johan Commelin <johan@commelin.net>

* Update src/algebraic_geometry/presheafed_space.lean

Co-Authored-By: Johan Commelin <johan@commelin.net>

* Update src/algebraic_geometry/presheafed_space.lean

Co-Authored-By: Johan Commelin <johan@commelin.net>

* Update src/category_theory/instances/TopCommRing/basic.lean

Co-Authored-By: Johan Commelin <johan@commelin.net>

* def to lemma

* remove useless lemma

* explicit associator

* broken

* can't get proofs to work...

* remove superfluous imports

* missing headers

* change example

* reverting changes to tidy

* remove presheaf_Z, as it doesn't work at the moment

* fixes

* fixes

* fix

* postponing stuff on structured stalks for a later PR

* coercions

* getting rid of all the `erw`

* omitting some proofs

* deleting more proofs

* convert begin ... end to by

* local

* feat(ring_theory): free_ring and free_comm_ring

* Define isomorphism with mv_polynomial int

* Ring hom free_ring -> free_comm_ring; 1 sorry left

* Coe from free_ring to free_comm_ring is ring_hom

* WIP

* WIP

* WIP

* WIP

* Refactoring a bunch of stuff

* functor.map_equiv

* Fix build

* Fix build

* Make multiset.subsingleton_equiv computable

* Define specific equivs using general machinery

* Fix build

* Remove old commented code

* feat(data/equiv/functor): map_equiv

* fix(data/multiset): remove duplicate setoid instance

* namespace changes

#1002)

* feat(category_theory/iso): missing lemmas

* formatting

* formatting

* almost

* oops

* getting there

* one more

* sleep

* good to go

* fix names

* renaming

* linebreak

* temporary notations

* notations for associator, unitors?

* more notation

* names

* more names

* oops

* renaming, and namespaces

* comment

* fix comment

* remove unnecessary open, formatting

* removing dsimps

* replace with simp lemmas

* fix