awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
p : FractionalIdeal S P
s : Set P
hs : s = (↑p : Set P)
x : P
h : x ∈ (↑p : Submodule R P).copy (↑p : Set P) ⋯ ↔ x ∈ (↑p : Submodule R P)
⊢ x ∈ (↑p : Submodule R P).copy s hs ↔ x ∈ (↑p : Submodule R P)

Tactic:
simp only [hs]
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
p : FractionalIdeal S P
s : Set P
hs : s = (↑p : Set P)
x : P
⊢ x ∈ (↑p : Submodule R P).copy (↑p : Set P) ⋯ ↔ x ∈ (↑p : Submodule R P)

Tactic:
rfl
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
p : FractionalIdeal S P
s : Set P
hs : s = (↑p : Set P)
⊢ (↑(p.copy s hs) : Set P) = s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
p : FractionalIdeal S P
s : Set P
hs : s = (↑p : Set P)
⊢ p.copy s hs = p

Tactic:
SetLike.coe_injective hs

Premises used: SetLike.coe_injective
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
I : FractionalIdeal S P
⊢ 0 ∈ I

Tactic:
I.coeToSubmodule.zero_mem

Premises used: Set.Mem, FractionalIdeal.coeToSubmodule, Submodule.zero_mem
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
I : FractionalIdeal S P
⊢ (↑I : Submodule R P) = (↑I : Submodule R P)

Tactic:
rfl

Premises used: FractionalIdeal.coeToSubmodule, rfl
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
I : Submodule R P
hI : IsFractional S I
⊢ (↑(Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) I hI) : Submodule R P) = I

Tactic:
rfl

Premises used: FractionalIdeal.coeToSubmodule, rfl
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
I : FractionalIdeal S P
⊢ (↑(↑I : Submodule R P) : Set P) = (↑I : Set P)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
⊢ Function.Injective (β := Submodule R P) fun (I : FractionalIdeal S P) ↦ (↑I : Submodule R P)

Tactic:
Subtype.coe_injective

Premises used: Subtype.coe_injective, FractionalIdeal, FractionalIdeal.coeToSubmodule
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
I J : FractionalIdeal S P
⊢ (↑I : Submodule R P) = (↑J : Submodule R P) ↔ I = J

Tactic:
coeToSubmodule_injective.eq_iff

Premises used: Function.Injective.eq_iff, FractionalIdeal.coeToSubmodule_injective
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
I : Submodule R P
h : I ≤ 1
right : ∀ b ∈ I, IsInteger R (HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 b)
⊢ IsFractional S I

Tactic:
use 1, S.one_mem

Premises used: Submonoid.one_mem
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
I : Submodule R P
h : I ≤ 1
b : P
hb : b ∈ I
right : IsInteger R b
⊢ IsInteger R (HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 b)

Tactic:
rw [one_smul]

Premises used: one_smul
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
I : Submodule R P
h : I ≤ 1
b : P
hb : b ∈ I
right :
  ∀ (b' : R) (hb : Membership.mem (α := P) I ((algebraMap R P : (a : R) → P) b' : P)),
    IsInteger.{u_1, u_2} R (S := P) ((algebraMap R P : (a : R) → P) b' : P)
⊢ IsInteger R b

Tactic:
obtain ⟨b', b'_mem, rfl⟩ := mem_one.mp (h hb)

Premises used: Submodule.mem_one, Iff.mp, rfl
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
I : Submodule R P
h : I ≤ 1
b' : R
hb : Membership.mem (α := P) I ((algebraMap R P : (a : R) → P) b' : P)
⊢ IsInteger.{u_1, u_2} R (S := P) ((algebraMap R P : (a : R) → P) b' : P)

Tactic:
Set.mem_range_self b'

Premises used: IsLocalization.IsInteger, Set.mem_range_self, Set.Mem, setOf, Set.range
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
I : Submodule R P
h : I ≤ 1
b' : R
hb : Membership.mem (α := P) I ((algebraMap R P : (a : R) → P) b' : P)
⊢ IsInteger.{u_1, u_2} R (S := P) ((algebraMap R P : (a : R) → P) b' : P)

Tactic:
exact Set.mem_range_self b'

Premises used: Set.mem_range_self
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
I : Submodule R P
J : FractionalIdeal S P
hIJ : I ≤ (↑J : Submodule R P)
obtain : ∀ (a : R) (a_mem : a ∈ S) (ha : ∀ b ∈ (↑J : Submodule R P), IsInteger R (a • b)), IsFractional S I
⊢ IsFractional S I

Tactic:
obtain ⟨a, a_mem, ha⟩ := J.isFractional

Premises used: FractionalIdeal.isFractional
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
I : Submodule R P
J : FractionalIdeal S P
hIJ : I ≤ (↑J : Submodule R P)
a : R
a_mem : a ∈ S
ha : ∀ b ∈ (↑J : Submodule R P), IsInteger R (a • b)
right : ∀ b ∈ I, IsInteger R (a • b)
⊢ IsFractional S I

Tactic:
use a, a_mem
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
I : Submodule R P
J : FractionalIdeal S P
hIJ : I ≤ (↑J : Submodule R P)
a : R
a_mem : a ∈ S
ha : ∀ b ∈ (↑J : Submodule R P), IsInteger R (a • b)
b : P
b_mem : b ∈ I
⊢ IsInteger R (a • b)

Tactic:
ha b (hIJ b_mem)
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
I : Submodule R P
J : FractionalIdeal S P
hIJ : I ≤ (↑J : Submodule R P)
a : R
a_mem : a ∈ S
ha : ∀ b ∈ (↑J : Submodule R P), IsInteger R (a • b)
b : P
b_mem : b ∈ I
⊢ IsInteger R (a • b)

Tactic:
exact ha b (hIJ b_mem)
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
I : Ideal R
⊢ LE.le (α := Submodule R P) (coeSubmodule P I : Submodule R P) 1

Tactic:
simpa using coeSubmodule_mono P (le_top : I ≤ ⊤)

Premises used: IsLocalization.coeSubmodule_mono, le_top
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
I : Ideal R
⊢ Eq.{u_2 + 1} (α := Submodule R P) (↑(↑I : FractionalIdeal S P) : Submodule R P) (coeSubmodule P I)

Tactic:
rfl

Premises used: FractionalIdeal.coeToSubmodule, Submodule.map, IsLocalization.coeSubmodule, rfl
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
x : P
I : Ideal R
⊢ Membership.mem (γ := FractionalIdeal S P) (↑I : FractionalIdeal S P) x ↔
    ∃ x' ∈ I, (algebraMap R P : (a : R) → P) x' = x

Tactic:
mem_coeSubmodule _ _

Premises used: Set.Mem, IsLocalization.mem_coeSubmodule
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
x : P
I : Ideal R
⊢ Membership.mem (γ := Submodule R P) (coeSubmodule P I) x ↔ ∃ x' ∈ I, (algebraMap R P : (a : R) → P) x' = x

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.image
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
x : R
I : Ideal R
hx : x ∈ I
⊢ Membership.mem.{u_2, u_2} (α := P) (γ := FractionalIdeal S P) (↑I : FractionalIdeal S P)
    ((algebraMap R P : (a : R) → P) x : P)

Tactic:
(mem_coeIdeal S).mpr ⟨x, hx, rfl⟩

Premises used: Iff.mpr, FractionalIdeal.mem_coeIdeal, And.intro, Exists.intro, rfl
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
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
h : S ≤ R⁰
I J : Ideal R
⊢ LE.le.{u_2} (α := FractionalIdeal S P) (↑I : FractionalIdeal S P) (↑J : FractionalIdeal S P) ↔ I ≤ J

Tactic:
coeSubmodule_le_coeSubmodule h

Premises used: Set.Mem, IsLocalization.coeSubmodule_le_coeSubmodule
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
K : Type u_3
inst_1 : CommRing K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
I J : Ideal R
⊢ LE.le.{u_3} (α := FractionalIdeal.{u_1, u_3} (R := R) R⁰ K) (↑I : FractionalIdeal R⁰ K) (↑J : FractionalIdeal R⁰ K) ↔
    I ≤ J

Tactic:
IsFractionRing.coeSubmodule_le_coeSubmodule

Premises used: Set.Mem, IsFractionRing.coeSubmodule_le_coeSubmodule
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
x : P
h : Membership.mem (γ := FractionalIdeal S P) 0 x
x' : R
x'_mem_zero : x' ∈ (↑0 : Set R)
x'_eq_x : (Algebra.linearMap R P : (a : R) → P) x' = x
⊢ x' = 0

Tactic:
have x'_eq_zero : x' = 0 := x'_mem_zero
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
x : P
h : Membership.mem (γ := FractionalIdeal S P) 0 x
x' : R
x'_mem_zero : x' ∈ (↑0 : Set R)
x'_eq_x : (Algebra.linearMap R P : (a : R) → P) x' = x
x'_eq_zero : x' = 0
⊢ x = 0

Tactic:
simp [x'_eq_x.symm, x'_eq_zero]

Premises used: Eq.symm
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
x : P
hx : x = 0
⊢ (Algebra.linearMap R P : (a : R) → P) 0 = x

Tactic:
simp [hx]
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
⊢ Eq.{u_2 + 1} (α := Submodule R P) (↑0 : Submodule R P) ⊥

Tactic:
Submodule.ext fun _ => mem_zero_iff S

Premises used: FractionalIdeal.mem_zero_iff, Submodule.ext
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
⊢ Eq.{u_2 + 1} (α := FractionalIdeal S P) (↑⊥ : FractionalIdeal S P) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
loc : IsLocalization S P
x : R
I : Ideal R
h : S ≤ R⁰
⊢ (∃ x' ∈ I, Eq.{u_2 + 1} (α := P) ((algebraMap R P : (a : R) → P) x' : P) ((algebraMap R P : (a : R) → P) x : P)) ↔
    x ∈ I

Tactic:
⟨fun ⟨_, hx', Eq⟩ => IsLocalization.injective _ h Eq ▸ hx', fun h => ⟨x, h, rfl⟩⟩

Premises used: IsLocalization.injective, Membership.mem, Eq.rec, And.intro, Iff.intro, Exists.intro, _private.0.FractionalIdeal.exists_mem_algebraMap_eq.match_1, rfl
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
loc : IsLocalization S P
h : S ≤ R⁰
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (β := FractionalIdeal S P) fun (I : Ideal R) ↦ (↑I : FractionalIdeal S P)

Tactic:
fun _ _ h' =>
  ((coeIdeal_le_coeIdeal' S h).mp h'.le).antisymm ((coeIdeal_le_coeIdeal' S h).mp
    h'.ge)

Premises used: Eq.ge, LE.le.antisymm, FractionalIdeal.coeIdeal_le_coeIdeal', Eq.le, Iff.mp, Function.Injective
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
loc : IsLocalization S P
h : S ≤ R⁰
I J : Ideal R
⊢ Eq.{u_2 + 1} (α := FractionalIdeal S P) (↑I : FractionalIdeal S P) (↑J : FractionalIdeal S P) ↔ I = J

Tactic:
(coeIdeal_injective' h).eq_iff

Premises used: Function.Injective.eq_iff, FractionalIdeal.coeIdeal_injective'
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
loc : IsLocalization S P
I : Ideal R
h : S ≤ R⁰
⊢ Eq.{u_2 + 1} (α := FractionalIdeal S P) (↑I : FractionalIdeal S P) 0 ↔ I = ⊥

Tactic:
coeIdeal_inj' h

Premises used: FractionalIdeal.coeIdeal_inj'
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
loc : IsLocalization S P
I : Ideal R
h : S ≤ R⁰
⊢ Ne.{u_2 + 1} (α := FractionalIdeal S P) (↑I : FractionalIdeal S P) 0 ↔ I ≠ ⊥

Tactic:
not_iff_not.mpr <| coeIdeal_eq_zero' h

Premises used: not_iff_not, Iff.mpr, FractionalIdeal.coeIdeal_eq_zero'
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
I : FractionalIdeal S P
h : (↑I : Submodule R P) = ⊥
⊢ Eq.{u_2 + 1} (α := Submodule R P) ((fun (I : FractionalIdeal S P) ↦ (↑I : Submodule R P)) I)
    ((fun (I : FractionalIdeal S P) ↦ (↑I : Submodule R P)) 0)

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
I : FractionalIdeal S P
h : I = 0
⊢ (↑I : Submodule R P) = ⊥

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
I : FractionalIdeal S P
⊢ (↑I : Submodule R P) ≠ ⊥ ↔ I ≠ 0

Tactic:
not_iff_not.mpr coeToSubmodule_eq_bot

Premises used: not_iff_not, Iff.mpr, FractionalIdeal.coeToSubmodule_eq_bot
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
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 : IsDomain R
inst_4 : Module.IsTorsionFree R P
hS : 0 ∉ S
I : FractionalIdeal S P
hI : I.num = ⊥
rw : (↑I : Submodule R P) ≤ ⊥
⊢ I = 0

Tactic:
rw [← coeToSubmodule_eq_bot, eq_bot_iff]

Premises used: FractionalIdeal.coeToSubmodule_eq_bot, eq_bot_iff
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
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 : IsDomain R
inst_4 : Module.IsTorsionFree R P
hS : 0 ∉ S
I : FractionalIdeal S P
hI : I.num = ⊥
x : P
hx : x ∈ (↑I : Submodule R P)
suffices : (↑I.den : R) • x = 0
⊢ Membership.mem (γ := Submodule R P) ⊥ x

Tactic:
suffices (den I : R) • x = 0 from
    (smul_eq_zero.mp this).resolve_left (ne_of_mem_of_not_mem (SetLike.coe_mem _) hS)
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
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 : IsDomain R
inst_4 : Module.IsTorsionFree R P
hS : 0 ∉ S
I : FractionalIdeal S P
hI : I.num = ⊥
x : P
hx : x ∈ (↑I : Submodule R P)
rw : Eq (α := Submodule R P) (Submodule.map (Algebra.linearMap R P) I.num) ⊥
rw₁ : Eq (α := Submodule R P) (Submodule.map (Algebra.linearMap R P) ⊥) ⊥
rw₂ rw₃ : Eq.{u_2 + 1} (α := Submodule R P) ⊥ ⊥
⊢ I.den • (↑I : Submodule R P) = ⊥

Tactic:
rw [den_mul_self_eq_num, hI, Submodule.map_bot]

Premises used: Submodule.map_bot, FractionalIdeal.den_mul_self_eq_num
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
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 : IsDomain R
inst_4 : Module.IsTorsionFree R P
hS : 0 ∉ S
I : FractionalIdeal S P
hI : I.num = ⊥
x : P
hx : x ∈ (↑I : Submodule R P)
⊢ I.den • (↑I : Submodule R P) = ⊥

Tactic:
have h_eq : I.den • (I : Submodule R P) = ⊥ := by rw [den_mul_self_eq_num, hI, Submodule.map_bot]
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
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 : IsDomain R
inst_4 : Module.IsTorsionFree R P
hS : 0 ∉ S
I : FractionalIdeal S P
hI : I.num = ⊥
x : P
hx : x ∈ (↑I : Submodule R P)
h_eq : I.den • (↑I : Submodule R P) = ⊥
⊢ (↑I.den : R) • x = 0

Tactic:
(Submodule.eq_bot_iff _).mp h_eq (den I • x) ⟨x, hx, rfl⟩

Premises used: FractionalIdeal.den, And.intro, Exists.intro, Iff.mp, HSMul.hSMul, Submodule.eq_bot_iff, rfl
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
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 : IsDomain R
inst_4 : Module.IsTorsionFree R P
hS : 0 ∉ S
I : FractionalIdeal S P
hI : I.num = ⊥
x : P
hx : x ∈ (↑I : Submodule R P)
h_eq : I.den • (↑I : Submodule R P) = ⊥
⊢ (↑I.den : R) • x = 0

Tactic:
exact (Submodule.eq_bot_iff _).mp h_eq (den I • x) ⟨x, hx, rfl⟩

Premises used: FractionalIdeal.den, And.intro, Exists.intro, Iff.mp, HSMul.hSMul, Submodule.eq_bot_iff, rfl
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
h_inj : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := P) (⇑(algebraMap R P) : (a : R) → P)
⊢ Eq.{u_1 + 1} (α := Ideal R) (num.{u_1, u_2} (S := S) (P := P) 0) 0

Tactic:
simpa [num, LinearMap.ker_eq_bot] using h_inj

Premises used: FractionalIdeal.num, LinearMap.ker_eq_bot
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
⊢ Eq.{u_2 + 1} (α := FractionalIdeal S P) (↑⊤ : FractionalIdeal S P) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
x : P
⊢ Membership.mem (γ := FractionalIdeal S P) 1 x ↔ ∃ (x' : R), (algebraMap R P : (a : R) → P) x' = x

Tactic:
Iff.intro (fun ⟨x', _, h⟩ => ⟨x', h⟩) fun ⟨x', h⟩ => ⟨x', ⟨⟩, h⟩

Premises used: _private.0.FractionalIdeal.mem_one_iff.match_2, Algebra.algebraMap, Membership.mem, Exists, And.intro, _private.0.FractionalIdeal.mem_one_iff.match_1, Iff.intro, Exists.intro, OfNat.ofNat, Eq, DFunLike.coe, True.intro
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
x : R
⊢ Membership.mem.{u_2, u_2} (α := P) (γ := FractionalIdeal S P) 1 ((algebraMap R P : (a : R) → P) x : P)

Tactic:
simp
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
⊢ Membership.mem (γ := FractionalIdeal S P) 1 1

Tactic:
(mem_one_iff S).mpr ⟨1, map_one _⟩

Premises used: Iff.mpr, FractionalIdeal.mem_one_iff, map_one, Exists.intro, OfNat.ofNat
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
⊢ Eq.{u_2 + 1} (α := Submodule R P) (↑1 : Submodule R P) (coeSubmodule P ⊤)

Tactic:
rfl

Premises used: FractionalIdeal.coeToSubmodule, Submodule.map, IsLocalization.coeSubmodule, rfl
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
rw : Eq (α := Submodule R P) (coeSubmodule P ⊤ : Submodule R P) 1
rw₁ rw₂ : Eq.{u_2 + 1} (α := Submodule R P) 1 1
⊢ Eq.{u_2 + 1} (α := Submodule R P) (↑1 : Submodule R P) 1

Tactic:
rw [coe_one_eq_coeSubmodule_top, coeSubmodule_top]

Premises used: FractionalIdeal.coe_one_eq_coeSubmodule_top, IsLocalization.coeSubmodule_top
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
I J : FractionalIdeal S P
⊢ (↑I : Submodule R P) ≤ (↑J : Submodule R P) ↔ I ≤ J

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
I : FractionalIdeal S P
x : P
hx : Membership.mem (γ := FractionalIdeal S P) 0 x
⊢ 0 ∈ I

Tactic:
zero_mem I

Premises used: FractionalIdeal.zero_mem
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
I : FractionalIdeal S P
x : P
hx : Membership.mem (γ := FractionalIdeal S P) 0 x
h : x = 0
⊢ x ∈ I

Tactic:
convert! zero_mem I

Premises used: FractionalIdeal.zero_mem
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
I : FractionalIdeal S P
x : P
hx : Membership.mem (γ := FractionalIdeal S P) 0 x
h h₁ : Eq.{u_2 + 1} (α := P) 0 0
⊢ x = 0

Tactic:
rw [(mem_zero_iff _).mp hx]

Premises used: FractionalIdeal.mem_zero_iff, Iff.mp
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
⊢ Eq.{u_2 + 1} (α := FractionalIdeal S P) ⊥ 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
I : FractionalIdeal S P
⊢ I ≤ 0 ↔ I = 0

Tactic:
le_bot_iff

Premises used: le_bot_iff, Set.Mem
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
I : FractionalIdeal S P
h : I = 0
x : P
hx : x ∈ I
⊢ x = 0

Tactic:
simpa [h, mem_zero_iff] using hx

Premises used: FractionalIdeal.mem_zero_iff
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
I J : Submodule R P
aI : R
haI : aI ∈ S
hI : ∀ b ∈ I, IsInteger R (aI • b)
aJ : R
haJ : aJ ∈ S
hJ : ∀ b ∈ J, IsInteger R (aJ • b)
b : P
hb : b ∈ I ⊔ J
rcases : ∀ (bI : P) (hbI : bI ∈ I) (bJ : P) (hbJ : bJ ∈ J) (hb : bI + bJ ∈ I ⊔ J), IsInteger R ((aI * aJ) • (bI + bJ))
⊢ IsInteger R ((aI * aJ) • b)

Tactic:
rcases mem_sup.mp hb with ⟨bI, hbI, bJ, hbJ, rfl⟩

Premises used: Iff.mp, Submodule.mem_sup, rfl
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
I J : Submodule R P
aI : R
haI : aI ∈ S
hI : ∀ b ∈ I, IsInteger R (aI • b)
aJ : R
haJ : aJ ∈ S
hJ : ∀ b ∈ J, IsInteger R (aJ • b)
bI : P
hbI : bI ∈ I
bJ : P
hbJ : bJ ∈ J
hb : bI + bJ ∈ I ⊔ J
rw : IsInteger R ((aI * aJ) • bI + (aI * aJ) • bJ)
⊢ IsInteger R ((aI * aJ) • (bI + bJ))

Tactic:
rw [smul_add]

Premises used: smul_add
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
I J : Submodule R P
aI : R
haI : aI ∈ S
hI : ∀ b ∈ I, IsInteger R (aI • b)
aJ : R
haJ : aJ ∈ S
hJ : ∀ b ∈ J, IsInteger R (aJ • b)
bI : P
hbI : bI ∈ I
bJ : P
hbJ : bJ ∈ J
hb : bI + bJ ∈ I ⊔ J
ha : IsInteger R ((aI * aJ) • bI)
hb₁ : IsInteger R ((aI * aJ) • bJ)
⊢ IsInteger R ((aI * aJ) • bI + (aI * aJ) • bJ)

Tactic:
apply isInteger_add

Premises used: IsLocalization.isInteger_add