awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PowerSeries.GaussNorm
Goal:
R : Type u_1
inst : Semiring R
v : R → ℝ
c : ℝ
f : R⟦X⟧
h : HasGaussNorm v c f
suffices :
  Eq (α := Set ℝ) (Set.range fun (t : ℕ) ↦ v ((coeff t : (a : R⟦X⟧) → R) f) * c ^ t)
    (Set.range fun (t : Unit →₀ ℕ) ↦
      v ((MvPowerSeries.coeff t : (a : MvPowerSeries Unit R) → R) f) * t.prod fun (x : Unit) (x2 : ℕ) ↦ c ^ x2)
⊢ MvPowerSeries.HasGaussNorm v (fun (x : Unit) ↦ c) f

Tactic:
suffices (Set.range (fun (t : ℕ) ↦ (v (coeff t f) * c ^ t))) =
      Set.range fun t ↦ v ((MvPowerSeries.coeff t) f) * t.prod fun _ x2 ↦ c ^ x2 by
    simpa only [MvPowerSeries.HasGaussNorm, ← this]
-- Module: Mathlib.RingTheory.PowerSeries.GaussNorm
Goal:
R : Type u_1
inst : Semiring R
v : R → ℝ
c : ℝ
f : R⟦X⟧
h : HasGaussNorm v c f
⊢ Eq (α := Set ℝ) (Set.range fun (t : ℕ) ↦ v ((coeff t : (a : R⟦X⟧) → R) f) * c ^ t)
    (Set.range fun (t : Unit →₀ ℕ) ↦
      v ((MvPowerSeries.coeff t : (a : MvPowerSeries Unit R) → R) f) * t.prod fun (x : Unit) (x2 : ℕ) ↦ c ^ x2)

Tactic:
Set.ext (fun _ ↦ ?_)

Premises used: Set.ext
-- Module: Mathlib.RingTheory.PowerSeries.GaussNorm
Goal:
R : Type u_1
inst : Semiring R
v : R → ℝ
c : ℝ
f : R⟦X⟧
h : HasGaussNorm v c f
refine :
  ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Set.range fun (t : ℕ) ↦ v ((coeff t : (a : R⟦X⟧) → R) f) * c ^ t) x ↔
      Membership.mem (γ := Set ℝ)
        (Set.range fun (t : Unit →₀ ℕ) ↦
          v ((MvPowerSeries.coeff t : (a : MvPowerSeries Unit R) → R) f) * t.prod fun (x : Unit) (x2 : ℕ) ↦ c ^ x2)
        x
⊢ Eq (α := Set ℝ) (Set.range fun (t : ℕ) ↦ v ((coeff t : (a : R⟦X⟧) → R) f) * c ^ t)
    (Set.range fun (t : Unit →₀ ℕ) ↦
      v ((MvPowerSeries.coeff t : (a : MvPowerSeries Unit R) → R) f) * t.prod fun (x : Unit) (x2 : ℕ) ↦ c ^ x2)

Tactic:
refine Set.ext (fun _ ↦ ?_)

Premises used: Set.ext
-- Module: Mathlib.RingTheory.PowerSeries.GaussNorm
Goal:
R : Type u_1
inst : Semiring R
v : R → ℝ
c : ℝ
f : R⟦X⟧
h : HasGaussNorm v c f
x : ℝ
simp :
  (∃ (y : ℕ), v ((coeff y : (a : R⟦X⟧) → R) f) * c ^ y = x) ↔
    ∃ (y : Unit →₀ ℕ),
      v ((MvPowerSeries.coeff y : (a : MvPowerSeries Unit R) → R) f) *
          HPow.hPow (β := ℕ) c ((y : (a : Unit) → ℕ) PUnit.unit : ℕ) =
        x
⊢ Membership.mem (γ := Set ℝ) (Set.range fun (t : ℕ) ↦ v ((coeff t : (a : R⟦X⟧) → R) f) * c ^ t) x ↔
    Membership.mem (γ := Set ℝ)
      (Set.range fun (t : Unit →₀ ℕ) ↦
        v ((MvPowerSeries.coeff t : (a : MvPowerSeries Unit R) → R) f) * t.prod fun (x : Unit) (x2 : ℕ) ↦ c ^ x2)
      x

Tactic:
simp only [Set.mem_range, Finsupp.prod_pow, Finset.univ_unique, PUnit.default_eq_unit,
    Finset.prod_singleton]

