awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality (goal)
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
x_1 : (↑((inhomogeneousCochains A).X 3) : Type u)
g : G × G × G
x : Fin 3
⊢ Eq (α := H)
    ((fun (x : Fin 3 → G) ↦ ((⇑f : (a : G) → H) ∘ x : Fin 3 → H))
        ((Equiv.symm
              (Equiv.trans (Equiv.symm (Fin.consEquiv.{u} (n := 2) fun (a : Fin 3) ↦ G))
                ((Equiv.refl G).prodCongr (piFinTwoEquiv fun (x : Fin 2) ↦ G))) :
            (a : G × G × G) → (i : Fin (2 + 1)) → G)
          g)
        x :
      H)
    ((Equiv.symm
            (Equiv.trans (Equiv.symm (Fin.consEquiv.{u} (n := 2) fun (a : Fin 3) ↦ H))
              ((Equiv.refl H).prodCongr (piFinTwoEquiv fun (x : Fin 2) ↦ H))) :
          (a : H × H × H) → (i : Fin (2 + 1)) → H)
        (Prod.map (⇑f : (a : G) → H) (Prod.map (⇑f : (a : G) → H) (⇑f : (a : G) → H)) g) x :
      H)
have hf : Eq (α := H)
  ((fun (x : Fin 3 → G) ↦ ((⇑f : (a : G) → H) ∘ x : Fin 3 → H))
      ((Equiv.symm
            (Equiv.trans (Equiv.symm (Fin.consEquiv.{u} (n := 2) fun (a : Fin 3) ↦ G))
              ((Equiv.refl G).prodCongr (piFinTwoEquiv fun (x : Fin 2) ↦ G))) :
          (a : G × G × G) → (i : Fin (2 + 1)) → G)
        g)
      ((fun (i : Fin ({ len := 2 : SimplexCategory }.len + 1)) ↦ i) ⟨0, sorry⟩) :
    H)
  ((Equiv.symm
          (Equiv.trans (Equiv.symm (Fin.consEquiv.{u} (n := 2) fun (a : Fin 3) ↦ H))
            ((Equiv.refl H).prodCongr (piFinTwoEquiv fun (x : Fin 2) ↦ H))) :
        (a : H × H × H) → (i : Fin (2 + 1)) → H)
      (Prod.map (⇑f : (a : G) → H) (Prod.map (⇑f : (a : G) → H) (⇑f : (a : G) → H)) g)
      ((fun (i : Fin ({ len := 2 : SimplexCategory }.len + 1)) ↦ i) ⟨0, sorry⟩) :
    H)
Tactic: fin_cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality (goal)
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
x_1 : (↑((inhomogeneousCochains A).X 3) : Type u)
g : G × G × G
x : Fin 3
hf :
  Eq (α := H)
    ((fun (x : Fin 3 → G) ↦ ((⇑f : (a : G) → H) ∘ x : Fin 3 → H))
        ((Equiv.symm
              (Equiv.trans (Equiv.symm (Fin.consEquiv.{u} (n := 2) fun (a : Fin 3) ↦ G))
                ((Equiv.refl G).prodCongr (piFinTwoEquiv fun (x : Fin 2) ↦ G))) :
            (a : G × G × G) → (i : Fin (2 + 1)) → G)
          g)
        ((fun (i : Fin ({ len := 2 : SimplexCategory }.len + 1)) ↦ i) ⟨0, ⋯⟩) :
      H)
    ((Equiv.symm
            (Equiv.trans (Equiv.symm (Fin.consEquiv.{u} (n := 2) fun (a : Fin 3) ↦ H))
              ((Equiv.refl H).prodCongr (piFinTwoEquiv fun (x : Fin 2) ↦ H))) :
          (a : H × H × H) → (i : Fin (2 + 1)) → H)
        (Prod.map (⇑f : (a : G) → H) (Prod.map (⇑f : (a : G) → H) (⇑f : (a : G) → H)) g)
        ((fun (i : Fin ({ len := 2 : SimplexCategory }.len + 1)) ↦ i) ⟨0, ⋯⟩) :
      H)
