awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (hypothesis)
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
s : Finset ι
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
this : (↑I : Set R) ⊆ ⋃ i ∈ (↑s : Set ι), (↑(f i) : Set R) → ∃ i ∈ s, I ≤ f i
⊢ (↑I : Set R) ⊆ ⋃ i ∈ (↑s : Set ι), (↑(f i) : Set R) ↔ ∃ i ∈ s, I ≤ f i
have aux : ∀ (h : (↑I : Set R) ⊆ ⋃ i ∈ (↑s : Set ι), (↑(f i) : Set R)), ∃ (x : ι) (_ : x ∈ s), I ≤ f x
Tactic: have aux := fun h => (bex_def.2 <| this h)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
s : Finset ι
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
this aux : ∀ (h : (↑I : Set R) ⊆ ⋃ i ∈ (↑s : Set ι), (↑(f i) : Set R)), ∃ x ∈ s, I ≤ f x
⊢ (↑I : Set R) ⊆ ⋃ i ∈ (↑s : Set ι), (↑(f i) : Set R) ↔ ∃ i ∈ s, I ≤ f i
have refine : (∃ i ∈ s, I ≤ f i) → ∀ (i : ι) (his : i ∈ s) (hi : I ≤ f i), (↑(f i) : Set R) ⊆ ⋃ i ∈ (↑s : Set ι), (↑(f i) : Set R)
Tactic: refine ⟨aux, fun ⟨i, his, hi⟩ ↦ Set.Subset.trans hi ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u_2
ι : Type u_3
inst : CommRing R
s : Set ι
hs : s.Finite
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
⊢ (↑I : Set R) ⊆ ⋃ i ∈ s, (↑(f i) : Set R) ↔ ∃ i ∈ s, I ≤ f i
have rcases : ∀ (t : Finset ι) (ht : ∀ (a : ι), a ∈ t ↔ a ∈ s), (↑I : Set R) ⊆ ⋃ i ∈ s, (↑(f i) : Set R) ↔ ∃ i ∈ s, I ≤ f i
Tactic: rcases Set.Finite.exists_finset hs with ⟨t, ht⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u_2
ι : Type u_3
inst : CommRing R
s : Set ι
hs : s.Finite
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
t : Finset ι
ht : ∀ (a : ι), a ∈ t ↔ a ∈ s
⊢ Eq.{u_2 + 1} (α := Set R) (⋃ i ∈ s, (↑(f i) : Set R)) (⋃ i ∈ t, (↑(f i) : Set R))
have h : ∀ (x : R),
  Membership.mem (γ := Set R) (⋃ i ∈ s, (↑(f i) : Set R)) x ↔ Membership.mem (γ := Set R) (⋃ i ∈ t, (↑(f i) : Set R)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (hypothesis)
Goal:
R : Type u_2
ι : Type u_3
inst : CommRing R
s : Set ι
hs : s.Finite
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
t : Finset ι
ht : ∀ (a : ι), a ∈ t ↔ a ∈ s
⊢ (↑I : Set R) ⊆ ⋃ i ∈ s, (↑(f i) : Set R) ↔ ∃ i ∈ s, I ≤ f i
have heq : Eq.{u_2 + 1} (α := Set R) (⋃ i ∈ s, (↑(f i) : Set R)) (⋃ i ∈ t, (↑(f i) : Set R))
Tactic: have heq : ⋃ i ∈ s, f i = ⋃ i ∈ t, (f i : Set R) := by
    ext
    simpa using exists_congr (fun i ↦ (and_congr_left fun a ↦ ht i).symm)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (hypothesis)
Goal:
R : Type u_2
ι : Type u_3
inst : CommRing R
s : Set ι
hs : s.Finite
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
t : Finset ι
ht : ∀ (a : ι), a ∈ t ↔ a ∈ s
heq : Eq.{u_2 + 1} (α := Set R) (⋃ i ∈ s, (↑(f i) : Set R)) (⋃ i ∈ t, (↑(f i) : Set R))
⊢ (↑I : Set R) ⊆ ⋃ i ∈ s, (↑(f i) : Set R) ↔ ∃ i ∈ s, I ≤ f i
have hmem_union : (↑I : Set R) ⊆ ⋃ i ∈ s, (↑(f i) : Set R) ↔ (↑I : Set R) ⊆ ⋃ i ∈ (↑t : Set ι), (↑(f i) : Set R)
Tactic: have hmem_union : ((I : Set R) ⊆ ⋃ i ∈ s, f i) ↔ ((I : Set R) ⊆ ⋃ i ∈ (t : Set ι), f i) :=
    (congrArg _ heq).to_iff
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u_2
ι : Type u_3
inst : CommRing R
s : Set ι
hs : s.Finite
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
t : Finset ι
ht : ∀ (a : ι), a ∈ t ↔ a ∈ s
heq : Eq.{u_2 + 1} (α := Set R) (⋃ i ∈ s, (↑(f i) : Set R)) (⋃ i ∈ t, (↑(f i) : Set R))
hmem_union : (↑I : Set R) ⊆ ⋃ i ∈ s, (↑(f i) : Set R) ↔ (↑I : Set R) ⊆ ⋃ i ∈ (↑t : Set ι), (↑(f i) : Set R)
⊢ (↑I : Set R) ⊆ ⋃ i ∈ s, (↑(f i) : Set R) ↔ ∃ i ∈ s, I ≤ f i
have rw : (∃ i ∈ t, I ≤ f i) ↔ ∃ i ∈ s, I ≤ f i
Tactic: rw [hmem_union, Ideal.subset_union_prime a b (fun i hin ↦ hp i ((ht i).mp hin))]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
inst_1 : I.IsMaximal
x : R
hx : x ∉ I
n : ℕ
⊢ ∃ (y : R), ∃ i ∈ I ^ n, y * x + i = 1
have obtain : ∀ (y i : R) (hmem : i ∈ I) (hi : y * x + i = 1), ∃ (y : R), ∃ i ∈ I ^ n, y * x + i = 1
Tactic: obtain ⟨y, i, hmem, hi⟩ := Ideal.IsMaximal.exists_inv ‹_› hx
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
inst_1 : I.IsMaximal
x : R
hx : x ∉ I
y i : R
hmem : i ∈ I
hi : y * x + i = 1
n : ℕ
ih : ∃ (y : R), y * x + i ^ n = 1
⊢ ∃ (y : R), y * x + i ^ (n + 1) = 1
have succ : ∀ (z : R) (hz : z * x + i ^ n = 1), ∃ (y : R), y * x + i ^ (n + 1) = 1
Tactic: obtain ⟨z, hz⟩ := ih
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
inst_1 : I.IsMaximal
x : R
hx : x ∉ I
y i : R
hmem : i ∈ I
hi : y * x + i = 1
n : ℕ
z : R
hz : z * x + i ^ n = 1
⊢ ∃ (y : R), y * x + i ^ (n + 1) = 1
have succ : (z * i + y) * x + i ^ (n + 1) = 1
Tactic: refine ⟨z * i + y, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
inst_1 : I.IsMaximal
x : R
hx : x ∉ I
y i : R
hmem : i ∈ I
hi : y * x + i = 1
n : ℕ
z : R
hz : z * x + i ^ n = 1
⊢ (z * i + y) * x + i ^ (n + 1) = 1
have trans : (z * i + y) * x + i ^ (n + 1) = z * i * x + i * i ^ n + y * x
Tactic: trans z * i * x + i * i ^ n + y * x
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
inst_1 : I.IsMaximal
x : R
hx : x ∉ I
y i : R
hmem : i ∈ I
hi : y * x + i = 1
n : ℕ
z : R
hz : z * x + i ^ n = 1
trans : (z * i + y) * x + i ^ (n + 1) = z * i * x + i * i ^ n + y * x
⊢ (z * i + y) * x + i ^ (n + 1) = 1
have trans₁ : z * i * x + i * i ^ n + y * x = 1
Tactic: trans z * i * x + i * i ^ n + y * x
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
inst_1 : I.IsMaximal
x : R
hx : x ∉ I
y i : R
hmem : i ∈ I
hi : y * x + i = 1
n : ℕ
z : R
hz : z * x + i ^ n = 1
⊢ z * i * x + i * i ^ n + y * x = 1
have rw : y * x + i * 1 = 1
Tactic: rw [mul_comm z i, mul_assoc, ← mul_add, hz, add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
inst_1 : I.IsMaximal
x : R
hx : x ∉ I
n : ℕ
y i : R
hmem : i ∈ I
hi : y * x + i = 1
⊢ ∃ (y : R), y * x + i ^ n = 1
have zero : ∃ (y : R), y * x + HPow.hPow (β := ℕ) i 0 = 1
Tactic: induction n with
    | zero => exact ⟨0, by simp⟩
    | succ n ih =>
      obtain ⟨z, hz⟩ := ih
      refine ⟨z * i + y, ?_⟩
      trans z * i * x + i * i ^ n + y * x
      · ring
      · rw [mul_comm z i, mul_assoc, ← mul_add, hz, add_comm]
        simpa
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
inst_1 : I.IsMaximal
x : R
hx : x ∉ I
n : ℕ
y i : R
hmem : i ∈ I
hi : y * x + i = 1
zero : ∃ (y : R), y * x + HPow.hPow (β := ℕ) i 0 = 1
⊢ ∃ (y : R), y * x + i ^ n = 1
have succ : ∀ (n : ℕ) (ih : ∃ (y : R), y * x + i ^ n = 1), ∃ (y : R), y * x + i ^ (n + 1) = 1
Tactic: induction n with
    | zero => exact ⟨0, by simp⟩
    | succ n ih =>
      obtain ⟨z, hz⟩ := ih
      refine ⟨z * i + y, ?_⟩
      trans z * i * x + i * i ^ n + y * x
      · ring
      · rw [mul_comm z i, mul_assoc, ← mul_add, hz, add_comm]
        simpa
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
inst_1 : I.IsMaximal
x : R
hx : x ∉ I
n : ℕ
y i : R
hmem : i ∈ I
hi : y * x + i = 1
⊢ ∃ (y : R), ∃ i ∈ I ^ n, y * x + i = 1
have obtain : ∀ (y : R) (hy : y * x + i ^ n = 1), ∃ (y : R), ∃ i ∈ I ^ n, y * x + i = 1
Tactic: obtain ⟨y, hy⟩ : ∃ y : R, y * x + i ^ n = 1 := by
    induction n with
    | zero => exact ⟨0, by simp⟩
    | succ n ih =>
      obtain ⟨z, hz⟩ := ih
      refine ⟨z * i + y, ?_⟩
      trans z * i * x + i * i ^ n + y * x
      · ring
      · rw [mul_comm z i, mul_assoc, ← mul_add, hz, add_comm]
        simpa
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
inst_1 : I.IsMaximal
a b : R
n : ℕ
h : a * b ∈ I ^ n
⊢ a ∈ I ∨ b ∈ I ^ n
have rw : a ∉ I → b ∈ I ^ n
Tactic: rw [Classical.or_iff_not_imp_left]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
inst_1 : I.IsMaximal
a b : R
n : ℕ
h : a * b ∈ I ^ n
ha : a ∉ I
⊢ b ∈ I ^ n
have obtain : ∀ (c i : R) (hi : i ∈ I ^ n) (hc : c * a + i = 1), b ∈ I ^ n
Tactic: obtain ⟨c, i, hi, hc⟩ := exists_inv_pow I ha n
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
inst_1 : I.IsMaximal
a b : R
n : ℕ
h : a * b ∈ I ^ n
ha : a ∉ I
c i : R
hi : i ∈ I ^ n
hc : c * a + i = 1
⊢ b ∈ I ^ n
have hb : (c * a + i) * b = 1 * b
Tactic: obtain hb := congr($hc * b)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
inst_1 : I.IsMaximal
a b : R
n : ℕ
h : a * b ∈ I ^ n
ha : a ∉ I
c i : R
hi : i ∈ I ^ n
hc : c * a + i = 1
hb : (c * a + i) * b = 1 * b
⊢ b ∈ I ^ n
have hb₁ : (c * a + i) * b = b
Tactic: rw [one_mul] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
inst_1 : I.IsMaximal
a b : R
n : ℕ
h : a * b ∈ I ^ n
ha : a ∉ I
c i : R
hi : i ∈ I ^ n
hc : c * a + i = 1
hb : (c * a + i) * b = b
⊢ b ∈ I ^ n
have rw : c * (a * b) + i * b ∈ I ^ n
Tactic: rw [← hb, add_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (hypothesis)
Goal:
R : Type u_2
inst : CommSemiring R
I : Ideal R
inst_1 : I.IsMaximal
a b : R
n : ℕ
h : a * b ∈ I ^ n
⊢ a ∈ I ^ n ∨ b ∈ I
have h₁ : b * a ∈ I ^ n
Tactic: rw [mul_comm] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u_2
inst : CommSemiring R
I : Ideal R
inst_1 : I.IsMaximal
a b : R
n : ℕ
h : b * a ∈ I ^ n
⊢ a ∈ I ^ n ∨ b ∈ I
have rw : b ∈ I ∨ a ∈ I ^ n
Tactic: rw [or_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
h : I = ⊤
⊢ ⊤ = I * ⊤
have rw : ⊤ = I
Tactic: rw [mul_top, h]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
h : I = ⊤
rw : ⊤ = I
⊢ ⊤ = I * ⊤
have rw₁ : Eq.{u + 1} (α := Ideal R) ⊤ ⊤
Tactic: rw [mul_top, h]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
ι : Type u_1
inst : CommSemiring R
I J K L : Ideal R
u : (Ideal R)ˣ
⊢ (↑u : Ideal R) = 1
have rw : Eq.{u + 1} (α := Ideal R) ⊤ 1
Tactic: rw [isUnit_iff.mp u.isUnit, one_eq_top]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
ι : Type u_1
inst : CommSemiring R
I J K L : Ideal R
u : (Ideal R)ˣ
rw : Eq.{u + 1} (α := Ideal R) ⊤ 1
⊢ (↑u : Ideal R) = 1
have rw₁ : Eq.{u + 1} (α := Ideal R) ⊤ ⊤
Tactic: rw [isUnit_iff.mp u.isUnit, one_eq_top]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
ι : Type u_1
M : Type u_2
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
I : Ideal R
v : ι → M
f : Finsupp.{u_1, u_3} ι ↥I
⊢ Eq.{u_2 + 1} (α := M) ((finsuppTotal ι M I v : (a : ι →₀ ↥I) → M) f : M)
    (f.sum fun (i : ι) (x : ↥I) ↦ (↑x : R) • v i : M)
have dsimp : Eq.{u_2 + 1} (α := M)
  ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) (Finsupp.mapRange (Subtype.val (p := fun (x : R) ↦ x ∈ I)) sorry f) :
    M)
  (f.sum fun (i : ι) (x : ↥I) ↦ (↑x : R) • v i : M)
Tactic: dsimp [finsuppTotal]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
ι : Type u_1
M : Type u_2
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
I : Ideal R
v : ι → M
f : Finsupp.{u_1, u_3} ι ↥I
⊢ Eq.{u_2 + 1} (α := M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M)
        (Finsupp.mapRange (Subtype.val (p := fun (x : R) ↦ x ∈ I)) ⋯ f) :
      M)
    (f.sum fun (i : ι) (x : ↥I) ↦ (↑x : R) • v i : M)
have rw : ∀ (a : ι), HSMul.hSMul.{u_3, u_2, u_2} (α := R) 0 (v a) = 0
Tactic: rw [Finsupp.linearCombination_apply, Finsupp.sum_mapRange_index]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
ι : Type u_1
M : Type u_2
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
I : Ideal R
v : ι → M
inst_3 : Fintype ι
f : Finsupp.{u_1, u_3} ι ↥I
⊢ Eq.{u_2 + 1} (α := M) ((finsuppTotal ι M I v : (a : ι →₀ ↥I) → M) f : M)
    (∑ i : ι, HSMul.hSMul.{u_3, u_2, u_2} (α := R) (↑((f : (a : ι) → ↥I) i) : R) (v i) : M)
have h : ∀ (i : ι), HSMul.hSMul.{u_3, u_2, u_2} (α := R) (↑0 : R) (v i) = 0
Tactic: rw [finsuppTotal_apply, Finsupp.sum_fintype]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
ι : Type u_1
M : Type u_2
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
I : Ideal R
v : ι → M
⊢ LinearMap.range (finsuppTotal ι M I v) = HSMul.hSMul (β := Submodule R M) I (Submodule.span R (Set.range v))
have h : ∀ (x : M),
  Membership.mem (γ := Submodule R M) (LinearMap.range (finsuppTotal ι M I v)) x ↔
    x ∈ HSMul.hSMul (β := Submodule R M) I (Submodule.span R (Set.range v))
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
ι : Type u_1
M : Type u_2
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
I : Ideal R
v : ι → M
x : M
⊢ Membership.mem (γ := Submodule R M) (LinearMap.range (finsuppTotal ι M I v)) x ↔
    x ∈ HSMul.hSMul (β := Submodule R M) I (Submodule.span R (Set.range v))
have h : Membership.mem (γ := Submodule R M) (LinearMap.range (finsuppTotal ι M I v)) x ↔
  ∃ (a : ι →₀ R) (_ : ∀ (i : ι), Membership.mem (α := R) I ((a : (a : ι) → R) i : R)),
    (a.sum fun (i : ι) (c : R) ↦ c • v i) = x
Tactic: rw [Submodule.mem_ideal_smul_span_iff_exists_sum]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
ι : Type u_1
M : Type u_2
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
I : Ideal R
v : ι → M
x : M
⊢ Membership.mem (γ := Submodule R M) (LinearMap.range (finsuppTotal ι M I v)) x ↔
    ∃ (a : ι →₀ R) (_ : ∀ (i : ι), Membership.mem (α := R) I ((a : (a : ι) → R) i : R)),
      (a.sum fun (i : ι) (c : R) ↦ c • v i) = x
have h : (∃ (a : ι →₀ R) (_ : ∀ (i : ι), Membership.mem (α := R) I ((a : (a : ι) → R) i : R)),
    (a.sum fun (i : ι) (c : R) ↦ c • v i) = x) →
  Membership.mem (γ := Submodule R M) (LinearMap.range (finsuppTotal ι M I v)) x
Tactic: refine ⟨fun ⟨f, h⟩ => ⟨Finsupp.mapRange.linearMap I.subtype f, fun i => (f i).2, h⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
ι : Type u_1
M : Type u_2
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
I : Ideal R
v : ι → M
a : ι →₀ R
ha : ∀ (i : ι), Membership.mem (α := R) I ((a : (a : ι) → R) i : R)
⊢ Eq.{u_3 + 1} (α := ↥I) ((fun (r : R) ↦ (if h : r ∈ I then Subtype.mk (p := fun (x : R) ↦ x ∈ I) r h else 0 : ↥I)) 0) 0
have simp : Subtype.mk (p := fun (x : R) ↦ x ∈ I) 0 sorry = 0
Tactic: simp only [Submodule.zero_mem, ↓reduceDIte]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
ι : Type u_1
M : Type u_2
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
I : Ideal R
v : ι → M
a : ι →₀ R
ha : ∀ (i : ι), Membership.mem (α := R) I ((a : (a : ι) → R) i : R)
⊢ Membership.mem (γ := Submodule R M) (LinearMap.range (finsuppTotal ι M I v)) (a.sum fun (i : ι) (c : R) ↦ c • v i)
have h : Eq.{u_2 + 1} (α := M)
  ((finsuppTotal ι M I v : (a : ι →₀ ↥I) → M)
      (Finsupp.mapRange (fun (r : R) ↦ if h : r ∈ I then Subtype.mk (p := fun (x : R) ↦ x ∈ I) r h else 0) sorry a) :
    M)
  (a.sum fun (i : ι) (c : R) ↦ c • v i : M)
Tactic: refine ⟨a.mapRange (fun r => if h : r ∈ I then ⟨r, h⟩ else 0)
      (by simp only [Submodule.zero_mem, ↓reduceDIte]; rfl), ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
ι : Type u_1
M : Type u_2
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
I : Ideal R
v : ι → M
a : ι →₀ R
ha : ∀ (i : ι), Membership.mem (α := R) I ((a : (a : ι) → R) i : R)
⊢ Eq.{u_2 + 1} (α := M)
    ((finsuppTotal ι M I v : (a : ι →₀ ↥I) → M)
        (Finsupp.mapRange (fun (r : R) ↦ if h : r ∈ I then Subtype.mk (p := fun (x : R) ↦ x ∈ I) r h else 0) ⋯ a) :
      M)
    (a.sum fun (i : ι) (c : R) ↦ c • v i : M)
have h : Eq.{u_2 + 1} (α := M)
  (a.sum fun (a : ι) (b : R) ↦
    HSMul.hSMul.{u_3, u_2, u_2} (α := R) (↑(if h : b ∈ I then Subtype.mk (p := fun (x : R) ↦ x ∈ I) b h else 0) : R)
      (v a))
  (a.sum fun (i : ι) (c : R) ↦ c • v i)
Tactic: rw [finsuppTotal_apply, Finsupp.sum_mapRange_index]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
ι : Type u_1
M : Type u_2
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
I : Ideal R
v : ι → M
a : ι →₀ R
ha : ∀ (i : ι), Membership.mem (α := R) I ((a : (a : ι) → R) i : R)
h :
  Eq.{u_2 + 1} (α := M)
    (a.sum fun (a : ι) (b : R) ↦
      HSMul.hSMul.{u_3, u_2, u_2} (α := R) (↑(if h : b ∈ I then Subtype.mk (p := fun (x : R) ↦ x ∈ I) b h else 0) : R)
        (v a))
    (a.sum fun (i : ι) (c : R) ↦ c • v i)
⊢ Eq.{u_2 + 1} (α := M)
    ((finsuppTotal ι M I v : (a : ι →₀ ↥I) → M)
        (Finsupp.mapRange (fun (r : R) ↦ if h : r ∈ I then Subtype.mk (p := fun (x : R) ↦ x ∈ I) r h else 0) ⋯ a) :
      M)
    (a.sum fun (i : ι) (c : R) ↦ c • v i : M)
have h₁ : ∀ (a : ι), HSMul.hSMul.{u_3, u_2, u_2} (α := R) (↑0 : R) (v a) = 0
Tactic: rw [finsuppTotal_apply, Finsupp.sum_mapRange_index]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
ι : Type u_1
M : Type u_2
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
I : Ideal R
v : ι → M
a : ι →₀ R
ha : ∀ (i : ι), Membership.mem (α := R) I ((a : (a : ι) → R) i : R)
⊢ Eq.{u_2 + 1} (α := M)
    (a.sum fun (a : ι) (b : R) ↦
      HSMul.hSMul.{u_3, u_2, u_2} (α := R) (↑(if h : b ∈ I then Subtype.mk (p := fun (x : R) ↦ x ∈ I) b h else 0) : R)
        (v a))
    (a.sum fun (i : ι) (c : R) ↦ c • v i)
have h : ∀ x ∈ a.support,
  HSMul.hSMul.{u_3, u_2, u_2} (α := R)
      (↑(if h : Membership.mem (α := R) I ((a : (a : ι) → R) x : R) then
            Subtype.mk (p := fun (x : R) ↦ x ∈ I) ((a : (a : ι) → R) x) h
          else 0) :
        R)
      (v x) =
    HSMul.hSMul.{u_3, u_2, u_2} (α := R) ((a : (a : ι) → R) x : R) (v x)
Tactic: apply Finsupp.sum_congr
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
ι : Type u_1
M : Type u_2
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
I : Ideal R
v : ι → M
a : ι →₀ R
ha : ∀ (i : ι), Membership.mem (α := R) I ((a : (a : ι) → R) i : R)
i : ι
h : i ∈ a.support
⊢ HSMul.hSMul.{u_3, u_2, u_2} (α := R)
      (↑(if h : Membership.mem (α := R) I ((a : (a : ι) → R) i : R) then
            Subtype.mk (p := fun (x : R) ↦ x ∈ I) ((a : (a : ι) → R) i) h
          else 0) :
        R)
      (v i) =
    HSMul.hSMul.{u_3, u_2, u_2} (α := R) ((a : (a : ι) → R) i : R) (v i)
have h : HSMul.hSMul.{u_3, u_2, u_2} (α := R) ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ I) ((a : (a : ι) → R) i) sorry) : R) : R)
    (v i) =
  HSMul.hSMul.{u_3, u_2, u_2} (α := R) ((a : (a : ι) → R) i : R) (v i)
