mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
⊢ ∑ j ∈ range K, (↑j ^ 2)⁻¹ * ∫ (a : Ω), (truncation X ↑j ^ 2) a ≤ 2 * ∫ (a : Ω), X a

Tactic:
by
  set Y := fun n : ℕ => truncation X n
  let ρ : Measure ℝ := Measure.map X ℙ
  have Y2 : ∀ n, 𝔼[Y n ^ 2] = ∫ x in 0..n, x ^ 2 ∂ρ := by
    intro n
    change 𝔼[fun x => Y n x ^ 2] = _
    rw [moment_truncation_eq_intervalIntegral_of_nonneg hint.1 two_ne_zero hnonneg]
  calc
    ∑ j ∈ range K, ((j : ℝ) ^ 2)⁻¹ * 𝔼[Y j ^ 2] =
        ∑ j ∈ range K, ((j : ℝ) ^ 2)⁻¹ * ∫ x in 0..j, x ^ 2 ∂ρ := by simp_rw [Y2]
    _ = ∑ j ∈ range K, ((j : ℝ) ^ 2)⁻¹ * ∑ k ∈ range j, ∫ x in k..(k + 1 : ℕ), x ^ 2 ∂ρ := by
      congr 1 with j
      congr 1
      rw [intervalIntegral.sum_integral_adjacent_intervals]
      · norm_cast
      intro k _
      exact (continuous_id.pow _).intervalIntegrable _ _
    _ = ∑ k ∈ range K, (∑ j ∈ Ioo k K, ((j : ℝ) ^ 2)⁻¹) * ∫ x in k..(k + 1 : ℕ), x ^ 2 ∂ρ := by
      simp_rw [mul_sum, sum_mul, sum_sigma']
      refine sum_nbij' (fun p ↦ ⟨p.2, p.1⟩) (fun p ↦ ⟨p.2, p.1⟩) ?_ ?_ ?_ ?_ ?_ <;>
        aesop (add unsafe lt_trans)
    _ ≤ ∑ k ∈ range K, 2 / (k + 1 : ℝ) * ∫ x in k..(k + 1 : ℕ), x ^ 2 ∂ρ := by
      gcongr with k
      · refine intervalIntegral.integral_nonneg_of_forall ?_ fun u => sq_nonneg _
        simp
      · apply sum_Ioo_inv_sq_le
    _ ≤ ∑ k ∈ range K, ∫ x in k..(k + 1 : ℕ), 2 * x ∂ρ := by
      gcongr with k
      have Ik : (k : ℝ) ≤ (k + 1 : ℕ) := by simp
      rw [← intervalIntegral.integral_const_mul, intervalIntegral.integral_of_le Ik,
        intervalIntegral.integral_of_le Ik]
      refine setIntegral_mono_on ?_ ?_ measurableSet_Ioc fun x hx => ?_
      · apply Continuous.integrableOn_Ioc (by fun_prop)
      · apply Continuous.integrableOn_Ioc (by fun_prop)
      · calc
          2 / (↑k + 1) * x ^ 2 = x / (k + 1) * (2 * x) := by ring
          _ ≤ 1 * (2 * x) := by
              have : 0 < x := k.cast_nonneg.trans_lt hx.1
              gcongr
              exact (div_le_one <| by positivity).2 <| mod_cast hx.2
          _ = 2 * x := by rw [one_mul]
    _ = 2 * ∫ x in (0 : ℝ)..K, x ∂ρ := by
      rw [intervalIntegral.sum_integral_adjacent_intervals fun k _ => ?_]
      swap; · exact (continuous_const.mul continuous_id').intervalIntegrable _ _
      rw [intervalIntegral.integral_const_mul]
      norm_cast
    _ ≤ 2 * 𝔼[X] := mul_le_mul_of_nonneg_left (by
      rw [← integral_truncation_eq_intervalIntegral_of_nonneg hint.1 hnonneg]
      exact integral_truncation_le_integral_of_nonneg hint hnonneg) zero_le_two

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

Tactic:
ext

Goal state after:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : Semiring 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
φ : ρ.Equiv σ
x✝ : V
⊢ (φ.trans φ.symm) x✝ = (refl ρ) x✝
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✝⁵ : Semiring 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
φ : ρ.Equiv σ
⊢ φ.symm.trans φ = refl σ

Tactic:
ext

Goal state after:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : Semiring 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
φ : ρ.Equiv σ
x✝ : W
⊢ (φ.symm.trans φ) x✝ = (refl σ) x✝
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₂ : ρ.IntertwiningMap σ
⊢ { toFun := ⇑(g₁ + g₂).toLinearMap, map_add' := ⋯, map_smul' := ⋯ } =
    { toFun := ⇑g₁.toLinearMap, map_add' := ⋯, map_smul' := ⋯ } +
      { toFun := ⇑g₂.toLinearMap, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
ext

Goal state after:
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₂ : ρ.IntertwiningMap σ
x✝ : ρ.asModule
⊢ { toFun := ⇑(g₁ + g₂).toLinearMap, map_add' := ⋯, map_smul' := ⋯ } x✝ =
    ({ toFun := ⇑g₁.toLinearMap, map_add' := ⋯, map_smul' := ⋯ } +
        { toFun := ⇑g₂.toLinearMap, map_add' := ⋯, map_smul' := ⋯ })
      x✝
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
t : A
g : ρ.IntertwiningMap σ
⊢ { toFun := ⇑(t • g).toLinearMap, map_add' := ⋯, map_smul' := ⋯ } =
    (RingHom.id A) t • { toFun := ⇑g.toLinearMap, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
ext

Goal state after:
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
t : A
g : ρ.IntertwiningMap σ
x✝ : ρ.asModule
⊢ { toFun := ⇑(t • g).toLinearMap, map_add' := ⋯, map_smul' := ⋯ } x✝ =
    ((RingHom.id A) t • { toFun := ⇑g.toLinearMap, map_add' := ⋯, map_smul' := ⋯ }) x✝
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 : σ.IntertwiningMap τ
x✝¹ x✝ : ρ.IntertwiningMap σ
⊢ LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (f.toLinearMap ∘ₗ (x✝¹ + x✝).toLinearMap) ⋯ =
    LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (f.toLinearMap ∘ₗ x✝¹.toLinearMap) ⋯ +
      LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (f.toLinearMap ∘ₗ x✝.toLinearMap) ⋯

Tactic:
ext

Goal state after:
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 τ
x✝² x✝¹ : ρ.IntertwiningMap σ
x✝ : V
⊢ (LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (f.toLinearMap ∘ₗ (x✝² + x✝¹).toLinearMap) ⋯).toLinearMap x✝ =
    (LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (f.toLinearMap ∘ₗ x✝².toLinearMap) ⋯ +
          LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (f.toLinearMap ∘ₗ x✝¹.toLinearMap) ⋯).toLinearMap
      x✝
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 : σ.IntertwiningMap τ
x✝¹ : A
x✝ : ρ.IntertwiningMap σ
⊢ LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (f.toLinearMap ∘ₗ (x✝¹ • x✝).toLinearMap) ⋯ =
    (RingHom.id A) x✝¹ • LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (f.toLinearMap ∘ₗ x✝.toLinearMap) ⋯

Tactic:
ext

Goal state after:
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 τ
x✝² : A
x✝¹ : ρ.IntertwiningMap σ
x✝ : V
⊢ (LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (f.toLinearMap ∘ₗ (x✝² • x✝¹).toLinearMap) ⋯).toLinearMap x✝ =
    ((RingHom.id A) x✝² •
          LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (f.toLinearMap ∘ₗ x✝¹.toLinearMap) ⋯).toLinearMap
      x✝
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
x✝¹ x✝ : σ.IntertwiningMap τ
⊢ { toFun := fun g ↦ LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ ((x✝¹ + x✝).toLinearMap ∘ₗ g.toLinearMap) ⋯,
      map_add' := ⋯, map_smul' := ⋯ } =
    { toFun := fun g ↦ LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (x✝¹.toLinearMap ∘ₗ g.toLinearMap) ⋯,
        map_add' := ⋯, map_smul' := ⋯ } +
      { toFun := fun g ↦ LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (x✝.toLinearMap ∘ₗ g.toLinearMap) ⋯,
        map_add' := ⋯, map_smul' := ⋯ }

Tactic:
ext

Goal state after:
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
x✝³ x✝² : σ.IntertwiningMap τ
x✝¹ : ρ.IntertwiningMap σ
x✝ : V
⊢ ({ toFun := fun g ↦ LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ ((x✝³ + x✝²).toLinearMap ∘ₗ g.toLinearMap) ⋯,
            map_add' := ⋯, map_smul' := ⋯ }
          x✝¹).toLinearMap
      x✝ =
    (({ toFun := fun g ↦ LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (x✝³.toLinearMap ∘ₗ g.toLinearMap) ⋯,
              map_add' := ⋯, map_smul' := ⋯ } +
            { toFun := fun g ↦ LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (x✝².toLinearMap ∘ₗ g.toLinearMap) ⋯,
              map_add' := ⋯, map_smul' := ⋯ })
          x✝¹).toLinearMap
      x✝
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
x✝¹ : A
x✝ : σ.IntertwiningMap τ
⊢ { toFun := fun g ↦ LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ ((x✝¹ • x✝).toLinearMap ∘ₗ g.toLinearMap) ⋯,
      map_add' := ⋯, map_smul' := ⋯ } =
    (RingHom.id A) x✝¹ •
      { toFun := fun g ↦ LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (x✝.toLinearMap ∘ₗ g.toLinearMap) ⋯,
        map_add' := ⋯, map_smul' := ⋯ }

Tactic:
ext

Goal state after:
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
x✝³ : A
x✝² : σ.IntertwiningMap τ
x✝¹ : ρ.IntertwiningMap σ
x✝ : V
⊢ ({ toFun := fun g ↦ LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ ((x✝³ • x✝²).toLinearMap ∘ₗ g.toLinearMap) ⋯,
            map_add' := ⋯, map_smul' := ⋯ }
          x✝¹).toLinearMap
      x✝ =
    (((RingHom.id A) x✝³ •
            { toFun := fun g ↦ LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (x✝².toLinearMap ∘ₗ g.toLinearMap) ⋯,
              map_add' := ⋯, map_smul' := ⋯ })
          x✝¹).toLinearMap
      x✝
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case e'_7
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst✝¹ : StandardBorelSpace Ω
inst✝ : IsFiniteMeasure μ
Y : Ω → ℝ
cX cY : ℝ≥0
hm : m ≤ mΩ
hX : Kernel.HasSubgaussianMGF X cX (Kernel.const Unit (μ.trim hm)) (Measure.dirac ())
hY : HasCondSubgaussianMGF m hm Y cY μ
hY' : Kernel.HasSubgaussianMGF Y cY (condExpKernel μ m) (⇑(Kernel.const Unit (μ.trim hm)) ∘ₘ Measure.dirac ())
e_3✝ : m.prod mΩ = Prod.instMeasurableSpace
⊢ Kernel.const Unit (Measure.map Function.diag μ) =
    Kernel.const Unit (μ.trim hm) ⊗ₖ Kernel.prodMkLeft Unit (condExpKernel μ m)

Tactic:
ext

Goal state after:
case e'_7
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst✝¹ : StandardBorelSpace Ω
inst✝ : IsFiniteMeasure μ
Y : Ω → ℝ
cX cY : ℝ≥0
hm : m ≤ mΩ
hX : Kernel.HasSubgaussianMGF X cX (Kernel.const Unit (μ.trim hm)) (Measure.dirac ())
hY : HasCondSubgaussianMGF m hm Y cY μ
hY' : Kernel.HasSubgaussianMGF Y cY (condExpKernel μ m) (⇑(Kernel.const Unit (μ.trim hm)) ∘ₘ Measure.dirac ())
e_3✝ : m.prod mΩ = Prod.instMeasurableSpace
a✝ : Unit
⊢ (Kernel.const Unit (Measure.map Function.diag μ)) a✝ =
    (Kernel.const Unit (μ.trim hm) ⊗ₖ Kernel.prodMkLeft Unit (condExpKernel μ m)) a✝
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
a : A
f g : ρ.IntertwiningMap ρ
⊢ f * a • g = a • (f * g)

Tactic:
ext

Goal state after:
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
a : A
f g : ρ.IntertwiningMap ρ
x✝ : V
⊢ (f * a • g).toLinearMap x✝ = (a • (f * g)).toLinearMap x✝
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
⊢ centralAlgebraMul ρ ⋯ = 1

Tactic:
ext

Goal state after:
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
x✝ : V
⊢ (centralAlgebraMul ρ ⋯).toLinearMap x✝ = (toLinearMap 1) x✝
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
x✝¹ x✝ : ↥(Submonoid.center A[G])
⊢ centralAlgebraMul ρ ⋯ = centralAlgebraMul ρ ⋯ * centralAlgebraMul ρ ⋯

Tactic:
ext

Goal state after:
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
x✝² x✝¹ : ↥(Submonoid.center A[G])
x✝ : V
⊢ (centralAlgebraMul ρ ⋯).toLinearMap x✝ = (centralAlgebraMul ρ ⋯ * centralAlgebraMul ρ ⋯).toLinearMap x✝
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
P : Type u_6
inst✝¹ : AddCommMonoid P
inst✝ : Module A P
π : Representation A G P
f : ρ.IntertwiningMap σ
g : τ.IntertwiningMap π
x : G
⊢ TensorProduct.map (σ x ∘ₗ f.toLinearMap) (g.toLinearMap ∘ₗ τ x) =
    (σ.tprod π) x ∘ₗ TensorProduct.map f.toLinearMap g.toLinearMap

Tactic:
g.2,

Goal state after:
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
P : Type u_6
inst✝¹ : AddCommMonoid P
inst✝ : Module A P
π : Representation A G P
f : ρ.IntertwiningMap σ
g : τ.IntertwiningMap π
x : G
⊢ TensorProduct.map (σ x ∘ₗ f.toLinearMap) (π x ∘ₗ g.toLinearMap) =
    (σ.tprod π) x ∘ₗ TensorProduct.map f.toLinearMap g.toLinearMap
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
P : Type u_6
inst✝¹ : AddCommMonoid P
inst✝ : Module A P
π : Representation A G P
f₁ f₂ : ρ.IntertwiningMap σ
g : τ.IntertwiningMap π
⊢ (f₁ + f₂).tensor g = f₁.tensor g + f₂.tensor g

Tactic:
ext

Goal state after:
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
P : Type u_6
inst✝¹ : AddCommMonoid P
inst✝ : Module A P
π : Representation A G P
f₁ f₂ : ρ.IntertwiningMap σ
g : τ.IntertwiningMap π
x✝¹ : V
x✝ : U
⊢ ((TensorProduct.AlgebraTensorModule.curry ((f₁ + f₂).tensor g).toLinearMap) x✝¹) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (f₁.tensor g + f₂.tensor g).toLinearMap) x✝¹) x✝
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
P : Type u_6
inst✝¹ : AddCommMonoid P
inst✝ : Module A P
π : Representation A G P
f : ρ.IntertwiningMap σ
g₁ g₂ : τ.IntertwiningMap π
⊢ f.tensor (g₁ + g₂) = f.tensor g₁ + f.tensor g₂

Tactic:
ext

Goal state after:
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
P : Type u_6
inst✝¹ : AddCommMonoid P
inst✝ : Module A P
π : Representation A G P
f : ρ.IntertwiningMap σ
g₁ g₂ : τ.IntertwiningMap π
x✝¹ : V
x✝ : U
⊢ ((TensorProduct.AlgebraTensorModule.curry (f.tensor (g₁ + g₂)).toLinearMap) x✝¹) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (f.tensor g₁ + f.tensor g₂).toLinearMap) x✝¹) x✝
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
P : Type u_6
inst✝¹ : AddCommMonoid P
inst✝ : Module A P
π : Representation A G P
a : A
f : ρ.IntertwiningMap σ
g : τ.IntertwiningMap π
⊢ (a • f).tensor g = a • f.tensor g

