awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
rw₂ : ¬Eq (α := Ideal R) (Ideal.span {r}) ⊥ ↔ r ≠ 0
⊢ Ne (α := Associates (Ideal R)) (Associates.mk (Ideal.span {r})) 0 ↔ r ≠ 0
have rw₃ : ¬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
inst_1 : NoZeroDivisors R
r : R
⊢ Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰ (span {r}) ↔ Membership.mem (γ := Submonoid R) R⁰ r
have inl : Subsingleton R →
  (Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰ (span {r}) ↔ Membership.mem (γ := Submonoid R) R⁰ r)
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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)
⊢ Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰ (span {r}) ↔ Membership.mem (γ := Submonoid R) R⁰ r
have inr : Nontrivial R →
  (Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰ (span {r}) ↔ Membership.mem (γ := Submonoid R) R⁰ r)
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
r : R
h : Subsingleton R
⊢ Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰ (span {r}) ↔ Membership.mem (γ := Submonoid R) R⁰ r
have inl : Membership.mem (γ := Submonoid (Ideal R)) (nonZeroDivisorsRight (Ideal R)) (span {r}) ↔
  Membership.mem (γ := Submonoid R) (nonZeroDivisorsRight R) r
Tactic: simp_rw [← nonZeroDivisorsRight_eq_nonZeroDivisors]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
r : R
h : Nontrivial R
⊢ Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰ (span {r}) ↔ Membership.mem (γ := Submonoid R) R⁰ r
have inr : Ne (α := Ideal R) (span {r}) 0 ↔ 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]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰ (span {r}) ↔ Membership.mem (γ := Submonoid R) R⁰ r
have inr₁ : Ne (α := Ideal R) (span {r}) 0 ↔ r ≠ 0
Tactic: rw [mem_nonZeroDivisors_iff_ne_zero, mem_nonZeroDivisors_iff_ne_zero, ne_eq, zero_eq_bot,
      span_singleton_eq_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰ (span {r}) ↔ Membership.mem (γ := Submonoid R) R⁰ r
have inr₂ : ¬Eq (α := Ideal R) (span {r}) 0 ↔ r ≠ 0
Tactic: rw [mem_nonZeroDivisors_iff_ne_zero, mem_nonZeroDivisors_iff_ne_zero, ne_eq, zero_eq_bot,
      span_singleton_eq_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰ (span {r}) ↔ Membership.mem (γ := Submonoid R) R⁰ r
have inr₃ : ¬Eq (α := Ideal R) (span {r}) ⊥ ↔ r ≠ 0
Tactic: rw [mem_nonZeroDivisors_iff_ne_zero, mem_nonZeroDivisors_iff_ne_zero, ne_eq, zero_eq_bot,
      span_singleton_eq_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰ (span {r}) ↔ Membership.mem (γ := Submonoid R) R⁰ r
have inr₄ : ¬r = 0 ↔ r ≠ 0
Tactic: rw [mem_nonZeroDivisors_iff_ne_zero, mem_nonZeroDivisors_iff_ne_zero, ne_eq, zero_eq_bot,
      span_singleton_eq_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ HSMul.hSMul (α := Ideal R) (Ideal.span s) N = s • N
have rw : (↑(Ideal.span s) : Set R) • N = s • N
Tactic: rw [← coe_set_smul, coe_span_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ HSMul.hSMul (α := Ideal R) (Ideal.span s) N = s • N
have rw₁ : s • N = s • N
Tactic: rw [← coe_set_smul, coe_span_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ Eq (α := Submodule R A) (map (Algebra.linearMap R A) 1) 1
have rw : Eq (α := Submodule R A) (map (Algebra.linearMap R A) (R ∙ 1)) 1
Tactic: rw [one_eq_span, map_span, Set.image_singleton, Algebra.linearMap_apply, map_one, one_eq_span]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ Eq (α := Submodule R A) (map (Algebra.linearMap R A) 1) 1
have rw₁ : Eq.{u_3 + 1} (α := Submodule R A) (span R (Set.image (α := R) (⇑(Algebra.linearMap R A) : (a : R) → A) {1})) 1
Tactic: rw [one_eq_span, map_span, Set.image_singleton, Algebra.linearMap_apply, map_one, one_eq_span]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ Eq (α := Submodule R A) (map (Algebra.linearMap R A) 1) 1
have rw₂ : Eq (α := Submodule R A) (span R (singleton (α := A) ((Algebra.linearMap R A : (a : R) → A) 1 : A))) 1
Tactic: rw [one_eq_span, map_span, Set.image_singleton, Algebra.linearMap_apply, map_one, one_eq_span]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ Eq (α := Submodule R A) (map (Algebra.linearMap R A) 1) 1
have rw₃ : Eq (α := Submodule R A) (span R (singleton (α := A) ((algebraMap R A : (a : R) → A) 1 : A))) 1
Tactic: rw [one_eq_span, map_span, Set.image_singleton, Algebra.linearMap_apply, map_one, one_eq_span]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ Eq (α := Submodule R A) (map (Algebra.linearMap R A) 1) 1
have rw₄ : Eq (α := Submodule R A) (R ∙ 1) 1
Tactic: rw [one_eq_span, map_span, Set.image_singleton, Algebra.linearMap_apply, map_one, one_eq_span]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ Eq (α := Submodule R A) (map (Algebra.linearMap R A) 1) 1
have rw₅ : Eq (α := Submodule R A) (R ∙ 1) (R ∙ 1)
Tactic: rw [one_eq_span, map_span, Set.image_singleton, Algebra.linearMap_apply, map_one, one_eq_span]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ 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
have 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' := sorry, map_mul' := sorry, map_zero' := sorry, map_add' := sorry :
            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]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ HMul.hMul (α := A) ((Algebra.linearMap R A : (a : R) → A) r : A) a ∈ I • M
have rw : r • a ∈ I • M
Tactic: rw [Algebra.linearMap_apply, ← Algebra.smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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)
⊢ comap f (HSMul.hSMul (β := Submodule R N) I ⊤) = HSMul.hSMul (β := Submodule R M) I ⊤ ⊔ f.ker
have rw : comap f (HSMul.hSMul (β := Submodule R N) I ⊤) = comap f (map f (HSMul.hSMul (β := Submodule R M) I ⊤))
Tactic: rw [← Submodule.comap_map_eq f, Submodule.map_smul'', map_top, LinearMap.range_eq_top.mpr h]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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 ⊤))
⊢ comap f (HSMul.hSMul (β := Submodule R N) I ⊤) = HSMul.hSMul (β := Submodule R M) I ⊤ ⊔ f.ker
have rw₁ : comap f (HSMul.hSMul (β := Submodule R N) I ⊤) = comap f (I • map f ⊤)
Tactic: rw [← Submodule.comap_map_eq f, Submodule.map_smul'', map_top, LinearMap.range_eq_top.mpr h]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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 ⊤)
⊢ comap f (HSMul.hSMul (β := Submodule R N) I ⊤) = HSMul.hSMul (β := Submodule R M) I ⊤ ⊔ f.ker
have rw₂ : comap f (HSMul.hSMul (β := Submodule R N) I ⊤) = comap f (I • f.range)
Tactic: rw [← Submodule.comap_map_eq f, Submodule.map_smul'', map_top, LinearMap.range_eq_top.mpr h]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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)
⊢ comap f (HSMul.hSMul (β := Submodule R N) I ⊤) = HSMul.hSMul (β := Submodule R M) I ⊤ ⊔ f.ker
have rw₃ : comap f (HSMul.hSMul (β := Submodule R N) I ⊤) = comap f (HSMul.hSMul (β := Submodule R N) I ⊤)
Tactic: rw [← Submodule.comap_map_eq f, Submodule.map_smul'', map_top, LinearMap.range_eq_top.mpr h]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (hypothesis)
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
⊢ ∃ (m : ℕ) (a : R) (b : R) (_ : a ∈ I) (_ : b ∈ J), a + b = (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ s) z hzs) : R) ^ m
have hs₁ : s ⊆
  (↑{ carrier := {r : R | ∃ (n : ℕ), ∃ y ∈ I, ∃ z ∈ J, y + z = r ^ n}, add_mem' := sorry, zero_mem' := sorry, smul_mem' := sorry } :
    Set R)
Tactic: simp only [Ideal.radical, Submodule.mem_sup] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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 : ℕ) (a : R) (b : R) (_ : a ∈ I) (_ : b ∈ J), a + b = (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ s) z hzs) : R) ^ m
have 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
Tactic: obtain ⟨m, y, hyq, b, hb, hy⟩ := hs hzs
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
s : Set R
I J : Ideal R
hs : s ⊆ (↑(I ⊔ 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)
have hs₁ : ∀ (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⟩
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ ∃ (t : (↑s : Type u_1) → R), Set.range t ⊆ (↑I : Set R) ∧ s ⊆ (↑(span (Set.range t) ⊔ J).radical : Set R)
have 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)
Tactic: choose m a b ha hb heq using hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ Set.range a ⊆ (↑I : Set R)
have rwa : ∀ (y : (↑s : Type u_1)), a y ∈ (↑I : Set R)
Tactic: rwa [Set.range_subset_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ ∃ (t : (↑s : Type u_1) → R), Set.range t ⊆ (↑I : Set R) ∧ s ⊆ (↑(span (Set.range t) ⊔ J).radical : Set R)
have refine : ∀ (z : R) (hz : z ∈ s),
  a (Subtype.mk (p := fun (x : R) ↦ x ∈ s) z hz) + b (Subtype.mk (p := fun (x : R) ↦ x ∈ s) z hz) ∈
    span (Set.range a) ⊔ J
Tactic: refine ⟨a, by rwa [Set.range_subset_iff], fun z hz ↦ ⟨m ⟨z, hz⟩, heq ⟨z, hz⟩ ▸ ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Over (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
p : Ideal R
P : Ideal S
inst_2 : Algebra R S
inst_3 : Algebra.{u_1, u_2} (R ⧸ p) (S ⧸ P)
inst_4 : IsScalarTower.{u_1, u_1, u_2} R (R ⧸ p) (S ⧸ P)
h :
  Function.Injective.{u_1 + 1, u_2 + 1} (α := R ⧸ p) (β := S ⧸ P) (⇑(algebraMap (R ⧸ p) (S ⧸ P)) : (a : R ⧸ p) → S ⧸ P)
⊢ comap (F := R →+* S) (algebraMap R S) P = p
have h₁ : ∀ (x : R), Membership.mem (γ := Ideal R) (comap (F := R →+* S) (algebraMap R S) P) x ↔ x ∈ p
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Over (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
p : Ideal R
P : Ideal S
inst_2 : Algebra R S
inst_3 : Algebra.{u_1, u_2} (R ⧸ p) (S ⧸ P)
inst_4 : IsScalarTower.{u_1, u_1, u_2} R (R ⧸ p) (S ⧸ P)
h :
  Function.Injective.{u_1 + 1, u_2 + 1} (α := R ⧸ p) (β := S ⧸ P) (⇑(algebraMap (R ⧸ p) (S ⧸ P)) : (a : R ⧸ p) → S ⧸ P)
x : R
⊢ Membership.mem (γ := Ideal R) (comap (F := R →+* S) (algebraMap R S) P) x ↔ x ∈ p
have h₁ : Eq.{u_2 + 1} (α := S ⧸ P)
    ((algebraMap (R ⧸ p) (S ⧸ P) : (a : R ⧸ p) → S ⧸ P) ((Quotient.mk p : (a : R) → R ⧸ p) x) : S ⧸ P) (0 : S ⧸ P) ↔
  Eq (α := R ⧸ p) ((Quotient.mk p : (a : R) → R ⧸ p) x : R ⧸ p) (0 : R ⧸ p)
Tactic: rw [mem_comap, ← Quotient.eq_zero_iff_mem, ← Quotient.eq_zero_iff_mem, Quotient.mk_algebraMap,
    IsScalarTower.algebraMap_apply R (R ⧸ p) (S ⧸ P), Quotient.algebraMap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Over (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
I J : Ideal S
p : Ideal R
P : Ideal S
inst_2 : Algebra R S
x : R
⊢ Eq.{u_2 + 1} (α := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
    ((algebraMap R (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) :
          (a : R) → S ⧸ map (algebraMap R S) p)
        x :
      HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
    ((algebraMap (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) :
          (a : R ⧸ p) → S ⧸ map (algebraMap R S) p)
        ((algebraMap R (R ⧸ p) : (a : R) → R ⧸ p) x) :
      HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
have rw : Eq.{u_2 + 1} (α := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
  ((algebraMap R (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) :
        (a : R) → S ⧸ map (algebraMap R S) p)
      x :
    HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
  ((algebraMap (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) :
        (a : R ⧸ p) → S ⧸ map (algebraMap R S) p)
      ((mk p : (a : R) → R ⧸ p) x) :
    HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
Tactic: rw [Quotient.algebraMap_eq, Quotient.algebraMap_quotient_map_quotient,
      Quotient.mk_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Over (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
I J : Ideal S
p : Ideal R
P : Ideal S
inst_2 : Algebra R S
x : R
rw :
  Eq.{u_2 + 1} (α := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
    ((algebraMap R (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) :
          (a : R) → S ⧸ map (algebraMap R S) p)
        x :
      HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
    ((algebraMap (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) :
          (a : R ⧸ p) → S ⧸ map (algebraMap R S) p)
        ((mk p : (a : R) → R ⧸ p) x) :
      HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
⊢ Eq.{u_2 + 1} (α := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
    ((algebraMap R (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) :
          (a : R) → S ⧸ map (algebraMap R S) p)
        x :
      HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
    ((algebraMap (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) :
          (a : R ⧸ p) → S ⧸ map (algebraMap R S) p)
        ((algebraMap R (R ⧸ p) : (a : R) → R ⧸ p) x) :
      HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
have rw₁ : Eq.{u_2 + 1} (α := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
  ((algebraMap R (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) :
        (a : R) → S ⧸ map (algebraMap R S) p)
      x :
    HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
  ((mk (map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ map (algebraMap R S) p)
      ((algebraMap R S : (a : R) → S) x) :
    HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
Tactic: rw [Quotient.algebraMap_eq, Quotient.algebraMap_quotient_map_quotient,
      Quotient.mk_algebraMap]