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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝¹ : TendstoCofinite f
R : Type u_6
inst✝ : CommRing R
d : τ →₀ ℕ
x : σ
⊢ x ∉ ⋃ i ∈ ↑d.support, f ⁻¹' {i} → x ∉ {s | (coeff d) ((X ∘ f) s) ≠ 0}

Tactic:
;

Goal state after:
σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝¹ : TendstoCofinite f
R : Type u_6
inst✝ : CommRing R
d : τ →₀ ℕ
x : σ
⊢ x ∉ ⋃ i ∈ ↑d.support, f ⁻¹' {i} → x ∉ {s | (coeff d) ((X ∘ f) s) ≠ 0}
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝¹ : TendstoCofinite f
R : Type u_6
inst✝ : CommRing R
d : τ →₀ ℕ
x : σ
a✝¹ : x ∉ ⋃ i ∈ ↑d.support, f ⁻¹' {i}
a✝ : x ∈ {s | (coeff d) ((X ∘ f) s) ≠ 0}
⊢ False

Tactic:
;

Goal state after:
σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝¹ : TendstoCofinite f
R : Type u_6
inst✝ : CommRing R
d : τ →₀ ℕ
x : σ
a✝¹ : x ∉ ⋃ i ∈ ↑d.support, f ⁻¹' {i}
a✝ : x ∈ {s | (coeff d) ((X ∘ f) s) ≠ 0}
⊢ False
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑A
⊢ (ConcreteCategory.hom (chainsIso₀ A).inv) x =
    (ConcreteCategory.hom (iCycles A 0)) ((ConcreteCategory.hom (cyclesIso₀ A).inv) x)

Tactic:
;

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑A
⊢ (ConcreteCategory.hom (chainsIso₀ A).inv) x =
    (ConcreteCategory.hom (iCycles A 0)) ((ConcreteCategory.hom (cyclesIso₀ A).inv) x)
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cycles₁ A)
⊢ (ModuleCat.Hom.hom (d₁₀ A ≫ (chainsIso₀ A).inv)) ↑x = 0

Tactic:
;

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cycles₁ A)
⊢ (ModuleCat.Hom.hom (d₁₀ A ≫ (chainsIso₀ A).inv)) ↑x = 0
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

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hXI : X ∉ I
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' : Ideal.map constantCoeff I = span (Set.range (⇑constantCoeff ∘ F))
T : R⟦X⟧ → Fin n✝ → R
hT : ∀ g ∈ I, ∑ i, T g i * constantCoeff (F i) = constantCoeff g
g : R⟦X⟧
hg : g ∈ I
G : ℕ → R⟦X⟧ := fun t ↦ Nat.rec g (fun x G' ↦ mk fun p ↦ (coeff (p + 1)) G' - ∑ i, T G' i * (coeff (p + 1)) (F i)) t
hG : ∀ (n : ℕ), G n ∈ I
hG' : ∀ (n : ℕ), G n - ∑ i, C (T (G n) i) * F i = X * G (n + 1)
H : Fin n✝ → R⟦X⟧ := fun i ↦ mk fun n ↦ T (G n) i
h₁ : ∀ (n : ℕ), g - ∑ i, ↑((trunc n) (H i)) * F i = X ^ n * G n
n : ℕ
⊢ (coeff n) g = (coeff n) (∑ i, H i * F i)

Tactic:
;

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hXI : X ∉ I
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' : Ideal.map constantCoeff I = span (Set.range (⇑constantCoeff ∘ F))
T : R⟦X⟧ → Fin n✝ → R
hT : ∀ g ∈ I, ∑ i, T g i * constantCoeff (F i) = constantCoeff g
g : R⟦X⟧
hg : g ∈ I
G : ℕ → R⟦X⟧ := fun t ↦ Nat.rec g (fun x G' ↦ mk fun p ↦ (coeff (p + 1)) G' - ∑ i, T G' i * (coeff (p + 1)) (F i)) t
hG : ∀ (n : ℕ), G n ∈ I
hG' : ∀ (n : ℕ), G n - ∑ i, C (T (G n) i) * F i = X * G (n + 1)
H : Fin n✝ → R⟦X⟧ := fun i ↦ mk fun n ↦ T (G n) i
h₁ : ∀ (n : ℕ), g - ∑ i, ↑((trunc n) (H i)) * F i = X ^ n * G n
n : ℕ
⊢ (coeff n) g = (coeff n) (∑ i, H i * F i)
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
g✝ : Fin 1 → G
x✝ : ↑(ModuleCat.of k ↑A)
⊢ ((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle g✝) ≫ (inhomogeneousChains A).d 1 0)) x✝) default =
    ((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle g✝) ≫ 0)) x✝) default

