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
inst_3 : IsDedekindDomain S
p : Ideal R
P : Ideal S
inst_4 : P.IsPrime
hp : P ≠ ⊥
hpP : map (F := R →+* S) f p ≤ P
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))
⊢ 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 _)⟩
-- 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
Sₚ : Type v := Localization.AtPrime P
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))
⊢ 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:
rw [← not_ne_iff (b := 1), ramificationIdx_ne_one_iff hpP, pow_two]

Premises used: pow_two, Ideal.ramificationIdx_ne_one_iff, not_ne_iff
-- 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
Sₚ : Type v := Localization.AtPrime P
H₁ : ¬map (F := R →+* S) f p ≤ P * P
⊢ P ∣ map (F := R →+* S) f p

Tactic:
Ideal.dvd_iff_le.mpr hpP

Premises used: Iff.mpr, Ideal.dvd_iff_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
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
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))
⊢ 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

Premises used: Iff.mpr, Ideal.dvd_iff_le, Algebra.algebraMap, Ideal.map
-- 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
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
⊢ ¬a ≤ P

Tactic:
have ha' : ¬ a ≤ P := fun h ↦ H₁ (ha.trans_le (Ideal.mul_mono_right h))
-- 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
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
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)
⊢ 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 [IsScalarTower.algebraMap_eq _ S, ← Ideal.map_map, ha, Ideal.map_mul,
    Localization.AtPrime.map_eq_maximalIdeal]

Premises used: Ideal.map_mul, Ideal.map_map, IsScalarTower.algebraMap_eq, Localization.AtPrime.map_eq_maximalIdeal
-- 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
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)) ⊤ =
    maximalIdeal (Localization (M := S) P.primeCompl)

Tactic:
Ideal.mul_top _

Premises used: Ideal.mul_top
-- 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
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) ⊤
convert_4 : IsTwoSided.{v} (α := Localization.AtPrime P) (maximalIdeal (Localization (M := S) P.primeCompl))
⊢ 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:
convert! Ideal.mul_top _

Premises used: Ideal.mul_top
-- 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
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
⊢ IsTwoSided.{v} (α := Localization.AtPrime P) (maximalIdeal (Localization (M := S) P.primeCompl))

Tactic:
infer_instance
-- 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
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
⊢ IsTwoSided.{v} (α := Localization.AtPrime P) (maximalIdeal (Localization (M := S) P.primeCompl))

Tactic:
on_goal 2 => infer_instance
-- 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
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 : ¬Disjoint (↑P.primeCompl : Set S) (↑a : Set S)
⊢ Eq (α := Ideal (Localization.AtPrime P))
    (map (F := S →+* Localization.AtPrime P) (algebraMap S (Localization.AtPrime P)) a) ⊤

Tactic:
rw [← not_ne_iff, IsLocalization.map_algebraMap_ne_top_iff_disjoint P.primeCompl]

Premises used: not_ne_iff, Ideal.primeCompl, IsLocalization.map_algebraMap_ne_top_iff_disjoint
-- 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
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
⊢ ¬Disjoint (↑P.primeCompl : Set S) (↑a : Set S)

Tactic:
simpa [primeCompl, Set.disjoint_compl_left_iff_subset]

Premises used: Set.disjoint_compl_left_iff_subset, Ideal.primeCompl
-- 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
S₀ : Type u_2
inst_6 : CommRing S₀
inst_7 : Algebra R S₀
inst_8 : Algebra S₀ S
inst_9 : IsScalarTower R S₀ S
p : Ideal R
P : Ideal S₀
Q : Ideal S
inst_10 : Q.LiesOver p
hP : P.LiesOver p
inst_11 : Q.IsPrime
hp : p ≠ ⊥
⊢ P.ramificationIdx Q ≤ p.ramificationIdx Q

Tactic:
p.ramificationIdx_le_ramificationIdx P Q ((liesOver_iff ..).mp hP) <|
    ramificationIdx_ne_zero_of_liesOver _ hp

Premises used: Ideal.IsDedekindDomain.ramificationIdx_ne_zero_of_liesOver, Ideal.liesOver_iff, Iff.mp, Ideal.ramificationIdx_le_ramificationIdx
-- 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 : 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

Tactic:
emultiplicity_eq_zero.2 fun h ↦ hvp.symm ?_

Premises used: Iff.mpr, emultiplicity_eq_zero, Ne.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
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
refine : ∀ (h : w ∣ map (F := R →+* S) f p), p = v
⊢ emultiplicity w (map (F := R →+* S) f p) = 0

Tactic:
refine emultiplicity_eq_zero.2 fun h ↦ hvp.symm ?_

Premises used: Iff.mpr, emultiplicity_eq_zero, Ne.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
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

Tactic:
rw [Ideal.dvd_iff_le, Ideal.map_le_iff_le_comap, ← under_def, ← Ideal.over_def w v] at h

Premises used: Ideal.dvd_iff_le, Ideal.map_le_iff_le_comap, Ideal.under_def, Ideal.over_def
-- 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 : 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 : p ≤ v
⊢ p = v

Tactic:
((isPrime_of_prime hp).isMaximal hp.ne_zero).eq_of_le (isPrime_of_prime hv.prime).ne_top h

Premises used: Ideal.IsPrime.isMaximal, Ideal.IsMaximal.eq_of_le, Prime.ne_zero, Ideal.isPrime_of_prime, Irreducible.prime, Ideal.IsPrime.ne_top
-- 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 : 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 : p ≤ v
⊢ p = v

