mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: k : Type u
G : Type v
inst✝³ : CommRing k
inst✝² : Group G
S : Subgroup G
inst✝¹ : DecidableRel ⇑(QuotientGroup.rightRel S)
inst✝ : S.FiniteIndex
A : Rep.{max w u v, u, v} k ↥S
B : Rep.{max (max u v) w, u, v} k G
f : coind.{u, v, v, max (max u v) w} S.subtype A ⟶ B
⊢ ((coindResAdjunction k S).homEquiv A B) f = (indResHomEquiv S.subtype A B) (A.indCoindIso.hom ≫ f)

Tactic:
rfl

Goal state after:
Module: Mathlib.RepresentationTheory.Induced

Goal state before:
pp: k : Type u
G : Type v
H : Type v'
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A x✝² : Rep k G
x✝¹ : H
x✝ : ↑x✝²
⊢ ((TensorProduct.AlgebraTensorModule.curry
            ((Hom.hom (indMap φ (𝟙 x✝²))).toLinearMap ∘ₗ
              Representation.Coinvariants.mk
                (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) x✝².ρ)) ∘ₗ
          MonoidAlgebra.lsingle x✝¹)
        1)
      x✝ =
    ((TensorProduct.AlgebraTensorModule.curry
            ((Hom.hom (𝟙 (ind φ x✝²))).toLinearMap ∘ₗ
              Representation.Coinvariants.mk
                (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) x✝².ρ)) ∘ₗ
          MonoidAlgebra.lsingle x✝¹)
        1)
      x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.RepresentationTheory.Induced

Goal state before:
pp: k : Type u
G : Type v
H : Type v'
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A X✝ Y✝ Z✝ : Rep k G
x✝³ : X✝ ⟶ Y✝
x✝² : Y✝ ⟶ Z✝
x✝¹ : H
x✝ : ↑X✝
⊢ ((TensorProduct.AlgebraTensorModule.curry
            ((Hom.hom (indMap φ (x✝³ ≫ x✝²))).toLinearMap ∘ₗ
              Representation.Coinvariants.mk
                (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) X✝.ρ)) ∘ₗ
          MonoidAlgebra.lsingle x✝¹)
        1)
      x✝ =
    ((TensorProduct.AlgebraTensorModule.curry
            ((Hom.hom (indMap φ x✝³ ≫ indMap φ x✝²)).toLinearMap ∘ₗ
              Representation.Coinvariants.mk
                (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) X✝.ρ)) ∘ₗ
          MonoidAlgebra.lsingle x✝¹)
        1)
      x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.RepresentationTheory.Induced

Goal state before:
pp: k : Type u
G : Type v
H : Type v'
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A : Rep k G
B : Rep k H
X✝ : Rep k G
Y✝ Y'✝ : Rep k H
f✝ : (indFunctor k φ).obj X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Y'✝
⊢ (indResHomEquiv φ X✝ Y'✝).toEquiv (f✝ ≫ g✝) = (indResHomEquiv φ X✝ Y✝).toEquiv f✝ ≫ (resFunctor φ).map g✝

Tactic:
rfl

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.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
i : ℕ
inst✝ : NeZero i
hi : Even i
x y : ↥(Hom.hom (A.applyAsHom g - 𝟙 A)).ker
⊢ ↑(x - y) ∈ (Hom.hom A.norm).range ↔ ↑x - ↑y ∈ (Hom.hom A.norm).range

Tactic:
rfl

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
n : ℕ
f : k[Fin (n + 1 + 1) → G]
⊢ (d k G (n + 1)) f = (d k G (n + 1)) f

Tactic:
rfl

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

Goal state before:
pp: case refine_1
K L : Type
inst✝¹⁶ : Field K
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra K L
inst✝¹³ : FiniteDimensional K L
inst✝¹² : IsGalois K L
inst✝¹¹ : IsCyclic Gal(L/K)
g : Gal(L/K)
A : Type u_1
B : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra A L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsScalarTower A K L
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : IsIntegralClosure B A L
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
η : B
hη : (Algebra.norm K) ((algebraMap B L) η) = 1
this✝¹ : Module.IsTorsionFree A L
this✝ : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
η' : Lˣ := Units.mk0 ((algebraMap B L) η) ⋯
ε : Lˣ
hε : ↑ε / g ↑ε = (algebraMap B L) η
a : B
b : ↥(Algebra.algebraMapSubmonoid B A⁰)
h : IsLocalization.mk' L a b = ↑ε
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑b
this : t • IsLocalization.mk' L a b = (algebraMap B L) a
⊢ a ≠ 0

pp: case refine_2
K L : Type
inst✝¹⁶ : Field K
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra K L
inst✝¹³ : FiniteDimensional K L
inst✝¹² : IsGalois K L
inst✝¹¹ : IsCyclic Gal(L/K)
g : Gal(L/K)
A : Type u_1
B : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra A L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsScalarTower A K L
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : IsIntegralClosure B A L
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
η : B
hη : (Algebra.norm K) ((algebraMap B L) η) = 1
this✝¹ : Module.IsTorsionFree A L
this✝ : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
η' : Lˣ := Units.mk0 ((algebraMap B L) η) ⋯
ε : Lˣ
hε : ↑ε / g ↑ε = (algebraMap B L) η
a : B
b : ↥(Algebra.algebraMapSubmonoid B A⁰)
h : IsLocalization.mk' L a b = ↑ε
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑b
this : t • IsLocalization.mk' L a b = (algebraMap B L) a
⊢ η * ((galRestrict A K L B) g) a = a

Tactic:
· rintro rfl
    simp only [IsLocalization.mk'_zero, _root_.map_zero, div_zero, ← h] at hε
    rw [← hε, Algebra.norm_zero] at hη
    exact zero_ne_one hη

Goal state after:
case refine_2
K L : Type
inst✝¹⁶ : Field K
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra K L
inst✝¹³ : FiniteDimensional K L
inst✝¹² : IsGalois K L
inst✝¹¹ : IsCyclic Gal(L/K)
g : Gal(L/K)
A : Type u_1
B : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra A L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsScalarTower A K L
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : IsIntegralClosure B A L
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
η : B
hη : (Algebra.norm K) ((algebraMap B L) η) = 1
this✝¹ : Module.IsTorsionFree A L
this✝ : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
η' : Lˣ := Units.mk0 ((algebraMap B L) η) ⋯
ε : Lˣ
hε : ↑ε / g ↑ε = (algebraMap B L) η
a : B
b : ↥(Algebra.algebraMapSubmonoid B A⁰)
h : IsLocalization.mk' L a b = ↑ε
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑b
this : t • IsLocalization.mk' L a b = (algebraMap B L) a
⊢ η * ((galRestrict A K L B) g) a = a
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x y : ↑A
g : G
⊢ (A.ρ g) x - x + ((A.ρ g) y - y) = ((fun g ↦ (A.ρ g) x - x) + fun g ↦ (A.ρ g) y - y) g

Tactic:
rfl

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
x : ↑(ModuleCat.of k ↑A)
⊢ (∀ (x_1 : G), (ModuleCat.Hom.hom (d₀₁ A)) x x_1 = 0 x_1) ↔ ∀ (g : G), (A.ρ g) x - x = 0

Tactic:
rfl

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✝¹ : ↑(ModuleCat.of k ↑A)
x✝ : G
⊢ 0 = (ModuleCat.Hom.hom 0) x✝¹ x✝

Tactic:
rfl

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

Goal state before:
pp: case e_a.e_6
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 1)
y : G × G
i : Fin 1
⊢ (Equiv.funUnique (Fin 1) G).symm y.2 0 = (piFinTwoEquiv fun x ↦ G).symm y (Fin.succ 0)

Tactic:
rfl

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

Goal state before:
pp: case e_a.e_a
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 1)
y : G × G
i : Fin 1
⊢ (Equiv.funUnique (Fin 1) G).symm (y.1 * y.2) 0 =
    Fin.contractNth 0 (fun x1 x2 ↦ x1 * x2) ((piFinTwoEquiv fun x ↦ G).symm y) 0

Tactic:
rfl

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

Goal state before:
pp: case e_a.e_a
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 1)
y : G × G
i : Fin 1
⊢ (Equiv.funUnique (Fin 1) G).symm y.1 0 = Fin.contractNth 1 (fun x1 x2 ↦ x1 * x2) ((piFinTwoEquiv fun x ↦ G).symm y) 0

Tactic:
rfl

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

Goal state before:
pp: case e_a.e_a.«_@»._internal._hyg.0.«0»
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 2)
y : G × G × G
⊢ (piFinTwoEquiv fun x ↦ G).symm (y.1 * y.2.1, y.2.2) ((fun i ↦ i) ⟨0, ⋯⟩) =
    Fin.contractNth 0 (fun x1 x2 ↦ x1 * x2)
      ((Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y)) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
rfl

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

Goal state before:
pp: case e_a.e_a.«_@»._internal._hyg.0.«1»
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 2)
y : G × G × G
⊢ (piFinTwoEquiv fun x ↦ G).symm (y.1 * y.2.1, y.2.2) ((fun i ↦ i) ⟨1, ⋯⟩) =
    Fin.contractNth 0 (fun x1 x2 ↦ x1 * x2)
      ((Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y)) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
rfl

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

Goal state before:
pp: case e_a.e_a.e_a.«_@»._internal._hyg.0.«0»
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 2)
y : G × G × G
⊢ (piFinTwoEquiv fun x ↦ G).symm (y.1, y.2.1 * y.2.2) ((fun i ↦ i) ⟨0, ⋯⟩) =
    Fin.contractNth 1 (fun x1 x2 ↦ x1 * x2)
      ((Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y)) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
rfl

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

Goal state before:
pp: case e_a.e_a.e_a.«_@»._internal._hyg.0.«1»
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 2)
y : G × G × G
⊢ (piFinTwoEquiv fun x ↦ G).symm (y.1, y.2.1 * y.2.2) ((fun i ↦ i) ⟨1, ⋯⟩) =
    Fin.contractNth 1 (fun x1 x2 ↦ x1 * x2)
      ((Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y)) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
rfl

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

Goal state before:
pp: case e_a.e_a.e_a.«_@»._internal._hyg.0.«0»
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 2)
y : G × G × G
⊢ (piFinTwoEquiv fun x ↦ G).symm (y.1, y.2.1) ((fun i ↦ i) ⟨0, ⋯⟩) =
    Fin.contractNth 2 (fun x1 x2 ↦ x1 * x2)
      ((Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y)) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
rfl

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

Goal state before:
pp: case e_a.e_a.e_a.«_@»._internal._hyg.0.«1»
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 2)
y : G × G × G
⊢ (piFinTwoEquiv fun x ↦ G).symm (y.1, y.2.1) ((fun i ↦ i) ⟨1, ⋯⟩) =
    Fin.contractNth 2 (fun x1 x2 ↦ x1 * x2)
      ((Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y)) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
rfl

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
f : G → ↑A
⊢ (∀ (a b : G), (A.ρ a) (f b) - f (a * b) + f a = 0 (a, b)) ↔ ∀ (g h : G), (A.ρ g) (f h) - f (g * h) + f g = 0

Tactic:
rfl

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
f : ↥(cocycles₁ A)
g : G
⊢ (A.ρ g) (f g⁻¹) = -f g

Tactic:
← add_eq_zero_iff_eq_neg,

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : ↥(cocycles₁ A)
g : G
⊢ (A.ρ g) (f g⁻¹) + f g = 0
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : G × G → ↑A
⊢ (∀ (a a_1 b : G), (A.ρ a) (f (a_1, b)) - f (a * a_1, b) + f (a, a_1 * b) - f (a, a_1) = 0 (a, a_1, b)) ↔
    ∀ (g h j : G), (A.ρ g) (f (h, j)) - f (g * h, j) + f (g, h * j) - f (g, h) = 0

Tactic:
rfl

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

Goal state before:
pp: G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : MulAction G A
f : G → A
hf : IsCocycle₁ f
g : G
⊢ g • f g⁻¹ = -f g

Tactic:
← add_eq_zero_iff_eq_neg,

Goal state after:
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : MulAction G A
f : G → A
hf : IsCocycle₁ f
g : G
⊢ g • f g⁻¹ + f g = 0
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cocycles₁ A)
this :
  (ConcreteCategory.hom ((shortComplexH1 A).moduleCatLeftHomologyData.i ≫ (cochainsIso₁ A).inv)) x =
    (ConcreteCategory.hom (iCocycles A 1)) ((ConcreteCategory.hom (isoCocycles₁ A).inv) x)
⊢ (ConcreteCategory.hom (cochainsIso₁ A).inv) ⇑x =
    (ConcreteCategory.hom ((shortComplexH1 A).moduleCatLeftHomologyData.i ≫ (cochainsIso₁ A).inv)) x

Tactic:
rfl

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
x : ↥(cocycles₂ A)
⊢ (ConcreteCategory.hom (cochainsIso₂ A).inv) ⇑x =
    (ConcreteCategory.hom ((shortComplexH2 A).moduleCatLeftHomologyData.i ≫ (cochainsIso₂ A).inv)) x

Tactic:
rfl

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
x y : ↥(cocycles₁ A)
⊢ ⇑(x - y) ∈ coboundaries₁ A ↔ ⇑x - ⇑y ∈ coboundaries₁ A

Tactic:
rfl

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
x y : ↥(cocycles₂ A)
⊢ ⇑(x - y) ∈ coboundaries₂ A ↔ ⇑x - ⇑y ∈ coboundaries₂ A

Tactic:
rfl

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
T : Type u_1
F : (f : G →* H) → (res f A ⟶ B) → T
⊢ F f₁ φ = F f₁ (⋯ ▸ φ)

Tactic:
rfl

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

Goal state before:
pp: k H : Type u
inst✝¹ : CommRing k
inst✝ : Group H
A : Rep k H
⊢ cochainsMap (MonoidHom.id H) (𝟙 A) = 𝟙 (inhomogeneousCochains A)

Tactic:
rfl

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

