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
inst_11 : Free ℤ R
inst_12 : Free ℤ S
inst_13 : Module.Finite ℤ S
inst_14 : PerfectField.{u_1} (FractionRing R)
I : Ideal S
this : Module.Finite ℤ R
hI : ¬I = ⊥
neg :
  Eq (α := ℕ)
    ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) (normalizedFactors I).prod : Ideal R) : ℕ)
    ((absNorm : (a : Ideal S) → ℕ) (normalizedFactors I).prod : ℕ)
⊢ Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) I : Ideal R) : ℕ)
    ((absNorm : (a : Ideal S) → ℕ) I : ℕ)

Tactic:
rw [← prod_normalizedFactors_eq_self hI]

Premises used: Ideal.prod_normalizedFactors_eq_self
-- 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) (normalizedFactors I).prod : Ideal R) : ℕ)
    ((absNorm : (a : Ideal S) → ℕ) (normalizedFactors I).prod : ℕ)

Tactic:
Multiset.prod_induction (fun I ↦ absNorm (relNorm R I) = absNorm I) _ ?_ ?_ ?_

Premises used: Multiset.prod_induction, Ideal.absNorm, Ideal.relNorm, Eq, DFunLike.coe
-- 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 = ⊥
neg :
  ∀ (a b : Ideal S),
    (fun (I : Ideal S) ↦
          Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) I : Ideal R) : ℕ)
            ((absNorm : (a : Ideal S) → ℕ) I : ℕ))
        a →
      (fun (I : Ideal S) ↦
            Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) I : Ideal R) : ℕ)
              ((absNorm : (a : Ideal S) → ℕ) I : ℕ))
          b →
        (fun (I : Ideal S) ↦
            Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) I : Ideal R) : ℕ)
              ((absNorm : (a : Ideal S) → ℕ) I : ℕ))
          (a * b)
neg₁ :
  Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) 1) : ℕ)
    ((absNorm : (a : Ideal S) → ℕ) 1 : ℕ)
neg₂ :
  ∀ a ∈ normalizedFactors I,
    (fun (I : Ideal S) ↦
        Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) I : Ideal R) : ℕ)
          ((absNorm : (a : Ideal S) → ℕ) I : ℕ))
      a
⊢ Eq (α := ℕ)
    ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) (normalizedFactors I).prod : Ideal R) : ℕ)
    ((absNorm : (a : Ideal S) → ℕ) (normalizedFactors I).prod : ℕ)

Tactic:
refine Multiset.prod_induction (fun I ↦ absNorm (relNorm R I) = absNorm I) _ ?_ ?_ ?_

Premises used: Multiset.prod_induction, Ideal.absNorm, Ideal.relNorm, Eq, DFunLike.coe
-- 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 = ⊥
a : Ideal S
neg :
  ∀ (b : Ideal S),
    (fun (I : Ideal S) ↦
          Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) I : Ideal R) : ℕ)
            ((absNorm : (a : Ideal S) → ℕ) I : ℕ))
        a →
      (fun (I : Ideal S) ↦
            Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) I : Ideal R) : ℕ)
              ((absNorm : (a : Ideal S) → ℕ) I : ℕ))
          b →
        (fun (I : Ideal S) ↦
            Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) I : Ideal R) : ℕ)
              ((absNorm : (a : Ideal S) → ℕ) I : ℕ))
          (a * b)
⊢ ∀ (b : Ideal S),
    (fun (I : Ideal S) ↦
          Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) I : Ideal R) : ℕ)
            ((absNorm : (a : Ideal S) → ℕ) I : ℕ))
        a →
      (fun (I : Ideal S) ↦
            Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) I : Ideal R) : ℕ)
              ((absNorm : (a : Ideal S) → ℕ) I : ℕ))
          b →
        (fun (I : Ideal S) ↦
            Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) I : Ideal R) : ℕ)
              ((absNorm : (a : Ideal S) → ℕ) I : ℕ))
          (a * b)

Tactic:
_
-- 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 = ⊥
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 : ℕ)
neg₄ 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 : ℕ)
⊢ Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) (a * b) : Ideal R) : ℕ)
    ((absNorm : (a : Ideal S) → ℕ) (a * b) : ℕ)

Tactic:
rw [map_mul, map_mul, map_mul, hx, hy]

Premises used: map_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
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 = ⊥
⊢ (fun (I : Ideal S) ↦
      Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) ((relNorm R : (a : Ideal S) → Ideal R) I : Ideal R) : ℕ)
        ((absNorm : (a : Ideal S) → ℕ) I : ℕ))
    1

