#!/usr/bin/python3 import fileinput import re files = { 'Analytic': 'Analytic Holomorphic Products Series Uniform', 'ComplexManifold': 'ChartedSpace ComplexManifold Continuation Inverse Nonseparating OneDimension RiemannSphere', 'Dynamics': 'Bottcher BottcherNear Grow Multibrot MultibrotConnected Multiple Postcritical Potential Ray', 'Hartogs': 'Duals FubiniBall MaxLog Osgood Subharmonic Hartogs', 'Misc': 'AbsoluteValue AtInf Bounds Connected Finset Interval Max Measure Multilinear Prod Pow Topology TotallyDisconnected', 'Tactic': 'Bound BoundRules', } names = { 'closed_ball': 'closedBall', 'analytic_at_const': 'analyticAt_const', 'metric.isOpen_iff': 'Metric.isOpen_iff', 'metric.is_open_iff': 'Metric.isOpen_iff', 'complex.abs': 'Complex.abs', 'max_log_norm': 'maxLog_norm', 'metric.continuous_at_iff': 'Metric.continuousAt_iff', 'metric.is_open_ball': 'Metric.isOpen_ball', 'is_max_on_iff': 'isMaxOn_iff', 'nice_volume': 'NiceVolume', 'NiceVolume.Itau': 'NiceVolume.itau', 'is_compact_Icc': 'isCompact_Icc', 'is_compact_closed_ball': 'isCompact_closedBall', 'mem_add_circle_iff_abs': 'mem_addCircle_iff_abs', 'at_top': 'atTop', 'uniformHarmonicLim': 'uniform_harmonic_lim', 'complex.continuous_of_real': 'Complex.continuous_ofReal', 'AEStronglyMeasurable': 'aestronglyMeasurable', 'eventually_at_top': 'eventually_atTop', 'is_open_interior': 'isOpen_interior', 'is_open_ball': 'isOpen_ball', 'nat.cast_pos': 'Nat.cast_pos', 'ennreal.coe_pos': 'ENNReal.coe_pos', 'ennreal.coe_lt_coe': 'ENNReal.coe_lt_coe', 'nnreal.coe_pos': 'NNReal.coe_pos', 'filter.eventually_atTop': 'Filter.eventually_atTop', 'metric.tendsto_uniformly_on_iff': 'Metric.tendstoUniformlyOn_iff', 'finset.mul_sum': 'Finset.mul_sum', 'nat.cast_ne_zero': 'Nat.cast_ne_zero', 'metric.eventually_nhds_iff': 'Metric.eventually_nhds_iff', 'asymptotics.is_O_with_iff': 'Asymptotics.isBigOWith_iff', 'Asymptotics.IsBigOWith_iff': 'Asymptotics.isBigOWith_iff', 'complex.continuous_abs': 'Complex.continuous_abs', 'set.mem_Union': 'set.mem_Union', 'is_closed_closure': 'isClosed_closure', 'mem_set_of': 'mem_setOf', 'set_of_false': 'setOf_false', 'subtype.coe_le_coe': 'Subtype.coe_le_coe', 'is_preconnected_Ioc': 'isPreconnected_Ioc', 'is_preconnected_Icc': 'isPreconnected_Icc', 'is_preconnected_Ioo': 'isPreconnected_Ioo', 'is_closed_Icc': 'isClosed_Icc', 'Icc_extend_apply': 'IccExtend_apply', 'continuous_subtype_coe': 'continuous_subtype_val', 'mem_closed_ball': 'mem_closedBall', 'is_closed_ball': 'isClosed_ball', 'continuous_linear_map': 'ContinuousLinearMap', 'holomorphicAtFst': 'holomorphicAt_fst', 'holomorphicAtSnd': 'holomorphicAt_snd', 'holomorphicAtId': 'holomorphicAt_id', 'continuous_at_fst': 'continuousAt_fst', 'continuous_at_snd': 'continuousAt_snd', 'mem_ext_chart_target': 'mem_ext_chart_target', 'continuous_at_const': 'continuousAt_const', 'compl_set_of': 'compl_setOf', 'Filter.tendsto': 'Filter.Tendsto', 'Classical.not_not': 'not_not', 'is_preconnected_univ': 'isPreconnected_univ', 'analytic_at_id': 'analyticAt_id', 'holomorphicAtConst': 'holomorphicAt_const', 'is_open_holomorphic_at': 'isOpen_holomorphicAt', 'filter.frequently_iff': 'Filter.frequently_iff', 'mem_closed_ball_self': 'mem_closedBall_self', 'analytic_on_const': 'analyticOn_const', 'metric.mem_nhds_iff': 'Metric.mem_nhds_iff', 'holomorphic_at_fst': 'holomorphicAt_fst', 'holomorphic_at_snd': 'holomorphicAt_snd', 'holomorphic_at_const': 'holomorphicAt_const', 'is_open_univ': 'isOpen_univ', 'prod.ext_iff': 'Prod.ext_iff', 'analytic_at_fst': 'analyticAt_fst', 'analytic_at_snd': 'analyticAt_snd', 'continuous_at_id': 'continuousAt_id', 'set_of_exists': 'setOf_exists', 'tendsto_at_top_nhds': 'tendsto_atTop_nhds', 'filter.has_basis_iff': 'Filter.hasBasis_iff', 'bdd_below_def': 'bddBelow_def', 'bdd_above_def': 'bddAbove_def', 'differentiable_at_id': 'differentiableAt_id', 'is_open_iff_eventually': 'isOpen_iff_eventually', 'metric.ball_eq_empty': 'Metric.ball_eq_empty', 'filter.eventually_iff_exists_mem': 'Filter.eventually_iff_exists_mem', 'filter.mem_prod_iff': 'Filter.mem_prod_iff', 'nhds_set_singleton': 'nhdsSet_singleton', 'eventually_nhds_set_iff': 'eventually_nhdsSet_iff', 'mem_closure_iff_nhds_within_ne_bot': 'mem_closure_iff_nhdsWithin_neBot', 'mem_closure_iff_nhdsWithin_ne_bot': 'mem_closure_iff_nhdsWithin_neBot', 'is_compact_singleton': 'isCompact_singleton', 'mem_nhds_set_iff_forall': 'mem_nhdsSet_iff_forall', 'nontrivialHolomorphicAtOfMfderivNeZero': 'nontrivialHolomorphicAt_of_mfderiv_ne_zero', 'complex.of_real_ne_zero': 'Complex.ofReal_ne_zero', 'set_of_subset_set_of': 'setOf_subset_setOf', 'at_inf_basis': 'atInf_basis', 'mem_set_of_eq': 'mem_setOf_eq', 'to_complex_coe': 'toComplex_coe', 'continuous_at_to_complex': 'continuousAt_toComplex', 'continuous_at_toComplex': 'continuousAt_toComplex', 'to_complex_inf': 'toComplex_inf', 'to_complex_zero': 'toComplex_zero', 'RiemannSphere.rec': 'OnePoint.rec', 'filter.tendsto_map': 'Filter.tendsto_map', 'inv_equiv': 'invEquiv', 'inv_equiv_apply': 'invEquiv_apply', 'inv_equiv_symm': 'invEquiv_symm', 'inv_homeomorph': 'invHomeomorph', 'coe_local_homeomorph': 'coeLocalHomeomorph', 'inv_coe_local_homeomorph': 'invCoeLocalHomeomorph', 'coe_local_equiv': 'coeLocalEquiv', 'inv_homeomorph_symm': 'invHomeomorph_symm', 'inv_homeomorph_apply': 'invHomeomorph_apply', 'chart_at_coe': 'chartAt_coe', 'chart_at_inf': 'chartAt_inf', 'ext_chart_at_coe': 'extChartAt_coe', 'ext_chart_at_inf': 'extChartAt_inf', 'coe_local_equiv_symm_apply': 'coeLocalEquiv_symm_apply', 'ext_chart_at_self_analytic': 'extChartAt_self_analytic', 'to_complex': 'toComplex', 'coe_to_complex': 'coe_toComplex', 'continuous_on_to_complex': 'continuousOn_toComplex', 'holomorphicCoe': 'holomorphic_coe', 'coe_local_equiv_apply': 'coeLocalEquiv_apply', 'continuous_at_fill_coe': 'continuousAt_fill_coe', 'continuous_at_fill_inf': 'continuousAt_fill_inf', 'holomorphic_at_to_complex': 'holomorphicAt_toComplex', 'inv_tendsto_at_inf': 'inv_tendsto_atInf', 'holomorphic_at_id': 'holomorphicAt_id', 'holomorphic_at_fill_coe': 'holomorphicAt_fill_coe', 'holomorphic_at_fill_inf': 'holomorphicAt_fill_inf', 'continuous_at_lift_coe': 'continuousAt_lift_coe', 'continuous_at_lift_inf': 'continuousAt_lift_inf', 'holomorphic_at_lift_inf': 'holomorphicAt_lift_inf', 'holomorphic_at_lift_coe': 'holomorphicAt_lift_coe', 'continuous_at_neg': 'continuousAt_neg', 'chart_at': 'chartAt', 'analytic_at_gl': 'analyticAt_gl', 'tendsto_inf_iff_tendsto_at_inf': 'tendsto_inf_iff_tendsto_atInf', 'nat.succ_le_iff': 'Nat.succ_le_iff', 'is_open_multibrot_ext': 'isOpen_multibrotExt', 'nat.cast_le': 'Nat.cast_le', 'metric.tendsto_at_top': 'Metric.tendsto_atTop', 'metric.tendsto_nhds': 'Metric.tendsto_nhds', 'mem_ext_chart_target': 'mem_extChartAt_target', # mathlib 92958d4be9a40419fd2625a27136e16f5b21b6a2 'isTotallyDisconnected_of_clopen_set': 'isTotallyDisconnected_of_isClopen_set', 'disjoint_or_subset_of_clopen': 'disjoint_or_subset_of_isClopen', # mathlib d61c95e1653dffe3f92c8927a905826929f50bce 'pow_le_pow_of_le_left': 'pow_le_pow_left', 'pow_mono': 'pow_right_mono', 'pow_le_pow': 'pow_le_pow_right', 'pow_le_pow_of_le_left': 'pow_le_pow_left', 'pow_lt_pow_of_lt_left': 'pow_lt_pow_left', 'strictMonoOn_pow': 'pow_left_strictMonoOn', 'pow_strictMono_right': 'pow_right_strictMono', 'pow_lt_pow': 'pow_lt_pow_right', 'pow_lt_pow_iff': 'pow_lt_pow_iff_right', 'pow_le_pow_iff': 'pow_le_pow_iff_right', 'self_lt_pow': 'lt_self_pow', 'strictAnti_pow': 'pow_right_strictAnti', 'pow_lt_pow_iff_of_lt_one': 'pow_lt_pow_iff_right_of_lt_one', 'pow_lt_pow_of_lt_one': 'pow_lt_pow_right_of_lt_one', 'lt_of_pow_lt_pow': 'lt_of_pow_lt_pow_left', 'le_of_pow_le_pow': 'le_of_pow_le_pow_left', 'pow_lt_pow₀': 'pow_lt_pow_right₀', 'pow_nat_rpow_nat_inv': 'pow_rpow_inv_natCast', # mathlib bbc6e56d76341e236fa4e15748bebff612b5cb4f, f7006a73d443b58eaf61494edacfeaae71d812f2 'LocalHomeomorph': 'PartialHomeomorph', 'LocalEquiv': 'PartialEquiv', 'toLocalEquiv': 'toPartialEquiv', 'Complex.abs_cast_nat': 'Complex.abs_natCast', 'coeLocalHomeomorph': 'coePartialHomeomorph', 'invCoeLocalHomeomorph': 'invCoePartialHomeomorph', 'coeLocalEquiv_target': 'coePartialEquiv_target', 'coeLocalHomeomorph_target': 'coePartialHomeomorph_target', 'invCoeLocalHomeomorph_target': 'invCoePartialHomeomorph_target', 'coeLocalEquiv_apply': 'coePartialEquiv_apply', 'coeLocalEquiv_symm_apply': 'coePartialEquiv_symm_apply', 'invCoeLocalHomeomorph_apply': 'invCoePartialHomeomorph_apply', 'invCoeLocalHomeomorph_symm_apply': 'invCoePartialHomeomorph_symm_apply', 'coeLocalEquiv': 'coePartialEquiv', } fields = { 'Continuous': 'continuous', 'ContinuousOn': 'continuousOn', 'ContinuousAt': 'continuousAt', 'continuous_on': 'continuousOn', 'continuous_at': 'continuousAt', 'DifferentiableAt': 'differentiableAt', 'DifferentiableOn': 'differentiableOn', 'HarmonicOn': 'harmonicOn', 'SubharmonicOn': 'subharmonicOn', 'is_closed': 'isClosed', 'cauchy_seq': 'cauchySeq', 'comp_continuous_on': 'comp_continuousOn', 'subharmonic_on': 'subharmonicOn', 'integrable_on_sphere': 'integrableOn_sphere', 'to_real': 'toReal', 'DifferentiableWithinAt': 'differentiableWithinAt', 'is_closed_compl': 'isClosed_compl', 'AnalyticAt': 'analyticAt', 'has_fpower_series_at': 'hasFPowerSeriesAt', 'has_sum': 'hasSum', 'change_origin': 'changeOrigin', 'to_nnreal': 'toNNReal', 'HasSum': 'hasSum', 'Sum': 'sum', 'prod_exists': 'prodExists', 'tprod_on_eq': 'tprodOn_eq', 'maps_to': 'mapsTo', 'SuperAtC': 'superAtC', 'IsClosed': 'isClosed', 'is_compact': 'isCompact', 'IsPathConnected': 'isPathConnected', 'joined_in': 'joinedIn', 'mdifferentiable_at': 'mdifferentiableAt', 'MDifferentiableAt': 'mdifferentiableAt', 'mDifferentiableAt': 'mdifferentiableAt', 'differentiable_at': 'differentiableAt', 'has_mfderiv_at': 'hasMFDerivAt', 'has_fderiv_at': 'hasFDerivAt', 'has_deriv_at': 'hasDerivAt', 'smul_right': 'smulRight', 'extChartAtSymm': 'extChartAt_symm', 'compOfEq': 'comp_of_eq', 'leftInv': 'left_inv', 'analytic_on': 'analyticOn', 'Frequently': 'frequently', 'eq_on_of_preconnected_of_frequently_eq': 'eqOn_of_preconnected_of_frequently_eq', 'nontrivial_analytic_on': 'nontrivialAnalyticOn', 'discrete_topology': 'discreteTopology', 'holomorphic_at': 'holomorphicAt', 'is_preconnected': 'isPreconnected', 'InjOn': 'injOn', 'Eventually': 'eventually', 'IsPreconnected': 'isPreconnected', 'HolomorphicAt': 'holomorphicAt', 'HasMFDerivAt': 'hasMFDerivAt', 'ContDiffAt': 'contDiffAt', 'cont_diff_at': 'contDiffAt', 'super_at_c': 'superAtC', 'SuperNearC': 'superNearC', 'is_open_near': 'isOpen_near', 'super_near_c': 'superNearC', 'is_open_preimage': 'isOpen_preimage', 'basinAttracts': 'basin_attracts', 'bottcher_near_eqn': 'bottcherNear_eqn', 'HasFDerivAt': 'hasFDerivAt', 'bottcher_near_holomorphic': 'bottcherNear_holomorphic', 'bottcher_near_mfderiv_ne_zero': 'bottcherNear_mfderiv_ne_zero', 'bottcher_near_a': 'bottcherNear_a', 'bottcher_near': 'bottcherNear', 'bottcher_near_lt_one': 'bottcherNear_lt_one', 'bottcher_near_eq_zero': 'bottcherNear_eq_zero', 'UpperSemicontinuousAt': 'upperSemicontinuousAt', 'potential_eq_zero_of_one_preimage': 'potential_eq_zero_of_onePreimage', 'LowerSemicontinuousAt': 'lowerSemicontinuousAt', 'is_open_compl': 'isOpen_compl', 'bottcherNearHolomorphic': 'bottcherNear_holomorphic', 'is_closed_critical_not_a': 'isClosed_critical_not_a', 'IsCompact': 'isCompact', 'bdd_below_ps': 'bddBelow_ps', 'lower_semicontinuous_p': 'lowerSemicontinuous_p', 'LowerSemicontinuous': 'lowerSemicontinuous', 'is_open_post': 'isOpen_post', 'bottcher_near_iter': 'bottcherNearIter', 'bottcher_near_iter_nontrivial_a': 'bottcherNearIter_nontrivial_a', 'continuous_at_iter': 'continuousAt_iter', 'bottcher_near_iter_holomorphic': 'bottcherNearIter_holomorphic', 'HasDerivAt': 'hasDerivAt', 'mem_nhds_set': 'mem_nhdsSet', 'continuous_within_at': 'continuousWithinAt', 'ContinuousWithinAt': 'continuousWithinAt', 'bottcher_near_iter_mfderiv_ne_zero': 'bottcherNearIter_mfderiv_ne_zero', 'Ray': 'ray', 'rayHolomorphic': 'ray_holomorphic', 'rayHolomorphicOn': 'ray_holomorphicOn', 'rayHolomorphicSlice': 'ray_holomorphic_slice', 'NonNeg': 'nonneg', 'raySpec': 'ray_spec', 'rayEqnSelf': 'ray_eqn_self', 'rayNontrivial': 'ray_nontrivial', 'is_open_ext': 'isOpen_ext', 'ray_holomorphic_on': 'ray_holomorphicOn', 'bottcherHolomorphicOn': 'bottcher_holomorphicOn', 'bottcher_holomorphic_on': 'bottcher_holomorphicOn', 'super_near': 'superNear', 'monomial_mul_leading_coeff': 'monomial_mul_leadingCoeff', 'criticalA': 'critical_a', 'curry_comp': 'comp₂', 'curry_comp_of_eq': 'comp₂_of_eq', 'curry_comp_continuousWithinAt': 'comp₂_continuousWithinAt', 'curry_comp_continuousWithinAt_of_eq': 'comp₂_continuousWithinAt_of_eq', 'in1': 'along_fst', 'in2': 'along_snd', 'toLocalEquiv': 'toPartialEquiv', 'trans_toLocalEquiv': 'trans_toPartialEquiv', 'symm_toLocalEquiv': 'symm_toPartialEquiv', 'prod_toLocalEquiv': 'prod_toPartialEquiv', 'toLocalEquiv_coe': 'toPartialEquiv_coe', 'toLocalEquiv_coe_symm': 'toPartialEquiv_coe_symm', 'preimage_open_of_open': 'isOpen_inter_preimage', 'preimage_open_of_open_symm': 'isOpen_inter_preimage_symm', 'preimage_closed_of_closed': 'preimage_isClosed_of_isClosed', 'toLocalHomeomorph': 'toPartialHomeomorph', 'toLocalHomeomorph_coe': 'toPartialHomeomorph_coe', 'mem_toLocalHomeomorph_source': 'mem_toPartialHomeomorph_source', 'toLocalHomeomorph_target': 'toPartialHomeomorph_target', 'toLocalHomeomorph_symm_apply': 'toPartialHomeomorph_symm_apply', 'image_mem_toLocalHomeomorph_target': 'image_mem_toPartialHomeomorph_target', 'toLocalEquiv_apply': 'toPartialEquiv_apply', 'toLocalHomeomorph_apply': 'toPartialHomeomorph_apply', 'toLocalEquiv_symm_apply': 'toPartialEquiv_symm_apply', 'toLocalEquiv_source': 'toPartialEquiv_source', } changes = [ *[(r'\b%s\b' % k.replace('.', r'\.'), k, v) for k,v in names.items()], *[(r'(?