Misaligned aligns

gistfile1.txt

===== File lean/library/init/meta/well_founded_tactics.lean =====
Missing aligns: {'psum.alt.sizeof', 'psum.has_sizeof_alt', 'well_founded_tactics.id_tag.wf'}

===== File mathlib/src/ring_theory/coprime/lemmas.lean =====
Missing aligns: {'nat.is_coprime_iff_coprime'}
Phantom aligns: {'nat.isCoprime_iff_coprime'}

===== File mathlib/src/algebra/smul_with_zero.lean =====
Missing aligns: {'left_ne_zero_of_smul', 'mul_action_with_zero.nontrivial', 'smul_monoid_with_zero_hom_apply', 'smul_eq_zero_of_right', 'mul_action_with_zero.subsingleton', 'smul_eq_zero_of_left', 'right_ne_zero_of_smul'}

===== File mathlib/src/algebra/invertible.lean =====
Missing aligns: {'invertible.of_left_inverse_inv_of', 'coe_unit_of_invertible', 'invertible_equiv_of_left_inverse_symm_apply', 'coe_inv_unit_of_invertible', 'invertible_equiv_of_left_inverse_apply'}

===== File mathlib/src/algebra/parity.lean =====
Missing aligns: {'even_of_exists_two_nsmul', 'is_square_of_exists_sq', 'even.neg', 'is_square.inv', 'even.trans_dvd', 'even.two_dvd', 'odd.exists_bit1', 'is_square.exists_sq', 'even.exists_bit0', 'has_dvd.dvd.even', 'even.exists_two_nsmul'}

===== File mathlib/src/algebra/opposites.lean =====
Missing aligns: {'add_opposite.op_equiv', 'mul_opposite.op_injective', 'mul_opposite.op_one', 'add_opposite.op_eq_zero_iff', 'add_opposite.rec', 'mul_opposite.unop', 'add_opposite.op_add', 'add_opposite.op_equiv_symm_apply', 'mul_opposite.op_equiv_symm_apply', 'mul_opposite.unop_inj', 'add_opposite.op_neg', 'add_opposite.unop_bijective', 'mul_opposite.op_smul', 'add_opposite.op_equiv_apply', 'mul_opposite.unop_comp_op', 'mul_opposite.op_inv', 'add_opposite.unop_op', 'add_opposite.unop_zero', 'add_opposite.op', 'mul_opposite.op_unop', 'mul_opposite.op_equiv', 'add_opposite.op_injective', 'mul_opposite.unop_mul', 'add_opposite.op_bijective', 'add_opposite.unop', 'mul_opposite.op_inj', 'mul_opposite.unop_one', 'mul_opposite.unop_eq_one_iff', 'add_opposite.unop_add', 'add_opposite', 'mul_opposite.unop_surjective', 'add_opposite.unop_surjective', 'mul_opposite.op_surjective', 'mul_opposite.unop_op', 'add_opposite.unop_neg', 'mul_opposite.op_bijective', 'mul_opposite.op_eq_one_iff', 'mul_opposite.unop_bijective', 'add_opposite.op_surjective', 'mul_opposite.op_equiv_apply', 'add_opposite.op_unop', 'add_opposite.unop_inj', 'mul_opposite', 'add_opposite.op_vadd', 'add_opposite.unop_injective', 'add_opposite.op_inj', 'add_opposite.unop_eq_zero_iff', 'mul_opposite.op_mul', 'mul_opposite.unop_smul', 'add_opposite.op_comp_unop', 'add_opposite.op_zero', 'add_opposite.unop_comp_op', 'mul_opposite.op_comp_unop', 'add_opposite.unop_vadd'}

===== File mathlib/src/algebra/ne_zero.lean =====
Missing aligns: {'four_ne_zero', 'one_ne_zero', "two_ne_zero'", "three_ne_zero'", 'ne_zero.ne', 'ne_zero_of_eq_one', 'three_ne_zero', 'ne_zero', 'zero_ne_one', "ne_zero.ne'", "one_ne_zero'", "zero_ne_one'", 'ne_zero.trans', 'two_ne_zero', 'ne_zero.of_pos', "four_ne_zero'"}

===== File mathlib/src/algebra/indicator_function.lean =====
Missing aligns: {'set.mul_indicator_mul_compl_eq_piecewise'}
Phantom aligns: {'set.mulIndicator_mul_compl_eq_piecewise'}

===== File mathlib/src/algebra/covariant_and_contravariant.lean =====
Missing aligns: {'contravariant_flip_mul_iff', "antitone.covariant_of_const'", 'antitone.covariant_of_const', 'rel_of_act_rel_act', 'covariant.flip', 'rel_iff_cov', 'group.covariant_swap_iff_contravariant_swap', 'covariant_le_iff_contravariant_lt', "monotone.covariant_of_const'", 'act_rel_act_of_rel_of_rel', 'contravariant_lt_of_contravariant_le', 'covariant.monotone_of_const', 'contravariant.flip', 'contravariant_class', 'covariant_lt_iff_contravariant_le', 'covariant', 'act_rel_act_of_rel', 'rel_act_of_act_rel_act_of_rel_act', 'group.covariant_iff_contravariant', 'covariant_flip_mul_iff', 'add_group.covariant_iff_contravariant', 'rel_act_of_rel_of_rel_act', 'contravariant', 'covariant_flip_add_iff', 'add_group.covariant_swap_iff_contravariant_swap', 'act_rel_of_rel_of_act_rel', 'act_rel_of_act_rel_of_rel_act_rel', 'monotone.covariant_of_const', 'covariant_le_of_covariant_lt', 'contravariant_flip_add_iff', 'covariant_class'}

===== File mathlib/src/algebra/divisibility/basic.lean =====
Missing aligns: {'dvd_of_mul_right_eq', 'has_dvd.dvd.trans', 'dvd_of_mul_left_eq', 'has_dvd.dvd.mul_left', 'has_dvd.dvd.mul_right'}

===== File mathlib/src/algebra/divisibility/units.lean =====
Missing aligns: {'is_unit.dvd', 'is_unit.mul_left_dvd', 'units.coe_dvd', 'is_unit.dvd_mul_right', 'is_unit.dvd_mul_left', 'units.dvd_mul_right', 'is_unit.mul_right_dvd'}

===== File mathlib/src/algebra/ring/add_aut.lean =====
Missing aligns: {'add_aut.mul_left_apply_apply', 'add_aut.mul_left_apply_symm_apply'}

===== File mathlib/src/algebra/ring/fin.lean =====
Missing aligns: {'ring_equiv.pi_fin_two_apply', 'ring_equiv.pi_fin_two_symm_apply'}

===== File mathlib/src/algebra/ring/equiv.lean =====
Missing aligns: {'ring_equiv.of_hom_inv_symm_apply', "ring_equiv.of_hom_inv'_symm_apply", 'ring_equiv.op_apply_apply', "ring_equiv.of_hom_inv'_apply", 'ring_equiv.to_mul_equiv', 'ring_equiv.Pi_congr_right_apply', 'ring_equiv.op_symm_apply_symm_apply', 'ring_equiv.of_hom_inv_apply', 'ring_equiv.to_add_equiv', 'ring_equiv.to_equiv', 'ring_equiv.op_symm_apply_apply', 'ring_equiv.op_apply_symm_apply'}
Phantom aligns: {'ring_equiv.to_equiv_mk'}

===== File mathlib/src/algebra/ring/opposite.lean =====
Missing aligns: {'non_unital_ring_hom.op_apply_to_fun', 'ring_hom.op_symm_apply_apply', 'non_unital_ring_hom.from_opposite_to_fun', 'non_unital_ring_hom.op_symm_apply_to_fun', 'ring_hom.to_opposite_apply', 'ring_hom.from_opposite_apply', 'non_unital_ring_hom.to_opposite_to_fun', 'ring_hom.op_apply_apply'}

===== File mathlib/src/algebra/ring/basic.lean =====
Missing aligns: {'add_hom.mul_right_apply', 'add_hom.mul_left_apply'}

===== File mathlib/src/algebra/ring/aut.lean =====
Missing aligns: {'mul_semiring_action.to_ring_aut_apply'}

===== File mathlib/src/algebra/ring/prod.lean =====
Missing aligns: {'ring_equiv.prod_zero_ring_symm_apply', 'ring_equiv.prod_zero_ring_apply', 'ring_equiv.zero_ring_prod_symm_apply', 'ring_equiv.zero_ring_prod_apply'}

===== File mathlib/src/algebra/ring/pi.lean =====
Missing aligns: {'pi.eval_ring_hom_apply', 'pi.const_ring_hom_apply', 'pi.eval_non_unital_ring_hom_to_fun', 'ring_hom.comp_left_apply', 'pi.const_non_unital_ring_hom_to_fun', 'pi.non_unital_ring_hom_to_fun', 'pi.ring_hom_apply', 'non_unital_ring_hom.comp_left_to_fun'}

===== File mathlib/src/algebra/ring/defs.lean =====
Missing aligns: {'mul_sub', 'one_sub_mul', 'mul_neg_one', 'add_ite', 'sub_one_mul', 'add_mul', 'sub_mul', 'ite_add', 'one_add_one_eq_two', 'mul_sub_one', 'neg_one_mul', 'mul_one_sub', 'mul_add', 'neg_eq_neg_one_mul'}

===== File mathlib/src/algebra/star/unitary.lean =====
Missing aligns: {'unitary.coe_inv_to_units_apply', 'unitary.coe_to_units_apply'}

===== File mathlib/src/algebra/star/basic.lean =====
Missing aligns: {'complex.conj_conj', 'star_mul_equiv_apply', 'star_add_equiv_apply', 'star_mul_aut_apply', 'star_ring_equiv_apply', 'star_ring_aut_apply', 'is_R_or_C.conj_conj'}

===== File mathlib/src/algebra/module/pointwise_pi.lean =====
Missing aligns: {'vadd_univ_pi', 'vadd_pi', 'vadd_pi_subset'}

===== File mathlib/src/algebra/module/hom.lean =====
Missing aligns: {'add_monoid_hom.coe_smul'}

===== File mathlib/src/algebra/module/basic.lean =====
Missing aligns: {'module.ext', 'module.ext_iff', 'module.to_add_monoid_End_apply_apply'}

===== File mathlib/src/algebra/module/linear_map.lean =====
Missing aligns: {'distrib_mul_action.to_module_End_apply', 'module.module_End_self_op_symm_apply', 'module.to_module_End_apply', 'distrib_mul_action.to_linear_map_apply', 'module.module_End_self_apply', 'module.module_End_self_symm_apply', 'linear_map.to_add_hom', 'module.module_End_self_op_apply', 'ring_hom.to_semilinear_map_apply', 'module.comp_hom.to_linear_map_apply'}
Phantom aligns: {'LinearMap.has_coe_to_fun'}

===== File mathlib/src/algebra/group_ring_action/basic.lean =====
Missing aligns: {'mul_semiring_action.to_ring_hom_apply', 'mul_semiring_action.to_ring_equiv_apply', 'mul_semiring_action.to_ring_equiv_symm_apply'}

===== File mathlib/src/algebra/free_monoid/basic.lean =====
Missing aligns: {'free_add_monoid.hom_map_lift', 'free_add_monoid.of_vadd', 'free_add_monoid.rec_on_of_add', 'free_add_monoid.comp_lift', 'free_add_monoid.cases_on', 'free_add_monoid.to_list_map', 'free_add_monoid.hom_eq', 'free_add_monoid.lift_symm_apply', 'free_add_monoid.lift', 'free_add_monoid.sum_aux_eq', 'free_add_monoid.rec_on_zero', 'free_monoid.prod_aux_eq', 'free_add_monoid.map_comp', 'free_add_monoid.of', 'free_add_monoid.mk_add_action', 'free_add_monoid.lift_apply', 'free_add_monoid.lift_eval_of', 'free_add_monoid.to_list', 'free_add_monoid.of_list_nil', 'free_add_monoid.to_list_of', 'free_add_monoid.lift_comp_of', 'free_add_monoid.lift_of_comp_eq_map', 'free_add_monoid.of_list', 'free_add_monoid.to_list_add', 'free_add_monoid.of_list_symm', 'free_add_monoid.of_list_join', 'free_add_monoid.to_list_of_add', 'free_add_monoid.rec_on', 'free_add_monoid.of_list_comp_to_list', 'free_add_monoid.to_list_symm', 'free_add_monoid.to_list_sum', 'free_add_monoid.of_list_vadd', 'free_add_monoid.of_list_singleton', 'free_add_monoid.to_list_zero', 'free_add_monoid.vadd_def', 'free_add_monoid.of_list_map', 'free_add_monoid', 'free_add_monoid.lift_restrict', 'free_add_monoid.map_id', 'free_add_monoid.to_list_comp_of_list', 'free_add_monoid.of_list_to_list', 'free_monoid.prod_aux', 'free_add_monoid.of_list_cons', 'free_add_monoid.cases_on_zero', 'free_add_monoid.of_list_append', 'free_add_monoid.to_list_of_list', 'free_add_monoid.map', 'free_add_monoid.sum_aux', 'free_add_monoid.cases_on_of_add', 'free_add_monoid.of_injective', 'free_add_monoid.map_of'}

===== File mathlib/src/algebra/group_with_zero/basic.lean =====
Missing aligns: {"div_self_mul_self'", 'mul_inv_cancel_right₀', 'inv_ne_zero', 'eq_zero_of_mul_eq_self_left', 'inv_mul_cancel_right₀', 'right_ne_zero_of_mul', 'inv_mul_mul_self', "mul_right_inj'", 'inv_mul_cancel', 'one_div_ne_zero', 'subsingleton_iff_zero_eq_one', 'eq_of_zero_eq_one', 'group_with_zero.mul_left_injective', 'mul_eq_mul_right_iff', 'mul_inv_mul_self', 'zero_div', 'mul_left_eq_self₀', 'left_ne_zero_of_mul', 'subsingleton_of_zero_eq_one', 'eq_zero_of_zero_eq_one', 'inv_eq_zero', 'div_self_mul_self', 'mul_ne_zero', 'mul_inv_cancel_left₀', 'inv_mul_cancel_left₀', 'mul_right_eq_self₀', 'zero_eq_inv', 'mul_eq_mul_left_iff', 'div_div_self', 'mul_left_surjective₀', 'eq_zero_of_one_div_eq_zero', 'mul_zero_eq_const', 'mul_self_div_self', 'group_with_zero.mul_right_injective', 'right_ne_zero_of_mul_eq_one', 'zero_ne_one_or_forall_eq_0', 'mul_eq_zero_of_ne_zero_imp_eq_zero', 'eq_zero_of_mul_eq_self_right', 'mul_right_surjective₀', 'zero_mul_eq_const', 'eq_zero_of_mul_self_eq_zero', 'ne_zero_and_ne_zero_of_mul', 'div_mul_eq_mul_div₀', 'div_zero', 'left_ne_zero_of_mul_eq_one', 'mul_self_mul_inv', 'ne_zero_of_one_div_ne_zero', "mul_left_inj'"}

===== File mathlib/src/algebra/group_with_zero/defs.lean =====
Missing aligns: {'mul_right_cancel₀', 'is_cancel_mul_zero', 'mul_zero_class', 'is_left_cancel_mul_zero.to_is_right_cancel_mul_zero', 'mul_eq_zero_of_left', 'comm_monoid_with_zero', 'mul_zero', 'is_right_cancel_mul_zero.to_is_cancel_mul_zero', 'mul_zero_one_class', 'group_with_zero', 'mul_ne_zero_iff', 'zero_ne_mul_self', 'no_zero_divisors', 'mul_self_eq_zero', 'mul_left_injective₀', 'zero_eq_mul_self', 'cancel_monoid_with_zero', 'zero_mul', 'mul_right_injective₀', 'is_left_cancel_mul_zero.to_is_cancel_mul_zero', 'mul_ne_zero_comm', 'inv_zero', 'comm_group_with_zero', 'semigroup_with_zero', 'is_left_cancel_mul_zero', 'mul_self_ne_zero', 'mul_eq_zero', 'cancel_comm_monoid_with_zero', 'mul_inv_cancel', 'is_right_cancel_mul_zero.to_is_left_cancel_mul_zero', 'mul_eq_zero_comm', 'zero_eq_mul', 'monoid_with_zero', 'mul_eq_zero_of_right', 'pullback_nonzero', 'is_right_cancel_mul_zero', 'mul_left_cancel₀'}

===== File mathlib/src/algebra/big_operators/pi.lean =====
Missing aligns: {'prod_mk_sum'}
Phantom aligns: {'sum_mk_sum'}

===== File mathlib/src/algebra/big_operators/ring.lean =====
Missing aligns: {'finset.sum_powerset_insert', 'finset.sum_powerset'}

===== File mathlib/src/algebra/big_operators/multiset/lemmas.lean =====
Missing aligns: {'multiset.sum_eq_zero_iff'}

===== File mathlib/src/algebra/big_operators/multiset/basic.lean =====
Missing aligns: {'multiset.single_le_sum', 'multiset.sum_eq_foldr', 'multiset.sum_pair', 'multiset.sum', 'multiset.sum_map_le_sum_map', 'multiset.le_sum_of_subadditive_on_pred', "multiset.sum_map_neg'", 'multiset.sum_to_list', 'multiset.sum_erase', 'multiset.sum_replicate', 'multiset.sum_zero', 'multiset.sum_map_add', 'map_multiset_sum', 'multiset.sum_hom_rel', 'multiset.sum_map_sub', 'multiset.le_sum_nonempty_of_subadditive', 'multiset.sum_le_sum_map', 'multiset.sum_map_zsmul', 'multiset.sum_eq_foldl', 'multiset.le_sum_of_subadditive', 'multiset.sum_map_erase', 'multiset.sum_cons', 'multiset.card_nsmul_le_sum', 'multiset.sum_le_card_nsmul', 'multiset.sum_eq_nsmul_single', 'multiset.sum_induction', 'multiset.all_zero_of_le_zero_le_of_sum_eq_zero', 'multiset.sum_le_sum_of_rel_le', 'multiset.sum_induction_nonempty', 'add_monoid_hom.map_multiset_sum', 'multiset.sum_map_eq_nsmul_single', 'multiset.coe_sum', "multiset.sum_hom'", 'multiset.sum_hom', 'multiset.nsmul_count', 'multiset.le_sum_of_mem', 'multiset.sum_map_neg', 'multiset.sum_hom₂', 'multiset.sum_map_zero', 'multiset.sum_nonneg', 'multiset.sum_add', 'multiset.sum_map_sum_map', 'multiset.sum_map_le_sum', 'multiset.sum_singleton', 'multiset.le_sum_nonempty_of_subadditive_on_pred', 'multiset.sum_eq_zero', 'multiset.sum_map_nsmul'}

===== File mathlib/src/algebra/order/with_zero.lean =====
Missing aligns: {"order_iso.mul_left₀'_apply", "order_iso.mul_left₀'_to_equiv", "order_iso.mul_right₀'_apply", "order_iso.mul_right₀'_to_equiv"}

===== File mathlib/src/algebra/order/lattice_group.lean =====
Missing aligns: {'neg_sup_eq_neg_inf_neg', 'add_inf', 'lattice_ordered_comm_group.add_inf_eq_add_inf_add', 'lattice_ordered_comm_group.abs_sub_sup_add_abs_sub_inf', 'lattice_ordered_comm_group.neg_abs', 'lattice_ordered_comm_group.neg_eq_pos_neg', "lattice_ordered_comm_group.neg_eq_zero_iff'", 'lattice_ordered_comm_group.neg_zero', 'lattice_ordered_comm_group.two_inf_eq_add_sub_abs_sub', 'lattice_ordered_comm_group.neg_nonneg', 'lattice_ordered_comm_group.pos_zero', 'lattice_ordered_comm_group.neg_part_def', 'lattice_ordered_comm_group.neg_of_inv_nonneg', 'lattice_ordered_comm_group.neg_of_nonneg', 'lattice_ordered_comm_group.neg_of_nonpos', 'lattice_ordered_comm_group.pos_part_def', 'lattice_ordered_comm_group.abs_neg_comm', 'lattice_ordered_comm_group.abs_abs', 'lattice_ordered_comm_group.neg_of_neg_nonpos', 'lattice_ordered_comm_group.lattice_ordered_add_comm_group_to_distrib_lattice', 'lattice_ordered_comm_group.pos_abs', 'lattice_ordered_comm_group.pos_eq_self_of_pos_pos', 'lattice_ordered_comm_group.neg_le_neg', 'lattice_ordered_comm_group.pos_of_nonpos', 'lattice_ordered_comm_group.neg_le_abs', 'lattice_ordered_comm_group.neg_eq_zero_iff', 'lattice_ordered_comm_group.neg_nonpos_iff', 'lattice_ordered_comm_group.abs_nonneg', 'lattice_ordered_comm_group.sup_sub_inf_eq_abs_sub', 'lattice_ordered_comm_group.le_iff_pos_le_neg_ge', 'add_sup', 'lattice_ordered_comm_group.pos_nonneg', 'lattice_ordered_comm_group.pos_nonpos_iff', 'lattice_ordered_comm_group.two_sup_eq_add_add_abs_sub', 'lattice_ordered_comm_group.abs_add_le', 'lattice_ordered_comm_group.pos_of_nonneg', 'lattice_ordered_comm_group.pos_eq_neg_neg', 'inf_add_sup', 'lattice_ordered_comm_group.inf_eq_sub_pos_sub', 'neg_inf_eq_sup_neg', 'lattice_ordered_comm_group.pos_inf_neg_eq_zero', 'lattice_ordered_comm_group.abs_sup_sub_sup_le_abs', 'lattice_ordered_comm_group.abs_inf_sub_inf_le_abs', 'lattice_ordered_comm_group.pos_sub_neg', 'lattice_ordered_comm_group.le_abs', 'lattice_ordered_comm_group.le_pos', 'lattice_ordered_comm_group.pos_add_neg', 'lattice_ordered_comm_group.neg_eq_neg_inf_zero', 'lattice_ordered_comm_group.Birkhoff_inequalities', 'lattice_ordered_comm_group.pos_eq_zero_iff', 'lattice_ordered_comm_group.sup_eq_add_pos_sub', 'lattice_ordered_comm_group.abs_abs_sub_abs_le', 'lattice_ordered_comm_group.abs_of_nonneg'}

===== File mathlib/src/algebra/order/smul.lean =====
Missing aligns: {'order_iso.smul_left_symm_apply', 'order_iso.smul_left_apply'}

===== File mathlib/src/algebra/order/absolute_value.lean =====
Missing aligns: {'is_absolute_value.to_absolute_value_to_mul_hom_apply', 'is_absolute_value.to_absolute_value_apply', 'absolute_value.abs_apply', 'absolute_value.abs_to_mul_hom_apply'}
Phantom aligns: {'is_absolute_value.abv_mul', 'is_absolute_value.abv_nonneg', 'is_absolute_value.abv_add', 'is_absolute_value.abv_eq_zero'}

===== File mathlib/src/algebra/order/zero_le_one.lean =====
Missing aligns: {'zero_le_one', "zero_lt_one'", 'one_pos', "zero_le_one'", 'zero_lt_one'}

===== File mathlib/src/algebra/order/archimedean.lean =====
Missing aligns: {'exists_unique_sub_zsmul_mem_Ioc', 'exists_unique_sub_zsmul_mem_Ico'}

===== File mathlib/src/algebra/order/pi.lean =====
Missing aligns: {'function.const_neg', 'function.const_pos', 'function.const_nonpos_of_nonpos', 'function.const_nonneg_of_nonneg', 'function.const_nonneg', 'function.const_nonpos'}

===== File mathlib/src/algebra/order/ring/lemmas.lean =====
Missing aligns: {'le_mul_of_le_of_one_le_of_nonneg', 'mul_lt_of_le_one_of_lt_of_nonneg', 'right.mul_nonneg', "exists_square_le'", 'lt_of_mul_lt_mul_of_nonneg_right', 'neg_of_mul_pos_left', 'lt_of_mul_lt_mul_right', 'right.neg_of_mul_neg_left', 'lt_mul_iff_one_lt_right', 'mul_le_of_mul_le_of_nonneg_right', 'mul_lt_of_le_of_lt_one_of_pos', 'le_mul_of_one_le_of_le_of_nonneg', 'mul_lt_mul_of_nonneg_of_pos', 'mul_lt_of_lt_one_of_lt_of_pos', 'mul_le_mul_of_le_of_le', 'le_of_mul_le_mul_of_pos_right', 'le_of_mul_le_mul_right', 'lt_mul_of_one_lt_left', 'left.one_le_mul_of_le_of_le', "le_mul_of_le_of_one_le'", 'mul_pos', 'mul_pos_mono.to_mul_pos_reflect_lt', 'mul_lt_of_lt_one_left', 'right.mul_pos', 'mul_pos_mono_rev', 'mul_lt_of_mul_lt_of_nonneg_left', 'lt_mul_of_one_lt_right', 'mul_right_cancel_iff_of_pos', "mul_lt_of_lt_of_le_one'", 'mul_le_mul_of_nonneg_left', 'mul_self_le_mul_self', 'lt_mul_of_one_lt_of_lt_of_pos', 'le_mul_of_one_le_left', 'mul_le_mul', 'lt_mul_iff_one_lt_left', 'right.mul_le_one_of_le_of_le', 'le_mul_iff_one_le_left', "lt_mul_of_le_of_one_lt'", "mul_lt_mul_of_lt_of_lt'", 'le_mul_of_le_mul_of_nonneg_right', 'pos_mul_mono', 'left.mul_lt_of_lt_of_le_one_of_nonneg', 'mul_le_of_le_one_left', 'neg_of_mul_pos_right', 'mul_pos_strict_mono', 'mul_lt_mul_of_pos_right', 'mul_nonpos_of_nonpos_of_nonneg', 'left.one_lt_mul_of_le_of_lt_of_pos', 'left.mul_lt_of_le_of_lt_one_of_pos', 'left.mul_nonneg', "mul_lt_of_le_of_lt_one'", 'le_of_mul_le_mul_left', 'mul_le_iff_le_one_left', 'lt_mul_of_lt_of_one_lt_of_pos', "mul_lt_mul_of_le_of_lt'", 'pos_mul_mono_iff_pos_mul_reflect_lt', 'right.one_lt_mul_of_lt_of_le_of_pos', 'mul_le_mul_left', 'lt_of_mul_lt_of_one_le_of_nonneg_left', 'mul_pos_mono', 'right.mul_lt_one_of_lt_of_le_of_pos', 'mul_lt_mul_of_pos_of_nonneg', 'neg_iff_neg_of_mul_pos', 'mul_lt_of_lt_one_right', 'mul_lt_mul_of_pos_of_pos', 'mul_pos_mono_rev.to_mul_pos_strict_mono', 'pos_iff_pos_of_mul_pos', "mul_le_of_le_one_of_le'", 'lt_of_lt_mul_of_le_one_of_nonneg_right', 'lt_mul_of_lt_of_one_le_of_nonneg', 'lt_mul_of_one_le_of_lt_of_nonneg', 'lt_mul_of_le_of_one_lt_of_pos', 'mul_left_cancel_iff_of_pos', 'mul_neg_of_pos_of_neg', 'lt_mul_of_lt_mul_of_nonneg_right', 'pos_mul_strict_mono_iff_pos_mul_mono_rev', 'mul_lt_iff_lt_one_right', 'pos_and_pos_or_neg_and_neg_of_mul_pos', 'pos_of_mul_pos_right', 'le_mul_iff_one_le_right', 'mul_lt_mul_left', 'right.one_lt_mul_of_lt_of_lt', 'mul_lt_of_lt_of_le_one_of_nonneg', 'mul_le_iff_le_one_right', 'mul_lt_of_lt_of_lt_one_of_pos', 'mul_nonpos_of_nonneg_of_nonpos', 'lt_mul_of_one_lt_of_le_of_pos', 'mul_pos_mono_iff_mul_pos_reflect_lt', "lt_mul_of_lt_of_one_le'", 'lt_mul_of_one_lt_of_lt_of_nonneg', 'le_of_mul_le_of_one_le_nonneg_right', 'mul_le_of_le_of_le_one_of_nonneg', 'left.neg_of_mul_neg_right', 'pos_mul_mono_rev.to_pos_mul_strict_mono', 'mul_lt_mul_of_pos_left', 'left.mul_pos', 'left.mul_le_one_of_le_of_le', 'right.one_lt_mul_of_le_of_lt_of_nonneg', 'le_of_mul_le_of_one_le_of_nonneg_left', "mul_le_of_le_of_le_one'", 'mul_lt_mul_right', "mul_lt_mul_of_le_of_le'", 'zero_lt_mul_right', 'right.one_le_mul_of_le_of_le', 'left.neg_of_mul_neg_left', 'pos_mul_mono.to_pos_mul_reflect_lt', 'right.neg_of_mul_neg_right', 'left.lt_mul_of_lt_of_one_le_of_nonneg', 'pos_mul_mono_rev', 'mul_neg_of_neg_of_pos', "mul_eq_mul_iff_eq_and_eq_of_pos'", 'mul_le_of_mul_le_of_nonneg_left', 'le_mul_of_le_mul_of_nonneg_left', 'le_of_le_mul_of_le_one_of_nonneg_left', 'right.mul_lt_one_of_le_of_lt_of_nonneg', 'pos_mul_strict_mono', 'mul_nonneg', "mul_lt_of_lt_one_of_le'", 'mul_eq_mul_iff_eq_and_eq_of_pos', 'mul_le_of_le_one_of_le_of_nonneg', 'lt_of_mul_lt_mul_of_nonneg_left', 'le_of_le_mul_of_le_one_of_nonneg_right', 'mul_le_mul_of_nonneg_right', 'zero_lt_mul_left', 'le_mul_of_one_le_right', 'lt_of_mul_lt_mul_left', 'lt_of_lt_mul_of_le_one_of_nonneg_left', 'mul_lt_iff_lt_one_left', 'mul_lt_of_lt_one_of_le_of_pos', 'le_of_mul_le_mul_of_pos_left', 'lt_mul_of_lt_mul_of_nonneg_left', "mul_lt_of_le_one_of_lt'", 'mul_le_mul_right', 'mul_lt_of_mul_lt_of_nonneg_right', 'mul_le_of_le_one_right', 'pos_of_mul_pos_left', 'mul_pos_strict_mono_iff_mul_pos_mono_rev'}

