interactive tactics in calc

Stream: new members

[Miguel Marco]

When using the calc tactic, we must provide a proof for each step, but I can't see the context and goal when writing it.

Is there a way to get it?

Also, I am being unable to prove this (apparently) simple goal:

c e : ℝ,
h : c < 0
⊢ c * e / -c = -e

I tried the usual simp, field_simp, norm_num, library_searchand so on, but they don't work.

[Kyle Miller]

When I want to see a context and goal somewhere, I usually insert a begin end or a by { }. (Sometimes you need parentheses, like (by { }).)

[Kyle Miller]

It seems that that the lemmas involved need that c is not equal to zero, rather than c is positive. You can get that fact from h.ne (or ne_of_le h, I believe).

A proof I found:

example (c e : ℝ) (h : c < 0) : c * e / -c = -e :=
begin
  rw [div_neg, neg_inj, mul_comm],
  simp [h.ne],
end

[Ruben Van de Velde]

A lemma like div_self is the main part of the argument; you just need to rearrange the terms until that applies