awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
Goal:
M : Type u_1
R : Type u_2
S : Type u_3
inst : Finite M
inst_1 : Semiring R
inst_2 : Semiring S
inst_3 : Module R S
inst_4 : Module.Finite R S
⊢ Module.Finite R S[M]

Tactic:
.finsupp

Premises used: MonoidAlgebra, Module.Finite.finsupp
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
Goal:
σ : Type u_1
inst : Finite σ
⊢ Module.Finite.{0, u_1} ℤ (FreeAbelianGroup σ)

Tactic:
.of_surjective _ (FreeAbelianGroup.equivFinsupp σ).toIntLinearEquiv.symm.surjective

Premises used: Module.Finite.of_surjective, LinearEquiv.symm, AddEquiv.toIntLinearEquiv, LinearEquiv.surjective, FreeAbelianGroup.equivFinsupp
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
Goal:
σ : Type u_1
inst : Finite σ
rw : Module.Finite.{0, u_1} ℤ (FreeAbelianGroup σ)
⊢ AddMonoid.FG.{u_1} (FreeAbelianGroup σ)

Tactic:
rw [← AddGroup.fg_iff_addMonoid_fg, ← Module.Finite.iff_addGroup_fg]

Premises used: AddGroup.fg_iff_addMonoid_fg, Module.Finite.iff_addGroup_fg
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
Goal:
σ : Type u_1
inst : Finite σ
⊢ Module.Finite.{0, u_1} ℤ (FreeAbelianGroup σ)

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

Tactic:
obtain ⟨s, hs⟩ := h
-- Module: Mathlib.RingTheory.Finiteness.Ideal
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) (map f I)

Tactic:
⟨s.image f, ?_⟩

Premises used: Ideal.FG, Exists.intro, DFunLike.coe, Finset.image
-- Module: Mathlib.RingTheory.Finiteness.Ideal
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
refine : Eq (α := Ideal S) (span (↑(Finset.image (⇑f : (a : R) → S) s) : Set S)) (Ideal.map f I)
⊢ FG.{u_4} (R := S) (Ideal.map f I)

Tactic:
refine ⟨s.image f, ?_⟩
-- Module: Mathlib.RingTheory.Finiteness.Ideal
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)
rw₂ rw₃ : Eq.{u_4 + 1} (α := Ideal S) (Ideal.map f I) (Ideal.map f I)
⊢ Eq (α := Ideal S) (span (↑(Finset.image (⇑f : (a : R) → S) s) : Set S)) (Ideal.map f I)

Tactic:
rw [Finset.coe_image, ← map_span, hs]

Premises used: Ideal.map_span, Finset.coe_image
-- Module: Mathlib.RingTheory.Finiteness.Ideal
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)
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)
⊢ 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]

