awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
inst_1 : I.IsPrime
hI : X ∉ I
S : Set R
hSI : Eq (α := Ideal R) (span S) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
hS : S.Finite
this : SurjOn (⇑constantCoeff : (a : R⟦X⟧) → R) (↑I : Set R⟦X⟧) S
T : Set R⟦X⟧
hTI : T ⊆ (↑I : Set R⟦X⟧)
hinj : InjOn (β := R) (⇑constantCoeff : (a : R⟦X⟧) → R) T
hT : (⇑constantCoeff : (a : R⟦X⟧) → R) '' T = S
⊢ ∃ (T : Set R⟦X⟧), I = span T ∧ T.Finite ∧ T.ncard = S.ncard
have refine : LE.le (α := Ideal R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff (span T))
Tactic: refine ⟨T, eq_of_le_of_X_notMem_of_fg_of_isPrime (span_le.2  hTI) hI (Submodule.fg_def.2
    ⟨T, (hT ▸ hS).of_finite_image hinj, rfl⟩) ?_, Finite.of_injOn
    (fun f hf ↦ hT ▸ Set.mem_image_of_mem _ hf) hinj hS, hT ▸ hinj.ncard_image.symm⟩
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
inst_1 : I.IsPrime
hI : X ∉ I
S : Set R
hSI : Eq (α := Ideal R) (span S) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
hS : S.Finite
this : SurjOn (⇑constantCoeff : (a : R⟦X⟧) → R) (↑I : Set R⟦X⟧) S
T : Set R⟦X⟧
hTI : T ⊆ (↑I : Set R⟦X⟧)
hinj : InjOn (β := R) (⇑constantCoeff : (a : R⟦X⟧) → R) T
hT : (⇑constantCoeff : (a : R⟦X⟧) → R) '' T = S
⊢ LE.le (α := Ideal R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
    (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff (span T))
have rw : I ≤ comap (F := R⟦X⟧ →+* R) constantCoeff (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff (span T))
Tactic: rw [map_le_iff_le_comap]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
inst_1 : I.IsPrime
hI : X ∉ I
S : Set R
hSI : Eq (α := Ideal R) (span S) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
hS : S.Finite
this : SurjOn (⇑constantCoeff : (a : R⟦X⟧) → R) (↑I : Set R⟦X⟧) S
T : Set R⟦X⟧
hTI : T ⊆ (↑I : Set R⟦X⟧)
hinj : InjOn (β := R) (⇑constantCoeff : (a : R⟦X⟧) → R) T
hT : (⇑constantCoeff : (a : R⟦X⟧) → R) '' T = S
f : R⟦X⟧
hf : f ∈ I
⊢ Membership.mem (γ := Submodule R⟦X⟧ R⟦X⟧)
    (comap (F := R⟦X⟧ →+* R) constantCoeff (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff (span T))) f
have rw : ∃ (x : R⟦X⟧),
  Membership.mem (γ := Ideal R⟦X⟧) (span T) x ∧
    Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) x : R) ((constantCoeff : (a : R⟦X⟧) → R) f : R)
Tactic: rw [mem_comap, mem_map_iff_of_surjective _ constantCoeff_surj]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
inst_1 : I.IsPrime
hI : X ∉ I
S : Set R
hSI : Eq (α := Ideal R) (span S) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
hS : S.Finite
this : SurjOn (⇑constantCoeff : (a : R⟦X⟧) → R) (↑I : Set R⟦X⟧) S
T : Set R⟦X⟧
hTI : T ⊆ (↑I : Set R⟦X⟧)
hinj : InjOn (β := R) (⇑constantCoeff : (a : R⟦X⟧) → R) T
hT : (⇑constantCoeff : (a : R⟦X⟧) → R) '' T = S
f : R⟦X⟧
hf : f ∈ I
⊢ ∃ (x : R⟦X⟧),
    Membership.mem (γ := Ideal R⟦X⟧) (span T) x ∧
      Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) x : R) ((constantCoeff : (a : R⟦X⟧) → R) f : R)
