awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : 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))
⊢ Eq (α := (↑(H1 (A.ofQuotient S)) : Type u))
    (((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (X := ModuleCat.of k ↥(cycles₁ (A.ofQuotient S))) (Y :=
              groupHomology (A.ofQuotient S) 1) (H1π (A.ofQuotient S)) :
            (↑(ModuleCat.of k ↥(cycles₁ (A.ofQuotient S))) : Type u) →ₗ[k]
              (↑(groupHomology (A.ofQuotient S) 1) : Type u)) :
          (a : ↥(cycles₁ (A.ofQuotient S))) → (↑(groupHomology (A.ofQuotient S) 1) : 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 : ↥(cycles₁ A)) → ↥(cycles₁ (A.ofQuotient S)))
            (Subtype.mk (p := fun (x : G →₀ (↑A : Type u)) ↦ x ∈ cycles₁ A) x hxc) :
          ↥(cycles₁ (A.ofQuotient S))) :
      (↑(groupHomology (A.ofQuotient S) 1) : Type u))
    (0 : (↑(H1 (A.ofQuotient S)) : Type u))

Tactic:
simp_all only [H1CoresCoinfOfTrivial_X₂, H1CoresCoinfOfTrivial_X₃, H1CoresCoinfOfTrivial_g,
    LinearMap.mem_ker, H1π_comp_map_apply (QuotientGroup.mk' S)]

Premises used: groupHomology.H1CoresCoinfOfTrivial_X₂, groupHomology.H1π_comp_map_apply, LinearMap.mem_ker, QuotientGroup.mk', groupHomology.H1CoresCoinfOfTrivial_g, groupHomology.H1CoresCoinfOfTrivial_X₃
-- 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 : G →₀ (↑A : Type u)
hxc : x ∈ cycles₁ A
hx :
  Eq (α := (↑(H1 (A.ofQuotient S)) : Type u))
    (((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (X := ModuleCat.of k ↥(cycles₁ (A.ofQuotient S))) (Y :=
              groupHomology (A.ofQuotient S) 1) (H1π (A.ofQuotient S)) :
            (↑(ModuleCat.of k ↥(cycles₁ (A.ofQuotient S))) : Type u) →ₗ[k]
              (↑(groupHomology (A.ofQuotient S) 1) : Type u)) :
          (a : ↥(cycles₁ (A.ofQuotient S))) → (↑(groupHomology (A.ofQuotient S) 1) : 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 : ↥(cycles₁ A)) → ↥(cycles₁ (A.ofQuotient S)))
            (Subtype.mk (p := fun (x : G →₀ (↑A : Type u)) ↦ x ∈ cycles₁ A) x hxc) :
          ↥(cycles₁ (A.ofQuotient S))) :
      (↑(groupHomology (A.ofQuotient S) 1) : Type u))
    (0 : (↑(H1 (A.ofQuotient S)) : Type u))
y : (↑(ModuleCat.of k ((G ⧸ S) × G ⧸ S →₀ (↑(A.ofQuotient S) : Type u))) : Type u)
hy :
  Eq (α := G ⧸ S →₀ (↑(A.ofQuotient S) : Type u))
    ((ModuleCat.Hom.hom (d₂₁ (A.ofQuotient S)) :
          (a : (↑(ModuleCat.of k ((G ⧸ S) × G ⧸ S →₀ (↑(A.ofQuotient S) : Type u))) : Type u)) →
            G ⧸ S →₀ (↑(A.ofQuotient S) : Type u))
        y :
      G ⧸ S →₀ (↑(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 : ↥(cycles₁ A)) → ↥(cycles₁ (A.ofQuotient S)))
            (Subtype.mk (p := fun (x : G →₀ (↑A : Type u)) ↦ x ∈ cycles₁ A) x hxc)) :
        G ⧸ S →₀ (↑(A.ofQuotient S) : Type u)) :
      G ⧸ S →₀ (↑(A.ofQuotient S) : Type u))