Premises used: Set.mem_range, Finset.prod_singleton, Finset.univ_unique, Finsupp.prod_pow, PUnit.default_eq_unit
-- Module: Mathlib.RingTheory.PowerSeries.GaussNorm
Goal:
R : Type u_1
inst : Semiring R
v : R → ℝ
c : ℝ
f : R⟦X⟧
h : HasGaussNorm v c f
x : ℝ
mp :
  (∃ (y : ℕ), v ((coeff y : (a : R⟦X⟧) → R) f) * c ^ y = x) →
    ∃ (y : Unit →₀ ℕ),
      v ((MvPowerSeries.coeff y : (a : MvPowerSeries Unit R) → R) f) *
          HPow.hPow (β := ℕ) c ((y : (a : Unit) → ℕ) PUnit.unit : ℕ) =
        x
mpr :
  (∃ (y : Unit →₀ ℕ),
      v ((MvPowerSeries.coeff y : (a : MvPowerSeries Unit R) → R) f) *
          HPow.hPow (β := ℕ) c ((y : (a : Unit) → ℕ) PUnit.unit : ℕ) =
        x) →
    ∃ (y : ℕ), v ((coeff y : (a : R⟦X⟧) → R) f) * c ^ y = x
⊢ (∃ (y : ℕ), v ((coeff y : (a : R⟦X⟧) → R) f) * c ^ y = x) ↔
    ∃ (y : Unit →₀ ℕ),
      v ((MvPowerSeries.coeff y : (a : MvPowerSeries Unit R) → R) f) *
          HPow.hPow (β := ℕ) c ((y : (a : Unit) → ℕ) PUnit.unit : ℕ) =
        x

Tactic:
constructor
-- Module: Mathlib.RingTheory.PowerSeries.GaussNorm
Goal:
R : Type u_1
inst : Semiring R
v : R → ℝ
c : ℝ
f : R⟦X⟧
h_1 : HasGaussNorm v c f
x : ℝ
h : ∃ (y : ℕ), v ((coeff y : (a : R⟦X⟧) → R) f) * c ^ y = x
mp :
  ∀ (y : ℕ) (hy : v ((coeff y : (a : R⟦X⟧) → R) f) * c ^ y = x),
    ∃ (y : Unit →₀ ℕ),
      v ((MvPowerSeries.coeff y : (a : MvPowerSeries Unit R) → R) f) *
          HPow.hPow (β := ℕ) c ((y : (a : Unit) → ℕ) PUnit.unit : ℕ) =
        x
⊢ ∃ (y : Unit →₀ ℕ),
    v ((MvPowerSeries.coeff y : (a : MvPowerSeries Unit R) → R) f) *
        HPow.hPow (β := ℕ) c ((y : (a : Unit) → ℕ) PUnit.unit : ℕ) =
      x

Tactic:
obtain ⟨y, hy⟩ := h
-- Module: Mathlib.RingTheory.PowerSeries.GaussNorm
Goal:
R : Type u_1
inst : Semiring R
v : R → ℝ
c : ℝ
f : R⟦X⟧
h : HasGaussNorm v c f
x : ℝ
y : ℕ
hy : v ((coeff y : (a : R⟦X⟧) → R) f) * c ^ y = x
h₁ :
  v
        ((MvPowerSeries.coeff ((Equiv.symm (Finsupp.uniqueEquiv ()) : (a : ℕ) → Unit →₀ ℕ) y) :
            (a : MvPowerSeries Unit R) → R)
          f) *
      HPow.hPow (β := ℕ) c
        ((((Equiv.symm (Finsupp.uniqueEquiv ()) : (a : ℕ) → Unit →₀ ℕ) y : Unit →₀ ℕ) : (a : Unit) → ℕ) PUnit.unit :
          ℕ) =
    x
⊢ ∃ (y : Unit →₀ ℕ),
    v ((MvPowerSeries.coeff y : (a : MvPowerSeries Unit R) → R) f) *
        HPow.hPow (β := ℕ) c ((y : (a : Unit) → ℕ) PUnit.unit : ℕ) =
      x

Tactic:
use (Finsupp.uniqueEquiv ()).symm y

