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

Goal state before:
pp: case e_6
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
x✝ : ↑((inhomogeneousCochains A).X 3)
g : G × G × G
x : Fin 3
⊢ (fun x ↦ ⇑f ∘ x) (((Fin.consEquiv fun a ↦ G).symm.trans ((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G))).symm g)
      x =
    ((Fin.consEquiv fun a ↦ H).symm.trans ((Equiv.refl H).prodCongr (piFinTwoEquiv fun x ↦ H))).symm
      (Prod.map (⇑f) (Prod.map ⇑f ⇑f) g) x

Tactic:
fin_cases x

Goal state after:
case e_6.«0»
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
x : ↑((inhomogeneousCochains A).X 3)
g : G × G × G
⊢ (fun x ↦ ⇑f ∘ x) (((Fin.consEquiv fun a ↦ G).symm.trans ((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G))).symm g)
      ((fun i ↦ i) ⟨0, ⋯⟩) =
    ((Fin.consEquiv fun a ↦ H).symm.trans ((Equiv.refl H).prodCongr (piFinTwoEquiv fun x ↦ H))).symm
      (Prod.map (⇑f) (Prod.map ⇑f ⇑f) g) ((fun i ↦ i) ⟨0, ⋯⟩)

case e_6.«1»
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
x : ↑((inhomogeneousCochains A).X 3)
g : G × G × G
⊢ (fun x ↦ ⇑f ∘ x) (((Fin.consEquiv fun a ↦ G).symm.trans ((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G))).symm g)
      ((fun i ↦ i) ⟨1, ⋯⟩) =
    ((Fin.consEquiv fun a ↦ H).symm.trans ((Equiv.refl H).prodCongr (piFinTwoEquiv fun x ↦ H))).symm
      (Prod.map (⇑f) (Prod.map ⇑f ⇑f) g) ((fun i ↦ i) ⟨1, ⋯⟩)

case e_6.«2»
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
x : ↑((inhomogeneousCochains A).X 3)
g : G × G × G
⊢ (fun x ↦ ⇑f ∘ x) (((Fin.consEquiv fun a ↦ G).symm.trans ((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G))).symm g)
      ((fun i ↦ i) ⟨2, ⋯⟩) =
    ((Fin.consEquiv fun a ↦ H).symm.trans ((Equiv.refl H).prodCongr (piFinTwoEquiv fun x ↦ H))).symm
      (Prod.map (⇑f) (Prod.map ⇑f ⇑f) g) ((fun i ↦ i) ⟨2, ⋯⟩)
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
⊢ M.tateNorm = ModuleCat.ofHom ((Finsupp.lsum R) fun x ↦ LinearMap.pi fun x ↦ M.ρ.norm)

Tactic:
ext

Goal state after:
R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
M : Rep R G
g✝¹ : Fin 0 → G
x✝ : ↑(ModuleCat.of R ↑M)
g✝ : Fin 0 → G
⊢ (ModuleCat.Hom.hom (ModuleCat.ofHom (Finsupp.lsingle g✝¹) ≫ M.tateNorm)) x✝ g✝ =
    (ModuleCat.Hom.hom
        (ModuleCat.ofHom (Finsupp.lsingle g✝¹) ≫
          ModuleCat.ofHom ((Finsupp.lsum R) fun x ↦ LinearMap.pi fun x ↦ M.ρ.norm)))
      x✝ g✝
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
⊢ Hom.toModuleCatHom M.norm ≫ d₀₁ M = 0

Tactic:
ext

Goal state after:
R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
M : Rep R G
x✝¹ : ↑(ModuleCat.of R ↑M)
x✝ : G
⊢ (ModuleCat.Hom.hom (Hom.toModuleCatHom M.norm ≫ d₀₁ M)) x✝¹ x✝ = (ModuleCat.Hom.hom 0) x✝¹ x✝
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:
ext

