awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : IsIntegrallyClosed R
inst_5 : IsIntegrallyClosed S
inst_6 : Algebra R S
inst_7 : Module.Finite R S
inst_8 : IsTorsionFree R S
inst_9 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
P : Ideal S
p : Ideal R
hPp : P.LiesOver p
inst_11 : p.IsMaximal
inst_12 : P.IsPrime
inst_13 : IsGalois.{u_1, u_3} (FractionRing R) (FractionRing S)
G : Type u_3 := Gal(FractionRing S/FractionRing R)
this_1 : MulSemiringAction Gal(FractionRing S/FractionRing R) S :=
  IsIntegralClosure.MulSemiringAction R (FractionRing R) (FractionRing S) S
this : IsGaloisGroup G R S
hp : ¬p = ⊥
s : ℕ
hs : (relNorm R : (a : Ideal S) → Ideal R) P = p ^ s
h₀ :
  ∀ (Q : Ideal S),
    Membership.mem (γ := Finset (Ideal S)) (Set.toFinset (p.primesOver S)) Q →
      HPow.hPow (α := Ideal R) ((relNorm R : (a : Ideal S) → Ideal R) Q : Ideal R) (p.ramificationIdx Q) =
        p ^ (p.ramificationIdxIn S * s)
⊢ s = p.inertiaDeg P
have h : (relNorm R : (a : Ideal S) → Ideal R) (∏ P ∈ Set.toFinset (p.primesOver S), P ^ p.ramificationIdx P) =
  p ^ finrank.{u_1, u_3} (FractionRing R) (FractionRing S)
Tactic: have h := (congr_arg (relNorm R ·) <|
    map_algebraMap_eq_finsetProd_pow hp).symm.trans <| relNorm_algebraMap S p
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : IsIntegrallyClosed R
inst_5 : IsIntegrallyClosed S
inst_6 : Algebra R S
inst_7 : Module.Finite R S
inst_8 : IsTorsionFree R S
inst_9 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
P : Ideal S
p : Ideal R
hPp : P.LiesOver p
inst_11 : p.IsMaximal
inst_12 : P.IsPrime
inst_13 : IsGalois.{u_1, u_3} (FractionRing R) (FractionRing S)
G : Type u_3 := Gal(FractionRing S/FractionRing R)
this_1 : MulSemiringAction Gal(FractionRing S/FractionRing R) S :=
  IsIntegralClosure.MulSemiringAction R (FractionRing R) (FractionRing S) S
this : IsGaloisGroup G R S
hp : ¬p = ⊥
s : ℕ
hs : (relNorm R : (a : Ideal S) → Ideal R) P = p ^ s
h₀ :
  ∀ (Q : Ideal S),
    Membership.mem (γ := Finset (Ideal S)) (Set.toFinset (p.primesOver S)) Q →
      HPow.hPow (α := Ideal R) ((relNorm R : (a : Ideal S) → Ideal R) Q : Ideal R) (p.ramificationIdx Q) =
        p ^ (p.ramificationIdxIn S * s)
h :
  (relNorm R : (a : Ideal S) → Ideal R) (∏ P ∈ Set.toFinset (p.primesOver S), P ^ p.ramificationIdx P) =
    p ^ finrank.{u_1, u_3} (FractionRing R) (FractionRing S)
⊢ s = p.inertiaDeg P
have h₁ : p ^ (p.ramificationIdxIn S * s * Finset.card (α := Ideal S) (Set.toFinset (p.primesOver S))) =
  p ^ finrank.{u_1, u_3} (FractionRing R) (FractionRing S)
Tactic: simp +contextual only [map_prod, map_pow, h₀, Finset.prod_const, ← pow_mul] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : IsIntegrallyClosed R
inst_5 : IsIntegrallyClosed S
inst_6 : Algebra R S
inst_7 : Module.Finite R S
inst_8 : IsTorsionFree R S
inst_9 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
P : Ideal S
p : Ideal R
hPp : P.LiesOver p
inst_11 : p.IsMaximal
inst_12 : P.IsPrime
inst_13 : IsGalois.{u_1, u_3} (FractionRing R) (FractionRing S)
G : Type u_3 := Gal(FractionRing S/FractionRing R)
this_1 : MulSemiringAction Gal(FractionRing S/FractionRing R) S :=
  IsIntegralClosure.MulSemiringAction R (FractionRing R) (FractionRing S) S
