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
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
pos : ∀ (hp : p = ⊥), (relNorm R : (a : Ideal S) → Ideal R) P = p ^ p.inertiaDeg P
⊢ (relNorm R : (a : Ideal S) → Ideal R) P = p ^ p.inertiaDeg P
have neg : ∀ (hp : ¬p = ⊥), (relNorm R : (a : Ideal S) → Ideal R) P = p ^ p.inertiaDeg P
Tactic: by_cases hp : 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 = ⊥
⊢ (relNorm R : (a : Ideal S) → Ideal R) P = p ^ p.inertiaDeg P
have h : p.inertiaDeg P ≠ 0
Tactic: have h : p.inertiaDeg P ≠ 0 := Nat.ne_zero_iff_zero_lt.mpr <| inertiaDeg_pos 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 : 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 = ⊥
h : p.inertiaDeg P ≠ 0
⊢ P = ⊥
have hPp₁ : LiesOver.{u_1, u_3} (A := R) P ⊥
Tactic: rw [hp] at hPp
Cleared hypotheses: hPp, inst_11, inst_12, inst_13, G, this_1, this, hp, h
-- 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 = ⊥
h : p.inertiaDeg P ≠ 0
⊢ (relNorm R : (a : Ideal S) → Ideal R) P = p ^ p.inertiaDeg P
have hP : P = ⊥
Tactic: have hP : P = ⊥ := by
      rw [hp] at hPp
      exact eq_bot_of_liesOver_bot R P
-- 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 = ⊥
h : p.inertiaDeg P ≠ 0
hP : P = ⊥
⊢ (relNorm R : (a : Ideal S) → Ideal R) P = p ^ p.inertiaDeg P
have pos : inertiaDeg.{u_1, u_3} (R := R) (S := S) ⊥ ⊥ ≠ 0
Tactic: rw [hp, hP, relNorm_bot, bot_pow]
-- 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 = ⊥
h : p.inertiaDeg P ≠ 0
hP : P = ⊥
⊢ inertiaDeg.{u_1, u_3} (R := R) (S := S) ⊥ ⊥ ≠ 0
have pos : ∀ (h : inertiaDeg.{u_1, u_3} (R := R) ⊥ P ≠ 0) (hP : P = ⊥), inertiaDeg.{u_1, u_3} (R := R) (S := S) ⊥ ⊥ ≠ 0
Tactic: rwa [hp, hP] at h
Cleared hypotheses: h, hP
-- 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 = ⊥
h : p.inertiaDeg P ≠ 0
hP : P = ⊥
pos : ∀ (h : inertiaDeg.{u_1, u_3} (R := R) ⊥ P ≠ 0) (hP : P = ⊥), inertiaDeg.{u_1, u_3} (R := R) (S := S) ⊥ ⊥ ≠ 0
⊢ inertiaDeg.{u_1, u_3} (R := R) (S := S) ⊥ ⊥ ≠ 0
have pos₁ : ∀ (h : inertiaDeg.{u_1, u_3} (R := R) (S := S) ⊥ ⊥ ≠ 0) (hP : P = ⊥), inertiaDeg.{u_1, u_3} (R := R) (S := S) ⊥ ⊥ ≠ 0
Tactic: rwa [hp, hP] at h
Cleared hypotheses: h, hP
-- 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 = ⊥
⊢ (relNorm R : (a : Ideal S) → Ideal R) P = p ^ p.inertiaDeg P
have neg : ∀ (s : ℕ) (hs : (relNorm R : (a : Ideal S) → Ideal R) P = p ^ s),
  (relNorm R : (a : Ideal S) → Ideal R) P = p ^ p.inertiaDeg P
Tactic: obtain ⟨s, hs⟩ := exists_relNorm_eq_pow_of_isPrime P p
-- 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_2 : IsGaloisGroup G R S
hp : ¬p = ⊥
s : ℕ
hs : (relNorm R : (a : Ideal S) → Ideal R) P = p ^ s
this : s = p.inertiaDeg P
⊢ (relNorm R : (a : Ideal S) → Ideal R) P = p ^ p.inertiaDeg P
have rwa : ∀ (hs : (relNorm R : (a : Ideal S) → Ideal R) P = p ^ p.inertiaDeg P) (this : s = p.inertiaDeg P),
  (relNorm R : (a : Ideal S) → Ideal R) P = p ^ p.inertiaDeg P
