awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ cyclesMap f φ 1 ≫ (isoCycles₁ B).hom = (isoCycles₁ A).hom ≫ mapCycles₁ f φ

Tactic:
simp [← cancel_mono (moduleCatLeftHomologyData (shortComplexH1 B)).i, mapShortComplexH1,
    chainsMap_f_1_comp_chainsIso₁ f]

Premises used: groupHomology.mapShortComplexH1, CategoryTheory.cancel_mono, groupHomology.chainsMap_f_1_comp_chainsIso₁, CategoryTheory.ShortComplex.moduleCatLeftHomologyData, groupHomology.shortComplexH1, CategoryTheory.ShortComplex.LeftHomologyData.i
-- 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
⊢ H1π A ≫ map f φ 1 = mapCycles₁ f φ ≫ H1π B

Tactic:
simp [H1π, Iso.inv_comp_eq, ← cyclesMap_comp_isoCycles₁_hom_assoc]

Premises used: CategoryTheory.Iso.inv_comp_eq, groupHomology.H1π, groupHomology.cyclesMap_comp_isoCycles₁_hom_assoc
-- 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
φ : A ⟶ res 1 B
simp : mapCycles₁ 1 φ ≫ H1π B = 0
⊢ Eq (α := groupHomology A 1 ⟶ groupHomology B 1) (map 1 φ 1) 0

