awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
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
rw :
  HPow.hPow (α := Ideal R) ((relNorm R : (a : Ideal S) → Ideal R) Q : Ideal R) (p.ramificationIdxIn S) =
    p ^ (p.ramificationIdxIn S * s)
⊢ HPow.hPow (α := Ideal R) ((relNorm R : (a : Ideal S) → Ideal R) Q : Ideal R) (p.ramificationIdx Q) =
    p ^ (p.ramificationIdxIn S * s)

Tactic:
rw [← ramificationIdxIn_eq_ramificationIdx p Q G]

Premises used: Ideal.ramificationIdxIn_eq_ramificationIdx
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
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
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)
⊢ HPow.hPow (α := Ideal R) ((relNorm R : (a : Ideal S) → Ideal R) Q : Ideal R) (p.ramificationIdxIn S) =
    p ^ (p.ramificationIdxIn S * s)

Tactic:
obtain ⟨σ, rfl⟩ := Ideal.exists_smul_eq_of_isGaloisGroup p P Q G

Premises used: Ideal.exists_smul_eq_of_isGaloisGroup, rfl
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
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)
rw₃ rw₄ : p ^ (p.ramificationIdxIn S * 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)

Tactic:
rw [relNorm_smul, hs, ← pow_mul, mul_comm]

Premises used: Ideal.relNorm_smul, pow_mul, mul_comm
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
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),
    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]
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
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)
⊢ (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
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
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)
⊢ 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

Premises used: map_pow, Finset.prod_const, map_prod, pow_mul
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
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)
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
⊢ s = p.inertiaDeg P

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

Premises used: IsDedekindDomain.primesOver_ncard_ne_zero, Function.Injective.eq_iff, FractionRing, IsLeftCancelMulZero.mul_left_cancel_of_ne_zero, Ideal.ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn, Set.ncard_eq_toFinset_card', IsLeftRegular.pow_injective, Ideal.ramificationIdxIn_ne_zero, mul_comm, Ideal.inertiaDegIn_eq_inertiaDeg, mul_right_inj', IsGaloisGroup.card_eq_finrank
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
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))
rw : p ≠ ⊤
⊢ p ≠ 1

Tactic:
rw [one_eq_top]

Premises used: Ideal.one_eq_top
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
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 ≠ ⊤

Tactic:
IsMaximal.ne_top inferInstance

Premises used: inferInstance, Ideal.IsMaximal.ne_top
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
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 ≠ ⊤

Tactic:
exact IsMaximal.ne_top inferInstance

Premises used: inferInstance, Ideal.IsMaximal.ne_top
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
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), Q.IsMaximal ∧ Q.LiesOver P

Tactic:
exists_maximal_ideal_liesOver_of_isIntegral P

Premises used: Ideal.exists_maximal_ideal_liesOver_of_isIntegral
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
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
obtain :
  ∀ (Q : Ideal T) (hQ₁ : Q.IsMaximal) (hQ₂ : Q.LiesOver 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

Tactic:
obtain ⟨Q, hQ₁, hQ₂⟩ : ∃ Q : Ideal T, Q.IsMaximal ∧ Q.LiesOver P :=
    exists_maximal_ideal_liesOver_of_isIntegral P

Premises used: Ideal.exists_maximal_ideal_liesOver_of_isIntegral, Ideal
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
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
⊢ Q.LiesOver p

Tactic:
have : Q.LiesOver p := LiesOver.trans Q P p
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
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 T) → Ideal R) Q = p ^ p.inertiaDeg Q

Tactic:
have h := relNorm_eq_pow_of_isPrime_isGalois Q p
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
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
⊢ 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)
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
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)
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
⊢ (relNorm R : (a : Ideal S) → Ideal R) P = p ^ p.inertiaDeg P

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

Premises used: Ideal.relNorm_relNorm, Ideal.relNorm_eq_pow_of_isPrime_isGalois, map_pow, pow_left_inj, pow_mul, Ideal.inertiaDeg_algebra_tower
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
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 :
  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:
Nat.ne_zero_iff_zero_lt.mpr <| inertiaDeg_pos P Q

Premises used: Iff.mpr, Nat.ne_zero_iff_zero_lt, Ideal.inertiaDeg_pos
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
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 :
  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:
exact Nat.ne_zero_iff_zero_lt.mpr <| inertiaDeg_pos P Q

Premises used: Iff.mpr, Nat.ne_zero_iff_zero_lt, Ideal.inertiaDeg_pos
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
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
⊢ Module.Finite ℤ R

Tactic:
have : Module.Finite ℤ R := Module.Finite.left ℤ R S
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
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 : ℕ)
neg :
  ∀ (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 : ℕ)

Tactic:
by_cases hI : I = ⊥
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
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 : ℕ)

Tactic:
simp [hI]