awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cycles₂ X.X₃)
y : G × G →₀ (↑X.X₂ : Type u)
hy :
  (mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap : (a : G × G →₀ (↑X.X₂ : Type u)) → G × G →₀ (↑X.X₃ : Type u)) y =
    (↑z : G × G →₀ (↑X.X₃ : Type u))
x : G →₀ (↑X.X₁ : Type u)
hx :
  Eq (α := G →₀ (↑X.X₂ : Type u))
    ((mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap : (a : G →₀ (↑X.X₁ : Type u)) → G →₀ (↑X.X₂ : 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) (d₂₁ X.X₂) :
          (a : (↑(ModuleCat.of k (G × G →₀ (↑X.X₂ : Type u))) : Type u)) →
            (↑(ModuleCat.of k (G →₀ (↑X.X₂ : Type u))) : Type u))
        y :
      (↑(ModuleCat.of k (G →₀ (↑X.X₂ : Type u))) : Type u))
x_1 : Fin 2 → G
⊢ Eq (α := (↑X.3 : Type u))
    ((((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                  ModuleCat.carrier) (X := (inhomogeneousChains X.X₂).X 2) (Y :=
                  HomologicalComplex.X (inhomogeneousChains (G := G) X.3) 2)
                  (HomologicalComplex.Hom.f (chainsMap (MonoidHom.id G) X.g) 2) :
                (a : (↑((inhomogeneousChains X.X₂).X 2) : Type u)) → (↑((inhomogeneousChains X.3).X 2) : Type u))
              ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                    ModuleCat.carrier) (chainsIso₂ X.X₂).inv :
                  (a : (↑(ModuleCat.of k (G × G →₀ (↑X.X₂ : Type u))) : Type u)) →
                    (↑((inhomogeneousChains X.X₂).X 2) : Type u))
                y) :
            (↑(HomologicalComplex.X (inhomogeneousChains (G := G) X.3) 2) : Type u)) :
          (a : Fin 2 → G) → (↑X.3 : Type u))
        x_1 :
      (↑X.3 : Type u))
    ((((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                  ModuleCat.carrier) (chainsIso₂ X.X₃).inv :
                (a : (↑(ModuleCat.of k (G × G →₀ (↑X.X₃ : Type u))) : Type u)) →
                  (↑((inhomogeneousChains X.X₃).X 2) : Type u))
              (↑z : G × G →₀ (↑X.X₃ : Type u)) :
            (↑((inhomogeneousChains X.X₃).X 2) : Type u)) :
          (a : Fin 2 → G) → (↑X.3 : Type u))
        x_1 :
      (↑X.3 : Type u))

Tactic:
simp [chainsIso₂, ← hy]

Premises used: groupHomology.chainsIso₂
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cycles₂ X.X₃)
y : G × G →₀ (↑X.X₂ : Type u)
hy :
  (mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap : (a : G × G →₀ (↑X.X₂ : Type u)) → G × G →₀ (↑X.X₃ : Type u)) y =
    (↑z : G × G →₀ (↑X.X₃ : Type u))
x : G →₀ (↑X.X₁ : Type u)
hx :
  Eq (α := G →₀ (↑X.X₂ : Type u))
    ((mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap : (a : G →₀ (↑X.X₁ : Type u)) → G →₀ (↑X.X₂ : 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) (d₂₁ X.X₂) :
          (a : (↑(ModuleCat.of k (G × G →₀ (↑X.X₂ : Type u))) : Type u)) →
            (↑(ModuleCat.of k (G →₀ (↑X.X₂ : Type u))) : Type u))
        y :
      (↑(ModuleCat.of k (G →₀ (↑X.X₂ : Type u))) : Type u))
x_1 : Fin 1 → G
rw :
  ((((ModuleCat.Hom.hom (d₂₁ X.X₂ ≫ (chainsIso₁ X.X₂).inv) :
              (a : (↑(ModuleCat.of k (G × G →₀ (↑X.X₂ : Type u))) : Type u)) →
                (↑((inhomogeneousChains X.X₂).X 1) : Type u))
            y :
          (↑((inhomogeneousChains X.X₂).X 1) : Type u)) :
        (a : Fin 1 → G) → (↑X.X₂ : Type u))
      x_1 :
    (↑X.X₂ : Type u))
| ((((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (X := (inhomogeneousChains X.X₂).X 2) (Y := (inhomogeneousChains X.X₂).X 1)
                ((inhomogeneousChains X.X₂).d 2 1) :
              (a : (↑((inhomogeneousChains X.X₂).X 2) : Type u)) → (↑((inhomogeneousChains X.X₂).X 1) : Type u))
            ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                  ModuleCat.carrier) (chainsIso₂ X.X₂).inv :
                (a : (↑(ModuleCat.of k (G × G →₀ (↑X.X₂ : Type u))) : Type u)) →
                  (↑((inhomogeneousChains X.X₂).X 2) : Type u))
              y) :
          (↑((inhomogeneousChains X.X₂).X 1) : Type u)) :
        (a : Fin 1 → G) → (↑X.X₂ : Type u))
      x_1 :
    (↑X.X₂ : Type u))

Tactic:
rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, eq_d₂₁_comp_inv]

Premises used: groupHomology.eq_d₂₁_comp_inv, LinearMap.comp_apply, ModuleCat.hom_comp
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cycles₂ X.X₃)
y : G × G →₀ (↑X.X₂ : Type u)
hy :
  (mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap : (a : G × G →₀ (↑X.X₂ : Type u)) → G × G →₀ (↑X.X₃ : Type u)) y =
    (↑z : G × G →₀ (↑X.X₃ : Type u))
x : G →₀ (↑X.X₁ : Type u)
hx :
  Eq (α := G →₀ (↑X.X₂ : Type u))
    ((mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap : (a : G →₀ (↑X.X₁ : Type u)) → G →₀ (↑X.X₂ : 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) (d₂₁ X.X₂) :
          (a : (↑(ModuleCat.of k (G × G →₀ (↑X.X₂ : Type u))) : Type u)) →
            (↑(ModuleCat.of k (G →₀ (↑X.X₂ : Type u))) : Type u))
        y :
      (↑(ModuleCat.of k (G →₀ (↑X.X₂ : Type u))) : Type u))
x_1 : Fin 1 → G
⊢ Eq (α := (↑X.X₂ : Type u))
    ((((mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap :
                (a : (Fin 1 → G) →₀ (↑X.X₁ : Type u)) → (Fin 1 → G) →₀ (↑X.X₂ : Type u))
              ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                    ModuleCat.carrier) (chainsIso₁ X.X₁).inv :
                  (a : (↑(ModuleCat.of k (G →₀ (↑X.X₁ : Type u))) : Type u)) →
                    (↑((inhomogeneousChains X.X₁).X 1) : Type u))
                x) :
            (Fin 1 → G) →₀ (↑X.X₂ : Type u)) :
          (a : Fin 1 → G) → (↑X.X₂ : Type u))
        x_1 :
      (↑X.X₂ : Type u))
    ((((ModuleCat.Hom.hom (d₂₁ X.X₂ ≫ (chainsIso₁ X.X₂).inv) :
                (a : (↑(ModuleCat.of k (G × G →₀ (↑X.X₂ : Type u))) : Type u)) →
                  (↑((inhomogeneousChains X.X₂).X 1) : Type u))
              y :
            (↑((inhomogeneousChains X.X₂).X 1) : Type u)) :
          (a : Fin 1 → G) → (↑X.X₂ : Type u))
        x_1 :
      (↑X.X₂ : Type u))

Tactic:
simp [← hx, chainsIso₁]

Premises used: groupHomology.chainsIso₁
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cycles₂ X.X₃)
y : G × G →₀ (↑X.X₂ : Type u)
hy :
  (mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap : (a : G × G →₀ (↑X.X₂ : Type u)) → G × G →₀ (↑X.X₃ : Type u)) y =
    (↑z : G × G →₀ (↑X.X₃ : Type u))
x : G →₀ (↑X.X₁ : Type u)
hx :
  Eq (α := G →₀ (↑X.X₂ : Type u))
    ((mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap : (a : G →₀ (↑X.X₁ : Type u)) → G →₀ (↑X.X₂ : 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) (d₂₁ X.X₂) :
          (a : (↑(ModuleCat.of k (G × G →₀ (↑X.X₂ : Type u))) : Type u)) →
            (↑(ModuleCat.of k (G →₀ (↑X.X₂ : Type u))) : Type u))
        y :
      (↑(ModuleCat.of k (G →₀ (↑X.X₂ : Type u))) : Type u))
