awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
inst_4 : IsDomain R₁
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
x : K
h :
  x ∈ Subtype.mk (p := fun (I : Submodule R₁ K) ↦ IsFractional R₁⁰ I) ((↑I : Submodule R₁ K) / (↑1 : Submodule R₁ K)) ⋯
⊢ x ∈ I

Tactic:
simpa using mem_div_iff_forall_mul_mem.mp h 1 ((algebraMap R₁ K).map_one ▸ coe_mem_one R₁⁰ 1)

Premises used: FractionalIdeal.coe_mem_one, Algebra.algebraMap, Submodule.mem_div_iff_forall_mul_mem, nonZeroDivisors, RingHom.map_one, Eq.rec, Iff.mp, OfNat.ofNat
-- 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
inst_4 : IsDomain R₁
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
x : K
h : x ∈ I
y' : R₁
left : y' ∈ (↑⊤ : Set R₁)
⊢ y' • x ∈ (↑I : Submodule R₁ K)

Tactic:
Submodule.smul_mem _ y' h

Premises used: Submodule.smul_mem
-- 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
inst_4 : IsDomain R₁
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
x : K
h : x ∈ I
y' : R₁
left : y' ∈ (↑⊤ : Set R₁)
h₁ : HMul.hMul (β := K) x ((Algebra.linearMap R₁ K : (a : R₁) → K) y' : K) = y' • x
⊢ HMul.hMul (β := K) x ((Algebra.linearMap R₁ K : (a : R₁) → K) y' : K) ∈ (↑I : Submodule R₁ K)

Tactic:
convert! Submodule.smul_mem _ y' h using 1

Premises used: Submodule.smul_mem
-- 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
inst_4 : IsDomain R₁
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
x : K
h : x ∈ I
y' : R₁
left : y' ∈ (↑⊤ : Set R₁)
h₁ : HMul.hMul (α := K) ((Algebra.linearMap R₁ K : (a : R₁) → K) y' : K) x = y' • x
h₂ : HMul.hMul (α := K) ((algebraMap R₁ K : (a : R₁) → K) y' : K) x = y' • x
h₃ h₄ : y' • x = y' • x
⊢ HMul.hMul (β := K) x ((Algebra.linearMap R₁ K : (a : R₁) → K) y' : K) = y' • x

Tactic:
rw [mul_comm, Algebra.linearMap_apply, ← Algebra.smul_def]

Premises used: Algebra.linearMap_apply, mul_comm, Algebra.smul_def
-- 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
inst_4 : IsDomain R₁
I J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
h : I * J = 1
⊢ I ≠ 0

Tactic:
have hI : I ≠ 0 := ne_zero_of_mul_eq_one I J h
-- 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
inst_4 : IsDomain R₁
I J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
h : I * J = 1
hI : I ≠ 0
suffices : I * (1 / I) = 1
⊢ J = 1 / I

Tactic:
suffices h' : I * (1 / I) = 1 from
    congr_arg Units.inv <| @Units.ext _ _ (Units.mkOfMulEqOne _ _ h) (Units.mkOfMulEqOne _ _ h') 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
inst_4 : IsDomain R₁
I J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
h : I * J = 1
hI : I ≠ 0
a : I * (1 / I) ≤ 1
a₁ : 1 ≤ I * (1 / I)
⊢ I * (1 / I) = 1

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- 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
inst_4 : IsDomain R₁
I J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
h : I * J = 1
hI : I ≠ 0
apply : ∀ i ∈ I, ∀ j ∈ 1 / I, Membership.mem (γ := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (i * j)
⊢ I * (1 / I) ≤ 1

Tactic:
apply mul_le.mpr _

Premises used: Iff.mpr, FractionalIdeal.mul_le
-- 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
inst_4 : IsDomain R₁
I J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
h : I * J = 1
hI : I ≠ 0
x : K
hx : x ∈ I
y : K
hy : y ∈ 1 / I
rw : Membership.mem (γ := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (y * x)
⊢ Membership.mem (γ := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (x * y)

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- 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
inst_4 : IsDomain R₁
I J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
h : I * J = 1
hI : I ≠ 0
x : K
hx : x ∈ I
y : K
hy : y ∈ 1 / I
⊢ Membership.mem (γ := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (y * x)

Tactic:
(mem_div_iff_of_ne_zero hI).mp hy x hx

Premises used: Set.Mem, Iff.mp, FractionalIdeal.mem_div_iff_of_ne_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
inst_4 : IsDomain R₁
I J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
h : I * J = 1
hI : I ≠ 0
x : K
hx : x ∈ I
y : K
hy : y ∈ 1 / I
⊢ Membership.mem (γ := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (y * x)

Tactic:
exact (mem_div_iff_of_ne_zero hI).mp hy x hx

Premises used: Iff.mp, FractionalIdeal.mem_div_iff_of_ne_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
inst_4 : IsDomain R₁
I J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
h : I * J = 1
hI : I ≠ 0
a : I * J ≤ I * (I * J / I)
⊢ 1 ≤ I * (1 / I)

Tactic:
rw [← h]
-- 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
inst_4 : IsDomain R₁
I J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
h : I * J = 1
hI : I ≠ 0
a : J ≤ I * J / I
⊢ I * J ≤ I * (I * J / I)

Tactic:
gcongr
-- 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
inst_4 : IsDomain R₁
I J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
h : I * J = 1
hI : I ≠ 0
apply : ∀ x ∈ J, ∀ y ∈ I, x * y ∈ I * J
⊢ J ≤ I * J / I

Tactic:
apply (le_div_iff_of_ne_zero hI).mpr _

Premises used: Iff.mpr, FractionalIdeal.le_div_iff_of_ne_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
inst_4 : IsDomain R₁
I J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
h : I * J = 1
hI : I ≠ 0
y : K
hy : y ∈ J
x : K
hx : x ∈ I
rw : y * x ∈ J * I
⊢ y * x ∈ I * J

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- 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
inst_4 : IsDomain R₁
I J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
h : I * J = 1
hI : I ≠ 0
y : K
hy : y ∈ J
x : K
hx : x ∈ I
⊢ y * x ∈ J * I

Tactic:
mul_mem_mul hy hx

Premises used: Set.Mem, FractionalIdeal.mul_mem_mul
-- 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
inst_4 : IsDomain R₁
I J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
h : I * J = 1
hI : I ≠ 0
y : K
hy : y ∈ J
x : K
hx : x ∈ I
⊢ y * x ∈ J * I

Tactic:
exact mul_mem_mul hy hx

Premises used: FractionalIdeal.mul_mem_mul
-- 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
inst_4 : IsDomain R₁
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
h : ∃ (J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K), I * J = 1
J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
hJ rwa rwa₁ rwa₂ rwa₃ : I * J = 1
⊢ I * (1 / I) = 1

Tactic:
rwa [← eq_one_div_of_mul_eq_one_right I J hJ]

Premises used: FractionalIdeal.eq_one_div_of_mul_eq_one_right
-- 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
inst_4 : IsDomain R₁
K' : Type u_5
inst_5 : Field K'
inst_6 : Algebra R₁ K'
inst_7 : IsFractionRing R₁ K'
I J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
h : K ≃ₐ[R₁] K'
pos : ∀ (H : J = 0), map (↑h : K →ₐ[R₁] K') (I / J) = map (↑h : K →ₐ[R₁] K') I / map (↑h : K →ₐ[R₁] K') J
neg : ∀ (H : ¬J = 0), map (↑h : K →ₐ[R₁] K') (I / J) = map (↑h : K →ₐ[R₁] K') I / map (↑h : K →ₐ[R₁] K') J
⊢ map (↑h : K →ₐ[R₁] K') (I / J) = map (↑h : K →ₐ[R₁] K') I / map (↑h : K →ₐ[R₁] K') J

Tactic:
by_cases H : J = 0
-- 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
inst_4 : IsDomain R₁
K' : Type u_5
inst_5 : Field K'
inst_6 : Algebra R₁ K'
inst_7 : IsFractionRing R₁ K'
I J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
h : K ≃ₐ[R₁] K'
H : J = 0
pos : map (↑h : K →ₐ[R₁] K') (I / 0) = map (↑h : K →ₐ[R₁] K') I / map (↑h : K →ₐ[R₁] K') 0
pos₁ : map (↑h : K →ₐ[R₁] K') 0 = map (↑h : K →ₐ[R₁] K') I / map (↑h : K →ₐ[R₁] K') 0
pos₂ : 0 = map (↑h : K →ₐ[R₁] K') I / 0
pos₃ pos₄ : Eq.{u_5 + 1} (α := FractionalIdeal.{u_3, u_5} (R := R₁) R₁⁰ K') 0 0
⊢ map (↑h : K →ₐ[R₁] K') (I / J) = map (↑h : K →ₐ[R₁] K') I / map (↑h : K →ₐ[R₁] K') J

Tactic:
rw [H, div_zero, FractionalIdeal.map_zero, div_zero]

Premises used: FractionalIdeal.div_zero, FractionalIdeal.map_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
inst_4 : IsDomain R₁
K' : Type u_5
inst_5 : Field K'
inst_6 : Algebra R₁ K'
inst_7 : IsFractionRing R₁ K'
I J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
h : K ≃ₐ[R₁] K'
H : ¬J = 0
⊢ map (↑h : K →ₐ[R₁] K') (I / J) = map (↑h : K →ₐ[R₁] K') I / map (↑h : K →ₐ[R₁] K') J

Tactic:
simp [← coeToSubmodule_inj, div_of_ne_zero H, div_of_ne_zero (map_ne_zero _ H)]

Premises used: FractionalIdeal.div_of_ne_zero, FractionalIdeal.map_ne_zero, FractionalIdeal.coeToSubmodule_inj
-- 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
inst_4 : IsDomain R₁
K' : Type u_5
inst_5 : Field K'
inst_6 : Algebra R₁ K'
inst_7 : IsFractionRing R₁ K'
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
h : K ≃ₐ[R₁] K'
rw : map (↑h : K →ₐ[R₁] K') 1 / map (↑h : K →ₐ[R₁] K') I = 1 / map (↑h : K →ₐ[R₁] K') I
rw₁ rw₂ : 1 / map (↑h : K →ₐ[R₁] K') I = 1 / map (↑h : K →ₐ[R₁] K') I
⊢ map (↑h : K →ₐ[R₁] K') (1 / I) = 1 / map (↑h : K →ₐ[R₁] K') I

Tactic:
rw [FractionalIdeal.map_div, FractionalIdeal.map_one]

Premises used: FractionalIdeal.map_div, FractionalIdeal.map_one
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsFractionRing K L
I : FractionalIdeal.{u_4, u_5} (R := K) K⁰ L
rw : ¬I = 0 → I = 1
⊢ I = 0 ∨ I = 1

Tactic:
rw [or_iff_not_imp_left]

Premises used: Classical.or_iff_not_imp_left
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsFractionRing K L
I : FractionalIdeal.{u_4, u_5} (R := K) K⁰ L
hI : ¬I = 0
simp_rw : ∀ (x : L), x ∈ I ↔ ∃ (x' : K), (algebraMap K L : (a : K) → L) x' = x
⊢ I = 1

Tactic:
simp_rw [@SetLike.ext_iff _ _ _ I 1, mem_one_iff]

Premises used: FractionalIdeal.mem_one_iff, SetLike.ext_iff
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsFractionRing K L
I : FractionalIdeal.{u_4, u_5} (R := K) K⁰ L
hI : ¬I = 0
x : L
mp : x ∈ I → ∃ (x' : K), (algebraMap K L : (a : K) → L) x' = x
mpr : (∃ (x' : K), (algebraMap K L : (a : K) → L) x' = x) → x ∈ I
⊢ x ∈ I ↔ ∃ (x' : K), (algebraMap K L : (a : K) → L) x' = x

Tactic:
constructor
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsFractionRing K L
I : FractionalIdeal.{u_4, u_5} (R := K) K⁰ L
hI : ¬I = 0
x : L
x_mem : x ∈ I
mp :
  ∀ (n : K) (d : ↥(K⁰ : Submonoid K)) (x_mem : mk' L n d ∈ I), ∃ (x' : K), (algebraMap K L : (a : K) → L) x' = mk' L n d
⊢ ∃ (x' : K), (algebraMap K L : (a : K) → L) x' = x

Tactic:
obtain ⟨n, d, rfl⟩ := IsLocalization.exists_mk'_eq K⁰ x

Premises used: nonZeroDivisors, rfl, IsLocalization.exists_mk'_eq
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsFractionRing K L
I : FractionalIdeal.{u_4, u_5} (R := K) K⁰ L
hI : ¬I = 0
n : K
d : ↥(K⁰ : Submonoid K)
x_mem : mk' L n d ∈ I
⊢ ∃ (x' : K), (algebraMap K L : (a : K) → L) x' = mk' L n d

Tactic:
⟨n / d, ?_⟩

Premises used: HDiv.hDiv, Exists.intro, Subtype.val
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsFractionRing K L
I : FractionalIdeal.{u_4, u_5} (R := K) K⁰ L
hI : ¬I = 0
n : K
d : ↥(K⁰ : Submonoid K)
x_mem : mk' L n d ∈ I
mp : (algebraMap K L : (a : K) → L) (n / (↑d : K)) = mk' L n d
⊢ ∃ (x' : K), (algebraMap K L : (a : K) → L) x' = mk' L n d

Tactic:
refine ⟨n / d, ?_⟩
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsFractionRing K L
I : FractionalIdeal.{u_4, u_5} (R := K) K⁰ L
hI : ¬I = 0
n : K
d : ↥(K⁰ : Submonoid K)
x_mem : mk' L n d ∈ I
mp :
  HDiv.hDiv (α := L) (β := L) ((algebraMap K L : (a : K) → L) n : L) ((algebraMap K L : (a : K) → L) (↑d : K) : L) =
    mk' L n d
mp₁ mp₂ :
  HDiv.hDiv (α := L) (β := L) ((algebraMap K L : (a : K) → L) n : L) ((algebraMap K L : (a : K) → L) (↑d : K) : L) =
    HDiv.hDiv (α := L) (β := L) ((algebraMap K L : (a : K) → L) n : L) ((algebraMap K L : (a : K) → L) (↑d : K) : L)
⊢ (algebraMap K L : (a : K) → L) (n / (↑d : K)) = mk' L n d

Tactic:
rw [map_div₀, IsFractionRing.mk'_eq_div]

Premises used: IsFractionRing.mk'_eq_div, map_div₀
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsFractionRing K L
I : FractionalIdeal.{u_4, u_5} (R := K) K⁰ L
hI : ¬I = 0
x : K
mpr :
  ∀ (y : K) (y_ne : y ≠ 0) (y_mem : Membership.mem (α := L) I ((algebraMap K L : (a : K) → L) y : L)),
    Membership.mem (α := L) I ((algebraMap K L : (a : K) → L) x : L)
⊢ Membership.mem (α := L) I ((algebraMap K L : (a : K) → L) x : L)

Tactic:
obtain ⟨y, y_ne, y_mem⟩ := exists_ne_zero_mem_isInteger hI

Premises used: FractionalIdeal.exists_ne_zero_mem_isInteger
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsFractionRing K L
I : FractionalIdeal.{u_4, u_5} (R := K) K⁰ L
hI : ¬I = 0
x y : K
y_ne : y ≠ 0
y_mem : Membership.mem (α := L) I ((algebraMap K L : (a : K) → L) y : L)
mpr : HSMul.hSMul (β := L) (x / y) ((algebraMap K L : (a : K) → L) y : L) ∈ I
⊢ Membership.mem (α := L) I ((algebraMap K L : (a : K) → L) x : L)

Tactic:
rw [← div_mul_cancel₀ x y_ne, map_mul, ← Algebra.smul_def]

Premises used: div_mul_cancel₀, map_mul, Algebra.smul_def
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsFractionRing K L
I : FractionalIdeal.{u_4, u_5} (R := K) K⁰ L
hI : ¬I = 0
x y : K
y_ne : y ≠ 0
y_mem : Membership.mem (α := L) I ((algebraMap K L : (a : K) → L) y : L)
⊢ HSMul.hSMul (β := L) (x / y) ((algebraMap K L : (a : K) → L) y : L) ∈ I

Tactic:
smul_mem (M := L) I (x / y) y_mem

Premises used: Set.Mem, HDiv.hDiv, Submodule.smul_mem
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsFractionRing K L
I : FractionalIdeal.{u_4, u_5} (R := K) K⁰ L
hI : ¬I = 0
x y : K
y_ne : y ≠ 0
y_mem : Membership.mem (α := L) I ((algebraMap K L : (a : K) → L) y : L)
⊢ HSMul.hSMul (β := L) (x / y) ((algebraMap K L : (a : K) → L) y : L) ∈ I

Tactic:
exact smul_mem (M := L) I (x / y) y_mem

Premises used: HDiv.hDiv, Submodule.smul_mem
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R₁ : Type u_3
K : Type u_4
inst : CommRing R₁
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
hF : IsField R₁
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
⊢ I = 0 ∨ I = 1

Tactic:
letI : Field R₁ := hF.toField
  eq_zero_or_one I

Premises used: FractionalIdeal.eq_zero_or_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
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
obtain :
  ∀ (a' : ↥(R₁⁰ : Submonoid R₁)) (ha' : ∀ i ∈ s, IsInteger R₁ ((↑a' : R₁) • f i)),
    IsFractional R₁⁰ (span R₁ (f '' (↑s : Set ι)))
⊢ IsFractional R₁⁰ (span R₁ (f '' (↑s : Set ι)))

Tactic:
obtain ⟨a', ha'⟩ := IsLocalization.exist_integer_multiples R₁⁰ s f

Premises used: nonZeroDivisors, IsLocalization.exist_integer_multiples
-- 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)
⊢ IsFractional R₁⁰ (span R₁ (f '' (↑s : Set ι)))

Tactic:
⟨a', a'.2, fun x hx => Submodule.span_induction ?_ ?_ ?_ ?_ hx⟩

Premises used: IsFractional, Submodule.span_induction, And.intro, Exists.intro, 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
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)
refine_1 :
  ∀ (x : K) (hx : Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) x) (x : K)
    (h : x ∈ f '' (↑s : Set ι)), IsInteger R₁ ((↑a' : R₁) • x)
refine_2 :
  ∀ (x : K) (hx : Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) x),
    IsInteger R₁ (HSMul.hSMul (β := K) (↑a' : R₁) 0)
refine_3 :
  ∀ (x : K) (hx : Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) x) (x y : K)
    (hx : Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) x)
    (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))
refine_4 :
  ∀ (x : K) (hx : Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) x) (a : R₁) (x : K)
    (hx : Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) x),
    IsInteger R₁ ((↑a' : R₁) • x) → IsInteger R₁ ((↑a' : R₁) • a • x)
⊢ IsFractional R₁⁰ (span R₁ (f '' (↑s : Set ι)))

Tactic:
refine ⟨a', a'.2, fun x hx => Submodule.span_induction ?_ ?_ ?_ ?_ hx⟩
-- 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 : K
hx : Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) x
i : ι
hi : i ∈ (↑s : Set ι)
⊢ IsInteger R₁ ((↑a' : R₁) • f i)

Tactic:
ha' i hi
-- 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 : K
hx : Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) x
i : ι
hi : i ∈ (↑s : Set ι)
⊢ IsInteger R₁ ((↑a' : R₁) • f i)

Tactic:
exact ha' i hi
-- 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 : K
hx : Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) x
refine_2 : IsInteger.{u_3, u_4} R₁ (S := K) 0
⊢ IsInteger R₁ (HSMul.hSMul (β := K) (↑a' : R₁) 0)

Tactic:
rw [smul_zero]

Premises used: smul_zero
-- 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 : K
hx : Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) x
⊢ IsInteger.{u_3, u_4} R₁ (S := K) 0

Tactic:
IsLocalization.isInteger_zero

Premises used: IsLocalization.isInteger_zero
-- 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 : K
hx : Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) x
⊢ IsInteger.{u_3, u_4} R₁ (S := K) 0

Tactic:
exact IsLocalization.isInteger_zero

Premises used: IsLocalization.isInteger_zero
-- 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
refine_3 :
  Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) x →
    ∀ (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))
⊢ ∀ (hx : Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) x)
    (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:
_