awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
ι : Type u_5
s : Finset ι
f : ι → K
a' : ↥(R₁⁰ : Submonoid R₁)
ha' : ∀ i ∈ s, IsInteger R₁ ((↑a' : R₁) • f i)
x_1 : K
hx : Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) x_1
x y : K
hx_1 : Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) x
refine_3 :
  Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) y →
    IsInteger R₁ ((↑a' : R₁) • x) → IsInteger R₁ ((↑a' : R₁) • y) → IsInteger R₁ ((↑a' : R₁) • (x + y))
⊢ ∀ (hy : Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) y),
    IsInteger R₁ ((↑a' : R₁) • x) → IsInteger R₁ ((↑a' : R₁) • y) → IsInteger R₁ ((↑a' : R₁) • (x + y))

Tactic:
_
-- 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
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
ι : Type u_5
s : Finset ι
f : ι → K
a' : ↥(R₁⁰ : Submonoid R₁)
ha' : ∀ i ∈ s, IsInteger R₁ ((↑a' : R₁) • f i)
x_1 : K
hx_1 : Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) x_1
x y : K
hx_2 : Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) x
hy_1 : Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) y
hx : IsInteger R₁ ((↑a' : R₁) • x)
hy : IsInteger R₁ ((↑a' : R₁) • y)
refine_3 : IsInteger R₁ ((↑a' : R₁) • x + (↑a' : R₁) • y)
⊢ IsInteger R₁ ((↑a' : R₁) • (x + y))

Tactic:
rw [smul_add]

Premises used: smul_add
-- 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
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
ι : Type u_5
s : Finset ι
f : ι → K
a' : ↥(R₁⁰ : Submonoid R₁)
ha' : ∀ i ∈ s, IsInteger R₁ ((↑a' : R₁) • f i)
x_1 : K
hx_1 : Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) x_1
x y : K
hx_2 : Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) x
hy_1 : Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) y
hx : IsInteger R₁ ((↑a' : R₁) • x)
hy : IsInteger R₁ ((↑a' : R₁) • y)
⊢ IsInteger R₁ ((↑a' : R₁) • x + (↑a' : R₁) • y)

Tactic:
IsLocalization.isInteger_add hx hy

Premises used: IsLocalization.isInteger_add
-- 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
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
ι : Type u_5
s : Finset ι
f : ι → K
a' : ↥(R₁⁰ : Submonoid R₁)
ha' : ∀ i ∈ s, IsInteger R₁ ((↑a' : R₁) • f i)
x_1 : K
hx_1 : Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) x_1
x y : K
hx_2 : Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) x
hy_1 : Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) y
hx : IsInteger R₁ ((↑a' : R₁) • x)
hy : IsInteger R₁ ((↑a' : R₁) • y)
⊢ IsInteger R₁ ((↑a' : R₁) • x + (↑a' : R₁) • y)

Tactic:
exact IsLocalization.isInteger_add hx hy

Premises used: IsLocalization.isInteger_add
-- 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
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
ι : Type u_5
s : Finset ι
f : ι → K
a' : ↥(R₁⁰ : Submonoid R₁)
ha' : ∀ i ∈ s, IsInteger R₁ ((↑a' : R₁) • f i)
x_1 : K
hx : Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) x_1
c : R₁
x : K
refine_4 :
  Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) x →
    IsInteger R₁ ((↑a' : R₁) • x) → IsInteger R₁ ((↑a' : R₁) • c • x)
⊢ ∀ (hx : Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) x),
    IsInteger R₁ ((↑a' : R₁) • x) → IsInteger R₁ ((↑a' : R₁) • c • x)

Tactic:
_
-- 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
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
ι : Type u_5
s : Finset ι
f : ι → K
a' : ↥(R₁⁰ : Submonoid R₁)
ha' : ∀ i ∈ s, IsInteger R₁ ((↑a' : R₁) • f i)
x_1 : K
hx_1 : Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) x_1
c : R₁
x : K
hx_2 : Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) x
hx : IsInteger R₁ ((↑a' : R₁) • x)
refine_4 : IsInteger R₁ (c • (↑a' : R₁) • x)
⊢ IsInteger R₁ ((↑a' : R₁) • c • x)

Tactic:
rw [smul_comm]

Premises used: SMulCommClass.smul_comm
-- 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
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
ι : Type u_5
s : Finset ι
f : ι → K
a' : ↥(R₁⁰ : Submonoid R₁)
ha' : ∀ i ∈ s, IsInteger R₁ ((↑a' : R₁) • f i)
x_1 : K
hx_1 : Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) x_1
c : R₁
x : K
hx_2 : Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) x
hx : IsInteger R₁ ((↑a' : R₁) • x)
⊢ IsInteger R₁ (c • (↑a' : R₁) • x)

Tactic:
IsLocalization.isInteger_smul hx

Premises used: IsLocalization.isInteger_smul
-- 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
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
ι : Type u_5
s : Finset ι
f : ι → K
a' : ↥(R₁⁰ : Submonoid R₁)
ha' : ∀ i ∈ s, IsInteger R₁ ((↑a' : R₁) • f i)
x_1 : K
hx_1 : Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) x_1
c : R₁
x : K
hx_2 : Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) x
hx : IsInteger R₁ ((↑a' : R₁) • x)
⊢ IsInteger R₁ (c • (↑a' : R₁) • x)

Tactic:
exact IsLocalization.isInteger_smul hx

Premises used: IsLocalization.isInteger_smul
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
ι : Type u_5
s : Finset ι
f : ι → K
⊢ Eq (α := Submodule R₁ K) (↑(spanFinset R₁ s f) : Submodule R₁ K) (span R₁ (f '' (↑s : Set ι)))

Tactic:
rfl

Premises used: Set.Mem, setOf, FractionalIdeal.coeToSubmodule, Submodule.span, rfl
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
ι : Type u_5
s : Finset ι
f : ι → K
⊢ Eq (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (spanFinset R₁ s f) 0 ↔ ∀ j ∈ s, f j = 0

Tactic:
simp only [← coeToSubmodule_inj, spanFinset_coe, coe_zero, Submodule.span_eq_bot,
    Set.mem_image, Finset.mem_coe, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]

Premises used: and_imp, Submodule.span_eq_bot, Set.mem_image, forall_exists_index, FractionalIdeal.coeToSubmodule_inj, FractionalIdeal.spanFinset_coe, Finset.mem_coe, forall_apply_eq_imp_iff₂, FractionalIdeal.coe_zero
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
ι : Type u_5
s : Finset ι
f : ι → K
⊢ Ne (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (spanFinset R₁ s f) 0 ↔ ∃ j ∈ s, f j ≠ 0

Tactic:
simp
-- 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
⊢ IsFractional S (P := P) (R ∙ x)

Tactic:
let ⟨a, ha⟩ := exists_integer_multiple S x
  isFractional_span_iff.mpr ⟨a, a.2, fun _ hx' => (Set.mem_singleton_iff.mp hx').symm ▸ ha⟩

Premises used: Iff.mpr, FractionalIdeal.isFractional_span_iff, IsFractional, _private.0.FractionalIdeal.isFractional_span_singleton.match_1, Eq.rec, Set.mem_singleton_iff, And.intro, Exists.intro, Submodule.span, Iff.mp, IsLocalization.exists_integer_multiple, Singleton.singleton, Eq.symm, Subtype.val, Subtype.property
-- 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
rw :
  Eq (α := Submodule R P) (↑(Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) (R ∙ x) ⋯) : Submodule R P)
    (R ∙ x)
⊢ Eq (α := Submodule R P) (↑(spanSingleton S x) : Submodule R P) (R ∙ x)

Tactic:
rw [spanSingleton]

Premises used: FractionalIdeal.spanSingleton
-- 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
⊢ Eq (α := Submodule R P) (↑(Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) (R ∙ x) ⋯) : Submodule R P)
    (R ∙ x)

Tactic:
rfl
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
inst_3 : IsLocalization S P
x y : P
rw :
  Membership.mem (γ := FractionalIdeal S P) (Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) (R ∙ y) ⋯) x ↔
    ∃ (z : R), z • y = x
⊢ Membership.mem (γ := FractionalIdeal S P) (spanSingleton S y) x ↔ ∃ (z : R), z • y = x

Tactic:
rw [spanSingleton]

Premises used: FractionalIdeal.spanSingleton
-- 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 y : P
⊢ Membership.mem (γ := FractionalIdeal S P) (Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) (R ∙ y) ⋯) x ↔
    ∃ (z : R), z • y = x

Tactic:
Submodule.mem_span_singleton

Premises used: Set.Mem, Submodule.mem_span_singleton
-- 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 y : P
⊢ Membership.mem (γ := FractionalIdeal S P) (Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) (R ∙ y) ⋯) x ↔
    ∃ (z : R), z • y = x

Tactic:
exact Submodule.mem_span_singleton

Premises used: Submodule.mem_span_singleton
-- 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
⊢ Membership.mem (γ := FractionalIdeal S P) (spanSingleton S x) x

Tactic:
(mem_spanSingleton S).mpr ⟨1, one_smul _ _⟩

Premises used: Iff.mpr, FractionalIdeal.mem_spanSingleton, 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
I : FractionalIdeal S P
a :
  Eq.{u_2 + 1} (α := Submodule R P)
    ((fun (I : FractionalIdeal S P) ↦ (↑I : Submodule R P))
      (HMul.hMul (α := FractionalIdeal S P)
        (spanSingleton S ((algebraMap R P : (a : R) → P) (↑I.den : R)) : FractionalIdeal S P) I))
    ((fun (I : FractionalIdeal S P) ↦ (↑I : Submodule R P)) (↑I.num : FractionalIdeal S P))
⊢ HMul.hMul (α := FractionalIdeal S P)
      (spanSingleton S ((algebraMap R P : (a : R) → P) (↑I.den : R)) : FractionalIdeal S P) I =
    (↑I.num : FractionalIdeal S P)

Tactic:
apply coeToSubmodule_injective

Premises used: FractionalIdeal.coeToSubmodule_injective
-- 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
a :
  HSMul.hSMul (α := P) ((algebraMap R P : (a : R) → P) (↑I.den : R) : P) (↑I : Submodule R P) =
    (↑(↑I.num : FractionalIdeal S P) : Submodule R P)
⊢ (↑(HMul.hMul (α := FractionalIdeal S P)
          (spanSingleton S ((algebraMap R P : (a : R) → P) (↑I.den : R)) : FractionalIdeal S P) I) :
      Submodule R P) =
    (↑(↑I.num : FractionalIdeal S P) : Submodule R P)

Tactic:
rw [coe_mul, ← smul_eq_mul, coe_spanSingleton, smul_eq_mul, Submodule.span_singleton_mul]

Premises used: FractionalIdeal.coe_mul, Submodule.span_singleton_mul, FractionalIdeal.coe_spanSingleton, smul_eq_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
I : FractionalIdeal S P
⊢ I.den • (↑I : Submodule R P) = Submodule.map (Algebra.linearMap R P) I.num

Tactic:
I.den_mul_self_eq_num

Premises used: 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
h :
  HSMul.hSMul (α := P) ((algebraMap R P : (a : R) → P) (↑I.den : R) : P) (↑I : Submodule R P) =
    I.den • (↑I : Submodule R P)
⊢ HSMul.hSMul (α := P) ((algebraMap R P : (a : R) → P) (↑I.den : R) : P) (↑I : Submodule R P) =
    (↑(↑I.num : FractionalIdeal S P) : Submodule R P)

Tactic:
convert! I.den_mul_self_eq_num using 1

Premises used: 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
h :
  ∀ (x : P),
    x ∈ HSMul.hSMul (α := P) ((algebraMap R P : (a : R) → P) (↑I.den : R) : P) (↑I : Submodule R P) ↔
      x ∈ I.den • (↑I : Submodule R P)
⊢ HSMul.hSMul (α := P) ((algebraMap R P : (a : R) → P) (↑I.den : R) : P) (↑I : Submodule R P) =
    I.den • (↑I : Submodule R P)

Tactic:
ext
-- 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
x : P
h :
  (∃ b ∈ (↑I : Submodule R P), HSMul.hSMul (α := P) ((algebraMap R P : (a : R) → P) (↑I.den : R) : P) b = x) ↔
    ∃ b ∈ (↑I : Submodule R P), I.den • b = x
⊢ x ∈ HSMul.hSMul (α := P) ((algebraMap R P : (a : R) → P) (↑I.den : R) : P) (↑I : Submodule R P) ↔
    x ∈ I.den • (↑I : Submodule R P)

Tactic:
rw [mem_smul_pointwise_iff_exists, mem_smul_pointwise_iff_exists]

Premises used: Submodule.mem_smul_pointwise_iff_exists
-- 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
x : P
⊢ (∃ b ∈ (↑I : Submodule R P), HSMul.hSMul (α := P) ((algebraMap R P : (a : R) → P) (↑I.den : R) : P) b = x) ↔
    ∃ b ∈ (↑I : Submodule R P), I.den • b = x

Tactic:
simp [smul_eq_mul, Algebra.smul_def, Submonoid.smul_def]

Premises used: Submonoid.smul_def, Algebra.smul_def, smul_eq_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 : FractionalIdeal S P
rw : (↑(spanSingleton S x) : Submodule R P) ≤ (↑I : Submodule R P) ↔ x ∈ I
rw₁ : R ∙ x ≤ (↑I : Submodule R P) ↔ x ∈ I
rw₂ : x ∈ (↑I : Submodule R P) ↔ x ∈ I
rw₃ rw₄ : x ∈ I ↔ x ∈ I
⊢ spanSingleton S x ≤ I ↔ x ∈ I

Tactic:
rw [← coe_le_coe, coe_spanSingleton, Submodule.span_singleton_le_iff_mem, mem_coe]

Premises used: FractionalIdeal.coe_le_coe, FractionalIdeal.mem_coe, FractionalIdeal.coe_spanSingleton, Submodule.span_singleton_le_iff_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
inst_4 : IsDomain R
inst_5 : Module.IsTorsionFree R P
x y : P
rw :
  Eq (α := FractionalIdeal S P) (Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) (R ∙ x) ⋯)
      (Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) (R ∙ y) ⋯) ↔
    Eq (α := Submodule R P) (R ∙ x) (R ∙ y)