Goal state before:
pp: k : Type u
inst✝³ : CommRing k
G H K : Type u
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Group K
A : Rep k K
B : Rep k H
C : Rep k G
f : H →* K
g : G →* H
φ : res f A ⟶ B
ψ : res g B ⟶ C
⊢ cochainsMap (f.comp g) ((resFunctor g).map φ ≫ ψ) = cochainsMap f φ ≫ cochainsMap g ψ

Tactic:
rfl

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

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

Tactic:
rfl

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
⊢ cochainsMap f 0 = 0

Tactic:
rfl

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
x : Fin 0 → H
x✝ : ↑A
⊢ (ModuleCat.Hom.hom
          ((ModuleCat.ofHom (LinearMap.funLeft k ↑A fun x ↦ default) ≫
              ModuleCat.ofHom ((Hom.hom φ).compLeft (Fin 0 → G))) ≫
            (cochainsIso₀ B).hom) ∘ₗ
        LinearMap.single k (fun i ↦ ↑A) x)
      x✝ =
    (ModuleCat.Hom.hom ((cochainsIso₀ A).hom ≫ Hom.toModuleCatHom φ) ∘ₗ LinearMap.single k (fun i ↦ ↑A) x) x✝

Tactic:
rfl

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

Goal state before:
pp: 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 2)
g : G × G
⊢ (fun x ↦ ⇑f ∘ x) ((piFinTwoEquiv fun x ↦ G).symm g) ((fun i ↦ i) ⟨0, ⋯⟩) =
    (piFinTwoEquiv fun x ↦ H).symm (Prod.map (⇑f) (⇑f) g) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
rfl

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

Goal state before:
pp: 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 2)
g : G × G
⊢ (fun x ↦ ⇑f ∘ x) ((piFinTwoEquiv fun x ↦ G).symm g) ((fun i ↦ i) ⟨1, ⋯⟩) =
    (piFinTwoEquiv fun x ↦ H).symm (Prod.map (⇑f) (⇑f) g) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
rfl

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

Goal state before:
pp: 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, ⋯⟩)

Tactic:
rfl

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

Goal state before:
pp: 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, ⋯⟩)

Tactic:
rfl

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

Goal state before:
pp: 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, ⋯⟩)

Tactic:
rfl

Goal state after:
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
⊢ (H0Iso A).hom ≫ (shortComplexH0 A).f ≫ Hom.toModuleCatHom f =
    (H0Iso A).hom ≫ (invariantsFunctor k G).map f ≫ (shortComplexH0 B).f

Tactic:
rfl

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
⊢ mapShortComplexH1 f 0 = 0

Tactic:
rfl

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

Goal state before:
pp: k H : Type u
inst✝¹ : CommRing k
inst✝ : Group H
A : Rep k H
⊢ mapShortComplexH1 (MonoidHom.id H) (𝟙 A) = 𝟙 (shortComplexH1 A)

Tactic:
rfl

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:
simp only [tateNorm, ← Category.assoc, Preadditive.IsIso.comp_right_eq_zero]

Goal state after:
R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
M : Rep R G
⊢ (ChainComplex.of.d (fun n ↦ ModuleCat.of R ((Fin n → G) →₀ ↑M)) (fun n ↦ inhomogeneousChains.d M n) 1 0 ≫
        (chainsIso₀ M).hom) ≫
      Hom.toModuleCatHom M.norm =
    0
Module: Mathlib.RepresentationTheory.Homological.TateCohomology.Basic

Goal state before:
pp: case ofNat
R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
X Y : Rep R G
f g : X ⟶ Y
i : ℕ
⊢ (map (f + g)).f (Int.ofNat i) = (map f + map g).f (Int.ofNat i)

Tactic:
rfl

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✝ Z✝ : Rep R G
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (tateComplexConnectData X✝).map (tateComplexConnectData Z✝) (chainsMap (MonoidHom.id G) (f ≫ g))
      (cochainsMap (MonoidHom.id G) (f ≫ g)) ⋯ =
    (tateComplexConnectData X✝).map (tateComplexConnectData Z✝)
      (chainsMap ((MonoidHom.id G).comp (MonoidHom.id G)) (f ≫ Rep.resMap (MonoidHom.id G) g))
      (cochainsMap (MonoidHom.id G) f ≫ cochainsMap (MonoidHom.id G) g) ⋯

Tactic:
rfl

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

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

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

Goal state after:
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
    simp [mul_assoc]

Goal state after:
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
    simp [mul_assoc]

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

Goal state before:
pp: k H : Type u
inst✝¹ : CommRing k
inst✝ : Group H
A : Rep k H
⊢ mapShortComplexH2 (MonoidHom.id H) (𝟙 A) = 𝟙 (shortComplexH2 A)

Tactic:
rfl

Goal state after: