awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Operations
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
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
⊢ 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:
refine ⟨fun ⟨f, h⟩ => ⟨Finsupp.mapRange.linearMap I.subtype f, fun i => (f i).2, h⟩, ?_⟩
-- Module: Mathlib.RingTheory.Ideal.Operations
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)
simp : Subtype.mk (p := fun (x : R) ↦ x ∈ I) 0 ⋯ = 0
⊢ 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

Tactic:
simp only [Submodule.zero_mem, ↓reduceDIte]

Premises used: reduceDIte, Submodule.zero_mem
-- Module: Mathlib.RingTheory.Ideal.Operations
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)
⊢ Subtype.mk (p := fun (x : R) ↦ x ∈ I) 0 ⋯ = 0

Tactic:
rfl
-- Module: Mathlib.RingTheory.Ideal.Operations
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)

Tactic:
refine ⟨a.mapRange (fun r => if h : r ∈ I then ⟨r, h⟩ else 0)
      (by simp only [Submodule.zero_mem, ↓reduceDIte]; rfl), ?_⟩
-- Module: Mathlib.RingTheory.Ideal.Operations
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)
h₁ : ∀ (a : ι), HSMul.hSMul.{u_3, u_2, u_2} (α := R) (↑0 : R) (v a) = 0
⊢ 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)

Tactic:
rw [finsuppTotal_apply, Finsupp.sum_mapRange_index]

Premises used: Ideal.finsuppTotal_apply, Finsupp.sum_mapRange_index
-- Module: Mathlib.RingTheory.Ideal.Operations
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 :
  ∀ 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)
⊢ 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:
apply Finsupp.sum_congr

Premises used: Finsupp.sum_congr
-- Module: Mathlib.RingTheory.Ideal.Operations
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)
⊢ 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)

Tactic:
_
-- Module: Mathlib.RingTheory.Ideal.Operations
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_1 : i ∈ a.support
h h₁ :
  HSMul.hSMul.{u_3, u_2, u_2} (α := R) ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ I) ((a : (a : ι) → R) i) ⋯) : R) : R)
      (v i) =
    HSMul.hSMul.{u_3, u_2, u_2} (α := R) ((a : (a : ι) → R) i : R) (v i)
⊢ 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)

Tactic:
rw [dif_pos (ha i)]

Premises used: dif_pos
-- Module: Mathlib.RingTheory.Ideal.Operations
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)
⊢ ∀ (a : ι), HSMul.hSMul.{u_3, u_2, u_2} (α := R) (↑0 : R) (v a) = 0

Tactic:
fun _ => zero_smul _ _

Premises used: zero_smul
-- Module: Mathlib.RingTheory.Ideal.Operations
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)
⊢ ∀ (a : ι), HSMul.hSMul.{u_3, u_2, u_2} (α := R) (↑0 : R) (v a) = 0

Tactic:
exact fun _ => zero_smul _ _

