mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
C : ↑(H0 A) → Prop
x : ↑(H0 A)
h : ∀ (x : ↥A.ρ.invariants), C ((ConcreteCategory.hom (H0Iso A).inv) x)
⊢ C x

Tactic:
by
  simpa using h ((H0Iso A).hom x)

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
x : ↑A
⊢ x ∈ A.ρ.invariants

Tactic:
by simp

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
f : ↥(cocycles₁ A)
x : Additive G
⊢ ((ConcreteCategory.hom (H1IsoOfIsTrivial A).hom) ((ConcreteCategory.hom (H1π A)) f)) x = f (Additive.toMul x)

Tactic:
by simp

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

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A : Rep k G
g✝ : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g✝
j : ℕ
a : ↑A
g : G
hj : Even (j + 1)
⊢ ∀ (i : G), i ∈ Finset.univ ↔ (MulEquiv.inv G) i ∈ Finset.univ

Tactic:
by simp

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

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A : Rep k G
g✝ : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g✝
j : ℕ
a : ↑A
g : G
hj : Even (j + 1)
⊢ ∀ i ∈ Finset.univ, (A.ρ (i * g⁻¹)) a = (A.ρ (((MulEquiv.inv G) i)⁻¹ * g⁻¹)) a

Tactic:
by simp

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

Goal state before:
pp: k G : Type u
inst✝³ : CommRing k
inst✝² : CommGroup G
inst✝¹ : Fintype G
A : Rep k G
g : G
inst✝ : DecidableEq G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
i : ℕ
h₀ : NeZero i
hi : Even i
⊢ (ComplexShape.down ℕ).Rel ((ComplexShape.down ℕ).prev i) i

Tactic:
by simp

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

Goal state before:
pp: k G : Type u
inst✝³ : CommRing k
inst✝² : CommGroup G
inst✝¹ : Fintype G
A : Rep k G
g : G
inst✝ : DecidableEq G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
i : ℕ
hi : Odd i
⊢ (ComplexShape.down ℕ).Rel ((ComplexShape.down ℕ).prev i) i

Tactic:
by simp

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

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
n✝ : ℕ
e : G ≃* H
e' : ↑B ≃ₗ[k] ↑A
he : ∀ (g : G), ↑e' ∘ₗ B.ρ g = A.ρ (e g) ∘ₗ ↑e'
n : ℕ
⊢ (↑e.symm).comp ↑e = MonoidHom.id G

Tactic:
by simp

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

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
n✝ : ℕ
e : G ≃* H
e' : ↑B ≃ₗ[k] ↑A
he : ∀ (g : G), ↑e' ∘ₗ B.ρ g = A.ρ (e g) ∘ₗ ↑e'
n : ℕ
⊢ (↑e).comp ↑e.symm = MonoidHom.id H

Tactic:
by simp

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

Goal state before:
pp: k G H : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Group H
A✝ : Rep k H
B✝ : Rep k G
f✝ : G →* H
φ : res f✝ A✝ ⟶ B✝
n : ℕ
A B : Rep k G
f : A ⟶ B
inst✝ : Mono f
Z✝ : ModuleCat k
g h : Z✝ ⟶ groupCohomology A 0
hgh : g ≫ map (MonoidHom.id G) f 0 = h ≫ map (MonoidHom.id G) f 0
⊢ g = h

Tactic:
by
    simp only [← cancel_mono (H0Iso B).hom, Category.assoc, map_id_comp_H0Iso_hom] at hgh
    simp_all [cancel_mono]

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

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
n : ℕ
⊢ Hom.toModuleCatHom φ ≫ (shortComplexH1 B).f = (shortComplexH1 A).f ≫ cochainsMap₁ f φ

Tactic:
ext x
    funext g
    simpa [shortComplexH1, d₀₁, cochainsMap₁] using (hom_comm_apply φ g x).symm

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.TateCohomology.Basic

Goal state before:
pp: R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
M : Rep R G
X✝ : Rep R G
Y✝ : Rep R G
X Y : Rep R G
⊢ (tateComplexFunctor R G).map 0 = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : Nontrivial k
s : G
⊢ ∀ ⦃a₂ : G⦄, (equivHom k G) s = (equivHom k G) a₂ → s = a₂

Tactic:
t

Goal state after:
k G : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : Nontrivial k
s t : G
⊢ (equivHom k G) s = (equivHom k G) t → s = t
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set σ
this :
  x ∈ Ideal.span ((fun x ↦ (monomial (Finsupp.single x 1)) 1) '' s) ↔
    ∀ xi ∈ x.support, ∃ si ∈ (fun i ↦ Finsupp.single i 1) '' s, si ≤ xi