Tactic:
;

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
g✝ : Fin 1 → G
x✝ : ↑(ModuleCat.of k ↑A)
⊢ ((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle g✝) ≫ (inhomogeneousChains A).d 1 0)) x✝) default =
    ((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle g✝) ≫ 0)) x✝) default
Module: Mathlib.RingTheory.PowerSeries.Ideal

Goal state before:
pp: 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
⊢ SurjOn (⇑constantCoeff) (↑I) S

Tactic:
intro r

Goal state after:
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
r : R
⊢ r ∈ S → r ∈ ⇑constantCoeff '' ↑I
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:
· intro r₁ r₂ hr₁ hr₂ ⟨s₁, hs₁mem, hs₁⟩ ⟨s₂, hs₂mem, hs₂⟩
    exact ⟨s₁ + s₂, Ideal.add_mem _ hs₁mem hs₂mem, by simp [hs₁, hs₂]⟩

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

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)
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

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
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ∀ (a : R) (i : ℕ), ∃ j, a • I ^ j ≤ I ^ i

Tactic:
intro r

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
r : R
⊢ ∀ (i : ℕ), ∃ j, r • I ^ j ≤ I ^ i
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsEmpty σ
x✝ : MvPowerSeries σ R
x : σ →₀ ℕ
⊢ (coeff x) (C ((↑↑constantCoeff).toFun x✝)) = (coeff x) x✝

Tactic:
;

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsEmpty σ
x✝ : MvPowerSeries σ R
x : σ →₀ ℕ
⊢ (coeff x) (C ((↑↑constantCoeff).toFun x✝)) = (coeff x) x✝
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : Option σ →₀ ℕ
r : R
n : ℕ
y : σ →₀ ℕ
h1 : ¬optionElim n y = x
h3 : n = x none
h : y = x.some
⊢ optionElim n y = x

Tactic:
;

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : Option σ →₀ ℕ
r : R
n : ℕ
y : σ →₀ ℕ
h1 : ¬optionElim n y = x
h3 : n = x none
h : y = x.some
⊢ optionElim n y = x
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: case refine_1
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
k : ℕ
x : σ →₀ ℕ
a✝ : (Option σ →₀ ℕ) × (Option σ →₀ ℕ)
ha✝ : a✝ ∈ antidiagonal (optionElim k x)
⊢ ⟨(a✝.1 none, a✝.2 none), (a✝.1.some, a✝.2.some)⟩ ∈ (antidiagonal k).sigma fun a ↦ antidiagonal x

Tactic:
;

