awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
i : ℕ
h₀ : NeZero i
hi : Even i
x : (↑(ModuleCat.of k (↑A : Type u)) : Type u)
⊢ Eq (α := (↑(ModuleCat.of k (↑A : Type u)) : Type u))
    ((ModuleCat.Hom.hom
            (ModuleCat.ofHom
                (Hom.hom (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (A.applyAsHom (k := k) g : A ⟶ A) (𝟙 A))).toLinearMap ≫
              ModuleCat.ofHom (Hom.hom A.norm).toLinearMap) :
          (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
        x :
      (↑(ModuleCat.of k (↑A : Type u)) : Type u))
    ((ModuleCat.Hom.hom 0 :
          (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
        x :
      (↑(ModuleCat.of k (↑A : Type u)) : Type u))

Tactic:
simp [sub_hom]

Premises used: Rep.sub_hom
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
i : ℕ
h₀ : NeZero i
hi : Even i
hf :
  ∀ (x : (↑(ModuleCat.of k (↑A : Type u)) : Type u)),
    Eq (α := (↑(ModuleCat.of k (↑A : Type u)) : Type u))
      ((ModuleCat.Hom.hom
              (ModuleCat.ofHom (Hom.hom A.norm).toLinearMap ≫
                ModuleCat.ofHom
                  (Hom.hom (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (A.applyAsHom (k := k) g : A ⟶ A) (𝟙 A))).toLinearMap) :
            (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
          x :
        (↑(ModuleCat.of k (↑A : Type u)) : Type u))
      ((ModuleCat.Hom.hom 0 :
            (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
          x :
        (↑(ModuleCat.of k (↑A : Type u)) : Type u))
⊢ ModuleCat.ofHom (Hom.hom A.norm).toLinearMap ≫
      ModuleCat.ofHom
        (Hom.hom (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (A.applyAsHom (k := k) g : A ⟶ A) (𝟙 A))).toLinearMap =
    0

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
i : ℕ
h₀ : NeZero i
hi : Even i
x : (↑(ModuleCat.of k (↑A : Type u)) : Type u)
⊢ Eq (α := (↑(ModuleCat.of k (↑A : Type u)) : Type u))
    ((ModuleCat.Hom.hom
            (ModuleCat.ofHom (Hom.hom A.norm).toLinearMap ≫
              ModuleCat.ofHom
                (Hom.hom (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (A.applyAsHom (k := k) g : A ⟶ A) (𝟙 A))).toLinearMap) :
          (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
        x :
      (↑(ModuleCat.of k (↑A : Type u)) : Type u))
    ((ModuleCat.Hom.hom 0 :
          (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
        x :
      (↑(ModuleCat.of k (↑A : Type u)) : Type u))

Tactic:
simp [sub_hom]

Premises used: Rep.sub_hom
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
i : ℕ
h₀ : NeZero i
hi : Even i
⊢ ∀ (i j : ℕ), (ComplexShape.up ℕ).Rel i j → Odd (i + j)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
h₀ : NeZero (R := ℕ) 0
hi : Even (α := ℕ) 0
⊢ (ComplexShape.up ℕ).Rel ((ComplexShape.up ℕ).prev 0) 0

Tactic:
(NeZero.ne 0 rfl).elim

Premises used: False.elim, OfNat.ofNat, rfl, NeZero.ne
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
h₀ : NeZero (R := ℕ) 0
hi : Even (α := ℕ) 0
⊢ (ComplexShape.up ℕ).Rel ((ComplexShape.up ℕ).prev 0) 0

Tactic:
exact (NeZero.ne 0 rfl).elim

Premises used: False.elim, OfNat.ofNat, rfl, NeZero.ne
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
n : ℕ
h : ∀ [h₀ : NeZero n] (hi : Even n), (ComplexShape.up ℕ).Rel ((ComplexShape.up ℕ).prev n) n
h₀ : NeZero (n + 1)
hi : Even (n + 1)
⊢ (ComplexShape.up ℕ).Rel ((ComplexShape.up ℕ).prev (n + 1)) (n + 1)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
i : ℕ
h₀ : NeZero i
hi : Even i
zero : ∀ [h₀ : NeZero (R := ℕ) 0] (hi : Even (α := ℕ) 0), (ComplexShape.up ℕ).Rel ((ComplexShape.up ℕ).prev 0) 0
succ :
  ∀ (n : ℕ),
    (∀ [h₀ : NeZero n] (hi : Even n), (ComplexShape.up ℕ).Rel ((ComplexShape.up ℕ).prev n) n) →
      ∀ [h₀ : NeZero (n + 1)] (hi : Even (n + 1)), (ComplexShape.up ℕ).Rel ((ComplexShape.up ℕ).prev (n + 1)) (n + 1)
⊢ (ComplexShape.up ℕ).Rel ((ComplexShape.up ℕ).prev i) i

Tactic:
induction i generalizing h₀ with | zero => exact (NeZero.ne 0 rfl).elim | succ n _ => simp

Premises used: False.elim, CategoryTheory.ShortComplex.zero, OfNat.ofNat, rfl, NeZero.ne
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
i : ℕ
h₀ : NeZero i
hi : Even i
⊢ (ComplexShape.up ℕ).Rel i ((ComplexShape.up ℕ).next i)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
i : ℕ
inst_3 : NeZero i
hi : Even i
x : ↥(Hom.hom (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (A.applyAsHom (k := k) g : A ⟶ A) (𝟙 A))).ker
⊢ Eq (α := (↑(groupCohomology A i) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (groupCohomologyπEven A g hg i hi) :
            (a : (↑(ModuleCat.of k ↥(Hom.hom (A.applyAsHom g - 𝟙 A)).ker) : Type u)) →
              (↑(groupCohomology A i) : Type u))
          x :
        (↑(groupCohomology A i) : Type u))
      (0 : (↑(groupCohomology A i) : Type u)) ↔
    (↑x : (↑A : Type u)) ∈ (Hom.hom A.norm).range

Tactic:
simp [groupCohomologyπEven, map_eq_zero_iff _ ((ModuleCat.mono_iff_injective _).1 inferInstance),
    moduleCatToCycles, -LinearMap.mem_range, LinearMap.range_codRestrict]

Premises used: inferInstance, ModuleCat.mono_iff_injective, CategoryTheory.ShortComplex.moduleCatToCycles, map_eq_zero_iff, LinearMap.mem_range, Iff.mp, Rep.FiniteCyclicGroup.groupCohomologyπEven, LinearMap.range_codRestrict
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
i : ℕ
inst_3 : NeZero i
hi : Even i
x y : ↥(Hom.hom (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (A.applyAsHom (k := k) g : A ⟶ A) (𝟙 A))).ker
rw :
  (↑(x - y) : (↑A : Type u)) ∈ (Hom.hom A.norm).range ↔
    (↑x : (↑A : Type u)) - (↑y : (↑A : Type u)) ∈ (Hom.hom A.norm).range
⊢ Eq (α := (↑(groupCohomology A i) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (groupCohomologyπEven A g hg i hi) :
            (a : (↑(ModuleCat.of k ↥(Hom.hom (A.applyAsHom g - 𝟙 A)).ker) : Type u)) →
              (↑(groupCohomology A i) : Type u))
          x :
        (↑(groupCohomology A i) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (groupCohomologyπEven A g hg i hi) :
            (a : (↑(ModuleCat.of k ↥(Hom.hom (A.applyAsHom g - 𝟙 A)).ker) : Type u)) →
              (↑(groupCohomology A i) : Type u))
          y :
        (↑(groupCohomology A i) : Type u)) ↔
    (↑x : (↑A : Type u)) - (↑y : (↑A : Type u)) ∈ (Hom.hom A.norm).range

Tactic:
rw [← sub_eq_zero, ← map_sub, groupCohomologyπEven_eq_zero_iff]

Premises used: map_sub, sub_eq_zero, Rep.FiniteCyclicGroup.groupCohomologyπEven_eq_zero_iff
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
i : ℕ
inst_3 : NeZero i
hi : Even i
x y : ↥(Hom.hom (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (A.applyAsHom (k := k) g : A ⟶ A) (𝟙 A))).ker
⊢ (↑(x - y) : (↑A : Type u)) ∈ (Hom.hom A.norm).range ↔
    (↑x : (↑A : Type u)) - (↑y : (↑A : Type u)) ∈ (Hom.hom A.norm).range

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
i : ℕ
hi : Odd i
hf :
  ∀ (x : (↑(ModuleCat.of k (↑A : Type u)) : Type u)),
    Eq (α := (↑(ModuleCat.of k (↑A : Type u)) : Type u))
      ((ModuleCat.Hom.hom
              (ModuleCat.ofHom
                  (Hom.hom (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (A.applyAsHom (k := k) g : A ⟶ A) (𝟙 A))).toLinearMap ≫
                ModuleCat.ofHom (Hom.hom A.norm).toLinearMap) :
            (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
          x :
        (↑(ModuleCat.of k (↑A : Type u)) : Type u))
      ((ModuleCat.Hom.hom 0 :
            (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
          x :
        (↑(ModuleCat.of k (↑A : Type u)) : Type u))
⊢ ModuleCat.ofHom (Hom.hom (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (A.applyAsHom (k := k) g : A ⟶ A) (𝟙 A))).toLinearMap ≫
      ModuleCat.ofHom (Hom.hom A.norm).toLinearMap =
    0

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
i : ℕ
hi : Odd i
x : (↑(ModuleCat.of k (↑A : Type u)) : Type u)
⊢ Eq (α := (↑(ModuleCat.of k (↑A : Type u)) : Type u))
    ((ModuleCat.Hom.hom
            (ModuleCat.ofHom
                (Hom.hom (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (A.applyAsHom (k := k) g : A ⟶ A) (𝟙 A))).toLinearMap ≫
              ModuleCat.ofHom (Hom.hom A.norm).toLinearMap) :
          (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
        x :
      (↑(ModuleCat.of k (↑A : Type u)) : Type u))
    ((ModuleCat.Hom.hom 0 :
          (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
        x :
      (↑(ModuleCat.of k (↑A : Type u)) : Type u))

Tactic:
simp [sub_hom]

Premises used: Rep.sub_hom
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
i : ℕ
hi : Odd i
hf :
  ∀ (x : (↑(ModuleCat.of k (↑A : Type u)) : Type u)),
    Eq (α := (↑(ModuleCat.of k (↑A : Type u)) : Type u))
      ((ModuleCat.Hom.hom
              (ModuleCat.ofHom (Hom.hom A.norm).toLinearMap ≫
                ModuleCat.ofHom
                  (Hom.hom (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (A.applyAsHom (k := k) g : A ⟶ A) (𝟙 A))).toLinearMap) :
            (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
          x :
        (↑(ModuleCat.of k (↑A : Type u)) : Type u))
      ((ModuleCat.Hom.hom 0 :
            (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
          x :
        (↑(ModuleCat.of k (↑A : Type u)) : Type u))
⊢ ModuleCat.ofHom (Hom.hom A.norm).toLinearMap ≫
      ModuleCat.ofHom
        (Hom.hom (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (A.applyAsHom (k := k) g : A ⟶ A) (𝟙 A))).toLinearMap =
    0

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
i : ℕ
hi : Odd i
x : (↑(ModuleCat.of k (↑A : Type u)) : Type u)
⊢ Eq (α := (↑(ModuleCat.of k (↑A : Type u)) : Type u))
    ((ModuleCat.Hom.hom
            (ModuleCat.ofHom (Hom.hom A.norm).toLinearMap ≫
              ModuleCat.ofHom
                (Hom.hom (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (A.applyAsHom (k := k) g : A ⟶ A) (𝟙 A))).toLinearMap) :
          (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
        x :
      (↑(ModuleCat.of k (↑A : Type u)) : Type u))
    ((ModuleCat.Hom.hom 0 :
          (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
        x :
      (↑(ModuleCat.of k (↑A : Type u)) : Type u))

Tactic:
simp [sub_hom]

Premises used: Rep.sub_hom
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
i : ℕ
hi : Odd i
⊢ ∀ (i j : ℕ), (ComplexShape.up ℕ).Rel i j → Odd (i + j)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
i : ℕ
hi : Odd i
rcases : ∀ (j : ℕ), (ComplexShape.up ℕ).Rel ((ComplexShape.up ℕ).prev (2 * j + 1)) (2 * j + 1)
⊢ (ComplexShape.up ℕ).Rel ((ComplexShape.up ℕ).prev i) i

Tactic:
rcases hi with ⟨j, rfl⟩

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
j : ℕ
⊢ (ComplexShape.up ℕ).Rel ((ComplexShape.up ℕ).prev (2 * j + 1)) (2 * j + 1)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
i : ℕ
hi : Odd i
⊢ (ComplexShape.up ℕ).Rel i ((ComplexShape.up ℕ).next i)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
i : ℕ
hi : Odd i
x : ↥(Hom.hom A.norm).ker
⊢ Eq (α := (↑(groupCohomology A i) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (X := ModuleCat.of k ↥(Hom.hom A.norm).ker) (groupCohomologyπOdd A g hg i hi) :
            (a : (↑(ModuleCat.of k ↥(Hom.hom A.norm).ker) : Type u)) → (↑(groupCohomology A i) : Type u))
          x :
        (↑(groupCohomology A i) : Type u))
      (0 : (↑(groupCohomology A i) : Type u)) ↔
    (↑x : (↑A : Type u)) ∈ (Hom.hom (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (A.applyAsHom (k := k) g : A ⟶ A) (𝟙 A))).range

Tactic:
simp [groupCohomologyπOdd, map_eq_zero_iff _ ((ModuleCat.mono_iff_injective _).1 inferInstance),
    moduleCatToCycles, -LinearMap.mem_range, LinearMap.range_codRestrict]

Premises used: inferInstance, Rep.FiniteCyclicGroup.groupCohomologyπOdd, ModuleCat.mono_iff_injective, CategoryTheory.ShortComplex.moduleCatToCycles, map_eq_zero_iff, LinearMap.mem_range, Iff.mp, LinearMap.range_codRestrict
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep.{u_2, u, u} k H
B : Rep.{u_2, u, u} k G
f₁ f₂ : G →* H
h : f₁ = f₂
φ : res f₁ A ⟶ B
T : Type u_1
F : (f : G →* H) → (φ : res f A ⟶ B) → T
subst : F f₁ φ = F f₁ (Eq.rec (motive := fun (x : G →* H) (h : f₁ = x) ↦ res x A ⟶ B) φ ⋯)
⊢ F f₁ φ = F f₂ (Eq.rec (motive := fun (x : G →* H) (h : f₁ = x) ↦ res x A ⟶ B) φ h)

Tactic:
subst h
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep.{u_2, u, u} k H
B : Rep.{u_2, u, u} 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₁ (Eq.rec (motive := fun (x : G →* H) (h : f₁ = x) ↦ res x A ⟶ B) φ ⋯)

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
n i j : ℕ
hij : i + 1 = j
subst :
  Eq (α := (inhomogeneousCochains A).X i ⟶ (inhomogeneousCochains B).X (i + 1))
    (ModuleCat.ofHom
        ((Hom.hom φ).compLeft (Fin i → G) ∘ₗ
          LinearMap.funLeft k (↑A : Type u) fun (x : Fin i → G) ↦ (⇑f : (a : G) → H) ∘ x) ≫
      (inhomogeneousCochains B).d i (i + 1))
    (CategoryStruct.comp (Y := (inhomogeneousCochains A).X (i + 1)) ((inhomogeneousCochains A).d i (i + 1))
      (ModuleCat.ofHom
        ((Hom.hom φ).compLeft (Fin (i + 1) → G) ∘ₗ
          LinearMap.funLeft k (↑A : Type u) fun (x : Fin (i + 1) → G) ↦ (⇑f : (a : G) → H) ∘ x)))
⊢ ModuleCat.ofHom
        ((Hom.hom φ).compLeft (Fin i → G) ∘ₗ
          LinearMap.funLeft k (↑A : Type u) fun (x : Fin i → G) ↦ (⇑f : (a : G) → H) ∘ x) ≫
      (inhomogeneousCochains B).d i j =
    (inhomogeneousCochains A).d i j ≫
      ModuleCat.ofHom
        ((Hom.hom φ).compLeft (Fin j → G) ∘ₗ
          LinearMap.funLeft k (↑A : Type u) fun (x : Fin j → G) ↦ (⇑f : (a : G) → H) ∘ x)

Tactic:
subst hij
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
n i : ℕ
hf :
  ∀ (x : (↑((inhomogeneousCochains A).X i) : Type u)) (g : Fin (i + 1) → G),
    Eq (α := (↑B : Type u))
      ((ModuleCat.Hom.hom
              (ModuleCat.ofHom
                  ((Hom.hom φ).compLeft (Fin i → G) ∘ₗ
                    LinearMap.funLeft k (↑A : Type u) fun (x : Fin i → G) ↦ (⇑f : (a : G) → H) ∘ x) ≫
                (inhomogeneousCochains B).d i (i + 1)) :
            (a : (↑((inhomogeneousCochains A).X i) : Type u)) → (↑((inhomogeneousCochains B).X (i + 1)) : Type u))
          x g :
        (↑B : Type u))
      ((ModuleCat.Hom.hom
              (CategoryStruct.comp (Y := (inhomogeneousCochains A).X (i + 1)) ((inhomogeneousCochains A).d i (i + 1))
                (ModuleCat.ofHom
                  ((Hom.hom φ).compLeft (Fin (i + 1) → G) ∘ₗ
                    LinearMap.funLeft k (↑A : Type u) fun (x : Fin (i + 1) → G) ↦ (⇑f : (a : G) → H) ∘ x))) :
            (a : (↑((inhomogeneousCochains A).X i) : Type u)) → (↑((inhomogeneousCochains B).X (i + 1)) : Type u))
          x g :
        (↑B : Type u))
⊢ Eq (α := (inhomogeneousCochains A).X i ⟶ (inhomogeneousCochains B).X (i + 1))
    (ModuleCat.ofHom
        ((Hom.hom φ).compLeft (Fin i → G) ∘ₗ
          LinearMap.funLeft k (↑A : Type u) fun (x : Fin i → G) ↦ (⇑f : (a : G) → H) ∘ x) ≫
      (inhomogeneousCochains B).d i (i + 1))
    (CategoryStruct.comp (Y := (inhomogeneousCochains A).X (i + 1)) ((inhomogeneousCochains A).d i (i + 1))
      (ModuleCat.ofHom
        ((Hom.hom φ).compLeft (Fin (i + 1) → G) ∘ₗ
          LinearMap.funLeft k (↑A : Type u) fun (x : Fin (i + 1) → G) ↦ (⇑f : (a : G) → H) ∘ x)))

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
n i : ℕ
x : (↑((inhomogeneousCochains A).X i) : Type u)
g : Fin (i + 1) → G
⊢ Eq (α := (↑B : Type u))
    ((ModuleCat.Hom.hom
            (ModuleCat.ofHom
                ((Hom.hom φ).compLeft (Fin i → G) ∘ₗ
                  LinearMap.funLeft k (↑A : Type u) fun (x : Fin i → G) ↦ (⇑f : (a : G) → H) ∘ x) ≫
              (inhomogeneousCochains B).d i (i + 1)) :
          (a : (↑((inhomogeneousCochains A).X i) : Type u)) → (↑((inhomogeneousCochains B).X (i + 1)) : Type u))
        x g :
      (↑B : Type u))
    ((ModuleCat.Hom.hom
            (CategoryStruct.comp (Y := (inhomogeneousCochains A).X (i + 1)) ((inhomogeneousCochains A).d i (i + 1))
              (ModuleCat.ofHom
                ((Hom.hom φ).compLeft (Fin (i + 1) → G) ∘ₗ
                  LinearMap.funLeft k (↑A : Type u) fun (x : Fin (i + 1) → G) ↦ (⇑f : (a : G) → H) ∘ x))) :
          (a : (↑((inhomogeneousCochains A).X i) : Type u)) → (↑((inhomogeneousCochains B).X (i + 1)) : Type u))
        x g :
      (↑B : Type u))

Tactic:
simpa [inhomogeneousCochains.d_hom_apply, Fin.comp_contractNth, CochainComplex.of.d]
      using (hom_comm_apply φ _ _).symm

Premises used: CochainComplex.of.d, inhomogeneousCochains.d_hom_apply, Rep.hom_comm_apply, Eq.symm, Fin.comp_contractNth
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k H : Type u
inst : CommRing k
inst_1 : Group H
A : Rep k H
⊢ cochainsMap (MonoidHom.id H) (𝟙 A) = 𝟙 (inhomogeneousCochains A)

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A B : Rep k G
f : A ⟶ B
i : ℕ
⊢ ModuleCat.Hom.hom (HomologicalComplex.Hom.f (cochainsMap (MonoidHom.id G) f) i) = (Hom.hom f).compLeft (Fin i → G)

Tactic:
rfl

Premises used: LinearMap.compLeft, rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k : Type u
inst : CommRing k
G H K : Type u
inst_1 : Group G
inst_2 : Group H
inst_3 : 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) (CategoryTheory.Functor.map (resFunctor g) φ ≫ ψ) = cochainsMap f φ ≫ cochainsMap g ψ

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A B C : Rep k G
φ : A ⟶ B
ψ : B ⟶ C
⊢ cochainsMap (MonoidHom.id G) (φ ≫ ψ) =
    CategoryStruct.comp (Y := inhomogeneousCochains B) (cochainsMap (MonoidHom.id G) φ) (cochainsMap (MonoidHom.id G) ψ)

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k H
B : Rep k G
f : G →* H
⊢ Eq (α := inhomogeneousCochains A ⟶ inhomogeneousCochains B) (cochainsMap f 0) 0

Tactic:
rfl