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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : Monoid G
inst✝² : Field k
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module k[G] M
⊢ ComplementedLattice (Submodule k[G] M) ↔ (ofModule M).IsSemisimpleRepresentation

Tactic:
]

Goal state after:
k : Type u_1
G : Type u_2
inst✝³ : Monoid G
inst✝² : Field k
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module k[G] M
⊢ ComplementedLattice (Submodule k[G] M) ↔ (ofModule M).IsSemisimpleRepresentation
Module: Mathlib.RepresentationTheory.Maschke

Goal state before:
pp: k : Type u_1
inst✝⁹ : CommRing k
G : Type u_2
inst✝⁸ : Group G
V : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : Module k[G] V
inst✝⁴ : IsScalarTower k k[G] V
W : Type u_4
inst✝³ : AddCommGroup W
inst✝² : Module k W
inst✝¹ : Module k[G] W
inst✝ : IsScalarTower k k[G] W
π : W →ₗ[k] V
i : V →ₗ[k[G]] W
h : ∀ (v : V), π (i v) = v
g : G
v : V
⊢ v = v

Tactic:
]

Goal state after:
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
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
⊢ ∀ (i : ℕ), ∀ᵐ (a : Ω) ∂μ, X i a = 0

Tactic:
]

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
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
⊢ ∀ (i : ℕ), ∀ᵐ (a : Ω) ∂μ, X i a = 0
Module: Mathlib.RepresentationTheory.Maschke

Goal state before:
pp: k : Type u_1
inst✝¹⁰ : CommRing k
G : Type u_2
inst✝⁹ : Group G
V : Type u_3
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : Module k[G] V
inst✝⁵ : IsScalarTower k k[G] V
W : Type u_4
inst✝⁴ : AddCommGroup W
inst✝³ : Module k W
inst✝² : Module k[G] W
inst✝¹ : IsScalarTower k k[G] W
π : W →ₗ[k] V
i : V →ₗ[k[G]] W
inst✝ : Fintype G
hcard : IsUnit ↑(Nat.card G)
h : ∀ (v : V), π (i v) = v
v : V
⊢ (↑(Nat.card G))⁻¹ʳ • ∑ g, (π.conjugate g) (i v) = v

Tactic:
]

Goal state after:
k : Type u_1
inst✝¹⁰ : CommRing k
G : Type u_2
inst✝⁹ : Group G
V : Type u_3
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : Module k[G] V
inst✝⁵ : IsScalarTower k k[G] V
W : Type u_4
inst✝⁴ : AddCommGroup W
inst✝³ : Module k W
inst✝² : Module k[G] W
inst✝¹ : IsScalarTower k k[G] W
π : W →ₗ[k] V
i : V →ₗ[k[G]] W
inst✝ : Fintype G
hcard : IsUnit ↑(Nat.card G)
h : ∀ (v : V), π (i v) = v
v : V
⊢ (↑(Nat.card G))⁻¹ʳ • ∑ g, (π.conjugate g) (i v) = v
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case neg
Ω : 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
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
this : IsProbabilityMeasure μ
hmeas : ∀ (i : ℕ), AEStronglyMeasurable (X i) μ
hint : Integrable (X 0) μ
havg : ∀ (n : ℕ), AEStronglyMeasurable (fun ω ↦ (↑n)⁻¹ • ∑ i ∈ range n, X i ω) μ
⊢ UnifIntegrable (fun n ↦ (↑n)⁻¹ • ∑ i ∈ range n, X i) p μ

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
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
this : IsProbabilityMeasure μ
hmeas : ∀ (i : ℕ), AEStronglyMeasurable (X i) μ
hint : Integrable (X 0) μ
havg : ∀ (n : ℕ), AEStronglyMeasurable (fun ω ↦ (↑n)⁻¹ • ∑ i ∈ range n, X i ω) μ
⊢ (fun n ω ↦ (↑n)⁻¹ • ∑ i ∈ range n, X i ω) = fun n ↦ (↑n)⁻¹ • ∑ i ∈ range n, X i

Tactic:
]

Goal state after:
case neg
Ω : 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
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
this : IsProbabilityMeasure μ
hmeas : ∀ (i : ℕ), AEStronglyMeasurable (X i) μ
hint : Integrable (X 0) μ
havg : ∀ (n : ℕ), AEStronglyMeasurable (fun ω ↦ (↑n)⁻¹ • ∑ i ∈ range n, X i ω) μ
⊢ UnifIntegrable (fun n ↦ (↑n)⁻¹ • ∑ i ∈ range n, X i) p μ

Ω : 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
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
this : IsProbabilityMeasure μ
hmeas : ∀ (i : ℕ), AEStronglyMeasurable (X i) μ
hint : Integrable (X 0) μ
havg : ∀ (n : ℕ), AEStronglyMeasurable (fun ω ↦ (↑n)⁻¹ • ∑ i ∈ range n, X i ω) μ
⊢ (fun n ω ↦ (↑n)⁻¹ • ∑ i ∈ range n, X i ω) = fun n ↦ (↑n)⁻¹ • ∑ i ∈ range n, X i
Module: Mathlib.RepresentationTheory.Maschke

Goal state before:
pp: k : Type u_1
inst✝¹⁰ : CommRing k
G : Type u_2
inst✝⁹ : Group G
V : Type u_3
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : Module k[G] V
inst✝⁵ : IsScalarTower k k[G] V
W : Type u_4
inst✝⁴ : AddCommGroup W
inst✝³ : Module k W
inst✝² : Module k[G] W
inst✝¹ : IsScalarTower k k[G] W
π : W →ₗ[k] V
i : V →ₗ[k[G]] W
inst✝ : Fintype G
hcard : IsUnit ↑(Nat.card G)
h : ∀ (v : V), π (i v) = v
v : V
⊢ v = v

Tactic:
]

Goal state after:
Module: Mathlib.RepresentationTheory.Maschke

Goal state before:
pp: k : Type u_1
inst✝⁸ : Field k
G : Type u_2
inst✝⁷ : Finite G
inst✝⁶ : NeZero ↑(Nat.card G)
inst✝⁵ : Group G
V : Type u_3
inst✝⁴ : AddCommGroup V
inst✝³ : Module k[G] V
W : Type u_4
inst✝² : AddCommGroup W
inst✝¹ : Module k[G] W
inst✝ : AddGroup G
⊢ NeZero ↑(Nat.card G)

Tactic:
]

Goal state after:
k : Type u_1
inst✝⁸ : Field k
G : Type u_2
inst✝⁷ : Finite G
inst✝⁶ : NeZero ↑(Nat.card G)
inst✝⁵ : Group G
V : Type u_3
inst✝⁴ : AddCommGroup V
inst✝³ : Module k[G] V
W : Type u_4
inst✝² : AddCommGroup W
inst✝¹ : Module k[G] W
inst✝ : AddGroup G
⊢ NeZero ↑(Nat.card G)
Module: Mathlib.RepresentationTheory.Maschke

Goal state before:
pp: k✝ : Type u_1
inst✝¹³ : Field k✝
G✝ : Type u_2
inst✝¹² : Finite G✝
inst✝¹¹ : NeZero ↑(Nat.card G✝)
inst✝¹⁰ : Group G✝
V✝ : Type u_3
inst✝⁹ : AddCommGroup V✝
inst✝⁸ : Module k✝[G✝] V✝
W : Type u_4
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module k✝[G✝] W
G : Type u_5
k : Type u_6
V : Type u_7
inst✝⁵ : Group G
inst✝⁴ : Field k
inst✝³ : Finite G
inst✝² : NeZero ↑(Nat.card G)
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ρ : Representation k G V
⊢ IsSemisimpleModule k[G] ρ.asModule

Tactic:
]

Goal state after:
k✝ : Type u_1
inst✝¹³ : Field k✝
G✝ : Type u_2
inst✝¹² : Finite G✝
inst✝¹¹ : NeZero ↑(Nat.card G✝)
inst✝¹⁰ : Group G✝
V✝ : Type u_3
inst✝⁹ : AddCommGroup V✝
inst✝⁸ : Module k✝[G✝] V✝
W : Type u_4
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module k✝[G✝] W
G : Type u_5
k : Type u_6
V : Type u_7
inst✝⁵ : Group G
inst✝⁴ : Field k
inst✝³ : Finite G
inst✝² : NeZero ↑(Nat.card G)
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ρ : Representation k G V
⊢ IsSemisimpleModule k[G] ρ.asModule
Module: Mathlib.RingTheory.SimpleModule.InjectiveProjective

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : IsSemisimpleRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
X Y : Type u_2
x✝⁴ : AddCommGroup X
x✝³ : AddCommGroup Y
x✝² : Module R X
x✝¹ : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective ⇑f
g : X →ₗ[R] M
h : Y →ₗ[R] M
comp : h ∘ₗ f = g
x✝ : X
⊢ h (f x✝) = h (f x✝)

