awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : IsDedekindDomain S
h₁ : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊤
h₂ : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
h : map (F := R →+* S) f p ≤ HPow.hPow (α := Ideal S) (map (F := R →+* S) f p) (HAdd.hAdd (α := ℕ) 1 1)
this :
  HPow.hPow (α := Ideal S) (β := ℕ) (map (F := R →+* S) f p) 1 =
    HPow.hPow (α := Ideal S) (β := ℕ) (map (F := R →+* S) f p) 2
⊢ Eq (α := ℕ) 1 2

Tactic:
have := IsMulTorsionFree.pow_right_injective₀ (by rwa [one_eq_top]) h₂ this
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : IsDedekindDomain S
h₁ : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊤
h₂ : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
h : map (F := R →+* S) f p ≤ HPow.hPow (α := Ideal S) (map (F := R →+* S) f p) (HAdd.hAdd (α := ℕ) 1 1)
this_1 :
  HPow.hPow (α := Ideal S) (β := ℕ) (map (F := R →+* S) f p) 1 =
    HPow.hPow (α := Ideal S) (β := ℕ) (map (F := R →+* S) f p) 2
this : Eq (α := ℕ) 1 2
⊢ False

Tactic:
simp_all
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
T : Type u_2
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
Q : Ideal T
hp : p = comap (F := R →+* S) f P
h : ¬Eq (α := ℕ) (sSup {n : ℕ | map (F := R →+* T) (algebraMap R T) p ≤ Q ^ n}) 0
⊢ LE.le (α := ℕ) (sSup {n : ℕ | map (F := S →+* T) (algebraMap S T) P ≤ Q ^ n})
    (sSup {n : ℕ | map (F := R →+* T) (algebraMap R T) p ≤ Q ^ n})

Tactic:
csSup_le_csSup' (h.imp_symm Nat.sSup_of_not_bddAbove) fun n hn ↦ ?_

Premises used: Nat.sSup_of_not_bddAbove, csSup_le_csSup', Not.imp_symm
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
T : Type u_2
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
Q : Ideal T
hp : p = comap (F := R →+* S) f P
h : ¬Eq (α := ℕ) (sSup {n : ℕ | map (F := R →+* T) (algebraMap R T) p ≤ Q ^ n}) 0
refine :
  ∀ (n : ℕ) (hn : Membership.mem (γ := Set ℕ) {n : ℕ | map (F := S →+* T) (algebraMap S T) P ≤ Q ^ n} n),
    Membership.mem (γ := Set ℕ) {n : ℕ | map (F := R →+* T) (algebraMap R T) p ≤ Q ^ n} n
⊢ LE.le (α := ℕ) (sSup {n : ℕ | map (F := S →+* T) (algebraMap S T) P ≤ Q ^ n})
    (sSup {n : ℕ | map (F := R →+* T) (algebraMap R T) p ≤ Q ^ n})

Tactic:
refine csSup_le_csSup' (h.imp_symm Nat.sSup_of_not_bddAbove) fun n hn ↦ ?_

Premises used: Nat.sSup_of_not_bddAbove, csSup_le_csSup', Not.imp_symm
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
T : Type u_2
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
Q : Ideal T
hp : p = comap (F := R →+* S) f P
h : ¬Eq (α := ℕ) (sSup {n : ℕ | map (F := R →+* T) (algebraMap R T) p ≤ Q ^ n}) 0
n : ℕ
hn : Membership.mem (γ := Set ℕ) {n : ℕ | map (F := S →+* T) (algebraMap S T) P ≤ Q ^ n} n
simp_rw :
  Membership.mem (γ := Set ℕ)
    {n : ℕ |
      LE.le (α := Ideal R) (comap (F := R →+* S) f P)
        (comap (F := R →+* S) f (comap (F := S →+* T) (algebraMap S T) (Q ^ n)))}
    n
⊢ Membership.mem (γ := Set ℕ) {n : ℕ | map (F := R →+* T) (algebraMap R T) p ≤ Q ^ n} n