Premises used: Ideal.map_span, Finset.coe_image
-- Module: Mathlib.RingTheory.Finiteness.Ideal
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
f : R →+* S
g : S →+* A
hf : FG (RingHom.ker f)
hg : FG (RingHom.ker g)
hsur : Surjective.{u_3 + 1, u_4 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
this_1 : Algebra R S := f.toAlgebra
this_2 : Algebra R A := (g.comp f).toAlgebra
this_3 : Algebra S A := g.toAlgebra
this : IsScalarTower R S A := ⋯
f₁ : R →ₗ[R] S := Algebra.linearMap R S
g₁ : S →ₗ[R] A := AlgHom.toLinearMap (IsScalarTower.toAlgHom R S A)
⊢ FG (RingHom.ker (g.comp f))

Tactic:
Submodule.fg_ker_comp f₁ g₁ hf
    (Submodule.FG.restrictScalars_of_surjective hg hsur) hsur

Premises used: Submodule.FG.restrictScalars_of_surjective, LinearMap.ker, Submodule.FG, Ideal.FG, Ideal.comap, Submodule.fg_ker_comp, RingHom.ker
-- Module: Mathlib.RingTheory.Finiteness.Ideal
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
f : R →+* S
g : S →+* A
hf : FG (RingHom.ker f)
hg : FG (RingHom.ker g)
hsur : Surjective.{u_3 + 1, u_4 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
this_1 : Algebra R S := f.toAlgebra
this_2 : Algebra R A := (g.comp f).toAlgebra
this_3 : Algebra S A := g.toAlgebra
this : IsScalarTower R S A := ⋯
f₁ : R →ₗ[R] S := Algebra.linearMap R S
g₁ : S →ₗ[R] A := AlgHom.toLinearMap (IsScalarTower.toAlgHom R S A)
⊢ FG (RingHom.ker (g.comp f))

Tactic:
exact Submodule.fg_ker_comp f₁ g₁ hf
    (Submodule.FG.restrictScalars_of_surjective hg hsur) hsur

Premises used: Submodule.FG.restrictScalars_of_surjective, Submodule.fg_ker_comp
-- Module: Mathlib.RingTheory.Finiteness.Ideal
Goal:
R : Type u_3
inst : CommSemiring R
I : Ideal R
h : I.radical.FG
hJ : ∀ (J : Ideal R), J.FG → J ≤ I.radical → ∃ (n : ℕ), J ^ n ≤ I
⊢ ∃ (n : ℕ), I.radical ^ n ≤ I

Tactic:
simpa using hJ I.radical h

Premises used: Ideal.radical
-- Module: Mathlib.RingTheory.Finiteness.Ideal
Goal:
R : Type u_3
inst : CommSemiring R
I : Ideal R
h : I.radical.FG
suffices : ∀ (J : Ideal R), J.FG → J ≤ I.radical → ∃ (n : ℕ), J ^ n ≤ I
⊢ ∃ (n : ℕ), I.radical ^ n ≤ I

Tactic:
suffices hJ : ∀ J : Ideal R, J.FG → J ≤ I.radical → ∃ n : ℕ, J ^ n ≤ I by
    simpa using hJ I.radical h
-- Module: Mathlib.RingTheory.Finiteness.Ideal
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
singleton : ∀ (n : ℕ) (hn : x ^ n ∈ I), ∃ (n : ℕ), HPow.hPow (α := Ideal R) (R ∙ x) n ≤ I
⊢ ∃ (n : ℕ), HPow.hPow (α := Ideal R) (R ∙ x) n ≤ I

Tactic:
obtain ⟨n, hn⟩ := hJK (subset_span (Set.mem_singleton x))

Premises used: Set.mem_singleton, Ideal.subset_span
-- Module: Mathlib.RingTheory.Finiteness.Ideal
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)
rwa₃ rwa₄ rwa₅ rwa₆ : x ^ n ∈ (↑I : Set R)
⊢ HPow.hPow (α := Ideal R) (R ∙ x) n ≤ I

Tactic:
rwa [← span, span_singleton_pow, span_le, Set.singleton_subset_iff]

Premises used: Ideal.span_le, Set.singleton_subset_iff, Ideal.span, Ideal.span_singleton_pow
-- Module: Mathlib.RingTheory.Finiteness.Ideal
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
⊢ ∃ (n : ℕ), HPow.hPow (α := Ideal R) (R ∙ x) n ≤ I

Tactic:
exact ⟨n, by rwa [← span, span_singleton_pow, span_le, Set.singleton_subset_iff]⟩
-- Module: Mathlib.RingTheory.Finiteness.Ideal
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
sup : ∀ (n : ℕ) (hn : J ^ n ≤ I), ∃ (n : ℕ), (J ⊔ K) ^ n ≤ I
⊢ ∃ (n : ℕ), (J ⊔ K) ^ n ≤ I

Tactic:
obtain ⟨n, hn⟩ := hJ fun x hx => hJK <| mem_sup_left hx

Premises used: Ideal.mem_sup_left
-- Module: Mathlib.RingTheory.Finiteness.Ideal
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
sup : ∀ (m : ℕ) (hm : K ^ m ≤ I), ∃ (n : ℕ), (J ⊔ K) ^ n ≤ I
⊢ ∃ (n : ℕ), (J ⊔ K) ^ n ≤ I

Tactic:
obtain ⟨m, hm⟩ := hK fun x hx => hJK <| mem_sup_right hx

Premises used: Ideal.mem_sup_right
-- Module: Mathlib.RingTheory.Finiteness.Ideal
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
h₁ : (J ⊔ K) ^ (n + m) ≤ I
⊢ ∃ (n : ℕ), (J ⊔ K) ^ n ≤ I

Tactic:
use n + m
-- Module: Mathlib.RingTheory.Finiteness.Ideal
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
h₁ : ∀ b ∈ Finset.range (n + m + 1), J ^ b * K ^ (n + m - b) * (↑((n + m).choose b) : Ideal R) ≤ I
⊢ (J ⊔ K) ^ (n + m) ≤ I

Tactic:
rw [← add_eq_sup, add_pow, sum_eq_sup, Finset.sup_le_iff]

Premises used: Ideal.sum_eq_sup, Ideal.add_eq_sup, add_pow, Finset.sup_le_iff
-- Module: Mathlib.RingTheory.Finiteness.Ideal
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

Tactic:
fun i _ => mul_le_right.trans ?_

Premises used: Ideal.mul_le_right, Set.Mem, LE.le.trans
-- Module: Mathlib.RingTheory.Finiteness.Ideal
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
h₁ : ∀ i ∈ Finset.range (n + m + 1), J ^ i * K ^ (n + m - i) ≤ I
⊢ ∀ b ∈ Finset.range (n + m + 1), J ^ b * K ^ (n + m - b) * (↑((n + m).choose b) : Ideal R) ≤ I

Tactic:
refine fun i _ => mul_le_right.trans ?_

Premises used: Ideal.mul_le_right, LE.le.trans
-- Module: Mathlib.RingTheory.Finiteness.Ideal
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
h₂ : ∀ (h : i < n), J ^ i * K ^ (n + m - i) ≤ I
⊢ J ^ i * K ^ (n + m - i) ≤ I

Tactic:
obtain h | h := le_or_gt n i

Premises used: le_or_gt
-- Module: Mathlib.RingTheory.Finiteness.Ideal
Goal:
R : Type u_3
inst : CommSemiring R
I : Ideal R
h_1 : 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_2 : i ∈ Finset.range (n + m + 1)
h : n ≤ i
⊢ J ^ i * K ^ (n + m - i) ≤ I

Tactic:
mul_le_right.trans ((pow_le_pow_right h).trans hn)

Premises used: Ideal.mul_le_right, Set.Mem, Ideal.pow_le_pow_right, LE.le.trans
-- Module: Mathlib.RingTheory.Finiteness.Ideal
Goal:
R : Type u_3
inst : CommSemiring R
I : Ideal R
h_1 : 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_2 : i ∈ Finset.range (n + m + 1)
h : n ≤ i
⊢ J ^ i * K ^ (n + m - i) ≤ I

Tactic:
exact mul_le_right.trans ((pow_le_pow_right h).trans hn)

Premises used: Ideal.mul_le_right, Ideal.pow_le_pow_right, LE.le.trans
-- Module: Mathlib.RingTheory.Finiteness.Ideal
Goal:
R : Type u_3
inst : CommSemiring R
I : Ideal R
h_1 : 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_2 : i ∈ Finset.range (n + m + 1)
h : i < n
⊢ m ≤ n + m - i

Tactic:
lia
-- Module: Mathlib.RingTheory.Finiteness.Ideal
Goal:
R : Type u_3
inst : CommSemiring R
I : Ideal R
h_1 : 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_2 : i ∈ Finset.range (n + m + 1)
h : i < n
⊢ J ^ i * K ^ (n + m - i) ≤ I

Tactic:
exact mul_le_left.trans ((pow_le_pow_right (by lia)).trans hm)

Premises used: Ideal.pow_le_pow_right, Ideal.mul_le_left, LE.le.trans
-- Module: Mathlib.RingTheory.Finiteness.Ideal
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
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
⊢ ∃ (n : ℕ), J ^ 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)

