awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
g h : G
a : (↑A : Type u)
⊢ HSub.hSub (α := G × G →₀ (↑A : Type u)) (β := G × G →₀ (↑A : Type u))
      (single (g, 1)
          ((((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 × G →₀ (↑A : Type u))
      (single (1, h) a) ∈
    boundaries₂ A
have h₁ : (ModuleCat.Hom.hom (d₃₂ A) : (a : (↑(ModuleCat.of k (G × G × G →₀ (↑A : Type u))) : Type u)) → G × G →₀ (↑A : Type u))
    (single (g, 1, h)
      ((((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))) =
  HSub.hSub (α := G × G →₀ (↑A : Type u)) (β := G × G →₀ (↑A : Type u))
    (single (g, 1)
        ((((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 × G →₀ (↑A : Type u))
    (single (1, h) a)
Tactic: use single (g, 1, h) (A.ρ g (-a))
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
g h : G
a : (↑A : Type u)
⊢ HSub.hSub (α := G × G →₀ (↑A : Type u)) (β := G × G →₀ (↑A : Type u))
      (single (h, 1)
          ((((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 × G →₀ (↑A : Type u))
      (single (g * h, 1) a) ∈
    boundaries₂ A
have h₁ : (ModuleCat.Hom.hom (d₃₂ A) : (a : (↑(ModuleCat.of k (G × G × G →₀ (↑A : Type u))) : Type u)) → G × G →₀ (↑A : Type u))
    (single (g, h, 1) a) =
  HSub.hSub (α := G × G →₀ (↑A : Type u)) (β := G × G →₀ (↑A : Type u))
    (single (h, 1)
        ((((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 × G →₀ (↑A : Type u))
    (single (g * h, 1) a)
Tactic: use single (g, h, 1) a
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
g : G
a : A
⊢ IsCycle₁ (single g a) ↔ g • a = a
have rw : IsCycle₁ (single g a) ↔ g⁻¹ • g • a = g⁻¹ • a
Tactic: rw [← (MulAction.bijective g⁻¹).1.eq_iff]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
g : G × G
a : A
⊢ IsCycle₂ (single g a) ↔ HAdd.hAdd (α := G →₀ A) (single g.2 a) (single g.1 (g.1 • a)) = single (g.1 * g.2) (g.1 • a)
have rw : IsCycle₂ (single g a) ↔
  mapRange (HSMul.hSMul g.1⁻¹) sorry (HAdd.hAdd (α := G →₀ A) (single g.2 a) (single g.1 (g.1 • a))) =
    mapRange (HSMul.hSMul g.1⁻¹) sorry (single (g.1 * g.2) (g.1 • a))
Tactic: rw [← (Finsupp.mapRange_injective (α := G) _ (smul_zero _) (MulAction.bijective g.1⁻¹).1).eq_iff]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
a : A
⊢ IsBoundary₀ G a ↔ ∃ (x : G →₀ A), (x.sum fun (g : G) (z : A) ↦ g • z - z) = a
have mp : IsBoundary₀ G a → ∃ (x : G →₀ A), (x.sum fun (g : G) (z : A) ↦ g • z - z) = a
Tactic: constructor
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
a : A
mp : IsBoundary₀ G a → ∃ (x : G →₀ A), (x.sum fun (g : G) (z : A) ↦ g • z - z) = a
⊢ IsBoundary₀ G a ↔ ∃ (x : G →₀ A), (x.sum fun (g : G) (z : A) ↦ g • z - z) = a
have mpr : (∃ (x : G →₀ A), (x.sum fun (g : G) (z : A) ↦ g • z - z) = a) → IsBoundary₀ G a
Tactic: constructor
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
a : A
x : G →₀ A
hx : (x.sum fun (g : G) (z : A) ↦ g⁻¹ • z - z) = a
⊢ ∃ (x : G →₀ A), (x.sum fun (g : G) (z : A) ↦ g • z - z) = a
have h : (sum (x.sum fun (g : G) (a : A) ↦ single g (-(g⁻¹ • a))) fun (g : G) (z : A) ↦ g • z - z) = a
Tactic: use x.sum (fun g a => single g (-(g⁻¹ • a)))
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
a : A
x : G →₀ A
hx : (x.sum fun (g : G) (z : A) ↦ g • z - z) = a
⊢ IsBoundary₀ G a
have h : (sum (x.sum fun (g : G) (a : A) ↦ single g (-(g • a))) fun (g : G) (z : A) ↦ g⁻¹ • z - z) = a
Tactic: use x.sum (fun g a => single g (-(g • a)))
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
x : G →₀ A
⊢ IsBoundary₁ x ↔
    ∃ (y : Finsupp.{u_1, u_2} (G × G) A),
      (y.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
have mp : IsBoundary₁ x →
  ∃ (y : Finsupp.{u_1, u_2} (G × G) A),
    (y.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
Tactic: constructor
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
x : G →₀ A
mp :
  IsBoundary₁ x →
    ∃ (y : Finsupp.{u_1, u_2} (G × G) A),
      (y.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
⊢ IsBoundary₁ x ↔
    ∃ (y : Finsupp.{u_1, u_2} (G × G) A),
      (y.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
have mpr : (∃ (y : Finsupp.{u_1, u_2} (G × G) A),
    (y.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) →
  IsBoundary₁ x
Tactic: constructor
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
x : G →₀ A
y : Finsupp.{u_1, u_2} (G × G) A
hy :
  (y.sum 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
⊢ ∃ (y : Finsupp.{u_1, u_2} (G × G) A),
    (y.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
have h : (sum (y.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 a) (single (g.1 * g.2) (g.1 • a)) + single g.1 (g.1 • a)) =
  x
Tactic: use y.sum (fun g a => single g (g.1⁻¹ • a))
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
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
⊢ IsBoundary₁ x_1
have h : (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: use x.sum (fun g a => single g (g.1 • a))
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
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
⊢ 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
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
⊢ 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
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
⊢ ∃ (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
have 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
Tactic: use y.sum (fun g a => single g (g.1⁻¹ • a))
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
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
⊢ IsBoundary₂ x_1
have 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
Tactic: use x.sum (fun g a => single g (g.1 • a))
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
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
⊢ Membership.mem (γ := Submodule k A) (Coinvariants.ker (Representation.ofDistribMulAction k G A)) x
have 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)
Tactic: rcases (isBoundary₀_iff G x).1 hx with ⟨y, rfl⟩
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
⊢ (shortComplexH0 A).Exact
have 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₂
Tactic: rw [ShortComplex.moduleCat_exact_iff]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
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
have _ : ∀
  (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
Tactic: (hx : Coinvariants.mk _ _ = 0)
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (hypothesis)
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
have hx₁ : x ∈ (ModuleCat.Hom.hom (d₁₀ A)).range
Tactic: rw [Coinvariants.mk_eq_zero, ← range_d₁₀_eq_coinvariantsKer] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
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
⊢ ∃ (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
have 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))
Tactic: rcases hx with ⟨x, hx, rfl⟩
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
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)
⊢ ∃ (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))
have 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))
Tactic: use x
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
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 := cycles A 0) (iCycles A 0) :
          (a : (↑(cycles A 0) : Type u)) → (↑((inhomogeneousChains A).X 0) : Type u))
        (cyclesMk 0 0 cyclesMk₀_eq._proof_1
          ((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))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := cycles A 0) (iCycles A 0) :
          (a : (↑(cycles A 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) (cyclesIso₀ A).inv :
            (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑(cycles A 0) : Type u))
          x) :
      (↑((inhomogeneousChains A).X 0) : Type u))
have rw : 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) (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))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (X := cycles A 0) (iCycles A 0) :
        (a : (↑(cycles A 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) (cyclesIso₀ A).inv :
          (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑(cycles A 0) : Type u))
        x) :
    (↑((inhomogeneousChains A).X 0) : Type u))
Tactic: rw [iCycles_mk]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : ↥(cycles₁ A)
⊢ 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 1) (Y := (inhomogeneousChains A).X 0)
            ((inhomogeneousChains A).d 1 0) :
          (a : (↑((inhomogeneousChains A).X 1) : 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 (G →₀ (↑A : Type u))) : Type u)) → (↑((inhomogeneousChains A).X 1) : Type u))
          (↑x : G →₀ (↑A : Type u))) :
      (↑((inhomogeneousChains A).X 0) : Type u))
    (0 : (↑((inhomogeneousChains A).X 0) : Type u))
have rw : Eq (α := (↑((inhomogeneousChains A).X 0) : Type u))
  ((ModuleCat.Hom.hom (d₁₀ A ≫ (chainsIso₀ A).inv) :
        (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) → (↑((inhomogeneousChains A).X 0) : Type u))
      (↑x : G →₀ (↑A : Type u)) :
    (↑((inhomogeneousChains A).X 0) : Type u))
  (0 : (↑((inhomogeneousChains A).X 0) : Type u))
Tactic: rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, eq_d₁₀_comp_inv]