⊢ Eq (α := (↑(groupHomology X.X₁ 1) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := groupHomology X.X₃ 2) (δ hX 2 1 ⋯) :
          (a : (↑(groupHomology X.X₃ 2) : Type u)) → (↑(groupHomology X.X₁ 1) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (H2π X.X₃) :
              (a : (↑(ModuleCat.of k ↥(cycles₂ X.X₃)) : Type u)) → (↑(H2 X.X₃) : Type u))
            z :
          (↑(H2 X.X₃) : Type u)) :
      (↑(groupHomology X.X₁ 1) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (H1π X.X₁) :
          (a : (↑(ModuleCat.of k ↥(cycles₁ X.X₁)) : Type u)) → (↑(H1 X.X₁) : Type u))
        (Subtype.mk (p := fun (x : G →₀ (↑X.X₁ : Type u)) ↦ x ∈ cycles₁ X.X₁) x ⋯) :
      (↑(H1 X.X₁) : Type u))

Tactic:
simpa only [H2π, ModuleCat.hom_comp, LinearMap.coe_comp, Function.comp_apply, H1π,
    ← cyclesMk₂_eq X.X₃, ← cyclesMk₁_eq X.X₁]
  using δ_apply hX (i := 2) (j := 1) rfl ((chainsIso₂ X.X₃).inv z.1) (by
    rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, eq_d₂₁_comp_inv]; simp)
    ((chainsIso₂ X.X₂).inv y) (Finsupp.ext fun _ => by simp [chainsIso₂, ← hy])
    ((chainsIso₁ X.X₁).inv x) (Finsupp.ext fun _ => by
    conv_rhs => rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, eq_d₂₁_comp_inv]
    simp [← hx, chainsIso₁])

Premises used: Finsupp.ext, CategoryTheory.ConcreteCategory.hom, groupHomology.H2π, CategoryTheory.ShortComplex.X₁, groupHomology.H1π, groupHomology.chainsIso₁, groupHomology.δ_apply, LinearMap.coe_comp, groupHomology.cyclesMk₂_eq, groupHomology.cyclesMk₁_eq, Function.comp_apply, groupHomology.chainsIso₂, Subtype.val, ModuleCat.hom_comp, DFunLike.coe, CategoryTheory.ShortComplex.X₃, CategoryTheory.Iso.inv, rfl, CategoryTheory.ShortComplex.X₂
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
g : G
a : (↑A : Type u)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (d₁₀ A) :
        (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
      (single g a) =
    HSub.hSub (α := (↑A : Type u))
      ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g⁻¹ : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
            (a : (↑A : Type u)) → (↑A : Type u))
          a :
        (↑A : Type u))
      a

Tactic:
simp [d₁₀]

Premises used: groupHomology.d₁₀
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
a : (↑A : Type u)
⊢ Eq (α := (↑(ModuleCat.of k (↑A : Type u)) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (d₁₀ A) :
          (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
        (single 1 a) :
      (↑(ModuleCat.of k (↑A : Type u)) : Type u))
    (0 : (↑(ModuleCat.of k (↑A : Type u)) : Type u))

Tactic:
simp [d₁₀]

Premises used: groupHomology.d₁₀
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
g : G
a : (↑A : Type u)
⊢ Eq (α := (↑(ModuleCat.of k (↑A : Type u)) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (d₁₀ A) :
          (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
        (single g⁻¹ a) :
      (↑(ModuleCat.of k (↑A : Type u)) : Type u))
    (-(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (d₁₀ A) :
            (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
          (single g
              ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                  (a : (↑A : Type u)) → (↑A : Type u))
                a) :
            G →₀ (↑A : Type u)) :
      (↑(ModuleCat.of k (↑A : Type u)) : Type u))

Tactic:
simp [d₁₀]

Premises used: groupHomology.d₁₀
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
symm : Coinvariants.ker A.ρ = (ModuleCat.Hom.hom (d₁₀ A)).range
⊢ (ModuleCat.Hom.hom (d₁₀ A)).range = Coinvariants.ker A.ρ

Tactic:
symm
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
h₁ :
  (Set.range fun (gv : G × (↑A : Type u)) ↦
      HSub.hSub (α := (↑A : Type u))
        ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) gv.1 : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
              (a : (↑A : Type u)) → (↑A : Type u))
            gv.2 :
          (↑A : Type u))
        gv.2) ⊆
    (↑(ModuleCat.Hom.hom (d₁₀ A)).range : Set (↑A : Type u))
h₂ :
  (ModuleCat.Hom.hom (d₁₀ A)).range ≤
    Submodule.span k
      (Set.range fun (gv : G × (↑A : Type u)) ↦
        HSub.hSub (α := (↑A : Type u))
          ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) gv.1 : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                (a : (↑A : Type u)) → (↑A : Type u))
              gv.2 :
            (↑A : Type u))
          gv.2)
⊢ Coinvariants.ker A.ρ = (ModuleCat.Hom.hom (d₁₀ A)).range

Tactic:
apply Submodule.span_eq_of_le

Premises used: Submodule.span_eq_of_le
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : G × (↑A : Type u)
h :
  Eq (α := (↑(ModuleCat.of k (↑A : Type u)) : Type u))
    ((ModuleCat.Hom.hom (d₁₀ A) :
          (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
        (single x.1⁻¹ x.2) :
      (↑(ModuleCat.of k (↑A : Type u)) : Type u))
    ((fun (gv : G × (↑A : Type u)) ↦
          HSub.hSub (α := (↑A : Type u))
            ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) gv.1 : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                  (a : (↑A : Type u)) → (↑A : Type u))
                gv.2 :
              (↑A : Type u))
            gv.2)
        x :
      (↑A : Type u))
⊢ (fun (gv : G × (↑A : Type u)) ↦
        HSub.hSub (α := (↑A : Type u))
          ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) gv.1 : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                (a : (↑A : Type u)) → (↑A : Type u))
              gv.2 :
            (↑A : Type u))
          gv.2)
      x ∈
    (↑(ModuleCat.Hom.hom (d₁₀ A)).range : Set (↑A : Type u))

Tactic:
use single x.1⁻¹ x.2

Premises used: Prod.fst, Inv.inv, Prod.snd, Finsupp.single
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : G × (↑A : Type u)
⊢ Eq (α := (↑(ModuleCat.of k (↑A : Type u)) : Type u))
    ((ModuleCat.Hom.hom (d₁₀ A) :
          (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
        (single x.1⁻¹ x.2) :
      (↑(ModuleCat.of k (↑A : Type u)) : Type u))
    ((fun (gv : G × (↑A : Type u)) ↦
          HSub.hSub (α := (↑A : Type u))
            ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) gv.1 : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                  (a : (↑A : Type u)) → (↑A : Type u))
                gv.2 :
              (↑A : Type u))
            gv.2)
        x :
      (↑A : Type u))

Tactic:
simp [d₁₀]

Premises used: groupHomology.d₁₀
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : (↑A : Type u)
hy :
  (ModuleCat.Hom.hom (d₁₀ A) :
        (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
      0 =
    x
⊢ Membership.mem (γ := Submodule k (↑A : Type u))
    (Submodule.span k
      (Set.range fun (gv : G × (↑A : Type u)) ↦
        HSub.hSub (α := (↑A : Type u))
          ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) gv.1 : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                (a : (↑A : Type u)) → (↑A : Type u))
              gv.2 :
            (↑A : Type u))
          gv.2))
    x

Tactic:
simp [← hy]
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
a : G
b : (↑A : Type u)
f : G →₀ (↑A : Type u)
h_1 : a ∉ f.support
h_2 : b ≠ 0
h :
  ∀ ⦃x : (↑A : Type u)⦄
    (hy :
      (ModuleCat.Hom.hom (d₁₀ A) :
            (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
          f =
        x),
    Membership.mem (γ := Submodule k (↑A : Type u))
      (Submodule.span k
        (Set.range fun (gv : G × (↑A : Type u)) ↦
          HSub.hSub (α := (↑A : Type u))
            ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) gv.1 : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                  (a : (↑A : Type u)) → (↑A : Type u))
                gv.2 :
              (↑A : Type u))
            gv.2))
      x
x : (↑A : Type u)
hy :
  (ModuleCat.Hom.hom (d₁₀ A) :
        (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
      (single a b + f) =
    x
⊢ Membership.mem (γ := Submodule k (↑A : Type u))
    (Submodule.span k
      (Set.range fun (gv : G × (↑A : Type u)) ↦
        HSub.hSub (α := (↑A : Type u))
          ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) gv.1 : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                (a : (↑A : Type u)) → (↑A : Type u))
              gv.2 :
            (↑A : Type u))
          gv.2))
    x

Tactic:
simpa [← hy, add_sub_add_comm, sum_add_index, d₁₀_single (G := G)]
        using Submodule.add_mem _ (Coinvariants.mem_ker_of_eq _ _ _ rfl) (h rfl)

Premises used: add_sub_add_comm, Representation.Coinvariants.mem_ker_of_eq, Finsupp.sum_add_index, rfl, groupHomology.d₁₀_single, Submodule.add_mem
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
hf :
  ∀ (a : G) (x : (↑A : Type u)),
    Eq (α := (↑(Functor.obj (coinvariantsFunctor k G) A) : Type u))
      ((ModuleCat.Hom.hom (d₁₀ A ≫ NatTrans.app (coinvariantsMk k G) A) ∘ₗ lsingle a :
            (a : (↑A : Type u)) → (↑((coinvariantsFunctor k G).obj A) : Type u))
          x :
        (↑(Functor.obj (coinvariantsFunctor k G) A) : Type u))
      (((ModuleCat.Hom.hom 0 :
                (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u) →ₗ[k]
                  (↑(Functor.obj (coinvariantsFunctor k G) A) : Type u)) ∘ₗ
              lsingle a :
            (a : (↑A : Type u)) → (↑((coinvariantsFunctor k G).obj A) : Type u))
          x :
        (↑(Functor.obj (coinvariantsFunctor k G) A) : Type u))
⊢ d₁₀ A ≫ NatTrans.app (coinvariantsMk k G) A = 0

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
a : G
x : (↑A : Type u)
⊢ Eq (α := (↑(Functor.obj (coinvariantsFunctor k G) A) : Type u))
    ((ModuleCat.Hom.hom (d₁₀ A ≫ NatTrans.app (coinvariantsMk k G) A) ∘ₗ lsingle a :
          (a : (↑A : Type u)) → (↑((coinvariantsFunctor k G).obj A) : Type u))
        x :
      (↑(Functor.obj (coinvariantsFunctor k G) A) : Type u))
    (((ModuleCat.Hom.hom 0 :
              (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u) →ₗ[k]
                (↑(Functor.obj (coinvariantsFunctor k G) A) : Type u)) ∘ₗ
            lsingle a :
          (a : (↑A : Type u)) → (↑((coinvariantsFunctor k G).obj A) : Type u))
        x :
      (↑(Functor.obj (coinvariantsFunctor k G) A) : Type u))

Tactic:
simp [d₁₀]

Premises used: groupHomology.d₁₀
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : (↑A : Type u)
hx : x ∈ Coinvariants.ker A.ρ
rcases :
  ∀ (y : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u))
    (hy :
      (ModuleCat.Hom.hom (d₁₀ A) :
            (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
          y =
        x),
    ∃ (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)),
      (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (chains₁ToCoinvariantsKer A) :
            (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) →
              (↑(ModuleCat.of k ↥(Coinvariants.ker A.ρ)) : Type u))
          a =
        Subtype.mk (p := fun (x : (↑A : Type u)) ↦ x ∈ Coinvariants.ker A.ρ) x hx
⊢ ∃ (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)),
    (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (chains₁ToCoinvariantsKer A) :
          (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) →
            (↑(ModuleCat.of k ↥(Coinvariants.ker A.ρ)) : Type u))
        a =
      Subtype.mk (p := fun (x : (↑A : Type u)) ↦ x ∈ Coinvariants.ker A.ρ) x hx

Tactic:
rcases range_d₁₀_eq_coinvariantsKer A ▸ hx with ⟨y, hy⟩
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : (↑A : Type u)
hx : x ∈ Coinvariants.ker A.ρ
y : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)
hy :
  (ModuleCat.Hom.hom (d₁₀ A) :
        (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
      y =
    x
w : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)
h :
  (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (chains₁ToCoinvariantsKer A) :
        (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) → (↑(ModuleCat.of k ↥(Coinvariants.ker A.ρ)) : Type u))
      y =
    Subtype.mk (p := fun (x : (↑A : Type u)) ↦ x ∈ Coinvariants.ker A.ρ) x hx
⊢ ∃ (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)),
    (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (chains₁ToCoinvariantsKer A) :
          (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) →
            (↑(ModuleCat.of k ↥(Coinvariants.ker A.ρ)) : Type u))
        a =
      Subtype.mk (p := fun (x : (↑A : Type u)) ↦ x ∈ Coinvariants.ker A.ρ) x hx

Tactic:
use y, Subtype.ext hy

Premises used: Subtype.ext
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
inst_2 : A.IsTrivial
hf :
  ∀ (a : G) (x : (↑A : Type u)),
    Eq (α := (↑(ModuleCat.of k (↑A : Type u)) : Type u))
      ((ModuleCat.Hom.hom (d₁₀ A) ∘ₗ lsingle a : (a : (↑A : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u)) x :
        (↑(ModuleCat.of k (↑A : Type u)) : Type u))
      (((ModuleCat.Hom.hom 0 :
                (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u) →ₗ[k] (↑(ModuleCat.of k (↑A : Type u)) : Type u)) ∘ₗ
              lsingle a :
            (a : (↑A : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
          x :
        (↑(ModuleCat.of k (↑A : Type u)) : Type u))
⊢ d₁₀ A = 0

Tactic:
ext