awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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 : ℕ)
⊢ 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 S) → ℕ) a : ℕ)
    ((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]
-- 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)
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 : ℕ)
neg₃ :
  HMul.hMul (α := ℕ) (β := ℕ) ((absNorm : (a : Ideal S) → ℕ) a : ℕ)
      ((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 : ℕ)
⊢ 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 S) → ℕ) a : ℕ) ((absNorm : (a : Ideal S) → ℕ) b : ℕ) =
  HMul.hMul (α := ℕ) (β := ℕ) ((absNorm : (a : Ideal S) → ℕ) a : ℕ) ((absNorm : (a : Ideal S) → ℕ) b : ℕ)
Tactic: rw [map_mul, map_mul, map_mul, hx, hy]
-- 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
this : Module.Finite ℤ R
hI : ¬I = ⊥
Q : Ideal S
hQ : Q ∈ normalizedFactors I
⊢ Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) Q : Ideal R) : ℕ)
    ((absNorm : (a : Ideal S) → ℕ) Q : ℕ)
have hQ' : Q ≠ ⊥
Tactic: have hQ' : Q ≠ ⊥ := ne_zero_of_mem_normalizedFactors hQ
-- 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
this : Module.Finite ℤ R
hI : ¬I = ⊥
Q : Ideal S
hQ : Q ∈ normalizedFactors I
hQ' : Q ≠ ⊥
⊢ Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) Q : Ideal R) : ℕ)
    ((absNorm : (a : Ideal S) → ℕ) Q : ℕ)
have hQ₁ : Q.IsPrime ∧ I ≤ Q
Tactic: rw [Ideal.mem_normalizedFactors_iff hI] at hQ
Cleared hypotheses: hQ, hQ'
-- 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
this : Module.Finite ℤ R
hI : ¬I = ⊥
Q : Ideal S
hQ : Q.IsPrime ∧ I ≤ Q
hQ' : Q ≠ ⊥
⊢ Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) Q : Ideal R) : ℕ)
    ((absNorm : (a : Ideal S) → ℕ) Q : ℕ)
have this₁ : Q.IsMaximal
Tactic: have : Q.IsMaximal := Ring.DimensionLEOne.maximalOfPrime hQ' hQ.1
-- 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
this_1 : Module.Finite ℤ R
hI : ¬I = ⊥
Q : Ideal S
hQ : Q.IsPrime ∧ I ≤ Q
hQ' : Q ≠ ⊥
this : Q.IsMaximal
P : Ideal R := under R Q
p : ℕ := (absNorm : (a : Ideal ℤ) → ℕ) (under ℤ P)
⊢ Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) Q : Ideal R) : ℕ)
    ((absNorm : (a : Ideal S) → ℕ) Q : ℕ)
have this₁ : NeZero P
Tactic: have : NeZero P := ⟨under_ne_bot R hQ'⟩
-- 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
this_1 : Module.Finite ℤ R
hI : ¬I = ⊥
Q : Ideal S
hQ : Q.IsPrime ∧ I ≤ Q
hQ' : Q ≠ ⊥
this_2 : Q.IsMaximal
P : Ideal R := under R Q
p : ℕ := (absNorm : (a : Ideal ℤ) → ℕ) (under ℤ P)
this : NeZero P
⊢ Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) Q : Ideal R) : ℕ)
    ((absNorm : (a : Ideal S) → ℕ) Q : ℕ)
have this₁ : Q.LiesOver P
Tactic: have : Q.LiesOver P := by simp [liesOver_iff, 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
inst_11 : Free ℤ R
inst_12 : Free ℤ S
inst_13 : Module.Finite ℤ S
inst_14 : PerfectField.{u_1} (FractionRing R)
I : Ideal S
this_1 : Module.Finite ℤ R
hI : ¬I = ⊥
Q : Ideal S
hQ : Q.IsPrime ∧ I ≤ Q
hQ' : Q ≠ ⊥
this_2 : Q.IsMaximal
P : Ideal R := under R Q
p : ℕ := (absNorm : (a : Ideal ℤ) → ℕ) (under ℤ P)
this_3 : NeZero P
this : Q.LiesOver P
⊢ Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) Q : Ideal R) : ℕ)
    ((absNorm : (a : Ideal S) → ℕ) Q : ℕ)
