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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cocycles₁ A)
this :
  (ConcreteCategory.hom ((shortComplexH1 A).moduleCatLeftHomologyData.i ≫ (cochainsIso₁ A).inv)) x =
    (ConcreteCategory.hom (iCocycles A 1)) ((ConcreteCategory.hom (isoCocycles₁ A).inv) x)
⊢ (ConcreteCategory.hom (cochainsIso₁ A).inv) ⇑x =
    (ConcreteCategory.hom ((forget₂ (ModuleCat k) Ab).map (HomologicalComplex.iCycles (inhomogeneousCochains A) 1)))
      ((ConcreteCategory.hom (isoCocycles₁ A).inv) x)

Tactic:
]

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cocycles₁ A)
this :
  (ConcreteCategory.hom ((shortComplexH1 A).moduleCatLeftHomologyData.i ≫ (cochainsIso₁ A).inv)) x =
    (ConcreteCategory.hom (iCocycles A 1)) ((ConcreteCategory.hom (isoCocycles₁ A).inv) x)
⊢ (ConcreteCategory.hom (cochainsIso₁ A).inv) ⇑x =
    (ConcreteCategory.hom ((forget₂ (ModuleCat k) Ab).map (HomologicalComplex.iCycles (inhomogeneousCochains A) 1)))
      ((ConcreteCategory.hom (isoCocycles₁ A).inv) x)
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cocycles₁ A)
this :
  (ConcreteCategory.hom ((shortComplexH1 A).moduleCatLeftHomologyData.i ≫ (cochainsIso₁ A).inv)) x =
    (ConcreteCategory.hom (iCocycles A 1)) ((ConcreteCategory.hom (isoCocycles₁ A).inv) x)
⊢ (ConcreteCategory.hom (cochainsIso₁ A).inv) ⇑x =
    (ConcreteCategory.hom ((shortComplexH1 A).moduleCatLeftHomologyData.i ≫ (cochainsIso₁ A).inv)) x

Tactic:
]

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cocycles₁ A)
this :
  (ConcreteCategory.hom ((shortComplexH1 A).moduleCatLeftHomologyData.i ≫ (cochainsIso₁ A).inv)) x =
    (ConcreteCategory.hom (iCocycles A 1)) ((ConcreteCategory.hom (isoCocycles₁ A).inv) x)
⊢ (ConcreteCategory.hom (cochainsIso₁ A).inv) ⇑x =
    (ConcreteCategory.hom ((shortComplexH1 A).moduleCatLeftHomologyData.i ≫ (cochainsIso₁ A).inv)) x
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cocycles₂ A)
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cocycles₂ A)
⊢ (ConcreteCategory.hom (cochainsIso₂ A).inv) ⇑x =
    (ConcreteCategory.hom ((forget₂ (ModuleCat k) Ab).map (HomologicalComplex.iCycles (inhomogeneousCochains A) 2)))
      ((ConcreteCategory.hom (isoCocycles₂ A).inv) x)

Tactic:
]

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cocycles₂ A)
⊢ (ConcreteCategory.hom (cochainsIso₂ A).inv) ⇑x =
    (ConcreteCategory.hom ((forget₂ (ModuleCat k) Ab).map (HomologicalComplex.iCycles (inhomogeneousCochains A) 2)))
      ((ConcreteCategory.hom (isoCocycles₂ A).inv) x)
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x y : ↥(cocycles₁ A)
⊢ ⇑(x - y) ∈ coboundaries₁ A ↔ ⇑x - ⇑y ∈ coboundaries₁ A

Tactic:
]

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x y : ↥(cocycles₁ A)
⊢ ⇑(x - y) ∈ coboundaries₁ A ↔ ⇑x - ⇑y ∈ coboundaries₁ A
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x y : ↥(cocycles₂ A)
⊢ ⇑(x - y) ∈ coboundaries₂ A ↔ ⇑x - ⇑y ∈ coboundaries₂ A

