awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality (goal)
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))
have 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
Tactic: refine (H1π_eq_zero_iff _).2 ?_
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality (goal)
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 := ModuleCat.of k ↥(cycles₁ (A.ofQuotient S)))
    (mapCycles₁ (QuotientGroup.mk' S) (Iso.inv (A.resOfQuotientIso S)))
have 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))
Tactic: rw [ModuleCat.epi_iff_surjective]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality (goal)
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
⊢ ∃ (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
have 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
Tactic: choose! s hs using QuotientGroup.mk_surjective (s := S)
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality (hypothesis)
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
⊢ ∃ (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
have hs₁ : QuotientGroup.mk ∘ s = id
Tactic: have hs₁ : QuotientGroup.mk ∘ s = id := funext hs
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality (goal)
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 : (↑(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
have refine : mapDomain s x ∈ cycles₁ A
Tactic: refine ⟨⟨mapDomain s x, ?_⟩, Subtype.ext <| by
    simp [mapCycles₁_hom, ← mapDomain_comp, hs₁, res, Rep.hom_id (of _)]⟩
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality (goal)
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
⊢ x = y
have rw : (↑(s x) : G ⧸ S) = y
Tactic: rw [← hs x, ← hs y, h]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality (goal)
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
⊢ x = y
have rw₁ : Eq (α := G ⧸ S) (↑(s x) : G ⧸ S) (↑(s y) : G ⧸ S)
Tactic: rw [← hs x, ← hs y, h]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality (goal)
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)
⊢ x = y
have rw₂ : Eq (α := G ⧸ S) (↑(s y) : G ⧸ S) (↑(s y) : G ⧸ S)
Tactic: rw [← hs x, ← hs y, h]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality (goal)
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)
⊢ 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
have 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
Tactic: rw [← map_comp, congr (QuotientGroup.mk'_comp_subtype S) (map (n := 1)), map₁_one]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality (goal)
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
⊢ 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
have 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))) sorry)
    1)
  0
Tactic: rw [← map_comp, congr (QuotientGroup.mk'_comp_subtype S) (map (n := 1)), map₁_one]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality (goal)
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
⊢ 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
have rw₂ : Eq.{u + 1} (α := H1 (res S.subtype A) ⟶ H1 (A.ofQuotient S)) 0 0
Tactic: rw [← map_comp, congr (QuotientGroup.mk'_comp_subtype S) (map (n := 1)), map₁_one]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality (goal)
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 := groupHomology A 1) (Y := groupHomology (A.ofQuotient S) 1)
    (map (QuotientGroup.mk' S) (Iso.inv (A.resOfQuotientIso S)) 1)
have convert_3 : Epi (Y := groupHomology (A.ofQuotient S) 1) (H1π A ≫ map (QuotientGroup.mk' S) (Iso.inv (A.resOfQuotientIso S)) 1)
Tactic: convert! epi_of_epi (H1π A) _
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality (goal)
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) (H1π A ≫ map (QuotientGroup.mk' S) (Iso.inv (A.resOfQuotientIso S)) 1)
have convert_3 : Epi (Y := groupHomology (A.ofQuotient S) 1)
  (mapCycles₁ (QuotientGroup.mk' S) (Iso.inv (A.resOfQuotientIso S)) ≫ H1π (A.ofQuotient S))
Tactic: rw [H1π_comp_map]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality (goal)
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)
⊢ (H1CoresCoinfOfTrivial A S).Exact
have rw : (ModuleCat.Hom.hom (H1CoresCoinfOfTrivial A S).g).ker ≤ (ModuleCat.Hom.hom (H1CoresCoinfOfTrivial A S).f).range
Tactic: rw [ShortComplex.moduleCat_exact_iff_ker_sub_range]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality (goal)
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))
⊢ 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))
have 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))
Tactic: rcases x with ⟨x, hxc⟩
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality (hypothesis)
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))
⊢ 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))
have 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))
Tactic: simp_all only [H1CoresCoinfOfTrivial_X₂, H1CoresCoinfOfTrivial_X₃, H1CoresCoinfOfTrivial_g,
    LinearMap.mem_ker, H1π_comp_map_apply (QuotientGroup.mk' S)]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality (hypothesis)
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
⊢ Membership.mem (α := (↑(H1 A) : 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 : ↥(cycles₁ A)) → (↑(H1 A) : Type u))
        (Subtype.mk (p := fun (x : G →₀ (↑A : Type u)) ↦ x ∈ cycles₁ A) x hxc) :
      (↑(H1 A) : Type u))
have hs₁ : QuotientGroup.mk ∘ s = id
Tactic: have hs₁ : QuotientGroup.mk (s := S) ∘ s = id := funext hs
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality (goal)
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
⊢ 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
have 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
Tactic: rw [← map_comp, congr (QuotientGroup.mk'_comp_subtype S) (map (n := 1)), map₁_one]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality (goal)
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
⊢ 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
have 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)) sorry)
    1)
  0
Tactic: rw [← map_comp, congr (QuotientGroup.mk'_comp_subtype S) (map (n := 1)), map₁_one]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality (goal)
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
⊢ 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
have rw₂ : Eq.{u + 1} (α := H1 (res S.subtype A) ⟶ H1 (A.quotientToCoinvariants S)) 0 0
Tactic: rw [← map_comp, congr (QuotientGroup.mk'_comp_subtype S) (map (n := 1)), map₁_one]