Tactic: rw [dif_pos (ha i)]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
ι : Type u_1
M : Type u_2
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
I : Ideal R
v : ι → M
a : ι →₀ R
ha : ∀ (i : ι), Membership.mem (α := R) I ((a : (a : ι) → R) i : R)
⊢ Membership.mem (γ := Submodule R M) (LinearMap.range (finsuppTotal ι M I v)) (a.sum fun (i : ι) (c : R) ↦ c • v i)
have h : Eq.{u_2 + 1} (α := M)
  ((finsuppTotal ι M I v : (a : ι →₀ ↥I) → M)
      (Finsupp.mapRange (fun (r : R) ↦ if h : r ∈ I then Subtype.mk (p := fun (x : R) ↦ x ∈ I) r h else 0) sorry a) :
    M)
  (a.sum fun (i : ι) (c : R) ↦ c • v i : M)
Tactic: classical
    refine ⟨a.mapRange (fun r => if h : r ∈ I then ⟨r, h⟩ else 0)
      (by simp only [Submodule.zero_mem, ↓reduceDIte]; rfl), ?_⟩
    rw [finsuppTotal_apply, Finsupp.sum_mapRange_index]
    · apply Finsupp.sum_congr
      intro i _
      rw [dif_pos (ha i)]
    · exact fun _ => zero_smul _ _
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
ι : Type u_1
M : Type u_2
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
I : Ideal R
v : ι → M
a : ι →₀ R
ha : ∀ (i : ι), Membership.mem (α := R) I ((a : (a : ι) → R) i : R)
h :
  Eq.{u_2 + 1} (α := M)
    ((finsuppTotal ι M I v : (a : ι →₀ ↥I) → M)
        (Finsupp.mapRange (fun (r : R) ↦ if h : r ∈ I then Subtype.mk (p := fun (x : R) ↦ x ∈ I) r h else 0) ⋯ a) :
      M)
    (a.sum fun (i : ι) (c : R) ↦ c • v i : M)
