construction of some basic things (beginner question)

Stream: maths

[Kind Bubble]

Hi, folk.

I'm Dean.

I just went through the Lean 4 tutorial, which is currently incomplete. I was hoping I could come here with a list of things I want to patch up. It's a long one, but definitely I want to patch as much of these things as possible so passing comments are appreciated.

• a : A gives id_a : a =_A a
• p : a = b, q : b = c gives p : a = c
• p : a = b gives p : b = a by switch_A
• p : X -> Prop, t: ev_x (p), s : x =_X y gives t : ev_y(p) [replacement - the most important to me on this list]

• the theorems involved in the equality type

• A unit type with a constituent const : unit

• A theorem: \forall x : unit, x = const

The tutorial for Lean 4 describes the use of simp, but I don't want this for now (I'm just a beginner).

[Andrew Yang]

I think the chapter in #tpil4 on equality should be useful to you.