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
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 (aJ • aI • bI)
⊢ IsInteger R ((aI * aJ) • bI)

Tactic:
rw [mul_smul, smul_comm]

Premises used: SMulCommClass.smul_comm, SemigroupAction.mul_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 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
⊢ IsInteger R (aJ • aI • bI)

Tactic:
isInteger_smul (hI bI hbI)

Premises used: IsLocalization.isInteger_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 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
⊢ IsInteger R (aJ • aI • bI)

Tactic:
exact isInteger_smul (hI bI hbI)

Premises used: IsLocalization.isInteger_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 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
hb₁ : IsInteger R (aI • aJ • bJ)
⊢ IsInteger R ((aI * aJ) • bJ)

Tactic:
rw [mul_smul]

Premises used: SemigroupAction.mul_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 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
⊢ IsInteger R (aI • aJ • bJ)

Tactic:
isInteger_smul (hJ bJ hbJ)

Premises used: IsLocalization.isInteger_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 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
⊢ IsInteger R (aI • aJ • bJ)

Tactic:
exact isInteger_smul (hJ bJ hbJ)

Premises used: IsLocalization.isInteger_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
aI : R
haI : aI ∈ S
hI : ∀ b ∈ I, IsInteger R (aI • b)
J : Submodule R P
b : P
hb : b ∈ I ⊓ J
⊢ b ∈ I

Tactic:
rcases mem_inf.mp hb with ⟨hbI, _⟩

Premises used: Submodule.mem_inf, 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
I : Submodule R P
aI : R
haI : aI ∈ S
hI : ∀ b ∈ I, IsInteger R (aI • b)
J : Submodule R P
b : P
hb : b ∈ I ⊓ J
hbI : b ∈ I
⊢ b ∈ J

Tactic:
rcases mem_inf.mp hb with ⟨hbI, _⟩

Premises used: Submodule.mem_inf, 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
I : Submodule R P
aI : R
haI : aI ∈ S
hI : ∀ b ∈ I, IsInteger R (aI • b)
J : Submodule R P
b : P
hb : b ∈ I ⊓ J
hbI : b ∈ I
right : b ∈ J
⊢ IsInteger R (aI • b)

Tactic:
hI b hbI
-- 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
aI : R
haI : aI ∈ S
hI : ∀ b ∈ I, IsInteger R (aI • b)
J : Submodule R P
b : P
hb : b ∈ I ⊓ J
hbI : b ∈ I
right : b ∈ J
⊢ IsInteger R (aI • b)

Tactic:
exact hI b hbI
-- 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 ⊓ J) : Submodule R P) = (↑I : Submodule R P) ⊓ (↑J : 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 J : FractionalIdeal S P
⊢ (↑(I ⊔ J) : Submodule R P) = (↑I : Submodule R P) ⊔ (↑J : 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 J : FractionalIdeal S P
⊢ I ⊔ J = I + J

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 J : FractionalIdeal S P
⊢ (↑(I + J) : Submodule R P) = (↑I : Submodule R P) + (↑J : Submodule R P)

Tactic:
rfl

Premises used: Set.Mem, setOf, 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 J : FractionalIdeal S P
x : P
rw : x ∈ (↑I : Submodule R P) ⊔ (↑J : Submodule R P) ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = x
⊢ x ∈ I + J ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = x

Tactic:
rw [← mem_coe, coe_add, Submodule.add_eq_sup]

Premises used: FractionalIdeal.coe_add, FractionalIdeal.mem_coe, Submodule.add_eq_sup
-- 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
x : P
⊢ x ∈ (↑I : Submodule R P) ⊔ (↑J : Submodule R P) ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = x

Tactic:
Submodule.mem_sup

Premises used: Set.Mem, Submodule.mem_sup
-- 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
x : P
⊢ x ∈ (↑I : Submodule R P) ⊔ (↑J : Submodule R P) ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = x

Tactic:
exact Submodule.mem_sup

Premises used: Submodule.mem_sup
-- 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 : FaithfulSMul R P
I J : Ideal R
a :
  Eq.{u_2 + 1} (α := Submodule R P)
    ((fun (I : FractionalIdeal S P) ↦ (↑I : Submodule R P)) (↑(I ⊓ J) : FractionalIdeal S P))
    ((fun (I : FractionalIdeal S P) ↦ (↑I : Submodule R P)) ((↑I : FractionalIdeal S P) ⊓ (↑J : FractionalIdeal S P)))
⊢ Eq.{u_2 + 1} (α := FractionalIdeal S P) (↑(I ⊓ J) : FractionalIdeal S P)
    ((↑I : FractionalIdeal S P) ⊓ (↑J : FractionalIdeal S P))

Tactic:
apply coeToSubmodule_injective

Premises used: 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
inst_3 : FaithfulSMul R P
I J : Ideal R
⊢ Eq.{u_2 + 1} (α := Submodule R P)
    ((fun (I : FractionalIdeal S P) ↦ (↑I : Submodule R P)) (↑(I ⊓ J) : FractionalIdeal S P))
    ((fun (I : FractionalIdeal S P) ↦ (↑I : Submodule R P)) ((↑I : FractionalIdeal S P) ⊓ (↑J : FractionalIdeal S P)))

Tactic:
Submodule.map_inf (Algebra.linearMap R P) (FaithfulSMul.algebraMap_injective R P)

Premises used: Algebra.linearMap, FractionalIdeal.coeToSubmodule, Submodule.map_inf, FaithfulSMul.algebraMap_injective, Submodule.map, IsLocalization.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
inst_3 : FaithfulSMul R P
I J : Ideal R
⊢ Eq.{u_2 + 1} (α := Submodule R P)
    ((fun (I : FractionalIdeal S P) ↦ (↑I : Submodule R P)) (↑(I ⊓ J) : FractionalIdeal S P))
    ((fun (I : FractionalIdeal S P) ↦ (↑I : Submodule R P)) ((↑I : FractionalIdeal S P) ⊓ (↑J : FractionalIdeal S P)))

Tactic:
exact Submodule.map_inf (Algebra.linearMap R P) (FaithfulSMul.algebraMap_injective R P)

Premises used: Algebra.linearMap, Submodule.map_inf, FaithfulSMul.algebraMap_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 J : Ideal R
⊢ (↑(I ⊔ J) : FractionalIdeal S P) =
    HAdd.hAdd (α := FractionalIdeal S P) (↑I : FractionalIdeal S P) (↑J : FractionalIdeal S P)

Tactic:
coeToSubmodule_injective <| coeSubmodule_sup _ _ _

Premises used: FractionalIdeal.coeToSubmodule_injective, IsLocalization.coeSubmodule_sup
-- 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 : IsFractional S I
⊢ IsFractional.{u_1, u_2} S (P := P) (↑(↑0 : FractionalIdeal S P) : Submodule R P)

Tactic:
((0 : Ideal R) : FractionalIdeal S P).isFractional

Premises used: FractionalIdeal.isFractional, OfNat.ofNat, FractionalIdeal.coeIdeal
-- 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_1 : IsFractional S I
h : Eq.{u_2 + 1} (α := Submodule R P) 0 (↑(↑0 : FractionalIdeal S P) : Submodule R P)
⊢ IsFractional.{u_1, u_2} S (P := P) 0

Tactic:
convert! ((0 : Ideal R) : FractionalIdeal S P).isFractional

Premises used: FractionalIdeal.isFractional, OfNat.ofNat, FractionalIdeal.coeIdeal
-- 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 : IsFractional S I
⊢ Eq.{u_2 + 1} (α := Submodule R P) 0 (↑(↑0 : FractionalIdeal S P) : Submodule R 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
I : Submodule R P
n : ℕ
h : IsFractional S I
rw : IsFractional S (n • I + I)
⊢ IsFractional S ((n + 1) • I)

Tactic:
rw [succ_nsmul]

Premises used: succ_nsmul
-- 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
n : ℕ
h : IsFractional S I
⊢ IsFractional S (n • I + I)

Tactic:
(IsFractional.nsmul n h).sup h

Premises used: IsFractional.sup
-- 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
n : ℕ
h : IsFractional S I
⊢ IsFractional S (n • I + I)

Tactic:
exact (IsFractional.nsmul n h).sup h

Premises used: IsFractional.sup
-- 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
n : ℕ
I : FractionalIdeal S P
⊢ (↑(n • I) : Submodule R P) = n • (↑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 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
⊢ IsInteger R ((aI * aJ) • b)

Tactic:
Submodule.mul_induction_on hb ?_ ?_

Premises used: Submodule.mul_induction_on
-- 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
refine_1 : ∀ m ∈ I, ∀ n ∈ J, IsInteger R ((aI * aJ) • (m * n))
refine_2 : ∀ (x y : P), IsInteger R ((aI * aJ) • x) → IsInteger R ((aI * aJ) • y) → IsInteger R ((aI * aJ) • (x + y))
⊢ IsInteger R ((aI * aJ) • b)

Tactic:
refine Submodule.mul_induction_on hb ?_ ?_
-- 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
m : P
hm : m ∈ I
n : P
hn : n ∈ J
refine_1 : ∀ (n' : R) (hn' : (algebraMap R P : (a : R) → P) n' = aJ • n), IsInteger R ((aI * aJ) • (m * n))
⊢ IsInteger R ((aI * aJ) • (m * n))

Tactic:
obtain ⟨n', hn'⟩ := hJ n hn
-- 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
m : P
hm : m ∈ I
n : P
hn : n ∈ J
n' : R
hn' : (algebraMap R P : (a : R) → P) n' = aJ • n
refine_1 : IsInteger R (aI • n' • m)
⊢ IsInteger R ((aI * aJ) • (m * n))

Tactic:
rw [mul_smul, mul_comm m, ← smul_mul_assoc, ← hn', ← Algebra.smul_def]

Premises used: smul_mul_assoc, mul_comm, Algebra.smul_def, SemigroupAction.mul_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 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
m : P
hm : m ∈ I
n : P
hn : n ∈ J
n' : R
hn' : (algebraMap R P : (a : R) → P) n' = aJ • n
refine_1 : n' • m ∈ I
⊢ IsInteger R (aI • n' • m)

Tactic:
apply hI
-- 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
m : P
hm : m ∈ I
n : P
hn : n ∈ J
n' : R
hn' : (algebraMap R P : (a : R) → P) n' = aJ • n
⊢ n' • m ∈ I

Tactic:
Submodule.smul_mem _ _ hm

Premises used: Set.Mem, Submodule.smul_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 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
m : P
hm : m ∈ I
n : P
hn : n ∈ J
n' : R
hn' : (algebraMap R P : (a : R) → P) n' = aJ • n
⊢ n' • m ∈ I

Tactic:
exact Submodule.smul_mem _ _ hm

Premises used: Submodule.smul_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 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
x y : P
hx : IsInteger R ((aI * aJ) • x)
hy : IsInteger R ((aI * aJ) • y)
refine_2 : IsInteger R ((aI * aJ) • x + (aI * aJ) • y)
⊢ IsInteger R ((aI * aJ) • (x + y))

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)
b : P
hb : b ∈ I * J
x y : P
hx : IsInteger R ((aI * aJ) • x)
hy : IsInteger R ((aI * aJ) • y)
⊢ IsInteger R ((aI * aJ) • x + (aI * aJ) • y)

Tactic:
apply isInteger_add hx hy

Premises used: IsLocalization.isInteger_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 : FractionalIdeal S P
⊢ I.mul J = I * J

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 J : FractionalIdeal S P
⊢ I * J = Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) ((↑I : Submodule R P) * (↑J : Submodule R P)) ⋯

Tactic:
simp only [← mul_eq_mul, mul_def']

Premises used: FractionalIdeal.mul_eq_mul, FractionalIdeal.mul_def'
-- 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 * J) : Submodule R P) = (↑I : Submodule R P) * (↑J : Submodule R P)

Tactic:
simp only [mul_def, coe_mk]

Premises used: FractionalIdeal.coe_mk, FractionalIdeal.mul_def
-- 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 : Ideal R
simp :
  (↑(I * J) : FractionalIdeal S P) =
    Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I)
      (HMul.hMul (α := Submodule R P) (↑(↑I : FractionalIdeal S P) : Submodule R P)
        (↑(↑J : FractionalIdeal S P) : Submodule R P))
      ⋯
⊢ (↑(I * J) : FractionalIdeal S P) =
    HMul.hMul (α := FractionalIdeal S P) (↑I : FractionalIdeal S P) (↑J : FractionalIdeal S P)

Tactic:
simp only [mul_def]

Premises used: FractionalIdeal.mul_def
-- 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 : Ideal R
⊢ (↑(I * J) : FractionalIdeal S P) =
    Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I)
      (HMul.hMul (α := Submodule R P) (↑(↑I : FractionalIdeal S P) : Submodule R P)
        (↑(↑J : FractionalIdeal S P) : Submodule R P))
      ⋯

Tactic:
coeToSubmodule_injective (coeSubmodule_mul _ _ _)

Premises used: IsLocalization.coeSubmodule_mul, 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 J : Ideal R
⊢ (↑(I * J) : FractionalIdeal S P) =
    Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I)
      (HMul.hMul (α := Submodule R P) (↑(↑I : FractionalIdeal S P) : Submodule R P)
        (↑(↑J : FractionalIdeal S P) : Submodule R P))
      ⋯

Tactic:
exact coeToSubmodule_injective (coeSubmodule_mul _ _ _)
-- 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 J' : FractionalIdeal S P
h : (fun (x1 x2 : FractionalIdeal S P) ↦ x1 ≤ x2) J J'
⊢ (fun (x1 x2 : FractionalIdeal S P) ↦ x1 ≤ x2) ((fun (x1 x2 : FractionalIdeal S P) ↦ x1 * x2) I J)
    ((fun (x1 x2 : FractionalIdeal S P) ↦ x1 * x2) I J')

Tactic:
simpa only [mul_def] using mul_le.mpr fun x hx y hy => mul_mem_mul hx (h hy)

Premises used: Iff.mpr, Submodule.mul_mem_mul, FractionalIdeal.mul_def, Submodule.mul_le
-- 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 J' : FractionalIdeal S P
h : (fun (x1 x2 : FractionalIdeal S P) ↦ x1 ≤ x2) J J'
⊢ (fun (x1 x2 : FractionalIdeal S P) ↦ x1 ≤ x2)
    (Function.swap (φ := fun (a a_1 : FractionalIdeal S P) ↦ FractionalIdeal S P)
      (fun (x1 x2 : FractionalIdeal S P) ↦ x1 * x2) I J)
    (Function.swap (φ := fun (a a_1 : FractionalIdeal S P) ↦ FractionalIdeal S P)
      (fun (x1 x2 : FractionalIdeal S P) ↦ x1 * x2) I J')

Tactic:
simpa only [mul_def] using mul_le.mpr fun x hx y hy => mul_mem_mul (h hx) hy

Premises used: Iff.mpr, Submodule.mul_mem_mul, FractionalIdeal.mul_def, Submodule.mul_le
-- 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 j : P
hi : i ∈ I
hj : j ∈ J
simp :
  i * j ∈ Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) ((↑I : Submodule R P) * (↑J : Submodule R P)) ⋯
⊢ i * j ∈ I * J

Tactic:
simp only [mul_def]

Premises used: FractionalIdeal.mul_def
-- 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 j : P
hi : i ∈ I
hj : j ∈ J
⊢ i * j ∈ Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) ((↑I : Submodule R P) * (↑J : Submodule R P)) ⋯

Tactic:
Submodule.mul_mem_mul hi hj

Premises used: Submodule.mul_mem_mul, 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 J : FractionalIdeal S P
i j : P
hi : i ∈ I
hj : j ∈ J
⊢ i * j ∈ Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) ((↑I : Submodule R P) * (↑J : Submodule R P)) ⋯

Tactic:
exact Submodule.mul_mem_mul hi hj

Premises used: Submodule.mul_mem_mul
-- 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 K : FractionalIdeal S P
simp :
  Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) ((↑I : Submodule R P) * (↑J : Submodule R P)) ⋯ ≤ K ↔
    ∀ i ∈ I, ∀ j ∈ J, i * j ∈ K
⊢ I * J ≤ K ↔ ∀ i ∈ I, ∀ j ∈ J, i * j ∈ K

Tactic:
simp only [mul_def]

Premises used: FractionalIdeal.mul_def
-- 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 K : FractionalIdeal S P
⊢ Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) ((↑I : Submodule R P) * (↑J : Submodule R P)) ⋯ ≤ K ↔
    ∀ i ∈ I, ∀ j ∈ J, i * j ∈ K

Tactic:
Submodule.mul_le

Premises used: Set.Mem, Submodule.mul_le
-- 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 K : FractionalIdeal S P
⊢ Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) ((↑I : Submodule R P) * (↑J : Submodule R P)) ⋯ ≤ K ↔
    ∀ i ∈ I, ∀ j ∈ J, i * j ∈ K

Tactic:
exact Submodule.mul_le

Premises used: Submodule.mul_le
-- 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
n : ℕ
⊢ (↑(I ^ n) : Submodule R P) = (↑I : Submodule R P) ^ n

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 J : FractionalIdeal S P
C : P → Prop
r : P
hr : r ∈ I * J
hm : ∀ i ∈ I, ∀ j ∈ J, C (i * j)
ha : ∀ (x y : P), C x → C y → C (x + y)
⊢ r ∈ Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) ((↑I : Submodule R P) * (↑J : Submodule R P)) ⋯

Tactic:
simp only [mul_def] at hr

Premises used: FractionalIdeal.mul_def
-- 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
C : P → Prop
r : P
hm : ∀ i ∈ I, ∀ j ∈ J, C (i * j)
ha : ∀ (x y : P), C x → C y → C (x + y)
hr : r ∈ Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) ((↑I : Submodule R P) * (↑J : Submodule R P)) ⋯
⊢ C r

Tactic:
Submodule.mul_induction_on hr hm ha

Premises used: Submodule.mul_induction_on