awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
simpa only [sup_mul_eq_of_coprime_right (h _ his)] using eq_top.ge

Premises used: Eq.ge, Ideal.sup_mul_eq_of_coprime_right
-- 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 ∈ s, J i = ⊤

Tactic:
exact s.induction_on' (by simp) fun {i t} his hts hit eq_top ↦ top_unique <| by
    rw [Finset.iInf_insert, inf_comm]
    refine le_trans ?_ (sup_le_sup_left mul_le_inf _)
    simpa only [sup_mul_eq_of_coprime_right (h _ his)] using eq_top.ge
-- 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 ∈ s, J i = ⊤

Tactic:
classical
  exact s.induction_on' (by simp) fun {i t} his hts hit eq_top ↦ top_unique <| by
    rw [Finset.iInf_insert, inf_comm]
    refine le_trans ?_ (sup_le_sup_left mul_le_inf _)
    simpa only [sup_mul_eq_of_coprime_right (h _ his)] using eq_top.ge
-- 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, J i ⊔ I = ⊤
rw : ∀ i ∈ s, I ⊔ J i = ⊤
⊢ (⨅ i ∈ s, J i) ⊔ I = ⊤

Tactic:
rw [sup_comm, sup_iInf_eq_top]

Premises used: sup_comm, Ideal.sup_iInf_eq_top
-- 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, J i ⊔ I = ⊤
i : ι
hi : i ∈ s
rw : J i ⊔ I = ⊤
rw₁ rw₂ : Eq.{u + 1} (α := Ideal R) ⊤ ⊤
⊢ I ⊔ J i = ⊤

Tactic:
rw [sup_comm, h i hi]

Premises used: sup_comm
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J : Ideal R
inst_1 : I.IsTwoSided
h : I ⊔ J = ⊤
⊢ I ⊔ HPow.hPow (β := ℕ) J 0 = ⊤

Tactic:
simp [J.pow_zero]

Premises used: Submodule.pow_zero
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J : Ideal R
inst_1 : I.IsTwoSided
h : I ⊔ J = ⊤
n : ℕ
ih : I ⊔ J ^ n = ⊤
succ : I ⊔ J ^ n * J = ⊤
succ₁ succ₂ succ₃ succ₄ : I ⊔ J = ⊤
⊢ I ⊔ J ^ (n + 1) = ⊤

Tactic:
rwa [J.pow_succ, sup_mul_eq_of_coprime_left ih]

Premises used: Submodule.pow_succ, Ideal.sup_mul_eq_of_coprime_left
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J : Ideal R
inst_1 : I.IsTwoSided
n : ℕ
h : I ⊔ J = ⊤
zero : I ⊔ HPow.hPow (β := ℕ) J 0 = ⊤
succ : ∀ (n : ℕ) (ih : I ⊔ J ^ n = ⊤), I ⊔ J ^ (n + 1) = ⊤
⊢ I ⊔ J ^ n = ⊤

Tactic:
induction n with
  | zero => simp [J.pow_zero]
  | succ n ih => rwa [J.pow_succ, sup_mul_eq_of_coprime_left ih]

Premises used: Submodule.pow_zero, Submodule.pow_succ
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J : Ideal R
inst_1 : J.IsTwoSided
h : I ⊔ J = ⊤
⊢ I ⊔ HPow.hPow (β := ℕ) J 0 = ⊤

Tactic:
simp [J.pow_zero]

Premises used: Submodule.pow_zero
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J : Ideal R
inst_1 : J.IsTwoSided
h : I ⊔ J = ⊤
n : ℕ
ih : I ⊔ J ^ n = ⊤
succ : ∀ (ih : I ⊔ HPow.hPow (β := ℕ) J 0 = ⊤), I ⊔ J ^ HAdd.hAdd (α := ℕ) 0 1 = ⊤
succ₁ : ∀ (hn : n ≠ 0), I ⊔ J ^ (n + 1) = ⊤
⊢ I ⊔ J ^ (n + 1) = ⊤

