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.IsPrime
hp : ¬p = ⊥
h :
  LE.le.{u_1} (α := Ideal R) ((relNorm R : (a : Ideal S) → Ideal R) (map (F := R →+* S) (algebraMap R S) p) : Ideal R)
    ((relNorm R : (a : Ideal S) → Ideal R) P : Ideal R)
⊢ ∃ i ≤ finrank.{u_1, u_3} (FractionRing R) (FractionRing S),
    Associated ((relNorm R : (a : Ideal S) → Ideal R) P) (p ^ i)

Tactic:
rw [relNorm_algebraMap S, ← dvd_iff_le, dvd_prime_pow (prime_of_isPrime hp inferInstance)] at h

Premises used: Ideal.dvd_iff_le, inferInstance, Ideal.relNorm_algebraMap, dvd_prime_pow, Ideal.prime_of_isPrime
-- 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.IsPrime
hp : ¬p = ⊥
h :
  ∃ i ≤ finrank.{u_1, u_3} (FractionRing R) (FractionRing S),
    Associated ((relNorm R : (a : Ideal S) → Ideal R) P) (p ^ i)
neg :
  ∀ s ≤ finrank.{u_1, u_3} (FractionRing R) (FractionRing S),
    ∀ (hs : Associated ((relNorm R : (a : Ideal S) → Ideal R) P) (p ^ s)),
      ∃ (s : ℕ), (relNorm R : (a : Ideal S) → Ideal R) P = p ^ s
⊢ ∃ (s : ℕ), (relNorm R : (a : Ideal S) → Ideal R) P = p ^ s

Tactic:
obtain ⟨s, _, hs⟩ := h
-- 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.IsPrime
hp : ¬p = ⊥
s : ℕ
left : s ≤ finrank.{u_1, u_3} (FractionRing R) (FractionRing S)
hs : Associated ((relNorm R : (a : Ideal S) → Ideal R) P) (p ^ s)
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (hs : (relNorm R : (a : Ideal S) → Ideal R) P = p ^ s), (relNorm R : (a : Ideal S) → Ideal R) P = p ^ s
⊢ (relNorm R : (a : Ideal S) → Ideal R) P = p ^ s

Tactic:
rwa [associated_iff_eq] at hs

Premises used: associated_iff_eq
-- 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.IsPrime
hp : ¬p = ⊥
s : ℕ
left : s ≤ finrank.{u_1, u_3} (FractionRing R) (FractionRing S)
hs : Associated ((relNorm R : (a : Ideal S) → Ideal R) P) (p ^ s)
⊢ ∃ (s : ℕ), (relNorm R : (a : Ideal S) → Ideal R) P = p ^ s

Tactic:
exact ⟨s, by rwa [associated_iff_eq] at hs⟩
-- 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 : MulSemiringAction Gal(FractionRing S/FractionRing R) S :=
  IsIntegralClosure.MulSemiringAction R (FractionRing R) (FractionRing S) S
⊢ IsGaloisGroup G R S

Tactic:
have := IsGaloisGroup.of_isFractionRing G R S (FractionRing R) (FractionRing 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
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
neg : ∀ (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

Tactic:
by_cases hp : 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 = ⊥
⊢ p.inertiaDeg P ≠ 0

Tactic:
have h : p.inertiaDeg P ≠ 0 := Nat.ne_zero_iff_zero_lt.mpr <| inertiaDeg_pos 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 : 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
⊢ LiesOver.{u_1, u_3} (A := R) P ⊥

Tactic:
rw [hp] at hPp
-- 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 = ⊥
h : p.inertiaDeg P ≠ 0
hPp₁ : LiesOver.{u_1, u_3} (A := R) P ⊥
⊢ p.IsMaximal

Tactic:
rw [hp] at hPp
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
Goal:
R : Type u_1
inst_1 : CommRing R
inst_2 : IsDomain R
S : Type u_3
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : IsIntegrallyClosed R
inst_6 : IsIntegrallyClosed S
inst_7 : Algebra R S
inst_8 : Module.Finite R S
inst_9 : IsTorsionFree R S
inst_10 : IsDedekindDomain R
inst_11 : IsDedekindDomain S
P : Ideal S
p : Ideal R
hPp : P.LiesOver p
inst_12 : p.IsMaximal
inst_13 : P.IsPrime
inst_14 : 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
hPp₁ : LiesOver.{u_1, u_3} (A := R) P ⊥
inst : p.IsMaximal
⊢ P.IsPrime

Tactic:
rw [hp] at hPp
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
Goal:
R : Type u_1
inst_1 : CommRing R
inst_2 : IsDomain R
S : Type u_3
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : IsIntegrallyClosed R
inst_6 : IsIntegrallyClosed S
inst_7 : Algebra R S
inst_8 : Module.Finite R S
inst_9 : IsTorsionFree R S
inst_10 : IsDedekindDomain R
inst_11 : IsDedekindDomain S
P : Ideal S
p : Ideal R
hPp : P.LiesOver p
inst_12 : p.IsMaximal
inst_13 : P.IsPrime
inst_14 : 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
hPp₁ : LiesOver.{u_1, u_3} (A := R) P ⊥
inst : p.IsMaximal
inst₁ : P.IsPrime
⊢ IsGalois.{u_1, u_3} (FractionRing R) (FractionRing S)

Tactic:
rw [hp] at hPp
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
Goal:
R : Type u_1
inst_1 : CommRing R
inst_2 : IsDomain R
S : Type u_3
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : IsIntegrallyClosed R
inst_6 : IsIntegrallyClosed S
inst_7 : Algebra R S
inst_8 : Module.Finite R S
inst_9 : IsTorsionFree R S
inst_10 : IsDedekindDomain R
inst_11 : IsDedekindDomain S
P : Ideal S
p : Ideal R
hPp : P.LiesOver p
inst_12 : p.IsMaximal
inst_13 : P.IsPrime
inst_14 : 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
hPp₁ : LiesOver.{u_1, u_3} (A := R) P ⊥
inst : p.IsMaximal
inst₁ : P.IsPrime
inst₂ : IsGalois.{u_1, u_3} (FractionRing R) (FractionRing S)
⊢ let G := Gal(FractionRing S/FractionRing R);
  let this : MulSemiringAction Gal(FractionRing S/FractionRing R) S :=
    IsIntegralClosure.MulSemiringAction R (FractionRing R) (FractionRing S) S;
  IsGaloisGroup G R S

Tactic:
rw [hp] at hPp
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
Goal:
R : Type u_1
inst_1 : CommRing R
inst_2 : IsDomain R
S : Type u_3
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : IsIntegrallyClosed R
inst_6 : IsIntegrallyClosed S
inst_7 : Algebra R S
inst_8 : Module.Finite R S
inst_9 : IsTorsionFree R S
inst_10 : IsDedekindDomain R
inst_11 : IsDedekindDomain S
P : Ideal S
p : Ideal R
hPp : P.LiesOver p
inst_12 : p.IsMaximal
inst_13 : P.IsPrime
inst_14 : 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
hPp₁ : LiesOver.{u_1, u_3} (A := R) P ⊥
inst : p.IsMaximal
inst₁ : P.IsPrime
inst₂ : IsGalois.{u_1, u_3} (FractionRing R) (FractionRing S)
this₁ :
  let G := Gal(FractionRing S/FractionRing R);
  let this : MulSemiringAction Gal(FractionRing S/FractionRing R) S :=
    IsIntegralClosure.MulSemiringAction R (FractionRing R) (FractionRing S) S;
  IsGaloisGroup G R S
⊢ p = ⊥

Tactic:
rw [hp] at hPp
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
Goal:
R : Type u_1
inst_1 : CommRing R
inst_2 : IsDomain R
S : Type u_3
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : IsIntegrallyClosed R
inst_6 : IsIntegrallyClosed S
inst_7 : Algebra R S
inst_8 : Module.Finite R S
inst_9 : IsTorsionFree R S
inst_10 : IsDedekindDomain R
inst_11 : IsDedekindDomain S
P : Ideal S
p : Ideal R
hPp : P.LiesOver p
inst_12 : p.IsMaximal
inst_13 : P.IsPrime
inst_14 : 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
hPp₁ : LiesOver.{u_1, u_3} (A := R) P ⊥
inst : p.IsMaximal
inst₁ : P.IsPrime
inst₂ : IsGalois.{u_1, u_3} (FractionRing R) (FractionRing S)
this₁ :
  let G := Gal(FractionRing S/FractionRing R);
  let this : MulSemiringAction Gal(FractionRing S/FractionRing R) S :=
    IsIntegralClosure.MulSemiringAction R (FractionRing R) (FractionRing S) S;
  IsGaloisGroup G R S
hp₁ : p = ⊥
⊢ p.inertiaDeg P ≠ 0

Tactic:
rw [hp] at hPp
-- 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 : LiesOver.{u_1, u_3} (A := R) 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 = ⊥

Tactic:
eq_bot_of_liesOver_bot R P

Premises used: Ideal.eq_bot_of_liesOver_bot
-- 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 : LiesOver.{u_1, u_3} (A := R) 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 = ⊥

Tactic:
exact eq_bot_of_liesOver_bot R P

Premises used: Ideal.eq_bot_of_liesOver_bot
-- 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 = ⊥
h : p.inertiaDeg P ≠ 0
⊢ P = ⊥

Tactic:
have hP : P = ⊥ := by
      rw [hp] at hPp
      exact eq_bot_of_liesOver_bot R 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 = ⊥
h : p.inertiaDeg P ≠ 0
hP : P = ⊥
pos : inertiaDeg.{u_1, u_3} (R := R) (S := S) ⊥ ⊥ ≠ 0
⊢ (relNorm R : (a : Ideal S) → Ideal R) P = p ^ p.inertiaDeg P

Tactic:
rw [hp, hP, relNorm_bot, bot_pow]

Premises used: Ideal.bot_pow, Ideal.relNorm_bot
-- 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 = ⊥
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
pos₁ pos₂ pos₃ pos₄ :
  ∀ (h : inertiaDeg.{u_1, u_3} (R := R) (S := S) ⊥ ⊥ ≠ 0) (hP : P = ⊥), inertiaDeg.{u_1, u_3} (R := R) (S := S) ⊥ ⊥ ≠ 0
⊢ inertiaDeg.{u_1, u_3} (R := R) (S := S) ⊥ ⊥ ≠ 0

Tactic:
rwa [hp, hP] at h
-- 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 = ⊥
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
⊢ (relNorm R : (a : Ideal S) → Ideal R) P = p ^ p.inertiaDeg P

Tactic:
obtain ⟨s, hs⟩ := exists_relNorm_eq_pow_of_isPrime P p

Premises used: Ideal.exists_relNorm_eq_pow_of_isPrime
-- 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
this : s = p.inertiaDeg P
rwa rwa₁ rwa₂ 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
⊢ (relNorm R : (a : Ideal S) → Ideal R) P = p ^ p.inertiaDeg P

Tactic:
rwa [this] at hs
-- 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
neg : s = p.inertiaDeg P
⊢ (relNorm R : (a : Ideal S) → Ideal R) P = p ^ p.inertiaDeg P

Tactic:
suffices s = p.inertiaDeg P by rwa [this] at hs
-- 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
hQ : Membership.mem (γ := Finset (Ideal S)) (Set.toFinset (p.primesOver S)) Q
⊢ Membership.mem (γ := Set (Ideal S)) (p.primesOver S) Q

Tactic:
rw [Set.mem_toFinset] at hQ

Premises used: Set.mem_toFinset
-- 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
hQ : Membership.mem (γ := Set (Ideal S)) (p.primesOver S) Q
⊢ Q.IsPrime

Tactic:
have : Q.IsPrime := hQ.1
-- 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 : Q.IsPrime
⊢ Q.LiesOver p

Tactic:
have : Q.LiesOver p := hQ.2