have this₁ : Q.LiesOver (A := ℤ) (span {(↑p : ℤ)})
Tactic: have : Q.LiesOver (span {(p : ℤ)}) := LiesOver.trans 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
inst_11 : Free ℤ R
inst_12 : Free ℤ S
inst_13 : Module.Finite ℤ S
inst_14 : PerfectField.{u_1} (FractionRing R)
I : Ideal S
this_1 : Module.Finite ℤ R
hI : ¬I = ⊥
Q : Ideal S
hQ : Q.IsPrime ∧ I ≤ Q
hQ' : Q ≠ ⊥
this_2 : Q.IsMaximal
P : Ideal R := under R Q
p : ℕ := (absNorm : (a : Ideal ℤ) → ℕ) (under ℤ P)
this_3 : NeZero P
this_4 : Q.LiesOver P
this : Q.LiesOver (A := ℤ) (span {(↑p : ℤ)})
⊢ Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) Q : Ideal R) : ℕ)
    ((absNorm : (a : Ideal S) → ℕ) Q : ℕ)
have this₁ : Fact (Nat.Prime p)
Tactic: have : Fact (p.Prime) := ⟨Nat.absNorm_under_prime _⟩
-- 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
this_1 : Module.Finite ℤ R
hI : ¬I = ⊥
Q : Ideal S
hQ : Q.IsPrime ∧ I ≤ Q
hQ' : Q ≠ ⊥
this_2 : Q.IsMaximal
P : Ideal R := under R Q
p : ℕ := (absNorm : (a : Ideal ℤ) → ℕ) (under ℤ P)
this_3 : NeZero P
this_4 : Q.LiesOver P
this_5 : Q.LiesOver (A := ℤ) (span {(↑p : ℤ)})
this : Fact (Nat.Prime p)
⊢ Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) Q : Ideal R) : ℕ)
    ((absNorm : (a : Ideal S) → ℕ) Q : ℕ)
have hp : Prime (M := ℤ) (↑p : ℤ)
Tactic: have hp : Prime (p : ℤ) := Nat.prime_iff_prime_int.mp <| Nat.absNorm_under_prime _
-- 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_1 : Module.Finite ℤ R
hI : ¬I = ⊥
Q : Ideal S
hQ : Q.IsPrime ∧ I ≤ Q
hQ' : Q ≠ ⊥
this_2 : Q.IsMaximal
P : Ideal R := under R Q
p : ℕ := (absNorm : (a : Ideal ℤ) → ℕ) (under ℤ P)
this_3 : NeZero P
this_4 : Q.LiesOver P
this_5 : Q.LiesOver (A := ℤ) (span {(↑p : ℤ)})
this : Fact (Nat.Prime p)
hp : Prime (M := ℤ) (↑p : ℤ)
⊢ Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) Q : Ideal R) : ℕ)
    ((absNorm : (a : Ideal S) → ℕ) Q : ℕ)
have neg : Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) (P ^ P.inertiaDeg Q) : ℕ) ((absNorm : (a : Ideal S) → ℕ) Q : ℕ)
Tactic: rw [relNorm_eq_pow_of_isMaximal Q P, map_pow, absNorm_eq_pow_inertiaDeg Q hp,
      absNorm_eq_pow_inertiaDeg P hp, inertiaDeg_algebra_tower (span {(p : ℤ)}) P Q, pow_mul]