Goal state after:
case refine_1
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
k : ℕ
x : σ →₀ ℕ
a✝ : (Option σ →₀ ℕ) × (Option σ →₀ ℕ)
ha✝ : a✝ ∈ antidiagonal (optionElim k x)
⊢ ⟨(a✝.1 none, a✝.2 none), (a✝.1.some, a✝.2.some)⟩ ∈ (antidiagonal k).sigma fun a ↦ antidiagonal x
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: case refine_2
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
k : ℕ
x : σ →₀ ℕ
a₁✝ : (Option σ →₀ ℕ) × (Option σ →₀ ℕ)
ha₁✝ : a₁✝ ∈ antidiagonal (optionElim k x)
a₂✝ : (Option σ →₀ ℕ) × (Option σ →₀ ℕ)
ha₂✝ : a₂✝ ∈ antidiagonal (optionElim k x)
a✝ : ⟨(a₁✝.1 none, a₁✝.2 none), (a₁✝.1.some, a₁✝.2.some)⟩ = ⟨(a₂✝.1 none, a₂✝.2 none), (a₂✝.1.some, a₂✝.2.some)⟩
⊢ a₁✝ = a₂✝

Tactic:
;

Goal state after:
case refine_2
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
k : ℕ
x : σ →₀ ℕ
a₁✝ : (Option σ →₀ ℕ) × (Option σ →₀ ℕ)
ha₁✝ : a₁✝ ∈ antidiagonal (optionElim k x)
a₂✝ : (Option σ →₀ ℕ) × (Option σ →₀ ℕ)
ha₂✝ : a₂✝ ∈ antidiagonal (optionElim k x)
a✝ : ⟨(a₁✝.1 none, a₁✝.2 none), (a₁✝.1.some, a₁✝.2.some)⟩ = ⟨(a₂✝.1 none, a₂✝.2 none), (a₂✝.1.some, a₂✝.2.some)⟩
⊢ a₁✝ = a₂✝
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: case h
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
k : ℕ
x : σ →₀ ℕ
m n : ℕ
u v : σ →₀ ℕ
h : ⟨(m, n), (u, v)⟩ ∈ (antidiagonal k).sigma fun a ↦ antidiagonal x
t : Option σ
⊢ (optionElim m u + optionElim n v) t = (optionElim k x) t

Tactic:
;

Goal state after:
case h
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
k : ℕ
x : σ →₀ ℕ
m n : ℕ
u v : σ →₀ ℕ
h : ⟨(m, n), (u, v)⟩ ∈ (antidiagonal k).sigma fun a ↦ antidiagonal x
t : Option σ
⊢ (optionElim m u + optionElim n v) t = (optionElim k x) t
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: case refine_4
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
k : ℕ
x : σ →₀ ℕ
a✝ : (Option σ →₀ ℕ) × (Option σ →₀ ℕ)
ha✝ : a✝ ∈ antidiagonal (optionElim k x)
⊢ (coeff a✝.1) p * (coeff a✝.2) q =
    (coeff
          (optionElim ⟨(a✝.1 none, a✝.2 none), (a✝.1.some, a✝.2.some)⟩.fst.1
            ⟨(a✝.1 none, a✝.2 none), (a✝.1.some, a✝.2.some)⟩.snd.1))
        p *
      (coeff
          (optionElim ⟨(a✝.1 none, a✝.2 none), (a✝.1.some, a✝.2.some)⟩.fst.2
            ⟨(a✝.1 none, a✝.2 none), (a✝.1.some, a✝.2.some)⟩.snd.2))
        q

Tactic:
;

Goal state after:
case refine_4
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
k : ℕ
x : σ →₀ ℕ
a✝ : (Option σ →₀ ℕ) × (Option σ →₀ ℕ)
ha✝ : a✝ ∈ antidiagonal (optionElim k x)
⊢ (coeff a✝.1) p * (coeff a✝.2) q =
    (coeff
          (optionElim ⟨(a✝.1 none, a✝.2 none), (a✝.1.some, a✝.2.some)⟩.fst.1
            ⟨(a✝.1 none, a✝.2 none), (a✝.1.some, a✝.2.some)⟩.snd.1))
        p *
      (coeff
          (optionElim ⟨(a✝.1 none, a✝.2 none), (a✝.1.some, a✝.2.some)⟩.fst.2
            ⟨(a✝.1 none, a✝.2 none), (a✝.1.some, a✝.2.some)⟩.snd.2))
        q
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x✝ : MvPowerSeries (Option σ) R
n✝ : Option σ →₀ ℕ
⊢ (coeff n✝) (optionInvFunLeft σ R (optionFunLeft σ R x✝)) = (coeff n✝) x✝

