Theorem: Section16Sheet2solutions.lemma1 (FormalisingMathematics2024/Solutions/Section16commutativeAlgebra/Sheet2.lean)

State before:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
⊢ Set.Nonempty (↑I \ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ)))
Tactic:
rw [Set.nonempty_iff_ne_empty]
State after:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
⊢ ↑I \ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ)) ≠ ∅

State before:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
⊢ ↑I \ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ)) ≠ ∅
Tactic:
intro h
State after:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
h : ↑I \ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ)) = ∅
⊢ False

State before:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
h : ↑I \ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ)) = ∅
⊢ False
Tactic:
rw [Set.diff_eq_empty] at h
State after:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
h : ↑I ⊆ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ))
⊢ False

State before:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
h : ↑I ⊆ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ))
⊢ False
Tactic:
apply hInonfg
State after:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
h : ↑I ⊆ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ))
⊢ Ideal.FG I

State before:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
h : ↑I ⊆ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ))
⊢ Ideal.FG I
Tactic:
refine' ⟨Finset.image (fun m : Fin n => (g m.1 m.2).1) Finset.univ, _⟩
State after:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
h : ↑I ⊆ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ))
⊢ Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ) = I

State before:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
h : ↑I ⊆ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ))
⊢ Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ) = I
Tactic:
refine' le_antisymm _ h
State after:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
h : ↑I ⊆ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ))
⊢ Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ) ≤ I

State before:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
h : ↑I ⊆ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ))
⊢ Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ) ≤ I
Tactic:
rw [Ideal.span_le]
State after:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
h : ↑I ⊆ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ))
⊢ ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ) ⊆ ↑I

State before:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
h : ↑I ⊆ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ))
⊢ ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ) ⊆ ↑I
Tactic:
intro a ha
State after:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
h : ↑I ⊆ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ))
a : A
ha : a ∈ ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ)
⊢ a ∈ ↑I

State before:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
h : ↑I ⊆ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ))
a : A
ha : a ∈ ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ)
⊢ a ∈ ↑I
Tactic:
simp only [Finset.coe_image, Finset.coe_univ, Set.image_univ,
  Set.mem_range] at ha
State after:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
h : ↑I ⊆ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ))
a : A
ha : ∃ y, ↑(g ↑y (_ : ↑y < n)) = a
⊢ a ∈ ↑I

State before:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
h : ↑I ⊆ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ))
a : A
ha : ∃ y, ↑(g ↑y (_ : ↑y < n)) = a
⊢ a ∈ ↑I
Tactic:
rcases ha with ⟨y, rfl⟩
State after:
case intro
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
h : ↑I ⊆ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ))
y : Fin n
⊢ ↑(g ↑y (_ : ↑y < n)) ∈ ↑I

State before:
case intro
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
h : ↑I ⊆ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ))
y : Fin n
⊢ ↑(g ↑y (_ : ↑y < n)) ∈ ↑I
Tactic:
exact (g y.1 y.2).2
State after:
no goals