Theorem: l1_2_3_2 (AlgebraI/Subgroups.lean)

State before:
n : ℤ
⊢ ↑(ex1232 n) = {k | n ∣ k}
Tactic:
ext
State after:
case h
n x✝ : ℤ
⊢ x✝ ∈ ↑(ex1232 n) ↔ x✝ ∈ {k | n ∣ k}

State before:
case h
n x✝ : ℤ
⊢ x✝ ∈ ↑(ex1232 n) ↔ x✝ ∈ {k | n ∣ k}
Tactic:
simp [ex1232, Int.mem_zmultiples_iff]
State after:
no goals