===== File mathlib/src/algebra/order/ring/cone.lean =====
Missing aligns: {'ring.positive_cone.to_positive_cone', 'ring.total_positive_cone.to_total_positive_cone'}

===== File mathlib/src/algebra/order/ring/with_top.lean =====
Missing aligns: {'monoid_with_zero_hom.with_top_map_apply', 'ring_hom.with_top_map_apply'}

===== File mathlib/src/algebra/order/ring/defs.lean =====
Missing aligns: {'one_lt_mul'}

===== File mathlib/src/algebra/order/sub/canonical.lean =====
Missing aligns: {'tsub_eq_zero_of_le'}

===== File mathlib/src/algebra/order/sub/defs.lean =====
Missing aligns: {'tsub_nonpos_of_le'}

===== File mathlib/src/algebra/order/hom/monoid.lean =====
Missing aligns: {"order_monoid_hom.mk'_to_monoid_hom", 'order_monoid_hom.comp_apply', "order_add_monoid_hom.mk'_to_add_monoid_hom"}

===== File mathlib/src/algebra/order/hom/basic.lean =====
Missing aligns: {'abs_sub_map_le_sub', 'map_sub_le_add', 'map_eq_zero_iff_eq_one', 'mul_ring_norm_class', 'map_div_rev', 'map_div_le_add', 'map_eq_zero_iff_eq_zero', 'map_pos_of_ne_one', 'group_seminorm_class', 'map_pos_of_ne_zero', 'le_map_sub_add_map_sub', 'ring_seminorm_class', "le_map_add_map_sub'", 'add_group_seminorm_class', 'mul_ring_seminorm_class', 'map_sub_rev', 'group_norm_class', "le_map_add_map_div'", 'map_ne_zero_iff_ne_one', 'ring_norm_class', 'abs_sub_map_le_div', 'add_group_norm_class', 'map_ne_zero_iff_ne_zero', 'le_map_add_map_sub'}

===== File mathlib/src/algebra/order/field/basic.lean =====
Missing aligns: {'div_le_div_of_mul_sub_mul_div_nonpos', 'order_iso.mul_right₀_apply', 'mul_sub_mul_div_mul_neg', 'inv_nonneg_of_nonneg', 'order_iso.mul_left₀_symm_apply', 'mul_sub_mul_div_mul_nonpos', 'div_lt_div_of_mul_sub_mul_div_neg', 'order_iso.mul_left₀_apply', 'order_iso.mul_right₀_symm_apply', 'inv_pos_of_pos'}

===== File mathlib/src/algebra/order/monoid/nat_cast.lean =====
Missing aligns: {'one_le_two', 'zero_lt_two', 'zero_le_two', 'three_pos', "one_le_two'", 'lt_add_one', "zero_lt_four'", 'lt_one_add', 'two_pos', 'one_lt_two', 'zero_lt_three', 'zero_lt_four', 'four_pos', 'zero_le_four', 'zero_le_three', "zero_lt_three'", "zero_lt_two'"}

===== File mathlib/src/algebra/order/monoid/lemmas.lean =====
Missing aligns: {'lt_of_add_lt_of_nonneg_right', 'mul_lt_of_mul_lt_left', "add_right_cancel''", "mul_lt_one'", 'mul_lt_of_lt_one_of_le', 'add_lt_of_lt_of_nonpos', 'mul_lt_of_mul_lt_right', 'lt_add_of_lt_of_pos', "mul_le_mul_left'", "one_lt_mul''", "le_mul_of_one_le_right'", 'le_of_add_le_of_nonneg_right', 'neg_of_add_lt_left', 'add_le_of_add_le_right', 'lt_add_of_pos_of_lt', 'add_le_add_right', 'eq_zero_of_add_nonneg_right', 'one_lt_of_lt_mul_right', 'le_of_le_mul_of_le_one_left', 'nonneg_of_le_add_right', 'lt_of_lt_mul_of_le_one_left', "mul_le_of_le_one_right'", 'add_lt_add', 'le_of_le_add_of_nonpos_right', 'le_mul_of_le_of_one_le', 'lt_of_mul_lt_of_one_le_right', "one_lt_mul_of_lt_of_le'", 'add_le_add_three', 'eq_zero_of_add_nonpos_left', 'min_le_max_of_mul_le_mul', "lt_of_mul_lt_mul_left'", "add_left_cancel''", "lt_mul_iff_one_lt_right'", 'lt_of_lt_add_of_nonpos_left', 'lt_mul_of_one_lt_of_le', 'add_le_of_nonpos_right', 'add_pos_of_pos_of_nonneg', 'mul_lt_one_of_lt_of_le', 'lt_mul_of_lt_of_one_lt', 'one_lt_of_lt_mul_left', 'le_add_of_nonneg_of_le', "lt_mul_of_lt_of_one_lt'", 'lt_of_lt_mul_of_le_one_right', 'add_lt_add_right', 'lt_add_iff_pos_left', 'add_pos_of_nonneg_of_pos', 'le_add_of_le_add_right', "lt_mul_iff_one_lt_left'", "mul_lt_of_lt_of_lt_one'", 'mul_le_of_le_of_le_one', 'nonpos_of_add_le_right', 'add_lt_iff_neg_left', 'lt_one_of_mul_lt_left', 'add_lt_add_left', 'le_add_iff_nonneg_right', 'le_one_of_mul_le_left', 'lt_add_of_nonneg_of_lt', 'add_lt_add_of_lt_of_le', "mul_le_mul'", 'mul_lt_mul_of_le_of_lt', 'mul_le_mul_iff_right', 'add_lt_of_add_lt_left', 'add_pos', 'mul_le_mul_three', 'add_neg', 'lt_mul_of_le_of_one_lt', 'lt_mul_of_one_le_of_lt', 'add_lt_iff_neg_right', "lt_mul_of_one_lt_of_lt'", 'eq_one_of_one_le_mul_right', 'add_lt_of_add_lt_right', 'lt_of_mul_lt_of_one_le_left', "le_mul_iff_one_le_left'", 'mul_lt_of_lt_of_le_one', "mul_le_mul_right'", 'mul_lt_one', "add_neg'", "add_pos'", 'add_le_add', 'add_nonpos', 'pos_of_lt_add_left', 'neg_of_add_lt_right', 'le_of_mul_le_of_one_le_right', 'add_neg_of_nonpos_of_neg', "mul_lt_iff_lt_one_right'", "mul_left_cancel''", 'add_le_of_le_of_nonpos', 'mul_le_of_mul_le_right', 'add_lt_of_neg_of_lt', 'add_le_of_nonpos_left', "lt_of_mul_lt_mul_right'", "mul_le_iff_le_one_left'", "le_mul_iff_one_le_right'", 'le_of_add_le_add_left', 'add_lt_of_neg_of_le', 'mul_lt_of_le_of_lt_one', 'add_le_add_iff_left', "le_mul_of_one_le_left'", 'le_add_of_nonneg_left', "mul_lt_iff_lt_one_left'", 'add_lt_of_nonpos_of_lt', 'eq_zero_of_add_nonneg_left', 'add_le_of_nonpos_of_le', 'lt_one_of_mul_lt_right', 'mul_lt_of_lt_one_of_lt', 'lt_add_of_pos_right', 'lt_of_lt_add_of_nonpos_right', 'le_of_add_le_add_right', "lt_mul_of_one_lt_right'", "cmp_mul_left'", 'exists_square_le', "mul_le_one'", 'le_of_add_le_of_nonneg_left', 'lt_add_of_pos_of_le', "lt_add_of_pos_of_lt'", 'le_add_of_nonneg_right', 'nonneg_of_le_add_left', 'cmp_add_left', 'lt_add_of_lt_add_left', 'lt_add_of_le_of_pos', "mul_le_iff_le_one_right'", "mul_eq_one_iff'", 'cmp_add_right', "add_lt_of_neg_of_lt'", 'add_lt_add_iff_left', 'add_le_iff_nonpos_left', "add_eq_zero_iff'", 'lt_mul_of_lt_of_one_le', 'add_lt_of_le_of_neg', 'lt_add_of_lt_add_right', "lt_add_of_lt_of_pos'", 'add_nonneg', "lt_mul_of_one_lt_left'", 'add_lt_of_neg_left', 'mul_eq_mul_iff_eq_and_eq', 'add_lt_of_neg_right', 'lt_mul_of_one_lt_of_lt', 'le_one_of_mul_le_right', 'mul_lt_one_of_le_of_lt', 'mul_lt_mul_iff_left', 'min_le_max_of_add_le_add', 'add_le_add_iff_right', 'lt_of_add_lt_of_nonneg_left', "mul_lt_of_lt_one_left'", "mul_lt_of_lt_one_right'", 'mul_lt_mul_iff_right', "mul_le_of_le_one_left'", 'add_le_of_add_le_left', 'lt_add_of_pos_left', "add_lt_of_lt_of_neg'", 'mul_lt_mul_of_lt_of_le', "one_lt_mul_of_le_of_lt'", 'le_add_iff_nonneg_left', 'mul_lt_of_le_one_of_lt', 'mul_le_of_mul_le_left', 'add_le_add_iff_of_ge', 'mul_lt_of_lt_of_lt_one', 'eq_zero_of_add_nonpos_right', 'mul_le_of_le_one_of_le', "le_of_mul_le_mul_right'", "mul_lt_mul_left'", 'le_mul_of_le_mul_left', 'mul_le_mul_iff_left', 'pos_of_lt_add_right', 'add_neg_of_neg_of_nonpos', 'one_le_of_le_mul_left', "cmp_mul_right'", 'lt_of_add_lt_add_left', 'add_lt_add_iff_right', "mul_lt_of_lt_one_of_lt'", 'nonpos_of_add_le_left', 'lt_add_of_lt_of_nonneg', 'le_of_le_mul_of_le_one_right', 'add_lt_add_of_le_of_lt', 'one_le_mul', 'le_add_of_le_of_nonneg', 'add_le_iff_nonpos_right', "mul_lt_mul_right'", "one_lt_mul'", 'le_of_mul_le_of_one_le_left', 'add_le_add_left', "mul_right_cancel''", 'eq_one_of_mul_le_one_left', 'le_mul_of_le_mul_right', 'lt_of_add_lt_add_right', 'add_lt_of_lt_of_neg', 'mul_le_mul_iff_of_ge', 'eq_one_of_one_le_mul_left', 'mul_lt_mul_of_lt_of_lt', 'le_of_le_add_of_nonpos_left', 'lt_mul_of_lt_mul_right', 'eq_one_of_mul_le_one_right', 'lt_mul_of_lt_mul_left', 'add_eq_add_iff_eq_and_eq', 'le_add_of_le_add_left', 'lt_add_iff_pos_right', 'add_lt_add_of_lt_of_lt', 'le_mul_of_one_le_of_le', "le_of_mul_le_mul_left'", 'one_le_of_le_mul_right'}

===== File mathlib/src/algebra/order/monoid/basic.lean =====
Missing aligns: {'order_embedding.add_right_apply', 'function.injective.linear_ordered_add_comm_monoid', 'order_embedding.add_left', 'order_embedding.add_left_apply', 'order_embedding.mul_right_apply', 'order_embedding.add_right', 'order_embedding.mul_left_apply', 'function.injective.ordered_add_comm_monoid'}

===== File mathlib/src/algebra/order/monoid/with_top.lean =====
Missing aligns: {'with_bot.coe_pos', 'with_top.zero_eq_coe', 'zero_hom.with_bot_map', 'with_bot.coe_eq_zero', 'with_top.coe_lt_zero', 'add_hom.with_bot_map_apply', 'one_hom.with_bot_map_apply', 'with_top.coe_zero', 'zero_hom.with_top_map_apply', 'add_monoid_hom.with_bot_map_apply', 'with_top.coe_pos', 'one_hom.with_top_map_apply', 'add_hom.with_top_map_apply', 'with_top.map_zero', 'with_top.zero_ne_top', 'with_top.coe_coe_add_hom', 'with_top.coe_eq_zero', 'with_top.top_ne_zero', 'with_bot.map_zero', 'zero_hom.with_bot_map_apply', 'with_bot.coe_lt_zero', 'zero_hom.with_top_map', 'with_bot.coe_zero', 'add_monoid_hom.with_top_map_apply'}

===== File mathlib/src/algebra/order/monoid/units.lean =====
Missing aligns: {'add_units.coe_lt_coe', 'add_units.coe_le_coe', 'add_units.max_coe', 'add_units.order_embedding_coe_apply', 'add_units.min_coe', 'units.order_embedding_coe_apply'}

===== File mathlib/src/algebra/order/monoid/min_max.lean =====
Missing aligns: {'fn_min_add_fn_max', 'min_add_add_left', 'max_add_add_left', 'min_add_max', 'min_add_add_right', 'min_le_add_of_nonneg_right', 'min_le_add_of_nonneg_left', 'max_add_add_right', 'lt_or_lt_of_add_lt_add', 'add_lt_add_iff_of_le_of_le', 'max_le_add_of_nonneg'}

===== File mathlib/src/algebra/order/monoid/canonical/defs.lean =====
Missing aligns: {'le_of_add_le_left', "min_add_distrib'", 'exists_pos_add_of_lt', 'min_zero', "exists_pos_add_of_lt'", 'le_self_add', 'le_iff_exists_add', 'min_add_distrib', 'zero_le', 'nonpos_iff_eq_zero', 'add_eq_zero_iff', 'le_add_right', 'self_le_add_left', 'zero_min', "le_iff_forall_pos_lt_add'", 'le_of_forall_pos_le_add', 'le_add_left', 'le_add_self', "le_iff_exists_add'", 'self_le_add_right', "le_of_forall_pos_lt_add'", 'pos_iff_ne_zero', 'eq_zero_or_pos', 'bot_eq_zero', 'add_pos_iff', 'lt_iff_exists_add', "bot_eq_zero'", 'le_of_add_le_right'}

===== File mathlib/src/algebra/order/group/order_iso.lean =====
Missing aligns: {'order_iso.add_left_apply', "inv_le_of_inv_le'", 'le_inv_of_le_inv', 'order_iso.mul_left_apply', 'order_iso.mul_right_apply', 'order_iso.inv_apply', 'order_iso.mul_left_to_equiv', 'order_iso.neg_symm_apply', 'order_iso.add_left_to_equiv', 'order_iso.neg_apply', 'neg_le_of_neg_le', 'order_iso.inv_symm_apply', 'order_iso.mul_right_to_equiv', 'order_iso.add_right_to_equiv', 'le_neg_of_le_neg', 'order_iso.add_right_apply'}

===== File mathlib/src/algebra/order/group/abs.lean =====
Missing aligns: {'abs_eq_sup_neg', "apply_abs_le_add_of_nonneg'", 'apply_abs_le_add_of_nonneg'}

===== File mathlib/src/algebra/order/group/inj_surj.lean =====
Missing aligns: {'function.injective.ordered_add_comm_group', 'function.injective.linear_ordered_add_comm_group'}

===== File mathlib/src/algebra/order/group/densely_ordered.lean =====
Missing aligns: {'le_iff_forall_neg_add_le', 'le_of_forall_pos_sub_le', 'le_of_forall_neg_add_le', 'le_iff_forall_pos_le_add'}

===== File mathlib/src/algebra/order/group/defs.lean =====
Missing aligns: {'lt_of_sub_neg', 'add_neg_neg_iff', 'neg_lt_self', 'add_neg_lt_iff_lt_add', 'lt_sub_iff_add_lt', 'neg_neg_of_pos', 'le_neg_iff_add_nonpos_right', 'add_neg_le_add_neg_iff', 'sub_le_self_iff', 'lt_add_neg_iff_add_lt', 'sub_lt_sub', 'ordered_comm_group.le_of_mul_le_mul_left', 'neg_add_lt_of_lt_add', 'sub_le_sub', 'linear_ordered_add_comm_group.add_lt_add_left', 'sub_lt_iff_lt_add', 'sub_le_sub_flip', 'lt_of_inv_lt_inv', 'le_one_of_one_le_inv', 'add_lt_of_lt_neg_add', 'sub_le_sub_iff_left', 'antitone_on.neg', 'le_sub_right_of_add_le', 'mul_le_of_le_inv_mul', 'sub_le_sub_iff', 'lt_sub_comm', 'add_neg_le_iff_le_add', 'lt_neg', 'ordered_comm_group.lt_of_mul_lt_mul_left', 'strict_anti.neg', 'left.neg_nonpos_iff', 'neg_add_nonpos_iff', 'sub_lt_self', 'le_neg_iff_add_nonpos_left', "sub_lt_iff_lt_add'", 'neg_add_neg_iff_lt', 'add_le_of_le_sub_right', 'le_of_sub_nonpos', 'add_lt_of_lt_sub_left', 'neg_le_neg', "neg_add_le_iff_le_add'", 'le_of_forall_pos_lt_add', 'sub_le_sub_iff_right', 'inv_mul_lt_of_lt_mul', 'left.neg_lt_self', 'neg_lt_zero', 'neg_add_le_iff_le_add', 'neg_add_lt_iff_lt_add', "neg_lt_iff_pos_add'", 'neg_nonpos', 'sub_lt_sub_iff', 'sub_le_comm', 'lt_inv_of_lt_inv', 'sub_lt_zero', 'one_lt_of_inv_lt_one', 'le_iff_forall_pos_lt_add', 'neg_pos', 'lt_neg_add_iff_lt', 'left.neg_neg_iff', 'sub_le_self', 'sub_nonpos_of_le', "add_neg_le_iff_le_add'", 'sub_lt_sub_iff_left', 'neg_lt_neg_iff', 'neg_add_neg_iff', 'sub_le_neg_add_iff', 'sub_nonpos', 'add_comm_group.total_positive_cone.to_positive_cone', 'neg_of_neg_pos', 'sub_lt_comm', 'neg_nonneg_of_nonpos', 'le_add_neg_iff_add_le', 'lt_mul_of_inv_mul_lt', 'monotone.neg', 'add_neg_lt_add_neg_iff', 'one_le_of_inv_le_one', 'add_neg_nonpos_iff_le', 'le_sub_comm', 'lt_sub_left_of_add_lt', 'exists_zero_lt', 'sub_le_sub_left', 'left.self_le_neg', 'left.neg_pos_iff', 'lt_mul_of_inv_mul_lt_left', 'cmp_sub_zero', 'strict_mono_on.neg', 'neg_lt_neg', 'le_neg_add_iff_add_le', 'lt_add_neg_iff_lt', 'strict_mono.neg', 'le_neg_add_of_add_le', 'le_add_neg_iff_le', 'sub_le_sub_right', "one_le_inv'", 'lt_of_neg_lt_neg', "lt_sub_iff_add_lt'", 'neg_pos_of_neg', 'sub_pos_of_lt', 'add_le_of_le_neg_add', 'left.self_lt_neg', 'lt_neg_add_iff_add_lt', 'right.self_lt_neg', 'sub_le_iff_le_add', 'lt_neg_add_of_add_lt', 'inv_mul_le_of_le_mul', 'sub_neg_of_lt', 'sub_lt_sub_left', 'neg_le_iff_add_nonneg', 'left.neg_le_self', 'lt_sub_right_of_add_lt', 'neg_lt_iff_pos_add', 'add_neg_lt_neg_add_iff', 'neg_neg_iff_pos', "sub_le_iff_le_add'", 'add_neg_le_neg_add_iff', 'sub_lt_self_iff', "neg_le_iff_add_nonneg'", 'sub_lt_sub_right', 'le_of_sub_nonneg', 'lt_add_of_sub_left_lt', 'strict_anti_on.neg', "inv_lt_of_inv_lt'", 'one_lt_inv_of_inv', 'le_sub_iff_add_le', 'lt_neg_iff_add_neg', 'neg_le_neg_iff', 'right.nonneg_neg_iff', "le_sub_iff_add_le'", 'lt_of_sub_pos', 'le_add_of_sub_left_le', 'neg_lt_sub_iff_lt_add', 'inv_of_one_lt_inv', 'le_of_neg_le_neg', 'right.neg_lt_self', 'lt_add_of_neg_add_lt', 'neg_nonneg', 'nonneg_of_neg_nonpos', 'add_lt_of_lt_sub_right', 'neg_lt_of_neg_lt', 'le_sub_self_iff', "ordered_comm_group.mul_lt_mul_left'", 'neg_lt', 'sub_left_lt_of_lt_add', 'inv_lt_one_iff_one_lt', 'sub_right_lt_of_lt_add', 'right.neg_pos_iff', 'antitone.neg', "inv_lt_one'", 'lt_neg_of_lt_neg', 'neg_le_self', 'sub_lt_sub_iff_right', "neg_add_lt_iff_lt_add'", 'pos_of_neg_neg', 'lt_add_of_neg_add_lt_left', 'le_sub_left_of_add_le', 'sub_nonneg', 'sub_pos', "neg_le_sub_iff_le_add'", 'monotone_on.neg', 'eq_zero_of_neg_eq', "neg_lt_sub_iff_lt_add'", 'add_neg_nonpos_iff', 'le_inv_mul_of_mul_le', 'ordered_add_comm_group.le_of_add_le_add_left', 'neg_le_sub_iff_le_add', "inv_le_one'", 'sub_left_le_of_le_add', 'ordered_add_comm_group.lt_of_add_lt_add_left', 'ordered_add_comm_group.add_lt_add_left', 'mul_lt_of_lt_inv_mul', 'lt_inv_mul_of_mul_lt', 'right.self_le_neg', 'sub_nonneg_of_le', 'add_le_of_le_sub_left', 'nonpos_of_neg_nonneg', 'le_neg_add_iff_le', 'right.neg_le_self', 'left.nonneg_neg_iff', "lt_neg_iff_add_neg'", 'right.neg_nonpos_iff', "add_neg_lt_iff_le_add'", 'lt_add_of_sub_right_lt', 'sub_neg', 'neg_nonpos_of_nonneg', "one_lt_inv'", 'right.neg_neg_iff'}

===== File mathlib/src/algebra/order/group/min_max.lean =====
Missing aligns: {'max_zero_sub_max_neg_zero_eq_self', 'max_sub_sub_left', 'min_sub_sub_right', 'min_sub_sub_left', 'max_zero_sub_eq_self', 'min_neg_neg', 'max_neg_neg', 'max_sub_sub_right'}

===== File mathlib/src/algebra/homology/complex_shape.lean =====
Missing aligns: {'complex_shape.up_rel', 'complex_shape', "complex_shape.down'_mk", "complex_shape.next_eq'", 'complex_shape.refl_rel', 'complex_shape.symm_symm', "complex_shape.down'_rel", 'complex_shape.symm_rel', "complex_shape.up'", "complex_shape.up'_rel", 'complex_shape.prev', 'complex_shape.ext', 'complex_shape.ext_iff', 'complex_shape.trans', 'complex_shape.refl', 'complex_shape.down_rel', "complex_shape.prev_eq'", 'complex_shape.down_mk', 'complex_shape.down', 'complex_shape.symm', "complex_shape.down'", 'complex_shape.up', 'complex_shape.next'}

===== File mathlib/src/algebra/group_power/lemmas.lean =====
Missing aligns: {'int.nat_abs_pow_two', 'int.abs_le_self_pow_two', 'int.le_self_pow_two', 'units.coe_inv_of_pow_eq_one', 'add_units.coe_neg_of_nsmul_eq_zero', 'units.coe_of_pow_eq_one', 'add_units.of_nsmul', 'add_units.coe_of_nsmul_eq_zero'}
Phantom aligns: {'units.of_nsmul'}

===== File mathlib/src/algebra/group_power/order.lean =====
Missing aligns: {'min_lt_max_of_mul_lt_mul', 'nsmul_nonneg', 'min_le_of_add_le_two_nsmul', 'min_lt_max_of_add_lt_add', 'lt_max_of_two_nsmul_lt_add', 'monotone.pow_right', 'strict_mono.nsmul_left', 'left.pow_nonneg', 'min_lt_of_add_lt_two_nsmul', 'left.pow_nonpos', 'nsmul_le_nsmul_of_nonpos', 'right.nsmul_neg_iff', 'min_le_of_mul_le_sq', 'nsmul_nonpos_iff', 'nsmul_pos_iff', 'le_max_of_two_nsmul_le_add', 'min_lt_of_mul_lt_sq', 'nsmul_strict_mono_left', 'right.pow_nonneg', "pow_strict_mono_right'", 'le_of_nsmul_le_nsmul', "le_of_pow_le_pow'", 'right.pow_neg', 'nsmul_lt_nsmul_iff', 'right.pow_nonpos', 'left.pow_neg', 'pow_strict_mono_right', 'nsmul_pos', 'nsmul_nonneg_iff', "lt_of_pow_lt_pow'", 'nsmul_le_nsmul_of_le_right', 'nsmul_nonpos', 'lt_of_nsmul_lt_nsmul', 'pow_two_pos_of_ne_zero', 'lt_max_of_sq_lt_mul', 'nsmul_eq_zero_iff', 'nsmul_strict_mono_right', 'two_mul_le_add_pow_two', 'pow_mono_right', 'zsmul_nonneg', 'pow_two_nonneg', 'nsmul_neg', 'nsmul_neg_iff', 'left.nsmul_neg_iff', 'nsmul_lt_nsmul', 'nsmul_le_nsmul', 'nsmul_le_nsmul_iff', 'le_max_of_sq_le_mul', "strict_mono.pow_right'", 'nsmul_mono_left', 'monotone.nsmul_left'}
Phantom aligns: {'strict_mono_pow'}

===== File mathlib/src/algebra/group_power/identities.lean =====
Missing aligns: {'sq_add_sq_mul_sq_add_sq', 'pow_four_add_four_mul_pow_four', 'sum_eight_sq_mul_sum_eight_sq', "pow_four_add_four_mul_pow_four'", 'sq_add_mul_sq_mul_sq_add_mul_sq', 'sum_four_sq_mul_sum_four_sq'}