Tactic:
]

Goal state after:
Module: Mathlib.RepresentationTheory.Continuous.Basic

Goal state before:
pp: R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
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
inst✝³ : AddCommGroup U
inst✝² : Module R U
inst✝¹ : TopologicalSpace U
inst✝ : IsTopologicalAddGroup U
π₁✝ : ContRepresentation R G V
π₂✝ : ContRepresentation R G W
π₃✝ : ContRepresentation R G U
π₁ : ContRepresentation R G V
π₂ : ContRepresentation R G W
π₃ : ContRepresentation R G U
f : π₂ →ⁱL π₃
g : π₁ →ⁱL π₂
h : G
⊢ π₃ h ∘SL f.toContinuousLinearMap ∘SL g.toContinuousLinearMap =
    π₃ h ∘SL f.toContinuousLinearMap ∘SL g.toContinuousLinearMap

Tactic:
]

Goal state after:
Module: Mathlib.RepresentationTheory.Continuous.Basic

Goal state before:
pp: R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
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
inst✝⁸ : AddCommGroup U
inst✝⁷ : Module R U
inst✝⁶ : TopologicalSpace U
inst✝⁵ : IsTopologicalAddGroup U
π₁ : ContRepresentation R G V
π₂ : ContRepresentation R G W
π₃ : ContRepresentation R G U
S : Type u_6
inst✝⁴ : Monoid S
inst✝³ : DistribMulAction S W
inst✝² : SMulCommClass R S W
inst✝¹ : ContinuousConstSMul S W
inst✝ : LinearMap.CompatibleSMul W W S R
s : S
f : π₁ →ⁱL π₂
g : G
⊢ s • π₂ g ∘SL f.toContinuousLinearMap = s • π₂ g ∘SL f.toContinuousLinearMap

Tactic:
]

Goal state after:
Module: Mathlib.RepresentationTheory.Continuous.Basic

Goal state before:
pp: R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
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
inst✝³ : AddCommGroup U
inst✝² : Module R U
inst✝¹ : TopologicalSpace U
inst✝ : IsTopologicalAddGroup U
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
τ : ContRepresentation R G U
φ : ρ.Equiv σ
g : G
⊢ (↑φ.toContinuousLinearEquiv ∘SL ↑φ.symm) ∘SL σ g = (↑φ.toContinuousLinearEquiv ∘SL ρ g) ∘SL ↑φ.symm

Tactic:
]

Goal state after:
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
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
inst✝³ : AddCommGroup U
inst✝² : Module R U
inst✝¹ : TopologicalSpace U
inst✝ : IsTopologicalAddGroup U
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
τ : ContRepresentation R G U
φ : ρ.Equiv σ
g : G
⊢ (↑φ.toContinuousLinearEquiv ∘SL ↑φ.symm) ∘SL σ g = (↑φ.toContinuousLinearEquiv ∘SL ρ g) ∘SL ↑φ.symm
Module: Mathlib.RepresentationTheory.Continuous.Basic

Goal state before:
pp: R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
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
inst✝³ : AddCommGroup U
inst✝² : Module R U
inst✝¹ : TopologicalSpace U
inst✝ : IsTopologicalAddGroup U
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
τ : ContRepresentation R G U
φ✝ φ : ρ.Equiv σ
ψ : σ.Equiv τ
g : G
⊢ τ g ∘SL ↑ψ.toContinuousLinearEquiv ∘SL ↑φ.toContinuousLinearEquiv =
    τ g ∘SL ↑ψ.toContinuousLinearEquiv ∘SL ↑φ.toContinuousLinearEquiv

Tactic:
]

Goal state after:
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
A✝ B✝ C A B : Rep k G
⊢ ofHom (Representation.IntertwiningMap.inl k A.ρ B.ρ) ≫ ofHom (Representation.IntertwiningMap.fst k A.ρ B.ρ) = 𝟙 A

Tactic:
by ext1; simp

Goal state after:
Module: Mathlib.RepresentationTheory.FinGroupCharZero

Goal state before:
pp: k : Type u
inst✝³ : Field k
G : Type u
inst✝² : Finite G
inst✝¹ : Group G
inst✝ : NeZero ↑(Nat.card G)
V : Rep k G
⊢ Module.Injective (MonoidAlgebra k G) ↑(equivalenceModuleMonoidAlgebra.functor.1 V)

Tactic:
]