Tactic:
]

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x y : ↥(cocycles₂ A)
⊢ ⇑(x - y) ∈ coboundaries₂ A ↔ ⇑x - ⇑y ∈ coboundaries₂ A
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 : ℕ
inst✝ : NeZero i
hi : Even i
x y : ↥(LinearMap.ker A.ρ.norm)
⊢ ↑x - ↑y ∈ (Hom.hom (A.applyAsHom g - 𝟙 A)).range ↔ ↑x - ↑y ∈ (Hom.hom (A.applyAsHom g - 𝟙 A)).range

Tactic:
]

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
inst✝ : DecidableEq G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
A : Rep k G
i : ℕ
hi : Odd i
x y : ↥(Hom.hom (A.applyAsHom g - 𝟙 A)).ker
⊢ ↑x - ↑y ∈ LinearMap.range A.ρ.norm ↔ ↑x - ↑y ∈ LinearMap.range A.ρ.norm

Tactic:
]

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A B C : Rep k G
φ : A ⟶ B
ψ : B ⟶ C
n : ℕ
⊢ HomologicalComplex.homologyMap (cochainsMap (MonoidHom.id G) φ) n ≫
      HomologicalComplex.homologyMap (cochainsMap (MonoidHom.id G) ψ) n =
    map (MonoidHom.id G) φ n ≫ map (MonoidHom.id G) ψ n

Tactic:
]

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
n✝ : ℕ
e : G ≃* H
e' : ↑B ≃ₗ[k] ↑A
he : ∀ (g : G), ↑e' ∘ₗ B.ρ g = A.ρ (e g) ∘ₗ ↑e'
n : ℕ
g : G
⊢ (MonoidHom.comp A.ρ ↑e) g = (↑e' ∘ₗ B.ρ g) ∘ₗ ↑e'.symm

Tactic:
]

Goal state after:
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
n✝ : ℕ
e : G ≃* H
e' : ↑B ≃ₗ[k] ↑A
he : ∀ (g : G), ↑e' ∘ₗ B.ρ g = A.ρ (e g) ∘ₗ ↑e'
n : ℕ
g : G
⊢ (MonoidHom.comp A.ρ ↑e) g = (↑e' ∘ₗ B.ρ g) ∘ₗ ↑e'.symm
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
n✝ : ℕ
e : G ≃* H
e' : ↑B ≃ₗ[k] ↑A
he : ∀ (g : G), ↑e' ∘ₗ B.ρ g = A.ρ (e g) ∘ₗ ↑e'
n : ℕ
⊢ map ((↑e.symm).comp ↑e)
      ((resFunctor ↑e).map (ofHom { toLinearMap := ↑e', isIntertwining' := ⋯ }) ≫
        ofHom { toLinearMap := ↑e'.symm, isIntertwining' := ⋯ })
      n =
    map (MonoidHom.id G) (𝟙 B) n

Tactic:
]

Goal state after:
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
n✝ : ℕ
e : G ≃* H
e' : ↑B ≃ₗ[k] ↑A
he : ∀ (g : G), ↑e' ∘ₗ B.ρ g = A.ρ (e g) ∘ₗ ↑e'
n : ℕ
⊢ map ((↑e.symm).comp ↑e)
      ((resFunctor ↑e).map (ofHom { toLinearMap := ↑e', isIntertwining' := ⋯ }) ≫
        ofHom { toLinearMap := ↑e'.symm, isIntertwining' := ⋯ })
      n =
    map (MonoidHom.id G) (𝟙 B) n
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
n✝ : ℕ
e : G ≃* H
e' : ↑B ≃ₗ[k] ↑A
he : ∀ (g : G), ↑e' ∘ₗ B.ρ g = A.ρ (e g) ∘ₗ ↑e'
n : ℕ
⊢ map ((↑e).comp ↑e.symm)
      ((resFunctor ↑e.symm).map (ofHom { toLinearMap := ↑e'.symm, isIntertwining' := ⋯ }) ≫
        ofHom { toLinearMap := ↑e', isIntertwining' := ⋯ })
      n =
    map (MonoidHom.id H) (𝟙 A) n

