awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
n : ℕ
inst_5 : CharZero S
this_1 :
  Finite.{max 1 (u_1 + 1)}
    { I : Ideal S // Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n }
this : Finite.{max 1 (u_1 + 1)} { I : Ideal S // I ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n }
e : { I : Ideal S // (absNorm : (a : Ideal S) → ℕ) I ≤ n } ≃
  { I : Ideal S // Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n } ⊕
    { I : Ideal S // I ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n } :=
  Equiv.trans
    (Equiv.subtypeEquivRight (p := fun (I : Ideal S) ↦ (absNorm : (a : Ideal S) → ℕ) I ≤ n) (q := fun (x : Ideal S) ↦
      Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ x ∧ (absNorm : (a : Ideal S) → ℕ) x ≤ n ∨
        x ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) x ≤ n)
      ⋯)
    (subtypeOrEquiv
      (fun (I : Ideal S) ↦ Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n)
      (fun (I : Ideal S) ↦ I ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n) ⋯)
I : Ideal S
h : Eq (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) (0 : ℕ)
⊢ 0 ≤ n

Tactic:
exact Nat.zero_le n

Premises used: Nat.zero_le
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
n : ℕ
inst_5 : CharZero S
this_1 :
  Finite.{max 1 (u_1 + 1)}
    { I : Ideal S // Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n }
this : Finite.{max 1 (u_1 + 1)} { I : Ideal S // I ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n }
e : { I : Ideal S // (absNorm : (a : Ideal S) → ℕ) I ≤ n } ≃
  { I : Ideal S // Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n } ⊕
    { I : Ideal S // I ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n } :=
  Equiv.trans
    (Equiv.subtypeEquivRight (p := fun (I : Ideal S) ↦ (absNorm : (a : Ideal S) → ℕ) I ≤ n) (q := fun (x : Ideal S) ↦
      Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ x ∧ (absNorm : (a : Ideal S) → ℕ) x ≤ n ∨
        x ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) x ≤ n)
      ⋯)
    (subtypeOrEquiv
      (fun (I : Ideal S) ↦ Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n)
      (fun (I : Ideal S) ↦ I ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n) ⋯)
I : Ideal S
h : I = ⊥
| I ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n

Tactic:
rw [← absNorm_ne_zero_iff_mem_nonZeroDivisors, ne_eq, not_not, and_iff_left_iff_imp.mpr
      (fun h ↦ by rw [h]; exact Nat.zero_le n), absNorm_eq_zero_iff]

Premises used: Iff.mpr, Classical.not_not, Ideal.absNorm_ne_zero_iff_mem_nonZeroDivisors, ne_eq, Ideal.absNorm_eq_zero_iff, and_iff_left_iff_imp
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
n : ℕ
inst_5 : CharZero S
this_1 :
  Finite.{max 1 (u_1 + 1)}
    { I : Ideal S // Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n }
this : Finite.{max 1 (u_1 + 1)} { I : Ideal S // I ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n }
e : { I : Ideal S // (absNorm : (a : Ideal S) → ℕ) I ≤ n } ≃
  { I : Ideal S // Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n } ⊕
    { I : Ideal S // I ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n } :=
  Equiv.trans
    (Equiv.subtypeEquivRight (p := fun (I : Ideal S) ↦ (absNorm : (a : Ideal S) → ℕ) I ≤ n) (q := fun (x : Ideal S) ↦
      Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ x ∧ (absNorm : (a : Ideal S) → ℕ) x ≤ n ∨
        x ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) x ≤ n)
      ⋯)
    (subtypeOrEquiv
      (fun (I : Ideal S) ↦ Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n)
      (fun (I : Ideal S) ↦ I ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n) ⋯)
h : ∀ (I : Ideal S), I = ⊥
| Nat.card.{u_1} { I : Ideal S // I ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n }

Tactic:
enter [1, 1, I]
    rw [← absNorm_ne_zero_iff_mem_nonZeroDivisors, ne_eq, not_not, and_iff_left_iff_imp.mpr
      (fun h ↦ by rw [h]; exact Nat.zero_le n), absNorm_eq_zero_iff]

Premises used: Iff.mpr, Classical.not_not, Ideal.absNorm_ne_zero_iff_mem_nonZeroDivisors, ne_eq, Ideal.absNorm_eq_zero_iff, and_iff_left_iff_imp
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
n : ℕ
inst_5 : CharZero S
this_1 :
  Finite.{max 1 (u_1 + 1)}
    { I : Ideal S // Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n }
this : Finite.{max 1 (u_1 + 1)} { I : Ideal S // I ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n }
e : { I : Ideal S // (absNorm : (a : Ideal S) → ℕ) I ≤ n } ≃
  { I : Ideal S // Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n } ⊕
    { I : Ideal S // I ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n } :=
  Equiv.trans
    (Equiv.subtypeEquivRight (p := fun (I : Ideal S) ↦ (absNorm : (a : Ideal S) → ℕ) I ≤ n) (q := fun (x : Ideal S) ↦
      Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ x ∧ (absNorm : (a : Ideal S) → ℕ) x ≤ n ∨
        x ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) x ≤ n)
      ⋯)
    (subtypeOrEquiv
      (fun (I : Ideal S) ↦ Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n)
      (fun (I : Ideal S) ↦ I ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n) ⋯)
conv_lhs : Nat.card.{u_1} { I : Ideal S // I = ⊥ } = 1
⊢ Nat.card.{u_1} { I : Ideal S // I ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n } = 1

Tactic:
conv_lhs =>
    enter [1, 1, I]
    rw [← absNorm_ne_zero_iff_mem_nonZeroDivisors, ne_eq, not_not, and_iff_left_iff_imp.mpr
      (fun h ↦ by rw [h]; exact Nat.zero_le n), absNorm_eq_zero_iff]

Premises used: Iff.mpr, Classical.not_not, Ideal.absNorm_ne_zero_iff_mem_nonZeroDivisors, ne_eq, Ideal.absNorm_eq_zero_iff, and_iff_left_iff_imp
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
n : ℕ
inst_5 : CharZero S
this_1 :
  Finite.{max 1 (u_1 + 1)}
    { I : Ideal S // Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n }
this : Finite.{max 1 (u_1 + 1)} { I : Ideal S // I ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n }
e : { I : Ideal S // (absNorm : (a : Ideal S) → ℕ) I ≤ n } ≃
  { I : Ideal S // Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n } ⊕
    { I : Ideal S // I ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n } :=
  Equiv.trans
    (Equiv.subtypeEquivRight (p := fun (I : Ideal S) ↦ (absNorm : (a : Ideal S) → ℕ) I ≤ n) (q := fun (x : Ideal S) ↦
      Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ x ∧ (absNorm : (a : Ideal S) → ℕ) x ≤ n ∨
        x ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) x ≤ n)
      ⋯)
    (subtypeOrEquiv
      (fun (I : Ideal S) ↦ Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n)
      (fun (I : Ideal S) ↦ I ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n) ⋯)
rw rw₁ : Eq (α := ℕ) 1 1
⊢ Nat.card.{u_1} { I : Ideal S // I = ⊥ } = 1

Tactic:
rw [Nat.card_unique]

Premises used: Nat.card_unique
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
x : S
hx : Prime (M := ℤ) ((Algebra.norm ℤ : (a : S) → ℤ) x : ℤ)
y : ℤ
rw : Nat.Prime ((absNorm : (a : Ideal S) → ℕ) (span {x}))
⊢ (Algebra.norm ℤ : (a : S) → ℤ) x ∣ y ↔ x ∣ (↑y : S)

Tactic:
rw [← Ideal.mem_span_singleton (y := x), ← eq_intCast (algebraMap ℤ S), ← Ideal.mem_comap,
    ← Ideal.span_singleton_absNorm, Ideal.mem_span_singleton, Ideal.absNorm_span_singleton,
    Int.natAbs_dvd]

Premises used: Algebra.algebraMap, Int, eq_intCast, Ideal.span_singleton_absNorm, Ideal.mem_span_singleton, Int.natAbs_dvd, Ideal.mem_comap, Ideal.absNorm_span_singleton
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
x : S
hx : Prime (M := ℤ) ((Algebra.norm ℤ : (a : S) → ℤ) x : ℤ)
y : ℤ
rwa : Nat.Prime (Int.natAbs ((Algebra.norm ℤ : (a : S) → ℤ) x))
rwa₁ rwa₂ rwa₃ rwa₄ : Prime (M := ℤ) ((Algebra.norm ℤ : (a : S) → ℤ) x : ℤ)
⊢ Nat.Prime ((absNorm : (a : Ideal S) → ℕ) (span {x}))

Tactic:
rwa [Ideal.absNorm_span_singleton, ← Int.prime_iff_natAbs_prime]

Premises used: Int.prime_iff_natAbs_prime, Ideal.absNorm_span_singleton
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
J : Ideal ℤ
obtain : ∀ (g : ℤ), Eq (α := Ideal ℤ) (span {(↑((absNorm : (a : Ideal ℤ) → ℕ) (ℤ ∙ g)) : ℤ)}) (ℤ ∙ g)
⊢ span {(↑((absNorm : (a : Ideal ℤ) → ℕ) J) : ℤ)} = J

Tactic:
obtain ⟨g, rfl⟩ := IsPrincipalIdealRing.principal J

Premises used: IsPrincipalIdealRing.principal, rfl
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
g : ℤ
⊢ Eq (α := Ideal ℤ) (span {(↑((absNorm : (a : Ideal ℤ) → ℕ) (ℤ ∙ g)) : ℤ)}) (ℤ ∙ g)

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
J : Ideal ℤ
obtain : ∀ (g : ℤ), Nat.Prime ((absNorm : (a : Ideal ℤ) → ℕ) (ℤ ∙ g)) ↔ Prime (M := Ideal ℤ) (ℤ ∙ g)
⊢ Nat.Prime ((absNorm : (a : Ideal ℤ) → ℕ) J) ↔ Prime J

Tactic:
obtain ⟨g, rfl⟩ := IsPrincipalIdealRing.principal J

Premises used: IsPrincipalIdealRing.principal, rfl
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
g : ℤ
⊢ Nat.Prime ((absNorm : (a : Ideal ℤ) → ℕ) (ℤ ∙ g)) ↔ Prime (M := Ideal ℤ) (ℤ ∙ g)

Tactic:
simp [prime_span_singleton_iff, prime_iff_natAbs_prime]

Premises used: Ideal.prime_span_singleton_iff, Int.prime_iff_natAbs_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
x : R
hx : Membership.mem (γ := Set R) ((⇑(Algebra.intNorm R S) : (a : S) → R) '' (↑⊥ : Set S)) x
⊢ x = 0

Tactic:
simpa using hx
-- 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
I : Ideal S
⊢ Eq (α := Ideal R) (spanNorm R I) ⊥ ↔ I = ⊥

Tactic:
simp only [spanNorm, span_eq_bot, Set.mem_image, SetLike.mem_coe, forall_exists_index, and_imp,
    forall_apply_eq_imp_iff₂, Algebra.intNorm_eq_zero, @eq_bot_iff _ _ _ I, SetLike.le_def, map,
    mem_bot]

Premises used: Ideal.mem_bot, and_imp, SetLike.le_def, Set.mem_image, forall_exists_index, Ideal.map, SetLike.mem_coe, Ideal.spanNorm, Ideal.span_eq_bot, eq_bot_iff, forall_apply_eq_imp_iff₂, Algebra.intNorm_eq_zero
-- 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
I : Ideal S
x : S
hx : x ∈ I
⊢ Membership.mem (α := R) (γ := Ideal R) (spanNorm R I) ((Algebra.intNorm R S : (a : S) → R) x : R)

Tactic:
subset_span (Set.mem_image_of_mem _ hx)

Premises used: Ideal.subset_span, Set.Mem, Set.mem_image_of_mem
-- 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 : Free R S
I : Ideal S
x : S
hx : x ∈ I
⊢ Membership.mem (α := R) (γ := Ideal R) (spanNorm R I) ((Algebra.norm R : (a : S) → R) x : R)

Tactic:
subset_span ⟨x, hx, ?_⟩

Premises used: Ideal.subset_span, Set.Mem, And.intro, Exists.intro
-- 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 : Free R S
I : Ideal S
x : S
hx : x ∈ I
refine : Eq.{u_1 + 1} (α := R) ((Algebra.intNorm R S : (a : S) → R) x : R) ((Algebra.norm R : (a : S) → R) x : R)
⊢ Membership.mem (α := R) (γ := Ideal R) (spanNorm R I) ((Algebra.norm R : (a : S) → R) x : R)

Tactic:
refine subset_span ⟨x, hx, ?_⟩
-- 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 : Free R S
I : Ideal S
x : S
hx : x ∈ I
rw rw₁ : Eq.{u_1 + 1} (α := R) ((Algebra.norm R : (a : S) → R) x : R) ((Algebra.norm R : (a : S) → R) x : R)
⊢ Eq.{u_1 + 1} (α := R) ((Algebra.intNorm R S : (a : S) → R) x : R) ((Algebra.norm R : (a : S) → R) x : R)

Tactic:
rw [Algebra.intNorm_eq_norm]

Premises used: Algebra.intNorm_eq_norm
-- 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
r : S
x : R
hx : Membership.mem (γ := Set R) ((⇑(Algebra.intNorm R S) : (a : S) → R) '' (↑(span {r}) : Set S)) x
obtain :
  ∀ (x : S) (hx' : x ∈ (↑(span {r}) : Set S))
    (hx :
      Membership.mem.{u_1, u_1} (α := R) (γ := Set R) ((⇑(Algebra.intNorm R S) : (a : S) → R) '' (↑(span {r}) : Set S))
        ((Algebra.intNorm R S : (a : S) → R) x : R)),
    Dvd.dvd.{u_1} (α := R) ((Algebra.intNorm R S : (a : S) → R) r : R) ((Algebra.intNorm R S : (a : S) → R) x : R)
⊢ (Algebra.intNorm R S : (a : S) → R) r ∣ x

Tactic:
obtain ⟨x, hx', rfl⟩ := (Set.mem_image _ _ _).mp hx

Premises used: Set.mem_image, Iff.mp, 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
r x : S
hx' : x ∈ (↑(span {r}) : Set S)
hx :
  Membership.mem.{u_1, u_1} (α := R) (γ := Set R) ((⇑(Algebra.intNorm R S) : (a : S) → R) '' (↑(span {r}) : Set S))
    ((Algebra.intNorm R S : (a : S) → R) x : R)
⊢ Dvd.dvd.{u_1} (α := R) ((Algebra.intNorm R S : (a : S) → R) r : R) ((Algebra.intNorm R S : (a : S) → R) x : R)

Tactic:
map_dvd _ (mem_span_singleton.mp hx')

Premises used: map_dvd, Iff.mp, Ideal.mem_span_singleton
-- 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
r x : S
hx' : x ∈ (↑(span {r}) : Set S)
hx :
  Membership.mem.{u_1, u_1} (α := R) (γ := Set R) ((⇑(Algebra.intNorm R S) : (a : S) → R) '' (↑(span {r}) : Set S))
    ((Algebra.intNorm R S : (a : S) → R) x : R)
⊢ Dvd.dvd.{u_1} (α := R) ((Algebra.intNorm R S : (a : S) → R) r : R) ((Algebra.intNorm R S : (a : S) → R) x : R)

Tactic:
exact map_dvd _ (mem_span_singleton.mp hx')

Premises used: map_dvd, Iff.mp, Ideal.mem_span_singleton
-- 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
⊢ Eq (α := Ideal R) (spanNorm.{u_1, u_3} R (S := S) ⊤) ⊤

Tactic:
simp [← Ideal.span_singleton_one]

Premises used: Ideal.span_singleton_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
I : Ideal S
T : Type u_4
inst_9 : Semiring T
f : R →+* T
⊢ Eq.{u_4 + 1} (α := Ideal T) (map (R := R) f (span ((⇑(Algebra.intNorm R S) : (a : S) → R) '' (↑I : Set S))))
    (span
      (Function.comp.{u_3 + 1, u_1 + 1, u_4 + 1} (β := R) (⇑f : (a : R) → T) (⇑(Algebra.intNorm R S) : (a : S) → R) ''
        (↑I : Set S)))

Tactic:
simp [map_span, Set.image_image]

Premises used: Set.image_image, Ideal.map_span
-- 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
I J : Ideal S
h : I ≤ J
⊢ LE.le (α := Ideal R) (spanNorm R I) (spanNorm R J)

Tactic:
Ideal.span_mono (Set.monotone_image h)

Premises used: Set.Mem, Ideal.span_mono, Set.monotone_image
-- 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
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_4
Sₘ : Type u_5
inst_9 : CommRing Rₘ
inst_10 : Algebra R Rₘ
inst_11 : CommRing Sₘ
inst_12 : Algebra S Sₘ
inst_13 : Algebra Rₘ Sₘ
inst_14 : Algebra R Sₘ
inst_15 : IsScalarTower R Rₘ Sₘ
inst_16 : IsScalarTower R S Sₘ
inst_17 : IsLocalization M Rₘ
inst_18 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst_19 : IsIntegrallyClosed Rₘ
inst_20 : IsDomain Rₘ
inst_21 : IsDomain Sₘ
inst_22 : IsTorsionFree Rₘ Sₘ
inst_23 : Module.Finite Rₘ Sₘ
inst_24 : IsIntegrallyClosed Sₘ
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map (M := M) (T := R⁰) K (RingHom.id R) hM
L : Type u_3 := FractionRing S
g : Sₘ →+* L := IsLocalization.map (M := Algebra.algebraMapSubmonoid S M) (T := S⁰) L (RingHom.id S) ⋯
algInst : Algebra Rₘ K := f.toAlgebra
algInst_1 : Algebra Sₘ L := g.toAlgebra
algInst_2 : Algebra Rₘ L := RingHom.toAlgebra (RingHom.comp (algebraMap K L) f)
scalarTowerInst : IsScalarTower Rₘ K L := ⋯
rw : Eq (α := R →+* K) (algebraMap R K) (f.comp (algebraMap R Rₘ))
rw₁ : Eq (α := R →+* K) (algebraMap R K) (RingHom.comp (algebraMap R K) (RingHom.id R))
rw₂ rw₃ : Eq (α := R →+* K) (algebraMap R K) (algebraMap R K)
⊢ Eq (α := R →+* K) (algebraMap R K)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₘ K) (algebraMap R Rₘ))

Tactic:
rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHomCompTriple.comp_eq]

Premises used: RingHomCompTriple.comp_eq, IsLocalization.map_comp, RingHom.algebraMap_toAlgebra
-- 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
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_4
Sₘ : Type u_5
inst_9 : CommRing Rₘ
inst_10 : Algebra R Rₘ
inst_11 : CommRing Sₘ
inst_12 : Algebra S Sₘ
inst_13 : Algebra Rₘ Sₘ
inst_14 : Algebra R Sₘ
inst_15 : IsScalarTower R Rₘ Sₘ
inst_16 : IsScalarTower R S Sₘ
inst_17 : IsLocalization M Rₘ
inst_18 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst_19 : IsIntegrallyClosed Rₘ
inst_20 : IsDomain Rₘ
inst_21 : IsDomain Sₘ
inst_22 : IsTorsionFree Rₘ Sₘ
inst_23 : Module.Finite Rₘ Sₘ
inst_24 : IsIntegrallyClosed Sₘ
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map (M := M) (T := R⁰) K (RingHom.id R) hM
L : Type u_3 := FractionRing S
g : Sₘ →+* L := IsLocalization.map (M := Algebra.algebraMapSubmonoid S M) (T := S⁰) L (RingHom.id S) ⋯
algInst : Algebra Rₘ K := f.toAlgebra
algInst_1 : Algebra Sₘ L := g.toAlgebra
algInst_2 : Algebra Rₘ L := RingHom.toAlgebra (RingHom.comp (algebraMap K L) f)
scalarTowerInst : IsScalarTower Rₘ K L := ⋯
⊢ IsScalarTower R Rₘ K

Tactic:
have : IsScalarTower R Rₘ K := IsScalarTower.of_algebraMap_eq'
    (by rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHomCompTriple.comp_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
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_4
Sₘ : Type u_5
inst_9 : CommRing Rₘ
inst_10 : Algebra R Rₘ
inst_11 : CommRing Sₘ
inst_12 : Algebra S Sₘ
inst_13 : Algebra Rₘ Sₘ
inst_14 : Algebra R Sₘ
inst_15 : IsScalarTower R Rₘ Sₘ
inst_16 : IsScalarTower R S Sₘ
inst_17 : IsLocalization M Rₘ
inst_18 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst_19 : IsIntegrallyClosed Rₘ
inst_20 : IsDomain Rₘ
inst_21 : IsDomain Sₘ
inst_22 : IsTorsionFree Rₘ Sₘ
inst_23 : Module.Finite Rₘ Sₘ
inst_24 : IsIntegrallyClosed Sₘ
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map (M := M) (T := R⁰) K (RingHom.id R) hM
L : Type u_3 := FractionRing S
g : Sₘ →+* L := IsLocalization.map (M := Algebra.algebraMapSubmonoid S M) (T := S⁰) L (RingHom.id S) ⋯
algInst : Algebra Rₘ K := f.toAlgebra
algInst_1 : Algebra Sₘ L := g.toAlgebra
algInst_2 : Algebra Rₘ L := RingHom.toAlgebra (RingHom.comp (algebraMap K L) f)
scalarTowerInst : IsScalarTower Rₘ K L := ⋯
this : IsScalarTower R Rₘ K
h : IsFractionRing Rₘ K := ⋯
rw : Eq (α := S →+* L) (algebraMap S L) (g.comp (algebraMap S Sₘ))
rw₁ : Eq (α := S →+* L) (algebraMap S L) (RingHom.comp (algebraMap S L) (RingHom.id S))
rw₂ rw₃ : Eq (α := S →+* L) (algebraMap S L) (algebraMap S L)
⊢ Eq (α := S →+* L) (algebraMap S L)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Sₘ L) (algebraMap S Sₘ))

Tactic:
rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHomCompTriple.comp_eq]

Premises used: RingHomCompTriple.comp_eq, IsLocalization.map_comp, RingHom.algebraMap_toAlgebra
-- 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
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_4
Sₘ : Type u_5
inst_9 : CommRing Rₘ
inst_10 : Algebra R Rₘ
inst_11 : CommRing Sₘ
inst_12 : Algebra S Sₘ
inst_13 : Algebra Rₘ Sₘ
inst_14 : Algebra R Sₘ
inst_15 : IsScalarTower R Rₘ Sₘ
inst_16 : IsScalarTower R S Sₘ
inst_17 : IsLocalization M Rₘ
inst_18 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst_19 : IsIntegrallyClosed Rₘ
inst_20 : IsDomain Rₘ
inst_21 : IsDomain Sₘ
inst_22 : IsTorsionFree Rₘ Sₘ
inst_23 : Module.Finite Rₘ Sₘ
inst_24 : IsIntegrallyClosed Sₘ
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map (M := M) (T := R⁰) K (RingHom.id R) hM
L : Type u_3 := FractionRing S
g : Sₘ →+* L := IsLocalization.map (M := Algebra.algebraMapSubmonoid S M) (T := S⁰) L (RingHom.id S) ⋯
algInst : Algebra Rₘ K := f.toAlgebra
algInst_1 : Algebra Sₘ L := g.toAlgebra
algInst_2 : Algebra Rₘ L := RingHom.toAlgebra (RingHom.comp (algebraMap K L) f)
scalarTowerInst : IsScalarTower Rₘ K L := ⋯
this : IsScalarTower R Rₘ K
h : IsFractionRing Rₘ K := ⋯
⊢ IsScalarTower S Sₘ L

Tactic:
have : IsScalarTower S Sₘ L := IsScalarTower.of_algebraMap_eq'
    (by rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHomCompTriple.comp_eq])