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

Goal state before:
pp: σ✝ : Type u_1
R✝ : Type u_2
n✝ : ℕ
inst✝³ : CommRing R✝
inst✝² : Finite σ✝
σ : Type u_3
R : Type u_4
inst✝¹ : Finite σ
inst✝ : CommRing R
n : ℕ
p q : MvPowerSeries σ R
⊢ (truncTotal n) (p * q) - (truncTotal n) p * (truncTotal n) q ∈ MvPolynomial.idealOfVars σ R ^ n

Tactic:
]

Goal state after:
σ✝ : Type u_1
R✝ : Type u_2
n✝ : ℕ
inst✝³ : CommRing R✝
inst✝² : Finite σ✝
σ : Type u_3
R : Type u_4
inst✝¹ : Finite σ
inst✝ : CommRing R
n : ℕ
p q : MvPowerSeries σ R
⊢ (truncTotal n) (p * q) - (truncTotal n) p * (truncTotal n) q ∈ MvPolynomial.idealOfVars σ R ^ n
Module: Mathlib.RingTheory.AdicCompletion.LocalRing

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
this : IsLocalRing (AdicCompletion (maximalIdeal R) R)
x : IsLocalRing.ResidueField (AdicCompletion (maximalIdeal R) R)
y : AdicCompletion (maximalIdeal R) R
hy : (residue (AdicCompletion (maximalIdeal R) R)) y = x
z : R
hz : (Ideal.Quotient.mk (maximalIdeal R ^ 1 • ⊤)) z = ↑y 1
⊢ (of (maximalIdeal R) R) ((algebraMap R R) z) - y ∈ (eval (maximalIdeal R) R 1).ker

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
this : IsLocalRing (AdicCompletion (maximalIdeal R) R)
x : IsLocalRing.ResidueField (AdicCompletion (maximalIdeal R) R)
y : AdicCompletion (maximalIdeal R) R
hy : (residue (AdicCompletion (maximalIdeal R) R)) y = x
z : R
hz : (Ideal.Quotient.mk (maximalIdeal R ^ 1 • ⊤)) z = ↑y 1
⊢ (of (maximalIdeal R) R) ((algebraMap R R) z) - y ∈ (eval (maximalIdeal R) R 1).ker
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ✝ : Type u_1
R✝ : Type u_2
n✝ : ℕ
inst✝³ : CommRing R✝
inst✝² : Finite σ✝
σ : Type u_3
R : Type u_4
inst✝¹ : Finite σ
inst✝ : CommRing R
n : ℕ
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ✝ : Type u_1
R✝ : Type u_2
n✝ : ℕ
inst✝³ : CommRing R✝
inst✝² : Finite σ✝
σ : Type u_3
R : Type u_4
inst✝¹ : Finite σ
inst✝ : CommRing R
n : ℕ
p : MvPolynomial σ R
⊢ ∀ (x : σ →₀ ℕ), degree x < n → MvPolynomial.coeff x ((truncTotal n) ↑p - p) = 0

Tactic:
]

Goal state after:
σ✝ : Type u_1
R✝ : Type u_2
n✝ : ℕ
inst✝³ : CommRing R✝
inst✝² : Finite σ✝
σ : Type u_3
R : Type u_4
inst✝¹ : Finite σ
inst✝ : CommRing R
n : ℕ
p : MvPolynomial σ R
⊢ ∀ (x : σ →₀ ℕ), degree x < n → MvPolynomial.coeff x ((truncTotal n) ↑p - p) = 0
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)) ⋯
⊢ ∀ (m : (maximalIdeal R).Cotangent), f m = 0 → m = 0

Tactic:
]

Goal state after:
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)) ⋯
⊢ ∀ (m : (maximalIdeal R).Cotangent), f m = 0 → m = 0
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ✝ : Type u_1
R✝ : Type u_2
n✝ : ℕ
inst✝³ : CommRing R✝
inst✝² : Finite σ✝
σ : Type u_3
R : Type u_4
inst✝¹ : Finite σ
inst✝ : CommRing R
n : ℕ
p : MvPolynomial σ R
x : σ →₀ ℕ
h : degree x < n
⊢ MvPolynomial.coeff x p = MvPolynomial.coeff x p

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
x : σ →₀ ℕ
p : MvPowerSeries σ R
n : ℕ
hx : degree x < n
⊢ MvPolynomial.coeff x (Quotient.out (↑((toAdicCompletion σ R) p) n) - (truncTotal n) p) = 0

