mathlib-initiative/mathlib-tactics huggingface dataset:
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
g : G
⊢ ↑(_root_.TensorProduct.rid A W) ∘ₗ (σ.tprod (trivial A G A)) g = σ g ∘ₗ ↑(_root_.TensorProduct.rid A W)

Tactic:
ext; simp

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
g : G
⊢ ↑(_root_.TensorProduct.lid A W) ∘ₗ ((trivial A G A).tprod σ) g = σ g ∘ₗ ↑(_root_.TensorProduct.lid A W)

Tactic:
ext; simp

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

Goal state before:
pp: k : Type u
inst✝² : Semiring k
G : Type v1
H : Type v2
inst✝¹ : Monoid G
inst✝ : Monoid H
f : H →* G
hf : Function.Surjective ⇑f
X Y : Rep k G
f' : (resFunctor f).obj X ⟶ (resFunctor f).obj Y
⊢ (resFunctor f).map (liftHomOfSurj f hf f') = f'

Tactic:
ext; simp

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)
this :
  ∀ (k : ℕ), ∀ᵐ (ω : Ω), Tendsto (fun n ↦ (∑ i ∈ range ⌊c k ^ n⌋₊, X i ω) / ↑⌊c k ^ n⌋₊) atTop (𝓝 (∫ (a : Ω), X 0 a))
ω : Ω
hω : ∀ (i : ℕ), Tendsto (fun n ↦ (∑ i ∈ range ⌊c i ^ n⌋₊, X i ω) / ↑⌊c i ^ n⌋₊) atTop (𝓝 (∫ (a : Ω), X 0 a))
m n : ℕ
hmn : m ≤ n
⊢ (fun n ↦ ∑ i ∈ range n, X i ω) m ≤ (fun n ↦ ∑ i ∈ range n, X i ω) n

Tactic:
exact sum_le_sum_of_subset_of_nonneg (range_mono hmn) fun i _ _ => hnonneg i ω

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := { toMeasurableSpace := m, volume := μ }
h : ∀ᵐ (ω : Ω), X 0 ω = 0
⊢ ∀ᵐ (ω : Ω), ∀ (i : ℕ), X i ω = 0

Tactic:
rw [ae_all_iff]

Goal state after:
Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := { toMeasurableSpace := m, volume := μ }
h : ∀ᵐ (ω : Ω), X 0 ω = 0
⊢ ∀ (i : ℕ), ∀ᵐ (a : Ω), X i a = 0
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
⊢ (LinearMap.funLeft k B fun x ↦ x * 1).restrict ⋯ = 1

Tactic:
ext; simp

Goal state after:
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 ρ
h : H
⊢ (f.compLeft H).restrict ⋯ ∘ₗ (coind φ σ) h = (coind φ ρ) h ∘ₗ (f.compLeft H).restrict ⋯

