awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Noetherian.OfPrime
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I (↑(span {a}) : Set R)).FG
w : ℕ
f : Fin w → R
hf : span (Set.range f) = I ⊔ span {a}
w_1 : ℕ
i : Fin w_1 → R
hi : Submodule.span R (Set.range i) = Submodule.colon I (↑(span {a}) : Set R)
r p : (k : Fin w) → R
p_mem_I : ∀ (k : Fin w), p k ∈ I
Hf : ∀ (k : Fin w), r k * a + p k = f k
⊢ I.FG

Tactic:
⟨image p univ ∪ image (a • i) univ, le_antisymm ?_ (fun y hy ↦ ?_)⟩

Premises used: Finset.univ, Ideal.FG, le_antisymm, Exists.intro, HSMul.hSMul, Union.union, Finset.image
-- Module: Mathlib.RingTheory.Noetherian.OfPrime
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I (↑(span {a}) : Set R)).FG
w : ℕ
f : Fin w → R
hf : span (Set.range f) = I ⊔ span {a}
w_1 : ℕ
i : Fin w_1 → R
hi : Submodule.span R (Set.range i) = Submodule.colon I (↑(span {a}) : Set R)
r p : (k : Fin w) → R
p_mem_I : ∀ (k : Fin w), p k ∈ I
Hf : ∀ (k : Fin w), r k * a + p k = f k
refine_1 : span (↑(Finset.image p Finset.univ ∪ Finset.image (a • i) Finset.univ) : Set R) ≤ I
refine_2 :
  ∀ (y : R) (hy : y ∈ I),
    Membership.mem (γ := Submodule R R)
      (span (↑(Finset.image p Finset.univ ∪ Finset.image (a • i) Finset.univ) : Set R)) y
⊢ I.FG

Tactic:
refine ⟨image p univ ∪ image (a • i) univ, le_antisymm ?_ (fun y hy ↦ ?_)⟩
-- Module: Mathlib.RingTheory.Noetherian.OfPrime
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I (↑(span {a}) : Set R)).FG
w : ℕ
f : Fin w → R
hf : span (Set.range f) = I ⊔ span {a}
w_1 : ℕ
i : Fin w_1 → R
hi : Submodule.span R (Set.range i) = Submodule.colon I (↑(span {a}) : Set R)
r p : (k : Fin w) → R
p_mem_I : ∀ (k : Fin w), p k ∈ I
Hf : ∀ (k : Fin w), r k * a + p k = f k
refine_1 : span (Set.range p) ⊔ span (Set.range fun (a_1 : Fin w_1) ↦ a • i a_1) ≤ I
⊢ span (↑(Finset.image p Finset.univ ∪ Finset.image (a • i) Finset.univ) : Set R) ≤ I

Tactic:
simp only [coe_union, coe_image, coe_univ, image_univ, Pi.smul_apply, span_union]

Premises used: Set.image_univ, Finset.coe_univ, Finset.coe_image, Ideal.span_union, Finset.coe_union, Pi.smul_apply
-- Module: Mathlib.RingTheory.Noetherian.OfPrime
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I (↑(span {a}) : Set R)).FG
w : ℕ
f : Fin w → R
hf : span (Set.range f) = I ⊔ span {a}
w_1 : ℕ
i : Fin w_1 → R
hi : Submodule.span R (Set.range i) = Submodule.colon I (↑(span {a}) : Set R)
r p : (k : Fin w) → R
p_mem_I : ∀ (k : Fin w), p k ∈ I
Hf : ∀ (k : Fin w), r k * a + p k = f k
y : R
hy : y ∈ I
refine_2 : Membership.mem (γ := Submodule R R) (span (Set.range p) ⊔ span (Set.range fun (a_1 : Fin w_1) ↦ a • i a_1)) y
⊢ Membership.mem (γ := Submodule R R) (span (↑(Finset.image p Finset.univ ∪ Finset.image (a • i) Finset.univ) : Set R))
    y

Tactic:
simp only [coe_union, coe_image, coe_univ, image_univ, Pi.smul_apply, span_union]