⊢ Membership.mem (γ := Submodule R M) (LinearMap.range (finsuppTotal ι M I v)) (a.sum fun (i : ι) (c : R) ↦ c • v i)
have h₁ : Eq.{u_2 + 1} (α := M)
  (a.sum fun (a : ι) (b : R) ↦
    HSMul.hSMul.{u_3, u_2, u_2} (α := R) (↑(if h : b ∈ I then Subtype.mk (p := fun (x : R) ↦ x ∈ I) b h else 0) : R)
      (v a))
  (a.sum fun (i : ι) (c : R) ↦ c • v i)
Tactic: classical
    refine ⟨a.mapRange (fun r => if h : r ∈ I then ⟨r, h⟩ else 0)
      (by simp only [Submodule.zero_mem, ↓reduceDIte]; rfl), ?_⟩
    rw [finsuppTotal_apply, Finsupp.sum_mapRange_index]
    · apply Finsupp.sum_congr
      intro i _
      rw [dif_pos (ha i)]
    · exact fun _ => zero_smul _ _
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
ι : Type u_1
M : Type u_2
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
I : Ideal R
v : ι → M
a : ι →₀ R
ha : ∀ (i : ι), Membership.mem (α := R) I ((a : (a : ι) → R) i : R)
h :
  Eq.{u_2 + 1} (α := M)
    ((finsuppTotal ι M I v : (a : ι →₀ ↥I) → M)
        (Finsupp.mapRange (fun (r : R) ↦ if h : r ∈ I then Subtype.mk (p := fun (x : R) ↦ x ∈ I) r h else 0) ⋯ a) :
      M)
    (a.sum fun (i : ι) (c : R) ↦ c • v i : M)
