awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact spanFinrank_of_not_fg hfg ▸ Nat.zero_le _
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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
neg : ∀ (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

Tactic:
by_cases hP : X ∈ P

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

Tactic:
spanFinrank_le_spanFinrank_map_constantCoeff_add_one_of_X_mem hP

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

Tactic:
exact spanFinrank_le_spanFinrank_map_constantCoeff_add_one_of_X_mem hP

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

Tactic:
le_trans (spanFinrank_eq_spanFinrank_map_constantCoeff_of_X_notMem_of_fg_of_isPrime
      hP hfg).le (Nat.le_succ _)

Premises used: Eq.le, Nat.le_succ, PowerSeries.spanFinrank_eq_spanFinrank_map_constantCoeff_of_X_notMem_of_fg_of_isPrime, le_trans
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R⟦X⟧
inst_1 : P.IsPrime
hfg : P.FG
hP : X ∉ P
⊢ spanFinrank P ≤ spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff P) + 1

Tactic:
exact le_trans (spanFinrank_eq_spanFinrank_map_constantCoeff_of_X_notMem_of_fg_of_isPrime
      hP hfg).le (Nat.le_succ _)

Premises used: Eq.le, Nat.le_succ, PowerSeries.spanFinrank_eq_spanFinrank_map_constantCoeff_of_X_notMem_of_fg_of_isPrime, le_trans
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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)
mpr : FG (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff P) → P.FG
⊢ P.FG ↔ FG (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff P)

Tactic:
constructor
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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)

Tactic:
(FG.map · _)

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

Tactic:
exact (FG.map · _)

Premises used: Ideal.FG.map
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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
neg : ∀ (hX : X ∉ P), P.FG
⊢ P.FG

Tactic:
by_cases hX : X ∈ P

Premises used: PowerSeries.X
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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 = 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
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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)))
⊢ 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
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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)))
⊢ Set.Finite (α := R⟦X⟧) (insert X ((⇑C : (a : R) → R⟦X⟧) '' (↑S : Set R)))

Tactic:
this
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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)))
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
⊢ P.FG

Tactic:
lift insert X <| (C (R := R)) '' S to Finset R⟦X⟧ using this with T hT

Premises used: Finset, Insert.insert, PowerSeries.X, PowerSeries.C, PowerSeries
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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 : 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:
⟨T, hT ▸ H.symm⟩

Premises used: Eq.rec, Ideal.FG, Exists.intro, Eq.symm
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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 : 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:
exact ⟨T, hT ▸ H.symm⟩
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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
neg : ∀ (T : Set R⟦X⟧) (hT : P = span T) (hT₂ : T.Finite), T.ncard = (↑S : Set R).ncard → P.FG
⊢ P.FG

Tactic:
obtain ⟨T, hT, hT₂, _⟩ := exist_eq_span_eq_ncard_of_X_notMem hX hS S.finite_toSet

Premises used: PowerSeries.exist_eq_span_eq_ncard_of_X_notMem, Finset.finite_toSet
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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
⊢ T.Finite

Tactic:
hT₂
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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
neg : ∀ (T : Finset R⟦X⟧) (hT : P = span (↑T : Set R⟦X⟧)), (↑T : Set R⟦X⟧).ncard = (↑S : Set R).ncard → P.FG
⊢ P.FG

Tactic:
lift T to Finset R⟦X⟧ using hT₂

Premises used: Finset, PowerSeries
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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 : Finset R⟦X⟧
hT : P = span (↑T : Set R⟦X⟧)
right : (↑T : Set R⟦X⟧).ncard = (↑S : Set R).ncard
⊢ P.FG

Tactic:
⟨T, hT.symm⟩

Premises used: Ideal.FG, Exists.intro, Eq.symm
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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 : Finset R⟦X⟧
hT : P = span (↑T : Set R⟦X⟧)
right : (↑T : Set R⟦X⟧).ncard = (↑S : Set R).ncard
⊢ P.FG

