awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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.{u_1, u, u} k G
f : G × G → (↑A : Type u_1)
simp_rw :
  (∀ (g h j : G),
      HSub.hSub (α := (↑A : Type u_1))
              ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                    (a : (↑A : Type u_1)) → (↑A : Type u_1))
                  (f (h, j)) :
                (↑A : Type u_1))
              (f (g * h, j)) +
            f (g, h * j) -
          f (g, h) =
        0) ↔
    ∀ (g h j : G),
      f (g * h, j) + f (g, h) =
        HAdd.hAdd (α := (↑A : Type u_1))
          ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                (a : (↑A : Type u_1)) → (↑A : Type u_1))
              (f (h, j)) :
            (↑A : Type u_1))
          (f (g, h * j))
simp_rw₁ :
  (∀ (g h j : G),
      HSub.hSub (α := (↑A : Type u_1))
            ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                  (a : (↑A : Type u_1)) → (↑A : Type u_1))
                (f (h, j)) :
              (↑A : Type u_1))
            (f (g * h, j)) +
          f (g, h * j) =
        f (g, h)) ↔
    ∀ (g h j : G),
      f (g * h, j) + f (g, h) =
        HAdd.hAdd (α := (↑A : Type u_1))
          ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                (a : (↑A : Type u_1)) → (↑A : Type u_1))
              (f (h, j)) :
            (↑A : Type u_1))
          (f (g, h * j))
⊢ f ∈ cocycles₂ A ↔
    ∀ (g h j : G),
      f (g * h, j) + f (g, h) =
        HAdd.hAdd (α := (↑A : Type u_1))
          ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                (a : (↑A : Type u_1)) → (↑A : Type u_1))
              (f (h, j)) :
            (↑A : Type u_1))
          (f (g, h * j))
have simp_rw₂ : (∀ (g h j : G),
    HAdd.hAdd (α := (↑A : Type u_1))
          ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                (a : (↑A : Type u_1)) → (↑A : Type u_1))
              (f (h, j)) :
            (↑A : Type u_1))
          (f (g, h * j)) -
        f (g * h, j) =
      f (g, h)) ↔
  ∀ (g h j : G),
    f (g * h, j) + f (g, h) =
      HAdd.hAdd (α := (↑A : Type u_1))
        ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
              (a : (↑A : Type u_1)) → (↑A : Type u_1))
            (f (h, j)) :
          (↑A : Type u_1))
        (f (g, h * j))
Tactic: simp_rw [mem_cocycles₂_def, sub_eq_zero, sub_add_eq_add_sub, sub_eq_iff_eq_add, eq_comm,
    add_comm (f (_ * _, _))]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree (hypothesis)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep.{u_1, u, u} k G
f : ↥(cocycles₂ A)
g : G
⊢ Eq.{u_1 + 1} (α := (↑A : Type u_1)) ((f : (a : G × G) → (↑A : Type u_1)) (1, g) : (↑A : Type u_1))
    ((f : (a : G × G) → (↑A : Type u_1)) (1, 1) : (↑A : Type u_1))
have this : HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1))
    (((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) 1 : (a : (↑A : Type u_1)) → (↑A : Type u_1))
        ((f : (a : G × G) → (↑A : Type u_1)) (1, g) : (↑A : Type u_1)) :
      (↑A : Type u_1))
    ((f : (a : G × G) → (↑A : Type u_1)) (1, 1 * g) : (↑A : Type u_1)) =
  HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1))
    ((f : (a : G × G) → (↑A : Type u_1)) (HMul.hMul (α := G) 1 1, g) : (↑A : Type u_1))
    ((f : (a : G × G) → (↑A : Type u_1)) (1, 1) : (↑A : Type u_1))
Tactic: have := ((mem_cocycles₂_iff f).1 f.2 1 1 g).symm
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree (hypothesis)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep.{u_1, u, u} k G
f : ↥(cocycles₂ A)
g : G
⊢ Eq.{u_1 + 1} (α := (↑A : Type u_1)) ((f : (a : G × G) → (↑A : Type u_1)) (g, 1) : (↑A : Type u_1))
    ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
          (a : (↑A : Type u_1)) → (↑A : Type u_1))
        ((f : (a : G × G) → (↑A : Type u_1)) (1, 1) : (↑A : Type u_1)) :
      (↑A : Type u_1))