Tactic:
;

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x✝ : MvPowerSeries (Option σ) R
n✝ : Option σ →₀ ℕ
⊢ (coeff n✝) (optionInvFunLeft σ R (optionFunLeft σ R x✝)) = (coeff n✝) x✝
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x✝ : PowerSeries (MvPowerSeries σ R)
n✝¹ : ℕ
n✝ : σ →₀ ℕ
⊢ (coeff n✝) ((PowerSeries.coeff n✝¹) (optionFunLeft σ R (optionInvFunLeft σ R x✝))) =
    (coeff n✝) ((PowerSeries.coeff n✝¹) x✝)

Tactic:
;

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x✝ : PowerSeries (MvPowerSeries σ R)
n✝¹ : ℕ
n✝ : σ →₀ ℕ
⊢ (coeff n✝) ((PowerSeries.coeff n✝¹) (optionFunLeft σ R (optionInvFunLeft σ R x✝))) =
    (coeff n✝) ((PowerSeries.coeff n✝¹) x✝)
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x✝¹ x✝ : MvPowerSeries (Option σ) R
n✝¹ : ℕ
n✝ : σ →₀ ℕ
⊢ (coeff n✝) ((PowerSeries.coeff n✝¹) (optionFunLeft σ R (x✝¹ + x✝))) =
    (coeff n✝) ((PowerSeries.coeff n✝¹) (optionFunLeft σ R x✝¹ + optionFunLeft σ R x✝))

Tactic:
;

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x✝¹ x✝ : MvPowerSeries (Option σ) R
n✝¹ : ℕ
n✝ : σ →₀ ℕ
⊢ (coeff n✝) ((PowerSeries.coeff n✝¹) (optionFunLeft σ R (x✝¹ + x✝))) =
    (coeff n✝) ((PowerSeries.coeff n✝¹) (optionFunLeft σ R x✝¹ + optionFunLeft σ R x✝))
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
a : Option σ
⊢ (optionElim 0 (single i 1)) a = (single (Option.some i) 1) a

Tactic:
;

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
a : Option σ
⊢ (optionElim 0 (single i 1)) a = (single (Option.some i) 1) a
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: M : Type u_3
inst✝ : AddCommMonoid M
n : ℕ
i : M
x : Fin n →₀ M
a : Option (Fin n)
⊢ (embDomain (finSuccEquiv n).toEmbedding (Finsupp.cons i x)) a = (optionElim i x) a

Tactic:
;

Goal state after:
M : Type u_3
inst✝ : AddCommMonoid M
n : ℕ
i : M
x : Fin n →₀ M
a : Option (Fin n)
⊢ (embDomain (finSuccEquiv n).toEmbedding (Finsupp.cons i x)) a = (optionElim i x) a
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
n k : ℕ
x : Fin n →₀ ℕ
⊢ (if Finsupp.cons k x = single 0 1 then 1 else 0) = (coeff x) (if k = 1 then 1 else 0)

Tactic:
cons_eq_single_zero_iff

Goal state after:
R : Type u_2
inst✝ : CommSemiring R
n k : ℕ
x : Fin n →₀ ℕ
⊢ (if x = 0 ∧ k = 1 then 1 else 0) = (coeff x) (if k = 1 then 1 else 0)
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
n : ℕ
x✝ : R
⊢ ((finSuccEquiv R n).symm.toRingEquiv.toRingHom.comp (PowerSeries.C.comp C)) x✝ = C x✝

Tactic:
;

Goal state after:
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
x✝ : R
⊢ ((finSuccEquiv R n).symm.toRingEquiv.toRingHom.comp (PowerSeries.C.comp C)) x✝ = C x✝
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ ψ : A ⟶ res f B
hφψ : (Hom.hom φ).toLinearMap = (Hom.hom ψ).toLinearMap
⊢ chainsMap f φ = chainsMap f ψ

Tactic:
;

Goal state after:
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ ψ : A ⟶ res f B
hφψ : (Hom.hom φ).toLinearMap = (Hom.hom ψ).toLinearMap
⊢ chainsMap f φ = chainsMap f ψ
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ ψ : A ⟶ res f B
hφψ : (Hom.hom φ).toLinearMap = (Hom.hom ψ).toLinearMap
⊢ φ = ψ

Tactic:
;

Goal state after:
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ ψ : A ⟶ res f B
hφψ : (Hom.hom φ).toLinearMap = (Hom.hom ψ).toLinearMap
⊢ φ = ψ
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ ψ : A ⟶ res f B
hφψ : (Hom.hom φ).toLinearMap = (Hom.hom ψ).toLinearMap
x✝ : ↑A
⊢ (Hom.hom φ).toLinearMap x✝ = (Hom.hom ψ).toLinearMap x✝

Tactic:
;

Goal state after:
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ ψ : A ⟶ res f B
hφψ : (Hom.hom φ).toLinearMap = (Hom.hom ψ).toLinearMap
x✝ : ↑A
⊢ (Hom.hom φ).toLinearMap x✝ = (Hom.hom ψ).toLinearMap x✝
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k G
B : Rep k H
f : G →* H
i✝ : ℕ
g✝ : Fin i✝ → G
x✝ : ↑(ModuleCat.of k ↑A)
a✝ : Fin i✝ → H
⊢ ((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle g✝) ≫ (chainsMap f 0).f i✝)) x✝) a✝ =
    ((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle g✝) ≫ HomologicalComplex.Hom.f 0 i✝)) x✝) a✝

Tactic:
;

Goal state after:
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k G
B : Rep k H
f : G →* H
i✝ : ℕ
g✝ : Fin i✝ → G
x✝ : ↑(ModuleCat.of k ↑A)
a✝ : Fin i✝ → H
⊢ ((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle g✝) ≫ (chainsMap f 0).f i✝)) x✝) a✝ =
    ((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle g✝) ≫ HomologicalComplex.Hom.f 0 i✝)) x✝) a✝
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
n : ℕ
ψ : A ⟶ res f B
hφψ : (Hom.hom φ).toLinearMap = (Hom.hom ψ).toLinearMap
⊢ map f φ n = map f ψ n

Tactic:
;

Goal state after:
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
n : ℕ
ψ : A ⟶ res f B
hφψ : (Hom.hom φ).toLinearMap = (Hom.hom ψ).toLinearMap
⊢ map f φ n = map f ψ n
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
n : ℕ
ψ : A ⟶ res f B
hφψ : (Hom.hom φ).toLinearMap = (Hom.hom ψ).toLinearMap
⊢ φ = ψ

Tactic:
;

Goal state after:
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
n : ℕ
ψ : A ⟶ res f B
hφψ : (Hom.hom φ).toLinearMap = (Hom.hom ψ).toLinearMap
⊢ φ = ψ
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
n : ℕ
ψ : A ⟶ res f B
hφψ : (Hom.hom φ).toLinearMap = (Hom.hom ψ).toLinearMap
x✝ : ↑A
⊢ (Hom.hom φ).toLinearMap x✝ = (Hom.hom ψ).toLinearMap x✝

Tactic:
;

Goal state after:
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
n : ℕ
ψ : A ⟶ res f B
hφψ : (Hom.hom φ).toLinearMap = (Hom.hom ψ).toLinearMap
x✝ : ↑A
⊢ (Hom.hom φ).toLinearMap x✝ = (Hom.hom ψ).toLinearMap x✝
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
p : MvPolynomial σ R
⊢ (AdicCompletion.of (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)) p = (toAdicCompletion σ R) ↑p