Tactic:
exact ⟨T, hT.symm⟩
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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 : IsNoetherianRing R
⊢ IsNoetherianRing.{u_1} R⟦X⟧

Tactic:
IsNoetherianRing.of_prime fun P _ ↦
    fg_iff_of_isPrime.2 <| (isNoetherianRing_iff_ideal_fg R).1 inferInstance (P.map constantCoeff)

Premises used: Iff.mpr, IsNoetherianRing.of_prime, isNoetherianRing_iff_ideal_fg, inferInstance, Ideal.map, PowerSeries.constantCoeff, PowerSeries.fg_iff_of_isPrime, Iff.mp
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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⟧

Tactic:
UniqueFactorizationMonoid.iff_exists_prime_mem_of_isPrime.mpr (fun P h₁ h₂ ↦ ?_)

Premises used: Iff.mpr, UniqueFactorizationMonoid.iff_exists_prime_mem_of_isPrime
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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
refine : ∀ (P : Ideal R⟦X⟧) (h₁ : P ≠ ⊥) (h₂ : P.IsPrime), ∃ x ∈ P, Prime x
⊢ UniqueFactorizationMonoid.{u_1} R⟦X⟧

Tactic:
refine UniqueFactorizationMonoid.iff_exists_prime_mem_of_isPrime.mpr (fun P h₁ h₂ ↦ ?_)

Premises used: Iff.mpr, UniqueFactorizationMonoid.iff_exists_prime_mem_of_isPrime
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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
neg : ∀ (hXP : X ∉ P), ∃ x ∈ P, Prime x
⊢ ∃ x ∈ P, Prime x

Tactic:
by_cases hXP : X ∈ P

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

Tactic:
⟨X, hXP, X_prime⟩

Premises used: PowerSeries.X_prime, PowerSeries.X, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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

Tactic:
exact ⟨X, hXP, X_prime⟩
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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
neg : ∀ (w : R) (h : Eq (α := Submodule R R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff P) (R ∙ w)), ∃ x ∈ P, Prime x
⊢ ∃ x ∈ P, Prime x

Tactic:
obtain ⟨_, h⟩ := (IsPrincipalIdealRing.principal (P.map constantCoeff)).principal

Premises used: Submodule.IsPrincipal.principal
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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)
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
⊢ ∃ x ∈ P, Prime x

Tactic:
obtain ⟨_, rfl, _, h⟩ := exist_eq_span_eq_ncard_of_X_notMem hXP h.symm (finite_singleton _)

Premises used: PowerSeries.exist_eq_span_eq_ncard_of_X_notMem, Eq.symm, Set.finite_singleton, rfl
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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
w : R
w_1 : Set R⟦X⟧
h₁ : Ne (α := Ideal R⟦X⟧) (span w_1) ⊥
h₂ : IsPrime (span w_1)
hXP : X ∉ span w_1
h_1 : Eq (α := Submodule R R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff (span w_1)) (R ∙ w)
left : w_1.Finite
h : w_1.ncard = ncard (α := R) {w}
⊢ ∃ (a : R⟦X⟧), w_1 = {a}

Tactic:
simp only [ncard_singleton, ncard_eq_one] at h

Premises used: Set.ncard_eq_one, Set.ncard_singleton
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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
w : R
w_1 : Set R⟦X⟧
h₁ : Ne (α := Ideal R⟦X⟧) (span w_1) ⊥
h₂ : IsPrime (span w_1)
hXP : X ∉ span w_1
h_1 : Eq (α := Submodule R R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff (span w_1)) (R ∙ w)
left : w_1.Finite
h : ∃ (a : R⟦X⟧), w_1 = {a}
neg :
  ∀ (w_2 : R⟦X⟧) (h₁ : Ne (α := Ideal R⟦X⟧) (span {w_2}) ⊥) (h₂ : IsPrime (α := R⟦X⟧) (span {w_2}))
    (hXP : X ∉ span {w_2})
    (h : Eq (α := Submodule R R) (Ideal.map (R := R⟦X⟧) (F := R⟦X⟧ →+* R) constantCoeff (span {w_2})) (R ∙ w)),
    Set.Finite (α := R⟦X⟧) {w_2} → ∃ (x : R⟦X⟧), Membership.mem (γ := Ideal R⟦X⟧) (span {w_2}) x ∧ Prime x
