awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J K : Ideal R
h : I ≤ J
⊢ I * K ≤ J * K

Tactic:
Submodule.smul_mono_left h

Premises used: Set.Mem, Submodule.smul_mono_left
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J K : Ideal R
h : J ≤ K
⊢ I * J ≤ I * K

Tactic:
smul_mono_right I h

Premises used: Set.Mem, smul_mono_right
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J K : Ideal R
⊢ I * (J ⊔ K) = I * J ⊔ I * K

Tactic:
Submodule.smul_sup I J K

Premises used: Set.Mem, setOf, Submodule.smul_sup
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J K : Ideal R
⊢ (I ⊔ J) * K = I * K ⊔ J * K

Tactic:
Submodule.sup_smul I J K

Premises used: Set.Mem, setOf, Submodule.sup_smul
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I : Ideal R
ι : Sort u_1
J : ι → Ideal R
⊢ I * ⨆ (i : ι), J i = ⨆ (i : ι), I * J i

Tactic:
Submodule.smul_iSup

Premises used: Submodule.smul_iSup
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
ι : Sort u_1
J : ι → Ideal R
I : Ideal R
⊢ (⨆ (i : ι), J i) * I = ⨆ (i : ι), J i * I

Tactic:
Submodule.iSup_smul

Premises used: Set.Mem, setOf, Submodule.iSup_smul
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I : Ideal R
m n : ℕ
h : m ≤ n
zero : ∀ (h : 0 ≤ n), I ^ n ≤ HPow.hPow (β := ℕ) I 0
succ : ∀ (m : ℕ) (h : m + 1 ≤ n), I ^ n ≤ I ^ (m + 1)
⊢ I ^ n ≤ I ^ m

Tactic:
obtain _ | m := m
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I : Ideal R
n : ℕ
h : 0 ≤ n
zero : I ^ n ≤ ⊤
⊢ I ^ n ≤ HPow.hPow (β := ℕ) I 0

Tactic:
rw [Submodule.pow_zero, one_eq_top]

Premises used: Submodule.pow_zero, Ideal.one_eq_top
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I : Ideal R
n : ℕ
h : 0 ≤ n
⊢ I ^ n ≤ ⊤

Tactic:
le_top

Premises used: Set.Mem, le_top
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I : Ideal R
n : ℕ
h : 0 ≤ n
⊢ I ^ n ≤ ⊤

Tactic:
exact le_top

Premises used: le_top
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I : Ideal R
n m : ℕ
h : m + 1 ≤ n
succ : ∀ (n : ℕ) (h : m + 1 ≤ m + 1 + n), I ^ (m + 1 + n) ≤ I ^ (m + 1)
⊢ I ^ n ≤ I ^ (m + 1)

Tactic:
obtain ⟨n, rfl⟩ := Nat.exists_eq_add_of_le h

Premises used: Nat.exists_eq_add_of_le, rfl
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I : Ideal R
m n : ℕ
h : m + 1 ≤ m + 1 + n
succ : I ^ n * I ^ (m + 1) ≤ I ^ (m + 1)
⊢ I ^ (m + 1 + n) ≤ I ^ (m + 1)

Tactic:
rw [add_comm, Submodule.pow_add _ m.add_one_ne_zero]

Premises used: Submodule.pow_add, Nat.add_one_ne_zero, add_comm
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I : Ideal R
m n : ℕ
h : m + 1 ≤ m + 1 + n
⊢ I ^ n * I ^ (m + 1) ≤ I ^ (m + 1)

Tactic:
mul_le_left

Premises used: Set.Mem, Ideal.mul_le_left
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I : Ideal R
m n : ℕ
h : m + 1 ≤ m + 1 + n
⊢ I ^ n * I ^ (m + 1) ≤ I ^ (m + 1)

Tactic:
exact mul_le_left

Premises used: Ideal.mul_le_left
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I : Ideal R
n : ℕ
hn : n ≠ 0
⊢ I ^ n ≤ I