Tactic:
obtain rfl | hn := 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 J : Ideal R
inst_1 : J.IsTwoSided
h : I ⊔ J = ⊤
ih : I ⊔ HPow.hPow (β := ℕ) J 0 = ⊤
⊢ I ⊔ J ^ HAdd.hAdd (α := ℕ) 0 1 = ⊤

Tactic:
simpa [J.pow_one] using h

Premises used: Submodule.pow_one
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J : Ideal R
inst_1 : J.IsTwoSided
h : I ⊔ J = ⊤
n : ℕ
ih : I ⊔ J ^ n = ⊤
hn : n ≠ 0
succ : I ⊔ J * J ^ n = ⊤
succ₁ succ₂ succ₃ succ₄ : I ⊔ J = ⊤
⊢ I ⊔ J ^ (n + 1) = ⊤

Tactic:
rwa [J.pow_succ' hn, sup_mul_eq_of_coprime_right ih]

Premises used: Ideal.sup_mul_eq_of_coprime_right, Submodule.pow_succ'
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J : Ideal R
inst_1 : J.IsTwoSided
n : ℕ
h : I ⊔ J = ⊤
zero : I ⊔ HPow.hPow (β := ℕ) J 0 = ⊤
succ : ∀ (n : ℕ) (ih : I ⊔ J ^ n = ⊤), I ⊔ J ^ (n + 1) = ⊤
⊢ I ⊔ J ^ n = ⊤

Tactic:
induction n with
  | zero => simp [J.pow_zero]
  | succ n ih =>
    obtain rfl | hn := eq_or_ne n 0; · simpa [J.pow_one] using h
    rwa [J.pow_succ' hn, sup_mul_eq_of_coprime_right ih]

Premises used: Submodule.pow_zero, eq_or_ne, OfNat.ofNat, rfl, Submodule.pow_one
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J : Ideal R
inst_1 : I.IsTwoSided
n : ℕ
h : I ⊔ J = ⊤
rw : J ⊔ I ^ n = ⊤
rw₁ rw₂ : Eq.{u + 1} (α := Ideal R) ⊤ ⊤
⊢ I ^ n ⊔ J = ⊤

Tactic:
rw [sup_comm, sup_pow_eq_top' (sup_comm I J ▸ h)]

Premises used: Ideal.sup_pow_eq_top', sup_comm
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J : Ideal R
inst_1 : J.IsTwoSided
n : ℕ
h : I ⊔ J = ⊤
rw : J ⊔ I ^ n = ⊤
rw₁ rw₂ : Eq.{u + 1} (α := Ideal R) ⊤ ⊤
⊢ I ^ n ⊔ J = ⊤

Tactic:
rw [sup_comm, sup_pow_eq_top (sup_comm I J ▸ h)]

Premises used: sup_comm, Ideal.sup_pow_eq_top
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J : Ideal R
inst_1 : I.IsTwoSided
m n : ℕ
h : I ⊔ J = ⊤
⊢ I ^ m ⊔ J ^ n = ⊤

Tactic:
pow_sup_eq_top (sup_pow_eq_top h)

Premises used: Ideal.pow_sup_eq_top, Ideal.sup_pow_eq_top
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J : Ideal R
inst_1 : J.IsTwoSided
m n : ℕ
h : I ⊔ J = ⊤
⊢ I ^ m ⊔ J ^ n = ⊤

Tactic:
pow_sup_eq_top' (sup_pow_eq_top' h)

Premises used: Ideal.sup_pow_eq_top', Ideal.pow_sup_eq_top'
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I : Ideal R
inst_1 : I.IsTwoSided
⊢ I * ⊤ = I

Tactic:
le_antisymm (mul_le.mpr fun _i hi _r _ ↦ mul_mem_right _ _ hi)
    fun i hi ↦ mul_one i ▸ mul_mem_mul hi Submodule.mem_top

Premises used: Iff.mpr, Eq.rec, Ideal.mul_le, Ideal.mul_mem_mul, le_antisymm, Ideal.mul_mem_right, mul_one, Submodule.mem_top
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
w x y z : R
inst_1 : IsTwoSided (α := R) (span {w, x})
rw : Eq (α := Ideal R) (span (HMul.hMul (α := Set R) {w, x} {y, z})) (span {w * y, w * z, x * y, x * z})
⊢ HMul.hMul (α := Ideal R) (span {w, x}) (span {y, z}) = span {w * y, w * z, x * y, x * z}

Tactic:
rw [span_mul_span']

Premises used: Ideal.span_mul_span'
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
w x y z : R
inst_1 : IsTwoSided (α := R) (span {w, x})
e_s : HMul.hMul (α := Set R) {w, x} {y, z} = {w * y, w * z, x * y, x * z}
⊢ Eq (α := Ideal R) (span (HMul.hMul (α := Set R) {w, x} {y, z})) (span {w * y, w * z, x * y, x * z})

Tactic:
congr
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
w x y z : R
inst_1 : IsTwoSided (α := R) (span {w, x})
e_s : ∀ (r : R), r ∈ HMul.hMul (α := Set R) {w, x} {y, z} ↔ Membership.mem (γ := Set R) {w * y, w * z, x * y, x * z} r
⊢ HMul.hMul (α := Set R) {w, x} {y, z} = {w * y, w * z, x * y, x * z}

Tactic:
ext r
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
w x y z : R
inst_1 : IsTwoSided (α := R) (span {w, x})
r : R
⊢ r ∈ HMul.hMul (α := Set R) {w, x} {y, z} ↔ Membership.mem (γ := Set R) {w * y, w * z, x * y, x * z} r

Tactic:
simp [Set.mem_mul, or_assoc, eq_comm (a := r)]

Premises used: eq_comm, Set.mem_mul, or_assoc
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
n_1 n : ℕ
ih : HPow.hPow (α := Ideal R) ⊤ n = ⊤
rw : HPow.hPow (α := Submodule R R) ⊤ n * ⊤ = ⊤
rw₁ : HMul.hMul (α := Submodule R R) ⊤ ⊤ = ⊤
rw₂ rw₃ : Eq.{u + 1} (α := Ideal R) ⊤ ⊤
⊢ HPow.hPow (α := Ideal R) ⊤ n.succ = ⊤

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

Premises used: Submodule.pow_succ, Ideal.top_mul
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I : Ideal R
n : ℕ
⊢ I ^ n = ⊤ ↔ I = ⊤ ∨ n = 0

Tactic:
⟨fun h ↦ or_iff_not_imp_right.mpr
      fun hn ↦ (eq_top_iff_one _).mpr <| pow_le_self hn <| (eq_top_iff_one _).mp h, ?_⟩

Premises used: Iff.mpr, Classical.or_iff_not_imp_right, Ideal.pow_le_self, Ideal.eq_top_iff_one, HPow.hPow, Iff.intro, Iff.mp
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I : Ideal R
n : ℕ
refine : I = ⊤ ∨ n = 0 → I ^ n = ⊤
⊢ I ^ n = ⊤ ↔ I = ⊤ ∨ n = 0

Tactic:
refine ⟨fun h ↦ or_iff_not_imp_right.mpr
      fun hn ↦ (eq_top_iff_one _).mpr <| pow_le_self hn <| (eq_top_iff_one _).mp h, ?_⟩
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I : Ideal R
n : ℕ
h : I = ⊤
inl : HPow.hPow (α := Ideal R) ⊤ n = ⊤
inl₁ inl₂ : Eq.{u + 1} (α := Ideal R) ⊤ ⊤
⊢ I ^ n = ⊤

Tactic:
rw [h, top_pow]

Premises used: Ideal.top_pow
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I : Ideal R
n : ℕ
h : n = 0
inr : HPow.hPow (β := ℕ) I 0 = ⊤
inr₁ : Eq.{u + 1} (α := Ideal R) 1 ⊤
inr₂ inr₃ : Eq.{u + 1} (α := Ideal R) ⊤ ⊤
⊢ I ^ n = ⊤

Tactic:
rw [h, 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
hn : Ne (α := ℕ) 0 0
⊢ Eq.{u + 1} (α := Ideal R) (↑0 : Ideal R) ⊤

Tactic:
(hn rfl).elim

Premises used: False.elim, rfl
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
hn : Ne (α := ℕ) 0 0
⊢ Eq.{u + 1} (α := Ideal R) (↑0 : Ideal R) ⊤

Tactic:
exact (hn rfl).elim

Premises used: False.elim, rfl
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
n : ℕ
ih : ∀ (hn : n ≠ 0), Eq.{u + 1} (α := Ideal R) (↑n : Ideal R) ⊤
hn : n + 1 ≠ 0
succ :
  ∀ (ih : ∀ (hn : Ne (α := ℕ) 0 0), Eq.{u + 1} (α := Ideal R) (↑0 : Ideal R) ⊤) (hn : HAdd.hAdd (α := ℕ) 0 1 ≠ 0),
    Eq.{u + 1} (α := Ideal R) (↑(HAdd.hAdd (α := ℕ) 0 1) : Ideal R) ⊤
succ₁ :
  ∀ (n : ℕ) (ih : ∀ (hn : n + 1 ≠ 0), Eq.{u + 1} (α := Ideal R) (↑(n + 1) : Ideal R) ⊤) (hn : n + 1 + 1 ≠ 0),
    Eq.{u + 1} (α := Ideal R) (↑(n + 1 + 1) : Ideal R) ⊤
⊢ Eq.{u + 1} (α := Ideal R) (↑(n + 1) : Ideal R) ⊤

Tactic:
obtain rfl | n := n

Premises used: rfl
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
ih : ∀ (hn : Ne (α := ℕ) 0 0), Eq.{u + 1} (α := Ideal R) (↑0 : Ideal R) ⊤
hn : HAdd.hAdd (α := ℕ) 0 1 ≠ 0
succ : Eq.{u + 1} (α := Ideal R) 1 ⊤
succ₁ succ₂ : Eq.{u + 1} (α := Ideal R) ⊤ ⊤
⊢ Eq.{u + 1} (α := Ideal R) (↑(HAdd.hAdd (α := ℕ) 0 1) : Ideal R) ⊤

Tactic:
rw [Nat.cast_one, one_eq_top]

Premises used: Ideal.one_eq_top, Nat.cast_one
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
n : ℕ
ih : ∀ (hn : n + 1 ≠ 0), Eq.{u + 1} (α := Ideal R) (↑(n + 1) : Ideal R) ⊤
hn : n + 1 + 1 ≠ 0
succ : HAdd.hAdd (α := Ideal R) (↑(n + 1) : Ideal R) 1 = ⊤
succ₁ : HAdd.hAdd (α := Ideal R) ⊤ 1 = ⊤
succ₂ : Eq.{u + 1} (α := Ideal R) (⊤ ⊔ 1) ⊤
succ₃ succ₄ : Eq.{u + 1} (α := Ideal R) ⊤ ⊤
⊢ Eq.{u + 1} (α := Ideal R) (↑(n + 1 + 1) : Ideal R) ⊤

Tactic:
rw [Nat.cast_succ, ih n.succ_ne_zero, add_eq_sup, top_sup_eq]

Premises used: Nat.cast_succ, Nat.succ_ne_zero, top_sup_eq, Ideal.add_eq_sup
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
n : ℕ
hn : n ≠ 0
zero : ∀ (hn : Ne (α := ℕ) 0 0), Eq.{u + 1} (α := Ideal R) (↑0 : Ideal R) ⊤
succ :
  ∀ (n : ℕ) (ih : ∀ (hn : n ≠ 0), Eq.{u + 1} (α := Ideal R) (↑n : Ideal R) ⊤) (hn : n + 1 ≠ 0),
    Eq.{u + 1} (α := Ideal R) (↑(n + 1) : Ideal R) ⊤
⊢ Eq.{u + 1} (α := Ideal R) (↑n : Ideal R) ⊤

Tactic:
induction n with
  | zero => exact (hn rfl).elim
  | succ n ih =>
    obtain rfl | n := n; · rw [Nat.cast_one, one_eq_top]
    rw [Nat.cast_succ, ih n.succ_ne_zero, add_eq_sup, top_sup_eq]

Premises used: Nat.cast_succ, Ideal.one_eq_top, False.elim, top_sup_eq, Ideal.add_eq_sup, Nat.cast_one, rfl
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
n : ℕ
inst_1 : n.AtLeastTwo
⊢ Eq.{u + 1} (α := Ideal R) (OfNat.ofNat n) ⊤

Tactic:
natCast_eq_top (NeZero.ne _)

Premises used: Ideal.natCast_eq_top, NeZero.ne
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I : Ideal R
n m : ℕ
hnI : I ^ n = 0
hmn : n ≤ m
x : R
hx : x ∈ I
⊢ x ^ m = 0

Tactic:
simpa [hnI] using pow_le_pow_right hmn <| pow_mem_pow hx m

Premises used: Ideal.pow_le_pow_right, Ideal.pow_mem_pow
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
r s : R
hr : r ∈ I
hs : s ∈ J
⊢ s * r ∈ I * J

Tactic:
mul_comm r s ▸ mul_mem_mul hr hs

Premises used: Set.Mem, Eq.rec, Ideal.mul_mem_mul, mul_comm
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
ι : Type u_2
s : Finset ι
I : ι → Ideal R
x : ι → R
⊢ (∀ i ∈ s, x i ∈ I i) → Membership.mem (γ := Ideal R) (∏ i ∈ s, I i) (∏ i ∈ s, x i)

Tactic:
Finset.induction_on s ?_ ?_

Premises used: Finset.induction_on
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
ι : Type u_2
s : Finset ι
I : ι → Ideal R
x : ι → R
refine_1 :
  (∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → x i ∈ I i) →
    Membership.mem (γ := Ideal R) (∏ i ∈ ∅, I i) (∏ i ∈ ∅, x i)
refine_2 :
  ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      ((∀ i ∈ s, x i ∈ I i) → Membership.mem (γ := Ideal R) (∏ i ∈ s, I i) (∏ i ∈ s, x i)) →
        (∀ i ∈ insert a s, x i ∈ I i) → Membership.mem (γ := Ideal R) (∏ i ∈ insert a s, I i) (∏ i ∈ insert a s, x i)
⊢ (∀ i ∈ s, x i ∈ I i) → Membership.mem (γ := Ideal R) (∏ i ∈ s, I i) (∏ i ∈ s, x i)

Tactic:
refine Finset.induction_on s ?_ ?_
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
ι : Type u_2
s : Finset ι
I : ι → Ideal R
x : ι → R
⊢ (∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → x i ∈ I i) →
    Membership.mem (γ := Ideal R) (∏ i ∈ ∅, I i) (∏ i ∈ ∅, x i)

Tactic:
grind [Submodule.mem_top]

Premises used: Submodule.mem_top
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
ι : Type u_2
s : Finset ι
I : ι → Ideal R
x : ι → R
⊢ ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      ((∀ i ∈ s, x i ∈ I i) → Membership.mem (γ := Ideal R) (∏ i ∈ s, I i) (∏ i ∈ s, x i)) →
        (∀ i ∈ insert a s, x i ∈ I i) → Membership.mem (γ := Ideal R) (∏ i ∈ insert a s, I i) (∏ i ∈ insert a s, x i)

Tactic:
grind [mul_mem_mul]

Premises used: Ideal.mul_mem_mul
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
ι : Type u_2
s : Finset ι
I : ι → Ideal R
x : ι → R
refine_1 :
  (∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → x i ∈ I i) →
    Membership.mem (γ := Ideal R) (∏ i ∈ ∅, I i) (∏ i ∈ ∅, x i)
refine_2 refine_2₁ :
  ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      ((∀ i ∈ s, x i ∈ I i) → Membership.mem (γ := Ideal R) (∏ i ∈ s, I i) (∏ i ∈ s, x i)) →
        (∀ i ∈ insert a s, x i ∈ I i) → Membership.mem (γ := Ideal R) (∏ i ∈ insert a s, I i) (∏ i ∈ insert a s, x i)
⊢ (∀ i ∈ s, x i ∈ I i) → Membership.mem (γ := Ideal R) (∏ i ∈ s, I i) (∏ i ∈ s, x i)

Tactic:
classical
    refine Finset.induction_on s ?_ ?_
    · grind [Submodule.mem_top]
    · grind [mul_mem_mul]

Premises used: Ideal.mul_mem_mul, Submodule.mem_top
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
n m : ℕ
rw :
  ((Finset.range (n + m + 1)).sup fun (m_1 : ℕ) ↦ I ^ m_1 * J ^ (n + m - m_1) * (↑((n + m).choose m_1) : Ideal R)) ≤
    I ^ n + J ^ m
⊢ (I ⊔ J) ^ (n + m) ≤ I ^ n ⊔ J ^ m

Tactic:
rw [← Ideal.add_eq_sup, ← Ideal.add_eq_sup, add_pow, Ideal.sum_eq_sup]

Premises used: Ideal.sum_eq_sup, Ideal.add_eq_sup, add_pow
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
n m : ℕ
a : ∀ b ∈ Finset.range (n + m + 1), I ^ b * J ^ (n + m - b) * (↑((n + m).choose b) : Ideal R) ≤ I ^ n + J ^ m
⊢ ((Finset.range (n + m + 1)).sup fun (m_1 : ℕ) ↦ I ^ m_1 * J ^ (n + m - m_1) * (↑((n + m).choose m_1) : Ideal R)) ≤
    I ^ n + J ^ m

Tactic:
apply Finset.sup_le

Premises used: Finset.sup_le
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
n m i : ℕ
hi : i ∈ Finset.range (n + m + 1)
pos : ∀ (hn : n ≤ i), I ^ i * J ^ (n + m - i) * (↑((n + m).choose i) : Ideal R) ≤ I ^ n + J ^ m
neg : ∀ (hn : ¬n ≤ i), I ^ i * J ^ (n + m - i) * (↑((n + m).choose i) : Ideal R) ≤ I ^ n + J ^ m
⊢ I ^ i * J ^ (n + m - i) * (↑((n + m).choose i) : Ideal R) ≤ I ^ n + J ^ m

Tactic:
by_cases hn : n ≤ i
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
n m i : ℕ
hi : i ∈ Finset.range (n + m + 1)
hn : n ≤ i
⊢ I ^ i * J ^ (n + m - i) * (↑((n + m).choose i) : Ideal R) ≤ I ^ n + J ^ m

Tactic:
(Ideal.mul_le_right.trans (Ideal.mul_le_right.trans
      ((Ideal.pow_le_pow_right hn).trans le_sup_left)))

Premises used: Ideal.mul_le_right, le_sup_left, Set.Mem, Ideal.pow_le_pow_right, LE.le.trans
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
n m i : ℕ
hi : i ∈ Finset.range (n + m + 1)
hn : n ≤ i
⊢ I ^ i * J ^ (n + m - i) * (↑((n + m).choose i) : Ideal R) ≤ I ^ n + J ^ m

Tactic:
exact (Ideal.mul_le_right.trans (Ideal.mul_le_right.trans
      ((Ideal.pow_le_pow_right hn).trans le_sup_left)))

Premises used: Ideal.mul_le_right, Ideal.pow_le_pow_right, LE.le.trans
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
n m i : ℕ
hi : i ∈ Finset.range (n + m + 1)
hn : ¬n ≤ i
⊢ I ^ i * J ^ (n + m - i) * (↑((n + m).choose i) : Ideal R) ≤ I ^ n + J ^ m

Tactic:
(Ideal.mul_le_right.trans (Ideal.mul_le_left.trans
      ((Ideal.pow_le_pow_right ?_).trans le_sup_right)))

Premises used: Ideal.mul_le_right, Set.Mem, le_sup_right, Ideal.pow_le_pow_right, Ideal.mul_le_left, LE.le.trans
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
n m i : ℕ
hi : i ∈ Finset.range (n + m + 1)
hn : ¬n ≤ i
neg : m ≤ n + m - i
⊢ I ^ i * J ^ (n + m - i) * (↑((n + m).choose i) : Ideal R) ≤ I ^ n + J ^ m

Tactic:
refine (Ideal.mul_le_right.trans (Ideal.mul_le_left.trans
      ((Ideal.pow_le_pow_right ?_).trans le_sup_right)))

Premises used: Ideal.mul_le_right, Ideal.pow_le_pow_right, Ideal.mul_le_left, LE.le.trans
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
n m i : ℕ
hi : i ∈ Finset.range (n + m + 1)
hn : ¬n ≤ i
⊢ m ≤ n + m - i

Tactic:
lia
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
⊢ I * J = J * I

Tactic:
le_antisymm (mul_le.2 fun _ hrI _ hsJ => mul_mem_mul_rev hsJ hrI)
    (mul_le.2 fun _ hrJ _ hsI => mul_mem_mul_rev hsI hrJ)

Premises used: Iff.mpr, Ideal.mul_le, le_antisymm, Ideal.mul_mem_mul_rev
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
x y : R
I : Ideal R
⊢ x ∈ span {y} * I ↔ ∃ z ∈ I, y * z = x

Tactic:
simp only [mul_comm, mem_mul_span_singleton]

Premises used: mul_comm, Ideal.mem_mul_span_singleton
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
a : A
⊢ Eq (α := Submodule R A)
    (LinearMap.range (R := R) (M := A) (τ₁₂ := RingHom.id R) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) a))
    (Submodule.restrictScalars R (span {a}))

Tactic:
aesop (add simp Ideal.mem_span_singleton) (add simp dvd_def)

Premises used: dvd_def, Ideal.mem_span_singleton
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
a : R
⊢ Eq (α := Submodule R R)
    (LinearMap.range (R := R) (M := R) (τ₁₂ := RingHom.id R) ((LinearMap.mul R R : (a : R) → R →ₗ[R] R) a)) (span {a})

Tactic:
range_mul ..

Premises used: iInf, Set.iInter, Submodule.restrictScalars, Ideal.range_mul, setOf, Submodule.span
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
x : R
I J : Ideal R
⊢ (∀ {zI : R}, zI ∈ I → zI ∈ span {x} * J) ↔ ∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI

Tactic:
simp only [mem_span_singleton_mul]

Premises used: Ideal.mem_span_singleton_mul
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
x : R
I J : Ideal R
⊢ span {x} * I ≤ J ↔ ∀ z ∈ I, x * z ∈ J

Tactic:
simp [SetLike.le_def, mem_span_singleton_mul]

Premises used: SetLike.le_def, Ideal.mem_span_singleton_mul
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
x y : R
I J : Ideal R
⊢ span {x} * I ≤ span {y} * J ↔ ∀ zI ∈ I, ∃ zJ ∈ J, x * zI = y * zJ

Tactic:
simp only [span_singleton_mul_le_iff, mem_span_singleton_mul, eq_comm]

Premises used: eq_comm, Ideal.mem_span_singleton_mul, Ideal.span_singleton_mul_le_iff
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
inst_1 : IsDomain R
x : R
hx : x ≠ 0
simp_rw : (∀ zI ∈ I, ∃ zJ ∈ J, x * zI = x * zJ) ↔ I ≤ J
simp_rw₁ : (∀ zI ∈ I, ∃ zJ ∈ J, zI = zJ) ↔ I ≤ J
simp_rw₂ : (∀ zI ∈ I, zI ∈ J) ↔ I ≤ J
⊢ span {x} * I ≤ span {x} * J ↔ I ≤ J

Tactic:
simp_rw [span_singleton_mul_le_span_singleton_mul, mul_right_inj' hx,
    exists_eq_right', SetLike.le_def]

Premises used: Ideal.span_singleton_mul_le_span_singleton_mul, exists_eq_right', SetLike.le_def, mul_right_inj'
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
inst_1 : IsDomain R
x : R
hx : x ≠ 0
⊢ span {x} * I = span {x} * J ↔ I = J

Tactic:
simp only [le_antisymm_iff, span_singleton_mul_right_mono hx]

Premises used: le_antisymm_iff, Ideal.span_singleton_mul_right_mono
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsDomain R
x : R
hx : x ≠ 0
⊢ Function.Injective (β := Ideal R) fun (x_1 : Ideal R) ↦ span {x} * x_1

Tactic:
fun _ _ =>
  (span_singleton_mul_right_inj hx).mp

Premises used: Ideal.span_singleton_mul_right_inj, Iff.mp, Function.Injective
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsDomain R
x : R
hx : x ≠ 0
⊢ Function.Injective (β := Ideal R) fun (I : Ideal R) ↦ I * span {x}

Tactic:
fun _ _ =>
  (span_singleton_mul_left_inj hx).mp

Premises used: Iff.mp, Ideal.span_singleton_mul_left_inj, Function.Injective
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
x : R
I J : Ideal R
⊢ I = span {x} * J ↔ (∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI) ∧ ∀ z ∈ J, x * z ∈ I

Tactic:
simp only [le_antisymm_iff, le_span_singleton_mul_iff, span_singleton_mul_le_iff]

Premises used: Ideal.le_span_singleton_mul_iff, le_antisymm_iff, Ideal.span_singleton_mul_le_iff
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
x y : R
I J : Ideal R
⊢ span {x} * I = span {y} * J ↔ (∀ zI ∈ I, ∃ zJ ∈ J, x * zI = y * zJ) ∧ ∀ zJ ∈ J, ∃ zI ∈ I, x * zI = y * zJ

Tactic:
simp only [le_antisymm_iff, span_singleton_mul_le_span_singleton_mul, eq_comm]

Premises used: Ideal.span_singleton_mul_le_span_singleton_mul, eq_comm, le_antisymm_iff
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
ι : Type u_2
s : Finset ι
I : ι → Set R
⊢ Eq.{u + 1} (α := Ideal R) (∏ i ∈ s, span (I i)) (span (∏ i ∈ s, I i))

Tactic:
Submodule.prod_span s I

Premises used: Submodule.prod_span
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
ι : Type u_2
s : Finset ι
I : ι → R
⊢ Eq (α := Ideal R) (∏ i ∈ s, span {I i}) (span {∏ i ∈ s, I i})

Tactic:
Submodule.prod_span_singleton s I

Premises used: Submodule.prod_span_singleton
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
m : Multiset R
⊢ Eq (α := Ideal R) (Multiset.prod (Multiset.map (fun (x : R) ↦ span {x}) 0)) (span {Multiset.prod 0})

Tactic:
simp