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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
p : MvPolynomial σ R
n : ℕ
this : p - (truncTotal n) ↑p ∈ MvPolynomial.idealOfVars σ R ^ n
⊢ ↑((AdicCompletion.of (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)) p) n = ↑((toAdicCompletion σ R) ↑p) n

Tactic:
simpa [toAdicCompletion, AdicCompletion.liftAlgHom, AdicCompletion.liftRingHom,
      Ideal.Quotient.mk_eq_mk_iff_sub_mem]

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

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

Tactic:
symm; ext n
  suffices p - (truncTotal n) p ∈ MvPolynomial.idealOfVars σ R ^ n by
    simpa [toAdicCompletion, AdicCompletion.liftAlgHom, AdicCompletion.liftRingHom,
      Ideal.Quotient.mk_eq_mk_iff_sub_mem]
  exact (MvPolynomial.mem_pow_idealOfVars_iff' ..).mpr fun x hx ↦ by simp [coeff_truncTotal _ hx]

Goal state after:
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:
simpa using

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
⊢ (Ideal.Quotient.mk (maximalIdeal R ^ 2 * ⊤)) l = ↑↑m' 2
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
⊢ (maximalIdeal (AdicCompletion (maximalIdeal R) R)).FG

Tactic:
simpa using

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
⊢ (Ideal.map (algebraMap R (AdicCompletion (maximalIdeal R) R)) (maximalIdeal R)).FG
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
g✝ : Fin 0 → G
x✝ : ↑(ModuleCat.of k ↑A)
⊢ (ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle g✝) ≫ (chainsMap f φ).f 0 ≫ (chainsIso₀ B).hom)) x✝ =
    (ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle g✝) ≫ (chainsIso₀ A).hom ≫ Hom.toModuleCatHom φ)) x✝

Tactic:
simp [chainsMap_f, Unique.eq_default (α := Fin 0 → G), Unique.eq_default (α := Fin 0 → H),
    chainsIso₀]

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
h : I ≤ ⊥.jacobson
x : M
hx : ∀ (n : ℕ), x ≡ 0 [SMOD I ^ n • ⊤]
⊢ x ∈ ⨅ i, I ^ i • ⊤

Tactic:
simpa using

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
h : I ≤ ⊥.jacobson
x : M
hx : ∀ (n : ℕ), x ≡ 0 [SMOD I ^ n • ⊤]
⊢ ∀ (i : ℕ), x ∈ I ^ i • ⊤
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
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
h : I ≠ ⊤
x : M
hx : ∀ (n : ℕ), x ≡ 0 [SMOD I ^ n • ⊤]
⊢ x ∈ ⨅ i, I ^ i • ⊤

Tactic:
simpa using

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
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
h : I ≠ ⊤
x : M
hx : ∀ (n : ℕ), x ≡ 0 [SMOD I ^ n • ⊤]
⊢ ∀ (i : ℕ), x ∈ I ^ i • ⊤
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
m : ℕ
⊢ f m ≡ f n [SMOD maximalIdeal A ^ m • ⊤]

Tactic:
by_cases h : m ≤ n

Goal state after:
case pos
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
m : ℕ
h : m ≤ n
⊢ f m ≡ f n [SMOD maximalIdeal A ^ m • ⊤]

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
hf : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD maximalIdeal A ^ m • ⊤]
n : ℕ
hn : maximalIdeal A ^ n = 0
m : ℕ
h : ¬m ≤ n
⊢ f m ≡ f n [SMOD maximalIdeal A ^ m • ⊤]
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 • ⊤)
z : ↥(I ^ b • ⊤)
⊢ (LinearMap.reduceModIdeal (I ^ a) (I ^ b • ⊤).subtype) (Submodule.Quotient.mk z) = 0