have hf₁ : Membership.mem (α := R) (γ := Ideal R) (span S) ((constantCoeff : (a : R⟦X⟧) → R) f : R)
Tactic: replace hf : constantCoeff f ∈ span S := hSI ▸ Ideal.mem_map_of_mem constantCoeff hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
inst_1 : I.IsPrime
hI : X ∉ I
S : Set R
hSI : Eq (α := Ideal R) (span S) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
hS : S.Finite
this : SurjOn (⇑constantCoeff : (a : R⟦X⟧) → R) (↑I : Set R⟦X⟧) S
T : Set R⟦X⟧
hTI : T ⊆ (↑I : Set R⟦X⟧)
hinj : InjOn (β := R) (⇑constantCoeff : (a : R⟦X⟧) → R) T
hT : (⇑constantCoeff : (a : R⟦X⟧) → R) '' T = S
f : R⟦X⟧
hf : Membership.mem (α := R) (γ := Ideal R) (span S) ((constantCoeff : (a : R⟦X⟧) → R) f : R)
⊢ ∃ (x : R⟦X⟧),
    Membership.mem (γ := Ideal R⟦X⟧) (span T) x ∧
      Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) x : R) ((constantCoeff : (a : R⟦X⟧) → R) f : R)
have refine_1 : ∀ (s : R) (hs : s ∈ S),
  ∃ (x : R⟦X⟧), Membership.mem (γ := Ideal R⟦X⟧) (span T) x ∧ (constantCoeff : (a : R⟦X⟧) → R) x = s
Tactic: refine Submodule.span_induction (fun s hs ↦ ?_) ⟨0, zero_mem _, by simp⟩ ?_ ?_ hf
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
inst_1 : I.IsPrime
hI : X ∉ I
S : Set R
hSI : Eq (α := Ideal R) (span S) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
hS : S.Finite
this : SurjOn (⇑constantCoeff : (a : R⟦X⟧) → R) (↑I : Set R⟦X⟧) S
T : Set R⟦X⟧
hTI : T ⊆ (↑I : Set R⟦X⟧)
hinj : InjOn (β := R) (⇑constantCoeff : (a : R⟦X⟧) → R) T
hT : (⇑constantCoeff : (a : R⟦X⟧) → R) '' T = S
f : R⟦X⟧
hf : Membership.mem (α := R) (γ := Ideal R) (span S) ((constantCoeff : (a : R⟦X⟧) → R) f : R)
refine_1 :
  ∀ (s : R) (hs : s ∈ S),
    ∃ (x : R⟦X⟧), Membership.mem (γ := Ideal R⟦X⟧) (span T) x ∧ (constantCoeff : (a : R⟦X⟧) → R) x = s
⊢ ∃ (x : R⟦X⟧),
    Membership.mem (γ := Ideal R⟦X⟧) (span T) x ∧
      Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) x : R) ((constantCoeff : (a : R⟦X⟧) → R) f : R)
have refine_2 : ∀ (x y : R) (hx : Membership.mem (γ := Submodule R R) (Submodule.span R S) x)
  (hy : Membership.mem (γ := Submodule R R) (Submodule.span R S) y),
  (∃ (x_1 : R⟦X⟧), Membership.mem (γ := Ideal R⟦X⟧) (span T) x_1 ∧ (constantCoeff : (a : R⟦X⟧) → R) x_1 = x) →
    (∃ (x : R⟦X⟧), Membership.mem (γ := Ideal R⟦X⟧) (span T) x ∧ (constantCoeff : (a : R⟦X⟧) → R) x = y) →
      ∃ (x_1 : R⟦X⟧), Membership.mem (γ := Ideal R⟦X⟧) (span T) x_1 ∧ (constantCoeff : (a : R⟦X⟧) → R) x_1 = x + y
Tactic: refine Submodule.span_induction (fun s hs ↦ ?_) ⟨0, zero_mem _, by simp⟩ ?_ ?_ hf
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
inst_1 : I.IsPrime
hI : X ∉ I
S : Set R
hSI : Eq (α := Ideal R) (span S) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
hS : S.Finite
this : SurjOn (⇑constantCoeff : (a : R⟦X⟧) → R) (↑I : Set R⟦X⟧) S
T : Set R⟦X⟧
hTI : T ⊆ (↑I : Set R⟦X⟧)
hinj : InjOn (β := R) (⇑constantCoeff : (a : R⟦X⟧) → R) T
hT : (⇑constantCoeff : (a : R⟦X⟧) → R) '' T = S
f : R⟦X⟧
hf : Membership.mem (α := R) (γ := Ideal R) (span S) ((constantCoeff : (a : R⟦X⟧) → R) f : R)
refine_1 :
  ∀ (s : R) (hs : s ∈ S),
    ∃ (x : R⟦X⟧), Membership.mem (γ := Ideal R⟦X⟧) (span T) x ∧ (constantCoeff : (a : R⟦X⟧) → R) x = s
