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 {x | ↑x ∉ Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ)}
Tactic:
set S : Set A := _
State after:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
S : Set A := ?m.3713
⊢ Set.Nonempty {x | ↑x ∉ 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
S : Set A := ?m.3713
⊢ Set.Nonempty {x | ↑x ∉ Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ)}
Tactic:
have ne1 : Set.Nonempty S := lemma1 hInonfg n g
State after:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
S : Set A := ↑I \ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ))
ne1 : Set.Nonempty S
⊢ Set.Nonempty {x | ↑x ∉ 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
S : Set A := ↑I \ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ))
ne1 : Set.Nonempty S
⊢ Set.Nonempty {x | ↑x ∉ Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ)}
Tactic:
choose x hx using ne1
State after:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
S : Set A := ↑I \ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ))
x : A
hx : x ∈ S
⊢ Set.Nonempty {x | ↑x ∉ 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
S : Set A := ↑I \ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ))
x : A
hx : x ∈ S
⊢ Set.Nonempty {x | ↑x ∉ Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ)}
Tactic:
refine ⟨⟨x, hx.1⟩, ?_⟩
State after:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
S : Set A := ↑I \ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ))
x : A
hx : x ∈ S
⊢ { val := x, property := (_ : x ∈ ↑I) } ∈
    {x | ↑x ∉ 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
S : Set A := ↑I \ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ))
x : A
hx : x ∈ S
⊢ { val := x, property := (_ : x ∈ ↑I) } ∈
    {x | ↑x ∉ Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ)}
Tactic:
simp only [Finset.coe_image, Finset.coe_univ, Set.image_univ, Set.mem_diff,
  SetLike.mem_coe, Set.mem_setOf_eq] at hx ⊢
State after:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
S : Set A := ↑I \ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ))
x : A
hx : x ∈ I ∧ x ∉ Ideal.span (Set.range fun m => ↑(g ↑m (_ : ↑m < n)))
⊢ x ∉ Ideal.span (Set.range fun m => ↑(g ↑m (_ : ↑m < n)))

State before:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
S : Set A := ↑I \ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ))
x : A
hx : x ∈ I ∧ x ∉ Ideal.span (Set.range fun m => ↑(g ↑m (_ : ↑m < n)))
⊢ x ∉ Ideal.span (Set.range fun m => ↑(g ↑m (_ : ↑m < n)))
Tactic:
exact hx.2
State after:
no goals