⊢ Eq (α := H)
    ((fun (x : Fin 3 → G) ↦ ((⇑f : (a : G) → H) ∘ x : Fin 3 → H))
        ((Equiv.symm
              (Equiv.trans (Equiv.symm (Fin.consEquiv.{u} (n := 2) fun (a : Fin 3) ↦ G))
                ((Equiv.refl G).prodCongr (piFinTwoEquiv fun (x : Fin 2) ↦ G))) :
            (a : G × G × G) → (i : Fin (2 + 1)) → G)
          g)
        x :
      H)
    ((Equiv.symm
            (Equiv.trans (Equiv.symm (Fin.consEquiv.{u} (n := 2) fun (a : Fin 3) ↦ H))
              ((Equiv.refl H).prodCongr (piFinTwoEquiv fun (x : Fin 2) ↦ H))) :
          (a : H × H × H) → (i : Fin (2 + 1)) → H)
        (Prod.map (⇑f : (a : G) → H) (Prod.map (⇑f : (a : G) → H) (⇑f : (a : G) → H)) g) x :
      H)
have hf₁ : Eq (α := H)
  ((fun (x : Fin 3 → G) ↦ ((⇑f : (a : G) → H) ∘ x : Fin 3 → H))
      ((Equiv.symm
            (Equiv.trans (Equiv.symm (Fin.consEquiv.{u} (n := 2) fun (a : Fin 3) ↦ G))
              ((Equiv.refl G).prodCongr (piFinTwoEquiv fun (x : Fin 2) ↦ G))) :
          (a : G × G × G) → (i : Fin (2 + 1)) → G)
        g)
      ((fun (i : Fin ({ len := 2 : SimplexCategory }.len + 1)) ↦ i) ⟨1, sorry⟩) :
    H)
  ((Equiv.symm
          (Equiv.trans (Equiv.symm (Fin.consEquiv.{u} (n := 2) fun (a : Fin 3) ↦ H))
            ((Equiv.refl H).prodCongr (piFinTwoEquiv fun (x : Fin 2) ↦ H))) :
        (a : H × H × H) → (i : Fin (2 + 1)) → H)
      (Prod.map (⇑f : (a : G) → H) (Prod.map (⇑f : (a : G) → H) (⇑f : (a : G) → H)) g)
      ((fun (i : Fin ({ len := 2 : SimplexCategory }.len + 1)) ↦ i) ⟨1, sorry⟩) :
    H)
Tactic: fin_cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A B : Rep k G
f : A ⟶ B
⊢ map (MonoidHom.id G) f 0 ≫ (H0Iso B).hom = (H0Iso A).hom ≫ CategoryTheory.Functor.map (invariantsFunctor k G) f
have simp : (H0Iso A).hom ≫ (shortComplexH0 A).f ≫ Hom.toModuleCatHom f =
  (H0Iso A).hom ≫ CategoryTheory.Functor.map (invariantsFunctor k G) f ≫ (shortComplexH0 B).f
Tactic: simp only [← cancel_mono (shortComplexH0 B).f, Category.assoc, map_H0Iso_hom_f]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality (hypothesis)
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A_1 : Rep k H
B_1 : Rep k G
f_1 : G →* H
φ : Quiver.Hom.{?u.156077, max (?u.156077 + 1) u} (res f_1 A_1) B_1
n : ℕ
A B : Rep k G
f : A ⟶ B
inst_3 : Mono f
Z : ModuleCat k
g h : Z ⟶ groupCohomology A 0
hgh : Eq (α := Z ⟶ groupCohomology B 0) (g ≫ map (MonoidHom.id G) f 0) (h ≫ map (MonoidHom.id G) f 0)
⊢ g = h
have hgh₁ : Eq (α := Z ⟶ ModuleCat.of k ↥B.ρ.invariants) (g ≫ (H0Iso A).hom ≫ CategoryTheory.Functor.map (invariantsFunctor k G) f)
  (h ≫ (H0Iso A).hom ≫ CategoryTheory.Functor.map (invariantsFunctor k G) f)