Tactic:
simpa using

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 • ⊤)
z : ↥(I ^ b • ⊤)
⊢ ↑z ∈ I ^ 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✝ : G × G
x✝ : ↑A
⊢ (ModuleCat.Hom.hom (chainsMap₂ f φ ≫ d₂₁ B) ∘ₗ lsingle a✝) x✝ =
    (ModuleCat.Hom.hom (d₂₁ A ≫ chainsMap₁ f φ) ∘ₗ lsingle a✝) x✝

Tactic:
simpa using

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✝ : G × G
x✝ : ↑A
⊢ single (f a✝.2) ((B.ρ (f a✝.1⁻¹)) ((Hom.hom φ) x✝)) = single (f a✝.2) ((Hom.hom φ) ((A.ρ a✝.1⁻¹) 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 : ℕ
a✝ : G
x✝ : ↑A
⊢ (ModuleCat.Hom.hom (chainsMap₁ f φ ≫ d₁₀ B) ∘ₗ lsingle a✝) x✝ =
    (ModuleCat.Hom.hom (d₁₀ A ≫ Hom.toModuleCatHom φ) ∘ₗ lsingle a✝) x✝

Tactic:
simpa using

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✝ : G
x✝ : ↑A
⊢ (B.ρ (f a✝⁻¹)) ((Hom.hom φ) x✝) = (Hom.hom φ) ((A.ρ a✝⁻¹) x✝)
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 : ℕ
x : AdicCompletion I M
h : c = b + a
ha : ↑x a = 0
⊢ ∃ t, (powSMulQuotInclusion I M h ⊤) t = ↑x c

Tactic:
simpa using

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 : ℕ
x : AdicCompletion I M
h : c = b + a
ha : ↑x a = 0
⊢ ↑x c ∈ I ^ a • ⊤
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_2
R : Type u_4
inst✝ : CommRing R
f : R⟦X⟧
hf : constantCoeff f = 0
d : σ →₀ ℕ
s : σ
⊢ s ∉ ↑d.support → s ∉ {s | (MvPowerSeries.coeff d) ((PowerSeries.toMvPowerSeries s) f) ≠ 0}

Tactic:
simpa using

Goal state after:
σ : Type u_2
R : Type u_4
inst✝ : CommRing R
f : R⟦X⟧
hf : constantCoeff f = 0
d : σ →₀ ℕ
s : σ
⊢ d s = 0 → (MvPowerSeries.coeff d) ((PowerSeries.toMvPowerSeries s) f) = 0
Module: Mathlib.RingTheory.AdicCompletion.RingHom

Goal state before:
pp: R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
I : Ideal S
inst✝² : IsAdicComplete I S
inst✝¹ : CommRing A
inst✝ : Algebra R A
f g : A →ₐ[R] S
H : ∀ (n : ℕ), (Quotient.mkₐ R (I ^ n)).comp f = (Quotient.mkₐ R (I ^ n)).comp g
x : A
n : ℕ
⊢ (evalₐ I n) (((↑(AlgEquiv.restrictScalars R (ofAlgEquiv I))).comp f) x) =
    (evalₐ I n) (((↑(AlgEquiv.restrictScalars R (ofAlgEquiv I))).comp g) x)

Tactic:
simpa using

Goal state after:
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
I : Ideal S
inst✝² : IsAdicComplete I S
inst✝¹ : CommRing A
inst✝ : Algebra R A
f g : A →ₐ[R] S
H : ∀ (n : ℕ), (Quotient.mkₐ R (I ^ n)).comp f = (Quotient.mkₐ R (I ^ n)).comp g
x : A
n : ℕ
⊢ (Ideal.Quotient.mk (I ^ n)) (f x) = (Ideal.Quotient.mk (I ^ n)) (g x)
Module: Mathlib.RingTheory.AdicCompletion.RingHom

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : NonAssocSemiring R
inst✝ : CommRing S
I : Ideal S
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → R →+* S ⧸ I ^ a n
m n : ℕ
hle : m ≤ n
x : R
s : ℕ
hf : ∀ {m : ℕ} (x : R), ((factorPow I ⋯).comp (f (m + 1))) x = (f m) x
⊢ (f s) x = (Submodule.factor ⋯) ((f (s + 1)) x)

Tactic:
simpa using

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : NonAssocSemiring R
inst✝ : CommRing S
I : Ideal S
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → R →+* S ⧸ I ^ a n
m n : ℕ
hle : m ≤ n
x : R
s : ℕ
hf : ∀ {m : ℕ} (x : R), ((factorPow I ⋯).comp (f (m + 1))) x = (f m) x
⊢ (f s) x = (factor ⋯) ((f (s + 1)) 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
φ : A ⟶ res 1 B
x : ↑(ModuleCat.of k ↥(cycles₁ A))
⊢ ↑((ModuleCat.Hom.hom (mapCycles₁ 1 φ)) x) ∈ boundaries₁ B

Tactic:
simpa using

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
φ : A ⟶ res 1 B
x : ↑(ModuleCat.of k ↥(cycles₁ A))
⊢ ((↑x).sum fun a b ↦ single 1 ((Hom.hom φ) b)) ∈ boundaries₁ B
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 : ℕ
S : Subgroup G
inst✝¹ : S.Normal
inst✝ : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
x : G ⧸ S →₀ ↑(A.ofQuotient S)
hx : x ∈ cycles₁ (A.ofQuotient S)
s : G ⧸ S → G
hs : ∀ (b : G ⧸ S), ↑(s b) = b
hs₁ : QuotientGroup.mk ∘ s = id
⊢ mapDomain s x ∈ cycles₁ A

Tactic:
simpa using

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 : ℕ
S : Subgroup G
inst✝¹ : S.Normal
inst✝ : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
x : G ⧸ S →₀ ↑(A.ofQuotient S)
hx : x ∈ cycles₁ (A.ofQuotient S)
s : G ⧸ S → G
hs : ∀ (b : G ⧸ S), ↑(s b) = b
hs₁ : QuotientGroup.mk ∘ s = id
⊢ (x.sum fun a b ↦ (A.ρ (s a)⁻¹) b) = x.sum fun g a ↦ ((A.ρ.ofQuotient S) g⁻¹) a
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
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
f : ι → R
i✝ : ι
a✝ : AdicCauchySequence I M
n✝ : ℕ
⊢ ↑(((((lsum (AdicCompletion I R)) fun i ↦ (algebraMap R (AdicCompletion I R)) (f i) • LinearMap.id) ∘ₗ
              ↑(finsuppLEquivDirectSum (AdicCompletion I R) (AdicCompletion I M) ι).symm) ∘ₗ
            DirectSum.lof (AdicCompletion I R) ι (fun i ↦ AdicCompletion I M) i✝)
          ((mk I M) a✝))
      n✝ =
    ↑((((map I ((lsum R) fun i ↦ f i • LinearMap.id) ∘ₗ map I ↑(finsuppLEquivDirectSum R M ι).symm) ∘ₗ
              ↑(sumEquivOfFintype I fun x ↦ M)) ∘ₗ
            DirectSum.lof (AdicCompletion I R) ι (fun i ↦ AdicCompletion I M) i✝)
          ((mk I M) a✝))
      n✝

Tactic:
simp only [algebraMap_apply, Algebra.algebraMap_self, RingHom.id_apply, LinearMap.coe_comp,
    coe_lsum, LinearMap.coe_smul, LinearMap.id_coe, LinearEquiv.coe_coe, Function.comp_apply,
    finsuppLEquivDirectSum_symm_lof, Pi.smul_apply, id_eq, smul_zero, sum_single_index, smul_eval,
    mapQ_eq_factor, factor_eq_factor, of_apply, mkQ_apply, Ideal.Quotient.mk_eq_mk, mk_apply_coe,
    sumEquivOfFintype_apply, sum_lof, map_mk, AdicCauchySequence.map_apply_coe, map_smul]

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
f : ι → R
i✝ : ι
a✝ : AdicCauchySequence I M
n✝ : ℕ
⊢ (Ideal.Quotient.mk (I ^ n✝ • ⊤)) (f i✝) • Submodule.Quotient.mk (↑a✝ n✝) = f i✝ • Submodule.Quotient.mk (↑a✝ n✝)
Module: Mathlib.RingTheory.AdicCompletion.Completeness

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
fg : I.FG
x : AdicCompletion I R
eq : I ^ 1 * ⊤ = I
⊢ Function.Injective ⇑(Ideal.Quotient.factor ⋯)

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
fg : I.FG
x : AdicCompletion I R
eq : I ^ 1 * ⊤ = I
⊢ Ideal.map (Ideal.Quotient.mk (I ^ 1 * ⊤)) I = ⊥
Module: Mathlib.RingTheory.AdicCompletion.Completeness

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
fg : I.FG
x : AdicCompletion I R
eq : I ^ 1 * ⊤ = I
this : Function.Injective ⇑(Ideal.Quotient.factor ⋯)
⊢ x ∈ RingHom.ker (evalOneₐ I).toRingHom ↔ x ∈ (eval I R 1).ker

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
fg : I.FG
x : AdicCompletion I R
eq : I ^ 1 * ⊤ = I
this : Function.Injective ⇑(Ideal.Quotient.factor ⋯)
⊢ (Ideal.Quotient.factor ⋯) ((eval I R 1) x) = 0 ↔ (eval I R 1) x = 0
Module: Mathlib.RingTheory.Artinian.Algebra

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Algebra.IsIntegral R A
x✝ : A
⊢ x✝ ∈ IsUnit.submonoid A ↔ x✝ ∈ A⁰

Tactic:
simpa using

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Algebra.IsIntegral R A
x✝ : A
⊢ IsUnit x✝ ↔ x✝ ∈ A⁰
Module: Mathlib.RingTheory.Coalgebra.GroupLike

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Coalgebra R A
inst✝ : Nontrivial R
ha : IsGroupLikeElem R 0
⊢ False

Tactic:
simpa using

Goal state after:
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Coalgebra R A
inst✝ : Nontrivial R
ha : IsGroupLikeElem R 0
⊢ False
Module: Mathlib.RingTheory.Coalgebra.GroupLike

Goal state before:
pp: case cons
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup A
inst✝² : Module R A
inst✝¹ : Coalgebra R A
inst✝ : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ih : ↑s ⊆ {a | IsGroupLikeElem R a} → LinearIndepOn R id ↑s
hs : ↑(Finset.cons a s has) ⊆ {a | IsGroupLikeElem R a}
⊢ LinearIndepOn R id ↑(Finset.cons a s has)

Tactic:
simp only [Finset.cons_eq_insert, Finset.coe_insert, Set.subset_def, Set.mem_insert_iff,
    Finset.mem_coe, Set.mem_ofPred_eq, forall_eq_or_imp] at hs

Goal state after:
case cons
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup A
inst✝² : Module R A
inst✝¹ : Coalgebra R A
inst✝ : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ih : ↑s ⊆ {a | IsGroupLikeElem R a} → LinearIndepOn R id ↑s
hs : IsGroupLikeElem R a ∧ ∀ a ∈ s, IsGroupLikeElem R a
⊢ LinearIndepOn R id ↑(Finset.cons a s has)
Module: Mathlib.RingTheory.Coalgebra.GroupLike

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup A
inst✝² : Module R A
inst✝¹ : Coalgebra R A
inst✝ : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ha : IsGroupLikeElem R a
hs : ∀ a ∈ s, IsGroupLikeElem R a
d : R
c : A → R
hc : ∑ a ∈ s, c a • a = d • a
ih :
  ∀ (f g : A × A → R), ∑ x ∈ s ×ˢ s, f x • x.1 ⊗ₜ[R] x.2 = ∑ x ∈ s ×ˢ s, g x • x.1 ⊗ₜ[R] x.2 → ∀ i ∈ s ×ˢ s, f i = g i
key : ∀ i ∈ s ×ˢ s, (if i.1 = i.2 then d * c i.1 else 0) = c i.1 * c i.2
x : A
hx : x ∈ s
hcx : c x ≠ 0
y : A
hys : y ∈ s
hyx : y ≠ x
⊢ c y = 0

Tactic:
simpa using

Goal state after:
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup A
inst✝² : Module R A
inst✝¹ : Coalgebra R A
inst✝ : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ha : IsGroupLikeElem R a
hs : ∀ a ∈ s, IsGroupLikeElem R a
d : R
c : A → R
hc : ∑ a ∈ s, c a • a = d • a
ih :
  ∀ (f g : A × A → R), ∑ x ∈ s ×ˢ s, f x • x.1 ⊗ₜ[R] x.2 = ∑ x ∈ s ×ˢ s, g x • x.1 ⊗ₜ[R] x.2 → ∀ i ∈ s ×ˢ s, f i = g i
key : ∀ i ∈ s ×ˢ s, (if i.1 = i.2 then d * c i.1 else 0) = c i.1 * c i.2
x : A
hx : x ∈ s
hcx : c x ≠ 0
y : A
hys : y ∈ s
hyx : y ≠ x
⊢ c y = 0
Module: Mathlib.RingTheory.Coalgebra.GroupLike

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup A
inst✝² : Module R A
inst✝¹ : Coalgebra R A
inst✝ : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ha : IsGroupLikeElem R a
hs : ∀ a ∈ s, IsGroupLikeElem R a
d : R
c : A → R
ih :
  ∀ (f g : A × A → R), ∑ x ∈ s ×ˢ s, f x • x.1 ⊗ₜ[R] x.2 = ∑ x ∈ s ×ˢ s, g x • x.1 ⊗ₜ[R] x.2 → ∀ i ∈ s ×ˢ s, f i = g i
key : ∀ i ∈ s ×ˢ s, (if i.1 = i.2 then d * c i.1 else 0) = c i.1 * c i.2
x : A
hc : c x • x = d • a
hx : x ∈ s
hcx : c x ≠ 0
hcy : ∀ y ∈ s, y ≠ x → c y = 0
⊢ (fun a ↦ a * c x) d = (fun a ↦ a * c x) (c x)

Tactic:
simpa using

Goal state after:
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup A
inst✝² : Module R A
inst✝¹ : Coalgebra R A
inst✝ : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ha : IsGroupLikeElem R a
hs : ∀ a ∈ s, IsGroupLikeElem R a
d : R
c : A → R
ih :
  ∀ (f g : A × A → R), ∑ x ∈ s ×ˢ s, f x • x.1 ⊗ₜ[R] x.2 = ∑ x ∈ s ×ˢ s, g x • x.1 ⊗ₜ[R] x.2 → ∀ i ∈ s ×ˢ s, f i = g i
key : ∀ i ∈ s ×ˢ s, (if i.1 = i.2 then d * c i.1 else 0) = c i.1 * c i.2
x : A
hc : c x • x = d • a
hx : x ∈ s
hcx : c x ≠ 0
hcy : ∀ y ∈ s, y ≠ x → c y = 0
⊢ d = c x ∨ c x = 0
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↑(shortComplexH1 (A.coinvariantsShortComplex S).X₁).X₂
a✝ : x ∈ ⊤
X : G →₀ ↥S →₀ ↑A
hX : mapRange ⇑(ConcreteCategory.hom (chains₁ToCoinvariantsKer (res S.subtype A))) ⋯ X = x
Y : ↥S →₀ ↑A :=
  X.sum fun g f ↦ (mapRange.linearMap (A.ρ g⁻¹)) ((lmapDomain (↑A) k fun s ↦ (MulAut.conjNormal g⁻¹) s) f) - f
Z : G × G →₀ ↑A :=
  X.sum fun g f ↦ (lmapDomain (↑A) k fun s ↦ (g, g⁻¹ * ↑s * g)) f - (lmapDomain (↑A) k fun s ↦ (↑s, g)) f
⊢ (ConcreteCategory.hom (d₂₁ A)) Z =
    mapRange id ⋯ ((lmapDomain (↑A) k Subtype.val) Y) -
      (mapRange.linearMap (Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)).subtype) (mapDomain id x)

Tactic:
simpa using

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↑(shortComplexH1 (A.coinvariantsShortComplex S).X₁).X₂
a✝ : x ∈ ⊤
X : G →₀ ↥S →₀ ↑A
hX : mapRange ⇑(ConcreteCategory.hom (chains₁ToCoinvariantsKer (res S.subtype A))) ⋯ X = x
Y : ↥S →₀ ↑A :=
  X.sum fun g f ↦ (mapRange.linearMap (A.ρ g⁻¹)) ((lmapDomain (↑A) k fun s ↦ (MulAut.conjNormal g⁻¹) s) f) - f
Z : G × G →₀ ↑A :=
  X.sum fun g f ↦ (lmapDomain (↑A) k fun s ↦ (g, g⁻¹ * ↑s * g)) f - (lmapDomain (↑A) k fun s ↦ (↑s, g)) f
⊢ ((X.sum fun a b ↦ b.sum fun a_1 b ↦ single a ((A.ρ (↑a_1)⁻¹) b)) + X.sum fun a b ↦ b.sum fun a ↦ single ↑a) =
    (X.sum fun a b ↦ b.sum fun a ↦ single ↑a) + X.sum fun a b ↦ b.sum fun a_1 b ↦ single a ((A.ρ (↑a_1)⁻¹) b)
Module: Mathlib.RingTheory.ClassGroup.ExtendedHom

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Module.IsTorsionFree A B
inst✝¹ : IsDedekindDomain A
inst✝ : IsDedekindDomain B
h : ∀ (I : Ideal A), Submodule.IsPrincipal (Ideal.map (algebraMap A B) I)
I : ↥(Ideal A)⁰
⊢ Submodule.IsPrincipal ↑(extendedIdeal A B I)

Tactic:
simpa using

Goal state after:
A : Type u_1
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Module.IsTorsionFree A B
inst✝¹ : IsDedekindDomain A
inst✝ : IsDedekindDomain B
h : ∀ (I : Ideal A), Submodule.IsPrincipal (Ideal.map (algebraMap A B) I)
I : ↥(Ideal A)⁰
⊢ Submodule.IsPrincipal (Ideal.map (algebraMap A B) ↑I)
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h : ¬p.coeff n = 0
⊢ p.coeff n ∈ ↑p.coeffs

Tactic:
simpa using

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h : ¬p.coeff n = 0
⊢ p.coeff n ∈ p.coeffs
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
p q : R[X]
P : Ideal R
hpq : (p * q).contentIdeal ≤ RingHom.ker (Ideal.Quotient.mk P)
hPprime : P.IsPrime
⊢ p.contentIdeal ≤ RingHom.ker (Ideal.Quotient.mk P) ∨ q.contentIdeal ≤ RingHom.ker (Ideal.Quotient.mk P)

Tactic:
simpa using

Goal state after:
R : Type u_3
inst✝ : CommRing R
p q : R[X]
P : Ideal R
hpq : (p * q).contentIdeal ≤ RingHom.ker (Ideal.Quotient.mk P)
hPprime : P.IsPrime
⊢ map (Ideal.Quotient.mk P) p = 0 ∨ map (Ideal.Quotient.mk P) q = 0