<commit_before>import data.nat
open nat
constant f : nat → nat

example (x y : nat) (H1 : (λ z, z + 0) x = y) : f x = f y :=
by rewrite [▸* at H1, ^[add, nat.rec_on, of_num] at H1, H1]

example (x y : nat) (H1 : (λ z, z + 0) x = y) : f x = f y :=
by rewrite [▸* at H1, ↑[add, nat.rec_on, of_num] at H1, H1]<commit_msg>fix(tests/lean/run/rewriter12): broken test, now `^[` is a token<commit_after>import data.nat
open nat
constant f : nat → nat

example (x y : nat) (H1 : (λ z, z + 0) x = y) : f x = f y :=
by rewrite [▸* at H1, ^ [add, nat.rec_on, of_num] at H1, H1]

example (x y : nat) (H1 : (λ z, z + 0) x = y) : f x = f y :=
by rewrite [▸* at H1, ↑[add, nat.rec_on, of_num] at H1, H1]
{'fraction_non_alphanumeric': 0.19040697674418605, 'fraction_numerical': 0.03197674418604651, 'mean_word_length': 3.005813953488372, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '753513', 'n_tokens_mistral': 329, 'n_tokens_neox': 321, 'n_words': 127}