awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
x_1 : G →₀ A
x : Finsupp.{u_1, u_2} (G × G) A
hx :
  (x.sum fun (g : G × G) (a : A) ↦
      HSub.hSub (α := G →₀ A) (single g.2 a) (single (g.1 * g.2) (g.1 • a)) + single g.1 (g.1 • a)) =
    x_1
⊢ (sum (x.sum fun (g : G × G) (a : A) ↦ single g (g.1 • a)) fun (g : G × G) (a : A) ↦
      HSub.hSub (α := G →₀ A) (single g.2 (g.1⁻¹ • a)) (single (g.1 * g.2) a) + single g.1 a) =
    x_1

Tactic:
simp_all [sum_sum_index]

Premises used: Finsupp.sum_sum_index
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
x : Finsupp.{u_1, u_2} (G × G) A
mp :
  IsBoundary₂ x →
    ∃ (y : Finsupp.{u_1, u_2} (G × G × G) A),
      (y.sum fun (g : G × G × G) (a : A) ↦
          HSub.hSub (α := Finsupp.{u_1, u_2} (G × G) A) (single (g.2.1, g.2.2) a)
                (single (g.1 * g.2.1, g.2.2) (g.1 • a)) +
              single (g.1, g.2.1 * g.2.2) (g.1 • a) -
            single (g.1, g.2.1) (g.1 • a)) =
        x
mpr :
  (∃ (y : Finsupp.{u_1, u_2} (G × G × G) A),
      (y.sum fun (g : G × G × G) (a : A) ↦
          HSub.hSub (α := Finsupp.{u_1, u_2} (G × G) A) (single (g.2.1, g.2.2) a)
                (single (g.1 * g.2.1, g.2.2) (g.1 • a)) +
              single (g.1, g.2.1 * g.2.2) (g.1 • a) -
            single (g.1, g.2.1) (g.1 • a)) =
        x) →
    IsBoundary₂ x
⊢ IsBoundary₂ x ↔
    ∃ (y : Finsupp.{u_1, u_2} (G × G × G) A),
      (y.sum fun (g : G × G × G) (a : A) ↦
          HSub.hSub (α := Finsupp.{u_1, u_2} (G × G) A) (single (g.2.1, g.2.2) a)
                (single (g.1 * g.2.1, g.2.2) (g.1 • a)) +
              single (g.1, g.2.1 * g.2.2) (g.1 • a) -
            single (g.1, g.2.1) (g.1 • a)) =
        x

Tactic:
constructor
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
x : Finsupp.{u_1, u_2} (G × G) A
y : Finsupp.{u_1, u_2} (G × G × G) A
hy :
  (y.sum fun (g : G × G × G) (a : A) ↦
      HSub.hSub (α := Finsupp.{u_1, u_2} (G × G) A) (single (g.2.1, g.2.2) (g.1⁻¹ • a))
            (single (g.1 * g.2.1, g.2.2) a) +
          single (g.1, g.2.1 * g.2.2) a -
        single (g.1, g.2.1) a) =
    x
h :
  (sum (y.sum fun (g : G × G × G) (a : A) ↦ single g (g.1⁻¹ • a)) fun (g : G × G × G) (a : A) ↦
      HSub.hSub (α := Finsupp.{u_1, u_2} (G × G) A) (single (g.2.1, g.2.2) a) (single (g.1 * g.2.1, g.2.2) (g.1 • a)) +
          single (g.1, g.2.1 * g.2.2) (g.1 • a) -
        single (g.1, g.2.1) (g.1 • a)) =
    x
⊢ ∃ (y : Finsupp.{u_1, u_2} (G × G × G) A),
    (y.sum fun (g : G × G × G) (a : A) ↦
        HSub.hSub (α := Finsupp.{u_1, u_2} (G × G) A) (single (g.2.1, g.2.2) a)
              (single (g.1 * g.2.1, g.2.2) (g.1 • a)) +
            single (g.1, g.2.1 * g.2.2) (g.1 • a) -
          single (g.1, g.2.1) (g.1 • a)) =
      x

Tactic:
use y.sum (fun g a => single g (g.1⁻¹ • a))