Premises used: Ideal.mul_le_right, Ideal.sum_eq_sup, Ideal.add_eq_sup, add_pow, Finset.sup_le_iff, Submodule.fg_induction, LE.le.trans, Singleton.singleton
-- Module: Mathlib.RingTheory.Finiteness.Ideal
Goal:
R : Type u_3
inst : CommSemiring R
I J : Ideal R
hIJ : I ≤ J.radical
hJ : J.radical.FG
obtain : ∀ (k : ℕ) (hk : J.radical ^ k ≤ J), ∃ (k : ℕ), I ^ k ≤ J
⊢ ∃ (k : ℕ), I ^ k ≤ J

Tactic:
obtain ⟨k, hk⟩ := J.exists_radical_pow_le_of_fg hJ

Premises used: Ideal.exists_radical_pow_le_of_fg
-- Module: Mathlib.RingTheory.Finiteness.Ideal
Goal:
R : Type u_3
inst : CommSemiring R
I J : Ideal R
hIJ : I ≤ J.radical
hJ : J.radical.FG
k : ℕ
hk : J.radical ^ k ≤ J
⊢ ∃ (k : ℕ), I ^ k ≤ J

Tactic:
⟨k, (pow_right_mono hIJ k).trans hk⟩

Premises used: Ideal.pow_right_mono, Exists.intro, LE.le.trans
-- Module: Mathlib.RingTheory.Finiteness.Ideal
Goal:
R : Type u_3
inst : CommSemiring R
I J : Ideal R
hIJ : I ≤ J.radical
hJ : J.radical.FG
k : ℕ
hk : J.radical ^ k ≤ J
⊢ ∃ (k : ℕ), I ^ k ≤ J

