Merge branch 'bicategory-coherence-tactic'' into bicategory-adjunction

.docker/gitpod/mathlib/Dockerfile

@@ -19,7 +19,7 @@ RUN curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | s
 RUN . ~/.profile && elan toolchain install $(curl https://raw.githubusercontent.com/leanprover-community/mathlib/master/leanpkg.toml | grep lean_version | awk -F'"' '{print $2}')
 # install `leanproject` using `pip`
 # RUN python3 -m pip install --user mathlibtools
-RUN python3 -m pip install --user pipx && python3 -m pipx ensurepath && source ~/.profile && pipx install mathlibtools==1.1.0
+RUN python3 -m pip install --user pipx && python3 -m pipx ensurepath && source ~/.profile && pipx install mathlibtools==1.1.1
 
 ENV PATH="/home/gitpod/.local/bin:/home/gitpod/.elan/bin:${PATH}"
 

CODE_OF_CONDUCT.md

@@ -126,5 +126,5 @@ enforcement ladder](https://github.com/mozilla/diversity).
 [homepage]: https://www.contributor-covenant.org
 
 For answers to common questions about this code of conduct, see the FAQ at
-https://www.contributor-covenant.org/faq. Translations are available at
-https://www.contributor-covenant.org/translations.
+<https://www.contributor-covenant.org/faq>. Translations are available at
+<https://www.contributor-covenant.org/translations>.

archive/100-theorems-list/82_cubing_a_cube.lean

@@ -7,7 +7,8 @@ import data.fin.tuple
 import data.real.basic
 import data.set.intervals
 import data.set.pairwise
-import set_theory.cardinal
+import set_theory.cardinal.basic
+
 /-!
 Proof that a cube (in dimension n ≥ 3) cannot be cubed:
 There does not exist a partition of a cube into finitely many smaller cubes (at least two)
@@ -509,7 +510,7 @@ omit h
 /-- The infinite sequence of cubes contradicts the finiteness of the family. -/
 theorem not_correct : ¬correct cs :=
 begin
-  intro h, apply not_le_of_lt (lt_omega_iff_fintype.mpr ⟨_inst_1⟩),
+  intro h, apply (lt_omega_of_fintype ι).not_le,
   rw [omega, lift_id], fapply mk_le_of_injective, exact λ n, (sequence_of_cubes h n).1,
   intros n m hnm, apply strict_mono.injective (strict_mono_sequence_of_cubes h),
   dsimp only [decreasing_sequence], rw hnm

archive/100-theorems-list/83_friendship_graphs.lean

@@ -256,7 +256,7 @@ begin
   -- but the trace is 1 mod p when computed the other way
   rw adj_matrix_pow_mod_p_of_regular hG dmod hd hp2,
   dunfold fintype.card at Vmod,
-  simp only [matrix.trace, diag_apply, mul_one, nsmul_eq_mul, linear_map.coe_mk, sum_const],
+  simp only [matrix.trace, matrix.diag, mul_one, nsmul_eq_mul, linear_map.coe_mk, sum_const],
   rw [Vmod, ← nat.cast_one, zmod.nat_coe_zmod_eq_zero_iff_dvd, nat.dvd_one,
     nat.min_fac_eq_one_iff],
   linarith,

archive/imo/imo1960_q1.lean

@@ -73,7 +73,7 @@ begin
   refine ⟨by ring, λ m l p, _⟩,
   obtain ⟨h₁, ⟨m, rfl⟩, h₂⟩ := id p,
   by_cases h : 11 * m < c * 11, { exact H _ h p },
-  have : m = c, {linarith}, subst m,
+  obtain rfl : m = c := by linarith,
   rw [nat.mul_div_cancel_left _ (by norm_num : 11 > 0), mul_comm] at h₂,
   refine (H' h₂).imp _ _; {rintro rfl, norm_num}
 end

archive/imo/imo2008_q3.lean

@@ -7,7 +7,7 @@ import data.real.basic
 import data.real.sqrt
 import data.nat.prime
 import number_theory.primes_congruent_one
-import number_theory.quadratic_reciprocity
+import number_theory.legendre_symbol.quadratic_reciprocity
 import tactic.linear_combination
 
 /-!
@@ -33,7 +33,7 @@ lemma p_lemma (p : ℕ) (hpp : nat.prime p) (hp_mod_4_eq_1 : p ≡ 1 [MOD 4]) (h
 begin
   haveI := fact.mk hpp,
   have hp_mod_4_ne_3 : p % 4 ≠ 3, { linarith [(show p % 4 = 1, by exact hp_mod_4_eq_1)] },
-  obtain ⟨y, hy⟩ := (zmod.exists_sq_eq_neg_one_iff_mod_four_ne_three p).mpr hp_mod_4_ne_3,
+  obtain ⟨y, hy⟩ := (zmod.exists_sq_eq_neg_one_iff p).mpr hp_mod_4_ne_3,
 
   let m := zmod.val_min_abs y,
   let n := int.nat_abs m,
@@ -81,7 +81,7 @@ theorem imo2008_q3 : ∀ N : ℕ, ∃ n : ℕ, n ≥ N ∧
   ∃ p : ℕ, nat.prime p ∧ p ∣ n ^ 2 + 1 ∧ (p : ℝ) > 2 * n + sqrt(2 * n) :=
 begin
   intro N,
-  obtain ⟨p, hpp, hineq₁, hpmod4⟩ := nat.exists_prime_ge_modeq_one 4 (N ^ 2 + 21) zero_lt_four,
+  obtain ⟨p, hpp, hineq₁, hpmod4⟩ := nat.exists_prime_ge_modeq_one (N ^ 2 + 21) zero_lt_four,
   obtain ⟨n, hnat, hreal⟩ := p_lemma p hpp hpmod4 (by linarith [hineq₁, nat.zero_le (N ^ 2)]),
 
   have hineq₂  : n ^ 2 + 1 ≥ p := nat.le_of_dvd (n ^ 2).succ_pos hnat,

docs/overview.yaml

@@ -51,7 +51,7 @@ General algebra:
     ring: 'ring'
     ring morphism: 'ring_hom'
     the category of rings: 'Ring'
-    subring: 'is_subring'
+    subring: 'subring'
     localization: 'localization'
     local ring: 'local_ring'
     noetherian ring: 'is_noetherian_ring'

docs/references.bib

@@ -459,6 +459,14 @@ @Book{            Elephant
   publisher     = {Oxford University Press}
 }
 
+@book{            engel1997,
+  title         = {Sperner theory},
+  author        = {Engel, Konrad},
+  publisher     = {Cambridge University Press},
+  place         = {Cambridge},
+  year          = {1997}
+}
+
 @Article{         erdosrenyisos,
   author        = {P. Erd\"os, A.R\'enyi, and V. S\'os},
   title         = {On a problem of graph theory},
@@ -1426,6 +1434,14 @@ @Book{            soare1987
   doi           = {10.1007/978-3-662-02460-7}
 }
 
+@book{            stanley2012,
+  author        = {Stanley, Richard P.},
+  title         = {Enumerative combinatorics},
+  place         = {Cambridge},
+  publisher     = {Cambridge Univ. Press},
+  year          = {2012}
+}
+
 @Article{         Stone1935,
   author        = {Stone, M. H.},
   year          = {1935},

docs/undergrad.yaml

@@ -124,7 +124,7 @@ Group Theory:
 Ring Theory:
   Fundamentals:
     ring: 'ring'
-    subrings: 'is_subring'
+    subrings: 'subring'
     ring morphisms: 'ring_hom'
     ring structure $\Z$: 'int.comm_ring'
     product of rings: 'pi.ring'
@@ -209,7 +209,7 @@ Bilinear and Quadratic Forms Over a Vector Space:
     Sylvester's law of inertia: 'https://en.wikipedia.org/wiki/Sylvester%27s_law_of_inertia'
     real classification: 'https://en.wikipedia.org/wiki/Sylvester%27s_law_of_inertia'
     complex classification: ''
-    Gram-Schmidt orthogonalisation: 'https://en.wikipedia.org/wiki/Gram%E2%80%93Schmidt_process'
+    Gram-Schmidt orthogonalisation: 'gram_schmidt_orthogonal'
   Euclidean and Hermitian spaces:
     Euclidean vector spaces: 'inner_product_space'
     Hermitian vector spaces: 'inner_product_space'

scripts/nolints.txt

@@ -1,6 +1,11 @@
 import .all
 run_cmd tactic.skip
 
+-- algebra/big_operators/fin.lean
+apply_nolint fin.prod_univ_cast_succ to_additive_doc
+apply_nolint fin.prod_univ_succ to_additive_doc
+apply_nolint fin.prod_univ_succ_above to_additive_doc
+
 -- algebra/category/Group/limits.lean
 apply_nolint CommGroup.category_theory.forget₂.category_theory.creates_limit to_additive_doc
 apply_nolint CommGroup.forget_preserves_limits to_additive_doc
@@ -23,10 +28,7 @@ apply_nolint one_hom.comp_assoc to_additive_doc
 
 -- algebra/order/group.lean
 apply_nolint inv_le_of_inv_le' to_additive_doc
-apply_nolint inv_le_one' to_additive_doc
 apply_nolint inv_lt_of_inv_lt' to_additive_doc
-apply_nolint inv_lt_one' to_additive_doc
-apply_nolint inv_lt_one_iff_one_lt to_additive_doc
 apply_nolint inv_mul_lt_of_lt_mul to_additive_doc
 apply_nolint inv_of_one_lt_inv to_additive_doc
 apply_nolint le_inv_mul_of_mul_le to_additive_doc
@@ -39,27 +41,18 @@ apply_nolint left.one_lt_inv_iff to_additive_doc
 apply_nolint lt_inv_mul_of_mul_lt to_additive_doc
 apply_nolint lt_inv_of_lt_inv to_additive_doc
 apply_nolint lt_mul_of_inv_mul_lt to_additive_doc
-apply_nolint lt_mul_of_inv_mul_lt_left to_additive_doc
 apply_nolint lt_of_inv_lt_inv to_additive_doc
 apply_nolint mul_le_of_le_inv_mul to_additive_doc
 apply_nolint mul_lt_of_lt_inv_mul to_additive_doc
-apply_nolint one_le_inv' to_additive_doc
 apply_nolint one_le_of_inv_le_one to_additive_doc
-apply_nolint one_lt_inv' to_additive_doc
 apply_nolint one_lt_inv_of_inv to_additive_doc
 apply_nolint one_lt_of_inv_lt_one to_additive_doc
-apply_nolint ordered_comm_group.le_of_mul_le_mul_left to_additive_doc
-apply_nolint ordered_comm_group.lt_of_mul_lt_mul_left to_additive_doc
-apply_nolint ordered_comm_group.mul_lt_mul_left' to_additive_doc
 apply_nolint right.inv_le_one_iff to_additive_doc
 apply_nolint right.one_le_inv_iff to_additive_doc
 
 -- algebra/order/lattice_group.lean
 apply_nolint lattice_ordered_comm_group.mabs_mul_le to_additive_doc
 
--- algebra/order/monoid_lemmas.lean
-apply_nolint mul_le_one' to_additive_doc
-
 -- category_theory/limits/filtered_colimit_commutes_finite_limit.lean
 apply_nolint category_theory.limits.colimit_limit_to_limit_colimit_is_iso fails_quickly
 
@@ -128,7 +121,7 @@ apply_nolint traversable.mfoldr doc_blame
 
 -- control/monad/cont.lean
 apply_nolint cont doc_blame
-apply_nolint cont_t doc_blame has_inhabited_instance
+apply_nolint cont_t has_inhabited_instance doc_blame
 apply_nolint cont_t.map doc_blame
 apply_nolint cont_t.monad_lift doc_blame
 apply_nolint cont_t.run doc_blame
@@ -138,7 +131,7 @@ apply_nolint except_t.mk_label doc_blame
 apply_nolint is_lawful_monad_cont doc_blame
 apply_nolint monad_cont doc_blame
 apply_nolint monad_cont.goto doc_blame
-apply_nolint monad_cont.label doc_blame has_inhabited_instance
+apply_nolint monad_cont.label has_inhabited_instance doc_blame
 apply_nolint option_t.call_cc doc_blame
 apply_nolint option_t.mk_label doc_blame
 apply_nolint reader_t.call_cc doc_blame
@@ -154,7 +147,7 @@ apply_nolint except_t.pass_aux doc_blame
 apply_nolint option_t.pass_aux doc_blame
 apply_nolint swap_right doc_blame
 apply_nolint writer doc_blame
-apply_nolint writer_t doc_blame has_inhabited_instance
+apply_nolint writer_t has_inhabited_instance doc_blame
 apply_nolint writer_t.adapt doc_blame
 apply_nolint writer_t.bind doc_blame
 apply_nolint writer_t.ext unused_arguments
@@ -198,7 +191,7 @@ apply_nolint filter.realizer has_inhabited_instance
 apply_nolint filter.realizer.of_eq doc_blame
 
 -- data/analysis/topology.lean
-apply_nolint compact.realizer doc_blame unused_arguments has_inhabited_instance
+apply_nolint compact.realizer has_inhabited_instance doc_blame unused_arguments
 apply_nolint ctop has_inhabited_instance
 apply_nolint ctop.realizer has_inhabited_instance
 apply_nolint ctop.realizer.id doc_blame
@@ -207,16 +200,13 @@ apply_nolint ctop.realizer.nhds_F unused_arguments
 apply_nolint ctop.realizer.nhds_σ unused_arguments
 apply_nolint ctop.realizer.of_equiv doc_blame
 apply_nolint ctop.to_realizer doc_blame
-apply_nolint locally_finite.realizer doc_blame has_inhabited_instance
+apply_nolint locally_finite.realizer has_inhabited_instance doc_blame
 
 -- data/finset/noncomm_prod.lean
 apply_nolint finset.noncomm_prod_union_of_disjoint to_additive_doc
 
 -- data/fintype/card.lean
-apply_nolint fin.prod_univ_cast_succ to_additive_doc
 apply_nolint fin.prod_univ_eq_prod_range to_additive_doc
-apply_nolint fin.prod_univ_succ to_additive_doc
-apply_nolint fin.prod_univ_succ_above to_additive_doc
 
 -- data/fp/basic.lean
 apply_nolint fp.div_nat_lt_two_pow doc_blame unused_arguments
@@ -452,12 +442,6 @@ apply_nolint is_subfield doc_blame
 -- deprecated/subring.lean
 apply_nolint ring.closure doc_blame
 
--- field_theory/finite/polynomial.lean
-apply_nolint mv_polynomial.R doc_blame unused_arguments
-apply_nolint mv_polynomial.evalᵢ doc_blame
-apply_nolint mv_polynomial.evalₗ doc_blame unused_arguments
-apply_nolint mv_polynomial.indicator doc_blame
-
 -- group_theory/coset.lean
 apply_nolint subgroup.card_subgroup_dvd_card to_additive_doc
 
@@ -480,17 +464,15 @@ apply_nolint left_cancel_monoid.to_has_faithful_opposite_scalar to_additive_doc
 apply_nolint monoid.to_opposite_mul_action to_additive_doc
 
 -- group_theory/group_action/pi.lean
+apply_nolint function.has_scalar to_additive_doc
+apply_nolint function.smul_comm_class to_additive_doc
 apply_nolint pi.has_faithful_scalar_at to_additive_doc
 
 -- group_theory/group_action/sub_mul_action.lean
 apply_nolint sub_mul_action.has_zero fails_quickly
 
--- group_theory/monoid_localization.lean
-apply_nolint submonoid.localization_map.lift_left_inverse to_additive_doc
-
 -- group_theory/order_of_element.lean
 apply_nolint image_range_order_of to_additive_doc
-apply_nolint is_of_fin_order.quotient to_additive_doc
 apply_nolint is_of_fin_order_iff_coe to_additive_doc
 apply_nolint order_of_eq_of_pow_and_pow_div_prime to_additive_doc
 apply_nolint pow_gcd_card_eq_one_iff to_additive_doc
@@ -517,15 +499,6 @@ apply_nolint sylow.fixed_points_mul_left_cosets_equiv_quotient doc_blame
 apply_nolint affine_span.nonempty fails_quickly
 apply_nolint affine_subspace.to_add_torsor fails_quickly
 
--- linear_algebra/pi.lean
-apply_nolint function.has_scalar to_additive_doc
-apply_nolint function.smul_comm_class to_additive_doc
-
--- logic/equiv/list.lean
-apply_nolint encodable.fintype_arrow doc_blame
-apply_nolint encodable.fintype_pi doc_blame
-apply_nolint encodable.trunc_encodable_of_fintype doc_blame
-
 -- logic/relator.lean
 apply_nolint relator.bi_total doc_blame
 apply_nolint relator.bi_unique doc_blame
@@ -535,33 +508,6 @@ apply_nolint relator.lift_fun doc_blame
 apply_nolint relator.right_total doc_blame
 apply_nolint relator.right_unique doc_blame
 
--- measure_theory/constructions/pi.lean
-apply_nolint measure_theory.pi.is_inv_invariant_volume to_additive_doc
-apply_nolint measure_theory.pi.is_mul_left_invariant_volume to_additive_doc
-
--- measure_theory/group/integration.lean
-apply_nolint measure_theory.integral_eq_zero_of_mul_left_eq_neg to_additive_doc
-apply_nolint measure_theory.integral_eq_zero_of_mul_right_eq_neg to_additive_doc
-apply_nolint measure_theory.integral_mul_left_eq_self to_additive_doc
-apply_nolint measure_theory.integral_mul_right_eq_self to_additive_doc
-apply_nolint measure_theory.lintegral_eq_zero_of_is_mul_left_invariant to_additive_doc
-apply_nolint measure_theory.lintegral_mul_left_eq_self to_additive_doc
-apply_nolint measure_theory.lintegral_mul_right_eq_self to_additive_doc
-
--- measure_theory/group/measure.lean
-apply_nolint measure_theory.forall_measure_preimage_mul_iff to_additive_doc
-apply_nolint measure_theory.forall_measure_preimage_mul_right_iff to_additive_doc
-apply_nolint measure_theory.is_mul_left_invariant.is_mul_right_invariant to_additive_doc
-apply_nolint measure_theory.is_open_pos_measure_of_mul_left_invariant_of_compact to_additive_doc
-apply_nolint measure_theory.is_open_pos_measure_of_mul_left_invariant_of_regular to_additive_doc
-apply_nolint measure_theory.measure.is_haar_measure.has_no_atoms to_additive_doc
-apply_nolint measure_theory.measure.is_haar_measure.sigma_finite to_additive_doc
-apply_nolint measure_theory.measure.is_haar_measure_map to_additive_doc
-apply_nolint measure_theory.measure.is_haar_measure_of_is_compact_nonempty_interior to_additive_doc
-apply_nolint measure_theory.measure_lt_top_of_is_compact_of_is_mul_left_invariant to_additive_doc
-apply_nolint measure_theory.measure_lt_top_of_is_compact_of_is_mul_left_invariant' to_additive_doc
-apply_nolint measure_theory.measure_preimage_mul to_additive_doc
-
 -- measure_theory/group/prod.lean
 apply_nolint measure_theory.absolutely_continuous_of_is_mul_left_invariant to_additive_doc
 apply_nolint measure_theory.map_prod_inv_mul_eq to_additive_doc
@@ -609,19 +555,6 @@ apply_nolint tactic.coinductive_predicate doc_blame
 apply_nolint tactic.interactive.coinduction doc_blame
 apply_nolint tactic.mono doc_blame
 
--- number_theory/dioph.lean
-apply_nolint poly has_inhabited_instance
-
--- number_theory/zsqrtd/basic.lean
-apply_nolint zsqrtd.le doc_blame
-apply_nolint zsqrtd.lt doc_blame
-apply_nolint zsqrtd.norm doc_blame
-
--- number_theory/zsqrtd/gaussian_int.lean
-apply_nolint gaussian_int doc_blame
-apply_nolint gaussian_int.div doc_blame
-apply_nolint gaussian_int.mod doc_blame
-
 -- order/filter/at_top_bot.lean
 apply_nolint filter.map_at_top_finset_prod_le_of_prod_eq to_additive_doc
 
@@ -631,24 +564,11 @@ apply_nolint order.ideal.is_prime.is_maximal fails_quickly
 -- ring_theory/witt_vector/basic.lean
 apply_nolint witt_vector.comm_ring check_reducibility
 
--- set_theory/cofinality.lean
-apply_nolint strict_order.cof doc_blame
-
--- set_theory/game.lean
-apply_nolint pgame.inv_ty has_inhabited_instance
-
 -- set_theory/lists.lean
 apply_nolint finsets doc_blame
 
--- set_theory/pgame.lean
-apply_nolint pgame.left_moves has_inhabited_instance
-apply_nolint pgame.relabelling has_inhabited_instance
-apply_nolint pgame.restricted has_inhabited_instance
-apply_nolint pgame.right_moves has_inhabited_instance
-
 -- set_theory/zfc.lean
 apply_nolint Set.map_definable_aux unused_arguments
-apply_nolint pSet.type has_inhabited_instance
 
 -- tactic/abel.lean
 apply_nolint tactic.abel.eval doc_blame

scripts/style-exceptions.txt

@@ -31,7 +31,6 @@ src/deprecated/subfield.lean : line 8 : ERR_MOD : Module docstring missing, or t
 src/deprecated/subring.lean : line 10 : ERR_MOD : Module docstring missing, or too late
 src/logic/relator.lean : line 11 : ERR_MOD : Module docstring missing, or too late
 src/meta/coinductive_predicates.lean : line 8 : ERR_MOD : Module docstring missing, or too late
-src/tactic/algebra.lean : line 8 : ERR_MOD : Module docstring missing, or too late
 src/tactic/apply_fun.lean : line 8 : ERR_MOD : Module docstring missing, or too late
 src/tactic/auto_cases.lean : line 8 : ERR_MOD : Module docstring missing, or too late
 src/tactic/chain.lean : line 8 : ERR_MOD : Module docstring missing, or too late
@@ -45,7 +44,6 @@ src/tactic/ext.lean : line 9 : ERR_MOD : Module docstring missing, or too late
 src/tactic/find.lean : line 8 : ERR_MOD : Module docstring missing, or too late
 src/tactic/hint.lean : line 9 : ERR_MOD : Module docstring missing, or too late
 src/tactic/interactive.lean : line 10 : ERR_MOD : Module docstring missing, or too late
-src/tactic/lint/default.lean : line 12 : ERR_MOD : Module docstring missing, or too late
 src/tactic/local_cache.lean : line 8 : ERR_MOD : Module docstring missing, or too late
 src/tactic/monotonicity/basic.lean : line 8 : ERR_MOD : Module docstring missing, or too late
 src/tactic/monotonicity/interactive.lean : line 11 : ERR_MOD : Module docstring missing, or too late