Tactic:
ext; simp

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
A B : Rep k G
f : A ⟶ B
h : H
⊢ Linear.rightComp k (res φ (leftRegular k H)) f ∘ₗ (Representation.coind' φ A) h =
    (Representation.coind' φ B) h ∘ₗ Linear.rightComp k (res φ (leftRegular k H)) f

Tactic:
ext; simp

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:
ext; simp

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:
ext; simp

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:
ext; simp

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:
ext; simp

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:
ext; simp

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:
ext; simp

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:
ext; simp

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:
ext; simp

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:
ext; simp

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:
ext; simp

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✝
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
inst✝ : S.Normal
X : Rep k G
⊢ ofHom
      { toLinearMap := ModuleCat.Hom.hom ((coinvariantsFunctor k ↥S).map ((resFunctor S.subtype).map (𝟙 X))),
        isIntertwining' := ⋯ } =
    𝟙 (X.quotientToCoinvariants S)

Tactic:
ext; simp

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) μ μ
h : ∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
⊢ ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), X i ω = 0

Tactic:
rw [ae_all_iff]

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 : ℕ), ∀ᵐ (a : Ω) ∂μ, X i a = 0
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✝
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
inst✝ : S.Normal
X✝ Y✝ Z✝ : Rep k G
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ofHom
      { toLinearMap := ModuleCat.Hom.hom ((coinvariantsFunctor k ↥S).map ((resFunctor S.subtype).map (f ≫ g))),
        isIntertwining' := ⋯ } =
    ofHom
        { toLinearMap := ModuleCat.Hom.hom ((coinvariantsFunctor k ↥S).map ((resFunctor S.subtype).map f)),
          isIntertwining' := ⋯ } ≫
      ofHom
        { toLinearMap := ModuleCat.Hom.hom ((coinvariantsFunctor k ↥S).map ((resFunctor S.subtype).map g)),
          isIntertwining' := ⋯ }

Tactic:
ext; simp

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 : ℕ), X i ω = 0

Tactic:
rw [ae_all_iff]

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.Continuous.Basic

Goal state before:
pp: 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
f g : π₁ →ⁱL π₂
h : f.toContinuousLinearMap = g.toContinuousLinearMap
⊢ f = g

Tactic:
by
  cases f; cases g; congr

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
f : π₂ →ⁱL π₃
g h : π₁ →ⁱL π₂
⊢ f.comp (g + h) = f.comp g + f.comp h

Tactic:
ext; simp

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
f g : π₂ →ⁱL π₃
h : π₁ →ⁱL π₂
⊢ (f + g).comp h = f.comp h + g.comp h

Tactic:
ext; simp

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
f g : π₂ →ⁱL π₃
h : π₁ →ⁱL π₂
⊢ (f - g).comp h = f.comp h - g.comp h

Tactic:
ext; simp

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
f : π₂ →ⁱL π₃
g h : π₁ →ⁱL π₂
⊢ f.comp (g - h) = f.comp g - f.comp h

Tactic:
ext; simp

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_7
inst✝⁴ : Monoid S
inst✝³ : DistribMulAction S U
inst✝² : SMulCommClass R S U
inst✝¹ : ContinuousConstSMul S U
inst✝ : LinearMap.CompatibleSMul U U S R
s : S
f : π₂ →ⁱL π₃
g : π₁ →ⁱL π₂
⊢ (s • f).comp g = s • f.comp g

Tactic:
ext; simp

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_7
inst✝⁹ : Monoid S
inst✝⁸ : DistribMulAction S U
inst✝⁷ : SMulCommClass R S U
inst✝⁶ : ContinuousConstSMul S U
inst✝⁵ : LinearMap.CompatibleSMul U U S R
inst✝⁴ : DistribMulAction S W
inst✝³ : SMulCommClass R S W
inst✝² : ContinuousConstSMul S W
inst✝¹ : LinearMap.CompatibleSMul W W S R
inst✝ : LinearMap.CompatibleSMul W U S R
s : S
f : π₂ →ⁱL π₃
g : π₁ →ⁱL π₂
⊢ f.comp (s • g) = s • f.comp g

Tactic:
ext; simp

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
x✝ : π₁ →ⁱL π₂
⊢ 1 • x✝ = x✝

Tactic:
ext; simp

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
x✝ : S
⊢ x✝ • 0 = 0

Tactic:
ext; simp

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 : Type u_7
inst✝⁴ : Ring S
inst✝³ : Module S W
inst✝² : SMulCommClass R S W
inst✝¹ : ContinuousConstSMul S W
inst✝ : LinearMap.CompatibleSMul W W S R
x✝ : π₁ →ⁱL π₂
⊢ 0 • x✝ = 0

Tactic:
ext; simp

Goal state after:
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
ι : Type u'
f : ι → (A ⟶ B)
s : Finset ι
⊢ Hom.hom (∑ i ∈ s, f i) = ∑ i ∈ s, Hom.hom (f i)

Tactic:
induction s using Finset.induction with
  | empty => simp
  | insert a s ha h => simp [Finset.sum_insert ha, add_hom, h]

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

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Semiring k
inst✝ : Monoid G
A : Rep k G
g1 g2 : G
⊢ A.ρ (g1 * g2) = A.ρ g1 ∘ₗ A.ρ g2

Tactic:
ext; simp

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 : Rep k G
x : ↑A
g : G
⊢ (((Finsupp.lift (↑A) k G) fun g ↦ (A.ρ g) x) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)) ∘ₗ
      (Representation.ofMulAction k G G) g =
    A.ρ g ∘ₗ ((Finsupp.lift (↑A) k G) fun g ↦ (A.ρ g) x) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)

Tactic:
ext; simp

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
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
φ : ρ.Equiv σ
⊢ φ.trans φ.symm = refl ρ

Tactic:
ext; simp

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
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
φ : ρ.Equiv σ
⊢ φ.symm.trans φ = refl σ

Tactic:
ext; simp

Goal state after: