awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
I : Ideal R
inst_3 : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ HSMul.hSMul (β := Submodule R M) I (span R (Set.range f))
c : R
a : ι →₀ R
ha : ∀ (i : ι), Membership.mem (α := R) I ((a : (a : ι) → R) i : R)
⊢ ∃ (a_1 : ι →₀ R) (_ : ∀ (i : ι), Membership.mem (α := R) I ((a_1 : (a : ι) → R) i : R)),
    (a_1.sum fun (i : ι) (c : R) ↦ c • f i) = HSMul.hSMul (β := M) c (a.sum fun (i : ι) (c : R) ↦ c • f i)
have mp : ((c • a).sum fun (i : ι) (c : R) ↦ c • f i) = HSMul.hSMul (β := M) c (a.sum fun (i : ι) (c : R) ↦ c • f i)
Tactic: refine ⟨c • a, fun i => I.mul_mem_left c (ha i), ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
I : Ideal R
inst_3 : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ HSMul.hSMul (β := Submodule R M) I (span R (Set.range f))
c : R
a : ι →₀ R
ha : ∀ (i : ι), Membership.mem (α := R) I ((a : (a : ι) → R) i : R)
⊢ ((c • a).sum fun (i : ι) (c : R) ↦ c • f i) = HSMul.hSMul (β := M) c (a.sum fun (i : ι) (c : R) ↦ c • f i)
have mp : Eq.{v + 1} (α := M) (a.sum fun (i : ι) (a : R) ↦ (c * a) • f i) (a.sum fun (a : ι) (b : R) ↦ c • b • f a)
Tactic: rw [Finsupp.sum_smul_index, Finsupp.smul_sum]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
I : Ideal R
inst_3 : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ HSMul.hSMul (β := Submodule R M) I (span R (Set.range f))
c : R
a : ι →₀ R
ha : ∀ (i : ι), Membership.mem (α := R) I ((a : (a : ι) → R) i : R)
mp : Eq.{v + 1} (α := M) (a.sum fun (i : ι) (a : R) ↦ (c * a) • f i) (a.sum fun (a : ι) (b : R) ↦ c • b • f a)
⊢ ((c • a).sum fun (i : ι) (c : R) ↦ c • f i) = HSMul.hSMul (β := M) c (a.sum fun (i : ι) (c : R) ↦ c • f i)
have mp₁ : ∀ (i : ι), HSMul.hSMul.{u, v, v} (α := R) 0 (f i) = 0
Tactic: rw [Finsupp.sum_smul_index, Finsupp.smul_sum]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
I : Ideal R
inst_3 : I.IsTwoSided
ι : Type u_4
s : Set ι
f : ι → M
x : M
⊢ x ∈ HSMul.hSMul (β := Submodule R M) I (span R (f '' s)) ↔
    ∃ (a : Finsupp.{u_4, u} (↑s : Type u_4) R) (_ :
      ∀ (i : (↑s : Type u_4)), Membership.mem (α := R) I ((a : (a : (↑s : Type u_4)) → R) i : R)),
      (a.sum fun (i : (↑s : Type u_4)) (c : R) ↦ c • f (↑i : ι)) = x
have rw : x ∈ HSMul.hSMul (β := Submodule R M) I (span R (f '' s)) ↔
  x ∈ HSMul.hSMul (β := Submodule R M) I (span R (Set.range fun (i : (↑s : Type u_4)) ↦ f (↑i : ι)))
Tactic: rw [← Submodule.mem_ideal_smul_span_iff_exists_sum, ← Set.image_eq_range]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
I : Ideal R
inst_3 : I.IsTwoSided
ι : Type u_4
s : Set ι
f : ι → M
x : M
rw :
  x ∈ HSMul.hSMul (β := Submodule R M) I (span R (f '' s)) ↔
    x ∈ HSMul.hSMul (β := Submodule R M) I (span R (Set.range fun (i : (↑s : Type u_4)) ↦ f (↑i : ι)))
⊢ x ∈ HSMul.hSMul (β := Submodule R M) I (span R (f '' s)) ↔
    ∃ (a : Finsupp.{u_4, u} (↑s : Type u_4) R) (_ :
      ∀ (i : (↑s : Type u_4)), Membership.mem (α := R) I ((a : (a : (↑s : Type u_4)) → R) i : R)),
      (a.sum fun (i : (↑s : Type u_4)) (c : R) ↦ c • f (↑i : ι)) = x