this : IsGaloisGroup G R S
hp : ¬p = ⊥
s : ℕ
hs : (relNorm R : (a : Ideal S) → Ideal R) P = p ^ s
h₀ :
  ∀ (Q : Ideal S),
    Membership.mem (γ := Finset (Ideal S)) (Set.toFinset (p.primesOver S)) Q →
      HPow.hPow (α := Ideal R) ((relNorm R : (a : Ideal S) → Ideal R) Q : Ideal R) (p.ramificationIdx Q) =
        p ^ (p.ramificationIdxIn S * s)
h :
  p ^ (p.ramificationIdxIn S * s * Finset.card (α := Ideal S) (Set.toFinset (p.primesOver S))) =
    p ^ finrank.{u_1, u_3} (FractionRing R) (FractionRing S)
⊢ s = p.inertiaDeg P
have rwa : ∀
  (h :
    p ^ (Set.ncard (α := Ideal S) (p.primesOver S) * (p.ramificationIdxIn S * s)) =
      p ^ (Set.ncard (α := Ideal S) (p.primesOver S) * (p.ramificationIdxIn S * p.inertiaDegIn S))),
  p ≠ 1
Tactic: rwa [← IsGaloisGroup.card_eq_finrank G (FractionRing R) (FractionRing S),
    ← Ideal.ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn hp S G, mul_comm,
    ← Set.ncard_eq_toFinset_card',
    ((IsLeftCancelMulZero.mul_left_cancel_of_ne_zero hp).pow_injective _).eq_iff,
    mul_right_inj' (IsDedekindDomain.primesOver_ncard_ne_zero p S),
    mul_right_inj' (ramificationIdxIn_ne_zero G hp),
    inertiaDegIn_eq_inertiaDeg p P G] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : IsIntegrallyClosed R
inst_5 : IsIntegrallyClosed S
inst_6 : Algebra R S
inst_7 : Module.Finite R S
inst_8 : IsTorsionFree R S
inst_9 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
P : Ideal S
p : Ideal R
hPp : P.LiesOver p
inst_11 : p.IsMaximal
inst_12 : P.IsPrime
inst_13 : IsGalois.{u_1, u_3} (FractionRing R) (FractionRing S)
G : Type u_3 := Gal(FractionRing S/FractionRing R)
this_1 : MulSemiringAction Gal(FractionRing S/FractionRing R) S :=
  IsIntegralClosure.MulSemiringAction R (FractionRing R) (FractionRing S) S
this : IsGaloisGroup G R S
hp : ¬p = ⊥
s : ℕ
hs : (relNorm R : (a : Ideal S) → Ideal R) P = p ^ s
h₀ :
  ∀ (Q : Ideal S),
    Membership.mem (γ := Finset (Ideal S)) (Set.toFinset (p.primesOver S)) Q →
      HPow.hPow (α := Ideal R) ((relNorm R : (a : Ideal S) → Ideal R) Q : Ideal R) (p.ramificationIdx Q) =
        p ^ (p.ramificationIdxIn S * s)
h :
  p ^ (Set.ncard (α := Ideal S) (p.primesOver S) * (p.ramificationIdxIn S * s)) =
    p ^ (Set.ncard (α := Ideal S) (p.primesOver S) * (p.ramificationIdxIn S * p.inertiaDegIn S))
