diff --git a/src/data/sigma/basic.lean b/src/data/sigma/basic.lean
index 864bfce04a105..5f0e6d27fc0f2 100644
--- a/src/data/sigma/basic.lean
+++ b/src/data/sigma/basic.lean
@@ -34,7 +34,7 @@ by simp
 | ⟨i, x⟩ := rfl
 
 @[ext]
-lemma ext {x₀ x₁ : sigma β}
+lemma sigma.ext {x₀ x₁ : sigma β}
   (h₀ : x₀.1 = x₁.1)
   (h₁ : x₀.1 = x₁.1 → x₀.2 == x₁.2) :
   x₀ = x₁ :=