mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: case inr
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
inst✝ : DecidableRel ⇑(QuotientGroup.rightRel S)
A : Rep.{w, u, v} k ↥S
g₁ g₂ : G
a : ↑A
s : ↥S
h : ¬(QuotientGroup.rightRel S) g₂ g₁
⊢ 0 = 0

pp: case inr.h
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
inst✝ : DecidableRel ⇑(QuotientGroup.rightRel S)
A : Rep.{w, u, v} k ↥S
g₁ g₂ : G
a : ↑A
s : ↥S
h : ¬(QuotientGroup.rightRel S) g₂ g₁
⊢ ¬(QuotientGroup.rightRel S) g₂ (↑s * g₁)

Tactic:
]

Goal state after:
case inr.h
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
inst✝ : DecidableRel ⇑(QuotientGroup.rightRel S)
A : Rep.{w, u, v} k ↥S
g₁ g₂ : G
a : ↑A
s : ↥S
h : ¬(QuotientGroup.rightRel S) g₂ g₁
⊢ ¬(QuotientGroup.rightRel S) g₂ (↑s * g₁)
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: case inr
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
inst✝ : DecidableRel ⇑(QuotientGroup.rightRel S)
A : Rep.{w, u, v} k ↥S
g₁ g₂ g₃ : G
a : ↑A
h : ¬(QuotientGroup.rightRel S) (g₂ * g₃⁻¹) g₁
⊢ 0 = 0

pp: case inr.h
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
inst✝ : DecidableRel ⇑(QuotientGroup.rightRel S)
A : Rep.{w, u, v} k ↥S
g₁ g₂ g₃ : G
a : ↑A
h : ¬(QuotientGroup.rightRel S) (g₂ * g₃⁻¹) g₁
⊢ ¬(QuotientGroup.rightRel S) g₂ (g₁ * g₃)

Tactic:
]

Goal state after:
case inr.h
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
inst✝ : DecidableRel ⇑(QuotientGroup.rightRel S)
A : Rep.{w, u, v} k ↥S
g₁ g₂ g₃ : G
a : ↑A
h : ¬(QuotientGroup.rightRel S) (g₂ * g₃⁻¹) g₁
⊢ ¬(QuotientGroup.rightRel S) g₂ (g₁ * g₃)
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
A : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
g : G
f : ↑(coind.{u, v, v, w} S.subtype A)
hx : Function.support ↑f ⊆ MulAction.orbit (↥S) g
⊢ ⟦g⟧.liftOn (fun g ↦ (IndV.mk S.subtype A.ρ g) (↑f g)) ⋯ = (IndV.mk S.subtype A.ρ g) (↑f g)

pp: case h₀
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
A : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
g : G
f : ↑(coind.{u, v, v, w} S.subtype A)
hx : Function.support ↑f ⊆ MulAction.orbit (↥S) g
⊢ ∀ b ∈ Finset.univ, b ≠ ⟦g⟧ → b.liftOn (fun g ↦ (IndV.mk S.subtype A.ρ g) (↑f g)) ⋯ = 0

pp: case h₁
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
A : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
g : G
f : ↑(coind.{u, v, v, w} S.subtype A)
hx : Function.support ↑f ⊆ MulAction.orbit (↥S) g
⊢ ⟦g⟧ ∉ Finset.univ → ⟦g⟧.liftOn (fun g ↦ (IndV.mk S.subtype A.ρ g) (↑f g)) ⋯ = 0

Tactic:
]

Goal state after:
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
A : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
g : G
f : ↑(coind.{u, v, v, w} S.subtype A)
hx : Function.support ↑f ⊆ MulAction.orbit (↥S) g
⊢ ⟦g⟧.liftOn (fun g ↦ (IndV.mk S.subtype A.ρ g) (↑f g)) ⋯ = (IndV.mk S.subtype A.ρ g) (↑f g)

case h₀
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
A : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
g : G
f : ↑(coind.{u, v, v, w} S.subtype A)
hx : Function.support ↑f ⊆ MulAction.orbit (↥S) g
⊢ ∀ b ∈ Finset.univ, b ≠ ⟦g⟧ → b.liftOn (fun g ↦ (IndV.mk S.subtype A.ρ g) (↑f g)) ⋯ = 0

