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 J : Submodule R₁ K
aI : R₁
haI : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aI
hI : ∀ b ∈ I, IsInteger R₁ (aI • b)
aJ : R₁
haJ : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aJ
hJ : ∀ b ∈ J, IsInteger R₁ (aJ • b)
h : J ≠ 0
⊢ 0 < J

Tactic:
simpa only using bot_lt_iff_ne_bot.mpr h

Premises used: Iff.mpr, bot_lt_iff_ne_bot
-- 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 : Submodule R₁ K
aI : R₁
haI : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aI
hI : ∀ b ∈ I, IsInteger R₁ (aI • b)
aJ : R₁
haJ : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aJ
hJ : ∀ b ∈ J, IsInteger R₁ (aJ • b)
h : J ≠ 0
obtain : ∀ (y : K) (mem_J : y ∈ J) (notMem_zero : y ∉ 0), IsFractional R₁⁰ (I / J)
⊢ IsFractional R₁⁰ (I / J)

Tactic:
obtain ⟨y, mem_J, notMem_zero⟩ :=
      SetLike.exists_of_lt (show 0 < J by simpa only using bot_lt_iff_ne_bot.mpr h)

Premises used: SetLike.exists_of_lt
-- 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 : Submodule R₁ K
aI : R₁
haI : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aI
hI : ∀ b ∈ I, IsInteger R₁ (aI • b)
aJ : R₁
haJ : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aJ
hJ : ∀ b ∈ J, IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
notMem_zero : y ∉ 0
obtain : ∀ (y' : R₁) (hy' : (algebraMap R₁ K : (a : R₁) → K) y' = aJ • y), IsFractional R₁⁰ (I / J)
⊢ IsFractional R₁⁰ (I / J)

Tactic:
obtain ⟨y', hy'⟩ := hJ y mem_J
-- 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 : Submodule R₁ K
aI : R₁
haI : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aI
hI : ∀ b ∈ I, IsInteger R₁ (aI • b)
aJ : R₁
haJ : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aJ
hJ : ∀ b ∈ J, IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
notMem_zero : y ∉ 0
y' : R₁
hy' : (algebraMap R₁ K : (a : R₁) → K) y' = aJ • y
h₁ : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) (aI * y') ∧ ∀ b ∈ I / J, IsInteger R₁ ((aI * y') • b)
⊢ IsFractional R₁⁰ (I / J)

