R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
inst✝¹ : IsDomain S
inst✝ : IsDedekindDomain S
hp0 : map f p ≠ ⊥
hP : IsPrime P
le : map f p ≤ P
hP0 : P ≠ ⊥
⊢ ramificationIdx f p P ≠ 0
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
inst✝¹ : IsDomain S
inst✝ : IsDedekindDomain S
hp0 : map f p ≠ ⊥
hP : IsPrime P
le : map f p ≤ P
⊢ ramificationIdx f p P ≠ 0
have hP0 : P ≠ ⊥ := by
  rintro rfl
  have := le_bot_iff.mp le
  contradiction
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
inst✝¹ : IsDomain S
inst✝ : IsDedekindDomain S
hp0 : map f p ≠ ⊥
hP : IsPrime P
le : map f p ≤ P
hP0 : P ≠ ⊥
hPirr : Irreducible P
⊢ ramificationIdx f p P ≠ 0
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
inst✝¹ : IsDomain S
inst✝ : IsDedekindDomain S
hp0 : map f p ≠ ⊥
hP : IsPrime P
le : map f p ≤ P
hP0 : P ≠ ⊥
⊢ ramificationIdx f p P ≠ 0
have hPirr := (Ideal.prime_of_isPrime hP0 hP).irreducible
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
inst✝¹ : IsDomain S
inst✝ : IsDedekindDomain S
hp0 : map f p ≠ ⊥
hP : IsPrime P
le : map f p ≤ P
hP0 : P ≠ ⊥
hPirr : Irreducible P
⊢ Multiset.count P (normalizedFactors (map f p)) ≠ 0
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
inst✝¹ : IsDomain S
inst✝ : IsDedekindDomain S
hp0 : map f p ≠ ⊥
hP : IsPrime P
le : map f p ≤ P
hP0 : P ≠ ⊥
hPirr : Irreducible P
⊢ ramificationIdx f p P ≠ 0
rw [IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count hp0 hP hP0]
case intro.intro
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
inst✝¹ : IsDomain S
inst✝ : IsDedekindDomain S
hp0 : map f p ≠ ⊥
hP : IsPrime P
le : map f p ≤ P
hP0 : P ≠ ⊥
hPirr : Irreducible P
P' : Ideal S
hP' : P' ∈ normalizedFactors (map f p)
P'_eq : Associated P P'
⊢ Multiset.count P (normalizedFactors (map f p)) ≠ 0
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
inst✝¹ : IsDomain S
inst✝ : IsDedekindDomain S
hp0 : map f p ≠ ⊥
hP : IsPrime P
le : map f p ≤ P
hP0 : P ≠ ⊥
hPirr : Irreducible P
⊢ Multiset.count P (normalizedFactors (map f p)) ≠ 0
obtain ⟨P', hP', P'_eq⟩ :=
  exists_mem_normalizedFactors_of_dvd hp0 hPirr (Ideal.dvd_iff_le.mpr le)
no goals
case intro.intro
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
inst✝¹ : IsDomain S
inst✝ : IsDedekindDomain S
hp0 : map f p ≠ ⊥
hP : IsPrime P
le : map f p ≤ P
hP0 : P ≠ ⊥
hPirr : Irreducible P
P' : Ideal S
hP' : P' ∈ normalizedFactors (map f p)
P'_eq : Associated P P'
⊢ Multiset.count P (normalizedFactors (map f p)) ≠ 0
rwa [Multiset.count_ne_zero, associated_iff_eq.mp P'_eq]
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
f : R →+* S
p : Ideal R
inst✝¹ : IsDomain S
inst✝ : IsDedekindDomain S
hp0 : map f p ≠ ⊥
hP : IsPrime ⊥
le : map f p ≤ ⊥
⊢ False
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
inst✝¹ : IsDomain S
inst✝ : IsDedekindDomain S
hp0 : map f p ≠ ⊥
hP : IsPrime P
le : map f p ≤ P
⊢ P ≠ ⊥
rintro rfl
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
f : R →+* S
p : Ideal R
inst✝¹ : IsDomain S
inst✝ : IsDedekindDomain S
hp0 : map f p ≠ ⊥
hP : IsPrime ⊥
le : map f p ≤ ⊥
this : map f p = ⊥
⊢ False
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
f : R →+* S
p : Ideal R
inst✝¹ : IsDomain S
inst✝ : IsDedekindDomain S
hp0 : map f p ≠ ⊥
hP : IsPrime ⊥
le : map f p ≤ ⊥
⊢ False
have := le_bot_iff.mp le
no goals
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
f : R →+* S
p : Ideal R
inst✝¹ : IsDomain S
inst✝ : IsDedekindDomain S
hp0 : map f p ≠ ⊥
hP : IsPrime ⊥
le : map f p ≤ ⊥
this : map f p = ⊥
⊢ False
contradiction