Premises used: Set.image_univ, Finset.coe_univ, Finset.coe_image, Ideal.span_union, Finset.coe_union, Pi.smul_apply
-- Module: Mathlib.RingTheory.Noetherian.OfPrime
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I (↑(span {a}) : Set R)).FG
w : ℕ
f : Fin w → R
hf : span (Set.range f) = I ⊔ span {a}
w_1 : ℕ
i : Fin w_1 → R
hi : Submodule.span R (Set.range i) = Submodule.colon I (↑(span {a}) : Set R)
r p : (k : Fin w) → R
p_mem_I : ∀ (k : Fin w), p k ∈ I
Hf : ∀ (k : Fin w), r k * a + p k = f k
refine_1 : (∀ (y : Fin w), p y ∈ (↑I : Set R)) ∧ ∀ (y : Fin w_1), a * i y ∈ (↑I : Set R)
⊢ span (Set.range p) ⊔ span (Set.range fun (a_1 : Fin w_1) ↦ a • i a_1) ≤ I

Tactic:
simp only [sup_le_iff, span_le, range_subset_iff, smul_eq_mul]

Premises used: Ideal.span_le, sup_le_iff, smul_eq_mul, Set.range_subset_iff
-- Module: Mathlib.RingTheory.Noetherian.OfPrime
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I (↑(span {a}) : Set R)).FG
w : ℕ
f : Fin w → R
hf : span (Set.range f) = I ⊔ span {a}
w_1 : ℕ
i : Fin w_1 → R
hi : Submodule.span R (Set.range i) = Submodule.colon I (↑(span {a}) : Set R)
r p : (k : Fin w) → R
p_mem_I : ∀ (k : Fin w), p k ∈ I
Hf : ∀ (k : Fin w), r k * a + p k = f k
⊢ (∀ (y : Fin w), p y ∈ (↑I : Set R)) ∧ ∀ (y : Fin w_1), a * i y ∈ (↑I : Set R)

Tactic:
⟨p_mem_I, fun _ ↦ mul_comm a _ ▸ mem_colon_span_singleton.1 (hi ▸ mem_span_range_self)⟩

Premises used: Ideal.mem_colon_span_singleton, Ideal.mem_span_range_self, Eq.rec, And.intro, Iff.mp, mul_comm, Eq.symm
-- Module: Mathlib.RingTheory.Noetherian.OfPrime
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I (↑(span {a}) : Set R)).FG
w : ℕ
f : Fin w → R
hf : span (Set.range f) = I ⊔ span {a}
w_1 : ℕ
i : Fin w_1 → R
hi : Submodule.span R (Set.range i) = Submodule.colon I (↑(span {a}) : Set R)
r p : (k : Fin w) → R
p_mem_I : ∀ (k : Fin w), p k ∈ I
Hf : ∀ (k : Fin w), r k * a + p k = f k
⊢ (∀ (y : Fin w), p y ∈ (↑I : Set R)) ∧ ∀ (y : Fin w_1), a * i y ∈ (↑I : Set R)

Tactic:
exact ⟨p_mem_I, fun _ ↦ mul_comm a _ ▸ mem_colon_span_singleton.1 (hi ▸ mem_span_range_self)⟩
-- Module: Mathlib.RingTheory.Noetherian.OfPrime
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I (↑(span {a}) : Set R)).FG
w : ℕ
f : Fin w → R
hf : span (Set.range f) = I ⊔ span {a}
w_1 : ℕ
i : Fin w_1 → R
hi : Submodule.span R (Set.range i) = Submodule.colon I (↑(span {a}) : Set R)
r p : (k : Fin w) → R
p_mem_I : ∀ (k : Fin w), p k ∈ I
Hf : ∀ (k : Fin w), r k * a + p k = f k
y : R
hy : y ∈ I
refine_2 :
  ∃ (y_1 : R),
    Membership.mem (γ := Submodule R R) (span (Set.range p)) y_1 ∧
      ∃ (z : R), Membership.mem (γ := Submodule R R) (span (Set.range fun (a_1 : Fin w_1) ↦ a • i a_1)) z ∧ y_1 + z = y
⊢ Membership.mem (γ := Submodule R R) (span (Set.range p) ⊔ span (Set.range fun (a_1 : Fin w_1) ↦ a • i a_1)) y

Tactic:
rw [Submodule.mem_sup]