refine_2 :
  ∀ (x y : R) (hx : Membership.mem (γ := Submodule R R) (Submodule.span R S) x)
    (hy : Membership.mem (γ := Submodule R R) (Submodule.span R S) y),
    (∃ (x_1 : R⟦X⟧), Membership.mem (γ := Ideal R⟦X⟧) (span T) x_1 ∧ (constantCoeff : (a : R⟦X⟧) → R) x_1 = x) →
      (∃ (x : R⟦X⟧), Membership.mem (γ := Ideal R⟦X⟧) (span T) x ∧ (constantCoeff : (a : R⟦X⟧) → R) x = y) →
        ∃ (x_1 : R⟦X⟧), Membership.mem (γ := Ideal R⟦X⟧) (span T) x_1 ∧ (constantCoeff : (a : R⟦X⟧) → R) x_1 = x + y
⊢ ∃ (x : R⟦X⟧),
    Membership.mem (γ := Ideal R⟦X⟧) (span T) x ∧
      Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) x : R) ((constantCoeff : (a : R⟦X⟧) → R) f : R)
have refine_3 : ∀ (a x : R) (hx : Membership.mem (γ := Submodule R R) (Submodule.span R S) x),
  (∃ (x_1 : R⟦X⟧), Membership.mem (γ := Ideal R⟦X⟧) (span T) x_1 ∧ (constantCoeff : (a : R⟦X⟧) → R) x_1 = x) →
    ∃ (x_1 : R⟦X⟧), Membership.mem (γ := Ideal R⟦X⟧) (span T) x_1 ∧ (constantCoeff : (a : R⟦X⟧) → R) x_1 = a • x
Tactic: refine Submodule.span_induction (fun s hs ↦ ?_) ⟨0, zero_mem _, by simp⟩ ?_ ?_ hf
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
inst_1 : I.IsPrime
hI : X ∉ I
S : Set R
hSI : Eq (α := Ideal R) (span S) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
hS : S.Finite
this : SurjOn (⇑constantCoeff : (a : R⟦X⟧) → R) (↑I : Set R⟦X⟧) S
T : Set R⟦X⟧
hTI : T ⊆ (↑I : Set R⟦X⟧)
hinj : InjOn (β := R) (⇑constantCoeff : (a : R⟦X⟧) → R) T
hT : (⇑constantCoeff : (a : R⟦X⟧) → R) '' T = S
f : R⟦X⟧
hf : Membership.mem (α := R) (γ := Ideal R) (span S) ((constantCoeff : (a : R⟦X⟧) → R) f : R)
s : R
hs : s ∈ S
⊢ ∃ (x : R⟦X⟧), Membership.mem (γ := Ideal R⟦X⟧) (span T) x ∧ (constantCoeff : (a : R⟦X⟧) → R) x = s
have refine_1 : ∀ (t : R⟦X⟧) (htmem : t ∈ T) (ht : (constantCoeff : (a : R⟦X⟧) → R) t = s),
  ∃ (x : R⟦X⟧), Membership.mem (γ := Ideal R⟦X⟧) (span T) x ∧ (constantCoeff : (a : R⟦X⟧) → R) x = s
Tactic: obtain ⟨t, htmem, ht⟩ := hT ▸ hs
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
inst_1 : I.IsPrime
hI : X ∉ I
S : Set R
hSI : Eq (α := Ideal R) (span S) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
hS : S.Finite
this : SurjOn (⇑constantCoeff : (a : R⟦X⟧) → R) (↑I : Set R⟦X⟧) S
T : Set R⟦X⟧
hTI : T ⊆ (↑I : Set R⟦X⟧)
hinj : InjOn (β := R) (⇑constantCoeff : (a : R⟦X⟧) → R) T
hT : (⇑constantCoeff : (a : R⟦X⟧) → R) '' T = S
f : R⟦X⟧
hf : Membership.mem (α := R) (γ := Ideal R) (span S) ((constantCoeff : (a : R⟦X⟧) → R) f : R)
r₁ r₂ : R
hr₁ : Membership.mem (γ := Submodule R R) (Submodule.span R S) r₁
hr₂ : Membership.mem (γ := Submodule R R) (Submodule.span R S) r₂
⊢ (∃ (x : R⟦X⟧), Membership.mem (γ := Ideal R⟦X⟧) (span T) x ∧ (constantCoeff : (a : R⟦X⟧) → R) x = r₁) →
    (∃ (x : R⟦X⟧), Membership.mem (γ := Ideal R⟦X⟧) (span T) x ∧ (constantCoeff : (a : R⟦X⟧) → R) x = r₂) →
      ∃ (x : R⟦X⟧), Membership.mem (γ := Ideal R⟦X⟧) (span T) x ∧ (constantCoeff : (a : R⟦X⟧) → R) x = r₁ + r₂