have rw₁ : x ∈ HSMul.hSMul (β := Submodule R M) I (span R (f '' s)) ↔ x ∈ HSMul.hSMul (β := Submodule R M) I (span R (f '' s))
Tactic: rw [← Submodule.mem_ideal_smul_span_iff_exists_sum, ← Set.image_eq_range]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
M : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
N : Submodule R M
| HSMul.hSMul (α := Ideal R) (Ideal.span {r}) N
have rw : span R (HSMul.hSMul (α := Set R) {r} (↑N : Set M))
Tactic: rw [← span_eq N, span_smul_span]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
M : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
N : Submodule R M
⊢ HSMul.hSMul (α := Ideal R) (Ideal.span {r}) N = r • N
have conv_lhs : span R (HSMul.hSMul (α := Set R) {r} (↑N : Set M)) = r • N
Tactic: conv_lhs => rw [← span_eq N, span_smul_span]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
M : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Submodule R M
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
x : M
H : ∀ (r : (↑s : Type u)), ∃ (n : ℕ), (↑r : R) ^ n • x ∈ M'
⊢ x ∈ M'
have choose : ∀ (f : (r : (↑s : Type u)) → ℕ) (hf : ∀ (r : (↑s : Type u)), (↑r : R) ^ f r • x ∈ M'), x ∈ M'
Tactic: choose f hf using H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
M : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Submodule R M
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
x : M
f : (r : (↑s : Type u)) → ℕ
hf : ∀ (r : (↑s : Type u)), (↑r : R) ^ f r • x ∈ M'
⊢ x ∈ M'
have H : ∀ (r : (↑(Set.range fun (x : (↑s : Type u)) ↦ (↑x : R) ^ f x) : Type u)), (↑r : R) • x ∈ M'
Tactic: apply M'.mem_of_span_top_of_smul_mem _ (Ideal.span_range_pow_eq_top s hs f)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
M : Type v
M' : Type u_1
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
r : R
N : Submodule R M
f : M →ₗ[R] M'
⊢ map f (r • N) = r • map f N
have simp_rw : map f (HSMul.hSMul (α := Ideal R) (Ideal.span {r}) N) = HSMul.hSMul (α := Ideal R) (Ideal.span {r}) (map f N)
Tactic: simp_rw [← ideal_span_singleton_smul, map_smul'']
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : Semiring R
⊢ Eq.{u + 1} (α := Ideal R) 1 ⊤
have rw : Eq (α := Ideal R) (R ∙ 1) ⊤
Tactic: rw [Submodule.one_eq_span, ← Ideal.span, Ideal.span_singleton_one]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : Semiring R
rw : Eq (α := Ideal R) (R ∙ 1) ⊤
⊢ Eq.{u + 1} (α := Ideal R) 1 ⊤
have rw₁ : Eq (α := Ideal R) (span {1}) ⊤
Tactic: rw [Submodule.one_eq_span, ← Ideal.span, Ideal.span_singleton_one]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : Semiring R
rw : Eq (α := Ideal R) (R ∙ 1) ⊤
rw₁ : Eq (α := Ideal R) (span {1}) ⊤
⊢ Eq.{u + 1} (α := Ideal R) 1 ⊤
have rw₂ : Eq.{u + 1} (α := Ideal R) ⊤ ⊤
Tactic: rw [Submodule.one_eq_span, ← Ideal.span, Ideal.span_singleton_one]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : Semiring R
I J : Ideal R
⊢ I + J = 1 ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = 1
have rw : I + J = ⊤ ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = 1
Tactic: rw [one_eq_top, eq_top_iff_one, add_eq_sup, Submodule.mem_sup]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : Semiring R
I J : Ideal R
rw : I + J = ⊤ ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = 1
⊢ I + J = 1 ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = 1
have rw₁ : 1 ∈ I + J ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = 1
Tactic: rw [one_eq_top, eq_top_iff_one, add_eq_sup, Submodule.mem_sup]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : Semiring R
I J : Ideal R
rw : I + J = ⊤ ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = 1
rw₁ : 1 ∈ I + J ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = 1
⊢ I + J = 1 ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = 1
have rw₂ : 1 ∈ I ⊔ J ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = 1
Tactic: rw [one_eq_top, eq_top_iff_one, add_eq_sup, Submodule.mem_sup]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : Semiring R
I J : Ideal R
rw : I + J = ⊤ ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = 1
rw₁ : 1 ∈ I + J ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = 1
rw₂ : 1 ∈ I ⊔ J ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = 1
⊢ I + J = 1 ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = 1
have rw₃ : (∃ y ∈ I, ∃ z ∈ J, y + z = 1) ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = 1
Tactic: rw [one_eq_top, eq_top_iff_one, add_eq_sup, Submodule.mem_sup]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : Semiring R
I : Ideal R
m n : ℕ
h : m ≤ n
⊢ I ^ n ≤ I ^ m
have zero : ∀ (h : 0 ≤ n), I ^ n ≤ HPow.hPow (β := ℕ) I 0
Tactic: obtain _ | m := m
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ I ^ n ≤ I ^ m
have succ : ∀ (m : ℕ) (h : m + 1 ≤ n), I ^ n ≤ I ^ (m + 1)
Tactic: obtain _ | m := m
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : Semiring R
I : Ideal R
n : ℕ
h : 0 ≤ n
⊢ I ^ n ≤ HPow.hPow (β := ℕ) I 0
have zero : I ^ n ≤ ⊤
Tactic: rw [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 m : ℕ
h : m + 1 ≤ n
⊢ I ^ n ≤ I ^ (m + 1)
have succ : ∀ (n : ℕ) (h : m + 1 ≤ m + 1 + n), I ^ (m + 1 + n) ≤ I ^ (m + 1)
Tactic: obtain ⟨n, rfl⟩ := Nat.exists_eq_add_of_le h
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : Semiring R
I : Ideal R
m n : ℕ
h : m + 1 ≤ m + 1 + n
⊢ I ^ (m + 1 + n) ≤ I ^ (m + 1)
have succ : I ^ n * I ^ (m + 1) ≤ I ^ (m + 1)
Tactic: rw [add_comm, Submodule.pow_add _ m.add_one_ne_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : Semiring R
I J : Ideal R
e : I ≤ J
⊢ HPow.hPow (β := ℕ) I 0 ≤ HPow.hPow (β := ℕ) J 0
have zero : 1 ≤ HPow.hPow (β := ℕ) J 0
Tactic: rw [Submodule.pow_zero, Submodule.pow_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : Semiring R
I J : Ideal R
e : I ≤ J
zero : 1 ≤ HPow.hPow (β := ℕ) J 0
⊢ HPow.hPow (β := ℕ) I 0 ≤ HPow.hPow (β := ℕ) J 0
have zero₁ : LE.le.{u} (α := Ideal R) 1 1
Tactic: rw [Submodule.pow_zero, Submodule.pow_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : Semiring R
I J : Ideal R
e : I ≤ J
n : ℕ
hn : I ^ n ≤ J ^ n
⊢ I ^ (n + 1) ≤ J ^ (n + 1)
have succ : I ^ n * I ≤ J ^ n * J
Tactic: rw [Submodule.pow_succ, Submodule.pow_succ]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : Semiring R
I J : Ideal R
e : I ≤ J
n : ℕ
⊢ I ^ n ≤ J ^ n
have zero : HPow.hPow (β := ℕ) I 0 ≤ HPow.hPow (β := ℕ) J 0
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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : Semiring R
I J : Ideal R
e : I ≤ J
n : ℕ
zero : HPow.hPow (β := ℕ) I 0 ≤ HPow.hPow (β := ℕ) J 0
⊢ I ^ n ≤ J ^ n
have succ : ∀ (n : ℕ) (hn : I ^ n ≤ J ^ n), I ^ (n + 1) ≤ J ^ (n + 1)
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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
have rw : i * (j * b) ∈ I * J
Tactic: rw [mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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 + y) * b ∈ I * J
have rw : x * b + y * b ∈ I * J
Tactic: rw [right_distrib]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : Semiring R
I J K L : Ideal R
inst_1 : I.IsTwoSided
m n : ℕ
⊢ (I ^ Nat.zero).IsTwoSided
have rw : IsTwoSided.{u} (α := R) ⊤
Tactic: rw [Submodule.pow_zero, one_eq_top]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : Semiring R
I J K L : Ideal R
inst_1 : I.IsTwoSided
m n x : ℕ
h : (I ^ x).IsTwoSided
⊢ (I ^ x.succ).IsTwoSided
have rw : IsTwoSided (I ^ x * I)
Tactic: rw [Submodule.pow_succ]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : Semiring R
I : Ideal R
inst_1 : I.IsTwoSided
m n : ℕ
⊢ I ^ (m + n) = I ^ m * I ^ n
have inl : I ^ (m + 0) = I ^ m * HPow.hPow (β := ℕ) I 0
Tactic: obtain rfl | h := eq_or_ne n 0
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ I ^ (m + n) = I ^ m * I ^ n
have inr : ∀ (h : n ≠ 0), I ^ (m + n) = I ^ m * I ^ n
Tactic: obtain rfl | h := eq_or_ne n 0
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : Semiring R
I : Ideal R
inst_1 : I.IsTwoSided
m : ℕ
⊢ I ^ (m + 0) = I ^ m * HPow.hPow (β := ℕ) I 0
have inl : I ^ m = I ^ m * HPow.hPow (β := ℕ) I 0
Tactic: rw [add_zero, Submodule.pow_zero, IsTwoSided.mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : Semiring R
I : Ideal R
inst_1 : I.IsTwoSided
m : ℕ
inl : I ^ m = I ^ m * HPow.hPow (β := ℕ) I 0
⊢ I ^ (m + 0) = I ^ m * HPow.hPow (β := ℕ) I 0
have inl₁ : I ^ m = I ^ m * 1
Tactic: rw [add_zero, Submodule.pow_zero, IsTwoSided.mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ I ^ (m + 0) = I ^ m * HPow.hPow (β := ℕ) I 0
have inl₂ : I ^ m = I ^ m
Tactic: rw [add_zero, Submodule.pow_zero, IsTwoSided.mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : Semiring R
I : Ideal R
inst_1 : I.IsTwoSided
n : ℕ
⊢ I ^ (n + 1) = I * I ^ n
have rw : I ^ (1 + n) = I * I ^ n
Tactic: rw [add_comm, IsTwoSided.pow_add, Submodule.pow_one]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : Semiring R
I : Ideal R
inst_1 : I.IsTwoSided
n : ℕ
rw : I ^ (1 + n) = I * I ^ n
⊢ I ^ (n + 1) = I * I ^ n
have rw₁ : HPow.hPow (β := ℕ) I 1 * I ^ n = I * I ^ n
Tactic: rw [add_comm, IsTwoSided.pow_add, Submodule.pow_one]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ I ^ (n + 1) = I * I ^ n
have rw₂ : I * I ^ n = I * I ^ n
Tactic: rw [add_comm, IsTwoSided.pow_add, Submodule.pow_one]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : Semiring R
r s : R
inst_1 : IsTwoSided (α := R) (span {r})
⊢ HMul.hMul (α := Ideal R) (span {r}) (span {s}) = span {r * s}
have rw : Eq (α := Ideal R) (span (HMul.hMul (α := Set R) {r} {s})) (span {r * s})
Tactic: rw [span_mul_span', Set.singleton_mul_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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})
⊢ HMul.hMul (α := Ideal R) (span {r}) (span {s}) = span {r * s}
have rw₁ : Eq (α := Ideal R) (span {r * s}) (span {r * s})
Tactic: rw [span_mul_span', Set.singleton_mul_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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}
⊢ HPow.hPow (α := Ideal R) (span {s}) (n + 1) = span {s ^ (n + 1)}
have 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}
Tactic: obtain rfl | ne := 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
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}
⊢ HPow.hPow (α := Ideal R) (span {s}) (n + 1) = span {s ^ (n + 1)}
have succ₁ : ∀ (ne : n ≠ 0), HPow.hPow (α := Ideal R) (span {s}) (n + 1) = span {s ^ (n + 1)}
Tactic: obtain rfl | ne := eq_or_ne n 0
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : Semiring R
s : R
inst_1 : IsTwoSided (α := R) (span {s})
n : ℕ
⊢ HPow.hPow (α := Ideal R) (span {s}) n = span {s ^ n}
have zero : HPow.hPow (α := Ideal R) (β := ℕ) (span {s}) 0 = span {HPow.hPow (β := ℕ) s 0}
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]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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}
⊢ HPow.hPow (α := Ideal R) (span {s}) n = span {s ^ n}
have 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)}
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]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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 ≠ ⊥
have grw : ¬(I = ⊥ ∨ J = ⊥)
Tactic: grw [← bot_lt_iff_ne_bot, ← mul_le_inf, bot_lt_iff_ne_bot, Ne, mul_eq_bot]
-- 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 : I ⊔ J = ⊤
i : R
hi : i ∈ I ⊔ K
⊢ i ∈ I ⊔ J * K
have rw : ∀ (h : 1 ∈ I ⊔ J) (i : R) (hi : i ∈ I ⊔ K), i ∈ I ⊔ J * K
Tactic: rw [eq_top_iff_one] at h
Cleared hypotheses: h, i, hi
-- 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 : 1 ∈ I ⊔ J
i : R
hi : i ∈ I ⊔ K
⊢ i ∈ I ⊔ J * K
have 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
Tactic: rw [Submodule.mem_sup] at h hi ⊢
Cleared hypotheses: h, i, hi
-- 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 : ∃ 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
have obtain : ∀ (i1 : R) (hi1 : i1 ∈ I) (j : R) (hj : j ∈ J) (h : i1 + j = 1), ∃ y ∈ I, ∃ z ∈ J * K, y + z = i
Tactic: obtain ⟨i1, hi1, j, hj, h⟩ := 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
i : R
hi : ∃ y ∈ I, ∃ z ∈ K, y + z = i
i1 : R
hi1 : i1 ∈ I
j : R
hj : j ∈ J
h : i1 + j = 1
⊢ ∃ y ∈ I, ∃ z ∈ J * K, y + z = i
have obtain : ∀ (i' : R) (hi' : i' ∈ I) (k : R) (hk : k ∈ K), ∃ y ∈ I, ∃ z ∈ J * K, y + z = i' + k
Tactic: obtain ⟨i', hi', k, hk, rfl⟩ := hi
Cleared hypotheses: i, hi
-- 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
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
have refine : i' + i1 * k + j * k = i' + k
Tactic: refine ⟨_, add_mem hi' (mul_mem_right k _ hi1), _, mul_mem_mul hj hk, ?_⟩
-- 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
i1 : R
hi1 : i1 ∈ I
j : R
hj : j ∈ J
h : i1 + j = 1
i' : R
hi' : i' ∈ I
k : R
hk : k ∈ K
⊢ i' + i1 * k + j * k = i' + k
have rw : i' + (i1 * k + j * k) = i' + k
Tactic: rw [add_assoc, ← add_mul, h, one_mul]
-- 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
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
⊢ i' + i1 * k + j * k = i' + k
have rw₁ : i' + (i1 + j) * k = i' + k
Tactic: rw [add_assoc, ← add_mul, h, one_mul]
-- 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
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
⊢ i' + i1 * k + j * k = i' + k
have rw₂ : i' + 1 * k = i' + k
Tactic: rw [add_assoc, ← add_mul, h, one_mul]
-- 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
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
⊢ i' + i1 * k + j * k = i' + k
have rw₃ : i' + k = i' + k
Tactic: rw [add_assoc, ← add_mul, h, one_mul]
-- 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 : I ⊔ K = ⊤
i : R
hi : i ∈ I ⊔ J
⊢ i ∈ I ⊔ J * K
have rw : ∀ (h : 1 ∈ I ⊔ K) (i : R) (hi : i ∈ I ⊔ J), i ∈ I ⊔ J * K
Tactic: rw [eq_top_iff_one] at h
Cleared hypotheses: h, i, hi
-- 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 : 1 ∈ I ⊔ K
i : R
hi : i ∈ I ⊔ J
⊢ i ∈ I ⊔ J * K
have 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
Tactic: rw [Submodule.mem_sup] at h hi ⊢
Cleared hypotheses: h, i, hi
-- 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 : ∃ 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
have obtain : ∀ (i1 : R) (hi1 : i1 ∈ I) (k : R) (hk : k ∈ K) (h : i1 + k = 1), ∃ y ∈ I, ∃ z ∈ J * K, y + z = i
Tactic: obtain ⟨i1, hi1, k, hk, h⟩ := 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
i : R
hi : ∃ y ∈ I, ∃ z ∈ J, y + z = i
i1 : R
hi1 : i1 ∈ I
k : R
hk : k ∈ K
h : i1 + k = 1
⊢ ∃ y ∈ I, ∃ z ∈ J * K, y + z = i
have obtain : ∀ (i' : R) (hi' : i' ∈ I) (j : R) (hj : j ∈ J), ∃ y ∈ I, ∃ z ∈ J * K, y + z = i' + j
Tactic: obtain ⟨i', hi', j, hj, rfl⟩ := hi
Cleared hypotheses: i, hi
-- 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
⊢ ∃ y ∈ I, ∃ z ∈ J * K, y + z = i' + j
have refine : i' + j * i1 + j * k = i' + j
Tactic: refine ⟨_, add_mem hi' (mul_mem_left _ j hi1), _, mul_mem_mul hj hk, ?_⟩
-- 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
⊢ i' + j * i1 + j * k = i' + j
have rw : i' + (j * i1 + j * k) = i' + j
Tactic: rw [add_assoc, ← mul_add, h, mul_one]