Tactic: rwa [this] at hs
Cleared hypotheses: hs, this
-- 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
⊢ (relNorm R : (a : Ideal S) → Ideal R) P = p ^ p.inertiaDeg P
have neg : s = p.inertiaDeg P
Tactic: suffices s = p.inertiaDeg P by rwa [this] at hs
-- 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
Q : Ideal S
hQ : 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)
have hQ₁ : Membership.mem (γ := Set (Ideal S)) (p.primesOver S) Q
Tactic: rw [Set.mem_toFinset] at hQ
Cleared hypotheses: 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
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
Q : Ideal S
hQ : Membership.mem (γ := Set (Ideal S)) (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)
have this₁ : Q.IsPrime
Tactic: have : Q.IsPrime := 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
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_2 : IsGaloisGroup G R S
hp : ¬p = ⊥
s : ℕ
hs : (relNorm R : (a : Ideal S) → Ideal R) P = p ^ s
Q : Ideal S
hQ : Membership.mem (γ := Set (Ideal S)) (p.primesOver S) Q
this : Q.IsPrime
⊢ HPow.hPow (α := Ideal R) ((relNorm R : (a : Ideal S) → Ideal R) Q : Ideal R) (p.ramificationIdx Q) =
    p ^ (p.ramificationIdxIn S * s)
have this₁ : Q.LiesOver p
Tactic: have : Q.LiesOver p := hQ.2
-- 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_2 : IsGaloisGroup G R S
hp : ¬p = ⊥
s : ℕ
hs : (relNorm R : (a : Ideal S) → Ideal R) P = p ^ s
Q : Ideal S
hQ : Membership.mem (γ := Set (Ideal S)) (p.primesOver S) Q
this_3 : Q.IsPrime
this : Q.LiesOver p
⊢ HPow.hPow (α := Ideal R) ((relNorm R : (a : Ideal S) → Ideal R) Q : Ideal R) (p.ramificationIdx Q) =
    p ^ (p.ramificationIdxIn S * s)
have rw : HPow.hPow (α := Ideal R) ((relNorm R : (a : Ideal S) → Ideal R) Q : Ideal R) (p.ramificationIdxIn S) =
  p ^ (p.ramificationIdxIn S * s)
Tactic: rw [← ramificationIdxIn_eq_ramificationIdx p Q G]
-- 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_2 : IsGaloisGroup G R S
hp : ¬p = ⊥
s : ℕ
hs : (relNorm R : (a : Ideal S) → Ideal R) P = p ^ s
Q : Ideal S
hQ : Membership.mem (γ := Set (Ideal S)) (p.primesOver S) Q
this_3 : Q.IsPrime
this : Q.LiesOver p
⊢ HPow.hPow (α := Ideal R) ((relNorm R : (a : Ideal S) → Ideal R) Q : Ideal R) (p.ramificationIdxIn S) =
    p ^ (p.ramificationIdxIn S * s)
have obtain : ∀ (σ : G) (hQ : Membership.mem (γ := Set (Ideal S)) (p.primesOver S) (σ • P)) (this : (σ • P).IsPrime)
  (this : (σ • P).LiesOver p),
  HPow.hPow (α := Ideal R) ((relNorm R : (a : Ideal S) → Ideal R) (σ • P) : Ideal R) (p.ramificationIdxIn S) =
    p ^ (p.ramificationIdxIn S * s)
Tactic: obtain ⟨σ, rfl⟩ := Ideal.exists_smul_eq_of_isGaloisGroup p P Q G
Cleared hypotheses: Q, hQ, this_3, this
-- 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_2 : IsGaloisGroup G R S
hp : ¬p = ⊥
s : ℕ
hs : (relNorm R : (a : Ideal S) → Ideal R) P = p ^ s
σ : G
hQ : Membership.mem (γ := Set (Ideal S)) (p.primesOver S) (σ • P)
this_3 : (σ • P).IsPrime
this : (σ • P).LiesOver p
⊢ HPow.hPow (α := Ideal R) ((relNorm R : (a : Ideal S) → Ideal R) (σ • P) : Ideal R) (p.ramificationIdxIn S) =
    p ^ (p.ramificationIdxIn S * s)
have rw : HPow.hPow (α := Ideal R) ((relNorm R : (a : Ideal S) → Ideal R) P : Ideal R) (p.ramificationIdxIn S) =
  p ^ (p.ramificationIdxIn S * s)
