Commit 2023-01-19 07:45 d6d859a7

View on Github →

chore: format by line breaks (#1523) During porting, I usually fix the desired format we seem to want for the line breaks around by with

awk '{do {{if (match($0, "^  by$") && length(p) < 98) {p=p " by";} else {if (NR!=1) {print p}; p=$0}}} while (getline == 1) if (getline==0) print p}' Mathlib/File/Im/Working/On.lean

I noticed there are some more files that slipped through. This pull request is the result of running this command:

grep -lr "^  by\$" Mathlib | xargs -n 1 awk -i inplace '{do {{if (match($0, "^  by$") && length(p) < 98 && not (match(p, "^[ \t]*--"))) {p=p " by";} else {if (NR!=1) {print p}; p=$0}}} while (getline == 1) if (getline==0) print p}'

Estimated changes

modified theorem Odd.neg_zpow
modified theorem div_sq_cancel
modified theorem pow_sub_of_lt
modified theorem pow_sub₀
modified theorem zero_zpow_eq
modified theorem zpow_add₀
modified theorem zpow_bit1₀
modified theorem zpow_neg_mul_zpow_self
modified theorem exists_floor
modified theorem exists_nat_ge
modified theorem exists_nat_one_div_lt
modified theorem exists_pow_lt_of_lt_one
modified theorem exists_rat_btwn
modified theorem sub_one_div_inv_le_two
modified theorem zpow_injective
modified theorem zpow_le_of_le
modified theorem IsLeftRegular.pow_iff
modified theorem IsRightRegular.pow
modified theorem unitary.coe_zpow
modified theorem Fin.val_add_one_of_lt
modified theorem Int.cinfₛ_mem
modified theorem Int.csupₛ_mem
modified theorem Int.div2_bit
modified theorem Int.le_coe_nat_sub
modified theorem Int.natAbs_eq_iff_sq_eq
modified theorem Int.natAbs_le_iff_sq_le
modified theorem Int.natAbs_lt_iff_sq_lt
modified theorem Int.gcd_a_modEq
modified theorem Int.modEq_iff_add_fac
modified theorem List.prod_eq_one
modified theorem List.prod_eq_zero
modified theorem List.dvd_prod
modified theorem List.dvd_sum
modified theorem List.Chain'.infix
modified theorem List.Chain'.rel_head?
modified theorem List.dedup_append
modified theorem List.destutter'_is_chain'
modified theorem List.destutter'_of_chain
modified theorem List.destutter'_sublist
modified theorem List.mem_destutter'
modified theorem List.Duplicate.mem
modified theorem List.Duplicate.mono_sublist
modified theorem List.Duplicate.ne_singleton
modified theorem List.duplicate_cons_iff
modified theorem List.duplicate_iff_sublist
modified theorem List.forall₂_eq_eq_eq
modified theorem List.range_map
modified theorem List.foldr_max_of_ne_nil
modified theorem List.le_max_of_le
modified theorem List.max_le_of_forall_le
modified theorem List.maximum_concat
modified theorem List.Nodup.union
modified theorem List.Perm.permutations'
modified theorem List.nodup_permutations
modified theorem List.perm_comp_perm
modified theorem List.perm_option_to_list
modified theorem List.subperm_cons_erase
modified theorem List.NodupKeys.kunion
modified theorem List.dlookup_dedupKeys
modified theorem List.nodupKeys_dedupKeys
modified theorem Nat.eq_of_testBit_eq
modified theorem Nat.testBit_eq_inth
modified theorem Nat.testBit_two_pow_of_ne
modified theorem Nat.half_le_of_sub_le_half
modified theorem Nat.le_half_of_half_lt_sub
modified theorem PNat.Coprime.mul
modified theorem PNat.Coprime.mul_right
modified theorem PNat.Coprime.symm
modified theorem PNat.Prime.ne_one
modified theorem PNat.Prime.not_dvd_one
modified theorem PNat.dvd_prime
modified theorem PNat.exists_prime_and_dvd
modified theorem PNat.gcd_comm
modified theorem PNat.gcd_eq_left
modified theorem PNat.gcd_eq_left_iff_dvd
modified theorem PNat.gcd_eq_right_iff_dvd
modified theorem PNat.one_gcd
modified theorem Rat.cast_inv_int
modified theorem Rat.cast_inv_nat
modified theorem Rat.cast_mk_of_ne_zero
modified theorem Rat.cast_pos_of_pos
modified theorem Rat.preimage_cast_Icc
modified theorem Rat.preimage_cast_Ici
modified theorem Rat.preimage_cast_Ico
modified theorem Rat.preimage_cast_Iic
modified theorem Rat.preimage_cast_Iio
modified theorem Rat.preimage_cast_Ioc
modified theorem Rat.preimage_cast_Ioi
modified theorem Rat.preimage_cast_Ioo
modified theorem Semiquot.get_mem
modified theorem Set.disjoint_ordT5Nhd
modified theorem Set.zero_mem_smul_set_iff
modified theorem Set.inv_mem_center₀
modified theorem IsSimpleOrder.bot_ne_top
modified theorem Set.Ici.isAtom_iff
modified theorem Set.Iic.isCoatom_iff
modified theorem supₛ_atoms_eq_top
modified theorem supₛ_atoms_le_eq
modified theorem Set.compl_cIcc
modified theorem Set.compl_cIoo
modified theorem sbtw_iff_not_btw
modified theorem LowerAdjoint.mem_iff
modified theorem Concept.ext'
modified theorem Concept.ext
modified theorem Concept.snd_subset_snd_iff