From 7d88a30acc714e2941ec12384a6263a28c7a6e90 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Sun, 23 Aug 2020 06:36:27 +0000
Subject: [PATCH] fix(data/sigma/basic): rename `ext` to `sigma.ext` (#3916)

---
 src/data/sigma/basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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₁ :=