⊢ p ≠ 1
have rw : p ≠ ⊤
Tactic: rw [one_eq_top]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : IsIntegrallyClosed R
inst_5 : IsIntegrallyClosed S
inst_6 : Algebra R S
inst_7 : Module.Finite R S
inst_8 : IsTorsionFree R S
inst_9 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
P : Ideal S
p : Ideal R
hPp : P.LiesOver p
inst_11 : PerfectField.{u_1} (FractionRing R)
inst_12 : P.IsMaximal
inst_13 : p.IsMaximal
T : Type u_3 := Ring.NormalClosure R S
⊢ (relNorm R : (a : Ideal S) → Ideal R) P = p ^ p.inertiaDeg P
have obtain : ∀ (Q : Ideal T) (hQ₁ : Q.IsMaximal) (hQ₂ : Q.LiesOver P), (relNorm R : (a : Ideal S) → Ideal R) P = p ^ p.inertiaDeg P
Tactic: obtain ⟨Q, hQ₁, hQ₂⟩ : ∃ Q : Ideal T, Q.IsMaximal ∧ Q.LiesOver P :=
    exists_maximal_ideal_liesOver_of_isIntegral P
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : IsIntegrallyClosed R
inst_5 : IsIntegrallyClosed S
inst_6 : Algebra R S
inst_7 : Module.Finite R S
inst_8 : IsTorsionFree R S
inst_9 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
P : Ideal S
p : Ideal R
hPp : P.LiesOver p
inst_11 : PerfectField.{u_1} (FractionRing R)
inst_12 : P.IsMaximal
inst_13 : p.IsMaximal
T : Type u_3 := Ring.NormalClosure R S
Q : Ideal T
hQ₁ : Q.IsMaximal
hQ₂ : Q.LiesOver P
⊢ (relNorm R : (a : Ideal S) → Ideal R) P = p ^ p.inertiaDeg P
have this : Q.LiesOver p
Tactic: have : Q.LiesOver p := LiesOver.trans Q P p
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : IsIntegrallyClosed R
inst_5 : IsIntegrallyClosed S
inst_6 : Algebra R S
inst_7 : Module.Finite R S
inst_8 : IsTorsionFree R S
inst_9 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
P : Ideal S
p : Ideal R
hPp : P.LiesOver p
inst_11 : PerfectField.{u_1} (FractionRing R)
inst_12 : P.IsMaximal
inst_13 : p.IsMaximal
T : Type u_3 := Ring.NormalClosure R S
Q : Ideal T
hQ₁ : Q.IsMaximal
hQ₂ : Q.LiesOver P
this : Q.LiesOver p
⊢ (relNorm R : (a : Ideal S) → Ideal R) P = p ^ p.inertiaDeg P
have h : (relNorm R : (a : Ideal T) → Ideal R) Q = p ^ p.inertiaDeg Q
Tactic: have h := relNorm_eq_pow_of_isPrime_isGalois Q p
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : IsIntegrallyClosed R
inst_5 : IsIntegrallyClosed S
inst_6 : Algebra R S
inst_7 : Module.Finite R S
inst_8 : IsTorsionFree R S
inst_9 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
P : Ideal S
p : Ideal R
hPp : P.LiesOver p
inst_11 : PerfectField.{u_1} (FractionRing R)
inst_12 : P.IsMaximal
inst_13 : p.IsMaximal
T : Type u_3 := Ring.NormalClosure R S
Q : Ideal T
hQ₁ : Q.IsMaximal
hQ₂ : Q.LiesOver P
this : Q.LiesOver p
h : (relNorm R : (a : Ideal T) → Ideal R) Q = p ^ p.inertiaDeg Q
⊢ (relNorm R : (a : Ideal S) → Ideal R) P = p ^ p.inertiaDeg P
have this₁ : IsGalois.{u_3, u_3} (FractionRing S) (FractionRing T)
Tactic: have : IsGalois (FractionRing S) (FractionRing T) :=
    IsGalois.tower_top_of_isGalois (FractionRing R) (FractionRing S) (FractionRing T)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : IsIntegrallyClosed R
inst_5 : IsIntegrallyClosed S
inst_6 : Algebra R S
inst_7 : Module.Finite R S
inst_8 : IsTorsionFree R S
inst_9 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
P : Ideal S
p : Ideal R
hPp : P.LiesOver p
inst_11 : PerfectField.{u_1} (FractionRing R)
inst_12 : P.IsMaximal
inst_13 : p.IsMaximal
T : Type u_3 := Ring.NormalClosure R S
Q : Ideal T
hQ₁ : Q.IsMaximal
hQ₂ : Q.LiesOver P
this_1 : Q.LiesOver p
h : (relNorm R : (a : Ideal T) → Ideal R) Q = p ^ p.inertiaDeg Q
this : IsGalois.{u_3, u_3} (FractionRing S) (FractionRing T)
⊢ (relNorm R : (a : Ideal S) → Ideal R) P = p ^ p.inertiaDeg P
have rwa : ∀
  (h :
    HPow.hPow (α := Ideal R) ((relNorm R : (a : Ideal S) → Ideal R) P : Ideal R) (P.inertiaDeg Q) =
      (p ^ p.inertiaDeg P) ^ P.inertiaDeg Q)
  (this : IsGalois.{u_3, u_3} (FractionRing S) (FractionRing T)), P.inertiaDeg Q ≠ 0
Tactic: rwa [← relNorm_relNorm R S, relNorm_eq_pow_of_isPrime_isGalois Q P, map_pow,
    inertiaDeg_algebra_tower p P Q, pow_mul, pow_left_inj] at h