Tactic:
ext

Goal state after:
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
P : Type u_6
inst✝¹ : AddCommMonoid P
inst✝ : Module A P
π : Representation A G P
a : A
f : ρ.IntertwiningMap σ
g : τ.IntertwiningMap π
x✝¹ : V
x✝ : U
⊢ ((TensorProduct.AlgebraTensorModule.curry ((a • f).tensor g).toLinearMap) x✝¹) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (a • f.tensor g).toLinearMap) x✝¹) x✝
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
P : Type u_6
inst✝¹ : AddCommMonoid P
inst✝ : Module A P
π : Representation A G P
f : ρ.IntertwiningMap σ
a : A
g : τ.IntertwiningMap π
⊢ f.tensor (a • g) = a • f.tensor g

Tactic:
ext

Goal state after:
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
P : Type u_6
inst✝¹ : AddCommMonoid P
inst✝ : Module A P
π : Representation A G P
f : ρ.IntertwiningMap σ
a : A
g : τ.IntertwiningMap π
x✝¹ : V
x✝ : U
⊢ ((TensorProduct.AlgebraTensorModule.curry (f.tensor (a • g)).toLinearMap) x✝¹) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (a • f.tensor g).toLinearMap) x✝¹) x✝
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
⊢ lTensor ρ (id σ) = id (ρ.tprod σ)

Tactic:
ext

Goal state after:
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
x✝¹ : V
x✝ : W
⊢ ((TensorProduct.AlgebraTensorModule.curry (lTensor ρ (id σ)).toLinearMap) x✝¹) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (id (ρ.tprod σ)).toLinearMap) x✝¹) x✝