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

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁶ : Semiring k
inst✝⁵ : Monoid G
inst✝⁴ : Monoid H
φ : G →* H
A : Type u_4
B : Type u_5
inst✝³ : AddCommMonoid A
inst✝² : Module k A
inst✝¹ : AddCommMonoid B
inst✝ : Module k B
σ : Representation k G A
ρ : Representation k G B
f : σ.IntertwiningMap ρ
x : H → A
h : ∀ (g : G) (h : H), x (φ g * h) = (σ g) (x h)
g : G
h0 : H
⊢ f (x (φ g * h0)) = (ρ g) (f (x h0))

Tactic:
simpa using

Goal state after:
k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁶ : Semiring k
inst✝⁵ : Monoid G
inst✝⁴ : Monoid H
φ : G →* H
A : Type u_4
B : Type u_5
inst✝³ : AddCommMonoid A
inst✝² : Module k A
inst✝¹ : AddCommMonoid B
inst✝ : Module k B
σ : Representation k G A
ρ : Representation k G B
f : σ.IntertwiningMap ρ
x : H → A
h : ∀ (g : G) (h : H), x (φ g * h) = (σ g) (x h)
g : G
h0 : H
⊢ f ((σ g) (x h0)) = (ρ g) (f (x h0))
Module: Mathlib.RepresentationTheory.Coinduced

Goal state before:
pp: k : Type u
G : Type v
H : Type w
inst✝² : CommRing k
inst✝¹ : Monoid G
inst✝ : Monoid H
φ : G →* H
A : Rep k G
f g : ↑(coind' φ A)
hfg : ∀ (h : H), (Hom.hom f).toLinearMap (MonoidAlgebra.single h 1) = (Hom.hom g).toLinearMap (MonoidAlgebra.single h 1)
h : H
⊢ ((Hom.hom f).toLinearMap ∘ₗ MonoidAlgebra.lsingle h) 1 = ((Hom.hom g).toLinearMap ∘ₗ MonoidAlgebra.lsingle h) 1

Tactic:
simpa using

Goal state after:
k : Type u
G : Type v
H : Type w
inst✝² : CommRing k
inst✝¹ : Monoid G
inst✝ : Monoid H
φ : G →* H
A : Rep k G
f g : ↑(coind' φ A)
hfg : ∀ (h : H), (Hom.hom f).toLinearMap (MonoidAlgebra.single h 1) = (Hom.hom g).toLinearMap (MonoidAlgebra.single h 1)
h : H
⊢ (Hom.hom f) (MonoidAlgebra.single h 1) = (Hom.hom g) (MonoidAlgebra.single h 1)
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
X : Type u_5
inst✝⁷ : CommRing k
inst✝⁶ : Monoid G
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : AddCommGroup W
inst✝² : Module k W
inst✝¹ : AddCommGroup X
inst✝ : Module k X
ρ : Representation k G V
τ : Representation k G W
υ : Representation k G X
f : V →ₗ[k] W
h : ∀ (x : G), f ∘ₗ ρ x = f
x : V
x✝ : x ∈ Set.range fun gv ↦ (ρ gv.1) gv.2 - gv.2
g : G
y : V
hy : (fun gv ↦ (ρ gv.1) gv.2 - gv.2) (g, y) = x
⊢ x ∈ ↑f.ker

Tactic:
simpa using

Goal state after:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
X : Type u_5
inst✝⁷ : CommRing k
inst✝⁶ : Monoid G
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : AddCommGroup W
inst✝² : Module k W
inst✝¹ : AddCommGroup X
inst✝ : Module k X
ρ : Representation k G V
τ : Representation k G W
υ : Representation k G X
f : V →ₗ[k] W
h : ∀ (x : G), f ∘ₗ ρ x = f
x : V
x✝ : x ∈ Set.range fun gv ↦ (ρ gv.1) gv.2 - gv.2
g : G
y : V
hy : (fun gv ↦ (ρ gv.1) gv.2 - gv.2) (g, y) = x
⊢ f ((ρ g) y) = f y
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
X : Type u_5
inst✝⁷ : CommRing k
inst✝⁶ : Monoid G
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : AddCommGroup W
inst✝² : Module k W
inst✝¹ : AddCommGroup X
inst✝ : Module k X
ρ : Representation k G V
τ : Representation k G W
υ : Representation k G X
f : ρ.IntertwiningMap τ
g : G
x : V
⊢ (τ g) (f x) - f x = ↑f ((ρ g) x) - ↑f x

Tactic:
simpa using

Goal state after:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
X : Type u_5
inst✝⁷ : CommRing k
inst✝⁶ : Monoid G
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : AddCommGroup W
inst✝² : Module k W
inst✝¹ : AddCommGroup X
inst✝ : Module k X
ρ : Representation k G V
τ : Representation k G W
υ : Representation k G X
f : ρ.IntertwiningMap τ
g : G
x : V
⊢ (τ g) (f x) = f ((ρ g) x)
Module: Mathlib.RepresentationTheory.Coinduced

Goal state before:
pp: k : Type u
G : Type v
H : Type w
inst✝² : CommRing k
inst✝¹ : Monoid G
inst✝ : Monoid H
φ : G →* H
A : Rep k G
f : res φ (leftRegular k H) ⟶ A
g : G
h : H
⊢ ?m.240

Tactic:
simpa using

Goal state after:
k : Type u
G : Type v
H : Type w
inst✝² : CommRing k
inst✝¹ : Monoid G
inst✝ : Monoid H
φ : G →* H
A : Rep k G
f : res φ (leftRegular k H) ⟶ A
g : G
h : H
⊢ ?m.240
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k : Type u_6
G : Type u_7
V : Type u_8
inst✝⁴ : CommRing k
inst✝³ : Group G
inst✝² : AddCommGroup V
inst✝¹ : Module k V
ρ : Representation k G V
S : Subgroup G
inst✝ : S.Normal
g : G
x✝¹ : V
x✝ : x✝¹ ∈ Set.range fun gv ↦ ((MonoidHom.comp ρ S.subtype) gv.1) gv.2 - gv.2
s : ↥S
x : V
hs : (fun gv ↦ ((MonoidHom.comp ρ S.subtype) gv.1) gv.2 - gv.2) (s, x) = x✝¹
⊢ x✝¹ ∈ ↑(Submodule.comap (ρ g) (ker (MonoidHom.comp ρ S.subtype)))

Tactic:
simpa using

Goal state after:
k : Type u_6
G : Type u_7
V : Type u_8
inst✝⁴ : CommRing k
inst✝³ : Group G
inst✝² : AddCommGroup V
inst✝¹ : Module k V
ρ : Representation k G V
S : Subgroup G
inst✝ : S.Normal
g : G
x✝¹ : V
x✝ : x✝¹ ∈ Set.range fun gv ↦ ((MonoidHom.comp ρ S.subtype) gv.1) gv.2 - gv.2
s : ↥S
x : V
hs : (fun gv ↦ ((MonoidHom.comp ρ S.subtype) gv.1) gv.2 - gv.2) (s, x) = x✝¹
⊢ (ρ g) ((ρ ↑s) x) - (ρ g) x ∈ ker (MonoidHom.comp ρ S.subtype)
Module: Mathlib.RepresentationTheory.Coinduced

Goal state before:
pp: k : Type u
G : Type v
H : Type w
inst✝² : CommRing k
inst✝¹ : Monoid G
inst✝ : Monoid H
φ : G →* H
A✝ : Rep k G
B : Rep k H
A : Rep k G
f : res φ B ⟶ A
x✝² : ↑B
x✝¹ : G
x✝ : H
⊢ (LinearMap.pi fun h ↦ (Hom.hom f).toLinearMap ∘ₗ B.ρ h) x✝² (φ x✝¹ * x✝) =
    (A.ρ x✝¹) ((LinearMap.pi fun h ↦ (Hom.hom f).toLinearMap ∘ₗ B.ρ h) x✝² x✝)

Tactic:
simpa using

Goal state after:
k : Type u
G : Type v
H : Type w
inst✝² : CommRing k
inst✝¹ : Monoid G
inst✝ : Monoid H
φ : G →* H
A✝ : Rep k G
B : Rep k H
A : Rep k G
f : res φ B ⟶ A
x✝² : ↑B
x✝¹ : G
x✝ : H
⊢ (Hom.hom f) ((B.ρ (φ x✝¹)) ((B.ρ x✝) x✝²)) = (A.ρ x✝¹) ((Hom.hom f) ((B.ρ x✝) x✝²))
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
I : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), X i ω = 0
ω : Ω
hω : ∀ (i : ℕ), X i ω = 0
⊢ Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))