case h₁
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
A : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
g : G
f : ↑(coind.{u, v, v, w} S.subtype A)
hx : Function.support ↑f ⊆ MulAction.orbit (↥S) g
⊢ ⟦g⟧ ∉ Finset.univ → ⟦g⟧.liftOn (fun g ↦ (IndV.mk S.subtype A.ρ g) (↑f g)) ⋯ = 0
Module: Mathlib.RepresentationTheory.Homological.ContCohomology.Functoriality

Goal state before:
pp: case succ
k : Type u
G : Type v
inst✝⁴ : Ring k
inst✝³ : TopologicalSpace k
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
i : ℕ
ih : resolutionMap (ContinuousMonoidHom.id G) (𝟙 X) i = 𝟙 (X.resolutionX i)
⊢ ofHom (coind₁ResMap (ContinuousMonoidHom.id G) (Hom.hom (𝟙 (X.resolutionX i)))) = 𝟙 (X.resolutionX (i + 1))

Tactic:
]

Goal state after:
case succ
k : Type u
G : Type v
inst✝⁴ : Ring k
inst✝³ : TopologicalSpace k
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
i : ℕ
ih : resolutionMap (ContinuousMonoidHom.id G) (𝟙 X) i = 𝟙 (X.resolutionX i)
⊢ ofHom (coind₁ResMap (ContinuousMonoidHom.id G) (Hom.hom (𝟙 (X.resolutionX i)))) = 𝟙 (X.resolutionX (i + 1))
Module: Mathlib.RepresentationTheory.Homological.ContCohomology.Functoriality

Goal state before:
pp: k : Type u
G : Type v
inst✝⁴ : Ring k
inst✝³ : TopologicalSpace k
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
i : ℕ
⊢ resolutionMap (ContinuousMonoidHom.id G) (𝟙 X) i = 𝟙 (X.resolutionX i)

Tactic:
induction i with
  | zero => rfl
  | succ i ih =>
    rw [resolutionMap_succ, ih]
    ext F x
    rfl

Goal state after:
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: k : Type u
G : Type v
inst✝³ : CommRing k
inst✝² : Group G
S : Subgroup G
inst✝¹ : DecidableRel ⇑(QuotientGroup.rightRel S)
A : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
g : ↑(coind.{u, v, v, w} S.subtype A)
a : G
| ↑(A.indToCoind (A.coindToInd g)) a

Tactic:
rw [coindToInd_apply]

Goal state after:
k : Type u
G : Type v
inst✝³ : CommRing k
inst✝² : Group G
S : Subgroup G
inst✝¹ : DecidableRel ⇑(QuotientGroup.rightRel S)
A : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
g : ↑(coind.{u, v, v, w} S.subtype A)
a : G
| ↑(A.indToCoind (∑ g_1, g_1.liftOn (fun g_2 ↦ (IndV.mk S.subtype A.ρ g_2) (↑g g_2)) ⋯)) a
Module: Mathlib.RepresentationTheory.Homological.ContCohomology.Functoriality

Goal state before:
pp: case succ
k : Type u
G H K : Type v
inst✝¹⁰ : Ring k
inst✝⁹ : TopologicalSpace k
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : Group H
inst✝⁴ : TopologicalSpace H
inst✝³ : IsTopologicalGroup H
inst✝² : Group K
inst✝¹ : TopologicalSpace K
inst✝ : IsTopologicalGroup K
X : TopRep k G
Y : TopRep k H
Z : TopRep k K
φ : H →ₜ* G
ψ : K →ₜ* H
f : res (↑φ) X ⟶ Y
g : res (↑ψ) Y ⟶ Z
i : ℕ
ih :
  resolutionMap (φ.comp ψ) ((resFunctor ↑ψ).map f ≫ g) i =
    (resFunctor ↑ψ).map (resolutionMap φ f i) ≫ resolutionMap ψ g i