⊢ Eq (α := FractionalIdeal S P) (spanSingleton S x) (spanSingleton S y) ↔ ∃ (z : Rˣ), z • x = y

Tactic:
rw [← Submodule.span_singleton_eq_span_singleton, spanSingleton, spanSingleton]

Premises used: FractionalIdeal.spanSingleton, Submodule.span_singleton_eq_span_singleton
-- 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
inst_4 : IsDomain R
inst_5 : Module.IsTorsionFree R P
x y : P
⊢ Eq (α := FractionalIdeal S P) (Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) (R ∙ x) ⋯)
      (Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) (R ∙ y) ⋯) ↔
    Eq (α := Submodule R P) (R ∙ x) (R ∙ y)

Tactic:
Subtype.mk_eq_mk

Premises used: FractionalIdeal, Subtype.mk_eq_mk
-- 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
inst_4 : IsDomain R
inst_5 : Module.IsTorsionFree R P
x y : P
⊢ Eq (α := FractionalIdeal S P) (Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) (R ∙ x) ⋯)
      (Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) (R ∙ y) ⋯) ↔
    Eq (α := Submodule R P) (R ∙ x) (R ∙ y)

Tactic:
exact Subtype.mk_eq_mk

Premises used: Subtype.mk_eq_mk
-- 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
inst_4 : (↑I : Submodule R P).IsPrincipal
rw : I = Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) (R ∙ generator (↑I : Submodule R P)) ⋯
rw₁ :
  (↑I : Submodule R P) =
    (↑(Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) (R ∙ generator (↑I : Submodule R P)) ⋯) :
      Submodule R P)
