mathlib-initiative/mathlib-tactics huggingface dataset:
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
x✝ : ↑(ModuleCat.of k ↑A)
⊢ (ModuleCat.Hom.hom
        (ModuleCat.ofHom (Hom.hom A.norm).toLinearMap ≫ ModuleCat.ofHom (Hom.hom (A.applyAsHom g - 𝟙 A)).toLinearMap))
      x✝ =
    (ModuleCat.Hom.hom 0) x✝

Tactic:
;

Goal state after:
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
x✝ : ↑(ModuleCat.of k ↑A)
⊢ (ModuleCat.Hom.hom
        (ModuleCat.ofHom (Hom.hom A.norm).toLinearMap ≫ ModuleCat.ofHom (Hom.hom (A.applyAsHom g - 𝟙 A)).toLinearMap))
      x✝ =
    (ModuleCat.Hom.hom 0) x✝
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
x✝ : ↑(ModuleCat.of k ↑A)
⊢ (ModuleCat.Hom.hom
        (ModuleCat.ofHom (Hom.hom (A.applyAsHom g - 𝟙 A)).toLinearMap ≫ ModuleCat.ofHom (Hom.hom A.norm).toLinearMap))
      x✝ =
    (ModuleCat.Hom.hom 0) x✝

Tactic:
;

Goal state after:
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
x✝ : ↑(ModuleCat.of k ↑A)
⊢ (ModuleCat.Hom.hom
        (ModuleCat.ofHom (Hom.hom (A.applyAsHom g - 𝟙 A)).toLinearMap ≫ ModuleCat.ofHom (Hom.hom A.norm).toLinearMap))
      x✝ =
    (ModuleCat.Hom.hom 0) x✝
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 : ℕ
ψ : res f A ⟶ 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 H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
n : ℕ
ψ : res f A ⟶ B
hφψ : (Hom.hom φ).toLinearMap = (Hom.hom ψ).toLinearMap
⊢ map f φ n = map f ψ n
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 : ℕ
ψ : res f A ⟶ 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 H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
n : ℕ
ψ : res f A ⟶ B
hφψ : (Hom.hom φ).toLinearMap = (Hom.hom ψ).toLinearMap
⊢ φ = ψ
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
j : ℕ
⊢ (ComplexShape.down ℕ).Rel (2 * j + 1) ((ComplexShape.down ℕ).next (2 * j + 1))

Tactic:
;

Goal state after:
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
j : ℕ
⊢ (ComplexShape.down ℕ).Rel (2 * j + 1) ((ComplexShape.down ℕ).next (2 * j + 1))
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 : ℕ
ψ : res f A ⟶ B
hφψ : (Hom.hom φ).toLinearMap = (Hom.hom ψ).toLinearMap
x✝ : ↑(res f 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 H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
n : ℕ
ψ : res f A ⟶ B
hφψ : (Hom.hom φ).toLinearMap = (Hom.hom ψ).toLinearMap
x✝ : ↑(res f A)
⊢ (Hom.hom φ).toLinearMap x✝ = (Hom.hom ψ).toLinearMap x✝
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cycles₁ X.X₃)
y : G →₀ ↑X.X₂
hy : (mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap) y = ↑z
x : ↑X.X₁
hx : (Rep.Hom.hom X.f) x = (ConcreteCategory.hom (d₁₀ X.X₂)) y
⊢ (ModuleCat.Hom.hom (d₁₀ X.X₃ ≫ (chainsIso₀ X.X₃).inv)) ↑z = 0

Tactic:
;

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cycles₁ X.X₃)
y : G →₀ ↑X.X₂
hy : (mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap) y = ↑z
x : ↑X.X₁
hx : (Rep.Hom.hom X.f) x = (ConcreteCategory.hom (d₁₀ X.X₂)) y
⊢ (ModuleCat.Hom.hom (d₁₀ X.X₃ ≫ (chainsIso₀ X.X₃).inv)) ↑z = 0
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

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

Tactic:
simp only [← cancel_mono (shortComplexH0 B).f, Category.assoc, map_H0Iso_hom_f]

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A B : Rep k G
f : A ⟶ B
⊢ (H0Iso A).hom ≫ (shortComplexH0 A).f ≫ Hom.toModuleCatHom f =
    (H0Iso A).hom ≫ (invariantsFunctor k G).map f ≫ (shortComplexH0 B).f
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cycles₂ X.X₃)
y : G × G →₀ ↑X.X₂
hy : (mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap) y = ↑z
x : G →₀ ↑X.X₁
hx : (mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap) x = (ConcreteCategory.hom (d₂₁ X.X₂)) y
⊢ (ModuleCat.Hom.hom (d₂₁ X.X₃ ≫ (chainsIso₁ X.X₃).inv)) ↑z = 0