Cleared hypotheses: h, this
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : IsIntegrallyClosed R
inst_5 : IsIntegrallyClosed S
inst_6 : Algebra R S
inst_7 : Module.Finite R S
inst_8 : IsTorsionFree R S
inst_9 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
inst_11 : Free ℤ R
inst_12 : Free ℤ S
inst_13 : Module.Finite ℤ S
inst_14 : PerfectField.{u_1} (FractionRing R)
I : Ideal S
⊢ Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) I : Ideal R) : ℕ)
    ((absNorm : (a : Ideal S) → ℕ) I : ℕ)
have this : Module.Finite ℤ R
Tactic: have : Module.Finite ℤ R := Module.Finite.left ℤ R S
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : IsIntegrallyClosed R
inst_5 : IsIntegrallyClosed S
inst_6 : Algebra R S
inst_7 : Module.Finite R S
inst_8 : IsTorsionFree R S
inst_9 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
inst_11 : Free ℤ R
inst_12 : Free ℤ S
inst_13 : Module.Finite ℤ S
inst_14 : PerfectField.{u_1} (FractionRing R)
I : Ideal S
this : Module.Finite ℤ R
⊢ Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) I : Ideal R) : ℕ)
    ((absNorm : (a : Ideal S) → ℕ) I : ℕ)
have pos : ∀ (hI : I = ⊥),
  Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) I : Ideal R) : ℕ)
    ((absNorm : (a : Ideal S) → ℕ) I : ℕ)
Tactic: by_cases hI : I = ⊥
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : IsIntegrallyClosed R
inst_5 : IsIntegrallyClosed S
inst_6 : Algebra R S
inst_7 : Module.Finite R S
inst_8 : IsTorsionFree R S
inst_9 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
inst_11 : Free ℤ R
inst_12 : Free ℤ S
inst_13 : Module.Finite ℤ S
inst_14 : PerfectField.{u_1} (FractionRing R)
I : Ideal S
this : Module.Finite ℤ R
pos :
  ∀ (hI : I = ⊥),
    Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) I : Ideal R) : ℕ)
      ((absNorm : (a : Ideal S) → ℕ) I : ℕ)
⊢ Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) I : Ideal R) : ℕ)
    ((absNorm : (a : Ideal S) → ℕ) I : ℕ)
have neg : ∀ (hI : ¬I = ⊥),
  Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) I : Ideal R) : ℕ)
    ((absNorm : (a : Ideal S) → ℕ) I : ℕ)
Tactic: by_cases hI : I = ⊥
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : IsIntegrallyClosed R
inst_5 : IsIntegrallyClosed S
inst_6 : Algebra R S
inst_7 : Module.Finite R S
inst_8 : IsTorsionFree R S
inst_9 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
inst_11 : Free ℤ R
inst_12 : Free ℤ S
inst_13 : Module.Finite ℤ S
inst_14 : PerfectField.{u_1} (FractionRing R)
I : Ideal S
this : Module.Finite ℤ R
hI : ¬I = ⊥
⊢ Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) I : Ideal R) : ℕ)
    ((absNorm : (a : Ideal S) → ℕ) I : ℕ)
have neg : Eq (α := ℕ)
  ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) (normalizedFactors I).prod : Ideal R) : ℕ)
  ((absNorm : (a : Ideal S) → ℕ) (normalizedFactors I).prod : ℕ)
Tactic: rw [← prod_normalizedFactors_eq_self hI]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : IsIntegrallyClosed R
inst_5 : IsIntegrallyClosed S
inst_6 : Algebra R S
inst_7 : Module.Finite R S
inst_8 : IsTorsionFree R S
inst_9 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
inst_11 : Free ℤ R
inst_12 : Free ℤ S
inst_13 : Module.Finite ℤ S
inst_14 : PerfectField.{u_1} (FractionRing R)
I : Ideal S
this : Module.Finite ℤ R
hI : ¬I = ⊥
⊢ Eq (α := ℕ)
    ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) (normalizedFactors I).prod : Ideal R) : ℕ)
    ((absNorm : (a : Ideal S) → ℕ) (normalizedFactors I).prod : ℕ)
have neg : ∀ (a b : Ideal S),
  (fun (I : Ideal S) ↦
        Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) I : Ideal R) : ℕ)
          ((absNorm : (a : Ideal S) → ℕ) I : ℕ))
      a →
    (fun (I : Ideal S) ↦
          Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) I : Ideal R) : ℕ)
            ((absNorm : (a : Ideal S) → ℕ) I : ℕ))
        b →
      (fun (I : Ideal S) ↦
          Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) I : Ideal R) : ℕ)
            ((absNorm : (a : Ideal S) → ℕ) I : ℕ))
        (a * b)