Premises used: Finsupp.sum, Prod.fst, Inv.inv, HSMul.hSMul, Finsupp.single
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
x : Finsupp.{u_1, u_2} (G × G) A
y : Finsupp.{u_1, u_2} (G × G × G) A
hy :
  (y.sum fun (g : G × G × G) (a : A) ↦
      HSub.hSub (α := Finsupp.{u_1, u_2} (G × G) A) (single (g.2.1, g.2.2) (g.1⁻¹ • a))
            (single (g.1 * g.2.1, g.2.2) a) +
          single (g.1, g.2.1 * g.2.2) a -
        single (g.1, g.2.1) a) =
    x
⊢ (sum (y.sum fun (g : G × G × G) (a : A) ↦ single g (g.1⁻¹ • a)) fun (g : G × G × G) (a : A) ↦
      HSub.hSub (α := Finsupp.{u_1, u_2} (G × G) A) (single (g.2.1, g.2.2) a) (single (g.1 * g.2.1, g.2.2) (g.1 • a)) +
          single (g.1, g.2.1 * g.2.2) (g.1 • a) -
        single (g.1, g.2.1) (g.1 • a)) =
    x

Tactic:
simp_all [sum_sum_index]

Premises used: Finsupp.sum_sum_index
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
x_1 : Finsupp.{u_1, u_2} (G × G) A
x : Finsupp.{u_1, u_2} (G × G × G) A
hx :
  (x.sum fun (g : G × G × G) (a : A) ↦
      HSub.hSub (α := Finsupp.{u_1, u_2} (G × G) A) (single (g.2.1, g.2.2) a) (single (g.1 * g.2.1, g.2.2) (g.1 • a)) +
          single (g.1, g.2.1 * g.2.2) (g.1 • a) -
        single (g.1, g.2.1) (g.1 • a)) =
    x_1
h :
  (sum (x.sum fun (g : G × G × G) (a : A) ↦ single g (g.1 • a)) fun (g : G × G × G) (a : A) ↦
      HSub.hSub (α := Finsupp.{u_1, u_2} (G × G) A) (single (g.2.1, g.2.2) (g.1⁻¹ • a))
            (single (g.1 * g.2.1, g.2.2) a) +
          single (g.1, g.2.1 * g.2.2) a -
        single (g.1, g.2.1) a) =
    x_1
⊢ IsBoundary₂ x_1

Tactic:
use x.sum (fun g a => single g (g.1 • a))

Premises used: Finsupp.sum, Prod.fst, HSMul.hSMul, Finsupp.single
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
x_1 : Finsupp.{u_1, u_2} (G × G) A
x : Finsupp.{u_1, u_2} (G × G × G) A
hx :
  (x.sum fun (g : G × G × G) (a : A) ↦
      HSub.hSub (α := Finsupp.{u_1, u_2} (G × G) A) (single (g.2.1, g.2.2) a) (single (g.1 * g.2.1, g.2.2) (g.1 • a)) +
          single (g.1, g.2.1 * g.2.2) (g.1 • a) -
        single (g.1, g.2.1) (g.1 • a)) =
    x_1
⊢ (sum (x.sum fun (g : G × G × G) (a : A) ↦ single g (g.1 • a)) fun (g : G × G × G) (a : A) ↦
      HSub.hSub (α := Finsupp.{u_1, u_2} (G × G) A) (single (g.2.1, g.2.2) (g.1⁻¹ • a))
            (single (g.1 * g.2.1, g.2.2) a) +
          single (g.1, g.2.1 * g.2.2) a -
        single (g.1, g.2.1) a) =
    x_1

Tactic:
simp_all [sum_sum_index]

Premises used: Finsupp.sum_sum_index
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k_1 G_1 : Type u
inst : CommRing k_1
inst_1 : Group G_1
A_1 : Rep k_1 G_1
k G A : Type u
inst_2 : CommRing k
inst_3 : Group G
inst_4 : AddCommGroup A
inst_5 : Module k A
inst_6 : DistribMulAction G A
inst_7 : SMulCommClass G k A
x : A
hx : IsBoundary₀ G x
rcases :
  ∀ (y : G →₀ A) (hx : IsBoundary₀ G (A := A) (y.sum fun (g : G) (z : A) ↦ g • z - z)),
    Membership.mem (γ := Submodule k A) (Coinvariants.ker (Representation.ofDistribMulAction k G A))
      (y.sum fun (g : G) (z : A) ↦ g • z - z)
⊢ Membership.mem (γ := Submodule k A) (Coinvariants.ker (Representation.ofDistribMulAction k G A)) x

Tactic:
rcases (isBoundary₀_iff G x).1 hx with ⟨y, rfl⟩

