awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic (goal)
Goal:
k G : Type u
inst : CommRing k
n_1 : ℕ
inst_1 : Group G
A : Rep k G
n : ℕ
simp : d A n ≫ d A (n + 1) = 0
simp₁ :
  Eq (α :=
    Quiver.Hom (V := ModuleCat k) (ModuleCat.of k ((Fin n → G) → (↑A : Type u)))
      (ModuleCat.of k ((Fin (n + 1 + 1) → G) → (↑A : Type u))))
    (CategoryStruct.comp (Y := ModuleCat.of k ((Fin (n + 1) → G) → (↑A : Type u)))
      (Iso.inv (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin n → G) A)) ≫
        HomologicalComplex.d (ChainComplex.linearYonedaObj (barComplex k G) k A) n (n + 1) ≫
          Iso.hom (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin (n + 1) → G) A)))
      (Iso.inv (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin (n + 1) → G) A)) ≫
        HomologicalComplex.d (ChainComplex.linearYonedaObj (barComplex k G) k A) (n + 1) (n + 1 + 1) ≫
          Iso.hom (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin (n + 1 + 1) → G) A))))
    0
simp₂ :
  Eq (α :=
    Quiver.Hom (V := ModuleCat k) (ModuleCat.of k ((Fin n → G) → (↑A : Type u)))
      (ModuleCat.of k ((Fin (n + 1 + 1) → G) → (↑A : Type u))))
    (Iso.inv (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin n → G) A)) ≫
      CategoryStruct.comp (Y := HomologicalComplex.X (ChainComplex.linearYonedaObj (barComplex k G) k A) (n + 1))
        (HomologicalComplex.d (ChainComplex.linearYonedaObj (barComplex k G) k A) n (n + 1))
        ((𝟙 (HomologicalComplex.X (ChainComplex.linearYonedaObj (barComplex k G) k A) (n + 1)) ≫
            HomologicalComplex.d (ChainComplex.linearYonedaObj (barComplex k G) k A) (n + 1) (n + 1 + 1)) ≫
          Iso.hom (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin (n + 1 + 1) → G) A))))
    0
⊢ Eq.{u + 1} (α :=
    Quiver.Hom (V := ModuleCat k) ((fun (n : ℕ) ↦ (ModuleCat.of k ((Fin n → G) → (↑A : Type u)) : ModuleCat k)) n)
      ((fun (n : ℕ) ↦ (ModuleCat.of k ((Fin n → G) → (↑A : Type u)) : ModuleCat k)) (n + 1 + 1)))
    (CategoryStruct.comp (Y := (fun (n : ℕ) ↦ (ModuleCat.of k ((Fin n → G) → (↑A : Type u)) : ModuleCat k)) (n + 1))
      ((fun (n : ℕ) ↦ d A n) n) ((fun (n : ℕ) ↦ d A n) (n + 1)))
    0
have simp₃ : Eq (α :=
  Quiver.Hom (V := ModuleCat k) (ModuleCat.of k ((Fin n → G) → (↑A : Type u)))
    (ModuleCat.of k ((Fin (n + 1 + 1) → G) → (↑A : Type u))))
  (Iso.inv (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin n → G) A)) ≫
    0 ≫ Iso.hom (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin (n + 1 + 1) → G) A)))
  0
Tactic: classical
    simp only
    rw [d_eq, d_eq]
    slice_lhs 3 4 => rw [Iso.hom_inv_id]
    slice_lhs 2 4 => rw [Category.id_comp, ((barComplex k G).linearYonedaObj k A).d_comp_d]
    simp
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic (goal)
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Group G
A : Rep k G
⊢ inhomogeneousCochains A ≅ ChainComplex.linearYonedaObj (barComplex k G) k A
have refine : ∀ (i j : ℕ),
  (ComplexShape.up ℕ).Rel i j →
    Eq (α := (inhomogeneousCochains A).X i ⟶ HomologicalComplex.X (ChainComplex.linearYonedaObj (barComplex k G) k A) j)
      (Iso.hom
          ((fun (i : ℕ) ↦
              (Iso.symm (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin i → G) A)) :
                Iso (C := ModuleCat k) (ModuleCat.of k ((Fin i → G) → (↑A : Type u)))
                  (ModuleCat.of k (free k G (Fin i → G) ⟶ A))))
            i) ≫
        HomologicalComplex.d (ChainComplex.linearYonedaObj (barComplex k G) k A) i j)
      ((inhomogeneousCochains A).d i j ≫
        Iso.hom
          ((fun (i : ℕ) ↦
              (Iso.symm (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin i → G) A)) :
                Iso (C := ModuleCat k) (ModuleCat.of k ((Fin i → G) → (↑A : Type u)))
                  (ModuleCat.of k (free k G (Fin i → G) ⟶ A))))
            j))
