Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-27 07:09 0d6d0b0f

View on Github →

chore(*): split long lines, unindent in namespaces (#2834) The diff is large but here is the word diff (search for [- or [+):

$ git diff --word-diff=plain --ignore-all-space master | grep '(^---|\[-|\[\+)'
--- a/src/algebra/big_operators.lean
[-λ l, @is_group_anti_hom.map_prod _ _ _ _ _ inv_is_group_anti_hom l-]-- TODO there is probably a cleaner proof of this
        { have : [-(to_finset s).sum (λx,-]{+∑ x in s.to_finset,+} ite (x = a) 1 [-0)-]{+0+} = [-({a} : finset α).sum (λx,-]{+∑ x in {a},+} ite (x = a) 1 [-0),-]
[-          { apply (finset.sum_subset _ _).symm,-]{+0,+}
          { [-intros _ H, rwa mem_singleton.1 H },-]
[-            { exact λ _ _ H, if_neg (mt finset.mem_singleton.2 H) }-]{+rw [finset.sum_ite_eq', if_pos h, finset.sum_singleton, if_pos rfl],+} },
--- a/src/algebra/category/Group/basic.lean
[-a-]{+an+} `add_equiv` between `add_group`s."]
--- a/src/algebra/category/Group/colimits.lean
--- a/src/algebra/category/Mon/basic.lean
[-a-]{+an+} `add_equiv` between `add_monoid`s."]
[-a-]{+an+} `add_equiv` between `add_comm_monoid`s."]
--- a/src/algebra/free.lean
--- a/src/algebra/group/units.lean
--- a/src/algebra/group/units_hom.lean
--- a/src/category_theory/category/default.lean
[-universes v u-]-- The order in this declaration matters: v often needs to be explicitly specified while u often
--- a/src/control/monad/cont.lean
    simp [-[call_cc,except_t.call_cc,call_cc_bind_right,except_t.goto_mk_label,map_eq_bind_pure_comp,bind_assoc,@call_cc_bind_left-]{+[call_cc,except_t.call_cc,call_cc_bind_right,except_t.goto_mk_label,map_eq_bind_pure_comp,+}
  call_cc_bind_left  := by { intros, simp [-[call_cc,option_t.call_cc,call_cc_bind_right,option_t.goto_mk_label,map_eq_bind_pure_comp,bind_assoc,@call_cc_bind_left-]{+[call_cc,option_t.call_cc,call_cc_bind_right,+}
  call_cc_bind_left  := by { intros, simp [-[call_cc,state_t.call_cc,call_cc_bind_left,(>>=),state_t.bind,state_t.goto_mk_label],-]{+[call_cc,state_t.call_cc,call_cc_bind_left,(>>=),+}
  call_cc_dummy := by { intros, simp [-[call_cc,state_t.call_cc,call_cc_bind_right,(>>=),state_t.bind,@call_cc_dummy-]{+[call_cc,state_t.call_cc,call_cc_bind_right,(>>=),+}
  call_cc_bind_left  := by { intros, simp [-[call_cc,reader_t.call_cc,call_cc_bind_left,reader_t.goto_mk_label],-]{+[call_cc,reader_t.call_cc,call_cc_bind_left,+}
--- a/src/control/monad/writer.lean
--- a/src/control/traversable/basic.lean
   online at <http://arxiv.org/pdf/1202.2919>[-Synopsis-]
--- a/src/data/analysis/filter.lean
--- a/src/data/equiv/basic.lean
--- a/src/data/fin.lean
--- a/src/data/finset.lean
  [-by-]{+{+} rw [-[eq],-]{+[eq] },+}
--- a/src/data/hash_map.lean
--- a/src/data/int/basic.lean
--- a/src/data/list/basic.lean
--- a/src/data/list/tfae.lean
--- a/src/data/num/lemmas.lean
[-Properties of the binary representation of integers.-]
--- a/src/data/zsqrtd/basic.lean
--- a/src/group_theory/congruence.lean
with [-a-]{+an+} addition."]
@[to_additive Sup_eq_add_con_gen "The supremum of a set of additive congruence relations [-S-]{+`S`+} equals
--- a/src/group_theory/monoid_localization.lean
--- a/src/group_theory/submonoid.lean
--- a/src/number_theory/dioph.lean
--- a/src/set_theory/ordinal.lean
--- a/src/tactic/apply.lean
--- a/src/tactic/lean_core_docs.lean
--- a/src/tactic/lint/type_classes.lean
--- a/src/tactic/omega/main.lean
--- a/test/coinductive.lean
--- a/test/localized/import3.lean
--- a/test/norm_num.lean
--- a/test/tidy.lean
--- a/test/where.lean

P.S.: I don't know how to make git diff hide all non-interesting chunks.

Estimated changes

modified theorem free_magma.map_mul'
modified theorem free_magma.mul_bind
modified theorem free_magma.mul_map_seq
modified theorem free_magma.mul_seq
modified theorem free_magma.traverse_mul'
modified theorem free_magma.traverse_mul
modified theorem free_semigroup.map_mul'
modified theorem free_semigroup.map_pure
modified theorem free_semigroup.mul_bind
modified theorem free_semigroup.mul_map_seq
modified theorem free_semigroup.mul_seq
modified theorem free_semigroup.pure_seq
modified theorem free_semigroup.traverse_mul
modified theorem list.all_cons
modified theorem list.any_cons
modified theorem list.append_inj'
modified theorem list.append_inj
modified theorem list.append_inj_left'
modified theorem list.append_inj_left
modified theorem list.append_inj_right'
modified theorem list.append_inj_right
modified theorem list.count_erase_of_ne
modified theorem list.count_erase_self
modified theorem list.eq_of_mem_map_const
modified theorem list.erase_cons
modified theorem list.erase_cons_tail
modified theorem list.erasep_append_right
modified theorem list.erasep_cons
modified theorem list.erasep_cons_of_neg
modified theorem list.exists_of_mem_bind
modified theorem list.ext_le
modified theorem list.filter_false
modified theorem list.filter_true
modified theorem list.foldl1_eq_foldr1
modified theorem list.foldl_eq_foldr'
modified theorem list.foldl_eq_foldr
modified theorem list.foldl_eq_of_comm'
modified theorem list.foldl_reverse
modified theorem list.foldr_eq_of_comm'
modified theorem list.foldr_reverse
modified theorem list.head_append
modified theorem list.head_mul_tail_prod'
modified theorem list.index_of_cons
modified theorem list.index_of_nth
modified theorem list.index_of_nth_le
modified theorem list.length_bind
modified theorem list.length_erase_of_mem
modified theorem list.mem_bind
modified theorem list.mem_bind_of_mem
modified theorem list.nth_le_reverse_aux1
modified theorem list.suffix_iff_eq_append
modified def int.of_snum
modified theorem num.add_of_nat
modified theorem num.add_one
modified theorem num.add_succ
modified theorem num.add_to_nat
modified theorem num.add_to_znum
modified theorem num.add_zero
modified theorem num.bit0_of_bit0
modified theorem num.bit1_of_bit1
modified theorem num.bit_to_nat
modified theorem num.bitwise_to_nat
modified theorem num.cast_add
modified theorem num.cast_bit0
modified theorem num.cast_bit1
modified theorem num.cast_inj
modified theorem num.cast_le
modified theorem num.cast_lt
modified theorem num.cast_mul
modified theorem num.cast_of_znum
modified theorem num.cast_one
modified theorem num.cast_pos
modified theorem num.cast_sub'
modified theorem num.cast_succ'
modified theorem num.cast_succ
modified theorem num.cast_to_int
modified theorem num.cast_to_nat
modified theorem num.cast_to_znum
modified theorem num.cast_to_znum_neg
modified theorem num.cast_zero'
modified theorem num.cast_zero
modified theorem num.cmp_eq
modified theorem num.cmp_swap
modified theorem num.cmp_to_nat
modified theorem num.div_to_nat
modified theorem num.dvd_iff_mod_eq_zero
modified theorem num.dvd_to_nat
modified theorem num.gcd_to_nat
modified theorem num.gcd_to_nat_aux
modified theorem num.land_to_nat
modified theorem num.ldiff_to_nat
modified theorem num.le_iff_cmp
modified theorem num.le_to_nat
modified theorem num.lor_to_nat
modified theorem num.lt_iff_cmp
modified theorem num.lt_to_nat
modified theorem num.lxor_to_nat
modified theorem num.mem_of_znum'
modified theorem num.mod_to_nat
modified theorem num.mul_to_nat
modified theorem num.nat_size_to_nat
modified theorem num.of_nat'_eq
modified theorem num.of_nat_cast
modified theorem num.of_nat_inj
modified theorem num.of_nat_to_znum
modified theorem num.of_nat_to_znum_neg
modified theorem num.of_to_nat
modified theorem num.of_znum'_to_nat
modified theorem num.of_znum_to_nat
modified theorem num.ppred_to_nat
modified theorem num.pred_to_nat
modified theorem num.shiftl_to_nat
modified theorem num.shiftr_to_nat
modified theorem num.size_eq_nat_size
modified theorem num.size_to_nat
modified theorem num.sub_to_nat
modified theorem num.succ'_to_nat
modified theorem num.succ_to_nat
modified theorem num.test_bit_to_nat
modified theorem num.to_nat_inj
modified theorem num.to_nat_to_int
modified theorem num.to_of_nat
modified theorem num.to_znum_inj
modified theorem num.zero_add
modified theorem num.zneg_to_znum
modified theorem num.zneg_to_znum_neg
modified theorem pos_num.add_one
modified theorem pos_num.add_succ
modified theorem pos_num.add_to_nat
modified theorem pos_num.bit0_of_bit0
modified theorem pos_num.bit1_of_bit1
modified theorem pos_num.bit_to_nat
modified theorem pos_num.cast_add
modified theorem pos_num.cast_bit0
modified theorem pos_num.cast_bit1
modified theorem pos_num.cast_inj
modified theorem pos_num.cast_le
modified theorem pos_num.cast_lt
modified theorem pos_num.cast_mul
modified theorem pos_num.cast_one'
modified theorem pos_num.cast_one
modified theorem pos_num.cast_pos
modified theorem pos_num.cast_sub'
modified theorem pos_num.cast_succ
modified theorem pos_num.cast_to_int
modified theorem pos_num.cast_to_nat
modified theorem pos_num.cast_to_num
modified theorem pos_num.cast_to_znum
modified theorem pos_num.cmp_eq
modified theorem pos_num.cmp_swap
modified theorem pos_num.cmp_to_nat
modified theorem pos_num.cmp_to_nat_lemma
modified theorem pos_num.div'_to_nat
modified theorem pos_num.divmod_to_nat
modified theorem pos_num.divmod_to_nat_aux
modified theorem pos_num.le_iff_cmp
modified theorem pos_num.le_to_nat
modified theorem pos_num.lt_iff_cmp
modified theorem pos_num.lt_to_nat
modified theorem pos_num.mod'_to_nat
modified theorem pos_num.mul_to_nat
modified theorem pos_num.nat_size_pos
modified theorem pos_num.nat_size_to_nat
modified theorem pos_num.of_to_nat
modified theorem pos_num.one_add
modified theorem pos_num.one_le_cast
modified theorem pos_num.one_sub'
modified theorem pos_num.pred'_succ'
modified theorem pos_num.pred'_to_nat
modified theorem pos_num.pred_to_nat
modified theorem pos_num.size_eq_nat_size
modified theorem pos_num.size_to_nat
modified theorem pos_num.sub'_one
modified theorem pos_num.succ'_pred'
modified theorem pos_num.succ_to_nat
modified theorem pos_num.to_int_eq_succ_pred
modified theorem pos_num.to_nat_eq_succ_pred
modified theorem pos_num.to_nat_inj
modified theorem pos_num.to_nat_pos
modified theorem pos_num.to_nat_to_int
modified theorem znum.abs_to_nat
modified theorem znum.abs_to_znum
modified theorem znum.add_one
modified theorem znum.add_zero
modified theorem znum.bit0_of_bit0
modified theorem znum.bit1_of_bit1
modified theorem znum.cast_add
modified theorem znum.cast_bit0
modified theorem znum.cast_bit1
modified theorem znum.cast_bitm1
modified theorem znum.cast_inj
modified theorem znum.cast_le
modified theorem znum.cast_lt
modified theorem znum.cast_mul
modified theorem znum.cast_neg
modified theorem znum.cast_one
modified theorem znum.cast_pos
modified theorem znum.cast_succ
modified theorem znum.cast_to_int
modified theorem znum.cast_zero'
modified theorem znum.cast_zero
modified theorem znum.cast_zneg
modified theorem znum.cmp_to_int
modified theorem znum.div_to_int
modified theorem znum.dvd_iff_mod_eq_zero
modified theorem znum.dvd_to_int
modified theorem znum.gcd_to_nat
modified theorem znum.le_to_int
modified theorem znum.lt_to_int
modified theorem znum.mod_to_int
modified theorem znum.mul_to_int
modified theorem znum.neg_of_int
modified theorem znum.neg_zero
modified theorem znum.of_int'_eq
modified theorem znum.of_int_cast
modified theorem znum.of_nat_cast
modified theorem znum.of_to_int
modified theorem znum.to_int_inj
modified theorem znum.to_of_int
modified theorem znum.zero_add
modified theorem znum.zneg_bit1
modified theorem znum.zneg_bitm1
modified theorem znum.zneg_neg
modified theorem znum.zneg_pos
modified theorem znum.zneg_pred
modified theorem znum.zneg_succ
modified theorem znum.zneg_zneg
modified def zsqrtd.add
modified theorem zsqrtd.add_def
modified theorem zsqrtd.add_im
modified theorem zsqrtd.add_re
modified theorem zsqrtd.bit0_im
modified theorem zsqrtd.bit0_re
modified theorem zsqrtd.bit1_im
modified theorem zsqrtd.bit1_re
modified theorem zsqrtd.coe_int_im
modified theorem zsqrtd.coe_int_re
modified theorem zsqrtd.coe_int_val
modified theorem zsqrtd.coe_nat_im
modified theorem zsqrtd.coe_nat_re
modified theorem zsqrtd.coe_nat_val
modified def zsqrtd.conj
modified theorem zsqrtd.conj_im
modified theorem zsqrtd.conj_mul
modified theorem zsqrtd.conj_re
modified theorem zsqrtd.d_pos
modified theorem zsqrtd.decompose
modified theorem zsqrtd.divides_sq_eq_zero
modified theorem zsqrtd.divides_sq_eq_zero_z
modified theorem zsqrtd.ext
modified theorem zsqrtd.le_antisymm
modified theorem zsqrtd.le_arch
modified theorem zsqrtd.le_of_le_le
modified theorem zsqrtd.le_refl
modified def zsqrtd.mul
modified theorem zsqrtd.mul_conj
modified theorem zsqrtd.mul_im
modified theorem zsqrtd.mul_re
modified theorem zsqrtd.muld_val
modified def zsqrtd.neg
modified theorem zsqrtd.neg_im
modified theorem zsqrtd.neg_re
modified def zsqrtd.nonneg
modified theorem zsqrtd.nonneg_add
modified theorem zsqrtd.nonneg_add_lem
modified theorem zsqrtd.nonneg_antisymm
modified theorem zsqrtd.nonneg_cases
modified theorem zsqrtd.nonneg_iff_zero_le
modified theorem zsqrtd.nonneg_mul
modified theorem zsqrtd.nonneg_mul_lem
modified theorem zsqrtd.nonneg_muld
modified theorem zsqrtd.nonneg_smul
modified def zsqrtd.nonnegg
modified theorem zsqrtd.nonnegg_cases_left
modified theorem zsqrtd.nonnegg_cases_right
modified theorem zsqrtd.nonnegg_comm
modified theorem zsqrtd.nonnegg_neg_pos
modified theorem zsqrtd.nonnegg_pos_neg
modified theorem zsqrtd.not_divides_square
modified theorem zsqrtd.not_sq_le_succ
modified def zsqrtd.of_int
modified theorem zsqrtd.of_int_eq_coe
modified theorem zsqrtd.of_int_im
modified theorem zsqrtd.of_int_re
modified def zsqrtd.one
modified theorem zsqrtd.one_im
modified theorem zsqrtd.one_re
modified theorem zsqrtd.smul_val
modified theorem zsqrtd.smuld_val
modified def zsqrtd.sq_le
modified theorem zsqrtd.sq_le_add
modified theorem zsqrtd.sq_le_add_mixed
modified theorem zsqrtd.sq_le_cancel
modified theorem zsqrtd.sq_le_mul
modified theorem zsqrtd.sq_le_of_le
modified theorem zsqrtd.sq_le_smul
modified def zsqrtd.sqrtd
modified theorem zsqrtd.sqrtd_im
modified theorem zsqrtd.sqrtd_re
modified def zsqrtd.zero
modified theorem zsqrtd.zero_im
modified theorem zsqrtd.zero_re
modified theorem dioph.abs_poly_dioph
modified theorem dioph.add_dioph
modified theorem dioph.and_dioph
modified theorem dioph.const_dioph
modified theorem dioph.dioph_comp2
modified theorem dioph.dioph_comp
modified def dioph.dioph_fn
modified theorem dioph.dioph_fn_comp1
modified theorem dioph.dioph_fn_comp2
modified theorem dioph.dioph_fn_comp
modified theorem dioph.dioph_fn_compn
modified theorem dioph.dioph_fn_iff_pfun
modified theorem dioph.dioph_fn_vec
modified theorem dioph.dioph_fn_vec_comp1
modified theorem dioph.dioph_list_all
modified def dioph.dioph_pfun
modified theorem dioph.dioph_pfun_comp1
modified theorem dioph.dioph_pfun_vec
modified theorem dioph.div_dioph
modified theorem dioph.dom_dioph
modified theorem dioph.dvd_dioph
modified theorem dioph.eq_dioph
modified theorem dioph.ex1_dioph
modified theorem dioph.ex_dioph
modified theorem dioph.ext
modified theorem dioph.inject_dummies
modified theorem dioph.inject_dummies_lem
modified theorem dioph.le_dioph
modified theorem dioph.lt_dioph
modified theorem dioph.mod_dioph
modified theorem dioph.modeq_dioph
modified theorem dioph.mul_dioph
modified theorem dioph.ne_dioph
modified theorem dioph.of_no_dummies
modified theorem dioph.or_dioph
modified theorem dioph.pell_dioph
modified theorem dioph.pow_dioph
modified theorem dioph.proj_dioph
modified theorem dioph.proj_dioph_of_nat
modified theorem dioph.reindex_dioph
modified theorem dioph.reindex_dioph_fn
modified theorem dioph.sub_dioph
modified theorem dioph.vec_ex1_dioph
modified theorem dioph.xn_dioph
modified theorem list_all.imp
modified theorem list_all_congr
modified theorem list_all_cons
modified theorem list_all_map
modified theorem vector3.append_insert
modified theorem vector_allp_iff_forall