Tactic: refine Multiset.prod_induction (fun I ↦ absNorm (relNorm R I) = absNorm I) _ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : IsIntegrallyClosed R
inst_5 : IsIntegrallyClosed S
inst_6 : Algebra R S
inst_7 : Module.Finite R S
inst_8 : IsTorsionFree R S
inst_9 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
inst_11 : Free ℤ R
inst_12 : Free ℤ S
inst_13 : Module.Finite ℤ S
inst_14 : PerfectField.{u_1} (FractionRing R)
I : Ideal S
this : Module.Finite ℤ R
hI : ¬I = ⊥
neg :
  ∀ (a b : Ideal S),
    (fun (I : Ideal S) ↦
          Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) I : Ideal R) : ℕ)
            ((absNorm : (a : Ideal S) → ℕ) I : ℕ))
        a →
      (fun (I : Ideal S) ↦
            Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) I : Ideal R) : ℕ)
              ((absNorm : (a : Ideal S) → ℕ) I : ℕ))
          b →
        (fun (I : Ideal S) ↦
            Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) I : Ideal R) : ℕ)
              ((absNorm : (a : Ideal S) → ℕ) I : ℕ))
          (a * b)
⊢ Eq (α := ℕ)
    ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) (normalizedFactors I).prod : Ideal R) : ℕ)
    ((absNorm : (a : Ideal S) → ℕ) (normalizedFactors I).prod : ℕ)
have neg₁ : (fun (I : Ideal S) ↦
    Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) I : Ideal R) : ℕ)
      ((absNorm : (a : Ideal S) → ℕ) I : ℕ))
  1
Tactic: refine Multiset.prod_induction (fun I ↦ absNorm (relNorm R I) = absNorm I) _ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : IsIntegrallyClosed R
inst_5 : IsIntegrallyClosed S
inst_6 : Algebra R S
inst_7 : Module.Finite R S
inst_8 : IsTorsionFree R S
inst_9 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
inst_11 : Free ℤ R
inst_12 : Free ℤ S
inst_13 : Module.Finite ℤ S
inst_14 : PerfectField.{u_1} (FractionRing R)
I : Ideal S
this : Module.Finite ℤ R
hI : ¬I = ⊥
neg :
  ∀ (a b : Ideal S),
    (fun (I : Ideal S) ↦
          Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) I : Ideal R) : ℕ)
            ((absNorm : (a : Ideal S) → ℕ) I : ℕ))
        a →
      (fun (I : Ideal S) ↦
            Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) I : Ideal R) : ℕ)
              ((absNorm : (a : Ideal S) → ℕ) I : ℕ))
          b →
        (fun (I : Ideal S) ↦
            Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) I : Ideal R) : ℕ)
              ((absNorm : (a : Ideal S) → ℕ) I : ℕ))
          (a * b)
neg₁ :
  Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) 1) : ℕ)
    ((absNorm : (a : Ideal S) → ℕ) 1 : ℕ)
⊢ Eq (α := ℕ)
    ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) (normalizedFactors I).prod : Ideal R) : ℕ)
    ((absNorm : (a : Ideal S) → ℕ) (normalizedFactors I).prod : ℕ)
have neg₂ : ∀ a ∈ normalizedFactors I,
  (fun (I : Ideal S) ↦
      Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) I : Ideal R) : ℕ)
        ((absNorm : (a : Ideal S) → ℕ) I : ℕ))
    a
Tactic: refine Multiset.prod_induction (fun I ↦ absNorm (relNorm R I) = absNorm I) _ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : IsIntegrallyClosed R
inst_5 : IsIntegrallyClosed S
inst_6 : Algebra R S
inst_7 : Module.Finite R S
inst_8 : IsTorsionFree R S
inst_9 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
inst_11 : Free ℤ R
inst_12 : Free ℤ S
inst_13 : Module.Finite ℤ S
inst_14 : PerfectField.{u_1} (FractionRing R)
I : Ideal S
this : Module.Finite ℤ R
hI : ¬I = ⊥
a b : Ideal S
hx :
  Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) a : Ideal R) : ℕ)
    ((absNorm : (a : Ideal S) → ℕ) a : ℕ)
hy :
  Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) b : Ideal R) : ℕ)
    ((absNorm : (a : Ideal S) → ℕ) b : ℕ)
