awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₁
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
a_inv : R₁
nonzero_1 : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) a_inv
ha : ∀ b ∈ (↑I : Submodule R₁ K), IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
map_a_nonzero : Ne.{u_4 + 1} (α := K) ((algebraMap R₁ K : (a : R₁) → K) a_inv : K) (0 : K)
x' : R₁
hx'_1 :
  x' ∈
    comap (Algebra.linearMap R₁ K)
      (↑(HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
            (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) a_inv) : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
            I) :
        Submodule R₁ K)
hy :
  Membership.mem.{u_4, u_4} (α := K) (γ := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
    (↑(comap (Algebra.linearMap R₁ K)
          (↑(HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
                (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) a_inv) :
                  FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
                I) :
            Submodule R₁ K)) :
      FractionalIdeal R₁⁰ K)
    ((algebraMap R₁ K : (a : R₁) → K) x' : K)
y' : K
hy' : y' ∈ I
hx' : (Algebra.linearMap R₁ K : (a : R₁) → K) x' = HMul.hMul (α := K) ((algebraMap R₁ K : (a : R₁) → K) a_inv : K) y'
⊢ HMul.hMul (α := K) (β := K) (((algebraMap R₁ K : (a : R₁) → K) a_inv)⁻¹ : K)
      ((algebraMap R₁ K : (a : R₁) → K) x' : K) ∈
    I
have hx'₁ : (algebraMap R₁ K : (a : R₁) → K) x' = HMul.hMul (α := K) ((algebraMap R₁ K : (a : R₁) → K) a_inv : K) y'
Tactic: rw [Algebra.linearMap_apply] at hx'
Cleared hypotheses: hx'
-- 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₁
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
a_inv : R₁
nonzero_1 : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) a_inv
ha : ∀ b ∈ (↑I : Submodule R₁ K), IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
map_a_nonzero : Ne.{u_4 + 1} (α := K) ((algebraMap R₁ K : (a : R₁) → K) a_inv : K) (0 : K)
x' : R₁
hx'_1 :
  x' ∈
    comap (Algebra.linearMap R₁ K)
      (↑(HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
            (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) a_inv) : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
            I) :
        Submodule R₁ K)
