case mk
q : ℕ+
y : X q
fst✝ snd✝ : ZMod ↑q
h₁ : (fst✝, snd✝).fst = y.fst
h₂ : (fst✝, snd✝).snd = y.snd
⊢ (fst✝, snd✝) = y
q : ℕ+
x y : X q
h₁ : x.fst = y.fst
h₂ : x.snd = y.snd
⊢ x = y
cases x
case mk.mk
q : ℕ+
fst✝¹ snd✝¹ fst✝ snd✝ : ZMod ↑q
h₁ : (fst✝¹, snd✝¹).fst = (fst✝, snd✝).fst
h₂ : (fst✝¹, snd✝¹).snd = (fst✝, snd✝).snd
⊢ (fst✝¹, snd✝¹) = (fst✝, snd✝)
case mk
q : ℕ+
y : X q
fst✝ snd✝ : ZMod ↑q
h₁ : (fst✝, snd✝).fst = y.fst
h₂ : (fst✝, snd✝).snd = y.snd
⊢ (fst✝, snd✝) = y
cases y
no goals
case mk.mk
q : ℕ+
fst✝¹ snd✝¹ fst✝ snd✝ : ZMod ↑q
h₁ : (fst✝¹, snd✝¹).fst = (fst✝, snd✝).fst
h₂ : (fst✝¹, snd✝¹).snd = (fst✝, snd✝).snd
⊢ (fst✝¹, snd✝¹) = (fst✝, snd✝)
congr