Tactic:
exact ⟨k, (pow_right_mono hIJ k).trans hk⟩
-- Module: Mathlib.RingTheory.Finiteness.Ideal
Goal:
R : Type u_3
inst : CommSemiring R
I J : Ideal R
x : R
h' : R ∙ x ≤ J.radical
⊢ x ∈ J.radical

Tactic:
simp only [submodule_span_eq, span_le, Set.singleton_subset_iff, SetLike.mem_coe] at h'

Premises used: Ideal.span_le, Set.singleton_subset_iff, Ideal.submodule_span_eq, SetLike.mem_coe
-- Module: Mathlib.RingTheory.Finiteness.Ideal
Goal:
R : Type u_3
inst : CommSemiring R
I J : Ideal R
x : R
h' : x ∈ J.radical
singleton : ∀ (n : ℕ) (hn : x ^ n ∈ J), ∃ (n : ℕ), HPow.hPow (α := Ideal R) (R ∙ x) n ≤ J
⊢ ∃ (n : ℕ), HPow.hPow (α := Ideal R) (R ∙ x) n ≤ J

Tactic:
obtain ⟨n, hn⟩ := h'
-- Module: Mathlib.RingTheory.Finiteness.Ideal
Goal:
R : Type u_3
inst : CommSemiring R
I J : Ideal R
x : R
n : ℕ
hn : x ^ n ∈ J
⊢ HPow.hPow (α := Ideal R) (R ∙ x) n ≤ J

Tactic:
simpa [span_singleton_pow, span_le]

Premises used: Ideal.span_le, Ideal.span_singleton_pow
-- Module: Mathlib.RingTheory.Finiteness.Ideal
Goal:
R : Type u_3
inst : CommSemiring R
I J : Ideal R
x : R
n : ℕ
hn : x ^ n ∈ J
⊢ ∃ (n : ℕ), HPow.hPow (α := Ideal R) (R ∙ x) n ≤ J

Tactic:
refine ⟨n, by simpa [span_singleton_pow, span_le]⟩
-- Module: Mathlib.RingTheory.Finiteness.Ideal
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
sup : ∀ (n₁ : ℕ) (hn₁ : I₁ ^ n₁ ≤ J), ∃ (n : ℕ), (I₁ ⊔ I₂) ^ n ≤ J
⊢ ∃ (n : ℕ), (I₁ ⊔ I₂) ^ n ≤ J