===== File mathlib/src/algebra/group_power/basic.lean =====
Missing aligns: {'sq', 'add_nsmul', 'pow_monoid_hom_apply', 'one_nsmul', 'has_dvd.dvd.pow', 'zsmul_add_group_hom_apply', 'pow_one', 'zpow_group_hom_apply', 'nsmul_zero', 'pow_add', 'nsmul_add_monoid_hom_apply', 'one_pow', 'zsmul_neg'}

===== File mathlib/src/algebra/group_power/ring.lean =====
Missing aligns: {'zero_pow_eq_zero', 'pow_eq_zero', 'add_pow_two', 'commute.sq_sub_sq', "zero_pow'", 'sq_sub_sq', 'neg_one_pow_eq_or', 'min_pow_dvd_add', 'pow_eq_zero_of_le', 'mul_neg_one_pow_eq_zero_iff', 'units.eq_or_eq_neg_of_sq_eq_sq', 'neg_one_pow_two', "pow_eq_zero_iff'", 'pow_ne_zero_iff', 'sub_pow_two', 'zero_pow_eq', 'ring.inverse_pow', 'neg_pow_two', 'pow_two_sub_pow_two', 'sq_eq_sq_iff_eq_or_eq_neg', 'zero_pow', 'neg_sq', 'eq_or_eq_neg_of_sq_eq_sq', 'pow_eq_zero_iff', 'pow_monoid_with_zero_hom', 'units.sq_eq_sq_iff_eq_or_eq_neg', 'sub_sq', 'neg_one_sq', 'neg_pow', 'neg_one_pow_mul_eq_zero_iff', 'pow_dvd_pow_iff', "sub_sq'"}

===== File mathlib/src/algebra/hom/group_instances.lean =====
Missing aligns: {'monoid_hom.comp_hom_apply_apply', 'add_monoid_hom.flip_apply', 'add_monoid_hom.compr₂', 'add_monoid_hom.map_one₂', 'add_monoid.End.mul_left_apply_apply', 'add_monoid_hom.compl₂_apply', 'add_monoid_hom.compr₂_apply', 'add_monoid_hom.ext_iff₂', 'monoid_hom.flip_hom_apply', 'add_monoid_hom.comp_hom_apply_apply', 'add_monoid_hom.map_div₂', 'add_monoid_hom.flip_hom_apply', "monoid_hom.comp_hom'_apply_apply", 'add_monoid_hom.flip_hom', 'add_monoid_hom.map_mul₂', 'add_monoid_hom.flip', "add_monoid_hom.comp_hom'_apply_apply", 'add_monoid_hom.compl₂', 'add_monoid_hom.comp_hom', 'add_monoid_hom.eval_apply_apply', 'add_monoid_hom.eval', 'add_monoid_hom.map_inv₂', 'monoid_hom.eval_apply_apply', 'add_monoid.End.mul_right_apply_apply', "add_monoid_hom.comp_hom'"}

===== File mathlib/src/algebra/hom/iterate.lean =====
Missing aligns: {'nsmul_iterate', 'add_monoid_hom.iterate_map_nsmul'}

===== File mathlib/src/algebra/hom/group.lean =====
Missing aligns: {'monoid_hom.to_mul_hom', 'monoid_with_zero_hom.coe_eq_to_zero_hom', 'monoid_with_zero_hom.id_apply', "monoid_hom.mk'_apply", 'monoid_hom.coe_eq_to_mul_hom', 'add_monoid_hom.to_add_hom', 'map_zsmul', 'one_hom.id_apply', 'monoid_with_zero_hom.to_zero_hom', 'add_monoid_hom.coe_eq_to_zero_hom', 'add_hom.coe_copy_eq', 'zero_hom.coe_copy_eq', 'monoid_with_zero_hom.to_fun_eq_coe', 'zero_hom.to_fun_eq_coe', 'add_monoid_hom.of_map_add_neg', 'one_hom.to_fun_eq_coe', 'mul_hom.coe_copy', 'mul_hom.to_fun_eq_coe', 'monoid_with_zero_hom.coe_copy', 'mul_hom.coe_copy_eq', "add_monoid_hom.map_zsmul'", 'monoid_hom.to_fun_eq_coe', 'zero_hom.coe_copy', 'add_monoid_hom.to_zero_hom', 'zero_hom.id_apply', 'add_monoid_hom.id_apply', "add_monoid_hom.mk'_apply", 'add_monoid_hom.coe_copy', 'add_monoid_hom.copy_eq', 'add_hom.to_fun_eq_coe', 'monoid_with_zero_hom.to_monoid_hom', 'monoid_hom.coe_eq_to_one_hom', 'monoid_hom.id_apply', 'mul_hom.id_apply', 'add_hom.id_apply', 'one_hom.coe_copy_eq', 'monoid_with_zero_hom.copy_eq', 'monoid_hom.copy_eq', 'add_monoid_hom.to_fun_eq_coe', 'map_zsmul.aux', 'one_hom.coe_copy', 'monoid_hom.to_one_hom', "map_zsmul'", 'monoid_hom.coe_copy', 'add_monoid_hom.coe_eq_to_add_hom', 'map_nsmul.aux', 'monoid_with_zero_hom.coe_eq_to_monoid_hom', 'add_hom.coe_copy'}
Phantom aligns: {'zero_hom_class.map_zero', "zero_hom.map_zero'"}

===== File mathlib/src/algebra/hom/centroid.lean =====
Missing aligns: {'centroid_hom.to_add_monoid_hom', 'centroid_hom.to_fun_eq_coe'}

===== File mathlib/src/algebra/hom/embedding.lean =====
Missing aligns: {'mul_left_embedding_apply', 'mul_left_embedding_eq_mul_right_embedding', 'add_left_embedding_eq_add_right_embedding', 'add_left_embedding_apply', 'add_right_embedding_apply', 'mul_right_embedding_apply'}

===== File mathlib/src/algebra/hom/aut.lean =====
Missing aligns: {'add_aut'}

===== File mathlib/src/algebra/hom/units.lean =====
Missing aligns: {"is_add_unit.coe_neg_add_unit'", "is_add_unit.coe_add_unit'", "is_unit.coe_unit'", "is_unit.coe_inv_unit'"}

===== File mathlib/src/algebra/hom/commute.lean =====
Missing aligns: {'add_semiconj_by.map', 'add_commute.map'}

===== File mathlib/src/algebra/hom/ring.lean =====
Missing aligns: {'ring_hom.to_non_unital_ring_hom', 'non_unital_ring_hom.to_mul_hom', 'ring_hom.map_bit0', 'ring_hom.map_bit1', 'non_unital_ring_hom.to_add_monoid_hom', 'map_bit1', 'ring_hom.to_monoid_with_zero_hom', 'ring_hom.to_add_monoid_hom', 'ring_hom.to_monoid_hom'}

===== File mathlib/src/algebra/hom/group_action.lean =====
Missing aligns: {'mul_semiring_action_hom.to_distrib_mul_action_hom', 'mul_action_hom.inverse_to_fun', 'distrib_mul_action_hom.to_add_monoid_hom', 'distrib_mul_action_hom.inverse_to_fun', 'mul_semiring_action_hom.to_ring_hom', 'distrib_mul_action_hom.to_mul_action_hom'}

===== File mathlib/src/algebra/hom/equiv/basic.lean =====
Missing aligns: {'add_equiv.arrow_congr_apply', 'mul_equiv.to_equiv', 'mul_equiv.Pi_congr_right_apply', 'add_equiv.coe_to_add_hom', 'add_equiv.Pi_congr_right_apply', 'add_equiv.to_equiv', 'add_monoid_hom.inverse_apply', 'monoid_hom.inverse_apply', 'add_equiv.to_add_hom', 'mul_equiv.to_mul_hom', 'mul_equiv.arrow_congr_apply'}

===== File mathlib/src/algebra/hom/equiv/units/group_with_zero.lean =====
Missing aligns: {'equiv.mul_right₀_symm_apply', 'equiv.mul_right₀_apply', 'equiv.mul_left₀_apply', 'equiv.mul_left₀_symm_apply'}

===== File mathlib/src/algebra/hom/equiv/units/basic.lean =====
Missing aligns: {'equiv.div_left_symm_apply', 'equiv.sub_left_apply', 'equiv.sub_left_symm_apply', 'add_units.add_left_apply', 'equiv.div_right_apply', 'equiv.div_right_symm_apply', 'units.mul_left_apply', 'add_units.add_right_apply', 'equiv.sub_right_symm_apply', 'units.mul_right_apply', 'equiv.div_left_apply', 'equiv.sub_right_apply'}

===== File mathlib/src/algebra/field/basic.lean =====
Missing aligns: {'one_div_mul_add_mul_one_div_eq_one_div_add_one_div', "div_sub'", "sub_div'", 'to_dual_rat_cast', 'neg_div_self', 'neg_div_neg_eq', 'sub_div', 'same_add_div', "div_add'", 'neg_div', 'inv_neg', 'div_sub_one', "add_div'", 'div_add_div_same', 'div_sub_div_same', 'neg_inv', 'one_sub_div', 'div_neg', 'one_div_add_one_div', 'div_add_one', 'div_add_same', 'to_lex_rat_cast', "inv_sub_inv'", "neg_div'", 'add_div_eq_mul_add_div', 'of_lex_rat_cast', 'same_sub_div', 'div_neg_self', 'div_sub_div', 'of_dual_rat_cast', 'one_add_div', 'div_sub_same', 'div_add_div', 'one_div_mul_sub_mul_one_div_eq_one_div_add_one_div', 'inv_sub_inv', 'one_div_neg_one_eq_neg_one', 'inv_add_inv', 'div_neg_eq_neg_div', 'add_div', 'one_div_neg_eq_neg_one_div'}

===== File mathlib/src/algebra/field/defs.lean =====
Phantom aligns: {'division_ring.rat_cast_mk'}

===== File mathlib/src/algebra/euclidean_domain/defs.lean =====
Phantom aligns: {'euclidean_domain.r_well_founded', 'euclidean_domain.r', 'euclidean_domain.quotient', 'euclidean_domain.quotient_zero', 'euclidean_domain.remainder_lt', 'euclidean_domain.remainder', 'euclidean_domain.quotient_mul_add_remainder_eq', 'euclidean_domain.mul_left_not_lt'}

===== File mathlib/src/algebra/char_zero/lemmas.lean =====
Missing aligns: {'nat.cast_embedding_apply'}

===== File mathlib/src/algebra/gcd_monoid/basic.lean =====
Missing aligns: {'associates_equiv_of_unique_units_symm_apply', 'associates_equiv_of_unique_units_apply'}

===== File mathlib/src/algebra/group/ext.lean =====
Missing aligns: {'add_cancel_monoid.to_left_cancel_add_monoid_injective', 'add_right_cancel_monoid.ext', 'add_group.ext', 'add_monoid.ext', 'add_comm_monoid.to_add_monoid_injective', 'add_comm_monoid.ext', 'add_cancel_comm_monoid.to_add_comm_monoid_injective', 'sub_neg_monoid.ext', 'add_left_cancel_monoid.ext', 'add_comm_group.ext', 'add_cancel_comm_monoid.ext', 'add_cancel_monoid.ext', 'add_right_cancel_monoid.to_add_monoid_injective', 'add_left_cancel_monoid.to_add_monoid_injective'}

===== File mathlib/src/algebra/group/type_tags.lean =====
Missing aligns: {"add_monoid_hom.to_multiplicative''_symm_apply_apply", 'monoid_hom.to_additive_apply_apply', 'add_monoid_hom.to_multiplicative_apply_apply', "monoid_hom.to_additive'_apply_apply", "add_monoid_hom.to_multiplicative''_apply_apply", "add_monoid_hom.to_multiplicative'_apply_apply", 'add_monoid_hom.to_multiplicative_symm_apply_apply', "monoid_hom.to_additive''_apply_apply", "monoid_hom.to_additive''_symm_apply_apply", "monoid_hom.to_additive'_symm_apply_apply", 'monoid_hom.to_additive_symm_apply_apply', "add_monoid_hom.to_multiplicative'_symm_apply_apply"}

===== File mathlib/src/algebra/group/order_synonym.lean =====
Missing aligns: {"to_lex_smul'", "of_lex_smul'"}

===== File mathlib/src/algebra/group/ulift.lean =====
Missing aligns: {'add_equiv.ulift'}
Phantom aligns: {'ulift.add_cancel_comm_monoid'}

===== File mathlib/src/algebra/group/inj_surj.lean =====
Missing aligns: {'function.injective.add_comm_group_with_one', 'function.injective.cancel_monoid', 'function.surjective.add_comm_group_with_one', 'function.injective.add_comm_monoid_with_one', 'function.surjective.add_comm_monoid_with_one'}

===== File mathlib/src/algebra/group/semiconj.lean =====
Missing aligns: {'add_semiconj_by', 'add_semiconj_by.add_right', 'add_semiconj_by.eq'}

===== File mathlib/src/algebra/group/opposite.lean =====
Missing aligns: {'add_equiv.mul_op_apply', 'add_hom.mul_op_apply_apply', 'mul_opposite.op_add_equiv_symm_apply', 'add_hom.mul_op_symm_apply_apply', "mul_equiv.inv'_symm_apply", 'add_opposite.op_mul_equiv_symm_apply', 'add_equiv.op_symm_apply_symm_apply', 'add_equiv.op_apply_symm_apply', 'add_monoid_hom.mul_op_symm_apply_apply', 'add_equiv.mul_op_symm_apply', 'mul_equiv.op_symm_apply_apply', 'monoid_hom.op_apply_apply', 'add_hom.to_opposite_apply', 'add_equiv.op_symm_apply_apply', 'add_hom.from_opposite_apply', 'mul_equiv.op_apply_apply', 'mul_hom.op_symm_apply_apply', 'add_monoid_hom.op_symm_apply_apply', 'monoid_hom.to_opposite_apply', 'monoid_hom.from_opposite_apply', 'add_monoid_hom.mul_op_apply_apply', 'mul_hom.to_opposite_apply', 'mul_hom.from_opposite_apply', 'add_monoid_hom.from_opposite_apply', 'add_hom.op_symm_apply_apply', 'add_monoid_hom.to_opposite_apply', "add_equiv.neg'_apply", 'mul_opposite.op_add_equiv_apply', 'add_monoid_hom.op_apply_apply', 'add_hom.op_apply_apply', 'add_equiv.op_apply_apply', "add_equiv.neg'_symm_apply", 'mul_equiv.op_symm_apply_symm_apply', 'monoid_hom.op_symm_apply_apply', 'mul_hom.op_apply_apply', "mul_equiv.inv'_apply", 'add_opposite.op_mul_equiv_apply', 'mul_equiv.op_apply_symm_apply'}

===== File mathlib/src/algebra/group/basic.lean =====
Missing aligns: {'sub_sub_eq_add_sub', 'add_eq_of_eq_sub', 'add_neg_eq_zero', 'inv_mul_eq_iff_eq_mul', "add_sub_cancel'_right", "div_div_div_cancel_right'", 'mul_eq_one_iff_inv_eq', 'comp_mul_left', 'inv_comp_inv', 'neg_add_eq_sub', 'sub_eq_of_eq_add', 'div_ne_one', 'sub_add_sub_comm', 'eq_one_div_of_mul_eq_one_left', 'sub_sub_sub_cancel_right', 'div_eq_iff_eq_mul', 'eq_neg_add_of_add_eq', 'mul_div_left_comm', 'mul_div', 'one_eq_inv', 'div_div_cancel', 'mul_one_div', 'sub_add', 'div_right_comm', 'eq_add_of_neg_add_eq', 'sub_add_add_cancel', 'sub_eq_neg_self', 'div_left_injective', 'add_eq_zero_iff_eq_neg', "div_mul_cancel''", "add_rotate'", 'comp_assoc_right', 'exists_npow_eq_one_of_zpow_eq_one', 'mul_left_surjective', 'div_eq_self', 'add_sub_add_comm', 'div_eq_one', 'add_eq_of_eq_add_neg', 'sub_add_eq_sub_sub_swap', 'sub_add_comm', 'mul_rotate', 'sub_neg_eq_add', 'mul_eq_one_iff_eq_inv', 'eq_neg_of_add_eq_zero_left', 'inv_div_left', 'multiplicative_of_symmetric_of_is_total', 'eq_mul_of_div_eq', 'zero_sub_zero_sub', 'zero_sub_zero', 'inv_surjective', 'sub_add_sub_cancel', 'comp_mul_right', 'neg_eq_zero', 'add_zero_eq_id', 'inv_eq_one_div', 'bit0_sub', 'div_mul_eq_div_mul_one_div', 'neg_add_eq_zero', 'sub_ne_zero', 'comp_add_left', 'one_div_mul_one_div_rev', 'bit0_neg', 'sub_sub_self', "eq_mul_of_div_eq'", 'div_left_inj', 'div_eq_div_mul_div', 'inv_eq_iff_mul_eq_one', 'div_eq_inv_mul', 'div_right_injective', 'neg_inj', 'eq_add_neg_of_add_eq', 'sub_eq_sub_add_sub', 'eq_inv_mul_of_mul_eq', 'mul_right_surjective', 'one_div_one', 'div_inv_eq_mul', 'add_add_add_comm', 'add_left_surjective', 'one_div_div', "mul_div_cancel''", "div_self'", 'add_neg_eq_iff_eq_add', 'neg_add_eq_of_eq_add', 'eq_iff_eq_of_sub_eq_sub', "eq_div_of_mul_eq'", 'eq_neg_iff_add_eq_zero', "eq_div_iff_mul_eq'", 'neg_eq_of_add_eq_zero_left', 'one_div', 'add_sub_sub_cancel', 'mul_inv_eq_of_eq_mul', 'eq_inv_of_eq_inv', 'one_div_mul_one_div', 'neg_sub_left', 'eq_of_zero_sub_eq_zero_sub', 'div_div', "mul_rotate'", 'sub_sub', 'mul_eq_of_eq_mul_inv', 'add_zero_sub', 'eq_of_one_div_eq_one_div', "div_eq_of_eq_mul''", 'sub_add_eq_sub_add_zero_sub', "div_mul_div_cancel'", "mul_mul_inv_cancel'_right", 'eq_of_div_eq_one', 'sub_eq_zero', 'sub_right_inj', 'eq_add_of_add_neg_eq', 'exists_nsmul_eq_zero_of_zsmul_eq_zero', 'add_sub_cancel', 'mul_left_comm', 'mul_eq_of_eq_div', 'neg_comp_neg', 'eq_neg_of_add_eq_zero_right', 'div_mul_eq_div_div', 'mul_inv_eq_one', 'div_div_eq_mul_div', 'sub_sub_sub_comm', 'self_eq_add_right', 'eq_one_iff_eq_one_of_mul_eq_one', "mul_div_cancel'''", 'add_sub_add_left_eq_sub', "mul_div_cancel'_right", 'eq_one_div_of_mul_eq_one_right', "eq_sub_of_add_eq'", 'zero_sub_sub', 'self_eq_mul_right', 'sub_left_inj', 'inv_mul_eq_of_eq_mul', 'comp_assoc_left', 'eq_mul_inv_iff_mul_eq', 'neg_surjective', 'neg_involutive', "sub_eq_iff_eq_add'", 'div_div_div_cancel_left', 'add_eq_of_eq_neg_add', 'eq_inv_of_mul_eq_one_right', 'sub_sub_cancel_left', 'sub_right_injective', 'zero_sub_add_zero_sub_rev', 'sub_sub_sub_eq', "neg_sub'", 'zero_add_eq_id', 'add_sub_assoc', 'inv_unique', 'sub_ne_zero_of_ne', 'neg_ne_zero', 'eq_sub_of_add_eq', 'mul_div_assoc', 'inv_eq_of_mul_eq_one_left', 'div_mul_eq_mul_div', 'mul_right_eq_self', 'neg_eq_zero_sub', 'add_left_comm', "div_mul_div_cancel''", 'eq_mul_inv_of_mul_eq', 'sub_add_cancel', 'comp_add_right', "div_eq_of_eq_mul'", 'eq_neg_iff_eq_neg', 'one_div_one_div', 'ite_zero_add', 'sub_zero', "sub_add_cancel'", 'add_sub_right_comm', 'mul_eq_of_eq_inv_mul', 'mul_mul_mul_comm', 'neg_injective', 'mul_div_div_cancel', 'neg_sub_neg', "add_add_neg_cancel'_right", 'inv_mul_eq_div', 'inv_div', 'div_mul', 'div_mul_eq_div_div_swap', 'div_eq_div_iff_div_eq_div', 'sub_eq_sub_iff_sub_eq_sub', 'add_comm_sub', 'sub_add_eq_sub_sub', "mul_eq_of_eq_div'", "neg_add'", 'eq_mul_of_mul_inv_eq', 'eq_iff_eq_of_div_eq_div', "add_sub_cancel'", 'self_eq_add_left', "div_eq_iff_eq_mul'", 'eq_zero_sub_of_add_eq_zero_right', "inv_div'", "eq_div_iff_mul_eq''", "add_sub_assoc'", 'mul_comm_div', 'div_div_cancel_left', 'neg_neg_sub_neg', 'eq_neg_of_eq_neg', 'neg_add', 'mul_div_right_comm', 'div_eq_one_of_eq', 'neg_eq_iff_add_eq_zero', 'neg_add_eq_iff_eq_add', 'sub_eq_add_zero_sub', 'ite_one_mul', 'add_eq_zero_iff_neg_eq', 'additive_of_symmetric_of_is_total', 'div_mul_div_comm', 'eq_zero_iff_eq_zero_of_add_eq_zero', 'div_eq_mul_one_div', 'self_eq_mul_left', 'one_mul_eq_id', 'add_neg_eq_of_eq_add', 'bit1_sub', 'add_right_comm', 'ite_mul_one', 'mul_one_eq_id', 'sub_eq_sub_iff_add_eq_add', 'sub_sub_sub_cancel_left', "mul_div_assoc'", 'eq_inv_iff_eq_inv', "div_div_self'", 'sub_eq_zero_of_eq', 'div_one', 'mul_mul_div_cancel', 'sub_left_injective', 'neg_unique', 'div_eq_inv_self', 'mul_right_comm', 'add_left_eq_self', 'div_eq_div_iff_mul_eq_mul', 'sub_right_comm', 'inv_inv_div_inv', 'add_right_surjective', 'sub_eq_self', 'mul_inv_eq_iff_eq_mul', 'inv_involutive', 'mul_div_mul_comm', 'eq_mul_of_inv_mul_eq', 'zero_sub', 'eq_of_sub_eq_zero', 'inv_ne_one', 'add_sub', 'neg_sub', 'add_sub_add_right_eq_sub', 'neg_eq_iff_neg_eq', 'zero_eq_neg', 'add_right_eq_self', "eq_div_of_mul_eq''", "div_mul_cancel'", 'eq_add_neg_iff_add_eq', 'mul_div_mul_right_eq_div', 'div_ne_one_of_ne', 'inv_mul_eq_one', 'div_div_div_eq', 'inv_eq_iff_inv_eq', 'sub_eq_iff_eq_add', 'eq_add_of_sub_eq', 'sub_eq_neg_add', 'div_mul_comm', 'ite_add_zero', 'inv_eq_one', 'mul_div_mul_left_eq_div', 'div_mul_mul_cancel', "eq_add_of_sub_eq'", 'eq_inv_iff_mul_eq_one', 'inv_injective', 'mul_left_eq_self', 'eq_inv_mul_iff_mul_eq', "add_eq_of_eq_sub'", 'add_rotate', "eq_sub_iff_add_eq'", 'sub_add_eq_add_sub', "sub_add_sub_cancel'", 'add_sub_left_comm', "inv_mul'", 'sub_sub_cancel', 'sub_self', "sub_eq_of_eq_add'", 'inv_div_inv', 'inv_inj', 'div_right_inj', 'eq_neg_add_iff_add_eq', 'div_div_div_comm', 'eq_sub_iff_add_eq', 'eq_zero_sub_of_add_eq_zero_left', 'eq_inv_of_mul_eq_one_left', 'mul_inv', 'add_add_sub_cancel', 'zero_sub_add_zero_sub'}

===== File mathlib/src/algebra/group/prod.lean =====
Missing aligns: {'mul_monoid_hom_apply', 'units.embed_product_apply', 'mul_monoid_with_zero_hom_apply', 'div_monoid_with_zero_hom_apply', 'sub_add_monoid_hom_apply', 'div_monoid_hom_apply', 'add_add_hom_apply', 'add_add_monoid_hom_apply', 'mul_mul_hom_apply', 'add_units.embed_product_apply'}

===== File mathlib/src/algebra/group/units.lean =====
Missing aligns: {'units.mul_eq_one_iff_inv_eq', 'divp_mul_divp', 'is_add_unit.add', 'divp_assoc', 'units.mul_eq_one_iff_eq_inv', 'units.mul_inv_eq_one', 'is_unit.mul_right_inj', 'add_units.add_left_inj', 'add_units.add_neg_eq_iff_eq_add', 'add_units.neg_add_eq_iff_eq_add', 'is_add_unit.add_left_injective', 'is_add_unit.add_right_inj', 'units.inv_mul_eq_iff_eq_mul', 'is_unit.mul_right_injective', 'is_add_unit.add_right_injective', 'add_units.add_right_inj', 'is_add_unit', 'eq_divp_iff_mul_eq', 'divp_mul_cancel', 'unique_has_zero', 'is_unit.mul_left_cancel', 'units.inv_unique', 'is_unit.exists_left_inv', 'is_unit.unit_spec', 'is_unit.mul_right_cancel', 'add_units.neg_add_eq_zero', "divp_assoc'", 'add_units.eq_add_neg_iff_add_eq', 'add_units.coe_copy', 'is_add_unit.add_unit_spec', 'add_units.add_neg_eq_zero', 'divp_eq_iff_mul_eq', 'mul_divp_cancel', 'add_units.neg_eq_of_add_eq_zero_right', 'divp_eq_one_iff_eq', 'is_add_unit.add_neg_cancel', 'is_unit.mul_left_inj', 'units.eq_inv_of_mul_eq_one_left', 'divp_one', 'divp_eq_divp_iff', 'units.coe_inv_copy', 'units.mul_inv_eq_iff_eq_mul', 'units.eq_mul_inv_iff_mul_eq', 'divp', 'is_add_unit.add_left_cancel', 'is_unit', 'is_unit.mul_inv_cancel', 'inv_eq_one_divp', 'units.eq_inv_of_mul_eq_one_right', "is_add_unit.exists_neg'", 'is_unit.inv_mul_cancel', 'add_units.neg_eq_of_add_eq_zero_left', 'add_units.eq_neg_of_add_eq_zero_left', 'add_units.coe_mk_of_add_eq_zero', 'units.mul_left_inj', 'divp_left_inj', 'add_units.coe_neg_copy', 'divp_mul_eq_mul_divp', 'add_units.neg_unique', 'units.inv_eq_of_mul_eq_one_right', 'units.inv_mul_eq_one', 'units.mk_of_mul_eq_one', 'units.coe_copy', 'is_unit.exists_right_inv', 'is_unit.mul', 'add_units.eq_neg_add_iff_add_eq', 'is_add_unit.neg_add_cancel', 'divp_self', "inv_eq_one_divp'", 'add_units.add_eq_zero_iff_neg_eq', 'units.inv_eq_of_mul_eq_one_left', 'add_units.eq_neg_of_add_eq_zero_right', 'add_units.coe_neg', 'add_units.add_eq_zero_iff_eq_neg', 'units.mul_right_inj', 'is_unit.mul_left_injective', 'is_add_unit.add_left_inj', 'is_add_unit.exists_neg', 'divp_inv', 'one_divp', 'divp_divp_eq_divp_mul', 'is_add_unit.add_right_cancel', 'add_units.mk_of_add_eq_zero', 'units.eq_inv_mul_iff_mul_eq'}
Phantom aligns: {'units.inv', 'units.val_inv', 'units.inv_val', 'add_units.neg', 'units.val', 'add_units.neg_val', 'add_units.val_neg', 'add_units.val'}

===== File mathlib/src/algebra/group/pi.lean =====
Missing aligns: {'pi.eval_add_hom_apply', 'pi.mul_hom_apply', 'pi.eval_mul_hom_apply', 'pi.const_add_monoid_hom_apply', 'add_monoid_hom.coe_fn_apply', 'mul_hom.comp_left_apply', 'add_hom.coe_fn_apply', 'add_monoid_hom.comp_left_apply', 'pi.const_monoid_hom_apply', 'pi.const_add_hom_apply', 'pi.monoid_hom_apply', 'pi.add_hom_apply', 'function.extend_by_one.hom_apply', 'pi.add_monoid_hom_apply', 'mul_hom.single_apply', 'pi.const_mul_hom_apply', 'pi.eval_monoid_hom_apply', 'mul_hom.coe_fn_apply', 'add_hom.comp_left_apply', 'function.extend_by_zero.hom_apply', 'monoid_hom.coe_fn_apply', 'monoid_hom.comp_left_apply', 'pi.eval_add_monoid_hom_apply'}

===== File mathlib/src/algebra/group/commute.lean =====
Missing aligns: {'commute.pow_self'}

===== File mathlib/src/algebra/group/defs.lean =====
Missing aligns: {'right_cancel_monoid', 'division_def', 'right_cancel_semigroup.ext', 'sub_neg_monoid', 'add_left_cancel_semigroup.ext', 'add_right_cancel_monoid', 'right_add', 'add_comm_semigroup.is_right_cancel_add.to_is_left_cancel_add', 'add_cancel_monoid', 'add_comm_group.to_add_group_injective', 'div_inv_one_monoid', 'inv_mul_cancel_right', 'add_ne_add_left', 'mul_inv_rev', 'mul_one', 'mul_right_cancel_iff', 'succ_nsmul', 'mul_right_injective', 'neg_add_self', 'semigroup.ext_iff', 'sub_neg_zero_monoid', 'add_comm_semigroup', 'comm_semigroup.ext_iff', 'subtraction_monoid', 'coe_nat_zsmul', 'cancel_monoid', 'add_group', 'mul_comm', 'npow_rec', 'add_right_cancel_semigroup.ext_iff', 'zero_add', 'monoid', 'add_zero_class', 'add_right_injective', 'mul_right_inv', 'add_group.to_add_monoid', 'mul_ne_mul_left', 'sub_eq_add_neg', 'zero_zsmul', 'left_neg_eq_right_neg', 'inv_inv', 'neg_eq_of_add_eq_zero_right', 'neg_add_cancel_right', 'neg_add_cancel_left', 'add_right_cancel_semigroup.ext', 'add_comm_semigroup.ext_iff', 'inv_one_class', 'is_right_cancel_add', 'add_ne_add_right', 'is_left_cancel_add', 'mul_inv_cancel_left', 'inv_one', 'comm_monoid', 'left_cancel_semigroup.ext', 'add_right_inj', 'comm_semigroup', 'mul_left_injective', 'inv_eq_of_mul_eq_one_right', 'mul_assoc', 'mul_ne_mul_right', 'mul_right_cancel', 'division_monoid', 'left_cancel_semigroup', 'add_right_cancel_iff', 'add_left_inj', 'add_right_cancel', 'nsmul_eq_smul', 'add_comm_semigroup.ext', 'is_cancel_mul', 'add_semigroup.ext', 'add_semigroup.ext_iff', 'has_smul.ext', 'add_semigroup', 'left_add', 'add_neg_self', 'of_nat_zsmul', 'add_monoid', 'add_zero', 'mul_right_inj', 'add_neg_cancel_right', 'right_mul', 'div_eq_mul_inv', 'mul_one_class.ext', 'left_inv_eq_right_inv', 'add_comm', 'neg_zero_class', 'left_cancel_monoid', 'add_left_neg', 'division_comm_monoid', 'neg_neg', 'group', 'add_zero_class.ext', 'pow_zero', 'subtraction_comm_monoid', 'is_cancel_add', 'add_left_cancel_semigroup.ext_iff', 'has_smul.ext_iff', 'mul_left_cancel_iff', 'add_right_cancel_semigroup', 'is_right_cancel_mul', 'add_comm_semigroup.is_left_cancel_add.to_is_right_cancel_add', 'nsmul_rec', 'neg_add_rev', 'zsmul_eq_smul', 'comm_group', 'neg_zero', 'add_left_cancel_semigroup', 'zero_nsmul', 'is_left_cancel_mul', 'right_cancel_semigroup', 'add_cancel_comm_monoid', 'add_left_injective', 'npow_eq_pow', 'inv_mul_cancel_left', 'semigroup.ext', 'add_left_cancel_iff', 'add_left_cancel_monoid', 'add_neg_cancel_left', 'zpow_rec', 'zpow_zero', 'add_comm_semigroup.is_left_cancel_add.to_is_cancel_add', 'mul_left_inv', 'div_inv_monoid', 'right_cancel_semigroup.ext_iff', 'pow_succ', 'mul_left_inj', 'mul_one_class', 'zsmul_rec', 'add_comm_monoid', 'add_assoc', 'mul_left_cancel', 'comm_semigroup.ext', 'cancel_comm_monoid', 'mul_inv_cancel_right', 'group.to_monoid', 'add_group.to_sub_neg_add_monoid_injective', 'add_left_cancel', 'add_comm_semigroup.is_right_cancel_add.to_is_cancel_add', 'add_right_neg', 'add_comm_group', 'inv_mul_self', 'zpow_eq_pow', 'semigroup', 'left_cancel_semigroup.ext_iff', 'one_mul', 'left_mul', 'mul_inv_self'}
Phantom aligns: {"monoid.npow_zero'", 'has_inv', "add_monoid.nsmul_zero'", "add_monoid.nsmul_succ'", "monoid.npow_succ'"}

===== File mathlib/src/algebra/group/with_one/basic.lean =====
Missing aligns: {'with_zero.coe_add_hom_apply', 'with_one.coe_mul_hom_apply'}

===== File mathlib/src/order/boolean_algebra.lean =====
Missing aligns: {'sdiff_eq_left', 'le_sdiff'}

===== File mathlib/src/order/modular_lattice.lean =====
Missing aligns: {'inf_Ioo_order_iso_Ioo_sup_apply_coe', 'inf_Icc_order_iso_Icc_sup_apply_coe', 'covby.inf_of_sup_right', 'covby.sup_of_inf_right', 'covby.inf_of_sup_of_sup_left', 'covby.inf_of_sup_left', 'covby.inf_of_sup_of_sup_right', 'inf_Ioo_order_iso_Ioo_sup_symm_apply_coe', 'inf_Icc_order_iso_Icc_sup_symm_apply_coe', 'covby.sup_of_inf_of_inf_right', 'covby.sup_of_inf_of_inf_left', 'covby.sup_of_inf_left'}

===== File mathlib/src/order/atoms.lean =====
Missing aligns: {'is_coatomic_iff', 'is_coatom.covby_top', 'is_simple_order.equiv_bool_apply', 'covby.is_coatom', 'covby.is_atom', 'is_simple_order.has_lt.lt.eq_top', 'is_atom.dual', 'is_simple_order.equiv_bool_symm_apply', 'is_atomic_iff', 'is_atom.bot_covby', 'is_simple_order.has_lt.lt.eq_bot', 'is_coatom.dual'}
Phantom aligns: {'is_coatomistic.eq_Inf_coatoms', 'is_atomistic.eq_Sup_atoms'}

===== File mathlib/src/order/synonym.lean =====
Missing aligns: {'order_dual.exists', 'to_lex', 'order_dual.rec', 'of_lex', 'has_le.le.dual', 'order_dual.forall', 'has_lt.lt.dual', 'lex.rec', 'lex'}

===== File mathlib/src/order/disjoint.lean =====
Missing aligns: {'disjoint_sup_left', 'disjoint_top', 'symmetric_codisjoint', 'codisjoint.eq_top_of_self', 'codisjoint_top_right', 'disjoint_iff', 'disjoint.eq_bot_of_self', 'codisjoint_inf_right', 'disjoint_right_comm', 'codisjoint_right_comm', 'disjoint_assoc', 'disjoint_self', 'disjoint_iff_inf_le', 'disjoint_sup_right', 'codisjoint_top_left', 'disjoint_bot_left', 'codisjoint_bot', 'codisjoint_inf_left', 'symmetric_disjoint', 'codisjoint_left_comm', 'bot_codisjoint', 'codisjoint_self', 'top_disjoint', 'disjoint_left_comm', 'codisjoint_assoc'}

===== File mathlib/src/order/directed.lean =====
Phantom aligns: {'is_directed.directed'}

===== File mathlib/src/order/closure.lean =====
Missing aligns: {'galois_connection.lower_adjoint_to_fun', "closure_operator.mk'_apply", 'lower_adjoint.id_to_fun', 'closure_operator.mk₂_apply', 'closure_operator.mk₃_apply', 'closure_operator.id_apply', 'galois_connection.closure_operator_apply', 'lower_adjoint.closure_operator_apply'}

===== File mathlib/src/order/cover.lean =====
Missing aligns: {'has_lt.lt.exists_lt_lt', 'has_le.le.wcovby_of_le', 'covby.to_dual', 'wcovby.of_dual', 'exists_lt_lt_of_not_covby', 'covby.of_dual', 'wcovby.eq_or_covby', 'wcovby.to_dual', 'wcovby.covby_or_eq'}

===== File mathlib/src/order/antisymmetrization.lean =====
Missing aligns: {'antisymm_rel.setoid_r', 'order_hom.to_antisymmetrization', 'order_hom.to_antisymmetrization_coe', 'antisymm_rel.eq', 'order_embedding.of_antisymmetrization_apply'}

===== File mathlib/src/order/initial_seg.lean =====
Missing aligns: {'initial_seg.coe_fn_mk', 'principal_seg.coe_fn_to_rel_embedding', 'initial_seg.coe_fn_to_rel_embedding', 'principal_seg.coe_coe_fn'}

===== File mathlib/src/order/lattice.lean =====
Missing aligns: {'inf_of_le_left', 'inf_eq_and_sup_eq_iff', 'sup_of_le_left', 'le_of_sup_eq', 'inf_eq_sup', 'sup_of_le_right', 'le_of_inf_eq', 'inf_of_le_right', 'sup_eq_inf'}

===== File mathlib/src/order/well_founded.lean =====
Phantom aligns: {'well_founded_relation.r'}

===== File mathlib/src/order/max.lean =====
Missing aligns: {'no_max_order.not_acc', 'is_bot.to_dual', 'is_min.of_dual', 'has_lt.lt.not_is_max', 'is_min', 'has_lt.lt.not_is_min', 'is_bot.of_dual', 'no_top_order_iff_no_max_order', 'no_bot_order_iff_no_min_order', 'no_min_order.not_acc', 'is_min.to_dual', 'is_max.of_dual', 'is_bot', 'is_top.to_dual', 'is_max', 'is_top.of_dual', 'is_top', 'is_max.to_dual'}

===== File mathlib/src/order/bounded_order.lean =====
Missing aligns: {'is_min.eq_bot', 'has_lt.lt.ne_top', 'is_max.eq_top', 'is_top.eq_top', 'has_lt.lt.ne_bot', 'is_bot.eq_bot'}

===== File mathlib/src/order/basic.lean =====
Missing aligns: {'has_lt.lt.trans', "has_le.le.trans'", 'has_le.le.eq_or_gt', 'has_le.le.eq_or_lt_dec', "has_lt.lt.trans'", 'has_le.le.trans_eq', 'eq.trans_lt', "has_lt.lt.trans_le'", 'has_le.ext', "has_lt.lt.trans_eq'", "has_le.le.lt_of_ne'", 'has_lt.lt.not_le', 'strong_lt.lt', 'has_le.le.eq_of_not_gt', "has_le.le.trans_lt'", 'has_lt.lt.trans_eq', 'eq.trans_gt', 'eq.trans_le', 'has_le.le.antisymm', 'has_lt.lt.not_lt', 'has_le.le.lt_or_eq_dec', 'eq.le', 'has_le.le.eq_or_lt', 'has_le.le.lt_of_ne', 'strong_lt.le', 'has_lt.lt.le', 'eq_or_eq_or_eq_of_forall_not_lt_lt', 'has_le.ext_iff', 'has_le.le.trans', 'has_le.le.trans_strong_lt', 'has_le.le.eq_of_not_lt', 'strong_lt.trans_le', 'has_le.le.trans_lt', 'has_lt.lt.asymm', 'has_le.le.lt_of_not_le', "has_le.le.trans_eq'", "has_le.le.antisymm'", 'has_lt.lt.trans_le', 'has_le.le.not_lt', 'eq.trans_ge', 'has_le.le.lt_or_eq'}

===== File mathlib/src/order/compare.lean =====
Missing aligns: {'linear_order_of_compares', 'ordering.compares.eq_eq', 'cmp_eq_lt_iff', 'ordering.compares.of_swap', 'ordering.swap_inj', 'ordering.compares.ne_lt', 'le_iff_le_of_cmp_eq_cmp', 'ordering.swap_eq_iff_eq_swap', 'ordering.compares.inj', 'ordering.compares.swap', 'cmp_eq_cmp_symm', 'ordering.compares.ne_gt', 'lt_iff_lt_of_cmp_eq_cmp', 'cmp_eq_eq_iff', 'ordering.compares.le_antisymm', 'ordering.compares_iff_of_compares_impl', 'ordering.compares', 'eq_iff_eq_of_cmp_eq_cmp', 'cmp_swap', 'ordering.compares.eq_lt', 'has_lt.lt.cmp_eq_gt', 'ordering.compares_swap', 'eq.cmp_eq_eq', 'ordering.compares.cmp_eq', 'ordering.compares.eq_gt', 'cmp_self_eq_eq', 'ordering.compares.le_total', 'cmp_compares', 'has_lt.lt.cmp_eq_lt', 'cmp_eq_gt_iff', "eq.cmp_eq_eq'"}

===== File mathlib/src/order/complete_lattice.lean =====
Missing aligns: {'prod.swap_Inf', 'prod.snd_Inf', 'prod.snd_Sup', 'prod.fst_Sup', 'prod.snd_infi', 'prod.swap_supr', 'prod.swap_Sup', 'prod.supr_mk', 'Sup_prod', 'prod.fst_infi', 'prod.snd_supr', 'prod.swap_infi', 'Inf_prod', 'prod.infi_mk', 'prod.fst_supr', 'prod.fst_Inf'}
Phantom aligns: {'has_Inf.Inf', 'has_Sup.Sup'}

===== File mathlib/src/order/rel_classes.lean =====
Missing aligns: {'has_subset.subset.ssubset_of_ne', 'is_well_founded.induction', 'is_nonstrict_strict_order', 'transitive_le', 'is_well_founded', 'is_total.swap', 'well_founded_gt.fix', 'transitive_gt', 'empty_relation_apply', 'linear_order_of_STO', 'has_subset.subset.ssubset_or_eq', 'has_subset.subset.not_ssubset', 'ssubset_of_subset_of_ssubset', 'comm', 'well_founded_gt.induction', 'is_well_founded.apply', "ne_of_irrefl'", 'is_well_founded.fix', 'has_ssubset.ssubset.not_subset', 'set.not_unbounded_iff', 'transitive_of_trans', 'ne.ssubset_of_subset', 'not_subset_of_ssubset', 'comm_of', 'right_iff_left_not_left', 'well_founded_gt', 'is_asymm.is_antisymm', 'is_strict_total_order.swap', 'eq_empty_relation', 'of_eq', 'is_trans.swap', 'set.bounded', 'well_founded_lt.apply', 'ssubset_iff_subset_ne', 'is_trichotomous.swap', 'ne_of_irrefl', 'well_founded_lt.fix', 'is_well_founded_iff', 'ssubset_of_subset_not_subset', 'has_subset.subset.ssubset_of_not_subset', 'superset_antisymm_iff', 'ssubset_iff_subset_not_subset', 'is_total_preorder.swap', 'trans_trichotomous_left', 'set.unbounded', 'well_founded_gt.fix_eq', 'well_founded_lt.induction', 'eq_or_ssubset_of_subset', 'antisymm_iff', 'ssubset_of_subset_of_ne', 'is_well_order.linear_order', 'is_order_connected.neg_trans', 'rel_of_subsingleton', 'well_founded.asymmetric', 'is_asymm.swap', 'well_founded_gt.apply', 'is_well_founded.to_has_well_founded', 'has_ssubset.ssubset.trans_subset', 'subset_of_ssubset', 'is_refl.swap', 'partial_order_of_SO', "antisymm'", 'well_founded_gt.to_has_well_founded', 'is_well_order', 'subsingleton.is_well_order', 'antisymm_of', 'subset_iff_ssubset_or_eq', 'is_asymm.is_irrefl', 'set.unbounded_of_is_empty', 'right_iff_left_not_left_of', 'ssubset_of_ne_of_subset', 'is_partial_order.swap', 'well_founded_gt_dual_iff', 'well_founded_lt_dual_iff', 'is_preorder.swap', 'has_subset.subset.trans_ssubset', 'trans_trichotomous_right', 'subset_antisymm_iff', "has_subset.subset.antisymm'", 'is_well_order.to_has_well_founded', 'set.not_bounded_iff', 'is_well_founded.fix_eq', 'transitive_ge', "antisymm_of'", 'is_total.is_trichotomous', 'is_linear_order.swap', 'well_founded_lt.to_has_well_founded', 'is_order_connected', 'has_subset.subset.eq_or_ssubset', 'not_ssubset_of_subset', 'is_antisymm.swap', 'ssubset_or_eq_of_subset', 'is_irrefl.swap', 'extensional_of_trichotomous_of_irrefl', 'subrelation.is_well_founded', 'is_strict_order.swap', 'well_founded_lt', 'well_founded_lt.fix_eq', 'not_rel_of_subsingleton', 'ssubset_of_ssubset_of_subset', 'transitive_lt'}
Phantom aligns: {'has_well_founded', 'has_well_founded.R', 'nat.lt_wf'}

===== File mathlib/src/order/concept.lean =====
Missing aligns: {'concept.swap_equiv_apply', 'concept.swap_equiv_symm_apply', 'concept.swap_to_prod'}

===== File mathlib/src/order/omega_complete_partial_order.lean =====
Missing aligns: {'omega_complete_partial_order.continuous_hom.flip_apply', 'omega_complete_partial_order.continuous_hom.to_mono_coe', 'omega_complete_partial_order.continuous_hom.of_fun_apply', 'omega_complete_partial_order.continuous_hom.coe_apply', 'omega_complete_partial_order.continuous_hom.of_mono_apply', 'omega_complete_partial_order.continuous_hom.seq_apply', 'omega_complete_partial_order.continuous_hom.ωSup_apply', 'prod.ωSup_snd', 'prod.omega_complete_partial_order_ωSup_snd', 'omega_complete_partial_order.continuous_hom.omega_complete_partial_order_ωSup', 'omega_complete_partial_order.continuous_hom.id_apply', 'omega_complete_partial_order.continuous_hom.prod.apply_apply', 'omega_complete_partial_order.order_hom.omega_complete_partial_order_ωSup_coe', 'omega_complete_partial_order.chain.zip_coe', 'prod.omega_complete_partial_order_ωSup_fst', 'omega_complete_partial_order.chain.map_coe', 'omega_complete_partial_order.continuous_hom.bind_apply', 'omega_complete_partial_order.order_hom.ωSup_coe', 'omega_complete_partial_order.continuous_hom.comp_apply', 'prod.ωSup_fst', 'omega_complete_partial_order.continuous_hom.map_apply', 'order_hom.bind_coe'}

===== File mathlib/src/order/bounds/basic.lean =====
Missing aligns: {'is_glb_empty_iff', 'is_least_univ_iff', 'is_greatest_univ_iff', 'image2_upper_bounds_lower_bounds_subset_upper_bounds_image2', 'is_lub_empty_iff'}
Phantom aligns: {'image2_upper_bounds_lower_bounds_subset_upperBounds_image2'}

===== File mathlib/src/order/monotone/basic.lean =====
Missing aligns: {'strict_anti.le_iff_le', 'monotone_on.dual_right', 'monotone.dual', 'monotone.prod_map', 'strict_mono.imp', 'monotone_id', 'antitone_on.reflect_lt', 'strict_anti', 'strict_mono.ite', 'monotone.ne_of_lt_of_lt_nat', 'antitone.dual_left', 'strict_anti.cmp_map_eq', 'strict_mono.prod_map', 'strict_anti_on.dual_right', 'int.rel_of_forall_rel_succ_of_lt', 'strict_mono', 'subsingleton.antitone', 'antitone_on.dual', 'monotone.comp_le_comp_left', 'antitone_on.dual_left', 'strict_mono.dual', 'strict_anti_on.dual', 'strict_mono.iterate', 'antitone.antitone_on', 'monotone.comp_antitone', 'strict_mono.monotone', 'strict_anti.minimal_of_maximal_image', 'strict_anti.lt_iff_lt', 'strict_mono.maximal_of_maximal_image', 'strict_mono_on.dual_right', 'strict_mono.id_le', 'strict_anti.maximal_of_minimal_image', 'strict_anti_on.le_iff_le', 'monotone.monotone_on', 'antitone.comp_monotone', 'strict_anti_on', 'antitone.ne_of_lt_of_lt_int', 'injective_of_le_imp_le', 'antitone_lam', 'strict_mono_on.dual', 'strict_mono.dual_left', 'strict_mono_on', 'int.rel_of_forall_rel_succ_of_le', 'strict_mono.compares', 'antitone.imp', 'monotone.reflect_lt', 'strict_anti_nat_of_succ_lt', 'strict_mono.dual_right', 'strict_mono_on.lt_iff_lt', 'list.foldr_monotone', 'strict_anti.comp', 'strict_anti_on.cmp_map_eq', 'antitone.prod_map', 'strict_anti.dual_right', 'antitone.dual', 'monotone.imp', 'strict_anti.dual_left', 'monotone_on.reflect_lt', 'not_monotone_not_antitone_iff_exists_lt_lt', 'monotone.dual_right', 'strict_mono_on.cmp_map_eq', 'strict_anti.compares', 'monotone_int_of_le_succ', 'monotone_fst', 'function.monotone_eval', 'strict_anti.antitone', 'antitone', 'strict_mono_on.le_iff_le', 'antitone_on.dual_right', 'monotone_on', 'strict_mono.minimal_of_minimal_image', "subsingleton.antitone'", 'monotone', 'antitone.comp', 'strict_mono.cmp_map_eq', 'antitone_int_of_succ_le', 'antitone_app', 'antitone_const', 'monotone_app', "strict_anti.ite'", 'strict_mono.comp', 'monotone.ne_of_lt_of_lt_int', 'list.foldl_monotone', "subsingleton.monotone'", "strict_mono.ite'", 'antitone.ne_of_lt_of_lt_nat', 'monotone_snd', 'strict_mono_on.dual_left', 'monotone_const', 'strict_anti_on.compares', 'antitone.reflect_lt', 'strict_anti.prod_map', 'strict_anti_on.lt_iff_lt', 'antitone.dual_right', 'subtype.mono_coe', 'monotone_lam', 'monotone_on.dual_left', 'function.const_mono', 'monotone.comp', 'antitone_iff_forall_lt', 'strict_mono.le_iff_le', 'not_monotone_not_antitone_iff_exists_le_le', 'monotone.dual_left', 'antitone_on', 'strict_anti_on.eq_iff_eq', 'monotone_iff_forall_lt', 'monotone_on.dual', 'subsingleton.monotone', 'strict_anti.imp', 'strict_anti_on.dual_left', 'strict_anti.dual', 'strict_mono_on.eq_iff_eq'}

===== File mathlib/src/order/rel_iso/basic.lean =====
Missing aligns: {'rel_embedding.sum_lex_inl_apply', 'rel_embedding.coe_fn_to_embedding', 'rel_embedding.coe_coe_fn', 'rel_embedding.to_rel_hom_eq_coe', 'rel_embedding.coe_fn_mk', 'rel_iso.refl_apply', 'rel_embedding.sum_lift_rel_map_apply', 'rel_iso.of_surjective_apply', 'well_founded.of_quotient_lift₂', 'rel_embedding.sum_lex_inr_apply', 'rel_embedding.prod_lex_mk_right_apply', 'rel_embedding.prod_lex_mk_left_apply', 'rel_embedding.sum_lex_map_apply', 'rel_iso.trans_apply', 'rel_embedding.sum_lift_rel_inl_apply', 'rel_iso.to_rel_embedding_eq_coe', 'rel_hom.comp_apply', 'well_founded.quotient_lift₂', 'rel_iso.cast_apply', 'rel_iso.cast_to_equiv', 'rel_hom.id_apply', 'quotient.out_rel_embedding_apply', 'rel_embedding.sum_lift_rel_inr_apply', 'rel_iso.coe_coe_fn', 'rel_embedding.refl_apply', 'rel_embedding.prod_lex_map_apply', 'rel_hom.coe_fn_mk'}

===== File mathlib/src/order/hom/set.lean =====
Missing aligns: {'strict_mono.order_iso_apply', 'order_iso.compl_apply', 'order_iso.compl_symm_apply'}

===== File mathlib/src/order/hom/order.lean =====
Missing aligns: {'order_hom.has_top_top', 'order_hom.has_sup_sup_coe', 'order_hom.has_inf_inf_coe', 'order_hom.has_bot_bot'}

===== File mathlib/src/order/hom/basic.lean =====
Missing aligns: {'order_embedding.with_bot_map_apply', 'order_hom.with_top_map_coe', 'rel_hom.to_order_hom_coe', 'order_hom.diag_coe', 'order_hom.pi_iso_symm_apply', 'order_iso.fun_unique_apply', 'order_embedding.subtype_apply', 'strict_mono.order_iso_of_right_inverse_symm_apply', 'order_hom.fst_coe', 'order_hom.comp_coe', 'order_hom.apply_coe', 'order_iso.fun_unique_to_equiv', 'pi.eval_order_hom_coe', 'order_hom.id_coe', 'order_hom.prod_coe', 'order_embedding.with_top_map_apply', 'order_hom.subtype.val_coe', 'order_embedding.to_order_hom_coe', 'order_hom.dual_apply_coe', 'order_hom.pi_iso_apply', 'order_hom.with_bot_map_coe', 'order_hom.prodₘ_coe_coe_coe', 'order_hom.prod_iso_apply', 'order_hom.dual_symm_apply_coe', 'order_iso.with_bot_congr_apply', 'order_hom.const_coe_coe', 'strict_mono.order_iso_of_right_inverse_apply', 'order_hom.on_diag_coe', 'order_hom.pi_coe', 'order_iso.with_top_congr_apply', 'order_hom.prod_map_coe', 'order_hom.prod_iso_symm_apply', 'order_hom.snd_coe', 'order_hom.compₘ_coe_coe_coe', 'order_hom.coe_fn_hom_coe'}

===== File mathlib/src/order/hom/bounded.lean =====
Missing aligns: {'bot_hom.dual_apply_apply', 'bot_hom.dual_symm_apply_apply', 'bounded_order_hom.dual_symm_apply_to_order_hom', 'bounded_order_hom.dual_apply_to_order_hom', 'top_hom.dual_symm_apply_apply', 'top_hom.dual_apply_apply'}

===== File mathlib/src/order/heyting/basic.lean =====
Missing aligns: {'sup_sdiff_self_right', 'le_compl_iff_le_compl', 'disjoint.le_compl_left', 'codisjoint.hnot_le_left', 'disjoint.le_compl_right', 'codisjoint.hnot_le_right', 'sup_sdiff_self_left', 'le_compl_of_le_compl'}

===== File mathlib/src/order/succ_pred/limit.lean =====
Missing aligns: {'order.is_succ_limit.dual', 'order.is_pred_limit.dual'}

===== File mathlib/src/order/succ_pred/basic.lean =====
Missing aligns: {'succ_order.of_core_succ', 'pred_order.ext', 'pred_order.of_core_pred', 'succ_order.ext_iff', 'succ_order.ext', 'pred_order.ext_iff'}