Tactic: refine HomologicalComplex.Hom.isoOfComponents
    (fun i ↦ (Rep.freeLiftLEquiv k G (Fin i → G) A).toModuleIso.symm) ?_
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic (goal)
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Group G
A : Rep k G
i j : ℕ
h : i + 1 = j
⊢ Eq (α := (inhomogeneousCochains A).X i ⟶ HomologicalComplex.X (ChainComplex.linearYonedaObj (barComplex k G) k A) j)
    (Iso.hom
        ((fun (i : ℕ) ↦
            (Iso.symm (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin i → G) A)) :
              Iso (C := ModuleCat k) (ModuleCat.of k ((Fin i → G) → (↑A : Type u)))
                (ModuleCat.of k (free k G (Fin i → G) ⟶ A))))
          i) ≫
      HomologicalComplex.d (ChainComplex.linearYonedaObj (barComplex k G) k A) i j)
    ((inhomogeneousCochains A).d i j ≫
      Iso.hom
        ((fun (i : ℕ) ↦
            (Iso.symm (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin i → G) A)) :
              Iso (C := ModuleCat k) (ModuleCat.of k ((Fin i → G) → (↑A : Type u)))
                (ModuleCat.of k (free k G (Fin i → G) ⟶ A))))
          j))
have subst : Eq (α :=
  (inhomogeneousCochains A).X i ⟶ HomologicalComplex.X (ChainComplex.linearYonedaObj (barComplex k G) k A) (i + 1))
  (Iso.hom
      ((fun (i : ℕ) ↦
          (Iso.symm (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin i → G) A)) :
            Iso (C := ModuleCat k) (ModuleCat.of k ((Fin i → G) → (↑A : Type u)))
              (ModuleCat.of k (free k G (Fin i → G) ⟶ A))))
        i) ≫
    HomologicalComplex.d (ChainComplex.linearYonedaObj (barComplex k G) k A) i (i + 1))
  (CategoryStruct.comp (Y := (inhomogeneousCochains A).X (i + 1)) ((inhomogeneousCochains A).d i (i + 1))
    (Iso.hom
      ((fun (i : ℕ) ↦
          (Iso.symm (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin i → G) A)) :
            Iso (C := ModuleCat k) (ModuleCat.of k ((Fin i → G) → (↑A : Type u)))
              (ModuleCat.of k (free k G (Fin i → G) ⟶ A))))
        (i + 1))))
Tactic: subst h
Cleared hypotheses: j, h
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
i : ℕ
⊢ Eq (α :=
    HomologicalComplex.X (ChainComplex.linearYonedaObj (ProjectiveResolution.complex (resolution k g hg)) k A) i ⟶
      (moduleCatCochainComplex A g).X (i + 1))
    (Iso.hom ((fun (x : ℕ) ↦ A.leftRegularHomEquiv.toModuleIso) i) ≫ (moduleCatCochainComplex A g).d i (i + 1))
    (CategoryStruct.comp (Y :=
      HomologicalComplex.X (ChainComplex.linearYonedaObj (ProjectiveResolution.complex (resolution k g hg)) k A)
        (i + 1))
      (HomologicalComplex.d (ChainComplex.linearYonedaObj (ProjectiveResolution.complex (resolution k g hg)) k A) i
        (i + 1))
      (Iso.hom ((fun (x : ℕ) ↦ A.leftRegularHomEquiv.toModuleIso) (i + 1))))
have hf : ∀ (x : leftRegular k G ⟶ A),
  Eq (α := (↑((moduleCatCochainComplex A g).X (i + 1)) : Type u))
    ((ModuleCat.Hom.hom
            (Iso.hom ((fun (x : ℕ) ↦ A.leftRegularHomEquiv.toModuleIso) i) ≫
              (moduleCatCochainComplex A g).d i (i + 1)) :
          (a : (↑(((resolution k g hg).complex.linearYonedaObj k A).X i) : Type u)) →
            (↑((moduleCatCochainComplex A g).X (i + 1)) : Type u))
        x :
      (↑((moduleCatCochainComplex A g).X (i + 1)) : Type u))
    ((ModuleCat.Hom.hom
            (CategoryStruct.comp (Y :=
              HomologicalComplex.X (ChainComplex.linearYonedaObj (ProjectiveResolution.complex (resolution k g hg)) k A)
                (i + 1))
              (HomologicalComplex.d
                (ChainComplex.linearYonedaObj (ProjectiveResolution.complex (resolution k g hg)) k A) i (i + 1))
              (Iso.hom ((fun (x : ℕ) ↦ A.leftRegularHomEquiv.toModuleIso) (i + 1)))) :
          (a : (↑(((resolution k g hg).complex.linearYonedaObj k A).X i) : Type u)) →
            (↑((moduleCatCochainComplex A g).X (i + 1)) : Type u))
        x :
      (↑((moduleCatCochainComplex A g).X (i + 1)) : Type u))
Tactic: ext (x : leftRegular _ _ ⟶ _)
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
i : ℕ
x : leftRegular k G ⟶ A
⊢ Eq (α := (↑((moduleCatCochainComplex A g).X (i + 1)) : Type u))
    ((ModuleCat.Hom.hom
            (Iso.hom ((fun (x : ℕ) ↦ A.leftRegularHomEquiv.toModuleIso) i) ≫
              (moduleCatCochainComplex A g).d i (i + 1)) :
          (a : (↑(((resolution k g hg).complex.linearYonedaObj k A).X i) : Type u)) →
            (↑((moduleCatCochainComplex A g).X (i + 1)) : Type u))
        x :
      (↑((moduleCatCochainComplex A g).X (i + 1)) : Type u))
    ((ModuleCat.Hom.hom
            (CategoryStruct.comp (Y :=
              HomologicalComplex.X (ChainComplex.linearYonedaObj (ProjectiveResolution.complex (resolution k g hg)) k A)
                (i + 1))
              (HomologicalComplex.d
                (ChainComplex.linearYonedaObj (ProjectiveResolution.complex (resolution k g hg)) k A) i (i + 1))
              (Iso.hom ((fun (x : ℕ) ↦ A.leftRegularHomEquiv.toModuleIso) (i + 1)))) :
          (a : (↑(((resolution k g hg).complex.linearYonedaObj k A).X i) : Type u)) →
            (↑((moduleCatCochainComplex A g).X (i + 1)) : Type u))
        x :
      (↑((moduleCatCochainComplex A g).X (i + 1)) : Type u))
have pos : ∀ (hi : Even i),
  Eq (α := (↑((moduleCatCochainComplex A g).X (i + 1)) : Type u))
    ((ModuleCat.Hom.hom
            (Iso.hom ((fun (x : ℕ) ↦ A.leftRegularHomEquiv.toModuleIso) i) ≫
              (moduleCatCochainComplex A g).d i (i + 1)) :
          (a : (↑(((resolution k g hg).complex.linearYonedaObj k A).X i) : Type u)) →
            (↑((moduleCatCochainComplex A g).X (i + 1)) : Type u))
        x :
      (↑((moduleCatCochainComplex A g).X (i + 1)) : Type u))
    ((ModuleCat.Hom.hom
            (CategoryStruct.comp (Y :=
              HomologicalComplex.X (ChainComplex.linearYonedaObj (ProjectiveResolution.complex (resolution k g hg)) k A)
                (i + 1))
              (HomologicalComplex.d
                (ChainComplex.linearYonedaObj (ProjectiveResolution.complex (resolution k g hg)) k A) i (i + 1))
              (Iso.hom ((fun (x : ℕ) ↦ A.leftRegularHomEquiv.toModuleIso) (i + 1)))) :
          (a : (↑(((resolution k g hg).complex.linearYonedaObj k A).X i) : Type u)) →
            (↑((moduleCatCochainComplex A g).X (i + 1)) : Type u))
        x :
      (↑((moduleCatCochainComplex A g).X (i + 1)) : Type u))
