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

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Monoid G
inst✝ : Semiring k
X : Type w
g : G
x : X
⊢ MonoidAlgebra.single ((ConcreteCategory.hom (1 g)) x) 1 = MonoidAlgebra.single x 1

Tactic:
rfl

Goal state after:
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hm : m ≤ mΩ
hXm : Measurable X
hX : HasSubgaussianMGF X c μ
t : ℝ
⊢ mgf X (μ.trim hm) t ≤ rexp (↑c * t ^ 2 / 2)

Tactic:
rw [mgf, ← integral_trim]

Goal state after:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hm : m ≤ mΩ
hXm : Measurable X
hX : HasSubgaussianMGF X c μ
t : ℝ
⊢ ∫ (x : Ω), rexp (t * X x) ∂μ ≤ rexp (↑c * t ^ 2 / 2)

case hf
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hm : m ≤ mΩ
hXm : Measurable X
hX : HasSubgaussianMGF X c μ
t : ℝ
⊢ StronglyMeasurable fun ω ↦ rexp (t * X ω)
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case e_s
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF (fun ω ↦ X ω - ∫ (x : Ω), X x ∂μ) cX μ
hY : HasSubgaussianMGF (fun ω ↦ Y ω - ∫ (x : Ω), Y x ∂μ) cY μ
hindep : X ⟂ᵢ[μ] Y
h_le : ∫ (x : Ω), Y x ∂μ ≤ ∫ (x : Ω), X x ∂μ
ω : Ω
⊢ X ω ≤ Y ω ↔ ∫ (x : Ω), X x ∂μ - ∫ (x : Ω), Y x ∂μ ≤ Y ω - ∫ (x : Ω), Y x ∂μ - (X ω - ∫ (x : Ω), X x ∂μ)

Tactic:
grind

Goal state after:
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case refine_2
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF (fun ω ↦ X ω - ∫ (x : Ω), X x ∂μ) cX μ
hY : HasSubgaussianMGF (fun ω ↦ Y ω - ∫ (x : Ω), Y x ∂μ) cY μ
hindep : X ⟂ᵢ[μ] Y
h_le : ∫ (x : Ω), Y x ∂μ ≤ ∫ (x : Ω), X x ∂μ
⊢ 0 ≤ ∫ (x : Ω), X x ∂μ - ∫ (x : Ω), Y x ∂μ

Tactic:
grind

Goal state after:
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case refine_3.e_a
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF (fun ω ↦ X ω - ∫ (x : Ω), X x ∂μ) cX μ
hY : HasSubgaussianMGF (fun ω ↦ Y ω - ∫ (x : Ω), Y x ∂μ) cY μ
hindep : X ⟂ᵢ[μ] Y
h_le : ∫ (x : Ω), Y x ∂μ ≤ ∫ (x : Ω), X x ∂μ
⊢ -(∫ (x : Ω), X x ∂μ - ∫ (x : Ω), Y x ∂μ) ^ 2 = -(∫ (x : Ω), Y x ∂μ - ∫ (x : Ω), X x ∂μ) ^ 2

Tactic:
grind

Goal state after:
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: case single
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f✝ : V →ₗ[A] W
f : ρ.IntertwiningMap σ
v : ρ.asModule
g : G
a : A
⊢ a • (σ g) (f (ρ.asModuleEquiv v)) = a • (σ g) (σ.asModuleEquiv (f v))

Tactic:
rfl

Goal state after:
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: case zero
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f✝ : V →ₗ[A] W
f : ρ.IntertwiningMap ρ
⊢ (f ^ 0).toLinearMap = f.toLinearMap ^ 0

Tactic:
rfl

Goal state after:
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f✝ : V →ₗ[A] W
f g : ρ.IntertwiningMap ρ
⊢ (equivLinearMapAsModule ρ ρ) (f * g) = (equivLinearMapAsModule ρ ρ) f * (equivLinearMapAsModule ρ ρ) g

Tactic:
rfl