h₁ :
  Eq.{u_2 + 1} (α := M)
    (a.sum fun (a : ι) (b : R) ↦
      HSMul.hSMul.{u_3, u_2, u_2} (α := R) (↑(if h : b ∈ I then Subtype.mk (p := fun (x : R) ↦ x ∈ I) b h else 0) : R)
        (v a))
    (a.sum fun (i : ι) (c : R) ↦ c • v i)
⊢ Membership.mem (γ := Submodule R M) (LinearMap.range (finsuppTotal ι M I v)) (a.sum fun (i : ι) (c : R) ↦ c • v i)
have h₂ : ∀ (a : ι), HSMul.hSMul.{u_3, u_2, u_2} (α := R) (↑0 : R) (v a) = 0
Tactic: classical
    refine ⟨a.mapRange (fun r => if h : r ∈ I then ⟨r, h⟩ else 0)
      (by simp only [Submodule.zero_mem, ↓reduceDIte]; rfl), ?_⟩
    rw [finsuppTotal_apply, Finsupp.sum_mapRange_index]
    · apply Finsupp.sum_congr
      intro i _
      rw [dif_pos (ha i)]
    · exact fun _ => zero_smul _ _
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u_1
inst : CommSemiring R
r : R
⊢ Ne (α := Associates (Ideal R)) (Associates.mk (Ideal.span {r})) 0 ↔ r ≠ 0
have rw : Ne (α := Ideal R) (Ideal.span {r}) 0 ↔ r ≠ 0
Tactic: rw [Associates.mk_ne_zero, Ideal.zero_eq_bot, Ne, Ideal.span_singleton_eq_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u_1
inst : CommSemiring R
r : R
rw : Ne (α := Ideal R) (Ideal.span {r}) 0 ↔ r ≠ 0
⊢ Ne (α := Associates (Ideal R)) (Associates.mk (Ideal.span {r})) 0 ↔ r ≠ 0
have rw₁ : Ne (α := Ideal R) (Ideal.span {r}) ⊥ ↔ r ≠ 0
Tactic: rw [Associates.mk_ne_zero, Ideal.zero_eq_bot, Ne, Ideal.span_singleton_eq_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u_1
inst : CommSemiring R
r : R
rw : Ne (α := Ideal R) (Ideal.span {r}) 0 ↔ r ≠ 0
rw₁ : Ne (α := Ideal R) (Ideal.span {r}) ⊥ ↔ r ≠ 0
⊢ Ne (α := Associates (Ideal R)) (Associates.mk (Ideal.span {r})) 0 ↔ r ≠ 0
have rw₂ : ¬Eq (α := Ideal R) (Ideal.span {r}) ⊥ ↔ r ≠ 0
Tactic: rw [Associates.mk_ne_zero, Ideal.zero_eq_bot, Ne, Ideal.span_singleton_eq_bot]