⊢ ofHom (coind₁ResMap (φ.comp ψ) (Hom.hom ((resFunctor ↑ψ).map (resolutionMap φ f i) ≫ resolutionMap ψ g i))) =
    (resFunctor ↑ψ).map (ofHom (coind₁ResMap φ (Hom.hom (resolutionMap φ f i)))) ≫
      ofHom (coind₁ResMap ψ (Hom.hom (resolutionMap ψ g i)))

Tactic:
]

Goal state after:
case succ
k : Type u
G H K : Type v
inst✝¹⁰ : Ring k
inst✝⁹ : TopologicalSpace k
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : Group H
inst✝⁴ : TopologicalSpace H
inst✝³ : IsTopologicalGroup H
inst✝² : Group K
inst✝¹ : TopologicalSpace K
inst✝ : IsTopologicalGroup K
X : TopRep k G
Y : TopRep k H
Z : TopRep k K
φ : H →ₜ* G
ψ : K →ₜ* H
f : res (↑φ) X ⟶ Y
g : res (↑ψ) Y ⟶ Z
i : ℕ
ih :
  resolutionMap (φ.comp ψ) ((resFunctor ↑ψ).map f ≫ g) i =
    (resFunctor ↑ψ).map (resolutionMap φ f i) ≫ resolutionMap ψ g i
⊢ ofHom (coind₁ResMap (φ.comp ψ) (Hom.hom ((resFunctor ↑ψ).map (resolutionMap φ f i) ≫ resolutionMap ψ g i))) =
    (resFunctor ↑ψ).map (ofHom (coind₁ResMap φ (Hom.hom (resolutionMap φ f i)))) ≫
      ofHom (coind₁ResMap ψ (Hom.hom (resolutionMap ψ g i)))
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: k : Type u
G : Type v
inst✝³ : CommRing k
inst✝² : Group G
S : Subgroup G
inst✝¹ : DecidableRel ⇑(QuotientGroup.rightRel S)
A : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
g : ↑(coind.{u, v, v, w} S.subtype A)
a : G
⊢ ↑(A.indToCoind (⟦a⟧.liftOn (fun g_1 ↦ (IndV.mk S.subtype A.ρ g_1) (↑g g_1)) ⋯)) a = ↑g a

pp: case h₀
k : Type u
G : Type v
inst✝³ : CommRing k
inst✝² : Group G
S : Subgroup G
inst✝¹ : DecidableRel ⇑(QuotientGroup.rightRel S)
A : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
g : ↑(coind.{u, v, v, w} S.subtype A)
a : G
⊢ ∀ b ∈ Finset.univ, b ≠ ⟦a⟧ → ↑(A.indToCoind (b.liftOn (fun g_1 ↦ (IndV.mk S.subtype A.ρ g_1) (↑g g_1)) ⋯)) a = 0

pp: case h₁
k : Type u
G : Type v
inst✝³ : CommRing k
inst✝² : Group G
S : Subgroup G
inst✝¹ : DecidableRel ⇑(QuotientGroup.rightRel S)
A : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
g : ↑(coind.{u, v, v, w} S.subtype A)
a : G
⊢ ⟦a⟧ ∉ Finset.univ → ↑(A.indToCoind (⟦a⟧.liftOn (fun g_1 ↦ (IndV.mk S.subtype A.ρ g_1) (↑g g_1)) ⋯)) a = 0

Tactic:
]

Goal state after:
k : Type u
G : Type v
inst✝³ : CommRing k
inst✝² : Group G
S : Subgroup G
inst✝¹ : DecidableRel ⇑(QuotientGroup.rightRel S)
A : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
g : ↑(coind.{u, v, v, w} S.subtype A)
a : G
⊢ ↑(A.indToCoind (⟦a⟧.liftOn (fun g_1 ↦ (IndV.mk S.subtype A.ρ g_1) (↑g g_1)) ⋯)) a = ↑g a

case h₀
k : Type u
G : Type v
inst✝³ : CommRing k
inst✝² : Group G
S : Subgroup G
inst✝¹ : DecidableRel ⇑(QuotientGroup.rightRel S)
A : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
g : ↑(coind.{u, v, v, w} S.subtype A)
a : G
⊢ ∀ b ∈ Finset.univ, b ≠ ⟦a⟧ → ↑(A.indToCoind (b.liftOn (fun g_1 ↦ (IndV.mk S.subtype A.ρ g_1) (↑g g_1)) ⋯)) a = 0

case h₁
k : Type u
G : Type v
inst✝³ : CommRing k
inst✝² : Group G
S : Subgroup G
inst✝¹ : DecidableRel ⇑(QuotientGroup.rightRel S)
A : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
g : ↑(coind.{u, v, v, w} S.subtype A)
a : G
⊢ ⟦a⟧ ∉ Finset.univ → ↑(A.indToCoind (⟦a⟧.liftOn (fun g_1 ↦ (IndV.mk S.subtype A.ρ g_1) (↑g g_1)) ⋯)) a = 0
Module: Mathlib.RepresentationTheory.Homological.ContCohomology.Functoriality

Goal state before:
pp: case succ
k : Type u
G H : Type v
inst✝⁷ : Ring k
inst✝⁶ : TopologicalSpace k
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : Group H
inst✝¹ : TopologicalSpace H
inst✝ : IsTopologicalGroup H
X : TopRep k G
Y : TopRep k H
φ : H →ₜ* G
f : res (↑φ) X ⟶ Y
i : ℕ
ih :
  (Hom.hom (Y.d i)).comp (Hom.hom (resolutionMap φ f i)) =
    (coind₁ResMap φ (Hom.hom (resolutionMap φ f i))).comp (ContIntertwiningMap.restrict (↑φ) (Hom.hom (X.d i)))
⊢ (coind₁ResMap φ (coind₁ResMap φ (Hom.hom (resolutionMap φ f i)))).comp
        (ContIntertwiningMap.restrict (↑φ) (X.resolutionX i).ρ.coind₁.coind₁ι) -
      coind₁ResMap φ
        ((coind₁ResMap φ (Hom.hom (resolutionMap φ f i))).comp (ContIntertwiningMap.restrict (↑φ) (Hom.hom (X.d i)))) =
    (coind₁ResMap φ (coind₁ResMap φ (Hom.hom (resolutionMap φ f i)))).comp
        (ContIntertwiningMap.restrict (↑φ) (X.resolutionX i).ρ.coind₁.coind₁ι) -
      coind₁ResMap φ
        ((coind₁ResMap φ (Hom.hom (resolutionMap φ f i))).comp (ContIntertwiningMap.restrict (↑φ) (Hom.hom (X.d i))))

Tactic:
]

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

Goal state before:
pp: k : Type u
G H K : Type v
inst✝¹⁰ : Ring k
inst✝⁹ : TopologicalSpace k
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : Group H
inst✝⁴ : TopologicalSpace H
inst✝³ : IsTopologicalGroup H
inst✝² : Group K
inst✝¹ : TopologicalSpace K
inst✝ : IsTopologicalGroup K
X : TopRep k G
Y : TopRep k H
Z : TopRep k K
φ : H →ₜ* G
f : res (↑φ) X ⟶ Y
i : ℕ
⊢ (invariantsFunctor k G).map (X.d (i + 1)) ≫ invariantsResMap (↑φ) (resolutionMap φ f (i + 1 + 1)) =
    (invariantsFunctor k G).map (X.d (i + 1)) ≫ invariantsResMap (↑φ) (resolutionMap φ f (i + 1 + 1))

Tactic:
]

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

Goal state before:
pp: k : Type u
G : Type v
inst✝⁴ : Ring k
inst✝³ : TopologicalSpace k
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
i : ℕ
⊢ invariantsResMap (↑(ContinuousMonoidHom.id G)) (𝟙 (X.resolutionX (i + 1))) = (𝟙 X.homogeneousCochains).f i

Tactic:
]

Goal state after:
k : Type u
G : Type v
inst✝⁴ : Ring k
inst✝³ : TopologicalSpace k
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
i : ℕ
⊢ invariantsResMap (↑(ContinuousMonoidHom.id G)) (𝟙 (X.resolutionX (i + 1))) = (𝟙 X.homogeneousCochains).f i
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: k : Type u
G : Type v
inst✝³ : CommRing k
inst✝² : Group G
S : Subgroup G
inst✝¹ : DecidableRel ⇑(QuotientGroup.rightRel S)
A : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
g : G
a : ↑A
⊢ (IndV.mk S.subtype A.ρ g)
      (↑(A.indToCoind
            ((Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ))
              ((MonoidAlgebra.lsingle g) 1 ⊗ₜ[k] a)))
        g) =
    (Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ))
      ((MonoidAlgebra.lsingle g) 1 ⊗ₜ[k] a)

pp: case hx
k : Type u
G : Type v
inst✝³ : CommRing k
inst✝² : Group G
S : Subgroup G
inst✝¹ : DecidableRel ⇑(QuotientGroup.rightRel S)
A : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
g : G
a : ↑A
⊢ Function.support
      ↑(A.indToCoind
          ((Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ))
            ((MonoidAlgebra.lsingle g) 1 ⊗ₜ[k] a))) ⊆
    MulAction.orbit (↥S) g

Tactic:
]

Goal state after:
k : Type u
G : Type v
inst✝³ : CommRing k
inst✝² : Group G
S : Subgroup G
inst✝¹ : DecidableRel ⇑(QuotientGroup.rightRel S)
A : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
g : G
a : ↑A
⊢ (IndV.mk S.subtype A.ρ g)
      (↑(A.indToCoind
            ((Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ))
              ((MonoidAlgebra.lsingle g) 1 ⊗ₜ[k] a)))
        g) =
    (Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ))
      ((MonoidAlgebra.lsingle g) 1 ⊗ₜ[k] a)

case hx
k : Type u
G : Type v
inst✝³ : CommRing k
inst✝² : Group G
S : Subgroup G
inst✝¹ : DecidableRel ⇑(QuotientGroup.rightRel S)
A : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
g : G
a : ↑A
⊢ Function.support
      ↑(A.indToCoind
          ((Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ))
            ((MonoidAlgebra.lsingle g) 1 ⊗ₜ[k] a))) ⊆
    MulAction.orbit (↥S) g
Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic

Goal state before:
pp: case refine_2
k : Type u_1
G : Type u_2
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
this✝ : Fintype G
x : MonoidAlgebra k G
hx : x ∈ ((linearCombination k fun x ↦ 1) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)).ker
this : x = x.coeff.sum fun g r ↦ MonoidAlgebra.single g r - MonoidAlgebra.single 1 r
⊢ (x.coeff.sum fun g r ↦ MonoidAlgebra.single g r - MonoidAlgebra.single 1 r) ∈ Coinvariants.ker (leftRegular k G)

Tactic:
]

Goal state after:
case refine_2
k : Type u_1
G : Type u_2
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
this✝ : Fintype G
x : MonoidAlgebra k G
hx : x ∈ ((linearCombination k fun x ↦ 1) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)).ker
this : x = x.coeff.sum fun g r ↦ MonoidAlgebra.single g r - MonoidAlgebra.single 1 r
⊢ (x.coeff.sum fun g r ↦ MonoidAlgebra.single g r - MonoidAlgebra.single 1 r) ∈ Coinvariants.ker (leftRegular k G)
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: k : Type u
G : Type v
inst✝³ : CommRing k
inst✝² : Group G
S : Subgroup G
inst✝¹ : DecidableRel ⇑(QuotientGroup.rightRel S)
inst✝ : S.FiniteIndex
A : Rep.{max w u v, u, v} k ↥S
B : Rep.{max w u v, u, v} k G
f : res S.subtype B ⟶ A
⊢ ((resCoindAdjunction k S.subtype).homEquiv B A) f ≫ (indCoindNatIso k S).symm.hom.app A =
    (resCoindHomEquiv.{max w u v, u, v, v} S.subtype B A) f ≫ A.indCoindIso.inv

Tactic:
]

