# Tag Info

### ∀ a b. a + b = b + a

Lean, 451 449 445 439 414 407 bytes ...

### ∀ a b. a + b = b + a

Lean, 268 bytes ...
• 38.9k

### Lean golf: Pascal vs. Fibonacci

Lean, 299 bytes ...
• 38.9k

### Lean golf: List Game Lv1 (rev_rev)

Lean, 101 bytes def r:∀s,rev(@rev A s)=s|[]:=rfl|(x::t):=by conv{to_rhs,rw<-r t};simp;induction rev t;simp;simp[ih] Try it online! I'm pretty happy with this. ...
• 94.5k

### Lean golf: List Game Lv2 (is_in_append, is_in_rev)

Lean, 188 bytes ...
• 38.9k

### Lean golf: List Game Lv1 (rev_rev)

Lean, 102 93 bytes def R:∀s,rev(@rev A s)=s:=by let:(∀s(h:A),rev(s++h::[])=h::rev s);intro;induction s;simp* Try it on Lean Web Editor The 102 byte solution I ...
• 38.9k

### Every Pong is Abelian

Lean, 115 103 100 bytes def P:=@add_assoc def V(A)[pong A](a b:A):a+b=_:=by rw[<-right_id\$a+b,<-P,P a,<-P b,left_id,left_id] Try it on Lean Web Editor! -...
• 70.2k

### Lean golf: Pascal vs. Fibonacci

Lean, 247 243 bytes ...
• 511

### Tips for golfing in Lean

Introductions If you've just finished the natural number game you may be familiar with the intro tactic, this can be used to create implications / functions. ...
• 94.5k

### Every Pong is Abelian

Lean, 141 140 121 bytes Saved one byte thanks to Wheat Witch/Wheat Wizard Saved 19 bytes thanks to Kyle Miller! ...
• 398

### Tips for golfing in Lean

Use by instead of begin ... end by can be shorter than ...