Unable to use and_symm theorem in World 7, Level 3

ImperialCollegeLondon / natural_number_game

Building the natural numbers in Lean 3. The original natural number game, now frozen. See README for Lean 4 information.

Apache License 2.0

288 stars 72 forks source link

Unable to use and_symm theorem in World 7, Level 3 #105

Open Gunjeet-Singh opened 3 years ago

Gunjeet-Singh commented 3 years ago

I am trying to apply theorem and_symm in World 7, level 3 to convert a hypothesis h from P -> Q to Q -> P (by doing have h1 := and_symm _ _ h) but am getting the error "unknown identifier and_symm". Rather, and.symm seems to work which is strange (I just got to know that and.symm is the counterpart of and_symm in actual Lean in VSCode).