awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥X.X₃.ρ.invariants
y : (↑X.X₂ : Type u)
hy : (Rep.Hom.hom X.g : (a : (↑X.X₂ : Type u)) → (↑X.X₃ : Type u)) y = (↑z : (↑X.X₃ : Type u))
x : G → (↑X.X₁ : Type u)
hx :
  Eq (α := G → (↑X.X₂ : Type u)) ((⇑(Rep.Hom.hom X.f) : (a : (↑X.X₁ : Type u)) → (↑X.X₂ : Type u)) ∘ x)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (d₀₁ X.X₂) :
        (a : (↑(ModuleCat.of k (↑X.X₂ : Type u)) : Type u)) → (↑(ModuleCat.of k (G → (↑X.X₂ : Type u))) : Type u))
      y)
g : Fin (HAdd.hAdd (α := ℕ) 0 1) → G
⊢ Eq (α := (↑X.X₂ : Type u))
    (Function.comp (β := (↑X.X₁ : Type u)) (⇑(Rep.Hom.hom X.f) : (a : (↑X.X₁ : Type u)) → (↑X.X₂ : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (cochainsIso₁ X.X₁).inv :
            (a : (↑(ModuleCat.of k (G → (↑X.X₁ : Type u))) : Type u)) → (↑((inhomogeneousCochains X.X₁).X 1) : Type u))
          x)
        g :
      (↑X.X₂ : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := (inhomogeneousCochains X.X₂).X 0) (Y :=
            (inhomogeneousCochains X.X₂).X (HAdd.hAdd (α := ℕ) 0 1))
            ((inhomogeneousCochains X.X₂).d 0 (HAdd.hAdd (α := ℕ) 0 1)) :
          (a : (↑((inhomogeneousCochains X.X₂).X 0) : Type u)) → (↑((inhomogeneousCochains X.X₂).X (0 + 1)) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (cochainsIso₀ X.X₂).inv :
              (a : (↑(ModuleCat.of k (↑X.X₂ : Type u)) : Type u)) → (↑((inhomogeneousCochains X.X₂).X 0) : Type u))
            y :
          (↑((inhomogeneousCochains X.X₂).X 0) : Type u))
        g :
      (↑X.X₂ : Type u))
have h : Eq (α := (↑X.X₂ : Type u))
  (Function.comp (β := (↑X.X₁ : Type u)) (⇑(Rep.Hom.hom X.f) : (a : (↑X.X₁ : Type u)) → (↑X.X₂ : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (cochainsIso₁ X.X₁).inv :
          (a : (↑(ModuleCat.of k (G → (↑X.X₁ : Type u))) : Type u)) → (↑((inhomogeneousCochains X.X₁).X 1) : Type u))
        x)
      g :
    (↑X.X₂ : Type u))
  ((ModuleCat.Hom.hom (d₀₁ X.X₂ ≫ (cochainsIso₁ X.X₂).inv) :
        (a : (↑(ModuleCat.of k (↑X.X₂ : Type u)) : Type u)) → (↑((inhomogeneousCochains X.X₂).X (0 + 1)) : Type u))
      y g :
    (↑X.X₂ : Type u))
Tactic: rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, eq_d₀₁_comp_inv]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X : ShortComplex (Rep.{u_1, u, u} k G)
hX : X.ShortExact
y : G → (↑X.X₂ : Type u_1)
x : G × G → (↑X.X₁ : Type u_1)
hx :
  Eq (α := G × G → (↑X.X₂ : Type u_1)) ((⇑(Rep.Hom.hom X.f) : (a : (↑X.X₁ : Type u_1)) → (↑X.X₂ : Type u_1)) ∘ x)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type (max u u_1)) →ₗ[k] (↑x2 : Type (max u u_1)))
          (CC := ModuleCat.carrier) (d₁₂ X.X₂) :
        (a : (↑(ModuleCat.of k (G → (↑X.X₂ : Type u_1))) : Type (max u u_1))) →
          (↑(ModuleCat.of k (G × G → (↑X.X₂ : Type u_1))) : Type (max u u_1)))
      y)
