awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90
Goal:
K L : Type
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
inst_4 : IsGalois K L
inst_5 : IsCyclic Gal(L/K)
g : Gal(L/K)
A : Type u_1
B : Type u_2
inst_6 : CommRing A
inst_7 : CommRing B
inst_8 : Algebra A B
inst_9 : Algebra A L
inst_10 : Algebra A K
inst_11 : Algebra B L
inst_12 : IsScalarTower A B L
inst_13 : IsScalarTower A K L
inst_14 : IsFractionRing A K
inst_15 : IsDomain A
inst_16 : IsIntegralClosure B A L
hg : ∀ (x : Gal(L/K)), Membership.mem (γ := Subgroup Gal(L/K)) (Subgroup.zpowers g) x
η : B
hη : Eq (α := K) ((Algebra.norm K : (a : L) → K) ((algebraMap B L : (a : B) → L) η : L) : K) (1 : K)
this_1 : Module.IsTorsionFree A L
this_2 : IsLocalization (Algebra.algebraMapSubmonoid.{u_1, u_2} (R := A) B A⁰) L
η' : Lˣ := Units.mk0 ((algebraMap B L : (a : B) → L) η) ⋯
ε : Lˣ
a : B
b : ↥(Algebra.algebraMapSubmonoid.{u_1, u_2} (R := A) B A⁰)
h : IsLocalization.mk' L a b = (↑ε : L)
t : A
ht : t ∈ (↑(A⁰ : Submonoid A) : Set A)
ht' : (algebraMap A B : (a : A) → B) t = (↑b : B)
this : t • IsLocalization.mk' L a b = (algebraMap B L : (a : B) → L) a
hε :
  HMul.hMul (α := L) (β := L) ((algebraMap B L : (a : B) → L) η : L)
      (((↑g : L →ₐ[K] L) : (a : L) → L) ((algebraMap B L : (a : B) → L) a : L) : L) =
    (algebraMap B L : (a : B) → L) a
refine_2 :
  Eq (α := L)
    ((algebraMap B L : (a : B) → L)
        ((((galRestrict A K L B : (a : Gal(L/K)) → B ≃ₐ[A] B) g : B ≃ₐ[A] B) : (a : B) → B) a : B) :
      L)
    (((↑g : L →ₐ[K] L) : (a : L) → L) ((algebraMap B L : (a : B) → L) a : L) : L)
⊢ HMul.hMul (α := L) (β := L) ((algebraMap B L : (a : B) → L) η : L)
      ((algebraMap B L : (a : B) → L)
          ((((galRestrict A K L B : (a : Gal(L/K)) → B ≃ₐ[A] B) g : B ≃ₐ[A] B) : (a : B) → B) a : B) :
        L) =
    HMul.hMul (α := L) (β := L) ((algebraMap B L : (a : B) → L) η : L)
      (((↑g : L →ₐ[K] L) : (a : L) → L) ((algebraMap B L : (a : B) → L) a : L) : L)

Tactic:
congr 1
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90
Goal:
K L : Type
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
inst_4 : IsGalois K L
inst_5 : IsCyclic Gal(L/K)
g : Gal(L/K)
A : Type u_1
B : Type u_2
inst_6 : CommRing A
inst_7 : CommRing B
inst_8 : Algebra A B
inst_9 : Algebra A L
inst_10 : Algebra A K
inst_11 : Algebra B L
inst_12 : IsScalarTower A B L
inst_13 : IsScalarTower A K L
inst_14 : IsFractionRing A K
inst_15 : IsDomain A
inst_16 : IsIntegralClosure B A L
hg : ∀ (x : Gal(L/K)), Membership.mem (γ := Subgroup Gal(L/K)) (Subgroup.zpowers g) x
η : B
hη : Eq (α := K) ((Algebra.norm K : (a : L) → K) ((algebraMap B L : (a : B) → L) η : L) : K) (1 : K)
this_1 : Module.IsTorsionFree A L
this_2 : IsLocalization (Algebra.algebraMapSubmonoid.{u_1, u_2} (R := A) B A⁰) L
η' : Lˣ := Units.mk0 ((algebraMap B L : (a : B) → L) η) ⋯
ε : Lˣ
a : B
b : ↥(Algebra.algebraMapSubmonoid.{u_1, u_2} (R := A) B A⁰)
h : IsLocalization.mk' L a b = (↑ε : L)
t : A
ht : t ∈ (↑(A⁰ : Submonoid A) : Set A)
ht' : (algebraMap A B : (a : A) → B) t = (↑b : B)
this : t • IsLocalization.mk' L a b = (algebraMap B L : (a : B) → L) a
hε :
  HMul.hMul (α := L) (β := L) ((algebraMap B L : (a : B) → L) η : L)
      (((↑g : L →ₐ[K] L) : (a : L) → L) ((algebraMap B L : (a : B) → L) a : L) : L) =
    (algebraMap B L : (a : B) → L) a