Tactic: by_cases hi : Even i
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic (hypothesis)
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
i : ℕ
x : leftRegular k G ⟶ A
hi : Even i
⊢ Eq (α := (↑((moduleCatCochainComplex A g).X (i + 1)) : Type u))
    ((ModuleCat.Hom.hom
            (Iso.hom ((fun (x : ℕ) ↦ A.leftRegularHomEquiv.toModuleIso) i) ≫
              (moduleCatCochainComplex A g).d i (i + 1)) :
          (a : (↑(((resolution k g hg).complex.linearYonedaObj k A).X i) : Type u)) →
            (↑((moduleCatCochainComplex A g).X (i + 1)) : Type u))
        x :
      (↑((moduleCatCochainComplex A g).X (i + 1)) : Type u))
    ((ModuleCat.Hom.hom
            (CategoryStruct.comp (Y :=
              HomologicalComplex.X (ChainComplex.linearYonedaObj (ProjectiveResolution.complex (resolution k g hg)) k A)
                (i + 1))
              (HomologicalComplex.d
                (ChainComplex.linearYonedaObj (ProjectiveResolution.complex (resolution k g hg)) k A) i (i + 1))
              (Iso.hom ((fun (x : ℕ) ↦ A.leftRegularHomEquiv.toModuleIso) (i + 1)))) :
          (a : (↑(((resolution k g hg).complex.linearYonedaObj k A).X i) : Type u)) →
            (↑((moduleCatCochainComplex A g).X (i + 1)) : Type u))
        x :
      (↑((moduleCatCochainComplex A g).X (i + 1)) : Type u))
have this : ¬Even (i + 1)
Tactic: have : ¬(Even (i + 1)) := Nat.even_add_one.not_left.mpr hi
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
⊢ A.ρ.invariants = (Hom.hom (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (A.applyAsHom (k := k) g : A ⟶ A) (𝟙 A))).ker
have h : ∀ (x : (↑A : Type u)),
  x ∈ A.ρ.invariants ↔ x ∈ (Hom.hom (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (A.applyAsHom (k := k) g : A ⟶ A) (𝟙 A))).ker
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
i : ℕ
h₀ : NeZero i
hi : Even i
⊢ ModuleCat.ofHom (Hom.hom (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (A.applyAsHom (k := k) g : A ⟶ A) (𝟙 A))).toLinearMap ≫
      ModuleCat.ofHom (Hom.hom A.norm).toLinearMap =
    0
