mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90

Goal state before:
pp: case refine_2
K L : Type
inst✝¹⁶ : Field K
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra K L
inst✝¹³ : FiniteDimensional K L
inst✝¹² : IsGalois K L
inst✝¹¹ : IsCyclic Gal(L/K)
g : Gal(L/K)
A : Type u_1
B : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra A L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsScalarTower A K L
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : IsIntegralClosure B A L
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
η : B
hη : (Algebra.norm K) ((algebraMap B L) η) = 1
this✝¹ : Module.IsTorsionFree A L
this✝ : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
η' : Lˣ := Units.mk0 ((algebraMap B L) η) ⋯
ε : Lˣ
a : B
b : ↥(Algebra.algebraMapSubmonoid B A⁰)
h : IsLocalization.mk' L a b = ↑ε
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑b
this : t • IsLocalization.mk' L a b = (algebraMap B L) a
hε : (algebraMap B L) η = IsLocalization.mk' L a b / g (IsLocalization.mk' L a b)
e : g (IsLocalization.mk' L a b) = 0
⊢ False

Tactic:
(map_eq_zero _).mp e,

Goal state after:
case refine_2
K L : Type
inst✝¹⁶ : Field K
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra K L
inst✝¹³ : FiniteDimensional K L
inst✝¹² : IsGalois K L
inst✝¹¹ : IsCyclic Gal(L/K)
g : Gal(L/K)
A : Type u_1
B : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra A L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsScalarTower A K L
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : IsIntegralClosure B A L
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
η : B
hη : (Algebra.norm K) ((algebraMap B L) η) = 1
this✝¹ : Module.IsTorsionFree A L
this✝ : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
η' : Lˣ := Units.mk0 ((algebraMap B L) η) ⋯
ε : Lˣ
a : B
b : ↥(Algebra.algebraMapSubmonoid B A⁰)
h : IsLocalization.mk' L a b = ↑ε
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑b
this : t • IsLocalization.mk' L a b = (algebraMap B L) a
hε : (algebraMap B L) η = 0 / g 0
e : g (IsLocalization.mk' L a b) = 0
⊢ False
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Basic

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
n : ℕ
g : Fin (n + 1) → G
a : ↑A
⊢ (ConcreteCategory.hom (d A n)) (single g a) =
    single (fun i ↦ g i.succ) ((A.ρ (g 0)⁻¹) a) +
      ∑ j, (-1) ^ (↑j + 1) • single (j.contractNth (fun x1 x2 ↦ x1 * x2) g) a

Tactic:
simp [d]

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Basic

Goal state before:
pp: case refine_1
k✝ G✝ : Type u
inst✝⁴ : CommRing k✝
inst✝³ : Group G✝
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
n : ℕ
inst✝ : DecidableEq G
⊢ (i : ℕ) → (inhomogeneousChains A).X i ≅ (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).X i

pp: case refine_2
k✝ G✝ : Type u
inst✝⁴ : CommRing k✝
inst✝³ : Group G✝
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
n : ℕ
inst✝ : DecidableEq G
⊢ ∀ (i j : ℕ),
    (ComplexShape.down ℕ).Rel i j →
      Iso.hom (?refine_1 i) ≫ (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d i j =
        (inhomogeneousChains A).d i j ≫ Iso.hom (?refine_1 j)

Tactic:
·

Goal state after:
case refine_1
k✝ G✝ : Type u
inst✝⁴ : CommRing k✝
inst✝³ : Group G✝
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
n : ℕ
inst✝ : DecidableEq G
⊢ (i : ℕ) → (inhomogeneousChains A).X i ≅ (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).X i
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : ↥(cocycles₁ A)
g : G
⊢ (A.ρ g) (f g⁻¹) + f g = f (g * g⁻¹)

Tactic:
(mem_cocycles₁_iff f).1 f.2 g g⁻¹

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : ↥(cocycles₁ A)
g : G
⊢ (A.ρ g) (f g⁻¹) + f g = (A.ρ g) (f g⁻¹) + f g
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic

Goal state before:
pp: case pos
k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A : Rep k G
g✝ : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g✝
j : ℕ
a : ↑A
g : G
hj : Even (j + 1)
⊢ (((A.coinvariantsTensorMk ((resolution k g✝⁻¹ ⋯).complex.X (j + 1))).compr₂
            (ModuleCat.Hom.hom
              (A.ρ.coinvariantsTprodLeftRegularLEquiv.toModuleIso.hom ≫ (moduleCatChainComplex A g✝).d (j + 1) j)))
          a ∘ₗ
        MonoidAlgebra.lsingle g)
      1 =
    (((A.coinvariantsTensorMk ((resolution k g✝⁻¹ ⋯).complex.X (j + 1))).compr₂
            (ModuleCat.Hom.hom
              ((HomologicalComplex.coinvariantsTensorObj A (resolution k g✝⁻¹ ⋯).complex).d (j + 1) j ≫
                A.ρ.coinvariantsTprodLeftRegularLEquiv.toModuleIso.hom)))
          a ∘ₗ
        MonoidAlgebra.lsingle g)
      1

pp: case neg
k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A : Rep k G
g✝ : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g✝
j : ℕ
a : ↑A
g : G
hj : ¬Even (j + 1)
⊢ (((A.coinvariantsTensorMk ((resolution k g✝⁻¹ ⋯).complex.X (j + 1))).compr₂
            (ModuleCat.Hom.hom
              (A.ρ.coinvariantsTprodLeftRegularLEquiv.toModuleIso.hom ≫ (moduleCatChainComplex A g✝).d (j + 1) j)))
          a ∘ₗ
        MonoidAlgebra.lsingle g)
      1 =
    (((A.coinvariantsTensorMk ((resolution k g✝⁻¹ ⋯).complex.X (j + 1))).compr₂
            (ModuleCat.Hom.hom
              ((HomologicalComplex.coinvariantsTensorObj A (resolution k g✝⁻¹ ⋯).complex).d (j + 1) j ≫
                A.ρ.coinvariantsTprodLeftRegularLEquiv.toModuleIso.hom)))
          a ∘ₗ
        MonoidAlgebra.lsingle g)
      1

Tactic:
·

Goal state after:
case pos
k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A : Rep k G
g✝ : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g✝
j : ℕ
a : ↑A
g : G
hj : Even (j + 1)
⊢ (((A.coinvariantsTensorMk ((resolution k g✝⁻¹ ⋯).complex.X (j + 1))).compr₂
            (ModuleCat.Hom.hom
              (A.ρ.coinvariantsTprodLeftRegularLEquiv.toModuleIso.hom ≫ (moduleCatChainComplex A g✝).d (j + 1) j)))
          a ∘ₗ
        MonoidAlgebra.lsingle g)
      1 =
    (((A.coinvariantsTensorMk ((resolution k g✝⁻¹ ⋯).complex.X (j + 1))).compr₂
            (ModuleCat.Hom.hom
              ((HomologicalComplex.coinvariantsTensorObj A (resolution k g✝⁻¹ ⋯).complex).d (j + 1) j ≫
                A.ρ.coinvariantsTprodLeftRegularLEquiv.toModuleIso.hom)))
          a ∘ₗ
        MonoidAlgebra.lsingle g)
      1
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic

Goal state before:
pp: case neg
k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A : Rep k G
g✝ : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g✝
j : ℕ
a : ↑A
g : G
hj : ¬Even (j + 1)
⊢ (((A.coinvariantsTensorMk ((resolution k g✝⁻¹ ⋯).complex.X (j + 1))).compr₂
            (ModuleCat.Hom.hom
              (A.ρ.coinvariantsTprodLeftRegularLEquiv.toModuleIso.hom ≫ (moduleCatChainComplex A g✝).d (j + 1) j)))
          a ∘ₗ
        MonoidAlgebra.lsingle g)
      1 =
    (((A.coinvariantsTensorMk ((resolution k g✝⁻¹ ⋯).complex.X (j + 1))).compr₂
            (ModuleCat.Hom.hom
              ((HomologicalComplex.coinvariantsTensorObj A (resolution k g✝⁻¹ ⋯).complex).d (j + 1) j ≫
                A.ρ.coinvariantsTprodLeftRegularLEquiv.toModuleIso.hom)))
          a ∘ₗ
        MonoidAlgebra.lsingle g)
      1

Tactic:
·

Goal state after:
case neg
k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A : Rep k G
g✝ : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g✝
j : ℕ
a : ↑A
g : G
hj : ¬Even (j + 1)
⊢ (((A.coinvariantsTensorMk ((resolution k g✝⁻¹ ⋯).complex.X (j + 1))).compr₂
            (ModuleCat.Hom.hom
              (A.ρ.coinvariantsTprodLeftRegularLEquiv.toModuleIso.hom ≫ (moduleCatChainComplex A g✝).d (j + 1) j)))
          a ∘ₗ
        MonoidAlgebra.lsingle g)
      1 =
    (((A.coinvariantsTensorMk ((resolution k g✝⁻¹ ⋯).complex.X (j + 1))).compr₂
            (ModuleCat.Hom.hom
              ((HomologicalComplex.coinvariantsTensorObj A (resolution k g✝⁻¹ ⋯).complex).d (j + 1) j ≫
                A.ρ.coinvariantsTprodLeftRegularLEquiv.toModuleIso.hom)))
          a ∘ₗ
        MonoidAlgebra.lsingle g)
      1
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic

Goal state before:
pp: k G : Type u
inst✝³ : CommRing k
inst✝² : CommGroup G
inst✝¹ : Fintype G
A : Rep k G
g : G
inst✝ : DecidableEq G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
i : ℕ
h₀ : NeZero i
hi : Even i
⊢ ModuleCat.ofHom (Hom.hom A.norm).toLinearMap ≫ ModuleCat.ofHom (Hom.hom (A.applyAsHom g - 𝟙 A)).toLinearMap = 0

Tactic:
ext; simp [sub_hom,
    Rep.applyAsHom, Rep.norm]

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic

Goal state before:
pp: k G : Type u
inst✝³ : CommRing k
inst✝² : CommGroup G
inst✝¹ : Fintype G
A : Rep k G
g : G
inst✝ : DecidableEq G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
i : ℕ
hi : Odd i
⊢ ModuleCat.ofHom (Hom.hom A.norm).toLinearMap ≫ ModuleCat.ofHom (Hom.hom (A.applyAsHom g - 𝟙 A)).toLinearMap = 0

Tactic:
ext; simp [sub_hom,
    Rep.applyAsHom, Rep.norm]

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic

Goal state before:
pp: k G : Type u
inst✝³ : CommRing k
inst✝² : CommGroup G
inst✝¹ : Fintype G
A : Rep k G
g : G
inst✝ : DecidableEq G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
i : ℕ
hi : Odd i
⊢ (ComplexShape.down ℕ).Rel i ((ComplexShape.down ℕ).next i)

Tactic:
by rcases hi with ⟨j, rfl⟩; simp

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.TateCohomology.Basic

Goal state before:
pp: case ofNat
R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
X Y : Rep R G
f g : X ⟶ Y
i : ℕ
⊢ (map (f + g)).f (Int.ofNat i) = (map f + map g).f (Int.ofNat i)

pp: case negSucc
R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
X Y : Rep R G
f g : X ⟶ Y
i : ℕ
⊢ (map (f + g)).f (Int.negSucc i) = (map f + map g).f (Int.negSucc i)

Tactic:
·

Goal state after:
case ofNat
R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
X Y : Rep R G
f g : X ⟶ Y
i : ℕ
⊢ (map (f + g)).f (Int.ofNat i) = (map f + map g).f (Int.ofNat i)
Module: Mathlib.RepresentationTheory.Homological.TateCohomology.Basic

Goal state before:
pp: case negSucc
R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
X Y : Rep R G
f g : X ⟶ Y
i : ℕ
⊢ (map (f + g)).f (Int.negSucc i) = (map f + map g).f (Int.negSucc i)

Tactic:
·

Goal state after:
case negSucc
R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
X Y : Rep R G
f g : X ⟶ Y
i : ℕ
⊢ (map (f + g)).f (Int.negSucc i) = (map f + map g).f (Int.negSucc i)
Module: Mathlib.RepresentationTheory.Homological.TateCohomology.Basic

Goal state before:
pp: case ofNat
R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
S : ShortComplex (Rep R G)
hS : S.ShortExact
a✝ : ℕ
⊢ (S.map (tateComplexFunctor R G ⋙ HomologicalComplex.eval (ModuleCat R) (ComplexShape.up ℤ) (Int.ofNat a✝))).ShortExact

pp: case negSucc
R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
S : ShortComplex (Rep R G)
hS : S.ShortExact
a✝ : ℕ
⊢ (S.map
      (tateComplexFunctor R G ⋙ HomologicalComplex.eval (ModuleCat R) (ComplexShape.up ℤ) (Int.negSucc a✝))).ShortExact

Tactic:
·

Goal state after:
case ofNat
R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
S : ShortComplex (Rep R G)
hS : S.ShortExact
a✝ : ℕ
⊢ (S.map (tateComplexFunctor R G ⋙ HomologicalComplex.eval (ModuleCat R) (ComplexShape.up ℤ) (Int.ofNat a✝))).ShortExact
Module: Mathlib.RepresentationTheory.Homological.TateCohomology.Basic

Goal state before:
pp: case negSucc
R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
S : ShortComplex (Rep R G)
hS : S.ShortExact
a✝ : ℕ
⊢ (S.map
      (tateComplexFunctor R G ⋙ HomologicalComplex.eval (ModuleCat R) (ComplexShape.up ℤ) (Int.negSucc a✝))).ShortExact

Tactic:
·

Goal state after:
case negSucc
R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
S : ShortComplex (Rep R G)
hS : S.ShortExact
a✝ : ℕ
⊢ (S.map
      (tateComplexFunctor R G ⋙ HomologicalComplex.eval (ModuleCat R) (ComplexShape.up ℤ) (Int.negSucc a✝))).ShortExact
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

Goal state before:
pp: case h.refine_2
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↥(cocycles₁ A)
hx :
  (ConcreteCategory.hom (H1π (res S.subtype A)))
      ((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x) =
    0
y : ↑A
hy :
  (ModuleCat.Hom.hom (d₀₁ (res S.subtype A))) y =
    ⇑((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x)
h1 : ∀ (g h : G), x (g * h) = (A.ρ g) (x h) + x g
h2 : ∀ s ∈ S, x s = (A.ρ s) y - y
g : G ⧸ S
⊢ ∀ (a b : G), (QuotientGroup.leftRel S) a b → ⟨↑x a - (A.ρ a) y + y, ⋯⟩ = ⟨↑x b - (A.ρ b) y + y, ⋯⟩

pp: case h.refine_3
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↥(cocycles₁ A)
hx :
  (ConcreteCategory.hom (H1π (res S.subtype A)))
      ((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x) =
    0
y : ↑A
hy :
  (ModuleCat.Hom.hom (d₀₁ (res S.subtype A))) y =
    ⇑((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x)
h1 : ∀ (g h : G), x (g * h) = (A.ρ g) (x h) + x g
h2 : ∀ s ∈ S, x s = (A.ρ s) y - y
⊢ (fun g ↦ Quotient.liftOn' g (fun g ↦ ⟨↑x g - (A.ρ g) y + y, ⋯⟩) ⋯) ∈ cocycles₁ (A.quotientToInvariants S)

pp: case h.refine_4
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↥(cocycles₁ A)
hx :
  (ConcreteCategory.hom (H1π (res S.subtype A)))
      ((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x) =
    0
y : ↑A
hy :
  (ModuleCat.Hom.hom (d₀₁ (res S.subtype A))) y =
    ⇑((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x)
h1 : ∀ (g h : G), x (g * h) = (A.ρ g) (x h) + x g
h2 : ∀ s ∈ S, x s = (A.ρ s) y - y
⊢ (ModuleCat.Hom.hom (map (QuotientGroup.mk' S) (ofHom (A.ρ.quotientToInvariants_lift S)) 1))
      ((ConcreteCategory.hom (H1π (A.quotientToInvariants S)))
        ⟨fun g ↦ Quotient.liftOn' g (fun g ↦ ⟨↑x g - (A.ρ g) y + y, ⋯⟩) ⋯, ?h.refine_3⟩) =
    (ConcreteCategory.hom (H1π A)) x

Tactic:
·

Goal state after:
case h.refine_2
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↥(cocycles₁ A)
hx :
  (ConcreteCategory.hom (H1π (res S.subtype A)))
      ((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x) =
    0
y : ↑A
hy :
  (ModuleCat.Hom.hom (d₀₁ (res S.subtype A))) y =
    ⇑((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x)
h1 : ∀ (g h : G), x (g * h) = (A.ρ g) (x h) + x g
h2 : ∀ s ∈ S, x s = (A.ρ s) y - y
g : G ⧸ S
⊢ ∀ (a b : G), (QuotientGroup.leftRel S) a b → ⟨↑x a - (A.ρ a) y + y, ⋯⟩ = ⟨↑x b - (A.ρ b) y + y, ⋯⟩
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

Goal state before:
pp: case h.refine_3
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↥(cocycles₁ A)
hx :
  (ConcreteCategory.hom (H1π (res S.subtype A)))
      ((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x) =
    0
y : ↑A
hy :
  (ModuleCat.Hom.hom (d₀₁ (res S.subtype A))) y =
    ⇑((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x)
h1 : ∀ (g h : G), x (g * h) = (A.ρ g) (x h) + x g
h2 : ∀ s ∈ S, x s = (A.ρ s) y - y
⊢ (fun g ↦ Quotient.liftOn' g (fun g ↦ ⟨↑x g - (A.ρ g) y + y, ⋯⟩) ⋯) ∈ cocycles₁ (A.quotientToInvariants S)

pp: case h.refine_4
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↥(cocycles₁ A)
hx :
  (ConcreteCategory.hom (H1π (res S.subtype A)))
      ((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x) =
    0
y : ↑A
hy :
  (ModuleCat.Hom.hom (d₀₁ (res S.subtype A))) y =
    ⇑((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x)
h1 : ∀ (g h : G), x (g * h) = (A.ρ g) (x h) + x g
h2 : ∀ s ∈ S, x s = (A.ρ s) y - y
⊢ (ModuleCat.Hom.hom (map (QuotientGroup.mk' S) (ofHom (A.ρ.quotientToInvariants_lift S)) 1))
      ((ConcreteCategory.hom (H1π (A.quotientToInvariants S)))
        ⟨fun g ↦ Quotient.liftOn' g (fun g ↦ ⟨↑x g - (A.ρ g) y + y, ⋯⟩) ⋯, ?h.refine_3⟩) =
    (ConcreteCategory.hom (H1π A)) x

Tactic:
·

Goal state after:
case h.refine_3
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↥(cocycles₁ A)
hx :
  (ConcreteCategory.hom (H1π (res S.subtype A)))
      ((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x) =
    0
y : ↑A
hy :
  (ModuleCat.Hom.hom (d₀₁ (res S.subtype A))) y =
    ⇑((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x)
h1 : ∀ (g h : G), x (g * h) = (A.ρ g) (x h) + x g
h2 : ∀ s ∈ S, x s = (A.ρ s) y - y
⊢ (fun g ↦ Quotient.liftOn' g (fun g ↦ ⟨↑x g - (A.ρ g) y + y, ⋯⟩) ⋯) ∈ cocycles₁ (A.quotientToInvariants S)
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

Goal state before:
pp: case h.refine_4
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↥(cocycles₁ A)
hx :
  (ConcreteCategory.hom (H1π (res S.subtype A)))
      ((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x) =
    0
y : ↑A
hy :
  (ModuleCat.Hom.hom (d₀₁ (res S.subtype A))) y =
    ⇑((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x)
h1 : ∀ (g h : G), x (g * h) = (A.ρ g) (x h) + x g
h2 : ∀ s ∈ S, x s = (A.ρ s) y - y
⊢ (ModuleCat.Hom.hom (map (QuotientGroup.mk' S) (ofHom (A.ρ.quotientToInvariants_lift S)) 1))
      ((ConcreteCategory.hom (H1π (A.quotientToInvariants S)))
        ⟨fun g ↦ Quotient.liftOn' g (fun g ↦ ⟨↑x g - (A.ρ g) y + y, ⋯⟩) ⋯, ⋯⟩) =
    (ConcreteCategory.hom (H1π A)) x

Tactic:
·

Goal state after:
case h.refine_4
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↥(cocycles₁ A)
hx :
  (ConcreteCategory.hom (H1π (res S.subtype A)))
      ((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x) =
    0
y : ↑A
hy :
  (ModuleCat.Hom.hom (d₀₁ (res S.subtype A))) y =
    ⇑((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x)
h1 : ∀ (g h : G), x (g * h) = (A.ρ g) (x h) + x g
h2 : ∀ s ∈ S, x s = (A.ρ s) y - y
⊢ (ModuleCat.Hom.hom (map (QuotientGroup.mk' S) (ofHom (A.ρ.quotientToInvariants_lift S)) 1))
      ((ConcreteCategory.hom (H1π (A.quotientToInvariants S)))
        ⟨fun g ↦ Quotient.liftOn' g (fun g ↦ ⟨↑x g - (A.ρ g) y + y, ⋯⟩) ⋯, ⋯⟩) =
    (ConcreteCategory.hom (H1π A)) x
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
⊢ idealOfVars σ R ≤ restrictSupportIdeal R (⇑degree ⁻¹' Set.Ici 1) ⋯

pp: case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
⊢ restrictSupportIdeal R (⇑degree ⁻¹' Set.Ici 1) ⋯ ≤ idealOfVars σ R

Tactic:
·

Goal state after:
case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
⊢ idealOfVars σ R ≤ restrictSupportIdeal R (⇑degree ⁻¹' Set.Ici 1) ⋯
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
⊢ restrictSupportIdeal R (⇑degree ⁻¹' Set.Ici 1) ⋯ ≤ idealOfVars σ R

Tactic:
·

Goal state after:
case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
⊢ restrictSupportIdeal R (⇑degree ⁻¹' Set.Ici 1) ⋯ ≤ idealOfVars σ R
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
hn : n = 0
⊢ Submodule.restrictScalars R (restrictSupportIdeal R (⇑degree ⁻¹' Set.Ici 1) ⋯ ^ n) =
    Submodule.restrictScalars R (restrictSupportIdeal R (⇑degree ⁻¹' Set.Ici n) ⋯)

pp: case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
hn : ¬n = 0
⊢ Submodule.restrictScalars R (restrictSupportIdeal R (⇑degree ⁻¹' Set.Ici 1) ⋯ ^ n) =
    Submodule.restrictScalars R (restrictSupportIdeal R (⇑degree ⁻¹' Set.Ici n) ⋯)

Tactic:
·

Goal state after:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
hn : n = 0
⊢ Submodule.restrictScalars R (restrictSupportIdeal R (⇑degree ⁻¹' Set.Ici 1) ⋯ ^ n) =
    Submodule.restrictScalars R (restrictSupportIdeal R (⇑degree ⁻¹' Set.Ici n) ⋯)
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
r : R
h : r = 0
⊢ C r ∈ idealOfVars σ R ^ n ↔ r = 0 ∨ n = 0

pp: case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
r : R
h : ¬r = 0
⊢ C r ∈ idealOfVars σ R ^ n ↔ r = 0 ∨ n = 0

Tactic:
·

Goal state after:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
r : R
h : r = 0
⊢ C r ∈ idealOfVars σ R ^ n ↔ r = 0 ∨ n = 0
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
m : MonomialOrder σ
B : Set (MvPolynomial σ R)
h : 0 ∈ B
⊢ span (m.leadingTerm '' insert 0 B) = span (m.leadingTerm '' B)

pp: case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
m : MonomialOrder σ
B : Set (MvPolynomial σ R)
h : 0 ∉ B
⊢ span (m.leadingTerm '' insert 0 B) = span (m.leadingTerm '' B)

Tactic:
·

Goal state after:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
m : MonomialOrder σ
B : Set (MvPolynomial σ R)
h : 0 ∈ B
⊢ span (m.leadingTerm '' insert 0 B) = span (m.leadingTerm '' B)
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
m : MonomialOrder σ
B : Set (MvPolynomial σ R)
h : 0 ∈ B
⊢ span (m.leadingTerm '' insert 0 B) = span (m.leadingTerm '' B)

Tactic:
Set.insert_eq_of_mem h

Goal state after:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
m : MonomialOrder σ
B : Set (MvPolynomial σ R)
h : 0 ∈ B
⊢ span (m.leadingTerm '' B) = span (m.leadingTerm '' B)
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
m : MonomialOrder σ
B : Set (MvPolynomial σ R)
h : 0 ∉ B
⊢ span (m.leadingTerm '' insert 0 B) = span (m.leadingTerm '' B)

Tactic:
·

Goal state after:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
m : MonomialOrder σ
B : Set (MvPolynomial σ R)
h : 0 ∉ B
⊢ span (m.leadingTerm '' insert 0 B) = span (m.leadingTerm '' B)
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
m : MonomialOrder σ
B : Set (MvPolynomial σ R)
hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p)
p : MvPolynomial σ R
hp : p ∈ B
⊢ p ∈ m.leadingTerm ⁻¹' ↑(span ((fun p ↦ (MvPolynomial.monomial (m.degree p)) 1) '' B))

pp: case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
m : MonomialOrder σ
B : Set (MvPolynomial σ R)
hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p)
p : MvPolynomial σ R
hp : p ∈ B
⊢ p ∈ (fun p ↦ (MvPolynomial.monomial (m.degree p)) 1) ⁻¹' ↑(span (m.leadingTerm '' B))

Tactic:
·

Goal state after:
case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
m : MonomialOrder σ
B : Set (MvPolynomial σ R)
hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p)
p : MvPolynomial σ R
hp : p ∈ B
⊢ p ∈ m.leadingTerm ⁻¹' ↑(span ((fun p ↦ (MvPolynomial.monomial (m.degree p)) 1) '' B))
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
m : MonomialOrder σ
B : Set (MvPolynomial σ R)
hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p)
p : MvPolynomial σ R
hp : p ∈ B
⊢ p ∈ (fun p ↦ (MvPolynomial.monomial (m.degree p)) 1) ⁻¹' ↑(span (m.leadingTerm '' B))

Tactic:
·

Goal state after:
case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
m : MonomialOrder σ
B : Set (MvPolynomial σ R)
hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p)
p : MvPolynomial σ R
hp : p ∈ B
⊢ p ∈ (fun p ↦ (MvPolynomial.monomial (m.degree p)) 1) ⁻¹' ↑(span (m.leadingTerm '' B))