Premises used: Unit.unit, Finsupp.uniqueEquiv, Equiv.symm, DFunLike.coe
-- Module: Mathlib.RingTheory.PowerSeries.GaussNorm
Goal:
R : Type u_1
inst : Semiring R
v : R → ℝ
c : ℝ
f : R⟦X⟧
h : HasGaussNorm v c f
x : ℝ
y : ℕ
hy : v ((coeff y : (a : R⟦X⟧) → R) f) * c ^ y = x
⊢ v
        ((MvPowerSeries.coeff ((Equiv.symm (Finsupp.uniqueEquiv ()) : (a : ℕ) → Unit →₀ ℕ) y) :
            (a : MvPowerSeries Unit R) → R)
          f) *
      HPow.hPow (β := ℕ) c
        ((((Equiv.symm (Finsupp.uniqueEquiv ()) : (a : ℕ) → Unit →₀ ℕ) y : Unit →₀ ℕ) : (a : Unit) → ℕ) PUnit.unit :
          ℕ) =
    x

Tactic:
simpa [coeff] using hy

Premises used: PowerSeries.coeff
-- Module: Mathlib.RingTheory.PowerSeries.GaussNorm
Goal:
R : Type u_1
inst : Semiring R
v : R → ℝ
c : ℝ
f : R⟦X⟧
h_1 : HasGaussNorm v c f
x : ℝ
h :
  ∃ (y : Unit →₀ ℕ),
    v ((MvPowerSeries.coeff y : (a : MvPowerSeries Unit R) → R) f) *
        HPow.hPow (β := ℕ) c ((y : (a : Unit) → ℕ) PUnit.unit : ℕ) =
      x
mpr :
  ∀ (y : Unit →₀ ℕ)
    (hy :
      v ((MvPowerSeries.coeff y : (a : MvPowerSeries Unit R) → R) f) *
          HPow.hPow (β := ℕ) c ((y : (a : Unit) → ℕ) PUnit.unit : ℕ) =
        x),
    ∃ (y : ℕ), v ((coeff y : (a : R⟦X⟧) → R) f) * c ^ y = x
⊢ ∃ (y : ℕ), v ((coeff y : (a : R⟦X⟧) → R) f) * c ^ y = x

Tactic:
obtain ⟨y, hy⟩ := h
-- Module: Mathlib.RingTheory.PowerSeries.GaussNorm
Goal:
R : Type u_1
inst : Semiring R
v : R → ℝ
c : ℝ
f : R⟦X⟧
h : HasGaussNorm v c f
x : ℝ
y : Unit →₀ ℕ
hy :
  v ((MvPowerSeries.coeff y : (a : MvPowerSeries Unit R) → R) f) *
      HPow.hPow (β := ℕ) c ((y : (a : Unit) → ℕ) PUnit.unit : ℕ) =
    x
h₁ :
  v ((coeff ((Finsupp.uniqueEquiv () : (a : Unit →₀ ℕ) → ℕ) y) : (a : R⟦X⟧) → R) f) *
      HPow.hPow (β := ℕ) c ((Finsupp.uniqueEquiv () : (a : Unit →₀ ℕ) → ℕ) y : ℕ) =
    x
⊢ ∃ (y : ℕ), v ((coeff y : (a : R⟦X⟧) → R) f) * c ^ y = x

Tactic:
use Finsupp.uniqueEquiv () y

Premises used: Unit.unit, Finsupp.uniqueEquiv, DFunLike.coe
-- Module: Mathlib.RingTheory.PowerSeries.GaussNorm
Goal:
R : Type u_1
inst : Semiring R
v : R → ℝ
c : ℝ
f : R⟦X⟧
h : HasGaussNorm v c f
x : ℝ
y : Unit →₀ ℕ
hy :
  v ((MvPowerSeries.coeff y : (a : MvPowerSeries Unit R) → R) f) *
      HPow.hPow (β := ℕ) c ((y : (a : Unit) → ℕ) PUnit.unit : ℕ) =
    x
⊢ Finsupp.single () ((y : (a : Unit) → ℕ) PUnit.unit) = y

Tactic:
grind
-- Module: Mathlib.RingTheory.PowerSeries.GaussNorm
Goal:
R : Type u_1
inst : Semiring R
v : R → ℝ
c : ℝ
f : R⟦X⟧
h : HasGaussNorm v c f
x : ℝ
y : Unit →₀ ℕ
hy :
  v ((MvPowerSeries.coeff y : (a : MvPowerSeries Unit R) → R) f) *
      HPow.hPow (β := ℕ) c ((y : (a : Unit) → ℕ) PUnit.unit : ℕ) =
    x