Tactic:
simp
-- 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 = ⊥
Q : Ideal S
hQ : Q ∈ normalizedFactors I
⊢ Q ≠ ⊥

Tactic:
have hQ' : Q ≠ ⊥ := ne_zero_of_mem_normalizedFactors hQ
-- 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 = ⊥
Q : Ideal S
hQ : Q ∈ normalizedFactors I
hQ' : Q ≠ ⊥
⊢ Q.IsPrime ∧ I ≤ Q

Tactic:
rw [Ideal.mem_normalizedFactors_iff hI] at hQ

Premises used: Ideal.mem_normalizedFactors_iff
-- 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 = ⊥
Q : Ideal S
hQ : Q ∈ normalizedFactors I
hQ' : Q ≠ ⊥
hQ₁ : Q.IsPrime ∧ I ≤ Q
⊢ Q ≠ ⊥

Tactic:
rw [Ideal.mem_normalizedFactors_iff hI] at hQ

Premises used: Ideal.mem_normalizedFactors_iff
-- 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 = ⊥
Q : Ideal S
hQ : Q.IsPrime ∧ I ≤ Q
hQ' : Q ≠ ⊥
⊢ Q.IsMaximal

Tactic:
have : Q.IsMaximal := Ring.DimensionLEOne.maximalOfPrime hQ' 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
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)
⊢ NeZero P

Tactic:
have : NeZero P := ⟨under_ne_bot R hQ'⟩
-- 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_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
⊢ Q.LiesOver P

Tactic:
simp [liesOver_iff, P]

Premises used: Ideal.liesOver_iff
-- 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_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
⊢ Q.LiesOver P

Tactic:
have : Q.LiesOver P := by simp [liesOver_iff, 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
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
⊢ Q.LiesOver (A := ℤ) (span {(↑p : ℤ)})

Tactic:
have : Q.LiesOver (span {(p : ℤ)}) := LiesOver.trans 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
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 : ℤ)})
⊢ Fact (Nat.Prime p)

Tactic:
have : Fact (p.Prime) := ⟨Nat.absNorm_under_prime _⟩
-- 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_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)
⊢ Prime (M := ℤ) (↑p : ℤ)

Tactic:
have hp : Prime (p : ℤ) := Nat.prime_iff_prime_int.mp <| Nat.absNorm_under_prime _
-- 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_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)
neg₅ 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 : ℕ)

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]

Premises used: map_pow, Nat.cast, pow_mul, Ideal.inertiaDeg_algebra_tower, Ideal.span, Ideal.absNorm_eq_pow_inertiaDeg, Singleton.singleton, Ideal.relNorm_eq_pow_of_isMaximal
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
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) : ℤ)})
rw₁ rw₂ :
  Eq (α := Ideal ℤ) (span {(↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)}) (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 ℤ)

Tactic:
rw [← Int.ideal_span_absNorm_eq_self (relNorm ℤ I), absNorm_relNorm]

Premises used: Int, Ideal.relNorm, Int.ideal_span_absNorm_eq_self, Ideal.absNorm_relNorm, DFunLike.coe
-- 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
I : Ideal R
inst_14 : Module.Finite ℤ R
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))
rw₁ :
  (absNorm : (a : Ideal ℤ) → ℕ)
      (((relNorm ℤ : Ideal R →*₀ Ideal ℤ) : (a : Ideal R) → Ideal ℤ)
          ((relNorm R : (a : Ideal S) → Ideal R) (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))
rw₂ :
  (absNorm : (a : Ideal ℤ) → ℕ)
      (((relNorm ℤ : Ideal R →*₀ Ideal ℤ) : (a : Ideal R) → Ideal ℤ)
          (I ^ finrank.{u_1, u_3} (FractionRing R) (FractionRing S)) :
        Ideal ℤ) =
    HPow.hPow (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) I : ℕ) (finrank.{u_1, u_3} (FractionRing R) (FractionRing S))
rw₃ :
  (absNorm : (a : Ideal R) → ℕ) (I ^ finrank.{u_1, u_3} (FractionRing R) (FractionRing S)) =
    HPow.hPow (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) I : ℕ) (finrank.{u_1, u_3} (FractionRing R) (FractionRing S))
rw₄ rw₅ :
  HPow.hPow (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) I : ℕ) (finrank.{u_1, u_3} (FractionRing R) (FractionRing S)) =
    HPow.hPow (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) I : ℕ) (finrank.{u_1, u_3} (FractionRing R) (FractionRing S))
⊢ (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))

Tactic:
rw [← absNorm_relNorm ℤ, ← relNorm_relNorm ℤ R, relNorm_algebraMap, absNorm_relNorm, map_pow]

