mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: case hs
σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝¹ : TendstoCofinite f
inst✝ : DecidableEq σ
x : τ →₀ ℕ
⊢ (↑(⋯.toFinset.sup fun y ↦ {y}.product (Finset.antidiagonal y))).Finite

pp: case ht
σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝¹ : TendstoCofinite f
inst✝ : DecidableEq σ
x : τ →₀ ℕ
⊢ {p | mapDomain f p.1 = x ∧ p.2 ∈ Finset.antidiagonal p.1} ⊆
    ↑(⋯.toFinset.sup fun y ↦ {y}.product (Finset.antidiagonal y))

Tactic:
·

Goal state after:
case hs
σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝¹ : TendstoCofinite f
inst✝ : DecidableEq σ
x : τ →₀ ℕ
⊢ (↑(⋯.toFinset.sup fun y ↦ {y}.product (Finset.antidiagonal y))).Finite
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: case ht
σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝¹ : TendstoCofinite f
inst✝ : DecidableEq σ
x : τ →₀ ℕ
⊢ {p | mapDomain f p.1 = x ∧ p.2 ∈ Finset.antidiagonal p.1} ⊆
    ↑(⋯.toFinset.sup fun y ↦ {y}.product (Finset.antidiagonal y))

Tactic:
·

Goal state after:
case ht
σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝¹ : TendstoCofinite f
inst✝ : DecidableEq σ
x : τ →₀ ℕ
⊢ {p | mapDomain f p.1 = x ∧ p.2 ∈ Finset.antidiagonal p.1} ⊆
    ↑(⋯.toFinset.sup fun y ↦ {y}.product (Finset.antidiagonal y))
Module: Mathlib.RingTheory.Noetherian.OfPrime

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I ↑(span {a})).FG
w✝¹ : ℕ
f : Fin w✝¹ → R
hf : span (Set.range f) = I ⊔ span {a}
w✝ : ℕ
i : Fin w✝ → R
hi : Submodule.span R (Set.range i) = Submodule.colon I ↑(span {a})
r p : Fin w✝¹ → R
p_mem_I : ∀ (k : Fin w✝¹), p k ∈ I
Hf : ∀ (k : Fin w✝¹), r k * a + p k = f k
⊢ span (Set.range p) ⊔ span (Set.range fun a_1 ↦ a • i a_1) ≤ I

pp: case refine_2
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I ↑(span {a})).FG
w✝¹ : ℕ
f : Fin w✝¹ → R
hf : span (Set.range f) = I ⊔ span {a}
w✝ : ℕ
i : Fin w✝ → R
hi : Submodule.span R (Set.range i) = Submodule.colon I ↑(span {a})
r p : Fin w✝¹ → R
p_mem_I : ∀ (k : Fin w✝¹), p k ∈ I
Hf : ∀ (k : Fin w✝¹), r k * a + p k = f k
y : R
hy : y ∈ I
⊢ y ∈ span (Set.range p) ⊔ span (Set.range fun a_1 ↦ a • i a_1)

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I ↑(span {a})).FG
w✝¹ : ℕ
f : Fin w✝¹ → R
hf : span (Set.range f) = I ⊔ span {a}
w✝ : ℕ
i : Fin w✝ → R
hi : Submodule.span R (Set.range i) = Submodule.colon I ↑(span {a})
r p : Fin w✝¹ → R
p_mem_I : ∀ (k : Fin w✝¹), p k ∈ I
Hf : ∀ (k : Fin w✝¹), r k * a + p k = f k
⊢ span (Set.range p) ⊔ span (Set.range fun a_1 ↦ a • i a_1) ≤ I
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: case hs
σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝¹ : TendstoCofinite f
inst✝ : DecidableEq τ
x : τ →₀ ℕ
⊢ (↑((Finset.antidiagonal x).sup fun q ↦ {q}.product (⋯.toFinset ×ˢ ⋯.toFinset))).Finite

pp: case ht
σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝¹ : TendstoCofinite f
inst✝ : DecidableEq τ
x : τ →₀ ℕ
⊢ {p | p.1 ∈ Finset.antidiagonal x ∧ p.2 ∈ ⋯.toFinset ×ˢ ⋯.toFinset} ⊆
    ↑((Finset.antidiagonal x).sup fun q ↦ {q}.product (⋯.toFinset ×ˢ ⋯.toFinset))