Tactic:
]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
x : σ →₀ ℕ
p : MvPowerSeries σ R
n : ℕ
hx : degree x < n
⊢ MvPolynomial.coeff x (Quotient.out (↑((toAdicCompletion σ R) p) n) - (truncTotal n) p) = 0
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)) ⋯
m : (maximalIdeal R).Cotangent
m' : ↥(maximalIdeal R)
hm' : (maximalIdeal R).toCotangent m' = m
hm : (algebraMap R (AdicCompletion (maximalIdeal R) R)) ↑m' ∈ (eval (maximalIdeal R) R 2).ker
⊢ m = 0

Tactic:
]

Goal state after:
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)) ⋯
m : (maximalIdeal R).Cotangent
m' : ↥(maximalIdeal R)
hm' : (maximalIdeal R).toCotangent m' = m
hm : (algebraMap R (AdicCompletion (maximalIdeal R) R)) ↑m' ∈ (eval (maximalIdeal R) R 2).ker
⊢ m = 0
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: case a
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
x : σ →₀ ℕ
p : MvPowerSeries σ R
n : ℕ
hx : degree x < n
⊢ Quotient.out ((Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n * ⊤)) ((truncTotal n) p)) - (truncTotal n) p ∈
    MvPolynomial.idealOfVars σ R ^ n

Tactic:
]

Goal state after:
case a
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
x : σ →₀ ℕ
p : MvPowerSeries σ R
n : ℕ
hx : degree x < n
⊢ Quotient.out ((Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n * ⊤)) ((truncTotal n) p)) - (truncTotal n) p ∈
    MvPolynomial.idealOfVars σ R ^ n
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: case a
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
x : σ →₀ ℕ
p : MvPowerSeries σ R
n : ℕ
hx : degree x < n
⊢ (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n * ⊤)) ((truncTotal n) p) =
    (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n * ⊤)) ((truncTotal n) p)

Tactic:
]

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A B C : Rep k G
φ : A ⟶ B
ψ : B ⟶ C
n : ℕ
⊢ HomologicalComplex.homologyMap (chainsMap (MonoidHom.id G) φ) n ≫
      HomologicalComplex.homologyMap (chainsMap (MonoidHom.id G) ψ) n =
    map (MonoidHom.id G) φ n ≫ map (MonoidHom.id G) ψ n

Tactic:
]

Goal state after:
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✝ : ℕ
e : G ≃* H
e' : ↑A ≃ₗ[k] ↑B
he : ∀ (g : G), ↑e' ∘ₗ A.ρ g = B.ρ (e g) ∘ₗ ↑e'
n : ℕ
h : H
⊢ B.ρ h = (↑e' ∘ₗ (MonoidHom.comp A.ρ ↑e.symm) h) ∘ₗ ↑e'.symm

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✝ : ℕ
e : G ≃* H
e' : ↑A ≃ₗ[k] ↑B
he : ∀ (g : G), ↑e' ∘ₗ A.ρ g = B.ρ (e g) ∘ₗ ↑e'
n : ℕ
h : H
⊢ B.ρ h = (↑e' ∘ₗ (MonoidHom.comp A.ρ ↑e.symm) h) ∘ₗ ↑e'.symm
Module: Mathlib.RingTheory.AdicCompletion.LocalRing

Goal state before:
pp: case h
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
m : (maximalIdeal (AdicCompletion (maximalIdeal R) R)).Cotangent
m' : ↥(maximalIdeal (AdicCompletion (maximalIdeal R) R))
hm' : (maximalIdeal (AdicCompletion (maximalIdeal R) R)).toCotangent m' = m
l : R
hl : Submodule.Quotient.mk l = ↑↑m' 2
lmem : l ∈ maximalIdeal R
⊢ (of (maximalIdeal R) R) l - ↑m' ∈ maximalIdeal R ^ 2 • ⊤

Tactic:
]

Goal state after:
case h
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
m : (maximalIdeal (AdicCompletion (maximalIdeal R) R)).Cotangent
m' : ↥(maximalIdeal (AdicCompletion (maximalIdeal R) R))
hm' : (maximalIdeal (AdicCompletion (maximalIdeal R) R)).toCotangent m' = m
l : R
hl : Submodule.Quotient.mk l = ↑↑m' 2
lmem : l ∈ maximalIdeal R
⊢ (of (maximalIdeal R) R) l - ↑m' ∈ maximalIdeal R ^ 2 • ⊤
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
n : ℕ
f : AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
⊢ (truncTotal n) (toAdicCompletionInv σ R f) - Quotient.out (↑f n) ∈ MvPolynomial.idealOfVars σ R ^ n • ⊤

Tactic:
]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
n : ℕ
f : AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
⊢ (truncTotal n) (toAdicCompletionInv σ R f) - Quotient.out (↑f n) ∈ MvPolynomial.idealOfVars σ R ^ 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✝ : ℕ
e : G ≃* H
e' : ↑A ≃ₗ[k] ↑B
he : ∀ (g : G), ↑e' ∘ₗ A.ρ g = B.ρ (e g) ∘ₗ ↑e'
n : ℕ
⊢ map ((↑e.symm).comp ↑e)
      (ofHom { toLinearMap := ↑e', isIntertwining' := ⋯ } ≫
        (resFunctor ↑e).map (ofHom { toLinearMap := ↑e'.symm, isIntertwining' := ⋯ }))
      n =
    map (MonoidHom.id G) (𝟙 A) 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✝ : ℕ