Premises used: Iff.mp, groupHomology.isBoundary₀_iff, rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k_1 G_1 : Type u
inst : CommRing k_1
inst_1 : Group G_1
A_1 : Rep k_1 G_1
k G A : Type u
inst_2 : CommRing k
inst_3 : Group G
inst_4 : AddCommGroup A
inst_5 : Module k A
inst_6 : DistribMulAction G A
inst_7 : SMulCommClass G k A
y : G →₀ A
hx : IsBoundary₀ G (A := A) (y.sum fun (g : G) (z : A) ↦ g • z - z)
⊢ Membership.mem (γ := Submodule k A) (Coinvariants.ker (Representation.ofDistribMulAction k G A))
    (y.sum fun (g : G) (z : A) ↦ g • z - z)

Tactic:
Submodule.finsuppSum_mem _ _ _ _ fun g _ => Coinvariants.mem_ker_of_eq g (y g) _ rfl

Premises used: HSub.hSub, Representation.Coinvariants.mem_ker_of_eq, HSMul.hSMul, Submodule.finsuppSum_mem, DFunLike.coe, rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k_1 G_1 : Type u
inst : CommRing k_1
inst_1 : Group G_1
A_1 : Rep k_1 G_1
k G A : Type u
inst_2 : CommRing k
inst_3 : Group G
inst_4 : AddCommGroup A
inst_5 : Module k A
inst_6 : DistribMulAction G A
inst_7 : SMulCommClass G k A
y : G →₀ A
hx : IsBoundary₀ G (A := A) (y.sum fun (g : G) (z : A) ↦ g • z - z)
⊢ Membership.mem (γ := Submodule k A) (Coinvariants.ker (Representation.ofDistribMulAction k G A))
    (y.sum fun (g : G) (z : A) ↦ g • z - z)

Tactic:
exact Submodule.finsuppSum_mem _ _ _ _ fun g _ => Coinvariants.mem_ker_of_eq g (y g) _ rfl

Premises used: HSub.hSub, Representation.Coinvariants.mem_ker_of_eq, Submodule.finsuppSum_mem, DFunLike.coe, rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G A : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : AddCommGroup A
inst_3 : Module k A
inst_4 : DistribMulAction G A
inst_5 : SMulCommClass G k A
x : A
hx : Membership.mem (γ := Submodule k A) (Coinvariants.ker (Representation.ofDistribMulAction k G A)) x
x_1 : A
h :
  Membership.mem (γ := Set A)
    (Set.range fun (gv : G × A) ↦
      HSub.hSub (α := A)
        ((((Representation.ofDistribMulAction k G A : (a : G) → A →ₗ[k] A) gv.1 : A →ₗ[k] A) : (a : A) → A) gv.2 : A)
        gv.2)
    x_1
g : G × A
hg :
  (fun (gv : G × A) ↦
        HSub.hSub (α := A)
          ((((Representation.ofDistribMulAction k G A : (a : G) → A →ₗ[k] A) gv.1 : A →ₗ[k] A) : (a : A) → A) gv.2 : A)
          gv.2)
      g =
    x_1
⊢ (sum (single g.1⁻¹ g.2) fun (g : G) (z : A) ↦ g⁻¹ • z - z) = x_1

Tactic:
simp_all
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G A : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : AddCommGroup A
inst_3 : Module k A
inst_4 : DistribMulAction G A
inst_5 : SMulCommClass G k A
x : A
hx : Membership.mem (γ := Submodule k A) (Coinvariants.ker (Representation.ofDistribMulAction k G A)) x
⊢ Eq.{u + 1} (α := A) (sum 0 fun (g : G) (z : A) ↦ g⁻¹ • z - z) 0

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G A : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : AddCommGroup A
inst_3 : Module k A
inst_4 : DistribMulAction G A
inst_5 : SMulCommClass G k A
x : A
hx : Membership.mem (γ := Submodule k A) (Coinvariants.ker (Representation.ofDistribMulAction k G A)) x
x_1 x_2 : A
h :
  Membership.mem (γ := Submodule k A)
    (Submodule.span k
      (Set.range fun (gv : G × A) ↦
        HSub.hSub (α := A)
          ((((Representation.ofDistribMulAction k G A : (a : G) → A →ₗ[k] A) gv.1 : A →ₗ[k] A) : (a : A) → A) gv.2 : A)
          gv.2))
    x_1