have this : HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1))
    ((f : (a : G × G) → (↑A : Type u_1)) (g * 1, 1) : (↑A : Type u_1))
    ((f : (a : G × G) → (↑A : Type u_1)) (g, 1) : (↑A : Type u_1)) =
  HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1))
    ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
          (a : (↑A : Type u_1)) → (↑A : Type u_1))
        ((f : (a : G × G) → (↑A : Type u_1)) (1, 1) : (↑A : Type u_1)) :
      (↑A : Type u_1))
    ((f : (a : G × G) → (↑A : Type u_1)) (g, HMul.hMul (α := G) 1 1) : (↑A : Type u_1))
Tactic: have := (mem_cocycles₂_iff f).1 f.2 g 1 1
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree (hypothesis)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep.{u_1, u, u} k G
f : ↥(cocycles₂ A)
g : G
⊢ HSub.hSub (α := (↑A : Type u_1)) (β := (↑A : Type u_1))
      ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
            (a : (↑A : Type u_1)) → (↑A : Type u_1))
          ((f : (a : G × G) → (↑A : Type u_1)) (g⁻¹, g) : (↑A : Type u_1)) :
        (↑A : Type u_1))
      ((f : (a : G × G) → (↑A : Type u_1)) (g, g⁻¹) : (↑A : Type u_1)) =
    HSub.hSub (α := (↑A : Type u_1)) (β := (↑A : Type u_1))
      ((f : (a : G × G) → (↑A : Type u_1)) (1, 1) : (↑A : Type u_1))
      ((f : (a : G × G) → (↑A : Type u_1)) (g, 1) : (↑A : Type u_1))
have this : HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1))
    ((f : (a : G × G) → (↑A : Type u_1)) (g * g⁻¹, g) : (↑A : Type u_1))
    ((f : (a : G × G) → (↑A : Type u_1)) (g, g⁻¹) : (↑A : Type u_1)) =
  HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1))
    ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
          (a : (↑A : Type u_1)) → (↑A : Type u_1))
        ((f : (a : G × G) → (↑A : Type u_1)) (g⁻¹, g) : (↑A : Type u_1)) :
      (↑A : Type u_1))
    ((f : (a : G × G) → (↑A : Type u_1)) (g, g⁻¹ * g) : (↑A : Type u_1))
Tactic: have := (mem_cocycles₂_iff f).1 f.2 g g⁻¹ g
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree (hypothesis)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep.{u_1, u, u} k G
f : ↥(cocycles₂ A)
g : G
this :
  HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1))
      ((f : (a : G × G) → (↑A : Type u_1)) (g * g⁻¹, g) : (↑A : Type u_1))
      ((f : (a : G × G) → (↑A : Type u_1)) (g, g⁻¹) : (↑A : Type u_1)) =
    HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1))
      ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
            (a : (↑A : Type u_1)) → (↑A : Type u_1))
          ((f : (a : G × G) → (↑A : Type u_1)) (g⁻¹, g) : (↑A : Type u_1)) :
        (↑A : Type u_1))
      ((f : (a : G × G) → (↑A : Type u_1)) (g, g⁻¹ * g) : (↑A : Type u_1))
⊢ HSub.hSub (α := (↑A : Type u_1)) (β := (↑A : Type u_1))
      ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
            (a : (↑A : Type u_1)) → (↑A : Type u_1))
          ((f : (a : G × G) → (↑A : Type u_1)) (g⁻¹, g) : (↑A : Type u_1)) :
        (↑A : Type u_1))
      ((f : (a : G × G) → (↑A : Type u_1)) (g, g⁻¹) : (↑A : Type u_1)) =
    HSub.hSub (α := (↑A : Type u_1)) (β := (↑A : Type u_1))
      ((f : (a : G × G) → (↑A : Type u_1)) (1, 1) : (↑A : Type u_1))
      ((f : (a : G × G) → (↑A : Type u_1)) (g, 1) : (↑A : Type u_1))
have this₁ : HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1)) ((f : (a : G × G) → (↑A : Type u_1)) (1, 1) : (↑A : Type u_1))
    ((f : (a : G × G) → (↑A : Type u_1)) (g, g⁻¹) : (↑A : Type u_1)) =
  HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1))
    ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
          (a : (↑A : Type u_1)) → (↑A : Type u_1))
        ((f : (a : G × G) → (↑A : Type u_1)) (g⁻¹, g) : (↑A : Type u_1)) :
      (↑A : Type u_1))
    ((f : (a : G × G) → (↑A : Type u_1)) (g, 1) : (↑A : Type u_1))
Tactic: simp only [mul_inv_cancel, inv_mul_cancel, cocycles₂_map_one_fst _ g]
    at this
Cleared hypotheses: this
-- 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
⊢ coboundaries₁.{u, u_1} A = ⊥
have simp_rw : Eq (α := Submodule k (G → (↑A : Type (max u u_1))))
  (LinearMap.range (R := k) (M := (↑A : Type (max u u_1))) (τ₁₂ := RingHom.id k) (ModuleCat.Hom.hom 0) :
    Submodule k (G → (↑A : Type (max u u_1))))
  (⊥ : Submodule k (G → (↑A : Type (max u u_1))))
Tactic: simp_rw [coboundaries₁, d₀₁_eq_zero]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree (goal)
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : MulAction G A
f : G → A
hf : IsCocycle₁ f
g : G
⊢ g • f g⁻¹ = -f g
have rw : g • f g⁻¹ + f g = 0
Tactic: rw [← add_eq_zero_iff_eq_neg, ← map_one_of_isCocycle₁ hf, ← mul_inv_cancel g, hf g g⁻¹]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree (goal)
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : MulAction G A
f : G → A
hf : IsCocycle₁ f
g : G
rw : g • f g⁻¹ + f g = 0
⊢ g • f g⁻¹ = -f g
have rw₁ : g • f g⁻¹ + f g = f 1
Tactic: rw [← add_eq_zero_iff_eq_neg, ← map_one_of_isCocycle₁ hf, ← mul_inv_cancel g, hf g g⁻¹]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree (goal)
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : MulAction G A
f : G → A
hf : IsCocycle₁ f
g : G
rw : g • f g⁻¹ + f g = 0
rw₁ : g • f g⁻¹ + f g = f 1
⊢ g • f g⁻¹ = -f g
have rw₂ : g • f g⁻¹ + f g = f (g * g⁻¹)
Tactic: rw [← add_eq_zero_iff_eq_neg, ← map_one_of_isCocycle₁ hf, ← mul_inv_cancel g, hf g g⁻¹]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree (goal)
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : MulAction G A
f : G → A
hf : IsCocycle₁ f
g : G
rw : g • f g⁻¹ + f g = 0
rw₁ : g • f g⁻¹ + f g = f 1
rw₂ : g • f g⁻¹ + f g = f (g * g⁻¹)
⊢ g • f g⁻¹ = -f g
have rw₃ : g • f g⁻¹ + f g = g • f g⁻¹ + f g
Tactic: rw [← add_eq_zero_iff_eq_neg, ← map_one_of_isCocycle₁ hf, ← mul_inv_cancel g, hf g g⁻¹]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree (hypothesis)
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : MulAction G A
f : G × G → A
hf : IsCocycle₂ f
g : G
⊢ g • f (g⁻¹, g) - f (g, g⁻¹) = f (1, 1) - f (g, 1)
have this : f (g * g⁻¹, g) + f (g, g⁻¹) = g • f (g⁻¹, g) + f (g, g⁻¹ * g)
Tactic: have := hf g g⁻¹ g
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree (hypothesis)
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : MulAction G A
f : G × G → A
hf : IsCocycle₂ f
g : G
this : f (g * g⁻¹, g) + f (g, g⁻¹) = g • f (g⁻¹, g) + f (g, g⁻¹ * g)
⊢ g • f (g⁻¹, g) - f (g, g⁻¹) = f (1, 1) - f (g, 1)
have this₁ : f (1, 1) + f (g, g⁻¹) = g • f (g⁻¹, g) + f (g, 1)
Tactic: simp only [mul_inv_cancel, inv_mul_cancel, map_one_fst_of_isCocycle₂ hf g] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree (goal)
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
f : G → A
hf :
  Membership.mem (γ := Submodule k (G → (↑(Rep.ofDistribMulAction k G A) : Type u)))
    (coboundaries₁ (Rep.ofDistribMulAction k G A)) f