have hf : ∀ (x : (↑(ModuleCat.of k (↑A : Type u)) : Type u)),
  Eq (α := (↑(ModuleCat.of k (↑A : Type u)) : Type u))
    ((ModuleCat.Hom.hom
            (ModuleCat.ofHom
                (Hom.hom (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (A.applyAsHom (k := k) g : A ⟶ A) (𝟙 A))).toLinearMap ≫
              ModuleCat.ofHom (Hom.hom A.norm).toLinearMap) :
          (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
        x :
      (↑(ModuleCat.of k (↑A : Type u)) : Type u))
    ((ModuleCat.Hom.hom 0 :
          (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
        x :
      (↑(ModuleCat.of k (↑A : Type u)) : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
i : ℕ
h₀ : NeZero i
hi : Even i
⊢ ModuleCat.ofHom (Hom.hom A.norm).toLinearMap ≫
      ModuleCat.ofHom
        (Hom.hom (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (A.applyAsHom (k := k) g : A ⟶ A) (𝟙 A))).toLinearMap =
    0
have hf : ∀ (x : (↑(ModuleCat.of k (↑A : Type u)) : Type u)),
  Eq (α := (↑(ModuleCat.of k (↑A : Type u)) : Type u))
    ((ModuleCat.Hom.hom
            (ModuleCat.ofHom (Hom.hom A.norm).toLinearMap ≫
              ModuleCat.ofHom
                (Hom.hom (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (A.applyAsHom (k := k) g : A ⟶ A) (𝟙 A))).toLinearMap) :
          (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
        x :
      (↑(ModuleCat.of k (↑A : Type u)) : Type u))
    ((ModuleCat.Hom.hom 0 :
          (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
        x :
      (↑(ModuleCat.of k (↑A : Type u)) : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
i : ℕ
h₀ : NeZero i
hi : Even i
⊢ (ComplexShape.up ℕ).Rel ((ComplexShape.up ℕ).prev i) i
have zero : ∀ [h₀ : NeZero (R := ℕ) 0] (hi : Even (α := ℕ) 0), (ComplexShape.up ℕ).Rel ((ComplexShape.up ℕ).prev 0) 0
Tactic: induction i generalizing h₀ with | zero => exact (NeZero.ne 0 rfl).elim | succ n _ => simp
Cleared hypotheses: i, h₀, hi
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
i : ℕ
h₀ : NeZero i
hi : Even i
zero : ∀ [h₀ : NeZero (R := ℕ) 0] (hi : Even (α := ℕ) 0), (ComplexShape.up ℕ).Rel ((ComplexShape.up ℕ).prev 0) 0
⊢ (ComplexShape.up ℕ).Rel ((ComplexShape.up ℕ).prev i) i
have succ : ∀ (n : ℕ),
  (∀ [h₀ : NeZero n] (hi : Even n), (ComplexShape.up ℕ).Rel ((ComplexShape.up ℕ).prev n) n) →
    ∀ [h₀ : NeZero (n + 1)] (hi : Even (n + 1)), (ComplexShape.up ℕ).Rel ((ComplexShape.up ℕ).prev (n + 1)) (n + 1)
Tactic: induction i generalizing h₀ with | zero => exact (NeZero.ne 0 rfl).elim | succ n _ => simp
Cleared hypotheses: i, h₀, hi
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
i : ℕ
inst_3 : NeZero i
hi : Even i
x y : ↥(Hom.hom (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (A.applyAsHom (k := k) g : A ⟶ A) (𝟙 A))).ker
⊢ Eq (α := (↑(groupCohomology A i) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (groupCohomologyπEven A g hg i hi) :
            (a : (↑(ModuleCat.of k ↥(Hom.hom (A.applyAsHom g - 𝟙 A)).ker) : Type u)) →
              (↑(groupCohomology A i) : Type u))
          x :
        (↑(groupCohomology A i) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (groupCohomologyπEven A g hg i hi) :
            (a : (↑(ModuleCat.of k ↥(Hom.hom (A.applyAsHom g - 𝟙 A)).ker) : Type u)) →
              (↑(groupCohomology A i) : Type u))
          y :
        (↑(groupCohomology A i) : Type u)) ↔
    (↑x : (↑A : Type u)) - (↑y : (↑A : Type u)) ∈ (Hom.hom A.norm).range
have rw : (↑(x - y) : (↑A : Type u)) ∈ (Hom.hom A.norm).range ↔
  (↑x : (↑A : Type u)) - (↑y : (↑A : Type u)) ∈ (Hom.hom A.norm).range
Tactic: rw [← sub_eq_zero, ← map_sub, groupCohomologyπEven_eq_zero_iff]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
i : ℕ
hi : Odd i
⊢ ModuleCat.ofHom (Hom.hom (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (A.applyAsHom (k := k) g : A ⟶ A) (𝟙 A))).toLinearMap ≫
      ModuleCat.ofHom (Hom.hom A.norm).toLinearMap =
    0
have hf : ∀ (x : (↑(ModuleCat.of k (↑A : Type u)) : Type u)),
  Eq (α := (↑(ModuleCat.of k (↑A : Type u)) : Type u))
    ((ModuleCat.Hom.hom
            (ModuleCat.ofHom
                (Hom.hom (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (A.applyAsHom (k := k) g : A ⟶ A) (𝟙 A))).toLinearMap ≫
              ModuleCat.ofHom (Hom.hom A.norm).toLinearMap) :
          (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
        x :
      (↑(ModuleCat.of k (↑A : Type u)) : Type u))
    ((ModuleCat.Hom.hom 0 :
          (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
        x :
      (↑(ModuleCat.of k (↑A : Type u)) : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
i : ℕ
hi : Odd i
⊢ ModuleCat.ofHom (Hom.hom A.norm).toLinearMap ≫
      ModuleCat.ofHom
        (Hom.hom (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (A.applyAsHom (k := k) g : A ⟶ A) (𝟙 A))).toLinearMap =
    0
have hf : ∀ (x : (↑(ModuleCat.of k (↑A : Type u)) : Type u)),
  Eq (α := (↑(ModuleCat.of k (↑A : Type u)) : Type u))
    ((ModuleCat.Hom.hom
            (ModuleCat.ofHom (Hom.hom A.norm).toLinearMap ≫
              ModuleCat.ofHom
                (Hom.hom (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (A.applyAsHom (k := k) g : A ⟶ A) (𝟙 A))).toLinearMap) :
          (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
        x :
      (↑(ModuleCat.of k (↑A : Type u)) : Type u))
    ((ModuleCat.Hom.hom 0 :
          (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
        x :
      (↑(ModuleCat.of k (↑A : Type u)) : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
i : ℕ
hi : Odd i
⊢ (ComplexShape.up ℕ).Rel ((ComplexShape.up ℕ).prev i) i
have rcases : ∀ (j : ℕ), (ComplexShape.up ℕ).Rel ((ComplexShape.up ℕ).prev (2 * j + 1)) (2 * j + 1)
Tactic: rcases hi with ⟨j, rfl⟩
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
i : ℕ
hi : Odd i
x y : ↥(Hom.hom A.norm).ker
⊢ Eq (α := (↑(groupCohomology A i) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (X := ModuleCat.of k ↥(Hom.hom A.norm).ker) (groupCohomologyπOdd A g hg i hi) :
            (a : (↑(ModuleCat.of k ↥(Hom.hom A.norm).ker) : Type u)) → (↑(groupCohomology A i) : Type u))
          x :
        (↑(groupCohomology A i) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (X := ModuleCat.of k ↥(Hom.hom A.norm).ker) (groupCohomologyπOdd A g hg i hi) :
            (a : (↑(ModuleCat.of k ↥(Hom.hom A.norm).ker) : Type u)) → (↑(groupCohomology A i) : Type u))
          y :
        (↑(groupCohomology A i) : Type u)) ↔
    (↑x : (↑A : Type u)) - (↑y : (↑A : Type u)) ∈
      (Hom.hom (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (A.applyAsHom (k := k) g : A ⟶ A) (𝟙 A))).range
have rw : HSub.hSub (α := (↑(groupCohomology A i) : Type u)) (β := (↑(groupCohomology A i) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (X := ModuleCat.of k ↥(Hom.hom A.norm).ker) (groupCohomologyπOdd A g hg i hi) :
            (a : (↑(ModuleCat.of k ↥(Hom.hom A.norm).ker) : Type u)) → (↑(groupCohomology A i) : Type u))
          x :
        (↑(groupCohomology A i) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (X := ModuleCat.of k ↥(Hom.hom A.norm).ker) (groupCohomologyπOdd A g hg i hi) :
            (a : (↑(ModuleCat.of k ↥(Hom.hom A.norm).ker) : Type u)) → (↑(groupCohomology A i) : Type u))
          y :
        (↑(groupCohomology A i) : Type u)) =
    0 ↔
  (↑x : (↑A : Type u)) - (↑y : (↑A : Type u)) ∈
    (Hom.hom (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (A.applyAsHom (k := k) g : A ⟶ A) (𝟙 A))).range
Tactic: rw [← sub_eq_zero, ← map_sub, groupCohomologyπOdd_eq_zero_iff, AddSubgroupClass.coe_sub]