e : G ≃* H
e' : ↑A ≃ₗ[k] ↑B
he : ∀ (g : G), ↑e' ∘ₗ A.ρ g = B.ρ (e g) ∘ₗ ↑e'
n : ℕ
⊢ map ((↑e.symm).comp ↑e)
      (ofHom { toLinearMap := ↑e', isIntertwining' := ⋯ } ≫
        (resFunctor ↑e).map (ofHom { toLinearMap := ↑e'.symm, isIntertwining' := ⋯ }))
      n =
    map (MonoidHom.id G) (𝟙 A) 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✝ : ℕ
e : G ≃* H
e' : ↑A ≃ₗ[k] ↑B
he : ∀ (g : G), ↑e' ∘ₗ A.ρ g = B.ρ (e g) ∘ₗ ↑e'
n : ℕ
⊢ map ((↑e).comp ↑e.symm)
      (ofHom { toLinearMap := ↑e'.symm, isIntertwining' := ⋯ } ≫
        (resFunctor ↑e.symm).map (ofHom { toLinearMap := ↑e', isIntertwining' := ⋯ }))
      n =
    map (MonoidHom.id H) (𝟙 B) 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✝ : ℕ
e : G ≃* H
e' : ↑A ≃ₗ[k] ↑B
he : ∀ (g : G), ↑e' ∘ₗ A.ρ g = B.ρ (e g) ∘ₗ ↑e'
n : ℕ
⊢ map ((↑e).comp ↑e.symm)
      (ofHom { toLinearMap := ↑e'.symm, isIntertwining' := ⋯ } ≫
        (resFunctor ↑e.symm).map (ofHom { toLinearMap := ↑e', isIntertwining' := ⋯ }))
      n =
    map (MonoidHom.id H) (𝟙 B) n
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
n : ℕ
f : AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
x : σ →₀ ℕ
h : degree x < n
⊢ MvPolynomial.coeff x (Quotient.out (↑f (degree x + 1)) - Quotient.out (↑f n)) = 0

Tactic:
]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
n : ℕ
f : AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
x : σ →₀ ℕ
h : degree x < n
⊢ MvPolynomial.coeff x (Quotient.out (↑f (degree x + 1)) - Quotient.out (↑f n)) = 0
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
rkeq :
  Module.rank (IsLocalRing.ResidueField R) (maximalIdeal R).Cotangent =
    Module.rank (IsLocalRing.ResidueField (AdicCompletion (maximalIdeal R) R))
      (maximalIdeal (AdicCompletion (maximalIdeal R) R)).Cotangent
fg' : (maximalIdeal (AdicCompletion (maximalIdeal R) R)).FG
⊢ Module.finrank (IsLocalRing.ResidueField R) (CotangentSpace R) =
    Module.finrank (IsLocalRing.ResidueField (AdicCompletion (maximalIdeal R) R))
      (CotangentSpace (AdicCompletion (maximalIdeal R) R))

Tactic:
]