Tactic:
exact ((isPrime_of_prime hp).isMaximal hp.ne_zero).eq_of_le (isPrime_of_prime hv.prime).ne_top h

Premises used: Ideal.IsPrime.isMaximal, Ideal.IsMaximal.eq_of_le, Prime.ne_zero, Ideal.isPrime_of_prime, Irreducible.prime, Ideal.IsPrime.ne_top
-- 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 : 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
⊢ 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
-- 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 : 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
neg : ∀ (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

Tactic:
by_cases hvp : v = 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
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

Tactic:
simp [hvp, (FiniteMultiplicity.of_prime_left hp hp.ne_zero).emultiplicity_self,
      ramificationIdx_eq_normalizedFactors_count hp_bot (isPrime_of_prime hw.prime) hw_bot,
      emultiplicity_eq_count_normalizedFactors hw hp_bot]

Premises used: FiniteMultiplicity.emultiplicity_self, Ideal.IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count, UniqueFactorizationMonoid.emultiplicity_eq_count_normalizedFactors, Prime.ne_zero, FiniteMultiplicity.of_prime_left, Ideal.isPrime_of_prime, Irreducible.prime
-- 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 : 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
neg₂ neg₃ : Eq (α := ℕ∞) 0 0
⊢ emultiplicity w (map (F := R →+* S) f p) = (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v p

Tactic:
rw [emultiplicity_eq_zero_of_irreducible_ne hv hp.irreducible hvp, mul_zero,
      emultiplicity_map_eq_zero_of_ne hv hp hvp]

Premises used: Prime.irreducible, MulZeroClass.mul_zero, emultiplicity_eq_zero_of_irreducible_ne, Ideal.IsDedekindDomain.emultiplicity_map_eq_zero_of_ne
-- 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 : 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
h : Ne.{u + 1} (α := Ideal R) 0 ⊥
⊢ emultiplicity w (map (R := R) (F := R →+* S) f 0) = (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v 0

Tactic:
aesop
-- 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 : 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 ≠ ⊥
⊢ I = ⊤

Tactic:
simpa using hI
-- 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 : 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 ≠ ⊥
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 ⊤
⊢ emultiplicity w (map (F := R →+* S) f I) = (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v I

Tactic:
obtain rfl : I = ⊤ := by simpa using hI

Premises used: rfl
-- 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 : 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) ⊤ ⊥
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))) :
        ℕ∞)
⊢ emultiplicity w (map (R := R) (F := R →+* S) f ⊤) = (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v ⊤

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]

Premises used: Ideal.one_eq_top, top_ne_bot, UniqueFactorizationMonoid.normalizedFactors_one, UniqueFactorizationMonoid.emultiplicity_eq_count_normalizedFactors, Ideal.map_top
-- 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 : 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) ⊤ ⊥
⊢ (↑(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
-- 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 : 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
h₈ 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
⊢ emultiplicity w (map (F := R →+* S) f (p * 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]

Premises used: Ideal.map_mul, mul_add, Irreducible.prime, _private.0.Ideal.IsDedekindDomain.emultiplicity_map_eq_ramificationIdx_mul_of_prime, emultiplicity_mul
-- 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 : IsDedekindDomain R
inst_5 : FaithfulSMul R S
v : Ideal R
w : Ideal S
I : Ideal R
h : I ≠ ⊥
hv : Irreducible v
hw : Irreducible w
hw_bot : w ≠ ⊥
inst_6 : w.LiesOver v
h₁ :
  ∀ (h : Ne.{u + 1} (α := Ideal R) 0 ⊥),
    emultiplicity w (map (R := R) (F := R →+* S) f 0) = (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v 0
h₂ :
  ∀ (I : Ideal R) (hI : IsUnit I) (h : I ≠ ⊥),
    emultiplicity w (map (F := R →+* S) f I) = (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v I
h₃ :
  ∀ (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)
⊢ emultiplicity w (map (F := R →+* S) f I) = (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v I

Tactic:
induction I using induction_on_prime with
  | h₁ => aesop
  | h₂ I hI =>
    obtain rfl : I = ⊤ := by simpa using hI
    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]
    simp
  | h₃ I p hI hp IH =>
    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]

Premises used: Ideal.one_eq_top, Ideal.map_mul, top_ne_bot, UniqueFactorizationMonoid.normalizedFactors_one, UniqueFactorizationMonoid.emultiplicity_eq_count_normalizedFactors, mul_add, Ideal.map_top, Irreducible.prime, rfl, emultiplicity_mul
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
inst_7 : IsDedekindDomain S
inst_8 : IsDedekindDomain T
p : Ideal R
P : Ideal S
Q : Ideal T
hpm : P.IsPrime
hqm : Q.IsPrime
hg0 : Ne.{u_3 + 1} (α := Ideal T) (map (F := S →+* T) (algebraMap S T) P) ⊥
hfg : Ne.{u_3 + 1} (α := Ideal T) (map (F := R →+* T) (algebraMap R T) p) ⊥
hg : map (F := S →+* T) (algebraMap S T) P ≤ Q
⊢ Ne.{u_3 + 1} (α := Ideal T) (map (R := S) (F := S →+* T) (algebraMap S T) (map (F := R →+* S) f p)) ⊥

Tactic:
rw [IsScalarTower.algebraMap_eq R S T, ← map_map] at hfg

Premises used: Ideal.map_map, IsScalarTower.algebraMap_eq