===== File mathlib/src/order/conditionally_complete_lattice/group.lean =====
Missing aligns: {'le_add_cinfi', 'add_csupr_le', 'csupr_add_le', 'le_cinfi_add', 'le_cinfi_add_cinfi', 'csupr_add_csupr_le'}

===== File mathlib/src/order/filter/basic.lean =====
Missing aligns: {'tactic_doc.tactic.filter_upwards', 'eventually_le.add_le_add'}
Phantom aligns: {'filter.eventually_le.add_le_add'}

===== File mathlib/src/order/filter/at_top_bot.lean =====
Missing aligns: {'filter.not_tendsto_pow_at_top_at_bot', 'filter.tendsto_const_mul_at_bot_of_pos', 'filter.tendsto_Iio_at_bot'}
Phantom aligns: {'filter.not_tendsto_pow_at_top_atBot', 'filter.tendsto_const_mul_atBot_of_pos', 'filter.tendsto_Iio_atBot'}

===== File mathlib/src/logic/relator.lean =====
Missing aligns: {'relator.rel_imp', 'relator.lift_fun', 'relator.left_total.rel_exists', 'relator.bi_total_eq', 'relator.rel_not', 'relator.right_total', 'relator.bi_total.rel_forall', 'relator.rel_eq', 'relator.rel_or', 'relator.bi_unique', 'relator.left_unique', 'relator.left_unique_of_rel_eq', 'relator.right_unique', 'relator.rel_and', 'relator.bi_total', 'relator.left_unique.flip', 'relator.rel_iff', 'relator.bi_total.rel_exists', 'relator.left_total', 'relator.right_total.rel_forall'}

===== File mathlib/src/logic/unique.lean =====
Missing aligns: {"unique.mk'", 'unique.default_eq', 'fin.default_eq_zero', 'heq_const_of_unique', "unique.subsingleton_unique'", 'pi.default_apply', 'unique_iff_exists_unique', 'unique.ext', 'unique.forall_iff', 'function.surjective.unique', 'function.injective.unique', 'function.surjective.unique_of_surjective_const', 'unique', 'unique.eq_default', 'unique.exists_iff', 'unique_subtype_iff_exists_unique', 'fin.eq_zero', 'unique_of_subsingleton', 'function.surjective.subsingleton', 'unique_prop', 'function.injective.subsingleton', 'eq_const_of_unique', 'unique.bijective', 'unique.ext_iff', 'unique_iff_subsingleton_and_nonempty', 'pi.default_def'}

===== File mathlib/src/logic/lemmas.lean =====
Missing aligns: {'ite_dite_distrib_right', 'Prop.forall', 'dite_dite_distrib_right', 'ite_ite_distrib_right', 'ite_ite_distrib_left', 'heq.eq', 'eq.heq', 'dite_ite_distrib_left', 'ne.trans_eq', 'dite_ite_distrib_right', 'eq.trans_ne', 'dite_dite_distrib_left', 'Prop.exists', 'ite_dite_distrib_left'}

===== File mathlib/src/logic/is_empty.lean =====
Missing aligns: {'is_empty_elim', 'is_empty.exists_iff', 'is_empty.forall_iff', 'is_empty', 'is_empty.elim', 'is_empty.prop_iff', "is_empty.elim'", 'not_nonempty_iff'}

===== File mathlib/src/logic/basic.lean =====
Missing aligns: {'not_imp_of_and_not', 'forall_swap', 'exists.classical_rec_on', 'decidable.peirce', 'forall_eq', 'not_iff_not', 'eq_equivalence', 'forall_eq_apply_imp_iff', 'iff_of_true', 'or_iff_not_imp_right', 'decidable.or_iff_not_and_not', "exists_eq_right'", 'and_iff_not_or_not', 'or_or_distrib_left', 'forall_prop_congr', 'or_iff_right', 'xor_iff_not_iff', 'iff_iff_and_or_not_and_not', 'exists_eq_right_right', 'forall_true_iff', 'auto_param.out', 'not_forall', "exists_prop_congr'", 'cast_cast', "forall_prop_congr'", 'exists_unique.exists', 'dite_eq_or_eq', 'and_self_left', 'not_and_self_iff', 'exists_comm', 'ite_eq_or_eq', 'not_iff_comm', "forall_true_iff'", 'forall_imp_iff_exists_imp', 'decidable.not_imp_not', 'not.decidable_imp_symm', 'decidable.and_forall_ne', 'xor_self', 'xor_comm', 'not_and_not_right', 'xor_not_right', 'decidable.and_iff_not_or_not', 'not_and_of_not_or_not', 'proof_irrel_heq', 'subsingleton_of_forall_eq', 'ball_mem_comm', 'forall₂_imp', 'iff.imp', 'forall₃_congr', 'heq_iff_eq', 'decidable.eq_or_ne', 'coe_sort_coe_base', 'ite_and', 'imp_not_comm', 'exists_eq_left', 'iff_self_and', 'eq_true_eq_id', "ne_of_mem_of_not_mem'", 'not_of_not_imp', 'imp_false', 'decidable.not_imp_self', 'Exists.imp', "classical.by_contradiction'", 'dite_ne_right_iff', 'or_or_or_comm', 'Exists.snd', 'by_contradiction', 'or_iff_not_and_not', 'exists_apply_eq_apply', 'decidable.not_not', 'forall₂_congr', 'iff_and_self', 'apply_dite', 'of_not_imp', 'and_not_self_iff', 'ite_eq_left_iff', 'exists_unique_prop', 'or_self_right', 'exists_unique_false', "exists_eq'", 'or_or_distrib_right', 'iff_false_left', 'eq.congr', 'ulift.down_injective', 'decidable.not_and_not_right', 'bex_of_exists', 'not_nonempty_pempty', 'decidable.not_iff_not', 'exists₃_congr', "coe_fn_coe_trans'", 'dite_eq_iff', 'pi_congr', 'ball_congr', 'and.imp_left', 'forall_const', 'dite_dite_comm', 'classical.dec_rel', 'not_imp_self', 'ball_cond_comm', 'and_and_and_comm', 'or.imp3', 'decidable.not_imp_symm', 'of_not_not', 'classical.dec', 'opt_param.out', 'and.exists', 'ite_ite_comm', 'not.imp_symm', 'ne.ne_or_ne', 'not_and_of_not_right', 'Exists₂.imp', "forall_eq_apply_imp_iff'", 'funext₃', 'eq_iff_eq_cancel_right', 'and.imp_right', 'function.mt', 'and.rotate', "xor_iff_not_iff'", 'not_imp_comm', "exists_or_eq_right'", 'decidable.not_forall', 'exists_eq', 'ite_ne_right_iff', "dec_em'", 'exists₂_comm', 'iff.iff', 'rec_heq_of_heq', 'decidable.or_iff_not_imp_left', 'forall₂_swap', 'ite_eq_right_iff', 'Exists.fst', 'not_exists', 'false_ne_true', 'decidable.not_ball', 'imp.swap', 'eq_rec_constant', 'fact.elim', 'exists₂_congr', 'ball_of_forall', 'iff.not_right', 'fact', 'decidable.of_not_imp', 'decidable.not_exists_not', 'and_iff_left_iff_imp', 'ne_of_mem_of_not_mem', 'iff.or', 'not.elim', 'not_imp_not', 'iff_def', 'decidable.and_or_imp', 'imp_iff_not_or', 'decidable.iff_iff_and_or_not_and_not', "em'", 'decidable.not_or_of_imp', 'imp_iff_right_iff', 'hidden', 'forall_prop_of_false', 'exists_prop', "has_mem.mem.ne_of_not_mem'", 'eq.congr_right', 'decidable.not_imp', 'ne_comm', 'xor_false', 'not_bex', 'congr_arg_heq', "coe_fn_coe_base'", 'iff_of_eq', 'iff_iff_not_or_and_or_not', 'forall₄_congr', 'dite_eq_right_iff', 'or_iff_right_iff_imp', 'exists_eq_right', 'exists_const', 'forall_prop_of_true', 'or_of_or_of_imp_right', 'exists_exists_and_eq_and', 'dec_em', 'or_of_or_of_imp_left', "iff_def'", 'ball_true_iff', 'dite_eq_ite', 'congr_refl_right', 'not_ball', 'not_and', "exists_eq_left'", 'and_rotate', 'cast_eq_iff_heq', 'decidable.imp_iff_not_or', 'dite_not', 'not_not', 'and_or_imp', 'forall₃_imp', 'congr_fun_congr_arg', 'iff_iff_eq', "exists_apply_eq_apply'", 'ite_eq_iff', 'or_not', 'function.mtr', "and_congr_left'", 'heq_of_cast_eq', 'iff_true_right', 'forall₅_congr', 'and_self_right', 'ite_not', 'and_iff_right_iff_imp', 'peirce', 'or_rotate', 'classical.exists_cases', "forall_eq'", 'ne_or_eq', 'or.rotate', "peirce'", 'decidable.not_iff', 'or_iff_not_imp_left', 'and_imp', 'imp_not_self', 'classical.cases', 'apply_ite', 'bex_def', 'ne.dite_ne_left_iff', 'exists_prop_of_false', 'exists_iff_of_forall', 'eq_iff_true_of_subsingleton', 'coe_coe', 'forall_of_ball', 'xor_iff_iff_not', 'imp_iff_or_not', 'plift.down_injective', 'forall_forall_const', 'not.imp', 'ne.ite_eq_right_iff', 'xor_true', 'dite_apply', 'function.swap₂', 'ne.ite_ne_left_iff', 'ne.dite_eq_left_iff', 'not_xor', 'not_ball_of_bex_not', 'decidable.not_iff_comm', 'bex_eq_left', 'not_or_of_imp', 'xor_not_left', "ite_eq_iff'", 'eq_mp_eq_cast', 'not_forall_of_exists_not', 'iff.not', 'plift.down_inj', 'exists₅_congr', 'and_forall_ne', 'congr_fun_rfl', 'iff.and', "not_and'", "exists_or_eq_left'", 'congr_refl_left', 'iff_not_comm', 'eq_true_iff', 'eq_iff_eq_cancel_left', 'decidable.not_imp_comm', 'forall_eq_or_imp', 'ite_apply', 'by_contra', 'coe_fn_coe_base', 'not_forall_not', 'ne.ite_eq_left_iff', 'exists_true_left', 'not_exists_of_forall_not', 'iff_mpr_iff_true_intro', 'funext₂', 'imp_self', 'subsingleton_iff_forall_eq', 'bex_congr', 'imp_imp_imp', 'xor.or', 'exists_exists_eq_and', 'congr_heq', 'exists_unique_iff_exists', 'congr_fun₃', 'forall_apply_eq_imp_iff', 'not_exists_not', "exists_unique_eq'", 'decidable.ne_or_eq', 'not_ne_iff', 'eq_mpr_eq_cast', 'coe_sort_coe_trans', 'em', 'exists_swap', 'decidable.or_not_of_imp', 'ite_ne_left_iff', 'congr_arg_refl', 'ne_of_apply_ne', 'exists_unique.unique', 'iff.not_left', 'or_iff_left_iff_imp', 'imp_true_iff', 'classical.dec_eq', 'exists_of_bex', 'or_not_of_imp', 'exists_false', 'iff_false_right', 'decidable.iff_iff_not_or_and_or_not', 'forall_or_of_or_forall', 'iff_of_false', 'classical.dec_pred', 'not_not_of_not_imp', 'decidable.iff_not_comm', 'ne_and_eq_iff_right', 'imp_intro', 'forall_true_left', 'Exists₃.imp', 'exists_prop_of_true', 'decidable.not_forall_not', 'exists_unique_eq', "exists_eq_right_right'", 'iff_true_left', 'dite_eq_left_iff', 'ne.ite_ne_right_iff', 'ulift.down_inj', 'not_and_of_not_left', 'has_mem.mem.ne_of_not_mem', 'or_of_or_of_imp_of_imp', 'exists₄_congr', 'exists_or_eq_right', 'eq.congr_left', "forall_apply_eq_imp_iff'", 'decidable.imp_iff_right_iff', "dite_eq_iff'", 'or_self_left', 'imp_forall_iff', 'congr_fun₂', 'exists_prop_congr', 'not_imp', 'and_iff_right_of_imp', 'forall_apply_eq_imp_iff₂', 'not_iff', 'forall_exists_index', 'exists_or_eq_left', 'xor_not_not', 'and_iff_left_of_imp', 'exists_unique_const', 'ne.dite_ne_right_iff', 'dite_ne_left_iff', 'fact_iff', 'pempty.elim', 'eq_iff_iff', 'forall_imp', 'exists_unique_prop_of_true', 'coe_fn_coe_trans', 'eq_or_ne', 'or.elim3', 'empty.elim', 'ne.dite_eq_right_iff'}
Phantom aligns: {'classical.by_cases', 'classical.by_contradiction'}

===== File mathlib/src/logic/relation.lean =====
Missing aligns: {'relation.refl_trans_gen.single', 'relation.fibration', 'is_refl.reflexive', 'reflexive_ne_imp_iff', 'equivalence.comap', 'relation.refl_gen', 'relation.trans_gen.closed', 'relation.equivalence_join', "relation.refl_trans_gen.lift'", 'relation.trans_gen.lift', "relation.trans_gen.tail'_iff", 'relation.comp_assoc', 'relation.trans_gen.head_induction_on', 'relation.join', 'relation.refl_trans_gen.cases_tail', 'relation.trans_gen.trans_left', 'relation.comp', 'relation.trans_gen.trans', 'relation.symmetric_join', 'reflexive.ne_imp_iff', 'relation.refl_trans_gen.trans_induction_on', 'relation.refl_trans_gen.lift', 'transitive.comap', 'relation.refl_trans_gen.head', 'symmetric.comap', 'relation.church_rosser', 'relation.trans_gen.swap', 'relation.refl_trans_gen.cases_tail_iff', "relation.trans_gen.lift'", 'relation.refl_trans_gen.cases_head', "relation.trans_gen.tail'", 'relation.iff_comp', 'symmetric.swap_eq', 'relation.join_of_equivalence', 'relation.refl_trans_gen.total_of_right_unique', 'relation.refl_trans_gen.swap', 'relation.eq_comp', 'relation.refl_trans_gen.mono', 'relation.transitive_join', 'relation.refl_trans_gen_idem', 'swap_eq_iff', 'relation.comp_eq', 'symmetric.flip_eq', 'relation.trans_gen.mono', 'relation.trans_gen.head', 'acc.of_downward_closed', 'relation.join_of_single', 'acc.trans_gen', 'relation.map', 'relation.reflexive_join', 'reflexive.comap', "relation.trans_gen.head'", 'relation.refl_trans_gen.symmetric', 'reflexive.rel_of_ne_imp', 'relation.trans_gen.trans_right', 'relation.refl_gen.mono', 'relation.comp_iff', 'flip_eq_iff', "relation.trans_gen.head'_iff", 'eqv_gen.mono', 'relation.flip_comp', 'relation.refl_trans_gen.cases_head_iff', 'acc.of_fibration', 'relation.refl_trans_gen.trans', 'relation.refl_trans_gen', 'symmetric.iff', 'relation.refl_trans_gen.head_induction_on', 'relation.trans_gen.trans_induction_on', 'relation.trans_gen'}

===== File mathlib/src/logic/nontrivial.lean =====
Missing aligns: {'nontrivial_iff', 'nontrivial_iff_exists_ne', 'nontrivial_of_ne', 'exists_pair_ne', 'false_of_nontrivial_of_subsingleton', 'nontrivial_psum_unique', 'pi.nontrivial_at', 'exists_pair_lt', 'subsingleton_iff', 'function.injective.exists_ne', 'subtype.nontrivial_iff_exists_ne', 'subsingleton_or_nontrivial', 'subsingleton.le', 'exists_ne', 'decidable.exists_ne', 'nontrivial', 'function.surjective.nontrivial', 'not_nontrivial', 'nontrivial_iff_lt', 'nontrivial_of_lt', 'not_subsingleton', 'function.injective.nontrivial', 'not_nontrivial_iff_subsingleton'}

===== File mathlib/src/logic/nonempty.lean =====
Missing aligns: {'nonempty_plift', 'function.surjective.nonempty', 'nonempty_psum', 'nonempty_psigma', 'classical.nonempty_pi', 'nonempty_sum', 'exists_true_iff_nonempty', 'nonempty_prod', 'nonempty.elim_to_inhabited', 'nonempty.forall', 'nonempty_empty', 'nonempty.map', "classical.inhabited_of_nonempty'", 'not_nonempty_iff_imp_false', 'nonempty.congr', 'nonempty_ulift', 'nonempty.some', 'subsingleton_of_not_nonempty', 'nonempty_Prop', 'nonempty_pprod', 'nonempty.exists', 'nonempty_subtype', 'classical.arbitrary', 'nonempty_sigma', 'nonempty.map2'}

===== File mathlib/src/logic/pairwise.lean =====
Missing aligns: {'function.injective.pairwise_ne'}

===== File mathlib/src/logic/equiv/nat.lean =====
Missing aligns: {'equiv.bool_prod_nat_equiv_nat_apply', 'equiv.nat_sum_nat_equiv_nat_symm_apply', 'equiv.bool_prod_nat_equiv_nat_symm_apply'}

===== File mathlib/src/logic/equiv/option.lean =====
Missing aligns: {'equiv.option_congr_apply'}

===== File mathlib/src/logic/equiv/fin.lean =====
Missing aligns: {'fin_two_arrow_equiv_apply', 'equiv.pi_fin_succ_above_equiv_symm_apply', 'pi_fin_two_equiv_symm_apply', 'equiv.pi_fin_succ_symm_apply', 'prod_equiv_pi_fin_two_apply', 'fin_prod_fin_equiv_apply_val', 'equiv.pi_fin_succ_apply', 'fin.cast_le_order_iso_apply', 'equiv.pi_fin_succ_above_equiv_apply', 'fin_prod_fin_equiv_symm_apply', 'fin_two_arrow_equiv_symm_apply', 'fin.cast_le_order_iso_symm_apply', 'prod_equiv_pi_fin_two_symm_apply', 'pi_fin_two_equiv_apply'}

===== File mathlib/src/logic/equiv/set.lean =====
Missing aligns: {'equiv.set.range_splitting_image_equiv_symm_apply_coe', 'equiv.image_symm_apply_coe', 'equiv.of_preimage_equiv_symm_apply', 'equiv.set.univ_symm_apply', 'equiv.of_left_inverse_symm_apply', 'equiv.set.univ_pi_apply_coe', 'equiv.sigma_preimage_equiv_symm_apply_fst', 'equiv.image_apply_coe', 'equiv.set_congr_apply', 'equiv.sigma_preimage_equiv_apply', 'equiv.set.range_splitting_image_equiv_apply_coe_coe', 'equiv.set.congr_apply', 'equiv.set.image_apply', 'equiv.set.congr_symm_apply', 'equiv.of_injective_apply', 'equiv.set.univ_apply', 'equiv.of_preimage_equiv_apply', 'equiv.sigma_preimage_equiv_symm_apply_snd_coe', 'equiv.set.of_eq_symm_apply', 'equiv.of_left_inverse_apply_coe', 'equiv.set.of_eq_apply', 'equiv.set.univ_pi_symm_apply_coe'}

===== File mathlib/src/logic/equiv/local_equiv.lean =====
Missing aligns: {'set.bij_on.to_local_equiv_apply', 'local_equiv.piecewise_source', 'set.bij_on.to_local_equiv_source', 'local_equiv.copy_source', 'set.bij_on.to_local_equiv_symm_apply', 'local_equiv.is_image.restr_source', 'local_equiv.piecewise_symm_apply', 'local_equiv.trans_equiv_apply', 'equiv.to_local_equiv_symm_apply', 'local_equiv.is_image.of_symm_preimage_eq', 'equiv.trans_local_equiv_symm_apply', 'local_equiv.pi_target', 'local_equiv.is_image.preimage_eq', 'local_equiv.piecewise_target', 'local_equiv.copy_apply', 'local_equiv.trans_equiv_target', 'local_equiv.disjoint_union_source', 'local_equiv.is_image.of_preimage_eq', 'local_equiv.is_image.restr_target', 'equiv.to_local_equiv_apply', 'equiv.to_local_equiv_source', 'local_equiv.is_image.restr_symm_apply', 'local_equiv.pi_symm_apply', 'equiv.to_local_equiv_target', 'local_equiv.disjoint_union_target', 'local_equiv.disjoint_union_apply', 'local_equiv.trans_equiv_source', 'local_equiv.disjoint_union_symm_apply', 'equiv.trans_local_equiv_target', 'local_equiv.is_image.symm_preimage_eq', 'local_equiv.copy_symm_apply', 'local_equiv.pi_apply', 'local_equiv.pi_source', 'local_equiv.trans_equiv_symm_apply', 'set.bij_on.to_local_equiv_target', 'local_equiv.is_image.restr_apply', 'equiv.trans_local_equiv_apply', 'equiv.trans_local_equiv_source', 'local_equiv.copy_target', 'local_equiv.piecewise_apply'}

===== File mathlib/src/logic/equiv/basic.lean =====
Missing aligns: {'equiv.pi_split_at_apply', 'equiv.subtype_subtype_equiv_subtype_apply_coe', 'equiv.sum_congr_apply', 'equiv.subtype_subtype_equiv_subtype_exists_apply_coe', 'equiv.option_is_some_equiv_symm_apply_coe', 'equiv.pprod_prod_apply', 'equiv.subtype_univ_equiv_apply', 'equiv.bool_prod_equiv_sum_symm_apply', 'equiv.fun_split_at_apply', 'equiv.pi_equiv_pi_subtype_prod_apply', 'equiv.empty_sum_symm_apply', 'equiv.prod_congr_apply', 'equiv.prod_punit_apply', 'equiv.sum_empty_symm_apply', 'equiv.Pi_comm_apply', 'equiv.prod_assoc_symm_apply', 'equiv.punit_prod_symm_apply', 'equiv.subtype_equiv_right_apply_coe', 'equiv.of_fiber_equiv_symm_apply', 'equiv.pprod_equiv_prod_apply', 'equiv.pi_split_at_symm_apply', 'equiv.subtype_subtype_equiv_subtype_exists_symm_apply_coe_coe', "equiv.Pi_congr_left'_apply", 'equiv.prod_shear_apply', 'equiv.prod_punit_symm_apply', 'equiv.pi_equiv_pi_subtype_prod_symm_apply', 'equiv.subtype_preimage_apply', 'equiv.subtype_subtype_equiv_subtype_inter_apply_coe', 'equiv.bool_arrow_equiv_prod_symm_apply', "equiv.Pi_congr_left'_symm_apply", 'equiv.bool_arrow_equiv_prod_apply', 'equiv.pi_option_equiv_prod_symm_apply', 'equiv.curry_apply', 'equiv.pprod_prod_symm_apply', 'equiv.punit_prod_apply', 'equiv.prod_pprod_symm_apply', 'equiv.fun_split_at_symm_apply', 'equiv.subtype_subtype_equiv_subtype_inter_symm_apply_coe_coe', 'equiv.subtype_univ_equiv_symm_apply', 'equiv.subtype_subtype_equiv_subtype_symm_apply_coe_coe', 'equiv.sigma_fiber_equiv_apply', 'equiv.sigma_sum_distrib_symm_apply', 'equiv.option_is_some_equiv_apply', 'equiv.of_bijective_apply', 'equiv.subtype_equiv_right_symm_apply_coe', 'equiv.sigma_fiber_equiv_symm_apply_snd_coe', 'equiv.subtype_preimage_symm_apply_coe', 'equiv.pprod_equiv_prod_symm_apply', 'equiv.pprod_equiv_prod_plift_apply', 'equiv.pi_option_equiv_prod_apply', 'equiv.sum_comm_apply', 'equiv.prod_assoc_apply', 'equiv.prod_shear_symm_apply', 'equiv.bool_prod_equiv_sum_apply', 'equiv.curry_symm_apply', 'equiv.prod_pprod_apply', 'equiv.sigma_fiber_equiv_symm_apply_fst', 'equiv.of_fiber_equiv_apply', 'equiv.pprod_equiv_prod_plift_symm_apply', 'equiv.sigma_sum_distrib_apply', 'equiv.pprod_congr_apply'}

===== File mathlib/src/logic/equiv/defs.lean =====
Missing aligns: {'equiv.comp_symm_eq', 'equiv.equiv_of_unique', 'equiv.refl_symm', 'equiv.conj_refl', 'equiv.psigma_equiv_sigma_plift_symm_apply', 'equiv.ext', 'quotient.congr_mk', 'equiv.Prop_equiv_bool', 'equiv.equiv_of_is_empty', 'equiv.conj', 'quotient.congr_right', 'equiv.cast', 'equiv.symm_trans_self', 'equiv.apply_eq_iff_eq_symm_apply', 'quot.congr', 'equiv.Pi_subsingleton_symm_apply', 'equiv.sigma_equiv_prod_symm_apply', 'equiv.forall₂_congr', 'equiv.psigma_equiv_sigma_apply', 'equiv.subsingleton_congr', 'equiv.ulift_symm_apply', 'equiv.plift', 'equiv.ulift_apply', 'equiv.trans_assoc', 'equiv.sigma_equiv_prod', 'equiv.nonempty_congr', 'equiv.sigma_assoc', 'equiv.coe_inj', 'equiv.congr_arg', 'equiv.symm_symm', 'equiv.injective_comp', 'equiv.right_inverse_symm', 'equiv.comp_injective', 'equiv.exists_congr_left', 'equiv.sigma_congr', 'equiv.perm.coe_subsingleton', 'equiv.perm', "equiv.forall₃_congr'", 'equiv.perm.subsingleton_eq_refl', 'equiv.congr_fun', "equiv.arrow_congr'_apply", 'equiv.psigma_equiv_sigma_plift_apply', 'equiv.conj_comp', 'equiv.coe_trans', 'equiv.cast_symm', 'equiv.sigma_congr_left_apply', "equiv.forall_congr'", 'equiv.refl_apply', 'equiv.perm_congr', 'equiv.cast_eq_iff_heq', 'equiv.nonempty', 'equiv.sigma_equiv_prod_apply', 'equiv.simps.symm_apply', 'equiv.cast_apply', 'equiv.self_trans_symm', 'equiv.symm_trans_apply', 'quotient.congr', 'equiv.sigma_congr_right_apply', 'equiv.symm_symm_apply', 'equiv.perm.ext', 'quot.congr_right', 'equiv.sigma_congr_left', 'equiv.Pi_subsingleton_apply', 'equiv.comp_bijective', 'equiv.trans_refl', 'equiv.equiv_empty', 'equiv.eq_comp_symm', 'equiv.apply_eq_iff_eq', 'equiv.of_iff', 'equiv.sigma_equiv_prod_of_equiv', 'equiv.bijective_comp', 'equiv.comp_surjective', 'equiv', 'equiv.perm.ext_iff', 'equiv.cast_trans', 'equiv.ulift', 'equiv.coe_fn_mk', 'equiv.fun_unique_symm_apply', 'equiv.forall_congr', 'equiv.forall₃_congr', 'equiv.perm.congr_arg', 'equiv.symm_apply_eq', 'equiv.unique', 'equiv.left_inverse_symm', 'equiv.subsingleton.symm', 'equiv.arrow_congr', 'equiv.Pi_subsingleton', 'equiv.plift_symm_apply', 'equiv.true_arrow_equiv', 'equiv.trans', 'equiv.ext_iff', 'equiv.symm_comp_self', 'equiv.psigma_congr_right', 'equiv.trans_apply', "equiv.forall₂_congr'", 'equiv.coe_fn_injective', "equiv.sigma_congr_left'", 'equiv.eq_symm_apply', 'equiv.decidable_eq', 'equiv.fun_unique_apply', 'equiv.cast_refl', 'equiv.conj_symm', 'equiv.psigma_equiv_sigma', 'equiv.fun_unique', 'equiv.symm_apply_apply', 'equiv.plift_apply', 'equiv.coe_fn_symm_mk', 'equiv.surjective_comp', 'equiv.conj_apply', 'equiv.refl_trans', 'equiv.psigma_congr_right_apply', 'equiv.inhabited', 'equiv.perm.sigma_congr_right', 'equiv.exists_unique_congr_left', 'equiv.forall_congr_left', 'equiv.perm.congr_fun', 'equiv.coe_refl', 'equiv.psigma_equiv_subtype', 'equiv.apply_symm_apply', 'equiv.refl', 'equiv.exists_unique_congr', 'equiv.self_comp_symm', 'equiv.eq_symm_comp', 'quot.congr_mk', 'quot.congr_left', 'equiv.sigma_congr_right_trans', 'equiv.conj_trans', 'equiv.symm_comp_eq', "equiv.forall_congr_left'", "equiv.arrow_congr'", 'equiv.punit_arrow_equiv', "equiv.exists_unique_congr_left'", 'equiv.symm', 'equiv.equiv_congr', 'equiv.psigma_equiv_sigma_symm_apply'}

