Commit 2023-05-07 05:02 14167e48

View on Github →

chore: bye-bye, solo bys! (#3825) This PR puts, with one exception, every single remaining by that lies all by itself on its own line to the previous line, thus matching the current behaviour of start-port.sh. The exception is when the by begins the second or later argument to a tuple or anonymous constructor; see https://github.com/leanprover-community/mathlib4/pull/3825#discussion_r1186702599. Essentially this is s/\n *by$/ by/g, but with manual editing to satisfy the linter's max-100-char-line requirement. The Python style linter is also modified to catch these "isolated bys".

Estimated changes

modified theorem neg_vsub_eq_vsub_rev
modified theorem vadd_vsub_assoc
modified theorem vsub_add_vsub_cancel
modified theorem vsub_right_cancel
modified theorem Multiset.pow_card_le_prod
modified theorem Multiset.prod_eq_zero
modified theorem Multiset.prod_le_pow_card
modified theorem Multiset.prod_toList
modified theorem FreeAlgebra.lift_comp_ι
modified theorem geom_sum_mul_neg
modified theorem op_geom_sum₂
modified theorem List.dProdIndex_eq_map_sum
modified theorem SetLike.pow_mem_graded
modified theorem map_div_le_add
modified theorem IsUpperSet.div_left
modified theorem IsUpperSet.div_right
modified theorem IsUpperSet.mul_left
modified theorem IsUpperSet.mul_right
modified theorem IsUpperSet.smul
modified theorem Set.OrdConnected.smul
modified theorem lowerClosure_mul
modified theorem upperClosure_mul
modified theorem Asymptotics.isBigO_one_iff
modified theorem tendsto_zpow_atTop_atTop
modified theorem Convex.linear_preimage
modified theorem convex_iff_pairwise_pos
modified theorem mem_openSegment_iff_div
modified theorem segment_eq_image_lineMap
modified theorem StarConvex.mem_smul
modified theorem StarConvex.union
modified theorem starConvex_iff_div
modified theorem starConvex_iff_forall_pos
modified theorem StrictConvex.add
modified theorem Absorbs.sub
modified theorem dist_inv_inv₀
modified theorem pow_mem_closedBall
modified theorem IsConformalMap.smul
modified theorem Tree.mem_treesOfNumNodesEq
modified theorem Colex.colex_le_of_subset
modified theorem Colex.colex_lt_of_ssubset
modified theorem Down.card_compression
modified theorem Down.compression_idem
modified theorem Down.erase_mem_compression
modified theorem Down.mem_compression
modified theorem Finset.mem_memberSubfamily
modified theorem UV.compress_idem
modified theorem Primrec₂.nat_iff
modified theorem Finset.nodup_toList
modified theorem Finset.one_lt_card_iff
modified theorem Finset.mem_finsupp_iff
modified theorem Finset.image₂_subset
modified theorem Finset.empty_mem_ssubsets
modified theorem Finset.powersetLen_self
modified theorem Finset.powersetLen_zero
modified theorem Finset.diag_card
modified theorem Finset.diag_union
modified theorem Finset.inter_product
modified theorem Finset.product_image_fst
modified theorem Finset.product_image_snd
modified theorem Finset.product_inter
modified theorem Finset.product_singleton
modified theorem Finset.product_union
modified theorem Finset.singleton_product
modified theorem Finset.union_product
modified theorem Finsupp.embDomain_single
modified theorem Finsupp.support_subset_iff
modified theorem Fin.image_succAbove_univ
modified theorem Finset.Nonempty.eq_univ
modified theorem Finset.compl_erase
modified theorem Finset.compl_insert
modified theorem Finset.insert_inj_on'
modified theorem Set.toFinset_compl
modified theorem Set.toFinset_diff
modified theorem Set.toFinset_empty
modified theorem Set.toFinset_inter
modified theorem Set.toFinset_singleton
modified theorem Set.toFinset_symmDiff
modified theorem Set.toFinset_union
modified theorem Fintype.mem_piFinset
modified theorem Nat.cast_int_covby_iff
modified theorem AList.insert_insert
modified theorem Cycle.Nodup.nontrivial_iff
modified theorem Cycle.Subsingleton.nodup
modified theorem Cycle.prev_mem
modified theorem List.mem_of_nextOr_ne
modified theorem List.nextOr_concat
modified theorem List.mem_sublists'
modified theorem Matrix.rank_le_card_height
modified theorem Matrix.rank_le_card_width
modified theorem Multiset.Rel.add
modified theorem Multiset.addHom_ext
modified theorem Multiset.count_inter
modified theorem Multiset.count_sub
modified theorem Multiset.filter_nsmul
modified theorem Multiset.inter_add_distrib
modified theorem Multiset.le_cons_of_not_mem
modified theorem Multiset.le_inter
modified theorem Multiset.map_comp_cons
modified theorem Multiset.map_lt_map
modified theorem Multiset.mem_nsmul
modified theorem Multiset.mem_of_mem_nsmul
modified theorem Multiset.mem_singleton_self
modified theorem Multiset.rel_eq
modified theorem Multiset.singleton_inj
modified theorem Multiset.sub_add_inter
modified theorem Multiset.union_add_inter
modified theorem Multiset.Ico_add_Ico_eq_Ico
modified theorem Multiset.range_add_eq_union
modified theorem Nat.mem_factors_mul_left
modified theorem Nat.Icc_pred_right
modified theorem Nat.Icc_succ_left
modified theorem Nat.Ico_succ_left
modified theorem Nat.Ico_succ_right
modified theorem Nat.Ico_succ_succ
modified theorem Nat.image_Ico_mod
modified theorem Nat.image_sub_const_Ico
modified theorem Nat.mod_injOn_Ico
modified theorem Nat.bit1_mod_bit0
modified theorem PNat.factorMultiset_le_iff'
modified theorem PNat.gcdA'_coe
modified theorem PNat.gcd_eq
modified theorem Polynomial.coeff_derivative
modified theorem Polynomial.derivative_comp
modified theorem Polynomial.hasseDeriv_coeff
modified theorem Polynomial.natDegree_mul
modified theorem Stream'.Seq.corec_eq
modified theorem Stream'.WSeq.LiftRelO.swap
modified def orderIsoIooNegOneOne
modified theorem Sym.exists_eq_cons_of_succ
modified theorem Sym.of_vector_cons
modified theorem Sym2.IsDiag.mem_range_diag
modified theorem Sym2.ball
modified theorem Sym2.congr_left
modified theorem Sym2.congr_right
modified theorem Sym2.eq_swap
modified theorem Sym2.fromRel_bot
modified theorem Sym2.fromRel_top
modified theorem Sym2.map.injective
modified theorem Sym2.map_comp
modified theorem Sym2.map_congr
modified theorem Sym2.mem_and_mem_iff
modified theorem Sym2.mem_map
modified theorem Sym2.mk''_eq_mk''_iff
modified theorem Sym2.mk''_prod_swap_eq
modified theorem Sym2.other_mem'
modified theorem Sym2.other_mem
modified theorem Sym2.other_ne
modified theorem Sym2.other_spec'
modified theorem Sym2.relBool_spec
modified theorem TypeVec.diag_sub_val
modified theorem TypeVec.fst_diag
modified theorem TypeVec.snd_diag
modified theorem Vector.head_map
modified theorem Vector.reverse_reverse
modified theorem Vector.tail_map
modified theorem Vector.toList_singleton
modified theorem ZMod.valMinAbs_mem_Ioc
modified theorem IsGroupHom.inv_ker_one'
modified theorem IsGroupHom.inv_ker_one
modified theorem IsGroupHom.one_ker_inv'
modified theorem IsGroupHom.one_ker_inv
modified theorem PerfectClosure.eq_pthRoot
modified theorem Con.infₛ_def
modified theorem Con.lift_funext
modified theorem Con.sup_eq_conGen
modified theorem Con.supₛ_eq_conGen
modified theorem Doset.eq
modified theorem Doset.left_bot_eq_left_quot
modified theorem MulAction.Supports.smul
modified theorem Subgroup.index_mul_card
modified theorem orderOf_map_dvd
modified theorem Equiv.Perm.cycleOf_apply
modified theorem Finset.exists_cycleOn
modified theorem List.formPerm_eq_one_iff
modified theorem List.formPerm_rotate_one
modified theorem Subgroup.eq_top_of_card_eq
modified theorem Submonoid.powers_eq_closure
modified def AffineSubspace.comap
modified def AffineSubspace.map
modified def AffineSubspace.mk'
modified def affineSpan
modified theorem AlternatingMap.map_add_swap
modified theorem AlternatingMap.map_swap_add
modified theorem Submodule.mem_map_equiv
modified theorem Submodule.subtype_comp_ofLe
modified theorem Lagrange.sum_basis
modified theorem LinearMap.curry_uncurryLeft
modified theorem MultilinearMap.mk_coe
modified theorem Encodable.decode_ge_two
modified theorem Encodable.decode₂_encode
modified theorem Int.coprime_of_sq_sum'
modified theorem supₛ_compact_le_eq
modified theorem disjointed_eq_inf_compl
modified theorem Filter.disjoint_atBot_atTop
modified theorem Filter.pmap_res
modified theorem Acc.sym2_gameAdd
modified theorem Sym2.GameAdd.fst_snd
modified theorem Sym2.GameAdd.snd_fst
modified theorem Filter.liminf_nat_add
modified theorem Submodule.fg_supᵢ
modified theorem Ideal.finsuppTotal_apply
modified theorem Ideal.prod.ext_iff
modified theorem multiplicity.pos_of_dvd
modified theorem Polynomial.primPart_mul
modified theorem pochhammer_succ_right
modified theorem Subsemiring.mem_map
modified theorem Associates.pow_factors
modified theorem Ordinal.cof_eq_infₛ_lsub
modified theorem Ordinal.exists_blsub_cof
modified theorem Ordinal.CNF_fst_le_log
modified theorem Ordinal.div_opow_log_pos
modified theorem Class.classToCong_empty
modified theorem Class.congToClass_empty
modified theorem Class.mem_unionₛ
modified theorem Class.unionₛ_apply
modified theorem ZFSet.Hereditarily.empty
modified theorem ZFSet.choice_mem
modified theorem ZFSet.eq_empty
modified theorem ZFSet.eq_empty_or_nonempty
modified theorem ZFSet.mem_pair
modified theorem ZFSet.mem_union
modified theorem ZFSet.pair_injective
modified theorem ZFSet.pair_mem_prod
modified theorem ZFSet.toSet_insert
modified theorem ZFSet.toSet_inter
modified theorem ZFSet.toSet_range
modified theorem ZFSet.toSet_sdiff
modified theorem ZFSet.toSet_singleton
modified theorem ZFSet.toSet_union
modified theorem Homeomorph.mulRight_symm
modified theorem HasSum.sub
modified theorem DiscreteQuotient.ofLE_ofLE
modified theorem Finset.coe_infsep
modified theorem Set.einfsep_insert
modified theorem Set.infsep_of_fintype