Diagnosing diamonds

Stream: general

[Eric Wieser]

I'm in a proof where my final goal is alternating_map.has_scalar = mul_action.to_has_scalar.

has_scalar has only one field - how do I change the equality to that field and get things to unfold?

[Alex J. Best]

Do cases or congr do what you want?

[Eric Wieser]

cases needs an argument

[Eric Wieser]

And congr fails with no error

[Eric Wieser]

(I got to this goal by applying congr anyway)

[Eric Wieser]

A mwe:

lemma has_scalar.ext {R M : Type*} (a b : has_scalar R M) : a.smul = b.smul → a = b :=
begin
  intro h,
  sorry,
end

[Eric Wieser]

@Bhavik Mehta golfed it with

lemma has_scalar.ext {R M : Type*} : ∀ (a b : has_scalar R M), a.smul = b.smul → a = b
| ⟨_⟩ ⟨_⟩ rfl := rfl

[Sebastien Gouezel]

A non-golfed version:

lemma has_scalar.ext {R M : Type*} (a b : has_scalar R M) : a.smul = b.smul → a = b :=
begin
  intro h,
  tactic.unfreeze_local_instances,
  cases a,
  cases b,
  dsimp at h,
  induction h,
  refl,
end

[Rob Lewis]

Golfed even more:

attribute [ext] has_scalar

[Eric Wieser]

I just noticed that we actually already have docs#module_ext, perhaps this should be expanded to at least semimodule_ext

[Eric Wieser]

And I think ultimately I need a nat version of docs#add_comm_group.module.subsingleton to close my diamond, which ought to be straightforward

[Eric Wieser]

Done in #5396