⊢ IsCoboundary₁ f
have rcases : ∀ (a : (↑(ModuleCat.of k (↑(Rep.ofDistribMulAction k G A) : Type u)) : Type u)),
  IsCoboundary₁.{u, u} (G := G) (A := A)
    ((ModuleCat.Hom.hom (d₀₁ (Rep.ofDistribMulAction k G A)) :
        (a : (↑(ModuleCat.of k (↑(Rep.ofDistribMulAction k G A) : Type u)) : Type u)) →
          G → (↑(Rep.ofDistribMulAction k G A) : Type u))
      a)
Tactic: rcases hf with ⟨a, rfl⟩
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree (goal)
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
f : G × G → A
hf :
  Membership.mem (γ := Submodule k (G × G → (↑(Rep.ofDistribMulAction k G A) : Type u)))
    (coboundaries₂ (Rep.ofDistribMulAction k G A)) f
⊢ IsCoboundary₂ f
have rcases : ∀ (a : (↑(ModuleCat.of k (G → (↑(Rep.ofDistribMulAction k G A) : Type u))) : Type u)),
  IsCoboundary₂.{u, u} (G := G) (A := A)
    ((ModuleCat.Hom.hom (d₁₂ (Rep.ofDistribMulAction k G A)) :
        (a : (↑(ModuleCat.of k (G → (↑(Rep.ofDistribMulAction k G A) : Type u))) : Type u)) →
          G × G → (↑(Rep.ofDistribMulAction k G A) : Type u))
      a)
Tactic: rcases hf with ⟨a, rfl⟩
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree (goal)
Goal:
G : Type u_1
M : Type u_2
inst : Group G
inst_1 : CommGroup M
inst_2 : MulAction G M
f : G → M
hf : IsMulCocycle₁ f
g : G
⊢ g • f g⁻¹ = (f g)⁻¹
have rw : g • f g⁻¹ * f g = 1
Tactic: rw [← mul_eq_one_iff_eq_inv, ← map_one_of_isMulCocycle₁ hf, ← mul_inv_cancel g, hf g g⁻¹]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree (goal)
Goal:
G : Type u_1
M : Type u_2
inst : Group G
inst_1 : CommGroup M
inst_2 : MulAction G M
f : G → M
hf : IsMulCocycle₁ f
g : G
rw : g • f g⁻¹ * f g = 1
⊢ g • f g⁻¹ = (f g)⁻¹
have rw₁ : g • f g⁻¹ * f g = f 1
Tactic: rw [← mul_eq_one_iff_eq_inv, ← map_one_of_isMulCocycle₁ hf, ← mul_inv_cancel g, hf g g⁻¹]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree (goal)
Goal:
G : Type u_1
M : Type u_2
inst : Group G
inst_1 : CommGroup M
inst_2 : MulAction G M
f : G → M
hf : IsMulCocycle₁ f
g : G
rw : g • f g⁻¹ * f g = 1
rw₁ : g • f g⁻¹ * f g = f 1
⊢ g • f g⁻¹ = (f g)⁻¹
have rw₂ : g • f g⁻¹ * f g = f (g * g⁻¹)
Tactic: rw [← mul_eq_one_iff_eq_inv, ← map_one_of_isMulCocycle₁ hf, ← mul_inv_cancel g, hf g g⁻¹]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree (goal)
Goal:
G : Type u_1
M : Type u_2
inst : Group G
inst_1 : CommGroup M
inst_2 : MulAction G M
f : G → M
hf : IsMulCocycle₁ f
g : G
rw : g • f g⁻¹ * f g = 1
rw₁ : g • f g⁻¹ * f g = f 1
rw₂ : g • f g⁻¹ * f g = f (g * g⁻¹)
⊢ g • f g⁻¹ = (f g)⁻¹
have rw₃ : g • f g⁻¹ * f g = g • f g⁻¹ * f g
Tactic: rw [← mul_eq_one_iff_eq_inv, ← map_one_of_isMulCocycle₁ hf, ← mul_inv_cancel g, hf g g⁻¹]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree (hypothesis)
Goal:
G : Type u_1
M : Type u_2
inst : Group G
inst_1 : CommGroup M
inst_2 : MulAction G M
f : G × G → M
hf : IsMulCocycle₂ f
g : G
⊢ g • f (g⁻¹, g) / f (g, g⁻¹) = f (1, 1) / f (g, 1)
have this : f (g * g⁻¹, g) * f (g, g⁻¹) = g • f (g⁻¹, g) * f (g, g⁻¹ * g)
Tactic: have := hf g g⁻¹ g
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree (hypothesis)
Goal:
G : Type u_1
M : Type u_2
inst : Group G
inst_1 : CommGroup M
inst_2 : MulAction G M
f : G × G → M
hf : IsMulCocycle₂ f
g : G
this : f (g * g⁻¹, g) * f (g, g⁻¹) = g • f (g⁻¹, g) * f (g, g⁻¹ * g)
⊢ g • f (g⁻¹, g) / f (g, g⁻¹) = f (1, 1) / f (g, 1)
have this₁ : f (1, 1) * f (g, g⁻¹) = g • f (g⁻¹, g) * f (g, 1)
Tactic: simp only [mul_inv_cancel, inv_mul_cancel, map_one_fst_of_isMulCocycle₂ hf g] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree (goal)
Goal:
G M : Type
inst : Group G
inst_1 : CommGroup M
inst_2 : MulDistribMulAction G M
f : G → M
hf :
  Membership.mem (γ := Submodule ℤ (G → (↑(Rep.ofMulDistribMulAction G M) : Type)))
    (coboundaries₁ (Rep.ofMulDistribMulAction G M)) f