⊢ ∃ (x : R⟦X⟧), Membership.mem (γ := Ideal R⟦X⟧) (span w_1) x ∧ Prime x

Tactic:
obtain ⟨_, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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
w : R
w_1 : R⟦X⟧
h₁ : Ne (α := Ideal R⟦X⟧) (span {w_1}) ⊥
h₂ : IsPrime (α := R⟦X⟧) (span {w_1})
hXP : X ∉ span {w_1}
h : Eq (α := Submodule R R) (Ideal.map (R := R⟦X⟧) (F := R⟦X⟧ →+* R) constantCoeff (span {w_1})) (R ∙ w)
left : Set.Finite (α := R⟦X⟧) {w_1}
⊢ ∃ (x : R⟦X⟧), Membership.mem (γ := Ideal R⟦X⟧) (span {w_1}) x ∧ Prime x

Tactic:
⟨_, mem_span_singleton_self _,
      (span_singleton_prime (span_singleton_eq_bot.not.1 h₁)).1 h₂⟩

Premises used: Ideal.span_singleton_eq_bot, Iff.not, And.intro, Exists.intro, Iff.mp, Ideal.span_singleton_prime, Ideal.mem_span_singleton_self
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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
w : R
w_1 : R⟦X⟧
h₁ : Ne (α := Ideal R⟦X⟧) (span {w_1}) ⊥
h₂ : IsPrime (α := R⟦X⟧) (span {w_1})
hXP : X ∉ span {w_1}
h : Eq (α := Submodule R R) (Ideal.map (R := R⟦X⟧) (F := R⟦X⟧ →+* R) constantCoeff (span {w_1})) (R ∙ w)
left : Set.Finite (α := R⟦X⟧) {w_1}
⊢ ∃ (x : R⟦X⟧), Membership.mem (γ := Ideal R⟦X⟧) (span {w_1}) x ∧ Prime x

Tactic:
exact ⟨_, mem_span_singleton_self _,
      (span_singleton_prime (span_singleton_eq_bot.not.1 h₁)).1 h₂⟩
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
R : Type u_1
inst : Ring R
n : ℕ
a : R
φ : R⟦X⟧
rw :
  (if Eq (α := Unit →₀ ℕ) (single () n) 0 then a
    else
      -a *
        ∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ (single () n),
          if x.2 < single () n then
            HMul.hMul (α := R) (β := R) ((MvPowerSeries.coeff x.1 : (a : MvPowerSeries Unit R) → R) φ : R)
              ((MvPowerSeries.coeff x.2 : (a : MvPowerSeries Unit R) → R) (MvPowerSeries.inv.aux a φ) : R)
          else 0) =
    if n = 0 then a
    else
      -a *
        ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
          if x.2 < n then
            HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) φ : R)
              ((coeff x.2 : (a : R⟦X⟧) → R) (MvPowerSeries.inv.aux a φ) : R)
          else 0
⊢ (coeff n : (a : R⟦X⟧) → R) (inv.aux a φ) =
    if n = 0 then a
    else
      -a *
        ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
          if x.2 < n then
            HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) φ : R)
              ((coeff x.2 : (a : R⟦X⟧) → R) (inv.aux a φ) : R)
          else 0

Tactic:
rw [coeff, inv.aux, MvPowerSeries.coeff_inv_aux]