Goal state after:
R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
M : Rep R G
a✝ : G
x✝ : ↑M
⊢ (ModuleCat.Hom.hom (d₁₀ M ≫ Hom.toModuleCatHom M.norm) ∘ₗ Finsupp.lsingle a✝) x✝ =
    (ModuleCat.Hom.hom 0 ∘ₗ Finsupp.lsingle a✝) x✝
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 Y : Rep R G
φ : X ⟶ Y
⊢ (chainsMap (MonoidHom.id G) φ).f 0 ≫ (tateComplexConnectData Y).d₀ =
    (tateComplexConnectData X).d₀ ≫ (cochainsMap (MonoidHom.id G) φ).f 0

Tactic:
ext

Goal state after:
R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
M : Rep R G
X Y : Rep R G
φ : X ⟶ Y
g✝¹ : Fin 0 → G
x✝ : ↑(ModuleCat.of R ↑X)
g✝ : Fin 0 → G
⊢ (ModuleCat.Hom.hom
        (ModuleCat.ofHom (Finsupp.lsingle g✝¹) ≫ (chainsMap (MonoidHom.id G) φ).f 0 ≫ (tateComplexConnectData Y).d₀))
      x✝ g✝ =
    (ModuleCat.Hom.hom
        (ModuleCat.ofHom (Finsupp.lsingle g✝¹) ≫ (tateComplexConnectData X).d₀ ≫ (cochainsMap (MonoidHom.id G) φ).f 0))
      x✝ g✝
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 : ℕ
⊢ Finsupp.mapRange.linearMap ((Rep.Hom.hom f).toLinearMap + (Rep.Hom.hom g).toLinearMap) =
    Finsupp.mapRange.linearMap (Rep.Hom.hom f).toLinearMap + Finsupp.mapRange.linearMap (Rep.Hom.hom g).toLinearMap

Tactic:
ext

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
⊢ LaxMonoidalFunctor.isoOfComponents (equivApp 1) ⋯ ⋯ ⋯ = 1

Tactic:
ext

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✝¹ x✝ : G
⊢ LaxMonoidalFunctor.isoOfComponents (equivApp (x✝¹ * x✝)) ⋯ ⋯ ⋯ =
    LaxMonoidalFunctor.isoOfComponents (equivApp x✝¹) ⋯ ⋯ ⋯ * LaxMonoidalFunctor.isoOfComponents (equivApp x✝) ⋯ ⋯ ⋯

Tactic:
ext

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
⊢ { toFun := fun f t ↦ f (t * 1), map_add' := ⋯, map_smul' := ⋯ } = 1

Tactic:
ext

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
x✝¹ : G → k
x✝ : G
⊢ { toFun := fun f t ↦ f (t * 1), map_add' := ⋯, map_smul' := ⋯ } x✝¹ x✝ = 1 x✝¹ x✝
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
x✝¹ x✝ : G
⊢ { toFun := fun f t ↦ f (t * (x✝¹ * x✝)), map_add' := ⋯, map_smul' := ⋯ } =
    { toFun := fun f t ↦ f (t * x✝¹), map_add' := ⋯, map_smul' := ⋯ } *
      { toFun := fun f t ↦ f (t * x✝), map_add' := ⋯, map_smul' := ⋯ }

Tactic:
ext

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
x✝³ x✝² : G
x✝¹ : G → k
x✝ : G
⊢ { toFun := fun f t ↦ f (t * (x✝³ * x✝²)), map_add' := ⋯, map_smul' := ⋯ } x✝¹ x✝ =
    ({ toFun := fun f t ↦ f (t * x✝³), map_add' := ⋯, map_smul' := ⋯ } *
        { toFun := fun f t ↦ f (t * x✝²), map_add' := ⋯, map_smul' := ⋯ })
      x✝¹ x✝
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
⊢ { toFun := fun f t ↦ f (1⁻¹ * t), map_add' := ⋯, map_smul' := ⋯ } = 1

