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
inst_3 : IsLocalization S P
P' : Type u_5
inst_4 : CommRing P'
inst_5 : Algebra R P'
inst_6 : IsLocalization S P'
x : P
z : R
h :
  Membership.mem (γ := FractionalIdeal S P')
    (spanSingleton S ((IsLocalization.map (M := S) (T := S) P' (RingHom.id R) ⋯ : (a : P) → P') x) :
      FractionalIdeal S P')
    (HSMul.hSMul (β := P') z ((IsLocalization.map (M := S) (T := S) P' (RingHom.id R) ⋯ : (a : P) → P') x : P'))
right :
  (IsLocalization.map (M := S) (T := S) P' (RingHom.id R) ⋯ : (a : P) → P') (z • x) =
    HSMul.hSMul (β := P') z ((IsLocalization.map (M := S) (T := S) P' (RingHom.id R) ⋯ : (a : P) → P') x : P')
⊢ Membership.mem (γ := FractionalIdeal S P) (spanSingleton S x) (z • x) ∧
    (IsLocalization.map (M := S) (T := S) P' (RingHom.id R) ⋯ : (a : P) → P') (z • x) =
      HSMul.hSMul (β := P') z ((IsLocalization.map (M := S) (T := S) P' (RingHom.id R) ⋯ : (a : P) → P') x : P')

Tactic:
use (mem_spanSingleton _).mpr ⟨z, rfl⟩

Premises used: Iff.mpr, FractionalIdeal.mem_spanSingleton, Exists.intro, 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
P' : Type u_5
inst_4 : CommRing P'
inst_5 : Algebra R P'
inst_6 : IsLocalization S P'
x : P
z : R
h :
  Membership.mem (γ := FractionalIdeal S P')
    (spanSingleton S ((IsLocalization.map (M := S) (T := S) P' (RingHom.id R) ⋯ : (a : P) → P') x) :
      FractionalIdeal S P')
    (HSMul.hSMul (β := P') z ((IsLocalization.map (M := S) (T := S) P' (RingHom.id R) ⋯ : (a : P) → P') x : P'))
⊢ (IsLocalization.map (M := S) (T := S) P' (RingHom.id R) ⋯ : (a : P) → P') (z • x) =
    HSMul.hSMul (β := P') z ((IsLocalization.map (M := S) (T := S) P' (RingHom.id R) ⋯ : (a : P) → P') x : P')

Tactic:
simp [IsLocalization.map_smul]

Premises used: IsLocalization.map_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
inst_3 : IsLocalization S P
x y : P
I : FractionalIdeal S P
mp : y ∈ spanSingleton S x * I → ∃ y' ∈ I, y = x * y'
mpr : (∃ y' ∈ I, y = x * y') → y ∈ spanSingleton S x * I
⊢ y ∈ spanSingleton S x * I ↔ ∃ y' ∈ I, y = x * y'

Tactic:
constructor
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
inst_3 : IsLocalization S P
x y : P
I : FractionalIdeal S P
h : y ∈ spanSingleton S x * I
⊢ ∃ y' ∈ I, y = x * y'

Tactic:
FractionalIdeal.mul_induction_on h ?_ ?_

Premises used: FractionalIdeal.mul_induction_on
-- 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
I : FractionalIdeal S P
h : y ∈ spanSingleton S x * I
mp : ∀ (i : P), Membership.mem (γ := FractionalIdeal S P) (spanSingleton S x) i → ∀ j ∈ I, ∃ y' ∈ I, i * j = x * y'
mp₁ : ∀ (x_1 y : P), (∃ y' ∈ I, x_1 = x * y') → (∃ y' ∈ I, y = x * y') → ∃ y' ∈ I, x_1 + y = x * y'
⊢ ∃ y' ∈ I, y = x * y'

Tactic:
refine FractionalIdeal.mul_induction_on 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
x y : P
I : FractionalIdeal S P
h : y ∈ spanSingleton S x * I
x' : P
hx' : Membership.mem (γ := FractionalIdeal S P) (spanSingleton S x) x'
y' : P
hy' : y' ∈ I
mp : ∀ (a : R) (ha : a • x = x'), ∃ y'_1 ∈ I, x' * y' = x * y'_1
⊢ ∃ y'_1 ∈ I, x' * y' = x * y'_1

Tactic:
obtain ⟨a, ha⟩ := (mem_spanSingleton S).mp hx'

Premises used: FractionalIdeal.mem_spanSingleton, Iff.mp
-- 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
I : FractionalIdeal S P
h : y ∈ spanSingleton S x * I
x' : P
hx' : Membership.mem (γ := FractionalIdeal S P) (spanSingleton S x) x'
y' : P
hy' : y' ∈ I
a : R
ha : a • x = x'
right : x' * y' = x * a • y'
⊢ ∃ y'_1 ∈ I, x' * y' = x * y'_1

Tactic:
use a • y', Submodule.smul_mem (I : Submodule R P) a hy'

Premises used: FractionalIdeal.coeToSubmodule, Submodule.smul_mem
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
inst_3 : IsLocalization S P
x y : P
I : FractionalIdeal S P
h : y ∈ spanSingleton S x * I
x' : P
hx' : Membership.mem (γ := FractionalIdeal S P) (spanSingleton S x) x'
y' : P
hy' : y' ∈ I
a : R
ha : a • x = x'
right : a • x * y' = x * a • y'
right₁ : a • x * y' = a • (x * y')
right₂ right₃ : a • (x * y') = a • (x * y')
⊢ x' * y' = x * a • y'

Tactic:
rw [← ha, Algebra.mul_smul_comm, Algebra.smul_mul_assoc]

Premises used: Algebra.mul_smul_comm, Algebra.smul_mul_assoc
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
inst_3 : IsLocalization S P
x y_1 : P
I : FractionalIdeal S P
h : y_1 ∈ spanSingleton S x * I
y : P
hy : y ∈ I
y' : P
hy' : y' ∈ I
⊢ ∃ y'_1 ∈ I, x * y + x * y' = x * y'_1

Tactic:
⟨y + y', Submodule.add_mem (I : Submodule R P) hy hy', (mul_add _ _ _).symm⟩

Premises used: FractionalIdeal.coeToSubmodule, HAdd.hAdd, And.intro, Exists.intro, mul_add, Eq.symm, Submodule.add_mem
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
inst_3 : IsLocalization S P
x y_1 : P
I : FractionalIdeal S P
h : y_1 ∈ spanSingleton S x * I
y : P
hy : y ∈ I
y' : P
hy' : y' ∈ I
⊢ ∃ y'_1 ∈ I, x * y + x * y' = x * y'_1

Tactic:
exact ⟨y + y', Submodule.add_mem (I : Submodule R P) hy hy', (mul_add _ _ _).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
I : FractionalIdeal S P
y' : P
hy' : y' ∈ I
⊢ x * y' ∈ spanSingleton S x * I

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

Premises used: Iff.mpr, FractionalIdeal.mem_spanSingleton, one_smul, Exists.intro, FractionalIdeal.mul_mem_mul, OfNat.ofNat
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
inst_3 : IsLocalization S P
x : P
I : FractionalIdeal S P
y' : P
hy' : y' ∈ I
⊢ x * y' ∈ spanSingleton S x * I

Tactic:
exact mul_mem_mul ((mem_spanSingleton S).mpr ⟨1, one_smul _ _⟩) hy'

Premises used: Iff.mpr, FractionalIdeal.mem_spanSingleton, Exists.intro, FractionalIdeal.mul_mem_mul, 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
I J : Ideal R₁
x y : R₁
hy : Membership.mem (γ := Submonoid R₁) R₁⁰ y
rw :
  Eq (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
    (spanSingleton R₁⁰
      (HMul.hMul (β := K)
        (mk' K 1 (Subtype.mk (p := fun (x : R₁) ↦ Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) x) y hy))
        ((algebraMap R₁ K : (a : R₁) → K) y : K)))
    1
rw₁ :
  Eq (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
    (spanSingleton R₁⁰
      (HMul.hMul (α := K) ((algebraMap R₁ K : (a : R₁) → K) y : K)
        (mk' K 1 (Subtype.mk (p := fun (x : R₁) ↦ Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) x) y hy))))
    1
rw₂ :
  Eq (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
    (spanSingleton R₁⁰
      (mk' K y (Subtype.mk (p := fun (x : R₁) ↦ Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) x) y hy)))
    1
rw₃ : Eq.{u_4 + 1} (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ 1) 1
rw₄ rw₅ : Eq.{u_4 + 1} (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 1
⊢ HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (β := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
      (spanSingleton R₁⁰
        (mk' K 1 (Subtype.mk (p := fun (x : R₁) ↦ Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) x) y hy)))
      (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) y) : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) =
    1

Tactic:
rw [spanSingleton_mul_spanSingleton, mul_comm, ← IsLocalization.mk'_eq_mul_mk'_one,
      IsLocalization.mk'_self, spanSingleton_one]

Premises used: FractionalIdeal.spanSingleton_mul_spanSingleton, IsLocalization.mk'_eq_mul_mk'_one, IsLocalization.mk'_self, mul_comm, FractionalIdeal.spanSingleton_one
-- 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
I J : Ideal R₁
x y : R₁
hy : Membership.mem (γ := Submonoid R₁) R₁⁰ y
⊢ HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (β := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
      (spanSingleton R₁⁰
        (mk' K 1 (Subtype.mk (p := fun (x : R₁) ↦ Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) x) y hy)))
      (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) y) : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) =
    1

Tactic:
have :
    spanSingleton R₁⁰ (IsLocalization.mk' _ (1 : R₁) ⟨y, hy⟩) *
        spanSingleton R₁⁰ (algebraMap R₁ K y) =
      1 := by
    rw [spanSingleton_mul_spanSingleton, mul_comm, ← IsLocalization.mk'_eq_mul_mk'_one,
      IsLocalization.mk'_self, spanSingleton_one]
-- 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
I J : Ideal R₁
x y : R₁
hy : Membership.mem (γ := Submonoid R₁) R₁⁰ y
this :
  HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (β := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
      (spanSingleton R₁⁰
        (mk' K 1 (Subtype.mk (p := fun (x : R₁) ↦ Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) x) y hy)))
      (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) y) : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) =
    1
y' : (FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)ˣ :=
  Units.mkOfMulEqOne
    (spanSingleton R₁⁰
      (mk' K 1 (Subtype.mk (p := fun (x : R₁) ↦ Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) x) y hy)))
    (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) y)) this
⊢ (↑y' : FractionalIdeal R₁⁰ K) =
    spanSingleton R₁⁰
      (mk' K 1 (Subtype.mk (p := fun (x : R₁) ↦ Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) x) y hy))

Tactic:
have coe_y' : ↑y' = spanSingleton R₁⁰ (IsLocalization.mk' K (1 : R₁) ⟨y, hy⟩) := 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
I J : Ideal R₁
x y : R₁
hy : Membership.mem (γ := Submonoid R₁) R₁⁰ y
this :
  HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (β := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
      (spanSingleton R₁⁰
        (mk' K 1 (Subtype.mk (p := fun (x : R₁) ↦ Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) x) y hy)))
      (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) y) : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) =
    1
y' : (FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)ˣ :=
  Units.mkOfMulEqOne
    (spanSingleton R₁⁰
      (mk' K 1 (Subtype.mk (p := fun (x : R₁) ↦ Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) x) y hy)))
    (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) y)) this
coe_y' :
  (↑y' : FractionalIdeal R₁⁰ K) =
    spanSingleton R₁⁰
      (mk' K 1 (Subtype.mk (p := fun (x : R₁) ↦ Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) x) y hy))
⊢ HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
        (spanSingleton R₁⁰
          (mk' K x (Subtype.mk (p := fun (x : R₁) ↦ Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) x) y hy)))
        (↑I : FractionalIdeal R₁⁰ K) =
      (↑J : FractionalIdeal R₁⁰ K) ↔
    Ideal.span {x} * I = Ideal.span {y} * J

Tactic:
Iff.trans ?_ (y'.mul_right_inj.trans coeIdeal_inj)

Premises used: FractionalIdeal.coeIdeal_inj, Iff.trans, Units.mul_right_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
I J : Ideal R₁
x y : R₁
hy : Membership.mem (γ := Submonoid R₁) R₁⁰ y
this :
  HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (β := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
      (spanSingleton R₁⁰
        (mk' K 1 (Subtype.mk (p := fun (x : R₁) ↦ Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) x) y hy)))
      (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) y) : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) =
    1
y' : (FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)ˣ :=
  Units.mkOfMulEqOne
    (spanSingleton R₁⁰
      (mk' K 1 (Subtype.mk (p := fun (x : R₁) ↦ Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) x) y hy)))
    (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) y)) this
coe_y' :
  (↑y' : FractionalIdeal R₁⁰ K) =
    spanSingleton R₁⁰
      (mk' K 1 (Subtype.mk (p := fun (x : R₁) ↦ Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) x) y hy))
refine :
  HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
        (spanSingleton R₁⁰
          (mk' K x (Subtype.mk (p := fun (x : R₁) ↦ Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) x) y hy)))
        (↑I : FractionalIdeal R₁⁰ K) =
      (↑J : FractionalIdeal R₁⁰ K) ↔
    (↑y' : FractionalIdeal R₁⁰ K) * (↑(Ideal.span {x} * I) : FractionalIdeal R₁⁰ K) =
      (↑y' : FractionalIdeal R₁⁰ K) * (↑(Ideal.span {y} * J) : FractionalIdeal R₁⁰ K)
⊢ HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
        (spanSingleton R₁⁰
          (mk' K x (Subtype.mk (p := fun (x : R₁) ↦ Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) x) y hy)))
        (↑I : FractionalIdeal R₁⁰ K) =
      (↑J : FractionalIdeal R₁⁰ K) ↔
    Ideal.span {x} * I = Ideal.span {y} * J

Tactic:
refine Iff.trans ?_ (y'.mul_right_inj.trans coeIdeal_inj)

Premises used: FractionalIdeal.coeIdeal_inj, Iff.trans, Units.mul_right_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
I J : Ideal R₁
z : K
rw :
  HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ z) (↑I : FractionalIdeal R₁⁰ K) =
      (↑J : FractionalIdeal R₁⁰ K) ↔
    HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
        (spanSingleton R₁⁰
          (mk'.{u_3, u_4} (R := R₁) (M := R₁⁰) K (sec R₁⁰ z).1
            (Subtype.mk (p := fun (x : R₁) ↦ Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) x)
              (↑(sec R₁⁰ z).2 : R₁) ⋯)))
        (↑I : FractionalIdeal R₁⁰ K) =
      (↑J : FractionalIdeal R₁⁰ K)
rw₁ rw₂ :
  HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ z) (↑I : FractionalIdeal R₁⁰ K) =
      (↑J : FractionalIdeal R₁⁰ K) ↔
    HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ z) (↑I : FractionalIdeal R₁⁰ K) =
      (↑J : FractionalIdeal R₁⁰ K)
⊢ HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ z) (↑I : FractionalIdeal R₁⁰ K) =
      (↑J : FractionalIdeal R₁⁰ K) ↔
    Ideal.span {(sec R₁⁰ z).1} * I = Ideal.span {(↑(sec R₁⁰ z).2 : R₁)} * J

Tactic:
rw [← mk'_mul_coeIdeal_eq_coeIdeal K (IsLocalization.sec R₁⁰ z).2.prop,
    IsLocalization.mk'_sec K z]

Premises used: IsLocalization.sec, FractionalIdeal.mk'_mul_coeIdeal_eq_coeIdeal, nonZeroDivisors, IsLocalization.mk'_sec, Subtype.prop, Prod.snd
-- 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₁
x : K
h : x = 0
⊢ HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ x) = spanSingleton R₁⁰ x⁻¹

Tactic:
simp [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₁
x : K
h : ¬x = 0
⊢ HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ x) (spanSingleton R₁⁰ x⁻¹) = 1

Tactic:
simp [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₁
x : K
⊢ HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ x) = spanSingleton R₁⁰ x⁻¹

Tactic:
exact if h : x = 0 then by simp [h] else (eq_one_div_of_mul_eq_one_right _ _ (by simp [h])).symm

Premises used: FractionalIdeal.eq_one_div_of_mul_eq_one_right, Eq.symm
-- 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₁
x : K
⊢ HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ x) = spanSingleton R₁⁰ x⁻¹

Tactic:
classical
  exact if h : x = 0 then by simp [h] else (eq_one_div_of_mul_eq_one_right _ _ (by simp [h])).symm

Premises used: FractionalIdeal.eq_one_div_of_mul_eq_one_right, Eq.symm
-- 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₁
J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
d : K
rw : J / spanSingleton R₁⁰ d = HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * J
⊢ J / spanSingleton R₁⁰ d = spanSingleton R₁⁰ d⁻¹ * J

Tactic:
rw [← one_div_spanSingleton]

Premises used: FractionalIdeal.one_div_spanSingleton
-- 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₁
J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
d : K
pos :
  ∀ (hd : d = 0),
    J / spanSingleton R₁⁰ d = HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * J
neg :
  ∀ (hd : ¬d = 0),
    J / spanSingleton R₁⁰ d = HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * J
⊢ J / spanSingleton R₁⁰ d = HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * J

Tactic:
by_cases hd : d = 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₁
J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
d : K
hd : d = 0
⊢ J / spanSingleton R₁⁰ d = HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * J

Tactic:
simp only [hd, spanSingleton_zero, div_zero, zero_mul]

Premises used: MulZeroClass.zero_mul, FractionalIdeal.spanSingleton_zero, FractionalIdeal.div_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₁
J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
d : K
hd : ¬d = 0
⊢ Ne (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ d) 0

Tactic:
have h_spand : spanSingleton R₁⁰ d ≠ 0 := mt spanSingleton_eq_zero_iff.mp hd
-- 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₁
J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
d : K
hd : ¬d = 0
h_spand : Ne (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ d) 0
neg : J / spanSingleton R₁⁰ d ≤ HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * J
neg₁ : HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * J ≤ J / spanSingleton R₁⁰ d
⊢ J / spanSingleton R₁⁰ d = HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * J

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₁
J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
d : K
hd : ¬d = 0
h_spand : Ne (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ d) 0
x : K
hx : x ∈ J / spanSingleton R₁⁰ d
⊢ ∀ (y : K),
    Membership.mem (γ := Submodule R₁ K) (↑(spanSingleton R₁⁰ d) : Submodule R₁ K) y → x * y ∈ (↑J : Submodule R₁ K)

Tactic:
rw [← mem_coe, coe_div h_spand, Submodule.mem_div_iff_forall_mul_mem] at hx

Premises used: Submodule.mem_div_iff_forall_mul_mem, FractionalIdeal.mem_coe, FractionalIdeal.coe_div
-- 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₁
J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
d : K
hd : ¬d = 0
h_spand : Ne (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ d) 0
x : K
hx :
  ∀ (y : K),
    Membership.mem (γ := Submodule R₁ K) (↑(spanSingleton R₁⁰ d) : Submodule R₁ K) y → x * y ∈ (↑J : Submodule R₁ K)
⊢ x * d ∈ (↑J : Submodule R₁ K)

Tactic:
specialize hx d (mem_spanSingleton_self R₁⁰ d)

Premises used: nonZeroDivisors, FractionalIdeal.mem_spanSingleton_self
-- 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₁
J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
d : K
hd : ¬d = 0
h_spand : Ne (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ d) 0
x : K
hx : x * d ∈ (↑J : Submodule R₁ K)
⊢ x = d⁻¹ * (x * d)

Tactic:
field
-- 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₁
J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
d : K
hd : ¬d = 0
h_spand : Ne (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ d) 0
x : K
hx : x * d ∈ (↑J : Submodule R₁ K)
⊢ x = d⁻¹ * (x * d)

Tactic:
have h_xd : x = d⁻¹ * (x * d) := by field
-- 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₁
J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
d : K
hd : ¬d = 0
h_spand : Ne (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ d) 0
x : K
hx : x * d ∈ (↑J : Submodule R₁ K)
h_xd : x = d⁻¹ * (x * d)
neg : d⁻¹ * (x * d) ∈ (↑(spanSingleton R₁⁰ d⁻¹) : Submodule R₁ K) * (↑J : Submodule R₁ K)
⊢ x ∈ HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * J

Tactic:
rw [← mem_coe, coe_mul, one_div_spanSingleton, h_xd]

Premises used: FractionalIdeal.one_div_spanSingleton, FractionalIdeal.coe_mul, FractionalIdeal.mem_coe
-- 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₁
J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
d : K
hd : ¬d = 0
h_spand : Ne (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ d) 0
x : K
hx : x * d ∈ (↑J : Submodule R₁ K)
h_xd : x = d⁻¹ * (x * d)
⊢ d⁻¹ * (x * d) ∈ (↑(spanSingleton R₁⁰ d⁻¹) : Submodule R₁ K) * (↑J : Submodule R₁ K)

Tactic:
Submodule.mul_mem_mul (mem_spanSingleton_self R₁⁰ _) hx

Premises used: Submodule.mul_mem_mul, Set.Mem, nonZeroDivisors, FractionalIdeal.mem_spanSingleton_self