Tactic:
simpa using

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
I : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), X i ω = 0
ω : Ω
hω : ∀ (i : ℕ), X i ω = 0
⊢ 0 = ∫ (x : Ω), X 0 x ∂μ
Module: Mathlib.RepresentationTheory.Continuous.TopRep

Goal state before:
pp: k : Type u
G : Type v
X✝ Y✝ : Type w
inst✝¹² : TopologicalSpace k
inst✝¹¹ : Ring k
inst✝¹⁰ : Monoid G
inst✝⁹ : AddCommGroup X✝
inst✝⁸ : Module k X✝
inst✝⁷ : TopologicalSpace X✝
inst✝⁶ : IsTopologicalAddGroup X✝
inst✝⁵ : ContinuousSMul k X✝
inst✝⁴ : AddCommGroup Y✝
inst✝³ : Module k Y✝
inst✝² : TopologicalSpace Y✝
inst✝¹ : IsTopologicalAddGroup Y✝
inst✝ : ContinuousSMul k Y✝
ρ : ContRepresentation k G X✝
σ : ContRepresentation k G Y✝
A B C : TopRep k G
X Y : Action (TopModuleCat k) G
f : X ⟶ Y
g : G
⊢ TopModuleCat.Hom.hom f.hom ∘SL { toMonoidHom := X.V.endRingEquiv.toMonoidHom.comp X.ρ } g =
    { toMonoidHom := Y.V.endRingEquiv.toMonoidHom.comp Y.ρ } g ∘SL TopModuleCat.Hom.hom f.hom

Tactic:
simpa using

Goal state after:
k : Type u
G : Type v
X✝ Y✝ : Type w
inst✝¹² : TopologicalSpace k
inst✝¹¹ : Ring k
inst✝¹⁰ : Monoid G
inst✝⁹ : AddCommGroup X✝
inst✝⁸ : Module k X✝
inst✝⁷ : TopologicalSpace X✝
inst✝⁶ : IsTopologicalAddGroup X✝
inst✝⁵ : ContinuousSMul k X✝
inst✝⁴ : AddCommGroup Y✝
inst✝³ : Module k Y✝
inst✝² : TopologicalSpace Y✝
inst✝¹ : IsTopologicalAddGroup Y✝
inst✝ : ContinuousSMul k Y✝
ρ : ContRepresentation k G X✝
σ : ContRepresentation k G Y✝
A B C : TopRep k G
X Y : Action (TopModuleCat k) G
f : X ⟶ Y
g : G
⊢ TopModuleCat.Hom.hom f.hom ∘SL TopModuleCat.Hom.hom (X.ρ g) =
    TopModuleCat.Hom.hom (Y.ρ g) ∘SL TopModuleCat.Hom.hom f.hom
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Semiring k
inst✝ : Monoid G
A B : Rep k G
f : A ⟶ B
g : G
a : ↑A
⊢ (Hom.hom f) ((A.ρ g) a) = (B.ρ g) ((Hom.hom f) a)

Tactic:
simpa using