Premises used: Submodule.mem_sup
-- Module: Mathlib.RingTheory.Noetherian.OfPrime
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I (↑(span {a}) : Set R)).FG
w : ℕ
f : Fin w → R
hf : span (Set.range f) = I ⊔ span {a}
w_1 : ℕ
i : Fin w_1 → R
hi : Submodule.span R (Set.range i) = Submodule.colon I (↑(span {a}) : Set R)
r p : (k : Fin w) → R
p_mem_I : ∀ (k : Fin w), p k ∈ I
Hf : ∀ (k : Fin w), r k * a + p k = f k
y : R
hy : y ∈ I
refine_2 :
  ∀ (s : Fin w → R) (H : ∑ i : Fin w, s i * f i = y),
    ∃ (y_1 : R),
      Membership.mem (γ := Submodule R R) (span (Set.range p)) y_1 ∧
        ∃ (z : R),
          Membership.mem (γ := Submodule R R) (span (Set.range fun (a_1 : Fin w_1) ↦ a • i a_1)) z ∧ y_1 + z = y
⊢ ∃ (y_1 : R),
    Membership.mem (γ := Submodule R R) (span (Set.range p)) y_1 ∧
      ∃ (z : R), Membership.mem (γ := Submodule R R) (span (Set.range fun (a_1 : Fin w_1) ↦ a • i a_1)) z ∧ y_1 + z = y

Tactic:
obtain ⟨s, H⟩ := mem_span_range_iff_exists_fun.1 (hf ▸ Ideal.mem_sup_left hy)

Premises used: Ideal.mem_span_range_iff_exists_fun, Iff.mp
-- Module: Mathlib.RingTheory.Noetherian.OfPrime
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I (↑(span {a}) : Set R)).FG
w : ℕ
f : Fin w → R
hf : span (Set.range f) = I ⊔ span {a}
w_1 : ℕ
i : Fin w_1 → R
hi : Submodule.span R (Set.range i) = Submodule.colon I (↑(span {a}) : Set R)
r p : (k : Fin w) → R
p_mem_I : ∀ (k : Fin w), p k ∈ I
Hf : ∀ (k : Fin w), r k * a + p k = f k
y : R
hy : y ∈ I
s : Fin w → R
H : ∑ i : Fin w, s i * f i = y
⊢ ∑ x : Fin w, s x * (r x * a + p x) = y

Tactic:
simp_rw [← Hf] at H
-- Module: Mathlib.RingTheory.Noetherian.OfPrime
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I (↑(span {a}) : Set R)).FG
w : ℕ
f : Fin w → R
hf : span (Set.range f) = I ⊔ span {a}
w_1 : ℕ
i : Fin w_1 → R
hi : Submodule.span R (Set.range i) = Submodule.colon I (↑(span {a}) : Set R)
r p : (k : Fin w) → R
p_mem_I : ∀ (k : Fin w), p k ∈ I
Hf : ∀ (k : Fin w), r k * a + p k = f k
y : R
hy : y ∈ I
s : Fin w → R
H : ∑ x : Fin w, s x * (r x * a + p x) = y
⊢ ∑ x : Fin w, (s x * r x * a + s x * p x) = y

Tactic:
ring_nf at H
-- Module: Mathlib.RingTheory.Noetherian.OfPrime
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I (↑(span {a}) : Set R)).FG
w : ℕ
f : Fin w → R
hf : span (Set.range f) = I ⊔ span {a}
w_1 : ℕ
i : Fin w_1 → R
hi : Submodule.span R (Set.range i) = Submodule.colon I (↑(span {a}) : Set R)
r p : (k : Fin w) → R
p_mem_I : ∀ (k : Fin w), p k ∈ I
Hf : ∀ (k : Fin w), r k * a + p k = f k
y : R
hy : y ∈ I
s : Fin w → R
H : ∑ x : Fin w, (s x * r x * a + s x * p x) = y
⊢ ∑ x : Fin w, s x * p x + (∑ i : Fin w, s i * r i) * a = y

Tactic:
rw [sum_add_distrib, ← sum_mul, add_comm] at H