Goal state after:
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
rkeq :
  Module.rank (IsLocalRing.ResidueField R) (maximalIdeal R).Cotangent =
    Module.rank (IsLocalRing.ResidueField (AdicCompletion (maximalIdeal R) R))
      (maximalIdeal (AdicCompletion (maximalIdeal R) R)).Cotangent
fg' : (maximalIdeal (AdicCompletion (maximalIdeal R) R)).FG
⊢ Module.finrank (IsLocalRing.ResidueField R) (CotangentSpace R) =
    Module.finrank (IsLocalRing.ResidueField (AdicCompletion (maximalIdeal R) R))
      (CotangentSpace (AdicCompletion (maximalIdeal R) R))
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: case a
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
n : ℕ
f : AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
x : σ →₀ ℕ
h : degree x < n
⊢ (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ (degree x + 1) • ⊤)) (Quotient.out (↑f (degree x + 1))) =
    (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ (degree x + 1) • ⊤)) (Quotient.out (↑f n))

Tactic:
]

Goal state after:
case a
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
n : ℕ
f : AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
x : σ →₀ ℕ
h : degree x < n
⊢ (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ (degree x + 1) • ⊤)) (Quotient.out (↑f (degree x + 1))) =
    (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ (degree x + 1) • ⊤)) (Quotient.out (↑f n))
Module: Mathlib.RingTheory.AdicCompletion.Completeness

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
a b c : ℕ
h : c = b + a
x : AdicCompletion I ↥(I ^ a • ⊤)
⊢ (LinearMap.reduceModIdeal (I ^ c) (I ^ a • ⊤).subtype) (↑x c) =
    (powSMulQuotInclusion I M h ⊤) ((transitionMap I ↥(I ^ a • ⊤) ⋯) (↑x c))

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b c : ℕ
h : c = b + a
x : AdicCompletion I ↥(I ^ a • ⊤)
⊢ (LinearMap.reduceModIdeal (I ^ c) (I ^ a • ⊤).subtype) (↑x c) =
    (powSMulQuotInclusion I M h ⊤) ((transitionMap I ↥(I ^ a • ⊤) ⋯) (↑x c))
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A B : Rep k G
f : A ⟶ B
⊢ H0π A ≫ map (MonoidHom.id G) f 0 ≫ (H0Iso B).hom = H0π A ≫ (H0Iso A).hom ≫ (coinvariantsFunctor k G).map f

Tactic:
]

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A B : Rep k G
f : A ⟶ B
⊢ H0π A ≫ map (MonoidHom.id G) f 0 ≫ (H0Iso B).hom = H0π A ≫ (H0Iso A).hom ≫ (coinvariantsFunctor k G).map f
Module: Mathlib.RingTheory.AdicCompletion.Completeness

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
a b : ℕ
h : a ≤ b
x : AdicCompletion I ↥(I ^ b • ⊤)
⊢ (LinearMap.reduceModIdeal (I ^ a) (I ^ b • ⊤).subtype) (↑x a) = 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b : ℕ
h : a ≤ b
x : AdicCompletion I ↥(I ^ b • ⊤)
⊢ (LinearMap.reduceModIdeal (I ^ a) (I ^ b • ⊤).subtype) (↑x a) = 0
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: case a
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
n : ℕ
f : AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
x : σ →₀ ℕ
h : degree x < n
⊢ (AdicCompletion.transitionMap (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R) ⋯)
      ((Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n • ⊤)) (Quotient.out (↑f n))) =
    ↑f (degree x + 1)

Tactic:
]

Goal state after:
case a
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
n : ℕ
f : AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
x : σ →₀ ℕ
h : degree x < n
⊢ (AdicCompletion.transitionMap (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R) ⋯)
      ((Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n • ⊤)) (Quotient.out (↑f n))) =
    ↑f (degree x + 1)
Module: Mathlib.RingTheory.AdicCompletion.Noetherian

Goal state before:
pp: case neg
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
n : ℕ
hn : maximalIdeal A ^ n = 0
m : ℕ
hf : f n = f m
h : ¬m ≤ n
⊢ f m ≡ f n [SMOD maximalIdeal A ^ m • ⊤]

Tactic:
]

Goal state after:
case neg
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
n : ℕ
hn : maximalIdeal A ^ n = 0
m : ℕ
hf : f n = f m
h : ¬m ≤ n
⊢ f m ≡ f n [SMOD maximalIdeal A ^ m • ⊤]
Module: Mathlib.RingTheory.AdicCompletion.Noetherian

