-- Mathlib/NumberTheory/RamificationInertia/Basic.lean
theorem ramificationIdx_ne_zero (hp0 : map f p ≠ ⊥) (hP : P.IsPrime) (le : map f p ≤ P) :
    ramificationIdx f p P ≠ 0

Proof state:
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
inst✝ : IsDedekindDomain S
hp0 : map f p ≠ ⊥
hP : P.IsPrime
le : map f p ≤ P
hP0 : P ≠ ⊥
hPirr : Irreducible P
⊢ Multiset.count P (normalizedFactors (map f p)) ≠ 0

Tactic:
obtain ⟨P', hP', P'_eq⟩ :=
  exists_mem_normalizedFactors_of_dvd hp0 hPirr (Ideal.dvd_iff_le.mpr le)

Result:
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✝ : IsDedekindDomain S
hp0 : map f p ≠ ⊥
hP : P.IsPrime
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

Proof state:
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
inst✝ : IsDedekindDomain S
hp0 : map f p ≠ ⊥
hP : P.IsPrime
le : map f p ≤ P
⊢ ramificationIdx f p P ≠ 0

Tactic:
classical
have hP0 : P ≠ ⊥ := by
  rintro rfl
  exact hp0 (le_bot_iff.mp le)
have hPirr := (Ideal.prime_of_isPrime hP0 hP).irreducible
rw [IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count hp0 hP hP0]
obtain ⟨P', hP', P'_eq⟩ :=
  exists_mem_normalizedFactors_of_dvd hp0 hPirr (Ideal.dvd_iff_le.mpr le)
rwa [Multiset.count_ne_zero, associated_iff_eq.mp P'_eq]

Result:
no goals

Proof state:
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
inst✝ : IsDedekindDomain S
hp0 : map f p ≠ ⊥
hP : P.IsPrime
le : map f p ≤ P
hP0 : P ≠ ⊥
hPirr : Irreducible P
⊢ ramificationIdx f p P ≠ 0

Tactic:
rw [IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count hp0 hP hP0]

Result:
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
inst✝ : IsDedekindDomain S
hp0 : map f p ≠ ⊥
hP : P.IsPrime
le : map f p ≤ P
hP0 : P ≠ ⊥
hPirr : Irreducible P
⊢ Multiset.count P (normalizedFactors (map f p)) ≠ 0

Proof state:
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
p : Ideal R
inst✝ : IsDedekindDomain S
hp0 : map f p ≠ ⊥
hP : ⊥.IsPrime
le : map f p ≤ ⊥
⊢ False

Tactic:
exact hp0 (le_bot_iff.mp le)

Result:
no goals

Proof state:
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✝ : IsDedekindDomain S
hp0 : map f p ≠ ⊥
hP : P.IsPrime
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

Tactic:
rwa [Multiset.count_ne_zero, associated_iff_eq.mp P'_eq]

Result:
no goals

Proof state:
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
inst✝ : IsDedekindDomain S
hp0 : map f p ≠ ⊥
hP : P.IsPrime
le : map f p ≤ P
hP0 : P ≠ ⊥
⊢ ramificationIdx f p P ≠ 0

Tactic:
have hPirr := (Ideal.prime_of_isPrime hP0 hP).irreducible

Result:
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
inst✝ : IsDedekindDomain S
hp0 : map f p ≠ ⊥
hP : P.IsPrime
le : map f p ≤ P
hP0 : P ≠ ⊥
hPirr : Irreducible P
⊢ ramificationIdx f p P ≠ 0

Proof state:
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
inst✝ : IsDedekindDomain S
hp0 : map f p ≠ ⊥
hP : P.IsPrime
le : map f p ≤ P
⊢ ramificationIdx f p P ≠ 0

Tactic:
have hP0 : P ≠ ⊥ := by
  rintro rfl
  exact hp0 (le_bot_iff.mp le)

Result:
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
inst✝ : IsDedekindDomain S
hp0 : map f p ≠ ⊥
hP : P.IsPrime
le : map f p ≤ P
hP0 : P ≠ ⊥
⊢ ramificationIdx f p P ≠ 0

Proof state:
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
inst✝ : IsDedekindDomain S
hp0 : map f p ≠ ⊥
hP : P.IsPrime
le : map f p ≤ P
⊢ P ≠ ⊥

Tactic:
rintro rfl

Result:
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
p : Ideal R
inst✝ : IsDedekindDomain S
hp0 : map f p ≠ ⊥
hP : ⊥.IsPrime
le : map f p ≤ ⊥
⊢ False