-- 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_1 : Module.Finite ℤ R
hI : ¬I = ⊥
Q : Ideal S
hQ : Q.IsPrime ∧ I ≤ Q
hQ' : Q ≠ ⊥
this_2 : Q.IsMaximal
P : Ideal R := under R Q
p : ℕ := (absNorm : (a : Ideal ℤ) → ℕ) (under ℤ P)
this_3 : NeZero P
this_4 : Q.LiesOver P
this_5 : Q.LiesOver (A := ℤ) (span {(↑p : ℤ)})
this : Fact (Nat.Prime p)
hp : Prime (M := ℤ) (↑p : ℤ)
neg : Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) (P ^ P.inertiaDeg Q) : ℕ) ((absNorm : (a : Ideal S) → ℕ) Q : ℕ)
⊢ Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) Q : Ideal R) : ℕ)
    ((absNorm : (a : Ideal S) → ℕ) Q : ℕ)
have neg₁ : HPow.hPow (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) P : ℕ) (P.inertiaDeg Q) = (absNorm : (a : Ideal S) → ℕ) Q
Tactic: rw [relNorm_eq_pow_of_isMaximal Q P, map_pow, absNorm_eq_pow_inertiaDeg Q hp,
      absNorm_eq_pow_inertiaDeg P hp, inertiaDeg_algebra_tower (span {(p : ℤ)}) P Q, pow_mul]
-- 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_1 : Module.Finite ℤ R
hI : ¬I = ⊥
Q : Ideal S
hQ : Q.IsPrime ∧ I ≤ Q
hQ' : Q ≠ ⊥
this_2 : Q.IsMaximal
P : Ideal R := under R Q
p : ℕ := (absNorm : (a : Ideal ℤ) → ℕ) (under ℤ P)
this_3 : NeZero P
this_4 : Q.LiesOver P
this_5 : Q.LiesOver (A := ℤ) (span {(↑p : ℤ)})
this : Fact (Nat.Prime p)
hp : Prime (M := ℤ) (↑p : ℤ)
neg : Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) (P ^ P.inertiaDeg Q) : ℕ) ((absNorm : (a : Ideal S) → ℕ) Q : ℕ)
neg₁ : HPow.hPow (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) P : ℕ) (P.inertiaDeg Q) = (absNorm : (a : Ideal S) → ℕ) Q
⊢ Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) Q : Ideal R) : ℕ)
    ((absNorm : (a : Ideal S) → ℕ) Q : ℕ)
have neg₂ : HPow.hPow (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) P : ℕ) (P.inertiaDeg Q) =
  Int.natAbs (↑p : ℤ) ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) Q
Tactic: rw [relNorm_eq_pow_of_isMaximal Q P, map_pow, absNorm_eq_pow_inertiaDeg Q hp,
      absNorm_eq_pow_inertiaDeg P hp, inertiaDeg_algebra_tower (span {(p : ℤ)}) P Q, pow_mul]
-- 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_1 : Module.Finite ℤ R
hI : ¬I = ⊥
Q : Ideal S
hQ : Q.IsPrime ∧ I ≤ Q
hQ' : Q ≠ ⊥
this_2 : Q.IsMaximal
P : Ideal R := under R Q
p : ℕ := (absNorm : (a : Ideal ℤ) → ℕ) (under ℤ P)
this_3 : NeZero P
this_4 : Q.LiesOver P
this_5 : Q.LiesOver (A := ℤ) (span {(↑p : ℤ)})
this : Fact (Nat.Prime p)
hp : Prime (M := ℤ) (↑p : ℤ)
neg : Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) (P ^ P.inertiaDeg Q) : ℕ) ((absNorm : (a : Ideal S) → ℕ) Q : ℕ)
neg₁ : HPow.hPow (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) P : ℕ) (P.inertiaDeg Q) = (absNorm : (a : Ideal S) → ℕ) Q
neg₂ :
  HPow.hPow (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) P : ℕ) (P.inertiaDeg Q) =
    Int.natAbs (↑p : ℤ) ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) Q