⊢ x ∈ cocycles₂ X.X₁
have a : Eq (α := G × G × G → (↑X.X₂ : Type u_1))
  ((fun (x : G × G × G → (↑X.X₁ : Type u_1)) ↦
      ((⇑(Rep.Hom.hom X.f) : (a : (↑X.X₁ : Type u_1)) → (↑X.X₂ : Type u_1)) ∘ x : G × G × G → (↑X.X₂ : Type u_1)))
    ((ModuleCat.Hom.hom (d₂₃ X.X₁) :
        (a : G × G → (↑X.X₁ : Type u_1)) → (↑(ModuleCat.of k (G × G × G → (↑X.X₁ : Type u_1))) : Type (max u u_1)))
      x))
  ((fun (x : G × G × G → (↑X.X₁ : Type u_1)) ↦
      ((⇑(Rep.Hom.hom X.f) : (a : (↑X.X₁ : Type u_1)) → (↑X.X₂ : Type u_1)) ∘ x : G × G × G → (↑X.X₂ : Type u_1)))
    0)
Tactic: apply Function.Injective.comp_left ((Rep.mono_iff_injective X.f).1 hX.2)
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence (hypothesis)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X : ShortComplex (Rep.{u_1, u, u} k G)
hX : X.ShortExact
y : G → (↑X.X₂ : Type u_1)
x : G × G → (↑X.X₁ : Type u_1)
hx :
  Eq (α := G × G → (↑X.X₂ : Type u_1)) ((⇑(Rep.Hom.hom X.f) : (a : (↑X.X₁ : Type u_1)) → (↑X.X₂ : Type u_1)) ∘ x)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type (max u u_1)) →ₗ[k] (↑x2 : Type (max u u_1)))
          (CC := ModuleCat.carrier) (d₁₂ X.X₂) :
        (a : (↑(ModuleCat.of k (G → (↑X.X₂ : Type u_1))) : Type (max u u_1))) →
          (↑(ModuleCat.of k (G × G → (↑X.X₂ : Type u_1))) : Type (max u u_1)))
      y)
⊢ Eq (α := G × G × G → (↑X.X₂ : Type u_1))
    ((fun (x : G × G × G → (↑X.X₁ : Type u_1)) ↦
        ((⇑(Rep.Hom.hom X.f) : (a : (↑X.X₁ : Type u_1)) → (↑X.X₂ : Type u_1)) ∘ x : G × G × G → (↑X.X₂ : Type u_1)))
      ((ModuleCat.Hom.hom (d₂₃ X.X₁) :
          (a : G × G → (↑X.X₁ : Type u_1)) → (↑(ModuleCat.of k (G × G × G → (↑X.X₁ : Type u_1))) : Type (max u u_1)))
        x))
    ((fun (x : G × G × G → (↑X.X₁ : Type u_1)) ↦
        ((⇑(Rep.Hom.hom X.f) : (a : (↑X.X₁ : Type u_1)) → (↑X.X₂ : Type u_1)) ∘ x : G × G × G → (↑X.X₂ : Type u_1)))
      0)
have this : Eq (α := (↑(shortComplexH2 X.X₂).X₃ : Type (max u u_1)))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type (max u u_1)) →ₗ[k] (↑x2 : Type (max u u_1)))
          (CC := ModuleCat.carrier) (X := X₂ (shortComplexH2.{u, u_1} (G := G) X.1)) (Y := (shortComplexH2 X.X₂).X₃)
          (g (shortComplexH2.{u, u_1} (G := G) X.1) ≫ Hom.τ₃ (mapShortComplexH2 (MonoidHom.id G) X.f)) :
        (a : (↑(shortComplexH2 X.1).X₂ : Type (max u u_1))) → (↑(shortComplexH2 X.X₂).X₃ : Type (max u u_1)))
      x :
    (↑(shortComplexH2 X.X₂).X₃ : Type (max u u_1)))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type (max u u_1)) →ₗ[k] (↑x2 : Type (max u u_1)))
          (CC := ModuleCat.carrier) (X := X₂ (shortComplexH2.{u, u_1} (G := G) X.1))
          (Hom.τ₂ (mapShortComplexH2 (MonoidHom.id G) X.f) ≫ (shortComplexH2 X.X₂).g) :
        (a : (↑(shortComplexH2 X.1).X₂ : Type (max u u_1))) → (↑(shortComplexH2 X.X₂).X₃ : Type (max u u_1)))
      x :
    (↑(shortComplexH2 X.X₂).X₃ : Type (max u u_1)))
Tactic: have := congr($((mapShortComplexH2 (MonoidHom.id G) X.f).comm₂₃.symm) x)
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cocycles₁ X.X₃)
y : G → (↑X.X₂ : Type u)
hy :
  Eq (α := G → (↑X.X₃ : Type u)) ((⇑(Rep.Hom.hom X.g) : (a : (↑X.X₂ : Type u)) → (↑X.X₃ : Type u)) ∘ y)
    (⇑z : (a : G) → (↑X.X₃ : Type u))
x : G × G → (↑X.X₁ : Type u)
hx :
  Eq (α := G × G → (↑X.X₂ : Type u)) ((⇑(Rep.Hom.hom X.f) : (a : (↑X.X₁ : Type u)) → (↑X.X₂ : Type u)) ∘ x)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (d₁₂ X.X₂) :
        (a : (↑(ModuleCat.of k (G → (↑X.X₂ : Type u))) : Type u)) →
          (↑(ModuleCat.of k (G × G → (↑X.X₂ : Type u))) : Type u))
      y)
⊢ Eq (α := (↑((inhomogeneousCochains X.X₃).X (HAdd.hAdd (α := ℕ) 1 1)) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := (inhomogeneousCochains X.X₃).X 1) (Y :=
            (inhomogeneousCochains X.X₃).X (HAdd.hAdd (α := ℕ) 1 1))
            ((inhomogeneousCochains X.X₃).d 1 (HAdd.hAdd (α := ℕ) 1 1)) :
          (a : (↑((inhomogeneousCochains X.X₃).X 1) : Type u)) → (↑((inhomogeneousCochains X.X₃).X (1 + 1)) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (cochainsIso₁ X.X₃).inv :
              (a : (↑(ModuleCat.of k (G → (↑X.X₃ : Type u))) : Type u)) →
                (↑((inhomogeneousCochains X.X₃).X 1) : Type u))
            (⇑z : (a : G) → (↑X.X₃ : Type u)) :
          (↑((inhomogeneousCochains X.X₃).X 1) : Type u)) :
      (↑((inhomogeneousCochains X.X₃).X (HAdd.hAdd (α := ℕ) 1 1)) : Type u))
    (0 : (↑((inhomogeneousCochains X.X₃).X (HAdd.hAdd (α := ℕ) 1 1)) : Type u))
have rw : Eq (α := (↑((inhomogeneousCochains X.X₃).X (HAdd.hAdd (α := ℕ) 1 1)) : Type u))
  ((ModuleCat.Hom.hom (d₁₂ X.X₃ ≫ (cochainsIso₂ X.X₃).inv) :
        (a : (↑(ModuleCat.of k (G → (↑X.X₃ : Type u))) : Type u)) →
          (↑((inhomogeneousCochains X.X₃).X (1 + 1)) : Type u))
      (⇑z : (a : G) → (↑X.X₃ : Type u)) :
    (↑((inhomogeneousCochains X.X₃).X (HAdd.hAdd (α := ℕ) 1 1)) : Type u))
  (0 : (↑((inhomogeneousCochains X.X₃).X (HAdd.hAdd (α := ℕ) 1 1)) : Type u))
Tactic: rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, eq_d₁₂_comp_inv]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cocycles₁ X.X₃)
y : G → (↑X.X₂ : Type u)
hy :
  Eq (α := G → (↑X.X₃ : Type u)) ((⇑(Rep.Hom.hom X.g) : (a : (↑X.X₂ : Type u)) → (↑X.X₃ : Type u)) ∘ y)
    (⇑z : (a : G) → (↑X.X₃ : Type u))
x : G × G → (↑X.X₁ : Type u)
hx :
  Eq (α := G × G → (↑X.X₂ : Type u)) ((⇑(Rep.Hom.hom X.f) : (a : (↑X.X₁ : Type u)) → (↑X.X₂ : Type u)) ∘ x)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (d₁₂ X.X₂) :
        (a : (↑(ModuleCat.of k (G → (↑X.X₂ : Type u))) : Type u)) →
          (↑(ModuleCat.of k (G × G → (↑X.X₂ : Type u))) : Type u))
      y)
g : Fin (HAdd.hAdd (α := ℕ) 1 1) → G
⊢ Eq (α := (↑X.X₂ : Type u))
    (Function.comp (β := (↑X.X₁ : Type u)) (⇑(Rep.Hom.hom X.f) : (a : (↑X.X₁ : Type u)) → (↑X.X₂ : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (cochainsIso₂ X.X₁).inv :
            (a : (↑(ModuleCat.of k (G × G → (↑X.X₁ : Type u))) : Type u)) →
              (↑((inhomogeneousCochains X.X₁).X 2) : Type u))
          x)
        g :
      (↑X.X₂ : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := (inhomogeneousCochains X.X₂).X 1) (Y :=
            (inhomogeneousCochains X.X₂).X (HAdd.hAdd (α := ℕ) 1 1))
            ((inhomogeneousCochains X.X₂).d 1 (HAdd.hAdd (α := ℕ) 1 1)) :
          (a : (↑((inhomogeneousCochains X.X₂).X 1) : Type u)) → (↑((inhomogeneousCochains X.X₂).X (1 + 1)) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (cochainsIso₁ X.X₂).inv :
              (a : (↑(ModuleCat.of k (G → (↑X.X₂ : Type u))) : Type u)) →
                (↑((inhomogeneousCochains X.X₂).X 1) : Type u))
            y :
          (↑((inhomogeneousCochains X.X₂).X 1) : Type u))
        g :
      (↑X.X₂ : Type u))
have h : Eq (α := (↑X.X₂ : Type u))
  (Function.comp (β := (↑X.X₁ : Type u)) (⇑(Rep.Hom.hom X.f) : (a : (↑X.X₁ : Type u)) → (↑X.X₂ : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (cochainsIso₂ X.X₁).inv :
          (a : (↑(ModuleCat.of k (G × G → (↑X.X₁ : Type u))) : Type u)) →
            (↑((inhomogeneousCochains X.X₁).X 2) : Type u))
        x)
      g :
    (↑X.X₂ : Type u))
  ((ModuleCat.Hom.hom (d₁₂ X.X₂ ≫ (cochainsIso₂ X.X₂).inv) :
        (a : (↑(ModuleCat.of k (G → (↑X.X₂ : Type u))) : Type u)) →
          (↑((inhomogeneousCochains X.X₂).X (1 + 1)) : Type u))
      y g :
    (↑X.X₂ : Type u))
Tactic: rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, eq_d₁₂_comp_inv]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x y : (↑A : Type (max u u_1))
g : G
⊢ HSub.hSub (α := (↑A : Type (max u u_1)))
      ((((A.ρ : (a : G) → (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) g :
              (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) :
            (a : (↑A : Type (max u u_1))) → (↑A : Type (max u u_1)))
          (x + y) :
        (↑A : Type (max u u_1)))
      (x + y) =
    HAdd.hAdd (α := G → (↑A : Type (max u u_1))) (β := G → (↑A : Type (max u u_1)))
      (fun (g : G) ↦
        HSub.hSub (α := (↑A : Type (max u u_1)))
          ((((A.ρ : (a : G) → (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) g :
                  (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) :
                (a : (↑A : Type (max u u_1))) → (↑A : Type (max u u_1)))
              x :
            (↑A : Type (max u u_1)))
          x)
      (fun (g : G) ↦
        HSub.hSub (α := (↑A : Type (max u u_1)))
          ((((A.ρ : (a : G) → (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) g :
                  (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) :
                (a : (↑A : Type (max u u_1))) → (↑A : Type (max u u_1)))
              y :
            (↑A : Type (max u u_1)))
          y)
      g
have simp : HSub.hSub (α := (↑A : Type (max u u_1)))
      ((((A.ρ : (a : G) → (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) g :
              (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) :
            (a : (↑A : Type (max u u_1))) → (↑A : Type (max u u_1)))
          x :
        (↑A : Type (max u u_1)))
      x +
    HSub.hSub (α := (↑A : Type (max u u_1)))
      ((((A.ρ : (a : G) → (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) g :
              (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) :
            (a : (↑A : Type (max u u_1))) → (↑A : Type (max u u_1)))
          y :
        (↑A : Type (max u u_1)))
      y =
  HAdd.hAdd (α := G → (↑A : Type (max u u_1))) (β := G → (↑A : Type (max u u_1)))
    (fun (g : G) ↦
      HSub.hSub (α := (↑A : Type (max u u_1)))
        ((((A.ρ : (a : G) → (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) g :
                (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) :
              (a : (↑A : Type (max u u_1))) → (↑A : Type (max u u_1)))
            x :
          (↑A : Type (max u u_1)))
        x)
    (fun (g : G) ↦
      HSub.hSub (α := (↑A : Type (max u u_1)))
        ((((A.ρ : (a : G) → (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) g :
                (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) :
              (a : (↑A : Type (max u u_1))) → (↑A : Type (max u u_1)))
            y :
          (↑A : Type (max u u_1)))
        y)
    g
Tactic: simp only [map_add, add_sub_add_comm]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
r : k
x : (↑A : Type (max u u_1))
g : G
⊢ HSub.hSub (α := (↑A : Type (max u u_1)))
      ((((A.ρ : (a : G) → (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) g :
              (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) :
            (a : (↑A : Type (max u u_1))) → (↑A : Type (max u u_1)))
          (r • x) :
        (↑A : Type (max u u_1)))
      (r • x) =
    HSMul.hSMul (α := k) (β := G → (↑A : Type (max u u_1))) ((RingHom.id k : (a : k) → k) r : k)
      (fun (g : G) ↦
        HSub.hSub (α := (↑A : Type (max u u_1)))
          ((((A.ρ : (a : G) → (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) g :
                  (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) :
                (a : (↑A : Type (max u u_1))) → (↑A : Type (max u u_1)))
              x :
            (↑A : Type (max u u_1)))
          x)
      g
have dsimp : HSub.hSub (α := (↑A : Type (max u u_1)))
    ((((A.ρ : (a : G) → (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) g :
            (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) :
          (a : (↑A : Type (max u u_1))) → (↑A : Type (max u u_1)))
        (r • x) :
      (↑A : Type (max u u_1)))
    (r • x) =
  r •
    HSub.hSub (α := (↑A : Type (max u u_1)))
      ((((A.ρ : (a : G) → (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) g :
              (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) :
            (a : (↑A : Type (max u u_1))) → (↑A : Type (max u u_1)))
          x :
        (↑A : Type (max u u_1)))
      x
Tactic: dsimp
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
r : k
x : (↑A : Type (max u u_1))
g : G
⊢ HSub.hSub (α := (↑A : Type (max u u_1)))
      ((((A.ρ : (a : G) → (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) g :
              (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) :
            (a : (↑A : Type (max u u_1))) → (↑A : Type (max u u_1)))
          (r • x) :
        (↑A : Type (max u u_1)))
      (r • x) =
    r •
      HSub.hSub (α := (↑A : Type (max u u_1)))
        ((((A.ρ : (a : G) → (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) g :
                (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) :
              (a : (↑A : Type (max u u_1))) → (↑A : Type (max u u_1)))
            x :
          (↑A : Type (max u u_1)))
        x
have rw : HSMul.hSMul (β := (↑A : Type (max u u_1))) r
      ((((A.ρ : (a : G) → (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) g :
              (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) :
            (a : (↑A : Type (max u u_1))) → (↑A : Type (max u u_1)))
          x :
        (↑A : Type (max u u_1))) -
    r • x =
  r •
    HSub.hSub (α := (↑A : Type (max u u_1)))
      ((((A.ρ : (a : G) → (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) g :
              (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) :
            (a : (↑A : Type (max u u_1))) → (↑A : Type (max u u_1)))
          x :
        (↑A : Type (max u u_1)))
      x
Tactic: rw [map_smul, smul_sub]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
r : k
x : (↑A : Type (max u u_1))
g : G
rw :
  HSMul.hSMul (β := (↑A : Type (max u u_1))) r
        ((((A.ρ : (a : G) → (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) g :
                (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) :
              (a : (↑A : Type (max u u_1))) → (↑A : Type (max u u_1)))
            x :
          (↑A : Type (max u u_1))) -
      r • x =
    r •
      HSub.hSub (α := (↑A : Type (max u u_1)))
        ((((A.ρ : (a : G) → (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) g :
                (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) :
              (a : (↑A : Type (max u u_1))) → (↑A : Type (max u u_1)))
            x :
          (↑A : Type (max u u_1)))
        x
⊢ HSub.hSub (α := (↑A : Type (max u u_1)))
      ((((A.ρ : (a : G) → (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) g :
              (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) :
            (a : (↑A : Type (max u u_1))) → (↑A : Type (max u u_1)))
          (r • x) :
        (↑A : Type (max u u_1)))
      (r • x) =
    r •
      HSub.hSub (α := (↑A : Type (max u u_1)))
        ((((A.ρ : (a : G) → (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) g :
                (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) :
              (a : (↑A : Type (max u u_1))) → (↑A : Type (max u u_1)))
            x :
          (↑A : Type (max u u_1)))
        x
have rw₁ : HSMul.hSMul (β := (↑A : Type (max u u_1))) r
      ((((A.ρ : (a : G) → (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) g :
              (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) :
            (a : (↑A : Type (max u u_1))) → (↑A : Type (max u u_1)))
          x :
        (↑A : Type (max u u_1))) -
    r • x =
  HSMul.hSMul (β := (↑A : Type (max u u_1))) r
      ((((A.ρ : (a : G) → (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) g :
              (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) :
            (a : (↑A : Type (max u u_1))) → (↑A : Type (max u u_1)))
          x :
        (↑A : Type (max u u_1))) -
    r • x
Tactic: rw [map_smul, smul_sub]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
⊢ (ModuleCat.Hom.hom (d₀₁.{u, u_1} A)).ker = A.ρ.invariants
have h : ∀ (x : (↑(ModuleCat.of k (↑A : Type (max u u_1))) : Type (max u u_1))),
  x ∈ (ModuleCat.Hom.hom (d₀₁.{u, u_1} A)).ker ↔ x ∈ A.ρ.invariants
Tactic: ext x
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : (↑(ModuleCat.of k (↑A : Type (max u u_1))) : Type (max u u_1))
⊢ x ∈ (ModuleCat.Hom.hom (d₀₁.{u, u_1} A)).ker ↔ x ∈ A.ρ.invariants
have h : (∀ (x_1 : G),
    Eq (α := (↑A : Type (max u u_1)))
      ((ModuleCat.Hom.hom (d₀₁.{u, u_1} A) : (a : (↑A : Type (max u u_1))) → G → (↑A : Type (max u u_1))) x x_1 :
        (↑A : Type (max u u_1)))
      (0 x_1 : (↑A : Type (max u u_1)))) ↔
  ∀ (g : G),
    HSub.hSub (α := (↑A : Type (max u u_1)))
        ((((A.ρ : (a : G) → (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) g :
                (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) :
              (a : (↑A : Type (max u u_1))) → (↑A : Type (max u u_1)))
            x :
          (↑A : Type (max u u_1)))
        x =
      0
Tactic: simp only [LinearMap.mem_ker, mem_invariants, ← @sub_eq_zero _ _ _ x, funext_iff]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
inst_2 : A.IsTrivial
⊢ d₀₁.{u, u_1} A = 0
have hf : ∀ (x : (↑(ModuleCat.of k (↑A : Type (max u u_1))) : Type (max u u_1))) (x_1 : G),
  Eq (α := (↑A : Type (max u u_1)))
    ((ModuleCat.Hom.hom (d₀₁.{u, u_1} A) :
          (a : (↑(ModuleCat.of k (↑A : Type (max u u_1))) : Type (max u u_1))) →
            (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u u_1)))
        x x_1 :
      (↑A : Type (max u u_1)))
    ((ModuleCat.Hom.hom 0 :
          (a : (↑(ModuleCat.of k (↑A : Type (max u u_1))) : Type (max u u_1))) →
            (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u u_1)))
        x x_1 :
      (↑A : Type (max u u_1)))
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
inst_2 : A.IsTrivial
x : (↑(ModuleCat.of k (↑A : Type (max u u_1))) : Type (max u u_1))
x_1 : G
⊢ Eq (α := (↑A : Type (max u u_1)))
    ((ModuleCat.Hom.hom (d₀₁.{u, u_1} A) :
          (a : (↑(ModuleCat.of k (↑A : Type (max u u_1))) : Type (max u u_1))) →
            (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u u_1)))
        x x_1 :
      (↑A : Type (max u u_1)))
    ((ModuleCat.Hom.hom 0 :
          (a : (↑(ModuleCat.of k (↑A : Type (max u u_1))) : Type (max u u_1))) →
            (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u u_1)))
        x x_1 :
      (↑A : Type (max u u_1)))
have hf : Eq (α := (↑A : Type (max u u_1))) (0 : (↑A : Type (max u u_1)))
  ((ModuleCat.Hom.hom 0 :
        (a : (↑(ModuleCat.of k (↑A : Type (max u u_1))) : Type (max u u_1))) →
          (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u u_1)))
      x x_1 :
    (↑A : Type (max u u_1)))
Tactic: rw [d₀₁_hom_apply, isTrivial_apply, sub_self]