Tactic:
ext

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
x✝¹ : G → k
x✝ : G
⊢ { toFun := fun f t ↦ f (1⁻¹ * t), map_add' := ⋯, map_smul' := ⋯ } x✝¹ x✝ = 1 x✝¹ x✝
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
x✝¹ x✝ : G
⊢ { toFun := fun f t ↦ f ((x✝¹ * x✝)⁻¹ * t), map_add' := ⋯, map_smul' := ⋯ } =
    { toFun := fun f t ↦ f (x✝¹⁻¹ * t), map_add' := ⋯, map_smul' := ⋯ } *
      { toFun := fun f t ↦ f (x✝⁻¹ * t), map_add' := ⋯, map_smul' := ⋯ }

Tactic:
ext

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
x✝³ x✝² : G
x✝¹ : G → k
x✝ : G
⊢ { toFun := fun f t ↦ f ((x✝³ * x✝²)⁻¹ * t), map_add' := ⋯, map_smul' := ⋯ } x✝¹ x✝ =
    ({ toFun := fun f t ↦ f (x✝³⁻¹ * t), map_add' := ⋯, map_smul' := ⋯ } *
        { toFun := fun f t ↦ f (x✝²⁻¹ * t), map_add' := ⋯, map_smul' := ⋯ })
      x✝¹ 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
x : σ →₀ ℕ
r : R
⊢ renameFun f ((monomial x) r) = (monomial (mapDomain f x)) r

Tactic:
ext

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.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
⊢ ∃ y_1 ∈ span (Set.range p), ∃ z ∈ span (Set.range fun a_1 ↦ a • i a_1), y_1 + z = y

Tactic:
obtain ⟨s, H⟩ := mem_span_range_iff_exists_fun.1 (hf ▸ Ideal.mem_sup_left hy)

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 : ∑ i, s i * f i = 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
S : Type u_5
f : σ → τ
g : τ → γ
inst✝² : TendstoCofinite f
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
⊢ renameFun f 0 = 0

Tactic:
ext

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
⊢ renameFun f (x✝¹ + x✝) = renameFun f x✝¹ + renameFun f x✝

Tactic:
ext

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.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ d₁₀ A ≫ (coinvariantsMk k G).app A = 0

Tactic:
ext

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
a✝ : G
x✝ : ↑A
⊢ (ModuleCat.Hom.hom (d₁₀ A ≫ (coinvariantsMk k G).app A) ∘ₗ lsingle a✝) x✝ = (ModuleCat.Hom.hom 0 ∘ₗ lsingle a✝) x✝
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
⊢ d₁₀ A = 0

Tactic:
ext

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
a✝ : G
x✝ : ↑A
⊢ (ModuleCat.Hom.hom (d₁₀ A) ∘ₗ lsingle a✝) x✝ = (ModuleCat.Hom.hom 0 ∘ₗ lsingle a✝) x✝
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
⊢ (rename f) ((map φ) p) = (map φ) ((rename f) p)

Tactic:
ext

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
⊢ killComplFun e ((monomial (embDomain e x)) r) = (monomial x) r

Tactic:
ext

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)
⊢ killComplFun e ((monomial x) r) = 0

Tactic:
ext

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
R : Type u_4
inst✝ : CommSemiring R
e : σ ↪ τ
p q : MvPowerSeries τ R
⊢ killComplFun e (p * q) = killComplFun e p * killComplFun e q

Tactic:
ext

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
e : σ ↪ τ
p q : MvPowerSeries τ R
n✝ : σ →₀ ℕ
⊢ (coeff n✝) (killComplFun e (p * q)) = (coeff n✝) (killComplFun e p * killComplFun e q)
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 : σ ↪ τ
⊢ killComplFun e 0 = 0

Tactic:
ext

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
⊢ killComplFun e (x✝¹ + x✝) = killComplFun e x✝¹ + killComplFun e x✝