⊢ Eq (α := L)
    ((algebraMap B L : (a : B) → L)
        ((((galRestrict A K L B : (a : Gal(L/K)) → B ≃ₐ[A] B) g : B ≃ₐ[A] B) : (a : B) → B) a : B) :
      L)
    (((↑g : L →ₐ[K] L) : (a : L) → L) ((algebraMap B L : (a : B) → L) a : L) : L)

Tactic:
algebraMap_galRestrictHom_apply A K L B g a

Premises used: AlgEquiv.toAlgHom, IsIntegralClosure.mk', Classical.choose, algebraMap_galRestrictHom_apply
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90
Goal:
K L : Type
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
inst_4 : IsGalois K L
inst_5 : IsCyclic Gal(L/K)
g : Gal(L/K)
A : Type u_1
B : Type u_2
inst_6 : CommRing A
inst_7 : CommRing B
inst_8 : Algebra A B
inst_9 : Algebra A L
inst_10 : Algebra A K
inst_11 : Algebra B L
inst_12 : IsScalarTower A B L
inst_13 : IsScalarTower A K L
inst_14 : IsFractionRing A K
inst_15 : IsDomain A
inst_16 : IsIntegralClosure B A L
hg : ∀ (x : Gal(L/K)), Membership.mem (γ := Subgroup Gal(L/K)) (Subgroup.zpowers g) x
η : B
hη : Eq (α := K) ((Algebra.norm K : (a : L) → K) ((algebraMap B L : (a : B) → L) η : L) : K) (1 : K)
this_1 : Module.IsTorsionFree A L
this_2 : IsLocalization (Algebra.algebraMapSubmonoid.{u_1, u_2} (R := A) B A⁰) L
η' : Lˣ := Units.mk0 ((algebraMap B L : (a : B) → L) η) ⋯
ε : Lˣ
a : B
b : ↥(Algebra.algebraMapSubmonoid.{u_1, u_2} (R := A) B A⁰)
h : IsLocalization.mk' L a b = (↑ε : L)
t : A
ht : t ∈ (↑(A⁰ : Submonoid A) : Set A)
ht' : (algebraMap A B : (a : A) → B) t = (↑b : B)
this : t • IsLocalization.mk' L a b = (algebraMap B L : (a : B) → L) a
hε :
  HMul.hMul (α := L) (β := L) ((algebraMap B L : (a : B) → L) η : L)
      (((↑g : L →ₐ[K] L) : (a : L) → L) ((algebraMap B L : (a : B) → L) a : L) : L) =
    (algebraMap B L : (a : B) → L) a
⊢ Eq (α := L)
    ((algebraMap B L : (a : B) → L)
        ((((galRestrict A K L B : (a : Gal(L/K)) → B ≃ₐ[A] B) g : B ≃ₐ[A] B) : (a : B) → B) a : B) :
      L)
    (((↑g : L →ₐ[K] L) : (a : L) → L) ((algebraMap B L : (a : B) → L) a : L) : L)

Tactic:
exact algebraMap_galRestrictHom_apply A K L B g a

Premises used: AlgEquiv.toAlgHom, algebraMap_galRestrictHom_apply
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90
Goal:
K L : Type
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
inst_4 : IsGalois K L
inst_5 : IsCyclic Gal(L/K)
g : Gal(L/K)
A : Type u_1
B : Type u_2
inst_6 : CommRing A
inst_7 : CommRing B
inst_8 : Algebra A B
inst_9 : Algebra A L
inst_10 : Algebra A K
inst_11 : Algebra B L
inst_12 : IsScalarTower A B L
inst_13 : IsScalarTower A K L
inst_14 : IsFractionRing A K
inst_15 : IsDomain A
inst_16 : IsIntegralClosure B A L
hg : ∀ (x : Gal(L/K)), Membership.mem (γ := Subgroup Gal(L/K)) (Subgroup.zpowers g) x
η : B
hη : Eq (α := K) ((Algebra.norm K : (a : L) → K) ((algebraMap B L : (a : B) → L) η : L) : K) (1 : K)
this_1 : Module.IsTorsionFree A L
this_2 : IsLocalization (Algebra.algebraMapSubmonoid.{u_1, u_2} (R := A) B A⁰) L
η' : Lˣ := Units.mk0 ((algebraMap B L : (a : B) → L) η) ⋯
ε : Lˣ
a : B
b : ↥(Algebra.algebraMapSubmonoid.{u_1, u_2} (R := A) B A⁰)
h : IsLocalization.mk' L a b = (↑ε : L)
t : A
ht : t ∈ (↑(A⁰ : Submonoid A) : Set A)
ht' : (algebraMap A B : (a : A) → B) t = (↑b : B)
this : t • IsLocalization.mk' L a b = (algebraMap B L : (a : B) → L) a
hε :
  (algebraMap B L : (a : B) → L) η =
    HDiv.hDiv (β := L) (IsLocalization.mk' L a b) ((g : (a : L) → L) (IsLocalization.mk' L a b) : L)
