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
I_1 J : Ideal S
inst_11 : Nontrivial R
h : Nontrivial S
hP : IsMaximal.{u_1} (α := R) ⊥
I : Ideal R
⊢ I = ⊥ ∨ I = ⊤

Tactic:
or_iff_not_imp_right.mpr fun hI ↦ (hP.eq_of_le hI bot_le).symm

Premises used: Iff.mpr, Classical.or_iff_not_imp_right, Ideal.IsMaximal.eq_of_le, Eq.symm, bot_le
-- 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
I_1 J : Ideal S
inst_11 : Nontrivial R
h : Nontrivial S
hP : IsMaximal.{u_1} (α := R) ⊥
I : Ideal R
⊢ I = ⊥ ∨ I = ⊤

Tactic:
exact or_iff_not_imp_right.mpr fun hI ↦ (hP.eq_of_le hI bot_le).symm

Premises used: Iff.mpr, Classical.or_iff_not_imp_right, Ideal.IsMaximal.eq_of_le, Eq.symm, bot_le
-- 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
I J : Ideal S
inst_11 : Nontrivial R
h : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
⊢ NeZero P

Tactic:
have : NeZero P := ⟨hP0⟩
-- 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
I J : Ideal S
inst_11 : Nontrivial R
h : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
this : NeZero P
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
neg :
  spanNorm (Localization.AtPrime P)
      (HMul.hMul (α := Ideal (Localization (M := S) P'))
        (map (F := S →+* Localization (M := S) P') (algebraMap S (Localization (M := S) P')) I)
        (map (F := S →+* Localization (M := S) P') (algebraMap S (Localization (M := S) P')) J)) =
    HMul.hMul (α := Ideal (Localization.AtPrime P))
      (spanNorm (Localization.AtPrime P) (S := Localization (M := S) P')
        (map (F := S →+* Localization (M := S) P') (algebraMap S (Localization (M := S) P')) I))
      (spanNorm (Localization.AtPrime P) (S := Localization (M := S) P')
        (map (F := S →+* Localization (M := S) P') (algebraMap S (Localization (M := S) P')) J))
⊢ Eq (α := Ideal (Localization.AtPrime P))
    (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P)) (spanNorm R (I * J)))
    (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P))
      (HMul.hMul (α := Ideal R) (spanNorm R I) (spanNorm R J)))