⊢ Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) (a * b) : Ideal R) : ℕ)
    ((absNorm : (a : Ideal S) → ℕ) (a * b) : ℕ)
have neg : Eq (α := ℕ)
  ((absNorm : (a : Ideal R) → ℕ)
      (HMul.hMul (α := Ideal R) (β := Ideal R) ((relNorm R : (a : Ideal S) → Ideal R) a : Ideal R)
        ((relNorm R : (a : Ideal S) → Ideal R) b : Ideal R)) :
    ℕ)
  ((absNorm : (a : Ideal S) → ℕ) (a * b) : ℕ)
Tactic: rw [map_mul, map_mul, map_mul, hx, hy]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : IsIntegrallyClosed R
inst_5 : IsIntegrallyClosed S
inst_6 : Algebra R S
inst_7 : Module.Finite R S
inst_8 : IsTorsionFree R S
inst_9 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
inst_11 : Free ℤ R
inst_12 : Free ℤ S
inst_13 : Module.Finite ℤ S
inst_14 : PerfectField.{u_1} (FractionRing R)
I : Ideal S
this : Module.Finite ℤ R
hI : ¬I = ⊥
a b : Ideal S
hx :
  Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) a : Ideal R) : ℕ)
    ((absNorm : (a : Ideal S) → ℕ) a : ℕ)
hy :
  Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) b : Ideal R) : ℕ)
    ((absNorm : (a : Ideal S) → ℕ) b : ℕ)
neg :
  Eq (α := ℕ)
    ((absNorm : (a : Ideal R) → ℕ)
        (HMul.hMul (α := Ideal R) (β := Ideal R) ((relNorm R : (a : Ideal S) → Ideal R) a : Ideal R)
          ((relNorm R : (a : Ideal S) → Ideal R) b : Ideal R)) :
      ℕ)
    ((absNorm : (a : Ideal S) → ℕ) (a * b) : ℕ)
⊢ Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) (a * b) : Ideal R) : ℕ)
    ((absNorm : (a : Ideal S) → ℕ) (a * b) : ℕ)
have neg₁ : HMul.hMul (α := ℕ) (β := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) a : Ideal R) : ℕ)
    ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) b : Ideal R) : ℕ) =
  (absNorm : (a : Ideal S) → ℕ) (a * b)
Tactic: rw [map_mul, map_mul, map_mul, hx, hy]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : IsIntegrallyClosed R
inst_5 : IsIntegrallyClosed S
inst_6 : Algebra R S
inst_7 : Module.Finite R S
inst_8 : IsTorsionFree R S
inst_9 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
inst_11 : Free ℤ R
inst_12 : Free ℤ S
inst_13 : Module.Finite ℤ S
inst_14 : PerfectField.{u_1} (FractionRing R)
I : Ideal S
this : Module.Finite ℤ R
hI : ¬I = ⊥
a b : Ideal S
hx :
  Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) a : Ideal R) : ℕ)
    ((absNorm : (a : Ideal S) → ℕ) a : ℕ)
hy :
  Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) b : Ideal R) : ℕ)
    ((absNorm : (a : Ideal S) → ℕ) b : ℕ)
neg :
  Eq (α := ℕ)
    ((absNorm : (a : Ideal R) → ℕ)
        (HMul.hMul (α := Ideal R) (β := Ideal R) ((relNorm R : (a : Ideal S) → Ideal R) a : Ideal R)
          ((relNorm R : (a : Ideal S) → Ideal R) b : Ideal R)) :
      ℕ)
    ((absNorm : (a : Ideal S) → ℕ) (a * b) : ℕ)
neg₁ :
  HMul.hMul (α := ℕ) (β := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) a : Ideal R) : ℕ)
      ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) b : Ideal R) : ℕ) =
    (absNorm : (a : Ideal S) → ℕ) (a * b)
⊢ Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) (a * b) : Ideal R) : ℕ)
    ((absNorm : (a : Ideal S) → ℕ) (a * b) : ℕ)
have neg₂ : HMul.hMul (α := ℕ) (β := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) a : Ideal R) : ℕ)
    ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) b : Ideal R) : ℕ) =
  HMul.hMul (α := ℕ) (β := ℕ) ((absNorm : (a : Ideal S) → ℕ) a : ℕ) ((absNorm : (a : Ideal S) → ℕ) b : ℕ)
Tactic: rw [map_mul, map_mul, map_mul, hx, hy]