awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
inst_3 : DecidableEq 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.GroupHomology.FiniteCyclic (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
inst_3 : DecidableEq 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.GroupHomology.FiniteCyclic (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
inst_3 : DecidableEq G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
i : ℕ
h₀ : NeZero i
hi : Even i
⊢ (ComplexShape.down ℕ).Rel i ((ComplexShape.down ℕ).next i)
have zero : ∀ [h₀ : NeZero (R := ℕ) 0] (hi : Even (α := ℕ) 0), (ComplexShape.down ℕ).Rel 0 ((ComplexShape.down ℕ).next 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.GroupHomology.FiniteCyclic (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
inst_3 : DecidableEq 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.down ℕ).Rel 0 ((ComplexShape.down ℕ).next 0)
⊢ (ComplexShape.down ℕ).Rel i ((ComplexShape.down ℕ).next i)
have succ : ∀ (n : ℕ),
  (∀ [h₀ : NeZero n] (hi : Even n), (ComplexShape.down ℕ).Rel n ((ComplexShape.down ℕ).next n)) →
    ∀ [h₀ : NeZero (n + 1)] (hi : Even (n + 1)), (ComplexShape.down ℕ).Rel (n + 1) ((ComplexShape.down ℕ).next (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.GroupHomology.FiniteCyclic (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
inst_3 : DecidableEq G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
i : ℕ
inst_4 : NeZero i
hi : Even i
x y : ↥(LinearMap.ker A.ρ.norm)
⊢ Eq (α := (↑(groupHomology 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 ↥(LinearMap.ker A.ρ.norm)) (groupHomologyπEven A g hg i hi) :
            (a : (↑(ModuleCat.of k ↥(LinearMap.ker A.ρ.norm)) : Type u)) → (↑(groupHomology A i) : Type u))
          x :
        (↑(groupHomology 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 ↥(LinearMap.ker A.ρ.norm)) (groupHomologyπEven A g hg i hi) :
            (a : (↑(ModuleCat.of k ↥(LinearMap.ker A.ρ.norm)) : Type u)) → (↑(groupHomology A i) : Type u))
          y :
        (↑(groupHomology 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 (α := (↑(groupHomology A i) : Type u)) (β := (↑(groupHomology 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 ↥(LinearMap.ker A.ρ.norm)) (groupHomologyπEven A g hg i hi) :
            (a : (↑(ModuleCat.of k ↥(LinearMap.ker A.ρ.norm)) : Type u)) → (↑(groupHomology A i) : Type u))
          x :
        (↑(groupHomology 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 ↥(LinearMap.ker A.ρ.norm)) (groupHomologyπEven A g hg i hi) :
            (a : (↑(ModuleCat.of k ↥(LinearMap.ker A.ρ.norm)) : Type u)) → (↑(groupHomology A i) : Type u))
          y :
        (↑(groupHomology 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, groupHomologyπEven_eq_zero_iff, AddSubgroupClass.coe_sub]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
inst_3 : DecidableEq G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
i : ℕ
inst_4 : NeZero i
hi : Even i
x y : ↥(LinearMap.ker A.ρ.norm)
rw :
  HSub.hSub (α := (↑(groupHomology A i) : Type u)) (β := (↑(groupHomology 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 ↥(LinearMap.ker A.ρ.norm)) (groupHomologyπEven A g hg i hi) :
              (a : (↑(ModuleCat.of k ↥(LinearMap.ker A.ρ.norm)) : Type u)) → (↑(groupHomology A i) : Type u))
            x :
          (↑(groupHomology 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 ↥(LinearMap.ker A.ρ.norm)) (groupHomologyπEven A g hg i hi) :
              (a : (↑(ModuleCat.of k ↥(LinearMap.ker A.ρ.norm)) : Type u)) → (↑(groupHomology A i) : Type u))
            y :
          (↑(groupHomology 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
⊢ Eq (α := (↑(groupHomology 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 ↥(LinearMap.ker A.ρ.norm)) (groupHomologyπEven A g hg i hi) :
            (a : (↑(ModuleCat.of k ↥(LinearMap.ker A.ρ.norm)) : Type u)) → (↑(groupHomology A i) : Type u))
          x :
        (↑(groupHomology 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 ↥(LinearMap.ker A.ρ.norm)) (groupHomologyπEven A g hg i hi) :
            (a : (↑(ModuleCat.of k ↥(LinearMap.ker A.ρ.norm)) : Type u)) → (↑(groupHomology A i) : Type u))
          y :
        (↑(groupHomology 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₁ : Eq (α := (↑(groupHomology 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 ↥(LinearMap.ker A.ρ.norm)) (groupHomologyπEven A g hg i hi) :
          (a : (↑(ModuleCat.of k ↥(LinearMap.ker A.ρ.norm)) : Type u)) → (↑(groupHomology A i) : Type u))
        (x - y) :
      (↑(groupHomology A i) : Type u))
    (0 : (↑(groupHomology 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
Tactic: rw [← sub_eq_zero, ← map_sub, groupHomologyπEven_eq_zero_iff, AddSubgroupClass.coe_sub]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
inst_3 : DecidableEq 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.GroupHomology.FiniteCyclic (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
inst_3 : DecidableEq 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.GroupHomology.FiniteCyclic (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
inst_3 : DecidableEq G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
i : ℕ
hi : Odd i
⊢ (ComplexShape.down ℕ).Rel i ((ComplexShape.down ℕ).next i)
have rcases : ∀ (j : ℕ), (ComplexShape.down ℕ).Rel (2 * j + 1) ((ComplexShape.down ℕ).next (2 * j + 1))
Tactic: rcases hi with ⟨j, rfl⟩
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
inst_3 : DecidableEq G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
A : Rep k G
i : ℕ
hi : Odd i
x y : ↥(Hom.hom (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (A.applyAsHom (k := k) g : A ⟶ A) (𝟙 A))).ker
⊢ Eq (α := (↑(groupHomology A i) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (groupHomologyπOdd A g hg i hi) :
            (a : (↑(ModuleCat.of k ↥(Hom.hom (A.applyAsHom g - 𝟙 A)).ker) : Type u)) → (↑(groupHomology A i) : Type u))
          x :
        (↑(groupHomology A i) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (groupHomologyπOdd A g hg i hi) :
            (a : (↑(ModuleCat.of k ↥(Hom.hom (A.applyAsHom g - 𝟙 A)).ker) : Type u)) → (↑(groupHomology A i) : Type u))
          y :
        (↑(groupHomology A i) : Type u)) ↔
    (↑x : (↑A : Type u)) - (↑y : (↑A : Type u)) ∈ LinearMap.range A.ρ.norm
have rw : HSub.hSub (α := (↑(groupHomology A i) : Type u)) (β := (↑(groupHomology A i) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (groupHomologyπOdd A g hg i hi) :
            (a : (↑(ModuleCat.of k ↥(Hom.hom (A.applyAsHom g - 𝟙 A)).ker) : Type u)) → (↑(groupHomology A i) : Type u))
          x :
        (↑(groupHomology A i) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (groupHomologyπOdd A g hg i hi) :
            (a : (↑(ModuleCat.of k ↥(Hom.hom (A.applyAsHom g - 𝟙 A)).ker) : Type u)) → (↑(groupHomology A i) : Type u))
          y :
        (↑(groupHomology A i) : Type u)) =
    0 ↔
  (↑x : (↑A : Type u)) - (↑y : (↑A : Type u)) ∈ LinearMap.range A.ρ.norm
Tactic: rw [← sub_eq_zero, ← map_sub, groupHomologyπOdd_eq_zero_iff, AddSubgroupClass.coe_sub]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
inst_3 : DecidableEq G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
A : Rep k G
i : ℕ
hi : Odd i
x y : ↥(Hom.hom (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (A.applyAsHom (k := k) g : A ⟶ A) (𝟙 A))).ker
rw :
  HSub.hSub (α := (↑(groupHomology A i) : Type u)) (β := (↑(groupHomology A i) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (groupHomologyπOdd A g hg i hi) :
              (a : (↑(ModuleCat.of k ↥(Hom.hom (A.applyAsHom g - 𝟙 A)).ker) : Type u)) →
                (↑(groupHomology A i) : Type u))
            x :
          (↑(groupHomology A i) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (groupHomologyπOdd A g hg i hi) :
              (a : (↑(ModuleCat.of k ↥(Hom.hom (A.applyAsHom g - 𝟙 A)).ker) : Type u)) →
                (↑(groupHomology A i) : Type u))
            y :
          (↑(groupHomology A i) : Type u)) =
      0 ↔
    (↑x : (↑A : Type u)) - (↑y : (↑A : Type u)) ∈ LinearMap.range A.ρ.norm
⊢ Eq (α := (↑(groupHomology A i) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (groupHomologyπOdd A g hg i hi) :
            (a : (↑(ModuleCat.of k ↥(Hom.hom (A.applyAsHom g - 𝟙 A)).ker) : Type u)) → (↑(groupHomology A i) : Type u))
          x :
        (↑(groupHomology A i) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (groupHomologyπOdd A g hg i hi) :
            (a : (↑(ModuleCat.of k ↥(Hom.hom (A.applyAsHom g - 𝟙 A)).ker) : Type u)) → (↑(groupHomology A i) : Type u))
          y :
        (↑(groupHomology A i) : Type u)) ↔
    (↑x : (↑A : Type u)) - (↑y : (↑A : Type u)) ∈ LinearMap.range A.ρ.norm
have rw₁ : Eq (α := (↑(groupHomology A i) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (groupHomologyπOdd A g hg i hi) :
          (a : (↑(ModuleCat.of k ↥(Hom.hom (A.applyAsHom g - 𝟙 A)).ker) : Type u)) → (↑(groupHomology A i) : Type u))
        (x - y) :
      (↑(groupHomology A i) : Type u))
    (0 : (↑(groupHomology A i) : Type u)) ↔
  (↑x : (↑A : Type u)) - (↑y : (↑A : Type u)) ∈ LinearMap.range A.ρ.norm
Tactic: rw [← sub_eq_zero, ← map_sub, groupHomologyπOdd_eq_zero_iff, AddSubgroupClass.coe_sub]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
inst_3 : DecidableEq G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
A : Rep k G
i : ℕ
hi : Odd i
x y : ↥(Hom.hom (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (A.applyAsHom (k := k) g : A ⟶ A) (𝟙 A))).ker
rw :
  HSub.hSub (α := (↑(groupHomology A i) : Type u)) (β := (↑(groupHomology A i) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (groupHomologyπOdd A g hg i hi) :
              (a : (↑(ModuleCat.of k ↥(Hom.hom (A.applyAsHom g - 𝟙 A)).ker) : Type u)) →
                (↑(groupHomology A i) : Type u))
            x :
          (↑(groupHomology A i) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (groupHomologyπOdd A g hg i hi) :
              (a : (↑(ModuleCat.of k ↥(Hom.hom (A.applyAsHom g - 𝟙 A)).ker) : Type u)) →
                (↑(groupHomology A i) : Type u))
            y :
          (↑(groupHomology A i) : Type u)) =
      0 ↔
    (↑x : (↑A : Type u)) - (↑y : (↑A : Type u)) ∈ LinearMap.range A.ρ.norm
rw₁ :
  Eq (α := (↑(groupHomology A i) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (groupHomologyπOdd A g hg i hi) :
            (a : (↑(ModuleCat.of k ↥(Hom.hom (A.applyAsHom g - 𝟙 A)).ker) : Type u)) → (↑(groupHomology A i) : Type u))
          (x - y) :
        (↑(groupHomology A i) : Type u))
      (0 : (↑(groupHomology A i) : Type u)) ↔
    (↑x : (↑A : Type u)) - (↑y : (↑A : Type u)) ∈ LinearMap.range A.ρ.norm
⊢ Eq (α := (↑(groupHomology A i) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (groupHomologyπOdd A g hg i hi) :
            (a : (↑(ModuleCat.of k ↥(Hom.hom (A.applyAsHom g - 𝟙 A)).ker) : Type u)) → (↑(groupHomology A i) : Type u))
          x :
        (↑(groupHomology A i) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (groupHomologyπOdd A g hg i hi) :
            (a : (↑(ModuleCat.of k ↥(Hom.hom (A.applyAsHom g - 𝟙 A)).ker) : Type u)) → (↑(groupHomology A i) : Type u))
          y :
        (↑(groupHomology A i) : Type u)) ↔
    (↑x : (↑A : Type u)) - (↑y : (↑A : Type u)) ∈ LinearMap.range A.ρ.norm
have rw₂ : (↑(x - y) : (↑A : Type u)) ∈ LinearMap.range A.ρ.norm ↔
  (↑x : (↑A : Type u)) - (↑y : (↑A : Type u)) ∈ LinearMap.range A.ρ.norm
Tactic: rw [← sub_eq_zero, ← map_sub, groupHomologyπOdd_eq_zero_iff, AddSubgroupClass.coe_sub]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
inst_3 : DecidableEq G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
A : Rep k G
i : ℕ
hi : Odd i
x y : ↥(Hom.hom (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (A.applyAsHom (k := k) g : A ⟶ A) (𝟙 A))).ker
rw :
  HSub.hSub (α := (↑(groupHomology A i) : Type u)) (β := (↑(groupHomology A i) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (groupHomologyπOdd A g hg i hi) :
              (a : (↑(ModuleCat.of k ↥(Hom.hom (A.applyAsHom g - 𝟙 A)).ker) : Type u)) →
                (↑(groupHomology A i) : Type u))
            x :
          (↑(groupHomology A i) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (groupHomologyπOdd A g hg i hi) :
              (a : (↑(ModuleCat.of k ↥(Hom.hom (A.applyAsHom g - 𝟙 A)).ker) : Type u)) →
                (↑(groupHomology A i) : Type u))
            y :
          (↑(groupHomology A i) : Type u)) =
      0 ↔
    (↑x : (↑A : Type u)) - (↑y : (↑A : Type u)) ∈ LinearMap.range A.ρ.norm
rw₁ :
  Eq (α := (↑(groupHomology A i) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (groupHomologyπOdd A g hg i hi) :
            (a : (↑(ModuleCat.of k ↥(Hom.hom (A.applyAsHom g - 𝟙 A)).ker) : Type u)) → (↑(groupHomology A i) : Type u))
          (x - y) :
        (↑(groupHomology A i) : Type u))
      (0 : (↑(groupHomology A i) : Type u)) ↔
    (↑x : (↑A : Type u)) - (↑y : (↑A : Type u)) ∈ LinearMap.range A.ρ.norm
rw₂ :
  (↑(x - y) : (↑A : Type u)) ∈ LinearMap.range A.ρ.norm ↔
    (↑x : (↑A : Type u)) - (↑y : (↑A : Type u)) ∈ LinearMap.range A.ρ.norm
⊢ Eq (α := (↑(groupHomology A i) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (groupHomologyπOdd A g hg i hi) :
            (a : (↑(ModuleCat.of k ↥(Hom.hom (A.applyAsHom g - 𝟙 A)).ker) : Type u)) → (↑(groupHomology A i) : Type u))
          x :
        (↑(groupHomology A i) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (groupHomologyπOdd A g hg i hi) :
            (a : (↑(ModuleCat.of k ↥(Hom.hom (A.applyAsHom g - 𝟙 A)).ker) : Type u)) → (↑(groupHomology A i) : Type u))
          y :
        (↑(groupHomology A i) : Type u)) ↔
    (↑x : (↑A : Type u)) - (↑y : (↑A : Type u)) ∈ LinearMap.range A.ρ.norm
have rw₃ : (↑x : (↑A : Type u)) - (↑y : (↑A : Type u)) ∈ LinearMap.range A.ρ.norm ↔
  (↑x : (↑A : Type u)) - (↑y : (↑A : Type u)) ∈ LinearMap.range A.ρ.norm
Tactic: rw [← sub_eq_zero, ← map_sub, groupHomologyπOdd_eq_zero_iff, AddSubgroupClass.coe_sub]
-- 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.{u_2, u, u} k G
B : Rep.{u_2, u, u} k H
f₁ f₂ : G →* H
h : f₁ = f₂
φ : A ⟶ res f₁ B
T : Type u_1
F : (f : G →* H) → (φ : A ⟶ res f B) → T
⊢ F f₁ φ = F f₂ (Eq.rec (motive := fun (x : G →* H) (h : f₁ = x) ↦ A ⟶ res x B) φ h)
have subst : F f₁ φ = F f₁ (Eq.rec (motive := fun (x : G →* H) (h : f₁ = x) ↦ A ⟶ res x B) φ sorry)
Tactic: subst h
Cleared hypotheses: f₂, h