Premises used: PowerSeries.inv.aux, PowerSeries.coeff, MvPowerSeries.coeff_inv_aux
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
R : Type u_1
inst : Ring R
n : ℕ
a : R
φ : R⟦X⟧
simp :
  (if n = 0 then a
    else
      -a *
        ∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ (single () n),
          if x.2 < single () n then
            HMul.hMul (α := R) (β := R) ((MvPowerSeries.coeff x.1 : (a : MvPowerSeries Unit R) → R) φ : R)
              ((MvPowerSeries.coeff x.2 : (a : MvPowerSeries Unit R) → R) (MvPowerSeries.inv.aux a φ) : R)
          else 0) =
    if n = 0 then a
    else
      -a *
        ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
          if x.2 < n then
            HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) φ : R)
              ((coeff x.2 : (a : R⟦X⟧) → R) (MvPowerSeries.inv.aux a φ) : R)
          else 0
⊢ (if Eq (α := Unit →₀ ℕ) (single () n) 0 then a
    else
      -a *
        ∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ (single () n),
          if x.2 < single () n then
            HMul.hMul (α := R) (β := R) ((MvPowerSeries.coeff x.1 : (a : MvPowerSeries Unit R) → R) φ : R)
              ((MvPowerSeries.coeff x.2 : (a : MvPowerSeries Unit R) → R) (MvPowerSeries.inv.aux a φ) : R)
          else 0) =
    if n = 0 then a
    else
      -a *
        ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
          if x.2 < n then
            HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) φ : R)
              ((coeff x.2 : (a : R⟦X⟧) → R) (MvPowerSeries.inv.aux a φ) : R)
          else 0

Tactic:
simp only [Finsupp.single_eq_zero]

Premises used: Finsupp.single_eq_zero
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
R : Type u_1
inst : Ring R
n : ℕ
a : R
φ : R⟦X⟧
pos : n = 0 → a = a
neg :
  ¬n = 0 →
    (-a *
        ∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ (single () n),
          if x.2 < single () n then
            HMul.hMul (α := R) (β := R) ((MvPowerSeries.coeff x.1 : (a : MvPowerSeries Unit R) → R) φ : R)
              ((MvPowerSeries.coeff x.2 : (a : MvPowerSeries Unit R) → R) (MvPowerSeries.inv.aux a φ) : R)
          else 0) =
      -a *
        ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
          if x.2 < n then
            HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) φ : R)
              ((coeff x.2 : (a : R⟦X⟧) → R) (MvPowerSeries.inv.aux a φ) : R)
          else 0
⊢ (if n = 0 then a
    else
      -a *
        ∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ (single () n),
          if x.2 < single () n then
            HMul.hMul (α := R) (β := R) ((MvPowerSeries.coeff x.1 : (a : MvPowerSeries Unit R) → R) φ : R)
              ((MvPowerSeries.coeff x.2 : (a : MvPowerSeries Unit R) → R) (MvPowerSeries.inv.aux a φ) : R)
          else 0) =
    if n = 0 then a
    else
      -a *
        ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
          if x.2 < n then
            HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) φ : R)
              ((coeff x.2 : (a : R⟦X⟧) → R) (MvPowerSeries.inv.aux a φ) : R)
          else 0

Tactic:
split_ifs
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
R : Type u_1
inst : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h : n = 0
⊢ a = a

Tactic:
rfl
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
R : Type u_1
inst : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h : ¬n = 0
neg :
  Eq.{u_1 + 1} (α := R)
    (∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ (single () n),
      if x.2 < single () n then
        HMul.hMul (α := R) (β := R) ((MvPowerSeries.coeff x.1 : (a : MvPowerSeries Unit R) → R) φ : R)
          ((MvPowerSeries.coeff x.2 : (a : MvPowerSeries Unit R) → R) (MvPowerSeries.inv.aux a φ) : R)
      else 0)
    (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
      if x.2 < n then
        HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) φ : R)
          ((coeff x.2 : (a : R⟦X⟧) → R) (MvPowerSeries.inv.aux a φ) : R)
      else 0)