⊢ v ((coeff ((Finsupp.uniqueEquiv () : (a : Unit →₀ ℕ) → ℕ) y) : (a : R⟦X⟧) → R) f) *
      HPow.hPow (β := ℕ) c ((Finsupp.uniqueEquiv () : (a : Unit →₀ ℕ) → ℕ) y : ℕ) =
    x

Tactic:
simpa [coeff, show (Finsupp.single () (y PUnit.unit)) = y by grind]

Premises used: PowerSeries.coeff
-- Module: Mathlib.RingTheory.PowerSeries.GaussNorm
Goal:
R : Type u_1
inst : Semiring R
v : R → ℝ
c : ℝ
vZero : v 0 = 0
⊢ gaussNorm v c 0 = 0

Tactic:
MvPowerSeries.gaussNorm_zero v (fun _ ↦ c) vZero

Premises used: MvPowerSeries.gaussNorm_zero
-- Module: Mathlib.RingTheory.PowerSeries.GaussNorm
Goal:
R : Type u_1
inst : Semiring R
v : R → ℝ
c : ℝ
f : R⟦X⟧
hbd : HasGaussNorm v c f
t : ℕ
rw : v ((coeff t : (a : R⟦X⟧) → R) f) * c ^ t ≤ ⨆ (i : ℕ), v ((coeff i : (a : R⟦X⟧) → R) f) * c ^ i
⊢ v ((coeff t : (a : R⟦X⟧) → R) f) * c ^ t ≤ gaussNorm v c f

Tactic:
rw [gaussNorm_eq]

Premises used: PowerSeries.gaussNorm_eq
-- Module: Mathlib.RingTheory.PowerSeries.GaussNorm
Goal:
R : Type u_1
inst : Semiring R
v : R → ℝ
c : ℝ
f : R⟦X⟧
hbd : HasGaussNorm v c f
t : ℕ
⊢ v ((coeff t : (a : R⟦X⟧) → R) f) * c ^ t ≤ ⨆ (i : ℕ), v ((coeff i : (a : R⟦X⟧) → R) f) * c ^ i

Tactic:
apply le_ciSup hbd

Premises used: le_ciSup
-- Module: Mathlib.RingTheory.PowerSeries.GaussNorm
Goal:
R : Type u_1
inst : Semiring R
v : R → ℝ
c : ℝ
f : R⟦X⟧
vNonneg : ∀ (a : R), v a ≥ 0
⊢ 0 ≤ gaussNorm v c f

Tactic:
MvPowerSeries.gaussNorm_nonneg v (fun _ ↦ c) f vNonneg

Premises used: MvPowerSeries.gaussNorm_nonneg
-- Module: Mathlib.RingTheory.PowerSeries.GaussNorm
Goal:
R : Type u_1
inst : Semiring R
v : R → ℝ
c : ℝ
f : R⟦X⟧
vZero : v 0 = 0
vNonneg : ∀ (a : R), v a ≥ 0
h_eq_zero : ∀ (x : R), v x = 0 → x = 0
hc : 0 < c
hbd : HasGaussNorm v c f
⊢ ∀ (i : Unit), LT.lt (α := ℝ) 0 ((fun (x : Unit) ↦ c) i)

Tactic:
grind
-- Module: Mathlib.RingTheory.PowerSeries.GaussNorm
Goal:
R : Type u_1
inst : Semiring R
v : R → ℝ
c : ℝ
f g : R⟦X⟧
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
hv : ∀ (x y : R), v (x + y) ≤ max (v x) (v y)
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
x : Unit
⊢ LE.le (α := (fun (a : Unit) ↦ ℝ) x) (0 x) ((fun (x : Unit) ↦ c) x)

Tactic:
simp [hc]
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
hXI : X ∈ I
this : ∀ x ∈ I, Membership.mem (α := R⟦X⟧) I ((C : (a : R) → R⟦X⟧) ((constantCoeff : (a : R⟦X⟧) → R) x : R) : R⟦X⟧)
⊢ Ideal.map (F := R⟦X⟧ →+* R⟦X⟧) (RingHom.comp C constantCoeff) I ≤ I

