awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : R
⊢ (∀ (m : M), ∃ (r : R), Membership.mem (γ := Submonoid R) (Submonoid.powers f) r ∧ r • m = 0) ↔
    Subset (α := Set (PrimeSpectrum R)) (Module.support R M) (PrimeSpectrum.zeroLocus {f})
have mp : (∀ (m : M), ∃ (r : R), Membership.mem (γ := Submonoid R) (Submonoid.powers f) r ∧ r • m = 0) →
  Subset (α := Set (PrimeSpectrum R)) (Module.support R M) (PrimeSpectrum.zeroLocus {f})
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : R
mp :
  (∀ (m : M), ∃ (r : R), Membership.mem (γ := Submonoid R) (Submonoid.powers f) r ∧ r • m = 0) →
    Subset (α := Set (PrimeSpectrum R)) (Module.support R M) (PrimeSpectrum.zeroLocus {f})
⊢ (∀ (m : M), ∃ (r : R), Membership.mem (γ := Submonoid R) (Submonoid.powers f) r ∧ r • m = 0) ↔
    Subset (α := Set (PrimeSpectrum R)) (Module.support R M) (PrimeSpectrum.zeroLocus {f})
have mpr : Subset (α := Set (PrimeSpectrum R)) (Module.support R M) (PrimeSpectrum.zeroLocus {f}) →
  ∀ (m : M), ∃ (r : R), Membership.mem (γ := Submonoid R) (Submonoid.powers f) r ∧ r • m = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
x : PrimeSpectrum R
hx' : Membership.mem (γ := Set (PrimeSpectrum R)) (Module.support R M) x
f : R
H : ∀ (m : M), ∃ (r : R), Membership.mem (γ := Submonoid R) (Submonoid.powers f) r ∧ r • m = 0
⊢ f ∈ (↑x.asIdeal : Set R)
have mp : ∀ (m : M) (hm : Submodule.annihilator (M := M) (R ∙ m) ≤ x.asIdeal), f ∈ (↑x.asIdeal : Set R)
Tactic: obtain ⟨m, hm⟩ := Module.mem_support_iff_exists_annihilator.mp hx'
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
x : PrimeSpectrum R
hx' : Membership.mem (γ := Set (PrimeSpectrum R)) (Module.support R M) x
f : R
H : ∀ (m : M), ∃ (r : R), Membership.mem (γ := Submonoid R) (Submonoid.powers f) r ∧ r • m = 0
m : M
hm : Submodule.annihilator (M := M) (R ∙ m) ≤ x.asIdeal
⊢ f ∈ (↑x.asIdeal : Set R)
have mp : ∀ (n : ℕ) (e : HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((fun (x : ℕ) ↦ f ^ x) n) m = 0), f ∈ (↑x.asIdeal : Set R)
Tactic: obtain ⟨_, ⟨n, rfl⟩, e⟩ := H m
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : R
H : Subset (α := Set (PrimeSpectrum R)) (Module.support R M) (PrimeSpectrum.zeroLocus {f})
m : M
⊢ ∃ (r : R), Membership.mem (γ := Submonoid R) (Submonoid.powers f) r ∧ r • m = 0
have pos : ∀ (h : Eq (α := Ideal R) (Submodule.annihilator (M := M) (R ∙ m)) ⊤),
  ∃ (r : R), Membership.mem (γ := Submonoid R) (Submonoid.powers f) r ∧ r • m = 0
Tactic: by_cases h : (Submodule.span R {m}).annihilator = ⊤
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : R
H : Subset (α := Set (PrimeSpectrum R)) (Module.support R M) (PrimeSpectrum.zeroLocus {f})
m : M
pos :
  ∀ (h : Eq (α := Ideal R) (Submodule.annihilator (M := M) (R ∙ m)) ⊤),
    ∃ (r : R), Membership.mem (γ := Submonoid R) (Submonoid.powers f) r ∧ r • m = 0
