golfing identical left and right cases

Stream: general

[Johan Commelin]

I've got

    cases is_valuation.map_add v₂ r s,
    { left,
      rw with_zero.map_le Hle,
      rwa [←H12, ←H12] at h },
    { right,
      rw with_zero.map_le Hle,
      rwa [←H12, ←H12] at h },

Is there a tactic that allows to golf this? The only difference is the left and right tactic...

[Seul Baek]

You can do slightly better with

    cases is_valuation.map_add v₂ r s;
    [{left},{right}];
    { rw with_zero.map_le Hle,
      rwa [←H12, ←H12] at h }

but it's not by much

[Johan Commelin]

Cool, that is more or less what I was looking for!
Can you explain the magic on line 2?

[Mario Carneiro]

How about

  apply (is_valuation.map_add v₂ r s).imp;
  { intro Hle,
    rw with_zero.map_le Hle,
    rwa [←H12, ←H12] at h }

[Mario Carneiro]

The magic on line 2 is the tac; [tac1, tac2] combinator. It applies tac1 to the first goal and tac2 to the second. If you put another ; tac at the end, it will be applied to all subgoals generated by the first combination of tactics

[Johan Commelin]

Ok, nice.

[Johan Commelin]

@Mario Carneiro Your suggestion isn't working. is_valuation.map_add _ _ _ returns an _ ∨ _. And I do cases on that.

[Mario Carneiro]

does refine (is_valuation.map_add v₂ r s).imp (\lam Hle, _) (\lam Hle, _); work?

[Mario Carneiro]

or refine (is_valuation.map_add v₂ r s).imp _ _ with the intro line

[Mario Carneiro]

You are casing on or, and then reconstructing an or where the left goes left and the right goes right. That's or.imp

[Seul Baek]

In general the syntax tac_0; [tac_1, ..., tac_n] will apply tac_i to the ith subgoal generated by tac_0, with the restriction that the number of tactics n matches the number of subgoals generated

[Johan Commelin]

@Mario Carneiro This works. Thanks!

    apply (is_valuation.map_add v₂ r s).imp _ _;
    erw [with_zero.map_le Hle, ←H12, ←H12];
    exact id