Tactic:
ext

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.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x✝¹ : Fin 3 → G
x✝ : ↑A
⊢ (ModuleCat.Hom.hom ((chainsIso₃ A).hom ≫ d₃₂ A)) (single x✝¹ x✝) =
    (ModuleCat.Hom.hom ((inhomogeneousChains A).d 3 2 ≫ (chainsIso₂ A).hom)) (single x✝¹ x✝)

Tactic:
by
    simp [chainsIso₂, ChainComplex.of.d, pow_succ, chainsIso₃,
      -domLCongr_apply, domLCongr_single, d₃₂, Fin.sum_univ_three,
      Fin.contractNth, Fin.tail_def, sub_eq_add_neg, add_assoc,
      inhomogeneousChains.d_single (G := G), add_rotate' (-(single (_ * _, _) _)),
      add_left_comm (single (_, _ * _) _)]

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 : σ ↪ τ
i : σ
⊢ (killCompl e) (X (e i)) = X i

Tactic:
ext

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 : σ ↪ τ
⊢ (killCompl e).comp (rename ⇑e) = AlgHom.id R (MvPowerSeries σ R)

Tactic:
ext

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
⊢ (killCompl e) ((map φ) p) = (map φ) ((killCompl e) p)

Tactic:
ext

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))
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
a : A
⊢ IsBoundary₀ G a ↔ ∃ x, (x.sum fun g z ↦ g • z - z) = a

Tactic:
constructor

Goal state after:
case mp
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
a : A
⊢ IsBoundary₀ G a → ∃ x, (x.sum fun g z ↦ g • z - z) = a

case mpr
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
a : A
⊢ (∃ x, (x.sum fun g z ↦ g • z - z) = a) → IsBoundary₀ G a
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
x : G →₀ A
⊢ IsBoundary₁ x ↔ ∃ y, (y.sum fun g a ↦ single g.2 a - single (g.1 * g.2) (g.1 • a) + single g.1 (g.1 • a)) = x

Tactic:
constructor

Goal state after:
case mp
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
x : G →₀ A
⊢ IsBoundary₁ x → ∃ y, (y.sum fun g a ↦ single g.2 a - single (g.1 * g.2) (g.1 • a) + single g.1 (g.1 • a)) = x

case mpr
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
x : G →₀ A
⊢ (∃ y, (y.sum fun g a ↦ single g.2 a - single (g.1 * g.2) (g.1 • a) + single g.1 (g.1 • a)) = x) → IsBoundary₁ x
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
x : G × G →₀ A
⊢ IsBoundary₂ x ↔
    ∃ y,
      (y.sum fun g a ↦
          single (g.2.1, g.2.2) a - single (g.1 * g.2.1, g.2.2) (g.1 • a) + single (g.1, g.2.1 * g.2.2) (g.1 • a) -
            single (g.1, g.2.1) (g.1 • a)) =
        x

Tactic:
constructor

Goal state after:
case mp
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
x : G × G →₀ A
⊢ IsBoundary₂ x →
    ∃ y,
      (y.sum fun g a ↦
          single (g.2.1, g.2.2) a - single (g.1 * g.2.1, g.2.2) (g.1 • a) + single (g.1, g.2.1 * g.2.2) (g.1 • a) -
            single (g.1, g.2.1) (g.1 • a)) =
        x

case mpr
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
x : G × G →₀ A
⊢ (∃ y,
      (y.sum fun g a ↦
          single (g.2.1, g.2.2) a - single (g.1 * g.2.1, g.2.2) (g.1 • a) + single (g.1, g.2.1 * g.2.2) (g.1 • a) -
            single (g.1, g.2.1) (g.1 • a)) =
        x) →
    IsBoundary₂ x
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 : G →₀ A
hx : x ∈ cycles₁ (Rep.ofDistribMulAction k G A)
⊢ IsCycle₁ x

Tactic:
simpa using! (mem_cycles₁_iff (A := Rep.ofDistribMulAction k G A) x).1 hx

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)
⊢ (ConcreteCategory.hom ((inhomogeneousChains A).d 1 0)) ((ConcreteCategory.hom (chainsIso₁ A).inv) ↑x) = 0

