awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : Membership.mem (γ := Submodule R (P →₀ R)) (supported R R (↑t1 : Set P)) l
hl2 : Eq.{u_4 + 1} (α := P) ((linearCombination R id : (a : P →₀ R) → P) l : P) ((f : (a : M) → P) x : P)
⊢ Eq (α := P) (∑ a ∈ l.support, HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((l : (a : P) → R) a : R) (id a))
    (∑ x ∈ l.support, (f : (a : M) → P) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((l : (a : P) → R) x : R) (id (g x))))
have a : ∀ (y : P) (hy : y ∈ l.support),
  HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((l : (a : P) → R) y : R) (id y) =
    (f : (a : M) → P) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((l : (a : P) → R) y : R) (id (g y)))
Tactic: refine Finset.sum_congr rfl fun y hy => ?_
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : Membership.mem (γ := Submodule R (P →₀ R)) (supported R R (↑t1 : Set P)) l
hl2 : Eq.{u_4 + 1} (α := P) ((linearCombination R id : (a : P →₀ R) → P) l : P) ((f : (a : M) → P) x : P)
y : P
hy : y ∈ l.support
⊢ HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((l : (a : P) → R) y : R) (id y) =
    (f : (a : M) → P) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((l : (a : P) → R) y : R) (id (g y)))
have a : HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((l : (a : P) → R) y : R) y =
  (f : (a : M) → P) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((l : (a : P) → R) y : R) (g y))
Tactic: unfold id
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : Membership.mem (γ := Submodule R (P →₀ R)) (supported R R (↑t1 : Set P)) l
hl2 : Eq.{u_4 + 1} (α := P) ((linearCombination R id : (a : P →₀ R) → P) l : P) ((f : (a : M) → P) x : P)
y : P
hy : y ∈ l.support
⊢ HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((l : (a : P) → R) y : R) y =
    (f : (a : M) → P) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((l : (a : P) → R) y : R) (g y))
have a : HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((l : (a : P) → R) y : R) y =
  HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := P) ((l : (a : P) → R) y : R) ((f : (a : M) → P) (g y) : P)
Tactic: rw [f.map_smul, (hg y (hl1 hy)).2]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : Membership.mem (γ := Submodule R (P →₀ R)) (supported R R (↑t1 : Set P)) l
hl2 : Eq.{u_4 + 1} (α := P) ((linearCombination R id : (a : P →₀ R) → P) l : P) ((f : (a : M) → P) x : P)
y : P
hy : y ∈ l.support
a :
  HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((l : (a : P) → R) y : R) y =
    HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := P) ((l : (a : P) → R) y : R) ((f : (a : M) → P) (g y) : P)
⊢ HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((l : (a : P) → R) y : R) y =
    (f : (a : M) → P) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((l : (a : P) → R) y : R) (g y))
have a₁ : HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((l : (a : P) → R) y : R) y =
  HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((l : (a : P) → R) y : R) y
Tactic: rw [f.map_smul, (hg y (hl1 hy)).2]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
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
hf1 : f.ker.FG
hf2 : g.ker.FG
hsur : Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ (g ∘ₗ f).ker.FG
have rw : (comap f g.ker).FG
Tactic: rw [LinearMap.ker_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
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
hf1 : f.ker.FG
hf2 : g.ker.FG
hsur : Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ (comap f g.ker).FG
have hs1 : (map f (comap f g.ker)).FG
Tactic: apply fg_of_fg_map_of_fg_inf_ker f
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
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
hf1 : f.ker.FG
hf2 : g.ker.FG
hsur : Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
hs1 : (map f (comap f g.ker)).FG
⊢ (comap f g.ker).FG
have hs2 : (comap f g.ker ⊓ f.ker).FG
Tactic: apply fg_of_fg_map_of_fg_inf_ker f
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
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
hf1 : f.ker.FG
hf2 : g.ker.FG
hsur : Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ (map f (comap f g.ker)).FG
have hs1 : (f.range ⊓ g.ker).FG
Tactic: rwa [Submodule.map_comap_eq, LinearMap.range_eq_top.2 hsur, top_inf_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
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
hf1 : f.ker.FG
hf2 : g.ker.FG
hsur : Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
hs1 : (f.range ⊓ g.ker).FG
⊢ (map f (comap f g.ker)).FG
have hs1₁ : (⊤ ⊓ g.ker).FG
Tactic: rwa [Submodule.map_comap_eq, LinearMap.range_eq_top.2 hsur, top_inf_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
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_exact : Function.Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
h_surj : Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
inst_7 : Module.Finite R M
inst_8 : Module.Finite R P
⊢ Module.Finite R N
have refine_1 : (map g ⊤).FG
Tactic: refine ⟨(⊤ : Submodule R _).fg_of_fg_map_of_fg_inf_ker g ?_ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
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_exact : Function.Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
h_surj : Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
inst_7 : Module.Finite R M
inst_8 : Module.Finite R P
refine_1 : (map g ⊤).FG
⊢ Module.Finite R N
have refine_2 : (⊤ ⊓ g.ker).FG
Tactic: refine ⟨(⊤ : Submodule R _).fg_of_fg_map_of_fg_inf_ker g ?_ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (hypothesis)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
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_exact : Function.Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
h_surj : Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
inst_7 : Module.Finite R M
inst_8 : Module.Finite R P
⊢ (map g ⊤).FG
have h_surj₁ : g.range = ⊤
Tactic: rw [← LinearMap.range_eq_top] at h_surj
Cleared hypotheses: h_surj, inst_7, inst_8
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
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_exact : Function.Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
h_surj : g.range = ⊤
inst_7 : Module.Finite R M
inst_8 : Module.Finite R P
⊢ (map g ⊤).FG
have refine_1 : FG.{u_1, u_4} (R := R) (M := P) ⊤
Tactic: rw [Submodule.map_top, h_surj]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
σ : Type u_1
inst : Finite σ
⊢ AddMonoid.FG.{u_1} (FreeAbelianGroup σ)
have rw : Module.Finite.{0, u_1} ℤ (FreeAbelianGroup σ)
Tactic: rw [← AddGroup.fg_iff_addMonoid_fg, ← Module.Finite.iff_addGroup_fg]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Ideal (goal)
Goal:
R : Type u_3
S : Type u_4
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
h : I.FG
f : R →+* S
⊢ FG.{u_4} (R := S) (Ideal.map f I)
have obtain : ∀ (s : Finset R) (hs : span (↑s : Set R) = I), FG.{u_4} (R := S) (Ideal.map f I)
Tactic: obtain ⟨s, hs⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Ideal (goal)
Goal:
R : Type u_3
S : Type u_4
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
f : R →+* S
s : Finset R
hs : span (↑s : Set R) = I
⊢ FG.{u_4} (R := S) (Ideal.map f I)
have refine : Eq (α := Ideal S) (span (↑(Finset.image (⇑f : (a : R) → S) s) : Set S)) (Ideal.map f I)
Tactic: refine ⟨s.image f, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Ideal (goal)
Goal:
R : Type u_3
S : Type u_4
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
f : R →+* S
s : Finset R
hs : span (↑s : Set R) = I
⊢ Eq (α := Ideal S) (span (↑(Finset.image (⇑f : (a : R) → S) s) : Set S)) (Ideal.map f I)
have rw : Eq.{u_4 + 1} (α := Ideal S) (span ((⇑f : (a : R) → S) '' (↑s : Set R))) (Ideal.map f I)
Tactic: rw [Finset.coe_image, ← map_span, hs]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Ideal (goal)
Goal:
R : Type u_3
S : Type u_4
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
f : R →+* S
s : Finset R
hs : span (↑s : Set R) = I
rw : Eq.{u_4 + 1} (α := Ideal S) (span ((⇑f : (a : R) → S) '' (↑s : Set R))) (Ideal.map f I)
⊢ Eq (α := Ideal S) (span (↑(Finset.image (⇑f : (a : R) → S) s) : Set S)) (Ideal.map f I)
have rw₁ : Eq.{u_4 + 1} (α := Ideal S) (Ideal.map f (span (↑s : Set R))) (Ideal.map f I)
Tactic: rw [Finset.coe_image, ← map_span, hs]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Ideal (goal)
Goal:
R : Type u_3
S : Type u_4
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
f : R →+* S
s : Finset R
hs : span (↑s : Set R) = I
rw : Eq.{u_4 + 1} (α := Ideal S) (span ((⇑f : (a : R) → S) '' (↑s : Set R))) (Ideal.map f I)
rw₁ : Eq.{u_4 + 1} (α := Ideal S) (Ideal.map f (span (↑s : Set R))) (Ideal.map f I)
⊢ Eq (α := Ideal S) (span (↑(Finset.image (⇑f : (a : R) → S) s) : Set S)) (Ideal.map f I)
have rw₂ : Eq.{u_4 + 1} (α := Ideal S) (Ideal.map f I) (Ideal.map f I)
Tactic: rw [Finset.coe_image, ← map_span, hs]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Ideal (goal)
Goal:
R : Type u_3
S : Type u_4
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
h : I.FG
f : R →+* S
⊢ FG.{u_4} (R := S) (Ideal.map f I)
have obtain : ∀ (s : Finset R) (hs : span (↑s : Set R) = I), FG.{u_4} (R := S) (Ideal.map f I)
Tactic: classical
    obtain ⟨s, hs⟩ := h
    refine ⟨s.image f, ?_⟩
    rw [Finset.coe_image, ← map_span, hs]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Ideal (goal)
Goal:
R : Type u_3
S : Type u_4
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
h : I.FG
f : R →+* S
obtain : ∀ (s : Finset R) (hs : span (↑s : Set R) = I), FG.{u_4} (R := S) (Ideal.map f I)
⊢ FG.{u_4} (R := S) (Ideal.map f I)
have obtain₁ : ∀ (s : Finset R) (hs : span (↑s : Set R) = I),
  Eq (α := Ideal S) (span (↑(Finset.image (⇑f : (a : R) → S) s) : Set S)) (Ideal.map f I)
Tactic: classical
    obtain ⟨s, hs⟩ := h
    refine ⟨s.image f, ?_⟩
    rw [Finset.coe_image, ← map_span, hs]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Ideal (goal)
Goal:
R : Type u_3
inst : CommSemiring R
I : Ideal R
h : I.radical.FG
⊢ ∃ (n : ℕ), I.radical ^ n ≤ I
have suffices : ∀ (J : Ideal R), J.FG → J ≤ I.radical → ∃ (n : ℕ), J ^ n ≤ I
Tactic: suffices hJ : ∀ J : Ideal R, J.FG → J ≤ I.radical → ∃ n : ℕ, J ^ n ≤ I by
    simpa using hJ I.radical h
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Ideal (goal)
Goal:
R : Type u_3
inst : CommSemiring R
I : Ideal R
h : I.radical.FG
J : Ideal R
x : R
hJK : R ∙ x ≤ I.radical
⊢ ∃ (n : ℕ), HPow.hPow (α := Ideal R) (R ∙ x) n ≤ I
have singleton : ∀ (n : ℕ) (hn : x ^ n ∈ I), ∃ (n : ℕ), HPow.hPow (α := Ideal R) (R ∙ x) n ≤ I
Tactic: obtain ⟨n, hn⟩ := hJK (subset_span (Set.mem_singleton x))
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Ideal (goal)
Goal:
R : Type u_3
inst : CommSemiring R
I : Ideal R
h : I.radical.FG
J : Ideal R
x : R
hJK : R ∙ x ≤ I.radical
n : ℕ
hn : x ^ n ∈ I
⊢ HPow.hPow (α := Ideal R) (R ∙ x) n ≤ I
have rwa : HPow.hPow (α := Ideal R) (span {x}) n ≤ I
Tactic: rwa [← span, span_singleton_pow, span_le, Set.singleton_subset_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Ideal (goal)
Goal:
R : Type u_3
inst : CommSemiring R
I : Ideal R
h : I.radical.FG
J : Ideal R
x : R
hJK : R ∙ x ≤ I.radical
n : ℕ
hn : x ^ n ∈ I
rwa : HPow.hPow (α := Ideal R) (span {x}) n ≤ I
⊢ HPow.hPow (α := Ideal R) (R ∙ x) n ≤ I
have rwa₁ : span {x ^ n} ≤ I
Tactic: rwa [← span, span_singleton_pow, span_le, Set.singleton_subset_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Ideal (goal)
Goal:
R : Type u_3
inst : CommSemiring R
I : Ideal R
h : I.radical.FG
J : Ideal R
x : R
hJK : R ∙ x ≤ I.radical
n : ℕ
hn : x ^ n ∈ I
rwa : HPow.hPow (α := Ideal R) (span {x}) n ≤ I
rwa₁ : span {x ^ n} ≤ I
⊢ HPow.hPow (α := Ideal R) (R ∙ x) n ≤ I
have rwa₂ : {x ^ n} ⊆ (↑I : Set R)
Tactic: rwa [← span, span_singleton_pow, span_le, Set.singleton_subset_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Ideal (goal)
Goal:
R : Type u_3
inst : CommSemiring R
I : Ideal R
h : I.radical.FG
J : Ideal R
x : R
hJK : R ∙ x ≤ I.radical
n : ℕ
hn : x ^ n ∈ I
rwa : HPow.hPow (α := Ideal R) (span {x}) n ≤ I
rwa₁ : span {x ^ n} ≤ I
rwa₂ : {x ^ n} ⊆ (↑I : Set R)
⊢ HPow.hPow (α := Ideal R) (R ∙ x) n ≤ I
have rwa₃ : x ^ n ∈ (↑I : Set R)
Tactic: rwa [← span, span_singleton_pow, span_le, Set.singleton_subset_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Ideal (goal)
Goal:
R : Type u_3
inst : CommSemiring R
I : Ideal R
h : I.radical.FG
J_1 : Ideal R
J K : Submodule R R
hN₁ : J.FG
hN₂ : K.FG
hJ : ∀ (hJK : J ≤ I.radical), ∃ (n : ℕ), J ^ n ≤ I
hK : ∀ (hJK : K ≤ I.radical), ∃ (n : ℕ), K ^ n ≤ I
hJK : J ⊔ K ≤ I.radical
⊢ ∃ (n : ℕ), (J ⊔ K) ^ n ≤ I
have sup : ∀ (n : ℕ) (hn : J ^ n ≤ I), ∃ (n : ℕ), (J ⊔ K) ^ n ≤ I
Tactic: obtain ⟨n, hn⟩ := hJ fun x hx => hJK <| mem_sup_left hx
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Ideal (goal)
Goal:
R : Type u_3
inst : CommSemiring R
I : Ideal R
h : I.radical.FG
J_1 : Ideal R
J K : Submodule R R
hN₁ : J.FG
hN₂ : K.FG
hJ : ∀ (hJK : J ≤ I.radical), ∃ (n : ℕ), J ^ n ≤ I
hK : ∀ (hJK : K ≤ I.radical), ∃ (n : ℕ), K ^ n ≤ I
hJK : J ⊔ K ≤ I.radical
n : ℕ
hn : J ^ n ≤ I
⊢ ∃ (n : ℕ), (J ⊔ K) ^ n ≤ I
have sup : ∀ (m : ℕ) (hm : K ^ m ≤ I), ∃ (n : ℕ), (J ⊔ K) ^ n ≤ I
Tactic: obtain ⟨m, hm⟩ := hK fun x hx => hJK <| mem_sup_right hx
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Ideal (goal)
Goal:
R : Type u_3
inst : CommSemiring R
I : Ideal R
h : I.radical.FG
J_1 : Ideal R
J K : Submodule R R
hN₁ : J.FG
hN₂ : K.FG
hJ : ∀ (hJK : J ≤ I.radical), ∃ (n : ℕ), J ^ n ≤ I
hK : ∀ (hJK : K ≤ I.radical), ∃ (n : ℕ), K ^ n ≤ I
hJK : J ⊔ K ≤ I.radical
n : ℕ
hn : J ^ n ≤ I
m : ℕ
hm : K ^ m ≤ I
⊢ ∃ (n : ℕ), (J ⊔ K) ^ n ≤ I
have h₁ : (J ⊔ K) ^ (n + m) ≤ I
Tactic: use n + m
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Ideal (goal)
Goal:
R : Type u_3
inst : CommSemiring R
I : Ideal R
h : I.radical.FG
J_1 : Ideal R
J K : Submodule R R
hN₁ : J.FG
hN₂ : K.FG
hJ : ∀ (hJK : J ≤ I.radical), ∃ (n : ℕ), J ^ n ≤ I
hK : ∀ (hJK : K ≤ I.radical), ∃ (n : ℕ), K ^ n ≤ I
hJK : J ⊔ K ≤ I.radical
n : ℕ
hn : J ^ n ≤ I
m : ℕ
hm : K ^ m ≤ I
⊢ (J ⊔ K) ^ (n + m) ≤ I
have h₁ : ∀ b ∈ Finset.range (n + m + 1), J ^ b * K ^ (n + m - b) * (↑((n + m).choose b) : Ideal R) ≤ I
Tactic: rw [← add_eq_sup, add_pow, sum_eq_sup, Finset.sup_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Ideal (goal)
Goal:
R : Type u_3
inst : CommSemiring R
I : Ideal R
h : I.radical.FG
J_1 : Ideal R
J K : Submodule R R
hN₁ : J.FG
hN₂ : K.FG
hJ : ∀ (hJK : J ≤ I.radical), ∃ (n : ℕ), J ^ n ≤ I
hK : ∀ (hJK : K ≤ I.radical), ∃ (n : ℕ), K ^ n ≤ I
hJK : J ⊔ K ≤ I.radical
n : ℕ
hn : J ^ n ≤ I
m : ℕ
hm : K ^ m ≤ I
⊢ ∀ b ∈ Finset.range (n + m + 1), J ^ b * K ^ (n + m - b) * (↑((n + m).choose b) : Ideal R) ≤ I
have h₁ : ∀ i ∈ Finset.range (n + m + 1), J ^ i * K ^ (n + m - i) ≤ I
Tactic: refine fun i _ => mul_le_right.trans ?_
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Ideal (goal)
Goal:
R : Type u_3
inst : CommSemiring R
I : Ideal R
h : I.radical.FG
J_1 : Ideal R
J K : Submodule R R
hN₁ : J.FG
hN₂ : K.FG
hJ : ∀ (hJK : J ≤ I.radical), ∃ (n : ℕ), J ^ n ≤ I
hK : ∀ (hJK : K ≤ I.radical), ∃ (n : ℕ), K ^ n ≤ I
hJK : J ⊔ K ≤ I.radical
n : ℕ
hn : J ^ n ≤ I
m : ℕ
hm : K ^ m ≤ I
i : ℕ
h_1 : i ∈ Finset.range (n + m + 1)
⊢ J ^ i * K ^ (n + m - i) ≤ I
have h₁ : ∀ (h : n ≤ i), J ^ i * K ^ (n + m - i) ≤ I
Tactic: obtain h | h := le_or_gt n i
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Ideal (goal)
Goal:
R : Type u_3
inst : CommSemiring R
I : Ideal R
h : I.radical.FG
J_1 : Ideal R
J K : Submodule R R
hN₁ : J.FG
hN₂ : K.FG
hJ : ∀ (hJK : J ≤ I.radical), ∃ (n : ℕ), J ^ n ≤ I
hK : ∀ (hJK : K ≤ I.radical), ∃ (n : ℕ), K ^ n ≤ I
hJK : J ⊔ K ≤ I.radical
n : ℕ
hn : J ^ n ≤ I
m : ℕ
hm : K ^ m ≤ I
i : ℕ
h_1 : i ∈ Finset.range (n + m + 1)
h₁ : ∀ (h : n ≤ i), J ^ i * K ^ (n + m - i) ≤ I
⊢ J ^ i * K ^ (n + m - i) ≤ I
have h₂ : ∀ (h : i < n), J ^ i * K ^ (n + m - i) ≤ I
Tactic: obtain h | h := le_or_gt n i
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Ideal (goal)
Goal:
R : Type u_3
inst : CommSemiring R
I : Ideal R
h : I.radical.FG
J : Ideal R
hJ : J.FG
hJK : J ≤ I.radical
⊢ ∃ (n : ℕ), J ^ n ≤ I
have singleton : ∀ (x : R) (hJK : R ∙ x ≤ I.radical), ∃ (n : ℕ), HPow.hPow (α := Ideal R) (R ∙ x) n ≤ I
Tactic: induction J, hJ using Submodule.fg_induction with
  | singleton x =>
    obtain ⟨n, hn⟩ := hJK (subset_span (Set.mem_singleton x))
    exact ⟨n, by rwa [← span, span_singleton_pow, span_le, Set.singleton_subset_iff]⟩
  | sup J K _ _ hJ hK =>
    obtain ⟨n, hn⟩ := hJ fun x hx => hJK <| mem_sup_left hx
    obtain ⟨m, hm⟩ := hK fun x hx => hJK <| mem_sup_right hx
    use n + m
    rw [← add_eq_sup, add_pow, sum_eq_sup, Finset.sup_le_iff]
    refine fun i _ => mul_le_right.trans ?_
    obtain h | h := le_or_gt n i
    · exact mul_le_right.trans ((pow_le_pow_right h).trans hn)
    · exact mul_le_left.trans ((pow_le_pow_right (by lia)).trans hm)
Cleared hypotheses: hJ, hJK
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Ideal (goal)
Goal:
R : Type u_3
inst : CommSemiring R
I : Ideal R
h : I.radical.FG
J : Ideal R
hJ : J.FG
hJK : J ≤ I.radical
singleton : ∀ (x : R) (hJK : R ∙ x ≤ I.radical), ∃ (n : ℕ), HPow.hPow (α := Ideal R) (R ∙ x) n ≤ I
⊢ ∃ (n : ℕ), J ^ n ≤ I
have sup : ∀ (J K : Submodule R R),
  J.FG →
    K.FG →
      ∀ (hJ : ∀ (hJK : J ≤ I.radical), ∃ (n : ℕ), J ^ n ≤ I) (hK : ∀ (hJK : K ≤ I.radical), ∃ (n : ℕ), K ^ n ≤ I)
        (hJK : J ⊔ K ≤ I.radical), ∃ (n : ℕ), (J ⊔ K) ^ n ≤ I
Tactic: induction J, hJ using Submodule.fg_induction with
  | singleton x =>
    obtain ⟨n, hn⟩ := hJK (subset_span (Set.mem_singleton x))
    exact ⟨n, by rwa [← span, span_singleton_pow, span_le, Set.singleton_subset_iff]⟩
  | sup J K _ _ hJ hK =>
    obtain ⟨n, hn⟩ := hJ fun x hx => hJK <| mem_sup_left hx
    obtain ⟨m, hm⟩ := hK fun x hx => hJK <| mem_sup_right hx
    use n + m
    rw [← add_eq_sup, add_pow, sum_eq_sup, Finset.sup_le_iff]
    refine fun i _ => mul_le_right.trans ?_
    obtain h | h := le_or_gt n i
    · exact mul_le_right.trans ((pow_le_pow_right h).trans hn)
    · exact mul_le_left.trans ((pow_le_pow_right (by lia)).trans hm)
Cleared hypotheses: hJ, hJK
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Ideal (goal)
Goal:
R : Type u_3
inst : CommSemiring R
I J : Ideal R
hIJ : I ≤ J.radical
hJ : J.radical.FG
⊢ ∃ (k : ℕ), I ^ k ≤ J
have obtain : ∀ (k : ℕ) (hk : J.radical ^ k ≤ J), ∃ (k : ℕ), I ^ k ≤ J
Tactic: obtain ⟨k, hk⟩ := J.exists_radical_pow_le_of_fg hJ
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Ideal (hypothesis)
Goal:
R : Type u_3
inst : CommSemiring R
I J : Ideal R
x : R
h' : R ∙ x ≤ J.radical
⊢ ∃ (n : ℕ), HPow.hPow (α := Ideal R) (R ∙ x) n ≤ J
have h'₁ : x ∈ J.radical
Tactic: simp only [submodule_span_eq, span_le, Set.singleton_subset_iff, SetLike.mem_coe] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Ideal (goal)
Goal:
R : Type u_3
inst : CommSemiring R
I J : Ideal R
x : R
h' : x ∈ J.radical
⊢ ∃ (n : ℕ), HPow.hPow (α := Ideal R) (R ∙ x) n ≤ J
have singleton : ∀ (n : ℕ) (hn : x ^ n ∈ J), ∃ (n : ℕ), HPow.hPow (α := Ideal R) (R ∙ x) n ≤ J
Tactic: obtain ⟨n, hn⟩ := h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Ideal (goal)
Goal:
R : Type u_3
inst : CommSemiring R
I J : Ideal R
I₁ I₂ : Submodule R R
hN₁ : I₁.FG
hN₂ : I₂.FG
h₁ : ∀ (h' : I₁ ≤ J.radical), ∃ (n : ℕ), I₁ ^ n ≤ J
h₂ : ∀ (h' : I₂ ≤ J.radical), ∃ (n : ℕ), I₂ ^ n ≤ J
h' : I₁ ⊔ I₂ ≤ J.radical
⊢ ∃ (n : ℕ), (I₁ ⊔ I₂) ^ n ≤ J
have sup : ∀ (n₁ : ℕ) (hn₁ : I₁ ^ n₁ ≤ J), ∃ (n : ℕ), (I₁ ⊔ I₂) ^ n ≤ J
Tactic: obtain ⟨n₁, hn₁⟩ := h₁ (le_sup_left.trans h')
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Ideal (goal)
Goal:
R : Type u_3
inst : CommSemiring R
I J : Ideal R
I₁ I₂ : Submodule R R
hN₁ : I₁.FG
hN₂ : I₂.FG
h₁ : ∀ (h' : I₁ ≤ J.radical), ∃ (n : ℕ), I₁ ^ n ≤ J
h₂ : ∀ (h' : I₂ ≤ J.radical), ∃ (n : ℕ), I₂ ^ n ≤ J
h' : I₁ ⊔ I₂ ≤ J.radical
n₁ : ℕ
hn₁ : I₁ ^ n₁ ≤ J
⊢ ∃ (n : ℕ), (I₁ ⊔ I₂) ^ n ≤ J
have sup : ∀ (n₂ : ℕ) (hn₂ : I₂ ^ n₂ ≤ J), ∃ (n : ℕ), (I₁ ⊔ I₂) ^ n ≤ J
Tactic: obtain ⟨n₂, hn₂⟩ := h₂ (le_sup_right.trans h')
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Ideal (goal)
Goal:
R : Type u_3
inst : CommSemiring R
I J : Ideal R
I₁ I₂ : Submodule R R
hN₁ : I₁.FG
hN₂ : I₂.FG
h₁ : ∀ (h' : I₁ ≤ J.radical), ∃ (n : ℕ), I₁ ^ n ≤ J
h₂ : ∀ (h' : I₂ ≤ J.radical), ∃ (n : ℕ), I₂ ^ n ≤ J
h' : I₁ ⊔ I₂ ≤ J.radical
n₁ : ℕ
hn₁ : I₁ ^ n₁ ≤ J
n₂ : ℕ
hn₂ : I₂ ^ n₂ ≤ J
⊢ ∃ (n : ℕ), (I₁ ⊔ I₂) ^ n ≤ J
have h : (I₁ ⊔ I₂) ^ (n₁ + n₂) ≤ J
Tactic: use n₁ + n₂