awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
a : R
ha : a ∈ p.primeCompl
y : M
k : ℕ
h : (f : (a : M) → M') y = a ^ k • x
b : R
n : ℕ
hb : b ^ n • x = 0
⊢ Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') (b ^ n • y) : M') ((f : (a : M) → M') 0 : M')
have h₁ : HSMul.hSMul (β := M') (b ^ n) ((f : (a : M) → M') y : M') = (f : (a : M) → M') 0
Tactic: rw [map_smul, h, smul_comm, hb, smul_zero, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
a : R
ha : a ∈ p.primeCompl
y : M
k : ℕ
h : (f : (a : M) → M') y = a ^ k • x
b : R
n : ℕ
hb : b ^ n • x = 0
h₁ : HSMul.hSMul (β := M') (b ^ n) ((f : (a : M) → M') y : M') = (f : (a : M) → M') 0
⊢ Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') (b ^ n • y) : M') ((f : (a : M) → M') 0 : M')
have h₂ : b ^ n • a ^ k • x = (f : (a : M) → M') 0
Tactic: rw [map_smul, h, smul_comm, hb, smul_zero, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
a : R
ha : a ∈ p.primeCompl
y : M
k : ℕ
h : (f : (a : M) → M') y = a ^ k • x
b : R
n : ℕ
hb : b ^ n • x = 0
h₁ : HSMul.hSMul (β := M') (b ^ n) ((f : (a : M) → M') y : M') = (f : (a : M) → M') 0
h₂ : b ^ n • a ^ k • x = (f : (a : M) → M') 0
⊢ Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') (b ^ n • y) : M') ((f : (a : M) → M') 0 : M')
have h₃ : a ^ k • b ^ n • x = (f : (a : M) → M') 0
Tactic: rw [map_smul, h, smul_comm, hb, smul_zero, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
a : R
ha : a ∈ p.primeCompl
y : M
k : ℕ
h : (f : (a : M) → M') y = a ^ k • x
b : R
n : ℕ
hb : b ^ n • x = 0
h₁ : HSMul.hSMul (β := M') (b ^ n) ((f : (a : M) → M') y : M') = (f : (a : M) → M') 0
h₂ : b ^ n • a ^ k • x = (f : (a : M) → M') 0
h₃ : a ^ k • b ^ n • x = (f : (a : M) → M') 0
⊢ Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') (b ^ n • y) : M') ((f : (a : M) → M') 0 : M')
have h₄ : HSMul.hSMul (β := M') (a ^ k) 0 = (f : (a : M) → M') 0
Tactic: rw [map_smul, h, smul_comm, hb, smul_zero, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
a : R
ha : a ∈ p.primeCompl
y : M
k : ℕ
h : (f : (a : M) → M') y = a ^ k • x
b : R
n : ℕ
hb : b ^ n • x = 0
h₁ : HSMul.hSMul (β := M') (b ^ n) ((f : (a : M) → M') y : M') = (f : (a : M) → M') 0
h₂ : b ^ n • a ^ k • x = (f : (a : M) → M') 0
h₃ : a ^ k • b ^ n • x = (f : (a : M) → M') 0
h₄ : HSMul.hSMul (β := M') (a ^ k) 0 = (f : (a : M) → M') 0
⊢ Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') (b ^ n • y) : M') ((f : (a : M) → M') 0 : M')
have h₅ : Eq.{u_3 + 1} (α := M') (0 : M') ((f : (a : M) → M') 0 : M')
Tactic: rw [map_smul, h, smul_comm, hb, smul_zero, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
a : R
ha : a ∈ p.primeCompl
y : M
k : ℕ
h : (f : (a : M) → M') y = a ^ k • x
b : R
n : ℕ
hb : b ^ n • x = 0
h₁ : HSMul.hSMul (β := M') (b ^ n) ((f : (a : M) → M') y : M') = (f : (a : M) → M') 0
h₂ : b ^ n • a ^ k • x = (f : (a : M) → M') 0
h₃ : a ^ k • b ^ n • x = (f : (a : M) → M') 0
h₄ : HSMul.hSMul (β := M') (a ^ k) 0 = (f : (a : M) → M') 0
h₅ : Eq.{u_3 + 1} (α := M') (0 : M') ((f : (a : M) → M') 0 : M')
⊢ Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') (b ^ n • y) : M') ((f : (a : M) → M') 0 : M')
have h₆ : Eq.{u_3 + 1} (α := M') 0 0
Tactic: rw [map_smul, h, smul_comm, hb, smul_zero, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
a : R
ha : a ∈ p.primeCompl
y : M
k : ℕ
h : (f : (a : M) → M') y = a ^ k • x
b : R
h_1 : Membership.mem (γ := Submodule R R) (Ideal.radical (colon (M := M) ⊥ {y})) b
n : ℕ
hb : Membership.mem (γ := Ideal R) (colon (M := M) ⊥ {y}) (b ^ n)
⊢ b ∈ p
have hb₁ : b ^ n • y = 0
Tactic: rw [mem_colon_singleton, mem_bot] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
a : R
ha : a ∈ p.primeCompl
y : M
k : ℕ
h : (f : (a : M) → M') y = a ^ k • x
b : R
h_1 : Membership.mem (γ := Submodule R R) (Ideal.radical (colon (M := M) ⊥ {y})) b
n : ℕ
hb : b ^ n • y = 0
⊢ b ∈ p
have hb₁ : Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') (b ^ n • y) : M') ((f : (a : M) → M') 0 : M')
Tactic: apply_fun f at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
a : R
ha : a ∈ p.primeCompl
y : M
k : ℕ
h : (f : (a : M) → M') y = a ^ k • x
b : R
h_1 : Membership.mem (γ := Submodule R R) (Ideal.radical (colon (M := M) ⊥ {y})) b
n : ℕ
hb : Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') (b ^ n • y) : M') ((f : (a : M) → M') 0 : M')
⊢ b ∈ p
have hb₁ : Membership.mem (γ := Ideal R) (colon (M := M') ⊥ {x}) (b ^ n * a ^ k)
Tactic: rw [map_smul, map_zero, h, ← mul_smul, ← mem_bot R, ← mem_colon_singleton] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
a : R
ha : a ∈ p.primeCompl
y : M
k : ℕ
h : (f : (a : M) → M') y = a ^ k • x
b : R
h_1 : Membership.mem (γ := Submodule R R) (Ideal.radical (colon (M := M) ⊥ {y})) b
n : ℕ
hb : Membership.mem (γ := Ideal R) (colon (M := M') ⊥ {x}) (b ^ n * a ^ k)
⊢ b ∈ p
have hb₁ : b ^ n * a ^ k ∈ p
Tactic: replace hb := hx.ge (Ideal.le_radical hb)
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
a : R
ha : a ∈ p.primeCompl
y : M
k : ℕ
h : (f : (a : M) → M') y = a ^ k • x
b : R
h_1 : Membership.mem (γ := Submodule R R) (Ideal.radical (colon (M := M) ⊥ {y})) b
n : ℕ
hb : b ^ n * a ^ k ∈ p
⊢ b ∈ p
have pos : ∀ (hb : ¬b ∈ p), b ^ n * a ^ k ∉ p
Tactic: contrapose hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
h : ∀ (a : R) (_ : a ∈ p.primeCompl) (y : M) (k : ℕ), (f : (a : M) → M') y ≠ a ^ k • x
⊢ Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M ∪ associatedPrimes R M'') p
have neg : Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M'') p
Tactic: right
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
h : ∀ (a : R) (_ : a ∈ p.primeCompl) (y : M) (k : ℕ), (f : (a : M) → M') y ≠ a ^ k • x
⊢ Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M'') p
have neg : ∀ (b : R) (hb : b ∈ p),
  Membership.mem (γ := Submodule R R)
    (Ideal.radical (colon (M := M'') ⊥ (singleton (α := M'') ((g : (a : M') → M'') x : M'')))) b
Tactic: refine ⟨‹_›, g x, le_antisymm (fun b hb ↦ ?_) (fun b ⟨n, hb⟩ ↦ ?_)⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
h : ∀ (a : R) (_ : a ∈ p.primeCompl) (y : M) (k : ℕ), (f : (a : M) → M') y ≠ a ^ k • x
neg :
  ∀ (b : R) (hb : b ∈ p),
    Membership.mem (γ := Submodule R R)
      (Ideal.radical (colon (M := M'') ⊥ (singleton (α := M'') ((g : (a : M') → M'') x : M'')))) b
⊢ Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M'') p
have neg₁ : ∀ (b : R),
  Membership.mem (γ := Submodule R R)
      (Ideal.radical (colon (M := M'') ⊥ (singleton (α := M'') ((g : (a : M') → M'') x : M'')))) b →
    ∀ (n : ℕ)
      (hb :
        Membership.mem (γ := Ideal R) (colon (M := M'') ⊥ (singleton (α := M'') ((g : (a : M') → M'') x : M'')))
          (b ^ n)),
      b ∈ p
Tactic: refine ⟨‹_›, g x, le_antisymm (fun b hb ↦ ?_) (fun b ⟨n, hb⟩ ↦ ?_)⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
h : ∀ (a : R) (_ : a ∈ p.primeCompl) (y : M) (k : ℕ), (f : (a : M) → M') y ≠ a ^ k • x
b : R
hb : b ∈ p
⊢ Membership.mem (γ := Submodule R R)
    (Ideal.radical (colon (M := M'') ⊥ (singleton (α := M'') ((g : (a : M') → M'') x : M'')))) b
have hb₁ : Membership.mem (γ := Submodule R R) (Ideal.radical (colon (M := M') ⊥ {x})) b
Tactic: rw [hx] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
h : ∀ (a : R) (_ : a ∈ p.primeCompl) (y : M) (k : ℕ), (f : (a : M) → M') y ≠ a ^ k • x
b : R
hb : Membership.mem (γ := Submodule R R) (Ideal.radical (colon (M := M') ⊥ {x})) b
⊢ Membership.mem (γ := Submodule R R)
    (Ideal.radical (colon (M := M'') ⊥ (singleton (α := M'') ((g : (a : M') → M'') x : M'')))) b
have neg : ∀ (b : R) (hb : Membership.mem (γ := Submodule R R) (colon (M := M') ⊥ {x}) b),
  Membership.mem (γ := Submodule R R) (colon (M := M'') ⊥ (singleton (α := M'') ((g : (a : M') → M'') x : M''))) b
Tactic: refine Ideal.radical_mono (fun b hb ↦ ?_) hb
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
h : ∀ (a : R) (_ : a ∈ p.primeCompl) (y : M) (k : ℕ), (f : (a : M) → M') y ≠ a ^ k • x
b_1 : R
hb_1 : Membership.mem (γ := Submodule R R) (Ideal.radical (colon (M := M') ⊥ {x})) b_1
b : R
hb : Membership.mem (γ := Submodule R R) (colon (M := M') ⊥ {x}) b
⊢ Membership.mem (γ := Submodule R R) (colon (M := M'') ⊥ (singleton (α := M'') ((g : (a : M') → M'') x : M''))) b
have neg : ∀ (hb : b • x = 0), HSMul.hSMul (β := M'') b ((g : (a : M') → M'') x : M'') = 0
Tactic: rw [mem_colon_singleton, mem_bot] at hb ⊢
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
h : ∀ (a : R) (_ : a ∈ p.primeCompl) (y : M) (k : ℕ), (f : (a : M) → M') y ≠ a ^ k • x
b_1 : R
hb_1 : Membership.mem (γ := Submodule R R) (Ideal.radical (colon (M := M') ⊥ {x})) b_1
b : R
hb : b • x = 0
⊢ HSMul.hSMul (β := M'') b ((g : (a : M') → M'') x : M'') = 0
have neg : Eq.{u_4 + 1} (α := M'') ((g : (a : M') → M'') (b • x) : M'') (0 : M'')
Tactic: rw [← map_smul, hb, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
h : ∀ (a : R) (_ : a ∈ p.primeCompl) (y : M) (k : ℕ), (f : (a : M) → M') y ≠ a ^ k • x
b_1 : R
hb_1 : Membership.mem (γ := Submodule R R) (Ideal.radical (colon (M := M') ⊥ {x})) b_1
b : R
hb : b • x = 0
neg : Eq.{u_4 + 1} (α := M'') ((g : (a : M') → M'') (b • x) : M'') (0 : M'')
⊢ HSMul.hSMul (β := M'') b ((g : (a : M') → M'') x : M'') = 0
have neg₁ : Eq.{u_4 + 1} (α := M'') ((g : (a : M') → M'') 0 : M'') (0 : M'')
Tactic: rw [← map_smul, hb, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
h : ∀ (a : R) (_ : a ∈ p.primeCompl) (y : M) (k : ℕ), (f : (a : M) → M') y ≠ a ^ k • x
b_1 : R
hb_1 : Membership.mem (γ := Submodule R R) (Ideal.radical (colon (M := M') ⊥ {x})) b_1
b : R
hb : b • x = 0
neg : Eq.{u_4 + 1} (α := M'') ((g : (a : M') → M'') (b • x) : M'') (0 : M'')
neg₁ : Eq.{u_4 + 1} (α := M'') ((g : (a : M') → M'') 0 : M'') (0 : M'')
⊢ HSMul.hSMul (β := M'') b ((g : (a : M') → M'') x : M'') = 0
have neg₂ : Eq.{u_4 + 1} (α := M'') 0 0
Tactic: rw [← map_smul, hb, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
h : ∀ (a : R) (_ : a ∈ p.primeCompl) (y : M) (k : ℕ), (f : (a : M) → M') y ≠ a ^ k • x
b : R
h_1 :
  Membership.mem (γ := Submodule R R)
    (Ideal.radical (colon (M := M'') ⊥ (singleton (α := M'') ((g : (a : M') → M'') x : M'')))) b
n : ℕ
hb : Membership.mem (γ := Ideal R) (colon (M := M'') ⊥ (singleton (α := M'') ((g : (a : M') → M'') x : M''))) (b ^ n)
⊢ b ∈ p
have hb₁ : b ^ n • x ∈ f.range
Tactic: rw [mem_colon_singleton, mem_bot, ← map_smul, ← LinearMap.mem_ker,
        hfg.linearMap_ker_eq] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
h : ∀ (a : R) (_ : a ∈ p.primeCompl) (y : M) (k : ℕ), (f : (a : M) → M') y ≠ a ^ k • x
b : R
h_1 :
  Membership.mem (γ := Submodule R R)
    (Ideal.radical (colon (M := M'') ⊥ (singleton (α := M'') ((g : (a : M') → M'') x : M'')))) b
n : ℕ
hb : b ^ n • x ∈ f.range
⊢ b ∈ p
have neg : ∀ (y : M) (hy : (f : (a : M) → M') y = b ^ n • x), b ∈ p
Tactic: obtain ⟨y, hy⟩ := hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
h : ∀ (a : R) (_ : a ∈ p.primeCompl) (y : M) (k : ℕ), (f : (a : M) → M') y ≠ a ^ k • x
b : R
h_1 :
  Membership.mem (γ := Submodule R R)
    (Ideal.radical (colon (M := M'') ⊥ (singleton (α := M'') ((g : (a : M') → M'') x : M'')))) b
n : ℕ
y : M
hy : (f : (a : M) → M') y = b ^ n • x
⊢ b ∈ p
have neg : ∀ (H : b ∉ p), False
Tactic: by_contra H