⊢ (-a *
      ∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ (single () n),
        if x.2 < single () n then
          HMul.hMul (α := R) (β := R) ((MvPowerSeries.coeff x.1 : (a : MvPowerSeries Unit R) → R) φ : R)
            ((MvPowerSeries.coeff x.2 : (a : MvPowerSeries Unit R) → R) (MvPowerSeries.inv.aux a φ) : R)
        else 0) =
    -a *
      ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
        if x.2 < n then
          HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) φ : R)
            ((coeff x.2 : (a : R⟦X⟧) → R) (MvPowerSeries.inv.aux a φ) : R)
        else 0

Tactic:
congr 1
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
R : Type u_1
inst : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h : ¬n = 0
neg :
  Eq.{u_1 + 1} (α := R)
    (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
      if x.2 < n then
        HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) φ : R)
          ((coeff x.2 : (a : R⟦X⟧) → R) (MvPowerSeries.inv.aux a φ) : R)
      else 0)
    (∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ (single () n),
      if x.2 < single () n then
        HMul.hMul (α := R) (β := R) ((MvPowerSeries.coeff x.1 : (a : MvPowerSeries Unit R) → R) φ : R)
          ((MvPowerSeries.coeff x.2 : (a : MvPowerSeries Unit R) → R) (MvPowerSeries.inv.aux a φ) : R)
      else 0)
⊢ Eq.{u_1 + 1} (α := R)
    (∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ (single () n),
      if x.2 < single () n then
        HMul.hMul (α := R) (β := R) ((MvPowerSeries.coeff x.1 : (a : MvPowerSeries Unit R) → R) φ : R)
          ((MvPowerSeries.coeff x.2 : (a : MvPowerSeries Unit R) → R) (MvPowerSeries.inv.aux a φ) : R)
      else 0)
    (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
      if x.2 < n then
        HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) φ : R)
          ((coeff x.2 : (a : R⟦X⟧) → R) (MvPowerSeries.inv.aux a φ) : R)
      else 0)

Tactic:
symm
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
R : Type u_1
inst : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h : ¬n = 0
⊢ ∀ a ∈ @antidiagonal _ Nat.instAddMonoid _ n,
    Membership.mem (α := (Unit →₀ ℕ) × (Unit →₀ ℕ)) (γ := Finset ((Unit →₀ ℕ) × (Unit →₀ ℕ)))
      (@antidiagonal _ Finsupp.instAddMonoid _ (single () n))
      (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) a with
        | (a, b) => (single () a, single () b) :
        (Unit →₀ ℕ) × (Unit →₀ ℕ))

Tactic:
aesop
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
R : Type u_1
inst : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h : ¬n = 0
⊢ ∀ (a : (Unit →₀ ℕ) × (Unit →₀ ℕ)),
    Membership.mem (γ := Finset ((Unit →₀ ℕ) × (Unit →₀ ℕ))) (@antidiagonal _ Finsupp.instAddMonoid _ (single () n)) a →
      Membership.mem (α := ℕ × ℕ) (@antidiagonal _ Nat.instAddMonoid _ n)
        (match (motive := (Unit →₀ ℕ) × (Unit →₀ ℕ) → ℕ × ℕ) a with
          | (f, g) => ((f : (a : Unit) → ℕ) (), (g : (a : Unit) → ℕ) ()) :
          ℕ × ℕ)

Tactic:
aesop
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
R : Type u_1
inst : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h : ¬n = 0
⊢ ∀ a ∈ @antidiagonal _ Nat.instAddMonoid _ n,
    (match (motive := (Unit →₀ ℕ) × (Unit →₀ ℕ) → ℕ × ℕ)
        match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) a with
        | (a, b) => (single () a, single () b) with
      | (f, g) => ((f : (a : Unit) → ℕ) (), (g : (a : Unit) → ℕ) ())) =
      a

Tactic:
aesop