Tactic: simp only [← cancel_mono (H0Iso B).hom, Category.assoc, map_id_comp_H0Iso_hom] at hgh
Cleared hypotheses: hgh
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality (goal)
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 : ℕ
⊢ Hom.toModuleCatHom φ ≫ (shortComplexH1.{u, u_1} B).f = (shortComplexH1.{u, u_1} A).f ≫ cochainsMap₁ f φ
have hf : ∀ (x : (↑(shortComplexH1.{u, u_1} A).X₁ : Type (max u u_1))),
  Eq (α := (↑(shortComplexH1.{u, u_1} B).X₂ : Type (max u u_1)))
    ((ModuleCat.Hom.hom (Hom.toModuleCatHom φ ≫ (shortComplexH1.{u, u_1} B).f) :
          (a : (↑(shortComplexH1 A).X₁ : Type (max u u_1))) → (↑(shortComplexH1 B).X₂ : Type (max u u_1)))
        x :
      (↑(shortComplexH1.{u, u_1} B).X₂ : Type (max u u_1)))
    ((ModuleCat.Hom.hom ((shortComplexH1.{u, u_1} A).f ≫ cochainsMap₁ f φ) :
          (a : (↑(shortComplexH1 A).X₁ : Type (max u u_1))) → (↑(shortComplexH1 B).X₂ : Type (max u u_1)))
        x :
      (↑(shortComplexH1.{u, u_1} B).X₂ : Type (max u u_1)))
Tactic: ext x
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality (goal)
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 : ℕ
x : (↑(shortComplexH1.{u, u_1} A).X₁ : Type (max u u_1))
⊢ Eq (α := (↑(shortComplexH1.{u, u_1} B).X₂ : Type (max u u_1)))
    ((ModuleCat.Hom.hom (Hom.toModuleCatHom φ ≫ (shortComplexH1.{u, u_1} B).f) :
          (a : (↑(shortComplexH1 A).X₁ : Type (max u u_1))) → (↑(shortComplexH1 B).X₂ : Type (max u u_1)))
        x :
      (↑(shortComplexH1.{u, u_1} B).X₂ : Type (max u u_1)))
    ((ModuleCat.Hom.hom ((shortComplexH1.{u, u_1} A).f ≫ cochainsMap₁ f φ) :
          (a : (↑(shortComplexH1 A).X₁ : Type (max u u_1))) → (↑(shortComplexH1 B).X₂ : Type (max u u_1)))
        x :
      (↑(shortComplexH1.{u, u_1} B).X₂ : Type (max u u_1)))
have hf : ∀ (g : G),
  Eq (α := (↑B : Type (max u u_1)))
    ((ModuleCat.Hom.hom (Hom.toModuleCatHom φ ≫ (shortComplexH1.{u, u_1} B).f) :
          (a : (↑(shortComplexH1 A).X₁ : Type (max u u_1))) → (↑(shortComplexH1 B).X₂ : Type (max u u_1)))
        x g :
      (↑B : Type (max u u_1)))
    ((ModuleCat.Hom.hom ((shortComplexH1.{u, u_1} A).f ≫ cochainsMap₁ f φ) :
          (a : (↑(shortComplexH1 A).X₁ : Type (max u u_1))) → (↑(shortComplexH1 B).X₂ : Type (max u u_1)))
        x g :
      (↑B : Type (max u u_1)))
Tactic: funext g
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality (goal)
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 : ℕ
⊢ cochainsMap₁ f φ ≫ (shortComplexH1.{u, u_1} B).g = (shortComplexH1.{u, u_1} A).g ≫ cochainsMap₂ f φ
have hf : ∀ (x : (↑(shortComplexH1.{u, u_1} A).X₂ : Type (max u u_1))),
  Eq (α := (↑(shortComplexH1.{u, u_1} B).X₃ : Type (max u u_1)))
    ((ModuleCat.Hom.hom (cochainsMap₁ f φ ≫ (shortComplexH1.{u, u_1} B).g) :
          (a : (↑(shortComplexH1 A).X₂ : Type (max u u_1))) → (↑(shortComplexH1 B).X₃ : Type (max u u_1)))
        x :
      (↑(shortComplexH1.{u, u_1} B).X₃ : Type (max u u_1)))
    ((ModuleCat.Hom.hom ((shortComplexH1.{u, u_1} A).g ≫ cochainsMap₂ f φ) :
          (a : (↑(shortComplexH1 A).X₂ : Type (max u u_1))) → (↑(shortComplexH1 B).X₃ : Type (max u u_1)))
        x :
      (↑(shortComplexH1.{u, u_1} B).X₃ : Type (max u u_1)))
Tactic: ext x
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality (goal)
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 : ℕ
x : (↑(shortComplexH1.{u, u_1} A).X₂ : Type (max u u_1))
⊢ Eq (α := (↑(shortComplexH1.{u, u_1} B).X₃ : Type (max u u_1)))
    ((ModuleCat.Hom.hom (cochainsMap₁ f φ ≫ (shortComplexH1.{u, u_1} B).g) :
          (a : (↑(shortComplexH1 A).X₂ : Type (max u u_1))) → (↑(shortComplexH1 B).X₃ : Type (max u u_1)))
        x :
      (↑(shortComplexH1.{u, u_1} B).X₃ : Type (max u u_1)))
    ((ModuleCat.Hom.hom ((shortComplexH1.{u, u_1} A).g ≫ cochainsMap₂ f φ) :
          (a : (↑(shortComplexH1 A).X₂ : Type (max u u_1))) → (↑(shortComplexH1 B).X₃ : Type (max u u_1)))
        x :
      (↑(shortComplexH1.{u, u_1} B).X₃ : Type (max u u_1)))
have hf : ∀ (g : G × G),
  Eq (α := (↑B : Type (max u u_1)))
    ((ModuleCat.Hom.hom (cochainsMap₁ f φ ≫ (shortComplexH1.{u, u_1} B).g) :
          (a : (↑(shortComplexH1 A).X₂ : Type (max u u_1))) → (↑(shortComplexH1 B).X₃ : Type (max u u_1)))
        x g :
      (↑B : Type (max u u_1)))
    ((ModuleCat.Hom.hom ((shortComplexH1.{u, u_1} A).g ≫ cochainsMap₂ f φ) :
          (a : (↑(shortComplexH1 A).X₂ : Type (max u u_1))) → (↑(shortComplexH1 B).X₃ : Type (max u u_1)))
        x g :
      (↑B : Type (max u u_1)))
Tactic: funext g
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality (goal)
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
φ : res 1 A ⟶ B
⊢ mapCocycles₁.{u, u_1} 1 φ = 0
have rw : (shortComplexH1.{u, u_1} A).moduleCatLeftHomologyData.i ≫ (mapShortComplexH1 1 φ).τ₂ =
  0 ≫ (shortComplexH1.{u, u_1} B).moduleCatLeftHomologyData.i