Tactic:
;

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cycles₂ X.X₃)
y : G × G →₀ ↑X.X₂
hy : (mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap) y = ↑z
x : G →₀ ↑X.X₁
hx : (mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap) x = (ConcreteCategory.hom (d₂₁ X.X₂)) y
⊢ (ModuleCat.Hom.hom (d₂₁ X.X₃ ≫ (chainsIso₁ X.X₃).inv)) ↑z = 0
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
⊢ d₁₀ M ≫ Hom.toModuleCatHom M.norm = 0

Tactic:
by
  ext
  simp [d₁₀_single M]

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
⊢ (inhomogeneousChains M).d 1 0 ≫ M.tateNorm = 0

Tactic:
by
  simp only [tateNorm, ← Category.assoc, Preadditive.IsIso.comp_right_eq_zero]
  simp [← comp_d₁₀_eq _]

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

Goal state before:
pp: case negSucc
R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
X Y : Rep R G
f g : X ⟶ Y
i : ℕ
x✝ : (Fin i → G) →₀ ↑X
a✝ : Fin i → G
⊢ ((Finsupp.mapRange.linearMap ((Rep.Hom.hom f).toLinearMap + (Rep.Hom.hom g).toLinearMap)) x✝) a✝ =
    ((Finsupp.mapRange.linearMap (Rep.Hom.hom f).toLinearMap + Finsupp.mapRange.linearMap (Rep.Hom.hom g).toLinearMap)
        x✝)
      a✝

Tactic:
;

Goal state after:
case negSucc
R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
X Y : Rep R G
f g : X ⟶ Y
i : ℕ
x✝ : (Fin i → G) →₀ ↑X
a✝ : Fin i → G
⊢ ((Finsupp.mapRange.linearMap ((Rep.Hom.hom f).toLinearMap + (Rep.Hom.hom g).toLinearMap)) x✝) a✝ =
    ((Finsupp.mapRange.linearMap (Rep.Hom.hom f).toLinearMap + Finsupp.mapRange.linearMap (Rep.Hom.hom g).toLinearMap)
        x✝)
      a✝
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
g : G
X✝ Y✝ : FDRep k G
⊢ Functor.LaxMonoidal.μ (forget k G).toFunctor X✝ Y✝ ≫ (equivApp g (X✝ ⊗ Y✝)).hom =
    ((equivApp g X✝).hom ⊗ₘ (equivApp g Y✝).hom) ≫ Functor.LaxMonoidal.μ (forget k G).toFunctor X✝ Y✝

Tactic:
;

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
g : G
X✝ Y✝ : FDRep k G
⊢ Functor.LaxMonoidal.μ (forget k G).toFunctor X✝ Y✝ ≫ (equivApp g (X✝ ⊗ Y✝)).hom =
    ((equivApp g X✝).hom ⊗ₘ (equivApp g Y✝).hom) ≫ Functor.LaxMonoidal.μ (forget k G).toFunctor X✝ Y✝
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
x✝¹ : FDRep k G
x✝ : ↑((forget k G).obj x✝¹).obj
⊢ (Hom.hom ((LaxMonoidalFunctor.isoOfComponents (equivApp 1) ⋯ ⋯ ⋯).hom.hom.app x✝¹).hom) x✝ =
    (Hom.hom ((Iso.hom 1).hom.app x✝¹).hom) x✝

Tactic:
;

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
x✝¹ : FDRep k G
x✝ : ↑((forget k G).obj x✝¹).obj
⊢ (Hom.hom ((LaxMonoidalFunctor.isoOfComponents (equivApp 1) ⋯ ⋯ ⋯).hom.hom.app x✝¹).hom) x✝ =
    (Hom.hom ((Iso.hom 1).hom.app x✝¹).hom) x✝
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
x✝¹ : FDRep k G
x✝ : ↑((forget k G).obj x✝¹).obj
⊢ 1 x✝ = (Hom.hom ((Iso.hom 1).hom.app x✝¹).hom) x✝