Premises used: Finset.sum_add_distrib, add_comm, Finset.sum_mul
-- Module: Mathlib.RingTheory.Noetherian.OfPrime
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I (↑(span {a}) : Set R)).FG
w : ℕ
f : Fin w → R
hf : span (Set.range f) = I ⊔ span {a}
w_1 : ℕ
i : Fin w_1 → R
hi : Submodule.span R (Set.range i) = Submodule.colon I (↑(span {a}) : Set R)
r p : (k : Fin w) → R
p_mem_I : ∀ (k : Fin w), p k ∈ I
Hf : ∀ (k : Fin w), r k * a + p k = f k
y : R
hy : y ∈ I
s : Fin w → R
H : ∑ x : Fin w, s x * p x + (∑ i : Fin w, s i * r i) * a = y
⊢ ∃ (y_1 : R),
    Membership.mem (γ := Submodule R R) (span (Set.range p)) y_1 ∧
      ∃ (z : R), Membership.mem (γ := Submodule R R) (span (Set.range fun (a_1 : Fin w_1) ↦ a • i a_1)) z ∧ y_1 + z = y

Tactic:
⟨(∑ k, s k * p k), sum_mem _ (fun _ _ ↦ mul_mem_left _ _ mem_span_range_self),
        (∑ k, s k * r k) * a, ?_, H⟩

Premises used: HMul.hMul, Finset.univ, Ideal.mem_span_range_self, Ideal.sum_mem, And.intro, Exists.intro, Ideal.span, Set.range, Ideal.mul_mem_left, Finset.sum
-- Module: Mathlib.RingTheory.Noetherian.OfPrime
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I (↑(span {a}) : Set R)).FG
w : ℕ
f : Fin w → R
hf : span (Set.range f) = I ⊔ span {a}
w_1 : ℕ
i : Fin w_1 → R
hi : Submodule.span R (Set.range i) = Submodule.colon I (↑(span {a}) : Set R)
r p : (k : Fin w) → R
p_mem_I : ∀ (k : Fin w), p k ∈ I
Hf : ∀ (k : Fin w), r k * a + p k = f k
y : R
hy : y ∈ I
s : Fin w → R
H : ∑ x : Fin w, s x * p x + (∑ i : Fin w, s i * r i) * a = y
refine_2 :
  Membership.mem (γ := Submodule R R) (span (Set.range fun (a_1 : Fin w_1) ↦ a • i a_1)) ((∑ k : Fin w, s k * r k) * a)
⊢ ∃ (y_1 : R),
    Membership.mem (γ := Submodule R R) (span (Set.range p)) y_1 ∧
      ∃ (z : R), Membership.mem (γ := Submodule R R) (span (Set.range fun (a_1 : Fin w_1) ↦ a • i a_1)) z ∧ y_1 + z = y

Tactic:
refine ⟨(∑ k, s k * p k), sum_mem _ (fun _ _ ↦ mul_mem_left _ _ mem_span_range_self),
        (∑ k, s k * r k) * a, ?_, H⟩
-- Module: Mathlib.RingTheory.Noetherian.OfPrime
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I (↑(span {a}) : Set R)).FG
w : ℕ
f : Fin w → R
hf : span (Set.range f) = I ⊔ span {a}
w_1 : ℕ
i : Fin w_1 → R
hi : Submodule.span R (Set.range i) = Submodule.colon I (↑(span {a}) : Set R)
r p : (k : Fin w) → R
p_mem_I : ∀ (k : Fin w), p k ∈ I
Hf : ∀ (k : Fin w), r k * a + p k = f k
y : R
hy : y ∈ I
s : Fin w → R
H : ∑ x : Fin w, s x * p x + (∑ i : Fin w, s i * r i) * a = y
refine_2 : HSMul.hSMul (β := R) a (∑ k : Fin w, s k * r k) ∈ a • Submodule.colon I (↑(span {a}) : Set R)
⊢ Membership.mem (γ := Submodule R R) (span (Set.range fun (a_1 : Fin w_1) ↦ a • i a_1)) ((∑ k : Fin w, s k * r k) * a)

Tactic:
rw [mul_comm, ← smul_eq_mul, range_smul, ← submodule_span_eq, Submodule.span_smul, hi]