Tactic:
simp only [← cancel_epi (H1π A), H1π_comp_map, Limits.comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, groupHomology.H1π, groupHomology.H1π_comp_map, CategoryTheory.cancel_epi
-- 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
φ : A ⟶ res 1 B
hf :
  ∀ (x : (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u)),
    Eq (α := (↑(H1 B) : Type u))
      ((ModuleCat.Hom.hom (mapCycles₁ 1 φ ≫ H1π B) :
            (a : (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u)) → (↑(H1 B) : Type u))
          x :
        (↑(H1 B) : Type u))
      ((ModuleCat.Hom.hom 0 : (a : (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u)) → (↑(H1 B) : Type u)) x :
        (↑(H1 B) : Type u))
⊢ mapCycles₁ 1 φ ≫ H1π B = 0

Tactic:
ext x
-- 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
φ : A ⟶ res 1 B
x : (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u)
⊢ Eq (α := (↑(H1 B) : Type u))
    ((ModuleCat.Hom.hom (H1π B) ∘ₗ ModuleCat.Hom.hom (mapCycles₁ 1 φ) :
          (a : (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u)) → (↑(H1 B) : Type u))
        x :
      (↑(H1 B) : Type u))
    ((ModuleCat.Hom.hom 0 : (a : (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u)) → (↑(H1 B) : Type u)) x :
      (↑(H1 B) : Type u))

Tactic:
(H1π_eq_zero_iff _).2 ?_

Premises used: Iff.mpr, groupHomology.H1π_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 k G
B : Rep k H
φ : A ⟶ res 1 B
x : (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u)
hf :
  (↑((ModuleCat.Hom.hom (mapCycles₁ 1 φ) :
            (a : (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u)) → (↑(ModuleCat.of k ↥(cycles₁ B)) : Type u))
          x) :
      H →₀ (↑B : Type u)) ∈
    boundaries₁ B
⊢ Eq (α := (↑(H1 B) : Type u))
    ((ModuleCat.Hom.hom (H1π B) ∘ₗ ModuleCat.Hom.hom (mapCycles₁ 1 φ) :
          (a : (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u)) → (↑(H1 B) : Type u))
        x :
      (↑(H1 B) : Type u))
    ((ModuleCat.Hom.hom 0 : (a : (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u)) → (↑(H1 B) : Type u)) x :
      (↑(H1 B) : Type u))

Tactic:
refine (H1π_eq_zero_iff _).2 ?_

Premises used: Iff.mpr, groupHomology.H1π_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 k G
B : Rep k H
φ : A ⟶ res 1 B
x : (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u)
⊢ (↑((ModuleCat.Hom.hom (mapCycles₁ 1 φ) :
            (a : (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u)) → (↑(ModuleCat.of k ↥(cycles₁ B)) : Type u))
          x) :
      H →₀ (↑B : Type u)) ∈
    boundaries₁ B

Tactic:
simpa [coe_mapCycles₁ _ φ x, mapDomain, map_finsuppSum] using
    (boundaries₁ B).finsuppSum_mem k x.1 _ fun _ _ => single_one_mem_boundaries₁ (A := B) _

Premises used: Finsupp.mapDomain, map_finsuppSum, groupHomology.coe_mapCycles₁, Submodule.finsuppSum_mem, Subtype.val, groupHomology.boundaries₁
-- 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 : ℕ
S : Subgroup G
inst_3 : S.Normal
inst_4 : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
rw :
  Function.Surjective (α := (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u)) (β :=
    (↑(ModuleCat.of k ↥(cycles₁ (A.ofQuotient S))) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (Y := ModuleCat.of k ↥(cycles₁ (A.ofQuotient S)))
          (mapCycles₁ (QuotientGroup.mk' S) (Iso.inv (A.resOfQuotientIso S)))) :
      (a : (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u)) → (↑(ModuleCat.of k ↥(cycles₁ (A.ofQuotient S))) : Type u))
⊢ Epi (Y := ModuleCat.of k ↥(cycles₁ (A.ofQuotient S)))
    (mapCycles₁ (QuotientGroup.mk' S) (Iso.inv (A.resOfQuotientIso S)))

Tactic:
rw [ModuleCat.epi_iff_surjective]

Premises used: ModuleCat.epi_iff_surjective
-- 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 : ℕ
S : Subgroup G
inst_3 : S.Normal
inst_4 : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
x : G ⧸ S →₀ (↑(A.ofQuotient S) : Type u)
hx : Membership.mem (γ := Submodule k (G ⧸ S →₀ (↑(A.ofQuotient S) : Type u))) (cycles₁ (A.ofQuotient S)) x
choose! :
  ∀ (s : (b : G ⧸ S) → G) (hs : ∀ (b : G ⧸ S), (↑(s b) : G ⧸ S) = b),
    ∃ (a : (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u)),
      (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (Y := ModuleCat.of k ↥(cycles₁ (A.ofQuotient S)))
              (mapCycles₁ (QuotientGroup.mk' S) (Iso.inv (A.resOfQuotientIso S))) :
            (a : (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u)) → (↑(ModuleCat.of k ↥(cycles₁ (A.ofQuotient S))) : Type u))
          a =
        Subtype.mk (p := fun (x : G ⧸ S →₀ (↑(A.ofQuotient S) : Type u)) ↦
          Membership.mem (γ := Submodule k (G ⧸ S →₀ (↑(A.ofQuotient S) : Type u))) (cycles₁ (A.ofQuotient S)) x) x hx
⊢ ∃ (a : (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u)),
    (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (Y := ModuleCat.of k ↥(cycles₁ (A.ofQuotient S)))
            (mapCycles₁ (QuotientGroup.mk' S) (Iso.inv (A.resOfQuotientIso S))) :
          (a : (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u)) → (↑(ModuleCat.of k ↥(cycles₁ (A.ofQuotient S))) : Type u))
        a =
      Subtype.mk (p := fun (x : G ⧸ S →₀ (↑(A.ofQuotient S) : Type u)) ↦
        Membership.mem (γ := Submodule k (G ⧸ S →₀ (↑(A.ofQuotient S) : Type u))) (cycles₁ (A.ofQuotient S)) x) x hx

Tactic:
choose! s hs using QuotientGroup.mk_surjective (s := S)

Premises used: QuotientGroup.mk_surjective
-- 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 : ℕ
S : Subgroup G
inst_3 : S.Normal
inst_4 : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
x : G ⧸ S →₀ (↑(A.ofQuotient S) : Type u)
hx : Membership.mem (γ := Submodule k (G ⧸ S →₀ (↑(A.ofQuotient S) : Type u))) (cycles₁ (A.ofQuotient S)) x
s : (b : G ⧸ S) → G
hs : ∀ (b : G ⧸ S), (↑(s b) : G ⧸ S) = b
⊢ QuotientGroup.mk ∘ s = id

Tactic:
have hs₁ : QuotientGroup.mk ∘ s = id := funext hs
-- 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 : ℕ
S : Subgroup G
inst_3 : S.Normal
inst_4 : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
x : G ⧸ S →₀ (↑(A.ofQuotient S) : Type u)
hx : Membership.mem (γ := Submodule k (G ⧸ S →₀ (↑(A.ofQuotient S) : Type u))) (cycles₁ (A.ofQuotient S)) x
s : (b : G ⧸ S) → G
hs : ∀ (b : G ⧸ S), (↑(s b) : G ⧸ S) = b
hs₁ : QuotientGroup.mk ∘ s = id
⊢ (↑((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (Y := ModuleCat.of k ↥(cycles₁ (A.ofQuotient S)))
              (mapCycles₁ (QuotientGroup.mk' S) (Iso.inv (A.resOfQuotientIso S))) :
            (a : (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u)) → (↑(ModuleCat.of k ↥(cycles₁ (A.ofQuotient S))) : Type u))
          (Subtype.mk (p := fun (x : G →₀ (↑A : Type u)) ↦ x ∈ cycles₁ A) (mapDomain s x) ⋯)) :
      G ⧸ S →₀ (↑(A.ofQuotient S) : Type u)) =
    (↑(Subtype.mk (p := fun (x : G ⧸ S →₀ (↑(A.ofQuotient S) : Type u)) ↦
          Membership.mem (γ := Submodule k (G ⧸ S →₀ (↑(A.ofQuotient S) : Type u))) (cycles₁ (A.ofQuotient S)) x) x
          hx) :
      G ⧸ S →₀ (↑(A.ofQuotient S) : Type u))

Tactic:
simp [mapCycles₁_hom, ← mapDomain_comp, hs₁, res, Rep.hom_id (of _)]

Premises used: Rep.hom_id, Rep.of, Rep.res, Finsupp.mapDomain_comp, groupHomology.mapCycles₁_hom
-- 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 : ℕ
S : Subgroup G
inst_3 : S.Normal
inst_4 : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
x : G ⧸ S →₀ (↑(A.ofQuotient S) : Type u)
hx : Membership.mem (γ := Submodule k (G ⧸ S →₀ (↑(A.ofQuotient S) : Type u))) (cycles₁ (A.ofQuotient S)) x
s : (b : G ⧸ S) → G
hs : ∀ (b : G ⧸ S), (↑(s b) : G ⧸ S) = b
hs₁ : QuotientGroup.mk ∘ s = id
refine : mapDomain s x ∈ cycles₁ A
⊢ ∃ (a : (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u)),
    (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (Y := ModuleCat.of k ↥(cycles₁ (A.ofQuotient S)))
            (mapCycles₁ (QuotientGroup.mk' S) (Iso.inv (A.resOfQuotientIso S))) :
          (a : (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u)) → (↑(ModuleCat.of k ↥(cycles₁ (A.ofQuotient S))) : Type u))
        a =
      Subtype.mk (p := fun (x : G ⧸ S →₀ (↑(A.ofQuotient S) : Type u)) ↦
        Membership.mem (γ := Submodule k (G ⧸ S →₀ (↑(A.ofQuotient S) : Type u))) (cycles₁ (A.ofQuotient S)) x) x hx

Tactic:
refine ⟨⟨mapDomain s x, ?_⟩, Subtype.ext <| by
    simp [mapCycles₁_hom, ← mapDomain_comp, hs₁, res, Rep.hom_id (of _)]⟩
-- 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 : ℕ
S : Subgroup G
inst_3 : S.Normal
inst_4 : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
x_1 : G ⧸ S →₀ (↑(A.ofQuotient S) : Type u)
hx : Membership.mem (γ := Submodule k (G ⧸ S →₀ (↑(A.ofQuotient S) : Type u))) (cycles₁ (A.ofQuotient S)) x_1
s : (b : G ⧸ S) → G
hs : ∀ (b : G ⧸ S), (↑(s b) : G ⧸ S) = b
hs₁ : QuotientGroup.mk ∘ s = id
x y : G ⧸ S
h : s x = s y
rw : (↑(s x) : G ⧸ S) = y
rw₁ : Eq (α := G ⧸ S) (↑(s x) : G ⧸ S) (↑(s y) : G ⧸ S)
rw₂ rw₃ : Eq (α := G ⧸ S) (↑(s y) : G ⧸ S) (↑(s y) : G ⧸ S)
⊢ x = y

Tactic:
rw [← hs x, ← hs y, 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 k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
n : ℕ
S : Subgroup G
inst_3 : S.Normal
inst_4 : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
x : G ⧸ S →₀ (↑(A.ofQuotient S) : Type u)
hx : Membership.mem (γ := Submodule k (G ⧸ S →₀ (↑(A.ofQuotient S) : Type u))) (cycles₁ (A.ofQuotient S)) x
s : (b : G ⧸ S) → G
hs : ∀ (b : G ⧸ S), (↑(s b) : G ⧸ S) = b
hs₁ : QuotientGroup.mk ∘ s = id
a_1 : G ⧸ S
b : a_1 ∈ x.support
a : G
⊢ Eq (α := G ⧸ S) (↑(s (↑a : G ⧸ S))⁻¹ : G ⧸ S) (↑a⁻¹ : G ⧸ S)

Tactic:
simp [hs]
-- 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 : ℕ
S : Subgroup G
inst_3 : S.Normal
inst_4 : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
x : G ⧸ S →₀ (↑(A.ofQuotient S) : Type u)
hx : Membership.mem (γ := Submodule k (G ⧸ S →₀ (↑(A.ofQuotient S) : Type u))) (cycles₁ (A.ofQuotient S)) x
s : (b : G ⧸ S) → G
hs : ∀ (b : G ⧸ S), (↑(s b) : G ⧸ S) = b
hs₁ : QuotientGroup.mk ∘ s = id
a_1 : G ⧸ S
b : a_1 ∈ x.support
a : G
⊢ Eq (α := (↑A : Type u))
    ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) (s (↑a : G ⧸ S))⁻¹ : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
          (a : (↑A : Type u)) → (↑A : Type u))
        ((x : (a : G ⧸ S) → (↑A : Type u)) (↑a : G ⧸ S) : (↑A : Type u)) :
      (↑A : Type u))
    ((((A.ρ.ofQuotient S : (a : G ⧸ S) → (↑A : Type u) →ₗ[k] (↑A : Type u)) (↑a : G ⧸ S)⁻¹ :
            (↑A : Type u) →ₗ[k] (↑A : Type u)) :
          (a : (↑A : Type u)) → (↑A : Type u))
        ((x : (a : G ⧸ S) → (↑A : Type u)) (↑a : G ⧸ S) : (↑A : Type u)) :
      (↑A : Type u))

Tactic:
simp [← QuotientGroup.mk_inv, apply_eq_of_coe_eq A.ρ S (s a)⁻¹ a⁻¹ (by simp [hs])]

Premises used: QuotientGroup.mk, Inv.inv, QuotientGroup.mk_inv, Rep.ρ, Representation.apply_eq_of_coe_eq
-- 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 : ℕ
S : Subgroup G
inst_3 : S.Normal
inst_4 : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
x : G ⧸ S →₀ (↑(A.ofQuotient S) : Type u)
hx : Membership.mem (γ := Submodule k (G ⧸ S →₀ (↑(A.ofQuotient S) : Type u))) (cycles₁ (A.ofQuotient S)) x
s : (b : G ⧸ S) → G
hs : ∀ (b : G ⧸ S), (↑(s b) : G ⧸ S) = b
hs₁ : QuotientGroup.mk ∘ s = id
⊢ mapDomain s x ∈ cycles₁ A

Tactic:
simpa [mem_cycles₁_iff, ← (mem_cycles₁_iff _).1 hx, sum_mapDomain_index_inj (f := s)
      (fun x y h => by rw [← hs x, ← hs y, h])]
    using Finsupp.sum_congr fun a b => QuotientGroup.induction_on a fun a => by
      simp [← QuotientGroup.mk_inv, apply_eq_of_coe_eq A.ρ S (s a)⁻¹ a⁻¹ (by simp [hs])]

Premises used: Finsupp.sum_mapDomain_index_inj, Finsupp.sum_congr, Iff.mp, QuotientGroup.induction_on, groupHomology.mem_cycles₁_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 k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
n : ℕ
S : Subgroup G
inst_3 : S.Normal
inst_4 : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
rw :
  Eq (α := H1 (res S.subtype A) ⟶ H1 (A.ofQuotient S))
    (map (MonoidHom.comp (QuotientGroup.mk' S) S.subtype)
      (𝟙 (res S.subtype A) ≫ CategoryTheory.Functor.map (resFunctor S.subtype) (Iso.inv (A.resOfQuotientIso S))) 1)
    0
rw₁ :
  Eq.{u + 1} (α := H1 (res S.subtype A) ⟶ H1 (A.ofQuotient S))
    (map 1
      (Eq.rec (motive := fun (x : ↥S →* G ⧸ S) (h : MonoidHom.comp (QuotientGroup.mk' S) S.subtype = x) ↦
        res S.subtype A ⟶ res x (A.ofQuotient S))
        (𝟙 (res S.subtype A) ≫ CategoryTheory.Functor.map (resFunctor S.subtype) (Iso.inv (A.resOfQuotientIso S))) ⋯)
      1)
    0
rw₂ rw₃ : Eq.{u + 1} (α := H1 (res S.subtype A) ⟶ H1 (A.ofQuotient S)) 0 0
⊢ Eq (α := H1 (res S.subtype A) ⟶ H1 (A.ofQuotient S))
    (map S.subtype (𝟙 (res S.subtype A)) 1 ≫ map (QuotientGroup.mk' S) (Iso.inv (A.resOfQuotientIso S)) 1) 0

Tactic:
rw [← map_comp, congr (QuotientGroup.mk'_comp_subtype S) (map (n := 1)), map₁_one]

Premises used: groupHomology.map₁_one, groupHomology.map_comp, QuotientGroup.mk'_comp_subtype, groupHomology.congr, OfNat.ofNat, groupHomology.map
-- 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 : ℕ
S : Subgroup G
inst_3 : S.Normal
inst_4 : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
⊢ Epi (X := H1 A) (Y := groupHomology (A.ofQuotient S) 1) (map (QuotientGroup.mk' S) (Iso.inv (A.resOfQuotientIso S)) 1)

Tactic:
epi_of_epi (H1π A) _

Premises used: CategoryTheory.epi_of_epi, groupHomology.H1π
-- 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 : ℕ
S : Subgroup G
inst_3 : S.Normal
inst_4 : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
convert_3 :
  Epi (Y := groupHomology (A.ofQuotient S) 1) (H1π A ≫ map (QuotientGroup.mk' S) (Iso.inv (A.resOfQuotientIso S)) 1)
⊢ Epi (X := groupHomology A 1) (Y := groupHomology (A.ofQuotient S) 1)
    (map (QuotientGroup.mk' S) (Iso.inv (A.resOfQuotientIso S)) 1)

Tactic:
convert! epi_of_epi (H1π A) _

Premises used: CategoryTheory.epi_of_epi, groupHomology.H1π
-- 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 : ℕ
S : Subgroup G
inst_3 : S.Normal
inst_4 : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
convert_3 :
  Epi (Y := groupHomology (A.ofQuotient S) 1)
    (mapCycles₁ (QuotientGroup.mk' S) (Iso.inv (A.resOfQuotientIso S)) ≫ H1π (A.ofQuotient S))
⊢ Epi (Y := groupHomology (A.ofQuotient S) 1) (H1π A ≫ map (QuotientGroup.mk' S) (Iso.inv (A.resOfQuotientIso S)) 1)

Tactic:
rw [H1π_comp_map]

Premises used: groupHomology.H1π_comp_map
-- 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 : ℕ
S : Subgroup G
inst_3 : S.Normal
inst_4 : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
⊢ Epi (Y := groupHomology (A.ofQuotient S) 1)
    (mapCycles₁ (QuotientGroup.mk' S) (Iso.inv (A.resOfQuotientIso S)) ≫ H1π (A.ofQuotient S))

Tactic:
@epi_comp _ _ _ _ _ _ (mapCycles₁_quotientGroupMk'_epi A S) (H1π _) inferInstance

Premises used: CategoryTheory.epi_comp, groupHomology.H1π
-- 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 : ℕ
S : Subgroup G
inst_3 : S.Normal
inst_4 : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
⊢ Epi (Y := groupHomology (A.ofQuotient S) 1)
    (mapCycles₁ (QuotientGroup.mk' S) (Iso.inv (A.resOfQuotientIso S)) ≫ H1π (A.ofQuotient S))

Tactic:
exact @epi_comp _ _ _ _ _ _ (mapCycles₁_quotientGroupMk'_epi A S) (H1π _) inferInstance

Premises used: CategoryTheory.epi_comp, groupHomology.H1π
-- 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 : ℕ
S : Subgroup G
inst_3 : S.Normal
inst_4 : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
⊢ Epi (H1CoresCoinfOfTrivial A S).g

Tactic:
inferInstanceAs <| Epi (map _ _ 1)

Premises used: _private.0.groupHomology.H1CoresCoinfOfTrivial_g_epi._proof_1
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
S : Subgroup G
inst_2 : S.Normal
inst_3 : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
rw : (ModuleCat.Hom.hom (H1CoresCoinfOfTrivial A S).g).ker ≤ (ModuleCat.Hom.hom (H1CoresCoinfOfTrivial A S).f).range
⊢ (H1CoresCoinfOfTrivial A S).Exact

Tactic:
rw [ShortComplex.moduleCat_exact_iff_ker_sub_range]

Premises used: CategoryTheory.ShortComplex.moduleCat_exact_iff_ker_sub_range
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
S : Subgroup G
inst_2 : S.Normal
inst_3 : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
x : ↥(cycles₁ A)
hx :
  Membership.mem (α := (↑(H1CoresCoinfOfTrivial A S).X₂ : Type u)) (ModuleCat.Hom.hom (H1CoresCoinfOfTrivial A S).g).ker
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (H1π A) :
          (a : (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u)) → (↑(H1 A) : Type u))
        x :
      (↑(H1 A) : Type u))
h :
  ∀ (x : G →₀ (↑A : Type u)) (hxc : x ∈ cycles₁ A)
    (hx :
      Membership.mem (α := (↑(H1CoresCoinfOfTrivial A S).X₂ : Type u))
        (ModuleCat.Hom.hom (H1CoresCoinfOfTrivial A S).g).ker
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (H1π A) :
              (a : (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u)) → (↑(H1 A) : Type u))
            (Subtype.mk (p := fun (x : G →₀ (↑A : Type u)) ↦ x ∈ cycles₁ A) x hxc) :
          (↑(H1 A) : Type u))),
    Membership.mem (α := (↑(H1CoresCoinfOfTrivial A S).X₂ : Type u))
      (ModuleCat.Hom.hom (H1CoresCoinfOfTrivial A S).f).range
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (H1π A) :
            (a : (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u)) → (↑(H1 A) : Type u))
          (Subtype.mk (p := fun (x : G →₀ (↑A : Type u)) ↦ x ∈ cycles₁ A) x hxc) :
        (↑(H1 A) : Type u))
⊢ Membership.mem (α := (↑(H1CoresCoinfOfTrivial A S).X₂ : Type u))
    (ModuleCat.Hom.hom (H1CoresCoinfOfTrivial A S).f).range
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (H1π A) :
          (a : (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u)) → (↑(H1 A) : Type u))
        x :
      (↑(H1 A) : Type u))

Tactic:
rcases x with ⟨x, hxc⟩