⊢ IsMulCoboundary₁ (M := M) ((⇑Additive.ofMul : (a : M) → Additive M) ∘ f)
have rcases : ∀ (x : (↑(ModuleCat.of ℤ (↑(Rep.ofMulDistribMulAction G M) : Type)) : Type)),
  IsMulCoboundary₁ (G := G) (M := M)
    (Function.comp (β := M) (⇑Additive.ofMul : (a : M) → Additive M)
      ((ModuleCat.Hom.hom (d₀₁ (Rep.ofMulDistribMulAction G M)) :
          (a : (↑(ModuleCat.of ℤ (↑(Rep.ofMulDistribMulAction G M) : Type)) : Type)) →
            G → (↑(Rep.ofMulDistribMulAction G M) : Type))
        x))
Tactic: rcases hf with ⟨x, rfl⟩
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree (goal)
Goal:
G M : Type
inst : Group G
inst_1 : CommGroup M
inst_2 : MulDistribMulAction G M
f : G × G → M
hf :
  Membership.mem (γ := Submodule ℤ (G × G → (↑(Rep.ofMulDistribMulAction G M) : Type)))
    (coboundaries₂ (Rep.ofMulDistribMulAction G M)) f
⊢ IsMulCoboundary₂ (M := M) ((⇑Additive.toMul : (a : Additive M) → M) ∘ f)
have rcases : ∀ (x : (↑(ModuleCat.of ℤ (G → (↑(Rep.ofMulDistribMulAction G M) : Type))) : Type)),
  IsMulCoboundary₂ (G := G) (M := M)
    (Function.comp (β := Additive M) (⇑Additive.toMul : (a : Additive M) → M)
      ((ModuleCat.Hom.hom (d₁₂ (Rep.ofMulDistribMulAction G M)) :
          (a : (↑(ModuleCat.of ℤ (G → (↑(Rep.ofMulDistribMulAction G M) : Type))) : Type)) →
            G × G → (↑(Rep.ofMulDistribMulAction G M) : Type))
        x))
Tactic: rcases hf with ⟨x, rfl⟩
Cleared hypotheses: f, hf
-- 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
⊢ Mono (shortComplexH0.{u, u_1} A).f
have rw : Function.Injective (α := (↑(shortComplexH0.{u, u_1} A).X₁ : Type (max u u_1))) (β :=
  (↑(shortComplexH0.{u, u_1} A).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) (shortComplexH0.{u, u_1} A).f) :
    (a : (↑(shortComplexH0 A).X₁ : Type (max u u_1))) → (↑(shortComplexH0 A).X₂ : Type (max u u_1)))
Tactic: rw [ModuleCat.mono_iff_injective]
-- 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
⊢ (shortComplexH0.{u, u_1} A).Exact
have rw : ∀ (x₂ : (↑(shortComplexH0.{u, u_1} A).X₂ : Type (max u u_1))),
  Eq (α := (↑(shortComplexH0.{u, u_1} A).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) (shortComplexH0.{u, u_1} A).g :
            (a : (↑(shortComplexH0 A).X₂ : Type (max u u_1))) → (↑(shortComplexH0 A).X₃ : Type (max u u_1)))
          x₂ :
        (↑(shortComplexH0.{u, u_1} A).X₃ : Type (max u u_1)))
      (0 : (↑(shortComplexH0.{u, u_1} A).X₃ : Type (max u u_1))) →
    ∃ (x₁ : (↑(shortComplexH0.{u, u_1} A).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) (shortComplexH0.{u, u_1} A).f :
            (a : (↑(shortComplexH0 A).X₁ : Type (max u u_1))) → (↑(shortComplexH0 A).X₂ : Type (max u u_1)))
          x₁ =
        x₂
Tactic: rw [ShortComplex.moduleCat_exact_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
x : (↑A : Type (max u u_1))
⊢ Eq (α := (↑(shortComplexH0.{u, u_1} A).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) (shortComplexH0.{u, u_1} A).g :
            (a : (↑(shortComplexH0 A).X₂ : Type (max u u_1))) → (↑(shortComplexH0 A).X₃ : Type (max u u_1)))
          x :
        (↑(shortComplexH0.{u, u_1} A).X₃ : Type (max u u_1)))
      (0 : (↑(shortComplexH0.{u, u_1} A).X₃ : Type (max u u_1))) →
    ∃ (x₁ : (↑(shortComplexH0.{u, u_1} A).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) (shortComplexH0.{u, u_1} A).f :
            (a : (↑(shortComplexH0 A).X₁ : Type (max u u_1))) → (↑(shortComplexH0 A).X₂ : Type (max u u_1)))
          x₁ =
        x
have d₀₁ : ∀
  (hx :
    Eq (α := (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u_1 u)))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type (max u_1 u)) →ₗ[k] (↑x2 : Type (max u_1 u)))
              (CC := ModuleCat.carrier) (d₀₁.{u, u_1} A) :
            (a : (↑(ModuleCat.of k (↑A : Type (max u u_1))) : Type (max u_1 u))) →
              (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u_1 u)))
          x :
        (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u_1 u)))
      (0 : (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u_1 u)))),
  ∃ (x₁ : (↑(shortComplexH0.{u, u_1} A).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) (shortComplexH0.{u, u_1} A).f :
          (a : (↑(shortComplexH0 A).X₁ : Type (max u u_1))) → (↑(shortComplexH0 A).X₂ : Type (max u u_1)))
        x₁ =
      x
Tactic: (hx : d₀₁ _ x = 0)
-- 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 : (↑A : Type (max u u_1))
hx :
  Eq (α := (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u_1 u)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type (max u_1 u)) →ₗ[k] (↑x2 : Type (max u_1 u)))
            (CC := ModuleCat.carrier) (d₀₁.{u, u_1} A) :
          (a : (↑(ModuleCat.of k (↑A : Type (max u u_1))) : Type (max u_1 u))) →
            (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u_1 u)))
        x :
      (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u_1 u)))
    (0 : (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u_1 u)))
⊢ ∃ (x₁ : (↑(shortComplexH0.{u, u_1} A).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) (shortComplexH0.{u, u_1} A).f :
          (a : (↑(shortComplexH0 A).X₁ : Type (max u u_1))) → (↑(shortComplexH0 A).X₂ : Type (max u u_1)))
        x₁ =
      x
have refine : ∀ (g : G),
  (((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 =
    x
Tactic: refine ⟨⟨x, fun g => ?_⟩, rfl⟩