s : (b : G ⧸ S) → G
hs : ∀ (b : G ⧸ S), (QuotientGroup.mk' S : (a : G) → G ⧸ S) (s b) = b
⊢ QuotientGroup.mk ∘ s = id

Tactic:
have hs₁ : QuotientGroup.mk (s := S) ∘ 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
rw :
  Eq (α := H1 (res S.subtype A) ⟶ H1 (A.quotientToCoinvariants S))
    (map (MonoidHom.comp (QuotientGroup.mk' S) S.subtype)
      (𝟙 (res S.subtype A) ≫ CategoryTheory.Functor.map (resFunctor S.subtype) (A.toCoinvariantsMkQ S)) 1)
    0
rw₁ :
  Eq.{u + 1} (α := H1 (res S.subtype A) ⟶ H1 (A.quotientToCoinvariants 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.quotientToCoinvariants S))
        (𝟙 (res S.subtype A) ≫ CategoryTheory.Functor.map (resFunctor S.subtype) (A.toCoinvariantsMkQ S)) ⋯)
      1)
    0
rw₂ rw₃ : Eq.{u + 1} (α := H1 (res S.subtype A) ⟶ H1 (A.quotientToCoinvariants S)) 0 0
⊢ Eq (α := H1 (res S.subtype A) ⟶ H1 (A.quotientToCoinvariants S))
    (map S.subtype (𝟙 (res S.subtype A)) 1 ≫ map (QuotientGroup.mk' S) (A.toCoinvariantsMkQ 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 : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
S : Subgroup G
inst_2 : S.Normal
rw :
  LE.le (α := Submodule k (↑(shortComplexH1 (A.coinvariantsShortComplex S).X₁).X₂ : Type u)) ⊤
    (Submodule.comap (M₂ := (↑(shortComplexH1 A).opcycles : Type u))
      (ModuleCat.Hom.hom
        (Hom.τ₂ (mapShortComplexH1 (MonoidHom.id G) (A.coinvariantsShortComplex S).f) ≫ (shortComplexH1 A).pOpcycles))
      (LinearMap.range
        (ModuleCat.Hom.hom ((mapShortComplexH1 S.subtype (𝟙 (res S.subtype A))).τ₂ ≫ (shortComplexH1 A).pOpcycles))))
⊢ Eq (α := Submodule k (↑(shortComplexH1 (A.coinvariantsShortComplex S).X₁).X₂ : Type u))
    (Submodule.comap (M₂ := (↑(shortComplexH1 A).opcycles : Type u))
      (ModuleCat.Hom.hom
        (Hom.τ₂ (mapShortComplexH1 (MonoidHom.id G) (A.coinvariantsShortComplex S).f) ≫ (shortComplexH1 A).pOpcycles))
      (LinearMap.range
        (ModuleCat.Hom.hom ((mapShortComplexH1 S.subtype (𝟙 (res S.subtype A))).τ₂ ≫ (shortComplexH1 A).pOpcycles))))
    ⊤

Tactic:
rw [eq_top_iff]

Premises used: eq_top_iff
-- 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
x : (↑(shortComplexH1 (A.coinvariantsShortComplex S).X₁).X₂ : Type u)
_ :
  Membership.mem (γ := Submodule k (↑(shortComplexH1 (A.coinvariantsShortComplex S).X₁).X₂ : Type u)) ⊤ x →
    Membership.mem (γ := Submodule k (↑(shortComplexH1 (A.coinvariantsShortComplex S).X₁).X₂ : Type u))
      (Submodule.comap (M₂ := (↑(shortComplexH1 A).opcycles : Type u))
        (ModuleCat.Hom.hom
          (Hom.τ₂ (mapShortComplexH1 (MonoidHom.id G) (A.coinvariantsShortComplex S).f) ≫ (shortComplexH1 A).pOpcycles))
        (LinearMap.range
          (ModuleCat.Hom.hom ((mapShortComplexH1 S.subtype (𝟙 (res S.subtype A))).τ₂ ≫ (shortComplexH1 A).pOpcycles))))
      x
⊢ Membership.mem (γ := Submodule k (↑(shortComplexH1 (A.coinvariantsShortComplex S).X₁).X₂ : Type u)) ⊤ x →
    Membership.mem (γ := Submodule k (↑(shortComplexH1 (A.coinvariantsShortComplex S).X₁).X₂ : Type u))
      (Submodule.comap (M₂ := (↑(shortComplexH1 A).opcycles : Type u))
        (ModuleCat.Hom.hom
          (Hom.τ₂ (mapShortComplexH1 (MonoidHom.id G) (A.coinvariantsShortComplex S).f) ≫ (shortComplexH1 A).pOpcycles))
        (LinearMap.range
          (ModuleCat.Hom.hom ((mapShortComplexH1 S.subtype (𝟙 (res S.subtype A))).τ₂ ≫ (shortComplexH1 A).pOpcycles))))
      x

Tactic:
_
-- 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
x : (↑(shortComplexH1 (A.coinvariantsShortComplex S).X₁).X₂ : Type u)
h : Membership.mem (γ := Submodule k (↑(shortComplexH1 (A.coinvariantsShortComplex S).X₁).X₂ : Type u)) ⊤ x
rcases :
  ∀ (X : G →₀ ↥S →₀ (↑A : Type u))
    (hX :
      mapRange
          (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (chains₁ToCoinvariantsKer (res S.subtype A))) :
            (a : (↑(ModuleCat.of k (↥S →₀ (↑(res S.subtype A) : Type u))) : Type u)) →
              (↑(ModuleCat.of k ↥(Coinvariants.ker (res S.subtype A).ρ)) : Type u))
          ⋯ X =
        x),
    Membership.mem (γ := Submodule k (↑(shortComplexH1 (A.coinvariantsShortComplex S).X₁).X₂ : Type u))
      (Submodule.comap (M₂ := (↑(shortComplexH1 A).opcycles : Type u))
        (ModuleCat.Hom.hom
          (Hom.τ₂ (mapShortComplexH1 (MonoidHom.id G) (A.coinvariantsShortComplex S).f) ≫ (shortComplexH1 A).pOpcycles))
        (LinearMap.range
          (ModuleCat.Hom.hom ((mapShortComplexH1 S.subtype (𝟙 (res S.subtype A))).τ₂ ≫ (shortComplexH1 A).pOpcycles))))
      x
⊢ Membership.mem (γ := Submodule k (↑(shortComplexH1 (A.coinvariantsShortComplex S).X₁).X₂ : Type u))
    (Submodule.comap (M₂ := (↑(shortComplexH1 A).opcycles : Type u))
      (ModuleCat.Hom.hom
        (Hom.τ₂ (mapShortComplexH1 (MonoidHom.id G) (A.coinvariantsShortComplex S).f) ≫ (shortComplexH1 A).pOpcycles))
      (LinearMap.range
        (ModuleCat.Hom.hom ((mapShortComplexH1 S.subtype (𝟙 (res S.subtype A))).τ₂ ≫ (shortComplexH1 A).pOpcycles))))
    x

Tactic:
rcases mapRange_surjective _ (map_zero _) (chains₁ToCoinvariantsKer_surjective
    (res S.subtype A)) x with ⟨(X : G →₀ S →₀ A), hX⟩

Premises used: groupHomology.chains₁ToCoinvariantsKer_surjective, Subgroup.subtype, map_zero, Rep.res, Finsupp.mapRange_surjective
-- 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
x : (↑(shortComplexH1 (A.coinvariantsShortComplex S).X₁).X₂ : Type u)
h_1 : Membership.mem (γ := Submodule k (↑(shortComplexH1 (A.coinvariantsShortComplex S).X₁).X₂ : Type u)) ⊤ x
X : G →₀ ↥S →₀ (↑A : Type u)
hX :
  mapRange
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (chains₁ToCoinvariantsKer (res S.subtype A))) :
        (a : (↑(ModuleCat.of k (↥S →₀ (↑(res S.subtype A) : Type u))) : Type u)) →
          (↑(ModuleCat.of k ↥(Coinvariants.ker (res S.subtype A).ρ)) : Type u))
      ⋯ X =
    x
Y : ↥S →₀ (↑A : Type u) :=
  X.sum fun (g : G) (f : ↥S →₀ (↑A : Type u)) ↦
    HSub.hSub (α := ↥S →₀ (↑A : Type u))
      ((mapRange.linearMap ((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g⁻¹) :
            (a : ↥S →₀ (↑A : Type u)) → ↥S →₀ (↑A : Type u))
          ((lmapDomain (↑A : Type u) k fun (s : ↥S) ↦
                (((MulAut.conjNormal : (a : G) → MulAut ↥S) g⁻¹ : MulAut ↥S) : (a : ↥S) → ↥S) s :
              (a : ↥S →₀ (↑A : Type u)) → ↥S →₀ (↑A : Type u))
            f) :
        ↥S →₀ (↑A : Type u))
      f
Z : G × G →₀ (↑A : Type u) :=
  X.sum fun (g : G) (f : ↥S →₀ (↑A : Type u)) ↦
    HSub.hSub (α := G × G →₀ (↑A : Type u)) (β := G × G →₀ (↑A : Type u))
      ((lmapDomain (↑A : Type u) k fun (s : ↥S) ↦ (g, g⁻¹ * (↑s : G) * g) :
            (a : ↥S →₀ (↑A : Type u)) → G × G →₀ (↑A : Type u))
          f :
        G × G →₀ (↑A : Type u))
      ((lmapDomain (↑A : Type u) k fun (s : ↥S) ↦ ((↑s : G), g) : (a : ↥S →₀ (↑A : Type u)) → G × G →₀ (↑A : Type u))
          f :
        G × G →₀ (↑A : Type u))
h :
  Eq (α := (↑(shortComplexH1 A).opcycles : Type u))
    ((ModuleCat.Hom.hom ((mapShortComplexH1 S.subtype (𝟙 (res S.subtype A))).τ₂ ≫ (shortComplexH1 A).pOpcycles) :
          (a : (↑(shortComplexH1 (res S.subtype A)).X₂ : Type u)) → (↑(shortComplexH1 A).opcycles : Type u))
        Y :
      (↑(shortComplexH1 A).opcycles : Type u))
    ((ModuleCat.Hom.hom
            (Hom.τ₂ (mapShortComplexH1 (MonoidHom.id G) (A.coinvariantsShortComplex S).f) ≫
              (shortComplexH1 A).pOpcycles) :
          (a : (↑(shortComplexH1 (A.coinvariantsShortComplex S).X₁).X₂ : Type u)) →
            (↑(shortComplexH1 A).opcycles : Type u))
        x :
      (↑(shortComplexH1 A).opcycles : Type u))
⊢ Membership.mem (γ := Submodule k (↑(shortComplexH1 (A.coinvariantsShortComplex S).X₁).X₂ : Type u))
    (Submodule.comap (M₂ := (↑(shortComplexH1 A).opcycles : Type u))
      (ModuleCat.Hom.hom
        (Hom.τ₂ (mapShortComplexH1 (MonoidHom.id G) (A.coinvariantsShortComplex S).f) ≫ (shortComplexH1 A).pOpcycles))
      (LinearMap.range
        (ModuleCat.Hom.hom ((mapShortComplexH1 S.subtype (𝟙 (res S.subtype A))).τ₂ ≫ (shortComplexH1 A).pOpcycles))))
    x

Tactic:
use Y
-- 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
rw :
  Function.Surjective (α := (↑(H1CoresCoinf A S).X₂ : Type u)) (β := (↑(H1CoresCoinf A S).X₃ : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (H1CoresCoinf A S).g) :
      (a : (↑(H1CoresCoinf A S).X₂ : Type u)) → (↑(H1CoresCoinf A S).X₃ : Type u))
⊢ Epi (H1CoresCoinf A S).g

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
x : ↥(cycles₁ (A.quotientToCoinvariants S))
h :
  ∀ (y : (↑(ModuleCat.of k ↥(cycles₁ (A.toCoinvariants S))) : Type u))
    (hy :
      (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (Y := ModuleCat.of k ↥(cycles₁ ((A.toCoinvariants S).ofQuotient S)))
              (mapCycles₁ (QuotientGroup.mk' S) (Iso.inv ((A.toCoinvariants S).resOfQuotientIso S))) :
            (a : (↑(ModuleCat.of k ↥(cycles₁ (A.toCoinvariants S))) : Type u)) →
              (↑(ModuleCat.of k ↥(cycles₁ ((A.toCoinvariants S).ofQuotient S))) : Type u))
          y =
        x),
    ∃ (a : (↑(H1CoresCoinf A S).X₂ : Type u)),
      Eq (α := (↑(H1CoresCoinf A S).X₃ : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (H1CoresCoinf A S).g :
              (a : (↑(H1CoresCoinf A S).X₂ : Type u)) → (↑(H1CoresCoinf A S).X₃ : Type u))
            a :
          (↑(H1CoresCoinf A S).X₃ : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (X := ModuleCat.of k ↥(cycles₁ (A.quotientToCoinvariants S)))
                (H1π (A.quotientToCoinvariants S)) :
              (a : (↑(ModuleCat.of k ↥(cycles₁ (A.quotientToCoinvariants S))) : Type u)) →
                (↑(H1 (A.quotientToCoinvariants S)) : Type u))
            x :
          (↑(H1 (A.quotientToCoinvariants S)) : Type u))
⊢ ∃ (a : (↑(H1CoresCoinf A S).X₂ : Type u)),
    Eq (α := (↑(H1CoresCoinf A S).X₃ : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (H1CoresCoinf A S).g :
            (a : (↑(H1CoresCoinf A S).X₂ : Type u)) → (↑(H1CoresCoinf A S).X₃ : Type u))
          a :
        (↑(H1CoresCoinf A S).X₃ : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (X := ModuleCat.of k ↥(cycles₁ (A.quotientToCoinvariants S)))
              (H1π (A.quotientToCoinvariants S)) :
            (a : (↑(ModuleCat.of k ↥(cycles₁ (A.quotientToCoinvariants S))) : Type u)) →
              (↑(H1 (A.quotientToCoinvariants S)) : Type u))
          x :
        (↑(H1 (A.quotientToCoinvariants S)) : Type u))

Tactic:
rcases (ModuleCat.epi_iff_surjective _).1
    (mapCycles₁_quotientGroupMk'_epi (A.toCoinvariants S) S) x with ⟨y, hy⟩

Premises used: ModuleCat.epi_iff_surjective, Rep.toCoinvariants, Iff.mp, groupHomology.mapCycles₁_quotientGroupMk'_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
f : G →* H
φ : A ⟶ res f B
n : ℕ
S : Subgroup G
inst_3 : S.Normal
x : ↥(cycles₁ (A.quotientToCoinvariants S))
y : (↑(ModuleCat.of k ↥(cycles₁ (A.toCoinvariants S))) : Type u)
hy :
  (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (Y := ModuleCat.of k ↥(cycles₁ ((A.toCoinvariants S).ofQuotient S)))
          (mapCycles₁ (QuotientGroup.mk' S) (Iso.inv ((A.toCoinvariants S).resOfQuotientIso S))) :
        (a : (↑(ModuleCat.of k ↥(cycles₁ (A.toCoinvariants S))) : Type u)) →
          (↑(ModuleCat.of k ↥(cycles₁ ((A.toCoinvariants S).ofQuotient S))) : Type u))
      y =
    x
h :
  ∀ (Y : G →₀ (↑A : Type u))
    (hY :
      mapRange
          (⇑(Coinvariants.mk (MonoidHom.comp A.ρ S.subtype)) :
            (a : (↑A : Type u)) → Coinvariants (MonoidHom.comp A.ρ S.subtype))
          ⋯ Y =
        (↑y : G →₀ (↑(A.toCoinvariants S) : Type u))),
    ∃ (a : (↑(H1CoresCoinf A S).X₂ : Type u)),
      Eq (α := (↑(H1CoresCoinf A S).X₃ : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (H1CoresCoinf A S).g :
              (a : (↑(H1CoresCoinf A S).X₂ : Type u)) → (↑(H1CoresCoinf A S).X₃ : Type u))
            a :
          (↑(H1CoresCoinf A S).X₃ : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (X := ModuleCat.of k ↥(cycles₁ (A.quotientToCoinvariants S)))
                (H1π (A.quotientToCoinvariants S)) :
              (a : (↑(ModuleCat.of k ↥(cycles₁ (A.quotientToCoinvariants S))) : Type u)) →
                (↑(H1 (A.quotientToCoinvariants S)) : Type u))
            x :
          (↑(H1 (A.quotientToCoinvariants S)) : Type u))
⊢ ∃ (a : (↑(H1CoresCoinf A S).X₂ : Type u)),
    Eq (α := (↑(H1CoresCoinf A S).X₃ : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (H1CoresCoinf A S).g :
            (a : (↑(H1CoresCoinf A S).X₂ : Type u)) → (↑(H1CoresCoinf A S).X₃ : Type u))
          a :
        (↑(H1CoresCoinf A S).X₃ : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (X := ModuleCat.of k ↥(cycles₁ (A.quotientToCoinvariants S)))
              (H1π (A.quotientToCoinvariants S)) :
            (a : (↑(ModuleCat.of k ↥(cycles₁ (A.quotientToCoinvariants S))) : Type u)) →
              (↑(H1 (A.quotientToCoinvariants S)) : Type u))
          x :
        (↑(H1 (A.quotientToCoinvariants S)) : Type u))

Tactic:
rcases mapRange_surjective _ (map_zero _)
    (Coinvariants.mk_surjective (A.ρ.comp S.subtype)) y.1 with ⟨Y, hY⟩

Premises used: Subgroup.subtype, map_zero, MonoidHom.comp, Finsupp.mapRange_surjective, Rep.ρ, Subtype.val, Representation.Coinvariants.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
x : ↥(cycles₁ (A.quotientToCoinvariants S))
y : (↑(ModuleCat.of k ↥(cycles₁ (A.toCoinvariants S))) : Type u)
hy :
  (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (Y := ModuleCat.of k ↥(cycles₁ ((A.toCoinvariants S).ofQuotient S)))
          (mapCycles₁ (QuotientGroup.mk' S) (Iso.inv ((A.toCoinvariants S).resOfQuotientIso S))) :
        (a : (↑(ModuleCat.of k ↥(cycles₁ (A.toCoinvariants S))) : Type u)) →
          (↑(ModuleCat.of k ↥(cycles₁ ((A.toCoinvariants S).ofQuotient S))) : Type u))
      y =
    x
Y : G →₀ (↑A : Type u)
hY :
  mapRange
      (⇑(Coinvariants.mk (MonoidHom.comp A.ρ S.subtype)) :
        (a : (↑A : Type u)) → Coinvariants (MonoidHom.comp A.ρ S.subtype))
      ⋯ Y =
    (↑y : G →₀ (↑(A.toCoinvariants S) : Type u))
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
have h' := congr($((mapShortComplexH1 (B := toCoinvariants A S)
      (MonoidHom.id G) (toCoinvariantsMkQ A S)).comm₂₃) Y)
-- 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
x : ↥(cycles₁ (A.quotientToCoinvariants S))
y : (↑(ModuleCat.of k ↥(cycles₁ (A.toCoinvariants S))) : Type u)
hy :
  (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (Y := ModuleCat.of k ↥(cycles₁ ((A.toCoinvariants S).ofQuotient S)))
          (mapCycles₁ (QuotientGroup.mk' S) (Iso.inv ((A.toCoinvariants S).resOfQuotientIso S))) :
        (a : (↑(ModuleCat.of k ↥(cycles₁ (A.toCoinvariants S))) : Type u)) →
          (↑(ModuleCat.of k ↥(cycles₁ ((A.toCoinvariants S).ofQuotient S))) : Type u))
      y =
    x
Y : G →₀ (↑A : Type u)
hY :
  mapRange
      (⇑(Coinvariants.mk (MonoidHom.comp A.ρ S.subtype)) :
        (a : (↑A : Type u)) → Coinvariants (MonoidHom.comp A.ρ S.subtype))
      ⋯ Y =
    (↑y : G →₀ (↑(A.toCoinvariants S) : Type u))
h' : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Membership.mem (α := (↑(ModuleCat.of k (↑A : Type u)) : Type u)) (Coinvariants.ker (MonoidHom.comp A.ρ S.subtype))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (d₁₀ A) :
          (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
        Y :
      (↑(ModuleCat.of k (↑A : Type u)) : Type u))

Tactic:
simp_all [shortComplexH1, ← Coinvariants.mk_eq_zero]

Premises used: Representation.Coinvariants.mk_eq_zero, groupHomology.shortComplexH1