Premises used: Ideal.submodule_span_eq, Submodule.span_smul, mul_comm, Set.range_smul, smul_eq_mul
-- Module: Mathlib.RingTheory.Noetherian.OfPrime
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I (↑(span {a}) : Set R)).FG
w : ℕ
f : Fin w → R
hf : span (Set.range f) = I ⊔ span {a}
w_1 : ℕ
i : Fin w_1 → R
hi : Submodule.span R (Set.range i) = Submodule.colon I (↑(span {a}) : Set R)
r p : (k : Fin w) → R
p_mem_I : ∀ (k : Fin w), p k ∈ I
Hf : ∀ (k : Fin w), r k * a + p k = f k
y : R
hy : y ∈ I
s : Fin w → R
H : ∑ x : Fin w, s x * p x + (∑ i : Fin w, s i * r i) * a = y
⊢ HSMul.hSMul (β := R) a (∑ k : Fin w, s k * r k) ∈ a • Submodule.colon I (↑(span {a}) : Set R)

Tactic:
smul_mem_smul_set <| mem_colon_span_singleton.2 <|
        (I.add_mem_iff_right <| I.sum_mem (fun _ _ ↦ mul_mem_left _ _ <| p_mem_I _)).1 (H ▸ hy)

Premises used: Iff.mpr, Ideal.mem_colon_span_singleton, Set.Mem, Ideal.sum_mem, Ideal.add_mem_iff_right, Iff.mp, Ideal.mul_mem_left, Set.smul_mem_smul_set
-- Module: Mathlib.RingTheory.Noetherian.OfPrime
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I (↑(span {a}) : Set R)).FG
w : ℕ
f : Fin w → R
hf : span (Set.range f) = I ⊔ span {a}
w_1 : ℕ
i : Fin w_1 → R
hi : Submodule.span R (Set.range i) = Submodule.colon I (↑(span {a}) : Set R)
r p : (k : Fin w) → R
p_mem_I : ∀ (k : Fin w), p k ∈ I
Hf : ∀ (k : Fin w), r k * a + p k = f k
y : R
hy : y ∈ I
s : Fin w → R
H : ∑ x : Fin w, s x * p x + (∑ i : Fin w, s i * r i) * a = y
⊢ HSMul.hSMul (β := R) a (∑ k : Fin w, s k * r k) ∈ a • Submodule.colon I (↑(span {a}) : Set R)

Tactic:
exact smul_mem_smul_set <| mem_colon_span_singleton.2 <|
        (I.add_mem_iff_right <| I.sum_mem (fun _ _ ↦ mul_mem_left _ _ <| p_mem_I _)).1 (H ▸ hy)

Premises used: Iff.mpr, Ideal.mem_colon_span_singleton, Ideal.sum_mem, Ideal.add_mem_iff_right, Iff.mp, Ideal.mul_mem_left, Set.smul_mem_smul_set
-- Module: Mathlib.RingTheory.Noetherian.OfPrime
Goal:
R : Type u_1
inst : CommRing R
H : ∀ (I : Ideal R), I.IsPrime → I.FG
⊢ IsNoetherianRing R

Tactic:
⟨isOka_fg.forall_of_forall_prime' (fun C hC₁ hC₂ I hI h ↦ ⟨sSup C, ?_, h⟩) H⟩

Premises used: Ideal.isOka_fg, And.intro, Exists.intro, Ideal.IsOka.forall_of_forall_prime', IsNoetherian.mk, SupSet.sSup
-- Module: Mathlib.RingTheory.Noetherian.OfPrime
Goal:
R : Type u_1
inst : CommRing R
H : ∀ (I : Ideal R), I.IsPrime → I.FG
refine :
  ∀ (C : Set (Ideal R)) (hC₁ : C ⊆ {I : Ideal R | ¬I.FG}) (hC₂ : IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) C)
    (I : Ideal R) (hI : I ∈ C) (h : (sSup C).FG), sSup C ∈ C
⊢ IsNoetherianRing R

Tactic:
refine ⟨isOka_fg.forall_of_forall_prime' (fun C hC₁ hC₂ I hI h ↦ ⟨sSup C, ?_, h⟩) H⟩
-- Module: Mathlib.RingTheory.Noetherian.OfPrime
Goal:
R : Type u_1
inst : CommRing R
H : ∀ (I : Ideal R), I.IsPrime → I.FG
C : Set (Ideal R)
hC₁ : C ⊆ {I : Ideal R | ¬I.FG}
hC₂ : IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) C
I : Ideal R
hI : I ∈ C
h : (sSup C).FG
obtain : ∀ (G : Finset R) (hG : span (↑G : Set R) = sSup C), sSup C ∈ C
⊢ sSup C ∈ C