Tactic:
;

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
x✝¹ : FDRep k G
x✝ : ↑((forget k G).obj x✝¹).obj
⊢ 1 x✝ = (Hom.hom ((Iso.hom 1).hom.app x✝¹).hom) x✝
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
x✝³ x✝² : G
x✝¹ : FDRep k G
x✝ : ↑((forget k G).obj x✝¹).obj
⊢ (Hom.hom ((LaxMonoidalFunctor.isoOfComponents (equivApp (x✝³ * x✝²)) ⋯ ⋯ ⋯).hom.hom.app x✝¹).hom) x✝ =
    (Hom.hom
        ((LaxMonoidalFunctor.isoOfComponents (equivApp x✝³) ⋯ ⋯ ⋯ *
                    LaxMonoidalFunctor.isoOfComponents (equivApp x✝²) ⋯ ⋯ ⋯).hom.hom.app
            x✝¹).hom)
      x✝

Tactic:
;

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
x✝³ x✝² : G
x✝¹ : FDRep k G
x✝ : ↑((forget k G).obj x✝¹).obj
⊢ (Hom.hom ((LaxMonoidalFunctor.isoOfComponents (equivApp (x✝³ * x✝²)) ⋯ ⋯ ⋯).hom.hom.app x✝¹).hom) x✝ =
    (Hom.hom
        ((LaxMonoidalFunctor.isoOfComponents (equivApp x✝³) ⋯ ⋯ ⋯ *
                    LaxMonoidalFunctor.isoOfComponents (equivApp x✝²) ⋯ ⋯ ⋯).hom.hom.app
            x✝¹).hom)
      x✝
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
x✝³ x✝² : G
x✝¹ : FDRep k G
x✝ : ↑((forget k G).obj x✝¹).obj
⊢ (x✝¹.ρ x✝³ * x✝¹.ρ x✝²) x✝ =
    (Hom.hom
        ((LaxMonoidalFunctor.isoOfComponents (equivApp x✝³) ⋯ ⋯ ⋯ *
                    LaxMonoidalFunctor.isoOfComponents (equivApp x✝²) ⋯ ⋯ ⋯).hom.hom.app
            x✝¹).hom)
      x✝

Tactic:
;

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
x✝³ x✝² : G
x✝¹ : FDRep k G
x✝ : ↑((forget k G).obj x✝¹).obj
⊢ (x✝¹.ρ x✝³ * x✝¹.ρ x✝²) x✝ =
    (Hom.hom
        ((LaxMonoidalFunctor.isoOfComponents (equivApp x✝³) ⋯ ⋯ ⋯ *
                    LaxMonoidalFunctor.isoOfComponents (equivApp x✝²) ⋯ ⋯ ⋯).hom.hom.app
            x✝¹).hom)
      x✝
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 t : G
h : (equivHom k G) s = (equivHom k G) t
⊢ s = t

Tactic:
classical
  apply_fun (fun x ↦ (x.hom.hom.app rightFDRep).hom (single t 1) 1) at h
  simp_all [single_apply]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set σ
⊢ x ∈ Ideal.span (X '' s) ↔ ∀ m ∈ x.support, ∃ i ∈ s, m i ≠ 0

Tactic:
have := @mem_ideal_span_monomial_image σ R _ x ((fun i => Finsupp.single i 1) '' s)

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : σ →₀ ℕ
i : σ
hx : 1 ≤ degree x
hi : ¬x i = 0
⊢ 1 ≤ x i

Tactic:
;

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : σ →₀ ℕ
i : σ
hx : 1 ≤ degree x
hi : ¬x i = 0
⊢ 1 ≤ x i
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
x : σ →₀ ℕ
r : R
h : r ≠ 0
⊢ (monomial x) r ∈ idealOfVars σ R ^ n ↔ n ≤ degree x

Tactic:
by
  classical
  grind only [mem_pow_idealOfVars_iff, mem_support_iff, coeff_monomial]

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

Goal state before:
pp: A : Type u_3
σ : Type u_4
inst✝ : CommRing A
I : Ideal (MvPolynomial σ A)
⊢ Ideal.Quotient.mkₐ A I = aeval fun d ↦ (Ideal.Quotient.mk I) (X d)

Tactic:
ext d
  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
x : σ →₀ ℕ
r : R
n✝ : τ →₀ ℕ
⊢ (coeff n✝) (renameFun f ((monomial x) r)) = (coeff n✝) ((monomial (mapDomain f x)) r)

Tactic:
;

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_4
f : σ → τ
inst✝¹ : TendstoCofinite f
inst✝ : Semiring R
x : σ →₀ ℕ
r : R
n✝ : τ →₀ ℕ
⊢ (coeff n✝) (renameFun f ((monomial x) r)) = (coeff n✝) ((monomial (mapDomain f x)) r)
Module: Mathlib.RingTheory.MvPowerSeries.Rename

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

Tactic:
;

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

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

Tactic:
;

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝² : TendstoCofinite f
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
x : τ →₀ ℕ
fst✝¹ fst✝ snd✝ : σ →₀ ℕ
⊢ fst✝ + snd✝ = fst✝¹ → (mapDomain f fst✝ + mapDomain f snd✝ = x ↔ mapDomain f fst✝¹ = x)

Tactic:
;

Goal state after:
σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝² : TendstoCofinite f
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
x : τ →₀ ℕ
fst✝¹ fst✝ snd✝ : σ →₀ ℕ
⊢ fst✝ + snd✝ = fst✝¹ → (mapDomain f fst✝ + mapDomain f snd✝ = x ↔ mapDomain f fst✝¹ = x)
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 : τ →₀ ℕ
x✝ : ((τ →₀ ℕ) × (τ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)
⊢ x✝.1.1 + x✝.1.2 = x →
    mapDomain f x✝.2.1 = x✝.1.1 →
      mapDomain f x✝.2.2 = x✝.1.2 →
        ∀ (a b : τ →₀ ℕ) (a_1 b_1 : σ →₀ ℕ),
          a + b = x →
            mapDomain f a_1 = a →
              mapDomain f b_1 = b → x✝.2.1 + x✝.2.2 = a_1 + b_1 → x✝.2 = (a_1, b_1) → x✝ = ((a, b), a_1, b_1)

Tactic:
;

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_4
f : σ → τ
inst✝¹ : TendstoCofinite f
inst✝ : Semiring R
p q : MvPowerSeries σ R
x : τ →₀ ℕ
x✝ : ((τ →₀ ℕ) × (τ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)
⊢ x✝.1.1 + x✝.1.2 = x →
    mapDomain f x✝.2.1 = x✝.1.1 →
      mapDomain f x✝.2.2 = x✝.1.2 →
        ∀ (a b : τ →₀ ℕ) (a_1 b_1 : σ →₀ ℕ),
          a + b = x →
            mapDomain f a_1 = a →
              mapDomain f b_1 = b → x✝.2.1 + x✝.2.2 = a_1 + b_1 → x✝.2 = (a_1, b_1) → x✝ = ((a, b), a_1, b_1)
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
n✝ : τ →₀ ℕ
⊢ (coeff n✝) (renameFun f 0) = (coeff n✝) 0

Tactic:
;

Goal state after:
σ : 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
n✝ : τ →₀ ℕ
⊢ (coeff n✝) (renameFun f 0) = (coeff n✝) 0
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
x✝¹ x✝ : MvPowerSeries σ R
n✝ : τ →₀ ℕ
⊢ (coeff n✝) (renameFun f (x✝¹ + x✝)) = (coeff n✝) (renameFun f x✝¹ + renameFun f x✝)

Tactic:
;

Goal state after:
σ : 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
x✝¹ x✝ : MvPowerSeries σ R
n✝ : τ →₀ ℕ
⊢ (coeff n✝) (renameFun f (x✝¹ + x✝)) = (coeff n✝) (renameFun f x✝¹ + renameFun f x✝)
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 : γ →₀ ℕ
⊢ (coeff y) ((rename g) ((rename f) p)) = (coeff y) ((rename (g ∘ f)) p)

Tactic:
;

Goal state after:
σ : 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 : γ →₀ ℕ
⊢ (coeff y) ((rename g) ((rename f) p)) = (coeff y) ((rename (g ∘ f)) p)
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 : γ →₀ ℕ
⊢ ∀ (a : τ →₀ ℕ) (b : σ →₀ ℕ), mapDomain f b = a → (mapDomain (g ∘ f) b = y ↔ mapDomain g a = y)

Tactic:
;

Goal state after:
σ : 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 : γ →₀ ℕ
⊢ ∀ (a : τ →₀ ℕ) (b : σ →₀ ℕ), mapDomain f b = a → (mapDomain (g ∘ f) b = y ↔ mapDomain g a = y)
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
g : G
a : ↑A
⊢ (ConcreteCategory.hom (d₂₁ A)) (single (g, g⁻¹) ((A.ρ g) a) - single (g⁻¹, g) a) = single 1 a - single 1 ((A.ρ g) a)

Tactic:
simp only [map_sub, d₂₁_single (G := G), inv_self_apply, mul_inv_cancel, inv_inv,
    inv_mul_cancel]
  abel

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 : σ ↪ τ
a₁✝ a₂✝ : MvPowerSeries σ R
h : (rename ⇑e) a₁✝ = (rename ⇑e) a₂✝
⊢ a₁✝ = a₂✝

Tactic:
;

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
e : σ ↪ τ
a₁✝ a₂✝ : MvPowerSeries σ R
h : (rename ⇑e) a₁✝ = (rename ⇑e) a₂✝
⊢ a₁✝ = a₂✝
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
f : σ → τ
inst✝² : TendstoCofinite f
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
φ : R →+* S
p : MvPowerSeries σ R
n✝ : τ →₀ ℕ
⊢ (coeff n✝) ((rename f) ((map φ) p)) = (coeff n✝) ((map φ) ((rename f) p))

Tactic:
;

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
f : σ → τ
inst✝² : TendstoCofinite f
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
φ : R →+* S
p : MvPowerSeries σ R
n✝ : τ →₀ ℕ
⊢ (coeff n✝) ((rename f) ((map φ) p)) = (coeff n✝) ((map φ) ((rename f) p))
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
e : σ ↪ τ
x : σ →₀ ℕ
r : R
n✝ : σ →₀ ℕ
⊢ (coeff n✝) (killComplFun e ((monomial (embDomain e x)) r)) = (coeff n✝) ((monomial x) r)

Tactic:
;

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
e : σ ↪ τ
x : σ →₀ ℕ
r : R
n✝ : σ →₀ ℕ
⊢ (coeff n✝) (killComplFun e ((monomial (embDomain e x)) r)) = (coeff n✝) ((monomial x) r)
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
e : σ ↪ τ
x : τ →₀ ℕ
r : R
h : x ∉ Set.range (embDomain e)
n✝ : σ →₀ ℕ
⊢ (coeff n✝) (killComplFun e ((monomial x) r)) = (coeff n✝) 0

Tactic:
;

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
e : σ ↪ τ
x : τ →₀ ℕ
r : R
h : x ∉ Set.range (embDomain e)
n✝ : σ →₀ ℕ
⊢ (coeff n✝) (killComplFun e ((monomial x) r)) = (coeff n✝) 0
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✝ e : σ ↪ τ
n✝ : σ →₀ ℕ
⊢ (coeff n✝) (killComplFun e 0) = (coeff n✝) 0

Tactic:
;

Goal state after:
σ : 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✝ e : σ ↪ τ
n✝ : σ →₀ ℕ
⊢ (coeff n✝) (killComplFun e 0) = (coeff n✝) 0
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✝ e : σ ↪ τ
x✝¹ x✝ : MvPowerSeries τ R
n✝ : σ →₀ ℕ
⊢ (coeff n✝) (killComplFun e (x✝¹ + x✝)) = (coeff n✝) (killComplFun e x✝¹ + killComplFun e x✝)

Tactic:
;

Goal state after:
σ : 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✝ e : σ ↪ τ
x✝¹ x✝ : MvPowerSeries τ R
n✝ : σ →₀ ℕ
⊢ (coeff n✝) (killComplFun e (x✝¹ + x✝)) = (coeff n✝) (killComplFun e x✝¹ + killComplFun e x✝)
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
e : σ ↪ τ
i : σ
n✝ : σ →₀ ℕ
⊢ (coeff n✝) ((killCompl e) (X (e i))) = (coeff n✝) (X i)

Tactic:
;

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
e : σ ↪ τ
i : σ
n✝ : σ →₀ ℕ
⊢ (coeff n✝) ((killCompl e) (X (e i))) = (coeff n✝) (X i)
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
e : σ ↪ τ
x✝ : MvPowerSeries σ R
n✝ : σ →₀ ℕ
⊢ (coeff n✝) (((killCompl e).comp (rename ⇑e)) x✝) = (coeff n✝) ((AlgHom.id R (MvPowerSeries σ R)) x✝)

Tactic:
;

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
e : σ ↪ τ
x✝ : MvPowerSeries σ R
n✝ : σ →₀ ℕ
⊢ (coeff n✝) (((killCompl e).comp (rename ⇑e)) x✝) = (coeff n✝) ((AlgHom.id R (MvPowerSeries σ R)) x✝)
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
e : σ ↪ τ
φ : R →+* S
p : MvPowerSeries τ R
n✝ : σ →₀ ℕ
⊢ (coeff n✝) ((killCompl e) ((map φ) p)) = (coeff n✝) ((map φ) ((killCompl e) p))

Tactic:
;

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
e : σ ↪ τ
φ : R →+* S
p : MvPowerSeries τ R
n✝ : σ →₀ ℕ
⊢ (coeff n✝) ((killCompl e) ((map φ) p)) = (coeff n✝) ((map φ) ((killCompl e) p))