mathlib-initiative/mathlib-tactics huggingface dataset:
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:
by

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 k G
f : res φ (leftRegular k H) ⟶ A
g : G
h : H
⊢ ?m.240

Tactic:
by

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
⊢ map ρ ρ (IntertwiningMap.id ρ) = LinearMap.id

Tactic:
by

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
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✝¹
⊢ ((MonoidHom.comp ρ S.subtype) ⟨g * ↑s * g⁻¹, ⋯⟩) ((ρ g) x) - (ρ g) x = (ρ g) ((ρ ↑s) x) - (ρ g) x

Tactic:
by

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 k G
f : res φ (leftRegular k H) ⟶ A
g : G
h : H
⊢ (fun h ↦ (Hom.hom f).toLinearMap (MonoidAlgebra.single h 1)) (φ g * h) =
    (A.ρ g) ((fun h ↦ (Hom.hom f).toLinearMap (MonoidAlgebra.single h 1)) h)

Tactic:
by

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 k G
x : ↥(Representation.coindV φ A.ρ)
⊢ (fun f ↦ ⟨fun h ↦ (Hom.hom f).toLinearMap (MonoidAlgebra.single h 1), ⋯⟩)
      ((fun f ↦
          ofHom { toLinearMap := linearCombination k ↑f ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k), isIntertwining' := ⋯ })
        x) =
    x

Tactic:
by

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
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:
by

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 k G
x : res φ (leftRegular k H) ⟶ A
x✝ : H
⊢ (Hom.hom
          ((fun f ↦
              ofHom
                { toLinearMap := linearCombination k ↑f ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k), isIntertwining' := ⋯ })
            ((fun f ↦ ⟨fun h ↦ (Hom.hom f).toLinearMap (MonoidAlgebra.single h 1), ⋯⟩) x))).toLinearMap
      (MonoidAlgebra.single x✝ 1) =
    (Hom.hom x).toLinearMap (MonoidAlgebra.single x✝ 1)

Tactic:
by

Goal state after:
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
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 : ↥S
⊢ (MonoidHom.comp (ρ.toCoinvariants S) S.subtype) g = LinearMap.id

Tactic:
by

Goal state after:
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
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✝ : G
⊢ mapRange.linearMap (Coinvariants.mk ρ) ∘ₗ (ρ.finsupp α) x✝ = mapRange.linearMap (Coinvariants.mk ρ)

Tactic:
by

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 : α
a : V
⊢ (ρ.coinvariantsToFinsupp α) ((Coinvariants.mk (ρ.finsupp α)) (single x a)) = single x ((Coinvariants.mk ρ) a)

Tactic:
by

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 k G
h : H
⊢ ↑(coindVEquiv φ A) ∘ₗ (Representation.coind φ A.ρ) h = (Representation.coind' φ A) h ∘ₗ ↑(coindVEquiv φ A)

Tactic:
by

Goal state after:
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
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
a : α
g : G
x : V
⊢ ((ρ.finsupp α) g) (single a x) - single a x = (lsingle a) ((ρ g) x) - (lsingle a) x

Tactic:
by

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
a : α
x : V
⊢ (ρ.finsuppToCoinvariants α) (single a ((Coinvariants.mk ρ) x)) = (Coinvariants.mk (ρ.finsupp α)) (single a x)

Tactic:
by

Goal state after:
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
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
⊢ ρ.coinvariantsToFinsupp α ∘ₗ ρ.finsuppToCoinvariants α = LinearMap.id

Tactic:
by

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 k G
X✝ Y✝ : Rep k G
x✝² : X✝ ⟶ Y✝
x✝¹ : ↑((coindFunctor k φ).obj X✝)
x✝ : H
⊢ (Hom.hom ((Hom.hom ((coindFunctor k φ).map x✝² ≫ (coindIso φ Y✝).hom)).toLinearMap x✝¹)).toLinearMap
      (MonoidAlgebra.single x✝ 1) =
    (Hom.hom ((Hom.hom ((coindIso φ X✝).hom ≫ (coindFunctor' k φ).map x✝²)).toLinearMap x✝¹)).toLinearMap
      (MonoidAlgebra.single x✝ 1)

Tactic:
by

Goal state after:
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
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
⊢ ρ.finsuppToCoinvariants α ∘ₗ ρ.coinvariantsToFinsupp α = LinearMap.id

Tactic:
by

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:
by

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 k G
X✝ Y✝ : Rep k G
x✝ : X✝ ⟶ Y✝
⊢ (coindFunctor k φ).map x✝ ≫ (coindIso φ Y✝).hom = (coindIso φ X✝).hom ≫ (coindFunctor' k φ).map x✝

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k : Type u_6
G : Type u_7
V : Type u_8
W : Type u_9
inst✝⁵ : CommRing k
inst✝⁴ : Group G
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AddCommGroup W
inst✝ : Module k W
ρ : Representation k G V
τ : Representation k G W
x : V
y : W
g : G
⊢ ((ρ.tprod τ) g⁻¹) (x ⊗ₜ[k] (τ g) y) - x ⊗ₜ[k] (τ g) y = (ρ g⁻¹) x ⊗ₜ[k] y - x ⊗ₜ[k] (τ g) y

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k : Type u_6
G : Type u_7
V : Type u_8
W : Type u_9
inst✝⁵ : CommRing k
inst✝⁴ : Group G
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AddCommGroup W
inst✝ : Module k W
ρ : Representation k G V
τ : Representation k G W
x : V
y : W
g : G
⊢ ((ρ.tprod τ) g⁻¹) ((ρ g) x ⊗ₜ[k] y) - (ρ g) x ⊗ₜ[k] y = x ⊗ₜ[k] (τ g⁻¹) y - (ρ g) x ⊗ₜ[k] y

Tactic:
by

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 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:
by

Goal state after:
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
k : Type u_6
G : Type u_7
V : Type u_8
W : Type u_9
inst✝⁵ : CommRing k
inst✝⁴ : Group G
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AddCommGroup W
inst✝ : Module k W
ρ : Representation k G V
τ : Representation k G W
x✝ : G
⊢ (TensorProduct.lift ((linearCombination k fun g ↦ ρ g⁻¹) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)) ∘ₗ
        ↑(_root_.TensorProduct.comm k V k[G])) ∘ₗ
      (ρ.tprod (leftRegular k G)) x✝ =
    TensorProduct.lift ((linearCombination k fun g ↦ ρ g⁻¹) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)) ∘ₗ
      ↑(_root_.TensorProduct.comm k V k[G])

Tactic:
by

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁵ : IsProbabilityMeasure μ
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) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
zero_s : 0 ∈ s
this✝¹ : SeparableSpace ↑s
this✝ : Nonempty ↑s
φ : ℕ → SimpleFunc E E := SimpleFunc.nearestPt fun k ↦ Nat.casesOn k 0 (Subtype.val ∘ denseSeq ↑s)
Y : ℕ → ℕ → Ω → E := fun k i ↦ ⇑(φ k) ∘ X i
A : ∀ᵐ (ω : Ω) ∂μ, ∀ (k : ℕ), Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
B :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto (fun n ↦ (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop
        (𝓝 (∫ (x : Ω), (fun ω ↦ ‖(X 0 - Y k 0) ω‖) x ∂μ))
ω : Ω
hω : ∀ (k : ℕ), Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
h'ω :
  ∀ (k : ℕ),
    Tendsto (fun n ↦ (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop (𝓝 (∫ (x : Ω), ‖(X 0 - Y k 0) x‖ ∂μ))
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : δ + δ + δ < ε
k : ℕ
hk : ∫ (ω : Ω), ‖(X 0 - Y k 0) ω‖ ∂μ < δ
this : ‖∫ (x : Ω), Y k 0 x ∂μ - ∫ (x : Ω), X 0 x ∂μ‖ < δ
I : ∀ᶠ (n : ℕ) in atTop, (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n < δ
J : ∀ᶠ (n : ℕ) in atTop, ‖(↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω - ∫ (x : Ω), Y k 0 x ∂μ‖ < δ
n : ℕ
hn : (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n < δ
h'n : ‖(↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω - ∫ (x : Ω), Y k 0 x ∂μ‖ < δ
⊢ ‖(↑n)⁻¹ • ∑ i ∈ Finset.range n, (X i ω - Y k i ω)‖ +
        ‖(↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω - ∫ (x : Ω), Y k 0 x ∂μ‖ +
      ‖∫ (x : Ω), Y k 0 x ∂μ - ∫ (x : Ω), X 0 x ∂μ‖ ≤
    (∑ i ∈ Finset.range n, ‖X i ω - Y k i ω‖) / ↑n + δ + δ

Tactic:
by

Goal state after:
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
k : Type u_6
G : Type u_7
V : Type u_8
W : Type u_9
inst✝⁵ : CommRing k
inst✝⁴ : Group G
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AddCommGroup W
inst✝ : Module k W
ρ : Representation k G V
τ : Representation k G W
⊢ ρ.ofCoinvariantsTprodLeftRegular ∘ₗ
      Coinvariants.mk (ρ.tprod (leftRegular k G)) ∘ₗ (TensorProduct.mk k V k[G]).flip (MonoidAlgebra.single 1 1) =
    LinearMap.id

Tactic:
by

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 k G
B : Rep k H
A : Rep k G
f : res φ B ⟶ A
g : H
⊢ LinearMap.codRestrict (Representation.coindV φ A.ρ) (LinearMap.pi fun h ↦ (Hom.hom f).toLinearMap ∘ₗ B.ρ h) ⋯ ∘ₗ
      B.ρ g =
    (Representation.coind φ A.ρ) g ∘ₗ
      LinearMap.codRestrict (Representation.coindV φ A.ρ) (LinearMap.pi fun h ↦ (Hom.hom f).toLinearMap ∘ₗ B.ρ h) ⋯

Tactic:
by

Goal state after:
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
k : Type u_6
G : Type u_7
V : Type u_8
W : Type u_9
inst✝⁵ : CommRing k
inst✝⁴ : Group G
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AddCommGroup W
inst✝ : Module k W
ρ : Representation k G V
τ : Representation k G W
⊢ (Coinvariants.mk (ρ.tprod (leftRegular k G)) ∘ₗ (TensorProduct.mk k V k[G]).flip (MonoidAlgebra.single 1 1)) ∘ₗ
      ρ.ofCoinvariantsTprodLeftRegular =
    LinearMap.id

Tactic:
by

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:
by

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case h₁
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁵ : IsProbabilityMeasure μ
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) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := ⋯
zero_s : 0 ∈ s
this✝¹ : SeparableSpace ↑s
this✝ : Nonempty ↑s
φ : ℕ → SimpleFunc E E := ⋯
Y : ℕ → ℕ → Ω → E := ⋯
A : ∀ᵐ (ω : Ω) ∂μ, ∀ (k : ℕ), Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
B :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto (fun n ↦ (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop
        (𝓝 (∫ (x : Ω), (fun ω ↦ ‖(X 0 - Y k 0) ω‖) x ∂μ))
ω : Ω
hω : ∀ (k : ℕ), Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
h'ω :
  ∀ (k : ℕ),
    Tendsto (fun n ↦ (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop (𝓝 (∫ (x : Ω), ‖(X 0 - Y k 0) x‖ ∂μ))
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : δ + δ + δ < ε
k : ℕ
hk : ∫ (ω : Ω), ‖(X 0 - Y k 0) ω‖ ∂μ < δ
this : ‖∫ (x : Ω), Y k 0 x ∂μ - ∫ (x : Ω), X 0 x ∂μ‖ < δ
I : ∀ᶠ (n : ℕ) in atTop, (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n < δ
J : ∀ᶠ (n : ℕ) in atTop, ‖(↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω - ∫ (x : Ω), Y k 0 x ∂μ‖ < δ
n : ℕ
hn : (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n < δ
h'n : ‖(↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω - ∫ (x : Ω), Y k 0 x ∂μ‖ < δ
⊢ (∑ i ∈ Finset.range n, ‖X i ω - Y k i ω‖) / ↑n ≤ δ

Tactic:
exact hn.le

Goal state after:
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
g : G
⊢ (Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)).subtype ∘ₗ (A.ρ.toCoinvariantsKer S) g =
    A.ρ g ∘ₗ (Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)).subtype

Tactic:
by

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
B : Rep.{max w t, u, w} k H
A : Rep.{max w t, u, v} k G
f : B ⟶ coind.{u, v, w, max t w} φ A
g : G
⊢ (LinearMap.proj 1 ∘ₗ (Representation.coindV φ A.ρ).subtype ∘ₗ (Hom.hom f).toLinearMap) ∘ₗ (MonoidHom.comp B.ρ φ) g =
    A.ρ g ∘ₗ LinearMap.proj 1 ∘ₗ (Representation.coindV φ A.ρ).subtype ∘ₗ (Hom.hom f).toLinearMap

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
⊢ ofHom { toLinearMap := (Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)).subtype, isIntertwining' := ⋯ } ≫
      A.toCoinvariantsMkQ S =
    0

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
A B x✝ : Rep k G
⊢ ModuleCat.ofHom (Coinvariants.map x✝.ρ x✝.ρ (Hom.hom (𝟙 x✝))) = 𝟙 (ModuleCat.of k x✝.ρ.Coinvariants)

Tactic:
by

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
B : Rep.{max w t, u, w} k H
A : Rep.{max w t, u, v} k G
x : res φ B ⟶ A
⊢ (fun f ↦
        ofHom
          { toLinearMap := LinearMap.proj 1 ∘ₗ (Representation.coindV φ A.ρ).subtype ∘ₗ (Hom.hom f).toLinearMap,
            isIntertwining' := ⋯ })
      ((fun f ↦ resCoindToHom φ B A f) x) =
    x

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
A B X✝ Y✝ Z✝ : Rep k G
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ ModuleCat.ofHom (Coinvariants.map X✝.ρ Z✝.ρ (Hom.hom (x✝¹ ≫ x✝))) =
    ModuleCat.ofHom (Coinvariants.map X✝.ρ Y✝.ρ (Hom.hom x✝¹)) ≫
      ModuleCat.ofHom (Coinvariants.map Y✝.ρ Z✝.ρ (Hom.hom x✝))

Tactic:
by

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁵ : IsProbabilityMeasure μ
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) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
zero_s : 0 ∈ s
this✝¹ : SeparableSpace ↑s
this✝ : Nonempty ↑s
φ : ℕ → SimpleFunc E E := SimpleFunc.nearestPt fun k ↦ Nat.casesOn k 0 (Subtype.val ∘ denseSeq ↑s)
Y : ℕ → ℕ → Ω → E := fun k i ↦ ⇑(φ k) ∘ X i
A : ∀ᵐ (ω : Ω) ∂μ, ∀ (k : ℕ), Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
B :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto (fun n ↦ (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop
        (𝓝 (∫ (x : Ω), (fun ω ↦ ‖(X 0 - Y k 0) ω‖) x ∂μ))
ω : Ω
hω : ∀ (k : ℕ), Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
h'ω :
  ∀ (k : ℕ),
    Tendsto (fun n ↦ (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop (𝓝 (∫ (x : Ω), ‖(X 0 - Y k 0) x‖ ∂μ))
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : δ + δ + δ < ε
k : ℕ
hk : ∫ (ω : Ω), ‖(X 0 - Y k 0) ω‖ ∂μ < δ
this : ‖∫ (x : Ω), Y k 0 x ∂μ - ∫ (x : Ω), X 0 x ∂μ‖ < δ
I : ∀ᶠ (n : ℕ) in atTop, (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n < δ
J : ∀ᶠ (n : ℕ) in atTop, ‖(↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω - ∫ (x : Ω), Y k 0 x ∂μ‖ < δ
n : ℕ
hn : (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n < δ
h'n : ‖(↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω - ∫ (x : Ω), Y k 0 x ∂μ‖ < δ
⊢ (∑ i ∈ Finset.range n, ‖X i ω - Y k i ω‖) / ↑n + δ + δ ≤ δ + δ + δ

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Monoid G
A B : Rep k G
inst✝ : B.ρ.IsTrivial
f : A ⟶ B
⊢ ∀ (x : G), (Hom.hom f).toLinearMap ∘ₗ A.ρ x = (Hom.hom f).toLinearMap

Tactic:
by

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
B : Rep.{max w t, u, w} k H
A : Rep.{max w t, u, v} k G
z : B ⟶ coind.{u, v, w, max t w} φ A
⊢ (fun f ↦ resCoindToHom φ B A f)
      ((fun f ↦
          ofHom
            { toLinearMap := LinearMap.proj 1 ∘ₗ (Representation.coindV φ A.ρ).subtype ∘ₗ (Hom.hom f).toLinearMap,
              isIntertwining' := ⋯ })
        z) =
    z

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
A B X : Rep k G
g : G
⊢ ModuleCat.Hom.hom ((coinvariantsMk k G).app X) ∘ₗ X.ρ g =
    (Representation.trivial k G ↑((coinvariantsFunctor k G).obj X)) g ∘ₗ ModuleCat.Hom.hom ((coinvariantsMk k G).app X)

Tactic:
by

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:
by

Goal state after: