-- Mathlib/NumberTheory/RamificationInertia/Basic.lean
lemma ramificationIdx_comap_eq [Algebra R S] (e : S ≃ₐ[R] S₁) (P : Ideal S₁) :
    ramificationIdx (algebraMap R S) p (P.comap e) = ramificationIdx (algebraMap R S₁) p P

Proof state:
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
p : Ideal R
S₁ : Type u_1
inst✝² : CommRing S₁
inst✝¹ : Algebra R S₁
inst✝ : Algebra R S
e : S ≃ₐ[R] S₁
P : Ideal S₁
⊢ ramificationIdx (algebraMap R S) p (comap e P) = ramificationIdx (algebraMap R S₁) p P

Tactic:
dsimp only [ramificationIdx]

Result:
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
p : Ideal R
S₁ : Type u_1
inst✝² : CommRing S₁
inst✝¹ : Algebra R S₁
inst✝ : Algebra R S
e : S ≃ₐ[R] S₁
P : Ideal S₁
⊢ sSup {n | map (algebraMap R S) p ≤ comap e P ^ n} = sSup {n | map (algebraMap R S₁) p ≤ P ^ n}

Proof state:
case e_a.h
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
p : Ideal R
S₁ : Type u_1
inst✝² : CommRing S₁
inst✝¹ : Algebra R S₁
inst✝ : Algebra R S
e : S ≃ₐ[R] S₁
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]

Result:
case e_a.h
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
p : Ideal R
S₁ : Type u_1
inst✝² : CommRing S₁
inst✝¹ : Algebra R S₁
inst✝ : Algebra R S
e : S ≃ₐ[R] S₁
P : Ideal S₁
n : ℕ
⊢ p ≤ comap (algebraMap R S) (comap e P ^ n) ↔ p ≤ comap (algebraMap R S₁) (P ^ n)

Proof state:
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
p : Ideal R
S₁ : Type u_1
inst✝² : CommRing S₁
inst✝¹ : Algebra R S₁
inst✝ : Algebra R S
e : S ≃ₐ[R] S₁
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

Result:
case e_a
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
p : Ideal R
S₁ : Type u_1
inst✝² : CommRing S₁
inst✝¹ : Algebra R S₁
inst✝ : Algebra R S
e : S ≃ₐ[R] S₁
P : Ideal S₁
⊢ {n | map (algebraMap R S) p ≤ comap e P ^ n} = {n | map (algebraMap R S₁) p ≤ P ^ n}

Proof state:
case e_a
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
p : Ideal R
S₁ : Type u_1
inst✝² : CommRing S₁
inst✝¹ : Algebra R S₁
inst✝ : Algebra R S
e : S ≃ₐ[R] S₁
P : Ideal S₁
⊢ {n | map (algebraMap R S) p ≤ comap e P ^ n} = {n | map (algebraMap R S₁) p ≤ P ^ n}

Tactic:
ext n

Result:
case e_a.h
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
p : Ideal R
S₁ : Type u_1
inst✝² : CommRing S₁
inst✝¹ : Algebra R S₁
inst✝ : Algebra R S
e : S ≃ₐ[R] S₁
P : Ideal S₁
n : ℕ
⊢ n ∈ {n | map (algebraMap R S) p ≤ comap e P ^ n} ↔ n ∈ {n | map (algebraMap R S₁) p ≤ P ^ n}

Proof state:
case e_a.h
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
p : Ideal R
S₁ : Type u_1
inst✝² : CommRing S₁
inst✝¹ : Algebra R S₁
inst✝ : Algebra R S
e : S ≃ₐ[R] S₁
P : Ideal S₁
n : ℕ
⊢ p ≤ comap (algebraMap R S) (comap e P ^ n) ↔ p ≤ comap (algebraMap R S₁) (P ^ n)

Tactic:
rw [← comap_coe e, ← e.toRingEquiv_toRingHom, comap_coe, ← RingEquiv.symm_symm (e : S ≃+* S₁),
  ← map_comap_of_equiv, ← Ideal.map_pow, map_comap_of_equiv, ← comap_coe (RingEquiv.symm _),
  comap_comap, RingEquiv.symm_symm, e.toRingEquiv_toRingHom, ← e.toAlgHom_toRingHom,
  AlgHom.comp_algebraMap]

Result:
no goals