Goal state after:
k : Type u
G : Type v
inst✝¹ : Semiring k
inst✝ : Monoid G
A B : Rep k G
f : A ⟶ B
g : G
a : ↑A
⊢ (Hom.hom f) ((A.ρ g) a) = (B.ρ g) ((Hom.hom f) a)
Module: Mathlib.RepresentationTheory.Continuous.Basic

Goal state before:
pp: case mk''.mk''
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁹ : Monoid G
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace V
inst✝⁵ : IsTopologicalAddGroup V
inst✝⁴ : Module R V
inst✝³ : AddCommGroup W
inst✝² : TopologicalSpace W
inst✝¹ : IsTopologicalAddGroup W
inst✝ : Module R W
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
toContinuousLinearEquiv✝¹ : W ≃L[R] V
cont✝¹ : Continuous (↑↑toContinuousLinearEquiv✝¹).toFun
isIntertwining'✝¹ :
  ∀ (g : G),
    { toLinearMap := ↑↑toContinuousLinearEquiv✝¹, cont := cont✝¹ } ∘SL σ g =
      ρ g ∘SL { toLinearMap := ↑↑toContinuousLinearEquiv✝¹, cont := cont✝¹ }
toContinuousLinearEquiv✝ : W ≃L[R] V
cont✝ : Continuous (↑↑toContinuousLinearEquiv✝).toFun
isIntertwining'✝ :
  ∀ (g : G),
    { toLinearMap := ↑↑toContinuousLinearEquiv✝, cont := cont✝ } ∘SL σ g =
      ρ g ∘SL { toLinearMap := ↑↑toContinuousLinearEquiv✝, cont := cont✝ }
h :
  { toContinuousLinearEquiv := toContinuousLinearEquiv✝¹, cont := cont✝¹,
        isIntertwining' := isIntertwining'✝¹ }.toContinuousLinearEquiv =
    { toContinuousLinearEquiv := toContinuousLinearEquiv✝, cont := cont✝,
        isIntertwining' := isIntertwining'✝ }.toContinuousLinearEquiv
⊢ { toContinuousLinearEquiv := toContinuousLinearEquiv✝¹, cont := cont✝¹, isIntertwining' := isIntertwining'✝¹ } =
    { toContinuousLinearEquiv := toContinuousLinearEquiv✝, cont := cont✝, isIntertwining' := isIntertwining'✝ }

Tactic:
simpa using

Goal state after:
case mk''.mk''
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁹ : Monoid G
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace V
inst✝⁵ : IsTopologicalAddGroup V
inst✝⁴ : Module R V
inst✝³ : AddCommGroup W
inst✝² : TopologicalSpace W
inst✝¹ : IsTopologicalAddGroup W
inst✝ : Module R W
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
toContinuousLinearEquiv✝¹ : W ≃L[R] V
cont✝¹ : Continuous (↑↑toContinuousLinearEquiv✝¹).toFun
isIntertwining'✝¹ :
  ∀ (g : G),
    { toLinearMap := ↑↑toContinuousLinearEquiv✝¹, cont := cont✝¹ } ∘SL σ g =
      ρ g ∘SL { toLinearMap := ↑↑toContinuousLinearEquiv✝¹, cont := cont✝¹ }
toContinuousLinearEquiv✝ : W ≃L[R] V
cont✝ : Continuous (↑↑toContinuousLinearEquiv✝).toFun
isIntertwining'✝ :
  ∀ (g : G),
    { toLinearMap := ↑↑toContinuousLinearEquiv✝, cont := cont✝ } ∘SL σ g =
      ρ g ∘SL { toLinearMap := ↑↑toContinuousLinearEquiv✝, cont := cont✝ }
h :
  { toContinuousLinearEquiv := toContinuousLinearEquiv✝¹, cont := cont✝¹,
        isIntertwining' := isIntertwining'✝¹ }.toContinuousLinearEquiv =
    { toContinuousLinearEquiv := toContinuousLinearEquiv✝, cont := cont✝,
        isIntertwining' := isIntertwining'✝ }.toContinuousLinearEquiv