have refine_2 : ∀ (s₁ : R⟦X⟧) (hs₁mem : Membership.mem (γ := Ideal R⟦X⟧) (span T) s₁) (hs₁ : (constantCoeff : (a : R⟦X⟧) → R) s₁ = r₁),
  (∃ (x : R⟦X⟧), Membership.mem (γ := Ideal R⟦X⟧) (span T) x ∧ (constantCoeff : (a : R⟦X⟧) → R) x = r₂) →
    ∃ (x : R⟦X⟧), Membership.mem (γ := Ideal R⟦X⟧) (span T) x ∧ (constantCoeff : (a : R⟦X⟧) → R) x = r₁ + r₂
Tactic: ⟨s₁, hs₁mem, hs₁⟩
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
inst_1 : I.IsPrime
hI : X ∉ I
S : Set R
hSI : Eq (α := Ideal R) (span S) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
hS : S.Finite
this : SurjOn (⇑constantCoeff : (a : R⟦X⟧) → R) (↑I : Set R⟦X⟧) S
T : Set R⟦X⟧
hTI : T ⊆ (↑I : Set R⟦X⟧)
hinj : InjOn (β := R) (⇑constantCoeff : (a : R⟦X⟧) → R) T
hT : (⇑constantCoeff : (a : R⟦X⟧) → R) '' T = S
f : R⟦X⟧
hf : Membership.mem (α := R) (γ := Ideal R) (span S) ((constantCoeff : (a : R⟦X⟧) → R) f : R)
r₁ r₂ : R
hr₁ : Membership.mem (γ := Submodule R R) (Submodule.span R S) r₁
hr₂ : Membership.mem (γ := Submodule R R) (Submodule.span R S) r₂
s₁ : R⟦X⟧
hs₁mem : Membership.mem (γ := Ideal R⟦X⟧) (span T) s₁
hs₁ : (constantCoeff : (a : R⟦X⟧) → R) s₁ = r₁
⊢ (∃ (x : R⟦X⟧), Membership.mem (γ := Ideal R⟦X⟧) (span T) x ∧ (constantCoeff : (a : R⟦X⟧) → R) x = r₂) →
    ∃ (x : R⟦X⟧), Membership.mem (γ := Ideal R⟦X⟧) (span T) x ∧ (constantCoeff : (a : R⟦X⟧) → R) x = r₁ + r₂
have refine_2 : ∀ (s₂ : R⟦X⟧) (hs₂mem : Membership.mem (γ := Ideal R⟦X⟧) (span T) s₂) (hs₂ : (constantCoeff : (a : R⟦X⟧) → R) s₂ = r₂),
  ∃ (x : R⟦X⟧), Membership.mem (γ := Ideal R⟦X⟧) (span T) x ∧ (constantCoeff : (a : R⟦X⟧) → R) x = r₁ + r₂
Tactic: ⟨s₂, hs₂mem, hs₂⟩
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
inst_1 : I.IsPrime
hI : X ∉ I
S : Set R
hSI : Eq (α := Ideal R) (span S) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
hS : S.Finite
this : SurjOn (⇑constantCoeff : (a : R⟦X⟧) → R) (↑I : Set R⟦X⟧) S
T : Set R⟦X⟧
hTI : T ⊆ (↑I : Set R⟦X⟧)
hinj : InjOn (β := R) (⇑constantCoeff : (a : R⟦X⟧) → R) T
hT : (⇑constantCoeff : (a : R⟦X⟧) → R) '' T = S
f : R⟦X⟧
hf : Membership.mem (α := R) (γ := Ideal R) (span S) ((constantCoeff : (a : R⟦X⟧) → R) f : R)
r₁ r₂ : R
hr₁ : Membership.mem (γ := Submodule R R) (Submodule.span R S) r₂
⊢ (∃ (x : R⟦X⟧), Membership.mem (γ := Ideal R⟦X⟧) (span T) x ∧ (constantCoeff : (a : R⟦X⟧) → R) x = r₂) →
    ∃ (x : R⟦X⟧), Membership.mem (γ := Ideal R⟦X⟧) (span T) x ∧ (constantCoeff : (a : R⟦X⟧) → R) x = r₁ • r₂
