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
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
⊢ p.ramificationIdx P ≠ 0
have 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
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
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))
have refine : 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: refine ⟨?_, ramificationIdx_eq_one_of_map_localization hpP hp (primeCompl_le_nonZeroDivisors _)⟩
-- 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
inst_3 : IsDedekindDomain S
p : Ideal R
P : Ideal S
inst_4 : P.IsPrime
hp : P ≠ ⊥
hpP : map (F := R →+* S) f p ≤ P
Sₚ : Type v := Localization.AtPrime 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))
have rw : ¬map (F := R →+* S) f p ≤ P * P →
  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: rw [← not_ne_iff (b := 1), ramificationIdx_ne_one_iff hpP, pow_two]
-- 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
inst_3 : IsDedekindDomain S
p : Ideal R
P : Ideal S
inst_4 : P.IsPrime
hp : P ≠ ⊥
hpP : map (F := R →+* S) f p ≤ P
Sₚ : Type v := Localization.AtPrime P
H₁ : ¬map (F := R →+* S) f p ≤ P * P
⊢ 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))
have obtain : ∀ (a : Ideal S) (ha : map (F := R →+* S) f p = P * a),
  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: obtain ⟨a, ha⟩ : P ∣ p.map (algebraMap R S) := Ideal.dvd_iff_le.mpr hpP
-- 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
inst_3 : IsDedekindDomain S
p : Ideal R
P : Ideal S
inst_4 : P.IsPrime
hp : P ≠ ⊥
hpP : map (F := R →+* S) f p ≤ P
Sₚ : Type v := Localization.AtPrime P
H₁ : ¬map (F := R →+* S) f p ≤ P * P
a : Ideal S
ha : map (F := R →+* S) f p = P * a
⊢ 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))
have ha' : ¬a ≤ P
Tactic: have ha' : ¬ a ≤ P := fun h ↦ H₁ (ha.trans_le (Ideal.mul_mono_right h))
-- 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
inst_3 : IsDedekindDomain S
p : Ideal R
P : Ideal S
inst_4 : P.IsPrime
hp : P ≠ ⊥
hpP : map (F := R →+* S) f p ≤ P
Sₚ : Type v := Localization.AtPrime P
H₁ : ¬map (F := R →+* S) f p ≤ P * P
a : Ideal S
ha : map (F := R →+* S) f p = P * a
ha' : ¬a ≤ P
⊢ 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))
have rw : HMul.hMul (α := Ideal (Localization.AtPrime P)) (maximalIdeal (Localization (M := S) P.primeCompl))
    (map (F := S →+* Localization.AtPrime P) (algebraMap S (Localization.AtPrime P)) a) =
  maximalIdeal (Localization.AtPrime P)
Tactic: rw [IsScalarTower.algebraMap_eq _ S, ← Ideal.map_map, ha, Ideal.map_mul,
    Localization.AtPrime.map_eq_maximalIdeal]
-- 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
inst_3 : IsDedekindDomain S
p : Ideal R
P : Ideal S
inst_4 : P.IsPrime
hp : P ≠ ⊥
hpP : map (F := R →+* S) f p ≤ P
Sₚ : Type v := Localization.AtPrime P
H₁ : ¬map (F := R →+* S) f p ≤ P * P
a : Ideal S
ha : map (F := R →+* S) f p = P * a
ha' : ¬a ≤ P
⊢ HMul.hMul (α := Ideal (Localization.AtPrime P)) (maximalIdeal (Localization (M := S) P.primeCompl))
      (map (F := S →+* Localization.AtPrime P) (algebraMap S (Localization.AtPrime P)) a) =
    maximalIdeal (Localization.AtPrime P)
have h : Eq (α := Ideal (Localization.AtPrime P))
  (map (F := S →+* Localization.AtPrime P) (algebraMap S (Localization.AtPrime P)) a) ⊤
Tactic: convert! Ideal.mul_top _
-- 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
inst_3 : IsDedekindDomain S
p : Ideal R
P : Ideal S
inst_4 : P.IsPrime
hp : P ≠ ⊥
hpP : map (F := R →+* S) f p ≤ P
Sₚ : Type v := Localization.AtPrime P
H₁ : ¬map (F := R →+* S) f p ≤ P * P
a : Ideal S
ha : map (F := R →+* S) f p = P * a
ha' : ¬a ≤ P
h :
  Eq (α := Ideal (Localization.AtPrime P))
    (map (F := S →+* Localization.AtPrime P) (algebraMap S (Localization.AtPrime P)) a) ⊤