Goal state after:
k : Type u
inst✝³ : Field k
G : Type u
inst✝² : Finite G
inst✝¹ : Group G
inst✝ : NeZero ↑(Nat.card G)
V : Rep k G
⊢ Module.Injective (MonoidAlgebra k G) ↑(equivalenceModuleMonoidAlgebra.functor.1 V)
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
A✝ B✝ C A B : Rep k G
⊢ ofHom (Representation.IntertwiningMap.inr k A.ρ B.ρ) ≫ ofHom (Representation.IntertwiningMap.snd k A.ρ B.ρ) = 𝟙 B

Tactic:
by ext1; simp

Goal state after:
Module: Mathlib.RepresentationTheory.FinGroupCharZero

Goal state before:
pp: k : Type u
inst✝³ : Field k
G : Type u
inst✝² : Finite G
inst✝¹ : Group G
inst✝ : NeZero ↑(Nat.card G)
V : Rep k G
⊢ Module.Projective (MonoidAlgebra k G) ↑(equivalenceModuleMonoidAlgebra.functor.1 V)

Tactic:
]

Goal state after:
k : Type u
inst✝³ : Field k
G : Type u
inst✝² : Finite G
inst✝¹ : Group G
inst✝ : NeZero ↑(Nat.card G)
V : Rep k G
⊢ Module.Projective (MonoidAlgebra k G) ↑(equivalenceModuleMonoidAlgebra.functor.1 V)
Module: Mathlib.RepresentationTheory.FinGroupCharZero

Goal state before:
pp: case refine_1
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
hf : IsZero W ∧ IsZero V
habs : f = 0
⊢ False

Tactic:
]

Goal state after:
case refine_1
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
hf : IsZero W ∧ IsZero V
habs : f = 0
⊢ False
Module: Mathlib.RepresentationTheory.FinGroupCharZero

Goal state before:
pp: 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
hf : f ≠ 0
this : Epi (Abelian.image.ι f)
⊢ Epi (Abelian.factorThruImage f ≫ Abelian.image.ι f)

Tactic:
]

Goal state after:
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
hf : f ≠ 0
this : Epi (Abelian.image.ι f)
⊢ Epi (Abelian.factorThruImage f ≫ Abelian.image.ι f)
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
hf : Abelian.factorThruImage f ≫ Abelian.image.ι f ≠ 0
⊢ Epi (Abelian.image.ι f)

Tactic:
]

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
hf : Abelian.factorThruImage f ≫ Abelian.image.ι f ≠ 0
⊢ Epi (Abelian.image.ι f)
Module: Mathlib.RepresentationTheory.FinGroupCharZero

Goal state before:
pp: case mpr
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 : ∑ g, V.character g * V.character g⁻¹ = ↑(Nat.card G)
eq : 1 = ↑(Module.finrank k (V ⟶ V))
⊢ Simple V

Tactic:
]

Goal state after:
case mpr
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 : ∑ g, V.character g * V.character g⁻¹ = ↑(Nat.card G)
eq : 1 = ↑(Module.finrank k (V ⟶ V))
⊢ Simple V
Module: Mathlib.RepresentationTheory.FinGroupCharZero

Goal state before:
pp: case mpr
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 : ∑ g, V.character g * V.character g⁻¹ = ↑(Nat.card G)
eq : 1 = ↑(Module.finrank k (V ⟶ V))
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
x✝² x✝¹ x✝ : Rep k G
⊢ x✝² ◁ 0 = 0

Tactic:
by ext1; simp

Goal state after:
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
x✝² x✝¹ x✝ : Rep k G
⊢ 0 ▷ x✝² = 0

Tactic:
by ext1; simp

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

Goal state before:
pp: case succ
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
n : ℕ
ih : X.d n ≫ X.d (n + 1) = 0
⊢ X.d (n + 1) ≫ ofHom (X.resolutionX (n + 1 + 1)).ρ.coind₁ι - X.d (n + 1) ≫ (coind₁Functor k G).map (X.d (n + 1)) = 0

Tactic:
]

Goal state after:
case succ
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
n : ℕ
ih : X.d n ≫ X.d (n + 1) = 0
⊢ X.d (n + 1) ≫ ofHom (X.resolutionX (n + 1 + 1)).ρ.coind₁ι - X.d (n + 1) ≫ (coind₁Functor k G).map (X.d (n + 1)) = 0
Module: Mathlib.RepresentationTheory.Homological.ContCohomology.Basic

