How to write in Lean

Stream: new members

[Ipojucã Moraes da Cruz]

I´d like to prove a * 0 = 0 by proving if a + ( a * 0 ) = a then a * 0 = 0 , how can I end this

theorem ZA_AnR: ∀ (a : ℤ), a * 0 = 0 :=
begin
  intro a,

  have h: a + (a * 0) = a,

    calc
    a + (a * 0) = a * 1 + (a * 0) : by rw [int.mul_one a]
            ... = a * (1 + 0)     : by rw ← int.distrib_left
            ... = a * 1           : by rw int.add_zero
            ... = a               : by rw int.mul_one,

end

[Ruben Van de Velde]

Maybe with this substep:

theorem ZA_AnR: ∀ (a : ℤ), a * 0 = 0 :=
begin
  intro a,

  have h: a + (a * 0) = a,

    calc
    a + (a * 0) = a * 1 + (a * 0) : by rw [int.mul_one a]
            ... = a * (1 + 0)     : by rw ← int.distrib_left
            ... = a * 1           : by rw int.add_zero
            ... = a               : by rw int.mul_one,
  have h' : a + (a * 0) = a + 0, sorry,
  exact add_left_cancel h',
end

[Yaël Dillies]

I've wanted a + b = b -> a = 0 as a lemma periodically, so we might just add it.

[Kyle Miller]

@Yaël Dillies docs#add_left_eq_self?

example (a b : ℤ) : a + b = b → a = 0 := add_left_eq_self.mp

[Ruben Van de Velde]

Looked for that, but I needed kyle_search, clearly :)

[Yaël Dillies]

Ah right. It's not missing but it's misnamed.

[Yaël Dillies]

Each time I look for add_eq_right, add_eq_right_iff...