Tactic:
rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, eq_d₁₀_comp_inv]; simp

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

Goal state before:
pp: case pos.refine_2
R : Type u_1
inst✝ : CommRing R
I : Ideal R⟦X⟧
hI : X ∈ I
hfg : (Ideal.map constantCoeff I).FG
⊢ (generators (Ideal.map constantCoeff I)).ncard ≤ spanFinrank (Ideal.map constantCoeff I)

Tactic:
FG.generators_ncard hfg

Goal state after:
case pos.refine_2
R : Type u_1
inst✝ : CommRing R
I : Ideal R⟦X⟧
hI : X ∈ I
hfg : (Ideal.map constantCoeff I).FG
⊢ spanFinrank (Ideal.map constantCoeff I) ≤ spanFinrank (Ideal.map constantCoeff I)
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
⊢ (inhomogeneousChains A).d 1 0 = 0

Tactic:
ext

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
g✝ : Fin 1 → G
x✝ : ↑(ModuleCat.of k ↑A)
⊢ ((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle g✝) ≫ (inhomogeneousChains A).d 1 0)) x✝) default =
    ((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle g✝) ≫ 0)) x✝) default
Module: Mathlib.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
⊢ (fun f ↦ f.comp ↑(cycles₁IsoOfIsTrivial A).symm.toLinearEquiv.toAddEquiv)
      (((fun f ↦ f.comp ↑(H1Iso A).symm.toLinearEquiv.toAddEquiv)
            (TensorProduct.lift (mkH1OfIsTrivial A) ∘ₗ H1ToTensorOfIsTrivial A).toAddMonoidHom).comp
        (QuotientAddGroup.mk' (shortComplexH1 A).moduleCatToCycles.range.toAddSubgroup)) =
    (fun f ↦ f.comp ↑(cycles₁IsoOfIsTrivial A).symm.toLinearEquiv.toAddEquiv)
      (((fun f ↦ f.comp ↑(H1Iso A).symm.toLinearEquiv.toAddEquiv) LinearMap.id.toAddMonoidHom).comp
        (QuotientAddGroup.mk' (shortComplexH1 A).moduleCatToCycles.range.toAddSubgroup))

Tactic:
ext

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
x✝¹ : G
x✝ : ↑A
⊢ (((fun f ↦ f.comp ↑(cycles₁IsoOfIsTrivial A).symm.toLinearEquiv.toAddEquiv)
            (((fun f ↦ f.comp ↑(H1Iso A).symm.toLinearEquiv.toAddEquiv)
                  (TensorProduct.lift (mkH1OfIsTrivial A) ∘ₗ H1ToTensorOfIsTrivial A).toAddMonoidHom).comp
              (QuotientAddGroup.mk' (shortComplexH1 A).moduleCatToCycles.range.toAddSubgroup))).comp
        (singleAddHom x✝¹))
      x✝ =
    (((fun f ↦ f.comp ↑(cycles₁IsoOfIsTrivial A).symm.toLinearEquiv.toAddEquiv)
            (((fun f ↦ f.comp ↑(H1Iso A).symm.toLinearEquiv.toAddEquiv) LinearMap.id.toAddMonoidHom).comp
              (QuotientAddGroup.mk' (shortComplexH1 A).moduleCatToCycles.range.toAddSubgroup))).comp
        (singleAddHom x✝¹))
      x✝
Module: Mathlib.RingTheory.PowerSeries.Ideal

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
P : Ideal R⟦X⟧
inst✝ : P.IsPrime
⊢ P.FG ↔ (Ideal.map constantCoeff P).FG

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R⟦X⟧
inst✝ : P.IsPrime
⊢ P.FG → (Ideal.map constantCoeff P).FG

case mpr
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R⟦X⟧
inst✝ : P.IsPrime
⊢ (Ideal.map constantCoeff P).FG → P.FG