awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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
⊢ I = 0

Tactic:
rw [h, Ideal.zero_eq_bot, coeIdeal_bot, mul_zero] at haJ

Premises used: Ideal.zero_eq_bot, MulZeroClass.mul_zero, FractionalIdeal.coeIdeal_bot
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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
haJ₁ : I = 0
⊢ J = 0

Tactic:
rw [h, Ideal.zero_eq_bot, coeIdeal_bot, mul_zero] at haJ

Premises used: Ideal.zero_eq_bot, MulZeroClass.mul_zero, FractionalIdeal.coeIdeal_bot
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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 = 0
h : J = 0
⊢ False

Tactic:
hI haJ
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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 = 0
h : J = 0
⊢ False

Tactic:
exact hI haJ
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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
⊢ a = 0

Tactic:
rw [Ideal.zero_eq_bot, Ideal.span_singleton_eq_bot] at h

Premises used: Ideal.span_singleton_eq_bot, Ideal.zero_eq_bot
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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
⊢ I = 0

Tactic:
rw [h, map_zero, inv_zero, spanSingleton_zero, zero_mul] at haJ

Premises used: inv_zero, MulZeroClass.zero_mul, map_zero, FractionalIdeal.spanSingleton_zero
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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
haJ₁ : I = 0
⊢ a = 0

Tactic:
rw [h, map_zero, inv_zero, spanSingleton_zero, zero_mul] at haJ

Premises used: inv_zero, MulZeroClass.zero_mul, map_zero, FractionalIdeal.spanSingleton_zero
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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 = 0
h : a = 0
⊢ False

Tactic:
hI haJ
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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 = 0
h : a = 0
⊢ False

Tactic:
exact hI haJ
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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
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
⊢ (↑I : Submodule R K).IsPrincipal

Tactic:
obtain ⟨a, aI, -, ha⟩ := exists_eq_spanSingleton_mul I

Premises used: FractionalIdeal.exists_eq_spanSingleton_mul
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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 :
  (↑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)
⊢ (↑I : Submodule R K).IsPrincipal

Tactic:
use (algebraMap R K a)⁻¹ * algebraMap R K (generator aI)

Premises used: Algebra.algebraMap, Submodule.IsPrincipal.generator, DFunLike.coe
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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 =
    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))
      ⋯

Tactic:
rw [spanSingleton] at this

Premises used: FractionalIdeal.spanSingleton
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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 =
    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))
      ⋯
⊢ (↑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:
congr_arg Subtype.val this

Premises used: congr_arg, FractionalIdeal.coeToSubmodule, Submodule.span, Subtype.val
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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 =
    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))
      ⋯
⊢ (↑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:
exact congr_arg Subtype.val this

Premises used: congr_arg, Subtype.val
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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 :
  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)

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
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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)
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)
| I

Tactic:
rw [ha, ← span_singleton_generator aI]

Premises used: Submodule.IsPrincipal.span_singleton_generator
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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)
      ((↑(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))
⊢ 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:
conv_lhs => rw [ha, ← span_singleton_generator aI]

Premises used: Submodule.IsPrincipal.span_singleton_generator
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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))
h₂ 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)))
⊢ 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:
rw [Ideal.submodule_span_eq, coeIdeal_span_singleton (generator aI),
    spanSingleton_mul_spanSingleton]

Premises used: FractionalIdeal.coeIdeal_span_singleton, Ideal.submodule_span_eq, FractionalIdeal.spanSingleton_mul_spanSingleton, Submodule.IsPrincipal.generator
-- 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
I J : FractionalIdeal S P
⊢ (∀ {zI : P}, zI ∈ I → zI ∈ spanSingleton S x * J) ↔ ∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI

Tactic:
simp only [mem_singleton_mul, eq_comm]

Premises used: eq_comm, FractionalIdeal.mem_singleton_mul
-- 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
I J : FractionalIdeal S P
simp : (∀ (i : P), (∃ (z : R), z • x = i) → ∀ j ∈ I, i * j ∈ J) ↔ ∀ z ∈ I, x * z ∈ J
⊢ spanSingleton S x * I ≤ J ↔ ∀ z ∈ I, x * z ∈ J

Tactic:
simp only [mul_le, mem_spanSingleton]

