-- Mathlib/NumberTheory/RamificationInertia/Basic.lean
lemma inertiaDeg_comap_eq (e : S ≃ₐ[R] S₁) (P : Ideal S₁) [p.IsMaximal] :
    inertiaDeg p (P.comap e) = inertiaDeg p P

Proof state:
case pos
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₁
inst✝ : p.IsMaximal
he : comap f (comap e P) = p ↔ comap (algebraMap R S₁) P = p
h : P.LiesOver p
⊢ finrank (R ⧸ p) (S ⧸ comap e P) = finrank (R ⧸ p) (S₁ ⧸ P)

Tactic:
exact (Quotient.algEquivOfEqComap p e rfl).toLinearEquiv.finrank_eq

Result:
no goals

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₁
inst✝ : p.IsMaximal
⊢ p.inertiaDeg (comap e P) = p.inertiaDeg P

Tactic:
have he : (P.comap e).comap (algebraMap R S) = p ↔ P.comap (algebraMap R S₁) = p := by
  rw [← comap_coe e, comap_comap, ← e.toAlgHom_toRingHom, AlgHom.comp_algebraMap]

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₁
inst✝ : p.IsMaximal
he : comap f (comap e P) = p ↔ comap (algebraMap R S₁) P = p
⊢ p.inertiaDeg (comap e P) = p.inertiaDeg 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₁
inst✝ : p.IsMaximal
⊢ comap f (comap e P) = p ↔ comap (algebraMap R S₁) P = p

Tactic:
rw [← comap_coe e, comap_comap, ← e.toAlgHom_toRingHom, AlgHom.comp_algebraMap]

Result:
no goals

Proof state:
case neg
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₁
inst✝ : p.IsMaximal
he : comap f (comap e P) = p ↔ comap (algebraMap R S₁) P = p
h : ¬P.LiesOver p
⊢ p.inertiaDeg (comap e P) = p.inertiaDeg P

Tactic:
rw [inertiaDeg, dif_neg (fun eq => h ⟨(he.mp eq).symm⟩)]

Result:
case neg
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₁
inst✝ : p.IsMaximal
he : comap f (comap e P) = p ↔ comap (algebraMap R S₁) P = p
h : ¬P.LiesOver p
⊢ 0 = p.inertiaDeg 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₁
inst✝ : p.IsMaximal
he : comap f (comap e P) = p ↔ comap (algebraMap R S₁) P = p
⊢ p.inertiaDeg (comap e P) = p.inertiaDeg P

Tactic:
by_cases h : P.LiesOver p

Result:
case pos
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₁
inst✝ : p.IsMaximal
he : comap f (comap e P) = p ↔ comap (algebraMap R S₁) P = p
h : P.LiesOver p
⊢ p.inertiaDeg (comap e P) = p.inertiaDeg P

case neg
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₁
inst✝ : p.IsMaximal
he : comap f (comap e P) = p ↔ comap (algebraMap R S₁) P = p
h : ¬P.LiesOver p
⊢ p.inertiaDeg (comap e P) = p.inertiaDeg P

Proof state:
case neg
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₁
inst✝ : p.IsMaximal
he : comap f (comap e P) = p ↔ comap (algebraMap R S₁) P = p
h : ¬P.LiesOver p
⊢ 0 = p.inertiaDeg P

Tactic:
rw [inertiaDeg, dif_neg (fun eq => h ⟨eq.symm⟩)]

Result:
no goals

Proof state:
case pos
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₁
inst✝ : p.IsMaximal
he : comap f (comap e P) = p ↔ comap (algebraMap R S₁) P = p
h : P.LiesOver p
⊢ p.inertiaDeg (comap e P) = p.inertiaDeg P

Tactic:
rw [inertiaDeg_algebraMap, inertiaDeg_algebraMap]

Result:
case pos
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₁
inst✝ : p.IsMaximal
he : comap f (comap e P) = p ↔ comap (algebraMap R S₁) P = p
h : P.LiesOver p
⊢ finrank (R ⧸ p) (S ⧸ comap e P) = finrank (R ⧸ p) (S₁ ⧸ P)