h_1 :
  Membership.mem (γ := Submodule k A)
    (Submodule.span k
      (Set.range fun (gv : G × A) ↦
        HSub.hSub (α := A)
          ((((Representation.ofDistribMulAction k G A : (a : G) → A →ₗ[k] A) gv.1 : A →ₗ[k] A) : (a : A) → A) gv.2 : A)
          gv.2))
    x_2
h_2 : IsBoundary₀ G x_1
h_3 : IsBoundary₀ G x_2
X : G →₀ A
hX : (X.sum fun (g : G) (z : A) ↦ g⁻¹ • z - z) = x_1
Y : G →₀ A
hY : (Y.sum fun (g : G) (z : A) ↦ g⁻¹ • z - z) = x_2
⊢ ((X + Y).sum fun (g : G) (z : A) ↦ g⁻¹ • z - z) = x_1 + x_2

Tactic:
simp_all [sum_add_index', add_sub_add_comm]

Premises used: Finsupp.sum_add_index', add_sub_add_comm
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G A : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : AddCommGroup A
inst_3 : Module k A
inst_4 : DistribMulAction G A
inst_5 : SMulCommClass G k A
x : A
hx : Membership.mem (γ := Submodule k A) (Coinvariants.ker (Representation.ofDistribMulAction k G A)) x
r : k
x_1 : A
h :
  Membership.mem (γ := Submodule k A)
    (Submodule.span k
      (Set.range fun (gv : G × A) ↦
        HSub.hSub (α := A)
          ((((Representation.ofDistribMulAction k G A : (a : G) → A →ₗ[k] A) gv.1 : A →ₗ[k] A) : (a : A) → A) gv.2 : A)
          gv.2))
    x_1
h_1 : IsBoundary₀ G x_1
X : G →₀ A
hX : (X.sum fun (g : G) (z : A) ↦ g⁻¹ • z - z) = x_1
⊢ ((r • X).sum fun (g : G) (z : A) ↦ g⁻¹ • z - z) = r • x_1

Tactic:
simp [← hX, sum_smul_index', smul_comm, smul_sub, smul_sum]

Premises used: Finsupp.sum_smul_index', smul_sub, Finsupp.smul_sum, SMulCommClass.smul_comm
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G A : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : AddCommGroup A
inst_3 : Module k A
inst_4 : DistribMulAction G A
inst_5 : SMulCommClass G k A
x : G →₀ A
hx :
  Membership.mem (γ := Submodule k (G →₀ (↑(Rep.ofDistribMulAction k G A) : Type u)))
    (cycles₁ (Rep.ofDistribMulAction k G A)) x
⊢ IsCycle₁ x

Tactic:
simpa using (mem_cycles₁_iff (A := Rep.ofDistribMulAction k G A) x).1 hx

Premises used: Iff.mp, groupHomology.mem_cycles₁_iff
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G A : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : AddCommGroup A
inst_3 : Module k A
inst_4 : DistribMulAction G A
inst_5 : SMulCommClass G k A
x : G →₀ A
hx :
  Membership.mem (γ := Submodule k (G →₀ (↑(Rep.ofDistribMulAction k G A) : Type u)))
    (boundaries₁ (Rep.ofDistribMulAction k G A)) x
⊢ IsBoundary₁ x

Tactic:
hx

Premises used: Multiset.sum, Multiset.foldr, Set.Mem, setOf, Finsupp.sum, groupHomology.IsBoundary₁, Set.range, Finset.sum, Finsupp.single
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G A : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : AddCommGroup A
inst_3 : Module k A
inst_4 : DistribMulAction G A
inst_5 : SMulCommClass G k A
x : G × G →₀ A
hx :
  Membership.mem (γ := Submodule k (G × G →₀ (↑(Rep.ofDistribMulAction k G A) : Type u)))
    (cycles₂ (Rep.ofDistribMulAction k G A)) x
⊢ IsCycle₂ x

Tactic:
(mem_cycles₂_iff (A := Rep.ofDistribMulAction k G A) x).1 hx

Premises used: groupHomology.mem_cycles₂_iff, groupHomology.IsCycle₂, Iff.mp
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G A : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : AddCommGroup A
inst_3 : Module k A
inst_4 : DistribMulAction G A
inst_5 : SMulCommClass G k A
x : G × G →₀ A
hx :
  Membership.mem (γ := Submodule k (G × G →₀ (↑(Rep.ofDistribMulAction k G A) : Type u)))
    (boundaries₂ (Rep.ofDistribMulAction k G A)) x
⊢ IsBoundary₂ x

Tactic:
hx

Premises used: Multiset.sum, groupHomology.IsBoundary₂, Multiset.foldr, Set.Mem, setOf, Finsupp.sum, Set.range, Finset.sum, Finsupp.single
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
⊢ Epi (shortComplexH0 A).g

Tactic:
inferInstanceAs <| Epi ((coinvariantsMk k G).app A)

Premises used: _private.0.groupHomology.instEpiModuleCatGShortComplexH0._proof_1
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
rw :
  ∀ (x₂ : (↑(shortComplexH0 A).X₂ : Type u)),
    Eq (α := (↑(shortComplexH0 A).X₃ : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (shortComplexH0 A).g :
              (a : (↑(shortComplexH0 A).X₂ : Type u)) → (↑(shortComplexH0 A).X₃ : Type u))
            x₂ :
          (↑(shortComplexH0 A).X₃ : Type u))
        (0 : (↑(shortComplexH0 A).X₃ : Type u)) →
      ∃ (x₁ : (↑(shortComplexH0 A).X₁ : Type u)),
        (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (shortComplexH0 A).f :
              (a : (↑(shortComplexH0 A).X₁ : Type u)) → (↑(shortComplexH0 A).X₂ : Type u))
            x₁ =
          x₂
⊢ (shortComplexH0 A).Exact

Tactic:
rw [ShortComplex.moduleCat_exact_iff]

Premises used: CategoryTheory.ShortComplex.moduleCat_exact_iff
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : (↑(shortComplexH0 A).X₂ : Type u)
_ :
  ∀
    (hx :
      Eq (α := A.ρ.Coinvariants)
        ((Coinvariants.mk A.ρ : (a : (↑(shortComplexH0 A).X₂ : Type u)) → A.ρ.Coinvariants) x : A.ρ.Coinvariants)
        (0 : A.ρ.Coinvariants)),
    ∃ (x₁ : (↑(shortComplexH0 A).X₁ : Type u)),
      (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (shortComplexH0 A).f :
            (a : (↑(shortComplexH0 A).X₁ : Type u)) → (↑(shortComplexH0 A).X₂ : Type u))
          x₁ =
        x
⊢ Eq (α := (↑(shortComplexH0 A).X₃ : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (shortComplexH0 A).g :
            (a : (↑(shortComplexH0 A).X₂ : Type u)) → (↑(shortComplexH0 A).X₃ : Type u))
          x :
        (↑(shortComplexH0 A).X₃ : Type u))
      (0 : (↑(shortComplexH0 A).X₃ : Type u)) →
    ∃ (x₁ : (↑(shortComplexH0 A).X₁ : Type u)),
      (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (shortComplexH0 A).f :
            (a : (↑(shortComplexH0 A).X₁ : Type u)) → (↑(shortComplexH0 A).X₂ : Type u))
          x₁ =
        x

Tactic:
(hx : Coinvariants.mk _ _ = 0)
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : (↑(shortComplexH0 A).X₂ : Type u)
hx :
  Eq (α := A.ρ.Coinvariants)
    ((Coinvariants.mk A.ρ : (a : (↑(shortComplexH0 A).X₂ : Type u)) → A.ρ.Coinvariants) x : A.ρ.Coinvariants)
    (0 : A.ρ.Coinvariants)
⊢ x ∈ (ModuleCat.Hom.hom (d₁₀ A)).range

Tactic:
rw [Coinvariants.mk_eq_zero, ← range_d₁₀_eq_coinvariantsKer] at hx

Premises used: groupHomology.range_d₁₀_eq_coinvariantsKer, Representation.Coinvariants.mk_eq_zero
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : (↑(shortComplexH0 A).X₂ : Type u)
hx : x ∈ (ModuleCat.Hom.hom (d₁₀ A)).range
rcases :
  ∀ (x : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)),
    ∃ (x₁ : (↑(shortComplexH0 A).X₁ : Type u)),
      Eq (α := (↑(shortComplexH0 A).X₂ : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (shortComplexH0 A).f :
              (a : (↑(shortComplexH0 A).X₁ : Type u)) → (↑(shortComplexH0 A).X₂ : Type u))
            x₁ :
          (↑(shortComplexH0 A).X₂ : 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))
            x :
          (↑(ModuleCat.of k (↑A : Type u)) : Type u))
