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
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
⊢ emultiplicity w (map (F := R →+* S) f I) = (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v I
have h₁ : ∀ (h : Ne.{u + 1} (α := Ideal R) 0 ⊥),
  emultiplicity w (map (R := R) (F := R →+* S) f 0) = (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v 0
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]
Cleared hypotheses: I, 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
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
⊢ emultiplicity w (map (F := R →+* S) f I) = (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v I
have h₂ : ∀ (I : Ideal R) (hI : IsUnit I) (h : 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]
Cleared hypotheses: I, 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
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
⊢ emultiplicity w (map (F := R →+* S) f I) = (↑(v.ramificationIdx w) : ℕ∞) * emultiplicity v I
have 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)
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]
Cleared hypotheses: I, h
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (hypothesis)
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_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
have hfg₁ : 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
Cleared hypotheses: hfg, hg
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (hypothesis)
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
⊢ p.ramificationIdx Q = p.ramificationIdx P * P.ramificationIdx Q
have hf0 : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
Tactic: have hf0 : map (algebraMap R S) p ≠ ⊥ := by
    rw [IsScalarTower.algebraMap_eq R S T, ← map_map] at hfg
    exact ne_bot_of_map_ne_bot hfg
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (hypothesis)
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
hf0 : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
⊢ p.ramificationIdx Q = p.ramificationIdx P * P.ramificationIdx Q
have hp0 : P ≠ ⊥
Tactic: have hp0 : P ≠ ⊥ := ne_bot_of_map_ne_bot hg0
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (hypothesis)
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
hf0 : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
hp0 : P ≠ ⊥
⊢ p.ramificationIdx Q = p.ramificationIdx P * P.ramificationIdx Q
have hq0 : Q ≠ ⊥
Tactic: have hq0 : Q ≠ ⊥ := ne_bot_of_le_ne_bot hg0 hg
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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
hf0 : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
hp0 : P ≠ ⊥
hq0 : Q ≠ ⊥
this : P.IsMaximal := ⋯
⊢ p.ramificationIdx Q = p.ramificationIdx P * P.ramificationIdx Q
have rw : Multiset.count Q (normalizedFactors (map (R := S) (F := S →+* T) (algebraMap S T) (map (F := R →+* S) f p))) =
  Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) *
    Multiset.count Q (normalizedFactors (map (F := S →+* T) (algebraMap S T) P))
Tactic: rw [IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count hf0 hpm hp0,
    IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count hg0 hqm hq0,
    IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count hfg hqm hq0,
    IsScalarTower.algebraMap_eq R S T, ← map_map]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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
hf0 : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
hp0 : P ≠ ⊥
hq0 : Q ≠ ⊥
this : P.IsMaximal := ⋯
⊢ Multiset.count Q (normalizedFactors (map (R := S) (F := S →+* T) (algebraMap S T) (map (F := R →+* S) f p))) =
    Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) *
      Multiset.count Q (normalizedFactors (map (F := S →+* T) (algebraMap S T) P))
have rcases : ∀ (I : Ideal S) (hcp : P ⊔ I = ⊤)
  (heq : map (F := R →+* S) f p = P ^ Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) * I),
  Multiset.count Q (normalizedFactors (map (R := S) (F := S →+* T) (algebraMap S T) (map (F := R →+* S) f p))) =
    Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) *
      Multiset.count Q (normalizedFactors (map (F := S →+* T) (algebraMap S T) P))
Tactic: rcases eq_prime_pow_mul_coprime hf0 P with ⟨I, hcp, heq⟩
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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
hf0 : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
hp0 : P ≠ ⊥
hq0 : Q ≠ ⊥
this : P.IsMaximal := ⋯
I : Ideal S
hcp : P ⊔ I = ⊤
heq : map (F := R →+* S) f p = P ^ Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) * I
⊢ Eq.{u_3 + 1} (α := Ideal T) ⊤ (map (F := S →+* T) (algebraMap S T) P ⊔ map (F := S →+* T) (algebraMap S T) I)
have rw : Eq.{u_3 + 1} (α := Ideal T) ⊤ (map (F := S →+* T) (algebraMap S T) (P ⊔ I))
Tactic: rw [← map_sup, hcp, map_top]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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
hf0 : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
hp0 : P ≠ ⊥
hq0 : Q ≠ ⊥
this : P.IsMaximal := ⋯
I : Ideal S
hcp : P ⊔ I = ⊤
heq : map (F := R →+* S) f p = P ^ Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) * I
rw : Eq.{u_3 + 1} (α := Ideal T) ⊤ (map (F := S →+* T) (algebraMap S T) (P ⊔ I))
⊢ Eq.{u_3 + 1} (α := Ideal T) ⊤ (map (F := S →+* T) (algebraMap S T) P ⊔ map (F := S →+* T) (algebraMap S T) I)
have rw₁ : Eq.{u_3 + 1} (α := Ideal T) ⊤ (map (R := S) (F := S →+* T) (algebraMap S T) ⊤)
Tactic: rw [← map_sup, hcp, map_top]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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
hf0 : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
hp0 : P ≠ ⊥
hq0 : Q ≠ ⊥
this : P.IsMaximal := ⋯
I : Ideal S
hcp : P ⊔ I = ⊤
heq : map (F := R →+* S) f p = P ^ Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) * I
rw : Eq.{u_3 + 1} (α := Ideal T) ⊤ (map (F := S →+* T) (algebraMap S T) (P ⊔ I))
rw₁ : Eq.{u_3 + 1} (α := Ideal T) ⊤ (map (R := S) (F := S →+* T) (algebraMap S T) ⊤)
⊢ Eq.{u_3 + 1} (α := Ideal T) ⊤ (map (F := S →+* T) (algebraMap S T) P ⊔ map (F := S →+* T) (algebraMap S T) I)
have rw₂ : Eq.{u_3 + 1} (α := Ideal T) ⊤ ⊤
Tactic: rw [← map_sup, hcp, map_top]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (hypothesis)
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
hf0 : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
hp0 : P ≠ ⊥
hq0 : Q ≠ ⊥
this : P.IsMaximal := ⋯
I : Ideal S
hcp : P ⊔ I = ⊤
heq : map (F := R →+* S) f p = P ^ Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) * I
⊢ Multiset.count Q (normalizedFactors (map (R := S) (F := S →+* T) (algebraMap S T) (map (F := R →+* S) f p))) =
    Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) *
      Multiset.count Q (normalizedFactors (map (F := S →+* T) (algebraMap S T) P))
have hcp₁ : Eq.{u_3 + 1} (α := Ideal T) ⊤ (map (F := S →+* T) (algebraMap S T) P ⊔ map (F := S →+* T) (algebraMap S T) I)
Tactic: have hcp : ⊤ = map (algebraMap S T) P ⊔ map (algebraMap S T) I := by rw [← map_sup, hcp, map_top]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (hypothesis)
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
hf0 : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
hp0 : P ≠ ⊥
hq0 : Q ≠ ⊥
this : P.IsMaximal := ⋯
I : Ideal S
hcp_1 : P ⊔ I = ⊤
heq : map (F := R →+* S) f p = P ^ Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) * I
hcp : Eq.{u_3 + 1} (α := Ideal T) ⊤ (map (F := S →+* T) (algebraMap S T) P ⊔ map (F := S →+* T) (algebraMap S T) I)
⊢ Multiset.count Q (normalizedFactors (map (R := S) (F := S →+* T) (algebraMap S T) (map (F := R →+* S) f p))) =
    Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) *
      Multiset.count Q (normalizedFactors (map (F := S →+* T) (algebraMap S T) P))
have hntq : ¬⊤ ≤ Q
Tactic: have hntq : ¬ ⊤ ≤ Q := fun ht ↦ IsPrime.ne_top hqm (Iff.mpr (eq_top_iff_one Q) (ht trivial))
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (hypothesis)
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
hf0 : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
hp0 : P ≠ ⊥
hq0 : Q ≠ ⊥
this : P.IsMaximal := ⋯
I : Ideal S
hcp_1 : P ⊔ I = ⊤
heq : map (F := R →+* S) f p = P ^ Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) * I
hcp : Eq.{u_3 + 1} (α := Ideal T) ⊤ (map (F := S →+* T) (algebraMap S T) P ⊔ map (F := S →+* T) (algebraMap S T) I)
hntq : ¬⊤ ≤ Q
h : Eq.{u_3 + 1} (α := Ideal T) (map (F := S →+* T) (algebraMap S T) I) 0
⊢ False
have hcp₁ : Eq.{u_3 + 1} (α := Ideal T) ⊤ (map (F := S →+* T) (algebraMap S T) P)
Tactic: simp only [h, Submodule.zero_eq_bot, bot_le, sup_of_le_left] at hcp
Cleared hypotheses: hcp
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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
hf0 : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
hp0 : P ≠ ⊥
hq0 : Q ≠ ⊥
this : P.IsMaximal := ⋯
I : Ideal S
hcp_1 : P ⊔ I = ⊤
heq : map (F := R →+* S) f p = P ^ Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) * I
hcp : Eq.{u_3 + 1} (α := Ideal T) ⊤ (map (F := S →+* T) (algebraMap S T) P ⊔ map (F := S →+* T) (algebraMap S T) I)
hntq : ¬⊤ ≤ Q
⊢ Multiset.count Q (normalizedFactors (map (R := S) (F := S →+* T) (algebraMap S T) (map (F := R →+* S) f p))) =
    Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) *
      Multiset.count Q (normalizedFactors (map (F := S →+* T) (algebraMap S T) P))