Premises used: zero_smul
-- Module: Mathlib.RingTheory.Ideal.Operations
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)
h₂ h₃ : ∀ (a : ι), HSMul.hSMul.{u_3, u_2, u_2} (α := R) (↑0 : R) (v a) = 0
⊢ Membership.mem (γ := Submodule R M) (LinearMap.range (finsuppTotal ι M I v)) (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 _ _

Premises used: Ideal.finsuppTotal_apply, Finsupp.sum_congr, zero_smul, Finsupp.sum_mapRange_index
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
α : Type u_1
R : Type u_2
inst : Semiring R
x : R
v : α → R
⊢ Membership.mem (γ := Ideal R) (Ideal.span (Set.range v)) x ↔ ∃ (c : α →₀ R), (c.sum fun (i : α) (a : R) ↦ a * v i) = x

Tactic:
Finsupp.mem_span_range_iff_exists_finsupp

Premises used: Set.Mem, Finsupp.mem_span_range_iff_exists_finsupp
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
α : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : Fintype α
x : R
v : α → R
⊢ Membership.mem (γ := Ideal R) (span (Set.range v)) x ↔ ∃ (c : α → R), ∑ i : α, c i * v i = x

Tactic:
Submodule.mem_span_range_iff_exists_fun _

Premises used: Set.Mem, Submodule.mem_span_range_iff_exists_fun
-- Module: Mathlib.RingTheory.Ideal.Operations
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
rw₂ : ¬Eq (α := Ideal R) (Ideal.span {r}) ⊥ ↔ r ≠ 0
rw₃ rw₄ : ¬r = 0 ↔ r ≠ 0
⊢ Ne (α := Associates (Ideal R)) (Associates.mk (Ideal.span {r})) 0 ↔ r ≠ 0

Tactic:
rw [Associates.mk_ne_zero, Ideal.zero_eq_bot, Ne, Ideal.span_singleton_eq_bot]

Premises used: Ideal.span_singleton_eq_bot, Ne, Ideal.zero_eq_bot, Associates.mk_ne_zero
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
r : R
inl :
  Subsingleton R →
    (Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰ (span {r}) ↔ Membership.mem (γ := Submonoid R) R⁰ r)
inr :
  Nontrivial R →
    (Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰ (span {r}) ↔ Membership.mem (γ := Submonoid R) R⁰ r)
⊢ Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰ (span {r}) ↔ Membership.mem (γ := Submonoid R) R⁰ r

Tactic:
cases subsingleton_or_nontrivial R

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
r : R
h : Subsingleton R
inl :
  Membership.mem (γ := Submonoid (Ideal R)) (nonZeroDivisorsRight (Ideal R)) (span {r}) ↔
    Membership.mem (γ := Submonoid R) (nonZeroDivisorsRight R) r
⊢ Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰ (span {r}) ↔ Membership.mem (γ := Submonoid R) R⁰ r

Tactic:
simp_rw [← nonZeroDivisorsRight_eq_nonZeroDivisors]

Premises used: nonZeroDivisorsRight_eq_nonZeroDivisors
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
r : R
h : Subsingleton R
⊢ Membership.mem (γ := Submonoid (Ideal R)) (nonZeroDivisorsRight (Ideal R)) (span {r}) ↔
    Membership.mem (γ := Submonoid R) (nonZeroDivisorsRight R) r

Tactic:
⟨fun _ _ _ ↦ Subsingleton.eq_zero _, fun _ _ _ ↦ Subsingleton.eq_zero _⟩

Premises used: Iff.intro, Subsingleton.eq_zero
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
r : R
h : Subsingleton R
⊢ Membership.mem (γ := Submonoid (Ideal R)) (nonZeroDivisorsRight (Ideal R)) (span {r}) ↔
    Membership.mem (γ := Submonoid R) (nonZeroDivisorsRight R) r

Tactic:
exact ⟨fun _ _ _ ↦ Subsingleton.eq_zero _, fun _ _ _ ↦ Subsingleton.eq_zero _⟩
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
r : R
h : Nontrivial R
inr : Ne (α := Ideal R) (span {r}) 0 ↔ Membership.mem (γ := Submonoid R) R⁰ r
inr₁ : Ne (α := Ideal R) (span {r}) 0 ↔ r ≠ 0
inr₂ : ¬Eq (α := Ideal R) (span {r}) 0 ↔ r ≠ 0
inr₃ : ¬Eq (α := Ideal R) (span {r}) ⊥ ↔ r ≠ 0
inr₄ inr₅ : ¬r = 0 ↔ r ≠ 0
⊢ Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰ (span {r}) ↔ Membership.mem (γ := Submonoid R) R⁰ r

Tactic:
rw [mem_nonZeroDivisors_iff_ne_zero, mem_nonZeroDivisors_iff_ne_zero, ne_eq, zero_eq_bot,
      span_singleton_eq_bot]

Premises used: Ideal.span_singleton_eq_bot, Ideal.zero_eq_bot, ne_eq, mem_nonZeroDivisors_iff_ne_zero
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
P : Ideal R
inst_2 : P.IsPrime
⊢ P.primeCompl ≤ nonZeroDivisors R

Tactic:
le_nonZeroDivisors_of_noZeroDivisors <| not_not_intro P.zero_mem

Premises used: Set.Mem, not_not_intro, Ideal.zero_mem, le_nonZeroDivisors_of_noZeroDivisors
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ ∀ (b : Submodule R M), HSMul.hSMul.{u_1, u_2, u_2} (α := Ideal R) 1 b = b

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set R
N : Submodule R M
rw : (↑(Ideal.span s) : Set R) • N = s • N
rw₁ rw₂ : s • N = s • N
⊢ HSMul.hSMul (α := Ideal R) (Ideal.span s) N = s • N

Tactic:
rw [← coe_set_smul, coe_span_smul]

Premises used: Submodule.coe_span_smul, Submodule.coe_set_smul
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_1
inst : CommSemiring R
s : Set R
⊢ HSMul.hSMul (β := Ideal R) s ⊤ = Ideal.span s

Tactic:
(span_smul_eq s ⊤).symm.trans (Ideal.span s).mul_top

Premises used: Set.Mem, setOf, Ideal.span, Submodule.span_smul_eq, Ideal.mul_top, Top.top, Eq.symm, Eq.trans
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_1
inst : CommSemiring R
s : Set R
I : Ideal R
⊢ s • I ≤ Ideal.span s

Tactic:
simp [← Submodule.set_smul_top_eq_span, smul_le_smul_left]

Premises used: Submodule.set_smul_top_eq_span, smul_le_smul_left
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
B : Type ?u.424716
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Algebra R A
inst_6 : Algebra R B
rw : Eq (α := Submodule R A) (map (Algebra.linearMap R A) (R ∙ 1)) 1
rw₁ : Eq.{u_3 + 1} (α := Submodule R A) (span R (Set.image (α := R) (⇑(Algebra.linearMap R A) : (a : R) → A) {1})) 1
rw₂ : Eq (α := Submodule R A) (span R (singleton (α := A) ((Algebra.linearMap R A : (a : R) → A) 1 : A))) 1
rw₃ : Eq (α := Submodule R A) (span R (singleton (α := A) ((algebraMap R A : (a : R) → A) 1 : A))) 1
rw₄ : Eq (α := Submodule R A) (R ∙ 1) 1
rw₅ rw₆ : Eq (α := Submodule R A) (R ∙ 1) (R ∙ 1)
⊢ Eq (α := Submodule R A) (map (Algebra.linearMap R A) 1) 1

Tactic:
rw [one_eq_span, map_span, Set.image_singleton, Algebra.linearMap_apply, map_one, one_eq_span]

Premises used: Set.image_singleton, Algebra.linearMap_apply, map_one, Submodule.map_span, Submodule.one_eq_span
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_1
inst : CommSemiring R
M_1 : Type u_2
inst_1 : AddCommMonoid M_1
inst_2 : Module R M_1
A : Type u_3
B : Type ?u.424716
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Algebra R A
inst_6 : Algebra R B
I : Ideal R
M : Submodule R A
r : R
left : r ∈ (↑I : Set R)
a : A
h : a ∈ M
⊢ Commute ((Algebra.linearMap R A : (a : R) → A) r) a

Tactic:
apply Algebra.commutes

Premises used: Algebra.commutes
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_1
inst : CommSemiring R
M_1 : Type u_2
inst_1 : AddCommMonoid M_1
inst_2 : Module R M_1
A : Type u_3
B : Type ?u.424716
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Algebra R A
inst_6 : Algebra R B
I : Ideal R
M : Submodule R A
r : R
hr : r ∈ I
a : A
ha : a ∈ M
rw :
  HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a ∈
    HMul.hMul (α := Submodule R A)
      (({ toFun := map (Algebra.linearMap R A), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ :
              RingHom.{u_1, u_3} (Ideal R) (Submodule R A) } :
            (a : Ideal R) → Submodule R A)
          I :
        Submodule R A)
      M
⊢ r • a ∈
    HMul.hMul (α := Submodule R A)
      (({ toFun := map (Algebra.linearMap R A), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ :
              RingHom.{u_1, u_3} (Ideal R) (Submodule R A) } :
            (a : Ideal R) → Submodule R A)
          I :
        Submodule R A)
      M

Tactic:
rw [Algebra.smul_def]

Premises used: Algebra.smul_def
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_1
inst : CommSemiring R
M_1 : Type u_2
inst_1 : AddCommMonoid M_1
inst_2 : Module R M_1
A : Type u_3
B : Type ?u.424716
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Algebra R A
inst_6 : Algebra R B
I : Ideal R
M : Submodule R A
r : R
hr : r ∈ I
a : A
ha : a ∈ M
⊢ HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a ∈
    HMul.hMul (α := Submodule R A)
      (({ toFun := map (Algebra.linearMap R A), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ :
              RingHom.{u_1, u_3} (Ideal R) (Submodule R A) } :
            (a : Ideal R) → Submodule R A)
          I :
        Submodule R A)
      M

Tactic:
Submodule.mul_mem_mul ⟨r, hr, rfl⟩ ha

Premises used: Submodule.mul_mem_mul, Set.Mem, And.intro, Exists.intro, rfl
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_1
inst : CommSemiring R
M_1 : Type u_2
inst_1 : AddCommMonoid M_1
inst_2 : Module R M_1
A : Type u_3
B : Type ?u.424716
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Algebra R A
inst_6 : Algebra R B
I : Ideal R
M : Submodule R A
r : R
hr : r ∈ I
a : A
ha : a ∈ M
⊢ HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a ∈
    HMul.hMul (α := Submodule R A)
      (({ toFun := map (Algebra.linearMap R A), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ :
              RingHom.{u_1, u_3} (Ideal R) (Submodule R A) } :
            (a : Ideal R) → Submodule R A)
          I :
        Submodule R A)
      M

Tactic:
exact Submodule.mul_mem_mul ⟨r, hr, rfl⟩ ha
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_1
inst : CommSemiring R
M_1 : Type u_2
inst_1 : AddCommMonoid M_1
inst_2 : Module R M_1
A : Type u_3
B : Type ?u.424716
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Algebra R A
inst_6 : Algebra R B
I : Ideal R
M : Submodule R A
r : R
hr : r ∈ (↑I : Set R)
a : A
ha : a ∈ M
rw : r • a ∈ I • M
⊢ HMul.hMul (α := A) ((Algebra.linearMap R A : (a : R) → A) r : A) a ∈ I • M

Tactic:
rw [Algebra.linearMap_apply, ← Algebra.smul_def]

Premises used: Algebra.linearMap_apply, Algebra.smul_def
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_1
inst : CommSemiring R
M_1 : Type u_2
inst_1 : AddCommMonoid M_1
inst_2 : Module R M_1
A : Type u_3
B : Type ?u.424716
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Algebra R A
inst_6 : Algebra R B
I : Ideal R
M : Submodule R A
r : R
hr : r ∈ (↑I : Set R)
a : A
ha : a ∈ M
⊢ r • a ∈ I • M

Tactic:
Submodule.smul_mem_smul hr ha

Premises used: Set.Mem, Submodule.smul_mem_smul
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_1
inst : CommSemiring R
M_1 : Type u_2
inst_1 : AddCommMonoid M_1
inst_2 : Module R M_1
A : Type u_3
B : Type ?u.424716
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Algebra R A
inst_6 : Algebra R B
I : Ideal R
M : Submodule R A
r : R
hr : r ∈ (↑I : Set R)
a : A
ha : a ∈ M
⊢ r • a ∈ I • M

Tactic:
exact Submodule.smul_mem_smul hr ha

Premises used: Submodule.smul_mem_smul
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
N : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
I : Ideal R
f : M →ₗ[R] N
⊢ HSMul.hSMul (β := Submodule R M) I ⊤ ≤ comap f (HSMul.hSMul (β := Submodule R N) I ⊤)

Tactic:
map_le_iff_le_comap.mp <| le_of_eq_of_le (map_smul'' _ _ _) <|
    smul_mono_right _ le_top

Premises used: Submodule.map_smul'', smul_mono_right, le_top, Iff.mp, le_of_eq_of_le, Submodule.map_le_iff_le_comap
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
N : Type u_3
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
I : Ideal R
f : M →ₗ[R] N
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
rw : comap f (HSMul.hSMul (β := Submodule R N) I ⊤) = comap f (map f (HSMul.hSMul (β := Submodule R M) I ⊤))
rw₁ : comap f (HSMul.hSMul (β := Submodule R N) I ⊤) = comap f (I • map f ⊤)
rw₂ : comap f (HSMul.hSMul (β := Submodule R N) I ⊤) = comap f (I • f.range)
rw₃ rw₄ : comap f (HSMul.hSMul (β := Submodule R N) I ⊤) = comap f (HSMul.hSMul (β := Submodule R N) I ⊤)
⊢ comap f (HSMul.hSMul (β := Submodule R N) I ⊤) = HSMul.hSMul (β := Submodule R M) I ⊤ ⊔ f.ker

Tactic:
rw [← Submodule.comap_map_eq f, Submodule.map_smul'', map_top, LinearMap.range_eq_top.mpr h]

Premises used: Iff.mpr, Submodule.map_smul'', Submodule.map_top, LinearMap.range_eq_top, Submodule.comap_map_eq
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_1
inst : CommSemiring R
s : Set R
I J : Ideal R
hs : s ⊆ (↑(I ⊔ J).radical : Set R)
z : R
hzs : z ∈ s
⊢ s ⊆
    (↑{ carrier := {r : R | ∃ (n : ℕ), ∃ y ∈ I, ∃ z ∈ J, y + z = r ^ n}, add_mem' := ⋯, zero_mem' := ⋯,
          smul_mem' := ⋯ } :
      Set R)

Tactic:
simp only [Ideal.radical, Submodule.mem_sup] at hs

Premises used: Submodule.mem_sup, Ideal.radical
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_1
inst : CommSemiring R
s : Set R
I J : Ideal R
z : R
hzs : z ∈ s
hs :
  s ⊆
    (↑{ carrier := {r : R | ∃ (n : ℕ), ∃ y ∈ I, ∃ z ∈ J, y + z = r ^ n}, add_mem' := ⋯, zero_mem' := ⋯,
          smul_mem' := ⋯ } :
      Set R)
obtain :
  ∀ (m : ℕ) (y : R) (hyq : y ∈ I) (b : R) (hb : b ∈ J) (hy : y + b = z ^ m),
    ∃ (m : ℕ) (a : R) (b : R) (_ : a ∈ I) (_ : b ∈ J), a + b = (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ s) z hzs) : R) ^ m
⊢ ∃ (m : ℕ) (a : R) (b : R) (_ : a ∈ I) (_ : b ∈ J), a + b = (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ s) z hzs) : R) ^ m