⊢ ∃ (x₁ : (↑(shortComplexH0 A).X₁ : Type u)),
    (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (shortComplexH0 A).f :
          (a : (↑(shortComplexH0 A).X₁ : Type u)) → (↑(shortComplexH0 A).X₂ : Type u))
        x₁ =
      x

Tactic:
rcases hx with ⟨x, hx, rfl⟩

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)
h :
  Eq (α := (↑(shortComplexH0 A).X₂ : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (shortComplexH0 A).f :
          (a : (↑(shortComplexH0 A).X₁ : Type u)) → (↑(shortComplexH0 A).X₂ : Type u))
        x :
      (↑(shortComplexH0 A).X₂ : 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))
        x :
      (↑(ModuleCat.of k (↑A : Type u)) : Type u))
⊢ ∃ (x₁ : (↑(shortComplexH0 A).X₁ : Type u)),
    Eq (α := (↑(shortComplexH0 A).X₂ : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (shortComplexH0 A).f :
            (a : (↑(shortComplexH0 A).X₁ : Type u)) → (↑(shortComplexH0 A).X₂ : Type u))
          x₁ :
        (↑(shortComplexH0 A).X₂ : 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))
          x :
        (↑(ModuleCat.of k (↑A : Type u)) : Type u))

Tactic:
use x
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)
⊢ Eq (α := (↑(shortComplexH0 A).X₂ : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (shortComplexH0 A).f :
          (a : (↑(shortComplexH0 A).X₁ : Type u)) → (↑(shortComplexH0 A).X₂ : Type u))
        x :
      (↑(shortComplexH0 A).X₂ : 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))
        x :
      (↑(ModuleCat.of k (↑A : Type u)) : Type u))

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
⊢ (ComplexShape.down ℕ).next 0 = 0

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
⊢ Eq (α := (inhomogeneousChains A).X 0 ⟶ (inhomogeneousChains A).X 0) ((inhomogeneousChains A).d 0 0) 0

Tactic:
simp [ChainComplex.of.d]

Premises used: ChainComplex.of.d
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
⊢ (cyclesIso₀ A).inv ≫ iCycles A 0 = (chainsIso₀ A).inv

Tactic:
simp [cyclesIso₀]

Premises used: groupHomology.cyclesIso₀
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
⊢ (ComplexShape.down ℕ).prev 0 = 1

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
⊢ HomologicalComplex.pOpcycles (inhomogeneousChains A) 0 ≫ (opcyclesIso₀ A).hom =
    (chainsIso₀ A).hom ≫ NatTrans.app (coinvariantsMk k G) A

Tactic:
CokernelCofork.π_mapOfIsColimit (φ := (d₁₀ArrowIso A).hom) _ _

Premises used: CategoryTheory.Limits.CokernelCofork.π_mapOfIsColimit, groupHomology.d₁₀, groupHomology.d₁₀ArrowIso, CategoryTheory.Iso.hom
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
⊢ NatTrans.app (coinvariantsMk k G) A ≫ (opcyclesIso₀ A).inv =
    (chainsIso₀ A).inv ≫ HomologicalComplex.pOpcycles (inhomogeneousChains A) 0

Tactic:
(CommSq.vert_inv ⟨pOpcycles_comp_opcyclesIso_hom A⟩).w

Premises used: CategoryTheory.CommSq.vert_inv, CategoryTheory.CommSq.mk, groupHomology.pOpcycles_comp_opcyclesIso_hom, CategoryTheory.CommSq.w
-- 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)
⊢ (ComplexShape.down ℕ).next 0 = 0

Tactic:
simp
-- 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)
⊢ Eq (α := (↑((inhomogeneousChains A).X 0) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := (inhomogeneousChains A).X 0) (Y := (inhomogeneousChains A).X 0)
            ((inhomogeneousChains A).d 0 0) :
          (a : (↑((inhomogeneousChains A).X 0) : Type u)) → (↑((inhomogeneousChains A).X 0) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (chainsIso₀ A).inv :
            (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑((inhomogeneousChains A).X 0) : Type u))
          x) :
      (↑((inhomogeneousChains A).X 0) : Type u))
    (0 : (↑((inhomogeneousChains A).X 0) : Type u))

Tactic:
simp [ChainComplex.of.d]

Premises used: ChainComplex.of.d