Tactic:
obtain ⟨G, hG⟩ := h
-- Module: Mathlib.RingTheory.Noetherian.OfPrime
Goal:
R : Type u_1
inst : CommRing R
H : ∀ (I : Ideal R), I.IsPrime → I.FG
C : Set (Ideal R)
hC₁ : C ⊆ {I : Ideal R | ¬I.FG}
hC₂ : IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) C
I : Ideal R
hI : I ∈ C
G : Finset R
hG : span (↑G : Set R) = sSup C
⊢ ∃ J ∈ C, (↑G : Set R) ⊆ (↑J : Set R)

Tactic:
hC₂.directedOn.exists_mem_subset_of_finset_subset_biUnion ⟨I, hI⟩ (fun _ hx ↦ ?_)

Premises used: DirectedOn.exists_mem_subset_of_finset_subset_biUnion, IsChain.directedOn, Exists.intro
-- Module: Mathlib.RingTheory.Noetherian.OfPrime
Goal:
R : Type u_1
inst : CommRing R
H : ∀ (I : Ideal R), I.IsPrime → I.FG
C : Set (Ideal R)
hC₁ : C ⊆ {I : Ideal R | ¬I.FG}
hC₂ : IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) C
I : Ideal R
hI : I ∈ C
G : Finset R
hG : span (↑G : Set R) = sSup C
refine : ∀ (x : R) (hx : x ∈ (↑G : Set R)), Membership.mem (γ := Set R) (⋃ i ∈ C, (↑i : Set R)) x
⊢ ∃ J ∈ C, (↑G : Set R) ⊆ (↑J : Set R)

Tactic:
refine hC₂.directedOn.exists_mem_subset_of_finset_subset_biUnion ⟨I, hI⟩ (fun _ hx ↦ ?_)

Premises used: DirectedOn.exists_mem_subset_of_finset_subset_biUnion, IsChain.directedOn, Exists.intro
-- Module: Mathlib.RingTheory.Noetherian.OfPrime
Goal:
R : Type u_1
inst : CommRing R
H : ∀ (I : Ideal R), I.IsPrime → I.FG
C : Set (Ideal R)
hC₁ : C ⊆ {I : Ideal R | ¬I.FG}
hC₂ : IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) C
I : Ideal R
hI : I ∈ C
G : Finset R
hG : span (↑G : Set R) = sSup C
x : R
hx : x ∈ (↑G : Set R)
simp : ∃ i ∈ C, x ∈ i
⊢ Membership.mem (γ := Set R) (⋃ i ∈ C, (↑i : Set R)) x

Tactic:
simp only [Set.mem_iUnion, SetLike.mem_coe, exists_prop]

Premises used: Set.mem_iUnion, exists_prop, SetLike.mem_coe
-- Module: Mathlib.RingTheory.Noetherian.OfPrime
Goal:
R : Type u_1
inst : CommRing R
H : ∀ (I : Ideal R), I.IsPrime → I.FG
C : Set (Ideal R)
hC₁ : C ⊆ {I : Ideal R | ¬I.FG}
hC₂ : IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) C
I : Ideal R
hI : I ∈ C
G : Finset R
hG : span (↑G : Set R) = sSup C
x : R
hx : x ∈ (↑G : Set R)
⊢ ∃ i ∈ C, x ∈ i

Tactic:
(Submodule.mem_sSup_of_directed ⟨I, hI⟩ hC₂.directedOn).1 <| hG ▸ subset_span hx

Premises used: Ideal.subset_span, Set.Mem, Eq.rec, IsChain.directedOn, Exists.intro, Iff.mp, Submodule.mem_sSup_of_directed
-- Module: Mathlib.RingTheory.Noetherian.OfPrime
Goal:
R : Type u_1
inst : CommRing R
H : ∀ (I : Ideal R), I.IsPrime → I.FG
C : Set (Ideal R)
hC₁ : C ⊆ {I : Ideal R | ¬I.FG}
hC₂ : IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) C
I : Ideal R
hI : I ∈ C
G : Finset R
hG : span (↑G : Set R) = sSup C
x : R
hx : x ∈ (↑G : Set R)
⊢ ∃ i ∈ C, x ∈ i