===== File mathlib/src/logic/function/iterate.lean =====
Missing aligns: {'function.commute.iterate_self', 'function.semiconj₂.iterate', 'function.commute.iterate_left', 'function.iterate_add_apply', 'function.iterate_add', 'function.iterate.rec_zero', 'function.iterate_succ_apply', 'function.iterate_pred_comp_of_pos', "function.iterate_succ'", 'function.iterate_id', 'function.right_inverse.iterate', 'function.iterate_zero_apply', 'function.commute.iterate_eq_of_map_eq', 'function.injective.iterate', 'function.iterate_succ', 'function.iterate_fixed', 'function.iterate_mul', 'function.iterate.rec', 'function.commute.iterate_right', 'function.semiconj.iterate_left', 'function.commute.iterate_iterate', 'function.iterate_one', 'function.iterate_commute', 'list.foldr_const', "function.iterate_succ_apply'", 'function.commute.comp_iterate', 'function.commute.iterate_iterate_self', 'function.comp_iterate_pred_of_pos', 'function.iterate_comm', 'function.iterate_zero', 'function.surjective.iterate', 'function.left_inverse.iterate', 'function.semiconj.iterate_right', 'list.foldl_const', 'function.commute.self_iterate', 'function.bijective.iterate'}

===== File mathlib/src/logic/function/conjugate.lean =====
Missing aligns: {'function.commute.symm', 'function.semiconj.commute', 'function.commute.refl', 'function.semiconj₂.comp_eq', 'function.semiconj.inverses_right', 'function.commute.option_map', 'function.commute.comp_left', 'function.semiconj.id_right', 'function.semiconj.comp_eq', 'function.semiconj₂.comp', 'function.semiconj.id_left', 'function.semiconj', 'function.semiconj₂.id_left', 'function.semiconj.comp_right', 'function.semiconj.eq', 'function.commute.comp_right', 'function.semiconj.option_map', 'function.semiconj₂.eq', 'function.commute.id_right', 'function.semiconj₂', 'function.commute.id_left', 'function.commute', 'function.semiconj.comp_left'}

===== File mathlib/src/logic/function/basic.lean =====
Missing aligns: {'function.surj_inv', 'function.surjective_to_subsingleton', 'function.const_injective', 'function.extend', 'function.update_same', 'function.sometimes_spec', "function.extend_apply'", 'function.factors_through.apply_extend', 'function.involutive.ite_not', 'function.injective.of_comp', 'function.uncurry_apply_pair', "function.bijective.of_comp_iff'", 'function.surjective.exists', 'function.bijective.of_comp_iff', 'function.const_comp', 'function.update_comm', 'function.const_def', 'function.factors_through', 'eq_mp_bijective', 'function.right_inverse.comp_eq_id', 'function.bijective.comp_right', 'function.update', 'function.factors_through_iff', 'function.surjective.right_cancellable', 'function.surjective.exists₂', 'function.factors_through.extend_apply', 'function.surjective.forall₃', 'cast_inj', 'function.forall_update_iff', 'function.bicompr', 'function.extend_def', 'function.eval', 'function.eval_apply', 'function.cantor_injective', 'function.surjective_eval', 'function.update_eq_self', 'function.curry_apply', 'function.cantor_surjective', 'set.piecewise', 'function.left_inverse.cast_eq', 'function.bicompl', 'function.injective.ne_iff', 'function.sometimes', 'function.uncurry_bicompl', 'function.right_inverse.comp', 'function.injective.apply_extend', 'function.injective.eq_iff', "function.injective2.left'", 'function.surjective.injective_comp_right', 'function.exists_update_iff', 'function.ne_update_self_iff', 'function.injective2.right', 'function.update_comp_eq_of_injective', 'function.injective2.left', 'function.involutive_iff_iter_2_eq_id', 'function.comp_update', 'function.injective.comp_left', 'function.is_partial_inv', 'function.surjective.of_comp_iff', 'function.ne_iff', 'function.surjective.forall', 'function.left_inverse.eq_rec_eq', 'function.has_uncurry', 'function.bijective.comp_left', 'function.left_inverse.surjective', 'function.surjective.forall₂', 'function.funext_iff', 'function.surjective.exists₃', 'set.separates_points', 'function.eq_update_self_iff', 'function.injective2.eq_iff', 'function.update_eq_iff', 'eq_rec_inj', "function.injective.eq_iff'", 'function.comp_apply', "function.injective.surjective_comp_right'", "function.update_comp_eq_of_injective'", 'function.injective.surjective_comp_right', 'function.inv_fun', 'function.sometimes_eq', 'function.injective.extend_apply', 'function.involutive.eq_iff', 'function.eq_update_iff', 'function.injective.decidable_eq', 'function.id_def', 'function.involutive.comp_self', 'function.involutive', 'function.left_inverse.comp', 'function.extend_injective', 'function.factors_through.extend_comp', 'function.injective2', 'function.hfunext', 'function.apply_update₂', 'function.surjective_of_right_cancellable_Prop', 'function.injective.of_comp_iff', 'function.surjective.comp_left', 'bool.involutive_bnot', 'function.not_surjective_Type', 'function.update_injective', 'is_symm_op.flip_eq', 'function.left_inverse.comp_eq_id', 'function.partial_inv', 'function.injective.dite', 'function.const_inj', 'eq_rec_on_bijective', "function.injective.ne_iff'", 'function.update_ne_self_iff', 'function.uncurry_bicompr', 'function.update_comp_eq_of_forall_ne', 'function.extend_comp', 'function.injective_of_subsingleton', "function.surjective.of_comp_iff'", 'function.injective.factors_through', "function.injective.of_comp_iff'", "function.update_comp_eq_of_forall_ne'", 'function.update_noteq', 'function.update_eq_self_iff', 'function.injective2.uncurry', 'function.update_apply', 'function.update_idem', 'inv_image.equivalence', 'function.comp_const', 'function.left_inverse.eq_rec_on_eq', 'function.const_apply', 'eq_mpr_bijective', 'cast_bijective', 'function.apply_update', 'function.right_inverse.injective', 'function.uncurry_def', 'function.bijective_iff_has_inverse', 'function.surjective.of_comp', "function.injective2.right'"}

===== File mathlib/src/logic/embedding/set.lean =====
Missing aligns: {'function.embedding.coe_with_top_apply', 'set.embedding_of_subset_apply', 'function.embedding.option_embedding_equiv_symm_apply', 'function.embedding.option_elim_apply', 'function.embedding.image_apply', 'function.embedding.option_embedding_equiv_apply_snd_coe', 'subtype_or_equiv_apply', 'function.embedding.option_embedding_equiv_apply_fst'}

===== File mathlib/src/logic/embedding/basic.lean =====
Missing aligns: {'function.embedding.congr_apply', 'function.embedding.Pi_congr_right_apply', 'function.embedding.trans_apply', 'function.embedding.inr_apply', 'subtype.imp_embedding_apply_coe', 'function.embedding.some_apply', 'equiv.embedding_congr_apply', 'equiv.coe_eq_to_embedding', 'function.embedding.inl_apply', 'function.embedding.option_map_apply', 'function.embedding.sigma_map_apply', 'function.embedding.coe_option_apply', 'function.embedding.sectr_apply', 'function.embedding.refl_apply', 'equiv.as_embedding_apply', 'function.embedding.sectl_apply'}

===== File mathlib/src/category_theory/isomorphism.lean =====
Missing aligns: {'category_theory.iso.hom_inv_id', 'category_theory.iso.refl_hom', 'category_theory.functor.map_iso_inv', 'category_theory.iso.inv_hom_id', 'category_theory.iso.refl_inv', 'category_theory.iso.trans_inv', 'category_theory.iso.trans_hom', 'category_theory.iso.hom_inv_id_assoc', 'category_theory.iso.inv_hom_id_assoc', 'category_theory.is_iso.inv_hom_id_assoc', 'category_theory.functor.map_iso_hom', 'category_theory.is_iso.hom_inv_id_assoc'}

===== File mathlib/src/category_theory/natural_transformation.lean =====
Missing aligns: {'category_theory.nat_trans.ext_iff', 'category_theory.nat_trans.naturality_assoc', 'category_theory.nat_trans.naturality', 'category_theory.nat_trans.ext'}

===== File mathlib/src/category_theory/whiskering.lean =====
Missing aligns: {'category_theory.whiskering_right_map_app_app', 'category_theory.whisker_right_app', 'category_theory.functor.right_unitor_hom_app', 'category_theory.functor.associator_inv_app', 'category_theory.whiskering_left_obj_obj', 'category_theory.whiskering_left_obj_map', 'category_theory.functor.left_unitor_inv_app', 'category_theory.whiskering_right_obj_map', 'category_theory.whiskering_left_map_app_app', 'category_theory.functor.right_unitor_inv_app', 'category_theory.whisker_left_app', 'category_theory.functor.associator_hom_app', 'category_theory.functor.left_unitor_hom_app', 'category_theory.whiskering_right_obj_obj'}

===== File mathlib/src/category_theory/essential_image.lean =====
Missing aligns: {'category_theory.functor.to_ess_image_map', 'category_theory.functor.to_ess_image_comp_essential_image_inclusion_hom_app', 'category_theory.functor.to_ess_image_comp_essential_image_inclusion_inv_app', 'category_theory.functor.ess_image_inclusion_obj', 'category_theory.functor.to_ess_image_obj_obj', 'category_theory.functor.ess_image_inclusion_map'}

===== File mathlib/src/category_theory/natural_isomorphism.lean =====
Missing aligns: {"category_theory.nat_iso.naturality_2'_assoc", 'category_theory.iso.app_hom', 'category_theory.iso.app_inv', 'category_theory.nat_iso.of_components_hom_app', 'category_theory.iso.hom_inv_id_app_assoc', 'category_theory.nat_iso.of_components_inv_app', 'category_theory.nat_iso.hcomp_hom', 'category_theory.iso.inv_hom_id_app_assoc', 'category_theory.nat_iso.hcomp_inv'}

===== File mathlib/src/category_theory/full_subcategory.lean =====
Missing aligns: {'category_theory.full_subcategory.map_map', 'category_theory.full_subcategory.map_obj_obj', 'category_theory.induced_functor_obj', 'category_theory.full_subcategory.lift_obj_obj', 'category_theory.full_subcategory.ext', 'category_theory.full_subcategory.lift_map', 'category_theory.induced_functor_map', 'category_theory.full_subcategory.ext_iff'}

What happened to my file? /home/lean/actions-runner/_work/doc-gen/doc-gen/mathlib/src/category_theory/functor/default.lean

===== File mathlib/src/category_theory/functor/functorial.lean =====
Phantom aligns: {'category_theory.functorial.map'}

===== File mathlib/src/category_theory/functor/category.lean =====
Missing aligns: {'category_theory.functor.flip_map_app', 'category_theory.map_hom_inv_app_assoc', 'category_theory.nat_trans.hcomp_app', 'category_theory.functor.flip_obj_obj', 'category_theory.functor.flip_obj_map', 'category_theory.map_inv_hom_app_assoc'}

===== File mathlib/src/category_theory/functor/fully_faithful.lean =====
Missing aligns: {'category_theory.functor.preimage_iso_hom', 'category_theory.iso_equiv_of_fully_faithful_symm_apply', 'category_theory.functor.preimage_iso_inv', 'category_theory.nat_trans_of_comp_fully_faithful_app', 'category_theory.nat_iso_of_comp_fully_faithful_inv_app', 'category_theory.iso.faithful_of_comp', 'category_theory.nat_trans.equiv_of_comp_fully_faithful_symm_apply', 'category_theory.equiv_of_fully_faithful_symm_apply', 'category_theory.full.witness', 'category_theory.nat_iso.equiv_of_comp_fully_faithful_symm_apply', 'category_theory.iso_equiv_of_fully_faithful_apply', 'category_theory.faithful.map_injective', 'eq.faithful_of_comp', 'category_theory.equiv_of_fully_faithful_apply', 'category_theory.nat_iso_of_comp_fully_faithful_hom_app', 'category_theory.nat_trans.equiv_of_comp_fully_faithful_apply', 'category_theory.nat_iso.equiv_of_comp_fully_faithful_apply'}

===== File mathlib/src/category_theory/functor/basic.lean =====
Missing aligns: {'category_theory.functor.comp_obj', 'category_theory.functor.map_id', 'category_theory.functor.to_prefunctor_obj', 'category_theory.functor.map_comp_assoc', 'category_theory.functor.to_prefunctor', 'category_theory.functor.to_prefunctor_map', 'category_theory.functor.map_comp'}

===== File mathlib/src/category_theory/category/basic.lean =====
Missing aligns: {'category_theory.category.comp_id', 'category_theory.category.id_comp', 'category_theory.category.assoc'}

===== File mathlib/src/category_theory/concrete_category/bundled.lean =====
Missing aligns: {'category_theory.bundled.of', 'category_theory.bundled', 'category_theory.bundled.map', 'category_theory.bundled.coe_mk'}

===== File mathlib/src/combinatorics/quiver/single_obj.lean =====
Missing aligns: {'quiver.single_obj.to_prefunctor_apply_map', 'quiver.single_obj.to_prefunctor_apply_obj', 'quiver.single_obj.to_hom_symm_apply', 'quiver.single_obj.to_hom_apply', 'quiver.single_obj.to_prefunctor_symm_apply'}

===== File mathlib/src/combinatorics/quiver/connected_component.lean =====
Missing aligns: {'quiver.wide_subquiver_symmetrify', 'quiver.weakly_connected_component', 'quiver.weakly_connected_component.eq', 'quiver.weakly_connected_component.mk', 'quiver.zigzag_setoid'}

===== File mathlib/src/combinatorics/quiver/symmetric.lean =====
Missing aligns: {'quiver.has_reverse', 'prefunctor.symmetrify_obj', 'quiver.symmetrify', 'quiver.path.reverse_reverse', 'quiver.symmetrify.lift', 'quiver.reverse', 'quiver.symmetrify.lift_reverse', 'quiver.symmetrify.of_map', 'prefunctor.symmetrify', 'quiver.symmetrify.of', 'prefunctor.symmetrify_map', 'quiver.symmetrify.of_obj', 'quiver.has_involutive_reverse', 'quiver.symmetrify.lift_spec', 'quiver.path.reverse_comp', 'quiver.path.reverse'}

===== File mathlib/src/combinatorics/quiver/subquiver.lean =====
Missing aligns: {'quiver.wide_subquiver_equiv_set_total', 'quiver.total.ext_iff', 'quiver.total.ext', 'quiver.total', 'quiver.labelling', 'wide_subquiver'}

===== File mathlib/src/combinatorics/quiver/basic.lean =====
Missing aligns: {'prefunctor.comp_obj', 'prefunctor.id_map', 'prefunctor.id_obj', 'prefunctor.comp_map'}
Phantom aligns: {'quiver.hom'}

===== File mathlib/src/combinatorics/quiver/path.lean =====
Missing aligns: {'quiver.path.nil_ne_cons', 'quiver.path.length', 'quiver.path.comp_inj_left', 'quiver.path.length_cons', 'quiver.hom.to_path', 'quiver.path.comp_injective_right', 'quiver.path', 'quiver.path.nil_comp', 'quiver.path.obj_eq_of_cons_eq_cons', 'quiver.path.comp_inj', 'quiver.path.comp', 'quiver.path.comp_assoc', 'quiver.path.comp_cons', 'quiver.path.comp_inj_right', 'quiver.path.comp_nil', 'quiver.path.length_nil', 'quiver.path.heq_of_cons_eq_cons', 'quiver.path.hom_heq_of_cons_eq_cons', "quiver.path.comp_inj'", 'quiver.path.comp_injective_left', 'quiver.path.to_list', 'quiver.path.eq_of_length_zero', 'quiver.path.cons_ne_nil', 'quiver.path.length_comp'}

===== File mathlib/src/deprecated/group.lean =====
Missing aligns: {"is_add_group_hom.mk'", 'add_monoid_hom.is_add_monoid_hom_coe', 'is_add_group_hom.add', 'is_add_group_hom.map_sub', 'add_monoid_hom.coe_of', 'is_add_monoid_hom.comp', 'is_add_group_hom.to_is_add_monoid_hom', 'is_add_group_hom.map_neg', 'is_add_hom.neg', 'is_add_hom.id', 'add_equiv.is_add_hom', 'add_monoid_hom.is_add_group_hom', 'add_monoid_hom.of', 'is_add_group_hom.neg', 'is_add_monoid_hom.neg', 'is_add_group_hom.comp', 'is_add_group_hom.map_zero', 'is_add_monoid_hom.id', 'is_add_hom.comp', 'is_add_hom.add', 'is_add_group_hom.id', 'is_add_group_hom.injective_iff', 'is_add_monoid_hom.map_add', 'add_equiv.is_add_monoid_hom', 'is_add_hom.to_is_add_monoid_hom', 'add_equiv.is_add_group_hom', 'neg.is_add_group_hom'}

===== File mathlib/src/control/basic.lean =====
Missing aligns: {'fish'}

===== File mathlib/src/control/equiv_functor.lean =====
Missing aligns: {'equiv_functor.map_trans', 'equiv_functor.map_refl'}

===== File mathlib/src/control/functor.lean =====
Phantom aligns: {'functor.map_const_rev'}

===== File mathlib/src/group_theory/congruence.lean =====
Missing aligns: {'add_con.quotient_ker_equiv_of_surjective', 'add_con.ker_lift', 'add_con.map_apply', 'add_con.quotient_ker_equiv_of_right_inverse', 'add_con.lift_surjective_of_surjective', 'add_con.lift_range', 'add_con.comap_quotient_equiv', 'con.quotient_ker_equiv_of_right_inverse_symm_apply', "add_con.mk'_ker", 'add_con.lift_unique', 'add_con.add_con_gen_of_add_con', 'add_con.ker_lift_range_eq', 'add_con.neg', 'add_con.ker_eq_lift_of_injective', "add_con.lift_comp_mk'", 'add_con.comap_eq', "add_con.lift_apply_mk'", "add_con.mrange_mk'", 'add_con.zsmul', 'add_con.quotient_ker_equiv_range', 'add_con.sub', 'add_con.map', 'add_con.ker_lift_injective', 'add_con.ker', 'add_con.ker_rel', 'con.quotient_ker_equiv_of_right_inverse_apply', 'add_con.lift_funext', 'add_con.induction_on_add_units', 'add_con.to_add_submonoid_inj', 'add_con.nsmul', "add_con.coe_mk'", 'add_con.lift_coe', 'add_con.quotient_quotient_equiv_quotient', 'add_con.ker_lift_mk', 'add_con.le_iff', 'add_con.quotient_ker_equiv_of_right_inverse_symm_apply', 'add_con.quotient_ker_equiv_of_right_inverse_apply', 'add_con.vadd', 'add_con.lift', "add_con.lift_mk'", 'add_con.mem_coe', "add_con.mk'_surjective", 'add_con.coe_vadd', 'add_con.ker_apply_eq_preimage', "add_con.mk'"}
Phantom aligns: {'add_con.add_con_gen_of_con'}

===== File mathlib/src/group_theory/eckmann_hilton.lean =====
Missing aligns: {'eckmann_hilton.add_zero_class.is_unital', 'eckmann_hilton.add_comm_group', 'eckmann_hilton.add_comm_monoid'}

===== File mathlib/src/group_theory/perm/basic.lean =====
Missing aligns: {'equiv.perm.extend_domain_hom_apply', 'equiv.add_right_add', 'equiv.zpow_add_left', 'set.bij_on.of_perm_inv', 'equiv.perm.subtype_equiv_subtype_perm_apply_coe', 'equiv.pow_mul_left', 'equiv.inv_mul_left', 'equiv.perm.subtype_congr_hom_apply', 'equiv.perm.extend_domain_pow', 'equiv.pow_add_left', 'equiv.perm.coe_equiv_units_End_apply', 'equiv.mul_right_one', 'set.bij_on_perm_inv', 'equiv.inv_add_left', 'equiv.pow_mul_right', 'equiv.perm.sum_congr_hom_apply', 'equiv.perm.equiv_units_End_symm_apply_apply', 'equiv.perm.subtype_equiv_subtype_perm_symm_apply', 'equiv.inv_add_right', 'equiv.perm.coe_inv_equiv_units_End_apply', 'monoid_hom.to_hom_perm_apply_symm_apply', 'equiv.mul_left_mul', 'equiv.mul_left_one', 'monoid_hom.to_hom_perm_apply_apply', 'equiv.perm.extend_domain_zpow', 'equiv.zpow_mul_left', 'equiv.add_left_zero', 'equiv.zpow_mul_right', 'equiv.inv_mul_right', 'equiv.pow_add_right', 'equiv.perm.equiv_units_End_symm_apply_symm_apply', 'equiv.add_right_zero', 'equiv.mul_right_mul', 'equiv.perm.sigma_congr_right_hom_apply', 'equiv.add_left_add', 'equiv.zpow_add_right'}

===== File mathlib/src/group_theory/subsemigroup/operations.lean =====
Missing aligns: {'subsemigroup.top_equiv_apply', 'mul_hom.subsemigroup_map_apply_coe', 'add_equiv.of_left_inverse_apply', 'mul_hom.cod_restrict_apply_coe', 'add_hom.restrict', 'mul_equiv.of_left_inverse_apply', 'subsemigroup.to_add_subsemigroup_symm_apply_coe', 'add_equiv.subsemigroup_map_apply_coe', 'add_subsemigroup.top_equiv_apply', 'mul_hom.subsemigroup_comap_apply_coe', 'add_equiv.of_left_inverse_symm_apply', 'subsemigroup.to_add_subsemigroup_apply_coe', 'add_hom.subsemigroup_comap_apply_coe', 'add_hom.subsemigroup_map_apply_coe', 'add_hom.cod_restrict_apply_coe', 'add_subsemigroup.to_subsemigroup_symm_apply_coe', 'mul_equiv.subsemigroup_map_symm_apply_coe', 'add_subsemigroup.to_subsemigroup_apply_coe', 'add_subsemigroup.top_equiv_symm_apply_coe', 'subsemigroup.top_equiv_symm_apply_coe', 'mul_equiv.subsemigroup_map_apply_coe', 'add_subsemigroup.equiv_map_of_injective', 'mul_equiv.of_left_inverse_symm_apply', 'add_equiv.subsemigroup_map_symm_apply_coe'}

===== File mathlib/src/group_theory/subsemigroup/membership.lean =====
Missing aligns: {'add_subsemigroup.mem_sup_left', 'add_subsemigroup.coe_Sup_of_directed_on', 'add_subsemigroup.mem_supr_of_mem', 'add_subsemigroup.mem_sup_right', 'add_subsemigroup.add_mem_sup', 'add_subsemigroup.supr_induction', 'add_subsemigroup.mem_supr_of_directed', 'add_subsemigroup.mem_Sup_of_directed_on', "add_subsemigroup.supr_induction'", 'add_subsemigroup.mem_Sup_of_mem', 'add_subsemigroup.coe_supr_of_directed'}

===== File mathlib/src/group_theory/submonoid/operations.lean =====
Missing aligns: {'monoid_hom.cod_restrict_apply', 'add_equiv.add_submonoid_map_symm_apply', "add_equiv.of_left_inverse'_apply", 'add_submonoid.to_submonoid_apply_coe', 'submonoid.top_equiv_symm_apply_coe', "mul_equiv.of_left_inverse'_apply", 'add_monoid_hom.cod_restrict_apply', 'submonoid.top_equiv_apply', 'add_monoid_hom.add_submonoid_comap_apply_coe', "add_equiv.of_left_inverse'_symm_apply", 'mul_equiv.submonoid_map_symm_apply', "mul_equiv.of_left_inverse'_symm_apply", 'add_monoid_hom.add_submonoid_map_apply_coe', 'add_equiv.coe_add_submonoid_map_apply', 'add_submonoid.top_equiv_apply', 'add_submonoid.coe_nsmul', 'submonoid.equiv_map_of_injective_coe_mul_equiv', 'add_submonoid.equiv_map_of_injective_coe_add_equiv', 'mul_equiv.coe_submonoid_map_apply', 'add_submonoid.top_equiv_symm_apply_coe', 'add_submonoid.to_submonoid_symm_apply_coe', 'monoid_hom.submonoid_map_apply_coe', 'submonoid.to_add_submonoid_apply_coe', 'monoid_hom.submonoid_comap_apply_coe', 'submonoid.to_add_submonoid_symm_apply_coe'}
Phantom aligns: {'add_submonoid.coe_smul'}

===== File mathlib/src/group_theory/submonoid/membership.lean =====
Missing aligns: {'submonoid.pow_coe', 'submonoid.pow_log_equiv_symm_apply', 'submonoid.pow_log_equiv_apply'}

===== File mathlib/src/group_theory/submonoid/basic.lean =====
Missing aligns: {'add_submonoid.copy_eq', 'add_submonoid.mk_le_mk', 'add_submonoid.mem_carrier', 'add_monoid_hom.eq_mlocus_same', 'add_monoid_hom.eq_of_eq_on_mtop', 'add_submonoid.mem_supr', 'add_submonoid.coe_top', 'add_submonoid.closure_singleton_le_iff_mem', 'add_submonoid.mem_mk', 'add_submonoid.closure_le', 'is_add_unit.add_submonoid', 'add_submonoid.copy', 'add_monoid_hom.coe_of_mclosure_eq_top_right', 'add_submonoid.closure_empty', 'add_monoid_hom.coe_of_mclosure_eq_top_left', 'add_submonoid.mem_closure', "add_submonoid.disjoint_def'", 'add_submonoid.disjoint_def', 'add_submonoid.coe_Inf', 'add_submonoid.closure_mono', 'add_monoid_hom.eq_on_mclosure', 'add_submonoid.closure_univ', "add_submonoid.closure_induction'", 'is_add_unit.mem_add_submonoid_iff', 'add_submonoid.supr_eq_closure', 'add_submonoid.not_mem_of_not_mem_closure', 'add_submonoid.zero_mem', 'add_submonoid.dense_induction', 'add_submonoid.closure_union', 'add_submonoid.mem_Inf', 'add_submonoid.to_add_subsemigroup', 'add_submonoid.closure_eq', 'add_submonoid.closure_eq_of_le', 'add_submonoid.closure', 'add_submonoid.coe_set_mk', 'add_submonoid.mem_top', 'submonoid.to_subsemigroup', 'add_monoid_hom.of_mclosure_eq_top_right', 'add_submonoid.subsingleton_iff', 'add_submonoid.gi', 'add_submonoid.subset_closure', 'add_submonoid.add_mem', 'add_submonoid.coe_infi', 'add_submonoid.mem_inf', 'add_submonoid.closure_induction', 'add_submonoid.nontrivial_iff', 'add_submonoid.closure_Union', 'add_monoid_hom.eq_mlocus', 'add_submonoid.simps.coe', 'add_submonoid.ext', 'add_submonoid.closure_induction₂', 'add_submonoid.mem_bot', 'add_submonoid.coe_inf', 'add_submonoid.coe_bot', 'add_monoid_hom.of_mclosure_eq_top_left', 'add_submonoid.coe_copy', 'add_submonoid.mem_infi', 'add_monoid_hom.eq_of_eq_on_mdense'}