have refine_3 : ∀ (f : R⟦X⟧) (hfmem : Membership.mem (γ := Ideal R⟦X⟧) (span T) f) (hf : (constantCoeff : (a : R⟦X⟧) → R) f = r₂),
  ∃ (x : R⟦X⟧), Membership.mem (γ := Ideal R⟦X⟧) (span T) x ∧ (constantCoeff : (a : R⟦X⟧) → R) x = r₁ • r₂
Tactic: ⟨f, hfmem, hf⟩
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
inst_1 : I.IsPrime
hI : X ∉ I
hfg : I.FG
⊢ spanFinrank I = spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
have refine_1 : spanFinrank I ≤ spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
inst_1 : I.IsPrime
hI : X ∉ I
hfg : I.FG
refine_1 : spanFinrank I ≤ spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
⊢ spanFinrank I = spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
have refine_2 : spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I) ≤ spanFinrank I
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
inst_1 : I.IsPrime
hI : X ∉ I
hfg : I.FG
⊢ spanFinrank I ≤ spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
have this : RingHomSurjective.{u_1, u_1} (R₁ := R⟦X⟧) constantCoeff
Tactic: have : RingHomSurjective (constantCoeff (R := R)) := ⟨constantCoeff_surj⟩
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
inst_1 : I.IsPrime
hI : X ∉ I
hfg : I.FG
this : RingHomSurjective.{u_1, u_1} (R₁ := R⟦X⟧) constantCoeff
⊢ spanFinrank I ≤ spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
have refine_1 : ∀ (S : Set R⟦X⟧) [IsPrime (Ideal.span S)] (hI : X ∉ Ideal.span S) (hfg : Ideal.FG (Ideal.span S)) (hS : S.Finite)
  (hScard : S.ncard = ncard (α := R) (generators (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff (Ideal.span S)))),
  spanFinrank (Ideal.span S) ≤ spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff (Ideal.span S))
Tactic: obtain ⟨S, rfl, hS, hScard⟩ := exist_eq_span_eq_ncard_of_X_notMem hI
    (I.map constantCoeff).span_generators
    (FG.finite_generators <| map_eq_submodule_map constantCoeff I ▸ Submodule.FG.map _ hfg)