⊢ toContinuousLinearEquiv✝¹ = toContinuousLinearEquiv✝
Module: Mathlib.RepresentationTheory.Continuous.Basic

Goal state before:
pp: case mk''.mk''
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁹ : Monoid G
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace V
inst✝⁵ : IsTopologicalAddGroup V
inst✝⁴ : Module R V
inst✝³ : AddCommGroup W
inst✝² : TopologicalSpace W
inst✝¹ : IsTopologicalAddGroup W
inst✝ : Module R W
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
toContinuousLinearEquiv✝¹ : V ≃L[R] W
cont✝¹ : Continuous (↑↑toContinuousLinearEquiv✝¹).toFun
isIntertwining'✝¹ :
  ∀ (g : G),
    { toLinearMap := ↑↑toContinuousLinearEquiv✝¹, cont := cont✝¹ } ∘SL ρ g =
      σ g ∘SL { toLinearMap := ↑↑toContinuousLinearEquiv✝¹, cont := cont✝¹ }
toContinuousLinearEquiv✝ : V ≃L[R] W
cont✝ : Continuous (↑↑toContinuousLinearEquiv✝).toFun
isIntertwining'✝ :
  ∀ (g : G),
    { toLinearMap := ↑↑toContinuousLinearEquiv✝, cont := cont✝ } ∘SL ρ g =
      σ g ∘SL { toLinearMap := ↑↑toContinuousLinearEquiv✝, cont := cont✝ }
h :
  ⇑{ toContinuousLinearEquiv := toContinuousLinearEquiv✝¹, cont := cont✝¹, isIntertwining' := isIntertwining'✝¹ } =
    ⇑{ toContinuousLinearEquiv := toContinuousLinearEquiv✝, cont := cont✝, isIntertwining' := isIntertwining'✝ }
⊢ { toContinuousLinearEquiv := toContinuousLinearEquiv✝¹, cont := cont✝¹, isIntertwining' := isIntertwining'✝¹ } =
    { toContinuousLinearEquiv := toContinuousLinearEquiv✝, cont := cont✝, isIntertwining' := isIntertwining'✝ }

Tactic:
simpa using

Goal state after:
case mk''.mk''
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁹ : Monoid G
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace V
inst✝⁵ : IsTopologicalAddGroup V
inst✝⁴ : Module R V
inst✝³ : AddCommGroup W
inst✝² : TopologicalSpace W
inst✝¹ : IsTopologicalAddGroup W
inst✝ : Module R W
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
toContinuousLinearEquiv✝¹ : V ≃L[R] W
cont✝¹ : Continuous (↑↑toContinuousLinearEquiv✝¹).toFun
isIntertwining'✝¹ :
  ∀ (g : G),
    { toLinearMap := ↑↑toContinuousLinearEquiv✝¹, cont := cont✝¹ } ∘SL ρ g =
      σ g ∘SL { toLinearMap := ↑↑toContinuousLinearEquiv✝¹, cont := cont✝¹ }
toContinuousLinearEquiv✝ : V ≃L[R] W
cont✝ : Continuous (↑↑toContinuousLinearEquiv✝).toFun
isIntertwining'✝ :
  ∀ (g : G),
    { toLinearMap := ↑↑toContinuousLinearEquiv✝, cont := cont✝ } ∘SL ρ g =
      σ g ∘SL { toLinearMap := ↑↑toContinuousLinearEquiv✝, cont := cont✝ }
h :
  ⇑{ toContinuousLinearEquiv := toContinuousLinearEquiv✝¹, cont := cont✝¹, isIntertwining' := isIntertwining'✝¹ } =
    ⇑{ toContinuousLinearEquiv := toContinuousLinearEquiv✝, cont := cont✝, isIntertwining' := isIntertwining'✝ }
