Theorem: Ideal.ramificationIdx_comap_eq (FltRegular/NumberTheory/AuxLemmas.lean)

State before:
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₂
⊢ ramificationIdx (algebraMap R S₁) p (comap e P) = ramificationIdx (algebraMap R S₂) p P
Tactic:
show sSup _ = sSup _
State after:
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₂
⊢ sSup {n | map (algebraMap R S₁) p ≤ comap e P ^ n} = sSup {n | map (algebraMap R S₂) p ≤ P ^ n}

State before:
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₂
⊢ sSup {n | map (algebraMap R S₁) p ≤ comap e P ^ n} = sSup {n | map (algebraMap R S₂) p ≤ P ^ n}
Tactic:
congr
State after:
case e_a
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 | map (algebraMap R S₁) p ≤ comap e P ^ n} = {n | map (algebraMap R S₂) p ≤ P ^ n}

State before:
case e_a
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 | map (algebraMap R S₁) p ≤ comap e P ^ n} = {n | map (algebraMap R S₂) p ≤ P ^ n}
Tactic:
ext n
State after:
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}

State before:
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}
Tactic:
simp only [Set.mem_setOf_eq, Ideal.map_le_iff_le_comap]
State after:
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)

State before:
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)
Tactic:
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]
State after:
no goals