⊢ (∀ xi ∈ x.support, ∃ si ∈ (fun i ↦ Finsupp.single i 1) '' s, si ≤ xi) ↔ ∀ m ∈ x.support, ∃ i ∈ s, m i ≠ 0

Tactic:
simp [Nat.one_le_iff_ne_zero]

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsDomain k
η : Aut (forget k G)
s : G
hs : (evalAlgHom k (fun a ↦ k) 1).comp (algHomOfRightFDRepComp η) = evalAlgHom k (fun i ↦ k) s
u t : G
nat :
  (forget k G).map (leftRegularFDRepHom t⁻¹) ≫ η.hom.hom.app rightFDRep =
    η.hom.hom.app rightFDRep ≫ (forget k G).map (leftRegularFDRepHom t⁻¹)
⊢ (Hom.hom (η.hom.hom.app (FDRep.of rightRegular)).hom) ((basisFun k G) u) t =
    (leftRegular t⁻¹) ((ConcreteCategory.hom (η.hom.hom.app rightFDRep).hom) (single u 1)) 1

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
c : σ →₀ ℕ
hx : c + single i 1 ∈ ⇑degree ⁻¹' Set.Ici 1
hi : i ∈ (c + single i 1).support
⊢ X i ∈ Set.range X

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
⊢ Submodule.span (MvPolynomial σ R) (Set.range X ^ n) = Ideal.span ((fun x ↦ (monomial x) 1) '' ⇑degree ⁻¹' {n})

Tactic:
← Set.image_univ,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
⊢ Submodule.span (MvPolynomial σ R) ((X '' Set.univ) ^ n) = Ideal.span ((fun x ↦ (monomial x) 1) '' ⇑degree ⁻¹' {n})
Module: Mathlib.RingTheory.Noetherian.OfPrime

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ span ↑{1} = ⊤

Tactic:
by simp

Goal state after:
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:
· simp only [sup_le_iff, span_le, range_subset_iff, smul_eq_mul]
      exact ⟨p_mem_I, fun _ ↦ mul_comm a _ ▸ mem_colon_span_singleton.1 (hi ▸ mem_span_range_self)⟩

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.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
f : σ → τ
inst✝¹ : TendstoCofinite f
inst✝ : Semiring R
p q : MvPowerSeries σ R
x : τ →₀ ℕ
⊢ ∀ (p : (σ →₀ ℕ) × (σ →₀ ℕ) × (σ →₀ ℕ)), p ∈ ⋯.toFinset ↔ p.1 ∈ ⋯.toFinset ∧ p.2 ∈ antidiagonal p.1

Tactic:
by simp

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
f : σ → τ
inst✝¹ : TendstoCofinite f
inst✝ : Semiring R
p q : MvPowerSeries σ R
x : τ →₀ ℕ
⊢ ∀ (p : ((τ →₀ ℕ) × (τ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)),
    p ∈ ⋯.toFinset ↔ p.1 ∈ antidiagonal x ∧ p.2 ∈ ⋯.toFinset ×ˢ ⋯.toFinset

Tactic:
by simp

Goal state after:
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
s : Fin w✝¹ → R
H : ∑ x, (s x * r x * a + s x * p x) = y
⊢ ∃ y_1 ∈ span (Set.range p), ∃ z ∈ span (Set.range fun a_1 ↦ a • i a_1), y_1 + z = y

Tactic:
sum_add_distrib,

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
s : Fin w✝¹ → R
H : ∑ x, s x * r x * a + ∑ x, s x * p x = y
⊢ ∃ y_1 ∈ span (Set.range p), ∃ z ∈ span (Set.range fun a_1 ↦ a • i a_1), y_1 + z = y
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
γ : Type u_3
R : Type u_4
f : σ → τ
g : τ → γ
inst✝² : TendstoCofinite f
inst✝¹ : CommSemiring R
inst✝ : TendstoCofinite g
p : MvPowerSeries σ R
y : γ →₀ ℕ
⊢ Set.InjOn (fun u ↦ (mapDomain f u, u)) ↑⋯.toFinset

Tactic:
by simp

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

Goal state before:
pp: σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
x✝ : MvPowerSeries σ R
y : σ →₀ ℕ
⊢ ∀ b ∈ ⋯.toFinset, b ≠ y → (coeff b) x✝ = 0

Tactic:
by simp

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

Goal state before:
pp: σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
x✝ : MvPowerSeries σ R
y : σ →₀ ℕ
⊢ y ∉ ⋯.toFinset → (coeff y) x✝ = 0

Tactic:
by simp

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

Goal state before:
pp: σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p : MvPowerSeries σ R
⊢ (rename id) p = p

Tactic:
by simp

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
f : σ → τ
inst✝¹ : TendstoCofinite f
inst✝ : CommSemiring R
p : MvPowerSeries σ R
⊢ 0 ∉ ⋯.toFinset → (coeff 0) p = 0

Tactic:
by simp

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
γ : Type u_3
R : Type u_4
S : Type u_5
f : σ → τ
g : τ → γ
inst✝² : TendstoCofinite f
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
e : σ ≃ τ
x✝ : MvPowerSeries σ R
⊢ (rename ⇑e.symm) ((↑↑(rename ⇑e).toRingHom).toFun x✝) = x✝

Tactic:
by simp

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
γ : Type u_3
R : Type u_4
S : Type u_5
f : σ → τ
g : τ → γ
inst✝² : TendstoCofinite f
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
e : σ ≃ τ
x✝ : MvPowerSeries τ R
⊢ (↑↑(rename ⇑e).toRingHom).toFun ((rename ⇑e.symm) x✝) = x✝

Tactic:
by simp

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

Goal state before:
pp: σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
⊢ ∀ (a : MvPowerSeries σ R), (renameEquiv R (Equiv.refl σ)) a = AlgEquiv.refl a

Tactic:
by simp

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
e : σ ↪ τ
t : τ
h : t ∉ Set.range ⇑e
⊢ 1 ≠ 0

Tactic:
by simp

Goal state after:
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
⊢ ∀ (s : σ), IsNilpotent (constantCoeff ((X ∘ f) s))

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
a : R
ha : a ≠ 0
ha₂ : ¬↑(span {a}) ∩ ↑(closure {r | Prime r}).toSubsemigroup = ∅
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod a

Tactic:
rcases nonempty_iff_ne_empty.2 ha₂ with ⟨x, hx, hx₂⟩

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
a : R
ha : a ≠ 0
ha₂ : ¬↑(span {a}) ∩ ↑(closure {r | Prime r}).toSubsemigroup = ∅
x : R
hx : x ∈ ↑(span {a})
hx₂ : x ∈ ↑(closure {r | Prime r}).toSubsemigroup
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod a
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: k G A : Type u
inst✝⁵ : CommRing k
inst✝⁴ : Group G
inst✝³ : AddCommGroup A
inst✝² : Module k A
inst✝¹ : DistribMulAction G A
inst✝ : SMulCommClass G k A
x : A
hx : x ∈ Coinvariants.ker (Representation.ofDistribMulAction k G A)
⊢ (sum 0 fun g z ↦ g⁻¹ • z - z) = 0

Tactic:
by simp

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (ComplexShape.down ℕ).next 0 = 0

Tactic:
by simp

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (ComplexShape.down ℕ).prev 0 = 1

Tactic:
by simp

Goal state after:
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
⊢ (ComplexShape.down ℕ).next 0 = 0

Tactic:
by simp

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (ComplexShape.down ℕ).prev 1 = 2

Tactic:
by simp

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (ComplexShape.down ℕ).next 1 = 0

Tactic:
by simp

Goal state after:
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)
⊢ (ComplexShape.down ℕ).next 1 = 0

Tactic:
by simp

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (ComplexShape.down ℕ).prev 2 = 3

Tactic:
by simp

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (ComplexShape.down ℕ).next 2 = 1

Tactic:
by simp

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

Goal state before:
pp: 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}
⊢ (∀ b ∈ ∅, Prime b) ∧ Associated ∅.prod 1

Tactic:
by simp

Goal state after:
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)
⊢ (ComplexShape.down ℕ).next 2 = 1

