[Question]
  [
*This question is a part of the [lean](/questions/tagged/lean "show questions tagged 'lean'") [LotM](https://codegolf.meta.stackexchange.com/questions/23916/).*
A ring is a type of structure that takes the rules of addition and multiplication we are familiar with and abstracts them, so we can reason about them. To do this we state a number of expected properties as axioms and see what we can say about systems that follow these axioms. For example \$a + (b + c) = (a + b) + c\$, is one of the axioms commonly given.
But exactly what the ring axioms are depends on whom you ask. Because, rings can be defined in a number of equivalent ways. Often one of the given axioms is that for any \$a\$ and \$b\$ then \$a + b = b + a\$. We call this *additive commutativity*. However this axiom is not needed! Usually we can prove it from more basic axioms.
In this challenge I will give a minimal axiom set for rings in the Lean programming language and your task is to prove commutativity.
The `ring` class is defined as follows:
```
universe u
class ring (α : Type u) extends has_add α, has_mul α, has_one α, has_zero α, has_neg α :=
  ( add_assoc : ∀ a b c : α, a + (b + c) = (a + b) + c )
  ( mul_assoc : ∀ a b c : α, a * (b * c) = (a * b) * c )
  ( add_left_id : ∀ a : α, 0 + a = a )
  ( mul_left_id : ∀ a : α, 1 * a = a )
  ( mul_right_id : ∀ a : α, a * 1 = a )
  ( add_left_inv : ∀ a : α, (-a) + a = 0 )
  ( left_distribute : ∀ a b c : α, a * (b + c) = a * b + a * c )
  ( right_distribute : ∀ a b c : α, (a + b) * c = a * c + b * c)
open ring
```
Your goal is to create an object with the same type as:
```
axiom add_comm {α : Type*} [ring α] : ∀ a b : α, a + b = b + a 
```
This is the same as proving the claim.
You may rename things here however you want as long as the underlying type is correct. So the following is a smaller but perfectly valid header for your proof:
```
def k{A:Type*}[ring A]:∀a b:A,a+b=b+a
```
You can't use different but similar looking types. So for example redefining the notation of `=` to make the proof trivial:
```
local notation a `=` b := true
def k{A:Type*}[ring A]:∀a b:A,a+b=b+a := λ x y, trivial
```
is not a valid answer, even though the type *looks* identical. (Thanks to [Eric](https://codegolf.stackexchange.com/users/4341/eric) for pointing this possible exploit out.)
You must actually prove the claim, so you may not use `sorry` or `axiom` in your proof.
This is [code-golf](/questions/tagged/code-golf "show questions tagged 'code-golf'") so answers will be scored in bytes with fewer bytes being the goal.
*If you want to do this challenge but don't know where to get started just use the links in [the LotM post](https://codegolf.meta.stackexchange.com/questions/23916/). I'll be happy to help anyway I can in chat.*
  
[Answer]
## Lean, ~~451~~ ~~449~~ ~~445~~ ~~439~~ ~~414~~ 407 bytes
```
def k{A}[ring A](a b:A):a+b=b+a:=let
L:=@add_left_inv A,I:=@add_left_id A,K:=@congr_arg,c:=λx y,K(+y)$L x in
by{let C:=add_assoc,simp[I]at*,let
e:=λb,(λ(a:A)h:a+a=a,(eq.trans(by
rw[<-I a,<-L,<-C,h])$L _:a=0))(b+-b)$by simp[<-C]at*;rw c,let
d:=K(λx,-b+x+-a)(left_distribute(1+1)b
a),simp[c,C,right_distribute,mul_left_id,mul_right_id,λa b,(by
rw[<-C,e,λa:A,(by rw[<-L,C,e,I]:a+0=a)]:b+a+-a=b)]at*,rw
d}
```
Unpacked:
```
def add_comm {A} [ring A] (a b : A) : a + b = b + a :=
let
  L := @add_left_inv A,
  I := @add_left_id A,
  K := @congr_arg,
  c := λ x y, K (+ y) (L x)
in begin
  have C := add_assoc,
  simp [I] at c,
  -- c: ∀ (x y : A), -x + x + y = y
  have e : ∀ (b : A), b + -b = 0 := λ b, 
    have ∀ (a : A), a + a = a → a = 0 :=
      λ (a : A) (h : a + a = a), show a = 0, from
        eq.trans (by rw [← I a, ← L, ← C, h]) (L _),
    this (b + -b) (by simp [← C] at c ⊢; rw c),
  have d : -b + ((1 + 1) * (b + a)) + -a = -b + ((1 + 1) * b + (1 + 1) * a) + -a :=
    K (λ x, -b + x + -a) (left_distribute (1+1) b a),
  simp [c, C, right_distribute, mul_left_id, mul_right_id,
    have ∀ (a b : A), b + a + -a = b :=
      λ a b : A, show b + a + -a = b, by
        rw [← C, e,
          have ∀ (a : A), a + 0 = a, from
            λ a : A, show a + 0 = a, by rw [← L, C, e, I],
          this],
    this] at d,
  -- d : a + b = b + a
  rw d
end
```
[Answer]
# Lean, 268 bytes
```
import tactic.cache
def k{A}[r:ring A](a b:A):a+b=b+a:=by{casesI
r with _ _ _ _ _ c _ d _ _ e f,let g:=λa:A,trans(by
simp*:_=-(a+-a)+(a+-a+a+-a))$by
simp[<-c,*],let:=λa,trans(by
rw[<-c,e,g]:a+b+_=a+(-a+a))$by
rw[c,g,d],transitivity-a+(1+1)*(a+b)+-b,rw f,simp*,simp*}
```
[Run with Lean Web Editor](https://leanprover-community.github.io/lean-web-editor/#code=import%20tactic.cache%0A%0Auniverse%20u%0A%0Aclass%20ring%20%28%CE%B1%20%3A%20Type%20u%29%20extends%20has_add%20%CE%B1%2C%20has_mul%20%CE%B1%2C%20has_one%20%CE%B1%2C%20has_zero%20%CE%B1%2C%20has_neg%20%CE%B1%20%3A%3D%0A%20%20%28%20add_assoc%20%3A%20%E2%88%80%20a%20b%20c%20%3A%20%CE%B1%2C%20a%20%2B%20%28b%20%2B%20c%29%20%3D%20%28a%20%2B%20b%29%20%2B%20c%20%29%0A%20%20%28%20mul_assoc%20%3A%20%E2%88%80%20a%20b%20c%20%3A%20%CE%B1%2C%20a%20*%20%28b%20*%20c%29%20%3D%20%28a%20*%20b%29%20*%20c%20%29%0A%20%20%28%20add_left_id%20%3A%20%E2%88%80%20a%20%3A%20%CE%B1%2C%200%20%2B%20a%20%3D%20a%20%29%0A%20%20%28%20mul_left_id%20%3A%20%E2%88%80%20a%20%3A%20%CE%B1%2C%201%20*%20a%20%3D%20a%20%29%0A%20%20%28%20mul_right_id%20%3A%20%E2%88%80%20a%20%3A%20%CE%B1%2C%20a%20*%201%20%3D%20a%20%29%0A%20%20%28%20add_left_inv%20%3A%20%E2%88%80%20a%20%3A%20%CE%B1%2C%20%28-a%29%20%2B%20a%20%3D%200%20%29%0A%20%20%28%20left_distribute%20%3A%20%E2%88%80%20a%20b%20c%20%3A%20%CE%B1%2C%20a%20*%20%28b%20%2B%20c%29%20%3D%20a%20*%20b%20%2B%20a%20*%20c%20%29%0A%20%20%28%20right_distribute%20%3A%20%E2%88%80%20a%20b%20c%20%3A%20%CE%B1%2C%20%28a%20%2B%20b%29%20*%20c%20%3D%20a%20*%20c%20%2B%20b%20*%20c%29%0A%0Aopen%20ring%0A%0Adef%20k%7BA%7D%5Br%3Aring%20A%5D%28a%20b%3AA%29%3Aa%2Bb%3Db%2Ba%3A%3Dby%7BcasesI%0Ar%20with%20_%20_%20_%20_%20_%20c%20_%20d%20_%20_%20e%20f%2Clet%20g%3A%3D%CE%BBa%3AA%2Ctrans%28by%0Asimp*%3A_%3D-%28a%2B-a%29%2B%28a%2B-a%2Ba%2B-a%29%29%24by%0Asimp%5B%3C-c%2C*%5D%2Clet%3A%3D%CE%BBa%2Ctrans%28by%0Arw%5B%3C-c%2Ce%2Cg%5D%3Aa%2Bb%2B_%3Da%2B%28-a%2Ba%29%29%24by%0Arw%5Bc%2Cg%2Cd%5D%2Ctransitivity-a%2B%281%2B1%29*%28a%2Bb%29%2B-b%2Crw%20f%2Csimp*%2Csimp*%7D%0A%0Aexample%20%7B%CE%B1%20%3A%20Type*%7D%20%5Bring%20%CE%B1%5D%20%3A%20%E2%88%80%20a%20b%20%3A%20%CE%B1%2C%20a%20%2B%20b%20%3D%20b%20%2B%20a%20%3A%3D%20k)
]