rw₂ : (↑I : Submodule R P) = R ∙ generator (↑I : Submodule R P)
rw₃ rw₄ : (↑I : Submodule R P) = (↑I : Submodule R P)
⊢ I = spanSingleton S (generator (↑I : Submodule R P))

Tactic:
rw [spanSingleton, ← coeToSubmodule_inj, coe_mk, span_singleton_generator]

Premises used: FractionalIdeal.spanSingleton, FractionalIdeal.coeToSubmodule_inj, FractionalIdeal.coe_mk, Submodule.IsPrincipal.span_singleton_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
I : FractionalIdeal S P
⊢ (↑I : Submodule R P).IsPrincipal ↔ ∃ (x : P), I = spanSingleton S x

Tactic:
⟨fun _ => ⟨generator (I : Submodule R P), eq_spanSingleton_of_principal I⟩,
    fun ⟨x, hx⟩ => { principal := ⟨x, Eq.trans (congr_arg _ hx) (coe_spanSingleton _ x)⟩ }⟩

Premises used: congr_arg, Submodule.IsPrincipal.mk, Submodule.IsPrincipal.generator, FractionalIdeal.eq_spanSingleton_of_principal, FractionalIdeal.coeToSubmodule, Iff.intro, Exists.intro, _private.0.FractionalIdeal.isPrincipal_iff.match_1, FractionalIdeal.coe_spanSingleton, Submodule.IsPrincipal, Eq.trans
-- 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
a :
  ∀ (x : P),
    Membership.mem (γ := FractionalIdeal S P) (spanSingleton S 0) x ↔ Membership.mem (γ := FractionalIdeal S P) 0 x