hy :
  Membership.mem.{u_4, u_4} (α := K) (γ := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
    (↑(comap (Algebra.linearMap R₁ K)
          (↑(HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
                (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) a_inv) :
                  FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
                I) :
            Submodule R₁ K)) :
      FractionalIdeal R₁⁰ K)
    ((algebraMap R₁ K : (a : R₁) → K) x' : K)
y' : K
hy' : y' ∈ I
hx' : (algebraMap R₁ K : (a : R₁) → K) x' = HMul.hMul (α := K) ((algebraMap R₁ K : (a : R₁) → K) a_inv : K) y'
⊢ HMul.hMul (α := K) (β := K) (((algebraMap R₁ K : (a : R₁) → K) a_inv)⁻¹ : K)
      ((algebraMap R₁ K : (a : R₁) → K) x' : K) ∈
    I
have refine_2 : HMul.hMul (α := K) (((algebraMap R₁ K : (a : R₁) → K) a_inv)⁻¹ : K)
    (HMul.hMul (α := K) ((algebraMap R₁ K : (a : R₁) → K) a_inv : K) y') ∈
  I
Tactic: rwa [hx', ← mul_assoc, inv_mul_cancel₀ map_a_nonzero, one_mul]
-- 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₁
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
a_inv : R₁
nonzero_1 : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) a_inv
ha : ∀ b ∈ (↑I : Submodule R₁ K), IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
map_a_nonzero : Ne.{u_4 + 1} (α := K) ((algebraMap R₁ K : (a : R₁) → K) a_inv : K) (0 : K)
x' : R₁
hx'_1 :
  x' ∈
    comap (Algebra.linearMap R₁ K)
      (↑(HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
            (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) a_inv) : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
            I) :
        Submodule R₁ K)
hy :
  Membership.mem.{u_4, u_4} (α := K) (γ := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
    (↑(comap (Algebra.linearMap R₁ K)
          (↑(HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
                (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) a_inv) :
                  FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
                I) :
            Submodule R₁ K)) :
      FractionalIdeal R₁⁰ K)
    ((algebraMap R₁ K : (a : R₁) → K) x' : K)
y' : K
hy' : y' ∈ I
hx' : (algebraMap R₁ K : (a : R₁) → K) x' = HMul.hMul (α := K) ((algebraMap R₁ K : (a : R₁) → K) a_inv : K) y'
refine_2 :
  HMul.hMul (α := K) (((algebraMap R₁ K : (a : R₁) → K) a_inv)⁻¹ : K)
      (HMul.hMul (α := K) ((algebraMap R₁ K : (a : R₁) → K) a_inv : K) y') ∈
    I
⊢ HMul.hMul (α := K) (β := K) (((algebraMap R₁ K : (a : R₁) → K) a_inv)⁻¹ : K)
      ((algebraMap R₁ K : (a : R₁) → K) x' : K) ∈
    I
have refine_2₁ : HMul.hMul (α := K) (β := K) (((algebraMap R₁ K : (a : R₁) → K) a_inv)⁻¹ : K)
      ((algebraMap R₁ K : (a : R₁) → K) a_inv : K) *
    y' ∈
  I
Tactic: rwa [hx', ← mul_assoc, inv_mul_cancel₀ map_a_nonzero, one_mul]
-- 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₁
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
a_inv : R₁
nonzero_1 : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) a_inv
ha : ∀ b ∈ (↑I : Submodule R₁ K), IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
map_a_nonzero : Ne.{u_4 + 1} (α := K) ((algebraMap R₁ K : (a : R₁) → K) a_inv : K) (0 : K)
x' : R₁
hx'_1 :
  x' ∈
    comap (Algebra.linearMap R₁ K)
      (↑(HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
            (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) a_inv) : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
            I) :
        Submodule R₁ K)
hy :
  Membership.mem.{u_4, u_4} (α := K) (γ := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
    (↑(comap (Algebra.linearMap R₁ K)
          (↑(HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
                (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) a_inv) :
                  FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
                I) :
            Submodule R₁ K)) :
      FractionalIdeal R₁⁰ K)
    ((algebraMap R₁ K : (a : R₁) → K) x' : K)
y' : K
hy' : y' ∈ I
hx' : (algebraMap R₁ K : (a : R₁) → K) x' = HMul.hMul (α := K) ((algebraMap R₁ K : (a : R₁) → K) a_inv : K) y'
refine_2 :
  HMul.hMul (α := K) (((algebraMap R₁ K : (a : R₁) → K) a_inv)⁻¹ : K)
      (HMul.hMul (α := K) ((algebraMap R₁ K : (a : R₁) → K) a_inv : K) y') ∈
    I
refine_2₁ :
  HMul.hMul (α := K) (β := K) (((algebraMap R₁ K : (a : R₁) → K) a_inv)⁻¹ : K)
        ((algebraMap R₁ K : (a : R₁) → K) a_inv : K) *
      y' ∈
    I
⊢ HMul.hMul (α := K) (β := K) (((algebraMap R₁ K : (a : R₁) → K) a_inv)⁻¹ : K)
      ((algebraMap R₁ K : (a : R₁) → K) x' : K) ∈
    I
have refine_2₂ : 1 * y' ∈ I
Tactic: rwa [hx', ← mul_assoc, inv_mul_cancel₀ map_a_nonzero, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (hypothesis)
Goal:
R : Type u_6
inst : CommRing R
K : Type u_5
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
I : FractionalIdeal.{u_6, u_5} (R := R) R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ :
  I =
    HMul.hMul (α := FractionalIdeal.{u_6, u_5} (R := R) R⁰ K) (β := FractionalIdeal.{u_6, u_5} (R := R) R⁰ K)
      (spanSingleton R⁰ ((algebraMap R K : (a : R) → K) a)⁻¹ : FractionalIdeal.{u_6, u_5} (R := R) R⁰ K)
      ((↑J : FractionalIdeal.{u_6, u_5} (R := R) R⁰ K) : FractionalIdeal.{u_6, u_5} (R := R) R⁰ K)
h : J = 0
⊢ False
have haJ₁ : I = 0
Tactic: rw [h, Ideal.zero_eq_bot, coeIdeal_bot, mul_zero] at haJ
Cleared hypotheses: haJ, h
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (hypothesis)
Goal:
R : Type u_6
inst : CommRing R
K : Type u_5
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
I : FractionalIdeal.{u_6, u_5} (R := R) R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ :
  I =
    HMul.hMul (α := FractionalIdeal.{u_6, u_5} (R := R) R⁰ K) (β := FractionalIdeal.{u_6, u_5} (R := R) R⁰ K)
      (spanSingleton R⁰ ((algebraMap R K : (a : R) → K) a)⁻¹ : FractionalIdeal.{u_6, u_5} (R := R) R⁰ K)
      ((↑J : FractionalIdeal.{u_6, u_5} (R := R) R⁰ K) : FractionalIdeal.{u_6, u_5} (R := R) R⁰ K)
h : Eq (α := Ideal R) (Ideal.span {a}) 0
⊢ False
have h₁ : a = 0
Tactic: rw [Ideal.zero_eq_bot, Ideal.span_singleton_eq_bot] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (hypothesis)
Goal:
R : Type u_6
inst : CommRing R
K : Type u_5
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
I : FractionalIdeal.{u_6, u_5} (R := R) R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ :
  I =
    HMul.hMul (α := FractionalIdeal.{u_6, u_5} (R := R) R⁰ K) (β := FractionalIdeal.{u_6, u_5} (R := R) R⁰ K)
      (spanSingleton R⁰ ((algebraMap R K : (a : R) → K) a)⁻¹ : FractionalIdeal.{u_6, u_5} (R := R) R⁰ K)
      ((↑J : FractionalIdeal.{u_6, u_5} (R := R) R⁰ K) : FractionalIdeal.{u_6, u_5} (R := R) R⁰ K)
h : a = 0
⊢ False
have haJ₁ : I = 0
Tactic: rw [h, map_zero, inv_zero, spanSingleton_zero, zero_mul] at haJ
Cleared hypotheses: haJ, h
-- 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
⊢ (↑I : Submodule R K).IsPrincipal
have obtain : ∀ (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)),
  (↑I : Submodule R K).IsPrincipal
Tactic: obtain ⟨a, aI, -, ha⟩ := exists_eq_spanSingleton_mul I
-- 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)
⊢ (↑I : Submodule R K).IsPrincipal
have h : (↑I : Submodule R K) =
  R ∙
    HMul.hMul (α := K) (β := K) (((algebraMap R K : (a : R) → K) a)⁻¹ : K)
      ((algebraMap R K : (a : R) → K) (generator aI) : K)
Tactic: use (algebraMap R K a)⁻¹ * algebraMap R K (generator aI)
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (hypothesis)
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)
this :
  I =
    spanSingleton R⁰
      (HMul.hMul (α := K) (β := K) (((algebraMap R K : (a : R) → K) a)⁻¹ : K)
        ((algebraMap R K : (a : R) → K) (generator aI) : K))
⊢ (↑I : Submodule R K) =
    R ∙
      HMul.hMul (α := K) (β := K) (((algebraMap R K : (a : R) → K) a)⁻¹ : K)
        ((algebraMap R K : (a : R) → K) (generator aI) : K)
have this₁ : I =
  Subtype.mk (p := fun (I : Submodule R K) ↦ IsFractional R⁰ I)
    (R ∙
      HMul.hMul (α := K) (β := K) (((algebraMap R K : (a : R) → K) a)⁻¹ : K)
        ((algebraMap R K : (a : R) → K) (generator aI) : K))
    sorry
Tactic: rw [spanSingleton] at this
Cleared hypotheses: this
-- 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)
⊢ (↑I : Submodule R K) =
    R ∙
      HMul.hMul (α := K) (β := K) (((algebraMap R K : (a : R) → K) a)⁻¹ : K)
        ((algebraMap R K : (a : R) → K) (generator aI) : K)
have h : I =
  spanSingleton R⁰
    (HMul.hMul (α := K) (β := K) (((algebraMap R K : (a : R) → K) a)⁻¹ : K)
      ((algebraMap R K : (a : R) → K) (generator aI) : K))
Tactic: suffices I = spanSingleton R⁰ ((algebraMap R K a)⁻¹ * algebraMap R K (generator aI)) by
    rw [spanSingleton] at this
    exact congr_arg Subtype.val this
-- 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)
| I
have rw : 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)
Tactic: rw [ha, ← span_singleton_generator aI]
-- 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)
⊢ I =
    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 : 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))
Tactic: conv_lhs => rw [ha, ← span_singleton_generator aI]
-- 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)
⊢ 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 : 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))
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_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))
⊢ 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₁ : 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))
Tactic: rw [Ideal.submodule_span_eq, coeIdeal_span_singleton (generator aI),
    spanSingleton_mul_spanSingleton]