e : Eq (α := L) ((g : (a : L) → L) (IsLocalization.mk' L a b) : L) (0 : L)
⊢ Eq (α := L) ((algebraMap B L : (a : B) → L) η : L) (0 : L)

Tactic:
rw [(map_eq_zero _).mp e, zero_div] at hε

Premises used: zero_div, map_eq_zero, Iff.mp
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90
Goal:
K L : Type
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
inst_4 : IsGalois K L
inst_5 : IsCyclic Gal(L/K)
g : Gal(L/K)
A : Type u_1
B : Type u_2
inst_6 : CommRing A
inst_7 : CommRing B
inst_8 : Algebra A B
inst_9 : Algebra A L
inst_10 : Algebra A K
inst_11 : Algebra B L
inst_12 : IsScalarTower A B L
inst_13 : IsScalarTower A K L
inst_14 : IsFractionRing A K
inst_15 : IsDomain A
inst_16 : IsIntegralClosure B A L
hg : ∀ (x : Gal(L/K)), Membership.mem (γ := Subgroup Gal(L/K)) (Subgroup.zpowers g) x
η : B
hη : Eq (α := K) ((Algebra.norm K : (a : L) → K) ((algebraMap B L : (a : B) → L) η : L) : K) (1 : K)
this_1 : Module.IsTorsionFree A L
this_2 : IsLocalization (Algebra.algebraMapSubmonoid.{u_1, u_2} (R := A) B A⁰) L
η' : Lˣ := Units.mk0 ((algebraMap B L : (a : B) → L) η) ⋯
ε : Lˣ
a : B
b : ↥(Algebra.algebraMapSubmonoid.{u_1, u_2} (R := A) B A⁰)
h : IsLocalization.mk' L a b = (↑ε : L)
t : A
ht : t ∈ (↑(A⁰ : Submonoid A) : Set A)
ht' : (algebraMap A B : (a : A) → B) t = (↑b : B)
this : t • IsLocalization.mk' L a b = (algebraMap B L : (a : B) → L) a
hε :
  (algebraMap B L : (a : B) → L) η =
    HDiv.hDiv (β := L) (IsLocalization.mk' L a b) ((g : (a : L) → L) (IsLocalization.mk' L a b) : L)
e : Eq (α := L) ((g : (a : L) → L) (IsLocalization.mk' L a b) : L) (0 : L)
hε₁ : Eq (α := L) ((algebraMap B L : (a : B) → L) η : L) (0 : L)
⊢ Eq (α := L) ((g : (a : L) → L) (IsLocalization.mk' L a b) : L) (0 : L)

Tactic:
rw [(map_eq_zero _).mp e, zero_div] at hε

Premises used: zero_div, map_eq_zero, Iff.mp
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90
Goal:
K L : Type
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
inst_4 : IsGalois K L
inst_5 : IsCyclic Gal(L/K)
g : Gal(L/K)
A : Type u_1
B : Type u_2
inst_6 : CommRing A
inst_7 : CommRing B
inst_8 : Algebra A B
inst_9 : Algebra A L
inst_10 : Algebra A K
inst_11 : Algebra B L
inst_12 : IsScalarTower A B L
inst_13 : IsScalarTower A K L
inst_14 : IsFractionRing A K
inst_15 : IsDomain A
inst_16 : IsIntegralClosure B A L
hg : ∀ (x : Gal(L/K)), Membership.mem (γ := Subgroup Gal(L/K)) (Subgroup.zpowers g) x
η : B
hη : Eq (α := K) ((Algebra.norm K : (a : L) → K) ((algebraMap B L : (a : B) → L) η : L) : K) (1 : K)
this_1 : Module.IsTorsionFree A L
this_2 : IsLocalization (Algebra.algebraMapSubmonoid.{u_1, u_2} (R := A) B A⁰) L
η' : Lˣ := Units.mk0 ((algebraMap B L : (a : B) → L) η) ⋯
ε : Lˣ
a : B
b : ↥(Algebra.algebraMapSubmonoid.{u_1, u_2} (R := A) B A⁰)
h : IsLocalization.mk' L a b = (↑ε : L)
t : A
ht : t ∈ (↑(A⁰ : Submonoid A) : Set A)
ht' : (algebraMap A B : (a : A) → B) t = (↑b : B)
this : t • IsLocalization.mk' L a b = (algebraMap B L : (a : B) → L) a
hε : Eq (α := L) ((algebraMap B L : (a : B) → L) η : L) (0 : L)
e : Eq (α := L) ((g : (a : L) → L) (IsLocalization.mk' L a b) : L) (0 : L)
refine_2 :
  ∀ (hη : Eq (α := K) 0 1) (this : Module.IsTorsionFree A L)
    (this : IsLocalization (Algebra.algebraMapSubmonoid.{u_1, u_2} (R := A) B A⁰) L) (ε : Lˣ) (a : B)
    (b : ↥(Algebra.algebraMapSubmonoid.{u_1, u_2} (R := A) B A⁰)) (h : IsLocalization.mk' L a b = (↑ε : L)) (t : A)
    (ht : t ∈ (↑(A⁰ : Submonoid A) : Set A)) (ht' : (algebraMap A B : (a : A) → B) t = (↑b : B))
    (this_3 : t • IsLocalization.mk' L a b = (algebraMap B L : (a : B) → L) a)
    (hε : Eq (α := L) ((algebraMap B L : (a : B) → L) η : L) (0 : L))
    (e : Eq (α := L) ((g : (a : L) → L) (IsLocalization.mk' L a b) : L) (0 : L)), False
⊢ False

Tactic:
rw [hε, Algebra.norm_zero] at hη

Premises used: Algebra.norm_zero
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90
Goal:
K L : Type
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
inst_4 : IsGalois K L
inst_5 : IsCyclic Gal(L/K)
g : Gal(L/K)
A : Type u_1
B : Type u_2
inst_6 : CommRing A
inst_7 : CommRing B
inst_8 : Algebra A B
inst_9 : Algebra A L
inst_10 : Algebra A K
inst_11 : Algebra B L
inst_12 : IsScalarTower A B L
inst_13 : IsScalarTower A K L
inst_14 : IsFractionRing A K
inst_15 : IsDomain A
inst_16 : IsIntegralClosure B A L
hg : ∀ (x : Gal(L/K)), Membership.mem (γ := Subgroup Gal(L/K)) (Subgroup.zpowers g) x
η : B
hη_1 : Eq (α := K) ((Algebra.norm K : (a : L) → K) ((algebraMap B L : (a : B) → L) η : L) : K) (1 : K)
hη : Eq (α := K) 0 1
this_1 : Module.IsTorsionFree A L
this_2 : IsLocalization (Algebra.algebraMapSubmonoid.{u_1, u_2} (R := A) B A⁰) L
η' : Lˣ := Units.mk0 ((algebraMap B L : (a : B) → L) η) ⋯
ε : Lˣ
a : B
b : ↥(Algebra.algebraMapSubmonoid.{u_1, u_2} (R := A) B A⁰)
h : IsLocalization.mk' L a b = (↑ε : L)
t : A
ht : t ∈ (↑(A⁰ : Submonoid A) : Set A)
ht' : (algebraMap A B : (a : A) → B) t = (↑b : B)
this : t • IsLocalization.mk' L a b = (algebraMap B L : (a : B) → L) a
hε : Eq (α := L) ((algebraMap B L : (a : B) → L) η : L) (0 : L)
e : Eq (α := L) ((g : (a : L) → L) (IsLocalization.mk' L a b) : L) (0 : L)
⊢ False

Tactic:
zero_ne_one hη

Premises used: zero_ne_one
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90
Goal:
K L : Type
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
inst_4 : IsGalois K L
inst_5 : IsCyclic Gal(L/K)
g : Gal(L/K)
A : Type u_1
B : Type u_2
inst_6 : CommRing A
inst_7 : CommRing B
inst_8 : Algebra A B
inst_9 : Algebra A L
inst_10 : Algebra A K
inst_11 : Algebra B L
inst_12 : IsScalarTower A B L
inst_13 : IsScalarTower A K L
inst_14 : IsFractionRing A K
inst_15 : IsDomain A
inst_16 : IsIntegralClosure B A L
hg : ∀ (x : Gal(L/K)), Membership.mem (γ := Subgroup Gal(L/K)) (Subgroup.zpowers g) x
η : B
hη_1 : Eq (α := K) ((Algebra.norm K : (a : L) → K) ((algebraMap B L : (a : B) → L) η : L) : K) (1 : K)
hη : Eq (α := K) 0 1
this_1 : Module.IsTorsionFree A L
this_2 : IsLocalization (Algebra.algebraMapSubmonoid.{u_1, u_2} (R := A) B A⁰) L
η' : Lˣ := Units.mk0 ((algebraMap B L : (a : B) → L) η) ⋯
ε : Lˣ
a : B
b : ↥(Algebra.algebraMapSubmonoid.{u_1, u_2} (R := A) B A⁰)
h : IsLocalization.mk' L a b = (↑ε : L)
t : A
ht : t ∈ (↑(A⁰ : Submonoid A) : Set A)
ht' : (algebraMap A B : (a : A) → B) t = (↑b : B)
this : t • IsLocalization.mk' L a b = (algebraMap B L : (a : B) → L) a
hε : Eq (α := L) ((algebraMap B L : (a : B) → L) η : L) (0 : L)
e : Eq (α := L) ((g : (a : L) → L) (IsLocalization.mk' L a b) : L) (0 : L)
⊢ False

Tactic:
exact zero_ne_one hη

Premises used: zero_ne_one
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
i : ℕ
⊢ (Rep.Hom.hom X.f).range = (Rep.Hom.hom X.g).ker

Tactic:
have : LinearMap.range X.f.hom.toLinearMap = LinearMap.ker X.g.hom.toLinearMap :=
        (hX.exact.map (forget₂ (Rep k G) (ModuleCat k))).moduleCat_range_eq_ker
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
i : ℕ
this : (Rep.Hom.hom X.f).range = (Rep.Hom.hom X.g).ker
⊢ Exact (ShortComplex.map (X.map (cochainsFunctor k G)) (HomologicalComplex.eval (ModuleCat k) (ComplexShape.up ℕ) i))

Tactic:
simp [moduleCat_exact_iff_range_eq_ker, LinearMap.range_compLeft,
        LinearMap.ker_compLeft, this]

Premises used: LinearMap.ker_compLeft, CategoryTheory.ShortComplex.moduleCat_exact_iff_range_eq_ker, LinearMap.range_compLeft
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
i j : ℕ
hij : i + 1 = j
⊢ (mapShortComplex₁ hX hij).Exact

Tactic:
(map_cochainsFunctor_shortExact hX).homology_exact₁ i j hij

Premises used: CategoryTheory.ShortComplex.leftHomologyMap', CategoryTheory.ShortComplex.SnakeInput.L₂', CategoryTheory.ShortComplex.homology, CategoryTheory.ShortComplex.homologyMap', HomologicalComplex.homologyMap, CategoryTheory.ShortComplex.LeftHomologyData.descH, groupCohomology.map_cochainsFunctor_shortExact, CategoryTheory.ShortComplex.ShortExact.homology_exact₁, HomologicalComplex.homology, CategoryTheory.ShortComplex.ShortExact.δ, CategoryTheory.ShortComplex.homologyMap
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
i : ℕ
⊢ (mapShortComplex₂ X i).Exact

Tactic:
(map_cochainsFunctor_shortExact hX).homology_exact₂ i

Premises used: groupCohomology, CategoryTheory.ShortComplex.leftHomologyMap', CategoryTheory.ShortComplex.homology, CategoryTheory.ShortComplex.homologyMap', HomologicalComplex.homologyMap, CategoryTheory.ShortComplex.map, CategoryTheory.ShortComplex.LeftHomologyData.descH, groupCohomology.map_cochainsFunctor_shortExact, HomologicalComplex.homology, CategoryTheory.ShortComplex.homologyMap, CategoryTheory.ShortComplex.ShortExact.homology_exact₂
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
i j : ℕ
hij : i + 1 = j
⊢ (mapShortComplex₃ hX hij).Exact

Tactic:
(map_cochainsFunctor_shortExact hX).homology_exact₃ i j hij

Premises used: CategoryTheory.ShortComplex.leftHomologyMap', CategoryTheory.ShortComplex.homology, CategoryTheory.ShortComplex.homologyMap', CategoryTheory.ShortComplex.ShortExact.homology_exact₃, CategoryTheory.ShortComplex.SnakeInput.L₁', HomologicalComplex.homologyMap, CategoryTheory.ShortComplex.LeftHomologyData.descH, groupCohomology.map_cochainsFunctor_shortExact, HomologicalComplex.homology, CategoryTheory.ShortComplex.ShortExact.δ, CategoryTheory.ShortComplex.homologyMap
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
n : ℕ
h : IsZero (groupCohomology X.X₂ (n + 1))
⊢ Epi (δ hX n (n + 1) ⋯)

Tactic:
SnakeInput.epi_δ _ h

Premises used: groupCohomology, CategoryTheory.ShortComplex.homology, CategoryTheory.ShortComplex.SnakeInput.epi_δ, HomologicalComplex.homology, CategoryTheory.ShortComplex.ShortExact.δ
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
n : ℕ
h : IsZero (groupCohomology X.X₂ n)
⊢ Mono (δ hX n (n + 1) ⋯)

Tactic:
SnakeInput.mono_δ _ h

Premises used: groupCohomology, CategoryTheory.ShortComplex.SnakeInput.mono_δ, CategoryTheory.ShortComplex.homology, HomologicalComplex.homology, CategoryTheory.ShortComplex.ShortExact.δ
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
n : ℕ
h : IsZero (groupCohomology X.X₂ n)
hs : IsZero (groupCohomology X.X₂ (n + 1))
⊢ IsIso (δ hX n (n + 1) ⋯)

Tactic:
SnakeInput.isIso_δ _ h hs

Premises used: groupCohomology, CategoryTheory.ShortComplex.SnakeInput.isIso_δ, CategoryTheory.ShortComplex.homology, HomologicalComplex.homology, CategoryTheory.ShortComplex.ShortExact.δ
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
i j : ℕ
y : (Fin i → G) → (↑X.X₂ : Type u)
x : (Fin j → G) → (↑X.X₁ : Type u)
hx :
  Eq (α := (Fin j → G) → (↑X.X₂ : Type u)) ((⇑(Rep.Hom.hom X.f) : (a : (↑X.X₁ : Type u)) → (↑X.X₂ : Type u)) ∘ x)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) ((inhomogeneousCochains X.X₂).d i j) :
        (a : (↑((inhomogeneousCochains X.X₂).X i) : Type u)) → (↑((inhomogeneousCochains X.X₂).X j) : Type u))
      y)
⊢ Eq (α := (↑(ModuleCat.of k ((Fin (j + 1) → G) → (↑X.X₁ : Type u))) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (inhomogeneousCochains.d X.X₁ j) :
          (a : (↑(ModuleCat.of k ((Fin j → G) → (↑X.X₁ : Type u))) : Type u)) →
            (↑(ModuleCat.of k ((Fin (j + 1) → G) → (↑X.X₁ : Type u))) : Type u))
        x :
      (↑(ModuleCat.of k ((Fin (j + 1) → G) → (↑X.X₁ : Type u))) : Type u))
    (0 : (↑(ModuleCat.of k ((Fin (j + 1) → G) → (↑X.X₁ : Type u))) : Type u))

Tactic:
simpa [CochainComplex.of.d] using
    ((map_cochainsFunctor_shortExact hX).d_eq_zero_of_f_eq_d_apply i j y x
      (by simpa using hx) (j + 1))

Premises used: CategoryTheory.ShortComplex.ShortExact.d_eq_zero_of_f_eq_d_apply, CochainComplex.of.d, HAdd.hAdd, groupCohomology.map_cochainsFunctor_shortExact, OfNat.ofNat
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
i : ℕ
z : (Fin i → G) → (↑X.X₃ : Type u)
y : (Fin i → G) → (↑X.X₂ : Type u)
hy :
  (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (X := HomologicalComplex.X (inhomogeneousCochains (G := G) X.2) i) (Y :=
          (inhomogeneousCochains X.X₃).X i) (HomologicalComplex.Hom.f (cochainsMap (MonoidHom.id G) X.g) i) :
        (a : (↑((inhomogeneousCochains X.2).X i) : Type u)) → (↑((inhomogeneousCochains X.X₃).X i) : Type u))
      y =
    z
hz :
  Eq (α := (↑((inhomogeneousCochains X.X₃).X (i + 1)) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (Y := (inhomogeneousCochains X.X₃).X (i + 1))
            ((inhomogeneousCochains X.X₃).d i (i + 1)) :
          (a : (↑((inhomogeneousCochains X.X₃).X i) : Type u)) → (↑((inhomogeneousCochains X.X₃).X (i + 1)) : Type u))
        z :
      (↑((inhomogeneousCochains X.X₃).X (i + 1)) : Type u))
    (0 : (↑((inhomogeneousCochains X.X₃).X (i + 1)) : Type u))
x : (Fin (i + 1) → G) → (↑X.X₁ : Type u)
hx :
  Eq (α := (Fin (i + 1) → G) → (↑X.X₂ : Type u)) ((⇑(Rep.Hom.hom X.f) : (a : (↑X.X₁ : Type u)) → (↑X.X₂ : Type u)) ∘ x)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (Y := (inhomogeneousCochains X.X₂).X (i + 1)) ((inhomogeneousCochains X.X₂).d i (i + 1)) :
        (a : (↑((inhomogeneousCochains X.X₂).X i) : Type u)) → (↑((inhomogeneousCochains X.X₂).X (i + 1)) : Type u))
      y)
⊢ Eq (α := (↑(ModuleCat.of k ((Fin (i + 1) → G) → (↑X.X₃ : Type u))) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (inhomogeneousCochains.d X.X₃ i) :
          (a : (↑(ModuleCat.of k ((Fin i → G) → (↑X.X₃ : Type u))) : Type u)) →
            (↑(ModuleCat.of k ((Fin (i + 1) → G) → (↑X.X₃ : Type u))) : Type u))
        z :
      (↑(ModuleCat.of k ((Fin (i + 1) → G) → (↑X.X₃ : Type u))) : Type u))
    (0 : (↑(ModuleCat.of k ((Fin (i + 1) → G) → (↑X.X₃ : Type u))) : Type u))

Tactic:
simpa [CochainComplex.of.d] using hz

Premises used: CochainComplex.of.d
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
i j : ℕ
hij : i + 1 = j
z : (Fin i → G) → (↑X.X₃ : Type u)
hz :
  Eq (α := (↑((inhomogeneousCochains X.X₃).X j) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) ((inhomogeneousCochains X.X₃).d i j) :
          (a : (↑((inhomogeneousCochains X.X₃).X i) : Type u)) → (↑((inhomogeneousCochains X.X₃).X j) : Type u))
        z :
      (↑((inhomogeneousCochains X.X₃).X j) : Type u))
    (0 : (↑((inhomogeneousCochains X.X₃).X j) : Type u))
y : (Fin i → G) → (↑X.X₂ : Type u)
hy :
  (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (X := HomologicalComplex.X (inhomogeneousCochains (G := G) X.2) i) (Y :=
          (inhomogeneousCochains X.X₃).X i) (HomologicalComplex.Hom.f (cochainsMap (MonoidHom.id G) X.g) i) :
        (a : (↑((inhomogeneousCochains X.2).X i) : Type u)) → (↑((inhomogeneousCochains X.X₃).X i) : Type u))
      y =
    z
x : (Fin j → G) → (↑X.X₁ : Type u)
hx :
  Eq (α := (Fin j → G) → (↑X.X₂ : Type u)) ((⇑(Rep.Hom.hom X.f) : (a : (↑X.X₁ : Type u)) → (↑X.X₂ : Type u)) ∘ x)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) ((inhomogeneousCochains X.X₂).d i j) :
        (a : (↑((inhomogeneousCochains X.X₂).X i) : Type u)) → (↑((inhomogeneousCochains X.X₂).X j) : Type u))
      y)
⊢ (ComplexShape.up ℕ).next j = j + 1

Tactic:
simp