Tactic:
obtain ⟨m, y, hyq, b, hb, hy⟩ := hs hzs
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_1
inst : CommSemiring R
s : Set R
I J : Ideal R
z : R
hzs : z ∈ s
hs :
  s ⊆
    (↑{ carrier := {r : R | ∃ (n : ℕ), ∃ y ∈ I, ∃ z ∈ J, y + z = r ^ n}, add_mem' := ⋯, zero_mem' := ⋯,
          smul_mem' := ⋯ } :
      Set R)
m : ℕ
y : R
hyq : y ∈ I
b : R
hb : b ∈ J
hy : y + b = z ^ m
⊢ ∃ (m : ℕ) (a : R) (b : R) (_ : a ∈ I) (_ : b ∈ J), a + b = (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ s) z hzs) : R) ^ m

Tactic:
⟨m, y, b, hyq, hb, hy⟩

Premises used: Exists.intro
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_1
inst : CommSemiring R
s : Set R
I J : Ideal R
z : R
hzs : z ∈ s
hs :
  s ⊆
    (↑{ carrier := {r : R | ∃ (n : ℕ), ∃ y ∈ I, ∃ z ∈ J, y + z = r ^ n}, add_mem' := ⋯, zero_mem' := ⋯,
          smul_mem' := ⋯ } :
      Set R)
m : ℕ
y : R
hyq : y ∈ I
b : R
hb : b ∈ J
hy : y + b = z ^ m
⊢ ∃ (m : ℕ) (a : R) (b : R) (_ : a ∈ I) (_ : b ∈ J), a + b = (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ s) z hzs) : R) ^ m