⊢ HMul.hMul (α := Ideal (Localization.AtPrime P)) (maximalIdeal (Localization (M := S) P.primeCompl))
      (map (F := S →+* Localization.AtPrime P) (algebraMap S (Localization.AtPrime P)) a) =
    maximalIdeal (Localization.AtPrime P)
have convert_4 : IsTwoSided.{v} (α := Localization.AtPrime P) (maximalIdeal (Localization (M := S) P.primeCompl))
Tactic: convert! Ideal.mul_top _
-- 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
inst_3 : IsDedekindDomain S
p : Ideal R
P : Ideal S
inst_4 : P.IsPrime
hp : P ≠ ⊥
hpP : map (F := R →+* S) f p ≤ P
Sₚ : Type v := Localization.AtPrime P
H₁ : ¬map (F := R →+* S) f p ≤ P * P
a : Ideal S
ha : map (F := R →+* S) f p = P * a
ha' : ¬a ≤ P
⊢ Eq (α := Ideal (Localization.AtPrime P))
    (map (F := S →+* Localization.AtPrime P) (algebraMap S (Localization.AtPrime P)) a) ⊤
have h : ¬Disjoint (↑P.primeCompl : Set S) (↑a : Set S)
Tactic: rw [← not_ne_iff, IsLocalization.map_algebraMap_ne_top_iff_disjoint P.primeCompl]
-- 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
inst_3 : IsDedekindDomain S
inst_4 : IsDedekindDomain R
v : Ideal R
w : Ideal S
p : Ideal R
hv : Irreducible v
hp : Prime p
hvp : v ≠ p
inst_5 : w.LiesOver v
⊢ emultiplicity w (map (F := R →+* S) f p) = 0
have refine : ∀ (h : w ∣ map (F := R →+* S) f p), p = v
Tactic: refine emultiplicity_eq_zero.2 fun h ↦ hvp.symm ?_
-- 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
inst_3 : IsDedekindDomain S
inst_4 : IsDedekindDomain R
v : Ideal R
w : Ideal S
p : Ideal R
hv : Irreducible v
hp : Prime p
hvp : v ≠ p
inst_5 : w.LiesOver v
h : w ∣ map (F := R →+* S) f p
⊢ p = v
have h₁ : p ≤ v
Tactic: rw [Ideal.dvd_iff_le, Ideal.map_le_iff_le_comap, ← under_def, ← Ideal.over_def w v] at h
Cleared hypotheses: h
-- 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
inst_3 : IsDedekindDomain S
inst_4 : IsDedekindDomain R
inst_5 : FaithfulSMul R S
v : Ideal R
w : Ideal S
p : Ideal R
hv : Irreducible v
hp : Prime p
hw : Irreducible w
hw_bot : w ≠ ⊥
inst_6 : w.LiesOver v
⊢ emultiplicity w (map (F := R →+* S) f p) = (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v p
have hp_bot : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
Tactic: have hp_bot : p.map (algebraMap R S) ≠ ⊥ := map_ne_bot_of_ne_bot hp.ne_zero
-- 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
inst_3 : IsDedekindDomain S
inst_4 : IsDedekindDomain R
inst_5 : FaithfulSMul R S
v : Ideal R
w : Ideal S
p : Ideal R
hv : Irreducible v
hp : Prime p
hw : Irreducible w
hw_bot : w ≠ ⊥
inst_6 : w.LiesOver v
hp_bot : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
⊢ emultiplicity w (map (F := R →+* S) f p) = (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v p
have pos : ∀ (hvp : v = p), emultiplicity w (map (F := R →+* S) f p) = (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v p
Tactic: by_cases hvp : v = 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
inst_3 : IsDedekindDomain S
inst_4 : IsDedekindDomain R
inst_5 : FaithfulSMul R S
v : Ideal R
w : Ideal S
p : Ideal R
hv : Irreducible v
hp : Prime p
hw : Irreducible w
hw_bot : w ≠ ⊥
inst_6 : w.LiesOver v
hp_bot : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
pos : ∀ (hvp : v = p), emultiplicity w (map (F := R →+* S) f p) = (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v p
⊢ emultiplicity w (map (F := R →+* S) f p) = (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v p
have neg : ∀ (hvp : ¬v = p), emultiplicity w (map (F := R →+* S) f p) = (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v p
Tactic: by_cases hvp : v = 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
inst_3 : IsDedekindDomain S
inst_4 : IsDedekindDomain R
inst_5 : FaithfulSMul R S
v : Ideal R
w : Ideal S
p : Ideal R
hv : Irreducible v
hp : Prime p
hw : Irreducible w
hw_bot : w ≠ ⊥
inst_6 : w.LiesOver v
hp_bot : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
hvp : ¬v = p
⊢ emultiplicity w (map (F := R →+* S) f p) = (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v p
have neg : emultiplicity w (map (F := R →+* S) f p) = HMul.hMul (α := ℕ∞) (↑(v.ramificationIdx w) : ℕ∞) 0
Tactic: rw [emultiplicity_eq_zero_of_irreducible_ne hv hp.irreducible hvp, mul_zero,
      emultiplicity_map_eq_zero_of_ne hv hp hvp]
-- 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
inst_3 : IsDedekindDomain S
inst_4 : IsDedekindDomain R
inst_5 : FaithfulSMul R S
v : Ideal R
w : Ideal S
p : Ideal R
hv : Irreducible v
hp : Prime p
hw : Irreducible w
hw_bot : w ≠ ⊥
inst_6 : w.LiesOver v
hp_bot : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
hvp : ¬v = p
neg : emultiplicity w (map (F := R →+* S) f p) = HMul.hMul (α := ℕ∞) (↑(v.ramificationIdx w) : ℕ∞) 0
⊢ emultiplicity w (map (F := R →+* S) f p) = (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v p
have neg₁ : emultiplicity w (map (F := R →+* S) f p) = 0
Tactic: rw [emultiplicity_eq_zero_of_irreducible_ne hv hp.irreducible hvp, mul_zero,
      emultiplicity_map_eq_zero_of_ne hv hp hvp]
-- 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
inst_3 : IsDedekindDomain S
inst_4 : IsDedekindDomain R
inst_5 : FaithfulSMul R S
v : Ideal R
w : Ideal S
p : Ideal R
hv : Irreducible v
hp : Prime p
hw : Irreducible w
hw_bot : w ≠ ⊥
inst_6 : w.LiesOver v
hp_bot : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
hvp : ¬v = p
neg : emultiplicity w (map (F := R →+* S) f p) = HMul.hMul (α := ℕ∞) (↑(v.ramificationIdx w) : ℕ∞) 0
neg₁ : emultiplicity w (map (F := R →+* S) f p) = 0
⊢ emultiplicity w (map (F := R →+* S) f p) = (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v p
have neg₂ : Eq (α := ℕ∞) 0 0
Tactic: rw [emultiplicity_eq_zero_of_irreducible_ne hv hp.irreducible hvp, mul_zero,
      emultiplicity_map_eq_zero_of_ne hv hp hvp]
-- 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
inst_3 : IsDedekindDomain S
inst_4 : IsDedekindDomain R
inst_5 : FaithfulSMul R S
v : Ideal R
w : Ideal S
hv : Irreducible v
hw : Irreducible w
hw_bot : w ≠ ⊥
inst_6 : w.LiesOver v
I : Ideal R
hI : IsUnit I
h : I ≠ ⊥
⊢ emultiplicity w (map (F := R →+* S) f I) = (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v I
have h₂ : ∀ (hI : IsUnit.{u} (M := Ideal R) ⊤) (h : Ne.{u + 1} (α := Ideal R) ⊤ ⊥),
  emultiplicity w (map (R := R) (F := R →+* S) f ⊤) = (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v ⊤
Tactic: obtain rfl : I = ⊤ := by simpa using hI
Cleared hypotheses: I, hI, h
-- 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
inst_3 : IsDedekindDomain S
inst_4 : IsDedekindDomain R
inst_5 : FaithfulSMul R S
v : Ideal R
w : Ideal S
hv : Irreducible v
hw : Irreducible w
hw_bot : w ≠ ⊥
inst_6 : w.LiesOver v
hI : IsUnit.{u} (M := Ideal R) ⊤
h : Ne.{u + 1} (α := Ideal R) ⊤ ⊥
⊢ emultiplicity w (map (R := R) (F := R →+* S) f ⊤) = (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v ⊤
have h₂ : (↑(Multiset.count (α := Ideal S) ((normalize : (a : Ideal S) → Ideal S) w : Ideal S) (0 : Multiset (Ideal S))) : ℕ∞) =
  HMul.hMul (α := ℕ∞) (↑(v.ramificationIdx w) : ℕ∞)
    (↑(Multiset.count (α := Ideal R) ((normalize : (a : Ideal R) → Ideal R) v : Ideal R) (0 : Multiset (Ideal R))) : ℕ∞)
Tactic: simp_rw [Ideal.map_top, emultiplicity_eq_count_normalizedFactors hw top_ne_bot,
      emultiplicity_eq_count_normalizedFactors hv h, ← Ideal.one_eq_top, normalizedFactors_one]
-- 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
inst_3 : IsDedekindDomain S
inst_4 : IsDedekindDomain R
inst_5 : FaithfulSMul R S
v : Ideal R
w : Ideal S
hv : Irreducible v
hw : Irreducible w
hw_bot : w ≠ ⊥
inst_6 : w.LiesOver v
I p : Ideal R
hI : I ≠ 0
hp : Prime p
IH : ∀ (h : I ≠ ⊥), emultiplicity w (map (F := R →+* S) f I) = (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v I
h : p * I ≠ ⊥
⊢ emultiplicity w (map (F := R →+* S) f (p * I)) = (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v (p * I)
have h₃ : emultiplicity w (HMul.hMul (α := Ideal S) (map (F := R →+* S) f p) (map (F := R →+* S) f I)) =
  (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v (p * I)
Tactic: rw [Ideal.map_mul, emultiplicity_mul hw.prime, emultiplicity_mul hv.prime, IH hI, mul_add,
      emultiplicity_map_eq_ramificationIdx_mul_of_prime hv hp hw hw_bot]
-- 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
inst_3 : IsDedekindDomain S
inst_4 : IsDedekindDomain R
inst_5 : FaithfulSMul R S
v : Ideal R
w : Ideal S
hv : Irreducible v
hw : Irreducible w
hw_bot : w ≠ ⊥
inst_6 : w.LiesOver v
I p : Ideal R
hI : I ≠ 0
hp : Prime p
IH : ∀ (h : I ≠ ⊥), emultiplicity w (map (F := R →+* S) f I) = (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v I
h : p * I ≠ ⊥
h₃ :
  emultiplicity w (HMul.hMul (α := Ideal S) (map (F := R →+* S) f p) (map (F := R →+* S) f I)) =
    (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v (p * I)
⊢ emultiplicity w (map (F := R →+* S) f (p * I)) = (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v (p * I)
have h₄ : emultiplicity w (map (F := R →+* S) f p) + emultiplicity w (map (F := R →+* S) f I) =
  (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v (p * I)
Tactic: rw [Ideal.map_mul, emultiplicity_mul hw.prime, emultiplicity_mul hv.prime, IH hI, mul_add,
      emultiplicity_map_eq_ramificationIdx_mul_of_prime hv hp hw hw_bot]
-- 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
inst_3 : IsDedekindDomain S
inst_4 : IsDedekindDomain R
inst_5 : FaithfulSMul R S
v : Ideal R
w : Ideal S
hv : Irreducible v
hw : Irreducible w
hw_bot : w ≠ ⊥
inst_6 : w.LiesOver v
I p : Ideal R
hI : I ≠ 0
hp : Prime p
IH : ∀ (h : I ≠ ⊥), emultiplicity w (map (F := R →+* S) f I) = (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v I
h : p * I ≠ ⊥
h₃ :
  emultiplicity w (HMul.hMul (α := Ideal S) (map (F := R →+* S) f p) (map (F := R →+* S) f I)) =
    (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v (p * I)
h₄ :
  emultiplicity w (map (F := R →+* S) f p) + emultiplicity w (map (F := R →+* S) f I) =
    (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v (p * I)
⊢ emultiplicity w (map (F := R →+* S) f (p * I)) = (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v (p * I)
have h₅ : emultiplicity w (map (F := R →+* S) f p) + emultiplicity w (map (F := R →+* S) f I) =
  (↑(v.ramificationIdx w) : ℕ∞) * (emultiplicity v p + emultiplicity v I)
Tactic: rw [Ideal.map_mul, emultiplicity_mul hw.prime, emultiplicity_mul hv.prime, IH hI, mul_add,
      emultiplicity_map_eq_ramificationIdx_mul_of_prime hv hp hw hw_bot]
-- 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
inst_3 : IsDedekindDomain S
inst_4 : IsDedekindDomain R
inst_5 : FaithfulSMul R S
v : Ideal R
w : Ideal S
hv : Irreducible v
hw : Irreducible w
hw_bot : w ≠ ⊥
inst_6 : w.LiesOver v
I p : Ideal R
hI : I ≠ 0
hp : Prime p
IH : ∀ (h : I ≠ ⊥), emultiplicity w (map (F := R →+* S) f I) = (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v I
h : p * I ≠ ⊥
h₃ :
  emultiplicity w (HMul.hMul (α := Ideal S) (map (F := R →+* S) f p) (map (F := R →+* S) f I)) =
    (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v (p * I)
h₄ :
  emultiplicity w (map (F := R →+* S) f p) + emultiplicity w (map (F := R →+* S) f I) =
    (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v (p * I)
h₅ :
  emultiplicity w (map (F := R →+* S) f p) + emultiplicity w (map (F := R →+* S) f I) =
    (↑(v.ramificationIdx w) : ℕ∞) * (emultiplicity v p + emultiplicity v I)
⊢ emultiplicity w (map (F := R →+* S) f (p * I)) = (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v (p * I)
have h₆ : emultiplicity w (map (F := R →+* S) f p) + (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v I =
  (↑(v.ramificationIdx w) : ℕ∞) * (emultiplicity v p + emultiplicity v I)
Tactic: rw [Ideal.map_mul, emultiplicity_mul hw.prime, emultiplicity_mul hv.prime, IH hI, mul_add,
      emultiplicity_map_eq_ramificationIdx_mul_of_prime hv hp hw hw_bot]
-- 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
inst_3 : IsDedekindDomain S
inst_4 : IsDedekindDomain R
inst_5 : FaithfulSMul R S
v : Ideal R
w : Ideal S
hv : Irreducible v
hw : Irreducible w
hw_bot : w ≠ ⊥
inst_6 : w.LiesOver v
I p : Ideal R
hI : I ≠ 0
hp : Prime p
IH : ∀ (h : I ≠ ⊥), emultiplicity w (map (F := R →+* S) f I) = (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v I
h : p * I ≠ ⊥
h₃ :
  emultiplicity w (HMul.hMul (α := Ideal S) (map (F := R →+* S) f p) (map (F := R →+* S) f I)) =
    (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v (p * I)
h₄ :
  emultiplicity w (map (F := R →+* S) f p) + emultiplicity w (map (F := R →+* S) f I) =
    (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v (p * I)
h₅ :
  emultiplicity w (map (F := R →+* S) f p) + emultiplicity w (map (F := R →+* S) f I) =
    (↑(v.ramificationIdx w) : ℕ∞) * (emultiplicity v p + emultiplicity v I)
h₆ :
  emultiplicity w (map (F := R →+* S) f p) + (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v I =
    (↑(v.ramificationIdx w) : ℕ∞) * (emultiplicity v p + emultiplicity v I)
⊢ emultiplicity w (map (F := R →+* S) f (p * I)) = (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v (p * I)
have h₇ : emultiplicity w (map (F := R →+* S) f p) + (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v I =
  (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v p + (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v I
Tactic: rw [Ideal.map_mul, emultiplicity_mul hw.prime, emultiplicity_mul hv.prime, IH hI, mul_add,
      emultiplicity_map_eq_ramificationIdx_mul_of_prime hv hp hw hw_bot]
-- 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
inst_3 : IsDedekindDomain S
inst_4 : IsDedekindDomain R
inst_5 : FaithfulSMul R S
v : Ideal R
w : Ideal S
hv : Irreducible v
hw : Irreducible w
hw_bot : w ≠ ⊥
inst_6 : w.LiesOver v
I p : Ideal R
hI : I ≠ 0
hp : Prime p
IH : ∀ (h : I ≠ ⊥), emultiplicity w (map (F := R →+* S) f I) = (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v I
h : p * I ≠ ⊥
h₃ :
  emultiplicity w (HMul.hMul (α := Ideal S) (map (F := R →+* S) f p) (map (F := R →+* S) f I)) =
    (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v (p * I)
h₄ :
  emultiplicity w (map (F := R →+* S) f p) + emultiplicity w (map (F := R →+* S) f I) =
    (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v (p * I)
h₅ :
  emultiplicity w (map (F := R →+* S) f p) + emultiplicity w (map (F := R →+* S) f I) =
    (↑(v.ramificationIdx w) : ℕ∞) * (emultiplicity v p + emultiplicity v I)
h₆ :
  emultiplicity w (map (F := R →+* S) f p) + (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v I =
    (↑(v.ramificationIdx w) : ℕ∞) * (emultiplicity v p + emultiplicity v I)
h₇ :
  emultiplicity w (map (F := R →+* S) f p) + (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v I =
    (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v p + (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v I
⊢ emultiplicity w (map (F := R →+* S) f (p * I)) = (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v (p * I)
have h₈ : (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v p + (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v I =
  (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v p + (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v I
Tactic: rw [Ideal.map_mul, emultiplicity_mul hw.prime, emultiplicity_mul hv.prime, IH hI, mul_add,
      emultiplicity_map_eq_ramificationIdx_mul_of_prime hv hp hw hw_bot]