English
There is a correspondence between equal first coordinates modulo I.goursatFst and equal second coordinates modulo I.goursatSnd, when x,y come from I.
Русский
Существуют соответствия между равенством первых координат по модулю I.goursatFst и равенством вторых координат по модулю I.goursatSnd, когда x,y принадлежат I.
LaTeX
$$$$\\forall {x y: G \\times H}, (hx : x \\in I) (hy : y\\in I) \\\\; (x.1 : G / I.goursatFst) = (y.1 : G / I.goursatFst) \\\\iff (x.2 : H / I.goursatSnd) = (y.2 : H / I.goursatSnd).$$$$
Lean4
@[to_additive]
theorem mk_goursatFst_eq_iff_mk_goursatSnd_eq {x y : G × H} (hx : x ∈ I) (hy : y ∈ I) :
(x.1 : G ⧸ I.goursatFst) = y.1 ↔ (x.2 : H ⧸ I.goursatSnd) = y.2 :=
by
have := normal_goursatFst hI₁
have := normal_goursatSnd hI₂
rw [eq_comm]
simp only [QuotientGroup.eq_iff_div_mem, mem_goursatFst, mem_goursatSnd]
constructor <;> intro h
· simpa [Prod.mul_def, Prod.div_def] using div_mem (mul_mem h hx) hy
· simpa [Prod.mul_def, Prod.div_def] using div_mem (mul_mem h hy) hx