Tactic:
exact ⟨m, y, b, hyq, hb, hy⟩
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_1
inst : CommSemiring R
s : Set R
I J : Ideal R
hs : s ⊆ (↑(I ⊔ J).radical : Set R)
⊢ ∀ (z : (↑s : Type u_1)), ∃ (m : ℕ) (a : R) (b : R) (_ : a ∈ I) (_ : b ∈ J), a + b = (↑z : R) ^ m

Tactic:
replace hs : ∀ z : s, ∃ (m : ℕ) (a b : R) (ha : a ∈ I) (hb : b ∈ J), a + b = z ^ m := by
    rintro ⟨z, hzs⟩
    simp only [Ideal.radical, Submodule.mem_sup] at hs
    obtain ⟨m, y, hyq, b, hb, hy⟩ := hs hzs
    exact ⟨m, y, b, hyq, hb, hy⟩
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_1
inst : CommSemiring R
s : Set R
I J : Ideal R
hs : ∀ (z : (↑s : Type u_1)), ∃ (m : ℕ) (a : R) (b : R) (_ : a ∈ I) (_ : b ∈ J), a + b = (↑z : R) ^ m
choose :
  ∀ (m : (z : (↑s : Type u_1)) → ℕ) (a b : (z : (↑s : Type u_1)) → R) (ha : ∀ (z : (↑s : Type u_1)), a z ∈ I)
    (hb : ∀ (z : (↑s : Type u_1)), b z ∈ J) (heq : ∀ (z : (↑s : Type u_1)), a z + b z = (↑z : R) ^ m z),
    ∃ (t : (↑s : Type u_1) → R), Set.range t ⊆ (↑I : Set R) ∧ s ⊆ (↑(span (Set.range t) ⊔ J).radical : Set R)
⊢ ∃ (t : (↑s : Type u_1) → R), Set.range t ⊆ (↑I : Set R) ∧ s ⊆ (↑(span (Set.range t) ⊔ J).radical : Set R)

Tactic:
choose m a b ha hb heq using hs
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_1
inst : CommSemiring R
s : Set R
I J : Ideal R
m : (z : (↑s : Type u_1)) → ℕ
a b : (z : (↑s : Type u_1)) → R
ha : ∀ (z : (↑s : Type u_1)), a z ∈ I
hb : ∀ (z : (↑s : Type u_1)), b z ∈ J
heq : ∀ (z : (↑s : Type u_1)), a z + b z = (↑z : R) ^ m z
rwa rwa₁ rwa₂ rwa₃ : ∀ (y : (↑s : Type u_1)), a y ∈ (↑I : Set R)
⊢ Set.range a ⊆ (↑I : Set R)

Tactic:
rwa [Set.range_subset_iff]

Premises used: Set.range_subset_iff