===== File mathlib/src/group_theory/group_action/support.lean =====
Missing aligns: {'add_action.supports.vadd', 'add_action.supports.mono', 'add_action.supports_of_mem', 'add_action.supports'}

===== File mathlib/src/group_theory/group_action/sigma.lean =====
Missing aligns: {'sigma.vadd_def', "sigma.has_faithful_vadd'", 'sigma.vadd_mk'}

===== File mathlib/src/group_theory/group_action/option.lean =====
Missing aligns: {'option.vadd_none', 'option.vadd_some', 'option.vadd_def'}

===== File mathlib/src/group_theory/group_action/sum.lean =====
Missing aligns: {'sum.vadd_swap', 'sum.vadd_inr', 'sum.vadd_def', 'sum.vadd_inl'}

===== File mathlib/src/group_theory/group_action/group.lean =====
Missing aligns: {'mul_aut_arrow_apply_apply', 'distrib_mul_action.to_add_equiv_symm_apply', 'mul_distrib_mul_action.to_mul_aut_apply', 'add_action.bijective', 'arrow_add_action', 'add_action.to_perm', 'vadd_eq_iff_eq_neg_vadd', 'add_action.to_perm_apply', 'mul_distrib_mul_action.to_mul_equiv_symm_apply', 'is_add_unit.vadd_left_cancel', 'vadd_neg_vadd', 'mul_action.to_perm_symm_apply', 'add_action.to_perm_injective', 'vadd_left_cancel', 'vadd_left_cancel_iff', 'mul_action.to_perm_apply', 'eq_neg_vadd_iff', 'arrow_action_to_has_smul_smul', 'add_action.injective', 'mul_distrib_mul_action.to_mul_equiv_apply', 'arrow_add_action_to_has_vadd_vadd', 'distrib_mul_action.to_add_aut_apply', 'neg_vadd_eq_iff', 'distrib_mul_action.to_add_equiv_apply', 'add_action.to_perm_symm_apply', 'neg_vadd_vadd', 'mul_action.to_perm_hom_apply', 'add_action.surjective', 'add_action.to_perm_hom_apply', 'mul_aut_arrow_apply_symm_apply'}

===== File mathlib/src/group_theory/group_action/prod.lean =====
Missing aligns: {'smul_mul_hom_apply', 'smul_monoid_hom_apply'}

===== File mathlib/src/group_theory/group_action/pi.lean =====
Missing aligns: {'function.update_vadd', 'set.piecewise_vadd', 'function.extend_vadd'}

===== File mathlib/src/group_theory/group_action/defs.lean =====
Missing aligns: {'function.surjective.add_action', 'mul_distrib_mul_action.to_monoid_End_apply', "has_vadd.comp.vadd_comm_class'", 'vadd_zero_hom_apply', 'vadd_vadd', 'vadd_comm_class.symm', 'add_action.exists_vadd_eq', 'smul_zero_class.to_zero_hom_apply', 'vadd_comm_class.of_add_vadd_zero', 'distrib_mul_action.to_add_monoid_hom_apply', 'add_action.ext', 'vadd_add_assoc', 'function.surjective.add_action_left', 'function.injective.add_action', 'distrib_mul_action.to_add_monoid_End_apply', 'vadd_zero_add', 'zero_vadd', 'add_action.ext_iff', 'vadd_add_vadd', 'vadd_ite', 'add_vadd_comm', 'ite_vadd', "vadd_left_injective'", 'vadd_zero_hom', 'add_commute.vadd_left', 'comp_vadd_left', 'is_central_vadd.unop_vadd_eq_vadd', 'add_action.to_fun', 'add_action.comp_hom', 'smul_one_hom_apply', 'has_vadd.comp.vadd_assoc_class', 'distrib_mul_action.ext_iff', 'distrib_smul.ext', 'add_commute.vadd_right', 'add_action.to_fun_apply', 'vadd_assoc_class.of_vadd_zero_add', 'vadd_eq_add', 'mul_action.ext_iff', 'mul_distrib_mul_action.ext', 'has_vadd.comp', 'add_action.surjective_vadd', 'vadd_zero_vadd', 'vadd_assoc', 'distrib_smul.to_add_monoid_hom_apply', 'has_vadd.comp.vadd', 'mul_action.ext', 'distrib_mul_action.ext', 'zero_vadd_eq_id', 'vadd_vadd_vadd_comm', 'has_vadd.comp.vadd_comm_class', 'distrib_smul.ext_iff', 'add_vadd_zero', 'mul_distrib_mul_action.ext_iff'}

===== File mathlib/src/data/subtype.lean =====
Missing aligns: {'subtype.val_injective', 'subtype.map_id', 'subtype.coind_coe', 'subtype.val_prop', 'subtype.val_inj', 'subtype.coind_injective', 'subtype.coind_surjective', 'subtype.symm', 'subtype.val_eq_coe', 'subtype.ext_iff_val', 'subtype.map_injective', 'subtype.ext', 'subtype.equiv_iff', "subtype.forall'", 'exists_eq_subtype_mk_iff', 'subtype.coe_eq_of_eq_mk', 'subtype.surjective_restrict', 'exists_subtype_mk_eq_iff', 'subtype.restrict_apply', 'subtype.map_involutive', 'subtype.mk_eq_mk', 'subtype.map_comp', 'subtype.refl', 'subtype.ext_iff', 'subtype.coe_inj', 'subtype.restrict_def', 'subtype.prop', 'subtype.coe_injective', "subtype.exists'", 'subtype.map', 'subtype.heq_iff_coe_eq', 'subtype.coe_eq_iff', 'subtype.trans', 'subtype.ext_val', 'subtype.restrict_injective', 'subtype.simps.coe', 'subtype.equivalence', 'subtype.coind_bijective', 'subtype.coe_prop', 'subtype.heq_iff_coe_heq', 'subtype.coind', 'subtype.exists', 'subtype.coe_mk', 'subtype.forall', 'subtype.map_coe', 'subtype.restrict', 'subtype.coe_eta'}

===== File mathlib/src/data/part.lean =====
Missing aligns: {'part.to_option_is_some', 'part.zero_mem_zero', 'part.add_get_eq', 'part.some_sub_some', 'part.sub_mem_sub', 'part.sub_get_eq', 'part.map_dom', 'part.neg_some', 'part.to_option_is_none', 'part.left_dom_of_sub_dom', 'part.neg_mem_neg', 'part.add_mem_add', 'part.right_dom_of_add_dom', 'part.right_dom_of_sub_dom', 'part.some_add_some', 'part.left_dom_of_add_dom', 'part.map_get'}

===== File mathlib/src/data/typevec.lean =====
Missing aligns: {'typevec.nil_fun_comp'}
Phantom aligns: {'typevec.nilFun_comp'}

===== File mathlib/src/data/quot.lean =====
Missing aligns: {"quotient.mk'_eq_mk", "quotient.map'_mk", "quotient.lift_on'", "quotient.sound'", 'quot.map', 'trunc.induction_on₂', "quotient.mk'", 'quot.map₂_mk', 'trunc.map', "quotient.lift_on₂'_mk'", 'quotient.lift_comp_mk', 'quotient.out_eq', 'surjective_quot_mk', 'trunc.exists_rep', 'quotient.choice', 'quotient.map_mk', 'quot.out_eq', 'quotient.eq_mk_iff_out', "quotient.map₂'", "quotient.hrec_on'", "quotient.mk_out'", 'quotient.mk_out', 'quot.map₂', "quotient.map'_mk'", 'setoid.ext', 'quot.induction_on₃', 'trunc.rec_on', 'trunc.mk', 'quot.eq', 'trunc.rec_on_subsingleton', 'trunc.induction_on', 'nonempty_quotient_iff', 'trunc.out_eq', 'quotient.map₂_mk', 'quot.factor_mk_eq', "quotient.rec_on_subsingleton₂'", "quotient.map'", 'quot.hrec_on₂', "quotient.rec_on_subsingleton'", 'quot.factor', 'quot.lift_mk', 'quotient.lift_mk', 'quotient.choice_eq', 'quotient.lift₂_mk', 'quotient.map₂', "quotient.hrec_on₂'", 'quot.lift_on₂', 'trunc.lift_on', 'trunc.eq', "quotient.exact'", 'trunc.out', "quotient.out_eq'", 'quotient.out_inj', 'quotient.eq', 'quot.out', 'quot.lift₂_mk', 'surjective_quotient_mk', 'quot.lift₂', 'trunc.nonempty', 'trunc.ind', 'trunc.bind', 'quot.map_right', "quotient.lift_on'_mk'", 'trunc.rec', 'quotient.map', 'quotient.induction_on_pi', 'trunc.lift', 'quot.induction_on₂', "quotient.ind₂'", "quotient.eq'", 'forall_quotient_iff', 'quot.rec_on_subsingleton₂', 'quotient.out_injective', 'trunc.lift_mk', 'true_equivalence', 'trunc', "quotient.lift_on₂'", 'quotient.out', 'quotient.hrec_on₂', "quotient.out'", "quotient.ind'", 'quotient.mk_eq_iff_out', "quotient.map₂'_mk'", 'quotient.out_equiv_out'}
Phantom aligns: {'setoid.r', 'quot.lift_beta', 'quotient.mk'}

===== File mathlib/src/data/two_pointing.lean =====
Missing aligns: {'two_pointing.ext', 'two_pointing.swap_to_prod', 'two_pointing.ext_iff'}

===== File mathlib/src/data/opposite.lean =====
Missing aligns: {'opposite.rec', 'opposite.equiv_to_opposite', 'opposite.op_eq_iff_eq_unop', 'opposite.op_injective', 'opposite.unop_eq_iff_eq_op', 'opposite.op', 'opposite.op_unop', 'opposite.unop_inj_iff', 'opposite.op_inj_iff', 'opposite.unop_op', 'opposite.unop'}

What happened to my file? /home/lean/.elan/toolchains/leanprover-community--lean---3.50.3/lib/lean/library/lean_core/data/vector.lean

===== File mathlib/src/data/vector/basic.lean =====
Missing aligns: {'vector.replicate', "vector.sum_update_nth'", 'vector.nth_replicate', 'vector.sum_update_nth'}
Phantom aligns: {'vector.nth_repeat'}

===== File mathlib/src/data/real/basic.lean =====
Missing aligns: {'real.ring_equiv_Cauchy_apply', 'real.ring_equiv_Cauchy_symm_apply_cauchy'}

===== File mathlib/src/data/real/cau_seq_completion.lean =====
Missing aligns: {'cau_seq.completion.of_rat_ring_hom_apply'}
Phantom aligns: {'cau_seq.is_complete.is_complete'}

===== File mathlib/src/data/num/basic.lean =====
Phantom aligns: {'num.pos', 'znum.pos'}

===== File mathlib/src/data/rat/init.lean =====
Missing aligns: {'rat.repr', 'rat', 'rat.ext_iff', 'rat.ext'}
Phantom aligns: {'rat.denom'}

===== File mathlib/src/data/rat/cast.lean =====
Missing aligns: {'rat.cast_order_embedding_apply'}

===== File mathlib/src/data/rat/floor.lean =====
Missing aligns: {'rat.floor'}

===== File mathlib/src/data/rat/defs.lean =====
Missing aligns: {'rat.mk'}
Phantom aligns: {'rat.pos'}

===== File mathlib/src/data/setoid/basic.lean =====
Missing aligns: {'setoid.quotient_ker_equiv_of_right_inverse_symm_apply', 'setoid.quotient_ker_equiv_of_right_inverse_apply'}

===== File mathlib/src/data/set/bool_indicator.lean =====
Missing aligns: {'set.preimage_bool_indicator_tt', 'set.preimage_bool_indicator_ff'}
Phantom aligns: {'set.preimage_bool_indicator_false', 'set.preimage_bool_indicator_true'}

===== File mathlib/src/data/set/sigma.lean =====
Missing aligns: {'set.image_sigma_mk_preimage_sigma_map_subset'}
Phantom aligns: {'set.image_sigma_mk_preimage_sigmaMap_subset'}

===== File mathlib/src/data/set/image.lean =====
Missing aligns: {'function.surjective.range_eq'}

===== File mathlib/src/data/set/opposite.lean =====
Missing aligns: {'set.op', 'set.op_equiv_symm_apply', 'set.unop', 'set.op_equiv', 'set.singleton_op_unop', 'set.mem_op', 'set.op_equiv_self_symm_apply_coe', 'set.singleton_unop_op', 'set.op_mem_op', 'set.op_unop', 'set.singleton_unop', 'set.mem_unop', 'set.singleton_op', 'set.unop_op', 'set.op_equiv_apply', 'set.unop_mem_unop', 'set.op_equiv_self_apply_coe'}

===== File mathlib/src/data/set/basic.lean =====
Missing aligns: {'set.eq_univ_of_univ_subset', 'has_le.le.subset', 'set.nonempty.not_disjoint', 'set.nonempty.ne_empty', 'has_lt.lt.ssubset', 'set.nontrivial.coe_sort', 'disjoint.subset_compl_left', 'set.subsingleton.not_nontrivial', 'set.disjoint_sdiff_right', 'has_ssubset.ssubset.lt', 'disjoint.subset_compl_right', 'set.nonempty.empty_ssubset', 'has_subset.subset.le', 'set.nonempty.coe_sort', 'has_subset.subset.disjoint_compl_right', 'has_subset.subset.disjoint_compl_left', 'set.disjoint_sdiff_left', 'set.nontrivial.not_subsingleton'}
Phantom aligns: {'set.mem_set_of_eq'}

===== File mathlib/src/data/set/prod.lean =====
Missing aligns: {'set.subsingleton.off_diag_eq_empty', 'set.nontrivial.off_diag_nonempty'}

===== File mathlib/src/data/set/function.lean =====
Missing aligns: {'function.injective.inj_on', 'set.inv_on_empty', 'set.inv_on_singleton', 'set.left_inv_on_singleton', 'strict_mono.of_restrict', 'set.right_inv_on_empty', 'function.injective.restrict_preimage', 'set.inj_on.injective', 'function.bijective.bij_on_univ', 'strict_mono_on.restrict', 'set.left_inv_on_empty', 'set.restrict_preimage_coe', 'set.inj_on.ne', 'function.injective.cod_restrict', 'function.bijective.restrict_preimage', 'set.eq_on.comp_eq', 'function.surjective.restrict_preimage', 'set.right_inv_on_singleton', 'set.eq_on_singleton'}

===== File mathlib/src/data/set/finite.lean =====
Missing aligns: {'set.finite_diff_Union_Ioo', 'finite.of_forall_not_lt_lt', "set.finite_diff_Union_Ioo'", 'set.finite_of_forall_not_lt_lt'}
Phantom aligns: {'set.finite_of_forall_between_eq_endpoints'}

===== File mathlib/src/data/set/n_ary.lean =====
Missing aligns: {'set.image2_right_identity', 'set.image2_left_identity'}

===== File mathlib/src/data/set/intervals/unordered_interval.lean =====
Missing aligns: {'set.uIoc_swap'}
Phantom aligns: {'set.uIoc_comm'}

===== File mathlib/src/data/set/intervals/group.lean =====
Missing aligns: {'set.neg_mem_Icc_iff', 'set.neg_mem_Ioc_iff', 'set.neg_mem_Ioo_iff', 'set.neg_mem_Ico_iff'}

===== File mathlib/src/data/set/intervals/ord_connected.lean =====
Phantom aligns: {'set.OrdConnected_Iio'}

===== File mathlib/src/data/set/pointwise/smul.lean =====
Missing aligns: {'set.vadd_set_Inter_subset', 'set.image2_vadd', 'set.vadd_set_singleton', 'set.vadd_subset_iff', 'set.vadd_set_Union', 'set.add_action', 'set.has_vadd_set', 'set.union_vadd', 'set.mem_vadd_set_iff_neg_vadd_mem', 'set.vadd_set_Union₂', 'set.set_vadd_subset_set_vadd_iff', 'set.subset_set_vadd_iff', 'set.bUnion_vadd_set', 'set.vadd_nonempty', 'set.vadd_inter_ne_empty_iff', 'set.vadd_univ', 'set.op_vadd_inter_ne_empty_iff', 'set.Inter₂_vadd_subset', 'set.inter_vadd_subset', 'set.vadd_set_union', 'set.Union₂_vadd', 'set.vadd_mem_vadd', 'set.Union_vadd', 'set.Inter_vadd_subset', 'set.mem_vadd', 'set.vadd_eq_empty', 'set.preimage_vadd', 'set.vadd_set_range', 'set.nonempty.vadd_set', "set.vadd_inter_ne_empty_iff'", 'set.pairwise_disjoint_vadd_iff', 'set.nonempty.of_vadd_left', 'set.vadd_set_inter', 'set.Union_vadd_eq_set_of_exists', 'set.vadd_subset_vadd_right', 'set.vadd_set_subset_iff', 'set.preimage_vadd_neg', 'set.singleton_vadd_singleton', 'set.bUnion_op_vadd_set', 'set.Union_vadd_left_image', 'set.vadd_set_symm_diff', 'set.Union_vadd_right_image', 'set.set_vadd_subset_iff', 'set.vadd_inter_subset', 'set.mem_neg_vadd_set_iff', 'set.vadd_Union₂', 'set.vadd_empty', 'set.vadd_set_eq_empty', 'set.vadd_set_nonempty', 'set.vadd_Union', 'set.vadd_Inter₂_subset', 'set.vadd_set_inter_subset', 'set.vadd_union', 'set.vadd_subset_vadd', 'set.vadd_mem_vadd_set', 'set.mem_vadd_set', 'set.vadd_singleton', 'set.empty_vadd', 'set.vadd_subset_vadd_left', 'set.has_vadd', 'set.singleton_vadd', 'set.range_vadd_range', 'set.nonempty.vadd', 'set.add_action_set', 'set.vadd_Inter_subset', 'set.vadd_set_empty', 'set.vadd_set_Inter₂_subset', 'set.vadd_mem_vadd_set_iff', 'set.vadd_set_mono', 'set.Union_neg_vadd', 'set.vadd_set_univ', 'set.image_vadd', 'set.vadd_set_sdiff', 'set.nonempty.of_vadd_right'}

===== File mathlib/src/data/set/pointwise/iterate.lean =====
Missing aligns: {'vadd_eq_self_of_preimage_zsmul_eq_self'}

===== File mathlib/src/data/set/pointwise/list_of_fn.lean =====
Missing aligns: {'set.mem_nsmul'}

===== File mathlib/src/data/set/pointwise/basic.lean =====
Missing aligns: {'set.is_add_unit_iff_singleton', 'set.singleton_add_hom', 'set.singleton_add', 'set.add_semigroup', 'set.inter_add_subset', 'set.neg_singleton', 'set.sub_subset_sub_right', 'set.neg_subset', 'set.singleton_zero_hom', 'set.add_monoid', 'set.sub_subset_sub_left', 'set.Inter_sub_subset', 'set.add_Union', 'set.empty_sub', 'set.is_add_unit_iff', 'set.sub_eq_empty', 'set.Union_sub_left_image', "set.preimage_add_right_zero'", 'set.nonempty.zero_mem_sub', 'set.preimage_sub_preimage_subset', 'set.coe_singleton_add_monoid_hom', 'set.empty_nsmul', 'set.nonempty.of_add_right', 'disjoint.one_not_mem_div_set', 'set.union_sub', 'is_add_unit.set', 'set.preimage_add_right_singleton', 'set.singleton_add_hom_apply', 'set.union_add', 'set.add_inter_subset', 'set.add_Inter₂_subset', 'set.nsmul_subset_nsmul', 'set.preimage_add_left_zero', 'set.Union_add_left_image', 'set.Union_sub_right_image', 'set.subtraction_monoid', 'set.singleton_zero', 'set.has_zero', 'set.singleton_add_singleton', 'set.image_zero', 'set.add_comm_semigroup', 'set.neg_mem_neg', 'set.nonempty.sub', 'set.nonempty.of_sub_left', 'set.sub_Inter₂_subset', 'set.image_op_add', 'set.add_empty', "set.image_add_right'", 'set.subset_add_right', 'set.preimage_add_right_zero', 'set.sub_subset_sub', 'set.add_subset_add_right', "set.preimage_add_left_zero'", "set.image_add_left'", 'set.image_add_left', 'set.add_subset_add', 'set.neg_insert', 'set.sub_subset_iff', 'set.neg_preimage', 'set.mem_zero', 'set.add_subset_add_left', 'set.neg_empty', 'set.has_neg', 'set.has_add', 'set.add_Inter_subset', 'set.sub_inter_subset', 'set.coe_singleton_zero_hom', 'set.sub_empty', 'set.image2_add', 'set.add_mem_add', 'set.nonempty.neg', 'set.add_univ_of_zero_mem', 'set.nsmul_subset_nsmul_of_zero_mem', 'set.Inter₂_add_subset', 'set.sub_union', 'set.subtraction_comm_monoid', 'set.add_image_prod', 'set.subset_zero_iff_eq', 'set.Union_neg', 'set.subset_add_left', 'set.mem_add', 'set.Union_add_right_image', 'set.univ_add_of_zero_mem', 'set.compl_neg', 'set.inter_sub_subset', 'set.sub_singleton', 'set.image_op_neg', 'set.zero_nonempty', 'set.not_zero_mem_sub_iff', 'set.add_comm_monoid', 'set.singleton_add_monoid_hom', 'set.sub_Union₂', 'disjoint.zero_not_mem_sub_set', 'set.image_neg', 'set.image_add', 'set.singleton_sub_singleton', 'set.nonempty.of_add_left', 'set.zero_subset', 'set.add_zero_class', 'set.preimage_add_left_singleton', 'set.nonempty.add', 'set.zero_mem_zero', 'set.add_singleton', 'set.empty_add', 'set.zero_mem_sub_iff', 'set.add_nonempty', 'set.sub_Inter_subset', 'set.add_Union₂', 'set.nonempty_neg', 'set.union_neg', 'set.Inter_add_subset', 'set.neg_subset_neg', 'set.nsmul_mem_nsmul', 'set.singleton_sub', 'set.bdd_above_add', 'set.sub_nonempty', 'set.preimage_add_preimage_subset', 'set.Inter_neg', 'set.nonempty.subset_zero_iff', 'set.inter_neg', 'set.is_add_unit_singleton', 'set.add_eq_zero_iff', 'set.Union₂_add', 'set.add_eq_empty', 'set.coe_singleton_add_hom', 'set.univ_add', 'set.neg_range', 'set.Union₂_sub', 'set.sub_Union', 'set.Inter₂_sub_subset', 'set.Union_add', 'set.has_sub', 'set.add_union', 'set.nonempty.of_sub_right', 'set.singleton_add_monoid_hom_apply', 'set.neg_univ', 'set.image2_sub', 'set.add_subset_iff', 'set.sub_mem_sub', 'set.add_univ', 'set.mem_neg', 'set.Union_sub', 'set.mem_sub', 'set.image_sub', 'set.univ_add_univ', 'set.image_add_right'}

===== File mathlib/src/data/dlist/basic.lean =====
Phantom aligns: {'dlist.lazy_of_list'}

===== File mathlib/src/data/prod/pprod.lean =====
Missing aligns: {"pprod.exists'", 'pprod.mk.eta', 'pprod.forall', 'pprod.exists', "pprod.forall'", 'function.injective.pprod_map'}

===== File mathlib/src/data/prod/basic.lean =====
Missing aligns: {'prod.swap_surjective', 'prod.fst_surjective', 'prod.id_prod', 'prod.snd_eq_iff', 'prod.lex.refl_left', 'prod.lex_def', 'prod.snd_comp_mk', 'prod.exists', 'prod.swap_swap_eq', 'prod.map_map', 'prod.lex_iff', 'prod.swap_injective', 'prod.mk.inj_right', 'prod.swap_bijective', 'prod.ext_iff', 'prod.fst_comp_mk', 'prod.mk.inj_iff', 'prod.swap_prod_mk', 'prod.snd_injective', "prod.map_fst'", 'prod.map_fst', 'prod.mk_inj_right', 'prod.fst_injective', 'prod.lex.trans', "prod.forall'", 'prod.lex.refl_right', 'prod.swap_swap', 'prod.map_comp_map', 'prod.forall', 'prod.swap_inj', 'prod.swap', 'prod.map_id', 'prod.map_snd', 'prod.snd_surjective', 'prod.eq_iff_fst_eq_snd_eq', 'prod.mk_inj_left', "prod.exists'", "prod.map_snd'", 'prod.fst_swap', 'prod.fst_eq_iff', 'prod.map_mk', 'prod.mk.inj_left', 'prod.map_def', 'prod.snd_swap'}

===== File mathlib/src/data/pnat/basic.lean =====
Missing aligns: {'equiv.pnat_equiv_nat_symm_apply', 'equiv.pnat_equiv_nat_apply', 'order_iso.pnat_iso_nat_apply'}

===== File mathlib/src/data/W/basic.lean =====
Missing aligns: {'W_type.equiv_sigma_symm_apply', 'W_type.equiv_sigma_apply'}

===== File mathlib/src/data/countable/defs.lean =====
Missing aligns: {'equiv.countable_iff', 'countable.of_equiv', 'exists_surjective_nat', 'function.injective.countable', 'countable_iff_exists_surjective', 'function.surjective.countable'}

===== File mathlib/src/data/int/absolute_value.lean =====
Missing aligns: {'int.nat_abs_hom_apply'}

===== File mathlib/src/data/int/gcd.lean =====
Missing aligns: {'tactic.norm_num.nat_coprime_helper_zero_left', 'tactic.norm_num.nat_gcd_helper_dvd_right', 'tactic.norm_num.nat_not_coprime_helper', 'tactic.norm_num.int_gcd_helper', 'nat.gcd_a_zero_right', 'tactic.norm_num.nat_gcd_helper_dvd_left', 'tactic.norm_num.nat_gcd_helper_1', 'tactic.norm_num.int_lcm_helper', 'tactic.norm_num.nat_lcm_helper', 'tactic.norm_num.int_lcm_helper_neg_left', 'tactic.norm_num.nat_coprime_helper_1', 'tactic.norm_num.int_gcd_helper_neg_right', 'tactic.norm_num.nat_coprime_helper_2', "tactic.norm_num.int_gcd_helper'", 'tactic.norm_num.nat_gcd_helper_2', 'tactic.norm_num.nat_coprime_helper_zero_right', 'tactic.norm_num.int_gcd_helper_neg_left', 'tactic.norm_num.int_lcm_helper_neg_right'}

===== File mathlib/src/data/int/basic.lean =====
Missing aligns: {'int.mul_sign', 'int.default_eq_zero', 'int.succ', "int.to_nat'", 'int.sign_neg', 'int.succ_neg_succ', 'int.succ_neg_nat_succ', 'int.neg_succ', 'int.neg_pred', 'int.zero_div', 'int.add_def', 'int.nat_succ_eq_int_succ', 'int.pred_neg_pred', 'int.pred_succ', 'int.mod_add_div_aux', 'int.induction_on', 'int.sign_mul', 'int.neg_nat_succ', 'int.pred_nat_succ', 'int.pred', 'int.add_neg_one', 'int.mul_def', 'int.div_zero', 'int.add_one_le_iff', 'int.coe_pred_of_pos', 'int.succ_pred', 'int.coe_nat_nonneg'}

===== File mathlib/src/data/int/order/basic.lean =====
Missing aligns: {"int.induction_on'"}

===== File mathlib/src/data/int/order/units.lean =====
Missing aligns: {'int.units_pow_two'}

===== File mathlib/src/data/int/cast/defs.lean =====
Missing aligns: {'int.cast_of_nat'}
Phantom aligns: {'add_group_with_one.int_cast_of_nat', 'add_group_with_one.to_int_cast', 'add_group_with_one.int_cast_neg_succ_of_nat'}

===== File mathlib/src/data/nat/prime.lean =====
Missing aligns: {'nat.prime.even_sub_one', 'nat.dvd_of_forall_prime_mul_dvd', 'nat.prime.prime', 'prime.nat_prime'}