Tactic:
calc
    I ^ n ≤ I ^ 1 := pow_le_pow_right (Nat.pos_of_ne_zero hn)
    _ = I := Submodule.pow_one _

Premises used: Trans.trans, Ideal.pow_le_pow_right, Nat.pos_of_ne_zero, Submodule.pow_one
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J : Ideal R
e : I ≤ J
zero : 1 ≤ HPow.hPow (β := ℕ) J 0
zero₁ zero₂ : LE.le.{u} (α := Ideal R) 1 1
⊢ HPow.hPow (β := ℕ) I 0 ≤ HPow.hPow (β := ℕ) J 0

Tactic:
rw [Submodule.pow_zero, Submodule.pow_zero]

Premises used: Submodule.pow_zero
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J : Ideal R
e : I ≤ J
n : ℕ
hn : I ^ n ≤ J ^ n
succ : I ^ n * I ≤ J ^ n * J
⊢ I ^ (n + 1) ≤ J ^ (n + 1)

Tactic:
rw [Submodule.pow_succ, Submodule.pow_succ]

Premises used: Submodule.pow_succ
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J : Ideal R
e : I ≤ J
n : ℕ
hn : I ^ n ≤ J ^ n
⊢ I ^ n * I ≤ J ^ n * J

Tactic:
Ideal.mul_mono hn e

Premises used: Set.Mem, Ideal.mul_mono
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J : Ideal R
e : I ≤ J
n : ℕ
hn : I ^ n ≤ J ^ n
⊢ I ^ n * I ≤ J ^ n * J

Tactic:
exact Ideal.mul_mono hn e

Premises used: Ideal.mul_mono
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J : Ideal R
e : I ≤ J
n : ℕ
zero : HPow.hPow (β := ℕ) I 0 ≤ HPow.hPow (β := ℕ) J 0
succ : ∀ (n : ℕ) (hn : I ^ n ≤ J ^ n), I ^ (n + 1) ≤ J ^ (n + 1)
⊢ I ^ n ≤ J ^ n

Tactic:
induction n with
  | zero => rw [Submodule.pow_zero, Submodule.pow_zero]
  | succ _ hn =>
    rw [Submodule.pow_succ, Submodule.pow_succ]
    exact Ideal.mul_mono hn e

Premises used: Submodule.pow_zero, Submodule.pow_succ
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J K L : Ideal R
inst_1 : J.IsTwoSided
a b : R
ha : a ∈ I * J
i : R
hi : i ∈ I
j : R
hj : j ∈ J
rw : i * (j * b) ∈ I * J
⊢ i * j * b ∈ I * J

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J K L : Ideal R
inst_1 : J.IsTwoSided
a b : R
ha : a ∈ I * J
i : R
hi : i ∈ I
j : R
hj : j ∈ J
⊢ i * (j * b) ∈ I * J

Tactic:
mul_mem_mul hi (mul_mem_right _ _ hj)

Premises used: Set.Mem, Ideal.mul_mem_mul, Ideal.mul_mem_right
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J K L : Ideal R
inst_1 : J.IsTwoSided
a b : R
ha : a ∈ I * J
i : R
hi : i ∈ I
j : R
hj : j ∈ J
⊢ i * (j * b) ∈ I * J

Tactic:
exact mul_mem_mul hi (mul_mem_right _ _ hj)

Premises used: Ideal.mul_mem_mul, Ideal.mul_mem_right
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J K L : Ideal R
inst_1 : J.IsTwoSided
a b : R
ha : a ∈ I * J
x y : R
hx : x * b ∈ I * J
hy : y * b ∈ I * J
rw : x * b + y * b ∈ I * J
⊢ (x + y) * b ∈ I * J

Tactic:
rw [right_distrib]

Premises used: right_distrib
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J K L : Ideal R
inst_1 : J.IsTwoSided
a b : R
ha : a ∈ I * J
x y : R
hx : x * b ∈ I * J
hy : y * b ∈ I * J
⊢ x * b + y * b ∈ I * J

Tactic:
add_mem hx hy

Premises used: AddMemClass.add_mem
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J K L : Ideal R
inst_1 : J.IsTwoSided
a b : R
ha : a ∈ I * J
x y : R
hx : x * b ∈ I * J
hy : y * b ∈ I * J
⊢ x * b + y * b ∈ I * J

Tactic:
exact add_mem hx hy

Premises used: AddMemClass.add_mem
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J K L : Ideal R
inst_1 : I.IsTwoSided
m n : ℕ
rw : IsTwoSided.{u} (α := R) ⊤
⊢ (I ^ Nat.zero).IsTwoSided

Tactic:
rw [Submodule.pow_zero, one_eq_top]

Premises used: Submodule.pow_zero, Ideal.one_eq_top
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J K L : Ideal R
inst_1 : I.IsTwoSided
m n : ℕ
⊢ IsTwoSided.{u} (α := R) ⊤

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J K L : Ideal R
inst_1 : I.IsTwoSided
m n x : ℕ
h : (I ^ x).IsTwoSided
rw : IsTwoSided (I ^ x * I)
⊢ (I ^ x.succ).IsTwoSided

Tactic:
rw [Submodule.pow_succ]

Premises used: Submodule.pow_succ
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J K L : Ideal R
inst_1 : I.IsTwoSided
m n x : ℕ
h : (I ^ x).IsTwoSided
⊢ IsTwoSided (I ^ x * I)

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I : Ideal R
inst_1 : I.IsTwoSided
⊢ I * 1 = I

Tactic:
mul_le_right.antisymm
    fun i hi ↦ mul_one i ▸ mul_mem_mul hi (one_eq_top (R := R) ▸ Submodule.mem_top)

Premises used: Ideal.mul_le_right, Ideal.one_eq_top, LE.le.antisymm, Eq.rec, Ideal.mul_mem_mul, mul_one, Eq.symm, Submodule.mem_top
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I : Ideal R
inst_1 : I.IsTwoSided
m n : ℕ
inl : I ^ (m + 0) = I ^ m * HPow.hPow (β := ℕ) I 0
inr : ∀ (h : n ≠ 0), I ^ (m + n) = I ^ m * I ^ n
⊢ I ^ (m + n) = I ^ m * I ^ n

Tactic:
obtain rfl | h := eq_or_ne n 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I : Ideal R
inst_1 : I.IsTwoSided
m : ℕ
inl : I ^ m = I ^ m * HPow.hPow (β := ℕ) I 0
inl₁ : I ^ m = I ^ m * 1
inl₂ inl₃ : I ^ m = I ^ m
⊢ I ^ (m + 0) = I ^ m * HPow.hPow (β := ℕ) I 0

Tactic:
rw [add_zero, Submodule.pow_zero, IsTwoSided.mul_one]

Premises used: Submodule.pow_zero, Ideal.IsTwoSided.mul_one, add_zero
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I : Ideal R
inst_1 : I.IsTwoSided
m n : ℕ
h : n ≠ 0
⊢ I ^ (m + n) = I ^ m * I ^ n

Tactic:
Submodule.pow_add _ h

Premises used: Set.Mem, Submodule.pow_add
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I : Ideal R
inst_1 : I.IsTwoSided
m n : ℕ
h : n ≠ 0
⊢ I ^ (m + n) = I ^ m * I ^ n

Tactic:
exact Submodule.pow_add _ h

Premises used: Submodule.pow_add
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I : Ideal R
inst_1 : I.IsTwoSided
n : ℕ
rw : I ^ (1 + n) = I * I ^ n
rw₁ : HPow.hPow (β := ℕ) I 1 * I ^ n = I * I ^ n
rw₂ rw₃ : I * I ^ n = I * I ^ n
⊢ I ^ (n + 1) = I * I ^ n

Tactic:
rw [add_comm, IsTwoSided.pow_add, Submodule.pow_one]

Premises used: add_comm, Ideal.IsTwoSided.pow_add, Submodule.pow_one
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J : Ideal R
inst_1 : NoZeroDivisors R
⊢ I * J = ⊥ ↔ I = ⊥ ∨ J = ⊥

Tactic:
Submodule.mul_eq_bot