⊢ Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) Q : Ideal R) : ℕ)
    ((absNorm : (a : Ideal S) → ℕ) Q : ℕ)
have neg₃ : (Int.natAbs (↑p : ℤ) ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P) ^ P.inertiaDeg Q =
  Int.natAbs (↑p : ℤ) ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) Q
Tactic: rw [relNorm_eq_pow_of_isMaximal Q P, map_pow, absNorm_eq_pow_inertiaDeg Q hp,
      absNorm_eq_pow_inertiaDeg P hp, inertiaDeg_algebra_tower (span {(p : ℤ)}) P Q, pow_mul]
-- 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_1 : Module.Finite ℤ R
hI : ¬I = ⊥
Q : Ideal S
hQ : Q.IsPrime ∧ I ≤ Q
hQ' : Q ≠ ⊥
this_2 : Q.IsMaximal
P : Ideal R := under R Q
p : ℕ := (absNorm : (a : Ideal ℤ) → ℕ) (under ℤ P)
this_3 : NeZero P
this_4 : Q.LiesOver P
this_5 : Q.LiesOver (A := ℤ) (span {(↑p : ℤ)})
this : Fact (Nat.Prime p)
hp : Prime (M := ℤ) (↑p : ℤ)
neg : Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) (P ^ P.inertiaDeg Q) : ℕ) ((absNorm : (a : Ideal S) → ℕ) Q : ℕ)
neg₁ : HPow.hPow (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) P : ℕ) (P.inertiaDeg Q) = (absNorm : (a : Ideal S) → ℕ) Q
neg₂ :
  HPow.hPow (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) P : ℕ) (P.inertiaDeg Q) =
    Int.natAbs (↑p : ℤ) ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) Q
neg₃ :
  (Int.natAbs (↑p : ℤ) ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P) ^ P.inertiaDeg Q =
    Int.natAbs (↑p : ℤ) ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) Q
⊢ Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) Q : Ideal R) : ℕ)
    ((absNorm : (a : Ideal S) → ℕ) Q : ℕ)
have neg₄ : (Int.natAbs (↑p : ℤ) ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P) ^ P.inertiaDeg Q =
  Int.natAbs (↑p : ℤ) ^ (inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P * P.inertiaDeg Q)
Tactic: rw [relNorm_eq_pow_of_isMaximal Q P, map_pow, absNorm_eq_pow_inertiaDeg Q hp,
      absNorm_eq_pow_inertiaDeg P hp, inertiaDeg_algebra_tower (span {(p : ℤ)}) P Q, pow_mul]
-- 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_1 : Module.Finite ℤ R
hI : ¬I = ⊥
Q : Ideal S
hQ : Q.IsPrime ∧ I ≤ Q
hQ' : Q ≠ ⊥
this_2 : Q.IsMaximal
P : Ideal R := under R Q
p : ℕ := (absNorm : (a : Ideal ℤ) → ℕ) (under ℤ P)
this_3 : NeZero P
this_4 : Q.LiesOver P
this_5 : Q.LiesOver (A := ℤ) (span {(↑p : ℤ)})
this : Fact (Nat.Prime p)
hp : Prime (M := ℤ) (↑p : ℤ)
neg : Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) (P ^ P.inertiaDeg Q) : ℕ) ((absNorm : (a : Ideal S) → ℕ) Q : ℕ)
neg₁ : HPow.hPow (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) P : ℕ) (P.inertiaDeg Q) = (absNorm : (a : Ideal S) → ℕ) Q
neg₂ :
  HPow.hPow (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) P : ℕ) (P.inertiaDeg Q) =
    Int.natAbs (↑p : ℤ) ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) Q
neg₃ :
  (Int.natAbs (↑p : ℤ) ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P) ^ P.inertiaDeg Q =
    Int.natAbs (↑p : ℤ) ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) Q
