awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
inst_3 : DecidableEq 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, Rep.applyAsHom, Rep.norm]

Premises used: Rep.norm, Rep.applyAsHom, Rep.sub_hom
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
inst_3 : DecidableEq G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
i : ℕ
h₀ : NeZero i
hi : Even i
⊢ (ComplexShape.down ℕ).Rel ((ComplexShape.down ℕ).prev i) i

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

Tactic:
(NeZero.ne 0 rfl).elim

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

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

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

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
inst_3 : DecidableEq 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.down ℕ).Rel 0 ((ComplexShape.down ℕ).next 0)
succ :
  ∀ (n : ℕ),
    (∀ [h₀ : NeZero n] (hi : Even n), (ComplexShape.down ℕ).Rel n ((ComplexShape.down ℕ).next n)) →
      ∀ [h₀ : NeZero (n + 1)] (hi : Even (n + 1)),
        (ComplexShape.down ℕ).Rel (n + 1) ((ComplexShape.down ℕ).next (n + 1))
⊢ (ComplexShape.down ℕ).Rel i ((ComplexShape.down ℕ).next i)

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

Premises used: False.elim, OfNat.ofNat, rfl, NeZero.ne
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
inst_3 : DecidableEq G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
i : ℕ
inst_4 : NeZero i
hi : Even i
x : ↥(LinearMap.ker A.ρ.norm)
⊢ Eq (α := (↑(groupHomology 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 ↥(LinearMap.ker A.ρ.norm)) (groupHomologyπEven A g hg i hi) :
            (a : (↑(ModuleCat.of k ↥(LinearMap.ker A.ρ.norm)) : Type u)) → (↑(groupHomology A i) : Type u))
          x :
        (↑(groupHomology A i) : Type u))
      (0 : (↑(groupHomology 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 [sub_hom, groupHomologyπEven, map_eq_zero_iff _ ((ModuleCat.mono_iff_injective _).1
    inferInstance), ShortComplex.moduleCatToCycles, -LinearMap.mem_range, Rep.applyAsHom, Rep.norm,
    LinearMap.range_codRestrict]

Premises used: Rep.norm, inferInstance, ModuleCat.mono_iff_injective, CategoryTheory.ShortComplex.moduleCatToCycles, Rep.FiniteCyclicGroup.groupHomologyπEven, Rep.applyAsHom, Rep.sub_hom, map_eq_zero_iff, LinearMap.mem_range, Iff.mp, LinearMap.range_codRestrict
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
inst_3 : DecidableEq 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.GroupHomology.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
inst_3 : DecidableEq 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,
    Rep.applyAsHom, Rep.norm]

Premises used: Rep.norm, Rep.applyAsHom, Rep.sub_hom
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
inst_3 : DecidableEq 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.GroupHomology.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
inst_3 : DecidableEq 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, Rep.applyAsHom, Rep.norm]

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

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

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

Tactic:
rcases hi with ⟨j, rfl⟩

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

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

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

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

Tactic:
rw [← sub_eq_zero, ← map_sub, groupHomologyπOdd_eq_zero_iff, AddSubgroupClass.coe_sub]

Premises used: AddSubgroupClass.coe_sub, map_sub, sub_eq_zero, Rep.FiniteCyclicGroup.groupHomologyπOdd_eq_zero_iff
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.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 G
B : Rep.{u_2, u, u} k H
f₁ f₂ : G →* H
h : f₁ = f₂
φ : A ⟶ res f₁ B
T : Type u_1
F : (f : G →* H) → (φ : A ⟶ res f B) → T
subst : F f₁ φ = F f₁ (Eq.rec (motive := fun (x : G →* H) (h : f₁ = x) ↦ A ⟶ res x B) φ ⋯)
⊢ F f₁ φ = F f₂ (Eq.rec (motive := fun (x : G →* H) (h : f₁ = x) ↦ A ⟶ res x B) φ h)

Tactic:
subst h
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.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 G
B : Rep.{u_2, u, u} k H
f₁ : G →* H
φ : A ⟶ res f₁ B
T : Type u_1
F : (f : G →* H) → (φ : A ⟶ res f B) → T
⊢ F f₁ φ = F f₁ (Eq.rec (motive := fun (x : G →* H) (h : f₁ = x) ↦ A ⟶ res x B) φ ⋯)

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

Tactic:
subst hij
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
n j : ℕ
h :
  ∀ (g : Fin (j + 1) → G) (x : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) (a : Fin j → H),
    Eq (α := (↑B : Type u))
      ((((ModuleCat.Hom.hom
                    (ModuleCat.ofHom (lsingle g) ≫
                      CategoryStruct.comp (Y := (inhomogeneousChains B).X (j + 1))
                        (ModuleCat.ofHom
                          (mapRange.linearMap (Hom.hom φ).toLinearMap ∘ₗ
                            lmapDomain (↑A : Type u) k fun (x : Fin (j + 1) → G) ↦ (⇑f : (a : G) → H) ∘ x))
                        ((inhomogeneousChains B).d (j + 1) j)) :
                  (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑((inhomogeneousChains B).X j) : Type u))
                x :
              (↑((inhomogeneousChains B).X j) : Type u)) :
            (a : Fin j → H) → (↑B : Type u))
          a :
        (↑B : Type u))
      ((((ModuleCat.Hom.hom
                    (ModuleCat.ofHom (lsingle g) ≫
                      (inhomogeneousChains A).d (j + 1) j ≫
                        ModuleCat.ofHom
                          (mapRange.linearMap (Hom.hom φ).toLinearMap ∘ₗ
                            lmapDomain (↑A : Type u) k fun (x : Fin j → G) ↦ (⇑f : (a : G) → H) ∘ x)) :
                  (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑((inhomogeneousChains B).X j) : Type u))
                x :
              (↑((inhomogeneousChains B).X j) : Type u)) :
            (a : Fin j → H) → (↑B : Type u))
          a :
        (↑B : Type u))
⊢ Eq (α := (inhomogeneousChains A).X (j + 1) ⟶ (inhomogeneousChains B).X j)
    (CategoryStruct.comp (Y := (inhomogeneousChains B).X (j + 1))
      (ModuleCat.ofHom
        (mapRange.linearMap (Hom.hom φ).toLinearMap ∘ₗ
          lmapDomain (↑A : Type u) k fun (x : Fin (j + 1) → G) ↦ (⇑f : (a : G) → H) ∘ x))
      ((inhomogeneousChains B).d (j + 1) j))
    ((inhomogeneousChains A).d (j + 1) j ≫
      ModuleCat.ofHom
        (mapRange.linearMap (Hom.hom φ).toLinearMap ∘ₗ
          lmapDomain (↑A : Type u) k fun (x : Fin j → G) ↦ (⇑f : (a : G) → H) ∘ x))

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
n j : ℕ
g : Fin (j + 1) → G
x : (↑(ModuleCat.of k (↑A : Type u)) : Type u)
a : Fin j → H
h :
  Eq (α := (↑B : Type u))
    (((single (fun (i : Fin j) ↦ (f : (a : G) → H) (g i.succ))
              ((((B.ρ : (a : H) → (↑B : Type u) →ₗ[k] (↑B : Type u)) ((f : (a : G) → H) (g 0))⁻¹ :
                    (↑B : Type u) →ₗ[k] (↑B : Type u)) :
                  (a : (↑B : Type u)) → (↑B : Type u))
                ((Hom.hom φ : (a : (↑A : Type u)) → (↑B : Type u)) x : (↑B : Type u))) :
            ((i : Fin j) → H) →₀ (↑B : Type u)) :
          (a : Fin j → H) → (↑B : Type u))
        a :
      (↑B : Type u))
    (((single (Function.comp (β := G) (⇑f : (a : G) → H) fun (i : Fin j) ↦ g i.succ)
              ((((B.ρ : (a : H) → (↑B : Type u) →ₗ[k] (↑B : Type u)) ((f : (a : G) → H) (g 0))⁻¹ :
                    (↑B : Type u) →ₗ[k] (↑B : Type u)) :
                  (a : (↑B : Type u)) → (↑B : Type u))
                ((Hom.hom φ : (a : (↑A : Type u)) → (↑B : Type u)) x : (↑B : Type u))) :
            (Fin j → H) →₀ (↑B : Type u)) :
          (a : Fin j → H) → (↑B : Type u))
        a :
      (↑B : Type u))
⊢ Eq (α := (↑B : Type u))
    ((((ModuleCat.Hom.hom
                  (ModuleCat.ofHom (lsingle g) ≫
                    CategoryStruct.comp (Y := (inhomogeneousChains B).X (j + 1))
                      (ModuleCat.ofHom
                        (mapRange.linearMap (Hom.hom φ).toLinearMap ∘ₗ
                          lmapDomain (↑A : Type u) k fun (x : Fin (j + 1) → G) ↦ (⇑f : (a : G) → H) ∘ x))
                      ((inhomogeneousChains B).d (j + 1) j)) :
                (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑((inhomogeneousChains B).X j) : Type u))
              x :
            (↑((inhomogeneousChains B).X j) : Type u)) :
          (a : Fin j → H) → (↑B : Type u))
        a :
      (↑B : Type u))
    ((((ModuleCat.Hom.hom
                  (ModuleCat.ofHom (lsingle g) ≫
                    (inhomogeneousChains A).d (j + 1) j ≫
                      ModuleCat.ofHom
                        (mapRange.linearMap (Hom.hom φ).toLinearMap ∘ₗ
                          lmapDomain (↑A : Type u) k fun (x : Fin j → G) ↦ (⇑f : (a : G) → H) ∘ x)) :
                (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑((inhomogeneousChains B).X j) : Type u))
              x :
            (↑((inhomogeneousChains B).X j) : Type u)) :
          (a : Fin j → H) → (↑B : Type u))
        a :
      (↑B : Type u))

Tactic:
simp [Fin.comp_contractNth, map_add, inhomogeneousChains.d, Rep.hom_comm_apply φ]

Premises used: groupHomology.inhomogeneousChains.d, map_add, Rep.hom_comm_apply, Fin.comp_contractNth
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
n j : ℕ
g : Fin (j + 1) → G
x : (↑(ModuleCat.of k (↑A : Type u)) : Type u)
a : Fin j → H
⊢ Eq (α := (↑B : Type u))
    (((single (fun (i : Fin j) ↦ (f : (a : G) → H) (g i.succ))
              ((((B.ρ : (a : H) → (↑B : Type u) →ₗ[k] (↑B : Type u)) ((f : (a : G) → H) (g 0))⁻¹ :
                    (↑B : Type u) →ₗ[k] (↑B : Type u)) :
                  (a : (↑B : Type u)) → (↑B : Type u))
                ((Hom.hom φ : (a : (↑A : Type u)) → (↑B : Type u)) x : (↑B : Type u))) :
            ((i : Fin j) → H) →₀ (↑B : Type u)) :
          (a : Fin j → H) → (↑B : Type u))
        a :
      (↑B : Type u))
    (((single (Function.comp (β := G) (⇑f : (a : G) → H) fun (i : Fin j) ↦ g i.succ)
              ((((B.ρ : (a : H) → (↑B : Type u) →ₗ[k] (↑B : Type u)) ((f : (a : G) → H) (g 0))⁻¹ :
                    (↑B : Type u) →ₗ[k] (↑B : Type u)) :
                  (a : (↑B : Type u)) → (↑B : Type u))
                ((Hom.hom φ : (a : (↑A : Type u)) → (↑B : Type u)) x : (↑B : Type u))) :
            (Fin j → H) →₀ (↑B : Type u)) :
          (a : Fin j → H) → (↑B : Type u))
        a :
      (↑B : Type u))

Tactic:
rfl