Tactic:
by simp

Goal state after:
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
⊢ (ComplexShape.down ℕ).prev 0 = 1

Tactic:
by simp

Goal state after:
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
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
⊢ constantCoeff 0 = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
U : Set R
i : ℕ
h : ↑(I ^ i) ⊆ U
⊢ ↑(I ^ i) = ↑((fun i ↦ toAddSubgroup (I ^ i • ⊤)) i)

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

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
m : M
i : ℕ
⊢ ↑(I ^ i • ⊤) = ↑((fun i ↦ toAddSubgroup (I ^ i • ⊤)) i)

Tactic:
by simp

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

Goal state before:
pp: case mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : UniformSpace R
inst✝ : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
this✝ : (𝓝 0).IsCountablyGenerated
this : (𝓤 R).IsCountablyGenerated
H : ∀ (f : ℕ → R), (∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m) → ∃ L, ∀ (n : ℕ), f n - L ∈ I ^ n
u : ℕ → R
hu : CauchySeq u
⊢ ∃ a, Filter.Tendsto u Filter.atTop (𝓝 a)

Tactic:
have : ∀ i, ∃ N, ∀ m, N ≤ m → ∀ n, N ≤ n → u n - u m ∈ I ^ i := by
      simpa using hI.hasBasis_nhds_zero.uniformity_of_nhds_zero.cauchySeq_iff.mp hu

Goal state after:
case mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : UniformSpace R
inst✝ : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
this✝¹ : (𝓝 0).IsCountablyGenerated
this✝ : (𝓤 R).IsCountablyGenerated
H : ∀ (f : ℕ → R), (∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m) → ∃ L, ∀ (n : ℕ), f n - L ∈ I ^ n
u : ℕ → R
hu : CauchySeq u
this : ∀ (i : ℕ), ∃ N, ∀ (m : ℕ), N ≤ m → ∀ (n : ℕ), N ≤ n → u n - u m ∈ I ^ i
⊢ ∃ a, Filter.Tendsto u Filter.atTop (𝓝 a)
Module: Mathlib.RingTheory.AdicCompletion.Topology

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : UniformSpace R
inst✝ : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
this✝ : (𝓝 0).IsCountablyGenerated
this : (𝓤 R).IsCountablyGenerated
H : ∀ (f : ℕ → R), (∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m) → ∃ L, ∀ (n : ℕ), f n - L ∈ I ^ n
u : ℕ → R
hu : CauchySeq u
N : ℕ → ℕ
hN : ∀ (i m : ℕ), N i ≤ m → ∀ (n : ℕ), N i ≤ n → u n - u m ∈ I ^ i
m✝ n✝ : ℕ
x✝ : m✝ ≤ n✝
⊢ m✝ ∈ Finset.Iic m✝

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : UniformSpace R
inst✝ : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
this✝ : (𝓝 0).IsCountablyGenerated
this : (𝓤 R).IsCountablyGenerated
H : ∀ (f : ℕ → R), (∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m) → ∃ L, ∀ (n : ℕ), f n - L ∈ I ^ n
u : ℕ → R
hu : CauchySeq u
N : ℕ → ℕ
hN : ∀ (i m : ℕ), N i ≤ m → ∀ (n : ℕ), N i ≤ n → u n - u m ∈ I ^ i
L : R
hL : ∀ (n : ℕ), u ((Finset.Iic n).sup N) - L ∈ I ^ n
i n : ℕ
hn : (Finset.Iic i).sup N ≤ n
⊢ i ∈ Finset.Iic i

Tactic:
by simp

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

Goal state before:
pp: case refine_2.fst
σ : 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)⟩
t : Option σ
⊢ a₁✝.1 t = a₂✝.1 t

Tactic:
cases t

Goal state after:
case refine_2.fst.none
σ : 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₁✝.1 none = a₂✝.1 none

case refine_2.fst.some
σ : 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)⟩
val✝ : σ
⊢ a₁✝.1 (Option.some val✝) = a₂✝.1 (Option.some val✝)
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: case refine_2.snd
σ : 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)⟩
t : Option σ
⊢ a₁✝.2 t = a₂✝.2 t

Tactic:
cases t

Goal state after:
case refine_2.snd.none
σ : 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₁✝.2 none = a₂✝.2 none

case refine_2.snd.some
σ : 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)⟩
val✝ : σ
⊢ a₁✝.2 (Option.some val✝) = a₂✝.2 (Option.some val✝)
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:
cases t

Goal state after:
case h.none
σ : 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
⊢ (optionElim m u + optionElim n v) none = (optionElim k x) none

case h.some
σ : 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
val✝ : σ
⊢ (optionElim m u + optionElim n v) (Option.some val✝) = (optionElim k x) (Option.some val✝)
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 : ℕ
x✝¹ x✝ : MvPowerSeries σ R
⊢ (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n)) ((truncTotal n) (x✝¹ + x✝)) =
    (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n)) ((truncTotal n) x✝¹) +
      (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n)) ((truncTotal n) x✝)

Tactic:
by simp

Goal state after: