Flexible linter doesn't trigger on `simp` + `exact`

Stream: mathlib4

[Snir Broshi]

I might be misunderstanding the flexible linter, but this looks like a bug to me.

1. Doesn't trigger:

theorem foo {x₁ x₂ : Nat} {l₁ l₂ : List Nat} (h : x₁ :: l₁ = x₂ :: l₂) : l₁ = l₂ := by
  simp at h
  exact h.right

2. Doesn't trigger:

theorem foo {x₁ x₂ : Nat} {l₁ l₂ : List Nat} (h : x₁ :: l₁ = x₂ :: l₂) : l₁ = l₂ := by
  simp at h
  have := h.right
  sorry

3. Triggers (false positive):

theorem foo {x₁ x₂ : Nat} {l₁ l₂ : List Nat} (h : x₁ :: l₁ = x₂ :: l₂) : l₁ = l₂ := by
  simp at h
  let h := 3
  sorry

[Damiano Testa]

The first one should definitely complain, and indeed this version does complain:

import Mathlib

set_option linter.flexible true

theorem foo {x₁ x₂ : Nat} {l₁ l₂ : List Nat} (h : x₁ :: l₁ = x₂ :: l₂) : l₁ = l₂ := by
  simp at h
  cases h
  assumption

[Damiano Testa]

I am a bit surprised that the linter even says anything when there is a sorry: I thought that the linter was quiet when there were other messages already.

[Snir Broshi]

Opened issue #32257