Goal state before:
pp: case neg
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
n : ℕ
hn : maximalIdeal A ^ n = 0
m : ℕ
hf : f n = f m
h : ¬m ≤ n
⊢ f m ≡ f m [SMOD maximalIdeal A ^ m • ⊤]

Tactic:
]

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

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
n : ℕ
⊢ ∀ (m : AdicCompletion I ↥(I ^ n • ⊤)), (ofPowSMul I M n) m = 0 → m = 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
⊢ ∀ (m : AdicCompletion I ↥(I ^ n • ⊤)), (ofPowSMul I M n) m = 0 → m = 0
Module: Mathlib.RingTheory.AdicCompletion.Completeness

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
n : ℕ
x : AdicCompletion I ↥(I ^ n • ⊤)
i : ℕ
hx : ↑((ofPowSMul I M n) x) (i + n) = 0
⊢ n + i = n + i

Tactic:
]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : CommRing S
I : Ideal S
inst✝ : IsAdicComplete I S
f : (n : ℕ) → R →+* S ⧸ I ^ n
hf : ∀ {m n : ℕ} (hle : m ≤ n), (factorPow I hle).comp (f n) = f m
n : ℕ
x : R
⊢ (evalₐ I n) ((of I S) ((ofAlgEquiv I).symm ((AdicCompletion.liftRingHom I f ⋯) x))) = (f n) x

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : CommRing S
I : Ideal S
inst✝ : IsAdicComplete I S
f : (n : ℕ) → R →+* S ⧸ I ^ n
hf : ∀ {m n : ℕ} (hle : m ≤ n), (factorPow I hle).comp (f n) = f m
n : ℕ
x : R
⊢ (evalₐ I n) ((of I S) ((ofAlgEquiv I).symm ((AdicCompletion.liftRingHom I f ⋯) x))) = (f n) 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
n : ℕ
⊢ chainsMap₁ f φ ≫ (shortComplexH1 B).g = (shortComplexH1 A).g ≫ Hom.toModuleCatHom φ

Tactic:
by
    simp only [shortComplexH1]
    ext : 3
    simpa [← map_inv, d₁₀] using (hom_comm_apply φ _ _).symm

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
i : σ
r : R
⊢ MvPowerSeries.C r = MvPowerSeries.C r

Tactic:
]

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

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
n : ℕ
x : AdicCompletion I ↥(I ^ n • ⊤)
i : ℕ
hx : ↑x i = 0
⊢ ↑x i = ↑0 i

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
x : AdicCompletion I ↥(I ^ n • ⊤)
i : ℕ
hx : ↑x i = 0
⊢ ↑x i = ↑0 i
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
i : σ
⊢ MvPowerSeries.X i = MvPowerSeries.X i

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_2
R : Type u_4
inst✝ : CommRing R
f : R⟦X⟧
i : σ
⊢ MvPowerSeries.subst (fun x ↦ MvPowerSeries.X i) f = MvPowerSeries.subst (fun x ↦ MvPowerSeries.X i) f

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_2
τ : Type u_3
R : Type u_4
inst✝ : CommRing R
f : R⟦X⟧
i : σ
a : σ → MvPowerSeries τ R
ha : MvPowerSeries.HasSubst a
⊢ MvPowerSeries.subst (fun s ↦ a i) f = MvPowerSeries.subst (fun x ↦ a i) f

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_2
R : Type u_4
inst✝ : CommRing R
f : R⟦X⟧
i : σ
d : σ →₀ ℕ
hd : d i = 0
hf : constantCoeff f = 0
⊢ 0 = 0

pp: σ : Type u_2
R : Type u_4
inst✝ : CommRing R
f : R⟦X⟧
i : σ
d : σ →₀ ℕ
hd : d i = 0
hf : constantCoeff f = 0
⊢ ∀ (x : ℕ), (coeff x) f • (MvPowerSeries.coeff d) (MvPowerSeries.X i ^ x) = 0

Tactic:
]

Goal state after:
σ : Type u_2
R : Type u_4
inst✝ : CommRing R
f : R⟦X⟧
i : σ
d : σ →₀ ℕ
hd : d i = 0
hf : constantCoeff f = 0
⊢ ∀ (x : ℕ), (coeff x) f • (MvPowerSeries.coeff d) (MvPowerSeries.X i ^ x) = 0