grind and goal management

Stream: new members

[Nathan]

i have some unrelated questions. does grind slow vscode? and i know <;> can apply a tactic to all goals at once. can i apply a tactic to only certain goals which i specify?

[Aaron Liu]

can you give a #mwe? also this probably belongs on a new thread

[Notification Bot]

2 messages were moved here from #new members > extrema, R^n by Ruben Van de Velde.

[Nathan]

thanks ruben

[Nathan]

for example, can i clear the first two goals here at the same time?

import Mathlib.Data.Real.Basic
import Mathlib.Data.Real.Sign

open Real

example {a b : ℝ} : sign a * sign b = sign (a*b) := by
  have : a = 0 ∨ b = 0 ∨ (a > 0 ∧ b > 0) ∨ (a > 0 ∧ b < 0) ∨ (a < 0 ∧ b > 0) ∨ (a < 0 ∧ b < 0) :=
    by grind
  rcases this with ah | bh | ⟨ah, bh⟩ | ⟨ah, bh⟩ | ⟨ah, bh⟩ | ⟨ah, bh⟩ <;> unfold sign
  · simp[ah]
  · simp[bh]
  · simp[ah, bh]
    simp[Std.not_gt_of_lt ah, Std.not_gt_of_lt bh, Std.not_gt_of_lt (Left.mul_pos ah bh)]
  · simp[ah, bh]; simp[Std.not_gt_of_lt ah, mul_neg_of_pos_of_neg ah bh]
  · simp[bh, ah]; simp[Std.not_gt_of_lt bh, mul_neg_of_neg_of_pos ah bh]
  · have := mul_pos_of_neg_of_neg ah bh
    simp[ah, bh, this, Std.not_gt_of_lt this]

[Aaron Liu]

well you can use case inl | inr.inl => tacs to select those first two goals

[Aaron Liu]

there's also on_goal which doesn't require you to know the tags of the goals you want but can only select one goal

[Aaron Liu]

maybe on_goal should have a version where it takes a list of goal numbers and does all of them

[Nathan]

thanks, that first suggestion is just what i was looking for :pray:

[Nathan]

oh i can do this

example {a b : ℝ} : sign a * sign b = sign (a*b) := by
  unfold sign; rcases (lt_trichotomy a 0) with c | c | c
  <;> rcases (lt_trichotomy b 0) with d | d | d
  <;> simp[c, d, Std.not_gt_of_lt, mul_neg_of_pos_of_neg, mul_pos_of_neg_of_neg]