⊢ Eq.{u_2 + 1} (α := FractionalIdeal S P) (spanSingleton S 0) 0

Tactic:
ext
-- 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
⊢ Membership.mem (γ := FractionalIdeal S P) (spanSingleton S 0) x ↔ Membership.mem (γ := FractionalIdeal S P) 0 x

Tactic:
simp [eq_comm]

Premises used: eq_comm
-- 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
y : P
h : Eq (α := FractionalIdeal S P) (spanSingleton S y) 0
⊢ Eq (α := Submodule R P) (R ∙ y) ⊥

Tactic:
simpa using congr_arg Subtype.val h

Premises used: congr_arg, Subtype.val
-- 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
y : P
h : y = 0
⊢ Eq (α := FractionalIdeal S P) (spanSingleton S y) 0

Tactic:
simp [h]
-- 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
y : P
⊢ Ne (α := FractionalIdeal S P) (spanSingleton S y) 0 ↔ y ≠ 0

Tactic:
not_congr spanSingleton_eq_zero_iff

Premises used: FractionalIdeal.spanSingleton_eq_zero_iff, not_congr
-- 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
a :
  ∀ (x : P),
    Membership.mem (γ := FractionalIdeal S P) (spanSingleton S 1) x ↔ Membership.mem (γ := FractionalIdeal S P) 1 x
⊢ Eq.{u_2 + 1} (α := FractionalIdeal S P) (spanSingleton S 1) 1

Tactic:
ext
-- 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
⊢ Membership.mem (γ := FractionalIdeal S P) (spanSingleton S 1) x ↔ Membership.mem (γ := FractionalIdeal S P) 1 x

Tactic:
(mem_spanSingleton S).trans ((exists_congr ?_).trans (mem_one_iff S).symm)

Premises used: FractionalIdeal.mem_one_iff, FractionalIdeal.mem_spanSingleton, exists_congr, Iff.trans, Iff.symm
-- 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
a : ∀ (a : R), HSMul.hSMul (β := P) a 1 = x ↔ (algebraMap R P : (a : R) → P) a = x
⊢ Membership.mem (γ := FractionalIdeal S P) (spanSingleton S 1) x ↔ Membership.mem (γ := FractionalIdeal S P) 1 x

Tactic:
refine (mem_spanSingleton S).trans ((exists_congr ?_).trans (mem_one_iff S).symm)

Premises used: FractionalIdeal.mem_one_iff, FractionalIdeal.mem_spanSingleton, exists_congr, Iff.trans, Iff.symm
-- 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
x' : R
a :
  HMul.hMul (α := P) (β := P) ((algebraMap R P : (a : R) → P) x' : P) (1 : P) = x ↔
    (algebraMap R P : (a : R) → P) x' = x
a₁ a₂ : (algebraMap R P : (a : R) → P) x' = x ↔ (algebraMap R P : (a : R) → P) x' = x
⊢ HSMul.hSMul (β := P) x' 1 = x ↔ (algebraMap R P : (a : R) → P) x' = x

Tactic:
rw [Algebra.smul_def, mul_one]

Premises used: Algebra.smul_def, mul_one
-- 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 y : P
a :
  Eq.{u_2 + 1} (α := Submodule R P)
    ((fun (I : FractionalIdeal S P) ↦ (↑I : Submodule R P))
      (HMul.hMul (α := FractionalIdeal S P) (spanSingleton S x) (spanSingleton S y)))
    ((fun (I : FractionalIdeal S P) ↦ (↑I : Submodule R P)) (spanSingleton S (x * y)))
⊢ HMul.hMul (α := FractionalIdeal S P) (spanSingleton S x) (spanSingleton S y) = spanSingleton S (x * y)

Tactic:
apply coeToSubmodule_injective

Premises used: FractionalIdeal.coeToSubmodule_injective