Tactic:
simp_rw [hp, IsScalarTower.algebraMap_eq R S T, ← map_map, map_le_iff_le_comap]

Premises used: Ideal.map_le_iff_le_comap, Ideal.map_map, IsScalarTower.algebraMap_eq
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
T : Type u_2
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
Q : Ideal T
hp : p = comap (F := R →+* S) f P
h : ¬Eq (α := ℕ) (sSup {n : ℕ | map (F := R →+* T) (algebraMap R T) p ≤ Q ^ n}) 0
n : ℕ
hn : Membership.mem (γ := Set ℕ) {n : ℕ | map (F := S →+* T) (algebraMap S T) P ≤ Q ^ n} n
rwa rwa₁ rwa₂ rwa₃ : map (F := S →+* T) (algebraMap S T) P ≤ Q ^ n
⊢ P ≤ comap (F := S →+* T) (algebraMap S T) (Q ^ n)

Tactic:
rwa [← map_le_iff_le_comap]

Premises used: Ideal.map_le_iff_le_comap
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
T : Type u_2
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
Q : Ideal T
hp : p = comap (F := R →+* S) f P
h : ¬Eq (α := ℕ) (sSup {n : ℕ | map (F := R →+* T) (algebraMap R T) p ≤ Q ^ n}) 0
n : ℕ
hn : Membership.mem (γ := Set ℕ) {n : ℕ | map (F := S →+* T) (algebraMap S T) P ≤ Q ^ n} n
⊢ Membership.mem (γ := Set ℕ)
    {n : ℕ |
      LE.le (α := Ideal R) (comap (F := R →+* S) f P)
        (comap (F := R →+* S) f (comap (F := S →+* T) (algebraMap S T) (Q ^ n)))}
    n

Tactic:
exact comap_mono <| by rwa [← map_le_iff_le_comap]

Premises used: Ideal.comap_mono
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
inst_3 : IsDedekindDomain S
hp0 : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
hP : P.IsPrime
hP0 : P ≠ ⊥
⊢ Irreducible P

Tactic:
have hPirr := (Ideal.prime_of_isPrime hP0 hP).irreducible
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
inst_3 : IsDedekindDomain S
hp0 : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
hP : P.IsPrime
hP0 : P ≠ ⊥
hPirr : Irreducible P
⊢ p.ramificationIdx P = Multiset.count P (normalizedFactors (map (F := R →+* S) f p))

Tactic:
ramificationIdx_spec (Ideal.le_of_dvd ?_) (mt Ideal.dvd_iff_le.mpr ?_)

Premises used: Iff.mpr, Ideal.dvd_iff_le, Ideal.le_of_dvd, mt, Ideal.ramificationIdx_spec
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
inst_3 : IsDedekindDomain S
hp0 : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
hP : P.IsPrime
hP0 : P ≠ ⊥
hPirr : Irreducible P
refine_1 : P ^ Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) ∣ map (F := R →+* S) f p
refine_2 : ¬P ^ (Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) + 1) ∣ map (F := R →+* S) f p
⊢ p.ramificationIdx P = Multiset.count P (normalizedFactors (map (F := R →+* S) f p))

Tactic:
refine ramificationIdx_spec (Ideal.le_of_dvd ?_) (mt Ideal.dvd_iff_le.mpr ?_)

Premises used: Iff.mpr, Ideal.dvd_iff_le, Ideal.le_of_dvd, mt, Ideal.ramificationIdx_spec
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
inst_3 : IsDedekindDomain S
hp0 : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
hP : P.IsPrime
hP0 : P ≠ ⊥
hPirr : Irreducible P
refine_1 :
  normalizedFactors (P ^ Multiset.count P (normalizedFactors (map (F := R →+* S) f p))) ≤
    normalizedFactors (map (F := R →+* S) f p)
