[
    {
        "content": "<p>This works:</p>\n<div class=\"codehilite\"><pre><span></span><span class=\"kn\">theorem</span> <span class=\"n\">one_plus_one_alt</span> <span class=\"o\">:</span> <span class=\"mi\">1</span> <span class=\"bp\">+</span> <span class=\"mi\">1</span> <span class=\"bp\">=</span> <span class=\"mi\">2</span> <span class=\"o\">:=</span> <span class=\"n\">rfl</span>\n\n<span class=\"kn\">example</span> <span class=\"o\">:</span> <span class=\"mi\">1</span> <span class=\"bp\">+</span> <span class=\"mi\">1</span> <span class=\"bp\">≤</span> <span class=\"mi\">2</span> <span class=\"o\">:=</span> <span class=\"n\">dec_trivial</span>\n</pre></div>\n\n\n<p>This doesn't work:</p>\n<div class=\"codehilite\"><pre><span></span><span class=\"kn\">example</span> <span class=\"o\">:</span> <span class=\"mi\">1</span> <span class=\"bp\">+</span> <span class=\"mi\">1</span> <span class=\"bp\">≤</span> <span class=\"mi\">2</span> <span class=\"o\">:=</span> <span class=\"n\">rfl</span>\n</pre></div>\n\n\n<p><span aria-label=\"confused\" class=\"emoji emoji-1f615\" role=\"img\" title=\"confused\">:confused:</span></p>",
        "id": 156766507,
        "sender_full_name": "<NAME>",
        "timestamp": 1548330555
    },
    {
        "content": "<p>Look at the type of <code>rfl</code>? It proves equality, not inequality.</p>",
        "id": 156767066,
        "sender_full_name": "<NAME>",
        "timestamp": 1548331312
    },
    {
        "content": "<p>You might be looking for <code>le_refl</code>.</p>",
        "id": 156767129,
        "sender_full_name": "<NAME>",
        "timestamp": 1548331349
    }
]