Cleared hypotheses: I, inst_1, hI, hfg
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
this : RingHomSurjective.{u_1, u_1} (R₁ := R⟦X⟧) constantCoeff
S : Set R⟦X⟧
inst_1 : IsPrime (Ideal.span S)
hI : X ∉ Ideal.span S
hfg : Ideal.FG (Ideal.span S)
hS : S.Finite
hScard : S.ncard = ncard (α := R) (generators (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff (Ideal.span S)))
⊢ spanFinrank (Ideal.span S) ≤ spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff (Ideal.span S))
have refine_1 : S.ncard ≤ spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff (Ideal.span S))
Tactic: refine le_trans (spanFinrank_span_le_ncard_of_finite hS) ?_
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
this : RingHomSurjective.{u_1, u_1} (R₁ := R⟦X⟧) constantCoeff
S : Set R⟦X⟧
inst_1 : IsPrime (Ideal.span S)
hI : X ∉ Ideal.span S
hfg : Ideal.FG (Ideal.span S)
hS : S.Finite
hScard : S.ncard = ncard (α := R) (generators (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff (Ideal.span S)))
⊢ S.ncard ≤ spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff (Ideal.span S))
have refine_1 : Submodule.FG (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff (Ideal.span S))
Tactic: rw [hScard, FG.generators_ncard]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R⟦X⟧
inst_1 : P.IsPrime
⊢ spanFinrank P ≤ spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff P) + 1
have pos : ∀ (hfg : P.FG), spanFinrank P ≤ spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff P) + 1
Tactic: by_cases hfg : P.FG
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R⟦X⟧
inst_1 : P.IsPrime
pos : ∀ (hfg : P.FG), spanFinrank P ≤ spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff P) + 1
⊢ spanFinrank P ≤ spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff P) + 1
have neg : ∀ (hfg : ¬P.FG), spanFinrank P ≤ spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff P) + 1
Tactic: by_cases hfg : P.FG
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R⟦X⟧
inst_1 : P.IsPrime
hfg : P.FG
⊢ spanFinrank P ≤ spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff P) + 1
have pos : ∀ (hP : X ∈ P), spanFinrank P ≤ spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff P) + 1
Tactic: by_cases hP : X ∈ P
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R⟦X⟧
inst_1 : P.IsPrime
hfg : P.FG
pos : ∀ (hP : X ∈ P), spanFinrank P ≤ spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff P) + 1
⊢ spanFinrank P ≤ spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff P) + 1
have neg : ∀ (hP : X ∉ P), spanFinrank P ≤ spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff P) + 1
Tactic: by_cases hP : X ∈ P
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R⟦X⟧
inst_1 : P.IsPrime
⊢ P.FG ↔ FG (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff P)
have mp : P.FG → FG (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff P)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R⟦X⟧
inst_1 : P.IsPrime
mp : P.FG → FG (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff P)
⊢ P.FG ↔ FG (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff P)
have mpr : FG (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff P) → P.FG
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R⟦X⟧
inst_1 : P.IsPrime
S : Finset R
hS : Eq (α := Ideal R) (span (↑S : Set R)) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff P)
⊢ P.FG
have pos : ∀ (hX : X ∈ P), P.FG
Tactic: by_cases hX : X ∈ P
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R⟦X⟧
inst_1 : P.IsPrime
S : Finset R
hS : Eq (α := Ideal R) (span (↑S : Set R)) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff P)
pos : ∀ (hX : X ∈ P), P.FG
⊢ P.FG
have neg : ∀ (hX : X ∉ P), P.FG
Tactic: by_cases hX : X ∈ P
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R⟦X⟧
inst_1 : P.IsPrime
S : Finset R
hS : Eq (α := Ideal R) (span (↑S : Set R)) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff P)
hX : X ∈ P
⊢ P.FG
have H : P = span (insert X ((⇑C : (a : R) → R⟦X⟧) '' (↑S : Set R)))
Tactic: have H := eq_span_insert_X_of_X_mem_of_span_eq hX hS
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R⟦X⟧
inst_1 : P.IsPrime
S : Finset R
hS : Eq (α := Ideal R) (span (↑S : Set R)) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff P)
hX : X ∈ P
H : P = span (insert X ((⇑C : (a : R) → R⟦X⟧) '' (↑S : Set R)))
⊢ P.FG
have this : Set.Finite (α := R⟦X⟧) (insert X ((⇑C : (a : R) → R⟦X⟧) '' (↑S : Set R)))
Tactic: have : (insert X <| (C (R := R)) '' S).Finite :=
        Finite.insert X <| Finite.image _ S.finite_toSet
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R⟦X⟧
inst_1 : P.IsPrime
S : Finset R
hS : Eq (α := Ideal R) (span (↑S : Set R)) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff P)
hX : X ∈ P
H : P = span (insert X ((⇑C : (a : R) → R⟦X⟧) '' (↑S : Set R)))
this : Set.Finite (α := R⟦X⟧) (insert X ((⇑C : (a : R) → R⟦X⟧) '' (↑S : Set R)))
⊢ P.FG
have pos : ∀ (T : Finset R⟦X⟧) (hT : (↑T : Set R⟦X⟧) = insert X ((⇑C : (a : R) → R⟦X⟧) '' (↑S : Set R)))
  (H : P = span (↑T : Set R⟦X⟧)), P.FG
Tactic: lift insert X <| (C (R := R)) '' S to Finset R⟦X⟧ using this with T hT
Cleared hypotheses: H, this
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R⟦X⟧
inst_1 : P.IsPrime
S : Finset R
hS : Eq (α := Ideal R) (span (↑S : Set R)) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff P)
hX : X ∉ P
⊢ P.FG
have neg : ∀ (T : Set R⟦X⟧) (hT : P = span T) (hT₂ : T.Finite), T.ncard = (↑S : Set R).ncard → P.FG
Tactic: obtain ⟨T, hT, hT₂, _⟩ := exist_eq_span_eq_ncard_of_X_notMem hX hS S.finite_toSet
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R⟦X⟧
inst_1 : P.IsPrime
S : Finset R
hS : Eq (α := Ideal R) (span (↑S : Set R)) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff P)
hX : X ∉ P
T : Set R⟦X⟧
hT : P = span T
hT₂ : T.Finite
right : T.ncard = (↑S : Set R).ncard
⊢ P.FG
have neg : ∀ (T : Finset R⟦X⟧) (hT : P = span (↑T : Set R⟦X⟧)), (↑T : Set R⟦X⟧).ncard = (↑S : Set R).ncard → P.FG
Tactic: lift T to Finset R⟦X⟧ using hT₂
Cleared hypotheses: T, hT, hT₂, right
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
S : Set R
P : Ideal R⟦X⟧
inst_1 : P.IsPrime
inst_2 : IsPrincipalIdealRing R
inst_3 : IsDomain R
⊢ UniqueFactorizationMonoid.{u_1} R⟦X⟧
have refine : ∀ (P : Ideal R⟦X⟧) (h₁ : P ≠ ⊥) (h₂ : P.IsPrime), ∃ x ∈ P, Prime x
Tactic: refine UniqueFactorizationMonoid.iff_exists_prime_mem_of_isPrime.mpr (fun P h₁ h₂ ↦ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
S : Set R
P_1 : Ideal R⟦X⟧
inst_1 : P_1.IsPrime
inst_2 : IsPrincipalIdealRing R
inst_3 : IsDomain R
P : Ideal R⟦X⟧
h₁ : P ≠ ⊥
h₂ : P.IsPrime
⊢ ∃ x ∈ P, Prime x
have pos : ∀ (hXP : X ∈ P), ∃ x ∈ P, Prime x
Tactic: by_cases hXP : X ∈ P
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
S : Set R
P_1 : Ideal R⟦X⟧
inst_1 : P_1.IsPrime
inst_2 : IsPrincipalIdealRing R
inst_3 : IsDomain R
P : Ideal R⟦X⟧
h₁ : P ≠ ⊥
h₂ : P.IsPrime
pos : ∀ (hXP : X ∈ P), ∃ x ∈ P, Prime x
⊢ ∃ x ∈ P, Prime x
have neg : ∀ (hXP : X ∉ P), ∃ x ∈ P, Prime x
Tactic: by_cases hXP : X ∈ P
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
S : Set R
P_1 : Ideal R⟦X⟧
inst_1 : P_1.IsPrime
inst_2 : IsPrincipalIdealRing R
inst_3 : IsDomain R
P : Ideal R⟦X⟧
h₁ : P ≠ ⊥
h₂ : P.IsPrime
hXP : X ∉ P
⊢ ∃ x ∈ P, Prime x
have neg : ∀ (w : R) (h : Eq (α := Submodule R R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff P) (R ∙ w)), ∃ x ∈ P, Prime x
Tactic: obtain ⟨_, h⟩ := (IsPrincipalIdealRing.principal (P.map constantCoeff)).principal
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
S : Set R
P_1 : Ideal R⟦X⟧
inst_1 : P_1.IsPrime
inst_2 : IsPrincipalIdealRing R
inst_3 : IsDomain R
P : Ideal R⟦X⟧
h₁ : P ≠ ⊥
h₂ : P.IsPrime
hXP : X ∉ P
w : R
h : Eq (α := Submodule R R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff P) (R ∙ w)
⊢ ∃ x ∈ P, Prime x
have neg : ∀ (w_1 : Set R⟦X⟧) (h₁ : Ne (α := Ideal R⟦X⟧) (span w_1) ⊥) (h₂ : IsPrime (span w_1)) (hXP : X ∉ span w_1)
  (h : Eq (α := Submodule R R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff (span w_1)) (R ∙ w)),
  w_1.Finite →
    ∀ (h : w_1.ncard = ncard (α := R) {w}), ∃ (x : R⟦X⟧), Membership.mem (γ := Ideal R⟦X⟧) (span w_1) x ∧ Prime x
Tactic: obtain ⟨_, rfl, _, h⟩ := exist_eq_span_eq_ncard_of_X_notMem hXP h.symm (finite_singleton _)
Cleared hypotheses: P, h₁, h₂, hXP, h