neg₄ :
  (Int.natAbs (↑p : ℤ) ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P) ^ P.inertiaDeg Q =
    Int.natAbs (↑p : ℤ) ^ (inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P * P.inertiaDeg Q)
⊢ Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) Q : Ideal R) : ℕ)
    ((absNorm : (a : Ideal S) → ℕ) Q : ℕ)
have neg₅ : (Int.natAbs (↑p : ℤ) ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P) ^ P.inertiaDeg Q =
  (Int.natAbs (↑p : ℤ) ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P) ^ P.inertiaDeg Q
Tactic: rw [relNorm_eq_pow_of_isMaximal Q P, map_pow, absNorm_eq_pow_inertiaDeg Q hp,
      absNorm_eq_pow_inertiaDeg P hp, inertiaDeg_algebra_tower (span {(p : ℤ)}) P Q, pow_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (goal)
Goal:
S : Type u_3
inst : CommRing S
inst_1 : IsDomain S
inst_2 : IsIntegrallyClosed S
inst_3 : IsDedekindDomain S
inst_4 : Free ℤ S
inst_5 : Module.Finite ℤ S
I : Ideal S
⊢ Eq (α := Ideal ℤ) (((relNorm ℤ : Ideal S →*₀ Ideal ℤ) : (a : Ideal S) → Ideal ℤ) I : Ideal ℤ)
    (span {(↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)} : Ideal ℤ)
have rw : Eq (α := Ideal ℤ)
  (span
    {(↑((absNorm : (a : Ideal ℤ) → ℕ) (((relNorm ℤ : Ideal S →*₀ Ideal ℤ) : (a : Ideal S) → Ideal ℤ) I : Ideal ℤ)) :
        ℤ)})
  (span {(↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)})
Tactic: rw [← Int.ideal_span_absNorm_eq_self (relNorm ℤ I), absNorm_relNorm]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (goal)
Goal:
S : Type u_3
inst : CommRing S
inst_1 : IsDomain S
inst_2 : IsIntegrallyClosed S
inst_3 : IsDedekindDomain S
inst_4 : Free ℤ S
inst_5 : Module.Finite ℤ S
I : Ideal S
rw :
  Eq (α := Ideal ℤ)
    (span
      {(↑((absNorm : (a : Ideal ℤ) → ℕ) (((relNorm ℤ : Ideal S →*₀ Ideal ℤ) : (a : Ideal S) → Ideal ℤ) I : Ideal ℤ)) :
          ℤ)})
    (span {(↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)})
⊢ Eq (α := Ideal ℤ) (((relNorm ℤ : Ideal S →*₀ Ideal ℤ) : (a : Ideal S) → Ideal ℤ) I : Ideal ℤ)
    (span {(↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)} : Ideal ℤ)
have rw₁ : Eq (α := Ideal ℤ) (span {(↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)}) (span {(↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)})
Tactic: rw [← Int.ideal_span_absNorm_eq_self (relNorm ℤ I), absNorm_relNorm]
-- 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
I : Ideal R
inst_14 : Module.Finite ℤ R
⊢ (absNorm : (a : Ideal S) → ℕ) (map (F := R →+* S) (algebraMap R S) I) =
    HPow.hPow (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) I : ℕ) (finrank.{u_1, u_3} (FractionRing R) (FractionRing S))
have rw : (absNorm : (a : Ideal ℤ) → ℕ)
    (((relNorm ℤ : Ideal S →*₀ Ideal ℤ) : (a : Ideal S) → Ideal ℤ) (map (F := R →+* S) (algebraMap R S) I) : Ideal ℤ) =
  HPow.hPow (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) I : ℕ) (finrank.{u_1, u_3} (FractionRing R) (FractionRing S))
Tactic: rw [← absNorm_relNorm ℤ, ← relNorm_relNorm ℤ R, relNorm_algebraMap, absNorm_relNorm, map_pow]