awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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
obtain :
  ∀ (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
⊢ ∃ (T : Set R⟦X⟧), I = span T ∧ T.Finite ∧ T.ncard = S.ncard

Tactic:
obtain ⟨T, hTI, hinj, hT⟩ := this.exists_subset_injOn_image_eq

Premises used: Set.SurjOn.exists_subset_injOn_image_eq
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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

Tactic:
⟨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⟩

Premises used: Ideal.span_le, Iff.mpr, PowerSeries.eq_of_le_of_X_notMem_of_fg_of_isPrime, Submodule.fg_def, Eq.rec, Set.InjOn.ncard_image, And.intro, Set.Finite.of_injOn, Exists.intro, Eq.symm, rfl
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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
refine :
  LE.le (α := Ideal R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
    (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff (span T))
⊢ ∃ (T : Set R⟦X⟧), I = span T ∧ T.Finite ∧ T.ncard = S.ncard

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⟩
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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
rw : I ≤ comap (F := R⟦X⟧ →+* R) constantCoeff (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff (span T))
⊢ LE.le (α := Ideal R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
    (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff (span T))

Tactic:
rw [map_le_iff_le_comap]

Premises used: Ideal.map_le_iff_le_comap
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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
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)
⊢ Membership.mem (γ := Submodule R⟦X⟧ R⟦X⟧)
    (comap (F := R⟦X⟧ →+* R) constantCoeff (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff (span T))) f

Tactic:
rw [mem_comap, mem_map_iff_of_surjective _ constantCoeff_surj]

Premises used: PowerSeries.constantCoeff_surj, Ideal.mem_map_iff_of_surjective, Ideal.mem_comap
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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 (α := 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
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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)
⊢ Eq.{u_1 + 1} (α := R) ((constantCoeff : (a : R⟦X⟧) → R) 0 : R) (0 : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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
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
⊢ ∃ (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:
refine Submodule.span_induction (fun s hs ↦ ?_) ⟨0, zero_mem _, by simp⟩ ?_ ?_ hf
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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
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
⊢ ∃ (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
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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
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:
⟨t, subset_span htmem, ht⟩

Premises used: Ideal.subset_span, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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
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:
exact ⟨t, subset_span htmem, ht⟩
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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₂
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₂
⊢ (∃ (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₂

Tactic:
⟨s₁, hs₁mem, hs₁⟩
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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₁
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₂
⊢ (∃ (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₂⟩
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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₁
s₂ : R⟦X⟧
hs₂mem : Membership.mem (γ := Ideal R⟦X⟧) (span T) s₂
hs₂ : (constantCoeff : (a : R⟦X⟧) → R) s₂ = r₂
⊢ (constantCoeff : (a : R⟦X⟧) → R) (s₁ + s₂) = r₁ + r₂

Tactic:
simp [hs₁, hs₂]
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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₁
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:
exact ⟨s₁ + s₂, Ideal.add_mem _ hs₁mem hs₂mem, by simp [hs₁, hs₂]⟩
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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₂
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₂
⊢ (∃ (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:
⟨f, hfmem, hf⟩
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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_1 : R⟦X⟧
hf_1 : Membership.mem (α := R) (γ := Ideal R) (span S) ((constantCoeff : (a : R⟦X⟧) → R) f_1 : R)
r₁ r₂ : R
hr₁ : Membership.mem (γ := Submodule R R) (Submodule.span R S) r₂
f : R⟦X⟧
hfmem : Membership.mem (γ := Ideal R⟦X⟧) (span T) f
hf : (constantCoeff : (a : R⟦X⟧) → R) f = r₂
⊢ (constantCoeff : (a : R⟦X⟧) → R) (r₁ • f) = r₁ • r₂

Tactic:
simp [hf]
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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_1 : R⟦X⟧
hf_1 : Membership.mem (α := R) (γ := Ideal R) (span S) ((constantCoeff : (a : R⟦X⟧) → R) f_1 : R)
r₁ r₂ : R
hr₁ : Membership.mem (γ := Submodule R R) (Submodule.span R S) r₂
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:
exact ⟨r₁ • f, Submodule.smul_of_tower_mem _ _ hfmem, by simp [hf]⟩
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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)

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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)
refine_2 : spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I) ≤ spanFinrank I
⊢ spanFinrank I = spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
inst_1 : I.IsPrime
hI : X ∉ I
hfg : I.FG
⊢ spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I) ≤ spanFinrank I

Tactic:
Ideal.spanFinrank_map_le_of_fg constantCoeff hfg

Premises used: Ideal.spanFinrank_map_le_of_fg, PowerSeries.constantCoeff
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
inst_1 : I.IsPrime
hI : X ∉ I
hfg : I.FG
⊢ spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I) ≤ spanFinrank I

Tactic:
exact Ideal.spanFinrank_map_le_of_fg constantCoeff hfg

Premises used: Ideal.spanFinrank_map_le_of_fg, PowerSeries.constantCoeff
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
inst_1 : I.IsPrime
hI : X ∉ I
hfg : I.FG
⊢ RingHomSurjective.{u_1, u_1} (R₁ := R⟦X⟧) constantCoeff

Tactic:
have : RingHomSurjective (constantCoeff (R := R)) := ⟨constantCoeff_surj⟩
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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
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))
⊢ spanFinrank I ≤ spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)

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)

Premises used: Submodule.FG.map, Eq.rec, Ideal.map, PowerSeries.constantCoeff, PowerSeries.exist_eq_span_eq_ncard_of_X_notMem, Ideal.map_eq_submodule_map, Submodule.FG.finite_generators, Eq.symm, rfl, Submodule.span_generators
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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))

Tactic:
le_trans (spanFinrank_span_le_ncard_of_finite hS) ?_

Premises used: Submodule.spanFinrank_span_le_ncard_of_finite, le_trans
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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)))
refine_1 : S.ncard ≤ spanFinrank (R := R) (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:
refine le_trans (spanFinrank_span_le_ncard_of_finite hS) ?_

Premises used: Submodule.spanFinrank_span_le_ncard_of_finite, le_trans
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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)))
refine_1 : Submodule.FG (R := R) (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))

Tactic:
rw [hScard, FG.generators_ncard]

Premises used: Submodule.FG.generators_ncard
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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)))
⊢ Submodule.FG (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff (Ideal.span S))

Tactic:
map_eq_submodule_map constantCoeff (Ideal.span S) ▸ Submodule.FG.map _ hfg

Premises used: Submodule.FG.map, Eq.rec, PowerSeries.constantCoeff, Ideal.map_eq_submodule_map, Ideal.span, Eq.symm
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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)))
⊢ Submodule.FG (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff (Ideal.span S))

Tactic:
exact map_eq_submodule_map constantCoeff (Ideal.span S) ▸ Submodule.FG.map _ hfg
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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
neg : ∀ (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

Tactic:
by_cases hfg : P.FG

Premises used: Ideal.FG
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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

Tactic:
spanFinrank_of_not_fg hfg ▸ Nat.zero_le _

Premises used: Nat.zero_le, Eq.rec, Submodule.spanFinrank_of_not_fg, Eq.symm