Tactic: rw [relNorm_smul, hs, ← pow_mul, mul_comm]
-- 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_2 : IsGaloisGroup G R S
hp : ¬p = ⊥
s : ℕ
hs : (relNorm R : (a : Ideal S) → Ideal R) P = p ^ s
σ : G
hQ : Membership.mem (γ := Set (Ideal S)) (p.primesOver S) (σ • P)
this_3 : (σ • P).IsPrime
this : (σ • P).LiesOver p
rw :
  HPow.hPow (α := Ideal R) ((relNorm R : (a : Ideal S) → Ideal R) P : Ideal R) (p.ramificationIdxIn S) =
    p ^ (p.ramificationIdxIn S * s)
⊢ HPow.hPow (α := Ideal R) ((relNorm R : (a : Ideal S) → Ideal R) (σ • P) : Ideal R) (p.ramificationIdxIn S) =
    p ^ (p.ramificationIdxIn S * s)
have rw₁ : (p ^ s) ^ p.ramificationIdxIn S = p ^ (p.ramificationIdxIn S * s)
Tactic: rw [relNorm_smul, hs, ← pow_mul, mul_comm]
-- 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_2 : IsGaloisGroup G R S
hp : ¬p = ⊥
s : ℕ
hs : (relNorm R : (a : Ideal S) → Ideal R) P = p ^ s
σ : G
hQ : Membership.mem (γ := Set (Ideal S)) (p.primesOver S) (σ • P)
this_3 : (σ • P).IsPrime
this : (σ • P).LiesOver p
rw :
  HPow.hPow (α := Ideal R) ((relNorm R : (a : Ideal S) → Ideal R) P : Ideal R) (p.ramificationIdxIn S) =
    p ^ (p.ramificationIdxIn S * s)
rw₁ : (p ^ s) ^ p.ramificationIdxIn S = p ^ (p.ramificationIdxIn S * s)
⊢ HPow.hPow (α := Ideal R) ((relNorm R : (a : Ideal S) → Ideal R) (σ • P) : Ideal R) (p.ramificationIdxIn S) =
    p ^ (p.ramificationIdxIn S * s)
have rw₂ : p ^ (s * p.ramificationIdxIn S) = p ^ (p.ramificationIdxIn S * s)
Tactic: rw [relNorm_smul, hs, ← pow_mul, mul_comm]
-- 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_2 : IsGaloisGroup G R S
hp : ¬p = ⊥
s : ℕ
hs : (relNorm R : (a : Ideal S) → Ideal R) P = p ^ s
σ : G
hQ : Membership.mem (γ := Set (Ideal S)) (p.primesOver S) (σ • P)
this_3 : (σ • P).IsPrime
this : (σ • P).LiesOver p
rw :
  HPow.hPow (α := Ideal R) ((relNorm R : (a : Ideal S) → Ideal R) P : Ideal R) (p.ramificationIdxIn S) =
    p ^ (p.ramificationIdxIn S * s)
rw₁ : (p ^ s) ^ p.ramificationIdxIn S = p ^ (p.ramificationIdxIn S * s)
rw₂ : p ^ (s * p.ramificationIdxIn S) = p ^ (p.ramificationIdxIn S * s)
⊢ HPow.hPow (α := Ideal R) ((relNorm R : (a : Ideal S) → Ideal R) (σ • P) : Ideal R) (p.ramificationIdxIn S) =
    p ^ (p.ramificationIdxIn S * s)
have rw₃ : p ^ (p.ramificationIdxIn S * s) = p ^ (p.ramificationIdxIn S * s)
Tactic: rw [relNorm_smul, hs, ← pow_mul, mul_comm]
-- 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
⊢ s = p.inertiaDeg P
have 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)
Tactic: have h₀ : ∀ Q ∈ (p.primesOver S).toFinset,
      relNorm R Q ^ ramificationIdx p Q = p ^ ((p.ramificationIdxIn S) * s) := by
    intro Q hQ
    rw [Set.mem_toFinset] at hQ
    have : Q.IsPrime := hQ.1
    have : Q.LiesOver p := hQ.2
    rw [← ramificationIdxIn_eq_ramificationIdx p Q G]
    obtain ⟨σ, rfl⟩ := Ideal.exists_smul_eq_of_isGaloisGroup p P Q G
    rw [relNorm_smul, hs, ← pow_mul, mul_comm]