⊢ toContinuousLinearEquiv✝¹ = toContinuousLinearEquiv✝
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
A B C : Rep k G
X✝ Y✝ : Action (ModuleCat k) G
f : X✝ ⟶ Y✝
g : G
⊢ ModuleCat.Hom.hom f.hom ∘ₗ (X✝.V.endRingEquiv.toMonoidHom.comp X✝.ρ) g =
    (Y✝.V.endRingEquiv.toMonoidHom.comp Y✝.ρ) g ∘ₗ ModuleCat.Hom.hom f.hom

Tactic:
simpa using

Goal state after:
k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
A B C : Rep k G
X✝ Y✝ : Action (ModuleCat k) G
f : X✝ ⟶ Y✝
g : G
⊢ ModuleCat.Hom.hom f.hom ∘ₗ ModuleCat.Hom.hom (X✝.ρ g) = ModuleCat.Hom.hom (Y✝.ρ g) ∘ₗ ModuleCat.Hom.hom f.hom
Module: Mathlib.RepresentationTheory.FinGroupCharZero

Goal state before:
pp: case refine_2
k : Type u
inst✝⁴ : Field k
G : Type u
inst✝³ : Finite G
inst✝² : Group G
inst✝¹ : IsAlgClosed k
inst✝ : NeZero ↑(Nat.card G)
V : FDRep k G
h : Module.finrank k (V ⟶ V) = 1
W : FDRep k G
f : W ⟶ V
x✝ : Mono f
ι : Abelian.image f ⟶ V := Abelian.image.ι f
hf : Abelian.factorThruImage f ≫ ι ≠ 0
φ : V ⟶ Abelian.image f := Injective.factorThru (𝟙 (Abelian.image f)) ι
hφι : φ ≫ ι ≠ 0
c : k
R✝ : FDRep k G
g : V ⟶ R✝
hg : ι ≫ g = 0
hc : (c • φ ≫ ι) ≫ g = 𝟙 V ≫ g
⊢ g = 0

Tactic:
simpa using

Goal state after:
case refine_2
k : Type u
inst✝⁴ : Field k
G : Type u
inst✝³ : Finite G
inst✝² : Group G
inst✝¹ : IsAlgClosed k
inst✝ : NeZero ↑(Nat.card G)
V : FDRep k G
h : Module.finrank k (V ⟶ V) = 1
W : FDRep k G
f : W ⟶ V
x✝ : Mono f
ι : Abelian.image f ⟶ V := Abelian.image.ι f
hf : Abelian.factorThruImage f ≫ ι ≠ 0
φ : V ⟶ Abelian.image f := Injective.factorThru (𝟙 (Abelian.image f)) ι
hφι : φ ≫ ι ≠ 0
c : k
R✝ : FDRep k G
g : V ⟶ R✝
hg : ι ≫ g = 0
hc : (c • φ ≫ ι) ≫ g = 𝟙 V ≫ g
⊢ g = 0
Module: Mathlib.RepresentationTheory.FinGroupCharZero

Goal state before:
pp: case mp
k : Type u
inst✝⁴ : Field k
G : Type u
inst✝³ : Group G
inst✝² : IsAlgClosed k
inst✝¹ : CharZero k
inst✝ : Fintype G
V : FDRep k G
this : Invertible ↑(Nat.card G)
h : Simple V
⊢ ↑(Nat.card G) = ∑ g, V.character g * V.character g⁻¹

Tactic:
simpa using

Goal state after:
case mp
k : Type u
inst✝⁴ : Field k
G : Type u
inst✝³ : Group G
inst✝² : IsAlgClosed k
inst✝¹ : CharZero k
inst✝ : Fintype G
V : FDRep k G
this : Invertible ↑(Nat.card G)
h : Simple V
⊢ ↑(Fintype.card G) = ∑ g, V.character g * V.character g⁻¹
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G✝ : Type v
inst✝² : CommRing k
inst✝¹ : Monoid G✝
G : Type v
inst✝ : Group G
A✝ B✝ C✝ : Rep k G
A B C : Rep k G
f : A ⊗ B ⟶ C
g : G
x : ↑B
y : ↑A
⊢ ?m.292

Tactic:
simpa using

