awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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
⊢ p.ramificationIdx P = Multiset.count P (normalizedFactors (map (F := R →+* S) f p))
have refine_2 : ¬P ^ (Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) + 1) ∣ map (F := R →+* S) f p
Tactic: refine ramificationIdx_spec (Ideal.le_of_dvd ?_) (mt Ideal.dvd_iff_le.mpr ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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 ^ Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) ∣ map (F := R →+* S) f p
have refine_1 : normalizedFactors (P ^ Multiset.count P (normalizedFactors (map (F := R →+* S) f p))) ≤
  normalizedFactors (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]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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)
⊢ P ^ Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) ∣ map (F := R →+* S) f p
have refine_1₁ : Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) • normalizedFactors P ≤
  normalizedFactors (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]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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)
⊢ P ^ Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) ∣ map (F := R →+* S) f p
have 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)
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]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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)
⊢ P ^ Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) ∣ map (F := R →+* S) f p
have 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)
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]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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)
⊢ P ^ Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) ∣ map (F := R →+* S) f p
have refine_1₄ : Multiset.replicate (Multiset.count P (normalizedFactors (map (F := R →+* S) f p))) P ≤
  normalizedFactors (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]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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)
⊢ P ^ Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) ∣ map (F := R →+* S) f p
have refine_1₅ : Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) ≤
  Multiset.count P (normalizedFactors (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]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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 ^ (Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) + 1) ∣ map (F := R →+* S) f p
have refine_2 : ¬Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) + 1 ≤
    Multiset.count P (normalizedFactors (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]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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
⊢ p.ramificationIdx P = multiplicity P (map (F := R →+* S) f p)
have pos : ∀ (hP₂ : P = ⊥), p.ramificationIdx P = multiplicity P (map (F := R →+* S) f p)
Tactic: by_cases hP₂ : P = ⊥
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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)
⊢ p.ramificationIdx P = multiplicity P (map (F := R →+* S) f p)
have neg : ∀ (hP₂ : ¬P = ⊥), p.ramificationIdx P = multiplicity P (map (F := R →+* S) f p)
Tactic: by_cases hP₂ : P = ⊥
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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 = ⊥
⊢ p.ramificationIdx P = multiplicity P (map (F := R →+* S) f p)
have pos : ramificationIdx.{u, v} (S := S) p 0 = 0
Tactic: rw [hP₂, ← Ideal.zero_eq_bot, multiplicity_zero_eq_zero_of_ne_zero _ hp]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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 = ⊥
⊢ p.ramificationIdx P = multiplicity P (map (F := R →+* S) f p)
have neg : emultiplicity P (map (F := R →+* S) f p) = (↑(p.ramificationIdx P) : ℕ∞)
Tactic: rw [multiplicity_eq_of_emultiplicity_eq_some]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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 = ⊥
⊢ emultiplicity P (map (F := R →+* S) f p) = (↑(p.ramificationIdx P) : ℕ∞)
have rw : Irreducible P
Tactic: rw [ramificationIdx_eq_normalizedFactors_count hp hP hP₂, ← normalize_eq P,
    ← UniqueFactorizationMonoid.emultiplicity_eq_count_normalizedFactors _ hp, normalize_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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
⊢ p.ramificationIdx P = multiplicity P (map (F := R →+* S) f p)
have pos : ∀ (hP₂ : 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
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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)
⊢ p.ramificationIdx P = multiplicity P (map (F := R →+* S) f p)
have neg : ∀ (hP₂ : ¬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
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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)
⊢ p.ramificationIdx P = multiplicity P (map (F := R →+* S) f p)
have neg₂ : ∀ (hP₂ : ¬P = ⊥), emultiplicity P (map (F := R →+* S) f p) = (↑(p.ramificationIdx 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
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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) : ℕ∞)
⊢ p.ramificationIdx P = multiplicity P (map (F := R →+* S) f p)
have by_cases : ∀ (hP₂ : ¬P = ⊥), Irreducible 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
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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 ≠ ⊥
⊢ p.ramificationIdx P = Multiset.count P (factors (map (F := R →+* S) f p))
have rw : Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) = Multiset.count P (factors (map (F := R →+* S) f p))
Tactic: rw [IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count hp0 hP hP0,
    factors_eq_normalizedFactors]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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))
⊢ p.ramificationIdx P = Multiset.count P (factors (map (F := R →+* S) f p))
have rw₁ : Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) =
  Multiset.count P (normalizedFactors (map (F := R →+* S) f p))
Tactic: rw [IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count hp0 hP hP0,
    factors_eq_normalizedFactors]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (hypothesis)
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.ramificationIdx P ≠ 0
have hP0 : P ≠ ⊥
Tactic: have hP0 : P ≠ ⊥ := by
    rintro rfl
    exact hp0 (le_bot_iff.mp le)
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (hypothesis)
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 ≠ ⊥
⊢ p.ramificationIdx P ≠ 0
have hPirr : Irreducible P
Tactic: have hPirr := (Ideal.prime_of_isPrime hP0 hP).irreducible
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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.ramificationIdx P ≠ 0
have rw : Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) ≠ 0
Tactic: rw [IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count hp0 hP hP0]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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
⊢ Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) ≠ 0
have 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
Tactic: obtain ⟨P', hP', P'_eq⟩ :=
    exists_mem_normalizedFactors_of_dvd hp0 hPirr (Ideal.dvd_iff_le.mpr le)
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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'
⊢ Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) ≠ 0
have rwa : Membership.mem (γ := Multiset (Ideal S)) (normalizedFactors (map (F := R →+* S) f p)) P
Tactic: rwa [Multiset.count_ne_zero, associated_iff_eq.mp P'_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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.ramificationIdx P ≠ 0
have have : P ≠ ⊥
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]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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 ≠ ⊥
⊢ p.ramificationIdx P ≠ 0
have have₁ : ∀ (hP0 : P ≠ ⊥), 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]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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
⊢ p.ramificationIdx P ≠ 0
have have₅ : ∀ (hP0 : P ≠ ⊥) (hPirr : Irreducible P), 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]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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
⊢ p.ramificationIdx P ≠ 0
have have₆ : ∀ (hP0 : P ≠ ⊥) (hPirr : Irreducible P), Multiset.count P (normalizedFactors (map (F := R →+* S) f 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]