How do I prove "not (false = true)" in Lean?

Question

As is perhaps obvious from the question, I am just starting with Lean and am missing some very basic knowledge about what features are available. Anyways, I'm trying to prove not (false = true) and I have this:

example : not (false = true) := not.intro (
    assume H: false = true,
    show false, from begin
        rw H,
        -- now I need to prove "true"
    end
)

The thing that's really confusing is me is that the program is telling me I have an unsolved goal, which is to prove the vacuous statement "true". I figure there's some boilerplate "cmon it's already true" statement like "qed" or "vacuous" or something but I have no idea what it is and I wasn't able to find it by skimming the documentation.

Also I'm sure this can be more succinct. But first I need it to work at all before I worry about succinct!

Answer 1

The exact axiom that accepts true is called true.intro:

example : not (false = true) := not.intro (
    assume H: false = true,
    show false, from begin
        rw H,
        exact true.intro
    end
)

From https://leanprover.github.io/theorem_proving_in_lean/propositions_and_proofs.html :

Incidentally, just as false has only an elimination rule, true has only an introduction rule, true.intro : true, sometimes abbreviated trivial : true. In other words, true is simply true, and has a canonical proof, trivial.

Other more general tactics that would have worked are trivial and simp.

From the documentation:

Trivial

Tries to solve the current goal using a canonical proof of true, or the reflexivity tactic, or the contradiction tactic.