⊢ ∃ (r : R), Membership.mem (γ := Submonoid R) (Submonoid.powers f) r ∧ r • m = 0
have neg : ∀ (h : ¬Eq (α := Ideal R) (Submodule.annihilator (M := M) (R ∙ m)) ⊤),
  ∃ (r : R), Membership.mem (γ := Submonoid R) (Submonoid.powers f) r ∧ r • m = 0
Tactic: by_cases h : (Submodule.span R {m}).annihilator = ⊤
-- Lean 4 proof step from Mathlib.RingTheory.Support (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : R
H : Subset (α := Set (PrimeSpectrum R)) (Module.support R M) (PrimeSpectrum.zeroLocus {f})
m : M
h : Eq (α := Ideal R) (Submodule.annihilator (M := M) (R ∙ m)) ⊤
⊢ ∃ (r : R), Membership.mem (γ := Submonoid R) (Submonoid.powers f) r ∧ r • m = 0
have h₁ : m = 0
Tactic: rw [Submodule.annihilator_eq_top_iff, Submodule.span_singleton_eq_bot] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : R
H : Subset (α := Set (PrimeSpectrum R)) (Module.support R M) (PrimeSpectrum.zeroLocus {f})
m : M
h : ¬Eq (α := Ideal R) (Submodule.annihilator (M := M) (R ∙ m)) ⊤
⊢ Membership.mem (γ := Ideal R) (Ideal.radical (Submodule.annihilator (M := M) (R ∙ m))) f
have rw : ∀ ⦃I : Ideal R⦄,
  Membership.mem (γ := Set (Ideal R)) {J : Ideal R | Submodule.annihilator (M := M) (R ∙ m) ≤ J ∧ J.IsPrime} I → f ∈ I
Tactic: rw [Ideal.radical_eq_sInf, Ideal.mem_sInf]
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : R
H : Subset (α := Set (PrimeSpectrum R)) (Module.support R M) (PrimeSpectrum.zeroLocus {f})
m : M
h : ¬Eq (α := Ideal R) (Submodule.annihilator (M := M) (R ∙ m)) ⊤
⊢ ∃ (r : R), Membership.mem (γ := Submonoid R) (Submonoid.powers f) r ∧ r • m = 0
have neg : ∀ (n : ℕ) (hn : Membership.mem (γ := Ideal R) (Submodule.annihilator (M := M) (R ∙ m)) (f ^ n)),
  ∃ (r : R), Membership.mem (γ := Submonoid R) (Submonoid.powers f) r ∧ r • m = 0
Tactic: obtain ⟨n, hn⟩ : f ∈ (Submodule.span R {m}).annihilator.radical := by
      rw [Ideal.radical_eq_sInf, Ideal.mem_sInf]
      rintro p ⟨hp, hp'⟩
      simpa using H (Module.mem_support_iff_exists_annihilator (p := ⟨p, hp'⟩).mpr ⟨_, hp⟩)
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ Eq (α := Set (PrimeSpectrum R)) (support R M) ∅ ↔ Subsingleton M
have rw : (∀ (m : M), ∃ (r : R), Membership.mem (γ := Submonoid R) (Submonoid.powers 1) r ∧ r • m = 0) ↔ ∀ (y : M), y = 0
Tactic: rw [← Set.subset_empty_iff, ← PrimeSpectrum.zeroLocus_singleton_one,
    ← LocalizedModule.subsingleton_iff_support_subset, LocalizedModule.subsingleton_iff,
    subsingleton_iff_forall_eq 0]
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ Set.Nonempty (α := PrimeSpectrum R) (support R M) ↔ Nontrivial M
have rw : Ne (α := Set (PrimeSpectrum R)) (support R M) ∅ ↔ Nontrivial M
Tactic: rw [Set.nonempty_iff_ne_empty, ne_eq,
    Module.support_eq_empty_iff, ← not_subsingleton_iff_nontrivial]
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
rw : Ne (α := Set (PrimeSpectrum R)) (support R M) ∅ ↔ Nontrivial M
⊢ Set.Nonempty (α := PrimeSpectrum R) (support R M) ↔ Nontrivial M
have rw₁ : ¬Eq (α := Set (PrimeSpectrum R)) (support R M) ∅ ↔ Nontrivial M
Tactic: rw [Set.nonempty_iff_ne_empty, ne_eq,
    Module.support_eq_empty_iff, ← not_subsingleton_iff_nontrivial]
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
rw : Ne (α := Set (PrimeSpectrum R)) (support R M) ∅ ↔ Nontrivial M
rw₁ : ¬Eq (α := Set (PrimeSpectrum R)) (support R M) ∅ ↔ Nontrivial M
⊢ Set.Nonempty (α := PrimeSpectrum R) (support R M) ↔ Nontrivial M
have rw₂ : ¬Subsingleton M ↔ Nontrivial M
Tactic: rw [Set.nonempty_iff_ne_empty, ne_eq,
    Module.support_eq_empty_iff, ← not_subsingleton_iff_nontrivial]
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
rw : Ne (α := Set (PrimeSpectrum R)) (support R M) ∅ ↔ Nontrivial M
rw₁ : ¬Eq (α := Set (PrimeSpectrum R)) (support R M) ∅ ↔ Nontrivial M
rw₂ : ¬Subsingleton M ↔ Nontrivial M
⊢ Set.Nonempty (α := PrimeSpectrum R) (support R M) ↔ Nontrivial M
have rw₃ : ¬Subsingleton M ↔ ¬Subsingleton M
Tactic: rw [Set.nonempty_iff_ne_empty, ne_eq,
    Module.support_eq_empty_iff, ← not_subsingleton_iff_nontrivial]
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_3
inst_1 : Ring A
inst_2 : Algebra R A
⊢ Eq (α := Set (PrimeSpectrum R)) (support R A)
    (PrimeSpectrum.zeroLocus (↑(RingHom.ker (F := R →+* A) (algebraMap R A)) : Set R))
have h : ∀ (p : PrimeSpectrum R),
  Membership.mem (γ := Set (PrimeSpectrum R)) (support R A) p ↔
    Membership.mem (γ := Set (PrimeSpectrum R))
      (PrimeSpectrum.zeroLocus (↑(RingHom.ker (F := R →+* A) (algebraMap R A)) : Set R)) p
Tactic: ext p
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_3
inst_1 : Ring A
inst_2 : Algebra R A
p : PrimeSpectrum R
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (support R A) p ↔
    Membership.mem (γ := Set (PrimeSpectrum R))
      (PrimeSpectrum.zeroLocus (↑(RingHom.ker (F := R →+* A) (algebraMap R A)) : Set R)) p
have h : (∃ (m : A), ∀ r ∉ p.asIdeal, ¬r • m = 0) ↔ RingHom.ker (F := R →+* A) (algebraMap R A) ≤ p.asIdeal
Tactic: simp only [mem_support_iff', ne_eq, PrimeSpectrum.mem_zeroLocus, SetLike.coe_subset_coe]
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_3
inst_1 : Ring A
inst_2 : Algebra R A
p : PrimeSpectrum R
⊢ (∃ (m : A), ∀ r ∉ p.asIdeal, ¬r • m = 0) ↔ RingHom.ker (F := R →+* A) (algebraMap R A) ≤ p.asIdeal
have h : (∃ (m : A), ∀ r ∉ p.asIdeal, ¬r • m = 0) →
  ∀ (x : R) (hx : Membership.mem (γ := Submodule R R) (RingHom.ker (F := R →+* A) (algebraMap R A)) x) (m : A)
    (hm : ∀ r ∉ p.asIdeal, ¬r • m = 0) (hx' : x ∉ p.asIdeal), False
Tactic: refine ⟨fun ⟨m, hm⟩ x hx ↦ not_not.mp fun hx' ↦ ?_, fun H ↦ ⟨1, fun r hr e ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_3
inst_1 : Ring A
inst_2 : Algebra R A
p : PrimeSpectrum R
h :
  (∃ (m : A), ∀ r ∉ p.asIdeal, ¬r • m = 0) →
    ∀ (x : R) (hx : Membership.mem (γ := Submodule R R) (RingHom.ker (F := R →+* A) (algebraMap R A)) x) (m : A)
      (hm : ∀ r ∉ p.asIdeal, ¬r • m = 0) (hx' : x ∉ p.asIdeal), False
⊢ (∃ (m : A), ∀ r ∉ p.asIdeal, ¬r • m = 0) ↔ RingHom.ker (F := R →+* A) (algebraMap R A) ≤ p.asIdeal
have h₁ : ∀ (H : RingHom.ker (F := R →+* A) (algebraMap R A) ≤ p.asIdeal) (r : R) (hr : r ∉ p.asIdeal)
  (e : HSMul.hSMul (β := A) r 1 = 0), False
Tactic: refine ⟨fun ⟨m, hm⟩ x hx ↦ not_not.mp fun hx' ↦ ?_, fun H ↦ ⟨1, fun r hr e ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
inst_5 : Nontrivial M
⊢ Eq (α := Set (PrimeSpectrum R)) (support R M) Set.univ
have simp : ∀ (x : PrimeSpectrum R), ∃ (m : M), ∀ r ∉ x.asIdeal, ¬r = 0 ∧ ¬m = 0
Tactic: simp only [Set.eq_univ_iff_forall, mem_support_iff', ne_eq, smul_eq_zero, not_or]
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
inst_5 : Nontrivial M
⊢ ∀ (x : PrimeSpectrum R), ∃ (m : M), ∀ r ∉ x.asIdeal, ¬r = 0 ∧ ¬m = 0
have obtain : ∀ (x : M) (hx : x ≠ 0) (x : PrimeSpectrum R), ∃ (m : M), ∀ r ∉ x.asIdeal, ¬r = 0 ∧ ¬m = 0
Tactic: obtain ⟨x, hx⟩ := exists_ne (0 : M)
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ Subset (α := Set (PrimeSpectrum R)) (support R M) (support R N)
have simp_rw : ∀ (x : PrimeSpectrum R), (∃ (m : M), ∀ r ∉ x.asIdeal, r • m ≠ 0) → ∃ (m : N), ∀ r ∉ x.asIdeal, r • m ≠ 0
Tactic: simp_rw [Set.subset_def, mem_support_iff']
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ Subset (α := Set (PrimeSpectrum R)) (support R N) (support R M)
have simp_rw : ∀ (x : PrimeSpectrum R), (∃ (m : N), ∀ r ∉ x.asIdeal, r • m ≠ 0) → ∃ (m : M), ∀ r ∉ x.asIdeal, r • m ≠ 0
Tactic: simp_rw [Set.subset_def, mem_support_iff']
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
x : PrimeSpectrum R
m : N
hm : ∀ r ∉ x.asIdeal, r • m ≠ 0
⊢ ∃ (m : M), ∀ r ∉ x.asIdeal, r • m ≠ 0
have obtain : ∀ (m : M) (hm : ∀ r ∉ x.asIdeal, HSMul.hSMul (β := N) r ((f : (a : M) → N) m : N) ≠ 0),
  ∃ (m : M), ∀ r ∉ x.asIdeal, r • m ≠ 0
Tactic: obtain ⟨m, rfl⟩ := hf m
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
P : Type u_4
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup P
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Function.Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
hg : Function.Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
⊢ Eq (α := Set (PrimeSpectrum R)) (support R N) (support R M ∪ support R P)
have refine : Subset (α := Set (PrimeSpectrum R)) (support R N) (support R M ∪ support R P)
Tactic: refine subset_antisymm ?_ (Set.union_subset (Module.support_subset_of_injective f hf)
    (Module.support_subset_of_surjective g hg))
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
P : Type u_4
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup P
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Function.Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
hg : Function.Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
x : PrimeSpectrum R
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (support R N) x →
    Membership.mem (γ := Set (PrimeSpectrum R)) (support R M ∪ support R P) x
have contrapose : x ∉ support R M ∪ support R P → x ∉ support R N
Tactic: contrapose
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
P : Type u_4
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup P
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Function.Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
hg : Function.Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
x : PrimeSpectrum R
⊢ x ∉ support R M ∪ support R P → x ∉ support R N
have simp : (∀ (m : M), ∃ r ∉ x.asIdeal, r • m = 0) →
  (∀ (m : P), ∃ r ∉ x.asIdeal, r • m = 0) → ∀ (m : N), ∃ r ∉ x.asIdeal, r • m = 0
Tactic: simp only [Set.mem_union, not_or, and_imp, notMem_support_iff']
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
P : Type u_4
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup P
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Function.Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
hg : Function.Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
x : PrimeSpectrum R
H₁ : ∀ (m : M), ∃ r ∉ x.asIdeal, r • m = 0
H₂ : ∀ (m : P), ∃ r ∉ x.asIdeal, r • m = 0
m : N
⊢ ∃ r ∉ x.asIdeal, r • m = 0
have obtain : ∀ (r : R) (hr : r ∉ x.asIdeal) (e₁ : HSMul.hSMul (β := P) r ((g : (a : N) → P) m : P) = 0), ∃ r ∉ x.asIdeal, r • m = 0
Tactic: obtain ⟨r, hr, e₁⟩ := H₂ (g m)
-- Lean 4 proof step from Mathlib.RingTheory.Support (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
P : Type u_4
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup P
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Function.Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
hg : Function.Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
x : PrimeSpectrum R
H₁ : ∀ (m : M), ∃ r ∉ x.asIdeal, r • m = 0
H₂ : ∀ (m : P), ∃ r ∉ x.asIdeal, r • m = 0
m : N
r : R
hr : r ∉ x.asIdeal
e₁ : HSMul.hSMul (β := P) r ((g : (a : N) → P) m : P) = 0
⊢ ∃ r ∉ x.asIdeal, r • m = 0
have e₂ : Membership.mem (γ := Set N) (Set.range.{u_3, u_2 + 1} (ι := M) (⇑f : (a : M) → N)) (r • m)
Tactic: rw [← map_smul, h] at e₁
Cleared hypotheses: e₁
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
P : Type u_4
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup P
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Function.Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
hg : Function.Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
x : PrimeSpectrum R
H₁ : ∀ (m : M), ∃ r ∉ x.asIdeal, r • m = 0
H₂ : ∀ (m : P), ∃ r ∉ x.asIdeal, r • m = 0
m : N
r : R
hr : r ∉ x.asIdeal
e₁ : Membership.mem (γ := Set N) (Set.range.{u_3, u_2 + 1} (ι := M) (⇑f : (a : M) → N)) (r • m)
⊢ ∃ r ∉ x.asIdeal, r • m = 0
have obtain : ∀ (m' : M) (hm' : (f : (a : M) → N) m' = r • m), ∃ r ∉ x.asIdeal, r • m = 0
Tactic: obtain ⟨m', hm'⟩ := e₁
Cleared hypotheses: e₁
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
P : Type u_4
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup P
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Function.Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
hg : Function.Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
x : PrimeSpectrum R
H₁ : ∀ (m : M), ∃ r ∉ x.asIdeal, r • m = 0
H₂ : ∀ (m : P), ∃ r ∉ x.asIdeal, r • m = 0
m : N
r : R
hr : r ∉ x.asIdeal
m' : M
hm' : (f : (a : M) → N) m' = r • m
⊢ ∃ r ∉ x.asIdeal, r • m = 0
have obtain : ∀ (s : R) (hs : s ∉ x.asIdeal) (e₁ : s • m' = 0), ∃ r ∉ x.asIdeal, r • m = 0
Tactic: obtain ⟨s, hs, e₁⟩ := H₁ m'
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
P : Type u_4
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup P
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Function.Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
hg : Function.Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
x : PrimeSpectrum R
H₁ : ∀ (m : M), ∃ r ∉ x.asIdeal, r • m = 0
H₂ : ∀ (m : P), ∃ r ∉ x.asIdeal, r • m = 0
m : N
r : R
hr : r ∉ x.asIdeal
m' : M
hm' : (f : (a : M) → N) m' = r • m
s : R
hs : s ∉ x.asIdeal
e₁ : s • m' = 0
⊢ (s * r) • m = 0
have rw : s • r • m = 0
Tactic: rw [mul_smul, ← hm', ← map_smul, e₁, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
P : Type u_4
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup P
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Function.Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
hg : Function.Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
x : PrimeSpectrum R
H₁ : ∀ (m : M), ∃ r ∉ x.asIdeal, r • m = 0
H₂ : ∀ (m : P), ∃ r ∉ x.asIdeal, r • m = 0
m : N
r : R
hr : r ∉ x.asIdeal
m' : M
hm' : (f : (a : M) → N) m' = r • m
s : R
hs : s ∉ x.asIdeal
e₁ : s • m' = 0
rw : s • r • m = 0
⊢ (s * r) • m = 0
have rw₁ : HSMul.hSMul (β := N) s ((f : (a : M) → N) m' : N) = 0
Tactic: rw [mul_smul, ← hm', ← map_smul, e₁, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
P : Type u_4
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup P
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Function.Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
hg : Function.Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
x : PrimeSpectrum R
H₁ : ∀ (m : M), ∃ r ∉ x.asIdeal, r • m = 0
H₂ : ∀ (m : P), ∃ r ∉ x.asIdeal, r • m = 0
m : N
r : R
hr : r ∉ x.asIdeal
m' : M
hm' : (f : (a : M) → N) m' = r • m
s : R
hs : s ∉ x.asIdeal
e₁ : s • m' = 0
rw : s • r • m = 0
rw₁ : HSMul.hSMul (β := N) s ((f : (a : M) → N) m' : N) = 0
⊢ (s * r) • m = 0
have rw₂ : Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) (s • m') : N) (0 : N)
Tactic: rw [mul_smul, ← hm', ← map_smul, e₁, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
P : Type u_4
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup P
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Function.Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
hg : Function.Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
x : PrimeSpectrum R
H₁ : ∀ (m : M), ∃ r ∉ x.asIdeal, r • m = 0
H₂ : ∀ (m : P), ∃ r ∉ x.asIdeal, r • m = 0
m : N
r : R
hr : r ∉ x.asIdeal
m' : M
hm' : (f : (a : M) → N) m' = r • m
s : R
hs : s ∉ x.asIdeal
e₁ : s • m' = 0
rw : s • r • m = 0
rw₁ : HSMul.hSMul (β := N) s ((f : (a : M) → N) m' : N) = 0
rw₂ : Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) (s • m') : N) (0 : N)
⊢ (s * r) • m = 0
have rw₃ : Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) 0 : N) (0 : N)
Tactic: rw [mul_smul, ← hm', ← map_smul, e₁, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
P : Type u_4
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup P
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Function.Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
hg : Function.Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
x : PrimeSpectrum R
H₁ : ∀ (m : M), ∃ r ∉ x.asIdeal, r • m = 0
H₂ : ∀ (m : P), ∃ r ∉ x.asIdeal, r • m = 0
m : N
r : R
hr : r ∉ x.asIdeal
m' : M
hm' : (f : (a : M) → N) m' = r • m
s : R
hs : s ∉ x.asIdeal
e₁ : s • m' = 0
rw : s • r • m = 0
rw₁ : HSMul.hSMul (β := N) s ((f : (a : M) → N) m' : N) = 0
rw₂ : Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) (s • m') : N) (0 : N)
rw₃ : Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) 0 : N) (0 : N)
⊢ (s * r) • m = 0
have rw₄ : Eq.{u_3 + 1} (α := N) 0 0
Tactic: rw [mul_smul, ← hm', ← map_smul, e₁, map_zero]