Tactic: rw [← cancel_mono (moduleCatLeftHomologyData (shortComplexH1 B)).i, cyclesMap'_i]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality (goal)
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
φ : res 1 A ⟶ B
⊢ (shortComplexH1.{u, u_1} A).moduleCatLeftHomologyData.i ≫ (mapShortComplexH1 1 φ).τ₂ =
    0 ≫ (shortComplexH1.{u, u_1} B).moduleCatLeftHomologyData.i
have refine : ∀ (x : (↑(shortComplexH1.{u, u_1} A).moduleCatLeftHomologyData.K : Type (max u u_1))) (y : G),
  Eq (α := (↑B : Type (max u u_1)))
    ((ModuleCat.Hom.hom ((shortComplexH1.{u, u_1} A).moduleCatLeftHomologyData.i ≫ (mapShortComplexH1 1 φ).τ₂) :
          (a : (↑(shortComplexH1 A).moduleCatLeftHomologyData.K : Type (max u u_1))) →
            (↑(shortComplexH1 B).X₂ : Type (max u u_1)))
        x y :
      (↑B : Type (max u u_1)))
    ((ModuleCat.Hom.hom (0 ≫ (shortComplexH1.{u, u_1} B).moduleCatLeftHomologyData.i) :
          (a : (↑(shortComplexH1 A).moduleCatLeftHomologyData.K : Type (max u u_1))) →
            (↑(shortComplexH1 B).X₂ : Type (max u u_1)))
        x y :
      (↑B : Type (max u u_1)))
Tactic: refine ModuleCat.hom_ext (LinearMap.ext fun _ ↦ funext fun y => ?_)
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality (goal)
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A_1 : Rep k H
B : Rep k G
f : G →* H
φ : Quiver.Hom.{?u.259726, max (?u.259726 + 1) u} (res f A_1) B
n : ℕ
A : Rep k G
S : Subgroup G
inst_3 : S.Normal
⊢ Eq (α := groupCohomology (A.quotientToInvariants S) 1 ⟶ groupCohomology (res S.subtype A) 1)
    (map (QuotientGroup.mk' S) (ofHom (A.ρ.quotientToInvariants_lift S)) 1 ≫ map S.subtype (𝟙 (res S.subtype A)) 1) 0
have rw : Eq (α := groupCohomology (A.quotientToInvariants S) 1 ⟶ groupCohomology (res S.subtype A) 1)
  (map (MonoidHom.comp (QuotientGroup.mk' S) S.subtype)
    (CategoryTheory.Functor.map (resFunctor S.subtype) (ofHom (A.ρ.quotientToInvariants_lift S)) ≫ 𝟙 (res S.subtype A))
    1)
  0
Tactic: rw [← map_comp, Category.comp_id, congr (QuotientGroup.mk'_comp_subtype S)
    (fun f φ => map f φ 1), map₁_one]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality (goal)
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A_1 : Rep k H
B : Rep k G
f : G →* H
φ : Quiver.Hom.{?u.259726, max (?u.259726 + 1) u} (res f A_1) B
n : ℕ
A : Rep k G
S : Subgroup G
inst_3 : S.Normal
rw :
  Eq (α := groupCohomology (A.quotientToInvariants S) 1 ⟶ groupCohomology (res S.subtype A) 1)
    (map (MonoidHom.comp (QuotientGroup.mk' S) S.subtype)
      (CategoryTheory.Functor.map (resFunctor S.subtype) (ofHom (A.ρ.quotientToInvariants_lift S)) ≫
        𝟙 (res S.subtype A))
      1)
    0
⊢ Eq (α := groupCohomology (A.quotientToInvariants S) 1 ⟶ groupCohomology (res S.subtype A) 1)
    (map (QuotientGroup.mk' S) (ofHom (A.ρ.quotientToInvariants_lift S)) 1 ≫ map S.subtype (𝟙 (res S.subtype A)) 1) 0
have rw₁ : Eq (α := groupCohomology (A.quotientToInvariants S) 1 ⟶ groupCohomology (res S.subtype A) 1)
  (map (MonoidHom.comp (QuotientGroup.mk' S) S.subtype)
    (CategoryTheory.Functor.map (resFunctor S.subtype) (ofHom (A.ρ.quotientToInvariants_lift S))) 1)
  0
Tactic: rw [← map_comp, Category.comp_id, congr (QuotientGroup.mk'_comp_subtype S)
    (fun f φ => map f φ 1), map₁_one]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality (goal)
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A_1 : Rep k H
B : Rep k G
f : G →* H
φ : Quiver.Hom.{?u.259726, max (?u.259726 + 1) u} (res f A_1) B
n : ℕ
A : Rep k G
S : Subgroup G
inst_3 : S.Normal
rw :
  Eq (α := groupCohomology (A.quotientToInvariants S) 1 ⟶ groupCohomology (res S.subtype A) 1)
    (map (MonoidHom.comp (QuotientGroup.mk' S) S.subtype)
      (CategoryTheory.Functor.map (resFunctor S.subtype) (ofHom (A.ρ.quotientToInvariants_lift S)) ≫
        𝟙 (res S.subtype A))
      1)
    0
rw₁ :
  Eq (α := groupCohomology (A.quotientToInvariants S) 1 ⟶ groupCohomology (res S.subtype A) 1)
    (map (MonoidHom.comp (QuotientGroup.mk' S) S.subtype)
      (CategoryTheory.Functor.map (resFunctor S.subtype) (ofHom (A.ρ.quotientToInvariants_lift S))) 1)
    0
⊢ Eq (α := groupCohomology (A.quotientToInvariants S) 1 ⟶ groupCohomology (res S.subtype A) 1)
    (map (QuotientGroup.mk' S) (ofHom (A.ρ.quotientToInvariants_lift S)) 1 ≫ map S.subtype (𝟙 (res S.subtype A)) 1) 0
have rw₂ : Eq.{u + 1} (α := groupCohomology (A.quotientToInvariants S) 1 ⟶ groupCohomology (res S.subtype A) 1)
  (map 1
    (Eq.rec (motive := fun (x : ↥S →* G ⧸ S) (h : MonoidHom.comp (QuotientGroup.mk' S) S.subtype = x) ↦
      res x (A.quotientToInvariants S) ⟶ res S.subtype A)
      (CategoryTheory.Functor.map (resFunctor S.subtype) (ofHom (A.ρ.quotientToInvariants_lift S))) sorry)
    1)
  0
Tactic: rw [← map_comp, Category.comp_id, congr (QuotientGroup.mk'_comp_subtype S)
    (fun f φ => map f φ 1), map₁_one]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality (goal)
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A_1 : Rep k H
B : Rep k G
f : G →* H
φ : Quiver.Hom.{?u.259726, max (?u.259726 + 1) u} (res f A_1) B
n : ℕ
A : Rep k G
S : Subgroup G
inst_3 : S.Normal
rw :
  Eq (α := groupCohomology (A.quotientToInvariants S) 1 ⟶ groupCohomology (res S.subtype A) 1)
    (map (MonoidHom.comp (QuotientGroup.mk' S) S.subtype)
      (CategoryTheory.Functor.map (resFunctor S.subtype) (ofHom (A.ρ.quotientToInvariants_lift S)) ≫
        𝟙 (res S.subtype A))
      1)
    0
rw₁ :
  Eq (α := groupCohomology (A.quotientToInvariants S) 1 ⟶ groupCohomology (res S.subtype A) 1)
    (map (MonoidHom.comp (QuotientGroup.mk' S) S.subtype)
      (CategoryTheory.Functor.map (resFunctor S.subtype) (ofHom (A.ρ.quotientToInvariants_lift S))) 1)
    0
rw₂ :
  Eq.{u + 1} (α := groupCohomology (A.quotientToInvariants S) 1 ⟶ groupCohomology (res S.subtype A) 1)
    (map 1
      (Eq.rec (motive := fun (x : ↥S →* G ⧸ S) (h : MonoidHom.comp (QuotientGroup.mk' S) S.subtype = x) ↦
        res x (A.quotientToInvariants S) ⟶ res S.subtype A)
        (CategoryTheory.Functor.map (resFunctor S.subtype) (ofHom (A.ρ.quotientToInvariants_lift S))) ⋯)
      1)
    0
⊢ Eq (α := groupCohomology (A.quotientToInvariants S) 1 ⟶ groupCohomology (res S.subtype A) 1)
    (map (QuotientGroup.mk' S) (ofHom (A.ρ.quotientToInvariants_lift S)) 1 ≫ map S.subtype (𝟙 (res S.subtype A)) 1) 0
have rw₃ : Eq.{u + 1} (α := groupCohomology (A.quotientToInvariants S) 1 ⟶ groupCohomology (res S.subtype A) 1) 0 0
Tactic: rw [← map_comp, Category.comp_id, congr (QuotientGroup.mk'_comp_subtype S)
    (fun f φ => map f φ 1), map₁_one]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality (goal)
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A_1 : Rep k H
B : Rep k G
f : G →* H
φ : Quiver.Hom.{?u.266374, max (?u.266374 + 1) u} (res f A_1) B
n : ℕ
A : Rep k G
S : Subgroup G
inst_3 : S.Normal
⊢ Mono (H1InfRes A S).f
have rw : ∀ (a : (↑(H1InfRes A S).X₁ : Type u)),
  Eq (α := (↑(H1InfRes A S).X₂ : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (H1InfRes A S).f :
            (a : (↑(H1InfRes A S).X₁ : Type u)) → (↑(H1InfRes A S).X₂ : Type u))
          a :
        (↑(H1InfRes A S).X₂ : Type u))
      (0 : (↑(H1InfRes A S).X₂ : Type u)) →
    a = 0
Tactic: rw [ModuleCat.mono_iff_injective, injective_iff_map_eq_zero]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality (hypothesis)
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A_1 : Rep k H
B : Rep k G
f : G →* H
φ : Quiver.Hom.{?u.266374, max (?u.266374 + 1) u} (res f A_1) B
n : ℕ
A : Rep k G
S : Subgroup G
inst_3 : S.Normal
x : ↥(cocycles₁ (A.quotientToInvariants S))
hx :
  Eq (α := (↑(H1InfRes A S).X₂ : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (H1InfRes A S).f :
          (a : (↑(H1InfRes A S).X₁ : Type u)) → (↑(H1InfRes 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 ↥(cocycles₁ (A.quotientToInvariants S)))
                (H1π (A.quotientToInvariants S)) :
              (a : (↑(ModuleCat.of k ↥(cocycles₁ (A.quotientToInvariants S))) : Type u)) →
                (↑(H1 (A.quotientToInvariants S)) : Type u))
            x :
          (↑(H1 (A.quotientToInvariants S)) : Type u)) :
      (↑(H1InfRes A S).X₂ : Type u))
    (0 : (↑(H1InfRes A S).X₂ : Type u))
⊢ Eq (α := (↑(H1InfRes 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 ↥(cocycles₁ (A.quotientToInvariants S)))
            (H1π (A.quotientToInvariants S)) :
          (a : (↑(ModuleCat.of k ↥(cocycles₁ (A.quotientToInvariants S))) : Type u)) →
            (↑(H1 (A.quotientToInvariants S)) : Type u))
        x :
      (↑(H1 (A.quotientToInvariants S)) : Type u))
    (0 : (↑(H1InfRes A S).X₁ : Type u))
have hx₁ : Eq (α := (↑(groupCohomology A 1) : Type u))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (H1π (of A.ρ)) :
        (a : ↥(cocycles₁ (of A.ρ))) → (↑(groupCohomology (of A.ρ) 1) : Type u))
      (((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (X := ModuleCat.of k ↥(cocycles₁ (A.quotientToInvariants S))) (Y :=
                ModuleCat.of k ↥(cocycles₁ (of A.ρ)))
                (mapCocycles₁ (QuotientGroup.mk' S) (ofHom (A.ρ.quotientToInvariants_lift S)) :
                  Quiver.Hom (V := ModuleCat k) (ModuleCat.of k ↥(cocycles₁ (A.quotientToInvariants S)))
                    (ModuleCat.of k ↥(cocycles₁ (of A.ρ)))) :
              (↑(ModuleCat.of k ↥(cocycles₁ (A.quotientToInvariants S))) : Type u) →ₗ[k]
                (↑(ModuleCat.of k ↥(cocycles₁ (of A.ρ))) : Type u)) :
            (a : ↥(cocycles₁ (A.quotientToInvariants S))) → ↥(cocycles₁ (of A.ρ)))
          x :
        ↥(cocycles₁ (of A.ρ))) :
    (↑(groupCohomology (of A.ρ) 1) : Type u))
  (0 : (↑(H1InfRes A S).X₂ : Type u))
Tactic: simp_all only [H1InfRes_X₂, H1InfRes_X₁, H1InfRes_f, H1π_comp_map_apply (QuotientGroup.mk' S)]
Cleared hypotheses: hx