Tactic:
]

Goal state after:
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
n✝ : ℕ
e : G ≃* H
e' : ↑B ≃ₗ[k] ↑A
he : ∀ (g : G), ↑e' ∘ₗ B.ρ g = A.ρ (e g) ∘ₗ ↑e'
n : ℕ
⊢ map ((↑e).comp ↑e.symm)
      ((resFunctor ↑e.symm).map (ofHom { toLinearMap := ↑e'.symm, isIntertwining' := ⋯ }) ≫
        ofHom { toLinearMap := ↑e', isIntertwining' := ⋯ })
      n =
    map (MonoidHom.id H) (𝟙 A) n
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cycles₁ X.X₃)
y : G →₀ ↑X.X₂
hy : (mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap) y = ↑z
x : ↑X.X₁
hx : (Rep.Hom.hom X.f) x = (ConcreteCategory.hom (d₁₀ X.X₂)) y
⊢ (ModuleCat.Hom.hom (d₁₀ X.X₃ ≫ (chainsIso₀ X.X₃).inv)) ↑z = 0

Tactic:
]

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cycles₁ X.X₃)
y : G →₀ ↑X.X₂
hy : (mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap) y = ↑z
x : ↑X.X₁
hx : (Rep.Hom.hom X.f) x = (ConcreteCategory.hom (d₁₀ X.X₂)) y
⊢ (ModuleCat.Hom.hom (d₁₀ X.X₃ ≫ (chainsIso₀ X.X₃).inv)) ↑z = 0
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cycles₂ X.X₃)
y : G × G →₀ ↑X.X₂
hy : (mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap) y = ↑z
x : G →₀ ↑X.X₁
hx : (mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap) x = (ConcreteCategory.hom (d₂₁ X.X₂)) y
⊢ (ModuleCat.Hom.hom (d₂₁ X.X₃ ≫ (chainsIso₁ X.X₃).inv)) ↑z = 0

Tactic:
]

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cycles₂ X.X₃)
y : G × G →₀ ↑X.X₂
hy : (mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap) y = ↑z
x : G →₀ ↑X.X₁
hx : (mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap) x = (ConcreteCategory.hom (d₂₁ X.X₂)) y
⊢ (ModuleCat.Hom.hom (d₂₁ X.X₃ ≫ (chainsIso₁ X.X₃).inv)) ↑z = 0
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
φ : res 1 A ⟶ B
⊢ (shortComplexH1 A).moduleCatLeftHomologyData.i ≫ (mapShortComplexH1 1 φ).τ₂ =
    0 ≫ (shortComplexH1 B).moduleCatLeftHomologyData.i

Tactic:
]

Goal state after:
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
φ : res 1 A ⟶ B
⊢ (shortComplexH1 A).moduleCatLeftHomologyData.i ≫ (mapShortComplexH1 1 φ).τ₂ =
    0 ≫ (shortComplexH1 B).moduleCatLeftHomologyData.i
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

Goal state before:
pp: k G H : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Group H
A✝ : Rep k H
B : Rep k G
f : G →* H
φ : res f A✝ ⟶ B
n : ℕ
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

Goal state before:
pp: k G H : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Group H
A✝ : Rep k H
B : Rep k G
f : G →* H
φ : res f A✝ ⟶ B
n : ℕ
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
⊢ ∀ (a : ↑(H1InfRes A S).X₁), (ConcreteCategory.hom (H1InfRes A S).f) a = 0 → a = 0

Tactic:
]

Goal state after:
k G H : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Group H
A✝ : Rep k H
B : Rep k G
f : G →* H
φ : res f A✝ ⟶ B
n : ℕ
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
⊢ ∀ (a : ↑(H1InfRes A S).X₁), (ConcreteCategory.hom (H1InfRes A S).f) a = 0 → a = 0
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
⊢ (ModuleCat.Hom.hom (H1InfRes A S).g).ker ≤ (ModuleCat.Hom.hom (H1InfRes A S).f).range

Tactic:
]

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
⊢ (ModuleCat.Hom.hom (H1InfRes A S).g).ker ≤ (ModuleCat.Hom.hom (H1InfRes A S).f).range
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

Goal state before:
pp: 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
g : G
s : ↥S
⊢ ((MonoidHom.comp A.ρ S.subtype) s) (↑x g - (A.ρ g) y + y) = x (↑s * g) - x ↑s - (A.ρ ↑s) ((A.ρ g) y) + (x ↑s + y)

Tactic:
simp [add_eq_of_eq_sub (h2 s s.2), sub_eq_of_eq_add (h1 s g)]

Goal state after:
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
⊢ ∀ (g h : G ⧸ S),
    Quotient.liftOn' (g * h) (fun g ↦ ⟨↑x g - (A.ρ g) y + y, ⋯⟩) ⋯ =
      ((A.quotientToInvariants S).ρ g) (Quotient.liftOn' h (fun g ↦ ⟨↑x g - (A.ρ g) y + y, ⋯⟩) ⋯) +
        Quotient.liftOn' g (fun g ↦ ⟨↑x g - (A.ρ g) y + y, ⋯⟩) ⋯

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
⊢ ∀ (g h : G ⧸ S),
    Quotient.liftOn' (g * h) (fun g ↦ ⟨↑x g - (A.ρ g) y + y, ⋯⟩) ⋯ =
      ((A.quotientToInvariants S).ρ g) (Quotient.liftOn' h (fun g ↦ ⟨↑x g - (A.ρ g) y + y, ⋯⟩) ⋯) +
        Quotient.liftOn' g (fun g ↦ ⟨↑x g - (A.ρ g) y + y, ⋯⟩) ⋯
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

Goal state before:
pp: case h
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π A)) x ∈ (ModuleCat.Hom.hom (H1InfRes A S).g).ker
⊢ (ConcreteCategory.hom (H1π A)) x ∈ (ModuleCat.Hom.hom (H1InfRes A S).f).range

