How to use calc

Stream: new members

[Ipojucã Moraes da Cruz]

I would like to rewrite the lemma ZA_Unid, using calc and in a way that apply the variables in the hypothesis and use the lemmas ZA_IdR, ZA_idR. I think by making the correct use of the tool this proof can get much smaller

lemma ZA_IdR : (∀a :ℤ, a + 0 = a) :=
begin
  intro a,
  rw int.add_zero, -- O add_zero aqui faz o papel do nosso Axiom
end

lemma ZA_IdL : (∀a :ℤ, 0 + a = a) :=
begin
  intro a,
  rw add_comm,
  rw ZA_IdR,
end

lemma ZA_UniId (u v: ℤ ): ∀ (a: ℤ ), ( u + a = a) ∧ ( a + v = a ) → u = v:=
begin
  intro a,                        -- Seja a inteiro
  intro h,                        -- Suponha h: u + a = a ∧ a + v = a
  cases h with hL hR,             -- Dividimos em casos hL: u + a = a  hR: a + v = a
                                  -- Calculamos
                                  -- hL:
  rw ← add_neg_eq_zero at hL,     -- u + a + -a = 0
  rw add_assoc at hL,             -- u + (a + -a) = 0
  rw int.add_right_neg at hL,     -- u + 0 = 0
  rw ZA_IdR at hL,                -- u = 0
                                  -- hR:
  rw ← add_neg_eq_zero at hR,     -- a + v + -a = 0
  rw int.add_comm a v at hR,      -- v + a + -a = 0
  rw add_assoc at hR,             -- v + (a + -a) = 0
  rw int.add_right_neg at hR,     -- v + 0 = 0
  rw ZA_IdR at hR,                -- v = 0
  rw hL,                          -- aplico hL no alvo  0 = v
  rw hR,                          -- aplico hR no alvo  0 = 0
end

[Kevin Buzzard]

import tactic

lemma ZA_UniId (u v: ℤ ): ∀ (a: ℤ ), ( u + a = a) ∧ ( a + v = a ) → u = v:=
begin
  rintro a ⟨hL, hR⟩,
  calc u = u + 0 : by rw add_zero
  ...    = u + (a + -a) : by rw int.add_right_neg
  ...    = (u + a) + -a : by rw add_assoc
  ...    = a + -a : by rw hL
  ...    = -a + a : by rw add_comm
  ...    = -a + (a + v) : by rw hR
  ...    = (-a + a) + v : by rw add_assoc
  ...    = 0 + v : by rw add_left_neg
  ...    = v : by rw zero_add
end

lemma ZA_UniId' (u v: ℤ ): ∀ (a: ℤ ), ( u + a = a) ∧ ( a + v = a ) → u = v:=
begin
  rintro a ⟨hL, hR⟩,
  linarith,
end