Goal state after:
k : Type u
G✝ : Type v
inst✝² : CommRing k
inst✝¹ : Monoid G✝
G : Type v
inst✝ : Group G
A✝ B✝ C✝ : Rep k G
A B C : Rep k G
f : A ⊗ B ⟶ C
g : G
x : ↑B
y : ↑A
⊢ ?m.292
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G✝ : Type v
inst✝² : CommRing k
inst✝¹ : Monoid G✝
G : Type v
inst✝ : Group G
A✝ B✝ C✝ : Rep k G
A B C : Rep k G
f : B ⟶ A.ihom.obj C
g : G
x : ↑A
y : ↑B
⊢ ((TensorProduct.uncurry (RingHom.id k) ↑A ↑B ↑C) (Hom.hom f).flip ∘ₗ (A.ρ.tprod B.ρ) g) (x ⊗ₜ[k] y) =
    (C.ρ g ∘ₗ (TensorProduct.uncurry (RingHom.id k) ↑A ↑B ↑C) (Hom.hom f).flip) (x ⊗ₜ[k] y)

Tactic:
simpa using

Goal state after:
k : Type u
G✝ : Type v
inst✝² : CommRing k
inst✝¹ : Monoid G✝
G : Type v
inst✝ : Group G
A✝ B✝ C✝ : Rep k G
A B C : Rep k G
f : B ⟶ A.ihom.obj C
g : G
x : ↑A
y : ↑B
⊢ ((Hom.hom f) ((B.ρ g) y)) ((A.ρ g) x) = (C.ρ g) (((Hom.hom f) y) x)
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y Z : Action (Type u) G
⊢ Hom.hom
      (ofHom (δ (X ⊗ Y) Z) ≫
        ofHom (δ X Y) ▷ (linearization k G).obj Z ≫
          (α_ ((linearization k G).obj X) ((linearization k G).obj Y) ((linearization k G).obj Z)).hom) =
    Hom.hom ((linearization k G).map (α_ X Y Z).hom ≫ ofHom (δ X (Y ⊗ Z)) ≫ (linearization k G).obj X ◁ ofHom (δ Y Z))

Tactic:
simpa using

Goal state after:
k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y Z : Action (Type u) G
⊢ ((↑(Representation.TensorProduct.assoc (Representation.linearize k G X) (Representation.linearize k G Y)
                (Representation.linearize k G Z))).comp
          (Representation.IntertwiningMap.rTensor (Representation.linearize k G Z) (δ X Y))).comp
      (δ (X ⊗ Y) Z) =
    ((Representation.IntertwiningMap.lTensor (Representation.linearize k G X) (δ Y Z)).comp (δ X (Y ⊗ Z))).comp
      (Representation.linearizeMap (α_ X Y Z).hom)
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
g₁ g₂ g₃ : G
a : ↑A
⊢ (A.indToCoindAux (g₁ * g₂⁻¹)) a g₃ = (A.indToCoindAux g₁) a (g₃ * g₂)

Tactic:
simpa using

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
g₁ g₂ g₃ : G
a : ↑A
⊢ (A.indToCoindAux (g₁ * g₂⁻¹)) a g₃ = (A.indToCoindAux g₁) a (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
inst✝¹ : DecidableRel ⇑(QuotientGroup.rightRel S)
A : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
x✝¹ x✝ : ↑(coind.{u, v, v, w} S.subtype A)
⊢ ∑ g, g.liftOn (fun g ↦ (IndV.mk S.subtype A.ρ g) (↑(x✝¹ + x✝) g)) ⋯ =
    ∑ g, g.liftOn (fun g ↦ (IndV.mk S.subtype A.ρ g) (↑x✝¹ g)) ⋯ +
      ∑ g, g.liftOn (fun g ↦ (IndV.mk S.subtype A.ρ g) (↑x✝ g)) ⋯

Tactic:
simpa using

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
x✝¹ x✝ : ↑(coind.{u, v, v, w} S.subtype A)
⊢ ∑ x,
      x.liftOn
        (fun g ↦
          (Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ))
              (MonoidAlgebra.single g 1 ⊗ₜ[k] ↑x✝¹ g) +
            (Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ))
              (MonoidAlgebra.single g 1 ⊗ₜ[k] ↑x✝ g))
        ⋯ =
    ∑ x,
      (x.liftOn
          (fun g ↦
            (Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ))
              (MonoidAlgebra.single g 1 ⊗ₜ[k] ↑x✝¹ g))
          ⋯ +
        x.liftOn
          (fun g ↦
            (Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ))
              (MonoidAlgebra.single g 1 ⊗ₜ[k] ↑x✝ 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)
A : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
x✝¹ : k
x✝ : ↑(coind.{u, v, v, w} S.subtype A)
⊢ ∑ g, g.liftOn (fun g ↦ (IndV.mk S.subtype A.ρ g) (↑(x✝¹ • x✝) g)) ⋯ =
    (RingHom.id k) x✝¹ • ∑ g, g.liftOn (fun g ↦ (IndV.mk S.subtype A.ρ g) (↑x✝ g)) ⋯

Tactic:
simpa using

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
x✝¹ : k
x✝ : ↑(coind.{u, v, v, w} S.subtype A)
⊢ ∑ x,
      x.liftOn
        (fun g ↦
          x✝¹ •
            (Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ))
              (MonoidAlgebra.single g 1 ⊗ₜ[k] ↑x✝ g))
        ⋯ =
    ∑ x,
      x✝¹ •
        x.liftOn
          (fun g ↦
            (Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ))
              (MonoidAlgebra.single g 1 ⊗ₜ[k] ↑x✝ g))
          ⋯
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: case h₀.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 b : G
a✝ : ⟦b⟧ ∈ Finset.univ
hb : ⟦b⟧ ≠ ⟦a⟧
⊢ ↑(A.indToCoind (⟦b⟧.liftOn (fun g_1 ↦ (IndV.mk S.subtype A.ρ g_1) (↑g g_1)) ⋯)) a = 0

Tactic:
simpa using

Goal state after:
case h₀.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 b : G
a✝ : ⟦b⟧ ∈ Finset.univ
hb : ⟦b⟧ ≠ ⟦a⟧
⊢ (A.indToCoindAux b) (↑g b) a = 0
Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic

Goal state before:
pp: case h
k : Type u_1
G : Type u_2
inst✝⁴ : CommRing k
inst✝³ : Group G
V : Type u_4
inst✝² : AddCommGroup V
inst✝¹ : Module k V
ρ : Representation k G V
g : G
inst✝ : Finite G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
α : V
n : ℕ
a✝ : (fun gv ↦ (ρ gv.1) gv.2 - gv.2) ((fun x ↦ g ^ x) n, α) ∈ ↑(ρ g - LinearMap.id).range
⊢ (ρ g - LinearMap.id) (Fin.partialSum (fun j ↦ (ρ (g ^ ↑j)) α) (Fin.last (n + 1))) =
    (fun gv ↦ (ρ gv.1) gv.2 - gv.2) ((fun x ↦ g ^ x) (n + 1), α)

Tactic:
simpa using

Goal state after:
case h
k : Type u_1
G : Type u_2
inst✝⁴ : CommRing k
inst✝³ : Group G
V : Type u_4
inst✝² : AddCommGroup V
inst✝¹ : Module k V
ρ : Representation k G V
g : G
inst✝ : Finite G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
α : V
n : ℕ
a✝ : (fun gv ↦ (ρ gv.1) gv.2 - gv.2) ((fun x ↦ g ^ x) n, α) ∈ ↑(ρ g - LinearMap.id).range
⊢ (ρ g) (Fin.partialSum (fun j ↦ (ρ g ^ ↑j) α) (Fin.last (n + 1))) -
      Fin.partialSum (fun j ↦ (ρ g ^ ↑j) α) (Fin.last (n + 1)) =
    (ρ g ^ (n + 1)) α - α