refine_1₁ :
  Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) • normalizedFactors P ≤
    normalizedFactors (map (F := R →+* S) f p)
refine_1₂ :
  HSMul.hSMul (β := Multiset (Ideal S)) (Multiset.count P (normalizedFactors (map (F := R →+* S) f p)))
      (singleton (α := Ideal S) ((normalize : (a : Ideal S) → Ideal S) P : Ideal S)) ≤
    normalizedFactors (map (F := R →+* S) f p)
refine_1₃ :
  HSMul.hSMul (β := Multiset (Ideal S)) (Multiset.count P (normalizedFactors (map (F := R →+* S) f p))) {P} ≤
    normalizedFactors (map (F := R →+* S) f p)
refine_1₄ :
  Multiset.replicate (Multiset.count P (normalizedFactors (map (F := R →+* S) f p))) P ≤
    normalizedFactors (map (F := R →+* S) f p)
refine_1₅ refine_1₆ :
  Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) ≤
    Multiset.count P (normalizedFactors (map (F := R →+* S) f p))
⊢ P ^ Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) ∣ map (F := R →+* S) f p

Tactic:
rw [dvd_iff_normalizedFactors_le_normalizedFactors (pow_ne_zero _ hP0) hp0,
      normalizedFactors_pow, normalizedFactors_irreducible hPirr, normalize_eq,
      Multiset.nsmul_singleton, ← Multiset.le_count_iff_replicate_le]

Premises used: pow_ne_zero, UniqueFactorizationMonoid.normalizedFactors_irreducible, UniqueFactorizationMonoid.normalizedFactors_pow, Multiset.nsmul_singleton, Multiset.le_count_iff_replicate_le, UniqueFactorizationMonoid.dvd_iff_normalizedFactors_le_normalizedFactors, normalize_eq
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
inst_3 : IsDedekindDomain S
hp0 : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
hP : P.IsPrime
hP0 : P ≠ ⊥
hPirr : Irreducible P
refine_2 :
  ¬Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) + 1 ≤
      Multiset.count P (normalizedFactors (map (F := R →+* S) f p))
⊢ ¬P ^ (Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) + 1) ∣ map (F := R →+* S) f p

Tactic:
rw [dvd_iff_normalizedFactors_le_normalizedFactors (pow_ne_zero _ hP0) hp0,
      normalizedFactors_pow, normalizedFactors_irreducible hPirr, normalize_eq,
      Multiset.nsmul_singleton, ← Multiset.le_count_iff_replicate_le]

Premises used: pow_ne_zero, UniqueFactorizationMonoid.normalizedFactors_irreducible, UniqueFactorizationMonoid.normalizedFactors_pow, Multiset.nsmul_singleton, Multiset.le_count_iff_replicate_le, UniqueFactorizationMonoid.dvd_iff_normalizedFactors_le_normalizedFactors, normalize_eq
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
inst_3 : IsDedekindDomain S
hp0 : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
hP : P.IsPrime
hP0 : P ≠ ⊥
hPirr : Irreducible P
⊢ ¬Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) + 1 ≤
      Multiset.count P (normalizedFactors (map (F := R →+* S) f p))

Tactic:
(Nat.lt_succ_self _).not_ge

Premises used: Nat.lt_succ_self, LT.lt.not_ge
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
inst_3 : IsDedekindDomain S
hp0 : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
hP : P.IsPrime
hP0 : P ≠ ⊥
hPirr : Irreducible P
⊢ ¬Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) + 1 ≤
      Multiset.count P (normalizedFactors (map (F := R →+* S) f p))

Tactic:
exact (Nat.lt_succ_self _).not_ge

Premises used: Nat.lt_succ_self, LT.lt.not_ge
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
inst_3 : IsDedekindDomain S
hp : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
hP : P.IsPrime
pos : ∀ (hP₂ : P = ⊥), p.ramificationIdx P = multiplicity P (map (F := R →+* S) f p)
neg : ∀ (hP₂ : ¬P = ⊥), p.ramificationIdx P = multiplicity P (map (F := R →+* S) f p)
⊢ p.ramificationIdx P = multiplicity P (map (F := R →+* S) f p)

