awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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)
⊢ 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)
    (↑(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)
    ((↑(spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) x)⁻¹) : Submodule R₁ K) : Submodule R₁ 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)
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)
h₄ :
  HMul.hMul (β := Submodule R₁ 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)
      ((↑(spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) x)⁻¹) : Submodule R₁ K) : Submodule R₁ 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)
        (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))
        (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)
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 : 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: classical
  by_cases hx : x = 0
  · rw [hx, map_zero, inv_zero, spanSingleton_zero, zero_mul]
    exact isNoetherian_zero
  have h_gx : algebraMap R₁ K x ≠ 0 :=
    mt ((injective_iff_map_eq_zero (algebraMap R₁ K)).mp (IsFractionRing.injective _ _) x) hx
  have h_spanx : spanSingleton R₁⁰ (algebraMap R₁ K x) ≠ 0 := spanSingleton_ne_zero_iff.mpr h_gx
  rw [isNoetherian_iff] at hI ⊢
  intro J hJ
  rw [← div_spanSingleton, le_div_iff_mul_le h_spanx] at hJ
  obtain ⟨s, hs⟩ := hI _ hJ
  use s * {(algebraMap R₁ K x)⁻¹}
  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 : 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: classical
  by_cases hx : x = 0
  · rw [hx, map_zero, inv_zero, spanSingleton_zero, zero_mul]
    exact isNoetherian_zero
  have h_gx : algebraMap R₁ K x ≠ 0 :=
    mt ((injective_iff_map_eq_zero (algebraMap R₁ K)).mp (IsFractionRing.injective _ _) x) hx
  have h_spanx : spanSingleton R₁⁰ (algebraMap R₁ K x) ≠ 0 := spanSingleton_ne_zero_iff.mpr h_gx
  rw [isNoetherian_iff] at hI ⊢
  intro J hJ
  rw [← div_spanSingleton, le_div_iff_mul_le h_spanx] at hJ
  obtain ⟨s, hs⟩ := hI _ hJ
  use s * {(algebraMap R₁ K x)⁻¹}
  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 : 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 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)
have neg₂ : ∀ (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)
Tactic: classical
  by_cases hx : x = 0
  · rw [hx, map_zero, inv_zero, spanSingleton_zero, zero_mul]
    exact isNoetherian_zero
  have h_gx : algebraMap R₁ K x ≠ 0 :=
    mt ((injective_iff_map_eq_zero (algebraMap R₁ K)).mp (IsFractionRing.injective _ _) x) hx
  have h_spanx : spanSingleton R₁⁰ (algebraMap R₁ K x) ≠ 0 := spanSingleton_ne_zero_iff.mpr h_gx
  rw [isNoetherian_iff] at hI ⊢
  intro J hJ
  rw [← div_spanSingleton, le_div_iff_mul_le h_spanx] at hJ
  obtain ⟨s, hs⟩ := hI _ hJ
  use s * {(algebraMap R₁ K x)⁻¹}
  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 : 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 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)
neg₂ :
  ∀ (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)
⊢ 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) (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)
Tactic: classical
  by_cases hx : x = 0
  · rw [hx, map_zero, inv_zero, spanSingleton_zero, zero_mul]
    exact isNoetherian_zero
  have h_gx : algebraMap R₁ K x ≠ 0 :=
    mt ((injective_iff_map_eq_zero (algebraMap R₁ K)).mp (IsFractionRing.injective _ _) x) hx
  have h_spanx : spanSingleton R₁⁰ (algebraMap R₁ K x) ≠ 0 := spanSingleton_ne_zero_iff.mpr h_gx
  rw [isNoetherian_iff] at hI ⊢
  intro J hJ
  rw [← div_spanSingleton, le_div_iff_mul_le h_spanx] at hJ
  obtain ⟨s, hs⟩ := hI _ hJ
  use s * {(algebraMap R₁ K x)⁻¹}
  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₁
inst_5 : IsNoetherianRing R₁
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
⊢ IsNoetherian.{u_3, u_4} R₁ ↥(↑I : Submodule R₁ K)
have 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)
Tactic: obtain ⟨d, J, _, rfl⟩ := exists_eq_spanSingleton_mul I
Cleared hypotheses: I
-- 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₁
inst_5 : IsNoetherianRing R₁
d : R₁
J : Ideal R₁
left : 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)
have hI : IsNoetherian.{u_3, u_4} R₁ ↥(↑(↑J : FractionalIdeal R₁⁰ K) : Submodule R₁ K)
Tactic: apply isNoetherian_spanSingleton_inv_to_map_mul
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
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
⊢ IsFractional S⁰ (Submodule.map (↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L) I)
have 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))
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 ⊢
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
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)
⊢ ∃ (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))
have 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))
Tactic: obtain ⟨r, hr0, hr⟩ := hI
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
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)
⊢ ∃ (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))
have 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))
Tactic: use f r
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
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) ∧
    ∀ 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))
have 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))
Tactic: refine ⟨by simp [hr0], ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (hypothesis)
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 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) x : L))
have hr₁ : IsInteger R (r • x)
Tactic: specialize hr x hx
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (hypothesis)
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)
⊢ 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) x : L))
have hr₁ : ∃ (x_1 : R), (algebraMap R K : (a : R) → K) x_1 = r • x
Tactic: simp only [IsLocalization.IsInteger, RingHom.mem_rangeS] at hr ⊢
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
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 : ∃ (x_1 : R), (algebraMap R K : (a : R) → K) x_1 = r • x
⊢ ∃ (x_1 : S),
    (algebraMap S L : (a : S) → L) x_1 =
      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) x : L)
have h : ∀ (r' : R) (hr' : (algebraMap R K : (a : R) → K) r' = r • x),
  ∃ (x_1 : S),
    (algebraMap S L : (a : S) → L) x_1 =
      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) x : L)
Tactic: obtain ⟨r', hr'⟩ := hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
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
r' : R
hr' : (algebraMap R K : (a : R) → K) r' = r • x
⊢ ∃ (x_1 : S),
    (algebraMap S L : (a : S) → L) x_1 =
      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) x : L)
have h : (algebraMap S L : (a : S) → L) ((f : (a : R) → S) r' : 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) x : L)
Tactic: use f r'
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
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
r' : R
hr' : (algebraMap R K : (a : R) → K) r' = r • x
⊢ (algebraMap S L : (a : S) → L) ((f : (a : R) → S) r' : 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) x : L)
have h : (algebraMap S L : (a : S) → L) ((f : (a : R) → S) r' : S) =
  HSMul.hSMul.{u_6, u_8, u_8} (α := S) (β := L) ((f : (a : R) → S) r : S)
    ((IsFractionRing.ringEquivOfRingEquiv f : (a : K) → L) x : L)
Tactic: simp only [semilinearEquivOfRingEquiv, RingEquiv.toEquiv_eq_coe, Equiv.toFun_as_coe,
    EquivLike.coe_coe, Equiv.invFun_as_coe, LinearMap.coe_mk, AddHom.coe_mk]