awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : FractionalIdeal (R := R) R⁰ (FractionRing R)
hI : IsPrincipal I.num
⊢ (↑I : Submodule R (FractionRing R)).IsPrincipal

Tactic:
Module.isPrincipal_submodule_iff.mp
    <| (FractionalIdeal.equivNumOfIsLocalization I).isPrincipal_iff.mpr
    <| Module.isPrincipal_submodule_iff.mpr hI

Premises used: Iff.mpr, Module.isPrincipal_submodule_iff, Iff.mp, FractionalIdeal.equivNumOfIsLocalization, LinearEquiv.isPrincipal_iff
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
I : Submodule R₁ K
hI : I ≤ (↑0 : Submodule R₁ K)
⊢ I = ⊥

Tactic:
rw [coe_zero, le_bot_iff] at hI

Premises used: le_bot_iff, FractionalIdeal.coe_zero
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
I : Submodule R₁ K
hI : I = ⊥
rw : FG.{u_3, u_4} (R := R₁) (M := K) ⊥
⊢ I.FG

Tactic:
rw [hI]
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
I : Submodule R₁ K
hI : I = ⊥
⊢ FG.{u_3, u_4} (R := R₁) (M := K) ⊥

Tactic:
fg_bot

Premises used: Submodule.fg_bot
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
I : Submodule R₁ K
hI : I = ⊥
⊢ FG.{u_3, u_4} (R := R₁) (M := K) ⊥

Tactic:
exact fg_bot

Premises used: Submodule.fg_bot
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
⊢ IsNoetherian.{u_3, u_4} R₁ ↥(↑I : Submodule R₁ K) ↔ ∀ J ≤ I, (↑J : Submodule R₁ K).FG

Tactic:
isNoetherian_submodule.trans ⟨fun h _ hJ => h _ hJ, fun h J hJ => h ⟨J, isFractional_of_le hJ⟩ hJ⟩

Premises used: isNoetherian_submodule, Subtype.mk, FractionalIdeal.coeToSubmodule, Iff.intro, Iff.trans, FractionalIdeal.isFractional_of_le
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsNoetherianRing R₁
I : Ideal R₁
rw : ∀ J ≤ (↑I : FractionalIdeal R₁⁰ K), (↑J : Submodule R₁ K).FG
⊢ IsNoetherian.{u_3, u_4} R₁ ↥(↑(↑I : FractionalIdeal R₁⁰ K) : Submodule R₁ K)

Tactic:
rw [isNoetherian_iff]

Premises used: FractionalIdeal.isNoetherian_iff
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsNoetherianRing R₁
I : Ideal R₁
J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
hJ : J ≤ (↑I : FractionalIdeal R₁⁰ K)
obtain :
  ∀ (J : Ideal R₁)
    (hJ :
      LE.le.{u_4} (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (↑J : FractionalIdeal R₁⁰ K)
        (↑I : FractionalIdeal R₁⁰ K)),
    FG.{u_3, u_4} (M := K) (↑(↑J : FractionalIdeal R₁⁰ K) : Submodule R₁ K)
⊢ (↑J : Submodule R₁ K).FG

Tactic:
obtain ⟨J, rfl⟩ := le_one_iff_exists_coeIdeal.mp (le_trans hJ coeIdeal_le_one)

Premises used: FractionalIdeal.coeIdeal_le_one, FractionalIdeal.le_one_iff_exists_coeIdeal, Iff.mp, rfl, le_trans
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsNoetherianRing R₁
I J : Ideal R₁
hJ :
  LE.le.{u_4} (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (↑J : FractionalIdeal R₁⁰ K)
    (↑I : FractionalIdeal R₁⁰ K)
⊢ FG.{u_3, u_4} (M := K) (↑(↑J : FractionalIdeal R₁⁰ K) : Submodule R₁ K)

Tactic:
(IsNoetherian.noetherian J).map _

Premises used: Submodule.FG.map, IsNoetherian.noetherian, FractionalIdeal.coeToSubmodule, Submodule.map, IsLocalization.coeSubmodule
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsNoetherianRing R₁
I J : Ideal R₁
hJ :
  LE.le.{u_4} (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (↑J : FractionalIdeal R₁⁰ K)
    (↑I : FractionalIdeal R₁⁰ K)
⊢ FG.{u_3, u_4} (M := K) (↑(↑J : FractionalIdeal R₁⁰ K) : Submodule R₁ K)

Tactic:
exact (IsNoetherian.noetherian J).map _

Premises used: Submodule.FG.map, IsNoetherian.noetherian
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
x : R₁
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
hI : IsNoetherian.{u_3, u_4} R₁ ↥(↑I : Submodule R₁ K)
pos :
  ∀ (hx : x = 0),
    IsNoetherian.{u_3, u_4} R₁
      ↥(↑(HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
              (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) x)⁻¹ : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
              I) :
          Submodule R₁ K)
neg :
  ∀ (hx : ¬x = 0),
    IsNoetherian.{u_3, u_4} R₁
      ↥(↑(HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
              (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) x)⁻¹ : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
              I) :
          Submodule R₁ K)
⊢ IsNoetherian.{u_3, u_4} R₁
    ↥(↑(HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
            (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) x)⁻¹ : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) I) :
        Submodule R₁ K)

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
x : R₁
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
hI : IsNoetherian.{u_3, u_4} R₁ ↥(↑I : Submodule R₁ K)
hx : x = 0
pos : IsNoetherian.{u_3, u_4} R₁ ↥(↑0 : Submodule R₁ K)
⊢ IsNoetherian.{u_3, u_4} R₁
    ↥(↑(HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
            (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) x)⁻¹ : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) I) :
        Submodule R₁ K)

Tactic:
rw [hx, map_zero, inv_zero, spanSingleton_zero, zero_mul]

Premises used: inv_zero, MulZeroClass.zero_mul, map_zero, FractionalIdeal.spanSingleton_zero
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
x : R₁
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
hI : IsNoetherian.{u_3, u_4} R₁ ↥(↑I : Submodule R₁ K)
hx : x = 0
⊢ IsNoetherian.{u_3, u_4} R₁ ↥(↑0 : Submodule R₁ K)

Tactic:
isNoetherian_zero

Premises used: Set.Mem, FractionalIdeal.isNoetherian_zero
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
x : R₁
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
hI : IsNoetherian.{u_3, u_4} R₁ ↥(↑I : Submodule R₁ K)
hx : x = 0
⊢ IsNoetherian.{u_3, u_4} R₁ ↥(↑0 : Submodule R₁ K)

Tactic:
exact isNoetherian_zero

Premises used: FractionalIdeal.isNoetherian_zero
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
x : R₁
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
hI : IsNoetherian.{u_3, u_4} R₁ ↥(↑I : Submodule R₁ K)
hx : ¬x = 0
⊢ Ne.{u_4 + 1} (α := K) ((algebraMap R₁ K : (a : R₁) → K) x : K) (0 : K)

Tactic:
have h_gx : algebraMap R₁ K x ≠ 0 :=
    mt ((injective_iff_map_eq_zero (algebraMap R₁ K)).mp (IsFractionRing.injective _ _) x) hx
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
x : R₁
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
hI : IsNoetherian.{u_3, u_4} R₁ ↥(↑I : Submodule R₁ K)
hx : ¬x = 0
h_gx : Ne.{u_4 + 1} (α := K) ((algebraMap R₁ K : (a : R₁) → K) x : K) (0 : K)
⊢ Ne.{u_4 + 1} (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
    (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) x) : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
    (0 : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)

Tactic:
have h_spanx : spanSingleton R₁⁰ (algebraMap R₁ K x) ≠ 0 := spanSingleton_ne_zero_iff.mpr h_gx
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
x : R₁
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
hI : IsNoetherian.{u_3, u_4} R₁ ↥(↑I : Submodule R₁ K)
hx : ¬x = 0
h_gx : Ne.{u_4 + 1} (α := K) ((algebraMap R₁ K : (a : R₁) → K) x : K) (0 : K)
h_spanx :
  Ne.{u_4 + 1} (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
    (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) x) : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
    (0 : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
neg :
  ∀ (hI : ∀ J ≤ I, (↑J : Submodule R₁ K).FG) (hx : ¬x = 0)
    (h_gx : Ne.{u_4 + 1} (α := K) ((algebraMap R₁ K : (a : R₁) → K) x : K) (0 : K))
    (h_spanx :
      Ne.{u_4 + 1} (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
        (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) x) : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
        (0 : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)),
    ∀
      J ≤
        HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
          (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) x)⁻¹ : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) I,
      (↑J : Submodule R₁ K).FG
⊢ IsNoetherian.{u_3, u_4} R₁
    ↥(↑(HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
            (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) x)⁻¹ : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) I) :
        Submodule R₁ K)

Tactic:
rw [isNoetherian_iff] at hI ⊢

Premises used: FractionalIdeal.isNoetherian_iff
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
x : R₁
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
hI : ∀ J ≤ I, (↑J : Submodule R₁ K).FG
hx : ¬x = 0
h_gx : Ne.{u_4 + 1} (α := K) ((algebraMap R₁ K : (a : R₁) → K) x : K) (0 : K)
h_spanx :
  Ne.{u_4 + 1} (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
    (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) x) : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
    (0 : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
hJ :
  J ≤
    HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
      (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) x)⁻¹ : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) I
⊢ HMul.hMul (β := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) J
      (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) x) : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) ≤
    I

Tactic:
rw [← div_spanSingleton, le_div_iff_mul_le h_spanx] at hJ

Premises used: FractionalIdeal.le_div_iff_mul_le, FractionalIdeal.div_spanSingleton
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
x : R₁
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
hI : ∀ J ≤ I, (↑J : Submodule R₁ K).FG
hx : ¬x = 0
h_gx : Ne.{u_4 + 1} (α := K) ((algebraMap R₁ K : (a : R₁) → K) x : K) (0 : K)
h_spanx :
  Ne.{u_4 + 1} (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
    (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) x) : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
    (0 : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
hJ :
  HMul.hMul (β := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) J
      (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) x) : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) ≤
    I
neg :
  ∀ (s : Finset K)
    (hs :
      span R₁ (↑s : Set K) =
        (↑(HMul.hMul (β := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) J
              (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) x) : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)) :
          Submodule R₁ K)),
    (↑J : Submodule R₁ K).FG
⊢ (↑J : Submodule R₁ K).FG

Tactic:
obtain ⟨s, hs⟩ := hI _ hJ
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
x : R₁
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
hI : ∀ J ≤ I, (↑J : Submodule R₁ K).FG
hx : ¬x = 0
h_gx : Ne.{u_4 + 1} (α := K) ((algebraMap R₁ K : (a : R₁) → K) x : K) (0 : K)
h_spanx :
  Ne.{u_4 + 1} (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
    (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) x) : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
    (0 : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
hJ :
  HMul.hMul (β := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) J
      (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) x) : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) ≤
    I
s : Finset K
hs :
  span R₁ (↑s : Set K) =
    (↑(HMul.hMul (β := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) J
          (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) x) : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)) :
      Submodule R₁ K)
h : span R₁ (↑(s * singleton (α := K) (((algebraMap R₁ K : (a : R₁) → K) x)⁻¹ : K)) : Set K) = (↑J : Submodule R₁ K)
⊢ (↑J : Submodule R₁ K).FG

Tactic:
use s * {(algebraMap R₁ K x)⁻¹}

Premises used: Algebra.algebraMap, DFunLike.coe
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
inst_5 : IsNoetherianRing R₁
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
obtain :
  ∀ (d : R₁) (J : Ideal R₁),
    d ≠ 0 →
      IsNoetherian.{u_3, u_4} R₁
        ↥(↑(HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (β :=
                FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
                (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) d)⁻¹ : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
                ((↑J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)) :
            Submodule R₁ K)
⊢ IsNoetherian.{u_3, u_4} R₁ ↥(↑I : Submodule R₁ K)

Tactic:
obtain ⟨d, J, _, rfl⟩ := exists_eq_spanSingleton_mul I

Premises used: FractionalIdeal.exists_eq_spanSingleton_mul, rfl
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
inst_5 : IsNoetherianRing R₁
d : R₁
J : Ideal R₁
left : d ≠ 0
hI : IsNoetherian.{u_3, u_4} R₁ ↥(↑(↑J : FractionalIdeal R₁⁰ K) : Submodule R₁ K)
⊢ IsNoetherian.{u_3, u_4} R₁
    ↥(↑(HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (β := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
            (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) d)⁻¹ : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
            ((↑J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)) :
        Submodule R₁ K)

Tactic:
apply isNoetherian_spanSingleton_inv_to_map_mul

Premises used: FractionalIdeal.isNoetherian_spanSingleton_inv_to_map_mul
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
inst_5 : IsNoetherianRing R₁
d : R₁
J : Ideal R₁
left : d ≠ 0
⊢ IsNoetherian.{u_3, u_4} R₁ ↥(↑(↑J : FractionalIdeal R₁⁰ K) : Submodule R₁ K)

Tactic:
apply isNoetherian_coeIdeal

Premises used: FractionalIdeal.isNoetherian_coeIdeal
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
inst_3 : IsLocalization S P
x : P
hx : IsIntegral R x
⊢ IsFractional.{u_1, u_2} S (P := P) ((Subalgebra.toSubmodule : (a : Subalgebra R P) → Submodule R P) R[x])

Tactic:
isFractional_of_fg hx.fg_adjoin_singleton

Premises used: IsIntegral.fg_adjoin_singleton, FractionalIdeal.isFractional_of_fg
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
inst_3 : IsLocalization S P
x : P
hx : IsIntegral R x
⊢ (↑(adjoinIntegral S x hx) : Submodule R P) = (Subalgebra.toSubmodule : (a : Subalgebra R P) → Submodule R P) R[x]

Tactic:
rfl

Premises used: Set.Mem, setOf, FractionalIdeal.coeToSubmodule, rfl
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
inst_3 : IsLocalization S P
x : P
hx : IsIntegral R x
⊢ x ∈ adjoinIntegral S x hx

Tactic:
Algebra.subset_adjoin (Set.mem_singleton x)

Premises used: Set.mem_singleton, iInf, Set.Mem, Set.iInter, Algebra.subset_adjoin, setOf
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R_1 : Type u_1
inst : CommRing R_1
S_1 : Submonoid R_1
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R_1 P
R₁ : Type u_3
inst_3 : CommRing R₁
K_1 : Type u_4
inst_4 : Field K_1
inst_5 : Algebra R₁ K_1
inst_6 : IsFractionRing R₁ K_1
inst_7 : IsDomain R₁
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst_8 : CommRing R
inst_9 : IsDomain R
inst_10 : CommRing S
inst_11 : IsDomain S
inst_12 : CommRing K
inst_13 : CommRing L
inst_14 : Algebra R K
inst_15 : Algebra S L
inst_16 : IsFractionRing R K
inst_17 : IsFractionRing S L
f_1 f : R ≃+* S
⊢ RingHomInvPair (↑f : R →+* S) (↑f.symm : S →+* R)

Tactic:
RingHomInvPair.of_ringEquiv f

Premises used: RingHomInvPair.of_ringEquiv
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : CommRing K
inst_5 : CommRing L
inst_6 : Algebra R K
inst_7 : Algebra S L
inst_8 : IsFractionRing R K
inst_9 : IsFractionRing S L
f : R ≃+* S
I : Submodule R K
hI : IsFractional R⁰ I
simp :
  ∀ (hI : ∃ (a : R), ¬a = 0 ∧ ∀ b ∈ I, IsInteger R (a • b)),
    ∃ (a : S),
      ¬a = 0 ∧
        ∀ a_1 ∈ I,
          IsInteger S
            (HSMul.hSMul (β := L) a
              (((↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L) : (a : K) → L) a_1 : L))
⊢ IsFractional S⁰ (Submodule.map (↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L) I)

Tactic:
simp only [IsFractional, mem_nonZeroDivisors_iff_ne_zero, ne_eq, Submodule.mem_map,
    forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] at hI ⊢

Premises used: Submodule.mem_map, and_imp, IsFractional, forall_exists_index, ne_eq, mem_nonZeroDivisors_iff_ne_zero, forall_apply_eq_imp_iff₂
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : CommRing K
inst_5 : CommRing L
inst_6 : Algebra R K
inst_7 : Algebra S L
inst_8 : IsFractionRing R K
inst_9 : IsFractionRing S L
f : R ≃+* S
I : Submodule R K
hI : ∃ (a : R), ¬a = 0 ∧ ∀ b ∈ I, IsInteger R (a • b)
obtain :
  ∀ (r : R) (hr0 : ¬r = 0) (hr : ∀ b ∈ I, IsInteger R (r • b)),
    ∃ (a : S),
      ¬a = 0 ∧
        ∀ a_1 ∈ I,
          IsInteger S
            (HSMul.hSMul (β := L) a
              (((↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L) : (a : K) → L) a_1 : L))
⊢ ∃ (a : S),
    ¬a = 0 ∧
      ∀ a_1 ∈ I,
        IsInteger S
          (HSMul.hSMul (β := L) a
            (((↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L) : (a : K) → L) a_1 : L))

Tactic:
obtain ⟨r, hr0, hr⟩ := hI
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : CommRing K
inst_5 : CommRing L
inst_6 : Algebra R K
inst_7 : Algebra S L
inst_8 : IsFractionRing R K
inst_9 : IsFractionRing S L
f : R ≃+* S
I : Submodule R K
r : R
hr0 : ¬r = 0
hr : ∀ b ∈ I, IsInteger R (r • b)
h :
  ¬Eq.{u_6 + 1} (α := S) ((f : (a : R) → S) r : S) (0 : S) ∧
    ∀ a ∈ I,
      IsInteger S
        (HSMul.hSMul.{u_6, u_8, u_8} (α := S) (β := L) ((f : (a : R) → S) r : S)
          (((↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L) : (a : K) → L) a : L))
⊢ ∃ (a : S),
    ¬a = 0 ∧
      ∀ a_1 ∈ I,
        IsInteger S
          (HSMul.hSMul (β := L) a
            (((↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L) : (a : K) → L) a_1 : L))

Tactic:
use f r

Premises used: DFunLike.coe
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : CommRing K
inst_5 : CommRing L
inst_6 : Algebra R K
inst_7 : Algebra S L
inst_8 : IsFractionRing R K
inst_9 : IsFractionRing S L
f : R ≃+* S
I : Submodule R K
r : R
hr0 : ¬r = 0
hr : ∀ b ∈ I, IsInteger R (r • b)
⊢ ¬Eq.{u_6 + 1} (α := S) ((f : (a : R) → S) r : S) (0 : S)

Tactic:
simp [hr0]
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : CommRing K
inst_5 : CommRing L
inst_6 : Algebra R K
inst_7 : Algebra S L
inst_8 : IsFractionRing R K
inst_9 : IsFractionRing S L
f : R ≃+* S
I : Submodule R K
r : R
hr0 : ¬r = 0
hr : ∀ b ∈ I, IsInteger R (r • b)
h :
  ∀ a ∈ I,
    IsInteger S
      (HSMul.hSMul.{u_6, u_8, u_8} (α := S) (β := L) ((f : (a : R) → S) r : S)
        (((↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L) : (a : K) → L) a : L))
⊢ ¬Eq.{u_6 + 1} (α := S) ((f : (a : R) → S) r : S) (0 : S) ∧
    ∀ a ∈ I,
      IsInteger S
        (HSMul.hSMul.{u_6, u_8, u_8} (α := S) (β := L) ((f : (a : R) → S) r : S)
          (((↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L) : (a : K) → L) a : L))

Tactic:
refine ⟨by simp [hr0], ?_⟩
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : CommRing K
inst_5 : CommRing L
inst_6 : Algebra R K
inst_7 : Algebra S L
inst_8 : IsFractionRing R K
inst_9 : IsFractionRing S L
f : R ≃+* S
I : Submodule R K
r : R
hr0 : ¬r = 0
hr : ∀ b ∈ I, IsInteger R (r • b)
x : K
hx : x ∈ I
⊢ IsInteger R (r • x)

Tactic:
specialize hr x hx
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : CommRing K
inst_5 : CommRing L
inst_6 : Algebra R K
inst_7 : Algebra S L
inst_8 : IsFractionRing R K
inst_9 : IsFractionRing S L
f : R ≃+* S
I : Submodule R K
r : R
hr0 : ¬r = 0
x : K
hx : x ∈ I
hr : IsInteger R (r • x)
⊢ ∃ (x_1 : R), (algebraMap R K : (a : R) → K) x_1 = r • x

Tactic:
simp only [IsLocalization.IsInteger, RingHom.mem_rangeS] at hr ⊢

Premises used: IsLocalization.IsInteger, RingHom.mem_rangeS