simp only sigma

Stream: lean4

[Patrick Massot]

In Lean 3 if we do

example {α : Type*} {β : α → Type*} (a : α) (x y : β a) (h : (⟨a, x⟩ : Σ a, β a) = ⟨a, y⟩) : false :=
begin
  simp only at h,
  sorry
end

the simp only at h changes h to a = a ∧ x == y. The corresponding Lean 4 code

example {α : Type _} {β : α → Type _} (a : α) (x y : β a) (h : (⟨a, x⟩ : Σ a, β a) = ⟨a, y⟩) : False :=
by
  simp only at h
  sorry

doesn't seem to do anything.

[Patrick Massot]

This isn't important but I wanted to report it since it breaks a proof I'm porting.

[Kevin Buzzard]

I think these things are important, because if we don't catch regressions with behaviour in simp when it's proving simple stuff, then it will be much harder to fix them once we're trying to make sense of why 50-line proofs with really complicated simp onlys are failing.

[Kevin Buzzard]

I hoped that adding

@[congr] theorem foo {α : Type _} {β : α → Type _} (a₁ : α) (b₁ : β a₁) (a₂ : α) (b₂ : β a₂)
    (h : (a₁ = a₂ ∧ HEq b₁ b₂)) : Sigma.mk a₁ b₁ = Sigma.mk a₂ b₂ := sorry

would fix it (I learnt recently that congr lemmas can change the behaviour of simp only) but it doesn't seem to work here.