Variable marked as unused when it isn't

Stream: lean4

[Niels Voss]

I was writing a tactic proof and declared a variable U with let, which I used throughout the proof. However, U is marked as unused by the linter. Am I doing something wrong or is there a bug in the linter? This isn't a big deal, but I'm just curious.

import Mathlib

set_option autoImplicit false

variable {α : Type*}

-- https://math.stackexchange.com/a/4204
theorem continuous_induction [ConditionallyCompleteLinearOrder α] {l : α} {s : Set α}
  (h₁ : ∀ x ∈ s, IsMax x ∨ ∃ y > x, Set.Ico x y ⊆ s) (h₂ : ∀ y ≥ l, Set.Ico l y ⊆ s → y ∈ s)
  : Set.Ici l ⊆ s := by
    by_contra hc
    let U := sᶜ ∩ Set.Ici l -- unused variable `U` [linter.unusedVariables]

    -- Proof that `U` is nonempty
    rw [Set.not_subset] at hc
    obtain ⟨t, ht₁, ht₂⟩ := hc
    have ht₃ : t ∈ U := ⟨ht₂, ht₁⟩
    have hU : U.Nonempty := ⟨t, ht₃⟩

    -- `l` is a lower bound to U
    have hl : l ∈ lowerBounds U := by
      apply union_lowerBounds_subset_lowerBounds_inter
      apply Set.mem_union_right
      rw [lowerBounds_Ici]
      exact Set.right_mem_Iic

    -- Let `y` be the greatest lower bound of `U`. From (iii), `y ∈ s`
    let y := sInf U
    have hyl : l ≤ y := le_csInf hU hl
    have hy : y ∈ s := by
      apply h₂ y hyl
      intro x ⟨hx₁, hx₂⟩
      have : x ∈ (sᶜ ∩ Set.Ici l)ᶜ := not_mem_of_lt_csInf hx₂ ⟨l, hl⟩
      rw [Set.compl_inter, Set.mem_union] at this
      cases this with
      | inl h => exact Set.not_not_mem.mp h
      | inr h => exact (h hx₁).elim

    cases h₁ y hy with
    | inr hz =>
      obtain ⟨z, hz₁, hz₂⟩ := hz
      apply not_le_of_lt hz₁
      apply le_csInf hU
      intro x hx
      cases le_or_lt y x with
      | inr h =>
        have : y ≤ x := csInf_le ⟨l, hl⟩ hx
        exact absurd h (not_lt_of_le this)
      | inl h =>
        by_contra hx'
        push_neg at hx'
        have : x ∈ s := hz₂ ⟨h, hx'⟩
        have : x ∈ sᶜ := Set.mem_of_mem_inter_left hx
        contradiction
    | inl hm =>
      have : y = t := IsMax.eq_of_le hm (csInf_le ⟨l, hl⟩  ht₃)
      rw [this] at hy
      exact absurd hy ht₂

This was tested both on a slightly outdated version of Lean and live.lean-lang.org so this must not be a new problem.

[Mauricio Collares]

Weird, the let U line appears twice if you #print continuous_induction.