awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ i' + j * i1 + j * k = i' + j
have rw₁ : i' + j * (i1 + k) = i' + j
Tactic: rw [add_assoc, ← mul_add, h, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ i' + j * i1 + j * k = i' + j
have rw₂ : i' + j * 1 = i' + j
Tactic: rw [add_assoc, ← mul_add, h, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ i' + j * i1 + j * k = i' + j
have rw₃ : i' + j = i' + j
Tactic: rw [add_assoc, ← mul_add, h, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (hypothesis)
Goal:
R : Type u
inst : Semiring R
I J K : Ideal R
inst_1 : J.IsTwoSided
h : I ⊔ J = ⊤
⊢ I * K ⊔ J = K ⊔ J
have h₁ : J ⊔ I = ⊤
Tactic: rw [sup_comm] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : Semiring R
I J K : Ideal R
inst_1 : J.IsTwoSided
h : J ⊔ I = ⊤
⊢ I * K ⊔ J = K ⊔ J
have rw : J ⊔ I * K = K ⊔ J
Tactic: rw [sup_comm, sup_mul_eq_of_coprime_left h, sup_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ I * K ⊔ J = K ⊔ J
have rw₁ : J ⊔ K = K ⊔ J
Tactic: rw [sup_comm, sup_mul_eq_of_coprime_left h, sup_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ I * K ⊔ J = K ⊔ J
have rw₂ : K ⊔ J = K ⊔ J
Tactic: rw [sup_comm, sup_mul_eq_of_coprime_left h, sup_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (hypothesis)
Goal:
R : Type u
inst : Semiring R
I J K : Ideal R
inst_1 : I.IsTwoSided
h : K ⊔ J = ⊤
⊢ I * K ⊔ J = I ⊔ J
have h₁ : J ⊔ K = ⊤
Tactic: rw [sup_comm] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : Semiring R
I J K : Ideal R
inst_1 : I.IsTwoSided
h : J ⊔ K = ⊤
⊢ I * K ⊔ J = I ⊔ J
have rw : J ⊔ I * K = I ⊔ J
Tactic: rw [sup_comm, sup_mul_eq_of_coprime_right h, sup_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ I * K ⊔ J = I ⊔ J
have rw₁ : J ⊔ I = I ⊔ J
Tactic: rw [sup_comm, sup_mul_eq_of_coprime_right h, sup_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ I * K ⊔ J = I ⊔ J
have rw₂ : I ⊔ J = I ⊔ J
Tactic: rw [sup_comm, sup_mul_eq_of_coprime_right h, sup_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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 ⊔ ⨅ i_1 ∈ insert i t, J i_1
have rw : ⊤ ≤ I ⊔ (⨅ x ∈ t, J x) ⊓ J i
Tactic: rw [Finset.iInf_insert, inf_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
have refine : ⊤ ≤ I ⊔ (⨅ x ∈ t, J x) * J i
Tactic: refine le_trans ?_ (sup_le_sup_left mul_le_inf _)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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 ∈ s, J i) ⊔ I = ⊤
have rw : ∀ i ∈ s, I ⊔ J i = ⊤
Tactic: rw [sup_comm, sup_iInf_eq_top]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ I ⊔ J i = ⊤
have rw : J i ⊔ I = ⊤
Tactic: rw [sup_comm, h i hi]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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 = ⊤
⊢ I ⊔ J i = ⊤
have rw₁ : Eq.{u + 1} (α := Ideal R) ⊤ ⊤
Tactic: rw [sup_comm, h i hi]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : Semiring R
I J : Ideal R
inst_1 : I.IsTwoSided
h : I ⊔ J = ⊤
n : ℕ
ih : I ⊔ J ^ n = ⊤
⊢ I ⊔ J ^ (n + 1) = ⊤
have succ : I ⊔ J ^ n * J = ⊤
Tactic: rwa [J.pow_succ, sup_mul_eq_of_coprime_left ih]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : Semiring R
I J : Ideal R
inst_1 : I.IsTwoSided
n : ℕ
h : I ⊔ J = ⊤
⊢ I ⊔ J ^ n = ⊤
have zero : I ⊔ HPow.hPow (β := ℕ) J 0 = ⊤
Tactic: induction n with
  | zero => simp [J.pow_zero]
  | succ n ih => rwa [J.pow_succ, sup_mul_eq_of_coprime_left ih]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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 = ⊤
⊢ I ⊔ J ^ n = ⊤
have succ : ∀ (n : ℕ) (ih : I ⊔ J ^ n = ⊤), I ⊔ J ^ (n + 1) = ⊤
Tactic: induction n with
  | zero => simp [J.pow_zero]
  | succ n ih => rwa [J.pow_succ, sup_mul_eq_of_coprime_left ih]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : Semiring R
I J : Ideal R
inst_1 : J.IsTwoSided
h : I ⊔ J = ⊤
n : ℕ
ih : I ⊔ J ^ n = ⊤
⊢ I ⊔ J ^ (n + 1) = ⊤
have succ : ∀ (ih : I ⊔ HPow.hPow (β := ℕ) J 0 = ⊤), I ⊔ J ^ HAdd.hAdd (α := ℕ) 0 1 = ⊤
Tactic: obtain rfl | hn := eq_or_ne n 0
Cleared hypotheses: n, ih
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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 = ⊤
⊢ I ⊔ J ^ (n + 1) = ⊤
have succ₁ : ∀ (hn : n ≠ 0), I ⊔ J ^ (n + 1) = ⊤
Tactic: obtain rfl | hn := eq_or_ne n 0
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ I ⊔ J ^ (n + 1) = ⊤
have succ : I ⊔ J * J ^ n = ⊤
Tactic: rwa [J.pow_succ' hn, sup_mul_eq_of_coprime_right ih]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : Semiring R
I J : Ideal R
inst_1 : J.IsTwoSided
n : ℕ
h : I ⊔ J = ⊤
⊢ I ⊔ J ^ n = ⊤
have zero : I ⊔ HPow.hPow (β := ℕ) J 0 = ⊤
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]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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 = ⊤
⊢ I ⊔ J ^ n = ⊤
have succ : ∀ (n : ℕ) (ih : I ⊔ J ^ n = ⊤), I ⊔ J ^ (n + 1) = ⊤
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]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : Semiring R
I J : Ideal R
inst_1 : I.IsTwoSided
n : ℕ
h : I ⊔ J = ⊤
⊢ I ^ n ⊔ J = ⊤
have rw : J ⊔ I ^ n = ⊤
Tactic: rw [sup_comm, sup_pow_eq_top' (sup_comm I J ▸ h)]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : Semiring R
I J : Ideal R
inst_1 : I.IsTwoSided
n : ℕ
h : I ⊔ J = ⊤
rw : J ⊔ I ^ n = ⊤
⊢ I ^ n ⊔ J = ⊤
have rw₁ : Eq.{u + 1} (α := Ideal R) ⊤ ⊤
Tactic: rw [sup_comm, sup_pow_eq_top' (sup_comm I J ▸ h)]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : Semiring R
I J : Ideal R
inst_1 : J.IsTwoSided
n : ℕ
h : I ⊔ J = ⊤
⊢ I ^ n ⊔ J = ⊤
have rw : J ⊔ I ^ n = ⊤
Tactic: rw [sup_comm, sup_pow_eq_top (sup_comm I J ▸ h)]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : Semiring R
I J : Ideal R
inst_1 : J.IsTwoSided
n : ℕ
h : I ⊔ J = ⊤
rw : J ⊔ I ^ n = ⊤
⊢ I ^ n ⊔ J = ⊤
have rw₁ : Eq.{u + 1} (α := Ideal R) ⊤ ⊤
Tactic: rw [sup_comm, sup_pow_eq_top (sup_comm I J ▸ h)]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : Semiring R
w x y z : R
inst_1 : IsTwoSided (α := R) (span {w, x})
⊢ HMul.hMul (α := Ideal R) (span {w, x}) (span {y, z}) = span {w * y, w * z, x * y, x * z}
have rw : Eq (α := Ideal R) (span (HMul.hMul (α := Set R) {w, x} {y, z})) (span {w * y, w * z, x * y, x * z})
Tactic: rw [span_mul_span']
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : Semiring R
w x y z : R
inst_1 : IsTwoSided (α := R) (span {w, x})
⊢ Eq (α := Ideal R) (span (HMul.hMul (α := Set R) {w, x} {y, z})) (span {w * y, w * z, x * y, x * z})
have e_s : HMul.hMul (α := Set R) {w, x} {y, z} = {w * y, w * z, x * y, x * z}
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : Semiring R
w x y z : R
inst_1 : IsTwoSided (α := R) (span {w, x})
⊢ HMul.hMul (α := Set R) {w, x} {y, z} = {w * y, w * z, x * y, x * z}
have 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
Tactic: ext r
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : Semiring R
n_1 n : ℕ
ih : HPow.hPow (α := Ideal R) ⊤ n = ⊤
⊢ HPow.hPow (α := Ideal R) ⊤ n.succ = ⊤
have rw : HPow.hPow (α := Submodule R R) ⊤ n * ⊤ = ⊤
Tactic: rw [Submodule.pow_succ, ih, top_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : Semiring R
n_1 n : ℕ
ih : HPow.hPow (α := Ideal R) ⊤ n = ⊤
rw : HPow.hPow (α := Submodule R R) ⊤ n * ⊤ = ⊤
⊢ HPow.hPow (α := Ideal R) ⊤ n.succ = ⊤
have rw₁ : HMul.hMul (α := Submodule R R) ⊤ ⊤ = ⊤
Tactic: rw [Submodule.pow_succ, ih, top_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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) ⊤ ⊤ = ⊤
⊢ HPow.hPow (α := Ideal R) ⊤ n.succ = ⊤
have rw₂ : Eq.{u + 1} (α := Ideal R) ⊤ ⊤
Tactic: rw [Submodule.pow_succ, ih, top_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : Semiring R
I : Ideal R
n : ℕ
⊢ I ^ n = ⊤ ↔ I = ⊤ ∨ n = 0
have refine : I = ⊤ ∨ n = 0 → I ^ n = ⊤
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, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : Semiring R
I : Ideal R
n : ℕ
h : I = ⊤
⊢ I ^ n = ⊤
have inl : HPow.hPow (α := Ideal R) ⊤ n = ⊤
Tactic: rw [h, top_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : Semiring R
I : Ideal R
n : ℕ
h : I = ⊤
inl : HPow.hPow (α := Ideal R) ⊤ n = ⊤
⊢ I ^ n = ⊤
have inl₁ : Eq.{u + 1} (α := Ideal R) ⊤ ⊤
Tactic: rw [h, top_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : Semiring R
I : Ideal R
n : ℕ
h : n = 0
⊢ I ^ n = ⊤
have inr : HPow.hPow (β := ℕ) I 0 = ⊤
Tactic: rw [h, Submodule.pow_zero, one_eq_top]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : Semiring R
I : Ideal R
n : ℕ
h : n = 0
inr : HPow.hPow (β := ℕ) I 0 = ⊤
⊢ I ^ n = ⊤
have inr₁ : Eq.{u + 1} (α := Ideal R) 1 ⊤
Tactic: rw [h, Submodule.pow_zero, one_eq_top]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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 ⊤
⊢ I ^ n = ⊤
have inr₂ : Eq.{u + 1} (α := Ideal R) ⊤ ⊤
Tactic: rw [h, Submodule.pow_zero, one_eq_top]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : Semiring R
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) ⊤
have 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) ⊤
Tactic: obtain rfl | n := n
Cleared hypotheses: n, ih, hn
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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) ⊤
⊢ Eq.{u + 1} (α := Ideal R) (↑(n + 1) : Ideal R) ⊤
have 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) ⊤
Tactic: obtain rfl | n := n
Cleared hypotheses: n, ih, hn
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ Eq.{u + 1} (α := Ideal R) (↑(HAdd.hAdd (α := ℕ) 0 1) : Ideal R) ⊤
have succ : Eq.{u + 1} (α := Ideal R) 1 ⊤
Tactic: rw [Nat.cast_one, one_eq_top]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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 ⊤
⊢ Eq.{u + 1} (α := Ideal R) (↑(HAdd.hAdd (α := ℕ) 0 1) : Ideal R) ⊤
have succ₁ : Eq.{u + 1} (α := Ideal R) ⊤ ⊤
Tactic: rw [Nat.cast_one, one_eq_top]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ Eq.{u + 1} (α := Ideal R) (↑(n + 1 + 1) : Ideal R) ⊤
have succ : HAdd.hAdd (α := Ideal R) (↑(n + 1) : Ideal R) 1 = ⊤
Tactic: rw [Nat.cast_succ, ih n.succ_ne_zero, add_eq_sup, top_sup_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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 = ⊤
⊢ Eq.{u + 1} (α := Ideal R) (↑(n + 1 + 1) : Ideal R) ⊤
have succ₁ : HAdd.hAdd (α := Ideal R) ⊤ 1 = ⊤
Tactic: rw [Nat.cast_succ, ih n.succ_ne_zero, add_eq_sup, top_sup_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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 = ⊤
⊢ Eq.{u + 1} (α := Ideal R) (↑(n + 1 + 1) : Ideal R) ⊤
have succ₂ : Eq.{u + 1} (α := Ideal R) (⊤ ⊔ 1) ⊤
Tactic: rw [Nat.cast_succ, ih n.succ_ne_zero, add_eq_sup, top_sup_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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) ⊤
⊢ Eq.{u + 1} (α := Ideal R) (↑(n + 1 + 1) : Ideal R) ⊤
have succ₃ : Eq.{u + 1} (α := Ideal R) ⊤ ⊤
Tactic: rw [Nat.cast_succ, ih n.succ_ne_zero, add_eq_sup, top_sup_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
hn : n ≠ 0
⊢ Eq.{u + 1} (α := Ideal R) (↑n : Ideal R) ⊤
have zero : ∀ (hn : Ne (α := ℕ) 0 0), Eq.{u + 1} (α := Ideal R) (↑0 : 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]
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
hn : n ≠ 0
zero : ∀ (hn : Ne (α := ℕ) 0 0), Eq.{u + 1} (α := Ideal R) (↑0 : Ideal R) ⊤
⊢ Eq.{u + 1} (α := Ideal R) (↑n : Ideal R) ⊤
have 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) ⊤
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]
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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)
have refine_1 : (∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → x i ∈ I i) →
  Membership.mem (γ := Ideal R) (∏ i ∈ ∅, I i) (∏ i ∈ ∅, x i)
Tactic: refine Finset.induction_on s ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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)
⊢ (∀ i ∈ s, x i ∈ I i) → Membership.mem (γ := Ideal R) (∏ i ∈ s, I i) (∏ i ∈ s, x i)
have 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)
Tactic: refine Finset.induction_on s ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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)
have refine_1 : (∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → x i ∈ I i) →
  Membership.mem (γ := Ideal R) (∏ i ∈ ∅, I i) (∏ i ∈ ∅, x i)
Tactic: classical
    refine Finset.induction_on s ?_ ?_
    · grind [Submodule.mem_top]
    · grind [mul_mem_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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)
⊢ (∀ i ∈ s, x i ∈ I i) → Membership.mem (γ := Ideal R) (∏ i ∈ s, I i) (∏ i ∈ s, x i)
have 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)
Tactic: classical
    refine Finset.induction_on s ?_ ?_
    · grind [Submodule.mem_top]
    · grind [mul_mem_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
n m : ℕ
⊢ (I ⊔ J) ^ (n + m) ≤ I ^ n ⊔ J ^ m
have 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
Tactic: rw [← Ideal.add_eq_sup, ← Ideal.add_eq_sup, add_pow, Ideal.sum_eq_sup]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
n 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
have a : ∀ b ∈ Finset.range (n + m + 1), I ^ b * J ^ (n + m - b) * (↑((n + m).choose b) : Ideal R) ≤ I ^ n + J ^ m
Tactic: apply Finset.sup_le
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
n m i : ℕ
hi : i ∈ Finset.range (n + m + 1)
⊢ I ^ i * J ^ (n + m - i) * (↑((n + m).choose i) : Ideal R) ≤ I ^ n + J ^ m
have pos : ∀ (hn : n ≤ i), I ^ i * J ^ (n + m - i) * (↑((n + m).choose i) : Ideal R) ≤ I ^ n + J ^ m
Tactic: by_cases hn : n ≤ i
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ I ^ i * J ^ (n + m - i) * (↑((n + m).choose i) : Ideal R) ≤ I ^ n + J ^ m
have neg : ∀ (hn : ¬n ≤ i), I ^ i * J ^ (n + m - i) * (↑((n + m).choose i) : Ideal R) ≤ I ^ n + J ^ m
Tactic: by_cases hn : n ≤ i
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
have neg : m ≤ n + m - i
Tactic: refine (Ideal.mul_le_right.trans (Ideal.mul_le_left.trans
      ((Ideal.pow_le_pow_right ?_).trans le_sup_right)))
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
have simp_rw : (∀ zI ∈ I, ∃ zJ ∈ J, x * zI = x * zJ) ↔ I ≤ J
Tactic: simp_rw [span_singleton_mul_le_span_singleton_mul, mul_right_inj' hx,
    exists_eq_right', SetLike.le_def]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ span {x} * I ≤ span {x} * J ↔ I ≤ J
have simp_rw₁ : (∀ zI ∈ I, ∃ zJ ∈ J, zI = zJ) ↔ I ≤ J
Tactic: simp_rw [span_singleton_mul_le_span_singleton_mul, mul_right_inj' hx,
    exists_eq_right', SetLike.le_def]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ span {x} * I ≤ span {x} * J ↔ I ≤ J
have simp_rw₂ : (∀ zI ∈ I, zI ∈ J) ↔ I ≤ J
Tactic: simp_rw [span_singleton_mul_le_span_singleton_mul, mul_right_inj' hx,
    exists_eq_right', SetLike.le_def]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
ι : Type u_2
s : Finset ι
I : ι → R
hI : (↑s : Set ι).Pairwise (IsCoprime on I)
⊢ Eq (α := Ideal R) (s.inf fun (i : ι) ↦ span {I i}) (span {∏ i ∈ s, I i})
have h : ∀ (x : R),
  Membership.mem (γ := Ideal R) (s.inf fun (i : ι) ↦ span {I i}) x ↔
    Membership.mem (γ := Ideal R) (span {∏ i ∈ s, I i}) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
ι : Type u_2
s : Finset ι
I : ι → R
hI : (↑s : Set ι).Pairwise (IsCoprime on I)
x : R
⊢ Membership.mem (γ := Ideal R) (s.inf fun (i : ι) ↦ span {I i}) x ↔
    Membership.mem (γ := Ideal R) (span {∏ i ∈ s, I i}) x
have h : (∀ i ∈ s, I i ∣ x) ↔ ∏ i ∈ s, I i ∣ x
Tactic: simp only [Submodule.mem_finsetInf, Ideal.mem_span_singleton]