Tactic:
simp_all only [H1InfRes_X₂, H1InfRes_X₃, H1InfRes_g, H1InfRes_X₁, LinearMap.mem_ker,
    H1π_comp_map_apply S.subtype, H1InfRes_f]
  rcases (H1π_eq_zero_iff _).1 hx with ⟨(y : A), hy⟩
  have h1 := (mem_cocycles₁_iff x).1 x.2
  have h2 : ∀ s ∈ S, x s = A.ρ s y - y :=
    fun s hs => funext_iff.1 hy.symm ⟨s, hs⟩
  refine ⟨H1π _ ⟨fun g => Quotient.liftOn' g (fun g => ⟨x.1 g - A.ρ g y + y, ?_⟩) ?_, ?_⟩, ?_⟩
  · intro s
    calc
      _ = x (s * g) - x s - A.ρ s (A.ρ g y) + (x s + y) := by
        simp [add_eq_of_eq_sub (h2 s s.2), sub_eq_of_eq_add (h1 s g)]
      _ = x (g * (g⁻¹ * s * g)) - A.ρ g (A.ρ (g⁻¹ * s * g) y - y) - A.ρ g y + y := by
        simp only [mul_assoc, mul_inv_cancel_left, map_mul, Module.End.mul_apply, map_sub,
          Representation.self_inv_apply]
        abel
      _ = x g - A.ρ g y + y := by
        simp [eq_sub_of_add_eq' (h1 g (g⁻¹ * s * g)).symm,
          h2 (g⁻¹ * s * g) (Subgroup.Normal.conj_mem' ‹_› _ s.2 _)]
  · intro g h hgh
    have := congr(A.ρ g $(h2 (g⁻¹ * h) <| QuotientGroup.leftRel_apply.1 hgh))
    simp_all [← sub_eq_add_neg, sub_eq_sub_iff_sub_eq_sub]
  · rw [mem_cocycles₁_iff]
    intro g h
    induction g using QuotientGroup.induction_on with | @H g =>
    induction h using QuotientGroup.induction_on with | @H h =>
    apply Subtype.ext
    simp [← QuotientGroup.mk_mul, h1 g h, sub_add_eq_add_sub, add_assoc]
  · symm
    simp only [H1π_comp_map_apply, H1π_eq_iff (A := A)]
    use y
    ext g
    simp [coe_mapCocycles₁ (QuotientGroup.mk' S),
      cocycles₁.coe_mk (A := A.quotientToInvariants S), ← sub_sub]

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
η : Aut (forget k G)
f g : G → k
nat :
  (forget k G).map mulRepHom ≫ η.hom.hom.app rightFDRep =
    (η.hom.hom.app rightFDRep ⊗ₘ η.hom.hom.app rightFDRep) ≫ (forget k G).map mulRepHom
tensor : ∀ (X Y : FDRep k G), η.hom.hom.app (X ⊗ Y) = η.hom.hom.app X ⊗ₘ η.hom.hom.app Y
⊢ let α := Hom.hom (η.hom.hom.app rightFDRep).hom;
  α (f * g) = α f * α g

Tactic:
]

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
η : Aut (forget k G)
f g : G → k
nat :
  (forget k G).map mulRepHom ≫ η.hom.hom.app rightFDRep =
    (η.hom.hom.app rightFDRep ⊗ₘ η.hom.hom.app rightFDRep) ≫ (forget k G).map mulRepHom
tensor : ∀ (X Y : FDRep k G), η.hom.hom.app (X ⊗ Y) = η.hom.hom.app X ⊗ₘ η.hom.hom.app Y
⊢ let α := Hom.hom (η.hom.hom.app rightFDRep).hom;
  α (f * g) = α f * α g
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
η : Aut (forget k G)
α : (G → k) →ₗ[k] G → k := Hom.hom (η.hom.hom.app rightFDRep).hom
α_inv : (G → k) →ₗ[k] G → k := Hom.hom (η.inv.hom.app rightFDRep).hom
this : (Hom.hom (η.hom.hom.app rightFDRep).hom) 1 = 1
h : α (α_inv 1) = 1
⊢ α 1 = 1

Tactic:
]

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
η : Aut (forget k G)
α : (G → k) →ₗ[k] G → k := Hom.hom (η.hom.hom.app rightFDRep).hom
α_inv : (G → k) →ₗ[k] G → k := Hom.hom (η.inv.hom.app rightFDRep).hom
this : (Hom.hom (η.hom.hom.app rightFDRep).hom) 1 = 1
h : α (α_inv 1) = 1
⊢ α 1 = 1
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
η₁ η₂ : Aut (forget k G)
h : η₁.hom.hom.app rightFDRep = η₂.hom.hom.app rightFDRep
this : Fintype G
X : FDRep k G
v : ↑((forget k G).obj X).obj
h1 : (forget k G).map (ofRightFDRep X v) ≫ η₁.hom.hom.app X = (forget k G).map (ofRightFDRep X v) ≫ η₂.hom.hom.app X
h2 :
  (forget k G).map (ofRightFDRep X v) ≫ η₂.hom.hom.app X =
    η₂.hom.hom.app rightFDRep ≫ (forget k G).map (ofRightFDRep X v)
⊢ (Hom.hom (η₁.hom.hom.app X).hom) v = (Hom.hom (η₂.hom.hom.app X).hom) v

Tactic:
]

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
η₁ η₂ : Aut (forget k G)
h : η₁.hom.hom.app rightFDRep = η₂.hom.hom.app rightFDRep
this : Fintype G
X : FDRep k G
v : ↑((forget k G).obj X).obj
h1 : (forget k G).map (ofRightFDRep X v) ≫ η₁.hom.hom.app X = (forget k G).map (ofRightFDRep X v) ≫ η₂.hom.hom.app X
h2 :
  (forget k G).map (ofRightFDRep X v) ≫ η₂.hom.hom.app X =
    η₂.hom.hom.app rightFDRep ≫ (forget k G).map (ofRightFDRep X v)
