Leave term mode/calc once you enter it?

Stream: new members

[Abhimanyu Pallavi Sudhir]

Part of my proof involved calc, but now I want to return to tactic mode to complete my proof. How do I do this?

[Abhimanyu Pallavi Sudhir]

The way I've done this in the past is to do the term mode in a separate lemma.

[Andrew Ashworth]

just type begin end again

[Mario Carneiro]

depends on how you have set it up. You could have the calc block inside tactic mode, or you could have a tactic block in one of the steps of a calc block

[Kevin Buzzard]

example : 2 + 2 = 5 :=
begin
  show 3 + 1 = 5,
  exact calc 3 + 1 = 1 + 3 : by simp
        ...        = 2 + 2 : by simp
        ...        = 5     : begin
             show 2 + 2 = 5,
             -- I'm not getting anywhere
             sorry
        end,
end

@Abhimanyu Pallavi Sudhir -- post a MWE if what I said doesn't help.

[Abhimanyu Pallavi Sudhir]

Here's the code:

import tactic.norm_num
definition cong_mod_37 (a b : ℤ) := ∃ k : ℤ, 37 * k = a - b

theorem cong_mod_37_equiv_reln : equivalence cong_mod_37 :=
begin
  split,
    rw reflexive,
    intro x,
    rw cong_mod_37,
    rw sub_self,
    fapply exists.intro,
      exact 0,
    norm_num,
  split,
    rw symmetric,
    intros x y,
    intro HXY,
    rw cong_mod_37,
    rw cong_mod_37 at HXY,
    cases HXY with n Hn,
    fapply exists.intro,
      exact -n,
    show 37 * -n = y - x,
    exact calc 37 * -n = -(37*n) : by rw ←neg_mul_eq_mul_neg
          ... = -(x - y) : by rw Hn
          ... = y - x : by rw neg_sub
--split,
    rw transitive,

    end

[Abhimanyu Pallavi Sudhir]

I did what you said, but that doesn't work.

[Rob Lewis]

You need a comma at the end of the calc.

[Abhimanyu Pallavi Sudhir]

Oh... thanks. Yep, now it's working.