Tactic:
obtain ⟨n₁, hn₁⟩ := h₁ (le_sup_left.trans h')

Premises used: le_sup_left, LE.le.trans
-- Module: Mathlib.RingTheory.Finiteness.Ideal
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
sup : ∀ (n₂ : ℕ) (hn₂ : I₂ ^ n₂ ≤ J), ∃ (n : ℕ), (I₁ ⊔ I₂) ^ n ≤ J
⊢ ∃ (n : ℕ), (I₁ ⊔ I₂) ^ n ≤ J

Tactic:
obtain ⟨n₂, hn₂⟩ := h₂ (le_sup_right.trans h')

Premises used: le_sup_right, LE.le.trans
-- Module: Mathlib.RingTheory.Finiteness.Ideal
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
h : (I₁ ⊔ I₂) ^ (n₁ + n₂) ≤ J
⊢ ∃ (n : ℕ), (I₁ ⊔ I₂) ^ n ≤ J

Tactic:
use n₁ + n₂
-- Module: Mathlib.RingTheory.Finiteness.Ideal
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
⊢ (I₁ ⊔ I₂) ^ (n₁ + n₂) ≤ J

Tactic:
sup_pow_add_le_pow_sup_pow.trans (sup_le hn₁ hn₂)

Premises used: Set.Mem, setOf, Ideal.sup_pow_add_le_pow_sup_pow, sup_le, LE.le.trans
-- Module: Mathlib.RingTheory.Finiteness.Ideal
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
⊢ (I₁ ⊔ I₂) ^ (n₁ + n₂) ≤ J

Tactic:
exact sup_pow_add_le_pow_sup_pow.trans (sup_le hn₁ hn₂)

Premises used: Ideal.sup_pow_add_le_pow_sup_pow, sup_le, LE.le.trans
-- Module: Mathlib.RingTheory.Finiteness.Ideal
Goal:
R : Type u_3
inst : CommSemiring R
I J : Ideal R
h' : I ≤ J.radical
h : I.FG
singleton : ∀ (x : R) (h' : R ∙ x ≤ J.radical), ∃ (n : ℕ), HPow.hPow (α := Ideal R) (R ∙ x) n ≤ J
sup :
  ∀ (I₁ I₂ : Submodule R R),
    I₁.FG →
      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
⊢ ∃ (n : ℕ), I ^ n ≤ J

Tactic:
induction I, h using Submodule.fg_induction with
  | singleton x =>
    simp only [submodule_span_eq, span_le, Set.singleton_subset_iff, SetLike.mem_coe] at h'
    obtain ⟨n, hn⟩ := h'
    refine ⟨n, by simpa [span_singleton_pow, span_le]⟩
  | sup I₁ I₂ _ _ h₁ h₂ =>
    obtain ⟨n₁, hn₁⟩ := h₁ (le_sup_left.trans h')
    obtain ⟨n₂, hn₂⟩ := h₂ (le_sup_right.trans h')
    use n₁ + n₂
    exact sup_pow_add_le_pow_sup_pow.trans (sup_le hn₁ hn₂)

Premises used: Ideal.span_le, Set.singleton_subset_iff, Ideal.submodule_span_eq, SetLike.mem_coe, Submodule.fg_induction, Singleton.singleton
-- Module: Mathlib.RingTheory.Finiteness.Ideal
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
I : Ideal R
inst_3 : I.IsTwoSided
N : Submodule R M
hI : I.FG
hN : N.FG
obtain : ∀ (s : Finset R) [IsTwoSided (span (↑s : Set R))], (HSMul.hSMul (α := Ideal R) (span (↑s : Set R)) N).FG
⊢ (I • N).FG

Tactic:
obtain ⟨s, rfl⟩ := hI

Premises used: rfl
-- Module: Mathlib.RingTheory.Finiteness.Ideal
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
hN : N.FG
s : Finset R
inst_3 : IsTwoSided (span (↑s : Set R))
obtain :
  ∀ (t : Finset M),
    (HSMul.hSMul (α := Ideal R) (β := Submodule R M) (span (↑s : Set R)) (Submodule.span R (↑t : Set M))).FG
⊢ (HSMul.hSMul (α := Ideal R) (span (↑s : Set R)) N).FG

Tactic:
obtain ⟨t, rfl⟩ := hN

Premises used: rfl
-- Module: Mathlib.RingTheory.Finiteness.Ideal
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Finset R
inst_3 : IsTwoSided (span (↑s : Set R))
t : Finset M
rw : Submodule.FG (Submodule.span R (↑(s • t) : Set M))
⊢ (HSMul.hSMul (α := Ideal R) (β := Submodule R M) (span (↑s : Set R)) (Submodule.span R (↑t : Set M))).FG

Tactic:
rw [Submodule.span_smul_span, ← s.coe_smul]

Premises used: Submodule.span_smul_span, Finset.coe_smul
-- Module: Mathlib.RingTheory.Finiteness.Ideal
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Finset R
inst_3 : IsTwoSided (span (↑s : Set R))
t : Finset M
classical : Submodule.FG (Submodule.span R (↑(s • t) : Set M))
⊢ (HSMul.hSMul (α := Ideal R) (β := Submodule R M) (span (↑s : Set R)) (Submodule.span R (↑t : Set M))).FG

Tactic:
classical rw [Submodule.span_smul_span, ← s.coe_smul]

Premises used: Submodule.span_smul_span, Finset.coe_smul
-- Module: Mathlib.RingTheory.Finiteness.Ideal
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Finset R
inst_3 : IsTwoSided (span (↑s : Set R))
t : Finset M
⊢ Submodule.FG (Submodule.span R (↑(s • t) : Set M))

Tactic:
⟨_, rfl⟩

Premises used: Submodule.FG, Exists.intro, rfl
-- Module: Mathlib.RingTheory.Finiteness.Ideal
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Finset R
inst_3 : IsTwoSided (span (↑s : Set R))
t : Finset M
⊢ Submodule.FG (Submodule.span R (↑(s • t) : Set M))

Tactic:
exact ⟨_, rfl⟩
-- Module: Mathlib.RingTheory.Finiteness.Ideal
Goal:
R : Type u_1
inst : Semiring R
I J : Ideal R
inst_1 : I.IsTwoSided
hI : I.FG
hJ : J.FG
⊢ (I * J).FG

Tactic:
Submodule.FG.smul hI hJ

Premises used: Submodule.FG, Ideal.FG, Submodule.FG.smul
-- Module: Mathlib.RingTheory.Finiteness.Ideal
Goal:
R : Type u_1
inst : Semiring R
I : Ideal R
inst_1 : I.IsTwoSided
n : ℕ
hI : I.FG
rw : FG.{u_1} (R := R) ⊤
⊢ (I ^ Nat.zero).FG

Tactic:
rw [I.pow_zero, one_eq_top]

Premises used: Submodule.pow_zero, Ideal.one_eq_top
-- Module: Mathlib.RingTheory.Finiteness.Ideal
Goal:
R : Type u_1
inst : Semiring R
I : Ideal R
inst_1 : I.IsTwoSided
n : ℕ
hI : I.FG
⊢ FG.{u_1} (R := R) ⊤

Tactic:
fg_top R

Premises used: Ideal.fg_top
-- Module: Mathlib.RingTheory.Finiteness.Ideal
Goal:
R : Type u_1
inst : Semiring R
I : Ideal R
inst_1 : I.IsTwoSided
n : ℕ
hI : I.FG
⊢ FG.{u_1} (R := R) ⊤

Tactic:
exact fg_top R

Premises used: Ideal.fg_top
-- Module: Mathlib.RingTheory.Finiteness.Ideal
Goal:
R : Type u_1
inst : Semiring R
I : Ideal R
inst_1 : I.IsTwoSided
n_1 : ℕ
hI : I.FG
n : ℕ
ih : (I ^ n).FG
rw : (I * I ^ n).FG
⊢ (I ^ n.succ).FG

Tactic:
rw [IsTwoSided.pow_succ]

Premises used: Ideal.IsTwoSided.pow_succ
-- Module: Mathlib.RingTheory.Finiteness.Ideal
Goal:
R : Type u_1
inst : Semiring R
I : Ideal R
inst_1 : I.IsTwoSided
n_1 : ℕ
hI : I.FG
n : ℕ
ih : (I ^ n).FG
⊢ (I * I ^ n).FG

Tactic:
hI.mul ih

Premises used: Ideal.FG.mul
-- Module: Mathlib.RingTheory.Finiteness.Ideal
Goal:
R : Type u_1
inst : Semiring R
I : Ideal R
inst_1 : I.IsTwoSided
n_1 : ℕ
hI : I.FG
n : ℕ
ih : (I ^ n).FG
⊢ (I * I ^ n).FG

Tactic:
exact hI.mul ih

Premises used: Ideal.FG.mul
-- Module: Mathlib.RingTheory.Finiteness.Lattice
Goal:
R : Type u_2
V : Type u_3
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
ι : Sort u_1
inst_3 : Finite ι
S : ι → Submodule R V
inst_4 : ∀ (i : ι), Module.Finite.{u_2, u_3} R ↥(S i)
intro : ∀ (val : Fintype (PLift ι)), Module.Finite.{u_2, u_3} R ↥(⨆ (i : ι), S i)
⊢ Module.Finite.{u_2, u_3} R ↥(⨆ (i : ι), S i)

Tactic:
cases nonempty_fintype (PLift ι)

Premises used: PLift, nonempty_fintype