simp only [Set.mem_setOf_eq, Ideal.map_le_iff_le_comap]
case e_a.h
R : Type u_1
S₁ : Type u_2
S₂ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S₁
inst✝² : CommRing S₂
inst✝¹ : Algebra R S₁
inst✝ : Algebra R S₂
e : S₁ ≃ₐ[R] S₂
p : Ideal R
P : Ideal S₂
n : ℕ
⊢ n ∈ {n | map (algebraMap R S₁) p ≤ comap e P ^ n} ↔ n ∈ {n | map (algebraMap R S₂) p ≤ P ^ n}
case e_a.h
R : Type u_1
S₁ : Type u_2
S₂ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S₁
inst✝² : CommRing S₂
inst✝¹ : Algebra R S₁
inst✝ : Algebra R S₂
e : S₁ ≃ₐ[R] S₂
p : Ideal R
P : Ideal S₂
n : ℕ
⊢ p ≤ comap (algebraMap R S₁) (comap e P ^ n) ↔ p ≤ comap (algebraMap R S₂) (P ^ n)