Tactic:
use aI * y'
-- 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 : Submodule R₁ K
aI : R₁
haI : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aI
hI : ∀ b ∈ I, IsInteger R₁ (aI • b)
aJ : R₁
haJ : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aJ
hJ : ∀ b ∈ J, IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
notMem_zero : y ∉ 0
y' : R₁
hy' : (algebraMap R₁ K : (a : R₁) → K) y' = aJ • y
h₁ : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) (aI * y')
h₂ : ∀ b ∈ I / J, IsInteger R₁ ((aI * y') • b)
⊢ Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) (aI * y') ∧ ∀ b ∈ I / J, IsInteger R₁ ((aI * y') • b)

Tactic:
constructor
-- 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 : Submodule R₁ K
aI : R₁
haI : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aI
hI : ∀ b ∈ I, IsInteger R₁ (aI • b)
aJ : R₁
haJ : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aJ
hJ : ∀ b ∈ J, IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
notMem_zero : y ∉ 0
y' : R₁
hy' : (algebraMap R₁ K : (a : R₁) → K) y' = aJ • y
apply : y' ≠ 0
⊢ Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) (aI * y')

Tactic:
apply (nonZeroDivisors R₁).mul_mem haI (mem_nonZeroDivisors_iff_ne_zero.mpr _)

Premises used: Iff.mpr, Submonoid.mul_mem, nonZeroDivisors, mem_nonZeroDivisors_iff_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 : Submodule R₁ K
aI : R₁
haI : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aI
hI : ∀ b ∈ I, IsInteger R₁ (aI • b)
aJ : R₁
haJ : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aJ
hJ : ∀ b ∈ J, IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
notMem_zero : y ∉ 0
y' : R₁
hy' : (algebraMap R₁ K : (a : R₁) → K) y' = aJ • y
y'_eq_zero : y' = 0
rw : aJ • y = 0
rw₁ : Eq.{u_4 + 1} (α := K) ((algebraMap R₁ K : (a : R₁) → K) y' : K) (0 : K)
rw₂ : Eq.{u_4 + 1} (α := K) ((algebraMap R₁ K : (a : R₁) → K) 0 : K) (0 : K)
rw₃ rw₄ : Eq.{u_4 + 1} (α := K) 0 0
⊢ HMul.hMul (α := K) ((algebraMap R₁ K : (a : R₁) → K) aJ : K) y = 0

Tactic:
rw [← Algebra.smul_def, ← hy', y'_eq_zero, map_zero]

Premises used: map_zero, 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 : Submodule R₁ K
aI : R₁
haI : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aI
hI : ∀ b ∈ I, IsInteger R₁ (aI • b)
aJ : R₁
haJ : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aJ
hJ : ∀ b ∈ J, IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
notMem_zero : y ∉ 0
y' : R₁
hy' : (algebraMap R₁ K : (a : R₁) → K) y' = aJ • y
y'_eq_zero : y' = 0
⊢ HMul.hMul (α := K) ((algebraMap R₁ K : (a : R₁) → K) aJ : K) y = 0

Tactic:
have : algebraMap R₁ K aJ * y = 0 := by
        rw [← Algebra.smul_def, ← hy', y'_eq_zero, 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₁
I J : Submodule R₁ K
aI : R₁
haI : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aI
hI : ∀ b ∈ I, IsInteger R₁ (aI • b)
aJ : R₁
haJ : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aJ
hJ : ∀ b ∈ J, IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
notMem_zero : y ∉ 0
y' : R₁
hy' : (algebraMap R₁ K : (a : R₁) → K) y' = aJ • y
y'_eq_zero : y' = 0
this : HMul.hMul (α := K) ((algebraMap R₁ K : (a : R₁) → K) aJ : K) y = 0
⊢ y = 0

Tactic:
have y_zero :=
        (mul_eq_zero.mp this).resolve_left
          (mt ((injective_iff_map_eq_zero (algebraMap R₁ K)).1 (IsFractionRing.injective _ _) _)
            (mem_nonZeroDivisors_iff_ne_zero.mp haJ))
-- 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 : Submodule R₁ K
aI : R₁
haI : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aI
hI : ∀ b ∈ I, IsInteger R₁ (aI • b)
aJ : R₁
haJ : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aJ
hJ : ∀ b ∈ J, IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
notMem_zero : y ∉ 0
y' : R₁
hy' : (algebraMap R₁ K : (a : R₁) → K) y' = aJ • y
y'_eq_zero : y' = 0
this : HMul.hMul (α := K) ((algebraMap R₁ K : (a : R₁) → K) aJ : K) y = 0
y_zero : y = 0
apply : Membership.mem (γ := Submodule R₁ K) 0 y
⊢ False

Tactic:
apply notMem_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 : Submodule R₁ K
aI : R₁
haI : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aI
hI : ∀ b ∈ I, IsInteger R₁ (aI • b)
aJ : R₁
haJ : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aJ
hJ : ∀ b ∈ J, IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
notMem_zero : y ∉ 0
y' : R₁
hy' : (algebraMap R₁ K : (a : R₁) → K) y' = aJ • y
y'_eq_zero : y' = 0
this : HMul.hMul (α := K) ((algebraMap R₁ K : (a : R₁) → K) aJ : K) y = 0
y_zero : y = 0
⊢ Membership.mem (γ := Submodule R₁ K) 0 y

Tactic:
simpa
-- 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 : Submodule R₁ K
aI : R₁
haI : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aI
hI : ∀ b ∈ I, IsInteger R₁ (aI • b)
aJ : R₁
haJ : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aJ
hJ : ∀ b ∈ J, IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
notMem_zero : y ∉ 0
y' : R₁
hy' : (algebraMap R₁ K : (a : R₁) → K) y' = aJ • y
b : K
hb : b ∈ I / J
⊢ IsInteger R₁ (aI • (b * aJ • y))

Tactic:
hI _ (hb _ (Submodule.smul_mem _ aJ mem_J))

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 J : Submodule R₁ K
aI : R₁
haI : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aI
hI : ∀ b ∈ I, IsInteger R₁ (aI • b)
aJ : R₁
haJ : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aJ
hJ : ∀ b ∈ J, IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
notMem_zero : y ∉ 0
y' : R₁
hy' : (algebraMap R₁ K : (a : R₁) → K) y' = aJ • y
b : K
hb : b ∈ I / J
h₁ : (aI * y') • b = aI • (b * aJ • y)
⊢ IsInteger R₁ ((aI * y') • b)

Tactic:
convert! hI _ (hb _ (Submodule.smul_mem _ aJ mem_J)) 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 J : Submodule R₁ K
aI : R₁
haI : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aI
hI : ∀ b ∈ I, IsInteger R₁ (aI • b)
aJ : R₁
haJ : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aJ
hJ : ∀ b ∈ J, IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
notMem_zero : y ∉ 0
y' : R₁
hy' : (algebraMap R₁ K : (a : R₁) → K) y' = aJ • y
b : K
hb : b ∈ I / J
h₁ : (aI * y') • b = aI • HMul.hMul (β := K) b ((algebraMap R₁ K : (a : R₁) → K) y' : K)
h₂ : (aI * y') • b = aI • HMul.hMul (α := K) ((algebraMap R₁ K : (a : R₁) → K) y' : K) b
h₃ : (aI * y') • b = aI • y' • b
h₄ h₅ : aI • y' • b = aI • y' • b
⊢ (aI * y') • b = aI • (b * aJ • y)

Tactic:
rw [← hy', mul_comm b, ← Algebra.smul_def, mul_smul]

Premises used: mul_comm, Algebra.smul_def, SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
I J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
h : J ≠ 0
⊢ IsFractional R₁⁰ ((↑I : Submodule R₁ K) / (↑J : Submodule R₁ K))

Tactic:
I.isFractional.div_of_nonzero J.isFractional fun H =>
    h <| coeToSubmodule_injective <| H.trans coe_zero.symm

Premises used: IsFractional.div_of_nonzero, FractionalIdeal.isFractional, FractionalIdeal.coeToSubmodule_injective, Eq.symm, Eq.trans, FractionalIdeal.coe_zero
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
⊢ I / 0 = 0

Tactic:
dif_pos rfl

Premises used: dif_pos, 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 : J ≠ 0
⊢ I / J =
    Subtype.mk (p := fun (I : Submodule R₁ K) ↦ IsFractional R₁⁰ I) ((↑I : Submodule R₁ K) / (↑J : Submodule R₁ K)) ⋯

Tactic:
dif_neg h

Premises used: dif_neg
-- 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
hJ : J ≠ 0
⊢ (↑(I / J) : Submodule R₁ K) = (↑I : Submodule R₁ K) / (↑J : Submodule R₁ K)

Tactic:
congr_arg _ (dif_neg hJ)

Premises used: dif_neg, congr_arg, FractionalIdeal.coeToSubmodule
-- 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 : J ≠ 0
x : K
rw :
  x ∈
      Subtype.mk (p := fun (I : Submodule R₁ K) ↦ IsFractional R₁⁰ I) ((↑I : Submodule R₁ K) / (↑J : Submodule R₁ K))
        ⋯ ↔
    ∀ y ∈ J, x * y ∈ I
⊢ x ∈ I / J ↔ ∀ y ∈ J, x * y ∈ I

Tactic:
rw [div_of_ne_zero h]

Premises used: FractionalIdeal.div_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 : J ≠ 0
x : K
⊢ x ∈
      Subtype.mk (p := fun (I : Submodule R₁ K) ↦ IsFractional R₁⁰ I) ((↑I : Submodule R₁ K) / (↑J : Submodule R₁ K))
        ⋯ ↔
    ∀ y ∈ J, x * y ∈ I

Tactic:
Submodule.mem_div_iff_forall_mul_mem

Premises used: Set.Mem, Submodule.mem_div_iff_forall_mul_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 J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
h : J ≠ 0
x : K
⊢ x ∈
      Subtype.mk (p := fun (I : Submodule R₁ K) ↦ IsFractional R₁⁰ I) ((↑I : Submodule R₁ K) / (↑J : Submodule R₁ K))
        ⋯ ↔
    ∀ y ∈ J, x * y ∈ I

Tactic:
exact Submodule.mem_div_iff_forall_mul_mem

Premises used: Submodule.mem_div_iff_forall_mul_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
pos : ∀ (hI : I = 0), I * (1 / I) ≤ 1
neg : ∀ (hI : ¬I = 0), I * (1 / I) ≤ 1
⊢ I * (1 / I) ≤ 1

Tactic:
by_cases hI : I = 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₁
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
hI : I = 0
pos : LE.le.{u_4} (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 0 1
⊢ I * (1 / I) ≤ 1

Tactic:
rw [hI, div_zero, mul_zero]

Premises used: MulZeroClass.mul_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₁
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
hI : I = 0
⊢ LE.le.{u_4} (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 0 1

Tactic:
zero_le 1

Premises used: Set.Mem, FractionalIdeal.zero_le, 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
hI : I = 0
⊢ LE.le.{u_4} (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 0 1

Tactic:
exact zero_le 1

Premises used: FractionalIdeal.zero_le, 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
hI : ¬I = 0
neg : (↑I : Submodule R₁ K) * (1 / (↑I : Submodule R₁ K)) ≤ 1
⊢ I * (1 / I) ≤ 1

Tactic:
rw [← coe_le_coe, coe_mul, coe_div hI, coe_one]

Premises used: FractionalIdeal.coe_le_coe, FractionalIdeal.coe_one, FractionalIdeal.coe_mul, 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₁
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
hI : ¬I = 0
⊢ (↑I : Submodule R₁ K) * (1 / (↑I : Submodule R₁ K)) ≤ 1

Tactic:
apply Submodule.mul_one_div_le_one

Premises used: Submodule.mul_one_div_le_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
inst_4 : IsDomain R₁
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
hI : I ≤ 1
pos : ∀ (hI_nz : I = 0), I ≤ I * (1 / I)
neg : ∀ (hI_nz : ¬I = 0), I ≤ I * (1 / I)
⊢ I ≤ I * (1 / I)

Tactic:
by_cases hI_nz : I = 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₁
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
hI : I ≤ 1
hI_nz : I = 0
pos : 0 ≤ 0 * (1 / 0)
pos₁ : 0 ≤ HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 0 0
pos₂ pos₃ : LE.le.{u_4} (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 0 0
⊢ I ≤ I * (1 / I)

Tactic:
rw [hI_nz, div_zero, mul_zero]

Premises used: MulZeroClass.mul_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₁
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
hI : I ≤ 1
hI_nz : ¬I = 0
neg : (↑I : Submodule R₁ K) ≤ (↑I : Submodule R₁ K) * (1 / (↑I : Submodule R₁ K))
⊢ I ≤ I * (1 / I)

Tactic:
rw [← coe_le_coe, coe_mul, coe_div hI_nz, coe_one]

Premises used: FractionalIdeal.coe_le_coe, FractionalIdeal.coe_one, FractionalIdeal.coe_mul, 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₁
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
hI : I ≤ 1
hI_nz : ¬I = 0
⊢ (↑I : Submodule R₁ K) ≤ 1

Tactic:
rw [← coe_le_coe, coe_one] at hI

Premises used: FractionalIdeal.coe_le_coe, FractionalIdeal.coe_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
inst_4 : IsDomain R₁
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
hI : I ≤ 1
hI_nz : ¬I = 0
hI₁ : (↑I : Submodule R₁ K) ≤ 1
⊢ ¬I = 0

Tactic:
rw [← coe_le_coe, coe_one] at hI

Premises used: FractionalIdeal.coe_le_coe, FractionalIdeal.coe_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
inst_4 : IsDomain R₁
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
hI : (↑I : Submodule R₁ K) ≤ 1
hI_nz : ¬I = 0
⊢ (↑I : Submodule R₁ K) ≤ (↑I : Submodule R₁ K) * (1 / (↑I : Submodule R₁ K))

Tactic:
Submodule.le_self_mul_one_div hI

Premises used: Submodule.le_self_mul_one_div, Set.Mem, setOf
-- 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
hI : (↑I : Submodule R₁ K) ≤ 1
hI_nz : ¬I = 0
⊢ (↑I : Submodule R₁ K) ≤ (↑I : Submodule R₁ K) * (1 / (↑I : Submodule R₁ K))

Tactic:
exact Submodule.le_self_mul_one_div hI

Premises used: Submodule.le_self_mul_one_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₁
I J J' : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
hJ' : J' ≠ 0
⊢ I ≤ J / J' ↔ ∀ x ∈ I, ∀ y ∈ J', x * y ∈ J

Tactic:
⟨fun h _ hx => (mem_div_iff_of_ne_zero hJ').mp (h hx), fun h x hx =>
    (mem_div_iff_of_ne_zero hJ').mpr (h x hx)⟩

Premises used: Iff.mpr, Iff.intro, 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 J' : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
hJ' : J' ≠ 0
rw :
  I ≤
      Subtype.mk (p := fun (I : Submodule R₁ K) ↦ IsFractional R₁⁰ I) ((↑J : Submodule R₁ K) / (↑J' : Submodule R₁ K))
        ⋯ ↔
    (↑I : Submodule R₁ K) * (↑J' : Submodule R₁ K) ≤ (↑J : Submodule R₁ K)
⊢ I ≤ J / J' ↔ I * J' ≤ J

Tactic:
rw [div_of_ne_zero hJ', ← coe_le_coe (I := I * J') (J := J), coe_mul]

Premises used: FractionalIdeal.coe_le_coe, FractionalIdeal.div_of_ne_zero, FractionalIdeal.coe_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 J' : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
hJ' : J' ≠ 0
⊢ I ≤
      Subtype.mk (p := fun (I : Submodule R₁ K) ↦ IsFractional R₁⁰ I) ((↑J : Submodule R₁ K) / (↑J' : Submodule R₁ K))
        ⋯ ↔
    (↑I : Submodule R₁ K) * (↑J' : Submodule R₁ K) ≤ (↑J : Submodule R₁ K)

Tactic:
Submodule.le_div_iff_mul_le

Premises used: Set.Mem, Submodule.le_div_iff_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 J' : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
hJ' : J' ≠ 0
⊢ I ≤
      Subtype.mk (p := fun (I : Submodule R₁ K) ↦ IsFractional R₁⁰ I) ((↑J : Submodule R₁ K) / (↑J' : Submodule R₁ K))
        ⋯ ↔
    (↑I : Submodule R₁ K) * (↑J' : Submodule R₁ K) ≤ (↑J : Submodule R₁ K)

Tactic:
exact Submodule.le_div_iff_mul_le

Premises used: Submodule.le_div_iff_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 : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
rw :
  Subtype.mk (p := fun (I : Submodule R₁ K) ↦ IsFractional R₁⁰ I) ((↑I : Submodule R₁ K) / (↑1 : Submodule R₁ K)) ⋯ = I
⊢ I / 1 = I

Tactic:
rw [div_of_ne_zero (one_ne_zero' (FractionalIdeal R₁⁰ K))]

Premises used: one_ne_zero', FractionalIdeal.div_of_ne_zero, nonZeroDivisors, FractionalIdeal
-- 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
a :
  ∀ (x : K),
    x ∈
        Subtype.mk (p := fun (I : Submodule R₁ K) ↦ IsFractional R₁⁰ I) ((↑I : Submodule R₁ K) / (↑1 : Submodule R₁ K))
          ⋯ ↔
      x ∈ I
⊢ Subtype.mk (p := fun (I : Submodule R₁ K) ↦ IsFractional R₁⁰ I) ((↑I : Submodule R₁ K) / (↑1 : Submodule R₁ K)) ⋯ = I

Tactic:
ext
-- 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
a :
  x ∈
      Subtype.mk (p := fun (I : Submodule R₁ K) ↦ IsFractional R₁⁰ I) ((↑I : Submodule R₁ K) / (↑1 : Submodule R₁ K))
        ⋯ →
    x ∈ I
a₁ :
  x ∈ I →
    x ∈
      Subtype.mk (p := fun (I : Submodule R₁ K) ↦ IsFractional R₁⁰ I) ((↑I : Submodule R₁ K) / (↑1 : Submodule R₁ K)) ⋯
⊢ x ∈
      Subtype.mk (p := fun (I : Submodule R₁ K) ↦ IsFractional R₁⁰ I) ((↑I : Submodule R₁ K) / (↑1 : Submodule R₁ K))
        ⋯ ↔
    x ∈ I

Tactic:
constructor