rw [← Ideal.comap_coe e, ← e.toRingEquiv_toRingHom, Ideal.comap_coe,
  ← RingEquiv.symm_symm (e : S₁ ≃+* S₂), ← Ideal.map_comap_of_equiv, ← Ideal.map_pow,
  Ideal.map_comap_of_equiv, ← Ideal.comap_coe (RingEquiv.symm _), Ideal.comap_comap,
  RingEquiv.symm_symm, e.toRingEquiv_toRingHom, ← e.toAlgHom_toRingHom, AlgHom.comp_algebraMap]
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)
no goals