Goal state after:
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring A
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module A V
ρ : Representation A G V
g : G
hg : ∀ (g_1 : G), g_1 * g = g * g_1
g' : G
v : V
⊢ (ρ g) ((ρ g') v) = (ρ g') ((ρ g) v)

Tactic:
rw [← Module.End.mul_apply, ← Module.End.mul_apply, ← ρ.map_mul, ← hg g', ρ.map_mul]

Goal state after:
Module: Mathlib.RepresentationTheory.FDRep

Goal state before:
pp: R : Type u
G : Type v
inst✝¹ : CommRing R
inst✝ : Monoid G
V : FDRep R G
g : G
v : ↑((forget₂ (FDRep R G) (Rep R G)).obj V)
⊢ (((forget₂ (FDRep R G) (Rep R G)).obj V).ρ g) v = (V.ρ g) v

Tactic:
rfl

Goal state after:
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : AddCommMonoid W
inst✝¹ : Module A V
inst✝ : Module A W
ρ : Representation A G V
σ : Representation A G W
⊢ (comm σ ρ).symm = comm ρ σ

Tactic:
rfl

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

Goal state before:
pp: G : Type v1
H : Type v2
inst✝² : Monoid G
inst✝¹ : Monoid H
f : H →* G
k : Type u
inst✝ : CommRing k
S : ShortComplex (Rep k G)
⊢ (S.map (resFunctor f)).Exact ↔ S.Exact

Tactic:
by
  rw [ShortComplex.exact_map_iff_of_faithful]

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

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
V : Rep k G
r : k
x : ↑V
⊢ (RestrictScalars.addEquiv k k[G] V.ρ.asModule).symm ((algebraMap k k[G]) r • V.ρ.asModuleEquiv.symm x) =
    (RingHom.id k) r • unitIsoAddEquiv.toFun x

Tactic:
rfl

Goal state after:
Module: Mathlib.RepresentationTheory.Invariants

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ρ : Representation k G V
v : V
⊢ v ∈ ρ.invariants ↔ ∀ (g : G), (ρ g) v = v

Tactic:
rfl

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hindep : Pairwise ((fun f g ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℕ → ℝ
cone : ∀ (n : ℕ), 1 < c n
clim : Tendsto c atTop (𝓝 1)
⊢ ∀ᵐ (ω : Ω), Tendsto (fun n ↦ (∑ i ∈ range n, X i ω) / ↑n) atTop (𝓝 (∫ (a : Ω), X 0 a))

Tactic:
have : ∀ k, ∀ᵐ ω,
      Tendsto (fun n : ℕ => (∑ i ∈ range ⌊c k ^ n⌋₊, X i ω) / ⌊c k ^ n⌋₊) atTop (𝓝 𝔼[X 0]) :=
    fun k => strong_law_aux6 X hint hindep hident hnonneg (cone k)

Goal state after:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hindep : Pairwise ((fun f g ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℕ → ℝ
cone : ∀ (n : ℕ), 1 < c n
clim : Tendsto c atTop (𝓝 1)
this :
  ∀ (k : ℕ), ∀ᵐ (ω : Ω), Tendsto (fun n ↦ (∑ i ∈ range ⌊c k ^ n⌋₊, X i ω) / ↑⌊c k ^ n⌋₊) atTop (𝓝 (∫ (a : Ω), X 0 a))
⊢ ∀ᵐ (ω : Ω), Tendsto (fun n ↦ (∑ i ∈ range n, X i ω) / ↑n) atTop (𝓝 (∫ (a : Ω), X 0 a))
Module: Mathlib.RepresentationTheory.Character

Goal state before:
pp: case a
k : Type u
inst✝³ : Field k
G : Type v
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Nat.card G)
V W : FDRep k G
| (↑(Nat.card G))⁻¹

pp: case a
k : Type u
inst✝³ : Field k
G : Type v
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Nat.card G)
V W : FDRep k G
| ∑ g, W.character g * V.character g⁻¹

Tactic:
rfl

Goal state after:
case a
k : Type u
inst✝³ : Field k
G : Type v
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Nat.card G)
V W : FDRep k G
| ∑ g, W.character g * V.character g⁻¹
Module: Mathlib.RepresentationTheory.Character

Goal state before:
pp: case a.s
k : Type u
inst✝³ : Field k
G : Type v
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Nat.card G)
V W : FDRep k G
| Finset.univ

pp: case a.f
k : Type u
inst✝³ : Field k
G : Type v
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Nat.card G)
V W : FDRep k G
| fun g ↦ W.character g * V.character g⁻¹

Tactic:
rfl

Goal state after:
case a.f
k : Type u
inst✝³ : Field k
G : Type v
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Nat.card G)
V W : FDRep k G
| fun g ↦ W.character g * V.character g⁻¹
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case e'_5
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : IsProbabilityMeasure μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ✝ φ ψ : SimpleFunc E E
hφ : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, φ (X i ω)) atTop (𝓝 (∫ (x : Ω), (⇑φ ∘ X 0) x ∂μ))
hψ : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, ψ (X i ω)) atTop (𝓝 (∫ (x : Ω), (⇑ψ ∘ X 0) x ∂μ))
ω : Ω
hωφ : Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, φ (X i ω)) atTop (𝓝 (∫ (x : Ω), (⇑φ ∘ X 0) x ∂μ))
hωψ : Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, ψ (X i ω)) atTop (𝓝 (∫ (x : Ω), (⇑ψ ∘ X 0) x ∂μ))
⊢ ∫ (x : Ω), (⇑(φ + ψ) ∘ X 0) x ∂μ = ∫ (a : Ω), (⇑φ ∘ X 0) a + (⇑ψ ∘ X 0) a ∂μ

Tactic:
rfl

Goal state after:
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommRing k
inst✝² : Monoid G
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ρ : Representation k G V
x✝ : V
⊢ (map ρ ρ (IntertwiningMap.id ρ) ∘ₗ mk ρ) x✝ = (LinearMap.id ∘ₗ mk ρ) x✝

Tactic:
rfl

Goal state after:
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
α : Type u_9
x : (ρ.finsupp α).Coinvariants
⊢ (ρ.coinvariantsFinsuppLEquiv α) x = (ρ.coinvariantsToFinsupp α) x

Tactic:
rfl

Goal state after:
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
x : (ρ.tprod (leftRegular k G)).Coinvariants
⊢ ρ.coinvariantsTprodLeftRegularLEquiv x = ρ.ofCoinvariantsTprodLeftRegular x

Tactic:
rfl

Goal state after:
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X : Rep k G
Y : ModuleCat k
f : (coinvariantsFunctor k G).obj X ⟶ Y
⊢ (Hom.hom (((coinvariantsAdjunction k G).homEquiv X Y) f)).toLinearMap =
    ModuleCat.Hom.hom ((coinvariantsMk k G).app X ≫ f)

Tactic:
rfl

Goal state after:
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.{?u.16, u, v} k G
X'✝ X✝ : Rep.{max w t, u, w} k H
Y✝ : Rep.{max w t, u, v} k G
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (coindFunctor k φ).obj Y✝
⊢ (resCoindHomEquiv.{?u.42, u, v, w} φ X'✝ Y✝).toEquiv.symm (f✝ ≫ g✝) =
    (resFunctor φ).map f✝ ≫ (resCoindHomEquiv.{?u.42, u, v, w} φ X✝ Y✝).toEquiv.symm g✝

Tactic:
rfl

Goal state after:
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.{?u.16, u, v} k G
X✝ : Rep.{max w t, u, w} k H
Y✝ Y'✝ : Rep.{max w t, u, v} k G
f✝ : (resFunctor φ).obj X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Y'✝
x✝ : ↑X✝
⊢ (Hom.hom ((resCoindHomEquiv.{t, u, v, w} φ X✝ Y'✝).toEquiv (f✝ ≫ g✝))).toLinearMap x✝ =
    (Hom.hom ((resCoindHomEquiv.{t, u, v, w} φ X✝ Y✝).toEquiv f✝ ≫ (coindFunctor k φ).map g✝)).toLinearMap x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
α : Type u
inst✝ : DecidableEq α
x : (A ⊗ free k G α).ρ.Coinvariants
⊢ (A.coinvariantsTensorFreeToFinsupp α) x = (A.coinvariantsTensorFreeToFinsupp α) x

Tactic:
rfl

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

Goal state before:
pp: k : Type u
G : Type v
X : 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
ρ : ContRepresentation k G X
⊢ ↑(of ρ) = X

Tactic:
rfl

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

Goal state before:
pp: k : Type u
G : Type v
X : 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
ρ : ContRepresentation k G X
⊢ (of ρ).ρ = ρ

Tactic:
rfl

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
X : ℕ → Ω → E
hint : Integrable (X 0) μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))

Tactic:
by_cases h : ∀ᵐ ω ∂μ, X 0 ω = 0
  · have I : ∀ᵐ ω ∂μ, ∀ i, X i ω = 0 := by
      rw [ae_all_iff]
      intro i
      exact (hident i).symm.ae_snd (p := fun x ↦ x = 0) measurableSet_eq h
    filter_upwards [I] with ω hω
    simpa [hω] using (integral_eq_zero_of_ae h).symm
  have : IsProbabilityMeasure μ :=
    hint.isProbabilityMeasure_of_indepFun (X 0) (X 1) h (hindep zero_ne_one)
  -- we reduce to the case of strongly measurable random variables, by using `Y i` which is strongly
  -- measurable and ae equal to `X i`.
  have A : ∀ i, Integrable (X i) μ := fun i ↦ (hident i).integrable_iff.2 hint
  let Y : ℕ → Ω → E := fun i ↦ (A i).1.mk (X i)
  have B : ∀ᵐ ω ∂μ, ∀ n, X n ω = Y n ω :=
    ae_all_iff.2 (fun i ↦ AEStronglyMeasurable.ae_eq_mk (A i).1)
  have Yint : Integrable (Y 0) μ := Integrable.congr hint (AEStronglyMeasurable.ae_eq_mk (A 0).1)
  have C : ∀ᵐ ω ∂μ,
      Tendsto (fun n : ℕ ↦ (n : ℝ)⁻¹ • (∑ i ∈ range n, Y i ω)) atTop (𝓝 μ[Y 0]) := by
    apply strong_law_ae_of_measurable Y Yint ((A 0).1.stronglyMeasurable_mk)
      (fun i j hij ↦ IndepFun.congr (hindep hij) (A i).1.ae_eq_mk (A j).1.ae_eq_mk)
      (fun i ↦ ((A i).1.identDistrib_mk.symm.trans (hident i)).trans (A 0).1.identDistrib_mk)
  filter_upwards [B, C] with ω h₁ h₂
  have : μ[X 0] = μ[Y 0] := integral_congr_ae (AEStronglyMeasurable.ae_eq_mk (A 0).1)
  rw [this]
  apply Tendsto.congr (fun n ↦ ?_) h₂
  congr with i
  exact (h₁ i).symm

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

Goal state before:
pp: k : Type u
G : Type v
inst✝³ : Semiring k
inst✝² : Monoid G
X : Type w
inst✝¹ : AddCommGroup X
inst✝ : Module k X
ρ : Representation k G X
⊢ ↑(of ρ) = X

Tactic:
rfl

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

Goal state before:
pp: k : Type u
G : Type v
inst✝³ : Semiring k
inst✝² : Monoid G
X : Type w
inst✝¹ : AddCommGroup X
inst✝ : Module k X
ρ : Representation k G X
⊢ (of ρ).ρ = ρ

Tactic:
rfl

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 : Rep k G
A : Action (ModuleCat k) G
g : G
⊢ ((RepToAction k G).obj ((ActionToRep k G).obj A)).ρ g ≫ 𝟙 ((RepToAction k G).obj ((ActionToRep k G).obj A)).V =
    𝟙 ((RepToAction k G).obj ((ActionToRep k G).obj A)).V ≫ A.ρ g

Tactic:
rfl

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 : Rep k G
A : Action (ModuleCat k) G
g : G
⊢ A.ρ g ≫ 𝟙 A.V = 𝟙 A.V ≫ ((RepToAction k G).obj ((ActionToRep k G).obj A)).ρ g

Tactic:
rfl

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✝¹ : 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
⊢ 0 < Module.finrank k (V ⟶ V)

Tactic:
grind

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 Y Z : Rep k G
x : ↑X
y : ↑Y
z : ↑Z
⊢ (Hom.hom (α_ X Y Z).hom).toLinearMap (x ⊗ₜ[k] y ⊗ₜ[k] z) = (↑(assoc X.ρ Y.ρ Z.ρ)).toLinearMap (x ⊗ₜ[k] y ⊗ₜ[k] z)

Tactic:
rfl

Goal state after:
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
x✝² : Rep k G
x✝¹ : ↑(of (A.ρ.linHom x✝².ρ))
x✝ : ↑A
⊢ ((Hom.hom
            (ofHom
              { toLinearMap := (LinearMap.llcomp k ↑A ↑x✝² ↑x✝²) (Hom.hom (𝟙 x✝²)).toLinearMap,
                isIntertwining' := ⋯ })).toLinearMap
        x✝¹)
      x✝ =
    ((Hom.hom (𝟙 (of (A.ρ.linHom x✝².ρ)))).toLinearMap x✝¹) x✝

Tactic:
rfl

Goal state after:
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
X✝ Y✝ Z✝ : Rep k G
x✝³ : X✝ ⟶ Y✝
x✝² : Y✝ ⟶ Z✝
x✝¹ : ↑(of (A.ρ.linHom X✝.ρ))
x✝ : ↑A
⊢ ((Hom.hom
            (ofHom
              { toLinearMap := (LinearMap.llcomp k ↑A ↑X✝ ↑Z✝) (Hom.hom (x✝³ ≫ x✝²)).toLinearMap,
                isIntertwining' := ⋯ })).toLinearMap
        x✝¹)
      x✝ =
    ((Hom.hom
            (ofHom { toLinearMap := (LinearMap.llcomp k ↑A ↑X✝ ↑Y✝) (Hom.hom x✝³).toLinearMap, isIntertwining' := ⋯ } ≫
              ofHom
                { toLinearMap := (LinearMap.llcomp k ↑A ↑Y✝ ↑Z✝) (Hom.hom x✝²).toLinearMap,
                  isIntertwining' := ⋯ })).toLinearMap
        x✝¹)
      x✝

Tactic:
rfl

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

Goal state before:
pp: k : Type u
inst✝¹ : CommRing k
G : Type v
inst✝ : Group G
A B : Rep k G
x✝ : ↑((ihom A ⋙ tensorLeft A).obj B)
⊢ (Hom.hom ((ihom.ev A).app B)).toLinearMap x✝ =
    ((TensorProduct.uncurry (RingHom.id k) (↑A) (↑A →ₗ[k] ↑B) ↑B) LinearMap.id.flip) x✝

Tactic:
rfl

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

Goal state before:
pp: k : Type u
inst✝¹ : CommRing k
G : Type v
inst✝ : Group G
A B C : Rep k G
f : B ⟶ (ihom A).obj C
⊢ (Hom.hom
        ({ toFun := ⇑(A.tensorHomEquiv B C), map_add' := ⋯, map_smul' := ⋯, invFun := ⇑(A.tensorHomEquiv B C).symm,
              left_inv := ⋯, right_inv := ⋯ }.symm
          f)).toLinearMap =
    (TensorProduct.uncurry (RingHom.id k) ↑A ↑B ↑C) (Hom.hom f).flip

Tactic:
rfl

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

Goal state before:
pp: case zero
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.d 0 ≫ X.d (0 + 1) = 0

Tactic:
ext
    simp [d_succ, ContIntertwiningMap.toContinuousLinearMap_apply, d_zero, hom_sub]

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₁ι =
    ofHom (X.resolutionX (n + 1)).ρ.coind₁ι ≫ (coind₁Functor k G).map (X.d (n + 1))

Tactic:
rfl

Goal state after:
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
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:
rfl

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

Goal state before:
pp: case zero
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
⊢ resolutionMap (ContinuousMonoidHom.id G) (𝟙 X) 0 = 𝟙 (X.resolutionX 0)

Tactic:
rfl

Goal state after:
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)
F : ↑(of ((X.resolutionX i).ρ.coind₁.restrict ↑(ContinuousMonoidHom.id G)))
x : G
⊢ ((Hom.hom (ofHom (coind₁ResMap (ContinuousMonoidHom.id G) (Hom.hom (𝟙 (X.resolutionX i)))))).toContinuousLinearMap F)
      x =
    ((Hom.hom (𝟙 (X.resolutionX (i + 1)))).toContinuousLinearMap F) x

Tactic:
rfl

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

Goal state before:
pp: case zero
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
⊢ resolutionMap (φ.comp ψ) ((resFunctor ↑ψ).map f ≫ g) 0 =
    (resFunctor ↑ψ).map (resolutionMap φ f 0) ≫ resolutionMap ψ g 0

Tactic:
rfl

Goal state after:
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
F : ↑(of ((X.resolutionX i).ρ.coind₁.restrict ↑(φ.comp ψ)))
x : K
⊢ ((Hom.hom
            (ofHom
              (coind₁ResMap (φ.comp ψ)
                (Hom.hom ((resFunctor ↑ψ).map (resolutionMap φ f i) ≫ resolutionMap ψ g i))))).toContinuousLinearMap
        F)
      x =
    ((Hom.hom
            ((resFunctor ↑ψ).map (ofHom (coind₁ResMap φ (Hom.hom (resolutionMap φ f i)))) ≫
              ofHom (coind₁ResMap ψ (Hom.hom (resolutionMap ψ g i))))).toContinuousLinearMap
        F)
      x

Tactic:
rfl

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

Goal state before:
pp: case zero
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
⊢ resolutionMap φ f 0 ≫ Y.d 0 = (resFunctor ↑φ).map (X.d 0) ≫ resolutionMap φ f (0 + 1)

Tactic:
rfl

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 : ℕ
v : ↑(X.resolution'X i).invariants.toModuleCat
a✝ : G
⊢ ↑((ConcreteCategory.hom (invariantsResMap (↑(ContinuousMonoidHom.id G)) (𝟙 (X.resolutionX (i + 1))))) v) a✝ =
    ↑((ConcreteCategory.hom ((𝟙 X.homogeneousCochains).f i)) v) a✝

Tactic:
rfl

Goal state after: