awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
S : 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 : Type u_4
inst_4 : Field K
inst_5 : Algebra R₁ K
inst_6 : IsFractionRing R₁ K
inst_7 : IsLocalization S P
inst_8 : IsDomain R₁
R : Type u_5
inst_9 : CommRing R
inst_10 : IsDomain R
inst_11 : IsPrincipalIdealRing R
inst_12 : Algebra R K
inst_13 : IsFractionRing R K
I : FractionalIdeal.{u_5, u_4} (R := R) R⁰ K
a : R
aI : Ideal R
ha :
  I =
    HMul.hMul (α := FractionalIdeal.{u_5, u_4} (R := R) R⁰ K) (β := FractionalIdeal.{u_5, u_4} (R := R) R⁰ K)
      (spanSingleton R⁰ ((algebraMap R K : (a : R) → K) a)⁻¹ : FractionalIdeal.{u_5, u_4} (R := R) R⁰ K)
      ((↑aI : FractionalIdeal.{u_5, u_4} (R := R) R⁰ K) : FractionalIdeal.{u_5, u_4} (R := R) R⁰ K)
h :
  HMul.hMul (α := FractionalIdeal.{u_5, u_4} (R := R) R⁰ K) (β := FractionalIdeal.{u_5, u_4} (R := R) R⁰ K)
      (spanSingleton R⁰ ((algebraMap R K : (a : R) → K) a)⁻¹ : FractionalIdeal.{u_5, u_4} (R := R) R⁰ K)
      ((↑(Ideal.span {generator aI}) : FractionalIdeal.{u_5, u_4} (R := R) R⁰ K) :
        FractionalIdeal.{u_5, u_4} (R := R) R⁰ K) =
    spanSingleton R⁰
      (HMul.hMul (α := K) (β := K) (((algebraMap R K : (a : R) → K) a)⁻¹ : K)
        ((algebraMap R K : (a : R) → K) (generator aI) : K))
h₁ :
  HMul.hMul (α := FractionalIdeal.{u_5, u_4} (R := R) R⁰ K) (β := FractionalIdeal.{u_5, u_4} (R := R) R⁰ K)
      (spanSingleton R⁰ ((algebraMap R K : (a : R) → K) a)⁻¹ : FractionalIdeal.{u_5, u_4} (R := R) R⁰ K)
      (spanSingleton R⁰ ((algebraMap R K : (a : R) → K) (generator aI)) : FractionalIdeal.{u_5, u_4} (R := R) R⁰ K) =
    spanSingleton R⁰
      (HMul.hMul (α := K) (β := K) (((algebraMap R K : (a : R) → K) a)⁻¹ : K)
        ((algebraMap R K : (a : R) → K) (generator aI) : K))
⊢ HMul.hMul (α := FractionalIdeal.{u_5, u_4} (R := R) R⁰ K) (β := FractionalIdeal.{u_5, u_4} (R := R) R⁰ K)
      (spanSingleton R⁰ ((algebraMap R K : (a : R) → K) a)⁻¹ : FractionalIdeal.{u_5, u_4} (R := R) R⁰ K)
      ((↑(R ∙ generator aI) : FractionalIdeal.{u_5, u_4} (R := R) R⁰ K) : FractionalIdeal.{u_5, u_4} (R := R) R⁰ K) =
    spanSingleton R⁰
      (HMul.hMul (α := K) (β := K) (((algebraMap R K : (a : R) → K) a)⁻¹ : K)
        ((algebraMap R K : (a : R) → K) (generator aI) : K))
have h₂ : Eq (α := FractionalIdeal.{u_5, u_4} (R := R) R⁰ K)
  (spanSingleton R⁰
    (HMul.hMul (α := K) (β := K) (((algebraMap R K : (a : R) → K) a)⁻¹ : K)
      ((algebraMap R K : (a : R) → K) (generator aI) : K)))
  (spanSingleton R⁰
    (HMul.hMul (α := K) (β := K) (((algebraMap R K : (a : R) → K) a)⁻¹ : K)
      ((algebraMap R K : (a : R) → K) (generator aI) : K)))
Tactic: rw [Ideal.submodule_span_eq, coeIdeal_span_singleton (generator aI),
    spanSingleton_mul_spanSingleton]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
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
I J : FractionalIdeal S P
⊢ spanSingleton S x * I ≤ J ↔ ∀ z ∈ I, x * z ∈ J
have simp : (∀ (i : P), (∃ (z : R), z • x = i) → ∀ j ∈ I, i * j ∈ J) ↔ ∀ z ∈ I, x * z ∈ J
Tactic: simp only [mul_le, mem_spanSingleton]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
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
I J : FractionalIdeal S P
⊢ (∀ (i : P), (∃ (z : R), z • x = i) → ∀ j ∈ I, i * j ∈ J) ↔ ∀ z ∈ I, x * z ∈ J
have mp : (∀ (i : P), (∃ (z : R), z • x = i) → ∀ j ∈ I, i * j ∈ J) → ∀ z ∈ I, x * z ∈ J
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
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
I J : FractionalIdeal S P
mp : (∀ (i : P), (∃ (z : R), z • x = i) → ∀ j ∈ I, i * j ∈ J) → ∀ z ∈ I, x * z ∈ J
⊢ (∀ (i : P), (∃ (z : R), z • x = i) → ∀ j ∈ I, i * j ∈ J) ↔ ∀ z ∈ I, x * z ∈ J
have mpr : (∀ z ∈ I, x * z ∈ J) → ∀ (i : P), (∃ (z : R), z • x = i) → ∀ j ∈ I, i * j ∈ J
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
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
I J : FractionalIdeal S P
h : ∀ z ∈ I, x * z ∈ J
z : R
zI : P
hzI : zI ∈ I
⊢ z • x * zI ∈ J
have mpr : z • (x * zI) ∈ J
Tactic: rw [Algebra.smul_mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
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
I : FractionalIdeal S P
⊢ (↑I.num : FractionalIdeal S P) ≤ I
have rw : ∀ z ∈ I, HMul.hMul (α := P) ((algebraMap R P : (a : R) → P) (↑I.den : R) : P) z ∈ I
Tactic: rw [← I.den_mul_self_eq_num', spanSingleton_mul_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
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
I : FractionalIdeal S P
z : P
h : z ∈ I
⊢ HMul.hMul (α := P) ((algebraMap R P : (a : R) → P) (↑I.den : R) : P) z ∈ I
have rw : (↑I.den : R) • z ∈ I
Tactic: rw [← Algebra.smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (hypothesis)
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.FG
have hI₁ : I = ⊥
Tactic: rw [coe_zero, le_bot_iff] at hI
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
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 = ⊥
⊢ I.FG
have rw : FG.{u_3, u_4} (R := R₁) (M := K) ⊥
Tactic: rw [hI]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
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₁
⊢ IsNoetherian.{u_3, u_4} R₁ ↥(↑(↑I : FractionalIdeal R₁⁰ K) : Submodule R₁ K)
have rw : ∀ J ≤ (↑I : FractionalIdeal R₁⁰ K), (↑J : Submodule R₁ K).FG
Tactic: rw [isNoetherian_iff]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
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)
⊢ (↑J : Submodule R₁ K).FG
have 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)
Tactic: obtain ⟨J, rfl⟩ := le_one_iff_exists_coeIdeal.mp (le_trans hJ coeIdeal_le_one)
Cleared hypotheses: J, hJ
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
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)
⊢ 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)
have 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)
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
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)
⊢ 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)
have 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)
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
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₁
    ↥(↑(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)
have pos : IsNoetherian.{u_3, u_4} R₁ ↥(↑0 : Submodule R₁ K)
Tactic: rw [hx, map_zero, inv_zero, spanSingleton_zero, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (hypothesis)
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₁
    ↥(↑(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)
have h_gx : 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
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (hypothesis)
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)
⊢ 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)
have 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)
Tactic: have h_spanx : spanSingleton R₁⁰ (algebraMap R₁ K x) ≠ 0 := spanSingleton_ne_zero_iff.mpr h_gx
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
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)
⊢ 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)
have 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
Tactic: rw [isNoetherian_iff] at hI ⊢
Cleared hypotheses: hI, hx, h_gx, h_spanx
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (hypothesis)
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
⊢ (↑J : Submodule R₁ K).FG
have 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
Tactic: rw [← div_spanSingleton, le_div_iff_mul_le h_spanx] at hJ
Cleared hypotheses: hJ
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
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
⊢ (↑J : Submodule R₁ K).FG
have 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
Tactic: obtain ⟨s, hs⟩ := hI _ hJ
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
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)
⊢ (↑J : Submodule R₁ K).FG
have h : span R₁ (↑(s * singleton (α := K) (((algebraMap R₁ K : (a : R₁) → K) x)⁻¹ : K)) : Set K) = (↑J : Submodule R₁ K)
Tactic: use s * {(algebraMap R₁ K x)⁻¹}
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
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)
⊢ span R₁ (↑(s * singleton (α := K) (((algebraMap R₁ K : (a : R₁) → K) x)⁻¹ : K)) : Set K) = (↑J : Submodule R₁ K)
have h : span R₁ ((↑s : Set K) * (↑(singleton (α := K) (((algebraMap R₁ K : (a : R₁) → K) x)⁻¹ : K)) : Set K)) =
  (↑J : Submodule R₁ K)