Tactic:
·

Goal state after:
case hs
σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝¹ : TendstoCofinite f
inst✝ : DecidableEq τ
x : τ →₀ ℕ
⊢ (↑((Finset.antidiagonal x).sup fun q ↦ {q}.product (⋯.toFinset ×ˢ ⋯.toFinset))).Finite
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: case ht
σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝¹ : TendstoCofinite f
inst✝ : DecidableEq τ
x : τ →₀ ℕ
⊢ {p | p.1 ∈ Finset.antidiagonal x ∧ p.2 ∈ ⋯.toFinset ×ˢ ⋯.toFinset} ⊆
    ↑((Finset.antidiagonal x).sup fun q ↦ {q}.product (⋯.toFinset ×ˢ ⋯.toFinset))

Tactic:
·

Goal state after:
case ht
σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝¹ : TendstoCofinite f
inst✝ : DecidableEq τ
x : τ →₀ ℕ
⊢ {p | p.1 ∈ Finset.antidiagonal x ∧ p.2 ∈ ⋯.toFinset ×ˢ ⋯.toFinset} ⊆
    ↑((Finset.antidiagonal x).sup fun q ↦ {q}.product (⋯.toFinset ×ˢ ⋯.toFinset))
Module: Mathlib.RingTheory.Noetherian.OfPrime

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I ↑(span {a})).FG
w✝¹ : ℕ
f : Fin w✝¹ → R
hf : span (Set.range f) = I ⊔ span {a}
w✝ : ℕ
i : Fin w✝ → R
hi : Submodule.span R (Set.range i) = Submodule.colon I ↑(span {a})
r p : Fin w✝¹ → R
p_mem_I : ∀ (k : Fin w✝¹), p k ∈ I
Hf : ∀ (k : Fin w✝¹), r k * a + p k = f k
y : R
hy : y ∈ I
⊢ y ∈ span (Set.range p) ⊔ span (Set.range fun a_1 ↦ a • i a_1)

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I ↑(span {a})).FG
w✝¹ : ℕ
f : Fin w✝¹ → R
hf : span (Set.range f) = I ⊔ span {a}
w✝ : ℕ
i : Fin w✝ → R
hi : Submodule.span R (Set.range i) = Submodule.colon I ↑(span {a})
r p : Fin w✝¹ → R
p_mem_I : ∀ (k : Fin w✝¹), p k ∈ I
Hf : ∀ (k : Fin w✝¹), r k * a + p k = f k
y : R
hy : y ∈ I
⊢ y ∈ span (Set.range p) ⊔ span (Set.range fun a_1 ↦ a • i a_1)
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: case h₁
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (Set.range fun gv ↦ (A.ρ gv.1) gv.2 - gv.2) ⊆ ↑(ModuleCat.Hom.hom (d₁₀ A)).range

pp: case h₂
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (ModuleCat.Hom.hom (d₁₀ A)).range ≤ Submodule.span k (Set.range fun gv ↦ (A.ρ gv.1) gv.2 - gv.2)

Tactic:
·

Goal state after:
case h₁
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (Set.range fun gv ↦ (A.ρ gv.1) gv.2 - gv.2) ⊆ ↑(ModuleCat.Hom.hom (d₁₀ A)).range
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: case h₂
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (ModuleCat.Hom.hom (d₁₀ A)).range ≤ Submodule.span k (Set.range fun gv ↦ (A.ρ gv.1) gv.2 - gv.2)

Tactic:
·

Goal state after:
case h₂
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (ModuleCat.Hom.hom (d₁₀ A)).range ≤ Submodule.span k (Set.range fun gv ↦ (A.ρ gv.1) gv.2 - gv.2)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky

Goal state before:
pp: case inl
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : 0 ∉ S
hC : ∅ ⊆ kaplanskySet S
hC₂ : IsChain (fun x1 x2 ↦ x1 ≤ x2) ∅
⊢ ∃ P ∈ kaplanskySet S, ∀ J ∈ ∅, J ≤ P

pp: case inr
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
C : Set (Ideal R)
hS : 0 ∉ S
hC : C ⊆ kaplanskySet S
hC₂ : IsChain (fun x1 x2 ↦ x1 ≤ x2) C
w✝ : Ideal R
hI : w✝ ∈ C
⊢ ∃ P ∈ kaplanskySet S, ∀ J ∈ C, J ≤ P

Tactic:
·

Goal state after:
case inl
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : 0 ∉ S
hC : ∅ ⊆ kaplanskySet S
hC₂ : IsChain (fun x1 x2 ↦ x1 ≤ x2) ∅
⊢ ∃ P ∈ kaplanskySet S, ∀ J ∈ ∅, J ≤ P
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky

Goal state before:
pp: case inr
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
C : Set (Ideal R)
hS : 0 ∉ S
hC : C ⊆ kaplanskySet S
hC₂ : IsChain (fun x1 x2 ↦ x1 ≤ x2) C
w✝ : Ideal R
hI : w✝ ∈ C
⊢ ∃ P ∈ kaplanskySet S, ∀ J ∈ C, J ≤ P

Tactic:
·

Goal state after:
case inr
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
C : Set (Ideal R)
hS : 0 ∉ S
hC : C ⊆ kaplanskySet S
hC₂ : IsChain (fun x1 x2 ↦ x1 ≤ x2) C
w✝ : Ideal R
hI : w✝ ∈ C
⊢ ∃ P ∈ kaplanskySet S, ∀ J ∈ C, J ≤ P
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: case mp
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
a : A
⊢ IsBoundary₀ G a → ∃ x, (x.sum fun g z ↦ g • z - z) = a

pp: case mpr
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
a : A
⊢ (∃ x, (x.sum fun g z ↦ g • z - z) = a) → IsBoundary₀ G a

Tactic:
·

Goal state after:
case mp
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
a : A
⊢ IsBoundary₀ G a → ∃ x, (x.sum fun g z ↦ g • z - z) = a
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: case mpr
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
a : A
⊢ (∃ x, (x.sum fun g z ↦ g • z - z) = a) → IsBoundary₀ G a

Tactic:
·

Goal state after:
case mpr
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
a : A
⊢ (∃ x, (x.sum fun g z ↦ g • z - z) = a) → IsBoundary₀ G a
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: case mp
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
x : G →₀ A
⊢ IsBoundary₁ x → ∃ y, (y.sum fun g a ↦ single g.2 a - single (g.1 * g.2) (g.1 • a) + single g.1 (g.1 • a)) = x

pp: case mpr
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
x : G →₀ A
⊢ (∃ y, (y.sum fun g a ↦ single g.2 a - single (g.1 * g.2) (g.1 • a) + single g.1 (g.1 • a)) = x) → IsBoundary₁ x

Tactic:
·

Goal state after:
case mp
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
x : G →₀ A
⊢ IsBoundary₁ x → ∃ y, (y.sum fun g a ↦ single g.2 a - single (g.1 * g.2) (g.1 • a) + single g.1 (g.1 • a)) = x
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: case mpr
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
x : G →₀ A
⊢ (∃ y, (y.sum fun g a ↦ single g.2 a - single (g.1 * g.2) (g.1 • a) + single g.1 (g.1 • a)) = x) → IsBoundary₁ x

Tactic:
·

Goal state after:
case mpr
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
x : G →₀ A
⊢ (∃ y, (y.sum fun g a ↦ single g.2 a - single (g.1 * g.2) (g.1 • a) + single g.1 (g.1 • a)) = x) → IsBoundary₁ x
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: case mp
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
x : G × G →₀ A
⊢ IsBoundary₂ x →
    ∃ y,
      (y.sum fun g a ↦
          single (g.2.1, g.2.2) a - single (g.1 * g.2.1, g.2.2) (g.1 • a) + single (g.1, g.2.1 * g.2.2) (g.1 • a) -
            single (g.1, g.2.1) (g.1 • a)) =
        x

pp: case mpr
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
x : G × G →₀ A
⊢ (∃ y,
      (y.sum fun g a ↦
          single (g.2.1, g.2.2) a - single (g.1 * g.2.1, g.2.2) (g.1 • a) + single (g.1, g.2.1 * g.2.2) (g.1 • a) -
            single (g.1, g.2.1) (g.1 • a)) =
        x) →
    IsBoundary₂ x

Tactic:
·

Goal state after:
case mp
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
x : G × G →₀ A
⊢ IsBoundary₂ x →
    ∃ y,
      (y.sum fun g a ↦
          single (g.2.1, g.2.2) a - single (g.1 * g.2.1, g.2.2) (g.1 • a) + single (g.1, g.2.1 * g.2.2) (g.1 • a) -
            single (g.1, g.2.1) (g.1 • a)) =
        x
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: case mpr
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
x : G × G →₀ A
⊢ (∃ y,
      (y.sum fun g a ↦
          single (g.2.1, g.2.2) a - single (g.1 * g.2.1, g.2.2) (g.1 • a) + single (g.1, g.2.1 * g.2.2) (g.1 • a) -
            single (g.1, g.2.1) (g.1 • a)) =
        x) →
    IsBoundary₂ x

Tactic:
·

Goal state after:
case mpr
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
x : G × G →₀ A
⊢ (∃ y,
      (y.sum fun g a ↦
          single (g.2.1, g.2.2) a - single (g.1 * g.2.1, g.2.2) (g.1 • a) + single (g.1, g.2.1 * g.2.2) (g.1 • a) -
            single (g.1, g.2.1) (g.1 • a)) =
        x) →
    IsBoundary₂ x
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: case refine_1
σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝¹ : TendstoCofinite f
R : Type u_6
inst✝ : CommRing R
p : MvPowerSeries σ R
n : τ →₀ ℕ
this : ∀ (d : σ →₀ ℕ), (coeff d) p * (coeff n) (d.prod fun s e ↦ X (f s) ^ e) ≠ 0 → mapDomain f d = n
⊢ Set.Finite.toFinset ⋯ ⊆ ⋯.toFinset

pp: case refine_2
σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝¹ : TendstoCofinite f
R : Type u_6
inst✝ : CommRing R
p : MvPowerSeries σ R
n : τ →₀ ℕ
this : ∀ (d : σ →₀ ℕ), (coeff d) p * (coeff n) (d.prod fun s e ↦ X (f s) ^ e) ≠ 0 → mapDomain f d = n
⊢ ∀ x ∈ ⋯.toFinset \ Set.Finite.toFinset ⋯, (coeff x) p = 0

pp: case refine_3
σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝¹ : TendstoCofinite f
R : Type u_6
inst✝ : CommRing R
p : MvPowerSeries σ R
n : τ →₀ ℕ
this : ∀ (d : σ →₀ ℕ), (coeff d) p * (coeff n) (d.prod fun s e ↦ X (f s) ^ e) ≠ 0 → mapDomain f d = n
x : σ →₀ ℕ
hx : x ∈ Set.Finite.toFinset ⋯
⊢ (coeff x) p • (coeff n) (x.prod fun s e ↦ (X ∘ f) s ^ e) = (coeff x) p

Tactic:
·

Goal state after:
case refine_1
σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝¹ : TendstoCofinite f
R : Type u_6
inst✝ : CommRing R
p : MvPowerSeries σ R
n : τ →₀ ℕ
this : ∀ (d : σ →₀ ℕ), (coeff d) p * (coeff n) (d.prod fun s e ↦ X (f s) ^ e) ≠ 0 → mapDomain f d = n
⊢ Set.Finite.toFinset ⋯ ⊆ ⋯.toFinset
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: case refine_2
σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝¹ : TendstoCofinite f
R : Type u_6
inst✝ : CommRing R
p : MvPowerSeries σ R
n : τ →₀ ℕ
this : ∀ (d : σ →₀ ℕ), (coeff d) p * (coeff n) (d.prod fun s e ↦ X (f s) ^ e) ≠ 0 → mapDomain f d = n
⊢ ∀ x ∈ ⋯.toFinset \ Set.Finite.toFinset ⋯, (coeff x) p = 0

pp: case refine_3
σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝¹ : TendstoCofinite f
R : Type u_6
inst✝ : CommRing R
p : MvPowerSeries σ R
n : τ →₀ ℕ
this : ∀ (d : σ →₀ ℕ), (coeff d) p * (coeff n) (d.prod fun s e ↦ X (f s) ^ e) ≠ 0 → mapDomain f d = n
x : σ →₀ ℕ
hx : x ∈ Set.Finite.toFinset ⋯
⊢ (coeff x) p • (coeff n) (x.prod fun s e ↦ (X ∘ f) s ^ e) = (coeff x) p

Tactic:
·

Goal state after:
case refine_2
σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝¹ : TendstoCofinite f
R : Type u_6
inst✝ : CommRing R
p : MvPowerSeries σ R
n : τ →₀ ℕ
this : ∀ (d : σ →₀ ℕ), (coeff d) p * (coeff n) (d.prod fun s e ↦ X (f s) ^ e) ≠ 0 → mapDomain f d = n
⊢ ∀ x ∈ ⋯.toFinset \ Set.Finite.toFinset ⋯, (coeff x) p = 0
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: case refine_3
σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝¹ : TendstoCofinite f
R : Type u_6
inst✝ : CommRing R
p : MvPowerSeries σ R
n : τ →₀ ℕ
this : ∀ (d : σ →₀ ℕ), (coeff d) p * (coeff n) (d.prod fun s e ↦ X (f s) ^ e) ≠ 0 → mapDomain f d = n
x : σ →₀ ℕ
hx : x ∈ Set.Finite.toFinset ⋯
⊢ (coeff x) p • (coeff n) (x.prod fun s e ↦ (X ∘ f) s ^ e) = (coeff x) p

Tactic:
·

Goal state after:
case refine_3
σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝¹ : TendstoCofinite f
R : Type u_6
inst✝ : CommRing R
p : MvPowerSeries σ R
n : τ →₀ ℕ
this : ∀ (d : σ →₀ ℕ), (coeff d) p * (coeff n) (d.prod fun s e ↦ X (f s) ^ e) ≠ 0 → mapDomain f d = n
x : σ →₀ ℕ
hx : x ∈ Set.Finite.toFinset ⋯
⊢ (coeff x) p • (coeff n) (x.prod fun s e ↦ (X ∘ f) s ^ e) = (coeff x) p
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky

Goal state before:
pp: case mem.inl
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
a x b : R
hsubset : closure {r | Prime r} ≤ closure {r | IsUnit r ∨ Prime r}
z : R
h : IsUnit z
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod z

pp: case mem.inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
a x b : R
hsubset : closure {r | Prime r} ≤ closure {r | IsUnit r ∨ Prime r}
z : R
h : Prime z
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod z

Tactic:
·

Goal state after:
case mem.inl
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
a x b : R
hsubset : closure {r | Prime r} ≤ closure {r | IsUnit r ∨ Prime r}
z : R
h : IsUnit z
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod z
Module: Mathlib.RingTheory.PowerSeries.Ideal

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
I : Ideal R⟦X⟧
hI : X ∈ I
hfg : ¬I.FG
⊢ spanFinrank I ≤ spanFinrank (Ideal.map constantCoeff I) + 1

pp: case pos
R : Type u_1
inst✝ : CommRing R
I : Ideal R⟦X⟧
hI : X ∈ I
hfg : I.FG
⊢ spanFinrank I ≤ spanFinrank (Ideal.map constantCoeff I) + 1

Tactic:
·

Goal state after:
case neg
R : Type u_1
inst✝ : CommRing R
I : Ideal R⟦X⟧
hI : X ∈ I
hfg : ¬I.FG
⊢ spanFinrank I ≤ spanFinrank (Ideal.map constantCoeff I) + 1
Module: Mathlib.RingTheory.PowerSeries.Ideal

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R⟦X⟧
hI : X ∈ I
hfg : I.FG
this : RingHomSurjective constantCoeff
⊢ (Ideal.map constantCoeff I).FG

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

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky

Goal state before:
pp: case mem.inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
a x b : R
hsubset : closure {r | Prime r} ≤ closure {r | IsUnit r ∨ Prime r}
z : R
h : Prime z
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod z

Tactic:
·

Goal state after:
case mem.inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
a x b : R
hsubset : closure {r | Prime r} ≤ closure {r | IsUnit r ∨ Prime r}
z : R
h : Prime z
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod z
Module: Mathlib.RingTheory.PowerSeries.Ideal

Goal state before:
pp: case pos.refine_1
R : Type u_1
inst✝ : CommRing R
I : Ideal R⟦X⟧
hI : X ∈ I
hfg : (Ideal.map constantCoeff I).FG
⊢ (insert X (⇑C '' generators (Ideal.map constantCoeff I))).Finite

pp: case pos.refine_2
R : Type u_1
inst✝ : CommRing R
I : Ideal R⟦X⟧
hI : X ∈ I
hfg : (Ideal.map constantCoeff I).FG
⊢ (⇑C '' generators (Ideal.map constantCoeff I)).ncard + 1 ≤ spanFinrank (Ideal.map constantCoeff I) + 1

Tactic:
·

Goal state after:
case pos.refine_1
R : Type u_1
inst✝ : CommRing R
I : Ideal R⟦X⟧
hI : X ∈ I
hfg : (Ideal.map constantCoeff I).FG
⊢ (insert X (⇑C '' generators (Ideal.map constantCoeff I))).Finite
Module: Mathlib.RingTheory.PowerSeries.Ideal

Goal state before:
pp: case pos.refine_2
R : Type u_1
inst✝ : CommRing R
I : Ideal R⟦X⟧
hI : X ∈ I
hfg : (Ideal.map constantCoeff I).FG
⊢ (⇑C '' generators (Ideal.map constantCoeff I)).ncard + 1 ≤ spanFinrank (Ideal.map constantCoeff I) + 1

Tactic:
·

Goal state after:
case pos.refine_2
R : Type u_1
inst✝ : CommRing R
I : Ideal R⟦X⟧
hI : X ∈ I
hfg : (Ideal.map constantCoeff I).FG
⊢ (⇑C '' generators (Ideal.map constantCoeff I)).ncard + 1 ≤ spanFinrank (Ideal.map constantCoeff I) + 1
Module: Mathlib.RingTheory.PowerSeries.Ideal

Goal state before:
pp: case refine_1
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hI : X ∉ I
S : Set R
hSI : span S = Ideal.map constantCoeff I
hS : S.Finite
this : SurjOn (⇑constantCoeff) (↑I) S
T : Set R⟦X⟧
hTI : T ⊆ ↑I
hinj : InjOn (⇑constantCoeff) T
hT : ⇑constantCoeff '' T = S
f : R⟦X⟧
hf : constantCoeff f ∈ span S
s : R
hs : s ∈ S
⊢ ∃ x ∈ span T, constantCoeff x = s

pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hI : X ∉ I
S : Set R
hSI : span S = Ideal.map constantCoeff I
hS : S.Finite
this : SurjOn (⇑constantCoeff) (↑I) S
T : Set R⟦X⟧
hTI : T ⊆ ↑I
hinj : InjOn (⇑constantCoeff) T
hT : ⇑constantCoeff '' T = S
f : R⟦X⟧
hf : constantCoeff f ∈ span S
⊢ ∀ (x y : R),
    x ∈ Submodule.span R S →
      y ∈ Submodule.span R S →
        (∃ x_1 ∈ span T, constantCoeff x_1 = x) →
          (∃ x ∈ span T, constantCoeff x = y) → ∃ x_1 ∈ span T, constantCoeff x_1 = x + y

pp: case refine_3
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hI : X ∉ I
S : Set R
hSI : span S = Ideal.map constantCoeff I
hS : S.Finite
this : SurjOn (⇑constantCoeff) (↑I) S
T : Set R⟦X⟧
hTI : T ⊆ ↑I
hinj : InjOn (⇑constantCoeff) T
hT : ⇑constantCoeff '' T = S
f : R⟦X⟧
hf : constantCoeff f ∈ span S
⊢ ∀ (a x : R),
    x ∈ Submodule.span R S → (∃ x_1 ∈ span T, constantCoeff x_1 = x) → ∃ x_1 ∈ span T, constantCoeff x_1 = a • x

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hI : X ∉ I
S : Set R
hSI : span S = Ideal.map constantCoeff I
hS : S.Finite
this : SurjOn (⇑constantCoeff) (↑I) S
T : Set R⟦X⟧
hTI : T ⊆ ↑I
hinj : InjOn (⇑constantCoeff) T
hT : ⇑constantCoeff '' T = S
f : R⟦X⟧
hf : constantCoeff f ∈ span S
s : R
hs : s ∈ S
⊢ ∃ x ∈ span T, constantCoeff x = s
Module: Mathlib.RingTheory.PowerSeries.Ideal

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hI : X ∉ I
S : Set R
hSI : span S = Ideal.map constantCoeff I
hS : S.Finite
this : SurjOn (⇑constantCoeff) (↑I) S
T : Set R⟦X⟧
hTI : T ⊆ ↑I
hinj : InjOn (⇑constantCoeff) T
hT : ⇑constantCoeff '' T = S
f : R⟦X⟧
hf : constantCoeff f ∈ span S
⊢ ∀ (x y : R),
    x ∈ Submodule.span R S →
      y ∈ Submodule.span R S →
        (∃ x_1 ∈ span T, constantCoeff x_1 = x) →
          (∃ x ∈ span T, constantCoeff x = y) → ∃ x_1 ∈ span T, constantCoeff x_1 = x + y

pp: case refine_3
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hI : X ∉ I
S : Set R
hSI : span S = Ideal.map constantCoeff I
hS : S.Finite
this : SurjOn (⇑constantCoeff) (↑I) S
T : Set R⟦X⟧
hTI : T ⊆ ↑I
hinj : InjOn (⇑constantCoeff) T
hT : ⇑constantCoeff '' T = S
f : R⟦X⟧
hf : constantCoeff f ∈ span S
⊢ ∀ (a x : R),
    x ∈ Submodule.span R S → (∃ x_1 ∈ span T, constantCoeff x_1 = x) → ∃ x_1 ∈ span T, constantCoeff x_1 = a • x

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hI : X ∉ I
S : Set R
hSI : span S = Ideal.map constantCoeff I
hS : S.Finite
this : SurjOn (⇑constantCoeff) (↑I) S
T : Set R⟦X⟧
hTI : T ⊆ ↑I
hinj : InjOn (⇑constantCoeff) T
hT : ⇑constantCoeff '' T = S
f : R⟦X⟧
hf : constantCoeff f ∈ span S
⊢ ∀ (x y : R),
    x ∈ Submodule.span R S →
      y ∈ Submodule.span R S →
        (∃ x_1 ∈ span T, constantCoeff x_1 = x) →
          (∃ x ∈ span T, constantCoeff x = y) → ∃ x_1 ∈ span T, constantCoeff x_1 = x + y
Module: Mathlib.RingTheory.PowerSeries.Ideal

Goal state before:
pp: case refine_3
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hI : X ∉ I
S : Set R
hSI : span S = Ideal.map constantCoeff I
hS : S.Finite
this : SurjOn (⇑constantCoeff) (↑I) S
T : Set R⟦X⟧
hTI : T ⊆ ↑I
hinj : InjOn (⇑constantCoeff) T
hT : ⇑constantCoeff '' T = S
f : R⟦X⟧
hf : constantCoeff f ∈ span S
⊢ ∀ (a x : R),
    x ∈ Submodule.span R S → (∃ x_1 ∈ span T, constantCoeff x_1 = x) → ∃ x_1 ∈ span T, constantCoeff x_1 = a • x

Tactic:
·

Goal state after:
case refine_3
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hI : X ∉ I
S : Set R
hSI : span S = Ideal.map constantCoeff I
hS : S.Finite
this : SurjOn (⇑constantCoeff) (↑I) S
T : Set R⟦X⟧
hTI : T ⊆ ↑I
hinj : InjOn (⇑constantCoeff) T
hT : ⇑constantCoeff '' T = S
f : R⟦X⟧
hf : constantCoeff f ∈ span S
⊢ ∀ (a x : R),
    x ∈ Submodule.span R S → (∃ x_1 ∈ span T, constantCoeff x_1 = x) → ∃ x_1 ∈ span T, constantCoeff x_1 = a • x
Module: Mathlib.RingTheory.PowerSeries.Ideal

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hI : X ∉ I
hfg : I.FG
⊢ spanFinrank (Ideal.map constantCoeff I) ≤ spanFinrank I

pp: case refine_1
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hI : X ∉ I
hfg : I.FG
⊢ spanFinrank I ≤ spanFinrank (Ideal.map constantCoeff I)

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hI : X ∉ I
hfg : I.FG
⊢ spanFinrank (Ideal.map constantCoeff I) ≤ spanFinrank I
Module: Mathlib.RingTheory.PowerSeries.Ideal

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R⟦X⟧
inst✝ : P.IsPrime
hfg : ¬P.FG
⊢ spanFinrank P ≤ spanFinrank (Ideal.map constantCoeff P) + 1

pp: case pos
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R⟦X⟧
inst✝ : P.IsPrime
hfg : P.FG
⊢ spanFinrank P ≤ spanFinrank (Ideal.map constantCoeff P) + 1

Tactic:
·

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R⟦X⟧
inst✝ : P.IsPrime
hfg : ¬P.FG
⊢ spanFinrank P ≤ spanFinrank (Ideal.map constantCoeff P) + 1