Tactic:
by_cases hP₂ : P = ⊥
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
inst_3 : IsDedekindDomain S
hp : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
hP : P.IsPrime
hP₂ : P = ⊥
pos : ramificationIdx.{u, v} (S := S) p 0 = 0
⊢ p.ramificationIdx P = multiplicity P (map (F := R →+* S) f p)

Tactic:
rw [hP₂, ← Ideal.zero_eq_bot, multiplicity_zero_eq_zero_of_ne_zero _ hp]

Premises used: Ideal.zero_eq_bot, multiplicity_zero_eq_zero_of_ne_zero
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
inst_3 : IsDedekindDomain S
hp : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
hP : P.IsPrime
hP₂ : P = ⊥
⊢ ramificationIdx.{u, v} (S := S) p 0 = 0

Tactic:
Ideal.ramificationIdx_of_not_le (mt le_bot_iff.mp hp)

Premises used: le_bot_iff, mt, Ideal.ramificationIdx_of_not_le, Iff.mp
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
inst_3 : IsDedekindDomain S
hp : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
hP : P.IsPrime
hP₂ : P = ⊥
⊢ ramificationIdx.{u, v} (S := S) p 0 = 0

Tactic:
exact Ideal.ramificationIdx_of_not_le (mt le_bot_iff.mp hp)

Premises used: le_bot_iff, mt, Ideal.ramificationIdx_of_not_le, Iff.mp
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
inst_3 : IsDedekindDomain S
hp : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
hP : P.IsPrime
hP₂ : ¬P = ⊥
neg : emultiplicity P (map (F := R →+* S) f p) = (↑(p.ramificationIdx P) : ℕ∞)
⊢ p.ramificationIdx P = multiplicity P (map (F := R →+* S) f p)

Tactic:
rw [multiplicity_eq_of_emultiplicity_eq_some]

Premises used: multiplicity_eq_of_emultiplicity_eq_some
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
inst_3 : IsDedekindDomain S
hp : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
hP : P.IsPrime
hP₂ : ¬P = ⊥
rw : Irreducible P
⊢ emultiplicity P (map (F := R →+* S) f p) = (↑(p.ramificationIdx P) : ℕ∞)

Tactic:
rw [ramificationIdx_eq_normalizedFactors_count hp hP hP₂, ← normalize_eq P,
    ← UniqueFactorizationMonoid.emultiplicity_eq_count_normalizedFactors _ hp, normalize_eq]

Premises used: Ideal.IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count, UniqueFactorizationMonoid.emultiplicity_eq_count_normalizedFactors, normalize_eq
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
inst_3 : IsDedekindDomain S
hp : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
hP : P.IsPrime
hP₂ : ¬P = ⊥
⊢ Irreducible P

Tactic:
irreducible_iff_prime.mpr <| prime_of_isPrime hP₂ hP

Premises used: Iff.mpr, irreducible_iff_prime, Ideal.prime_of_isPrime
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
inst_3 : IsDedekindDomain S
hp : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
hP : P.IsPrime
hP₂ : ¬P = ⊥
⊢ Irreducible P

Tactic:
exact irreducible_iff_prime.mpr <| prime_of_isPrime hP₂ hP

Premises used: Iff.mpr, irreducible_iff_prime, Ideal.prime_of_isPrime
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
inst_3 : IsDedekindDomain S
hp : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
hP : P.IsPrime
pos : ∀ (hP₂ : P = ⊥), p.ramificationIdx P = multiplicity P (map (F := R →+* S) f p)
neg neg₁ : ∀ (hP₂ : ¬P = ⊥), p.ramificationIdx P = multiplicity P (map (F := R →+* S) f p)
neg₂ : ∀ (hP₂ : ¬P = ⊥), emultiplicity P (map (F := R →+* S) f p) = (↑(p.ramificationIdx P) : ℕ∞)
by_cases : ∀ (hP₂ : ¬P = ⊥), Irreducible P
⊢ p.ramificationIdx P = multiplicity P (map (F := R →+* S) f p)

Tactic:
classical
  by_cases hP₂ : P = ⊥
  · rw [hP₂, ← Ideal.zero_eq_bot, multiplicity_zero_eq_zero_of_ne_zero _ hp]
    exact Ideal.ramificationIdx_of_not_le (mt le_bot_iff.mp hp)
  rw [multiplicity_eq_of_emultiplicity_eq_some]
  rw [ramificationIdx_eq_normalizedFactors_count hp hP hP₂, ← normalize_eq P,
    ← UniqueFactorizationMonoid.emultiplicity_eq_count_normalizedFactors _ hp, normalize_eq]
  exact irreducible_iff_prime.mpr <| prime_of_isPrime hP₂ hP

Premises used: le_bot_iff, Iff.mpr, mt, Ideal.zero_eq_bot, Ideal.ramificationIdx_of_not_le, UniqueFactorizationMonoid.emultiplicity_eq_count_normalizedFactors, multiplicity_zero_eq_zero_of_ne_zero, Iff.mp, irreducible_iff_prime, normalize_eq, multiplicity_eq_of_emultiplicity_eq_some
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
inst_3 : IsDedekindDomain S
hp0 : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
hP : P.IsPrime
hP0 : P ≠ ⊥
rw : Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) = Multiset.count P (factors (map (F := R →+* S) f p))
rw₁ rw₂ :
  Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) =
    Multiset.count P (normalizedFactors (map (F := R →+* S) f p))
⊢ p.ramificationIdx P = Multiset.count P (factors (map (F := R →+* S) f p))

Tactic:
rw [IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count hp0 hP hP0,
    factors_eq_normalizedFactors]

Premises used: UniqueFactorizationMonoid.factors_eq_normalizedFactors, Ideal.IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : IsDedekindDomain S
hp0 : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
hP : IsPrime.{v} (α := S) ⊥
le : LE.le.{v} (α := Ideal S) (map (F := R →+* S) f p) ⊥
⊢ False

Tactic:
hp0 (le_bot_iff.mp le)

Premises used: le_bot_iff, Iff.mp
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : IsDedekindDomain S
hp0 : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
hP : IsPrime.{v} (α := S) ⊥
le : LE.le.{v} (α := Ideal S) (map (F := R →+* S) f p) ⊥
⊢ False

Tactic:
exact hp0 (le_bot_iff.mp le)

Premises used: le_bot_iff, Iff.mp
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
inst_3 : IsDedekindDomain S
hp0 : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
hP : P.IsPrime
le : map (F := R →+* S) f p ≤ P
⊢ P ≠ ⊥

Tactic:
have hP0 : P ≠ ⊥ := by
    rintro rfl
    exact hp0 (le_bot_iff.mp le)
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
inst_3 : IsDedekindDomain S
hp0 : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
hP : P.IsPrime
le : map (F := R →+* S) f p ≤ P
hP0 : P ≠ ⊥
⊢ Irreducible P

Tactic:
have hPirr := (Ideal.prime_of_isPrime hP0 hP).irreducible
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
inst_3 : IsDedekindDomain S
hp0 : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
hP : P.IsPrime
le : map (F := R →+* S) f p ≤ P
hP0 : P ≠ ⊥
hPirr : Irreducible P
rw : Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) ≠ 0
⊢ p.ramificationIdx P ≠ 0

Tactic:
rw [IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count hp0 hP hP0]

Premises used: Ideal.IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
inst_3 : IsDedekindDomain S
hp0 : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
hP : P.IsPrime
le : map (F := R →+* S) f p ≤ P
hP0 : P ≠ ⊥
hPirr : Irreducible P
obtain :
  ∀ (P' : Ideal S) (hP' : Membership.mem (γ := Multiset (Ideal S)) (normalizedFactors (map (F := R →+* S) f p)) P')
    (P'_eq : Associated P P'), Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) ≠ 0
⊢ Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) ≠ 0

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

Premises used: Iff.mpr, Ideal.dvd_iff_le, UniqueFactorizationMonoid.exists_mem_normalizedFactors_of_dvd
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
inst_3 : IsDedekindDomain S
hp0 : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
hP : P.IsPrime
le : map (F := R →+* S) f p ≤ P
hP0 : P ≠ ⊥
hPirr : Irreducible P
P' : Ideal S
hP' : Membership.mem (γ := Multiset (Ideal S)) (normalizedFactors (map (F := R →+* S) f p)) P'
P'_eq : Associated P P'
rwa : Membership.mem (γ := Multiset (Ideal S)) (normalizedFactors (map (F := R →+* S) f p)) P
rwa₁ rwa₂ rwa₃ rwa₄ : Membership.mem (γ := Multiset (Ideal S)) (normalizedFactors (map (F := R →+* S) f p)) P'
⊢ Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) ≠ 0

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

Premises used: Multiset.count_ne_zero, associated_iff_eq, Iff.mp
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
inst_3 : IsDedekindDomain S
hp0 : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
hP : P.IsPrime
le : map (F := R →+* S) f p ≤ P
have : P ≠ ⊥
have₁ : ∀ (hP0 : P ≠ ⊥), p.ramificationIdx P ≠ 0
have₂ : P ≠ ⊥
have₃ have₄ : ∀ (hP0 : P ≠ ⊥), p.ramificationIdx P ≠ 0
have₅ : ∀ (hP0 : P ≠ ⊥) (hPirr : Irreducible P), p.ramificationIdx P ≠ 0
have₆ : ∀ (hP0 : P ≠ ⊥) (hPirr : Irreducible P), Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) ≠ 0
have₇ :
  ∀ (hP0 : P ≠ ⊥) (hPirr : Irreducible P) (P' : Ideal S)
    (hP' : Membership.mem (γ := Multiset (Ideal S)) (normalizedFactors (map (F := R →+* S) f p)) P')
    (P'_eq : Associated P P'), Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) ≠ 0
⊢ p.ramificationIdx 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]

Premises used: Multiset.count_ne_zero
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDedekindDomain S
inst_4 : IsDomain R
inst_5 : IsTorsionFree R S
P : Ideal S
hP : P.IsPrime
p : Ideal R
hp : p ≠ ⊥
hPp : P.LiesOver p
⊢ p.ramificationIdx P ≠ 0

Tactic:
IsDedekindDomain.ramificationIdx_ne_zero (map_ne_bot_of_ne_bot hp) hP <|
    map_le_iff_le_comap.mpr <| le_of_eq <| (liesOver_iff _ _).mp hPp

Premises used: Iff.mpr, Ideal.liesOver_iff, Ideal.map_le_iff_le_comap, Ideal.IsDedekindDomain.ramificationIdx_ne_zero, Iff.mp, Ideal.map_ne_bot_of_ne_bot, le_of_eq
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDedekindDomain S
p : Ideal R
P : Ideal S
inst_4 : P.IsPrime
hp : P ≠ ⊥
hpP : map (F := R →+* S) f p ≤ P
⊢ p.ramificationIdx P = 1 ↔
    Eq.{v + 1} (α := Ideal (Localization.AtPrime P))
      (map (F := RingHom.{u, v} R (Localization.AtPrime P)) (algebraMap R (Localization.AtPrime P)) p)
      (maximalIdeal (Localization.AtPrime P))

Tactic:
⟨?_, ramificationIdx_eq_one_of_map_localization hpP hp (primeCompl_le_nonZeroDivisors _)⟩

Premises used: Ideal.ramificationIdx_eq_one_of_map_localization, Iff.intro, Ideal.primeCompl_le_nonZeroDivisors