Premises used: Ideal.relNorm_relNorm, Int, map_pow, Ideal.relNorm_algebraMap, Ideal.absNorm_relNorm
-- Module: Mathlib.RingTheory.Ideal.Oka
Goal:
R : Type u_1
inst : CommSemiring R
P : Ideal R → Prop
hP : IsOka P
I : Ideal R
hI : Maximal (fun (x : Ideal R) ↦ ¬P x) I
by_contra! : ∀ (a b : R) (hab : a * b ∈ I) (ha : a ∉ I) (hb : b ∉ I), False
⊢ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I

Tactic:
by_contra! ⟨a, b, hab, ha, hb⟩
-- Module: Mathlib.RingTheory.Ideal.Oka
Goal:
R : Type u_1
inst : CommSemiring R
P : Ideal R → Prop
hP : IsOka P
I : Ideal R
hI : Maximal (fun (x : Ideal R) ↦ ¬P x) I
a b : R
hab : a * b ∈ I
ha : a ∉ I
hb : b ∉ I
⊢ P (I ⊔ span {a})

Tactic:
have h₁ : P (I ⊔ span {a}) := of_not_not <| hI.not_prop_of_gt (Submodule.lt_sup_iff_notMem.2 ha)
-- Module: Mathlib.RingTheory.Ideal.Oka
Goal:
R : Type u_1
inst : CommSemiring R
P : Ideal R → Prop
hP : IsOka P
I : Ideal R
hI : Maximal (fun (x : Ideal R) ↦ ¬P x) I
a b : R
hab : a * b ∈ I
ha : a ∉ I
hb : b ∉ I
h₁ : P (I ⊔ span {a})
⊢ P (Submodule.colon I (↑(span {a}) : Set R))

Tactic:
have h₂ : P (I.colon (span {a})) := of_not_not <| hI.not_prop_of_gt <| lt_of_le_of_ne le_colon
      (fun H ↦ hb <| H ▸ mem_colon_span_singleton.2 (mul_comm a b ▸ hab))
-- Module: Mathlib.RingTheory.Ideal.Oka
Goal:
R : Type u_1
inst : CommSemiring R
P : Ideal R → Prop
hP : IsOka P
I : Ideal R
hI : Maximal (fun (x : Ideal R) ↦ ¬P x) I
a b : R
hab : a * b ∈ I
ha : a ∉ I
hb : b ∉ I
h₁ : P (I ⊔ span {a})
h₂ : P (Submodule.colon I (↑(span {a}) : Set R))
⊢ False

Tactic:
hI.prop (hP.oka h₁ h₂)

Premises used: Maximal.prop, Ideal.IsOka.oka
-- Module: Mathlib.RingTheory.Ideal.Oka
Goal:
R : Type u_1
inst : CommSemiring R
P : Ideal R → Prop
hP : IsOka P
I : Ideal R
hI : Maximal (fun (x : Ideal R) ↦ ¬P x) I
a b : R
hab : a * b ∈ I
ha : a ∉ I
hb : b ∉ I
h₁ : P (I ⊔ span {a})
h₂ : P (Submodule.colon I (↑(span {a}) : Set R))
⊢ False

Tactic:
exact hI.prop (hP.oka h₁ h₂)

Premises used: Maximal.prop, Ideal.IsOka.oka
-- Module: Mathlib.RingTheory.Ideal.Oka
Goal:
R : Type u_1
inst : CommSemiring R
P : Ideal R → Prop
hP : IsOka P
hmax : ∀ (I : Ideal R), ¬P I → ∃ (I : Ideal R), Maximal (fun (x : Ideal R) ↦ ¬P x) I
hprime : ∀ (I : Ideal R), I.IsPrime → P I
I : Ideal R
by_contra : ∀ (hI : ¬P I), False
⊢ P I

Tactic:
by_contra hI
-- Module: Mathlib.RingTheory.Ideal.Oka
Goal:
R : Type u_1
inst : CommSemiring R
P : Ideal R → Prop
hP : IsOka P
hmax : ∀ (I : Ideal R), ¬P I → ∃ (I : Ideal R), Maximal (fun (x : Ideal R) ↦ ¬P x) I
hprime : ∀ (I : Ideal R), I.IsPrime → P I
I : Ideal R
hI : ¬P I
obtain : ∀ (I : Ideal R) (hI : Maximal (fun (x : Ideal R) ↦ ¬P x) I), False
⊢ False

Tactic:
obtain ⟨I, hI⟩ := hmax I hI