Tactic:
exact (Submodule.mem_sSup_of_directed ⟨I, hI⟩ hC₂.directedOn).1 <| hG ▸ subset_span hx

Premises used: IsChain.directedOn, Exists.intro, Iff.mp, Submodule.mem_sSup_of_directed
-- Module: Mathlib.RingTheory.Noetherian.OfPrime
Goal:
R : Type u_1
inst : CommRing R
H : ∀ (I : Ideal R), I.IsPrime → I.FG
C : Set (Ideal R)
hC₁ : C ⊆ {I : Ideal R | ¬I.FG}
hC₂ : IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) C
I : Ideal R
hI : I ∈ C
G : Finset R
hG : span (↑G : Set R) = sSup C
obtain : ∀ (J : Ideal R) (J_mem_C : J ∈ C) (G_subset_J : (↑G : Set R) ⊆ (↑J : Set R)), sSup C ∈ C
⊢ sSup C ∈ C

Tactic:
obtain ⟨J, J_mem_C, G_subset_J⟩ : ∃ J ∈ C, (G : Set R) ⊆ J := by
    refine hC₂.directedOn.exists_mem_subset_of_finset_subset_biUnion ⟨I, hI⟩ (fun _ hx ↦ ?_)
    simp only [Set.mem_iUnion, SetLike.mem_coe, exists_prop]
    exact (Submodule.mem_sSup_of_directed ⟨I, hI⟩ hC₂.directedOn).1 <| hG ▸ subset_span hx

Premises used: SetLike.coe
-- Module: Mathlib.RingTheory.Noetherian.OfPrime
Goal:
R : Type u_1
inst : CommRing R
H : ∀ (I : Ideal R), I.IsPrime → I.FG
C : Set (Ideal R)
hC₁ : C ⊆ {I : Ideal R | ¬I.FG}
hC₂ : IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) C
I : Ideal R
hI : I ∈ C
G : Finset R
hG : span (↑G : Set R) = sSup C
J : Ideal R
J_mem_C : J ∈ C
G_subset_J : (↑G : Set R) ⊆ (↑J : Set R)
suffices : J = sSup C
⊢ sSup C ∈ C

Tactic:
suffices J_eq_sSup : J = sSup C from J_eq_sSup ▸ J_mem_C
-- Module: Mathlib.RingTheory.Noetherian.OfPrime
Goal:
R : Type u_1
inst : CommRing R
H : ∀ (I : Ideal R), I.IsPrime → I.FG
C : Set (Ideal R)
hC₁ : C ⊆ {I : Ideal R | ¬I.FG}
hC₂ : IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) C
I : Ideal R
hI : I ∈ C
G : Finset R
hG : span (↑G : Set R) = sSup C
J : Ideal R
J_mem_C : J ∈ C
G_subset_J : (↑G : Set R) ⊆ (↑J : Set R)
⊢ J = sSup C

Tactic:
le_antisymm (le_sSup J_mem_C) (hG ▸ Ideal.span_le.2 G_subset_J)

Premises used: Ideal.span_le, Iff.mpr, Eq.rec, le_antisymm, le_sSup
-- Module: Mathlib.RingTheory.Noetherian.OfPrime
Goal:
R : Type u_1
inst : CommRing R
H : ∀ (I : Ideal R), I.IsPrime → I.FG
C : Set (Ideal R)
hC₁ : C ⊆ {I : Ideal R | ¬I.FG}
hC₂ : IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) C
I : Ideal R
hI : I ∈ C
G : Finset R
hG : span (↑G : Set R) = sSup C
J : Ideal R
J_mem_C : J ∈ C
G_subset_J : (↑G : Set R) ⊆ (↑J : Set R)
⊢ J = sSup C

Tactic:
exact le_antisymm (le_sSup J_mem_C) (hG ▸ Ideal.span_le.2 G_subset_J)

Premises used: Ideal.span_le, Iff.mpr, Eq.rec, le_antisymm, le_sSup
-- Module: Mathlib.RingTheory.Noetherian.OfPrime
Goal:
R : Type u_1
inst : CommRing R
H : ∀ (I : Ideal R), I.IsPrime → I ≠ ⊥ → I.FG
⊢ IsNoetherianRing R

Tactic:
.of_prime fun I hi ↦ (eq_or_ne I ⊥).elim (· ▸ Submodule.fg_bot) <| H _ hi