Tactic:
;

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
p : MvPolynomial σ R
⊢ (AdicCompletion.of (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)) p = (toAdicCompletion σ R) ↑p
Module: Mathlib.RingTheory.AdicCompletion.LocalRing

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
comapeq :
  comap (algebraMap R (AdicCompletion (maximalIdeal R) R)) (maximalIdeal (AdicCompletion (maximalIdeal R) R)) =
    maximalIdeal R
f : (maximalIdeal R).Cotangent →ₗ[R] (maximalIdeal (AdicCompletion (maximalIdeal R) R)).Cotangent :=
  (maximalIdeal R).mapCotangent (maximalIdeal (AdicCompletion (maximalIdeal R) R))
    (Algebra.ofId R (AdicCompletion (maximalIdeal R) R)) ⋯
inj : Function.Injective ⇑f
surj : Function.Surjective ⇑f
r : IsLocalRing.ResidueField R
m : (maximalIdeal R).Cotangent
⊢ (LinearEquiv.ofBijective f ⋯).toAddEquiv (r • m) =
    (IsLocalRing.ResidueField.map (algebraMap R (AdicCompletion (maximalIdeal R) R))) r •
      (LinearEquiv.ofBijective f ⋯).toAddEquiv m

Tactic:
by
      rcases IsLocalRing.residue_surjective r with ⟨s, rfl⟩
      exact map_smul f s m

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Noetherian

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : IsNoetherianRing R
inst✝³ : Module.Finite R M
A : Type u_3
inst✝² : CommRing A
inst✝¹ : IsArtinianRing A
inst✝ : IsLocalRing A
f : ℕ → A
hf : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD maximalIdeal A ^ m • ⊤]
⊢ ∃ L, ∀ (n : ℕ), f n ≡ L [SMOD maximalIdeal A ^ n • ⊤]

Tactic:
obtain ⟨n, hn⟩ := (isArtinianRing_iff_isNilpotent_maximalIdeal A).mp ‹_›

Goal state after:
R : Type u_1
inst✝⁷ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : IsNoetherianRing R
inst✝³ : Module.Finite R M
A : Type u_3
inst✝² : CommRing A
inst✝¹ : IsArtinianRing A
inst✝ : IsLocalRing A
f : ℕ → A
hf : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD maximalIdeal A ^ m • ⊤]
n : ℕ
hn : maximalIdeal A ^ n = 0
⊢ ∃ L, ∀ (n : ℕ), f n ≡ L [SMOD maximalIdeal A ^ n • ⊤]
Module: Mathlib.RingTheory.AdicCompletion.Noetherian

Goal state before:
pp: case h
R : Type u_1
inst✝⁷ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : IsNoetherianRing R
inst✝³ : Module.Finite R M
A : Type u_3
inst✝² : CommRing A
inst✝¹ : IsArtinianRing A
inst✝ : IsLocalRing A
f : ℕ → A
hf : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD maximalIdeal A ^ m • ⊤]
n : ℕ
hn : maximalIdeal A ^ n = 0
⊢ ∀ (n_1 : ℕ), f n_1 ≡ f n [SMOD maximalIdeal A ^ n_1 • ⊤]

Tactic:
;

Goal state after:
case h
R : Type u_1
inst✝⁷ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : IsNoetherianRing R
inst✝³ : Module.Finite R M
A : Type u_3
inst✝² : CommRing A
inst✝¹ : IsArtinianRing A
inst✝ : IsLocalRing A
f : ℕ → A
hf : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD maximalIdeal A ^ m • ⊤]
n : ℕ
hn : maximalIdeal A ^ n = 0
⊢ ∀ (n_1 : ℕ), f n_1 ≡ f n [SMOD maximalIdeal A ^ n_1 • ⊤]