have nth_rw : Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) *
      Multiset.count Q (normalizedFactors (map (F := S →+* T) (algebraMap S T) P)) +
    Multiset.count Q (normalizedFactors (map (F := S →+* T) (algebraMap S T) I)) =
  Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) *
    Multiset.count Q (normalizedFactors (map (F := S →+* T) (algebraMap S T) P))
Tactic: nth_rw 1 [heq, Ideal.map_mul, Ideal.map_pow, normalizedFactors_mul (pow_ne_zero _ hg0) <| by
    by_contra h
    simp only [h, Submodule.zero_eq_bot, bot_le, sup_of_le_left] at hcp
    exact hntq (hcp.trans_le hg), Multiset.count_add, normalizedFactors_pow, Multiset.count_nsmul]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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
⊢ p.ramificationIdx Q = p.ramificationIdx P * P.ramificationIdx Q
have have : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
Tactic: classical
  have hf0 : map (algebraMap R S) p ≠ ⊥ := by
    rw [IsScalarTower.algebraMap_eq R S T, ← map_map] at hfg
    exact ne_bot_of_map_ne_bot hfg
  have hp0 : P ≠ ⊥ := ne_bot_of_map_ne_bot hg0
  have hq0 : Q ≠ ⊥ := ne_bot_of_le_ne_bot hg0 hg
  letI : P.IsMaximal := Ring.DimensionLEOne.maximalOfPrime hp0 hpm
  rw [IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count hf0 hpm hp0,
    IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count hg0 hqm hq0,
    IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count hfg hqm hq0,
    IsScalarTower.algebraMap_eq R S T, ← map_map]
  rcases eq_prime_pow_mul_coprime hf0 P with ⟨I, hcp, heq⟩
  have hcp : ⊤ = map (algebraMap S T) P ⊔ map (algebraMap S T) I := by rw [← map_sup, hcp, map_top]
  have hntq : ¬ ⊤ ≤ Q := fun ht ↦ IsPrime.ne_top hqm (Iff.mpr (eq_top_iff_one Q) (ht trivial))
  nth_rw 1 [heq, Ideal.map_mul, Ideal.map_pow, normalizedFactors_mul (pow_ne_zero _ hg0) <| by
    by_contra h
    simp only [h, Submodule.zero_eq_bot, bot_le, sup_of_le_left] at hcp
    exact hntq (hcp.trans_le hg), Multiset.count_add, normalizedFactors_pow, Multiset.count_nsmul]
  exact add_eq_left.mpr <| Decidable.byContradiction fun h ↦ hntq <| hcp.trans_le <|
    sup_le hg <| le_of_dvd <| dvd_of_mem_normalizedFactors <| Multiset.count_ne_zero.mp h
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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
have : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
⊢ p.ramificationIdx Q = p.ramificationIdx P * P.ramificationIdx Q
have have₁ : ∀ (hf0 : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥),
  p.ramificationIdx Q = p.ramificationIdx P * P.ramificationIdx Q
Tactic: classical
  have hf0 : map (algebraMap R S) p ≠ ⊥ := by
    rw [IsScalarTower.algebraMap_eq R S T, ← map_map] at hfg
    exact ne_bot_of_map_ne_bot hfg
  have hp0 : P ≠ ⊥ := ne_bot_of_map_ne_bot hg0
  have hq0 : Q ≠ ⊥ := ne_bot_of_le_ne_bot hg0 hg
  letI : P.IsMaximal := Ring.DimensionLEOne.maximalOfPrime hp0 hpm
  rw [IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count hf0 hpm hp0,
    IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count hg0 hqm hq0,
    IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count hfg hqm hq0,
    IsScalarTower.algebraMap_eq R S T, ← map_map]
  rcases eq_prime_pow_mul_coprime hf0 P with ⟨I, hcp, heq⟩
  have hcp : ⊤ = map (algebraMap S T) P ⊔ map (algebraMap S T) I := by rw [← map_sup, hcp, map_top]
  have hntq : ¬ ⊤ ≤ Q := fun ht ↦ IsPrime.ne_top hqm (Iff.mpr (eq_top_iff_one Q) (ht trivial))
  nth_rw 1 [heq, Ideal.map_mul, Ideal.map_pow, normalizedFactors_mul (pow_ne_zero _ hg0) <| by
    by_contra h
    simp only [h, Submodule.zero_eq_bot, bot_le, sup_of_le_left] at hcp
    exact hntq (hcp.trans_le hg), Multiset.count_add, normalizedFactors_pow, Multiset.count_nsmul]
  exact add_eq_left.mpr <| Decidable.byContradiction fun h ↦ hntq <| hcp.trans_le <|
    sup_le hg <| le_of_dvd <| dvd_of_mem_normalizedFactors <| Multiset.count_ne_zero.mp h