Tactic:
simpa [Ideal.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⟧
hXI : X ∈ I
suffices : ∀ x ∈ I, Membership.mem (α := R⟦X⟧) I ((C : (a : R) → R⟦X⟧) ((constantCoeff : (a : R⟦X⟧) → R) x : R) : R⟦X⟧)
⊢ Ideal.map (F := R⟦X⟧ →+* R⟦X⟧) (RingHom.comp C constantCoeff) I ≤ I

Tactic:
suffices ∀ x ∈ I, C (constantCoeff x) ∈ I by simpa [Ideal.map_le_iff_le_comap]
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
hXI : X ∈ I
f : R⟦X⟧
hf : f ∈ I
rw : f - HMul.hMul (α := R⟦X⟧) X (mk fun (p : ℕ) ↦ (coeff (p + 1) : (a : R⟦X⟧) → R) f) ∈ I
⊢ Membership.mem (α := R⟦X⟧) I ((C : (a : R) → R⟦X⟧) ((constantCoeff : (a : R⟦X⟧) → R) f : R) : R⟦X⟧)

Tactic:
rw [← sub_eq_iff_eq_add'.mpr f.eq_X_mul_shift_add_const]

Premises used: Iff.mpr, PowerSeries.eq_X_mul_shift_add_const, sub_eq_iff_eq_add'
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
hXI : X ∈ I
f : R⟦X⟧
hf : f ∈ I
⊢ f - HMul.hMul (α := R⟦X⟧) X (mk fun (p : ℕ) ↦ (coeff (p + 1) : (a : R⟦X⟧) → R) f) ∈ I

Tactic:
sub_mem hf (I.mul_mem_right _ hXI)

Premises used: Set.Mem, sub_mem, Ideal.mul_mem_right
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
hXI : X ∈ I
f : R⟦X⟧
hf : f ∈ I
⊢ f - HMul.hMul (α := R⟦X⟧) X (mk fun (p : ℕ) ↦ (coeff (p + 1) : (a : R⟦X⟧) → R) f) ∈ I

Tactic:
exact sub_mem hf (I.mul_mem_right _ hXI)

Premises used: sub_mem, Ideal.mul_mem_right
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
S : Set R
hXI : X ∈ I
hSI : Eq (α := Ideal R) (span S) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
rw : I = span {X} ⊔ Ideal.map (F := R⟦X⟧ →+* R⟦X⟧) (RingHom.comp C constantCoeff) I
⊢ I = span (insert X ((⇑C : (a : R) → R⟦X⟧) '' S))

Tactic:
rw [Ideal.span_insert, ← Ideal.map_span, hSI, Ideal.map_map]

Premises used: Ideal.map_span, Ideal.map_map, Ideal.span_insert
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
S : Set R
hXI : X ∈ I
hSI : Eq (α := Ideal R) (span S) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
⊢ span {X} ⊔ Ideal.map (F := R⟦X⟧ →+* R⟦X⟧) (RingHom.comp C constantCoeff) I ≤ I

Tactic:
simp [Ideal.span_le, hXI, map_constantCoeff_le_self_of_X_mem]

Premises used: Ideal.span_le, PowerSeries.map_constantCoeff_le_self_of_X_mem
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
S : Set R
hXI : X ∈ I
hSI : Eq (α := Ideal R) (span S) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
refine : I ≤ span {X} ⊔ Ideal.map (F := R⟦X⟧ →+* R⟦X⟧) (RingHom.comp C constantCoeff) I
⊢ I = span {X} ⊔ Ideal.map (F := R⟦X⟧ →+* R⟦X⟧) (RingHom.comp C constantCoeff) I

Tactic:
refine le_antisymm ?_ (by simp [Ideal.span_le, hXI, map_constantCoeff_le_self_of_X_mem])

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
S : Set R
hXI : X ∈ I
hSI : Eq (α := Ideal R) (span S) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
⊢ I ≤ span {X} ⊔ Ideal.map (F := R⟦X⟧ →+* R⟦X⟧) (RingHom.comp C constantCoeff) I

Tactic:
fun f hf ↦ mem_span_singleton_sup.mpr
    ⟨_, _, mem_map_of_mem _ hf, f.eq_shift_mul_X_add_const.symm⟩

Premises used: Iff.mpr, Ideal.mem_map_of_mem, Set.Mem, PowerSeries.coeff, PowerSeries.constantCoeff, Ideal.mem_span_singleton_sup, PowerSeries.C, RingHom.comp, HAdd.hAdd, PowerSeries.eq_shift_mul_X_add_const, And.intro, Exists.intro, PowerSeries.mk, OfNat.ofNat, Eq.symm, DFunLike.coe
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
S : Set R
hXI : X ∈ I
hSI : Eq (α := Ideal R) (span S) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
⊢ I ≤ span {X} ⊔ Ideal.map (F := R⟦X⟧ →+* R⟦X⟧) (RingHom.comp C constantCoeff) I

Tactic:
exact fun f hf ↦ mem_span_singleton_sup.mpr
    ⟨_, _, mem_map_of_mem _ hf, f.eq_shift_mul_X_add_const.symm⟩

Premises used: Iff.mpr, Ideal.mem_map_of_mem, Ideal.mem_span_singleton_sup, And.intro, Exists.intro, DFunLike.coe
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
hI : X ∈ I
pos : ∀ (hfg : I.FG), spanFinrank I ≤ spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I) + 1
neg : ∀ (hfg : ¬I.FG), spanFinrank I ≤ spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I) + 1
⊢ spanFinrank I ≤ spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I) + 1