Premises used: Submodule.mul_eq_bot
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I_1 J K L : Ideal R
S : Type u_1
A : Type u_2
inst_1 : Semiring S
inst_2 : SMul R S
inst_3 : AddCommMonoid A
inst_4 : Module R A
inst_5 : Module S A
inst_6 : IsScalarTower R S A
inst_7 : IsTorsionFree R A
I : Submodule S A
⊢ IsTorsionFree.{u, u_2} R ↥I

Tactic:
(I.restrictScalars R).instIsTorsionFree

Premises used: Set.Mem, Submodule.restrictScalars, Submodule.instIsTorsionFree
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
S T : Set R
inst_1 : IsTwoSided (span S)
⊢ HMul.hMul (α := Ideal R) (span S) (span T) = span (S * T)

Tactic:
Submodule.span_smul_span S T

Premises used: Submodule.span_smul_span
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
S T : Set R
inst_1 : IsTwoSided (span S)
⊢ ∀ (x : R), x ∈ S * T ↔ x ∈ S * T

Tactic:
simp [Set.mem_mul, eq_comm]

Premises used: eq_comm, Set.mem_mul
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
r s : R
inst_1 : IsTwoSided (α := R) (span {r})
rw : Eq (α := Ideal R) (span (HMul.hMul (α := Set R) {r} {s})) (span {r * s})
rw₁ rw₂ : Eq (α := Ideal R) (span {r * s}) (span {r * s})
⊢ HMul.hMul (α := Ideal R) (span {r}) (span {s}) = span {r * s}

Tactic:
rw [span_mul_span', Set.singleton_mul_singleton]

Premises used: Ideal.span_mul_span', Set.singleton_mul_singleton
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
s : R
inst_1 : IsTwoSided (α := R) (span {s})
⊢ HPow.hPow (α := Ideal R) (β := ℕ) (span {s}) 0 = span {HPow.hPow (β := ℕ) s 0}

Tactic:
simp [Submodule.pow_zero, Set.singleton_one]

Premises used: Submodule.pow_zero, Set.singleton_one
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
s : R
inst_1 : IsTwoSided (α := R) (span {s})
n : ℕ
ih : HPow.hPow (α := Ideal R) (span {s}) n = span {s ^ n}
succ :
  ∀ (ih : HPow.hPow (α := Ideal R) (β := ℕ) (span {s}) 0 = span {HPow.hPow (β := ℕ) s 0}),
    HPow.hPow (α := Ideal R) (span {s}) (HAdd.hAdd (α := ℕ) 0 1) = span {s ^ HAdd.hAdd (α := ℕ) 0 1}
succ₁ : ∀ (ne : n ≠ 0), HPow.hPow (α := Ideal R) (span {s}) (n + 1) = span {s ^ (n + 1)}
⊢ HPow.hPow (α := Ideal R) (span {s}) (n + 1) = span {s ^ (n + 1)}

Tactic:
obtain rfl | ne := eq_or_ne n 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
s : R
inst_1 : IsTwoSided (α := R) (span {s})
ih : HPow.hPow (α := Ideal R) (β := ℕ) (span {s}) 0 = span {HPow.hPow (β := ℕ) s 0}
⊢ HPow.hPow (α := Ideal R) (span {s}) (HAdd.hAdd (α := ℕ) 0 1) = span {s ^ HAdd.hAdd (α := ℕ) 0 1}

Tactic:
simp [Submodule.pow_one]

Premises used: Submodule.pow_one
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
s : R
inst_1 : IsTwoSided (α := R) (span {s})
n : ℕ
ih : HPow.hPow (α := Ideal R) (span {s}) n = span {s ^ n}
ne : n ≠ 0
⊢ HPow.hPow (α := Ideal R) (span {s}) (n + 1) = span {s ^ (n + 1)}

Tactic:
simp only [Submodule.pow_succ' _ ne, pow_succ', ih, span_singleton_mul_span_singleton]

Premises used: Ideal.span_singleton_mul_span_singleton, Submodule.pow_succ', pow_succ'
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
s : R
inst_1 : IsTwoSided (α := R) (span {s})
n : ℕ
zero : HPow.hPow (α := Ideal R) (β := ℕ) (span {s}) 0 = span {HPow.hPow (β := ℕ) s 0}
succ :
  ∀ (n : ℕ) (ih : HPow.hPow (α := Ideal R) (span {s}) n = span {s ^ n}),
    HPow.hPow (α := Ideal R) (span {s}) (n + 1) = span {s ^ (n + 1)}
⊢ HPow.hPow (α := Ideal R) (span {s}) n = span {s ^ n}

Tactic:
induction n with
  | zero => simp [Submodule.pow_zero, Set.singleton_one]
  | succ n ih =>
    obtain rfl | ne := eq_or_ne n 0; · simp [Submodule.pow_one]
    simp only [Submodule.pow_succ' _ ne, pow_succ', ih, span_singleton_mul_span_singleton]

Premises used: Submodule.pow_zero, Ideal.span_singleton_mul_span_singleton, eq_or_ne, OfNat.ofNat, pow_succ', rfl, Set.singleton_one, Submodule.pow_one
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
x y : R
I : Ideal R
inst_1 : I.IsTwoSided
⊢ x ∈ I * span {y} ↔ ∃ z ∈ I, z * y = x

Tactic:
Submodule.mem_smul_span_singleton

Premises used: Submodule.mem_smul_span_singleton, Set.Mem
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J : Ideal R
inst_1 : IsDomain R
inst_2 : I.IsTwoSided
inst_3 : J.IsTwoSided
x : R
hx : x ≠ 0
⊢ I * span {x} ≤ J * span {x} ↔ I ≤ J

Tactic:
simp [SetLike.le_def, mem_mul_span_singleton, hx]

Premises used: SetLike.le_def, Ideal.mem_mul_span_singleton
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J : Ideal R
inst_1 : IsDomain R
inst_2 : I.IsTwoSided
inst_3 : J.IsTwoSided
x : R
hx : x ≠ 0
⊢ I * span {x} = J * span {x} ↔ I = J

Tactic:
simp only [le_antisymm_iff, span_singleton_mul_left_mono hx]

Premises used: Ideal.span_singleton_mul_left_mono, le_antisymm_iff
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J : Ideal R
inst_1 : I.IsTwoSided
⊢ I * J ≤ I ⊓ J

Tactic:
mul_le.2 fun r hri s hsj => ⟨I.mul_mem_right s hri, J.mul_mem_left r hsj⟩

Premises used: Iff.mpr, Ideal.mul_le, Ideal.mul_mem_right, And.intro, Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
I J : Ideal R
inst_2 : I.IsTwoSided
inst_3 : J.IsTwoSided
hI : I ≠ ⊥
hJ : J ≠ ⊥
grw : ¬(I = ⊥ ∨ J = ⊥)
⊢ I ⊓ J ≠ ⊥

Tactic:
grw [← bot_lt_iff_ne_bot, ← mul_le_inf, bot_lt_iff_ne_bot, Ne, mul_eq_bot]

Premises used: bot_lt_iff_ne_bot, Ne, Ideal.mul_le_inf, Ideal.mul_eq_bot
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
I J : Ideal R
inst_2 : I.IsTwoSided
inst_3 : J.IsTwoSided
hI : I ≠ ⊥
hJ : J ≠ ⊥
⊢ ¬(I = ⊥ ∨ J = ⊥)

Tactic:
not_or_intro hI hJ

Premises used: not_or_intro
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
I J : Ideal R
inst_2 : I.IsTwoSided
inst_3 : J.IsTwoSided
hI : I ≠ ⊥
hJ : J ≠ ⊥
⊢ ¬(I = ⊥ ∨ J = ⊥)

Tactic:
exact not_or_intro hI hJ

Premises used: not_or_intro
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J K : Ideal R
inst_1 : I.IsTwoSided
h : I ⊔ J = ⊤
i : R
hi : i ∈ I ⊔ K
rw : ∀ (h : 1 ∈ I ⊔ J) (i : R) (hi : i ∈ I ⊔ K), i ∈ I ⊔ J * K
⊢ i ∈ I ⊔ J * K

Tactic:
rw [eq_top_iff_one] at h

Premises used: Ideal.eq_top_iff_one
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J K : Ideal R
inst_1 : I.IsTwoSided
h : 1 ∈ I ⊔ J
i : R
hi : i ∈ I ⊔ K
rw : ∀ (h : ∃ y ∈ I, ∃ z ∈ J, y + z = 1) (i : R) (hi : ∃ y ∈ I, ∃ z ∈ K, y + z = i), ∃ y ∈ I, ∃ z ∈ J * K, y + z = i
⊢ i ∈ I ⊔ J * K

Tactic:
rw [Submodule.mem_sup] at h hi ⊢

Premises used: Submodule.mem_sup
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J K : Ideal R
inst_1 : I.IsTwoSided
h : ∃ y ∈ I, ∃ z ∈ J, y + z = 1
i : R
hi : ∃ y ∈ I, ∃ z ∈ K, y + z = i
obtain : ∀ (i1 : R) (hi1 : i1 ∈ I) (j : R) (hj : j ∈ J) (h : i1 + j = 1), ∃ y ∈ I, ∃ z ∈ J * K, y + z = i
⊢ ∃ y ∈ I, ∃ z ∈ J * K, y + z = i

Tactic:
obtain ⟨i1, hi1, j, hj, h⟩ := h
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J K : Ideal R
inst_1 : I.IsTwoSided
i : R
hi : ∃ y ∈ I, ∃ z ∈ K, y + z = i
i1 : R
hi1 : i1 ∈ I
j : R
hj : j ∈ J
h : i1 + j = 1
obtain : ∀ (i' : R) (hi' : i' ∈ I) (k : R) (hk : k ∈ K), ∃ y ∈ I, ∃ z ∈ J * K, y + z = i' + k
⊢ ∃ y ∈ I, ∃ z ∈ J * K, y + z = i

Tactic:
obtain ⟨i', hi', k, hk, rfl⟩ := hi

Premises used: rfl
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J K : Ideal R
inst_1 : I.IsTwoSided
i1 : R
hi1 : i1 ∈ I
j : R
hj : j ∈ J
h : i1 + j = 1
i' : R
hi' : i' ∈ I
k : R
hk : k ∈ K
⊢ ∃ y ∈ I, ∃ z ∈ J * K, y + z = i' + k

Tactic:
⟨_, add_mem hi' (mul_mem_right k _ hi1), _, mul_mem_mul hj hk, ?_⟩

Premises used: Ideal.mul_mem_mul, Ideal.mul_mem_right, And.intro, Exists.intro, AddMemClass.add_mem
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J K : Ideal R
inst_1 : I.IsTwoSided
i1 : R
hi1 : i1 ∈ I
j : R
hj : j ∈ J
h : i1 + j = 1
i' : R
hi' : i' ∈ I
k : R
hk : k ∈ K
refine : i' + i1 * k + j * k = i' + k
⊢ ∃ y ∈ I, ∃ z ∈ J * K, y + z = i' + k

Tactic:
refine ⟨_, add_mem hi' (mul_mem_right k _ hi1), _, mul_mem_mul hj hk, ?_⟩
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J K : Ideal R
inst_1 : I.IsTwoSided
i1 : R
hi1 : i1 ∈ I
j : R
hj : j ∈ J
h : i1 + j = 1
i' : R
hi' : i' ∈ I
k : R
hk : k ∈ K
rw : i' + (i1 * k + j * k) = i' + k
rw₁ : i' + (i1 + j) * k = i' + k
rw₂ : i' + 1 * k = i' + k
rw₃ rw₄ : i' + k = i' + k
⊢ i' + i1 * k + j * k = i' + k

Tactic:
rw [add_assoc, ← add_mul, h, one_mul]

Premises used: add_mul, add_assoc, one_mul
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J K : Ideal R
inst_1 : J.IsTwoSided
h : I ⊔ K = ⊤
i : R
hi : i ∈ I ⊔ J
rw : ∀ (h : 1 ∈ I ⊔ K) (i : R) (hi : i ∈ I ⊔ J), i ∈ I ⊔ J * K
⊢ i ∈ I ⊔ J * K

Tactic:
rw [eq_top_iff_one] at h

Premises used: Ideal.eq_top_iff_one
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J K : Ideal R
inst_1 : J.IsTwoSided
h : 1 ∈ I ⊔ K
i : R
hi : i ∈ I ⊔ J
rw : ∀ (h : ∃ y ∈ I, ∃ z ∈ K, y + z = 1) (i : R) (hi : ∃ y ∈ I, ∃ z ∈ J, y + z = i), ∃ y ∈ I, ∃ z ∈ J * K, y + z = i
⊢ i ∈ I ⊔ J * K

Tactic:
rw [Submodule.mem_sup] at h hi ⊢

Premises used: Submodule.mem_sup
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J K : Ideal R
inst_1 : J.IsTwoSided
h : ∃ y ∈ I, ∃ z ∈ K, y + z = 1
i : R
hi : ∃ y ∈ I, ∃ z ∈ J, y + z = i
obtain : ∀ (i1 : R) (hi1 : i1 ∈ I) (k : R) (hk : k ∈ K) (h : i1 + k = 1), ∃ y ∈ I, ∃ z ∈ J * K, y + z = i
⊢ ∃ y ∈ I, ∃ z ∈ J * K, y + z = i

Tactic:
obtain ⟨i1, hi1, k, hk, h⟩ := h
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J K : Ideal R
inst_1 : J.IsTwoSided
i : R
hi : ∃ y ∈ I, ∃ z ∈ J, y + z = i
i1 : R
hi1 : i1 ∈ I
k : R
hk : k ∈ K
h : i1 + k = 1
obtain : ∀ (i' : R) (hi' : i' ∈ I) (j : R) (hj : j ∈ J), ∃ y ∈ I, ∃ z ∈ J * K, y + z = i' + j
⊢ ∃ y ∈ I, ∃ z ∈ J * K, y + z = i

Tactic:
obtain ⟨i', hi', j, hj, rfl⟩ := hi

Premises used: rfl
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J K : Ideal R
inst_1 : J.IsTwoSided
i1 : R
hi1 : i1 ∈ I
k : R
hk : k ∈ K
h : i1 + k = 1
i' : R
hi' : i' ∈ I
j : R
hj : j ∈ J
⊢ ∃ y ∈ I, ∃ z ∈ J * K, y + z = i' + j

Tactic:
⟨_, add_mem hi' (mul_mem_left _ j hi1), _, mul_mem_mul hj hk, ?_⟩

Premises used: Ideal.mul_mem_mul, And.intro, Exists.intro, AddMemClass.add_mem, Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J K : Ideal R
inst_1 : J.IsTwoSided
i1 : R
hi1 : i1 ∈ I
k : R
hk : k ∈ K
h : i1 + k = 1
i' : R
hi' : i' ∈ I
j : R
hj : j ∈ J
refine : i' + j * i1 + j * k = i' + j
⊢ ∃ y ∈ I, ∃ z ∈ J * K, y + z = i' + j

Tactic:
refine ⟨_, add_mem hi' (mul_mem_left _ j hi1), _, mul_mem_mul hj hk, ?_⟩
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J K : Ideal R
inst_1 : J.IsTwoSided
i1 : R
hi1 : i1 ∈ I
k : R
hk : k ∈ K
h : i1 + k = 1
i' : R
hi' : i' ∈ I
j : R
hj : j ∈ J
rw : i' + (j * i1 + j * k) = i' + j
rw₁ : i' + j * (i1 + k) = i' + j
rw₂ : i' + j * 1 = i' + j
rw₃ rw₄ : i' + j = i' + j
⊢ i' + j * i1 + j * k = i' + j

Tactic:
rw [add_assoc, ← mul_add, h, mul_one]

Premises used: add_assoc, mul_add, mul_one
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J K : Ideal R
inst_1 : J.IsTwoSided
h : I ⊔ J = ⊤
⊢ J ⊔ I = ⊤

Tactic:
rw [sup_comm] at h

Premises used: sup_comm
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J K : Ideal R
inst_1 : J.IsTwoSided
h : J ⊔ I = ⊤
rw : J ⊔ I * K = K ⊔ J
rw₁ : J ⊔ K = K ⊔ J
rw₂ rw₃ : K ⊔ J = K ⊔ J
⊢ I * K ⊔ J = K ⊔ J

Tactic:
rw [sup_comm, sup_mul_eq_of_coprime_left h, sup_comm]

Premises used: sup_comm, Ideal.sup_mul_eq_of_coprime_left
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J K : Ideal R
inst_1 : I.IsTwoSided
h : K ⊔ J = ⊤
⊢ J ⊔ K = ⊤

Tactic:
rw [sup_comm] at h

Premises used: sup_comm
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J K : Ideal R
inst_1 : I.IsTwoSided
h : J ⊔ K = ⊤
rw : J ⊔ I * K = I ⊔ J
rw₁ : J ⊔ I = I ⊔ J
rw₂ rw₃ : I ⊔ J = I ⊔ J
⊢ I * K ⊔ J = I ⊔ J

Tactic:
rw [sup_comm, sup_mul_eq_of_coprime_right h, sup_comm]

Premises used: Ideal.sup_mul_eq_of_coprime_right, sup_comm
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I : Ideal R
ι : Type u_1
s : Finset ι
J : ι → Ideal R
inst_1 : ∀ (i : ι), (J i).IsTwoSided
h : ∀ i ∈ s, I ⊔ J i = ⊤
⊢ I ⊔ ⨅ (i : ι), ⨅ (_ : Membership.mem (γ := Finset ι) ∅ i), J i = ⊤

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I : Ideal R
ι : Type u_1
s : Finset ι
J : ι → Ideal R
inst_1 : ∀ (i : ι), (J i).IsTwoSided
h : ∀ i ∈ s, I ⊔ J i = ⊤
i : ι
t : Finset ι
his : i ∈ s
hts : t ⊆ s
hit : i ∉ t
eq_top : I ⊔ ⨅ i ∈ t, J i = ⊤
rw : ⊤ ≤ I ⊔ (⨅ x ∈ t, J x) ⊓ J i
⊢ ⊤ ≤ I ⊔ ⨅ i_1 ∈ insert i t, J i_1

Tactic:
rw [Finset.iInf_insert, inf_comm]

Premises used: Finset.iInf_insert, inf_comm
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I : Ideal R
ι : Type u_1
s : Finset ι
J : ι → Ideal R
inst_1 : ∀ (i : ι), (J i).IsTwoSided
h : ∀ i ∈ s, I ⊔ J i = ⊤
i : ι
t : Finset ι
his : i ∈ s
hts : t ⊆ s
hit : i ∉ t
eq_top : I ⊔ ⨅ i ∈ t, J i = ⊤
⊢ ⊤ ≤ I ⊔ (⨅ x ∈ t, J x) ⊓ J i

Tactic:
le_trans ?_ (sup_le_sup_left mul_le_inf _)

Premises used: sup_le_sup_left, le_trans
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I : Ideal R
ι : Type u_1
s : Finset ι
J : ι → Ideal R
inst_1 : ∀ (i : ι), (J i).IsTwoSided
h : ∀ i ∈ s, I ⊔ J i = ⊤
i : ι
t : Finset ι
his : i ∈ s
hts : t ⊆ s
hit : i ∉ t
eq_top : I ⊔ ⨅ i ∈ t, J i = ⊤
refine : ⊤ ≤ I ⊔ (⨅ x ∈ t, J x) * J i
⊢ ⊤ ≤ I ⊔ (⨅ x ∈ t, J x) ⊓ J i

Tactic:
refine le_trans ?_ (sup_le_sup_left mul_le_inf _)

Premises used: sup_le_sup_left, le_trans