Tactic: rw [Finset.coe_mul, Finset.coe_singleton, ← span_mul_span, hs, ← coe_spanSingleton R₁⁰, ←
    coe_mul, mul_assoc, spanSingleton_mul_spanSingleton, mul_inv_cancel₀ h_gx, spanSingleton_one,
    mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
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 : Set K) * (↑(singleton (α := K) (((algebraMap R₁ K : (a : R₁) → K) x)⁻¹ : K)) : Set K)) =
    (↑J : Submodule R₁ K)
⊢ span R₁ (↑(s * singleton (α := K) (((algebraMap R₁ K : (a : R₁) → K) x)⁻¹ : K)) : Set K) = (↑J : Submodule R₁ K)
have h₁ : span R₁ ((↑s : Set K) * singleton (α := K) (((algebraMap R₁ K : (a : R₁) → K) x)⁻¹ : K)) = (↑J : Submodule R₁ K)
Tactic: rw [Finset.coe_mul, Finset.coe_singleton, ← span_mul_span, hs, ← coe_spanSingleton R₁⁰, ←
    coe_mul, mul_assoc, spanSingleton_mul_spanSingleton, mul_inv_cancel₀ h_gx, spanSingleton_one,
    mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
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 : Set K) * (↑(singleton (α := K) (((algebraMap R₁ K : (a : R₁) → K) x)⁻¹ : K)) : Set K)) =
    (↑J : Submodule R₁ K)
h₁ : span R₁ ((↑s : Set K) * singleton (α := K) (((algebraMap R₁ K : (a : R₁) → K) x)⁻¹ : K)) = (↑J : Submodule R₁ K)
⊢ span R₁ (↑(s * singleton (α := K) (((algebraMap R₁ K : (a : R₁) → K) x)⁻¹ : K)) : Set K) = (↑J : Submodule R₁ K)
have h₂ : HMul.hMul (α := Submodule R₁ K) (span R₁ (↑s : Set K))
    (span R₁ (singleton (α := K) (((algebraMap R₁ K : (a : R₁) → K) x)⁻¹ : K))) =
  (↑J : Submodule R₁ K)
Tactic: rw [Finset.coe_mul, Finset.coe_singleton, ← span_mul_span, hs, ← coe_spanSingleton R₁⁰, ←
    coe_mul, mul_assoc, spanSingleton_mul_spanSingleton, mul_inv_cancel₀ h_gx, spanSingleton_one,
    mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
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 : Set K) * (↑(singleton (α := K) (((algebraMap R₁ K : (a : R₁) → K) x)⁻¹ : K)) : Set K)) =
    (↑J : Submodule R₁ K)
h₁ : span R₁ ((↑s : Set K) * singleton (α := K) (((algebraMap R₁ K : (a : R₁) → K) x)⁻¹ : K)) = (↑J : Submodule R₁ K)
h₂ :
  HMul.hMul (α := Submodule R₁ K) (span R₁ (↑s : Set K))
      (span R₁ (singleton (α := K) (((algebraMap R₁ K : (a : R₁) → K) x)⁻¹ : K))) =
    (↑J : Submodule R₁ K)
⊢ span R₁ (↑(s * singleton (α := K) (((algebraMap R₁ K : (a : R₁) → K) x)⁻¹ : K)) : Set K) = (↑J : Submodule R₁ K)
have h₃ : (↑(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) *
    span R₁ (singleton (α := K) (((algebraMap R₁ K : (a : R₁) → K) x)⁻¹ : K)) =
  (↑J : Submodule R₁ K)
Tactic: rw [Finset.coe_mul, Finset.coe_singleton, ← span_mul_span, hs, ← coe_spanSingleton R₁⁰, ←
    coe_mul, mul_assoc, spanSingleton_mul_spanSingleton, mul_inv_cancel₀ h_gx, spanSingleton_one,
    mul_one]