Tactic:
by_cases hfg : I.FG

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

Tactic:
spanFinrank_of_not_fg hfg ▸ Nat.zero_le _

Premises used: Nat.zero_le, Eq.rec, Submodule.spanFinrank_of_not_fg, Eq.symm
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
hI : X ∈ I
hfg : ¬I.FG
⊢ spanFinrank I ≤ spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I) + 1

Tactic:
exact spanFinrank_of_not_fg hfg ▸ Nat.zero_le _
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
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⟧
hI : X ∈ I
hfg : I.FG
this : RingHomSurjective.{u_1, u_1} (R₁ := R⟦X⟧) constantCoeff
⊢ Ideal.FG (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)

Tactic:
map_eq_submodule_map constantCoeff I ▸ Submodule.FG.map _ hfg

Premises used: Submodule.FG.map, Eq.rec, PowerSeries.constantCoeff, Ideal.map_eq_submodule_map, Eq.symm
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
hI : X ∈ I
hfg : I.FG
this : RingHomSurjective.{u_1, u_1} (R₁ := R⟦X⟧) constantCoeff
⊢ Ideal.FG (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)

Tactic:
exact map_eq_submodule_map constantCoeff I ▸ Submodule.FG.map _ hfg
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
hI : X ∈ I
hfg : I.FG
⊢ Ideal.FG (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)

Tactic:
replace hfg : (Ideal.map constantCoeff I).FG := by
    have : RingHomSurjective (constantCoeff (R := R)) := ⟨constantCoeff_surj⟩
    exact map_eq_submodule_map constantCoeff I ▸ Submodule.FG.map _ hfg
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
hI : X ∈ I
hfg : Ideal.FG (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
pos :
  spanFinrank (R := R⟦X⟧)
      (Ideal.span
        (insert X
          (Set.image (α := R) (⇑C : (a : R) → R⟦X⟧) (generators (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I))))) ≤
    spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I) + 1
⊢ spanFinrank I ≤ spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I) + 1

Tactic:
nth_rw 1 [eq_span_insert_X_of_X_mem_of_span_eq hI (I.map constantCoeff).span_generators]

Premises used: Ideal.map, PowerSeries.constantCoeff, Submodule.span_generators, PowerSeries.eq_span_insert_X_of_X_mem_of_span_eq
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
hI : X ∈ I
hfg : Ideal.FG (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
⊢ spanFinrank (R := R⟦X⟧)
      (Ideal.span
        (insert X
          (Set.image (α := R) (⇑C : (a : R) → R⟦X⟧) (generators (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I))))) ≤
    spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I) + 1

Tactic:
le_trans (spanFinrank_span_le_ncard_of_finite ?_) (le_trans (Set.ncard_insert_le _ _) ?_)

Premises used: Submodule.spanFinrank_span_le_ncard_of_finite, Set.ncard_insert_le, le_trans
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
hI : X ∈ I
hfg : Ideal.FG (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
pos :
  Set.Finite (α := R⟦X⟧)
    (insert X (Set.image (α := R) (⇑C : (a : R) → R⟦X⟧) (generators (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I))))
pos₁ :
  ncard (α := R⟦X⟧)
        (Set.image (α := R) (⇑C : (a : R) → R⟦X⟧) (generators (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I))) +
      1 ≤
    spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I) + 1
⊢ spanFinrank (R := R⟦X⟧)
      (Ideal.span
        (insert X
          (Set.image (α := R) (⇑C : (a : R) → R⟦X⟧) (generators (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I))))) ≤
    spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I) + 1

Tactic:
refine le_trans (spanFinrank_span_le_ncard_of_finite ?_) (le_trans (Set.ncard_insert_le _ _) ?_)

Premises used: Submodule.spanFinrank_span_le_ncard_of_finite, Set.ncard_insert_le, le_trans
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
hI : X ∈ I
hfg : Ideal.FG (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
⊢ Set.Finite (α := R⟦X⟧)
    (insert X (Set.image (α := R) (⇑C : (a : R) → R⟦X⟧) (generators (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I))))

Tactic:
simpa using Set.Finite.map _ (FG.finite_generators hfg)

Premises used: Set.Finite.map, Submodule.FG.finite_generators
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
hI : X ∈ I
hfg : Ideal.FG (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
pos :
  ncard (α := R⟦X⟧)
      (Set.image (α := R) (⇑C : (a : R) → R⟦X⟧) (generators (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I))) ≤
    spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
⊢ ncard (α := R⟦X⟧)
        (Set.image (α := R) (⇑C : (a : R) → R⟦X⟧) (generators (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I))) +
      1 ≤
    spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I) + 1

Tactic:
simp only [add_le_add_iff_right]

Premises used: add_le_add_iff_right
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
hI : X ∈ I
hfg : Ideal.FG (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
⊢ ncard (α := R⟦X⟧)
      (Set.image (α := R) (⇑C : (a : R) → R⟦X⟧) (generators (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I))) ≤
    spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)

Tactic:
le_trans (Set.ncard_image_le (FG.finite_generators hfg)) ?_

Premises used: Set.ncard_image_le, Submodule.FG.finite_generators, le_trans
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
hI : X ∈ I
hfg : Ideal.FG (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
pos :
  ncard (α := R) (generators (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)) ≤
    spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
⊢ ncard (α := R⟦X⟧)
      (Set.image (α := R) (⇑C : (a : R) → R⟦X⟧) (generators (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I))) ≤
    spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)

Tactic:
refine le_trans (Set.ncard_image_le (FG.finite_generators hfg)) ?_

Premises used: Set.ncard_image_le, Submodule.FG.finite_generators, le_trans
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
hI : X ∈ I
hfg : Ideal.FG (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
pos pos₁ :
  spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I) ≤
    spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
⊢ ncard (α := R) (generators (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)) ≤
    spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)

Tactic:
rw [FG.generators_ncard hfg]

Premises used: Submodule.FG.generators_ncard
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
inst_1 : I.IsPrime
J : Ideal R⟦X⟧
hJI : J ≤ I
hXI : X ∉ I
hJ : J.FG
h' : LE.le (α := Ideal R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff J)
⊢ I = J

Tactic:
hJI.antisymm' ?_

Premises used: LE.le.antisymm'
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
inst_1 : I.IsPrime
J : Ideal R⟦X⟧
hJI : J ≤ I
hXI : X ∉ I
hJ : J.FG
h' : LE.le (α := Ideal R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff J)
refine : I ≤ J
⊢ I = J

Tactic:
refine hJI.antisymm' ?_

Premises used: LE.le.antisymm'
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
inst_1 : I.IsPrime
J : Ideal R⟦X⟧
hJI : J ≤ I
hXI : X ∉ I
hJ : J.FG
h' : LE.le (α := Ideal R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff J)
⊢ Eq (α := Ideal R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff J)

Tactic:
replace h' := h'.antisymm (Ideal.map_mono hJI)
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
inst_1 : I.IsPrime
J : Ideal R⟦X⟧
hJI : J ≤ I
hXI : X ∉ I
hJ : J.FG
h' : Eq (α := Ideal R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff J)
obtain :
  ∀ (n : ℕ) (F : Fin n → R⟦X⟧) (hJI : Submodule.span R⟦X⟧ (Set.range F) ≤ I)
    (hJ : FG (Submodule.span R⟦X⟧ (Set.range F)))
    (h' :
      Eq (α := Ideal R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
        (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff (Submodule.span R⟦X⟧ (Set.range F)))),
    I ≤ Submodule.span R⟦X⟧ (Set.range F)
⊢ I ≤ J

Tactic:
obtain ⟨n, F, rfl⟩ := Submodule.fg_iff_exists_fin_generating_family.mp hJ

Premises used: Submodule.fg_iff_exists_fin_generating_family, Iff.mp, rfl