Tactic:
simp only [Ideal.map_mul, ← spanIntNorm_localization (R := R) (Sₘ := Localization P')
    _ _ P.primeCompl_le_nonZeroDivisors]

Premises used: Ideal.spanIntNorm_localization, Ideal.map_mul, Localization, Ideal.primeCompl_le_nonZeroDivisors
-- 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
T : Type u_4
inst_9 : CommRing T
inst_10 : IsDomain T
inst_11 : IsIntegrallyClosed T
inst_12 : Algebra R T
inst_13 : Algebra T S
inst_14 : Module.Finite R T
inst_15 : Module.Finite T S
inst_16 : IsTorsionFree R T
inst_17 : IsTorsionFree T S
inst_18 : IsScalarTower R T S
I : Ideal S
⊢ LE.le.{u_1} (α := Ideal R) (span ((⇑(intNorm R S) : (a : S) → R) '' (↑I : Set S)))
    (span ((⇑(intNorm R T) : (a : T) → R) '' (↑(span ((⇑(intNorm T S) : (a : S) → T) '' (↑I : Set S))) : Set T)))

Tactic:
span_mono ?_

Premises used: Ideal.span_mono
-- 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
T : Type u_4
inst_9 : CommRing T
inst_10 : IsDomain T
inst_11 : IsIntegrallyClosed T
inst_12 : Algebra R T
inst_13 : Algebra T S
inst_14 : Module.Finite R T
inst_15 : Module.Finite T S
inst_16 : IsTorsionFree R T
inst_17 : IsTorsionFree T S
inst_18 : IsScalarTower R T S
I : Ideal S
refine :
  Subset.{u_1} (α := Set R) ((⇑(intNorm R S) : (a : S) → R) '' (↑I : Set S))
    ((⇑(intNorm R T) : (a : T) → R) '' (↑(span ((⇑(intNorm T S) : (a : S) → T) '' (↑I : Set S))) : Set T))
⊢ LE.le.{u_1} (α := Ideal R) (span ((⇑(intNorm R S) : (a : S) → R) '' (↑I : Set S)))
    (span ((⇑(intNorm R T) : (a : T) → R) '' (↑(span ((⇑(intNorm T S) : (a : S) → T) '' (↑I : Set S))) : Set T)))

Tactic:
refine span_mono ?_

Premises used: Ideal.span_mono
-- 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
T : Type u_4
inst_9 : CommRing T
inst_10 : IsDomain T
inst_11 : IsIntegrallyClosed T
inst_12 : Algebra R T
inst_13 : Algebra T S
inst_14 : Module.Finite R T
inst_15 : Module.Finite T S
inst_16 : IsTorsionFree R T
inst_17 : IsTorsionFree T S
inst_18 : IsScalarTower R T S
I : Ideal S
x : S
hx : x ∈ (↑I : Set S)
rw rw₁ : Eq.{u_1 + 1} (α := R) ((intNorm R S : (a : S) → R) x : R) ((intNorm R S : (a : S) → R) x : R)
⊢ Eq.{u_1 + 1} (α := R) ((intNorm R T : (a : T) → R) ((intNorm T S : (a : S) → T) x : T) : R)
    ((intNorm R S : (a : S) → R) x : R)

Tactic:
rw [intNorm_intNorm]

Premises used: Algebra.intNorm_intNorm
-- 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
T : Type u_4
inst_9 : CommRing T
inst_10 : IsDomain T
inst_11 : IsIntegrallyClosed T
inst_12 : Algebra R T
inst_13 : Algebra T S
inst_14 : Module.Finite R T
inst_15 : Module.Finite T S
inst_16 : IsTorsionFree R T
inst_17 : IsTorsionFree T S
inst_18 : IsScalarTower R T S
I : Ideal S
x : S
hx : x ∈ (↑I : Set S)
⊢ Membership.mem.{u_1, u_1} (α := R) (γ := Set R)
    ((⇑(intNorm R T) : (a : T) → R) '' (↑(span ((⇑(intNorm T S) : (a : S) → T) '' (↑I : Set S))) : Set T))
    ((intNorm R S : (a : S) → R) x : R)

Tactic:
exact ⟨intNorm T S x, subset_span <| Set.mem_image_of_mem _ hx, by rw [intNorm_intNorm]⟩
-- 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
T : Type u_4
inst_9 : CommRing T
inst_10 : IsDomain T
inst_11 : IsIntegrallyClosed T
inst_12 : Algebra R T
inst_13 : Algebra T S
inst_14 : Module.Finite R T
inst_15 : Module.Finite T S
inst_16 : IsTorsionFree R T
inst_17 : IsTorsionFree T S
inst_18 : IsScalarTower R T S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I : Ideal S
inl : ∀ (h : Eq (α := Ideal R) (spanNorm R I) ⊥), Eq (α := Ideal R) (spanNorm R (spanNorm T I)) (spanNorm R I)
inr : ∀ (h : Eq (α := Ideal R) (spanNorm R I) ⊤), Eq (α := Ideal R) (spanNorm R (spanNorm T I)) (spanNorm R I)
⊢ Eq (α := Ideal R) (spanNorm R (spanNorm T I)) (spanNorm R I)

Tactic:
obtain h | h := eq_bot_or_top (spanNorm R I)

Premises used: Ideal.spanNorm
-- 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
T : Type u_4
inst_9 : CommRing T
inst_10 : IsDomain T
inst_11 : IsIntegrallyClosed T
inst_12 : Algebra R T
inst_13 : Algebra T S
inst_14 : Module.Finite R T
inst_15 : Module.Finite T S
inst_16 : IsTorsionFree R T
inst_17 : IsTorsionFree T S
inst_18 : IsScalarTower R T S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I : Ideal S
h : Eq (α := Ideal R) (spanNorm R I) ⊥
inl : Eq (α := Ideal R) (spanNorm R (spanNorm T I)) ⊥
inl₁ : Eq (α := Ideal T) (spanNorm T I) ⊥
inl₂ : I = ⊥
inl₃ inl₄ : Eq.{u_3 + 1} (α := Ideal S) ⊥ ⊥
⊢ Eq (α := Ideal R) (spanNorm R (spanNorm T I)) (spanNorm R I)

Tactic:
rw [h, spanNorm_eq_bot_iff, spanNorm_eq_bot_iff, spanNorm_eq_bot_iff.mp h]

Premises used: Iff.mp, Ideal.spanNorm_eq_bot_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
T : Type u_4
inst_9 : CommRing T
inst_10 : IsDomain T
inst_11 : IsIntegrallyClosed T
inst_12 : Algebra R T
inst_13 : Algebra T S
inst_14 : Module.Finite R T
inst_15 : Module.Finite T S
inst_16 : IsTorsionFree R T
inst_17 : IsTorsionFree T S
inst_18 : IsScalarTower R T S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I : Ideal S
h : Eq (α := Ideal R) (spanNorm R I) ⊤
⊢ Eq (α := Ideal R) (spanNorm R (spanNorm T I)) (spanNorm R I)

Tactic:
exact h ▸ (eq_top_iff_one _).mpr <| le_spanNorm_spanNorm R T I <| (eq_top_iff_one _).mp h

Premises used: Ideal.le_spanNorm_spanNorm, Ideal.eq_top_iff_one, Iff.mp
-- 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
T : Type u_4
inst_9 : CommRing T
inst_10 : IsDomain T
inst_11 : IsIntegrallyClosed T
inst_12 : Algebra R T
inst_13 : Algebra T S
inst_14 : Module.Finite R T
inst_15 : Module.Finite T S
inst_16 : IsTorsionFree R T
inst_17 : IsTorsionFree T S
inst_18 : IsScalarTower R T S
inst_19 : IsDedekindDomain R
inst_20 : IsDedekindDomain T
inst_21 : IsDedekindDomain S
I : Ideal S
⊢ Eq (α := Ideal R) (spanNorm R (spanNorm T I)) (spanNorm R I)

Tactic:
eq_of_localization_maximal fun P hP ↦ ?_

Premises used: Ideal.eq_of_localization_maximal
-- 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
T : Type u_4
inst_9 : CommRing T
inst_10 : IsDomain T
inst_11 : IsIntegrallyClosed T
inst_12 : Algebra R T
inst_13 : Algebra T S
inst_14 : Module.Finite R T
inst_15 : Module.Finite T S
inst_16 : IsTorsionFree R T
inst_17 : IsTorsionFree T S
inst_18 : IsScalarTower R T S
inst_19 : IsDedekindDomain R
inst_20 : IsDedekindDomain T
inst_21 : IsDedekindDomain S
I : Ideal S
refine :
  ∀ (P : Ideal R) (hP : P.IsMaximal),
    Eq (α := Ideal (Localization.AtPrime P))
      (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P)) (spanNorm R (spanNorm T I)))
      (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P)) (spanNorm R I))
⊢ Eq (α := Ideal R) (spanNorm R (spanNorm T I)) (spanNorm R I)

Tactic:
refine eq_of_localization_maximal fun P hP ↦ ?_

Premises used: Ideal.eq_of_localization_maximal
-- 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
T : Type u_4
inst_9 : CommRing T
inst_10 : IsDomain T
inst_11 : IsIntegrallyClosed T
inst_12 : Algebra R T
inst_13 : Algebra T S
inst_14 : Module.Finite R T
inst_15 : Module.Finite T S
inst_16 : IsTorsionFree R T
inst_17 : IsTorsionFree T S
inst_18 : IsScalarTower R T S
inst_19 : IsDedekindDomain R
inst_20 : IsDedekindDomain T
inst_21 : IsDedekindDomain S
I : Ideal S
P : Ideal R
hP : P.IsMaximal
pos :
  ∀ (hP_1 : P = ⊥),
    Eq (α := Ideal (Localization.AtPrime P))
      (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P)) (spanNorm R (spanNorm T I)))
      (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P)) (spanNorm R I))
neg :
  ∀ (hP_1 : ¬P = ⊥),
    Eq (α := Ideal (Localization.AtPrime P))
      (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P)) (spanNorm R (spanNorm T I)))
      (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P)) (spanNorm R I))
⊢ Eq (α := Ideal (Localization.AtPrime P))
    (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P)) (spanNorm R (spanNorm T I)))
    (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P)) (spanNorm R I))

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
T : Type u_4
inst_9 : CommRing T
inst_10 : IsDomain T
inst_11 : IsIntegrallyClosed T
inst_12 : Algebra R T
inst_13 : Algebra T S
inst_14 : Module.Finite R T
inst_15 : Module.Finite T S
inst_16 : IsTorsionFree R T
inst_17 : IsTorsionFree T S
inst_18 : IsScalarTower R T S
inst_19 : IsDedekindDomain R
inst_20 : IsDedekindDomain T
inst_21 : IsDedekindDomain S
I : Ideal S
P : Ideal R
hP_1 : P.IsMaximal
hP : P = ⊥
pos :
  ∀ (hP : IsMaximal.{u_1} (α := R) ⊥),
    Eq (α := Ideal (Localization.AtPrime (R := R) ⊥))
      (map (F := R →+* Localization.AtPrime (R := R) ⊥) (algebraMap R (Localization.AtPrime (R := R) ⊥))
        (spanNorm R (spanNorm T I)))
      (map (F := R →+* Localization.AtPrime (R := R) ⊥) (algebraMap R (Localization.AtPrime (R := R) ⊥)) (spanNorm R I))
⊢ Eq (α := Ideal (Localization.AtPrime P))
    (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P)) (spanNorm R (spanNorm T I)))
    (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P)) (spanNorm R I))

Tactic:
subst hP
-- 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
T : Type u_4
inst_9 : CommRing T
inst_10 : IsDomain T
inst_11 : IsIntegrallyClosed T
inst_12 : Algebra R T
inst_13 : Algebra T S
inst_14 : Module.Finite R T
inst_15 : Module.Finite T S
inst_16 : IsTorsionFree R T
inst_17 : IsTorsionFree T S
inst_18 : IsScalarTower R T S
inst_19 : IsDedekindDomain R
inst_20 : IsDedekindDomain T
inst_21 : IsDedekindDomain S
I : Ideal S
hP : IsMaximal.{u_1} (α := R) ⊥
pos : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
⊢ Eq (α := Ideal (Localization.AtPrime (R := R) ⊥))
    (map (F := R →+* Localization.AtPrime (R := R) ⊥) (algebraMap R (Localization.AtPrime (R := R) ⊥))
      (spanNorm R (spanNorm T I)))
    (map (F := R →+* Localization.AtPrime (R := R) ⊥) (algebraMap R (Localization.AtPrime (R := R) ⊥)) (spanNorm R I))

Tactic:
rw [spanNorm_spanNorm_of_bot_or_top]

Premises used: Ideal.spanNorm_spanNorm_of_bot_or_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
T : Type u_4
inst_9 : CommRing T
inst_10 : IsDomain T
inst_11 : IsIntegrallyClosed T
inst_12 : Algebra R T
inst_13 : Algebra T S
inst_14 : Module.Finite R T
inst_15 : Module.Finite T S
inst_16 : IsTorsionFree R T
inst_17 : IsTorsionFree T S
inst_18 : IsScalarTower R T S
inst_19 : IsDedekindDomain R
inst_20 : IsDedekindDomain T
inst_21 : IsDedekindDomain S
I : Ideal S
hP : IsMaximal.{u_1} (α := R) ⊥
⊢ ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤

Tactic:
fun I ↦ or_iff_not_imp_right.mpr fun hI ↦ (hP.eq_of_le hI bot_le).symm

Premises used: Iff.mpr, Classical.or_iff_not_imp_right, Ideal.IsMaximal.eq_of_le, Eq.symm, bot_le
-- 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
T : Type u_4
inst_9 : CommRing T
inst_10 : IsDomain T
inst_11 : IsIntegrallyClosed T
inst_12 : Algebra R T
inst_13 : Algebra T S
inst_14 : Module.Finite R T
inst_15 : Module.Finite T S
inst_16 : IsTorsionFree R T
inst_17 : IsTorsionFree T S
inst_18 : IsScalarTower R T S
inst_19 : IsDedekindDomain R
inst_20 : IsDedekindDomain T
inst_21 : IsDedekindDomain S
I : Ideal S
hP : IsMaximal.{u_1} (α := R) ⊥
⊢ ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤

Tactic:
exact fun I ↦ or_iff_not_imp_right.mpr fun hI ↦ (hP.eq_of_le hI bot_le).symm

Premises used: Iff.mpr, Classical.or_iff_not_imp_right, Ideal.IsMaximal.eq_of_le, Eq.symm, bot_le
-- 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
T : Type u_4
inst_9 : CommRing T
inst_10 : IsDomain T
inst_11 : IsIntegrallyClosed T
inst_12 : Algebra R T
inst_13 : Algebra T S
inst_14 : Module.Finite R T
inst_15 : Module.Finite T S
inst_16 : IsTorsionFree R T
inst_17 : IsTorsionFree T S
inst_18 : IsScalarTower R T S
inst_19 : IsDedekindDomain R
inst_20 : IsDedekindDomain T
inst_21 : IsDedekindDomain S
I : Ideal S
P : Ideal R
hP_1 : P.IsMaximal
hP : ¬P = ⊥
Rₚ : Type u_1 := Localization.AtPrime P
Tₚ : Type u_4 := Localization (M := T) (algebraMapSubmonoid T P.primeCompl)
Sₚ : Type u_3 := Localization (M := S) (algebraMapSubmonoid S P.primeCompl)
⊢ NeZero P

Tactic:
have : NeZero P := ⟨hP⟩
-- 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
T : Type u_4
inst_9 : CommRing T
inst_10 : IsDomain T
inst_11 : IsIntegrallyClosed T
inst_12 : Algebra R T
inst_13 : Algebra T S
inst_14 : Module.Finite R T
inst_15 : Module.Finite T S
inst_16 : IsTorsionFree R T
inst_17 : IsTorsionFree T S
inst_18 : IsScalarTower R T S
inst_19 : IsDedekindDomain R
inst_20 : IsDedekindDomain T
inst_21 : IsDedekindDomain S
I : Ideal S
P : Ideal R
hP_1 : P.IsMaximal
hP : ¬P = ⊥
Rₚ : Type u_1 := Localization.AtPrime P
Tₚ : Type u_4 := Localization (M := T) (algebraMapSubmonoid T P.primeCompl)
Sₚ : Type u_3 := Localization (M := S) (algebraMapSubmonoid S P.primeCompl)
this : NeZero P
⊢ LE.le (α := Submonoid T) (algebraMapSubmonoid T P.primeCompl) T⁰

Tactic:
have h : algebraMapSubmonoid T P.primeCompl ≤ T⁰ :=
      algebraMapSubmonoid_le_nonZeroDivisors_of_faithfulSMul _ (primeCompl_le_nonZeroDivisors P)
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
Goal:
R : Type u_1
S_1 : Type u_2
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
rw : Eq (α := Ideal R) (spanNorm.{u_1, u_3} R (S := S) ⊤) 1
rw₁ : Eq.{u_1 + 1} (α := Ideal R) ⊤ 1
rw₂ rw₃ : Eq.{u_1 + 1} (α := Ideal R) ⊤ ⊤
⊢ Eq (α := Ideal R) (spanNorm.{u_1, u_3} R (S := S) 1) 1

Tactic:
rw [one_eq_top, spanNorm_top R, one_eq_top]

Premises used: Ideal.one_eq_top, Ideal.spanNorm_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
I : Ideal S
⊢ Eq.{u_1 + 1} (α := Ideal R) ((relNorm R : (a : Ideal S) → Ideal R) I : Ideal R)
    (span ((⇑(Algebra.intNorm R S) : (a : S) → R) '' (↑I : Set S)) : Ideal R)

Tactic:
rfl

Premises used: Set.Mem, setOf, Ideal.map, Ideal.spanNorm, Submodule.span, 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
I : Ideal S
⊢ Eq (α := Ideal R) (spanNorm R I) ((relNorm R : (a : Ideal S) → Ideal R) I)

Tactic:
rfl

Premises used: Ideal.map, Ideal.spanNorm, Submodule.span, 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
⊢ Eq.{u_1 + 1} (α := Ideal R) ((relNorm R : (a : Ideal S) → Ideal R) ⊥) ⊥

Tactic:
simpa only [zero_eq_bot] using map_zero (relNorm R : Ideal S →*₀ _)

Premises used: map_zero, Ideal.zero_eq_bot, Ideal.relNorm
-- 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
⊢ Eq.{u_1 + 1} (α := Ideal R) ((relNorm R : (a : Ideal S) → Ideal R) ⊤) ⊤

Tactic:
simpa only [one_eq_top] using map_one (relNorm R : Ideal S →*₀ _)

Premises used: Ideal.one_eq_top, Ideal.relNorm, map_one
-- 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
I : Ideal S
⊢ Eq.{u_1 + 1} (α := Ideal R) ((relNorm R : (a : Ideal S) → Ideal R) I : Ideal R) (⊥ : Ideal R) ↔ I = ⊥

Tactic:
spanNorm_eq_bot_iff

Premises used: Ideal.map, Ideal.spanNorm, Submodule.span, Ideal.spanNorm_eq_bot_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 S
I : Ideal S
x : S
hx : x ∈ I
⊢ Membership.mem.{u_1, u_1} (α := R) (γ := Ideal R) ((relNorm R : (a : Ideal S) → Ideal R) I : Ideal R)
    ((Algebra.norm R : (a : S) → R) x : R)

Tactic:
norm_mem_spanNorm R x hx

Premises used: Set.Mem, Ideal.norm_mem_spanNorm