Goal state after:
k : Type u
G : Type v
inst✝³ : CommRing k
inst✝² : Group G
S : Subgroup G
inst✝¹ : DecidableRel ⇑(QuotientGroup.rightRel S)
inst✝ : S.FiniteIndex
A : Rep.{max w u v, u, v} k ↥S
B : Rep.{max w u v, u, v} k G
f : res S.subtype B ⟶ A
⊢ ((resCoindAdjunction k S.subtype).homEquiv B A) f ≫ (indCoindNatIso k S).symm.hom.app A =
    (resCoindHomEquiv.{max w u v, u, v, v} S.subtype B A) f ≫ A.indCoindIso.inv
Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic

Goal state before:
pp: case zero
k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
⊢ {
        X₁ :=
          ((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).obj
              ((chainComplexFunctor k g).obj (leftRegular k G))).X₁,
        X₂ :=
          ((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).obj
              ((chainComplexFunctor k g).obj (leftRegular k G))).X₂,
        X₃ :=
          ((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).obj
              ((ChainComplex.single₀ (Rep k G)).obj (trivial k G k))).X₂,
        f :=
          ((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).obj
              ((chainComplexFunctor k g).obj (leftRegular k G))).f,
        g :=
          ((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).map
              ((((chainComplexFunctor k g).obj (leftRegular k G)).toSingle₀Equiv (trivial k G k)).symm
                ⟨(trivial k G k).leftRegularHom 1, ⋯⟩)).τ₂,
        zero := ⋯ }.Exact ∧
    Epi
      ((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).map
          ((((chainComplexFunctor k g).obj (leftRegular k G)).toSingle₀Equiv (trivial k G k)).symm
            ⟨(trivial k G k).leftRegularHom 1, ⋯⟩)).τ₂

Tactic:
]

Goal state after:
case zero
k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
⊢ {
        X₁ :=
          ((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).obj
              ((chainComplexFunctor k g).obj (leftRegular k G))).X₁,
        X₂ :=
          ((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).obj
              ((chainComplexFunctor k g).obj (leftRegular k G))).X₂,
        X₃ :=
          ((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).obj
              ((ChainComplex.single₀ (Rep k G)).obj (trivial k G k))).X₂,
        f :=
          ((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).obj
              ((chainComplexFunctor k g).obj (leftRegular k G))).f,
        g :=
          ((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).map
              ((((chainComplexFunctor k g).obj (leftRegular k G)).toSingle₀Equiv (trivial k G k)).symm
                ⟨(trivial k G k).leftRegularHom 1, ⋯⟩)).τ₂,
        zero := ⋯ }.Exact ∧
    Epi
      ((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).map
          ((((chainComplexFunctor k g).obj (leftRegular k G)).toSingle₀Equiv (trivial k G k)).symm
            ⟨(trivial k G k).leftRegularHom 1, ⋯⟩)).τ₂
Module: Mathlib.RepresentationTheory.Homological.ContCohomology.LowDegree

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝⁴ : Ring k
inst✝³ : Group G
inst✝² : TopologicalSpace k
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
σ : ↑(X.homogeneousCochains.X 0).toModuleCat
hσ : (X.resolutionX (0 + 1)).ρ.coind₁ι ↑σ = (Hom.hom ((coind₁Functor k G).map (ofHom X.ρ.coind₁ι))) ↑σ
g : G
⊢ (X.ρ g) (↑σ 1) = ↑σ 1

Tactic:
]

Goal state after:
k : Type u_1
G : Type u_2
inst✝⁴ : Ring k
inst✝³ : Group G
inst✝² : TopologicalSpace k
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
σ : ↑(X.homogeneousCochains.X 0).toModuleCat
hσ : (X.resolutionX (0 + 1)).ρ.coind₁ι ↑σ = (Hom.hom ((coind₁Functor k G).map (ofHom X.ρ.coind₁ι))) ↑σ
g : G
⊢ (X.ρ g) (↑σ 1) = ↑σ 1
Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic

Goal state before:
pp: case zero.right
k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
⊢ Function.Surjective
    ⇑(Hom.hom
        ((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).map
            ((((chainComplexFunctor k g).obj (leftRegular k G)).toSingle₀Equiv (trivial k G k)).symm
              ⟨(trivial k G k).leftRegularHom 1, ⋯⟩)).τ₂)