===== File mathlib/src/data/nat/sqrt.lean =====
Missing aligns: {'nat.sqrt'}

===== File mathlib/src/data/nat/pow.lean =====
Missing aligns: {'nat.pow_two_sub_pow_two'}

===== File mathlib/src/data/nat/basic.lean =====
Missing aligns: {'nat.succ_le_succ_iff', 'nat.div_add_mod', "nat.exists_eq_add_of_le'"}
Phantom aligns: {'nat.eq_of_mul_eq_mul_right'}

===== File mathlib/src/data/nat/pairing.lean =====
Missing aligns: {'nat.mkpair_equiv_symm_apply', 'nat.mkpair_equiv_apply'}

===== File mathlib/src/data/nat/factorial/basic.lean =====
Missing aligns: {'nat.add_desc_factorial_eq_asc_factorial', 'nat.desc_factorial_of_lt'}
Phantom aligns: {'nat.add_descFactorial_eq_asc_factorial'}

===== File mathlib/src/data/nat/gcd/basic.lean =====
Missing aligns: {'nat.coprime.coprime_dvd_right', 'nat.gcd_dvd_right', 'nat.gcd_gcd_self_right_right', 'nat.coprime.gcd_mul_left_cancel_right', 'nat.gcd_dvd_gcd_mul_right', 'nat.coprime.pow_left', 'nat.coprime_mul_iff_left', 'nat.gcd_eq_left', 'nat.coprime.coprime_div_left', 'nat.gcd_gcd_self_left_right', 'nat.lcm_ne_zero', 'nat.gcd_div', 'nat.gcd_mul_gcd_of_coprime_of_mul_eq_mul', 'nat.coprime_self', 'nat.gcd_dvd_gcd_of_dvd_left', 'nat.coprime_one_right', 'nat.gcd_mul_left_left', 'nat.coprime.mul_right', 'nat.coprime.symm', 'nat.coprime_div_gcd_div_gcd', 'nat.lcm_zero_left', 'nat.gcd_eq_left_iff_dvd', 'nat.lcm_zero_right', 'nat.gcd_eq_zero_iff', 'nat.coprime.coprime_dvd_left', 'nat.gcd_pos_of_pos_right', 'nat.dvd_lcm_right', 'nat.gcd_mul_right', 'nat.eq_zero_of_gcd_eq_zero_left', 'nat.coprime.gcd_mul_right_cancel_right', 'nat.coprime.coprime_mul_right_right', 'nat.coprime.mul_dvd_of_dvd_of_dvd', "nat.exists_coprime'", 'nat.gcd_dvd_gcd_of_dvd_right', 'nat.lcm_one_left', 'nat.gcd_le_right', 'nat.coprime.pow', 'nat.coprime.gcd_right', 'nat.coprime_zero_right', 'nat.gcd_gcd_self_left_left', 'nat.lcm_self', 'nat.lcm_one_right', 'nat.coprime.gcd_mul', 'nat.coprime.gcd_left', 'nat.gcd_mul_right_right', 'nat.eq_zero_of_gcd_eq_zero_right', 'nat.exists_coprime', 'nat.coprime.eq_one_of_dvd', 'nat.gcd_dvd', 'nat.dvd_lcm_left', 'nat.coprime.mul', 'nat.coprime.gcd_both', 'nat.gcd_assoc', 'nat.gcd_dvd_gcd_mul_left_right', 'nat.gcd_dvd_gcd_mul_left', 'nat.lcm_dvd', 'nat.coprime.gcd_mul_right_cancel', 'nat.coprime.pow_right', 'nat.gcd_pos_of_pos_left', 'nat.lcm_assoc', 'nat.coprime.coprime_mul_right', 'nat.gcd_comm', 'nat.dvd_gcd', 'nat.gcd_dvd_gcd_mul_right_right', 'nat.gcd_mul_dvd_mul_gcd', 'nat.coprime.dvd_of_dvd_mul_left', 'nat.coprime.coprime_mul_left_right', 'nat.coprime_zero_left', 'nat.gcd_mul_right_left', 'nat.coprime_one_left', 'nat.coprime.gcd_eq_one', 'nat.coprime.coprime_div_right', 'nat.gcd_mul_left_right', 'nat.gcd_dvd_left', 'nat.gcd_gcd_self_right_left', 'nat.gcd_le_left', 'nat.lcm_comm', 'nat.coprime.dvd_of_dvd_mul_right', 'nat.gcd_mul_left', 'nat.coprime.gcd_mul_left_cancel', 'nat.gcd_mul_lcm', 'nat.gcd_eq_right_iff_dvd', 'nat.coprime_iff_gcd_eq_one', 'nat.gcd_eq_right', 'nat.coprime_comm', 'nat.gcd_one_right', 'nat.coprime_mul_iff_right', 'nat.coprime.coprime_mul_left', 'nat.not_coprime_of_dvd_of_dvd', 'nat.dvd_gcd_iff'}

===== File mathlib/src/data/nat/cast/basic.lean =====
Missing aligns: {"ext_nat'", 'nat.cast_ring_hom_nat', 'nat.cast_add_monoid_hom', 'mul_opposite.unop_nat_cast', 'has_dvd.dvd.nat_cast', 'nat.cast_min', "map_nat_cast'", 'pi.nat_apply', 'nat.one_lt_cast', 'nat.one_le_cast', 'ne_zero.nat_of_ne_zero', 'nat.cast_add_one_pos', 'ne_zero.nat_of_injective', 'add_monoid_hom.ext_nat', 'nat.cast_nonneg', 'nat.abs_cast', 'monoid_with_zero_hom.ext_nat', 'nat.cast_le', 'mul_opposite.op_nat_cast', 'nat.cast_le_one', 'pi.coe_nat', 'nat.cast_max', 'nat.cast_comm', 'nat.cast_mul', 'nat.mono_cast', "eq_nat_cast'", 'nat.cast_lt', 'nat.commute_cast', 'nat.cast_pos', 'nat.cast_order_embedding_apply', 'nat.cast_tsub', 'map_nat_cast', 'sum.elim_nat_cast_nat_cast', 'nat.cast_order_embedding', 'nat.cast_id', 'nat.cast_ring_hom', 'nat.cast_lt_one', 'nat.coe_nat_dvd', 'nat.cast_commute', "ext_nat''", 'eq_nat_cast', 'ext_nat'}

===== File mathlib/src/data/nat/cast/defs.lean =====
Phantom aligns: {'add_monoid_with_one.nat_cast_succ', 'has_nat_cast.nat_cast', 'add_monoid_with_one.nat_cast_zero'}

===== File mathlib/src/data/fintype/card.lean =====
Missing aligns: {'equiv.of_right_inverse_of_card_le_apply', 'equiv.of_right_inverse_of_card_le_symm_apply', 'equiv.of_left_inverse_of_card_le_symm_apply', 'equiv.of_left_inverse_of_card_le_apply'}

===== File mathlib/src/data/fintype/basic.lean =====
Missing aligns: {'units_equiv_ne_zero_symm_apply', 'coe_units_equiv_prod_subtype_symm_apply', 'units_equiv_ne_zero_apply_coe', 'units_equiv_prod_subtype_apply_coe', 'coe_inv_units_equiv_prod_subtype_symm_apply'}

===== File mathlib/src/data/sigma/basic.lean =====
Missing aligns: {'psigma.forall', 'psigma.mk.inj_iff', 'function.injective.sigma_map_iff', 'function.injective.of_sigma_map', 'sigma.forall', 'function.surjective.sigma_map', 'sigma.eta', 'sigma.ext', 'prod.to_sigma', 'psigma.ext', 'sigma.uncurry', 'sigma.curry', 'function.injective.sigma_map', 'sigma.map', 'sigma.mk.inj_iff', 'psigma.subtype_ext', 'sigma.exists', 'psigma.subtype_ext_iff', 'psigma.elim', 'psigma.elim_val', 'psigma.exists', 'sigma.subtype_ext_iff', 'sigma_mk_injective', 'psigma.map', 'sigma.curry_uncurry', 'sigma.subtype_ext', 'sigma.uncurry_curry', 'sigma.ext_iff', 'psigma.ext_iff'}

===== File mathlib/src/data/pi/algebra.lean =====
Missing aligns: {'function.surjective_pi_map', 'pi.neg_def', 'sum.elim_zero_zero', 'sum.elim_sub_sub', 'function.extend_div', 'pi.inv_def', 'pi.const_div', 'function.injective_pi_map', 'pi.zero_apply', 'pi.one_comp', 'pi.neg_comp', 'pi.sub_def', 'pi.prod_fst_snd', 'function.extend_zero', 'pi.const_neg', 'pi.inv_apply', 'pi.bit0_apply', 'pi.const_mul', 'unique_of_surjective_one', 'pi.one_def', 'pi.pow_comp', 'pi.prod', 'pi.const_inv', 'pi.vadd_comp', 'sum.elim_add_add', 'sum.elim_neg_neg', 'pi.vadd_def', 'sum.elim_mul_mul', 'pi.bit1_apply', 'sum.elim_div_div', 'pi.smul_const', 'pi.zero_comp', 'pi.add_apply', 'pi.const_one', 'pi.vadd_const', 'pi.mul_def', 'function.extend_inv', 'pi.pow_apply', 'function.extend_neg', 'function.extend_add', 'function.extend_one', 'pi.mul_comp', 'pi.const_zero', 'pi.sub_comp', 'pi.const_pow', 'pi.inv_comp', 'pi.smul_def', 'pi.smul_apply', 'pi.prod_snd_fst', 'pi.add_comp', 'pi.add_def', 'pi.const_add', 'function.extend_sub', 'pi.const_sub', 'pi.neg_apply', 'sum.elim_one_one', 'pi.vadd_apply', 'pi.smul_comp', 'pi.comp_one', 'pi.comp_zero', 'pi.div_def', 'pi.sub_apply', 'pi.zero_def', 'pi.mul_apply', 'unique_of_surjective_zero', 'function.extend_mul', 'pi.one_apply', 'function.bijective_pi_map', 'sum.elim_inv_inv', 'pi.pow_def', 'pi.div_apply', 'pi.div_comp'}

===== File mathlib/src/data/finset/nat_antidiagonal.lean =====
Missing aligns: {'finset.nat.sigma_antidiagonal_equiv_prod_apply', 'finset.nat.sigma_antidiagonal_equiv_prod_symm_apply_snd_coe', 'finset.nat.sigma_antidiagonal_equiv_prod_symm_apply_fst'}

===== File mathlib/src/data/finset/basic.lean =====
Missing aligns: {'finset.to_list_singleton', 'finset.erase_cons_of_ne', 'finset.sep_def', 'finset.val_eq_singleton_iff', 'finset.to_list_eq_singleton_iff'}

===== File mathlib/src/data/finset/n_ary.lean =====
Missing aligns: {'finset.image₂_left_identity', 'finset.image₂_right_identity'}

===== File mathlib/src/data/finite/defs.lean =====
Missing aligns: {'finite.not_infinite', 'finite.of_not_infinite'}

===== File mathlib/src/data/fin/fin2.lean =====
Missing aligns: {'fin2.elim0', 'fin2.left', 'fin2.insert_perm', 'fin2', 'fin2.to_nat', 'fin2.add', 'fin2.remap_left', 'fin2.opt_of_nat', "fin2.cases'", 'fin2.is_lt', "fin2.of_nat'"}

===== File mathlib/src/data/fin/basic.lean =====
Missing aligns: {"fin.of_nat'_eq_coe", 'fin.rev_order_iso_to_equiv', 'fin.rev_order_iso_apply', 'fin.coe_embedding_apply', 'fin.equiv_subtype_apply', 'fin.coe_order_embedding_apply', 'fin.equiv_subtype_symm_apply', 'fin.order_iso_subtype_symm_apply', 'fin.order_iso_subtype_apply'}
Phantom aligns: {'fin.pred'}

===== File mathlib/src/data/sum/order.lean =====
Missing aligns: {'order_iso.sum_comm_apply'}

===== File mathlib/src/data/sum/basic.lean =====
Missing aligns: {'sum.inr_ne_inl', 'sum.lift_rel.mono_right', 'sum.update_inl_apply_inl', 'function.injective.sum_map', 'sum.swap_left_inverse', 'sum.elim', 'sum.update_inr_comp_inr', 'sum.update_inr_comp_inl', 'sum.elim_inr', 'sum.lift_rel.mono', 'sum.lift_rel.swap', 'sum.update_inl_comp_inr', 'sum.swap_swap', 'sum.map_map', 'sum.forall', 'sum.map', 'sum.get_left_eq_some_iff', 'sum.elim_map', 'sum.lex.mono_left', 'sum.get_left', 'sum.swap_inr', 'sum.elim_inl_inr', 'sum.elim_inl', 'sum.update_elim_inr', 'sum.update_elim_inl', 'sum.is_right', 'sum.lex.mono_right', 'sum.swap_swap_eq', 'sum.elim_comp_inr', 'sum.inl_injective', 'sum.inr_injective', 'sum3.in₀', 'sum.lex_inr_inl', 'sum.comp_elim', 'sum.lex_inr_inr', 'sum.lift_rel.mono_left', 'sum.map_id_id', 'sum.elim_comp_inl_inr', 'sum.elim_update_left', 'sum.lex_inl_inl', 'sum.lift_rel.lex', 'sum.get_right_eq_some_iff', 'sum.lex_wf', 'sum.elim_lam_const_lam_const', 'sum.lex_acc_inr', 'sum.update_inr_apply_inl', 'sum.lex', 'sum.swap_right_inverse', 'sum.elim_const_const', 'sum3.in₁', 'sum.exists', 'sum.map_comp_map', 'sum.elim_update_right', 'sum.elim_comp_inl', 'sum.update_inl_apply_inr', 'sum.update_inr_apply_inr', 'sum.lex_acc_inl', 'sum.is_left', 'sum.get_right', 'sum.swap', 'sum.update_inl_comp_inl', 'sum.lift_rel', 'sum.swap_inl', 'sum.lex.mono', 'function.surjective.sum_map', 'sum3.in₂', 'sum.map_inr', 'sum.inl_ne_inr', 'function.injective.sum_elim', 'sum.map_inl', 'sum.elim_comp_map'}
Phantom aligns: {'sum.lex.inr', 'sum.lex.sep', 'sum.lex.inl'}

===== File mathlib/src/data/list/chain.lean =====
Missing aligns: {'list.chain_iff'}
Phantom aligns: {'list.chain.cons', 'list.chain.nil'}

===== File mathlib/src/data/list/forall2.lean =====
Missing aligns: {'list.forall₂_iff', 'list.rel_sum'}
Phantom aligns: {'list.sublist_forall₂.nil', 'list.sublist_forall₂.cons', 'list.forall₂.nil', 'list.sublist_forall₂.cons_right', 'list.forall₂.cons'}

===== File mathlib/src/data/list/zip.lean =====
Missing aligns: {'list.sum_add_sum_eq_sum_zip_with_add_sum_drop', 'list.nth_le_zip_with', 'list.sum_add_sum_eq_sum_zip_with_of_length_eq', 'list.length_zip_with'}

===== File mathlib/src/data/list/infix.lean =====
Missing aligns: {'list.slice_sublist', 'list.eq_nil_of_suffix_nil', 'list.is_infix.reverse', 'list.slice_subset', 'list.eq_nil_of_prefix_nil', 'list.is_suffix.reverse', 'list.mem_of_mem_slice', 'list.is_prefix.reverse'}

===== File mathlib/src/data/list/of_fn.lean =====
Missing aligns: {'list.equiv_sigma_tuple_apply_snd', 'list.equiv_sigma_tuple_symm_apply', 'list.array_eq_of_fn', 'list.equiv_sigma_tuple_apply_fst', 'list.of_fn_fin_append', 'list.of_fn_fin_repeat'}

===== File mathlib/src/data/list/perm.lean =====
Missing aligns: {'list.subperm.cons', "list.perm.sum_eq'", 'list.perm.subset_congr_right', 'list.perm_replicate_append_replicate', 'list.perm.subset_congr_left', 'list.perm.sum_eq', 'list.subperm.of_cons', 'list.sum_reverse'}

===== File mathlib/src/data/list/nodup_equiv_fin.lean =====
Missing aligns: {'list.nodup.nth_le_equiv_of_forall_mem_list_symm_apply_val', 'list.nodup.nth_le_equiv_of_forall_mem_list_apply', 'list.nodup.nth_le_bijection_of_forall_mem_list_coe', 'list.nodup.nth_le_equiv_apply_coe', 'list.nodup.nth_le_equiv_symm_apply_val'}

===== File mathlib/src/data/list/sigma.lean =====
Missing aligns: {'list.nodupkeys_of_nodupkeys_cons', 'list.not_mem_keys_of_nodupkeys_cons'}

===== File mathlib/src/data/list/fin_range.lean =====
Missing aligns: {'list.map_nth_le'}

===== File mathlib/src/data/list/count.lean =====
Missing aligns: {'list.sum_eq_nsmul_single', 'list.sum_map_eq_nsmul_single'}

===== File mathlib/src/data/list/alist.lean =====
Missing aligns: {'alist.insert_rec_insert', 'alist.mk_cons_eq_insert', 'alist.insert_of_neg', 'alist.insert_rec_empty', 'alist.recursion_insert_mk', 'alist.insert_rec'}

===== File mathlib/src/data/list/range.lean =====
Missing aligns: {"list.sum_range_succ'", 'list.sum_range_succ'}
Phantom aligns: {'list.range_core', 'list.map_nth_le'}

===== File mathlib/src/data/list/basic.lean =====
Missing aligns: {'list.eq_of_mem_replicate', 'list.length_replicate', 'list.mem_replicate'}
Phantom aligns: {'list.sublist.cons2', 'list.filter_cons_of_pos', 'list.empty', 'list.eq_or_mem_of_mem_cons', 'list.filter_nil', 'list.filter_sublist', 'list.filter_append', 'list.filter_cons_of_neg', 'list.has_singleton', 'list.length_le_of_sublist', 'list.reverse_core', 'list.mem_cons_iff'}

===== File mathlib/src/data/list/nodup.lean =====
Missing aligns: {'list.nodup.of_attach', 'list.nodup.attach'}

===== File mathlib/src/data/list/lex.lean =====
Phantom aligns: {'list.lex.nil', 'list.lex.cons', 'list.lex.rel'}

===== File mathlib/src/data/list/rotate.lean =====
Missing aligns: {"list.head'_rotate", 'list.rotate_replicate', 'list.rotate_eq_self_iff_eq_replicate', 'list.nth_rotate', 'list.rotate_one_eq_self_iff_eq_replicate'}

===== File mathlib/src/data/list/defs.lean =====
Missing aligns: {'list.transpose_aux', 'list.mmap_with_index_aux', 'list.split_on_p_aux', 'list.sublists_aux', 'list.foldr_with_index_aux', 'list.of_fn_aux', 'list.sublists_aux₁', 'list.foldl_with_index_aux', "list.sublists'_aux", 'list.scanr_aux', 'list.replicate'}

===== File mathlib/src/data/list/pairwise.lean =====
Missing aligns: {'list.pairwise_iff', 'list.pairwise.pw_filter'}
Phantom aligns: {'list.pairwise.nil', 'list.pairwise.cons'}

===== File mathlib/src/data/list/big_operators/lemmas.lean =====
Missing aligns: {'list.alternating_sum_reverse', 'list.card_nsmul_le_sum', 'list.alternating_sum_append', 'list.sum_eq_zero_iff'}

===== File mathlib/src/data/list/big_operators/basic.lean =====
Missing aligns: {'list.sum_concat', 'list.alternating_sum_nil', "list.sum_update_nth'", 'list.sum_singleton', 'list.sum_append', 'list.sum_hom_rel', 'list.sublist.sum_le_sum', 'list.sum_take_succ', 'list.sum_is_add_unit_iff', 'list.sum_map_hom', "list.alternating_sum_cons_cons'", 'list.exists_le_of_sum_le', 'add_commute.list_sum_left', 'map_list_sum', 'list.sum_hom₂', 'list.sum_lt_sum', 'list.sum_eq_card_nsmul', "list.alternating_sum_cons'", 'list.sum_take_add_sum_drop', 'list.sum_hom', 'list.sum_update_nth', 'list.all_zero_of_le_zero_le_of_sum_eq_zero', 'list.sum_eq_zero', 'list.sum_is_add_unit', 'list.single_le_sum', 'list.exists_mem_ne_zero_of_sum_ne_zero', 'list.head_add_tail_sum_of_ne_nil', 'list.nth_zero_add_tail_sum', 'list.alternating_sum_cons', 'list.sum_lt_sum_of_ne_nil', 'list.sum_erase', 'list.sum_nil', 'list.sum_join', 'list.length_pos_of_sum_neg', 'list.sum_le_card_nsmul', 'list.monotone_sum_take', 'list.sum_eq_foldr', 'list.sum_map_erase', 'add_commute.list_sum_right', 'list.sum_neg', 'list.sum_replicate', 'list.forall₂.sum_le_sum', 'list.eq_of_sum_take_eq', 'list.sum_nonneg', 'list.length_pos_of_sum_ne_zero', 'list.sum_reverse_noncomm', 'list.alternating_sum_singleton', 'list.alternating_sum_cons_cons', 'list.length_pos_of_sum_pos', 'list.sum_drop_succ', 'list.exists_lt_of_sum_lt', 'list.sum_pos', 'list.sum_map_add', 'list.sublist_forall₂.sum_le_sum', 'list.sum_cons', 'list.sum_neg_reverse', 'list.sum_le_sum', 'add_monoid_hom.map_list_sum'}

===== File mathlib/src/data/stream/defs.lean =====
Phantom aligns: {'state'}

===== File mathlib/src/data/bool/basic.lean =====
Missing aligns: {'bool.coe_sort_ff', 'bool.coe_bool_iff', 'bool.injective_iff', 'bool.dichotomy', 'bool.cond_ff', 'bool.of_nat_le_of_nat', 'bool.default_bool', 'bool.of_nat_to_nat', 'bool.forall_bool', 'bool.lt_iff', 'bool.cond_tt', 'bool.to_nat_le_to_nat', 'bool.cond_eq_ite', 'bool.apply_apply_apply', 'bool.exists_bool', 'bool.le_iff_imp', 'bool.coe_sort_tt'}

===== File mathlib/src/data/sym/basic.lean =====
Missing aligns: {'sym_option_succ_equiv_apply', 'sym.mk_coe', 'sym_option_succ_equiv_symm_apply', 'sym.equiv_congr_apply', 'sym.equiv_congr_symm_apply'}

===== File mathlib/src/data/option/basic.lean =====
Missing aligns: {'option.bind_eq_none', 'option.pmap_map', 'option.orelse_eq_none', "option.cases_on'_some", 'option.iget_mem', 'option.some_get', "option.orelse_eq_some'", 'option.forall_mem_map', 'option.not_mem_none', 'option.bind_pmap', "option.map_bind'", "option.ne_none_iff_exists'", 'option.pbind_eq_bind', "option.cases_on'_none", 'option.orelse_eq_some', 'option.get_some', 'option.eq_of_mem_of_mem', 'option.some_bind', 'option.map_eq_some', 'option.join_eq_some', 'option.bind_id_eq_join', "option.map_some'", "option.map_eq_some'", 'option.join_eq_none', 'option.pbind_map', 'option.iget_of_mem', 'option.guard_eq_some', 'option.map_eq_none', 'option.comp_map', 'option.exists', 'option.ne_none_iff_exists', "option.bind_eq_none'", "option.guard_eq_some'", 'option.bind_map_comm', 'option.join_pmap_eq_pmap_join', 'option.eq_none_iff_forall_not_mem', 'option.get_or_else_some', 'option.map_injective', 'option.map_some', 'option.bind_some', 'option.ext', 'option.coe_get', 'option.pmap_some', 'option.seq_some', 'option.exists_mem_map', 'option.to_list_some', "option.map_injective'", 'option.get_mem', 'option.to_list_none', 'option.elim_none_some', 'option.some_injective', 'option.bind_comm', 'option.some_eq_coe', 'option.map_none', 'option.pmap_eq_none_iff', 'option.map_inj', 'option.eq_some_iff_get_eq', 'option.some_ne_none', 'option.join_ne_none', 'option.map_comp_map', 'option.map_comp_some', 'option.map_comm', 'option.mem_unique', 'option.bind_assoc', 'option.map_eq_map', 'option.bind_eq_some', 'option.mem_of_mem_join', 'option.map_pmap', 'option.map_pbind', 'option.choice', 'option.get_or_else_map', 'option.join_map_eq_map_join', 'option.get_of_mem', 'option.join_join', 'option.choice_eq', 'option.mem_pmem', 'option.pbind_eq_none', "option.bind_eq_some'", 'option.coe_def', 'option.map_bind', "option.map_none'", 'option.pmap_bind', "option.join_ne_none'", 'option.map_congr', "option.bind_some'", 'option.ball_ne_none', 'option.get_or_else_of_ne_none', 'option.coe_ne_none', 'option.mem_map', 'option.get_or_else_none', 'option.bex_ne_none', 'option.mem_map_of_mem', 'option.map_coe', "option.cases_on'_coe", "option.map_eq_none'", "option.none_bind'", "option.cases_on'", 'option.pmap_eq_some_iff', 'option.bind_eq_bind', "option.cases_on'_none_coe", 'option.map_eq_id', "option.some_bind'", 'option.pmap_none', "option.map_coe'", 'option.pbind_eq_some', 'option.map_map', 'option.pmap_eq_map', "option.orelse_eq_none'", 'option.forall', 'option.choice_eq_none', 'option.none_bind'}
Phantom aligns: {'option.get_or_else'}

===== File mathlib/src/data/option/defs.lean =====
Missing aligns: {'option.join', 'option.iget_some', 'option.maybe', 'option.iget', 'option.pmap', 'option.rel', 'option.some_inj', 'option.mem_iff', 'option.guard', 'option.mem_def', 'option.is_none_iff_eq_none', 'option.pbind', 'option.decidable_eq_none', 'option.to_list', 'option.filter', 'option.traverse', 'option.mem_some_iff'}

===== File mathlib/src/data/option/n_ary.lean =====
Missing aligns: {'option.map₂_right_identity', 'option.map₂_left_identity'}

===== File mathlib/src/data/fun_like/equiv.lean =====
Missing aligns: {'equiv_like.apply_inv_apply', 'equiv_like.comp_bijective', 'equiv_like.apply_eq_iff_eq', 'equiv_like.inv_injective', 'equiv_like.comp_surjective', 'equiv_like.subsingleton_dom', 'equiv_like.injective_comp', 'equiv_like.surjective_comp', 'equiv_like', 'equiv_like.inv_apply_apply', 'equiv_like.bijective', 'equiv_like.comp_injective', 'equiv_like.bijective_comp', 'equiv_like.surjective', 'equiv_like.injective'}

===== File mathlib/src/data/fun_like/basic.lean =====
Missing aligns: {'fun_like.congr_arg', 'fun_like.coe_fn_eq', 'fun_like.ne_iff', 'fun_like.ext', 'fun_like.coe_injective', 'fun_like.subsingleton_cod', 'fun_like', "fun_like.ext'_iff", 'fun_like.congr', 'fun_like.ext_iff', 'fun_like.congr_fun', "fun_like.ext'", 'fun_like.coe_eq_coe_fn', 'fun_like.exists_ne'}

===== File mathlib/src/data/fun_like/embedding.lean =====
Missing aligns: {'embedding_like.comp_injective', 'embedding_like.injective', 'embedding_like', 'embedding_like.apply_eq_iff_eq'}

===== File mathlib/src/data/multiset/basic.lean =====
Missing aligns: {'multiset.to_list_eq_singleton_iff', 'multiset.map_embedding_apply', 'multiset.coe_eq_singleton', 'multiset.rel_iff', 'multiset.to_list_singleton', 'multiset.replicate_add_monoid_hom_apply', 'multiset.replicate'}

===== File mathlib/src/data/multiset/bind.lean =====
Missing aligns: {'multiset.sum_bind'}