⊢ (Hom.hom (η₁.hom.hom.app X).hom) v = (Hom.hom (η₂.hom.hom.app X).hom) v
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set σ
this :
  x ∈ Ideal.span ((fun x ↦ (monomial (Finsupp.single x 1)) 1) '' s) ↔
    ∀ xi ∈ x.support, ∃ si ∈ (fun i ↦ Finsupp.single i 1) '' s, si ≤ xi
⊢ x ∈ Ideal.span (X '' s) ↔ ∀ m ∈ x.support, ∃ i ∈ s, m i ≠ 0

Tactic:
]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set σ
this :
  x ∈ Ideal.span ((fun x ↦ (monomial (Finsupp.single x 1)) 1) '' s) ↔
    ∀ xi ∈ x.support, ∃ si ∈ (fun i ↦ Finsupp.single i 1) '' s, si ≤ xi
⊢ x ∈ Ideal.span (X '' s) ↔ ∀ m ∈ x.support, ∃ i ∈ s, m i ≠ 0
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
⊢ ⇑degree ⁻¹' Set.Ici 1 ⊆ (fun x ↦ (monomial x) 1) ⁻¹' ↑(Submodule.restrictScalars R (idealOfVars σ R))

Tactic:
]

Goal state after:
case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
⊢ ⇑degree ⁻¹' Set.Ici 1 ⊆ (fun x ↦ (monomial x) 1) ⁻¹' ↑(Submodule.restrictScalars R (idealOfVars σ R))
Module: Mathlib.RingTheory.MvPolynomial.Ideal

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

Tactic:
]

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

Goal state before:
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 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) ⋯)
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
⊢ Submodule.span (MvPolynomial σ R)
      ((fun x ↦ x.prod fun x1 x2 ↦ X x1 ^ x2) '' {x | degree x = n ∧ ↑x.support ⊆ Set.univ}) =
    Ideal.span ((fun x ↦ (monomial x) 1) '' ⇑degree ⁻¹' {n})

Tactic:
]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
⊢ Submodule.span (MvPolynomial σ R)
      ((fun x ↦ x.prod fun x1 x2 ↦ X x1 ^ x2) '' {x | degree x = n ∧ ↑x.support ⊆ Set.univ}) =
    Ideal.span ((fun x ↦ (monomial x) 1) '' ⇑degree ⁻¹' {n})
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial σ R
⊢ p ∈ restrictSupportIdeal R (⇑degree ⁻¹' Set.Ici n) ⋯ ↔ ∀ x ∈ p.support, n ≤ degree x

Tactic:
]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial σ R
⊢ p ∈ restrictSupportIdeal R (⇑degree ⁻¹' Set.Ici n) ⋯ ↔ ∀ x ∈ p.support, n ≤ degree x
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 '' B) = span (m.leadingTerm '' B)

Tactic:
]

Goal state after:
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)
⊢ B ⊆ m.leadingTerm ⁻¹' ↑(span ((fun p ↦ (MvPolynomial.monomial (m.degree p)) 1) '' 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)
⊢ B ⊆ 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)
⊢ B ⊆ (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)
⊢ B ⊆ (fun p ↦ (MvPolynomial.monomial (m.degree p)) 1) ⁻¹' ↑(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
⊢ MvPolynomial.C (m.leadingCoeff p) * (MvPolynomial.monomial (m.degree p)) 1 ∈
    span ((fun p ↦ (MvPolynomial.monomial (m.degree p)) 1) '' 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
⊢ MvPolynomial.C (m.leadingCoeff p) * (MvPolynomial.monomial (m.degree p)) 1 ∈
    span ((fun p ↦ (MvPolynomial.monomial (m.degree p)) 1) '' B)