Premises used: IsNoetherianRing.of_prime, Eq.rec, Bot.bot, eq_or_ne, Submodule.fg_bot, Or.elim, Eq.symm
-- Module: Mathlib.RingTheory.Noetherian.Orzech
Goal:
R : Type u_1
M : Type u_2
N : Type w
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsNoetherian R M
i f : N →ₗ[R] M
hi : Injective.{w + 1, u_2 + 1} (α := N) (β := M) (⇑i : (a : N) → M)
hf : Surjective.{w + 1, u_2 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
⊢ IsNoetherian R N

Tactic:
haveI := isNoetherian_of_injective i hi
-- Module: Mathlib.RingTheory.Noetherian.Orzech
Goal:
R : Type u_1
M : Type u_2
N : Type w
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsNoetherian R M
i f : N →ₗ[R] M
hi : Injective.{w + 1, u_2 + 1} (α := N) (β := M) (⇑i : (a : N) → M)
hf : Surjective.{w + 1, u_2 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
this : IsNoetherian R N
⊢ Submodule.map f ⊥ ≤ Submodule.map i ⊥

Tactic:
simp
-- Module: Mathlib.RingTheory.Noetherian.Orzech
Goal:
R : Type u_1
M : Type u_2
N : Type w
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsNoetherian R M
i f : N →ₗ[R] M
hi : Injective.{w + 1, u_2 + 1} (α := N) (β := M) (⇑i : (a : N) → M)
hf : Surjective.{w + 1, u_2 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
this : IsNoetherian R N
obtain :
  ∀ (n : ℕ)
    (H :
      ∀ (m : ℕ),
        n ≤ m →
          Eq (α := Submodule R N)
            (({ toFun := fun (n : ℕ) ↦ f.iterateMapComap i n ⊥, monotone' := ⋯ : ℕ →o Submodule R N } :
                  (a : ℕ) → Submodule R N)
                n :
              Submodule R N)
            (({ toFun := fun (n : ℕ) ↦ f.iterateMapComap i n ⊥, monotone' := ⋯ : ℕ →o Submodule R N } :
                  (a : ℕ) → Submodule R N)
                m :
              Submodule R N)),
    Injective.{w + 1, u_2 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
⊢ Injective.{w + 1, u_2 + 1} (α := N) (β := M) (⇑f : (a : N) → M)

Tactic:
obtain ⟨n, H⟩ := monotone_stabilizes_iff_noetherian.2 ‹_›
    ⟨_, monotone_nat_of_le_succ <| f.iterateMapComap_le_succ i ⊥ (by simp)⟩

Premises used: Iff.mpr, Bot.bot, monotone_stabilizes_iff_noetherian, OrderHom.mk, LinearMap.iterateMapComap_le_succ, monotone_nat_of_le_succ
-- Module: Mathlib.RingTheory.Noetherian.Orzech
Goal:
R : Type u_1
M : Type u_2
N : Type w
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsNoetherian R M
i f : N →ₗ[R] M
hi : Injective.{w + 1, u_2 + 1} (α := N) (β := M) (⇑i : (a : N) → M)
hf : Surjective.{w + 1, u_2 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
this : IsNoetherian R N
n : ℕ
H :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := Submodule R N)
        (({ toFun := fun (n : ℕ) ↦ f.iterateMapComap i n ⊥, monotone' := ⋯ : ℕ →o Submodule R N } :
              (a : ℕ) → Submodule R N)
            n :
          Submodule R N)
        (({ toFun := fun (n : ℕ) ↦ f.iterateMapComap i n ⊥, monotone' := ⋯ : ℕ →o Submodule R N } :
              (a : ℕ) → Submodule R N)
            m :
          Submodule R N)
⊢ Injective.{w + 1, u_2 + 1} (α := N) (β := M) (⇑f : (a : N) → M)

Tactic:
LinearMap.ker_eq_bot.1 <| bot_unique <|
    f.ker_le_of_iterateMapComap_eq_succ i ⊥ n (H _ (Nat.le_succ _)) hf hi

Premises used: LinearMap.ker_le_of_iterateMapComap_eq_succ, LinearMap.ker_eq_bot, Nat.le_succ, Bot.bot, Iff.mp, bot_unique