Premises used: FractionalIdeal.mem_spanSingleton, FractionalIdeal.mul_le
-- 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
I J : FractionalIdeal S P
mp : (∀ (i : P), (∃ (z : R), z • x = i) → ∀ j ∈ I, i * j ∈ J) → ∀ z ∈ I, x * z ∈ J
mpr : (∀ z ∈ I, x * z ∈ J) → ∀ (i : P), (∃ (z : R), z • x = i) → ∀ j ∈ I, i * j ∈ J
⊢ (∀ (i : P), (∃ (z : R), z • x = i) → ∀ j ∈ I, i * j ∈ J) ↔ ∀ z ∈ I, x * z ∈ J

Tactic:
constructor
-- 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
I J : FractionalIdeal S P
h : ∀ (i : P), (∃ (z : R), z • x = i) → ∀ j ∈ I, i * j ∈ J
zI : P
hzI : zI ∈ I
⊢ x * zI ∈ J

Tactic:
h x ⟨1, one_smul _ _⟩ zI hzI

Premises used: one_smul, Exists.intro, OfNat.ofNat
-- 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
I J : FractionalIdeal S P
h : ∀ (i : P), (∃ (z : R), z • x = i) → ∀ j ∈ I, i * j ∈ J
zI : P
hzI : zI ∈ I
⊢ x * zI ∈ J

Tactic:
exact h x ⟨1, one_smul _ _⟩ zI hzI

Premises used: one_smul, Exists.intro, OfNat.ofNat
-- 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
I J : FractionalIdeal S P
h : ∀ z ∈ I, x * z ∈ J
z : R
zI : P
hzI : zI ∈ I
mpr : z • (x * zI) ∈ J
⊢ z • x * zI ∈ J

Tactic:
rw [Algebra.smul_mul_assoc]

Premises used: Algebra.smul_mul_assoc
-- 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
I J : FractionalIdeal S P
h : ∀ z ∈ I, x * z ∈ J
z : R
zI : P
hzI : zI ∈ I
⊢ z • (x * zI) ∈ J

Tactic:
Submodule.smul_mem J.1 _ (h zI hzI)

Premises used: Set.Mem, Subtype.val, Submodule.smul_mem
-- 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
I J : FractionalIdeal S P
h : ∀ z ∈ I, x * z ∈ J
z : R
zI : P
hzI : zI ∈ I
⊢ z • (x * zI) ∈ J

Tactic:
exact Submodule.smul_mem J.1 _ (h zI hzI)

Premises used: Subtype.val, Submodule.smul_mem
-- 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
I J : FractionalIdeal S P
⊢ I = spanSingleton S x * J ↔ (∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI) ∧ ∀ z ∈ J, x * z ∈ I

Tactic:
simp only [le_antisymm_iff, le_spanSingleton_mul_iff, spanSingleton_mul_le_iff]

Premises used: FractionalIdeal.le_spanSingleton_mul_iff, FractionalIdeal.spanSingleton_mul_le_iff, le_antisymm_iff
-- 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
I : FractionalIdeal S P
rw : ∀ z ∈ I, HMul.hMul (α := P) ((algebraMap R P : (a : R) → P) (↑I.den : R) : P) z ∈ I
⊢ (↑I.num : FractionalIdeal S P) ≤ I

Tactic:
rw [← I.den_mul_self_eq_num', spanSingleton_mul_le_iff]

Premises used: FractionalIdeal.spanSingleton_mul_le_iff, FractionalIdeal.den_mul_self_eq_num'
-- 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
I : FractionalIdeal S P
z : P
h : z ∈ I
rw : (↑I.den : R) • z ∈ I
⊢ HMul.hMul (α := P) ((algebraMap R P : (a : R) → P) (↑I.den : R) : P) z ∈ I

Tactic:
rw [← Algebra.smul_def]

Premises used: Algebra.smul_def
-- 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
I : FractionalIdeal S P
z : P
h : z ∈ I
⊢ (↑I.den : R) • z ∈ I

Tactic:
Submodule.smul_mem _ _ h

Premises used: Set.Mem, Submodule.smul_mem
-- 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
I : FractionalIdeal S P
z : P
h : z ∈ I
⊢ (↑I.den : R) • z ∈ I

Tactic:
exact Submodule.smul_mem _ _ h

Premises used: Submodule.smul_mem