Goal state before:
pp: case succ
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
n : ℕ
ih : X.d n ≫ X.d (n + 1) = 0
⊢ X.d (n + 1) ≫ ofHom (X.resolutionX (n + 1 + 1)).ρ.coind₁ι -
      (ofHom (X.resolutionX (n + 1)).ρ.coind₁ι - (coind₁Functor k G).map (X.d n)) ≫
        (coind₁Functor k G).map (X.d (n + 1)) =
    0

Tactic:
]

Goal state after:
case succ
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
n : ℕ
ih : X.d n ≫ X.d (n + 1) = 0
⊢ X.d (n + 1) ≫ ofHom (X.resolutionX (n + 1 + 1)).ρ.coind₁ι -
      (ofHom (X.resolutionX (n + 1)).ρ.coind₁ι - (coind₁Functor k G).map (X.d n)) ≫
        (coind₁Functor k G).map (X.d (n + 1)) =
    0
Module: Mathlib.RepresentationTheory.Homological.ContCohomology.Basic

Goal state before:
pp: case succ
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
n : ℕ
ih : X.d n ≫ X.d (n + 1) = 0
⊢ X.d (n + 1) ≫ ofHom (X.resolutionX (n + 1 + 1)).ρ.coind₁ι =
    ofHom (X.resolutionX (n + 1)).ρ.coind₁ι ≫ (coind₁Functor k G).map (X.d (n + 1))

Tactic:
]

Goal state after:
case succ
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
n : ℕ
ih : X.d n ≫ X.d (n + 1) = 0
⊢ X.d (n + 1) ≫ ofHom (X.resolutionX (n + 1 + 1)).ρ.coind₁ι =
    ofHom (X.resolutionX (n + 1)).ρ.coind₁ι ≫ (coind₁Functor k G).map (X.d (n + 1))
Module: Mathlib.RepresentationTheory.Homological.ContCohomology.Basic

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
i : ℕ
⊢ TopModuleCat.ofHom (Hom.hom (X.resolution'd i)).mapInvariants =
    TopModuleCat.ofHom (Hom.hom (X.resolution'd i)).mapInvariants

Tactic:
]

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

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
i : ℕ
σ : ↑(X.homogeneousCochains.X i).toModuleCat
⊢ ↑((TopModuleCat.Hom.hom ((invariantsFunctor k G).map (X.d (i + 1)))) σ) = (Hom.hom (X.d (i + 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
i : ℕ
σ : ↑(X.homogeneousCochains.X i).toModuleCat
⊢ ↑((TopModuleCat.Hom.hom ((invariantsFunctor k G).map (X.d (i + 1)))) σ) = (Hom.hom (X.d (i + 1))) ↑σ
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
a : ↑A
⊢ (A.ρ ⟨g * g⁻¹, ⋯⟩) a = a

pp: case hc
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
a : ↑A
⊢ (QuotientGroup.rightRel S) g 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
g : G
a : ↑A
⊢ (A.ρ ⟨g * g⁻¹, ⋯⟩) a = a

case hc
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
a : ↑A
⊢ (QuotientGroup.rightRel S) g g
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: case inl
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
a : ↑A
s s₁ : ↥S
⊢ (A.ρ ⟨↑s * s₁ • g * g⁻¹, ⋯⟩) a = (A.ρ s) ((A.ρ ⟨s₁ • g * g⁻¹, ⋯⟩) a)

Tactic:
]

Goal state after:
case inl
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
a : ↑A
s s₁ : ↥S
⊢ (A.ρ ⟨↑s * s₁ • g * g⁻¹, ⋯⟩) a = (A.ρ s) ((A.ρ ⟨s₁ • g * g⁻¹, ⋯⟩) a)
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) (↑s * 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
a : ↑A
s : ↥S
h : ¬(QuotientGroup.rightRel S) g₁ g
⊢ ¬(QuotientGroup.rightRel S) (↑s * g₁) g
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: case inl
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
a : ↑A
s s₁ : ↥S
⊢ (A.ρ (⟨s₁ • g₁ * (↑s * g₁)⁻¹, ⋯⟩ * s)) a = (A.ρ ⟨s₁ • g₁ * g₁⁻¹, ⋯⟩) a

Tactic:
]

Goal state after:
case inl
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
a : ↑A
s s₁ : ↥S
⊢ (A.ρ (⟨s₁ • g₁ * (↑s * g₁)⁻¹, ⋯⟩ * s)) a = (A.ρ ⟨s₁ • g₁ * g₁⁻¹, ⋯⟩) a