Tactic:
]

Goal state after:
case zero.right
k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
⊢ Function.Surjective
    ⇑(Hom.hom
        ((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).map
            ((((chainComplexFunctor k g).obj (leftRegular k G)).toSingle₀Equiv (trivial k G k)).symm
              ⟨(trivial k G k).leftRegularHom 1, ⋯⟩)).τ₂)
Module: Mathlib.RepresentationTheory.Homological.ContCohomology.LowDegree

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝⁴ : Ring k
inst✝³ : Group G
inst✝² : TopologicalSpace k
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
x : ↑X
h : ContinuousMap.const G x ∈ (X.resolution'.X 0).ρ.invariants
⊢ (Hom.hom (X.d (0 + 1))) ↑⟨ContinuousMap.const G x, h⟩ = ↑0

Tactic:
]

Goal state after:
k : Type u_1
G : Type u_2
inst✝⁴ : Ring k
inst✝³ : Group G
inst✝² : TopologicalSpace k
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
x : ↑X
h : ContinuousMap.const G x ∈ (X.resolution'.X 0).ρ.invariants
⊢ (Hom.hom (X.d (0 + 1))) ↑⟨ContinuousMap.const G x, h⟩ = ↑0
Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic

Goal state before:
pp: case succ
k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
m : ℕ
a✝ : QuasiIsoAt (resolution.π k g) m
⊢ (HomologicalComplex.sc' ((chainComplexFunctor k g).obj (leftRegular k G)) (m + 2) (m + 1) m).Exact

Tactic:
]

Goal state after:
case succ
k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
m : ℕ
a✝ : QuasiIsoAt (resolution.π k g) m
⊢ (HomologicalComplex.sc' ((chainComplexFunctor k g).obj (leftRegular k G)) (m + 2) (m + 1) m).Exact
Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic

Goal state before:
pp: case succ
k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
m : ℕ
a✝ : QuasiIsoAt (resolution.π k g) m
⊢ (ModuleCat.Hom.hom
        ((HomologicalComplex.sc' ((chainComplexFunctor k g).obj (leftRegular k G)) (m + 2) (m + 1) m).map
            (forget₂ (Rep k G) (ModuleCat k))).f).range =
    (ModuleCat.Hom.hom
        ((HomologicalComplex.sc' ((chainComplexFunctor k g).obj (leftRegular k G)) (m + 2) (m + 1) m).map
            (forget₂ (Rep k G) (ModuleCat k))).g).ker

Tactic:
]

Goal state after:
case succ
k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
m : ℕ
a✝ : QuasiIsoAt (resolution.π k g) m
⊢ (ModuleCat.Hom.hom
        ((HomologicalComplex.sc' ((chainComplexFunctor k g).obj (leftRegular k G)) (m + 2) (m + 1) m).map
            (forget₂ (Rep k G) (ModuleCat k))).f).range =
    (ModuleCat.Hom.hom
        ((HomologicalComplex.sc' ((chainComplexFunctor k g).obj (leftRegular k G)) (m + 2) (m + 1) m).map
            (forget₂ (Rep k G) (ModuleCat k))).g).ker
Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic

Goal state before:
pp: case pos
k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
m : ℕ
a✝ : QuasiIsoAt (resolution.π k g) m
hm : Odd (m + 1)
⊢ (ModuleCat.Hom.hom
        ((HomologicalComplex.sc' ((chainComplexFunctor k g).obj (leftRegular k G)) (m + 2) (m + 1) m).map
            (forget₂ (Rep k G) (ModuleCat k))).f).range =
    (ModuleCat.Hom.hom
        ((HomologicalComplex.sc' ((chainComplexFunctor k g).obj (leftRegular k G)) (m + 2) (m + 1) m).map
            (forget₂ (Rep k G) (ModuleCat k))).g).ker

Tactic:
simpa [if_pos (Nat.even_add_one.2 (Nat.not_even_iff_odd.2 hm)),
          if_neg (Nat.not_even_iff_odd.2 hm)]
          using! leftRegular.range_norm_eq_ker_applyAsHom_sub k g hg

Goal state after: